BRICS RS-02-5 Crazzolara & Winskel: Composing Strand Spaces BRICS

Basic Research in Computer Science

Composing Strand Spaces

Federico Crazzolara Glynn Winskel BRICS Report Series RS-02-5 ISSN 0909-0878 February 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, 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/02/5/

Composing strand spaces

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

Computer Laboratory University of Cambridge

Abstract

The strand space model for the analysis of security protocols is known to have some limitations in the patterns of nondeterminism it allows and in the ways in which strand spaces can be composed. Its successful application to a broad range of security protocols may therefore seem surprising. This paper gives a formal explanation of the wide applicability of strand spaces. We start with an extension of strand spaces which permits several operations to be defined in a compositional way, forming a process language for building up strand spaces. We then show, under reasonable conditions how to reduce the extended strand spaces to ones of a traditional kind. For security protocols we are mainly interested in their safety properties. This suggests a strand-space equivalence: two strand spaces are equivalent if and only if they have essentially the same sets of bundles. However this equivalence is not a congruence with respect to the strandspace operations. By extending the notion of bundle we show how to define the strand-space operations directly on “bundle spaces”. This leads to a characterisation of the largest congruence within the strand-space equivalence. Finally, we relate strand spaces to event structures, a well known model for concurrency.

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

Contents

1 Introduction 2

2 Strand spaces 4

3 Strand spaces with conflict 6

4 Constructions on strand spaces 10

5 A process language for strand spaces 14

6 Bundle spaces 15

7 A strand space congruence 19

8 Eliminating conflict 22

9 Event structures from strand spaces 25

1 Introduction

Security protocols describe a way of exchanging data over an untrusted medium so that, for example, data is not leaked and authentication between the participants in the protocol is guaranteed. 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. Typically, a secrecy property (or some strengthening of it) is established by showing that there cannot be an earliest event in the causal dependency which violates the property, while authentication is often established by showing certain events of one agent depend on certain events of another. The method of strand spaces [THG98b, THG98a, TG00] has been designed to support such an intensional, event-based, style of reasoning and has successfully been applied to a broad number of security protocols.

Security properties such as secrecy and authentication or even anonymity can be expressed as safety properties, properties which stand or fall according to whether they hold for all finite behaviours. The results in this paper express the adequacy of strand spaces and relate strand spaces to event structures only with respect to the languages i.e. sets of finite behaviours, they generate. This is not unduly restrictive however as in security protocols we are mainly interested in safety properties.

When we were relating strand spaces to a Petri-net semantics for a process language designed to describe security protocols [CW01], we had to 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. That strand spaces are able to tackle a broad class of security protocols may therefore seem surprising. A reason for the adequacy of strand spaces lies in the fact that they can sidestep conflict if there are enough replicated strands available, which is the case for a broad range of security protocols.

This paper has four main objectives. Firstly it extends the strand space formalism to allow several operations on strand spaces to be defined. The operations form a strand-space language. Secondly the wide applicability of strand spaces to numerous security protocols and properties is backed up formally. The paper documents part of the work done in proving the relation between nets and strand spaces we reported in [CW01]. Thirdly we address another issue of compositionality. Because we are only interested in safety properties we can make do with languages of strand-space bundles as models of process behaviour. We show how to compose such languages so that they may be used directly in giving the semantics of security protocols. Strand spaces that have substantially the same bundles can be regarded as equivalent and are congruent if they exhibit substantially the same open bundles. This congruence lays the ground for equational reasoning between strand spaces. Finally we show how strand spaces relate to event structures.

In Section 2 we briefly introduce the strand space formalism in its traditional form and discuss some limitations. Section 3 shows how to extend strand spaces in order to compose them, chiefly with conflict to permit their nondeterministic sum. A treatment of “unique origination” on the bundle rather than on the strand space allows us to define parallel composition of strand spaces by juxtaposition. The operations of prefixing, parallel composition and nondeterministic sum of strand spaces are illustrated in Section 5 and form a language for strand spaces. In Section 7 we give a congruence relation between terms of the strand-space language based on the underlying bundle languages studied in Section 6. In Section 8 we show that conflict can be eliminated, without upsetting the strand-space behaviour if enough “replication” is introduced. Section 9 describes how strand spaces relate to event structures.

2 Strand spaces

We briefly introduce the strand space formalism of [THG98b] and discuss some apparent limitations.

A strand spaces consists of ⟨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 output or input actions of the kind outM or inM respectively with M a message built up by encryption and pairing from a set of values (here names) and keys. In the rest of this paper we use n, n_{0} to indicate names, A, B, A_{0}, B_{0} to indicate special names which are agent identifiers, and k standing for a cryptographic key. A name whose first appearance in a strand is on an output message, is said to be originating on that strand. A value is said to be uniquely originating on a strand space if it is originating on only one of its strands.

A strand space has an associated graph whose nodes identify an event of a strand by strand index and position of the event in that strand. Edges are between output and input events concerning the same message and between consecutive events on a same strand. Bundles model protocol runs. A bundle selects from the events of a strand space those that occur in a run of the protocol and shows the causal dependencies among them which determine the partial order of the events in the run. A bundle is a finite and acyclic subgraph of the strand space graph. Each node in the bundle requires all events that precede it on the same strand (together with the edges that denote the strand precedence). Moreover each input node in the bundle has exactly one incoming edge from an output node.

As an example consider a simplified version of the ISO symmetric key two-pass unilateral authentication protocol (see [CJ97]):

\begin{matrix}A → B : n \\ B → A : \{n, A\}_{k} \end{matrix}

Agents can engage in a protocol exchange under two different roles. The initiator, here A and the responder, here B. In a protocol round the initiator A chooses a fresh name n and sends it to the responder B. After

\xymatrix{out n_{0} \ar[r] \ar@{=>}[d] & in n_{0} \ar@{=>}[d] & … & out n_{i} \ar[r] \ar@{=>}[d] & in n_{i} \ar@{=>}[d] & … \\ in \{n_{0}, A_{0}\}_{k} & out \{n_{0}, A_{0}\}_{k} \ar[l] &  & in \{n_{i}, A_{0}\}_{k} & out \{n_{i}, A_{0}\}_{k} \ar[l]}

Figure 1: ISO protocol

getting the value, B encrypts it together with the initiator’s identifier using a common shared key k. After getting the answer to her challenge, A can decrypt using the shared key and check whether the value sent matches the value received. In that case A can conclude that B is in fact operational. The strand space graph in Figure 1 describes the simple case of only two agents, A_{0} and B_{0}, acting as initiator and responder respectively. For simplicity the graph has been drawn using the actions labelling the events in place of the events themselves. In this simple case the strand space itself forms a bundle. All the names n_{i} are uniquely originating on that strand space.

Unique origination intends to describe a name as fresh, perhaps chosen at random, and under the assumptions of Dolev and Yao [DY83], unguessable. For a construction of parallel composition of strand spaces it is therefore reasonable to require that names uniquely originating on components remain so on the composed strand space. Simple juxtaposition of strand spaces does not ensure this. For example consider a strand space for the ISO protocol which allows both agents A_{0} and B_{0} to engage in the protocol in any of the two possible roles. In Figure 2 the strand space formed out of two copies of the one in Figure 1. Figure 3 shows a possible bundle on such strand space. It describes a protocol run with two complete rounds. One in which A_{0} is initiator and B_{0} responder and another where the roles are inverted. Though the name n_{0} is no longer uniquely originating on that strand space. A name’s freshness is with respect to a run of a protocol more than to the whole set of possible executions. A notion of unique origination “on the bundle” seems more appropriate.

Nondeterminism in strand spaces arises only through the choice in a bundle of where input comes from. There is no recognisable way of modelling situations in which bundles may be taken either only over one strand space or over another. Juxtaposing strands as we did for example in Figure 2 allows bundles to include events of both components as is the

