Composing Strand Spaces
Federico Crazzolara
February 2002 |
Abstract:
The strand space model for the analysis of security protocols
is known to have some limitations in the patterns of nondeterminism it allows
and in the ways in which strand spaces can be composed. Its successful
application to a broad range of security protocols may therefore seem
surprising. This paper gives a formal explanation of the wide applicability
of strand spaces. We start with an extension of strand spaces which permits
several operations to be defined in a compositional way, forming a process
language for building up strand spaces. We then show, under reasonable
conditions how to reduce the extended strand spaces to ones of a traditional
kind. For security protocols we are mainly interested in their safety
properties. This suggests a strand-space equivalence: two strand spaces are
equivalent if and only if they have essentially the same sets of bundles.
However this equivalence is not a congruence with respect to the strand-space
operations. By extending the notion of bundle we show how to define the
strand-space operations directly on ``bundle spaces''. This leads to a
characterisation of the largest congruence within the strand-space
equivalence. Finally, we relate strand spaces to event structures, a well
known model for concurrency.
Available as PostScript, PDF, DVI. |