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.
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.
» Download Paper [PDF, 459KB]
