9.8. Strand spaces
The strand spaces approach has been developed fairly recently by Guttman et al. from MITRE. Roughly speaking, a strand represents the sequence of actions in which a particular protocol principal may participate. For an honest principal this encodes the expected sequence of send and receive messages associated with a particular role of the protocol. Agents can play multiple roles simultaneously. Thus for the (corrected) Needham-Schroeder-Lowe Public-Key protocol the initiator strand is:
The + and − signs signify whether the term is transmitted or received respectively by the agent in question. Thus the initiator, a in this ...
Get The Modelling and Analysis of Security Protocols: the CSP Approach now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
