Introduction

The exponential growth of the Internet and electronic commerce brings not only prosperity, but also vulnerability. Numerous attacks pose a real challenge to different aspects of security mechanisms. Among these security mechanisms, security protocols play an essential role. They use cryptographic primitives as building blocks to achieve security goals such as authentication, confidentiality, and integrity. New applications and systems eagerly demand security protocols suitable to their system requirements. Unfortunately, designing security protocols is a delicate task and experience shows that security protocols are notoriously hard to get right [BAN89, Low96]. This naturally raises the question whether the current security protocol design process is satisfactory. If the answer is no, how can we improve it?

The current process of finding a solution is usually ad-hoc and involves little formalism, and almost no mechanical assistance. Such a design process is not satisfactory for the following reasons:

• Error-prone. Security protocols are intricate and attackers are powerful.
  • If the designer has limited experience, it is likely that the security protocol is flawed. Evidence shows that even when security protocols are designed with care and examined intensely (even over time of years), they can still be fundamentally flawed.
  • Due to the lack of formalism and mechanical assistance, manually designed protocols often suffer from the fact that they contain undocumented assumptions. Since the implementation might not respect these assumptions the resulting protocols might be insecure/flawed.
  • Without proofs, these protocols cannot give any guarantee on satisfying the desired security properties, and hence degrade the level of confidence.
• Non-optimal. Such designed protocols may contain unnecessary operations. Simply because the designer cannot search a large number of candidates, she may not find the optimal protocol for the given system requirements. Moreover, conservative designers might put unnecessary operations just to play safe.
• Inefficient and Expensive. The current design process is often slow. It can be a serious bottleneck of the project and severely delay product development. If the protocol is flawed, high costs might incur, due to forced redesign, update plans, or liability claims.

In this paper, we present automatic protocol generation, APG for short, a mechanism which addresses these shortcomings. With automatic protocol generation, the protocol designer specifies the desired security properties, such as authentication and secrecy, and system requirements, i.e., symmetric or asymmetric encryption/decryption, low bandwidth. A protocol generator then generates candidate security protocols which satisfy the system requirements. In the final step, a protocol screener analyzes the candidate protocols, discards the flawed protocols, and outputs the correct protocols that satisfy the desired security properties.

Our approach provides several advantages:

• Automatic. The protocol designer specifies the security properties and the system requirements. The remaining process is fully automatic.
• High Confidence. Since the input specifications are written in a well-defined specification language and the automatic protocol generation is fully mechanical, there are no hidden assumptions, in contrast to the manual design process. The protocol screener has a powerful engine which can automatically generate a proof if a protocol is correct, or a counterexample otherwise.
• High Quality. The user-defined system requirements includes a metric function which specifies the cost or overhead of a protocol. APG tries to generate correct protocols with minimal cost with respect to the metric function hence suits the system requirements the best.
• Flexible. The approach works for different security properties, system requirements, and attacker models.

The remainder of this paper is organized as follows. We begin with an overview of the general framework and requirements of APG. Next, we present a case study of automatic generation of authentication protocols. In our case study, we show how we deal with the arising difficulties to make APG feasible. Following the case study, we discuss some of the limitations of APG, as well as the insights and results of the case study and the interesting directions for further research. Finally, we summarize the contributions of this paper.