| Strand Spaces: Why is a Security Protocol Correct?
March 2000
Joshua D. Guttman, The MITRE Corporation
Jonathan C. Herzog, The MITRE Corporation
F. Javier Thayer, The MITRE Corporation
ABSTRACT
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 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 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 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.
Publication
Published in Proceedings, 1998 IEEE Symposium on Security and Privacy, May 1998.
Additional Search Keywords
N/A
|