\xymatrix{out n_{0} \ar[r] \ar@{=>}[d] \ar[ddr] & in n_{0} \ar@{=>}[d] & … & out n_{i} \ar[r] \ar@{=>}[d] \ar[ddr] & in n_{i} \ar@{=>}[d] \\ in \{n_{0}, A_{0}\}_{k} & out \{n_{0}, A_{0}\}_{k} \ar[l] &  & in \{n_{i}, A_{0}\}_{k} & out \{n_{i}, A_{0}\}_{k} \ar[l] \\ out n_{0} \ar[r] \ar[uur] \ar@{=>}[d] & in n_{0} \ar@{=>}[d] &  & out n_{i} \ar[r] \ar[uur] \ar@{=>}[d] & in n_{i} \ar@{=>}[d] \\ in \{n_{0}, B_{0}\}_{k} & out \{n_{0}, B_{0}\}_{k} \ar[l] &  & in \{n_{i}, B_{0}\}_{k} & out \{n_{i}, B_{0}\}_{k} \ar[l]}

Figure 2: ISO protocol - symmetric roles

\xymatrix{out n_{0} \ar@{=>}[d] \ar[ddr] \ar[r] & in n_{0} \ar@{=>}[d] \\ in \{n_{0}, A_{0}\}_{k} & out \{n_{0}, A_{0}\}_{k} \ar[l] \\ out n_{0} \ar@{=>}[d] & in n_{0} \ar@{=>}[d] \\ in \{n_{0}, B_{0}\}_{k} & out \{n_{0}, B_{0}\}_{k} \ar[l]}

Figure 3: A possible bundle

case for the bundle in Figure 3.

One seems to encounter even more difficulties in the attempt to define a construction of prefixing a strand space with an action. Strands can’t branch to parallel sub-strands and prefixing each strand of the space with an action would cause as many repetitions of that action as there are strands participating in a bundle.

3 Strand spaces with conflict

In this section we extend the definition of strand space, introducing a notion of conflict, which we adapt from event structures (see e.g.[Win88]). We differ from the original definition of strand spaces 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 a similar effect as to unique origination and are related.

As mentioned in the previous section, the strands of a strand space consist of sequences of output and input actions. Actions are

Act = {out new n⃗ M | M msg, n⃗ distinct names} ∪ {in M | M msg}.

In out new n⃗ M, the list n⃗ contains distinct names that are intended to be fresh (“uniquely originating”) at the event.

