BRICS RS-01-13 Crazzolara & Winskel: Events in Security Protocols BRICS

Basic Research in Computer Science

Events in Security Protocols

Federico Crazzolara Glynn Winskel BRICS Report Series RS-01-13 ISSN 0909-0878 April 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Federico Crazzolara & Glynn Winskel.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/01/13/

Events in Security Protocols

Federico Crazzolara^{∗} Glynn Winskel {fc232, gw104}@cl.cam.ac.uk

Computer Laboratory University of Cambridge

Abstract

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.

1 Introduction

The last few years have seen the emergence of successful intensional, event-based, approaches to reasoning about security protocols. The methods are concerned with reasoning about the events that a security protocol can perform, and make use of a causal dependency that exists between events. For example, to show secrecy in a protocol it is shown that there can be no earliest event violating a secrecy property; any such event is shown to depend on some earlier event which itself violates secrecy— because the behaviour of the protocol does not permit such an infinite regress, the secrecy property is established. In a similar way, dependency between events is used to establish forms of authentication by showing that a sequence of communication events of one agent entails a corresponding sequence of events of the intended participant.

∗BRICS Basic Research in Computer Science, Centre of the Danish National Research Foundation

Both the method of strand spaces [THG98c, THG98a, THG98b] and the inductive method of Paulson [Pau99, Pau98] have been designed to support such an intensional, event-based, style of reasoning. Strand spaces are based on an explicit causal dependency of events, whereas in Paulson’s method the dependency is implicit in the inductive rules, which might express, for instance, that the input of a message depends on its previous output. Both methods have successfully tackled a number of protocols though in an ad hoc fashion. Both make an informal spring from a protocol to its representation, as either a strand space or a set of inductive rules. Both methods do not address how to build up their representation of a protocol in a compositional fashion. Both are remarkably similar, to the extent that a proof using one seems at an informal level to suggest a proof using the other.

We show that Petri nets, and specifically a restricted form of contextual nets [MR95], provide a common framework in which to understand both the strand-space and inductive methods, and it seems, although we understand it less well, the recent multiset rewriting and linear-logic methods of [CDL^{+}99, CDL^{+}00].^{1} But, more importantly, by moving to a broader class of models we can show how event-based models can be structured in a compositional way and so used to give a formal semantics to security protocols which supports proofs of their correctness. To make the case, and provide semantics to a whole range of protocols once and for all, we study the semantics of SPL (Security Protocol Language).

We demonstrate the usefulness of the net semantics in deriving (in contrast to postulating) proof principles for security protocols and apply them to prove an authentication property—the diagrammatic style of proof may be of interest in itself. (We hope in future to address the issue of logics for security protocols and see the semantics of SPL as providing a good basis for a model theory.) We establish precise relationships between the net semantics and transition semantics, strand spaces, inductive rules, and trace languages and event structures. The results formally back up the adequacy of strand-space and inductive-rule representations for broad classes of security protocols and properties— showing when nothing is lost in moving to these more restrictive models.

1Although Petri nets have been used before in the analysis of security protocols, e.g. [NT92], our use is significantly different and more closely related to the strandspace and inductive methods.

2 Security protocols

As a running example we consider the Needham-Schröder-Lowe (NSL) protocol:

\begin{matrix}(1) & A ⟶ B : \{m, A\}_{P ub(B)} \\ (2) & B ⟶ A : \{m, n, B\}_{P ub(A)} \\ (3) & A ⟶ B : \{n\}_{P ub(B)} \end{matrix}

This protocol, like many others of its kind has two roles: one for the initiator, here played by agent A (say Alice), and one for the responder, here B (Bob). It is a public-key protocol that assumes an underlying public-key infrastructure, such as RSA [RSA78]. Both agents have their own, secret private key. Public keys in contrast are available to all participants in the protocol. The NSL protocol makes use of nonces which one can think of as newly generated, unguessable numbers whose purpose is to ensure the freshness of messages.

The protocol describes an interaction between A in the role of initiator and B as responder: A sends to B a new nonce m together with her own agent name A, both encrypted with B’s public key. When the message is received by B, he decrypts it with his secret private key. Once decrypted, B prepares an encrypted message for A that contains a new nonce together with the nonce received from A and his name B. Acting as responder, B sends it to A, who recovers the clear text using her private key. A convinces herself that this message really comes from B by checking whether she got back the same nonce sent out in the first message. If that is the case, she acknowledges B by returning his nonce. B does a similar test.

Although in this informal explanation only two agents in their respective roles are described, the protocol is really a shorthand for a situation in which a network of distributed agents are each able participate in multiple concurrent sessions as both initiator and responder. There is no assurance that they all stick to the protocol, or indeed that communication goes to the intended agent. An attacker might dissemble and pretend to be one or several agents, taking advantage of any leaked keys it possesses in deciphering, and preparing the messages it sends.

The NSL protocol aims at distributing nonces m and n in a secure way, allowing no one but the initiator and the responder to know them (secrecy). Another aim of the protocol is that, for example, Bob should be guaranteed that m is indeed the nonce sent by Alice (authentication). Lowe pointed out that the NSL protocol is prone to a “middle-man” attack, violating both these secrecy and authentication properties, if the name B is not included in the second message [Low96]—the second message did not include B in the original protocol of Needham and Schröder.

3 SPL—a language for security protocols

In order to be more explicit about the activities of participants in a protocol and those of a possible attacker, and to express these compositionally, we design an economical process language for the purpose. The language SPL(Security Protocol Language) is close to an asynchronous Pi-Calculus [Mil99] and is similar to that adopted in [AG97], though in its treatment of new names its transition semantics will be closer to that in [PS93] (it separates concerns of freshness from concerns of scope which are combined in the Pi-Calculus restriction).

3.1 The syntax of SPL

We start by giving the syntactic sets of the language:

• An infinite set of Names, with elements n, m, ⋯, A, B, · · ·. Names will range over nonces as well as agent names, and could also include other values.

• Variables over names x, y, ⋯, X, Y, · · ·.

• Variables over messages ψ, ψ′, ψ_{1}, · · ·.

• Indices i ∈ Indices with which to index components of parallel compositions.

Name expressions v ::= n, A, ⋯ | x, X, ⋯
Key expressions k ::= P ub(v) | P riv(v) | Key(v_{1}, v_{2})
Messages  M ::= v | k | M_{1}, M_{2} | {M}_{k} |ψ
Processes  p ::= out newx⃗M.p |

in patx⃗ψ⃗M.p |

∥_{i∈I}p_{i}

Figure 1: Syntax of SPL

The other syntactic sets of the language are described by the grammar shown in Figure 1. Note we use “vector” notation; for example, the “vector” x⃗ abbreviates some possibly empty list x_{1}, ⋯, x_{l}.

We take fv(M), the free variables of a a message M, to be the set of variables which appear in M, and define the free variables of process terms by:

\begin{aligned}fv(out newx⃗M.p) & = & (fv(p) ∪ fv(M))\\{x⃗\} \\ fv(in patx⃗ψ⃗M.p) & = & (fv(p) ∪ fv(M))\\{x⃗, ψ⃗\}) \\ fv(∥_{i∈I}p_{i}) & = & ⋃_{i∈I} fv(p_{i}) \end{aligned}

