Verifying layered security protocols

Abstract

Many security protocols are built as the composition of an application-layer protocol and a secure transport protocol, such as TLS. There are several approaches to proving the correctness of such protocols. One popular approach is verification by abstraction, in which the correctness of the application-layer protocol is proven under the assumption that the transport layer satisfies certain properties, such as confidentiality. Following this approach, we adapt the strand spaces model in order to analyse application-layer protocols that depend on secure transport protocols; we consider both bilaterally and unilaterally authenticating secure transport protocols, such as bilateral and unilateral TLS.

The paper’s main contribution is a proof of the model’s soundness. In particular, we prove that, subject to a suitable independence assumption, if there is an attack against the application-layer protocol when layered on top of a particular secure transport protocol, then there is an attack against the abstracted model of the application-layer protocol. In contrast to existing work in this area, the independence assumption consists of eight statically checkable conditions, meaning that it is not necessary to consider all possible runs of the protocol.

Keywords

Protocol verification strand spaces compositional verification

1. Introduction

Modern security protocols tend to be constructed as two separate layers. The bottom layer, known as the secure transport layer, is a generic secure transport protocol, such as TLS [11], that can send arbitrary messages, protected in some way. For example, the secure transport layer might guarantee confidentiality of the messages (i.e. the messages can only be read by the intended recipient) or authenticity (i.e. the recipient can be sure of the identity of the sender). The second layer, known as the application layer, uses the guarantees provided by the transport layer to provide some useful functionality. For example, WebAuth [25] is an application-layer protocol that uses the security guarantees provided by the transport layer to provide a single-sign-on service, so that users can login to multiple websites with just one account.

There are two main tactics for verifying layered security protocols. Firstly, a combined protocol formed from the composition of the application and transport-layer protocols, can be analysed using standard techniques. Alternatively, verification by abstraction can be used to prove the application-layer protocol correct in isolation, assuming only that the transport protocol satisfies certain properties, rather than considering a particular implementation.

There are several advantages to verifying protocols by abstraction. Firstly, the proofs are simpler, as the combined protocols are often very large, and transport-layer protocols (particularly TLS) are highly complex. It also permits the proof of transport-layer correctness to be reused for multiple application-layer protocols. Further, the application-layer proof no longer depends on a particular transport layer, meaning that any protocol that provides equivalent (or stronger) properties can be used. Lastly, such a proof often reveals precisely why the transport layer has to satisfy some property to guarantee the security of the application layer. This can be informative for the protocol designer, who may be able to alter the application-layer protocol to weaken its requirements, or even change the transport-layer protocol required.

Proof by abstraction. The first contribution of this paper, in Section 3, is an extension to the strand spaces model [26], the high-level strand spaces model, that can be used to prove application-layer protocols correct by abstracting away from the transport-layer protocol. Our model allows us to capture the properties of a wide variety of transport-layer protocols, including TLS, to be modelled. In contrast to other techniques, we are able to model the guarantees provided by so-called unilaterally authenticating secure transport protocols, such as unilateral TLS. In these protocols, the server is authenticated to the client, but the client is not authenticated to the server, although the server can assume all messages come from the same source. Many other techniques for verifying layered security protocols have focused on modelling the security guarantees provided by bilateral transport-layer protocols, such as bilateral TLS, where each participant is authenticated to the other. However, many application-layer protocols, in particular those used on the web, are unable to make use of bilateral TLS since each party must possess a public-key certificate. Thus, web-based protocols almost exclusively use unilateral TLS, making it important that protocol analysis techniques can model its guarantees.

There have been many approaches to verifying layered-security protocols by abstraction. For example, [4] extends the Inductive Approach [24] to verify application-layer protocols that are layered on a simple type of secure transport protocol. In [3] the authors give a LTL-based model checking approach to verifying layered security protocols by abstraction that supports many types of secure transport protocol, although not unilateral protocols. In [12] the authors use CSP to verify application-layer protocols layered on a similar range of transport-layer protocols to those we support, with the exception of unilaterally authenticating secure transport protocols. In [22] the authors define a model-checking based approach that allows verification of application-layer protocols that are layered on unilateral or bilateral protocols. In [6] the authors define a variant of the pi-calculus that allows the guarantees provided by both unilateral and bilateral transport-layer protocols to be modelled. [1] presents a variant of the join-calculus that allows strong secure channels to be modelled. Further comparisons are made in Section 8.

Soundness. Proving a layered security protocol correct by abstraction introduces an obligation to prove that the analysis captures all attacks that verifying the combined protocol would find. Clearly, such a proof requires a number of assumptions on the application and transport-layer protocols, as it is possible to construct protocols that break the security guarantees of others by, for example, deliberately leaking keys. Further, it is highly desirable for these assumptions to be statically checkable (i.e. such that they can be checked simply by inspection of the protocol messages), or checkable using existing tools, in order to easily determine if a composition is sound.

Our main contribution is a proof of the soundness of the high-level strand spaces model, with respect to the Dolev–Yao model [13]. In particular, we prove that, subject to statically checkable conditions, whenever there is an attack against the combined protocol, then there is an attack against the application-layer protocol in the high-level model. This is a particularly difficult problem for a number of reasons. The central challenge was to ensure that the proof did not impose restrictions that prevented real-world protocols from being modelled. For example, we could have proven the result easily had we insisted that the messages of the application and transport layer were entirely disjoint, or that transport-layer messages were of a certain format. This would have substantially restricted the utility of the proof. Instead, we believe that our static assumptions are satisfied by large classes of both application and transport-layer protocols, including WebAuth and TLS (although TLS does require an attack-preserving transformation).

Our statically checkable conditions take some inspiration from [17] since they are primarily concerned with what encryptions can be shared between the layers. For example, we prohibit any encrypted term from being shared between the application layer and certain parts of the transport layer. We also make several assumptions about the penetrator initial knowledge and how regular agents behave. These assumptions allow us to prove our main result as follows.

In the following, a bundle is a collection of runs of a protocol by various agents, possibly involving the penetrator. A low-level bundle models the messages of the secure transport protocol explicitly, whereas a high-level bundle abstracts from the details of the secure transport protocol.

In Section 4, we prove that there exists a class of low-level bundles, known as interference-free bundles, that can be converted into high-level bundles that have corresponding application-layer behaviour.

In Section 5, assuming that our statically checkable condition holds, we prove that any low-level bundle can be transformed to a corresponding interference-free low-level bundle.

In Section 6 we show that the above transformations preserve attacks against protocols. We prove that the transformations from Section 5 ensure that if a low-level bundle does not satisfy a particular protocol-correctness property then neither does the transformed low-level bundle. Further, we show that whenever a low-level bundle does not satisfy a protocol-correctness property, and the application-layer protocol is layered on a correct transport-layer protocol, then the high-level bundle created by Section 4 also does not satisfy the protocol-correctness property.

Using the above, we can then observe that the high-level strand spaces model is sound, in the sense that any proof of correctness at the high-level implies there can be no bundle at the low-level that does not satisfy the property.

In Section 7 we show how a simple attack-preserving transformation allows both forms of TLS to be considered within our model.

The soundness of protocol composition has been widely considered before. Most work [2,7,8,10,17] considers when it is sound to compose protocols in parallel. Generally, the results of these papers require various disjointness properties to hold, not unlike the properties we consider in this paper. However, we are attempting to prove the correctness of the layers independently, even though messages are formed from those of multiple layers.

There has been relatively little work done on the soundness of techniques that prove protocol correctness by abstraction. Therefore, we consider the fact that the high-level strand spaces has a general soundness result to be the most novel aspect of our work. The work closest to ours is [16], in which the authors show that their analysis technique is sound, assuming a statically checkable condition. Compared to the assumptions developed in this paper, the conditions the authors specify are more restrictive and, in particular, TLS does not satisfy their definition. Further comparisons to this and other closely related pieces of work are given in Section 8.

The proofs for many of the results are contained in the Appendices of the online version (see Supplemental material).

Relationship to previous work. This paper builds on existing work of the authors in [15,19,20]. The version of the high-level strand spaces model defined in Section 3 is from [15], which in turn extended [19]; the only difference is that this version supports compound keys. Section 4 is loosely based on [20] in that the translation between the low and high-level strand spaces are similar. However, the semantic condition and the resulting correctness proof have been reformulated. [14] contains a slightly extended version of the model that models the guarantees provided by protocols that additionally prevent message reordering.

Notation. In this paper we use the following notation for sequences. A sequence is denoted as, for example, $⟨ 1, 2 ⟩$ . Given two sequences, x and y: the concatenation of x and y is denoted by $x^y$ ; $x ⩽ y$ denotes that x is a prefix of y or $x = y$ . The length of a sequence x is denoted by $| x |$ and, if $1 ⩽ i ⩽ | x |$ then $x (i)$ denotes the ith element of x. If A is a set, then $A^{*}$ represents the set of all possible sequences of elements from A, including the empty sequence.

2. Introduction to strand spaces

The strand spaces model [26] allows security protocols to be proven correct under the Dolev–Yao model [13]. In this section we review the strand spaces model.

Terms and strands. The basic components of protocol messages are terms, which can be an atom, a concatenation of terms or an encryption of a term. This is based on [26] and has been augmented with support for compound keys.

Definition 2.1 (Based on [26]).

The set of atoms $A$ includes atomic messages and two disjoint subsets, firstly of names $A_{names}$ and secondly of cryptographic keys $K$ with a subset of symmetric keys $K_{sym}$ . We assume that the set of names is partitioned into two subsets, $A_{names}^{reg}$ and $A_{names}^{pen}$ that represent the set of names that honest (regular) agents and dishonest (penetrator) agents use, respectively. Further, we assume that $A_{names}^{reg} \cap A_{names}^{pen} = {?}$ , where $?$ denotes a name that is used exclusively in the high-level strand spaces model (and will be discussed further in Section 3.1). We also assume that there exists a function giving the inverse of a key $k \in K$ , written $k^{- 1}$ and functions giving the public and secret key of a name, which we write as $PK (A)$ and $SK (A)$ for $A \in A_{names}$ .

The set of terms $T$ 1

¹
This differs from [26] where the set of atoms was denoted by $T$ and the set of terms by $A$ .

is the closure of

A

under encryption (written as

{| m |}_{k}

) and concatenation (written

t_{1}^t_{2}

). Concatenation is right associative.

The set of key generation functions $Kgf$ consists of functions that generate symmetric keys from terms; i.e. if $g \in Kgf$ then $g : T \to K$ . We assume each function $g \in Kgf$ is injective and that distinct key generation functions have disjoint ranges. A key $k \in K$ is complex iff there exists $g \in Kgf$ and $t \in T$ such that $g (t) = k$ , and is simple otherwise.

We assume an ordering relation, the subterm relation, ⊑, over $T$ such that $t_{1} ⊑ t_{2}$ iff $t_{1}$ can be obtained from $t_{2}$ by a finite number of decryption and splitting operations. The relation $ingredient$ is defined as the least reflexive transitive relation such that: $k ingredient {| m |}_{k}$ , $m ingredient {| m |}_{k}$ , $t_{1} ingredient t_{1}^t_{2}$ , $t_{2} ingredient t_{1}^t_{2}$ and $t ingredient g (t)$ .

Note that the ⊑ relation is defined such that $k ⋢ {| m |}_{k}$ ; intuitively, k is not contained within (and cannot be extracted from) ${| m |}_{k}$ as it is used only to construct the message. In contrast, $k ingredient {| m |}_{k}$ , and indicates that k is required in order to construct the message ${| m |}_{k}$ .

Whilst the term algebra does not include explicit support for hash functions, it is possible to model protocols that use hash functions by making use of key generation functions. For example, hashing a term t using a hash function h could be modelled as encrypting 0 using h as a key-generation function; i.e. ${| 0 |}_{h (t)}$ . Note that this is equivalent to hashing since the algebra provides no way of inverting the key generation function to reveal the value of t.

A strand represents one principal’s view of a protocol’s execution and it consists of a sequence of message transmissions (written $+ t$ ) and receptions (written $- t$ ). For example, the strand $⟨ - t, + t ⟩$ represents a principal who received one message and then immediately echoed it. A strand space is a set of strands, generally consisting of all strands for a protocol.

Definition 2.2 (From [26]).

A signed term is a pair $(σ, a)$ with $a \in T$ and $σ \in {+, -}$ . A signed term is written as either $+ t$ or $- t$ . The set of finite sequences of signed terms is denoted by ${(\pm T)}^{*}$ and a typical element is of the form $⟨ (σ_{1}, t_{1}), \dots, (σ_{n}, t_{n}) ⟩$ .

Definition 2.3 (From [26]).

A strand space over $T$ is a set Σ together with a trace mapping $tr : Σ \to {(\pm T)}^{*}$ . Each $s \in Σ$ is known as a strand. Fix a strand space Σ:

A node is a pair $(s, i)$ with $s \in Σ$ and $i \in {1. . | tr (s) |}$ . We say that $(s, i)$ belongs to the strand s. Note every node belongs to a unique strand. The set of nodes is denoted by $N$ .

If $n = (s, i) \in N$ then $index (n) = i$ and $strand (n) = s$ . Further, $msg (n) \hat{=} tr (s) (i)$ .

There is an edge $n_{1} \to n_{2}$ iff there exists $a \in T$ with $msg (n_{1}) = + a$ and $msg (n_{2}) = - a$ .

There is an edge $n_{1} \Rightarrow n_{2}$ iff $n_{1} = (s, i)$ and $n_{2} = (s, i + 1)$ . The transitive closure of ⇒ is written $\Rightarrow^{+}$ .

