The Shapes of Bundles
Abstract
When analyzing cryptographic protocols, one often finds that there is really only one thing that can happen in a run of the protocol, or at worst a small number of different things. For instance, every execution of the familiar Needham-Schroeder-Lowe protocol consists of a matching pair consisting of a run of the initiator and one of the responder; no other interaction is possible. We call such a collection of local executions by honest principals a shape. In this paper, we use the strand space theory to develop a framework for explaining observations such as this one, that most protocols allow very few shapes, and frequently only one. We view protocol analysis as a process of assembling different instances of the roles of the protocol. Perhaps one starts with a single execution of a single role. This execution provides the "point of view" of the analysis: Suppose the initiator has sent and received the following messages; what other principals must have had runs? Having started with a single run, one would like to add instances of the roles of the protocol, suitably instantiated, to explore what explanations are possible for the experience of the original principal. If in this process there are very rarely essentially different choices to make, then there will be very few shapes to be found at the leaves of the exploration. In carrying out this program, we have taken an algebraic view. We define a notion of homomorphism, and the exploration consists of applying homomorphisms of a special kind we call augmentations. The algebraic framework has turned out to be highly suggestive for the development of our theory.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 31, 2004
- Accession Number
- ADA460267
Entities
People
- F. J. Thayer
- Joshua D. Guttman
- Shaddin F. Doghmi
Organizations
- MITRE Corporation