Full paper: Postscript, PS.GZ, PDF

Introduction

As the Internet and electronic commerce prospers, new applications emerge rapidly and require that new security protocols and systems are designed and deployed quickly. Unfortunately, numerous examples show that security protocols are difficult to design, to verify the correctness, and particularly hard to implement correctly:

• Different security protocols even with the same security properties vary in many system aspects such as computation overhead, communication overhead and battery power consumption. Therefore it is important to design optimal security protocols that suit specific applications. Unfortunately the current process of designing a security protocol is usually ad-hoc and involves little formalism and mechanical assistance. Such a design process is not only slow and error prone but also often miss the optimal protocols for specific applications.
• Experience shows that security protocols are often flawed even when they are designed with care. To guarantee the correctness of security protocols, we need formal and rigorous analysis of the protocols, especially automatic protocol verifiers.
• Software is notoriously flawed. Even if the design of the security protocol is correct, various implementation bugs introduced by programmers could still easily break the security of the system.

To solve these problems, we designed and implemented the AGVI toolkit which stands for Automatic Generation, Verification, and Implementation of Security Protocols. With AGVI, the protocol designer specifies the desired security requirements, such as authentication and secrecy, and system specification, e.g., symmetric or asymmetric encryption/decryption, low bandwidth. A protocol generator then generates candidate security protocols which satisfy the system requirements using an intelligent exhaustive search in a combinatorial protocol space. Then a protocol screener analyzes the candidate protocols, discards the flawed protocols, and outputs the correct protocols that satisfy the desired security properties. In the final step, a code generator automatically outputs a Java implementation from the formal specification of the generated security protocols.

Even a simple security protocol can have an enormous protocol space (for example, for a four-round authentication protocol, even after constraining message format and sending order, we estimate that there are at least $1012$ possible variation protocols that one would need to consider to find an optimal one for the specific application!). Facing this challenge, we have developed powerful reduction techniques for the protocol generator to weed out obviously flawed protocols. Because the protocol generator uses simple criteria to rule out obviously flawed protocols, it is fast and can analyze $10,000$ protocols per second. Protocols that were not found flawed by the protocol generator are then send to the protocol screener which can prove whether the protocol is correct or not. Our protocol screener has the ability to analyze protocol executions with any arbitrary protocol configuration. When it terminates, it either provides a proof that a protocol satisfies its specified property under any arbitrary protocol configuration if it is the case, or it generates a counterexample if the property does not hold. It also exploits many state space reduction techniques to achieve high efficiency. On average, our protocol screener can check 5 to 10 synthesized protocols per second (measured on a 500 MHz Pentium III workstation running Linux).

We have successfully experimented with AGVIin several applications. We have found new protocols for authentication and key distribution protocols using AGVIand some of them are even simpler than the standard protocols documented in the literature such as ISO standards [Int93]. Details about the experiments and techniques in the tool can be found in [PS00a, PS00b].