As usual, we say that a process without free variables is closed, as is a message without variables. We shall use standard notation for substitution into the free variables of an expression, though we will only be concerned with the substitution of names or closed (variable-free) messages, obviating the problems of variable capture.

We use P ub(v), P riv(v) for the public, private keys of v, and we use Key(v_{1}, v_{2}) for the symmetric key of v_{1} and v_{2}. Keys can be used in building up encrypted messages. Messages may consist of a name or a key, be the composition of two messages (M_{1}, M_{2}), or an encrypted message {M}_{k} representing the message M encrypted using the key k.

An informal explanation of the language:

out newx⃗M.p This process chooses fresh, distinct names n⃗ = n_{1}, ⋯, n_{l} and binds them to the variables x⃗ = x_{1}, ⋯, x_{l}. The message M[n⃗/x⃗] is output to the network and the process resumes as p[n⃗/x⃗]. The communication is asynchronous in the sense that the action of output does not await input. The new construct is like that of Pitts and Stark [PS93] and abstracts out an important property of a value chosen randomly from some large set; such a value is likely to be new. in patx⃗ψ⃗M.p This process awaits an input that matches the pattern M

for some binding of the pattern variables x⃗ψ⃗ and resumes as p under this binding. All the pattern variables x⃗ψ⃗ must appear in the pattern M.

∥_{i∈I}p_{i} This process is the parallel composition of all components p_{i} for i in the indexing set I. The set I is a subset of Indices. Indices will help us distinguish in what agent, which role and what run a particular action occurs. The process, written nil, abbreviates the empty parallel composition (where the indexing set is empty).

Convention 3.1 It simplifies the writing of process expressions if we adopt some conventions. Firstly, we simply write out M.p when the list of “new” variables is empty. Secondly, and more significantly, we allow ourselves to write

⋯ in M.p ⋯

in an expression, to be understood as meaning the expression

⋯ in patx⃗ψ⃗M.p ⋯

where the pattern variables x⃗, ψ⃗ are precisely those variables left free in M by the surrounding expression. For example, we can describe a responder in NSL as the process

Resp(B) ≡ in{x, Z}_{P ub(B)}. out new y{x, y, B}_{P ub(Z)}. in{y}_{P ub(B)}. nil

For the first input, the variables x, Z in {x, Z}_{P ub(B)} are free in the whole expression, so by convention are pattern variables, and we could instead write in pat x, Z{x, Z}_{P ub(B)}. · · ·. On the other hand, in the second input the variable y in {y}_{P ub(B)} is bound by the outer new y ⋯ and so by the convention is not a pattern variable, and has to be that value sent out earlier. Often we will not write the nil process explicitly, so, for example, omitting its mention at the end of the responder code above. A parallel composition can be written in infix form via the notation

p_{1}∥p_{2} ⋯ ∥p_{r} ≡ ∥_{i∈{1,···,r}}p_{i} .

Replication of a process, !p, abbreviates ∥_{i∈ω}p, consisting of a countably infinite copies of p set in parallel.

An obvious structural induction defines the set of names of a process. We define size(p) of a process term p to be an ordinal measuring the depth of process operations in the term.

\begin{aligned}Init(A, B) & ≡ & out new x\{x, A\}_{P ub(B)}. \\ & & in\{x, y, B\}_{P ub(A)}. \\ & & out\{y\}_{P ub(B)}. \\ & & nil \\ Resp(B) & ≡ & in\{x, Z\}_{P ub(B)}. \\ & & out new y\{x, y, B\}_{P ub(Z)}. \\ & & in\{y\}_{P ub(B)}. \\ & & nil \end{aligned}

Figure 2: Initiator and responder code

Definition 3.1 The size of a closed process term is an ordinal given by the structural induction:

\begin{aligned}size(out newx⃗M.p) & = & 1 + size(p) \\ size(in patx⃗ψ⃗M.p) & = & 1 + size(p) \\ size(∥_{i∈I}p_{i}) & = & 1 + sup_{i∈I}size(p_{i}). \end{aligned}

3.2 NSL as a process

As an illustration, we can program the NSL protocol in our language, and so formalise the introductory description given in the Section 2. We assume given a set of agent names, Agents, of agents participating in the protocol. The agents participating in the NSL protocol play two roles, as initiator and responder with any other agent. Abbreviate by Init(A, B) the program of initiator A ∈ Agents communicating with B ∈ Agents and by Resp(B) the program of responder B ∈ Agents. The code of both an arbitrary initiator and an arbitrary responder is given in Figure 2. In the code we are forced to formalise aspects that are implicit in the informal description, such as the creation of new nonces, the decryption of messages and the matching of nonces.

We can model the attacker by directly programming it as a process. Figure 3, shows a general, active attacker or “spy”. The spy has the capability of composing eavesdropped messages, decomposing composite message, and using cryptography whenever the appropriate keys are available; the available keys are all the public keys and the leaked private keys. By choosing a different program for the spy we can restrict or augment its power, e.g., to passive eavesdropping or active falsification.

The whole system is obtained by putting all components in parallel. Components are replicated, to model multiple concurrent runs of the

Spy_{1} ≡ in ψ_{1}.in ψ_{2}.out(ψ_{1}, ψ_{2}).nil  (composing)
Spy_{2} ≡ in(ψ_{1}, ψ_{2}).out ψ_{1}.out ψ_{2}.nil  (decomposing)
Spy_{3} ≡ in x.in ψ.out {ψ}_{P ub(x)}.nil  (encryption)
Spy_{4} ≡ in P riv(x).in {ψ}_{P ub(x)}.out ψ.nil (decryption)
Spy ≡ ∥_{i∈{1,...,4}}Spy_{i}

Figure 3: Attacker code

\begin{aligned}P_{init} & ≡ & ∥_{A,B} ! Init(A, B) \\ P_{resp} & ≡ & ∥_{A} ! Resp(A) \\ P_{spy} & ≡ & ! Spy \\ NSL & ≡ & ∥_{i∈\{resp,init,spy\}} P_{i} \end{aligned}

Figure 4: The system

protocol. The system is described in Figure 4.

3.3 A transition semantics

We first give a, fairly traditional, transition semantics to SPL. It says how input and output actions affect configurations; a configuration expresses the state of execution of the process, the messages so far output to the network and the names currently in use.

A configuration consists of a triple

⟨p, s, t⟩

where p is a closed process term, s is a subset of the set of names Names, and t is a subset of closed (i.e., variable-free) messages. We say the configuration is proper iff the names in p and t are included in s. The idea is that a closed process p acts in the context of the set of names s that have been used so far, and the set of messages t which have been output, to input a message or to generate new names before outputting a message.

Actions α may be inputs or new-outputs, possibly tagged by indices to show at which parallel component they occur:

α ::= out new n⃗.M | in M | i : α

(output) Provided the names n⃗ are all distinct and not in s,

⟨out new x⃗M.p, s, t⟩ ⟶^{out new n⃗M[n⃗/x⃗]} ⟨p[n⃗/x⃗], s ∪ {n⃗}, t ∪ {M[n⃗/x⃗]}⟩

