The Diffie-Hellman key exchange scheme is a standard component of cryptographic protocols. In this paper, we propose a way in which protocols that use this computational primitive can be verified using formal methods. In particular, we separate the computational aspects of such an analysis from the formal aspects. First, we use Strand Space terminology to define a security condition that summarizes the security guarantees of Diffie-Hellman. Once this property is assumed, the analysis of a protocol is a purely formal enterprise. (We demonstrate the applicability and usefulness of this property by analyzing a sample protocol.) Furthermore, we show that this property is sound in the computational setting by mapping formal attacks to computational algorithms. We demonstrate that if there exists a formal attack that violates the formal security condition, then it maps to a computational algorithm that solves the Diffie-Hellman problem. Hence, if the Diffie-Hellman problem is hard, the security condition holds globally.

Strand space analysis is a method for stating and proving correctness properties for cryptographic protocols. In this paper we apply the same method to the related problem of mixed protocols, and show that a protocol can remain correct even when used in combination with a range of other protocols. We illustrate the method with the familiar Otway-Rees protocol. We identify a simple and easily verified characteristic of protocols, and show that the Otway-Rees protocol remains correct even when used in combination with other protocols that have this characteristic. We also illustrate this method on the Neuman-Stubblebine protocol. This protocol has two parts, an authentication protocol (I) in which a key distribution center creates and distributes a Kerberos-like key, and a reauthentication protocol (II) in which a client resubmits a ticket containing that key. The re-authentication protocol II is known to be flawed. We show that in the presence of protocol II, there are also attacks against protocol I. We then define a variant of protocol II, and prove an authentication property of I that holds even in combination with the modified II.

A strand is a sequence of events; it represents either an execution by a legitimate party in a security protocol or else a sequence of actions by a penetrator. A strand space is a collection of strands, equipped with a graph structure generated by causal interaction. In this framework, protocol cor rectness claims may be expressed in terms of the connections between strands of different kinds. Preparing for a first example, the Needham–Schroeder–Lowe protocol, we prove a lemma that gives a bound on the abilities of the penetrator in any protocol. Our analysis of the example gives a detailed view of the conditions under which it achieves authentication and protects the secrecy of the values exchanged. We also use our proof methods to explain why the original Needham–Schroeder protocol fails. Before turning to a second example, we introduce ideals as a method to prove additional bounds on the abilities of the penetrator. We can then prove a number of correctness properties of the Otway–Rees protocol, and we clarify its limitations. We believe that our approach is distinguished from other work by the simplicity of the model, the precision of the results it produces, and the ease of developing intelligible and reliable proofs even without automated support.

In security protocol analysis, it is important to learn general principles that limit the abilities of an attacker and that can be applied repeatedly to a variety of protocols. The authors introduce the notion of an ideal-a set of messages closed under encryption and invariant under composition with arbitrary messages-to express such principles. In conjunction with the strand space formalism, they use the concept of ideals to prove bounds on a penetrator's capabilities, independent of the security protocol being analyzed. From this they prove a number of correctness properties of the Otway Rees protocol, using these results to explain the limitations of the protocol.

A strand is a sequence of events; it represents either the execution of an action by a legitimate party in a security protocol or else a sequence of actions by a penetrator. A strand space is a collection of strands, equipped with a graph structure generated by causal interaction. In this framework, protocol correctness claims may be expressed in terms of the connections between strands of different kinds. In this paper, we develop the notion of a strand space. We then prove a generally useful lemma, as a sample result giving a general bound on the abilities of the penetrator in any protocol. We apply the strand space formalism to prove the correctness of the Needham-Schroeder-Lowe protocol (G. Lowe, 1995, 1996). Our approach gives a detailed view of the conditions under which the protocol achieves authentication and protects the secrecy of the values exchanged. We also use our proof methods to explain why the original Needham-Schroeder (1978) protocol fails. We believe that our approach is distinguished from other work on protocol verification by the simplicity of the model and the ease of producing intelligible and reliable proofs of protocol correctness even without automated support.