Strand spaces: why is a security protocol correct?
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
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.Keywords
This publication has 20 references indexed in Scilit:
- Verifying authentication protocols: methodology and examplePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Cryptographic protocol flaws: know your enemyPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Number theoretic attacks on secure password schemesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Casper: a compiler for the analysis of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A hierarchy of authentication specificationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- An attack on the Needham-Schroeder public-key authentication protocolInformation Processing Letters, 1995
- A logic of authenticationPublished by Association for Computing Machinery (ACM) ,1989
- Protocol failures in cryptosystemsProceedings of the IEEE, 1988
- Timestamps in key distribution protocolsCommunications of the ACM, 1981
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978