(input) Provided M[n⃗/x⃗, N⃗/ψ⃗] ∈ t,

⟨in patx⃗ψ⃗M.p, s, t⟩ ⟶^{in M[n⃗/x⃗,N⃗/ψ⃗]} ⟨p[n⃗/x⃗, N⃗/ψ⃗], s, t⟩

(par)

{⟨p_{j}, s, t⟩ ⟶^{α} ⟨p′_{j}, s′, t′⟩ \atop ⟨∥_{i∈I}p_{i}, s, t⟩ ⟶^{j:α} ⟨∥_{i∈I}p_{i}[p′_{j}/j], s′, t′⟩} j ∈ I

Figure 5: Transition semantics

where M is a closed message, n⃗ are names and i is an index drawn from Indices. We write out M for an output action, outputting a message M, where no new names are generated.

The way configurations evolve is expressed by transitions

⟨p, s, t⟩ ⟶^{α} ⟨p′, s′, t′⟩ ,

given by the rules displayed in Figure 5.

The transition semantics allows us to state formally many security properties. However, it does not support directly local reasoning of the kind one might wish to apply in the analysis of security protocols. To give an idea of the difficulty, imagine we wished to establish that the nonce generated by B as responder in NSL was never revealed as an open message on the network. A reasonable way to prove such a property is to find a stronger invariant, a property which can be shown to be preserved by all the actions of the process. Equivalently, one can assume that there is an earliest action α_{l} in a run which violates the invariant, and derive a contradiction by showing that this action must depend on a previous action, which itself violates the invariant.

An action might depend on another action through being, for example, an input depending on a previous output, or simply through occurring at a later control point in a process. A problem with the transition semantics is that it masks such local dependency, and even the underlying process events on which the dependency rests. The wish to support arguments based on local dependency leads to a more refined semantics based on events.

4 The events of SPL

We must first address the issue of what constitutes an event of a security protocol. Here, we follow the lead from Petri nets,^{2} and define events in terms of how they affect conditions. Conditions are to represent some form of local state and we discern conditions of three kinds: control, output and name conditions.

The set of control conditions C consists of output or input processes, perhaps tagged by indices, and is given by the grammar

b ::= out new x⃗M.p | in patx⃗ψ⃗M.p | i : b

where i ∈ Indices. A condition in C stands for the point of control in a (single-thread) process. When C is a subset of control conditions we will write i : C to mean {i : b | b ∈ C}.

The set of output conditions O consists of closed message expressions. An individual condition M in O stands for the message M having been output on the network. Output conditions are persistent; once output conditions are made to hold they continue to hold forever. This squares with our understanding that once a message has been output to the network it can never be removed, and can be input repeatedly.

The set of name conditions is precisely the set of names Names. A condition n in Names stands for the name n being in use.

We define the initial conditions of a closed process term p, to be the subset Ic(p) of C, given by the following structural induction:

Ic(out new x⃗M.p) = {out new x⃗M.p} Ic(in patx⃗ψ⃗M.p) = {in patx⃗ψ⃗M.p}

Ic(∥_{i∈I}p_{i}) = ⋃_{i∈I} i : Ic(p_{i})

where the last case also includes the base case nil, when the indexing set is empty.

2A brief summary of Petri nets is given in the Appendix.

We will shortly define the set of events Events as a subset of

Pow(C)×Pow(O)×Pow(Names)×Pow(C)×Pow(O)×Pow(Names) .

So an individual event e ∈ Events is a tuple

e = (^{c}e,^{o}e,^{n}e, e^{c}, e^{o}, e^{n})

where^{c}e is the set of C-preconditions of e, e^{c} is the set of C-postconditions of e, etc. Write ^{·}e for ^{c}e ∪^{o} e ∪^{n} e, all preconditions of e, and e^{·} for all postconditions e^{c} ∪ e^{o} ∪ e^{n}.

Earlier in the transition semantics we used actions α to specify the nature of transitions. An event e is associated with a unique action act(e).

The set of events associated with SPL is given by an inductive definition. Define Events to be the smallest set which includes all output, input and indexed events:

• output events Out(out new x⃗M.p; n⃗), where n⃗ = n_{1}, ⋯, n_{l} are distinct names to match the variables x⃗ = x_{1}, ⋯, x_{l}, consists of an event e with these pre- and postconditions:

\begin{matrix}^{c}e = \{out new x⃗M.p\} , ^{o}e = ∅ , ^{n}e = ∅ , \\ e^{c} = Ic(p[n⃗/x⃗]) , e^{o} = \{M[n⃗/x⃗]\} e^{n} = \{n_{1}, ⋯, n_{l}\} . \end{matrix}

The action of an output event is

act(Out(out new x⃗M.p; n⃗)) = out new n⃗.M[n⃗/x⃗].

[figure: M[n⃗/x⃗]; out new x⃗ M . p; out new n⃗ M[n⃗/x⃗]; . .; n_{1}; n_{l}; …; Ic(p[n⃗/x⃗])]

An occurrence of the output event Out(out new x⃗M.p; n⃗) affects the control conditions and puts the new names n_{1}, ⋯, n_{l} into use, necessarily for the first time as according to the token game the event occurrence must avoid contact with names already in use.

The definition includes the special case when x⃗ and n⃗ are empty lists, and we write Out(out M.p) for the output event with no name conditions and action out M.

• input events In(in patx⃗ψ⃗M.p; n⃗, L⃗), where n⃗ is a list of names to match x⃗ and L⃗ is a list of closed messages to match ψ⃗, consists of an event e with these pre- and postconditions:

\begin{matrix}^{c}e = \{in patx⃗ψ⃗M.p\} , ^{o}e = \{M[n⃗/x⃗, L⃗/ψ⃗]\} , ^{n}e = ∅ , \\ e^{c} = Ic(p[n⃗/x⃗, L⃗/ψ⃗]) , e^{o} = ∅ , e^{n} = ∅ . \end{matrix}

The action of an input event is

act(In(in patx⃗ψ⃗M.p; n⃗, L⃗)) = in M[n⃗/x⃗, L⃗/ψ⃗].

[figure: M[n⃗/x⃗, L⃗/ψ⃗]; in M[n⃗/x⃗, L⃗/ψ⃗]; …; Ic(p[n⃗/x⃗, L⃗/ψ⃗]); in patx⃗ψ⃗M.p]

• indexed events i : e where e ∈ Events, where i ∈ Indices and

\begin{matrix}^{c}(i : e) = i :^{c} e , ^{o}(i : e) =^{o} e , ^{n}(i : e) =^{n} e , \\ (i : e)^{c} = i : e^{c} , (i : e)^{o} = e^{o} , (i : e)^{n} = e^{n} . \end{matrix}

The action of an indexed event act(i : e) is i : α, where α is the action of e.

When E is a subset of events we will generally use i : E to mean {i : e | e ∈ E}.

In defining the set of conditions and, inductively, the set of events, we have in fact defined a (rather large) net from the syntax of SPL. The SPL-net has conditions C ∪ O ∪ Names and events Events. Its markings M will be subsets of conditions and so of the form

M = c ∪ s ∪ t

where c ⊆ C, s ⊆ Names, and t ⊆ O. By assumption the set of conditions O are persistent so the net is a contextual net with the following token game—see Appendix C.

