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.
The Shapes of Bundles
Download Resources
PDF Accessibility
One or more of the PDF files on this page fall under E202.2 Legacy Exceptions and may not be completely accessible. You may request an accessible version of a PDF using the form on the Contact Us page.
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 [6, 5] 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 [4] to develop a framework for explaining observations such as this one, that most protocols allow very few shapes, and frequently only one.