An unsigned term t originates at a positive node $n \in N$ iff $t ⊑ msg (n)$ and, for all nodes $n^{'}$ such that $n^{'} \Rightarrow^{+} n$ , $t ⋢ msg (n^{'})$ .

An unsigned term t is uniquely originating iff t originates on a unique $n \in N$ .

A bundle represents possible real-world runs of the protocol; it is a set of strands such that every message that is received by a strand is sent by another strand in the bundle. Since the above definition of a strand space allows us to view a strand space as a connected graph $G = (N, \to \cup \Rightarrow)$ , a bundle is a sub-graph of G that satisfies certain well-formedness conditions.

Definition 2.4 (From [26]).

Suppose $\to_{B} \subset \to$ , $\Rightarrow_{B} \subset \Rightarrow$ and $B = (N_{B}, \to_{B} \cup \Rightarrow_{B})$ is a subgraph of $(N, \to \cup \Rightarrow)$ . Then $B$ is a bundle iff:

$B$ is finite;

If $n_{2} \in N_{B}$ and $msg (n_{2})$ is negative then there exists a unique $n_{1} \in N_{B}$ such that $n_{1} \to_{B} n_{2}$ ;

If $n_{2} \in N_{B}$ and $n_{1} \Rightarrow n_{2}$ then $n_{1} \Rightarrow_{B} n_{2}$ ;

$B$ is acyclic.

A node n is in a bundle

B = (N_{B}, \to_{B} \cup \Rightarrow_{B})

, written

n \in B

, iff

n \in N_{B}

. A strand s is in

B

iff a non-empty subset of its nodes are in

N_{B}

Definition 2.5 (From [26]).

If $B$ is a bundle then the $B$ -height of a strand s is the largest i such that $(s, i) \in B$ .

Definition 2.6 (From [26]).

If $S$ is a set of edges, i.e. $S \subseteq \to \cup \Rightarrow$ , then $≺_{S}$ is the transitive closure of $S$ and $≼_{S}$ is the reflexive, transitive closure of $S$ .

Lemma 2.7 (From [26]).

Let $B$ be a bundle; then $≼_{B}$ is a partial order (i.e. a reflexive, antisymmetric, transitive relation). Every non-empty subset of the nodes in $B$ has $≼_{B}$ -minimal members (this is abbreviated to ≼ when the bundle is clear).

The penetrator. The capabilities of the penetrator are defined by the operations that he can perform. In the case of the strand spaces model this means that we need to define penetrator strands that allow the penetrator to manipulate messages according to the Dolev–Yao model.

Definition 2.8 (From [26]).

A penetrator strand for $T_{P}$ is one of the following, where $t_{i}$ ranges over $T$ and k over $K$ : M

Text message: $⟨ + t ⟩$ where $t \in T_{P}$ ;

Concatenation: $⟨ - t_{0}, - t_{1}, + t_{0}^t_{1} ⟩$ ;

Separation into components: $⟨ - t_{0}^t_{1}, + t_{0}, + t_{1} ⟩$ ;

Encryption: $⟨ - k, - t, + {| t |}_{k} ⟩$ ;

Decryption: $⟨ - k^{- 1}, - {| t |}_{k}, + t ⟩$ ;

Key generation: $⟨ - t, + g (t) ⟩$ where $g \in Kgf$ .

On a D or E strand the incoming edge with k on is known as the key edge.

Definition 2.9 (Adapted from [26]).

An infiltrated strand space is a tuple $(Σ, P, T_{P})$ with Σ a strand space, $P \subseteq Σ$ and containing only penetrator strands for $T_{P}$ , and $T_{P} \subseteq T$ denotes the set of public terms that the penetrator initially knows. A node $(s, i)$ in an infiltrated strand space is known as a penetrator node iff $s \in P$ and as a regular node otherwise. The set of regular nodes in a bundle $B$ is denoted by $N_{B}^{reg}$ .

We define $A_{P} \hat{=} T_{P} \cap A$ and $K_{P} \hat{=} T_{P} \cap K$ , which are the sets of atoms and keys initially known to the penetrator, respectively.

For the remainder of this paper we will refer to an infiltrated strand space simply as a strand space and implicitly consider P and $T_{P}$ .

Definition 2.10 (From [18]).

Bundles $B$ , $B^{'}$ of a strand space Σ are equivalent iff they have the same regular nodes.

Definition 2.11 (From [18]).

A path p through a bundle $B$ is a finite sequence of nodes such that for each consecutive pair of nodes m and n, either $m \to n$ , or $m \Rightarrow^{+} n$ with $msg (m)$ negative and $msg (n)$ positive. A penetrator path is a path where every node, aside from possibly the first and the last, is a penetrator node.

In order to simplify protocol correctness proofs, a bundle normal form is defined, as follows.

Definition 2.12 (Based on [18]).

A $\Rightarrow^{+}$ -edge is constructive if it is part of a E, KG or C strand. It is destructive if it is part of a D or S strand. A penetrator node is initial if it is a M node.

Definition 2.13 (Based on [18]).

A bundle $B$ is normal if for any penetrator path of $B$ , whenever a constructive edge sends to a destructive edge, the constructive edge must be a KG strand (i.e. the KG strand must feed into the key-edge).

Intuitively, a normal bundle is one where the penetrator first de-constructs any term that it needs in order to build the new term, and only then starts constructing the outgoing term. In particular, if the bundle does not contain KG strands, then every destructive edge precedes every constructive edge (i.e. no destructive edge occurs after a constructive edge).

Lemma 2.14 (Based on [18]).

For any bundle there exists an equivalent normal bundle.

3. The high-level strand spaces model

This section defines the high-level strand spaces model. In Section 3.1, we define the basics of the model, including the necessary adaptations to support unilaterally authenticating secure transport protocols. In Section 3.2 we define the operations that the penetrator can perform, including how he can manipulate messages sent over secure channels. In Section 3.3 we give a simple example that demonstrates how the high-level strand spaces model can be used.

3.1. Basic definitions

We consider a channel as an object that allows two participants to exchange messages: messages sent at one end of the channel are intended to be received at the other end. A fundamental property of many transport protocols, including TLS, is that a principal is able to send or receive on a channel only if she has the relevant cryptographic keys; these are different for different channels, which prevents messages being replayed between sessions.

A channel end conceptually encapsulates all the information that is required to communicate on a particular channel. However, as we abstract away from the details of the transport protocol, we treat channel ends as opaque values. For generality, we also consider channels (for protocols that are weaker than TLS) that do not provide a separation between sessions; we denote the channel end by $?$ in such cases. Messages will be addressed by channel endpoints that consist of a name and a channel end. In channel endpoints we also permit the name to be $?$ ; this corresponds to a message that does not include the sender’s/receiver’s name, as in the case of unilateral TLS (recall that $A_{names}^{reg} \cap A_{names}^{pen} = {?}$ ).

We denote by $A_{ψ}$ a channel endpoint that belongs to A and uses channel end ψ. We will later ensure that for a confidential channel (Definition 3.9), messages sent to $A_{ψ}$ will only be received there; in particular, if A has two endpoints, $A_{ψ}$ and $A_{ϕ}$ , an attacker cannot redirect messages intended for one so that it is received at the other. Also, we will later ensure that for an authenticated channel (Definition 3.10), messages that claim to come from $A_{ψ}$ really do; in particular, if A has two endpoints, $A_{ψ}$ and $A_{ϕ}$ , an attacker cannot change a message sent from one so that it appears to have been sent from the other. Thus the endpoints provide a separation between sessions.

However, some protocols, such as unilateral TLS, do not authenticate a participant’s name. We denote the endpoint by $?_{ψ}$ in this case. Note that, if $ψ \neq ?$ , this channel will still provide a separation between sessions; this means that if the agent in question is authenticated at the application layer, for example via a username and password, the other participant can deduce that all the messages in the session were sent by that agent.

Definition 3.1.
We assume a set of channel types, $ChannelTypes$ , that contains a value ⊥ that represents the channel that provides no security guarantees.

$E$ denotes the set of channel ends. It has two subsets: penetrator channel ends, $E^{pen}$ , used by the penetrator; and regular channel ends, $E^{reg}$ , used by regular agents; we have $E^{reg} \cap E^{pen} = {?}$ .

The set of regular endpoints $I^{reg}$ is defined as $A_{names}^{reg} \times E^{reg}$ ; the set of penetrator endpoints $I^{pen}$ as $A_{names}^{pen} \times E^{pen}$ ; the set of endpoints $I$ as $I^{reg} \cup I^{pen}$ (note $I^{reg} \cap I^{pen} = {(?, ?)}$ ). $(A, ψ) \in I$ is denoted as $A_{ψ}$ . We abbreviate $?_{?}$ to $?$ . If $A_{ψ} \in I$ , then $name (A_{ψ}) \hat{=} A$ and $end (A_{ψ}) \hat{=} ψ$ .

In examples, we write ${TLS}^{C \to S}$ and ${TLS}^{S \to C}$ to represent the channel types of a unilateral TLS connection from client to server and server to client, respectively. The main difference between these channels concerns where $?$ occurs: in the case of ${TLS}^{C \to S}$ (i.e. unilateral TLS from the client to the server), the sender will be of the form $?_{ψ}$ , since unilateral TLS does not authenticate the client. Conversely, the recipient of a message over ${TLS}^{S \to C}$ (i.e. unilateral TLS from the sever to the client) will be of the form $?_{ψ}$ , whilst the sender will be of the form $A_{ψ}$ .

High-level terms model data being sent across the network.
Definition 3.2.
A high-level term is a tuple denoted as $σ (S_{ψ}, R_{ϕ}, m, c)$ where:
$σ \in {+, -}$ represents a message being sent or received, respectively;

$S_{ψ} \in I$ is the claimed sending endpoint of m;

$R_{ϕ} \in I$ is the intended recipient endpoint of m;

$m \in T$ is the application-layer message;

$c \in ChannelTypes$ is the channel type along which the term is communicated.
Let $\hat{T}$ be set of high-level terms. Given a high-level term $t = σ (S_{ψ}, R_{ϕ}, m, c)$ , we define $sender (t) \hat{=} S_{ψ}$ , $recipient (t) \hat{=} R_{ϕ}$ , $appmsg (t) \hat{=} m$ and $chan (t) \hat{=} c$ .

When the sign of a high-level term is irrelevant, we will elide $σ \in {+, -}$ .

From the above definition of high-level terms, high-level nodes, high-level strands, high-level strand spaces, high-level bundles and high-level origination can be defined analogously to the standard case presented in Section 2. We also lift the definitions of $sender (t)$ , $recipient (t)$ etc. to be defined over high-level nodes by defining $sender (n)$ as $sender (msg (n))$ , for example.

For the remainder of this section, fix a high-level strand space Σ.

Channel types determine the acceptable format of high-level terms. In particular, they determine the permissible channel endpoints. For example, if the channel was a bilateral TLS channel then the sender and recipient endpoints $A_{ψ}$ and $B_{ϕ}$ could not contain $?$ , either as a name or a channel end; conversely, if the channel was a ${TLS}^{C \to S}$ channel, where the sender’s name is not authenticated, then the sender’s channel endpoint would be of the form $?_{ψ}$ . The following assumption formalises the idea that channels have an associated high-level term format.
Assumption 3.3.
For every channel $c \in ChannelTypes$ :
Either every $(S_{ψ}, R_{ϕ}, m, c) \in \hat{T}$ has $S = ?$ , or none has $S = ?$ ;

Either every $(S_{ψ}, R_{ϕ}, m, c) \in \hat{T}$ has $ψ = ?$ , or none has $ψ = ?$ ;

Either every $(S_{ψ}, R_{ϕ}, m, c) \in \hat{T}$ has $R = ?$ , or none has $R = ?$ ;

Either every $(S_{ψ}, R_{ϕ}, m, c) \in \hat{T}$ has $ϕ = ?$ , or none has $ϕ = ?$ .

Note that if a strand makes exclusive use of bilateral channels then the sender’s name will typically be the same on each node and would be, for example, the name contained in the sender’s certificate if public-key certificates were being used by the transport protocol. Further, there is nothing to prohibit a transport protocol that reuses the same channel end with multiple names, e.g. $A_{ψ}$ and $B_{ψ}$ .
Definition 3.4.
The function $endpoints : Σ \to P (I^{reg})$ gives the set of local endpoints that a regular strand uses. $X_{χ} \in endpoints (st)$ iff there exists a node n on $st$ with $msg (n) = σ (S_{ψ}, R_{ϕ}, m, c)$ and such that: if $σ = +$ then $X_{χ} = S_{ψ}$ ; and if $σ = -$ then $X_{χ} = R_{ϕ}$ . Similarly, $ends : Σ \to P (E^{reg})$ gives the set of local channel ends that a strand uses.

As an example consider Fig. 1. This bundle represents a client retrieving e-mail via a hypothetical protocol that makes use of unilateral TLS. It contains a client strand ${st}_{C}$ and a server strand ${st}_{S}$ , such that $ends ({st}_{C}) = {ψ}$ and $ends ({st}_{S}) = {ϕ}$ . All messages are sent over a unilateral TLS channel where the server is authenticated and the client is not; thus, the client is identified as $?$ in every high-level term.

Fig. 1.
An example bundle illustrating how a regular agent on strand ${st}_{C}$ can retrieve e-mail from a server on strand ${st}_{S}$ via a hypothetical protocol.

This example illustrates the necessity of channel ends. Note that we need to ensure that $Messages$ is sent only to the source of $Passwd$ , even though the client herself is not authenticated by the transport channel. Without channel ends, a message sent along a unilateral channel c to the unauthenticated end would be represented by $(S, ?, m, c)$ . As this representation does not identify the recipient in any way, it would not be possible to decide if the penetrator was allowed to receive the message. Later we will specify that, for TLS-like channels, the penetrator is able to send and receive messages only on penetrator channel ends ( $E^{pen}$ ), thus ensuring he is unable to receive the second message.
3.2. The penetrator

We now consider how to model the penetrator. We start with messages that are sent over the unprotected channel ⊥ (i.e. not over a secure transport protocol). Clearly, we need to model the penetrator as the full Dolev–Yao penetrator and therefore we allow the penetrator to perform all the usual actions.

Definition 3.5.
The application-layer penetrator strands are strands of the following form: M
Text message: $⟨ + (?, ?, r, ⊥) ⟩$ where $r \in T_{P}$ ;
C
Concatenation: $⟨ - (?, ?, t_{0}, ⊥), - (?, ?, t_{1}, ⊥), + (?, ?, t_{0}^t_{1}, ⊥) ⟩$ ;
S
Separation: $⟨ - (?, ?, t_{0}^t_{1}, ⊥), + (?, ?, t_{0}, ⊥), + (?, ?, t_{1}, ⊥) ⟩$ ;
E
Encryption: $⟨ - (?, ?, k, ⊥), - (?, ?, t, ⊥), + (?, ?, {| t |}_{k}, ⊥) ⟩$ where $k \in K$ ;
D
Decryption: $⟨ - (?, ?, k^{- 1}, ⊥), - (?, ?, {| t |}_{k}), + (?, ?, t, ⊥) ⟩$ where $k \in K$ ;
KG
Key generation: $⟨ - (?, ?, t, ⊥), + (?, ?, g (t), ⊥) ⟩$ where $g \in Kgf$ .

We now consider what the penetrator can do with messages sent over a secure transport channel. For ease of exposition we firstly consider a restricted model in which the only secure transport protocols are bilateral and unilateral TLS. Clearly, we must allow the penetrator to receive messages intended for him, and to send messages coming from himself.
Definition 3.6.
The transport-layer penetrator strands for TLS-like protocols are of the following form, where $c \neq ⊥$ : SD
Send: $⟨ - (?, ?, m, ⊥), + (P_{ψ}, B_{ϕ}, m, c) ⟩$ where $P_{ψ} \in I^{pen}$ , $B_{ϕ} \in I^{reg}$ ;
RV
Receive: $⟨ - (A_{ψ}, P_{ϕ}, m, c), + (?, ?, m, ⊥) ⟩$ where $P_{ϕ} \in I^{pen}$ , $A_{ψ} \in I^{reg}$ .

Note that the side conditions $B_{ϕ} \in I^{reg}$ and $A_{ψ} \in I^{reg}$ merely avoid redundancies caused by the penetrator sending a message to himself.

Observe that SD strands allow the penetrator to send messages to regular strands from the client end of a unilateral TLS connection, and to claim to be some honest agent A within the application-layer message, e.g. $+ (?_{ψ}, B_{ϕ}, A^\dots, {TLS}^{C \to S})$ . However, from the server end of a unilateral TLS (or bilateral TLS) connection, he has to use a penetrator identity $P \in A_{names}^{pen}$ such that $P \neq ?$ , e.g. $+ (P_{ψ}, ?_{ϕ}, m, {TLS}^{S \to C})$ , so could not claim to have an identity other than P within m. Similarly RV strands allow the penetrator to receive, at the client end, messages intended for regular agents, e.g. $- (A_{ψ}, ?_{ϕ}, B^\dots, {TLS}^{S \to C})$ . But at the server end, such a message would have to have a penetrator identity as the recipient to allow a RV strand, e.g. $- (?, P_{ϕ}, P^\dots, {TLS}^{C \to S})$ .

Further, the definition captures session properties of TLS-like protocols. The condition $P_{ψ} \in I^{pen}$ ensures that if a regular strand receives two messages $(?_{ψ}, B_{ϕ}, m, c)$ and $(?_{ψ}, B_{ϕ}, m^{'}, c)$ , either both came from another regular strand (if $?_{ψ} \in I^{reg}$ ), or both come from penetrator SD strands (if $?_{ψ} \in I^{pen}$ ).

Figure 2 gives an example illustrating how the penetrator can use these strands to check his e-mail, using the same hypothetical protocol as earlier.

Fig. 2.
A figure illustrating how the penetrator can check his e-mail, using the same protocol as Fig. 1.

Generalising the secure transport protocol. For secure transport protocols that are weaker than TLS, there are many other ways for the penetrator to interact with transport messages. We now generalise the above in order to model such protocols. In particular, we follow the approach taken in [12,19] to define a more general penetrator that can also:
Learn a message sent to an honest endpoint (i.e. overhear);

Fake a message as coming from an honest endpoint;

Hijack a message, redirecting it to a different endpoint, and/or re-ascribing it as from a different endpoint (changing name and/or channel end).
Later, we will restrict the use of such strands to channels that do not provide confidentiality (in the case of learning) or authentication (in the case of faking or hijacking). Formally, we exclude penetrator strands from the strand spaces according to the guarantees it provides (noting that this introduces a proof obligation on the transport protocol). For example, in the case of bilateral TLS we exclude all of the above penetrator strands from the strand space.
Definition 3.7.
The transport-layer penetrator strands are SD and RV strands, as above, and strands of the following forms, where $c \neq ⊥$ : LN
Learn: $⟨ - (A_{ψ}, B_{ϕ}, m, c), + (?, ?, m, ⊥) ⟩$ where $A_{ψ}, B_{ϕ} \in I^{reg}$ ;
FK
Fake: $⟨ - (?, ?, m, ⊥), + (A_{ψ}, B_{ϕ}, m, c) ⟩$ where $A_{ψ}, B_{ϕ} \in I^{reg}$ ;
HJ
Hijack: $⟨ - (S_{ψ}, R_{ϕ}, m, c), + (S_{ψ^{'}}^{'}, R_{ϕ^{'}}^{'}, m, c) ⟩$ providing $S_{ψ} \neq S_{ψ^{'}}^{'}$ or $R_{ϕ} \neq R_{ϕ^{'}}^{'}$ .

Note that by Assumption 3.3 it is not possible for a HJ strand to change a message that uses $?$ as the sending channel end to one that uses a value different to $?$ .

Having defined the set of penetrator strands, we lift the usual definitions of penetrator paths, regular nodes, penetrator nodes, and bundle equivalence from the low-level strand space definitions in the obvious way.

We make one further assumption to ensure that a regular agent has exclusive usage of a number of channel ends to send and receive messages.
Assumption 3.8.
Let $B$ be a high-level bundle. For every pair of regular strands $st$ and ${st}^{'}$ in $B$ : $st \neq {st}^{'} ⟹ ends (st) \cap ends ({st}^{'}) \subseteq {?} .$ (3.1)

Channel properties. We now define channel properties that restrict the penetrator’s behaviour. There are many different channel properties. We consider only the most important; other definitions could be made if specialised applications require them. We define channel properties by stating the restrictions they impose upon the strand space.

The first property we consider is confidentiality. Intuitively this needs to prohibit the penetrator from learning any value that was sent along a confidential channel to a regular agent. Clearly, this requires LN strands to be prohibited; however, this is not sufficient. For example, suppose $A_{ψ}$ sends a message to $B_{ϕ}$ along a channel c that is confidential; if the penetrator could redirect the message to $P_{χ} \in I^{pen}$ , then he would be able to do a receive and thus can obtain the message indirectly; we therefore prohibit such behaviours.
Definition 3.9 (Confidential).

We let $Conf \subseteq ChannelTypes ∖ {⊥}$ denote the subset of channels that are confidential. If $c \in Conf$ then $\hat{Σ}$ contains no LN strands on c, or HJ strands of the form $⟨ - (S_{ψ}, R_{ϕ}, m, c), + (S_{ψ^{'}}^{'}, R_{ϕ^{'}}^{'}, m, c) ⟩$ where $R_{ϕ} \neq R_{ϕ^{'}}^{'}$ and $R_{ϕ} \in I^{reg}$ .

Note that the above definition also prohibits changing the recipient from $R_{ψ}$ to $R_{ψ^{'}}$ where $R \in A_{names}^{reg}$ and $ψ, ψ^{'} \in E^{reg}$ , i.e. it prevents the receiving channel end from being changed, even if it is still being received by the same entity. For example, suppose a single agent is running multiple services that hold data in different levels of security. If the agent also broadcasts data that was received at a lower security level, then it is essential that data cannot be re-routed to different services and thus different channel ends.

The above is a significant difference to other formalisations. For example, [3] defines a confidentiality property, but does not consider sessions so confidentiality is only considered relative to a particular name. Further, [22] defines a Confidential Channel, but has no direct support for modelling segmented sessions, as above. We believe the above is a very useful guarantee and, actually more accurately corresponds to the guarantees a channel implementation is likely to provide.

Many application-layer protocols require a guarantee that messages came from a certain source or were intended for a particular destination, i.e. that the channel is authenticated. Thus, this means that FK strands must be prohibited on this channel. Further, hijacks must be prohibited since these allow messages to be sent to unintended destinations or have incorrect senders.

Definition 3.10 (Authenticated).

We let $Auth \subseteq ChannelTypes ∖ {⊥}$ denote the subset of channels that are authenticated. If $c \in Auth$ then there are no FK or HJ strands on c in $\hat{Σ}$ .

Note that an authenticated channel does not authenticate the origin of the message, but only the sender. Thus, if B receives a message of the form $(A_{ψ}, B_{ϕ}, m, c)$ where $c \in Auth$ , then B can conclude A knows the message m, and intended to send it to B, but cannot conclude that A originated the message: A may merely be a relaying party.

The definition of $Auth$ does not prohibit the channel end or name being $?$ . Clearly, for authenticity to mean something to the application-layer protocol, the application layer may (for example) require the name to be not equal to $?$ . This is a requirement of the protocol model: the model needs to specify what assumptions it is making about the channel ends and names.

The conjunction of $Auth$ and $Conf$ is known as $AuthConf$ . Note that the only penetrator strands allowed on a $AuthConf$ are SD and RV strands and thus, as discussed earlier, it corresponds to the security guarantees modelled by TLS. See, e.g. [21], for a proof that TLS satisfies the claimed properties.2

²
[21] uses the low-level strand spaces model to prove TLS correct. Utilising Section 4 it would be straightforward to prove that TLS indeed only allows RV and SD strands; however, this is beyond the scope of this paper.

Henceforth, we assume

{TLS}^{C \to S}

and

{TLS}^{S \to C}

satisfy

AuthConf

High-level normality. As with the low-level strand spaces model, there are a large number of ways for the penetrator to construct a message and thus, we define a normal form for bundles that avoids redundancies. We will require that bundles contain no low-level redundancies, as per Definition 2.13, but also that there are no redundancies amongst the high-level strands (e.g. FK–LN strand pairs).

We proceed as per the low-level case, and begin by defining what it means for $\Rightarrow^{+}$ -edges to be constructive and destructive. This definition is then used to define several types of penetrator paths, which are then used to define what it means for a bundle to be normal. We formalise these notions as follows.

Definition 3.11.

A $\Rightarrow^{+}$ -edge is constructive if it lies on a E, C, KG, SD or FK strand, destructive if it lies on a D, S, RV or LN strand, or normal if it lies on a HJ strand. A penetrator path p in a high-level bundle $B$ is constructive iff it consists entirely of constructive edges, destructive iff it consists entirely of destructive edges, or normal iff either:

p is a single HJ strand; or

whenever a constructive edge sends to a destructive edge in p, the constructive edge must be a KG strand.

A high-level bundle

B

is normal iff every penetrator path that does not traverse a key edge is normal.

In order to prove that every high-level bundle is equivalent to a normal bundle, we require several assumptions on what transport-layer strands the strand space contains. For example, by the above definition, penetrator paths that consist of a SD strand followed by a HJ strand are prohibited in a normal bundle. Thus, we replace this by a single FK or SD strand that sends the message to the correct agent immediately. Hence, we need to ensure that whenever the strand space contains the SD–HJ strand pair, it also allows the equivalent FK or SD strand. More generally, we need a number of assumptions about what strands the strand space has to allow, given that it allows a particular strand or pair of strands.

Fig. 3.

An illustration of Assumption 3.12(1).

Assumption 3.12.

Every high-level strand space Σ satisfies the following properties:

If a HJ strand immediately followed by a RV or LN strand is in the strand space then the equivalent RV or LN strand is also in the strand space. This is illustrated in Fig. 3.

If a SD or FK strand immediately followed by a HJ strand is in the strand space then the equivalent SD or FK strand is also in the strand space.

If multiple adjacent HJ strands are in the strand space then the equivalent singleton HJ strand is also in the strand space.

Note that the strands prohibited by the $Auth$ , $Conf$ and $AuthConf$ definitions do not conflict with the strands required by the above definition. Further, observe that the above assumptions only consider penetrator paths and simply modify their internal structure. From an observer’s point of view (e.g. a regular agent), the behaviour of the new strand is indistinguishable from the behaviour of the previous penetrator path.

Lemma 3.13.

Every high-level bundle is equivalent to a normal high-level bundle.

3.3. Example

We now present a simple example of how the model can be used. A more complex example can be found in [14,15] in which WebAuth [25], a single-sign-on protocol, is analysed.

The following protocol allows a user U to authenticate to a login server $LS$ , who authorises U to access an application server $AS$ , which provides U with access to a resource. $\begin{matrix} (1) & U & \to & LS & : & AS^U^{Password}_{LS} (U), \\ (2) & LS & \to & U & : & {| {| U |}_{PK (AS)} |}_{SK (LS)}, \\ (3) & U & \to & AS & : & {| {| U |}_{PK (AS)} |}_{SK (LS)}, \\ (4) & AS & \to & U & : & {Resource}_{AS}^{U} . \end{matrix}$

Using the above, the strands can be defined as follows (assuming that $Password$ is a function). Note that all communication occurs over unilateral TLS where U is unauthenticated. Further, there are two distinct session (as identified by the channel ends): the first session consists of the first two messages with $LS$ , whilst the second consists of the messages with $AS$ . $\begin{array}{l} User [ψ, ψ^{'}, ϕ, ϕ^{'}, U, LS, AS, t] \\ \hat{=} ⟨ + (?_{ψ}, {LS}_{ϕ}, AS^U^{Password}_{LS} (U), {TLS}^{C \to S}), \\ - ({LS}_{ϕ}, ?_{ψ}, t, {TLS}^{S \to C}), \\ + (?_{ψ^{'}}, {AS}_{ϕ^{'}}, t, {TLS}^{C \to S}), \\ - ({AS}_{ϕ^{'}}, ?_{ψ^{'}}, {Resource}_{AS}^{U}, {TLS}^{S \to C}) ⟩, \\ LoginServer [ψ, ϕ, U, LS, AS] \\ \hat{=} ⟨ - (?_{ψ}, {LS}_{ϕ}, AS^U^{Password}_{LS} (U), {TLS}^{C \to S}), \\ + ({LS}_{ϕ}, ?_{ψ}, {| {| U |}_{PK (AS)} |}_{SK (LS)}, {TLS}^{S \to C}) ⟩, \\ AppServer [ψ^{'}, ϕ^{'}, U, LS, AS] \\ \hat{=} ⟨ - (?_{ψ^{'}}, {AS}_{ϕ^{'}}, {| {| U |}_{PK (AS)} |}_{SK (LS)}, {TLS}^{C \to S}), \\ + ({AS}_{ϕ^{'}}, ?_{ψ^{'}}, {Resource}_{AS}^{U}, {TLS}^{S \to C}) ⟩ . \end{array}$

In order to prove the above protocol correct, some assumptions on the security of the password are required. We formalise what it means for a term t to be confidential as follows.

Definition 3.14.
A term t is confidential in a high-level bundle $B$ iff no equivalent bundle contains a positive node n such that $msg (n) = + (?, ?, t, ⊥)$ .

If the above holds then it is impossible for the penetrator to obtain the term t in any way. We quantify over all equivalent bundles in order to ensure we consider all possible ways in which the penetrator could obtain the value without altering the regular behaviour.

In [14,15] we present proof rules that allow one to verify properties of protocols such as these. For example, it is possible to verify that, assuming U, $LS$ and $AS$ are regular and that the password is confidential, only U obtains ${Resource}_{AS}^{U}$ . Note that these proof rules essentially ignore the prospect of type-flaw attacks, where a term can be viewed in two different ways (e.g. as a nonce and as an encryption). In the strand spaces model it is common to ignore the possibility of type-flaw attacks since the term algebra is assumed to be freely generated. However, it would be possible to extend the algebra to allow type-flaw attacks to be modelled, although it would require a different proof style to the above.
4. Soundness of the abstraction

Analysing layered security protocols by abstracting away from the implementation of the transport layer introduces a proof obligation that this abstraction is sound. In this section we begin to prove that if there is an attack on the protocol when implemented using a transport-layer protocol that satisfies the channel properties, then there is also an attack on the abstracted protocol. The outline of the overall proof is as follows:

In Section 4.2 and Section 4.3 we define what it means for a high-level bundle to abstract a low-level bundle. Informally, this means that they have the same application-layer behaviour. In Section 4.4 we define what it means for a bundle to be interference-free and use this to prove that every interference-free bundle can be abstracted.

Section 5 proves that every bundle $B$ of a low-level strand space Σ that satisfies our statically checkable condition, known as disjoint-layered encryption, can be transformed to an interference-free low-level bundle $B^{'}$ of a related strand space $Σ_{E}$ . Further, $B ⊵ B^{'}$ which, informally, means that $B^{'}$ has similar application-layer behaviour.

Lastly, Section 6 introduces a logic in which protocol-correctness properties can be expressed. We also prove that if ϕ is such a property, whenever $B ⊵ B^{'}$ and ϕ is not satisfied by $B$ , then ϕ is not satisfied by $B^{'}$ . This implies that the transformations of Section 5 preserve any application-layer incorrectness. Lastly, we prove that whenever ${\hat{B}}^{'}$ abstracts $B^{'}$ and $B^{'}$ does not satisfy a property ϕ, then ${\hat{B}}^{'}$ also does not.

Hence the model is sound since if there is an attack against a low-level bundle, there is an attack against a high-level bundle.

For the remainder of this paper, we will denote high-level objects with a hat (e.g. $\hat{B}$ denotes a high-level bundle).

4.1. Preliminaries

In order to define low-level penetrator behaviours like sending and hijacking, we define different types of penetrator paths. Recall that a penetrator path is a sequence of nodes where each consecutive pair of nodes is linked by either $\Rightarrow^{+}$ or → and, with the exception of the first and last nodes, must all be penetrator nodes.

Definition 4.1.
A penetrator path p in a low-level bundle is:
normal iff whenever a constructive edge sends to a destructive edge, the constructive edge is a KG strand (cf. Definition 2.12);

constructive iff it only traverses constructive edges;

destructive iff it only traverses destructive edges.

We will frequently wish to check if a given term is the application-layer message of a transport-layer message. However, we cannot use the subterm relation to check this since the transport-layer packaging may include the application-layer message. Hence, we would like the ability to retrieve the term that lies in a particular position. We thus define extraction paths which allow us to specify the subterm to extract from a term, given the position of it. Conceptually, they are paths in the abstract syntax tree.
Definition 4.2.
The set of all extraction paths, $E P$ , is defined as ${1, 2, Decrypt}^{}$ . The partial function $extract : T \times E P \to T$ is defined by: $\begin{array}{l} extract (t, ⟨ ⟩) \hat{=} t, \\ extract (t_{1}^t_{2}, ⟨ i ⟩^p) \hat{=} extract (t_{i}, p), \\ extract ({| m |}_{k}, ⟨ Decrypt ⟩^p) \hat{=} extract (m, p) . \end{array}$ Given an extraction path $es$ and $x \in {1, 2, Decrypt}$ , we write $x in es$ iff there exists an index i such that the ith element is x. We denote $t_{1} = extract (t_{2}, es)$ by $t_{1} ⊑_{es} t_{2}$ , i.e. $t_{1}$ is the subterm of $t_{2}$ at position $es$ .

For example, if $t = {| t_{1} |}_{k}^t_{2}$ , then $t_{1} = extract (t, ⟨ 1, Decrypt ⟩)$ (i.e. $t_{1} ⊑_{⟨ 1, Decrypt ⟩} t$ ) and $t_{2} = extract (t, ⟨ 2 ⟩)$ .

Fig. 4.
A bundle containing a destructive penetrator path $⟨ n_{1}, n_{2}, n_{5}, n_{6} ⟩$ .

It will be helpful, particularly in Section 5, to consider what the penetrator is doing in terms of extraction paths. For example, consider Fig. 4 and the destructive penetrator path $⟨ n_{1}, n_{2}, n_{5}, n_{6} ⟩$ . This penetrator path takes the first component of a concatenation and then decrypts the message. Therefore, this can be represented by the extraction path $⟨ 1, Decrypt ⟩$ . In general, given a destructive or constructive penetrator path that does not cross a key-edge, it is possible to obtain a corresponding extraction path. This is formalised below.
Lemma 4.3.
Let p be a constructive or destructive penetrator path in a bundle starting at a node* $n_{1}$ and ending at a node $n_{| p |}$ . Providing p does not traverse a key edge or a KG strand there exists a unique extraction path $es$ such that:
If p is destructive $extract (msg (n_{1}), es) = msg (n_{| p |})$ ; we define $expath (p) \hat{=} es$ ;

If p is constructive $extract (msg (n_{| p |}), es) = msg (n_{1})$ ; we define ${expath}^{\sim} (p) \hat{=} es$ .

Transport-layer modelling. We now define how to extract application-layer information, such as the sender of a transport-layer message, from a low-level strand space. We also define some assumptions on the transport-layer protocols in order to ensure well-definedness. Throughout this section we use the example of a simple transport-layer protocol that sends an application-layer message m from A to B as follows: $\begin{matrix} (1) & A & \to & B & : & {| k |}_{PK (B)}, \\ (2) & A & \to & B & : & A^B^{| m |}_{k} . \end{matrix}$ This channel is confidential, as only B can decrypt the message containing they key k, but is not authentic as the penetrator can trivially alter the apparent sender by changing message 2. An example bundle, which is used throughout the following, is given in Fig. 5.

Fig. 5.
A low-level bundle that sends application-layer messages, one over the unprotected channel and another using a simple transport-layer protocol. The corresponding high-level bundle is also given. (a) The low-level bundle. (b) The corresponding high-level bundle.

We start by stating an assumption regarding the partitioning of the set of regular nodes according to the type of transport-layer content they contain. Note that in the following we give informal meanings to the different sets of nodes; other assumptions in this section will impose sufficient conditions on the partition to ensure that the partition satisfies these informal descriptions.
Assumption 4.4.
The set of regular nodes $N^{reg}$ is partitioned between:
The set of transport-layer nodes, denoted $N_{trpt}$ , that contains all regular nodes that send or receive application-layer messages on a channel other than ⊥. For all $c \in ChannelTypes ∖ {⊥}$ , $N_{trpt}^{c}$ denotes the subset of $N_{trpt}$ that send or receive messages on channel c; we assume that these sets are disjoint.

The set of unprotected regular nodes, denoted $N_{⊥}$ , that contains all regular nodes that send or receive application-layer messages over ⊥.

The set of transport-layer non-message nodes, denoted $N_{non - payload}$ , that contains all regular nodes that are related to the transport layer, but do not send or receive application-layer messages (e.g. handshake nodes). For all $c \in ChannelTypes ∖ {⊥}$ , let $N_{non - payload}^{c}$ denote the subset of $N_{non - payload}$ that relate to channel c; again, we assume that these sets are disjoint.
The set of application-layer nodes, denoted $N_{payload}$ , is defined as $N_{trpt} \cup N_{⊥}$ .

For example, in Fig. 5, set definitions that would satisfy the intuition above are ${n_{1}, n_{4}} = N_{⊥}^{c}$ , ${n_{2}, n_{5}} = N_{non - payload}^{c}$ and ${n_{3}, n_{6}} = N_{trpt}^{c}$ .

We now consider how to transform transport-layer messages into high-level terms by making a number of assumptions on the structure of transport-layer messages, as formalised below.
Assumption 4.5.
For each channel $c \in ChannelTypes ∖ {⊥}$ we assume the existence of an extraction path ${expath}^{c} (c) \neq ⟨ ⟩$ such that $extract ({expath}^{c} (c), t)$ is defined for all $msg (n)$ where $n \in N_{trpt}^{c}$ .
Definition 4.6.
For all channels $c \in ChannelTypes ∖ {⊥}$ , define:
The set of transport-layer payload terms, $T_{payload}^{c}$ , that contains all terms that carry an application-layer payload on channel c by: $T_{payload}^{c} \hat{=} {msg (n) ∣ n \in N_{trpt}^{c}}$ .

The set of transport-layer non-payload terms, $T_{non - payload}^{c} \subseteq T$ , that contains non-message carrying terms used by channel c (e.g. handshake terms) by: $T_{non - payload}^{c} \hat{=} {msg (n) ∣ n \in N_{non - payload}^{c}}$ .
Further, we define: $\begin{matrix} T_{payload}^{⊥} \hat{=} {msg (n) ∣ n \in N_{⊥}}, & T_{non - payload}^{⊥} \hat{=} \emptyset, \\ T_{payload} \hat{=} ⋃_{c \in ChannelTypes} T_{payload}^{c}, & T_{non - payload} \hat{=} ⋃_{c \in ChannelTypes} T_{non - payload}^{c} . \end{matrix}$

For example, considering Fig. 5, the example channel c, and the above sets of nodes, $T_{payload}^{c}$ contains all terms of the form $A^B^{| {appmsg}_{2} |}_{k}$ , $T_{non - payload}^{c}$ contains all terms of the form ${| k |}_{PK (B)}$ and ${expath}^{c} (c) = ⟨ 2, 2, Decrypt ⟩$ (recall ^ associates to the right).

Note that the existence of ${expath}^{c} (c)$ implicitly assumes that the application-layer message is a subterm of the transport-layer payload term. Further, it requires that all application-layer messages on a given channel are packaged in the same way. These conditions are satisfied by every secure transport protocol that we have considered, including TLS, IPsec and SSH.
Assumption 4.7.
For each low-level bundle $B$ of Σ there exists: ${sender}_{B}^{c} : T_{payload}^{c} \to I$ that gives the sender of a transport-layer payload term on channel c; ${recipient}_{B}^{c} : T_{payload}^{c} \to I$ that gives the recipient of a transport-layer payload term on channel c. Further, for each regular node $n \in N_{trpt}$ , if n is positive, ${sender}_{B} (msg (n)) \in I^{reg}$ and, if n is negative, ${recipient}_{B} (msg (n)) \in I^{reg}$ .

Observe that we cannot define $sender$ and $recipient$ over the strand space since it is possible for the sender or recipient of a particular transport-layer term to be different in different bundles. For example, if the transport-layer protocol in use was TLS then the sender and recipient of a given transport-layer term are determined by the encryption key used to protect the application-layer message, which can be reused in different bundles.

Using the above functions we define several functions that extract components from arbitrary transport-layer payload terms. In order to define these functions it is necessary to know which channel a particular transport-layer payload term was sent on. To ensure such a function is well-defined we need to ensure that no two channels share any transport-layer payload terms.
Assumption 4.8.
For all distinct channels $c_{1} \neq ⊥$ and $c_{2} \neq ⊥$ , $T_{payload}^{c_{1}} \cap T_{payload}^{c_{2}} = \emptyset$ .

Given the above assumption we can now define the following functions.
Definition 4.9.
Let Σ be a low-level strand space. Define the following functions over $T_{payload}$ : $chan (t) \hat{=} c where t \in T_{payload}^{c}, appmsg (t) \hat{=} extract (t, {expath}^{c} (chan (t))) .$ Thus $chan$ gives the channel of a transport-layer term; and $appmsg$ gives the application-layer message contained in a transport-layer term.

For each bundle $B$ of Σ we define ${sender}_{B}, {recipient}_{B} : T_{payload} \to I$ , which give the claimed sender and intended recipient end points of a transport-layer term, respectively: ${sender}_{B} (t) \hat{=} {sender}_{B}^{chan (t)} (t), {recipient}_{B} (t) \hat{=} {recipient}_{B}^{chan (t)} (t) .$ When the bundle is clear from the context we simply write $sender (t)$ and $recipient (t)$ . We lift $chan$ , $sender$ and $recipient$ to be defined on $N_{trpt}$ in the obvious way (e.g. $chan (n) = chan (msg (n))$ . We lift $appmsg$ to be defined on $N_{payload}$ by defining $appmsg (n)$ to be $msg (n)$ if $n \in N_{⊥}$ and $appmsg (msg (n))$ otherwise (i.e. if $n \in N_{trpt}$ ).

For example, in Fig. 5, $sender (msg (n_{3})) = A_{?}$ , $recipient (msg (n_{3})) = B_{?}$ , $appmsg (msg (n_{3})) = {appmsg}_{2}$ and $chan (msg (n_{3})) = c$ .

Recall that in Assumption 3.3 we disallowed the penetrator from transforming a message where, for example, the sending channel end was $?$ into one where the sending channel end was not $?$ . Further, in Eq. (3.1), we required that distinct regular strands use disjoint channel ends. In order to ensure that there are no penetrator behaviours that would be prohibited at the high-level we need to lift these assumptions to the low-level, as follows.
Assumption 4.10.
For all low-level bundles $B$ , channels $c \in ChannelTypes ∖ {⊥}$ , and terms $t_{1}, t_{2} \in T_{payload}^{c}$ sent on c:
$name ({sender}_{B} (t_{1})) = ?$ iff $name ({sender}_{B} (t_{2})) = ?$ ;

$end ({sender}_{B} (t_{1})) = ?$ iff $end ({sender}_{B} (t_{2})) = ?$ ;

$name ({recipient}_{B} (t_{1})) = ?$ iff $name ({recipient}_{B} (t_{2})) = ?$ ;

$end ({recipient}_{B} (t_{1})) = ?$ iff $end ({recipient}_{B} (t_{2})) = ?$ .
For all low-level bundles $B$ and strands $st$ and ${st}^{'}$ in $B$ , if $st \neq {st}^{'}$ then ${ends}_{B}^{'} (st) \cap {ends}_{B}^{'} ({st}^{'}) = \emptyset$ (cf. Assumption 3.8), where ${ends}_{B}^{'}$ is the low-level version of $ends$ : $\begin{array}{rcl} {ends}_{B}^{'} (st) & \hat{=} & {end ({sender}_{B} (n)) ∣ n \in N_{trpt} \land sign (n) = + \land n is on st} \\ \cup {end ({recipient}_{B} (n)) ∣ n \in N_{trpt} \land sign (n) = - \land n is on st} . \end{array}$
4.2. Relating regular nodes

The first step in the proof is to define an abstraction function, ${\hat{α}}_{B}$ , that translates low-level terms from $B$ into the corresponding high-level terms. For example, given the low-level term $A^B^{| m |}_{PK (B)}$ above, ${\hat{α}}_{B}$ returns $(A, B, m, c)$ .

Definition 4.11.
Let $B$ be a low-level bundle. The term mapping function ${\hat{α}}_{B} : T \to \hat{T}$ that maps low-level terms to the corresponding high-level terms is defined as follows:
for $m \in T_{payload}$ : ${\hat{α}}_{B} (m) \hat{=} ({sender}_{B} (m), {recipient}_{B} (m), appmsg (m), chan (m))$ ;

for $m \in T ∖ T_{payload}$ , ${\hat{α}}_{B} (m) = (?_{?}, ?_{?}, m, ⊥)$ .
The bundle is omitted when it is clear from the context.

Using the above we specify how the low and high-level regular nodes are related, as follows.
Definition 4.12.
A regular node map is a partial function $\hat{ϕ}$ that maps regular nodes of a low-level bundle $B$ onto those of a high-level bundle $\hat{B}$ and such that:
$dom (\hat{ϕ}) = N_{payload}$ ;

${\hat{α}}_{B} (msg (n)) = msg (\hat{ϕ} (n))$ ;

$\hat{ϕ}$ is injective and surjective onto the regular nodes of $\hat{B}$ ;

for $n, n^{'} \in dom (\hat{ϕ})$ , $n \Rightarrow_{B}^{+} n^{'}$ iff $\hat{ϕ} (n) \Rightarrow_{\hat{B}}^{+} \hat{ϕ} (n^{'})$ .

For example, the regular node map between the low and high-level bundles of Fig. 5 is given by the function $\hat{ϕ}$ where $\hat{ϕ} (n_{1}) = {\hat{n}}_{1}$ , $\hat{ϕ} (n_{3}) = {\hat{n}}_{3}$ , $\hat{ϕ} (n_{4}) = {\hat{n}}_{4}$ , $\hat{ϕ} (n_{8}) = {\hat{n}}_{8}$ .
4.3. Relating penetrator nodes

In this section we define how the penetrator nodes of the low-level bundle are related to the penetrator nodes of the high-level bundle. This is done by defining two different maps, the first of which maps application-layer nodes to high-level penetrator nodes. This definition is similar to Definition 4.12.

Definition 4.13.
An application-layer penetrator node map is a partial injective function ${\hat{β}}_{1}$ from penetrator nodes of $B$ to those of $\hat{B}$ , whose domain is a subset of $N ∖ N_{payload}$ , and such that if $n \in dom ({\hat{β}}_{1})$ then:
${\hat{α}}_{B} (msg (n)) = msg ({\hat{β}}_{1} (n)) = (?_{?}, ?_{?}, msg (n), ⊥)$ ;

${\hat{β}}_{1} (n)$ is on the same type of strand as n (e.g. if n is on a low-level E strand then ${\hat{β}}_{1} (n)$ is on a high-level E strand);

${\hat{β}}_{1}$ respects the strand structure: for $n, n^{'} \in dom ({\hat{β}}_{1})$ , $n \Rightarrow^{+} n^{'}$ iff ${\hat{β}}_{1} (n) \Rightarrow^{+} {\hat{β}}_{1} (n^{'})$ .

For example, considering the bundles shown in Fig. 6, a valid application-layer penetrator node map would map $n_{1}$ , $n_{2}$ , $n_{3}$ , $n_{4}$ and $n_{5}$ to ${\hat{n}}_{1}$ , ${\hat{n}}_{2}$ , ${\hat{n}}_{3}$ , ${\hat{n}}_{4}$ and ${\hat{n}}_{5}$ , respectively.

Relating transport-layer penetrator nodes requires more thought since some of the transport-layer high-level penetrator strands (i.e. HJ, FK strands etc.) do not correspond directly to single low-level penetrator strands, but instead to a collection of them. For example, consider the transport-layer protocol (which we will use as a running example for the remainder of this section) that encodes a high-level term $t = (A_{?}, B_{?}, m, c)$ by $A^{| m |}_{PK (B)}$ . Using this protocol, the path from $n_{8}$ to $n_{13}$ in Fig. 6(a) is the low-level representation of a high-level SD strand that sends the message $m^n$ to an honest agent B. We will define a mapping from such low-level penetrator paths to the corresponding high-level penetrator strands.

Fig. 6.
An illustration of how the low-level penetrator paths and high-level penetrator strands relate. (a) A bundle containing a low-level Send penetrator path. (b) The corresponding high-level bundle, including the high-level SD strand.

We will also require a high-level penetrator strand that simply copies the application-layer message. This is required for technical reasons, which are discussed in Remark 4.18.
Definition 4.14.
The transmit strand is defined as: TX
Transmit: $⟨ - (A_{ψ}, B_{ϕ}, m, c), + (A_{ψ}, B_{ϕ}, m, c) ⟩$ .

Clearly TX strands are unnecessary in a high-level bundle, in the sense that they can be replaced by a direct message sending edge. This is formalised in Proposition 6.17 which proves it is sufficient to consider high-level bundles without TX strands. Note that we also assume that all channels permit TX strands, which will be required in Proposition 4.28.

In order to define the various transport-layer penetrator strands, we will need to identify when a penetrator path is sending or receiving an application-layer message. We can formalise such a definition by using extraction paths, as follows.
Definition 4.15.
We say that a destructive penetrator path $p_{d}$ starting at a node n extracts the application message from n, written $p_{d} app - extracts n$ , iff $expath (p_{d}) = {expath}^{c} (chan (n))$ . A constructive penetrator path $p_{c}$ ending at a node n packages the application message of n, denoted $p_{c} app - packages n$ , iff ${expath}^{\sim} (p_{c}) = {expath}^{c} (chan (n))$ .

Consider the low-level penetrator paths that correspond to the normal high-level penetrator strands, i.e. HJ and TX strands. All of these penetrator strands do not alter, or even inspect the enclosed application-layer message. Therefore, a low-level penetrator path that corresponds to one of these strands should, again, not extract the application-layer message from the transport-layer packaging. We formalise this as follows.
Definition 4.16.
A normal penetrator path p transports the application-layer message iff $p (1), p (| p |) \in N_{trpt}$ , $chan (p (1)) = chan (p (| p |))$ , and there exists $p_{d}$ , and $p_{c}$ such that $p = p_{d}^p_{c}$ , $p_{d}$ is destructive, $p_{c}$ is constructive and $expath (p_{d}) = {expath}^{\sim} (p_{c}) ⩽ {expath}^{c} (chan (p (1)))$ .

We now define how low-level penetrator paths correspond to high-level penetrator strands.

Fig. 7.
Various penetrator paths from Definition 4.17 using the running example of a secure transport protocol. In each case, the penetrator path runs from the top-left node, to the bottom-right node. (a) A Receive path for $A \in A_{names}^{reg}$ , $P \in A_{names}^{pen}$ . (b) A Send path for $A \in A_{names}^{reg}$ , $P \in A_{names}^{pen}$ . (c) A Learn path for $A, B \in A_{names}^{reg}$ , assuming that the penetrator obtains $SK (B)$ somehow. (d) A Fake path for $A, B \in A_{names}^{reg}$ . (e) A Hijack path for $A \in A_{names}^{reg}$ , $P \in A_{names}^{pen}$ . (f) A Transmit path, assuming that the running example has been augmented with nonces.
Definition 4.17.
Let p be a penetrator path in a low-level bundle, starting at a node n and ending at a node $n^{'}$ . p is a transport-layer penetrator path iff it is of one of the following forms (these paths are illustrated in Fig. 7): Receive

n is a positive regular node and $n^{'}$ is a negative penetrator node;

p is destructive;

$n \in N_{trpt}$ ;

$sender (msg (n)) \in I^{reg}$ ;

$recipient (msg (n)) \in I^{pen}$ ;

$p app - extracts n$ .

Learn
As per a Receive path, but $recipient (msg (n)) \in I^{reg}$ .
Fake

n is a positive penetrator node and $n^{'}$ is a negative regular node;

p is constructive;

$n^{'} \in N_{trpt}$ ;

$sender (msg (n^{'})) \in I^{reg}$ ;

$recipient (msg (n^{'})) \in I^{reg}$ ;

$p app - packages n^{'}$ .

Send
As per a Fake path, but $sender (msg (n^{'})) \in I^{pen}$ .
Hijack

n is a positive regular node and $n^{'}$ is a negative regular node;

p is normal;

$n, n^{'} \in N_{trpt}$ ;

$appmsg (n^{'}) = appmsg (n)$ ;

$chan (msg (n^{'})) = chan (msg (n))$ ;

$sender (msg (n)) \neq sender (msg (n^{'}))$ or $recipient (msg (n)) \neq recipient (msg (n^{'}))$ ;

p transports the application-layer message.

Transmit
As per Hijack path, but $sender (msg (n)) = sender (msg (n^{'}))$ and $recipient (msg (n)) = recipient (msg (n^{'}))$ .

Remark 4.18.
As an example of why Transmit paths are needed consider the transport-layer protocol that encodes the high-level term $(A, B, m, c)$ as $d^A^{| m |}_{PK (B)}$ where d is a nonce. This can be transformed by the penetrator to $d^{'}^A^{| m |}_{PK (B)}$ where $d \neq d^{'}$ . However, the corresponding high-level term is unchanged and thus, as we do not wish to remove penetrator paths from the high-level bundle, there needs to be a penetrator path to reflect this.

We now define a second map involving penetrator nodes that maps nodes on penetrator paths to nodes on high-level penetrator strands. Note that the map cannot be a function since a subsequence of a penetrator path could be part of two different penetrator paths. For example, consider the penetrator path in Fig. 6(a); if the penetrator wanted to send the message from two different penetrator identities then he could create another C strand that would receive from the E strand and thus the first nodes of the penetrator paths would be shared.
Definition 4.19.
A transport-layer penetrator node map is a relation ${\hat{β}}_{2}$ between the penetrator nodes of $B$ and $\hat{B}$ that:
Maps the first and last penetrator nodes of Send, Receive, Learn, Fake, Hijack and Transmit paths to the first and last nodes of high-level SD, RV, LN, FK, HJ and TX strands respectively, and relates no other nodes;

${\hat{α}}_{B} (msg (n)) = msg (\hat{n})$ for $(n, \hat{n}) \in {\hat{β}}_{2}$ .

For example, again considering the bundles from Fig. 6, a suitable transport-layer penetrator node map would map $n_{8}$ and $n_{13}$ to ${\hat{n}}_{8}$ and ${\hat{n}}_{13}$ , respectively.

Using the above definitions in conjunction with those from Section 4.2 it is now possible to define a node map for a bundle $B$ that maps the regular and penetrator nodes to nodes of a high-level bundle. In particular, the map explains how each high-level node and strand corresponds to low-level nodes and strands.
Definition 4.20.
A node map is a relation $\hat{ψ}$ between the nodes of $B$ and $\hat{B}$ , such that:
$\hat{ψ}$ is of the form $\hat{ϕ} \cup {\hat{β}}_{1} \cup {\hat{β}}_{2}$ , where $\hat{ϕ}$ , ${\hat{β}}_{1}$ and ${\hat{β}}_{2}$ are as in Definitions 4.12, 4.13, 4.19, respectively;

$\hat{ψ}$ is surjective onto the nodes of $\hat{B}$ ;

$\hat{ψ}$ respects the strand structure:

if $n, n^{'} \in dom (\hat{ψ})$ and $n \to_{B} n^{'}$ then $\exists \hat{n}, {\hat{n}}^{'} \cdot n \hat{ψ} \hat{n} \land n^{'} \hat{ψ} {\hat{n}}^{'} \land \hat{n} \to_{\hat{B}} {\hat{n}}^{'}$ ;

if $\hat{n} \to_{\hat{B}} {\hat{n}}^{'}$ , then $\exists n, n^{'} \cdot n \hat{ψ} \hat{n} \land n^{'} \hat{ψ} {\hat{n}}^{'} \land n \to_{B} n^{'}$ .

Note that in some cases there may be multiple, equally valid, node maps from a low-level bundle. For example, a Receive path followed by a Send path could be mapped to a RV and SD strand. However, providing the receive and send are both on the same channel this could be viewed as a Hijack path, and thus mapped to a HJ strand.
4.4. Interference-freedom and abstract correctness

In this section we consider the conditions under which we can safely abstract away from the transport-layer behaviour. In particular, we develop a condition that holds whenever a term t is constructed by the penetrator in a way that can be mirrored in a high-level bundle. Further, we describe a bundle condition, interference-freedom that is true whenever the bundle can be safely abstracted, in the following sense.

Definition 4.21.
A high-level bundle $\hat{B}$ abstracts a low-level bundle $B$ iff there exists a node map $\hat{ψ}$ between the nodes of $B$ and $\hat{B}$ . A low-level bundle $B$ is abstractable iff there is a high-level bundle $\hat{B}$ that abstracts $B$ .

Interference-freedom. When proving that a low-level bundle is abstractable we will need to ensure that application-layer messages constructed by the penetrator are constructed only from terms that he can obtain in the high-level model, otherwise the bundle cannot be abstracted. For example, suppose the penetrator takes a nonce sent by an honest agent in the key establishment phase of the transport-layer protocol and replays it within an application-layer message. Clearly, this case has to be disallowed since the node providing the nonce will not exist in the abstracted bundle.

To define interference-freedom we require an auxiliary definition. Informally, a negative low-level node n is abstractly constructible precisely when $msg (n)$ is constructed only from:
Terms in the penetrator’s initial knowledge, obtained from M strands;

Terms sent by honest agents on ⊥;

Terms sent by honest agents on non-⊥ channels that are unpacked by the penetrator.
Thus, if a negative node is abstractly constructible it follows that all the nodes that are required to construct the message will be in the abstracted bundle.

Note that in all subsequent definitions and lemmas we assume, without loss of generality, that bundles are normal to simplify the definitions and proofs. In the following, an initial penetrator path starts at an initial penetrator node (i.e. at a M strand), or starts at a regular node.

To define abstractly constructible, we need to define what it means for a penetrator path to contribute to the message of a node $n^{'}$ . In particular, a penetrator path that merely provides a key to decrypt a transport-layer message whose application-layer content is later used in constructing $msg (n^{'})$ should not be considered as contributing to $msg (n^{'})$ .
Definition 4.22.
A penetrator path p directly-contributes iff, for every node n on p that lies on the key edge of a D strand, there exists a destructive penetrator path $p_{d}$ ending at n such that:
$p_{d}$ does not traverse a key edge or contain a KG strand;

$p_{d} (1) \in N_{⊥}$ ; or $p_{d} (1) \in N_{trpt}$ and ${expath}^{c} (chan (p_{d} (1))) ⩽ expath (p_{d})$ .

Thus, the above definition identifies penetrator paths that only provide a key to decrypt a transport-layer message. Using the above, we can now define what it means for penetrator paths and nodes to be abstractly constructible.
Definition 4.23.
Let $B$ be a normal low-level bundle. An initial penetrator path p is abstractly constructible iff either:
p starts at a M strand; or

p starts at a regular node $n_{1} \in N_{⊥}$ ; or

p starts at a regular node $n_{1} \in N_{trpt}$ and there exists a destructive penetrator path $p_{d} ⩽ p$ such that $p_{d} app - extracts n_{1}$ .
A penetrator node $n_{2} \in B$ is abstractly constructible iff every initial penetrator path p that ends at $n_{2}$ and directly-contributes is abstractly constructible. A regular node $n_{2} \in B$ is abstractly constructible iff $n_{2} \in N_{⊥}$ .

We now define what it means for a bundle to be interference-free. The intention is that this property is true precisely when a low-level bundle can be safely abstracted, in the sense that high-level terms are not constructed from transport-layer terms.
Definition 4.24.
Let $B$ be a normal low-level bundle. A negative regular application-layer node $n_{2} \in N_{payload}$ is interference-free iff either:
$n_{2} \in N_{⊥}$ and there exists an abstractly constructible node $n_{1}$ such that $n_{1} \to n_{2}$ ; or

$n_{2} \in N_{trpt}$ and there exists a penetrator path p ending at $n_{2}$ such that either:

p is normal, p starts at a regular node $n_{1} \in N_{trpt}$ , $appmsg (n_{1}) = appmsg (n_{2})$ , $chan (n_{1}) = chan (n_{2})$ and p transports the application-layer message; or

p is constructive and starts at an abstractly constructible node $n_{1}$ such that $p app - packages n_{2}$ .
$B$ is interference-free iff every negative regular application-layer node is interference-free.

Thus, a negative regular node $n_{2}$ is interference-free providing the penetrator has constructed any messages that are sent to $n_{2}$ in a way that can be safely abstracted. In particular, this means that the penetrator must either:

Hijack, or simply alter the packaging of an existing message (Case (2a)); or

send a message that has been properly constructed (i.e. from an abstractly constructible node) via a Send or a Fake path (Case (2b)), or directly on the ⊥ channel (Case (1)).

The above definition prevents several kinds of attacks from appearing in interference-free bundles. In particular, it disallows penetrator paths where the penetrator transforms a transport-layer term from one channel into one for another channel, without fully decrypting the application-layer message (a multi-channel attack). It also prevents the penetrator from sending transport-layer terms as application-layer messages (a multi-layer attack – e.g. Fig. 8(a)). We have to prohibit both of these cases otherwise the bundle cannot be safely abstracted as there would be attacks that depend on the transport-layer implementation. See Fig. 8 for an example.

The above definition is a semantic condition, in that it quantifies over all bundles, making it hard to verify directly. We define a statically checkable condition on the protocol’s definition in Section 5 that implies interference-freedom.

Fig. 8.
Two bundles that illustrate abstractly constructible and interference-freedom. (a) $n_{13}$ is not interference-free as there is no penetrator path that satisfies condition (1) or (2) of Definition 4.24. In particular, the penetrator path that sends the application-layer message (i.e. $⟨ n_{3}, n_{5}, n_{7}, n_{10}, n_{11}, n_{13} ⟩$ ) starts at a non-abstractly constructible node $n_{3}$ . This is because it is taking a term, U, from a non-application-layer source (that will not be in the high-level bundle) and attempting to send it as an application-layer message. (b) This bundle is interference-free as $n_{3}$ is now abstractly constructible (as it lies on a M strand).

Abstract correctness. The channel properties, such as $AuthConf$ , require that certain high-level strands are not contained in the high-level strand space. Therefore, when abstracting low-level bundles we must take care to ensure that we only abstract bundles that do not contain any prohibited penetrator behaviours. For example, if bilateral TLS was being used, then the high-level strand space contains no high-level LN, FK or HJ strands on the bilateral TLS channel. Therefore, we can only abstract low-level bundles that contain no Learn, Fake or Hijack paths.

Unfortunately, this is too strong. Recall that a RV strand followed by a SD strand is actually equivalent to a HJ strand where the recipient of the first message and the sender of the second message are penetrator identities. Hence, since the penetrator is always allowed to send and receive messages, it follows that some Hijack paths will be present for even the most secure transport-layer protocols. As a result, the high-level bundles that we abstract to will contain some prohibited penetrator strands, but only if they are equivalent to combinations of permitted strands. This is addressed in Proposition 4.28, but we formalise the type of penetrator path that is problematic as follows.
Definition 4.25.
A Hijack path p is an innocuous penetrator path iff $recipient (p (1)) \in I^{pen}$ and $sender (p (| p |)) \in I^{pen}$ . An innocuous penetrator path p is expanded iff it is the concatenation of Receive and Send paths.

We now define a property of low-level bundles that is true iff the bundle contains only penetrator behaviours that are compatible with the channel’s security properties (i.e. $Conf$ and $Auth$ ). For example, a channel that satisfies $Conf$ should not permit any Learn paths, etc.
Definition 4.26.
A channel c is abstractly correct in a bundle $B$ iff:
If $c \in Conf$ then $B$ contains no Learn paths on c, or non-innocuous Hijack paths p on c such that $recipient (p (1)) \neq recipient (p (| p |))$ and $sender (p (1)) \in I^{reg}$ .

If $c \in Auth$ then $B$ contains no Fake paths on c, or non-innocuous Hijack paths on c.
A bundle $B$ is abstractly correct iff every channel $c \in ChannelTypes ∖ {⊥}$ is abstractly correct in $B$ . A strand space Σ is abstractly correct iff every bundle of Σ is abstractly correct.

Observe that this definition precisely specifies what it means for a channel to be correct in a low-level strand space, and thus specifies what proof obligations there are on the user.

Henceforth, we will only consider abstractly correct strand spaces.
Assumption 4.27.
Σ is abstractly correct.

We can now state that any interference-free low-level bundle is abstractable.
Proposition 4.28.
Let $B$ be a normal, abstractly correct, interference-free bundle such that every innocuous penetrator path is expanded. Then $B$ is abstractable by a high-level bundle $\hat{B}$ .
4.5. Summary

In this section we have proven the soundness of the high-level strand spaces model by proving that every bundle that satisfies our independence assumption, defined in Definition 4.24, and is abstractly correct, can be abstracted to a high-level bundle.

We defined a mapping $\hat{α}$ that converts low-level transport terms into the corresponding high-level terms. Using this a function $\hat{ϕ}$ was defined that relates the low-level regular nodes of a bundle to the corresponding high-level regular nodes. Further, $\hat{ϕ}$ abstracts away from the details of how the transport layer is implemented by not including, for instance, handshake nodes. We then defined two further maps, ${\hat{β}}_{1}$ and ${\hat{β}}_{2}$ , that relate the low-level penetrator nodes to high-level penetrator nodes. These three maps are all combined into a single map, $\hat{ψ}$ , that maps the nodes of a low-level bundle to the corresponding nodes of a high-level bundle. Using this we define what it means for a high-level bundle to abstract a low-level bundle.

To define our semantic condition we firstly defined what it means for a node to be abstractly constructible, which is true whenever a node’s message is built from only application-layer values. Intuitively, this means that the node can be safely abstracted. We then defined our main semantic property, interference-freedom, and proved that all interference-free bundles that are also abstractly correct (which requires that channels are being used correctly) are abstractable.

5. Disjoint encryption

In the previous section we proved that any interference-free bundle can be safely abstracted. Unfortunately, interference-freedom is not a statically checkable condition, based on the syntax of the transport and application-layer messages, but instead explicitly quantifies over all possible bundles. This makes testing for it automatically rather difficult, and also lessens our understanding of the assumption. In this section we instead address this problem by introducing a new statically checkable condition based on disjoint encryption [17]. We then prove that if a strand space satisfies our condition, then any bundle of the strand space can be transformed to an equivalent bundle that is interference-free.

Note that in addition to the statically checkable assumptions that we develop in this section, we will require Assumption 4.27 (which assumes the strand space is abstractly correct). This is not a statically checkable assumption, but can be verified using existing tools such as ProVerif [5] or Scyther [9] etc.

The main challenge we address is the presence of paths in the low-level bundle that transform a value that is part of the transport-layer packaging (e.g. a nonce) and send it as part of an application-layer message. We term such penetrator paths crossing-paths. These paths prevent us from abstracting bundles as the paths are not abstractly-constructible. However, under the new assumptions that we define, any crossing-paths that do exist are actually superfluous, in that an equivalent bundle exists that contains no crossing-path.

The outline of the proof is as follows. In Section 5.1 we define a few preliminaries including: several sets of encryptions (for the disjointness condition) and a type of penetrator path that are used by the penetrator to send application-layer messages. We also introduce a new, stronger, form of bundle equivalence that preserves the satisfaction of application-layer correctness properties. In Section 5.2 we define the statically checkable assumptions that the low-level strand space must satisfy. In Section 5.3 we consider crossing-paths, which are penetrator paths that, for example, transfer transport-layer nonces into the application layer. We prove that any bundle can be transformed to an equivalent bundle that contains no crossing-paths. We remove these crossing-paths by defining a new strand space that is related to the previous strand space, but in which the penetrator has been given a larger set of initial knowledge (this set will not contain any values of relevance to the application layer). In Section 5.4 we prove that any crossing-path-free bundle can be transformed into an equivalent one that is interference-free. This is used in Section 6 to prove that the high-level strand spaces model is sound, since any bundle that contains an attack is equivalent to an abstractable bundle that also contains the attack.

5.1. Preliminaries

Encryption sets. Firstly, we define various sets of terms and encryptions that will be used to define the disjointness conditions.

Definition 5.1.
The set of application-layer messages sent over the unprotected channel, ⊥ is defined by $T_{app}^{⊥} \hat{=} {msg (n) ∣ n \in N_{⊥}}$ . The following sets of terms are defined for each channel $c \in ChannelTypes ∖ {⊥}$ :
The set of application-layer terms is defined by: $T_{app}^{c} \hat{=} {extract (t, {expath}^{c} (c)) ∣ t \in T_{payload}^{c}}$ .

The (subterm closed) set of transport-layer non-message terms, $T_{non - msg}^{c}$ , that contains all non-application-layer terms that appear in transport terms, defined as: $\begin{array}{rcl} T_{non - msg}^{c} & \hat{=} & {extract (t, es) ∣ t \in T_{payload}^{c}, es \in E P, {expath}^{c} (c) ≰ es, es ≰ {expath}^{c} (c)} \\ \cup {s ∣ t \in T_{non - payload}^{c}, s ⊑ t} . \end{array}$ The first line extracts all subterms of a transport-layer message that do not contain the application-layer message (i.e. $es ≰ {expath}^{c} (c)$ ), or occur within the application-layer message (i.e. ${expath}^{c} (c) ≰ es$ ).

The set of application-layer ingredients, $T_{app}$ , defined by: $T_{app} \hat{=} X \cup {k, k^{- 1} ∣ k \in X \cap K}$ where $X \hat{=} {t^{'} ∣ t \in T_{app}^{c}, c \in ChannelTypes, t^{'} ingredient t}$ .

Recalling the running example used in Section 4.1, in the case of Fig. 5, $T_{app}^{c} = {{appmsg}_{2}}$ , $T_{non - msg}^{c} = {A, B, {| k |}_{PK (B)}, k}$ , $T_{app}^{⊥} = {{appmsg}_{1}}$ and $T_{app} = {{appmsg}_{1}, {appmsg}_{2}}$ , assuming ${appmsg}_{1}$ and ${appmsg}_{2}$ are atomic.
Definition 5.2.
The set of all encryptions, denoted by E, is defined as: ${{| m |}_{k} ∣ {| m |}_{k} \in T}$ . For each channel $c \in ChannelTypes$ , the set of application-layer encryptions of all encryptions that appear in an application-layer message is defined by: $E_{app}^{c} \hat{=} E \cap {e ∣ t \in T_{app}^{c}, e ⊑ t, e \in E}$ . The union of $E_{app}^{c}$ over $ChannelTypes$ is denoted by $E_{app}$ . For each channel $c \in ChannelTypes ∖ {⊥}$ :
The set of transport-layer message encryptions, of all encryptions that enclose an application-layer message is defined by $E_{trpt}^{c} \hat{=} {e ∣ t \in T_{payload}^{c}, e \in E, es \in E P, es ⩽ {expath}^{c} (c), e ⊑_{es} t}$ .

The set of transport-layer non-message encryptions for a channel c is defined by $E_{trpt - non - msg}^{c} \hat{=} T_{non - msg}^{c} \cap E$ .
The union of $E_{trpt}^{c}$ over $ChannelTypes ∖ {⊥}$ is denoted by $E_{trpt}$ (similarly $E_{trpt - non - msg}$ ).

Message sending. In the following sections we will need to identify which penetrator nodes are manipulating application-layer messages. We term such nodes application-layer penetrator nodes. In order to identify such nodes, we firstly identify all penetrator paths that manipulate terms that are eventually incorporated into application-layer messages. The following definition identifies when a constructive penetrator path constructs a message and then sends it over a transport channel. For ease we consider only normal bundles.
Definition 5.3.
Let $B$ be a normal low-level bundle. A penetrator path p that starts at a positive regular node $n_{1}$ and ends at a negative regular node $n_{2} \in N_{payload}$ is a penetrator message-construction path iff either:
$n_{2} \in N_{⊥}$ and p is directly contributing; or

$n_{2} \in N_{trpt}$ , $p = p_{n}^p_{s}$ such that $p_{n}$ is directly contributing and ${expath}^{c} (chan (n_{2})) = {expath}^{\sim} (p_{s})$ .

Bundle correctness properties. In Section 6 we will prove that the high-level strand spaces model is sound, by showing that whenever a low-level bundle does not satisfy a correctness property, a high-level bundle that also does not satisfy the property exists. We prove this by showing that we can transform the low-level bundle to a related bundle that is abstractable, but also does not satisfy the correctness property. Clearly, in order to prove the above we need the bundle transformation to preserve the incorrectness of the correctness property. Unfortunately, the standard definition of bundle equivalence is not strong enough to do this.

For example, consider specifying a node causally precedes, i.e. ≼, another node. Since bundle equivalence only requires the regular behaviour to be the same, this relation is not necessarily preserved by bundle equivalence. Further, the transformations we define will change the ≼ relation: they will remove some penetrator paths that cannot be safely abstracted. However, as we will only want to write ≼ as a conclusion of an implication in our correctness properties, it will therefore only occur positively. Thus, it suffices to ensure that the transformed ≼ relation relates fewer nodes. Thus, we introduce a relation on bundles ⊵ that holds when the bundles are equivalent and the resulting ≼ relation is a restriction of the original relation.
Definition 5.4.
A low-level bundle $B$ can be reduced to $B^{'}$ , denoted $B ⊵ B^{'}$ , iff $B$ and $B^{'}$ are equivalent and $≼_{B^{'}}$ relates no more regular nodes than $≼_{B}$ , i.e.: $(N_{B}^{reg} \times N_{B}^{reg}) \cap ≼_{B} \supseteq (N_{B^{'}}^{reg} \times N_{B^{'}}^{reg}) \cap ≼_{B^{'}} .$

Abstract correctness preserving transformations. Later in this section we will develop a number of bundle transformations. We then prove that the resulting bundles satisfy certain properties. However, in these proofs we will need to assume that the bundle is abstractly correct. Therefore, when transforming bundles we need to be careful not to go outside of the set of abstractly correct bundles. In order to ensure this, we define a class of transformations, known as abstract correctness preserving transformations, that preserve the abstract correctness of bundles.
Definition 5.5.
A bundle transformation f is abstract correctness preserving (henceforth ACP) iff whenever $B$ is abstractly correct, $f (B)$ is abstractly correct.

Observe that the composition of ACP bundle transformations is ACP.

In order to prove that the transformations we use in this section are ACP, we will need an additional assumption that the channel restrictions are sensible. For example, recall that a RV strand followed by a SD strand is equivalent to a HJ strand when the channel types and application-layer messages match. We require that if a channel prohibits certain HJ strands, then it also prohibits the equivalent RV, SD strand combination. This is merely a well-formedness condition on the channel and is satisfied by all existing definitions. Assumption 5.6.
A low-level strand space Σ contains only sensible channels iff: the strand space contains a Receive, Send subpath pair $⟨ - (A_{ψ}, P_{ϕ}, m, c), + (?, ?, m, ⊥) ⟩$ and $⟨ - (?, ?, m, ⊥), + (P_{ψ^{'}}^{'}, B_{ϕ^{'}}, m, c) ⟩$ iff it contains the equivalent Hijack path $⟨ - (A_{ψ}, P_{ϕ}, m, c), + (P_{ψ^{'}}^{'}, B_{ϕ^{'}}, i^{'}, m, c) ⟩$ .

5.2. Formulating the assumption

In this section we consider what statically checkable assumptions are necessary in order to prove our main result of this section, i.e. that every bundle can be made interference-free. In particular, we consider what behaviours we need to prohibit in order to safely abstract the bundles of a given strand space. We intersperse the definition of our assumptions with the reasons for their necessity.

Note that the aim of this section is to define assumptions that can reasonably be checked given a textual description of a protocol, such as the description given to a tool such as Casper, ProVerif or Scyther. We discuss how these assumptions can be checked at the end of the section.

The first condition requires that different transport protocols do not share any encryptions that enclose application-layer messages. This ensures that a message for one transport protocol cannot be partially deconstructed to produce a component of a message for another transport protocol. In particular, this ensures that any penetrator path starting at a regular transport-layer node on a channel $c_{1}$ and ending at a regular transport-layer node on a channel $c_{2}$ must traverse a node n such that the application-layer message is unencrypted on n. This is necessary as HJ strands do not allow the channel to be changed, meaning that there is no high-level strand that could represent the opposite of the above behaviour.

Definition 5.7.
Two transport-layer channels $c_{1}, c_{2} \in ChannelTypes ∖ {⊥}$ satisfy disjoint message encryption iff $E_{trpt}^{c_{1}} \cap E_{trpt}^{c_{2}} = \emptyset$ . A set of channels $C \subseteq ChannelTypes ∖ {⊥}$ satisfies disjoint message encryption iff each distinct pair of channels from C satisfies disjoint message encryption.

Using the above definition we can easily state our first assumption.

$ChannelTypes ∖ {⊥}$ satisfies disjoint message encryption.

The next few conditions impose further disjointness conditions on various types of encryptions. Recall that the set of all encryptions is given by $E_{app} \cup E_{trpt} \cup E_{trpt - non - msg}$ (cf. Definition 5.1); the next few conditions concern the overlaps that are allowed between these sets. In particular, our second condition ensures that the penetrator cannot send transport-layer messages as application-layer messages. The third condition ensures that the penetrator cannot send encryptions that contain application-layer payloads in the transport-layer packaging or as part of the handshake. Clearly if a bundle were to exist that exhibited either of these behaviours, then it would not be possible to make the bundle interference-free as there is no high-level strand to represent such behaviour.

No application-layer encryption is also a transport-layer encryption, i.e. $E_{app} \cap E_{trpt} = \emptyset$ .

No non-message transport encryption is also a transport-layer encryption, i.e. $E_{trpt} \cap E_{trpt - non - msg} = \emptyset$ .

Note that we do not require that $E_{app} \cap E_{trpt - non - msg} = \emptyset$ as there may be values, such as public-key certificates, that can be shared safely between the layers. Instead we require that, for each encryption in $E_{app} \cap E_{trpt - non - msg}$ , the inverse key must be public.

If a term ${| m |}_{k}$ is an application-layer encryption and a non-message transport encryption then $k^{- 1}$ must be public, i.e. $\forall {| m |}_{k} \in E_{app} \cap E_{trpt - non - msg} \cdot k^{- 1} \in T_{P}$ .

To see why a condition like this is necessary consider the bundle in Fig. 9, where ${| t |}_{k} \in E_{app} \cap E_{trpt - non - msg}$ . In this figure, nodes within dotted boxes are application-layer nodes whilst nodes within dashed boxes are handshake nodes (i.e. transport non-message nodes). Observe that the bundle is not interference-free as $n_{5}$ is not abstractly-constructible (as the penetrator obtains t from a handshake node). However, under the above assumption we can easily transform the bundle to add a path between $n_{1}$ and $n_{5}$ via a D strand, with the key coming from a M strand (as $k^{- 1} \in T_{P}$ ). This condition will be required in the following section when crossing-paths are considered.

Fig. 9.
A bundle that does not satisfy Assumption 5.10 (4).

The fifth condition ensures that the penetrator cannot possess any transport-layer encryptions in his initial knowledge. This is required as it prevents the penetrator from creating transport-layer messages for which he does not know the application-layer message: clearly there is no high-level strand that permits this.
Definition 5.8.
The set of terms initially deducible by the penetrator, denoted $T_{P}^{I}$ , is defined as ${t^{'} ∣ t \in T_{P} \land t^{'} ⊑ t}$ .

No transport-layer encryptions are initially deducible by the penetrator, i.e. $T_{P}^{I} \cap E_{trpt} = \emptyset$ .

The sixth condition ensures that the penetrator cannot possess non-public application-layer terms surrounded by non-application-layer encryptions. If the penetrator initially knew a non-public term that contained an application-layer term surrounded by some transport-layer encryptions, then there could exist a penetrator path on which he extracts the application-layer term by decrypting using transport-layer keys. However, such a path would not be valid in the high-level bundle and thus we cannot safely abstract the bundle.

Non-public application-layer terms must only appear in the penetrator’s initial knowledge surrounded by application-layer encryptions, i.e. if $t \in T_{app} ∖ T_{P}$ , then for all $s \in T_{P}$ , if $es$ is an extraction path such that $t ⊑_{es} s$ then for each ${es}^{'} < es$ such that ${| m |}_{k} ⊑_{{es}^{'}} s$ , ${| m |}_{k} \in E_{app}$ .

The seventh condition disallows bundles in which an application-layer secret (e.g. a key) originates at both the application layer and the transport layer. Such occurrences are likely to be coincidences (and are certainly indicative of poor design) and may result in the bundle being unable to be abstracted. For instance, suppose a node n originates a value t at both the application layer and the transport layer. Further, assume that the application-layer value is unavailable to the penetrator (as it is sent over a confidential channel, or similar) but that the transport-layer value can be obtained by the penetrator. Therefore, the low-level bundle may contain a penetrator path from n to another application-layer node along which the penetrator uses t. However, such a path is not abstractable since it requires a particular configuration of the transport-layer protocol.

Atomic or encrypted application-layer values originate only at the application layer. That is, if a non-public application-layer term $t \in T_{app} ∖ T_{P}$ originates at a regular node n and t is an atom or encryption, then either $n \in N_{⊥}$ , or $n \in N_{trpt}$ and, for every extraction path $es$ such that $t ⊑_{es} msg (n)$ , ${expath}^{c} (c) ⩽ es$ (i.e. t originates only at the application layer at n).

The eighth condition disallows bundles in which a transport-layer encryption is also an application-layer ingredient (cf. Definition 2.1). Clearly any such bundle is not abstractable, since the transport-layer encryptions are not available in the abstracted bundle, and thus the key cannot be generated.
No transport-layer encryption can be an application-layer ingredient; i.e. $T_{app} \cap E_{trpt} = \emptyset$ .
Note that the above condition actually subsumes the first part of Assumption 5.10 (2); we keep these as separate conditions for clarity.

Lastly, we require that the strand space is abstractly correct. This is required as without this condition we are unable to abstract any bundles as there would be transport-layer behaviours that have no accompanying representation in the high-level bundles. In particular, recall that Proposition 4.28 required a bundle to be abstractly correct in order for it to be abstractable.
Definition 5.9.
A strand space Σ satisfies layered-disjoint encryption iff it satisfies conditions (1)–(8) above.
Assumption 5.10.
Σ satisfies layer-disjoint encryption.

Unfortunately, TLS [11] does not satisfy the above condition. This is discussed further in Section 7.

We now briefly outline how these properties can be checked using static analysis on an appropriate protocol description. Assumption 5.10 (1)–(4) and (8) all require various sets of encryptions to be disjoint. In most cases, the corresponding plaintexts are disjoint: this can be verified by inspection of the specifications of the formats of the plaintexts (e.g. XML formats). In other cases, it is necessary to prove that keys are disjoint: this follows immediately when the protocols generates the keys freshly; for long-term keys, it may be necessary to assume that such keys are not shared between protocols.

Assumption 5.10 (7) could be easily verified given a symbolic definition of the regular agents that included details of where terms originate (i.e. which terms are fresh). Assumption 5.10 (5) and Assumption 5.10 (6) are assumptions on the penetrator’s initial knowledge and thus could be verified by considering a symbolic definition of $T_{P}$ .
5.3. Crossing-paths

As discussed in the introduction to Section 5, there is nothing to prevent the penetrator from taking terms from the transport layer and moving them into the application layer. We term such penetrator paths crossing-paths and the corresponding terms crossing terms. Clearly, we cannot safely abstract such bundles as the transport-layer sections of such penetrator paths will not appear in the high-level bundle and therefore there is nowhere to obtain the crossing term.

Note that penetrator paths from the application layer to the transport layer (which could also be considered as crossing paths) are not prohibited. This is because such crossovers do not affect our ability to abstract the bundle as they affect transport-layer, rather than application-layer, behaviour. Further, as we assume that the bundle is abstractly correct, we are already assuming that the application-layer protocol does nothing to break the transport-layer protocol.

In this section we prove that we are able to remove crossing-paths from a bundle $B$ and produce a bundle $B^{'}$ , of a related strand space, such that $B ⊵ B^{'}$ (cf. Definition 5.4). We begin by formally defining what a crossing-path is.

Definition 5.11.
Let $B$ be a normal low-level bundle and p be a penetrator message-construction path that starts at a positive regular node $n_{1}$ and finishes at a negative regular node $n_{2} \in N_{payload}$ . Let $p_{d}$ be the longest destructive prefix of p that does not traverse a key-edge. p is a crossing-path iff either:
$n_{1} \in N_{trpt}$ and, letting $c = chan (n_{1})$ , $expath (p_{d}) ≰ {expath}^{c} (c)$ , and ${expath}^{c} (c) ≰ expath (p_{d})$ ; or

$n_{1} \in N_{non - payload}$ .
A bundle $B$ is crossing-path-free iff it contains no crossing paths. The crossing point is defined as the last node on $p_{d}$ and the crossing term is defined as $msg (n)$ where n is the crossing point.

The first clause in the above captures the case where the penetrator takes a term that originated within a transport-layer message, but not from within the application-layer content or enclosing the application-layer content, and then uses it in constructing the application-layer content of another message. The second clause captures the case where the penetrator takes a term obtained from a handshake node and uses it to construct the application-layer content of another message. Both of these take terms from a non-application-layer source and move it into the application layer, and are therefore crossing-paths.

In order to abstract our bundles we need to remove any crossing-paths, as such paths will not be abstractly-constructible. Our basic approach is to replace the crossing edge with a M strand that simply originates the required term; the resulting bundle would clearly have no crossing-paths and therefore could be safely abstracted. A difficulty with this approach is that the unique origination assumptions that held on the original low-level bundle would no longer hold in the transformed bundle. This means that if a low-level bundle does not satisfy a given property, then the high-level bundle may satisfy it (as the high-level bundle may not satisfy the unique origination assumptions and thus the property holds vacuously). Therefore, we remove crossing-paths, taking care not to break any unique origination assumptions.

Enlarging the strand space. When removing crossing-paths from a bundle we may need to add extra values to the penetrator’s initial knowledge. For instance, consider a bundle containing a crossing-path where the penetrator takes a handshake nonce and then uses it in an application-layer message. This bundle will be transformed to an equivalent bundle in which the crossing-path has been replaced by a M strand. From the application-layer’s point of view, this behaviour is indistinguishable from the original behaviour.

We now consider how to enlarge the set of public terms in such a way as to allow transformations like those discussed above. We do this by defining a new strand space, based on the existing strand space, that differs only in the penetrator’s initial knowledge (cf. Definition 2.9). Further, we restrict the penetrator’s behaviour so that the transport-layer behaviour is identical (but the application-layer behaviour is enlarged, as discussed above). Clearly, such a transformation has the potential to introduce false attacks against the application-layer protocol by giving the penetrator encryption keys that he could not otherwise obtain. However, we avoid doing this by only adding values that are not in $T_{app}$ (Definition 5.1) which contains all terms of interest to the application layer.

In order to define this transformation we firstly define a set that contains all terms that may appear at crossing points and may need transforming as above.
Definition 5.12.
The set of transport extractable components, denoted $T_{X}$ is defined as the set of all terms that are not in $T_{app}$ , but are in the following set: $\begin{array}{rcl} {extract (t, es) ∣ t \in T_{payload}, es \in E P, {expath}^{c} (chan (t)) ≰ es, es ≰ {expath}^{c} (chan (t))} \\ \cup {s ∣ t \in T_{non - payload}, s ⊑ t} . \end{array}$

Recall that $T_{payload}$ gives the set of terms that carry an application-layer payload. Thus, the first clause in the above extracts all the transport-layer packaging of a payload-carrying message, whilst the second clause gives all the terms that the penetrator could extract from other transport-layer messages.

Using the above it is now possible to define the enlarged strand space.
Definition 5.13.
Let Σ be an abstractly correct low-level strand space. The enlarged strand space of Σ, denoted $Σ_{E}$ is defined to be as Σ but with the set of public terms enlarged to be: $T_{P}^{Σ_{E}} = T_{P}^{Σ} \cup T_{X}$ .

This has some repercussions on application-layer proofs. In general, in order to prove the required application-layer result we will need an assumption on the terms in $T_{P}$ . Since we add terms to $T_{P}$ , the application-layer correctness proof is only allowed to assume that certain terms are not in $T_{P}$ , rather than specifying exactly what is allowed. Further, the assumption may only consider terms in $T_{app}$ , as terms that are not in $T_{app}$ may be added to the penetrator’s initial knowledge by the transformation. Thus, proofs may not assume that $x \notin T_{P}$ for any $x \in T_{X}$ . In practice this is not a restriction, since terms that are not in $T_{app}$ cannot possibly affect the security of the application layer.

For the remainder of this section we make exclusive use of the enlarged strand space, $Σ_{E}$ , rather than Σ.

Crossing path removal. Using the above, we can prove that crossing-paths can be removed. Proposition 5.14.
Let $B$ be a normal low-level bundle. Then there exists a bundle $B^{'}$ in $Σ_{E}$ that contains no crossing-paths such that $B ⊵ B^{'}$ and the transformation is ACP.

5.4. Interference freedom

In this section we state that we can transform any bundle of Σ into an equivalent interference-free bundle of $Σ_{E}$ .

Lemma 5.15.
Let $B$ be a normal crossing-path-free bundle with a negative regular node $n_{2} \in N_{payload}$ that is not interference-free. Then there exists, by an ACP transformation, a normal, crossing-path-free, bundle $B^{'}$ such that $n_{2}$ is interference-free and $B ⊵ B^{'}$ .

Recall that Proposition 4.28 required that each innocuous penetrator path in $B$ is expanded. Thus, before we can apply the proposition, we need to ensure that all innocuous paths are expanded. Clearly, such a transformation should be possible, since an innocuous penetrator path is equivalent to a Receive path followed by a Send path. However, in general, this transformation would be very hard to specify, since arbitrary encryption keys could be required in order to achieve the necessary decryption or encryptions. Therefore, we instead make an assumption on the underlying transport-layer protocol that each innocuous penetrator path can be expanded. Whilst this does impose a proof obligation on the transport layer, it is essentially requiring that the transport layer allows the penetrator to send and receive messages from his own channel ends. Clearly, every sensible channel will satisfy this.
Assumption 5.16.
Let $B$ be a normal bundle and p be an innocuous non-expanded penetrator path between n and $n^{'}$ . There exists a bundle $B^{'}$ , obtainable via an ACP transformation, in which p is expanded and such that $B ⊵ B^{'}$ .

Using the above we are now able to prove our main proposition of this section as follows.
Proposition 5.17.
Let $B$ be a bundle of an strand space Σ that satisfies layer-disjoint encryption. Then there exists a normal, abstractable bundle $B^{'}$ of the enlarged strand space $Σ_{E}$ such that $B ⊵ B^{'}$ .

The proof of Proposition 5.17 uses Proposition 5.14 to remove the crossing paths in the original bundle. Lemma 5.15 can then be applied multiple times to remove each of the non-interference-free nodes in the resulting bundle.
5.5. Summary

In this section we have proven that whenever there exists a low-level bundle in a strand space satisfying Definition 5.9, then there exists a related (cf. Definition 5.4) bundle that can be abstracted. This assumption can be checked statically and also allows us to understand more about the problem, e.g. where care should be taken to avoid key sharing.

Firstly, we defined the bundle relation ⊵, which formalises how a bundle is related to its abstractable version, before defining Assumption 5.10. In Section 5.3 we proved that any path on which the penetrator takes a values from the transport layer into the application layer is incidental. In Section 5.4 we then showed that Assumption 5.10 implies that all bundles can be transformed to a related bundle that is interference-free.

Given Definition 5.13, when proving the correctness of the application-layer protocol, $T_{P}$ in the high-level strand space must include at least $T_{P}^{Σ_{E}}$ . In practice, this is not an issue since $T_{P}^{Σ_{E}} = T_{P}^{Σ} \cup T_{X}$ and $T_{X} \cap T_{app} = \emptyset$ . However, from a practical point of view, it means that the assumptions should specify what $T_{P}$ cannot contain, rather than what $T_{P}$ can contain.

6. Abstracting correctness properties

In the previous sections we have proven that any low-level bundle can be transformed to an abstractable bundle. Further, the transformed bundle has the same application-layer behaviour as the original bundle. In this section we prove that whenever there is an attack against the low-level model, there must be an attack against the high-level model. This shows that the high-level strand spaces model is sound, in that if a proof of protocol correctness can be constructed in the high-level model, then there are no attacks against the low-level model.

In Section 6.1 we formalise a logic in which protocol-correctness properties can be expressed. In Section 6.2 and Section 6.3, we define two semantics for the logic, one for low-level bundles and another for high-level bundles. In Section 6.4, we consider how the values of the terms of the logic are related when interpreted in both a low-level bundle and a high-level bundle that abstracts it. We then prove that, for a large subclass of correctness properties, whenever an abstractable low-level bundle does not satisfy a correctness property, its high-level abstraction also does not. In Section 6.5, we show that the transformations applied in Section 5 preserve the correctness of bundle formulas. Then, we use Proposition 5.17 to prove that whenever a low-level bundle does not satisfy a correctness property, the bundle can be transformed to an abstractable bundle such that its abstraction does not satisfy the correctness property.

6.1. A logic of correctness properties

In this section we define a logic in which we can express correctness properties. We do not intend the logic to be a practical usable logic. Instead, the logic is merely a tool that we can use to show that results about protocols in the high-level model also apply to low-level models. In a sense, the logic is an assembly language for logics, rather than being inherently useful itself.

In order to define standard correctness properties, the logic needs to be able to specify properties such as:

A regular node precedes another node;

A term (e.g. a password) is confidential or uniquely originating;

A channel is confidential or authentic;

Certain message components are equal;

A node lies on a particular type of strand (e.g. on an $AS 1$ strand).

The logic that we will define allows all of the above to be expressed.

Note that the logic cannot express that a node must send a message directly to another node. The reason why we cannot express the latter is that it is, in general, rather complex. Defining what it means in a normal high-level bundle is not difficult; either the nodes must be connected using →, or there must be a TX strand between them. However, we also need to define an equivalent semantics for both normal and non-normal low-level bundles, which is far more complex. Whilst this may appear to be a restriction of the logic, in reality this property is not required; what really matters is the application-layer behaviour of the regular agents and, to a lesser extent, the ordering (i.e. ≼) of nodes.

In order to define the last of the above properties, namely that a node lies on a strand of a particular type, we assume the existence of a set of roles

R

. The definition of

R

will depend on the protocol in question, and we will later assume that there are suitable sets of low-level and high-level strands for each role. Further, in Assumption 6.8 we will assume that these sets of strands are defined in a related way: namely that the strands for a role in a low-level bundle abstract to strands for a role in a high-level bundle.

Table 1
An informal explanation of the meaning of the terms of our correctness property logic

Logical term	Informal meaning
v	$v \in V$ , a variable
c	c is a constant (including terms, sets of terms, etc.)
${\| t_{1} \|}_{t_{2}}$	encryption of a logical term
$t_{1}^t_{2}$	concatenation of two logical terms
$f (t_{1}, \dots, t_{n})$	the application of a n-ary function f to $t_{1}, \dots, t_{n}$
$t_{t^{'}}$	a channel endpoint with name t and channel end $t^{'}$
$σ (t_{1}, t_{2}, t_{3}, t_{4})$	$σ \in {+, -}$ , a high-level term
$height (t)$	bundle height of a strand
$msg (t)$	high-level message of a node
$sign (t)$	sign of a high-level term
$sender (t)$	sending endpoint of a high-level term
$recipient (t)$	receiving endpoint of a high-level term
$appmsg (t)$	application message of a high-level term
$channel (t)$	channel of a high-level term
$t_{1} σ t_{2}$	$σ \in {+, -, \dots}$ , standard mathematical functions
$name (t)$	name contained in an endpoint
$end (t)$	channel end contained in an endpoint
${role}_{k}$	the set of strands for the regular agent in role $k \in R$
$node (t, n)$	nth node on a strand t
$strand (t)$	strand of a node

As a simple example of how the logic can be utilised, recall the example protocol presented in Section 3.3. This protocol allows a user U to login to an application server

AS

using a login server

LS

. Consider the following property: “if an honest login server issues an authentication token for an honest user, then the user must have previously presented their username and password”. This can be expressed in our logic as follows; see Tables 1 and 2 for an informal description of the logic:

\begin{array}{rcl} \forall ls \in A_{names}^{reg} \cdot \forall u \in A_{names}^{reg} \cdot \forall as \in A_{names} \cdot \forall ψ \in E \cdot \forall ϕ \in E \cdot \forall {st}_{ls} \in {role}_{LS} \\ \cdot height ({st}_{ls}) = 2 \land msg (node ({st}_{ls}, 2)) = + ({ls}_{ϕ}, ?_{ψ}, {| {| u |}_{PK (as)} |}_{SK (ls)}, {TLS}^{S \to C}) \\ ⟹ \exists {st}_{u} \in {role}_{U} \cdot node ({st}_{u}, 1) ≼ node ({st}_{ls}, 1) \\ \land msg (node ({st}_{u}, 1)) = + (?_{ψ}, {ls}_{ϕ}, as^u^{Password}_{ls} (u), {TLS}^{C \to S}) . \end{array}

Note that the above uses several functions on terms including

PK

SK

and

Password

, and utilises several sets of constants including

A_{names}^{reg}

and

E

. The example also assumes the existence of two roles:

LS

and U standing for the login server and user, respectively.

Table 2

An informal explanation of the bundle formulas

Predicate	Informal meaning
$t_{1} ≼ t_{2}$	$t_{1}$ causally precedes $t_{2}$
$AuthChan (t)$	t is an authenticated channel
$ConfChan (t)$	t is a confidential channel
$Confidential (t)$	t is a confidential term
$UniquelyOriginates (t_{1}, t_{2})$	$t_{1}$ uniquely originates at the node $t_{2}$
$t_{1} σ t_{2}$	$σ \in {⊑, =, <}$ , comparison of $t_{1}$ and $t_{2}$
$\forall v \in t \cdot ϕ$	universal quantification
$\exists v \in t \cdot ϕ$	existential quantification
$\neg ϕ_{1}$	logical negation
$ϕ_{1} \land ϕ_{2}$	logical and
$ϕ_{1} \lor ϕ_{2}$	logical or

We start by defining the terms in our logic, which we call logical terms. The informal meaning behind the terms of the logic is given in Table 1.

Definition 6.1.

We assume the existence of a set of variables V and a set of constants C. The set of logical terms, denoted $LogicalTerm$ , is defined by the following grammar, where c denotes a constant and v denotes a variable: $\begin{array}{rcl} Term ::= Term^Term ∣ {| Term |}_{Term} ∣ appmsg (\hat{Term}) ∣ name (Endpoint) \\ ∣ f (Term, \dots, Term) where f is a n -ary function on terms ∣ c \in T ∣ v, \\ Natural ::= height (Strand) ∣ Natural σ Natural, σ \in {+, -, \dots} ∣ c \in N ∣ v, \\ ChannelEnd ::= end (Endpoint) ∣ c \in E, \\ Endpoint ::= {Term}_{ChannelEnd} ∣ sender (\hat{Term}) ∣ recipient (\hat{Term}) ∣ c \in I, \\ \hat{Term} ::= msg (Node) ∣ Sign (Endpoint, Endpoint, Term, Channel), \\ Channel ::= channel (\hat{Term}) ∣ c \in ChannelTypes, \\ Node ::= node (Strand, Natural), \\ Strand ::= strand (Node) ∣ v, \\ Sign ::= sign (\hat{Term}) ∣ + ∣ -, \\ TermSet ::= c \in P (T) ∣ v, \\ StrandSet ::= {role}_{k}, k \in R ∣ v, \\ EndpointSet ::= c \in I, \\ Set ::= TermSet ∣ StrandSet ∣ EndpointSet ∣ N, \\ LogicalTerm ::= Term ∣ Natural ∣ ChannelEnd ∣ Endpoint ∣ \hat{Term} ∣ Channel ∣ Node \\ ∣ Strand ∣ Sign . \end{array}$

Note that the structure of the terms is typed, meaning that the logic we define is actually a many-sorted logic. Further, the logic requires infinite sets as constants, most notably as sets of terms. For example, to specify that something is in the set of public terms, the set of public terms has to be explicitly encoded as an infinite constant set.

Using the definition of logical terms we are now able to define what a bundle formula is. The informal meaning of the formulas is given in Table 2.

Definition 6.2.

The set of high-level bundle formulas is given by the following grammar: $\begin{array}{rcl} Formula & ::= & Node ≼ Node ∣ AuthChan (Channel) ∣ ConfChan (Channel) \\ ∣ Confidential (Term) ∣ UniquelyOriginates (Term, Node) \\ ∣ Term ⊑ Term ∣ LogicalTerm = LogicalTerm \\ ∣ Natural < Natural ∣ Formula \land Formula ∣ Formula \lor Formula ∣ \neg Formula \\ ∣ \forall v \in Set \cdot Formula ∣ \exists v \in Set \cdot Formula . \end{array}$ A free variable in a high-level bundle formula is a variable v that is not enclosed by a quantification of the form $\forall v \in S$ or $\exists v \in S$ . A high-level bundle formula ϕ is closed iff it contains no free variables.

We include a number of cases that could be removed by using logical equivalences (e.g. $ϕ_{1} \land ϕ_{2} = \neg (\neg ϕ_{1} \lor \neg ϕ_{2})$ ), in order to obtain formulas in negation normal form, where negations only occur next to atomic formulas; this is used in several of the proofs.

6.2. High-level semantics

We now consider how to define the semantics of the logic when applied to low and high-level bundles. We start by considering the case of the high-level semantics. In order to define this we assume the existence of a set of regular high-level strands, ${\hat{Role}}_{k}$ , for each role $k \in R$ . For example, in the case of WebAuth, we assume the existence of a set of all possible $AS 1$ strands.

Definition 6.3.
The set of high-level logical term values in a high-level strand space $\hat{Σ}$ is given by: $T \cup N \cup E \cup I \cup \hat{T} \cup ChannelTypes \cup \hat{N} \cup \hat{Σ} \cup {+, -} \cup P (T) \cup P (\hat{Σ})$ . Let $\hat{B}$ be a high-level bundle, t be a logical term and $\hat{Γ}$ be a high-level term map, from variables to high-level logical term values, defined on all free-variables in t such that t is well typed. Then, the high-level logical term value of t in $\hat{B}$ , denoted ${⟦ t ⟧}_{\hat{B}}^{\hat{Γ}}$ , is defined inductively as follows:
${⟦ v ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} \hat{Γ} (v)$ ;

${⟦ c ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} c$ ;

${⟦ {| t_{1} |}_{t_{2}} ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} {| {⟦ t_{1} ⟧}_{\hat{B}}^{\hat{Γ}} |}_{{⟦ t_{2} ⟧}_{\hat{B}}^{\hat{Γ}}}$ ;

${⟦ t_{1}^t_{2} ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} {⟦ t_{1} ⟧}_{\hat{B}}^{\hat{Γ}}^{⟦ t_{2} ⟧}_{\hat{B}}^{\hat{Γ}}$ ;

${⟦ t_{t^{'}} ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} ({⟦ t ⟧}_{\hat{B}}^{\hat{Γ}}, {⟦ t^{'} ⟧}_{\hat{B}}^{\hat{Γ}})$ ;

${⟦ f (t_{1}, \dots, t_{n}) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} f ({⟦ t_{1} ⟧}_{\hat{B}}^{\hat{Γ}}, \dots, {⟦ t_{n} ⟧}_{\hat{B}}^{\hat{Γ}})$ ;

${⟦ height (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} {height}_{\hat{B}} ({⟦ t ⟧}_{\hat{B}}^{\hat{Γ}})$ , where ${height}_{\hat{B}} (st)$ denotes the $\hat{B}$ -height of the strand $st$ ;

${⟦ msg (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} msg ({⟦ t ⟧}_{\hat{B}}^{\hat{Γ}})$ ;

If ${⟦ t ⟧}_{\hat{B}}^{\hat{Γ}} = σ (A_{ϕ}, B_{ψ}, m, c)$ then: ${⟦ sign (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} σ$ , ${⟦ sender (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} A_{ϕ}$ , ${⟦ recipient (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} B_{ψ}$ , ${⟦ appmsg (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} m$ and ${⟦ channel (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} c$ ;

${⟦ t_{1} σ t_{2} ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} {⟦ t_{1} ⟧}_{\hat{B}}^{\hat{Γ}} σ {⟦ t_{2} ⟧}_{\hat{B}}^{\hat{Γ}}$ , where $σ \in {+, -, \dots}$ ;

${⟦ name (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} A$ where ${⟦ t ⟧}_{\hat{B}}^{\hat{Γ}} = A_{ϕ}$ ;

${⟦ end (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} ϕ$ where ${⟦ t ⟧}_{\hat{B}}^{\hat{Γ}} = A_{ϕ}$ ;

${⟦ {role}_{k} ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} {\hat{Role}}_{k} \cap {strand (\hat{n}) ∣ \hat{n} \in N_{\hat{B}}^{reg}}$ ;

${⟦ node (t, n) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} ({⟦ t ⟧}_{\hat{B}}^{\hat{Γ}}, {⟦ n ⟧}_{\hat{B}}^{\hat{Γ}})$ , providing ${⟦ n ⟧}_{\hat{B}}^{\hat{Γ}} ⩽ {height}_{\hat{B}} ({⟦ t ⟧}_{\hat{B}}^{\hat{Γ}})$ ;

${⟦ strand (t) ⟧}_{\hat{B}}^{\hat{Γ}} \hat{=} strand ({⟦ t ⟧}_{\hat{B}}^{\hat{Γ}})$ .
Let $\hat{B}$ be a high-level bundle, ϕ be a high-level bundle formula, and $\hat{Γ}$ be a high-level term map defined on all free-variables of ϕ. Then, $\hat{B}$ and $\hat{Γ}$ satisfy ϕ, denoted $(\hat{B}, \hat{Γ}) \hat{⊨} ϕ$ , according to the following inductive definition:
$(\hat{B}, \hat{Γ}) \hat{⊨} t_{1} ≼ t_{2}$ iff ${⟦ t_{1} ⟧}_{\hat{B}}^{\hat{Γ}} ≼_{\hat{B}} {⟦ t_{2} ⟧}_{\hat{B}}^{\hat{Γ}}$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} AuthChan (t)$ iff ${⟦ t ⟧}_{\hat{B}}^{\hat{Γ}} \in Auth$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} ConfChan (t)$ iff ${⟦ t ⟧}_{\hat{B}}^{\hat{Γ}} \in Conf$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} Confidential (t)$ iff ${⟦ t ⟧}_{\hat{B}}^{\hat{Γ}}$ is confidential (Definition 3.14) in $\hat{B}$ and ${⟦ t ⟧}_{\hat{B}}^{\hat{Γ}} \in T_{app}$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} UniquelyOriginates (t_{1}, t_{2})$ iff ${⟦ t_{1} ⟧}_{\hat{B}}^{\hat{Γ}} \in A ∖ T_{P}^{I}$ and uniquely originates on ${⟦ t_{2} ⟧}_{\hat{B}}^{\hat{Γ}}$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} t_{1} σ t_{2}$ , $σ \in {⊑, =, <}$ iff ${⟦ t_{1} ⟧}_{\hat{B}}^{\hat{Γ}} σ {⟦ t_{2} ⟧}_{\hat{B}}^{\hat{Γ}}$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} \forall v \in S \cdot ϕ$ iff for all $t \in {⟦ S ⟧}_{\hat{B}}^{\hat{Γ}}$ , $(\hat{B}, \hat{Γ} [v \mapsto t]) \hat{⊨} ϕ$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} \exists v \in S \cdot ϕ$ iff there exists $t \in {⟦ S ⟧}_{\hat{B}}^{\hat{Γ}}$ , $(\hat{B}, \hat{Γ} [v \mapsto t]) \hat{⊨} ϕ$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} \neg ϕ_{1}$ iff $(\hat{B}, \hat{Γ}) \hat{⊭} ϕ_{1}$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} ϕ_{1} \land ϕ_{2}$ iff $(\hat{B}, \hat{Γ}) \hat{⊨} ϕ_{1}$ and $(\hat{B}, \hat{Γ}) \hat{⊨} ϕ_{2}$ ;

$(\hat{B}, \hat{Γ}) \hat{⊨} ϕ_{1} \lor ϕ_{2}$ iff $(\hat{B}, \hat{Γ}) \hat{⊨} ϕ_{1}$ or $(\hat{B}, \hat{Γ}) \hat{⊨} ϕ_{2}$ .

In the semantics of $Confidential (t)$ we require t to be in $T_{app}$ to ensure that the formula does not claim that a transport-layer value is confidential. If the formula were to require that a transport-layer value was confidential then clearly this could be true in the high-level bundle, as it may have been abstracted away, but may not be true in the low-level bundle.

Note $UniquelyOriginates (t_{1}, t_{2})$ is restricted to atoms that the penetrator cannot obtain from a term he initially knows. This simplifies the low-level semantics (which has to correspond to the high-level semantics). However, as we are only interested in writing correctness properties that require values that regular agents created to uniquely originate, this is not an issue.
6.3. Low-level semantics

We now develop a semantics for high-level bundle formulas when applied to low-level bundles. As we aim to prove that the correctness of bundle formulas can be abstracted, we define the semantics of the logic in a way that is both intuitive and compatible with the high-level semantics.

To define a low-level semantics that corresponds to the high-level semantics we need to consider how to interpret $UniquelyOriginates (t_{1}, t_{2})$ . We cannot map it directly to the standard notion of unique origination, as this would also consider values that originate as part of the transport-layer packaging. Hence, we define what it means to originate in the application layer.

Definition 6.4.
Let $B$ be a low-level bundle. An atom $t \notin T_{P}^{I}$ originates in the application layer at a regular node $n \in N_{B}$ iff $t ⊑ appmsg (n)$ and, for all $n^{'}$ such that $n^{'} \Rightarrow^{+} n$ , $t ⋢ appmsg (n^{'})$ . An atom $t \notin T_{P}^{I}$ uniquely originates in the application layer at a regular node $n \in N_{B}$ iff t originates in the application layer on a unique n.

We now consider how to define the semantics of high-level bundle formulas when applied to low-level bundles. We need to assume a few things about how the strand spaces are defined. Firstly, we assume that for each role $k \in R$ there is a set of regular strands ${Role}_{k}$ . Clearly, we will need this set to be related to ${\hat{Role}}_{k}$ and we formalise this, in Assumption 6.8. We also define several partial functions:

$app_node (st, n)$ gives the index of the nth application-layer node on $st$ : $app_node (st, n) \hat{=} i$ where $(st, i) \in N_{payload} \land app_{node}^{- 1} (st, i) = n$ .

$app_{node}^{- 1} (st, n)$ gives the application-layer index of the nth node if one exists: $app_{node}^{- 1} (st, n) \hat{=} # {i ∣ 1 ⩽ i ⩽ n \land (st, i) \in N_{payload}}$ if $(st, n) \in N_{payload}$ .

$app_{height}_{B} (st)$ gives the application-layer height of the transport-layer strand $st$ from $B$ : $app_{height}_{B} (st) \hat{=} # {i ∣ (st, i) \in N_{B} \cap N_{payload}}$ .

We also need to define what it means for a term t to be confidential in a low-level bundle, analogously to Definition 3.14. Definition 6.5.
A term t is confidential in a low-level bundle $B$ iff no equivalent bundle contains a positive node n such that $msg (n) = + t$ .
Definition 6.6.
The set of low-level logical term values in a low-level strand space Σ is given by: $T \cup N \cup E \cup I \cup \hat{T} \cup ChannelTypes \cup N \cup Σ \cup {+, -} \cup P (T) \cup P (Σ)$ . Let $B$ be a low-level bundle, t be a logical term and Γ be a low-level term map, from variables to low-level logical term values, defined on all free-variables in t, such that t is well typed. Then, the low-level logical term value of t in $B$ , denoted ${⟦ t ⟧}_{B}^{Γ}$ , is defined inductively as follows (for ease we omit cases that are equivalent to the high-level semantics):
${⟦ node (t, n) ⟧}_{B}^{Γ} \hat{=} ({⟦ t ⟧}_{B}^{Γ}, app_node ({⟦ t ⟧}_{B}^{Γ}, {⟦ n ⟧}_{B}^{Γ}))$ , providing ${⟦ n ⟧}_{B}^{Γ} ⩽ app_{height}_{B} ({⟦ t ⟧}_{B}^{Γ})$ ;

${⟦ strand (t) ⟧}_{B}^{Γ} \hat{=} strand ({⟦ t ⟧}_{B}^{Γ})$ ;

${⟦ height (t) ⟧}_{B}^{Γ} \hat{=} app_{height}_{B} ({⟦ t ⟧}_{B}^{Γ})$ ;

${⟦ {role}_{k} ⟧}_{B}^{Γ} \hat{=} {Role}_{k} \cap {strand (n) ∣ n \in N_{B}^{reg}}$ ;

${⟦ msg (t) ⟧}_{B}^{Γ} \hat{=} {\hat{α}}_{B} ({⟦ t ⟧}_{B}^{Γ})$ .
Let $B$ be a low-level bundle, ϕ be a high-level bundle formula, and Γ be a low-level term map defined on all free-variables of ϕ. Then, $B$ and Γ satisfy ϕ, denoted $(B, Γ) ⊨ ϕ$ , according to the following inductive definition (we omit cases that are equivalent to the high-level semantics):
$(B, Γ) ⊨ Confidential (t)$ iff ${⟦ t ⟧}_{B}^{Γ}$ is confidential in $B$ and ${⟦ t ⟧}_{B}^{Γ} \in T_{app}$ ;

$(B, Γ) ⊨ UniquelyOriginates (t_{1}, t_{2})$ iff ${⟦ t_{1} ⟧}_{B}^{Γ} \in A ∖ T_{P}^{I}$ and uniquely originates in the application layer on ${⟦ t_{2} ⟧}_{B}^{Γ}$ .

6.4. Logical equivalence

To prove that the low and high-level semantics of our logic correspond, we firstly consider the problem of relating terms of the logic. Firstly, we define a relation $↗_{\hat{ψ}}$ that pairs low-level term values with the high-level term value that they abstract to. We then prove that, given a logical term t and a high-level bundle $\hat{B}$ that abstracts a low-level bundle $B$ , ${⟦ t ⟧}_{B}^{Γ} ↗_{\hat{ψ}} {⟦ t ⟧}_{\hat{B}}^{\hat{Γ}}$ .

Definition 6.7.
Let $B$ be a low-level bundle and $\hat{B}$ be a bundle that abstracts it using a node map $\hat{ψ}$ . x is abstracted by y, denoted $x ↗_{\hat{ψ}} y$ , iff one of the following clauses applies:
$x, y \in T \cup N \cup E \cup I \cup \hat{T} \cup ChannelTypes \cup {+, -}$ and $x = y$ ;

$x \in N_{B}$ , $y \in N_{\hat{B}}$ and $x \hat{ψ} y$ ;

x is a low-level strand, y is a high-level strand, $app_{height}_{B} (x) = {height}_{\hat{B}} (y)$ and, for all $i ⩽ {height}_{\hat{B}} (y)$ , $(x, app_node (x, i)) ↗_{\hat{ψ}} (y, i)$ ;

x is a set of strands, y is a set of strands and there exists a bijection μ between x and y such that, for each pair $(st, {st}^{'}) \in μ$ , $st ↗_{\hat{ψ}} {st}^{'}$ .
We lift the above definition to apply to logical term environments. $Γ ↗_{\hat{ψ}} \hat{Γ}$ iff Γ and $\hat{Γ}$ are defined on the same variables and for each variable v, $Γ (v) ↗_{\hat{ψ}} Γ (v)$ .

In order to prove compatibility we need to assume that the set of regular strands (i.e. ${Role}_{k}$ and ${\hat{Role}}_{k}$ ) are properly defined as follows.
Assumption 6.8.
Let $B$ be a low-level bundle and $\hat{B}$ be a high-level bundle that abstracts $B$ using an abstraction function $\hat{ψ}$ . Then, for all k: ${strand (n) ∣ n \in N_{B}} \cap {Role}_{k} ↗_{\hat{ψ}} {\hat{Role}}_{k} \cap {strand (\hat{n}) ∣ \hat{n} \in N_{\hat{B}}}$ .

Using the above we are now able to prove the required result.
Lemma 6.9.
Let t be a logical term, $B$ be a low-level bundle and $\hat{B}$ be a high-level bundle that abstracts $B$ using a node map $\hat{ψ}$ . Further, let Γ and $\hat{Γ}$ be logical term environments defined on all free variables in t such that $Γ ↗_{\hat{ψ}} \hat{Γ}$ . Then, ${⟦ t ⟧}_{B}^{Γ} ↗_{\hat{ψ}} {⟦ t ⟧}_{\hat{B}}^{\hat{Γ}}$ .

We now consider under what circumstances the ≼ relation between application-layer nodes is preserved between low and high-level bundles. Consider two nodes $n_{1}$ and $n_{2}$ in a low-level bundle such that $n_{1} ≼ n_{2}$ . If the path between $n_{1}$ and $n_{2}$ transfers only transport-layer values then the path does not need to be abstracted. Hence, it is not necessarily the case that the same relation holds amongst the abstracted nodes and, therefore, we can only prove that if ${\hat{n}}_{1} ≼ {\hat{n}}_{2}$ in the high-level bundle, then $n_{1} ≼ n_{2}$ .
Lemma 6.10.
Let $B$ be a normal low-level bundle and $\hat{B}$ be a high-level bundle that abstracts it using a node map $\hat{ψ}$ . Then, if $n_{1}, n_{2} \in N_{payload}$ , $\hat{ψ} (n_{1}) = {\hat{n}}_{1}$ , $\hat{ψ} (n_{2}) = {\hat{n}}_{2}$ and ${\hat{n}}_{1} ≼_{\hat{B}} {\hat{n}}_{2}$ , then $n_{1} ≼_{B} n_{2}$ .

Using the above we are now able to state that bundle satisfaction is preserved by abstraction. In light of Lemma 6.10 we are only able to consider formulas where ≼ only occurs positively (i.e. within the scope of an even number of negations only). However, this is not a restriction in practice; all formulas that we want to express will take the form of an implication where ≼ will occur only on the right-hand side (i.e. as a conclusion), and thus will occur positively.
Proposition 6.11.
Let ϕ be a closed high-level bundle predicate in which ≼ occurs only positively. Further, let $B$ be a normal low-level bundle in a strand space and $\hat{B}$ be a high-level bundle that abstracts $B$ . If $(\hat{B}, \hat{Γ}) \hat{⊨} ϕ$ then $(B, Γ) ⊨ ϕ$ .

It is not necessarily the case that $(B, \emptyset) ⊨ ϕ$ implies $(\hat{B}, \emptyset) \hat{⊨} ϕ$ . For example, consider ≼ and suppose that $n_{1}, n_{2} \in N_{payload}$ are such that $n_{1} ≼_{B} n_{2}$ . If the path between $n_{1}$ and $n_{2}$ is not abstracted, perhaps because it is purely a transport-layer path, then the corresponding property will not necessarily hold in $\hat{B}$ . However, if ≼ does not appear in the formula, then the reverse implication does hold.
6.5. Proofs by abstraction

We now consider how to combine the results of Proposition 5.17 and Proposition 6.11 to show that the high-level strand spaces model is sound. We prove that whenever a low-level bundle $B$ does not satisfy a bundle formula there is a high-level bundle ${\hat{B}}^{'}$ that also does not satisfy the formula. We prove this by using Proposition 5.17 to obtain a bundle $B^{'}$ that is abstractable and such that $B ⊵ B^{'}$ . Then, we apply Proposition 6.11 to deduce that if $B^{'}$ does not satisfy a particular bundle, then there exists a high-level bundle ${\hat{B}}^{'}$ that abstracts $B$ and such that ${\hat{B}}^{'}$ also does not. Hence, it suffices to show that whenever $B ⊵ B^{'}$ and $B$ does not satisfy a property, $B^{'}$ also does not satisfy this property. We state this as follows.

Lemma 6.12.
Let ϕ be a closed high-level bundle formula in which ≼ occurs only positively. Let $B$ , $B^{'}$ be two low-level bundles such that $B ⊵ B^{'}$ and $(B^{'}, \emptyset) ⊨ ϕ$ . Then $(B, \emptyset) ⊨ ϕ$ .

Lastly, we can state our main result that shows that a proof of protocol correctness in the high-level model is sound, in that it will consider all attacks that could have occurred in the low-level model.
Proposition 6.13.
Let ϕ be a closed high-level bundle predicate in which ≼ occurs only positively. Further, let $B$ be a normal low-level bundle in a strand space and $\hat{B}$ be a high-level bundle that abstracts $B$ . If $(\hat{B}, \hat{Γ}) \hat{⊨} ϕ$ then $(B, Γ) ⊨ ϕ$ .

Note that the above proposition requires the high-level strand space to abstract $Σ_{E}$ , rather than Σ. Therefore, when doing the proof of protocol correctness in the high-level model the penetrator’s initial knowledge must include $T_{X}$ . In practice, this should not cause any difficulty as $T_{X}$ contains only items that are not in $T_{app}$ , meaning that nothing of consequence to the application-layer security of the protocol is added to $T_{P}$ . This means that when constructing proofs of protocol correctness, any assumptions on the contents of $T_{P}$ should be negative, in that they should specify what is not in $T_{P}$ , rather than what is.

High-level proofs. When proving the correctness of application-layer protocols in the high-level strand spaces model we will frequently only consider normal bundles, for ease. Further, recall that the high-level bundles produced as abstractions of low-level bundles in Proposition 4.28 contain TX strands, which we do not want to consider in high-level proofs. We thus need to prove that this is sound. We start by defining a high-level version of ⊵, $\hat{⊵}$ , and then prove that, given an arbitrary high-level bundle, we can find a normal high-level bundle that relates to the original bundle using $\hat{⊵}$ but contains no TX strands.
Definition 6.14.
A high-level bundle $\hat{B}$ can be reduced to ${\hat{B}}^{'}$ , denoted $\hat{B} \hat{⊵} {\hat{B}}^{'}$ , iff $\hat{B}$ and ${\hat{B}}^{'}$ are equivalent and $≼_{{\hat{B}}^{'}}$ relates no more regular nodes than $≼_{\hat{B}}$ , i.e.: $(N_{\hat{B}}^{reg} \times N_{\hat{B}}^{reg}) \cap ≼_{\hat{B}} \supseteq (N_{{\hat{B}}^{'}}^{reg} \times N_{{\hat{B}}^{'}}^{reg}) \cap ≼_{{\hat{B}}^{'}} .$
Lemma 6.15.
If $\hat{B}$ is a high-level bundle then there exists a normal bundle ${\hat{B}}^{'}$ such that $\hat{B} \hat{⊵} {\hat{B}}^{'}$ .
Lemma 6.16.
Let ϕ be a closed high-level bundle formula in which ≼ occurs only positively and let $\hat{B}$ , ${\hat{B}}^{'}$ be two high-level bundles such that $\hat{B} \hat{⊵} {\hat{B}}^{'}$ and $({\hat{B}}^{'}, \emptyset) \hat{⊨} ϕ$ . Then $(\hat{B}, \emptyset) \hat{⊨} ϕ$ .
Proposition 6.17.
Let $\hat{Σ}$ be a high-level strand space and ϕ be a closed high-level bundle formula in which ≼ occurs only positively. If every normal bundle of $\hat{Σ}$ that contains no TX strands satisfies ϕ, then every bundle of $\hat{Σ}$ satisfies ϕ.

Thus, in all high-level strand spaces proofs we can, without loss of generality, consider only normal bundles.
6.6. Summary

In this section we have proven that the high-level strand spaces model is sound. In particular, we proved in Proposition 6.13 that, if a protocol has been proven to satisfy a given property in the high-level strand spaces model, then it also satisfies the same property in any corresponding low-level strand spaces model, assuming the transport protocols satisfy the relevant channel types. We also showed, in Proposition 6.17, that if a correctness property is satisfied by all high-level normal bundles then that it is satisfied by all high-level bundles. This is particularly useful since we often only consider normal bundles, for ease.

We began, in Section 6.1, by defining a logic of correctness properties. Then, in Section 6.2 and Section 6.3 we defined what it meant for high and low-level bundles to satisfy the correctness properties. In Section 6.4 we then proved that, given a high-level bundle that abstracts a low-level bundle, the value of any logical term in the low-level bundle is related, according to Definition 6.7, to its value in the high-level bundle. This was then used in Section 6.5 to prove that whenever a low-level bundle satisfies a correctness property, then the corresponding high-level bundle also satisfies the property.

7. TLS

As TLS [11] is the most widespread secure transport protocol, we need to ensure that our model allows application-layer protocols that use TLS to be analysed. TLS is really two separate protocols: bilateral TLS (denoted ${TLS}^{C \leftrightarrow S}$ ), where the server is authenticated to the client and the client is authenticated to the server; and unilateral TLS, where only the former occurs. Both forms of the protocol are confidential and authentic (i.e. they are in $AuthConf$ ), but differ in what information they provide about the client. Unilateral TLS does not provide an identity for the client (i.e. the client endpoint is of the form $?_{ψ}$ ), whereas bilateral TLS does (i.e. the client endpoint is of the form $A_{ψ}$ ).

Unfortunately, as we illustrate below, TLS does not satisfy Assumption 5.10 as it is possible for some encryptions to be shared between the two forms of TLS in a harmless way that is not allowed by Assumption 5.10. In particular, this violates Assumption 5.10 (1), which requires that the sets of transport-layer message encryptions for the two protocols are disjoint.

In this section we describe how any low-level bundle that uses TLS can be transformed into a bundle of a strand space that does satisfy Assumption 5.10 and has the same application-layer behaviour.

TLS. Unilateral and bilateral TLS both have two stages. The first phase, called the handshake phase, involves the two participants exchanging data in order to derive a master key; this is then used in the second phase to protect the messages sent in the session. In the second phase, the identities of the sender and recipient of the message are not included in the message packaging. Thus, if the penetrator can somehow cause two sessions to use the same encryption keys then he will be able to pass messages between the two sessions without the other participants detecting it. If the two participants are regular agents then this is not possible [21]. However, if the penetrator is a legitimate participant in two different TLS sessions, one as the client and one as the server (i.e. both regular agents are aware they are communicating with the penetrator), he is able to manipulate the messages to cause this to occur.

Fig. 10.

A example of a session where the penetrator causes a unilateral TLS session between C and $P_{Server}$ to use the same encryption key as the bilateral TLS session between $P_{Client}$ and S. The above uses a simplified version of TLS.

The encryption keys used in the second phase are generated from a nonce $n_{c}$ sent by the client, a nonce $n_{s}$ sent by the server and the pre-master secret $p m s$ , which is sent by the client. The penetrator could act as the server in one session, taking the client nonce and pre-master secret and play these into a second session, in which he acts as the client. He can then pass back the server nonce from the second session to the client in the first session, as illustrated in Fig. 10. The participants will all generate the same master key.

If one of the sessions is using unilateral TLS and the other is using bilateral TLS then $E_{trpt}^{{TLS}^{C \to S}}$ and $E_{trpt}^{{TLS}^{C \leftrightarrow S}}$ are not disjoint, as required by Assumption 4.10 and Assumption 5.10 (1). Further, there are some penetrator paths that start at a bilateral TLS node and end at a unilateral TLS node, as the penetrator can forward messages from one session into the other. There is no high-level strand that corresponds to this behaviour.

Transforming bundles. Whilst such behaviour contradicts our assumptions, it is clear that any bundle in which such behaviour occurs could be replaced by a bundle in which disjoint message encryption is satisfied by:

Making the penetrator generate fresh nonces, rather than passing the nonces directly between the sessions; then

replacing every path that crosses between the two sessions by a Receive path, then a Send path.

The second step ensures that messages are no longer passed directly between the strands, whilst the first step ensures that the sessions will use disjoint keys and hence $E_{trpt}^{{TLS}^{C \to S}}$ and $E_{trpt}^{{TLS}^{C \leftrightarrow S}}$ are disjoint. The second transformation step is possible as the above situation can only arise when the penetrator is legitimately involved with both sessions, and thus he knows the keys required to send and receive messages. The first transformation is permitted as the penetrator was the intended participant, so can change the values that he uses.

Unfortunately, the low-level bundle that results from the above transformation is not equivalent to the original bundle, since the regular behaviour has changed as the keys used have been altered. However, the application-layer behaviour has not changed. We formalise the notion of equivalence as follows.

Definition 7.1.

Two low-level bundles $B$ and $B^{'}$ are application-layer-equivalent iff there exists a bijection γ between the regular application-layer nodes of $B$ and $B^{'}$ (i.e. $γ : N_{B}^{reg} \cap N_{payload} \to N_{B^{'}}^{reg} \cap N_{payload}$ ) such that:

For all $(n, n^{'}) \in γ$ , ${\hat{α}}_{B} (msg (n)) = {\hat{α}}_{B^{'}} (msg (n^{'}))$ ;

γ respects the regular strand structure on application-layer nodes, i.e. for all $n_{1}, n_{2} \in N_{payload}$ , $n_{1} \Rightarrow_{B}^{+} n_{2}$ iff $γ (n_{1}) \Rightarrow_{B^{'}}^{+} γ (n_{2})$ .

In the above, the first clause ensure that the application-layer messages are identical. The second clause then ensures that none of the nodes have been re-ordered, as two regular strands will be related by this bijection iff every application-layer node is related by γ. Together, these ensure that, if two regular strands in two application-layer-equivalent bundles are related by γ, then the strands abstract to the same high-level strand.

As with standard bundle equivalence, application-layer equivalence does not preserve the correctness of application-layer correctness properties that include ≼ (cf. Definition 5.4). Thus, we introduce a relation $⊵_{app}$ , analogous to ⊵, that ensures ≼ only decreases in size. We also require that transport-layer encryptions are replaced with encryptions such that the inverse keys are equivalently confidential. This ensures that the penetrator cannot learn the value of application-layer messages in one bundle, but not the other.

Definition 7.2.

A low-level bundle $B$ can be application-layer reduced to $B^{'}$ , denoted $B ⊵_{app} B^{'}$ , iff:

$B$ and $B^{'}$ are application-layer-equivalent using a bijection γ;

For all regular application-layer nodes $n_{1}, n_{2} \in N_{payload} \cap N_{B^{'}}$ , if $n_{1} ≼_{B^{'}} n_{2}$ then $γ^{- 1} (n_{1}) ≼_{B} γ^{- 1} (n_{2})$ ;

For all regular application-layer nodes $n \in N_{payload} \cap N_{B}$ , if $es ⩽ {expath}^{c} (chan (n))$ is such that ${| m |}_{k} ⊑_{es} msg (n)$ then, letting ${| m^{'} |}_{k^{'}} ⊑_{es} msg (γ (n))$ , $k^{' - 1}$ is confidential iff $k^{- 1}$ is confidential.

It is clear that the transformation that we described above will result in a bundle that is application-layer-equivalent to the original bundle. Thus, we can formalise the notion that any TLS bundle can be converted into an application-layer-equivalent bundle that satisfies our assumptions as follows.

Claim 7.3.

Let Σ be a low-level strand space that satisfies layer-disjoint encryption, except for disjoint message encryption or disjoint transport-layer payload messages between unilateral and bilateral TLS. There exists a strand space $Σ^{{TLS}^{C \leftrightarrow S}}$ , satisfying full layer-disjoint encryption and such that there is a bijection χ between the bundles of Σ and $Σ^{{TLS}^{C \leftrightarrow S}}$ such that, for all $(B, B^{'}) \in χ$ , $B ⊵_{app} B^{'}$ .

We believe the truth of the above claim is intuitively clear. A formal proof requires a full analysis of both forms of TLS, which is far beyond scope of this paper. [21] contains a suitable formalisation of bilateral TLS in the strand spaces model. This could be extended to a model of unilateral TLS, which would allow this claim to be formalised and proven.

The following proposition shows that whenever a property is proven correct in a high-level abstraction of the transformed TLS strand space, then it is also correct in the original strand space that did not satisfy Assumption 5.10.

Claim 7.4.

Let Σ be a low-level strand space that satisfies layer-disjoint encryption, except for disjoint message encryption between unilateral and bilateral TLS or disjoint transport-layer payload messages between unilateral and bilateral TLS. Further, let $Σ^{{TLS}^{C \leftrightarrow S}}$ be the strand space resulting from Claim 7.3 , $Σ_{E}^{{TLS}^{C \leftrightarrow S}}$ be related to $Σ^{{TLS}^{C \leftrightarrow S}}$ by Definition 5.13, ϕ be a closed high-level bundle formula and ${\hat{Σ}}_{E}^{{TLS}^{C \leftrightarrow S}}$ be a strand space abstracting $Σ_{E}^{{TLS}^{C \leftrightarrow S}}$ . Then, if every bundle of ${\hat{Σ}}_{E}^{{TLS}^{C \leftrightarrow S}}$ satisfies ϕ then every bundle of Σ satisfies ϕ.

8. Conclusions

In this paper we have presented the high-level strand spaces model which models the guarantees provided by both unilateral and bilateral transport-layer protocols. Further, it supports transport-layer protocols that, like TLS, can group messages into sessions.

The main contribution of this paper is the soundness proof of the high-level strand spaces model. We have proven that, subject to certain statically checkable assumptions, whenever there exists a low-level bundle that does not satisfy a protocol correctness property, then there exists a high-level bundle that also does not satisfy the property. Thus, if a protocol can be proven correct at the high-level, then it is guaranteed to be correct at the low-level. We have also sketched how our results can be extended to prove that any bundle that contains a use of TLS can be transformed to an equivalent bundle that satisfies our assumptions.

The soundness result was proven by firstly, in Section 4, proving that all interference-free bundles can be abstracted. In Section 5 we proved that a bundle $B$ of a strand space Σ that satisfies disjoint-layered encryption can be transformed to an interference-free bundle $B^{'}$ of a strand space $Σ_{E}$ such that $B ⊵ B^{'}$ . In Section 6 we defined a logic of protocol-correctness properties, before proving that whenever $B$ does not satisfy a correctness property ϕ and $B ⊵ B^{'}$ , then $B^{'}$ also does not satisfy ϕ. Lastly, we proved that whenever ${\hat{B}}^{'}$ abstracts $B^{'}$ and $B^{'}$ does not satisfy a property ϕ, then ${\hat{B}}^{'}$ also does not satisfy ϕ.

Related work. As stated in Section 1, there are many other formalisms for verifying layered security protocols. [1,3,4,6,12] all provide ways of modelling application-layer protocols that are layered on secure transport-layer protocols, varying in exactly what types of secure transport protocols they support. However, none of these models have a formally proven and general soundness result that supports commonly used transport-layer protocols such as TLS: we consider this to be a strength of the high-level strand spaces model. On the other hand, the above techniques all allow for some form of automated analysis, whilst there is, at the present time, no tool support for the high-level strand spaces model. [14] does present some proof rules that dramatically simplifies the process of developing these proofs.

The LTL-based model that [3] proposes is similar to the model presented here, but does not include support for protocols that group messages into sessions, such as TLS, or for unilateral protocols. [12] models the protocol in CSP and supports both bilateral protocols and protocols that group messages into sessions, but does not support unilateral protocols. It also supports protocols that prevent messages from being reordered, which is not supported by the model presented in this paper: see [14] for a version that does support such protocols. [4] extends the inductive approach [24] and supports simple bilateral transport-layer protocols that do not group messages into sessions. [6] presents a formalism based on the pi-calculus that supports extremely strong channel definitions based on observational equivalence; as such these channels are likely to be difficult to implement in practice. [1] models the protocols using a variant of the join-calculus that supports very strong channel definitions that are difficult to implement in practice.

The most similar approach to verifying layered protocols by abstraction is that of Mödersheim and Viganò [22]. They define a model, the Ideal Channel Model (ICM), that abstracts away from how the channels are implemented. They then consider how to model the guarantees given by unilaterally authenticating transport-layer protocols (or secure pseudonymous channels). In their model they specify confidential, authentic and secure channels, which roughly correspond to $Conf$ , $Auth$ and $AuthConf$ , respectively. The primary difference between the two approaches is that whilst both formalisms permit analysis of protocols that use bilateral or unilateral transport protocols, ours also allows protocols that do not group messages into sessions to be analysed (i.e. by letting the channel end be $?$ ). Another difference is that they address unauthenticated clients using pseudonyms rather than our name and channel end combination. These are essentially equivalent, but we think that using a combination of a channel end is close to what is occurring at the transport layer.

In [16] Groß and Mödersheim consider what they term vertical protocol composition, which corresponds to our notion of layering protocols. They develop a semantic condition that proves arbitrary composition of protocols introduces no new attacks. In one sense, this is more general than the result we prove since it permits arbitrary stacks of protocols to be composed, whereas we have only considered the two layer case. However, it only allows transport-layer protocols that establish two symmetric keys, one for protecting messages sent in each direction, meaning it is not a general result.

In [23] Mödersheim and Viganò also propose a statically checkable condition that allows for the composition of precisely two layers in a very similar way to the approach presented in this paper. However, their assumptions are more restrictive than ours, and prevent TLS from being used as a secure transport layer, as well as prohibiting a large class of application-layer protocols. For example, their Disjointness condition requires the disjointness of all non-atomic messages, whereas we only require certain encryptions to be disjoint. Also, their Disjointness of Concrete Payloads requires that distinct agents send disjoint payloads, which appears to prohibit messages from being forwarded by agents, as is commonplace. Additionally, they currently only consider transport-layer protocols where a single message is sent, although this is not likely to be a problem in practice.

Future work. One obvious enhancement to the high-level strand spaces model would be to allow protocols that consist of more than two layers to be modelled. For example, consider a simple transport-layer protocol that transmits a username and a password over a unilateral TLS connection, and then transmits application-layer messages. It would be desirable to prove that this implements a bilateral $AuthConf$ channel that also authenticates the user to the server.

In order to prove results about such protocols, it would be interesting to give some simple proof rules that detail how the security guarantees provided by different layers combine. Further, it would be useful to adapt the soundness proof of this paper to prove that any such analysis is sound. We expect that this particular case should be solvable by a sort of induction over the protocol in question, but the details need to be checked carefully. Whilst this problem has been considered in [22] before, no general proof rules were provided and a statically checkable soundness result is not available, as discussed above.

It would be useful to develop a tool that could check if the assumptions of Section 5.2 are satisfied. This could then automatically inform the user of potential implementations of their protocol that are guaranteed to be secure. We have developed a prototype tool that accomplishes some of this, but further work is required in order to enable the tool to automatically search for a proof.

Supplemental material

Online supplement consisting of Appendices is available at: https://dx-doi-org.web.bisu.edu.cn/10.3233/JCS-150526.

Appendices

Footnotes

Acknowledgments

We would like to thank Michael Goldsmith, Joshua Guttman and Bill Roscoe for useful comments and discussions. We would also like to thank the anonymous reviews for their many helpful contributions that helped to improve the paper.

References

[1]

Abadi,

Fournet and

Gonthier, Secure implementation of channel abstractions, Information and Computation 174(1) (2002), 37–83.

[2]

Andova,

Cremers,

Gjøsteen,

Mauw,

S.F.

Mjølsnes and

Radomirović, A framework for compositional verification of security protocols, Information and Computation 206(2–4) (2008), 425–459.

[3]

Armando,

Carbone and

Compagna, LTL model checking for security protocols, in: Computer Security Foundations Symposium, 2007, pp. 385–396.

[4]

Bella,

Longo and

L.C.

Paulson, Verifying second-level security protocols, in: Theorem Proving in Higher Order Logics, 2003, pp. 352–366.

[5]

Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in: Proceedings of the 14th IEEE Computer Security Foundations Workshop, 2001, pp. 82–96.

[6]

Bugliesi and

Focardi, Channel abstractions for network security, Mathematical Structures in Computer Science 20(1) (2010), 3–44.

[7]

Ciobâcă and

Cortier, Protocol composition for arbitrary primitives, in: Computer Security Foundations Symposium, 2010.

[8]

Cortier and

Delaune, Safely composing security protocols, Formal Methods in System Design 34(1) (2008), 1–36.

[9]

C.J.F.

Cremers, The Scyther tool: Verification, falsification, and analysis of security protocols, in: Computer Aided Verification, 2008.

10.

[10]

Datta,

Derek,

J.C.

Mitchell and

Roy, Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science 172 (2007), 311–358.

11.

[11]

Dierks and

Rescorla, The TLS protocol: Version 1.2, 2008.

12.

[12]

Dilloway and

Lowe, Specifying secure transport channels, in: Computer Security Foundations Symposium, 2008, pp. 210–223.

13.

[13]

Dolev and

Yao, On the security of public key protocols, IEEE Transactions on Information Theory 29(2) (1983), 198–208.

14.

[14]

Gibson-Robinson, Analysing layered security protocols, PhD thesis, University of Oxford, 2013.

15.

[15]

Gibson-Robinson and

Lowe, Analysing applications layered on unilaterally authenticating secure transport protocols, in: Formal Aspects in Security and Trust, 2011.

16.

[16]

Groß and

Mödersheim, Vertical protocol composition, in: Computer Security Foundations Symposium, 2011.

17.

[17]

Guttman and

F.J.

Thayer, Protocol independence through disjoint encryption, in: Computer Security Foundations Workshop, 2000, pp. 24–34.

18.

[18]

Guttman and

F.J.

Thayer, Authentication tests and the structure of bundles, Theoretical Computer Science 283(2) (2002), 333–380.

19.

[19]

Kamil and

Lowe, Specifying and modelling secure channels in strand spaces, in: Formal Aspects in Security and Trust, 2009.

20.

[20]

Kamil and

Lowe, Understanding abstractions of secure channels, in: Formal Aspects in Security and Trust, 2010.

21.

[21]

Kamil and

Lowe, Analysing TLS in the strand spaces model, Journal of Computer Security 19(5) (2011), 975–1025.

22.

[22]

Mödersheim and

Viganò, Secure pseudonymous channels, in: European Symposium on Research in Computer Security, 2009.

23.

[23]

Mödersheim and

Viganò, Sufficient conditions for vertical composition of security protocols, in: Proceedings of the 9th ACM Symposium on Information, Computer and Communications Security, 2014, pp. 435–446.

24.

[24]

L.C.

Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security 6(1) (1998), 85–128.

25.

[25]

Schemers and

Allbery, WebAuth technical specification v.3, 2009.

26.

[26]

F.J.

Thayer Fábrega,

Herzog and

Guttman, Strand spaces: Proving security protocols correct, Journal of Computer Security 7(2,3) (1999), 191–230.

Verifying layered security protocols

Abstract

Keywords

1. Introduction

2. Introduction to strand spaces

Definition 2.1 (Based on [26]).

1 This differs from [26] where the set of atoms was denoted by T and the set of terms by A .

Definition 2.3 (From [26]).

Definition 2.4 (From [26]).

Definition 2.5 (From [26]).

Definition 2.6 (From [26]).

Lemma 2.7 (From [26]).

Definition 2.8 (From [26]).

Definition 2.9 (Adapted from [26]).

Definition 2.10 (From [18]).

Definition 2.11 (From [18]).

Definition 2.12 (Based on [18]).

Definition 2.13 (Based on [18]).

Lemma 2.14 (Based on [18]).

3. The high-level strand spaces model

3.1. Basic definitions

Definition 3.10 (Authenticated).

2 [21] uses the low-level strand spaces model to prove TLS correct. Utilising Section 4 it would be straightforward to prove that TLS indeed only allows RV and SD strands; however, this is beyond the scope of this paper.

4.1. Preliminaries

5. Disjoint encryption

5.1. Preliminaries

6. Abstracting correctness properties

6.1. A logic of correctness properties

Table 1 An informal explanation of the meaning of the terms of our correctness property logic

7. TLS

Supplemental material

Footnotes

Acknowledgments

References

¹
This differs from [26] where the set of atoms was denoted by $T$ and the set of terms by $A$ .

²
[21] uses the low-level strand spaces model to prove TLS correct. Utilising Section 4 it would be straightforward to prove that TLS indeed only allows RV and SD strands; however, this is beyond the scope of this paper.

Table 1
An informal explanation of the meaning of the terms of our correctness property logic