Letting c ∪ s ∪ t and c′ ∪ s′ ∪ t′ be two markings, c ∪ s ∪ t ⟶^{e} c′ ∪ s′ ∪ t′

iff

·e ⊆ c ∪ s ∪ t & e^{c} ∩ c = ∅ & e^{n} ∩ s = ∅ (event e has concession), and c′ = (c \^{c}e) ∪ e^{c} & s′ = s ∪ e^{n} & t′ = t ∪ e^{o} .

In particular, the occurrence of e begins the holding of its name postconditions e^{n}—these names have to be distinct from those already in use to avoid contact.

5 Relating net and transition semantics

The behaviour of the SPL-net is closely related to the transition semantics given earlier.

Theorem 5.1

i) If ⟨p, s, t⟩ ⟶^{α} ⟨p′, s′, t′⟩, then Ic(p) ∪ s ∪ t ⟶^{e} Ic(p′) ∪ s′ ∪ t′ in the

SPL-net, for some e ∈ Events with act(e) = α.

ii) If Ic(p) ∪ s ∪ t ⟶^{e} M′ in the SPL-net, then ⟨p, s, t⟩ ⟶^{act(e)} ⟨p′, s′, t′⟩

and M′ = Ic(p′) ∪ s′ ∪ t′, for some closed process p′, s′ ⊆ Names and t′ ⊆ O.

Definition 5.1 Let e ∈ Events. Let p be a closed process, s ⊆ Names,

and t ⊆ O. Write ⟨p, s, t⟩ ⟶^{e} ⟨p′, s′, t′⟩ iff Ic(p)∪s∪t ⟶^{e} Ic(p′)∪s′∪t′

in the SPL-net.

6 The events of a process

Generally for a process p only a small subset of the events Events can ever come into play. For this reason it’s useful to restrict the events to those reachable in the behaviour of a process.

The set Ev(p) of events of a closed process term p are defined by induction on size:

Ev(out new x⃗M.p) ={Out(out new x⃗M.p; n⃗) | n⃗ distinct names}
∪ ⋃ {Ev(p[n⃗/x⃗]) | n⃗ distinct names} ,
Ev(in patx⃗ψ⃗M.p) ={In(in patx⃗ψ⃗M.p; n⃗, L⃗) | n⃗ names, L⃗ closed messages}

∪ ⋃ {Ev(p[n⃗/x⃗, L⃗/ψ⃗]) | n⃗ names, L⃗ closed messages} ,

Ev(∥_{i∈I}p_{i}) = ⋃_{i∈I} i : Ev(p_{i}) .

As an example, the events Ev(NSL) of NSL are shown in the Appendix.

A closed process term p denotes a net Net(p) consisting of the global set of conditions C ∪ O ∪ Names built from SPL, events Ev(p) and initial control conditions Ic(p). We can define the token game on the net Net(p) exactly as we did earlier for the SPL-net, but this time events are restricted to being in the set Ev(p). It’s clear that if an event transition is possible in the restricted net Net(p) then so is it in the SPL-net. The converse also holds provided one starts from a marking whose control conditions either belong to Ic(p) or are conditions of events in Ev(p).

Definition 6.1 Let p be a closed process term. Define the controlconditions of p to be

p^{c} = Ic(p) ∪ ⋃ {e^{c} | e ∈ Ev(p)} .

Lemma 6.1 Let M ∩ C ⊆ p^{c}. Let e ∈ Events. Then,

M ⟶^{e} M′ in the SPL-net iff e ∈ Ev(p) & M ⟶^{e} M′ in Net(p) .

Consequently, in analysing those sequences of event transitions

⟨p_{0}, s_{0}, t_{0}⟩ ⟶^{e_{1}} ⋯ ⟶^{e_{r}} ⟨p_{r}, s_{r}, t_{r}⟩ ⟶^{e_{r+1}} ⋯,

a closed process p can perform, or correspondingly those of the transition semantics, it suffices to study the behaviour of Net(p) with its restricted set of events Ev(p). This simplification is especially useful in proving invariance properties because these amount to an argument by cases on the form of events a process can do.

Recall that we say a configuration ⟨p, s, t⟩ is proper iff the names in p and t are included in s.

Proposition 6.2 Let e ∈ Events. Suppose that ⟨p, s, t⟩ and ⟨p′, s′, t′⟩ are configurations, and that ⟨p, s, t⟩ is proper. If ⟨p, s, t⟩ ⟶^{e} ⟨p′, s′, t′⟩, then ⟨p′, s′, t′⟩ is also proper.

Important convention: From now on we assume that all configurations ⟨p, s, t⟩ are proper.

7 Proving security properties

To demonstrate the viability of the net semantics as a tool in proving security properties, we use the semantics to derive general principles for proving secrecy and authentication. The principles capture the kind of dependency reasoning found in the strand spaces and inductive methods. To illustrate the principles in action, we apply them to establish an authentication guarantee for the responder part of the NSL protocol. We introduce a diagrammatic style of reasoning which we find helpful.

7.1 General proof principles

From the net semantics we can derive several principles useful in proving authentication and secrecy of security protocols. Write M ⊏ M′ to mean message M in a subexpression of message M′, i.e., ⊏ is the smallest binary relation on messages such that:

M ⊏ M
M ⊏ N ⇒ M ⊏ (N, N′) ∧ M ⊏ (N′, N)
M ⊏ N ⇒ M ⊏ {N}_{k}

where M, N, N′ are messages and k is a key expression. We also write M ⊏ t iff ∃M′ . M ⊏ M′ ∧ M′ ∈ t, for a set of messages t.

Proposition 7.1 (Well-foundedness) Given a property P on configurations, if a run

⟨p_{0}, s_{0}, t_{0}⟩ ⟶^{e_{1}} ⋯ ⟶^{e_{r}} ⟨p_{r}, s_{r}, t_{r}⟩ ⟶^{e_{r+1}} ⋯,

contains a configurations such that P(p_{0}, s_{0}, t_{0}) and ¬P(p_{j}, s_{j}, t_{j}), then there is an event e_{h}, 0 < h ≤ j, such that P(p_{i}, s_{i}, t_{i}) for all i ≤ h and ¬P(p_{h}, s_{h}, t_{h}).

We say that a name m ∈ Names is fresh on an event e if m ∈ e^{n} and we write F resh(m, e).

Proposition 7.2 (Freshness) Within a run

⟨p_{0}, s_{0}, t_{0}⟩ ⟶^{e_{1}} ⋯ ⟶^{e_{r}} ⟨p_{r}, s_{r}, t_{r}⟩ ⟶^{e_{r+1}} ⋯,

the following properties hold:

1. If n ∈ s_{i} then either n ∈ s_{0} or there is a previous event e_{j} such that F resh(n, e_{j}).

2. Given a name n there exists at most one event e_{i} s.t. F resh(n, e_{i}).

3. If F resh(n, e_{i}) then for all j < i the name n does not appear in ⟨p_{j}, s_{j}, t_{j}⟩.

Proposition 7.3 (Control precedence) Within a run