Definition 3.1 A strand space with conflict (⟨s_{i}⟩_{i∈I}, #) consists of:

(i) ⟨s_{i}⟩_{i∈I} an indexed set of strands. An individual stand s_{i}, where i ∈ I, is a finite sequence of output or input actions in Act.

(ii) # ⊆ I ×I a symmetric, irreflexive binary conflict relation on strand indexes.

Strand spaces with an empty conflict relation correspond to those of the standard definition of [THG98b]. We denote by ϵ the empty strand space with no strands and with an empty conflict relation. ^{1} If λ stands for an empty sequence of actions then the empty strand space is different to a strand space where each strand is the empty sequence of actions (⟨λ⟩_{i∈I}, #). We write |s| for the length of the sequence s. Given a strand space (⟨s_{i}⟩_{i∈I}, #), given an index j ∈ I, and given l such that 1 ≤ l ≤ |s_{j}| we write act(j, l) for the action at position l in s_{j}.

Given a strand space (⟨s_{i}⟩_{i∈I}, #), we can find a strand-space graph

(E, ⇒, →)

associated with it as usual (see [THG98b]). The graph has nodes (events)

E = {(i, l) | i ∈ I , 1 ≤ l ≤ |s_{i}|}

and edges

• (i, l) ⇒ (i, l + 1) iff (i, l), (i, l + 1) ∈ E,

• (i, l) → (j, h) iff act(i, l) = out new n⃗ M and act(j, h) = in M.

1We won’t make much use of this particular strand space; it is however the identity for the operations of parallel composition and nondeterministic sum of strand spaces.

For the components of G strand-space graph or subgraph of the strandspace graph we often write E_{G}, ⇒_{G}, and →_{G}, and we write

≤_{G}= (⇒_{G} ∪ →_{G})^{∗}

for the reflexive and transitive closure of the relation ⇒_{G} ∪ →_{G}. We refer to →_{G} as the communication edges of G. The names of a node e are all the names appearing on the action associated with e – the ones that are marked as “new” together with those in the message of the action. Write names(e) for the names of node e. We say that an event is an input event if the action associated with it is an input action and we say an event is an output event if its action is an output.

Bundles of a strand space describe runs in a computation.

Definition 3.2 A bundle b of a strand space (⟨s_{i}⟩_{i∈I}, #) is a finite, acyclic subgraph of G the graph of (⟨s_{i}⟩_{i∈I}, #) such that:

(i) if e ⇒_{G} e′ and e′ ∈ E_{b} then e ⇒_{b} e′, (control precedence)

(ii) if e ∈ E_{b} and act(e) = in M then there exists a unique e′ ∈ E_{b} such that e′ →_{b} e, (output-input precedence)

(iii) if e, e′ ∈ E_{b} such that act(e) = out new n⃗ M and n ∈ v⃗ ∩ names(e′) then either e ⇒_{b}^{∗} e′ or there exists an input event e′′ such that n ∈ names(e′′) and e′′ ⇒_{b}^{∗} e′, (freshness)

(iv) if (i, h), (j, k) ∈ E_{b} then ¬(i # j). (conflict freeness)

The empty graph, denoted by λ, is a bundle. It will be clear from the context whether λ stands for the empty bundle or whether it denotes the empty sequence of actions. The empty strand space has only one bundle, the empty bundle.

The first two points of the definition of bundle for a strand space with conflict match with the standard definition of [THG98b]. There are two additional requirements. Point (iii) ensures freshness of “new” values in a bundle. Point (iv) doesn’t allow events from conflicting strands to appear in a bundle.

Proposition 3.3 If b is a bundle then ≤_{b} is a partial order on E_{b}.

Proof. A bundle is an acyclic subgraph of the strand-space graph. □

The relation ≤_{b} determines the partial order that events respect when occurring in a computation described by the bundle. As one would expect, names that are introduced as “new” don’t appear on events preceding their introduction and are never introduced as “new” more than once.

Proposition 3.4 Let b be a bundle of a strand space. If e, e′ ∈ E_{b} such that act(e) = out new n⃗ M and n ∈ v⃗ ∩ names(e′) then e ≤_{b} e′ and if act(e′) = out new m⃗ M′ then n ∉ m⃗.

Proof. Suppose that e ≰_{b} e′ and therefore e ⇏^{∗} e′. There exists an input event e′′ ∈ b such that n ∈ names(e′′) and e′′ ⇒_{b}^{∗} e′ (freshness). The bundle b is acyclic and each input event in b is preceded by a matching output event (output-input precedence). Therefore there exists an output event e_{1} ∈ E_{b} such that n ∈ names(e_{1}) and such that for every input event e_{2} if e_{2} ⇒_{b}^{∗} e_{1} then n ∉ names(e_{2}). The event e can’t precede e_{1} on the same strand (e ⇏_{b}^{∗} e_{1}), otherwise e ≤_{b} e′. The events e and e_{1} are both in b thus contradicting the freshness property of b.

If act(e′) = out new m⃗ M′ and n ∈ m⃗ then e ≤_{b} e′ and e′ ≤_{b} e, and therefore e = e′. □

There are other possible choices for the freshness condition (iii). A weaker condition could be the following:

if e, e′ ∈ E_{b} such that act(e) = out new n⃗ M and such that
n ∈ v⃗ ∩ names(e′) then e ≤_{b} e′.

This condition however would allow bundles of the kind

\xymatrix{out new n M \ar@{=>}[d] & in m \ar@{=>}[d] \\ out m \ar[ur] & out n}

If the two strands are distinct processes, the second strand is not supposed to send the name n without receiving it first from somewhere. Graphs like that are not considered bundles in the original treatment of strand spaces [THG98b] and are also excluded by the slightly more involved freshness condition of Definition 3.2.

We regard two strand spaces as equivalent if they differ only on the indexes of their strands and therefore one strand space can be obtained from the other by a simple “re-indexing” operation. ^{2} Definition 3.5 Given (⟨s_{i}⟩_{i∈I}, #) and (⟨t_{j}⟩_{j∈J}, #′) two strand spaces write (⟨s_{i}⟩_{i∈I}, #) ≅ (⟨t_{j}⟩_{j∈J}, #′) if there exists a bijection σ : I → J such that:

2If the indexes carry structure (some might involve agent names for example) we might refine the permissible re-indexings.

(i) ∀i ∈ I . s_{i} = t_{σ(i)} and

(ii) ∀i, j ∈ I . i # j ⇔ σ(i) #′ σ(j).

The relation ≅ is an equivalence relation on strand spaces. A bijection σ which establishes such equivalence is called a re-indexing of strand spaces. Moreover take (⟨s_{i}⟩_{i∈I}, #) a strand space, J a set, and σ : I → J a bijection. We define the strand space (⟨t_{j}⟩_{j∈J}, σ(#)) where

• ∀j ∈ J . t_{j} = s_{σ^{−1}(j)} and

• ∀j, j′ ∈ J . j σ(#) j′ iff σ^{−1}(j) # σ^{−1}(j′).

The relation σ(#) is irreflexive and symmetric and establishes the equivalence (⟨s_{σ(i)}⟩_{i∈I}, σ(#)) ≅ (⟨s_{i}⟩_{i∈I}, #).

Proposition 3.6 Let (⟨s_{i}⟩_{i∈I}, #) and (⟨t_{j}⟩_{j∈J}, #′) be two strand spaces such that (⟨s_{i}⟩_{i∈I}, #) ≅ (⟨t_{j}⟩_{j∈J}, #′) for a bijection σ : I → J. Given b a bundle of (⟨s_{i}⟩_{i∈I}, #) then σ(b) obtained from b by changing all strand indexes according to σ is a bundle of (⟨t_{j}⟩_{j∈J}, #′).

Proof. Follows from the assumption that b is a bundle and from the definition of re-indexing on bundles. □

4 Constructions on strand spaces

The extension of the strand-space formalism with a conflict relation and the different treatment of unique origination as illustrated in the previous section allow operations such as prefixing, parallel composition, and sum of strand spaces to be defined in terms of traditional process operations.

The operation of prefixing a strand space with an action is complicated by the strand-space formalism not permitting strands to branch. Only if the strand space to be prefixed is such that every two different strands are in conflict can each strand be prefixed with the action. The conflict relation in this case doesn’t allow repetitions of the prefixing action in bundles. Given α an action and given a strand space (⟨s_{i}⟩_{i∈I}, #) such that for all i, j ∈ I if i ≠ j then i#j, define

α.(⟨s_{i}⟩_{i∈I}, #) =^{def} (⟨αs_{i}⟩_{i∈I}, #) .

We understand the special case of prefixing the empty strand space with an action, to yield the empty strand space:

α.ϵ = ϵ .

For example, when prefixing a strand space consisting of only empty strands one obtains a strand space with the same number of strands each one with only one action, the prefixing action. More precisely

α.(⟨λ⟩_{i∈I}, #) = (⟨α⟩_{i∈I}, #) .

The operation of parallel composition of two strand spaces is the disjoint union of their sets of strands and conflict relations. Disjoint union is achieved by tagging the first space with index 0 and the second with index 1. Given strand spaces (⟨s_{i}^{0}⟩_{i∈I}, #^{0}) and (⟨s_{j}^{1}⟩_{j∈J}, #^{1}) define

(⟨s_{i}^{0}⟩_{i∈I}, #^{0}) || (⟨s_{j}^{1}⟩_{j∈J}, #^{1}) =^{def} (⟨s_{h}⟩_{h∈H}, #)

where H = ({0} × I) ∪ ({1} × J), s_{(0,i)} = s_{i}^{0} and s_{(1,i)} = s_{i}^{1}. Two strands are in conflict only if they belong to the same component of the parallel composition and are in conflict within that component. More precisely for k either 0 or 1 define h # h′ if h = (k, i), h′ = (k, j) and i #^{k} j.

The operation of nondeterministic sum of two strand spaces constructs the same indexed set of strands as the operation of parallel composition. The conflict relation of a summed space however, in addition to the existing conflicts, imposes conflict between every two strands that belong to different components. Given strand spaces (⟨s_{i}^{0}⟩_{i∈I}, #^{0}) and (⟨s_{j}^{1}⟩_{j∈J}, #^{1}) define

(⟨s_{i}^{0}⟩_{i∈I}, #^{0}) + (⟨s_{j}^{1}⟩_{j∈J}, #^{1}) =^{def} (⟨s_{h}⟩_{h∈H}, #)

where H = ({0} × I) ∪ ({1} × J), s_{(0,i)} = s_{i}^{0} and s_{(1,i)} = s_{i}^{1}. Two strands are in conflict only if they belong to different components or are already in conflict within a component. More precisely for k and k′ either 0 or 1 define (k, i) # (k′, j) if k ≠ k′ or if k = k′ and i #^{k} j.

In both operations of strand-space composition the relation # is irreflexive and symmetric.

The operations of parallel composition and nondeterministic sum satisfy some desired properties with respect to the equivalence ≅ of strand spaces:

Proposition 4.1 Let S_{0} , S_{1}, and S_{2} be strand spaces.

1. S_{0}||ϵ ≅ S_{0}

2. S_{0}||(S_{1}||S_{2}) ≅ (S_{0}||S_{1})||S_{2}

3. S_{0}||S_{1} ≅ S_{1}||S_{2}

and similarly for +.

Proof. Let S_{0} = (⟨s_{i}^{0}⟩_{i∈I}, #^{0}), S_{1} = (⟨s_{j}^{1}⟩_{j∈J}, #^{1}), and S_{2} = (⟨s_{k}^{2}⟩_{k∈K}, #^{2}).

1. The strand space S_{0}||ϵ has the same strands as S_{0}, but indexing set {0} × I. Take σ : {0} × I → I to be the projection to the second component which, in this case, is a bijection. It gives an equivalence between the two strand spaces. Every strand s_{(0,i)} in S_{0}||ϵ is equal to s_{i}, therefore s_{(0,i)} = s_{σ(0,i)}. Let # be the conflict relation of S||ϵ. If (0, i) # (0, i′) then by definition of # there is conflict i #^{0} i′, therefore σ(0, i) #^{0} σ(0, i′).

2. Both spaces have the same strands but the first has indexing set

H = ({0} × I) ∪ ({1} × (({0} × J) ∪ ({1} × K)))

while the second has indexing set

H′ = ({0} × (({0} × I) ∪ ({1} × J))) ∪ ({1} × K).

Consider the following function σ : H → H′

σ(h) = \{ \begin{matrix}(0, (0, i)) & if h = (0, i) \\ (0, (1, j)) & if h = (1, (0, j)) \\ (1, k) & if h = (1, (1, k)) \end{matrix}

which is a bijection and establishes the desired equivalence.

3. Straightforward.

□

The equivalence S + S ≅ S does not always hold. For example consider the strand space S composed out of one single strand with index i. The indexing set of S + S is {(0, i), (1, i)}. There is no bijection between a set of one element and a set of two elements.

Strands are not permitted to branch and the prefixing operation prefixes each single strand of the space. The following proposition holds:

Proposition 4.2 Let S_{0} and S_{1} be strand spaces and α an action. Then

α.(S_{0} + S_{1}) = α.S_{1} + α.S_{0}.

Proof. Follows from the definition of prefixing operation and sum. □

We can extend the definition of binary parallel composition and nondeterministic sum of strand spaces to operations indexed over a set. Given a collection of strand spaces (⟨s_{i}^{k}⟩_{i∈I_{k}}, #^{k}) indexed by k in a set K, define

||_{k∈K}(⟨s_{i}^{k}⟩_{i∈I_{k}}, #^{k}) =^{def} (⟨s_{h}⟩_{h∈H}, #),

where H = ∑_{k∈K} I_{k}, s_{(k,i)} = s_{i}^{k}, and where (k, i) # (k′, i′) iff k = k′ and i #^{k} i′. In particular if K is the empty set then the parallel composition yields the empty strand space.

As a special case of parallel composition of strand spaces consider the strand space obtained by composing infinitely many but equal strand spaces. Abbreviate

||_{k∈ω}(⟨s_{i}⟩_{i∈I}, #) =^{def}! (⟨s_{i}⟩_{i∈I}, #).

One easily observes that

! (⟨s_{i}⟩_{i∈I}, #) = (⟨s_{(n,i)}⟩_{(n,i)∈ω×I},!#)

where !# is the binary relation over ω × I such that (n, i) !# (m, i′) iff n = m and i # i′.

We define the sum of strand spaces over a set of indexes K in a similar way as we did for the parallel composition of strand spaces over K. The indexing set H and the strands remain the same. Define

∑_{k∈K} S_{k} =^{def} (⟨s_{h}⟩_{h∈H}, #)

where (k, i) # (k′, i′) iff either k ≠ k′ or (k = k′ and i #^{k} i′).

5 A process language for strand spaces

The constructions we have shown in the previous section form a language S of strand spaces with the following grammar:

S ::= ϵ | L | ∑_{j∈J} S_{j} | ||_{j∈J}S_{j}

where L ∈ L, the language of “sequential strand spaces” given by

L ::= ⟨λ⟩ | α.L | ∑_{j∈J} L_{j} .

The strand space ⟨λ⟩ has only one strand which is the empty sequence of actions and with the empty conflict relation.^{3} The bundles of strand spaces in L form linearly ordered sets of events, and therefore can be thought of as runs of a sequential process.

A strand-space term of language S is a “par” process in the sense that parallel composition is only at the top level and therefore consists of a parallel composition and sum of sequential processes. Of particular interest are “!-par” processes which are those terms of S of the form !S. As shown in Section 8 conflict can be eliminated from such strand spaces.

It will be useful to weaken the definition of bundle to the one of open bundle, so that bundles can be composed. An open bundle is a graph with the same structure of a bundle, but where input events need not necessarily be related to output events. In this sense the open bundle is “open” to the environment for communication on input events that are not already linked to output events.

Definition 5.1 An open bundle b of a strand space (⟨s_{i}⟩_{i∈I}, #) is a finite, acyclic subgraph of G graph of (⟨s_{i}⟩_{i∈I}, #) such that:

(i) if e ⇒_{G} e′ and e′ ∈ E_{b} then e ⇒_{b} e′, (control precedence)

(ii) if e′ →_{b} e and e′′ →_{b} e then e′ = e′′, (output-input correspondence)

(iii) if e, e′ ∈ E_{b} s.t. act(e) = out newn⃗M and n ∈ n⃗ ∩ names(e′) then either e ⇒_{b}^{∗} e′ or there exists an input event e′′ ∈ E_{b} such that n ∈ names(e′′), e′′ ≰_{b} e and e′′ ⇒_{b}^{∗} e′, (open freshness)

(iv) if (i, h), (j, k) ∈ E_{b} then ¬(i # j). (conflict freeness)

3Let the index of the empty strand in ⟨λ⟩ be a distinguished index ∗.

Proposition 3.4 does not necessarily hold for open bundles. Input events are open to communication from the environment and therefore not necessarily linked to any output event. The additional requirement e′′ ≰_{b} e in point (iii) ensures that e′ ≰_{b} e; so an open bundle can be transformed into a bundle by composition with other open bundles and addition of communication edges.

Proposition 5.2 If b is open bundle of a strand space in L then all events in E_{b} have the same index and ⇒_{b} is a linear order on E_{b}.

Proof. A strand space (⟨s_{i}⟩_{i∈I}, #) denoted by a term in L is such that for all indexes i, j ∈ I if i ≠ j then i # j. Open bundles are conflict free, therefore all events in E_{b} have the same index. Let i be the index of the events in E_{b} and let (i, h) be the event in E_{b} with greatest position index h. The control precedence of b determines its events to be

E_{b} = {(i, l) | 1 ≤ l ≤ h} .

The events in E_{b} are linearly ordered by ⇒_{G} and therefore linearly ordered by ⇒_{b} (control precedence). □

6 Bundle spaces

The usual semantics of a strand space is in terms of its set of bundles. In this section we show how, by broadening to open bundles, the bundle space can be constructed in a compositional way from bundle spaces. As shown in Section 7 an interesting congruence relation between strand spaces is based on open bundles rather than bundles and the compositional account of the bundle space presented here is useful in showing that such relation is indeed a congruence.

First we introduce two simple operations on open bundles. The first operation takes an open bundle of a strand space and transforms it into an open bundle of that space prefixed by an action. This operation simply adds an initial node and leaves all the remaining graph structure of the original open bundle intact. More precisely let α.S be a strand space in L and b open bundle of S with at least one event. All events of b share the same index i and are linearly ordered (Proposition 5.2). Control precedence and the shape of the strand space graph of S determines the events of b to be the set

E_{b} = {(i, h) | 1 ≤ h ≤ k}

and determines ⇒_{b} to be the smallest binary relation on E_{b} such that

(i, h) ⇒_{b} (i, h + 1) for 1 ≤ h < k

for some k ≥ 1. Consider the graph

b^{+} = (E_{b}^{+}, ⇒_{b}^{+}, →_{b}^{+})

where • E_{b}^{+} = {(i, h) | h ≤ k + 1},

• (i, h) ⇒_{b}^{+} (i, h + 1) for h ≤ k and e ⇏_{b}^{+} e′, otherwise

• (i, h + 1) →_{b}^{+} (i, k + 1) iff (i, h) →_{b} (i, k). Proposition 6.1 The graph b^{+} is an open bundle of α.S. Proof. Straightforward. □

The second operation that we introduce shows how to juxtapose open bundles of strand spaces to get an open bundle of the composed space. Take the strand space ||_{j∈J}S_{j} and a finite subset I of J. For every i ∈ I let b_{i} be an open bundle of S_{i}. Define

||_{i∈I}b_{i} = (⋃_{i∈I} E_{i}, ⋃_{i∈I} ⇒_{i}, ⋃_{i∈I} →_{i})

where for each i ∈ I • E_{i} = {i : e | e ∈ E_{b_{i}}},

• i : e ⇒_{i} i : e′ iff e ⇒_{b_{i}} e′,

• i : e →_{i} i : e′ iff e →_{b_{i}} e′. Tagging an event e with an index i is denoted by i : e and is the event with index the pair consisting of i and the index of e. Proposition 6.2 The graph ||_{i∈I}b_{i} is an open bundle of ||_{j∈J}S_{j}.

Proof. Straightforward. □

Let b and d be two open bundles of the same strand space. We write b ⪯ d if d can be obtained from b by adding more communication edges. More precisely define

b ⪯ d iff E_{b} = E_{d}, ⇒_{b} = ⇒_{d}, and →_{b}⊆→_{d} ,

and abbreviate b ↑ = {d | b ⪯ d}. In the following definition we make use of a further shorthand notation j : B which stands for {j : b | b ∈ B} where j is an index, B a set of bundles and j : b is the bundle obtained by tagging all events of b with j and extending the bundle-edges accordingly.

Definition 6.3 (Bundle space) Let S be a term from the language of strand spaces denoting the strand space (⟨s_{i}⟩_{i∈I}, ♯). The language B(S) is defined on the structure of S as follows:

B(ϵ) = {λ}
B(⟨λ⟩) = {λ}
B(α.S) = {λ} ∪ {({(i, 1)}, ∅, ∅) | i ∈ I} ∪ ⋃_{b∈B(S)\{λ}} b^{+} ↑
B(∑_{j∈J} S_{j}) = ⋃_{j∈J} j : B(S_{j})
B(||_{j∈J}S_{j}) = ⋃_{b_{i}∈B(S_{i})^{I⊆_{f} J}}(||_{i∈I}b_{i})↑

Theorem 6.4 If S is a strand-space term in S then the elements of B(S) are exactly the open bundles of the strand space denoted by S.

Proof. Let S be the strand-space term. The proof has two parts:

1. If b is an open bundle of S then b ∈ B(S). By induction on the structure of S:

If S = ϵ or S = ⟨λ⟩ then b = λ and obviously λ ∈ B(S).

If S = α.S′ then by Proposition 5.2 all events in b share the same index and are linearly ordered. By control precedence and the shape of the strand-space graph of S the events of b are either the empty set or are E_{b} = {(i, h) | h ≤ k} for some k ≥ 1 with common index i. If the set of events of b is empty then b = λ and λ ∈ B(α.S′). The same holds for open bundles with only one node (when k = 1). Suppose that k > 1 and let G′ be the strand-space graph of S′. Consider the graph b′ with components

– E_{b′} = {(i, h) | h ≤ k − 1},

– ⇒_{b′} = ⇒_{G′} ∩ (E_{b′} × E_{b′}),

– →_{b′} such that →_{b′}^{+} = →_{b} ∩ (E_{b′}^{+} × E_{b′}^{+}).

This graph is an open bundle of S′. In fact b′ is a finite and acyclic subgraph of G′ satisfying all requirements of Definition 5.1. In particular open freshness follows from that of b and from the linear ordering of the events in b′. Output-input correspondence and conflict freeness hold since b′ is a subgraph of b and control precedence follows easily from the shape of E_{b′} and ⇒_{b′}. By the induction hypothesis b′ ∈ B(S′) and from b ∈ b^{′+} ↑ it follows that b ∈ B(α.S′).

If S = ∑_{j∈J} S_{j} then by conflict freeness b has the form j : b′ for some index j ∈ J and open bundle b′ of S_{j}. From the induction hypothesis it follows that b′ ∈ B(S_{j}) and therefore j : b′ ∈ B(∑_{j∈J} S_{j}).

Let S = ||_{j∈J}S_{j} and for every j ∈ J let G_{j} be the strand-space graph of j : S_{j} (obtained via a re-indexing that adds j to each index of S_{j}) and let j : b_{j} be the graph with components

– E_{j} = E_{b} ∩ E_{G_{j}},

– ⇒_{j} = ⇒_{b} ∩ ⇒_{G_{j}},

– →_{j} = →_{b} ∩ →_{G_{j}}.

The graph b_{j} is an open bundle of S_{j}; it is a finite and acyclic subgraph of G_{j} satisfying all requirements of Definition 5.1. In particular open freshness of b_{j} follows from that of b since j : b_{j} is a subgraph of b which satisfies control precedence. By the induction hypothesis b_{j} ∈ B(S_{j}) for all j ∈ J and from b ∈ (||_{j∈J}b_{j}) ↑ it follows that b ∈ B(||_{j∈J}S_{j}).

2. Every b ∈ B(S) is an open bundle of the strand space denoted by S. By induction on the structure of S:

If S = ϵ or S = ⟨λ⟩ then b = λ. The empty graph λ is an open bundle of every strand space.

If S = α.S′ then either b = λ or it has only one node, therefore b is an open bundle of the strand space α.S′, or instead b ∈ b^{′+} ↑ for some b′ ∈ B(S′). In this last case from the induction hypothesis it follows that b′ is an open bundle of S′ and by Proposition 6.1 that b^{′+} is an open bundle of α.S′. From b ∈ b^{′+} ↑ it follows that b^{′+} ⪯ b and therefore b is an open bundle of α.S′.

If S = ∑_{j∈J} S_{j} then there exist j ∈ J and b′ ∈ B(S_{j}) such that b = j : b′. By the induction hypothesis b′ is an open bundle of S_{j} and therefore j : b′ is an open bundle of ∑_{j∈J} S_{j}.

If S = ||_{j∈J}S_{j} then b ∈ (||_{i∈I}b_{i}) ↑ such that b_{i} ∈ B(S_{i}) for every i ∈ I. By the induction hypothesis for every i ∈ I the graph b_{i} is an open bundle of S_{i}. Thus by Proposition 6.2 the graph ||_{i∈I}b_{i} is an open bundle of ||_{j∈J}S_{i}. From ||_{i∈I}b_{i} ⪯ b it follows that b is an open bundle of ||_{i∈I}S_{i}.

□

7 A strand space congruence

We have seen an equivalence relation that relates two strand spaces if, via re-indexing, they become the same space. It is easy to check that this relation is a congruence with respect to the operations of the strandspace language we introduced in this paper. It is however a very concrete relation and too discriminating for a model in which security properties are expressed as safety properties on the language of bundles of a strand space. One doesn’t want to distinguish between strand spaces that have isomorphic bundle languages. Unfortunately the equivalence relation ≈ on strand space terms, obtained by taking term equivalence iff they denote strand spaces with essentially the same bundles, is not a congruence. In this section we study a finer equivalence that takes account of the open bundles of a strand space rather than bundles. This relation turns out to be an interesting congruence, in fact the largest congruence within ≈.

Two bundles and more generally two open bundles are isomorphic if they are isomorphic graphs:

Definition 7.1 Given b an open bundle of a strand space S and given b′ an open bundle of a strand space S′ define b ≅ b′ iff there exists a bijection ϕ : E_{b} → E_{b′} such that (i) if e →_{b} e′ then ϕ(e) →_{b′} ϕ(e′),

(ii) if e ⇒_{b} e′ then ϕ(e) ⇒_{b′} ϕ(e′),

(iii) act_{S}(e) = act_{S′}(ϕ(e)).

Sometimes we write ϕ(b) for the open bundle obtained from b through ϕ. This open bundle has events ϕ(E_{b}) and edges

• ϕ(e) →_{ϕ(b)} ϕ(e′) iff e →_{b} e′,

• ϕ(e) ⇒_{ϕ(b)} ϕ(e′) iff e ⇒_{b} e′.

Definition 7.2 Let S and S′ be two strand-space terms in S. Define ≈ the symmetric relation such that S ≈ S′ iff for every bundle b of S there exists a bundle b′ of S′ such that b ≅ b′.

Proposition 7.3 The relation ≈ is an equivalence relation.

Proof. Straightforward. □

The equivalence relation ≈ is not a congruence relation. Consider, for example, the strand-space terms in M.ϵ and in N.ϵ where N and M are two different messages. These two strand-space terms are in the relation ≈ – they both have only one bundle, the empty bundle and they can be easily distinguished in a simple context when, for example, composed in parallel with out M.ϵ. Then

in M.ϵ || out M.ϵ ≉ in N.ϵ || out M.ϵ .

The parallel composition on the left hand side has a bundle of the form

in M ⟵ out M

(for convenience in the previous bundle we show the action associated to the nodes instead of the nodes themselves). The parallel composition on the right hand side only allows the empty bundle.

A context for a strand-space term in the language S is defined as follows:

C ::= [ ] | α.C | ||_{i∈I}T_{i} | Σ_{i∈I}T_{i}

where for each context of the form ||_{i∈I}T_{i} or Σ_{i∈I}T_{i} there is exactly one i ∈ I such that T_{i} is a context C and T_{i} ∈ S for all i ∈ I \ {i}. The context [ ] is a placeholder for a strand-space term. We write C[S] for the term obtained by replacing the strand-space term S for [ ] in context C in the obvious way. An equivalence relation on strand-space terms is a congruence if it respects all contexts.

Definition 7.4 Let S and S′ be two strand-space terms in S. Define ≈_{B} to be the symmetric relation such that S ≈_{B} S′ iff for every open bundle b of S there exists an open bundle b′ of S′ such that b ≅ b′.

Proposition 7.5 The relation ≈_{B} is a congruence.

Proof. The relation ≈_{B} is obviously an equivalence relation. We show by induction on the structure of contexts that if S ≈_{B} S′ then C[S] ≈_{B} C[S′] for every context C.

Obvious for the context [ ].

Consider the context α.C and let b ∈ B(α.C[S]). From Definition 6.3 of bundle space it follows that b is one of the following graphs:

• λ and therefore belongs to B(α.C[S′]).

• ({(i, 1)}, ∅, ∅) with i index of α.C[S]. Then b ≅ ({(j, 1)}, ∅, ∅) and ({(j, 1)}, ∅, ∅) ∈ B(α.C[S′]) for any j index of α.C[S′].

• b ∈ b_{1}^{+} ↑ for some b_{1} ∈ B(C[S]). By the induction hypothesis there exists b_{2} ∈ B(C[S′]) such that b_{1} ≅ b_{2} and therefore b_{1}^{+} ≅ b_{2}^{+}. If ϕ : E_{b_{1}^{+}} → E_{b_{2}^{+}} is a bijection such that ϕ(b_{1}^{+}) = b_{2}^{+} then ϕ(b) ∈ b_{2}^{+} ↑.

Consider the context Σ_{i∈I}T_{i} such that the term T_{i_{0}} is a context C for the index i_{0} in I. Let b ∈ B(Σ_{i∈I}T_{i}[S]). By Definition 6.3 of bundle space the open bundle b is of the form i : b_{i} for some i ∈ I and for some b_{i} ∈ B(T_{i}[S]). If i ≠ i_{0} then i : b_{i} ∈ B(Σ_{i∈I}T_{i}[S′]). If instead i = i_{0} then by the induction hypothesis there exists b′_{i} ∈ B(C[S′]) such that b_{i} ≅ b′_{i} and therefore i : b′_{i} ∈ B(Σ_{i∈I}T_{i}[S′]) and i : b_{i} ≅ i : b′_{i}.

Consider the context ||_{i∈I}T_{i} such that the term T_{i_{0}} is a context C for the index i_{0} in I. If b ∈ B(||_{i∈I}T_{i}[S]) then b ∈ (||_{j∈J}j : b_{j}) ↑ where b_{j} ∈ B(T_{j}) when j ≠ i_{0} and b_{j} ∈ B(C[S]) for j = i_{0}. By the induction hypothesis there exists b′_{i_{0}} ∈ B(C[S′]) such that b_{i_{0}} ≅ b′_{i_{0}}. Let b′_{j} = b_{j} for all j ≠ i_{0}. It follows that ||_{j∈J}b′_{j} ∈ B(||_{i∈I}T_{i}[S′]) and ||_{j∈J}b_{j} ≅ ||_{j∈J}b′_{j}. If ϕ is the bijection such that ϕ(||_{j∈J}b_{j}) = ||_{j∈J}b′_{j} then ϕ(b) ∈ B(||_{j∈J}b′_{j}). □

Theorem 7.6 The relation ≈_{B} is the largest congruence relation inside ≈.

Proof. Consider the set

D = {R | R congruence relation and R ⊆≈} Clearly ⋃ D is a congruence relation and the largest congruence inside ≈. It remains to show that ≈_{B}= ⋃ D. By Proposition 7.5 the relation ≈_{B} is a congruence and since ≈_{B}⊂≈ it follows that ≈_{B}⊆ ⋃ D. Let S and S′ be two strand-space terms and let b be an open bundle of S such that b ≅ b̸′ for all open bundles b′ of S′. If no congruence relation in D contains the pair (S, S′) then ⋃ D ⊆≈_{B}. Let R ∈ D and suppose (S, S′) ∈ R. We find a context C such that (C[S], C[S′]) ∉ R and therefore R is not a congruence relation. Consider the strand space T composed of a single strand whose only events are those output events that correspond exactly to the open input events of b. The strand space T itself forms a bundle that we denote by t. Consider the context T || [ ]. Let b_{1} ∈ (t||b) ↑ be the graph that has no open inputs – it is a bundle of T || S. If there is a bundle b_{2} of T || S′ such that b_{1} ≅ b_{2} then b_{2} ∈ (t′||b′)↑ for some open bundles b′ and t′ such that b ≅ b′ and t ≅ t′. By control precedence either t′ is a bundle of T, therefore b′ is an open bundle of S′ contradicting our assumptions, or b_{2} is a bundle of S′, therefore b′ is an open bundle of S′ and we reach a contradiction again. □

8 Eliminating conflict

An agent that participates in a security protocol is often thought of as executing a sequential program during which it sends messages and chooses from a number of available messages which one to input. If one doesn’t restrict the number of rounds of the protocol an agent can do one can hope to model the protocol with a strand space with conflict of the form ! (⟨s_{i}⟩_{i∈I}, #). In this section we show that under these conditions a simpler model, obtained by dropping the conflict relation, exhibits substantially the same behaviour as the more complex strand space with conflict.

Consider a conflict relation # on a set I and consider the relation !# on ω × I such that (n, i) !# (m, j) iff n = m and i # j. The form of the !# conflict relation suggests the following lemma:

Lemma 8.1 Given I a set of indexes, a finite set A ⊆ ω × I, and # a conflict relation over I. There exists a bijection σ : ω × I → ω × I such that

∀(n, i) ∈ ω × I . ∃m ∈ ω . σ(n, i) = (m, i)

and such that the set A is conflict free with respect to σ^{−1}(!#), meaning ¬(σ(u) !# σ(v)) for all u, v ∈ A.

Proof. By induction on the size of the set A.

The basic case A = ∅: take σ for example to be the identity function. The induction step: Given a set A suppose there is a bijection σ satis-

fying the desired property and such that A is conflict free with respect to σ^{−1}(!#). Take A′ = A ∪ {(n′, i′)} with (n′, i′) ∉ A. Let σ(n′, i′) = (m′, i′) and distinguish two cases:

If m ≠ m′ for all (m, j) ∈ σ(A) then A′ is conflict free with respect to σ^{−1}(!#). Suppose the contrary. Suppose there is (n, i) ∈ A such that σ(n, i) !# σ(n′, i′). If σ(n, i) = (m, i) then m = m′ by definition of !#.

If there exists (m, j) ∈ σ(A) such that m = m′, then consider the following function:

σ′(n, i) = \{ \begin{matrix}(m′′, i′) & if (n, i) = (n′, i′) \\ (m′, i′) & if (n, i) = σ^{−1}(m′′, i′) \\ σ(n, i) & otherwise \end{matrix}

where m′′ ∈ ω such that m ≠ m′′ for all (m, j) ∈ σ(A). Since A is a finite set, such m′′ exists. This function is as σ but swaps the new element (n′, i′), that could introduce conflict, with one that doesn’t. It is easy to check that σ′ is a bijection and that it satisfies the required property. It remains to check that A′ is conflict free with respect to σ′^{−1}(!#). First observe that σ′(A) = σ(A) because (n′, i′) ∉ A and σ^{−1}(m′′, i′) ∉ A (we chose m′′ so that (m′′, i′) ∉ σ(A)). It follows that A is conflict free with respect to σ′^{−1}(!#). Since σ′^{−1}(!#) is irreflexive and symmetric we require:

∀(n, i) ∈ A . ¬(σ′(n, i) !# σ′(n′, i′)).

Suppose instead that there exists (n, i) ∈ A such that σ(n, i) !# σ(n′, i′). Let σ(n, i) = (m, i), then (m, i) !# (m′′, i′). From the conflict relation !# it follows that m = m′′. On the other hand (m, i) ∈ σ(A). Therefore m ≠ m′′.

□

Together with the previous lemma, the observation that two different copies of the same strand space have same strands at same corresponding positions, yields the following theorem:

Theorem 8.2 Consider strand spaces ! (⟨s_{i}⟩_{i∈I}, ∅) and ! (⟨s_{i}⟩_{i∈I}, #). Let b be a bundle of ! (⟨s_{i}⟩_{i∈I}, ∅). There exists a strand space S such that b is a bundle of S and S ≅! (⟨s_{i}⟩_{i∈I}, #).

Proof. Given b a bundle of ! (⟨s_{i}⟩_{i∈I}, ∅) take A the set of indexes of strands participating with nodes in b. The set A is finite because so is b and A ⊆ ω × I. By Lemma 8.1 there is a bijection σ : ω × I → ω × I such that

∀(n, i) ∈ ω × I . σ(n, i) = (n′, i)

for some n′ ∈ ω and A is conflict free with respect to σ^{−1}(!#). Consider the strand space with conflict

S = (⟨t_{(m,i)}⟩_{(m,i)∈ω×I}, σ^{−1}(!#))

where t_{(m,i)} = s_{i} for all m ∈ ω. The equivalence S ≅!(⟨s_{i}⟩_{i∈I}, #) stands. In fact σ is a bijection such that

(i) t_{(m,i)} = s_{σ(m,i)} since s_{σ(m,i)} = s_{(n′,i)} = s_{i} = t_{(m,i)}

(ii) (m, i) σ^{−1}(!#) (u, j) iff σ(m, i) !# σ(u, j).

The two strand spaces ! (⟨s_{i}⟩_{i∈I}, ∅) and S have the same strand-space graph, therefore since b is a bundle over !(⟨s_{i}⟩_{i∈I}, ∅), and since A is conflict free with respect to σ^{−1}(!#) follows b bundle of S. □

To summarise, the behaviour in terms of bundles of a replicated strand space with conflict corresponds, modulo re-indexing, to that of the strand space we obtain dropping the conflict relation.

Corollary 8.3 Consider strand spaces !(⟨s_{i}⟩_{i∈I}, ∅) and !(⟨s_{i}⟩_{i∈I}, #) strand spaces.

1. If b is bundle of ! (⟨s_{i}⟩_{i∈I}, #) then b is bundle of ! (⟨s_{i}⟩_{i∈I}, ∅).

2. If b is bundle of ! (⟨s_{i}⟩_{i∈I}, ∅) then there exists a re-indexing π such that π(b) is a bundle of ! (⟨s_{i}⟩_{i∈I}, #).

Proof. The first point is obvious, the second point follows directly form Theorem 8.2 and Proposition 3.6. □

Consequently, the strand space with conflict denoted by a “!-par” process has the same bundles up to re-indexing as a strand space without conflict.

9 Event structures from strand spaces

In this section we show how strand spaces relate to event structures. Recall that a bundle of a strand space is a graph and therefore a set of edges and nodes. It turns out that the bundles of a strand space ordered by inclusion correspond to the finite configurations of a prime event structure. Prime event structures are a particularly simple kind of event structure where the enabling of events can be expressed as a global partial order of causal dependency. Event structures as a model of concurrent processes were introduced in [NPW81, Win80] – see also [Win82, Win87, Win88, WN95].

Definition 9.1 A prime event structure (E, #, ≤) consists of a set E of events partially ordered by the causal dependency relation ≤ and a binary, symmetric, irreflexive conflict relation # ⊆ E × E, which satisfy

(i) {e′ | e′ ≤ e} is finite for all e ∈ E, and

(ii) if e # e′ ≤ e′′ then e # e′′ for all e, e′, e′′ ∈ E.

Definition 9.2 The configurations of an event structure E = (E, #, ≤) consist of those subsets x ⊆ E which are

(i) conflict free: ∀e, e′ ∈ x . ¬(e # e′) and

(ii) left closed: ∀e, e′.e′ ≤ e ∈ x ⇒ e′ ∈ x.

Write F(E) for the set of configurations of an event structure and F^{fin}(E) for its finite configurations.

For a strand space S write B for the set of bundles of S. Consider the partial order (B, ⊆). Say a subset X of B is compatible iff

∃b ∈ B . ∀b′ ∈ X . b ⊆ b′ .

Proposition 9.3 Let S be a strand space and B the set of bundles of S. The partial order (B, ⊆) satisfies the following properties:

1. if X ⊆ B, X is finite and pairwise compatible, then ⋃ X ∈ B. (coherence )

2. if X ⊆ B and X is compatible, then ⋂ X ∈ B. (stability)

Proof. Let G be the strand space graph of S.

1. The graph ⋃ X is obviously a finite subgraph of G since X is finite and each element in X is finite. Let e be an event in ⋃ X. The set X is pairwise compatible therefore there exists b ∈ X with e ∈ b and such that if e′ →_{⋃ X} e then e′ →_{b} e. Since b is a bundle if e′ ⇒_{⋃ X} e then e′ ⇒_{b} e (control precedence). Therefore {e′ | e′ ≤_{⋃ X} e} = {e′ |e′ ≤_{b} e} and it follows that ⋃ X is acyclic. We check the requirements of Definition 3.2:

(i) Consider an event e ∈ ⋃ X. There is a bundle b ∈ X with e ∈ b. By control precedence if e′ ⇒_{G} e then e′ ⇒_{b} e. From b ⊆ ⋃ X it follows that e′ ⇒_{⋃ X} e.

(ii) Output-input precedence stands for the set ⋃ X. Let e be an input event in ⋃ X. There is a bundle b ∈ ⋃ X with e ∈ b. An output event e′ exists such that e′ →_{b} e (output-input precedence of b) and therefore e′ →_{⋃ X} e. We require that there is a unique such output event. Suppose the contrary. Suppose there are two output events e′, e′′ such that e′ →_{⋃ X} e and e′′ →_{⋃ X} e. Then two distinct bundles b, b′ ∈ X exist such that e′ →_{b} e and e′′ →_{b′} e. However X is pairwise compatible. Therefore there is a bundle in X containing both b and b′. This can’t be the case and we reach a contradiction.

(iii) Let e, e′ be two events in ⋃ X such that act(e) = out new n⃗ M and n ∈ n⃗ ∩ names(e′). Since X is pairwise compatible, there exists a bundle b′ in X which contains both e and e′. The bundle b′ respects freshness. Thus either e ⇒_{b′}^{∗} e′ or there exists an input event e′′ such that n ∈ names(e′′) and e′′ ⇒_{b′}^{∗} e′. Consequently freshness holds for ⋃ X.

(vi) That the graph ⋃ X does not contain conflicting events follows easily from the pairwise compatibility of X.

Therefore ⋃ X is a bundle in B.

2. Every element of X is a bundle in B. Therefore ⋂ X forms a finite and acyclic subgraph of G. Following Definition 3.2 we check all requirements and thus show that ⋂ X ∈ B:

(i) Consider an event e ∈ ⋂ X. Every bundle b ∈ X is such that e ∈ b. For each b ∈ X if e′ ⇒_{G} e then e′ ⇒_{b} e (control precedence). From this it follows that e′ ⇒_{⋂ X} e.

(ii) If e is an input event in ⋂ X then every bundle b ∈ ⋂ X contains the event e and contains an output event e_{b} such that e_{b} →_{b} e. The set X is compatible. Let b′ ∈ B be an upper bound. Therefore there exists a unique e′ such that e′ = e_{b} for all bundles b ∈ X and e′ →_{b} e. The event e′ is the unique event such that e′ →_{⋂ X} e.

(iii) Let e, e′ be two events in ⋂ X such that act(e) = out new n⃗ M and n ∈ n⃗ ∩ names(e′). The events e, e′ belong to every bundle in X. Freshness holds for each bundle b in X. Thus either e ⇒_{b}^{∗} e′ or there exists an input event e′′ such that n ∈ names(e′′) and e′′ ⇒_{b}^{∗} e′. If e ⇒_{b′}^{∗} e′ for some bundle b′ in X then e ⇒_{G}^{∗} e and therefore e ⇒_{b}^{∗} e′ for every bundle b in X. The case of a bundle b′ such that e′′ ⇒_{b}^{∗} e′ is similar. Freshness of ⋂ X follows.

(vi) The elements of X are bundles and therefore conflict free. Consequently ⋂ X is conflict free.

□

Given a bundle b ∈ B and an event e ∈ E_{b} define

⌈e⌉_{b} =^{def} ⋂{b′ ∈ B | e ∈ b′ ∧ b′ ⊆ b} .

Proposition 9.4 Let B be the bundles of a strand space. For every bundle b ∈ B and every event e ∈ E_{b} the set ⌈e⌉_{b} is a bundle in B. For every finite and compatible subset X ⊆ B

if ⌈e⌉_{b} ⊆ ⋃ X then ∃b′ ∈ X . ⌈e⌉_{b} ⊆ b′

We call a bundle ⌈e⌉_{b} a prime of (B, ⊆).

Proof. That the elements ⌈e⌉_{b} are bundles in B follows from the stability property of (B, ⊆) (Proposition 9.3). The set {b′ ∈ B | e ∈ b′ ∧ b′ ⊆ b} is in fact compatible.

Let X ⊆ B be finite and compatible. If ⌈e⌉_{b} ⊆ ⋃ X then e ∈ b′ for some b′ ∈ X. The two bundles b′ and ⌈e⌉_{b} in B are compatible (they are both included in ⋃ X), therefore from the stability property of (B, ⊆) it follows that b′ ∩ ⌈e⌉_{b} ∈ B. We know that e ∈ b′ and that b′ ∩ ⌈e⌉_{b} ⊆ b. Therefore ⌈e⌉_{b} ⊆ b′ ∩ ⌈e⌉_{b} ⊆ b′. □

The primes form a basis for the partial order (B, ⊆) as the following proposition shows.

Proposition 9.5 Let S be a strand space and B its bundles. Every bundle b ∈ B can be obtained as the union of the primes included in b

b = ⋃{p | p ⊆ b, p prime}.

Proof. Obviously ⋃{p | p ⊆ b, p prime} ⊆ b. On the other hand, if e ∈ b then e ∈ ⌈e⌉_{b}. The prime ⌈e⌉_{b} is a bundle included in b and therefore if e′ ⇒_{b} e then e′ ⇒_{⌈e⌉_{b}} e, and if e′ →_{b} e then e′ →_{⌈e⌉_{b}} e. Thus b ⊆ ⋃{⌈e⌉_{b} | e ∈ b}. □

Let B the set of bundles of a strand space S. Consider the following structure

P r(B) =^{def} (P, #, ⊆)

where P is the set of primes of B and where p # p′ iff the two primes p and p′ are not compatible.

Theorem 9.6 The structure P r(B) is a prime event structure. The map ϕ : (B, ⊆) ≅ (F^{fin}P r(B), ⊆) such that ϕ(b) = {p | p ⊆ b, p prime} is an isomorphism of partial orders with inverse map θ : F^{fin}P r(B) → B given by θ(x) = ⋃ x.

Proof. It is easy to check that P r(B) is a prime event structure. The relation ⊆ is a partial order of primes. Bundles and in particular primes are finite sets. Thus for each prime p the set {p′ | p′ ⊆ p} is finite. Moreover if p, p′, p′′ are primes such that p # p′ ⊆ p′′ then p # p′′ – otherwise p and p′′ would be compatible and therefore p and p′ would be compatible too.

The map ϕ is obviously well-defined and so is θ. In fact x is a finite configuration of P r(B) thus a finite set of bundles in B which is conflict free and left closed. Since it is conflict free it is pairwise compatible and therefore from the coherence property of Proposition 9.3 it follows that ⋃ x ∈ B.

It is clear that both maps ϕ and θ are order preserving. We show that they are mutual inverses and therefore give the required isomorphism. From Proposition 9.5 it follows that θ(ϕ(b)) = b for all b ∈ B. Let x be a finite configuration of P r(B). We require that ϕ(θ(x)) = x, i.e., {p | p ⊆ ⋃ x, p prime} = x. If p is a prime such that p ⊆ ⋃ x, then there exists a bundle p′ in x (another prime) such that p ⊆ p′ (Proposition 9.4). The configuration x is left-closed, thus p ∈ x. On the other hand, x is a set of primes and therefore x ⊆ {p | p ⊆ ⋃ x, p prime}. □

Observation 9.7 Since P r(B) is a prime event structure the partial order (FP r(B), ⊆) is a Scott domain of information, in particular a prime algebraic domain (see [NPW81, Win87, Win88]). This domain however can include configurations which are infinite and therefore are not bundles in the usual sense.

The prime event structure P r(B) underlies the strand space semantics Syverson gave to the BAN logic [Syv99].

References

[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.

[CJ97] J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0. 1997.

[CW01] F. Crazzolara and G. Winskel. Events in security protocols. In Proceedings of the Eight ACM Conference on Computer and Communications Security, Philadelphia, November 2001. ACM Press.

[DY83] D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 2(29), 1983.

[NPW81] M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, Event structures and Domains. Theoretical Computer Science, 13, 1981.

[Syv99] P. Syverson. Towards a Strand Semantics for Authentication Logic. Electronic Notes in Theoretical Computer Science, (20), 1999.

[TG00] J. Thayer and J. Guttman. Authentication tests. In 2000 IEEE Symposium on Security and Privacy, Oakland CA, May 2000.

[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 spaces: Why is a security protocol correct? In 1998 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, 1998.

[Win80] G. Winskel. Events in computation. PhD thesis, Comp. Sc. Dept. University of Edinburgh, 1980.

[Win82] G. Winskel. Event structure semantics of ccs and related languages. In Proceedings of the International Colloquium on Automata, Languages and Programming - ICALP 82, volume 140 of LNCS. Springer–Verlag, 1982. Extended version, Computer Science Report, University of Aarhus, 1982.

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

[Win88] G. Winskel. An introduction to event structures. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS. Springer–Verlag, 1988.

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

Recent BRICS Report Series Publications

RS-02-5 Federico Crazzolara and Glynn Winskel. Composing Strand Spaces. February 2002. 30 pp.

RS-02-4 Olivier Danvy and Lasse R. Nielsen. Syntactic Theories in Practice. January 2002. 34 pp. This revised report supersedes the earlier BRICS report RS-01-31.

RS-02-3 Olivier Danvy and Lasse R. Nielsen. On One-Pass CPS Transformations. January 2002. 18 pp.

RS-02-2 Lasse R. Nielsen. A Simple Correctness Proof of the Direct-Style Transformation. January 2002.

RS-02-1 Claus Brabrand, Anders Møller, and Michael I. Schwartzbach. The <bigwig> Project. January 2002. 36 pp. This revised report supersedes the earlier BRICS report RS-00-42.

RS-01-55 Daniel Damian and Olivier Danvy. A Simple CPS Transformation of Control-Flow Information. December 2001.

RS-01-54 Daniel Damian and Olivier Danvy. Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation. December 2001. 41 pp. To appear in the Journal of Functional Programming. This report supersedes the earlier BRICS report RS-00-15.

RS-01-53 Zoltán Ésik and Masami Ito. Temporal Logic with Cyclic Counting and the Degree of Aperiodicity of Finite Automata. December 2001. 31 pp.

RS-01-52 Jens Groth. Extracting Witnesses from Proofs of Knowledge in the Random Oracle Model. December 2001. 23 pp.

RS-01-51 Ulrich Kohlenbach. On Weak Markov’s Principle. December 2001. 10 pp.

RS-01-50 Jiří Srba. Note on the Tableau Technique for Commutative Transition Systems. December 2001. 19 pp. To appear in Nielsen and Engberg, editors, Foundations of Software Science and Computation Structures, FoSSaCS ’02 Proceedings, LNCS 2303, 2002.