Events in Security Protocols

Resumé

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