⟨p_{0}, s_{0}, t_{0}⟩ ⟶^{e_{1}} ⋯ ⟶^{e_{r}} ⟨p_{r}, s_{r}, t_{r}⟩ ⟶^{e_{r+1}} ⋯,

if b ∈ ^{c}e_{i} either b ∈ Ic(p_{0}) or there is an earlier event e_{j}, j < i, such that b ∈ e_{j}^{c}.

Proposition 7.4 (Output-input precedence) In a run

⟨p_{0}, s_{0}, t_{0}⟩ ⟶^{e_{1}} ⋯ ⟶^{e_{r}} ⟨p_{r}, s_{r}, t_{r}⟩ ⟶^{e_{r+1}} ⋯,

if M ∈ ^{o}e_{i}, then either M ∈ t_{0} or there is an earlier event e_{j}, j < i, such that M ∈ e_{j}^{o}.

7.2 An example: authentication for NSL

We will prove authentication for a responder in an NSL protocol in the sense that: to any complete session of agent B_{0} as responder, apparently with agent A_{0}, there corresponds a complete session of agent A_{0} as initiator. We refer to the Appendix for the events of NSL.

In the proof it’s helpful to make use of a form of diagrammatic reasoning which captures the precedence of events. When the run is understood we draw \xymatrix{e \ar[r] & e′} when e precedes e′ in the run, allowing e = e′.

Theorem 7.5 (Authentication) If a run of NSL

⟨NSL, s_{0}, t_{0}⟩ ⟶^{e_{1}} ⋯ ⟶^{e_{r}} ⟨p_{r}, s_{r}, t_{r}⟩ ⟶^{e_{r+1}} ⋯,

contains the responder events b_{1}, b_{2}, b_{3}, with actions

\begin{aligned}act(b_{1}) & = & resp : B_{0} : i : in \{m_{0}, A_{0}\}_{P ub(B_{0})} , \\ act(b_{2}) & = & resp : B_{0} : i : out new n_{0} \{m_{0}, n_{0}, B_{0}\}_{P ub(A_{0})} , \\ act(b_{3}) & = & resp : B_{0} : i : in\{n_{0}\}_{P ub(B_{0})}) , \end{aligned}

for an index i, and P riv(A_{0}) ⊏̸ t_{0}, then the run contains initiator events a_{1}, a_{2}, a_{3} with \xymatrix{a_{3} \ar[r] & b_{3}} , where, for some index j,

\begin{aligned}act(a_{1}) & = & init : (A_{0}, B_{0}) : j : out new m_{0} \{m_{0}, A_{0}\}_{P ub(B_{0})} , \\ act(a_{2}) & = & init : (A_{0}, B_{0}) : j : in\{m_{0}, n_{0}, B_{0}\}_{P ub(A_{0})} , \\ act(a_{3}) & = & init : (A_{0}, B_{0}) : j : out\{n_{0}\}_{P ub(B_{0})} . \end{aligned}

Proof. By control precedence we obtain: \xymatrix{b_{1} \ar[r] & b_{2} \ar[r] & b_{3}} . Consider the property of configurations

Q(p, s, t) ⇔ ∀M ∈ t. n_{0} ⊏ M ⇒ {m_{0}, n_{0}, B_{0}}_{P ub(A_{0})} ⊏ M .

By freshness, the property Q holds immediately after b_{2}, but clearly not immediately before b_{3}. By well-foundedness there is a earliest event following b_{2} but preceding b_{3} that violates Q. Let e be such an event.

\xymatrix{b_{1} \ar[r] & b_{2} \ar[rr] \ar[dr] &  & b_{3} \\  &  & e \ar[ur]}

Inspecting the events of the NSL protocol (see Appendix), using the assumption that P riv(A_{0}) ⊏̸ t_{0}, one can show that e can only be an initiator event a′_{3} with action

act(a′_{3}) = init : (A, B_{0}) : j : out{n_{0}}_{P ub(B_{0})}

for some index j and agent A. There must also be preceding events a′_{1}, a′_{2} with actions

\begin{aligned}act(a′_{1}) & = & init : (A, B_{0}) : j : out new m \{m, A\}_{P ub(B_{0})} \\ act(a′_{2}) & = & init : (A, B_{0}) : j : in\{m, n_{0}, B_{0}\}_{P ub(A)} \end{aligned}

\xymatrix{b_{1} \ar[r] & b_{2} \ar[rr] \ar[dr] &  & b_{3} \\ a′_{1} \ar[r] & a′_{2} \ar[r] & a′_{3} \ar@{-->}[ur]}

Since F resh(b_{2}, n_{0}), the event b_{2} must precede a′_{2}. The property Q holds on configurations up to a′_{3} and, in particular, on the configuration immediately before a′_{2}. From this we conclude that m = m_{0} and A = A_{0}. Hence a′_{3} = a_{3}, a′_{2} = a_{2}, and a′_{1} = a_{1} as described below.

\xymatrix{b_{1} \ar[r] & b_{2} \ar[r] \ar[d] & b_{3} \\ a_{1} \ar[r] & a_{2} \ar[r] & a_{3} \ar[u]}

(Since F resh(a_{1}, m_{0}), the event a_{1} precedes b_{1}.) □

8 Relating security models

We have related our net semantics of SPL to a transition semantics. Now we establish its relations to the security models of strand spaces, inductive rules, as well as other traditional models. In security protocols we are largely interested in safety properties, which reduce to a property holding of all finite behaviours. Thus it suffices to show how a finite behaviour in one model can be matched by the finite behaviour in another. In relating the net semantics to strand spaces and inductive rules we need to constrain process terms, to allow some repetition of actions, though this does not seem unduly restrictive in formalising security protocols.

8.1 Strand spaces

In relating the net semantics to strand spaces we must face the fact that strand spaces don’t compose readily, not using traditional process operations at least. Their form doesn’t allow prefixing by a single event. Nondeterminism only arises through the choice as to where input comes from, and there is not a recognisable nondeterministic sum of strand spaces. Even an easy definition of parallel composition by juxtaposition is thwarted if “unique origination” is handled as a global condition on the entire strand space. This complicates the relation between a compositional semantics and strand spaces.

We can however relate the net behaviour of a !-par process to to that of an associated strand space; a !-par process is a closed process of the form !∥_{i∈I}p_{i} for which no subterm p_{i} contains a parallel composition. In proving the relation (though unfortunately not in this short write-up) we find it useful to extend strand spaces in order to compose them, chiefly with conflict to permit their nondeterministic sum, and then finally to observe that for processes with replication the conflict can be eliminated, without upsetting the strand-space behaviour. (Strand spaces can be viewed as special forms of event structures—see below; so ideas, such as the use of a conflict relation, can be adapted from there.)

Definition 8.1 A strand space consists of S = ⟨S_{i}⟩_{i∈I} an indexed set of strands. An individual strand S_{i}, where i ∈ I, is a finite sequence of output or input events carrying respectively output or input actions of the kind out newn⃗M or in M, where M is a closed message and n⃗ a list of distinct names that are intended to be fresh (“uniquely originating”) at the event. We permit only strands on which any “new” names do appear in previous actions of the strand. (A set of strands is canonically a strand space in which each strand has itself as index.)

