<p>The events of a security protocol and their causal dependency<br />can play an important role in the analysis of security properties.<br /> This insight underlies both strand spaces and the inductive<br />method. But neither of these approaches builds up the events of<br />a protocol in a compositional way, so that there is an informal<br />spring from the protocol to its model. By broadening the models<br />to certain kinds of Petri nets, a restricted form of contextual nets,<br />a compositional event-based semantics is given to an economical,<br />but expressive, language for describing security protocols; so the<br />events and dependency of a wide range of protocols are determined<br /> once and for all. The net semantics is formally related to a<br />transition semantics, strand spaces and inductive rules, as well as<br />trace languages and event structures, so unifying a range of <br />approaches, as well as providing conditions under which particular,<br />more limited, models are adequate for the analysis of protocols.<br />The net semantics allows the derivation of general properties and<br />proof principles which are demonstrated in establishing an <br />authentication property, following a diagrammatic style of proof.</p>
Composing Strand Spaces
