A Diagram of Strand Spaces for Security Protocols

The strand space model illustrated with the diagram of strand spaces is adopted as a formalism of security protocols. The open bundle is defined, which is only one element for composing diagrams of strand spaces. And the two operators such as prefixing and parallel composition over the set of open bundles are defined. A novel method is proposed to generate diagrams of strand spaces of security protocols that run in an infinite concurrent way through operating of prefixing and parallel composition between open bundles. The bi-simulation equivalence relation between diagrams of strand spaces based on the bi-simulation between open bundles is defined. Reduction rules for eliminating redundancies of diagrams of strand spaces are also proposed. The case analysis and the comparison between this work and other related work show that the diagram of strand spaces can be used as an effective model for proving security properties of cryptographic protocols that run in an infinite concurrent way.