As usual, a strand space can be seen as a graph whose nodes are of the form (i, l) with i ∈ I index of a strand and l position of an event in that strand (1 ≤ l ≤ length(s_{i})). Each node uniquely identifies an event in a strand. Edges are of two different kinds: ⇒ between two nodes that identify two events of a same strand, one immediately preceding the other and → between two nodes identifying respectively an output event and an input event with the same message. A bundle of a strand space S is a finite, acyclic subgraph such that

• if a node belongs to the bundle then so do all the nodes that precede it on its strand,

• each input node has exactly one incoming → edge,

• two different strands that have a “new” name in common don’t both contribute to the same bundle.

Our definition is not quite standard. But the only significant difference is in the treatment of unique origination which is taken care of in the definition of bundle rather than being a condition on the entire strand space—the “parametric strand spaces” of [CDL^{+}00] achieve the same effect and are closely related.

A strand space can be seen as a form of event structure [Win87a]. A strand space determines a stable event structure, whose family of configurations is the same as the bundles of the strand space; the bundles of a strand space when ordered by inclusion form a stable family which ensures not only that each configuration of events in the family can be equipped with a local partial order of causal dependency, but that at the cost renaming events these local partial orders can be extended to a global partial order of causal dependency, yielding a prime event structure.

Often in strand spaces the precise identity of indices doesn’t matter. A re-indexing of a strand space S = ⟨S_{i}⟩_{i∈I} is a permutation π of I such that S_{i} and S_{π(i)} are sequences of the same length with the same actions at corresponding events. A re-indexing of a strand space induces a reindexing on its bundles; a bundle’s nodes and arcs are changed according to the correspondence given by π.

To relate the net behaviour of a process to its behaviour as a strand space we need to linearise bundles. More precisely:

Definition 8.2 Given a bundle C of a strand space S, a linearisation of C is a sequence of nodes e_{1} … e_{k} such that {e_{1}, …, e_{k}} = C and for all e in C and for all e_{i} in L, if e⇒_{C}e_{i} or e→_{C}e_{i} then e precedes e_{i} in the sequence. An event-linearisation of a bundle is the sequence of strand-space events associated with the nodes of a linearisation.

Let p be a !-par process and s a set of names containing all names in p. Take T r(p, s) to be the strand space with strands consisting of all the maximal sequences e_{1} … e_{k} of events in Ev(p) such that:

i) ^{c}e_{1} ⊆ Ic(p) and

ii) for all i, 1 ≤ i < k, we have e_{i}^{n} ∩ (s ∪ {e_{j}^{n} | j < i}) = ∅ and e_{i}^{c} = ^{c}e_{i+1}.

Sequences satisfying the above conditions are necessarily finite as the size of control conditions strictly decreases along the sequence. The events of the net are already associated with input and output actions. The net and strand space behaviour are closely related:

Theorem 8.3 Given p a !-par process and s set of names containing all names in p, we have that:

1. The sequence of events in a finite run in Net(p) from the initial configuration ⟨p, s, ∅⟩ is an event-linearisation of a bundle over T r(p, s).

2. Every bundle over T r(p, s) can be re-indexed so that any of its event-linearisations is a run in Net(p).

The only way a strand space can cope with there being a nonempty set of initial output messages is through the slight clumsiness of introducing extra output events; we avoid this above by assuming the initial set of output messages is empty.

8.2 Inductive rules

Paulson’s inductive rules for a security protocol capture the actions it and a spy can perform [Pau98]. Through allowing persistent conditions, we can represent a collection of inductive rules as a net in which the events stand for rule instances and runs to sequences of rule instances which form a derivation from the rules. In particular, instances of inductive rules for security protocols can be represented as events in a net for which all but the name conditions are persistent. According to such a semantics, once a protocol can input it can do so repeatedly. Once it can output generating new names it can do so repeatedly, provided this doesn’t lead to clashes with names already in use. Paulson’s traces and the associated runs of the net will necessarily include such “stuttering.”

We define a net of rule instances from a closed process term. Take the set of “rule-conditions” to consist of name conditions and persistent output conditions, as before, but now with additional persistent conditions consisting of closed input and output process terms. Let r be the function from SPL-conditions to rule-conditions which removes the indices tagging control conditions and leaves output and name conditions unchanged. Extend r to SPL-events: let r replace all the control conditions of an SPL-event by their images under r—intuitively, an event is replaced by a rule instance. Define the “net of rule instances” R(p) of a closed process term p to be the net with rule-conditions and events the image r Ev(p).

For a closed process term p, let p^{∗} be the process term obtained by inserting a replication before every input and output process subterm in p. Note that R(p^{∗}) = R(p) as R drops indices. Now, having restricted to a process with sufficient replication, we can establish a close relation between the behaviours of Net(p^{∗}) and R(p^{∗}).

Theorem 8.4 Let p be a closed process term. Let t be a subset of closed messages and s a subset of names including those of p and t. Let M_{0} = Ic(p^{∗}) ∪ s ∪ t.

1. A run M_{0} ⟶^{e_{1}} ⋯ ⟶^{e_{l}} M_{l} of Net(p^{∗}) yields rM_{0} ⟶^{r(e_{1})} ⋯ ⟶^{r(e_{l})} rM_{l}

a run of R(p^{∗}).

2. If M′_{0} ⟶^{e′_{1}} ⋯ ⟶^{e′_{l}} M′_{l} is a run of R(p^{∗}) with M′_{0} = rM_{0}, then

there is a run M_{0} ⟶^{e_{1}} ⋯ ⟶^{e_{l}} M_{l} of Net(p^{∗}), with r(e_{i}) = e′_{i} and r(M_{i}) = M′_{i} for all i, 0 < i ≤ l.

8.3 Basic nets, trace languages and event structures

Because strand spaces can be easily turned into event structures, Section 8.1 yields an event structure for each !-par process. But, without any restrictions, we can relate the net semantics to traditional independence models such as event structures and Mazurkiewicz trace languages. The crux of the construction is that of eliminating the persistent conditions from the net Net(p), of a closed process term p, in an initial marking Init(p) ∪ s ∪ t, to produce a basic net. It’s well-known how to “unfold” a basic net to a Mazurkiewicz trace language and event structure. Assume Net(p) has input events In and output events Out. Then:

Theorem 8.5 There is a basic net N with events

E = Out
∪ {(∗, e) | e ∈ In & ^{o}e ⊆ t}
∪ {(e_{1}, e) | e ∈ In & e_{1} ∈ Out & ^{o}e = e_{1}^{o}}

Let the map σ : E → Out∪In leave events in Out unchanged and project pairs (∗, e), (e_{1}, e) to the component e.

i) If N has a run with events e′_{1}, ⋯, e′_{k}, then there is a run with events σ(e′_{1}), ⋯, σ(e′_{k}) of Net(p) from the initial marking Init(p) ∪ s ∪ t.

ii) If Net(p) has a run e_{1}, ⋯, e_{k} from the initial marking Init(p)∪s∪t, then N has a run e′_{1}, ⋯, e′_{k} where e_{1}, ⋯, e_{k} = σ(e′_{1}), ⋯, σ(e′_{k}).

