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 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. 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 NeedhamSchroeder protocol fails. We believe that our approach is distinguished from other work on protoc...

• Type: Conference
• Year: 1998
• Where: SP
• Authors: F. Javier Thayer, Jonathan C. Herzog, Joshua D. Guttman
• Keywords: Protocol Correctness, Protocol Correctness Claims, Security Privacy, SP 1998, Strand Space