Strand Spaces: Why is a Security Protocol Correct?

A strand is a sequence of events; it represents either the execution of 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 gen-erated by causal interaction. In this framework, protocol correctness claims may be expressed in terms of the con-nections 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 re-sult giving a general bound on the abilities of the penetra-tor in any protocol. We apply the strand space formalism to prove the correctness of the Needham-Schroeder-Lowe protocol. Our approach gives a detailed view of the condi-tions 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 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.