The construction used to obtain N above is an example of the construction for eliminating colours from a coloured net—see [Win87b]; first colours are introduced to the persistent conditions and input events of Net(p) to distinguish the different ways in which they are made to occur, and then eliminated through splitting the conditions and events according to their colours. The result in this case is a basic net. Its runs form a Mazurkiewicz trace language from which we can then obtain an event structure–see [WN95] for details.

Appendix

A Petri nets

The explanation of general Petri nets involves a little algebra of multisets (or bags), which are like sets but where multiplicities of elements matters. It’s convenient to also allow infinite multiplicities, so we adjoin an extra element ∞ to the natural numbers, though care must be taken to avoid subtracting ∞. ∞-Multisets support addition + and multiset inclusion ≤, and even multiset subtraction X − Y provided Y ≤ X and Y has no infinite multiplicities, in which case we call Y simply a multiset.

A.1 General Petri nets

A general Petri net (often called a place-transition system) consists of

• a set of conditions (or places), P,

• a set of events (or transitions), T,

• a precondition map pre, which to each t ∈ T assigns a multiset pre(t) over P. It is traditional to write ^{·}t for pre(t).

• a postcondition map post which to each t ∈ T assigns an ∞-multiset post(t) over P, traditionally written t^{·}.

• a capacity function Cap which is an ∞-multiset over P, assigning a nonnegative number or ∞ to each condition p, bounding the multiplicity to which the condition can hold; a capacity of ∞ means the capacity is unbounded.

A state of a Petri net consists of a marking which is an ∞-multiset M over P bounded by the capacity function, i.e.

M ≤ Cap .

A marking captures a notion of distributed, global state. Token game for general nets: Markings can change as events occur, precisely how being expressed by the transitions

M →^{t} M′

events t determine between markings M and M′. For markings M, M′ and t ∈ T, define

M ⟶^{t} M′ iff ^{·}t ≤ M and M′ = M −^{·}t + t^{·} .

An event t is said to have concession (or be enabled) at a marking M iff its occurrence would lead to a marking, i.e.iff

·t ≤ M and M −^{·}t + t^{·} ≤ Cap .

There is a widely-used graphical notation for nets in which events are represented by squares, conditions by circles and the pre- and postcondition maps by directed arcs carrying numbers or ∞. A marking is represented by the presence of tokens on a condition, the number of tokens representing the multiplicity to which the condition holds. When an event with concession occurs tokens are removed from its preconditions and put on its postconditions with multiplicities according to the pre- and postcondition maps. Because of this presentation, the transition relation on Petri nets is described as the “token game”.

B Basic nets

We instantiate the definition of general Petri nets to an important case where in all the multisets the multiplicities are either 0 or 1, and so can be regarded as sets. In particular, we take the capacity function to assign 1 to every condition, so that markings become simply subsets of conditions. The general definition now specialises to the following.

A basic Petri net consists of

• a set of conditions, B,

• a set of events, E, and

• two maps: a precondition map pre : E→Pow(B), a postcondition map post : E → Pow(B). We can still write^{·}e for the preconditions and e^{·} for the postconditions of e ∈ E and we require ^{.}e ∪ e^{.} ≠ ∅.

Now a marking consists of a subset of conditions, specifying those conditions which hold. Token game for basic nets: Markings can change as events occur, precisely how being expressed by the transitions

M →^{e} M′

events e determine between markings M, M′.

For M, M′ ⊆ B and e ∈ E, define

M →^{e} M′ iff (1) ^{·}e ⊆ M & (M \^{·}e) ∩ e^{·} = ∅ (Concession), and
(2) M′ = (M \^{·}e) ∪ e^{·} .

Property (1) expresses that the event e has concession at the marking M. Returning to the definition of concession for general nets, of which it is an instance, it ensures that the event does not load another token on a condition that is already marked. Property (2) expresses in terms of sets the marking that results from the occurrence of an event. So, an occurrence of the event ends the holding of its preconditions and begins the holding of its postconditions. (It is possible for a condition to be both a precondition and a postcondition of the same event, in which case the event is imagined to end the precondition before immediately restarting it.)

There is contact at a marking M when for some event e

·e ⊆ M & (M \^{·}e) ∩ e^{·} ≠ ∅.

The occurrence of an event is blocked through conditions, which it should begin, holding already. Blocking through contact is consistent with the understanding that the occurrence of an event should end the holding of its preconditions and begin the holding of its postconditions; if the postconditions already hold, and are not also preconditions of the event, then they cannot begin to hold on the occurrence of the event. Avoiding contact ensures the freshness of names in the semantics of name creation.

Basic nets are important because they are related to many other models of concurrent computation, in particular, Mazurkiewicz trace languages (languages subject to trace equivalence determined by the independence of actions) and event structures (sets of events with extra relations of causality and conflict)—see [WN95].

C Nets with persistent conditions

Sometimes we have use for conditions which once established continue to hold and can be used repeatedly. This is true of assertions in traditional logic, for example, where once an assertion is established to be true it can be used again and again in the proof of further assertions. Similarly, if we are to use net events to represent rules of the kind we find in inductive definitions, we need conditions that persist.

Persistent conditions can be understood as an abbreviation for conditions within general nets which once they hold, do so with infinite multiplicity. Consequently any number of events can make use of them as preconditions but without their ever ceasing to hold. Such conditions, having unbounded capacity, can be postconditions of several events without there being conflict.

To be more precise, we modify the definition of basic net given above by allowing certain conditions to be persistent. A net with persistent conditions will still consist of events and conditions related by pre- and postcondition maps which to an event will assign a set of preconditions and a set of postconditions. But, now amongst the conditions are the persistent conditions forming a subset P. A marking of a net with persistent conditions will be simply a subset of conditions, of which some may be persistent. Nets with persistent conditions have arisen independently several times and have been studied for example in contextual nets [MR95].

A net with persistent conditions can be understood on its own terms, or as standing for a general net with the same sets for conditions and events. The general net’s capacity function will be either 1 or ∞ on a condition, being ∞ precisely on the persistent conditions. When p is persistent, p ∈ e^{·} is interpreted in the general net as (e^{·})_{p} = ∞, and p ∈ ^{·}e as (^{·}e)_{p} = 1. A marking of a net with persistent conditions will correspond to a marking in the general Petri net in which those persistent conditions which hold do so with infinite multiplicity.

Graphically, we’ll distinguish persistent conditions by drawing them as double circles:

[figure]

Token game with persistent conditions: The token game is modified to account for the subset of conditions P being persistent. Let M and M′ be markings (i.e. subsets of conditions), and e an event. Define

M →^{e} M′ iff ^{·}e ⊆ M & (M \ (^{.}e ∪ P)) ∩ e^{·} = ∅ (e has concession), and
M′ = (M \^{·}e) ∪ e^{·} ∪ (M ∩ P) .

The token game fits our understanding of persistence, and specifically it matches the token game in its interpretation as a general net. In this paper, these special contextual nets are used in modelling and analysing security protocols.

D The events of NSL

We can classify the events Ev(NSL) involved in the NSL protocol. Initiator events:

Out(Init(A, B); m):

[figure: {m, A}_{P ub(B)}; m; Init(A, B); in{m, y, B}_{P ub(A)}out{y}_{P ub(B)}; out new m {m, A}_{P ub(B)}]

In(in{m, y, B}_{P ub(A)}out{y}_{P ub(B)}; n):

[figure: {m, n, B}_{P ub(A)}; in{m, y, B}_{P ub(A)}out{y}_{P ub(B)}; out{n}_{P ub(B)}; in{m, n, B}_{P ub(A)}]

Out(out{n}_{P ub(B)}):

[figure: {n}_{P ub(B)}; out{n}_{P ub(B)}; out{n}_{P ub(B)}]

Responder events: In(Resp(B); m, A):

[figure: {m, A}_{P ub(B)}; Resp(B); out new y {m, y, B}_{P ub(A)}.in {y}_{P ub(B)}; in {m, A}_{P ub(B)}]

Out(out new y {m, y, B}_{P ub(A)}.in {y}_{P ub(B)}; n):

[figure: {m, n, B}_{P ub(A)}; n; out new y {m, y, B}_{P ub(A)}.in {y}_{P ub(B)}; in {n}_{P ub(B)}; out new n {n, B}_{P ub(A)}]

In(in {n}_{P ub(B)}):

[figure: {n}_{P ub(B)}; in {n}_{P ub(B)}; in {n}_{P ub(B)}]

Spy events: Composing, Spy_{1} ≡ in ψ_{1}.in ψ_{2}.out(ψ_{1}, ψ_{2}):

[figure: M_{1}; M_{2}; (M_{1}, M_{2})]

Decomposing, Spy_{2} ≡ in(ψ_{1}, ψ_{2}).out ψ_{1}.out ψ_{2}:

[figure: (M_{1}, M_{2}); M_{1}; M_{2}]

Encryption, Spy_{3} ≡ in x.in ψ.out {ψ}_{P ub(x)}:

[figure: n; M; {M}_{P ub(n)}]

Decryption, Spy_{4} ≡ in P riv(x).in {ψ}_{P ub(x)}.out ψ:

[figure: P riv(n); {M}_{P ub(n)}; M]

References

[AG97] M. Abadi and A. Gordon. A calculus for cryptographic protocols: The Spi calculus. In Proceedings of the Fourth ACM Conference on Computer and Communications Security. ACM Press, 1997.

[CDL^{+}99] I. Cervesato, N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. A meta-notation for protocol analysis. In R. Gorrieri, editor, Proceedings of the 12th IEEE Computer Security Foundations Workshop - CSFW’99, pages 55–69, Mordano, Italy, 28–30 June 1999. IEEE Computer Society Press.

[CDL^{+}00] I. Cervesato, N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. Relating strands and multiset rewriting for security protocol analysis. In P. Syverson, editor, 13th IEEE Computer Security Foundations Workshop - CSFW’00, Cambridge, UK, 3-5 July 2000. IEEE Computer Society Press.

[Low96] G. Lowe. Breaking and fixing the Needham-Schroeder publickey protocol using FDR. In 2nd International Workshop on Tools and Algorithms for the construction and Analysis of Systems. Springer-Verlag, 1996.

[Mil99] R. Milner. Communicating and mobile systems: The πcalculus. Cambridge University Press, 1999.

[MR95] U. Montanari and F. Rossi. Contextual nets. Acta Informatica, (32), 1995.

[NT92] B. B. Nieh and S. E. Tavares. Modelling and analyzing cryptographic protocols using Petri Nets. In Advances in Cryptology-AUSCRYPT ’92, volume 718 of LNCS, pages 275– 295. Springer-Verlag, 1992.

[Pau98] L. C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.

[Pau99] L. C. Paulson. Proving security protocols correct. In Proceedings of the 14th Symposium on Logic in Computer Science, July 1999.

[PS93] A. M. Pitts and I. Stark. Observable properties of higher order functions that dynamically create local names, or: What’s new? In Mathematical Foundations of Computer Science, Proc. 18th Int. Symp., Gdańsk, 1993, volume 711 of Lecture Notes in Computer Science, pages 122–141. Springer-Verlag, Berlin, 1993.

[RSA78] R. L. Rivest, A. Shamir, and L. Adleman. A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM, 21(2):120–126, 1978.

[THG98a] J. Thayer, J. Herzog, and J. Guttman. Honest ideals on strand spaces. In Proceedings of the 11th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, 1998.

[THG98b] J. Thayer, J. Herzog, and J. Guttman. Strand space pictures. Workshop on Formal Methods and Security Protocols, Indianapolis, Indiana, June 1998.

[THG98c] J. Thayer, J. Herzog, and J. Guttman. Strand spaces: Why is a security protocol correct? In 1998 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, 1998.

[Win87a] G. Winskel. Event structures. In Proceedings of the Advanced Course on Petri nets, volume 255 of LNCS. Springer–Verlag, 1987.

[Win87b] G. Winskel. Petri nets, algebras, morphisms, and compositionality. Information and Computation, 72:197–238, 1987.

[WN95] G. Winskel and M. Nielsen. Models for concurrency, volume IV. Oxford University Press, 1995.

Recent BRICS Report Series Publications

RS-01-13 Federico Crazzolara and Glynn Winskel. Events in Security Protocols. April 2001. 30 pp.

RS-01-12 Torben Amtoft, Charles Consel, Olivier Danvy, and Karoline Malmkjær. The Abstraction and Instantiation of String-Matching Programs. April 2001.

RS-01-11 Alexandre David and M. Oliver Möller. From HUppaal to Uppaal: A Translation from Hierarchical Timed Automata to Flat Timed Automata. March 2001. 40 pp.

RS-01-10 Daniel Fridlender and Mia Indrika. Do we Need Dependent Types? March 2001. 6 pp. Appears in Journal of Functional Programming, 10(4):409–415, 2000. Superseeds BRICS Report RS-98-38.

RS-01-9 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. Static Validation of Dynamically Generated HTML. February 2001. 18 pp.

RS-01-8 Ulrik Frendrup and Jesper Nyholm Jensen. Checking for Open Bisimilarity in the π-Calculus. February 2001. 61 pp.

RS-01-7 Gregory Gutin, Khee Meng Koh, Eng Guan Tay, and Anders Yeo. On the Number of Quasi-Kernels in Digraphs. January 2001. 11 pp.

RS-01-6 Gregory Gutin, Anders Yeo, and Alexey Zverovich. Traveling Salesman Should not be Greedy: Domination Analysis of Greedy-Type Heuristics for the TSP. January 2001. 7 pp.

RS-01-5 Thomas S. Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. Linear Parametric Model Checking of Timed Automata. January 2001. 44 pp. To appear in Margaria and Yi, editors, Tools and Algorithms for The Construction and Analysis of Systems: 7th International Conference, TACAS ’01 Proceedings, LNCS, 2001.

RS-01-4 Gerd Behrmann, Ansgar Fehnker, Thomas S. Hune, Kim G. Larsen, Paul Pettersson, and Judi Romijn. Efficient Guiding Towards Cost-Optimality in Uppaal. January 2001. 21 pp. To appear in Margaria and Yi, editors, Tools and Algorithms for The Construction and Analysis of Systems: 7th International Conference, TACAS ’01 Proceedings, LNCS, 2001.