Verification of stateful cryptographic protocols with exclusive OR

Abstract

In cryptographic protocols, in particular RFID protocols, exclusive-or (XOR) operations are common. Due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. In this paper, we improve the Tamarin prover and its underlying theory to deal with an equational theory modeling XOR operations. The XOR theory can be combined with all equational theories previously supported, including user-defined equational theories. This makes Tamarin the first verification tool for cryptographic protocols in the symbolic model to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.

Keywords

Formal verification cryptographic protocols exclusive or

1. Introduction

Security protocols aim to protect communication in the presence of malicious parties, for example against an attacker on the internet or an attacker on the local wireless network. They are vital for applications including e-commerce, online voting, e-government, and online banking to ensure security properties, such as confidentiality, entity and message authentication, anonymity, and untraceability. To this end, security protocols employ cryptographic primitives, most commonly symmetric and asymmetric encryption, digital signatures, and cryptographic hash functions. Many protocols, in particular those designed for applications where the participants have limited power or computational resources, employ exclusive-or (XOR) operations. Typical examples are RFID protocols [30,42,45] and mobile communication protocols (3G [1], 4G/LTE [2], 5G [3]).

As illustrated by many attacks, e.g., [4,7,16], security protocols are notoriously difficult to get right. Consequently, many tools for the automated analysis of security protocols have been developed, e.g., [6,20,32,37,39,49]. Historically, the main focus of these tools has been the analysis of authentication and confidentiality properties of protocols that employ standard cryptographic primitives in a Dolev–Yao adversary model. More recently there has been active research on widening the scope of automated protocol verification, for example by extending the class of properties that can be verified to include equivalence properties [13,18,24,27,52], extending the adversary model with complex forms of compromise [12], and extending the expressiveness of protocols by allowing different sessions to update a global, mutable state [5,43].

Perhaps the most significant development is tool support for user-specified equational theories allowing for the modeling of particular cryptographic primitives [20,24,34,37,49]. However, these tools do not allow a faithful modeling of XOR or have other strong limitations such as bounded verification or no support for state. We refer to the related work, in Section 5, for a detailed discussion. The difficulty in faithfully modeling XOR is due to the unique combination of algebraic properties that XOR satisfies, specifically (i) the associativity ( $x \oplus (y \oplus z) = (x \oplus y) \oplus z$ ) and commutativity ( $x \oplus y = y \oplus x$ ) properties and (ii) the cancellation properties (e.g., $x \oplus x = 0$ ). Modeling XOR without one of the two classes of properties provides only weak security guarantees since whole classes of attacks are missed.

The Tamarin prover [49,57] is a state-of-the-art cryptographic protocol verifier which allows the user to combine all of the following: specifying complex security properties (both trace and equivalence properties [13]), modeling cryptographic primitives by means of equational theories, and allowing protocols to maintain state information. The class of user-specified equational theories supported by the tool is the class of convergent equational theories that have the finite variant property [31] in addition to built-in theories for Diffie–Hellman exponentiations, bilinear pairings, and multisets. Although Tamarin supports such a large class of user-defined equational theories, one cannot simply model XOR using a user-defined theory due to its associativity and commutativity (AC) properties. While Tamarin supports AC symbols in some built-in theories such as Diffie–Hellman exponentiation, the cancellation properties of XOR (see (ii) above) require a special treatment, as a naive implementation often results in non-termination.

Our contributions. In this paper, we significantly extend Tamarin to support a precise modeling of XOR operations taking into account its AC and cancellation properties. More technically, we model XOR in Tamarin’s term algebra by introducing a symbol for XOR, treated modulo AC, that satisfies the expected cancellation properties. To avoid systematic non-termination issues in Tamarin’s backward search, the exploration needs to be constrained without affecting completeness (i.e., preserving all attacks). We show that the previously implemented constraints are not adequate for XOR since they yield systematic non-termination in the presence of XOR. We carefully devise new dedicated constraints for XOR and prove that completeness is still ensured under the combination of all constraints. Finally, we show that the previous attacker model of Tamarin is not suitable for XOR when analyzing equivalence properties as it yields spurious attacks (i.e., attacks that are solely artifacts of this internal model). We improve the attacker model to considerably enhance the precision of the analysis in the presence of XOR. We have implemented these extensions in the Tamarin prover and demonstrate that the tool succeeds to effectively analyze diverse protocols including some that were previously out of scope of automated verification.

We model and analyze the RFID protocol LAK’06 [45], which consists of two roles exchanging five messages. This protocol is stateful, heavily relies on XOR, and features an else branch. We analyze secrecy, non-injective agreement (in both directions) as well as three unlinkability notions. Considering an unbounded number of sessions, we obtain semi-automatic proofs and attacks (i.e., limited number of interactions to guide state exploration, all steps machine-checked) for the reachability properties (i.e., secrecy and agreement). We obtain fully automatic proofs for and attacks on the different unlinkability notions for a bounded number of sessions. Considering such a faithful modeling, all these analyses were out of the scope of existing tools. We also analyze the stateful RFID protocols OTYT’06 [50] and LD’07 [46] against similar properties. These protocols feature key updates, and rely on XOR. Again, we obtain proofs and attacks. For these two protocols we analyze unlinkability for their full stateful version, unlike LAK’06 for which only the stateless version is considered for unlinkability.

We fully automatically analyze two further XOR-based RFID protocols, CH’07 [30] and KCL’07 [42], a version of Needham–Schroeder–Lowe (NSL) with XOR, and a challenge response protocol using XOR. Finally, we analyze the off-line variant of Chaum’s digital cash protocol [25] which uses XOR and blind signatures and thus provides a case study in which the equational theory for XOR is combined with another non-subterm-convergent, user-defined equational theory. In this protocol we prove that a customer remains anonymous when not double-spending coins, and find an attack on anonymity when double-spending. Previous analyses [34,36] could not model XOR precisely and therefore provide weaker guarantees.

This paper is an extended version of [35]. In comparison to the conference paper, this paper includes the detailed proofs, and two additional case studies (OTYT’06 and LD’07). Tamarin’s extension described in this paper has also been used to formally verify 5G AKA [15] and to find a privacy attack on different AKA versions [21], all used for mobile communication.

Outline. We present necessary preliminaries in Section 2. Our extensions of the theory and the Tamarin tool are described in Section 3. We evaluate the latter with the case studies shown in Section 4, and we also argue why one needs both associativity-commutativity (AC) and cancellation properties for faithfully modeling XOR. We review related work in Section 5, and give concluding remarks in Section 6.

2. Preliminaries

In Tamarin, messages are represented as terms. Protocols and adversaries are modeled using multiset rewriting rules. We also show how security properties are specified.

2.1. Messages represented as terms

As usual in symbolic security protocol verification we represent messages and operations on them as terms in an order-sorted term algebra, using an equational theory. We assume a set of operators with their arities as signature $Σ_{Op}$ . We define three sorts, a top sort $msg$ including all terms together with two incomparable subsorts $fr$ and $pub$ , where terms of the former model random (“fresh”) values in general, and nonces and keys in particular, while terms of the latter represent publicly known (“public”) values. We also assume countably infinite sets of variables $V_{s}$ , for each sort s, and call the union of all such sets $V$ . We similarly treat names, with a countable set $N_{s}$ for each sort s, and their union $N$ . The set of terms given by the closure of using operators from the signature containing variables in $V$ and names in $N$ is denoted $T_{Σ_{Op}} (V, N)$ . A term t is ground if it contains no variables and we write $T_{Σ_{Op}} (N)$ for the set of all ground terms, or simply $T_{Σ_{Op}}$ . A substitution σ is a function from variables to terms. We homomorphically lift substitutions to terms and use postfix notation, so $σ (t)$ is written $t σ$ .

Given a signature $Σ_{Op}$ , an equation is an unordered pair of terms s and t, written $s = t$ , for $s, t \in T_{Σ_{Op}} (V)$ . An equational presentation over $Σ_{Op}$ for a given set of equations E is $E = (Σ_{Op}, E)$ . The associated equational theory is the smallest congruence closure containing all instances of E, for which we write $=_{E}$ . Whenever it is clear from the context we drop the signature and simply write $=_{E}$ . Two terms s and t are equal modulo E if and only if $s =_{E} t$ . We consider sets, sequences, and multisets modulo E by using the subscript E.

In Tamarin, user-defined equational theories are given using their rewrite rules oriented left to right. They have to be confluent and terminating, i.e., convergent. In this case there are unique normal forms for all terms, written $t ↓_{E}$ . Thus we reason about terms in normal form in the following.

Example 1.
To model asymmetric signatures, let $Σ_{Op}$ be the signature consisting of the functions $sign (\cdot, \cdot)$ , $checksign (\cdot, \cdot)$ , and $pk (\cdot)$ together with the equation $checksign (sign (x, k), pk (k)) = x$ .

Tamarin also requires that equational theories have the finite variant property (FVP) [31]. For a theory with the FVP, for any term t, we can compute a finite set of terms $t_{1}, \dots, t_{n}$ (all of which are normalized instances of t) with the following property: For any substitution σ, there is an $i \in {1, \dots, n}$ and substitution ϕ such that $t σ ↓_{E} = t_{i} ϕ$ . This enables efficient symbolic protocol analysis by using a pre-computation to replace the equational theory. More precisely, the complete set of variants modulo E for a term t is denoted ${⌈ t ⌉}^{E}$ . This set can be computed via folding variant narrowing [38].

Fig. 1.
Equational theory $E_{XOR}$ for XOR.

XOR operations are usually (see, e.g., [31]) modeled using the equations given in Fig. 1. Equation (1) models the main cancellation property of XOR, (2) models the fact that 0 is the neutral element, and (3) is required for technical reasons (to achieve AC-coherence, shown in [38]). Equations (1) to (3) can be ordered from left to right and result in a convergent rewriting system with the finite variant property, and could thus even be used in a user-specified equational theory in Tamarin. However, equations (4) and (5) cannot be handled in the same way as the resulting equational theory would not be terminating.
2.2. Modeling protocols and adversaries using multiset rewriting rules

Security protocols are modeled by multiset rewriting rules. These rules work on sets of facts. Formally, we assume an unsorted fact signature $Σ_{Fact}$ , partitioned into linear and persistent facts. The set of facts is defined as $F = {F (t_{1}, \dots, t_{n}) ∣ t_{i} \in T_{Σ_{Op}} (V, N), F \in Σ_{Fact} of arity n}$ . Linear facts can only be consumed as often as they have been created, while persistent facts can be consumed an unbounded number of times. We denote the set of multisets of facts as $F^{♯}$ and the set of ground facts as $G^{♯}$ . The function $set (\cdot)$ converts multisets to sets by dropping the multiplicity. We use the superscript $^{♯}$ to denote operations on multisets, e.g., $\cup^{♯}$ denotes the union on multisets.

Labeled multiset rewriting rules give the system’s state transitions. Such rules are given as $(id, l, a, r)$ with $id$ a unique identifier, and l, a, and r multisets of facts. The resulting rule is $r i = id : l - - [a] \to r$ . We say its name is $name (r i) = id$ , its premises are $prems (r i) = l$ , its conclusions $concs (r i) = r$ , and its actions $acts (r i) = a$ .

We denote the ground instances $ginsts (R)$ for a set of multiset rewriting rules R. We denote by $lfacts (l)$ the multiset of linear facts and by $pfacts (l)$ the set of persistent facts in l. The semantics of a set of multiset rewriting rules R are given by a labeled transition relation $\to_{R} \subseteq G^{♯} \times G^{♯} \times G^{♯}$ , defined by the following step rule, where S is the current state (a multiset of facts): $\begin{matrix} \frac{r i = id : l - - [a] \to r \in_{E} ginsts (R) lfacts (l) \subseteq^{♯} S pfacts (l) \subseteq S}{S \overset{set (a)}{\to}_{R} ((S ∖^{♯} lfacts (l)) \cup^{♯} r)} \end{matrix}$ Note that the initial state of a labeled transition system derived from multiset rewriting rules is the empty multiset of facts ∅. The transition according to the step rule transforms a multiset of facts into another multiset of facts. The actions of the rule are the label attached to the transition. We define our security properties over these labels. We rewrite modulo equations E, so we use $\in_{E}$ for the rule instance modulo. Linear facts are consumed and need to be available sufficiently often, while persistent facts just need to be present. The next state is derived by removing consumed linear facts and adding all generated linear (with correct multiplicity) and persistent facts.

There is a single distinguished fresh rule: $Fresh : - - [] \to Fr (n)$ . This rule has no premise and is the only rule allowed to create the linear $Fr$ facts. To ensure that the generated n is unique, there is an additional condition enforcing that within an execution the variables n from two instances are different. A detailed explanation is available in [55].

We define an execution e of a protocol P as the alternating sequence of states and rule instances: $S_{0}, (l_{1} - - [a_{1}] \to r_{1}), S_{1}, \dots, S_{n - 1}, (l_{n} - - [a_{n}] \to r_{n}), S_{n}$ such that $S_{0} = \emptyset$ , and that for all $i \in {1, \dots, n}$ we have all $(S_{i - 1}, (l_{i} - - [a_{i}] \to r_{i}), S_{i})$ are valid steps according to the step rule. We associate the trace $trace (e) = [set (a_{1}), \dots, set (a_{n})]$ with such an execution e. We write $exec (P)$ for the set of executions of P.

We consider a standard Dolev–Yao style adversary with full control over the network and the ability to apply all operators. The message deduction rules are given by $MD$ below. The adversary learns all messages sent by participants as they are put into the linear $Out$ facts and are subsequently stored in the persistent adversary knowledge $K$ . The adversary can send messages to protocol participants by putting them into linear $In$ facts. Moreover, the adversary can generate his own random values and knows all public values. He can also apply functions from the signature using the rules in the third line of $MD$ . $\begin{array}{l} MD = & {Out (x) - - [] \to K (x), K (x) - - [K (x)] \to In (x), \\ Fr (x : fr) - - [] \to K (x : fr), [] - - [] \to K (x : pub)} \\ \cup {K (x_{1}), \dots, K (x_{n}) - - [] \to K (f (x_{1}, \dots, x_{n})) ∣ f \in Σ_{Op} with arity n} \end{array}$ We consider all terms modulo the given equational theory, so these rules do not deal explicitly with the equations modeling the cryptographic theory. As a more efficient form, Tamarin uses dependency graphs to represent the protocol and adversary deduction rules which are applied.

Definition 1 (Dependency Graph).

We say that the pair $dg = (I, D)$ is a dependency graph modulo $E$ for R if I is a sequence of $E$ -ground instances of rules from $R \cup Fresh$ , $D \in N^{2} \times N^{2}$ , and $dg$ satisfies the conditions:

For every edge $(i, u) ↣ (j, v) \in D$ it holds that $i ⩽ j$ and the conclusion fact of $(i, u)$ is syntactically equal to the premise fact of $(j, v)$ .

Every premise of $dg$ has exactly one incoming edge.

Every linear conclusion of $dg$ has at most one outgoing edge.

The Fresh instances are unique.

We denote the set of all dependency graphs modulo

E

for R by

{dgraphs}_{E} (R)

Example 2.
Consider a protocol $P_{basic}$ where agent A sends a nonce m on the network and then receives it, specified using the following rules: $\begin{array}{l} P_{basic} & = {\frac{Fr (m)}{St (A, m) Out (m)} [Start (m)], \frac{St (A, m) In (m)}{} [End (m)]} \end{array}$ Figure 2 gives a sample execution of this protocol as a dependency graph. It also illustrates how the dependency graph represents the trace and intermediate states.

Fig. 2.
Example execution of $(P_{basic} \cup MD)$ .

We write $dgraphs (R)$ to denote all possible dependency graphs for the multiset rules R, and $traces (dg)$ for the traces of a dependency graph $dg$ . It is easy to see that the dependency graphs have the same traces as the labeled transition system executions. Lemma 1 ([55], Lemma 4).

Let E be an equational theory. Then for all protocols P: $\begin{array}{l} {trace (e) | e \in exec (P \cup MD)} =_{E} {t | t \in traces (dg), dg \in {dgraphs}_{E} (P \cup MD)} \end{array}$

2.3. Security property specification

We consider both trace properties and indistinguishability properties. Examples of trace properties are secrecy and mutual agreement. These properties are expressed as first-order logic formulas. Formulas use variables of a new sort, temp, for reasoning about the order of events, and are evaluated on traces. The informal semantics of our atomic formulas are

⊥: false;

$t_{1} \approx t_{2}$ : $t_{1}$ and $t_{2}$ are equal in the equational theory;

$F @ i$ : fact $F \in_{E} tr [i]$ where i is of sort $temp$ and $tr [i]$ is the i-th element of the trace $tr$ on which we evaluate the formula;

$i ≐ j$ : timepoints i and j are equal;

$i ⋖ j$ : timepoint i occurs before timepoint j.

See [55] for all the details on the semantics and fragment of first order logic accepted by Tamarin. We write $tr ⊧ φ$ when φ holds on trace $tr$ and lift the semantics to sets of traces: given a set of traces $Tr$ we write $Tr ⊧^{\forall} φ$ if $tr ⊧ φ$ for any $tr \in Tr$ and $Tr ⊧^{\exists} φ$ if $tr ⊧ φ$ for some $tr \in Tr$ .

We specify unlinkability, anonymity, and more generally equivalence properties by use of diff-terms (defining bi-systems, i.e., two systems differing only in some terms) and check their observational equivalence, see [13].

Example 3 ([13], Ex. 10).

An equational theory representing probabilistic encryption is $\begin{matrix} pdec (penc (m, pk (k), r), k) = m \end{matrix}$ This equation gives rise to the decryption rule for probabilistic encryption for the adversary automatically generated by Tamarin: $\begin{matrix} Dpenc : K (penc (m, pk (k), r)), K (k) - - [] \to K (m) . \end{matrix}$ Consider now the following bi-system: $\begin{matrix} S = & {GEN : Fr (k) - - [] \to Key (k), Out (pk (k)), \\ ENC : Key (k), Fr (r_{1}), Fr (r_{2}), In (x) - - [] \to Out (diff [r_{1}, penc (x, pk (k), r_{2})])} . \end{matrix}$ Here Tamarin will compare the system where $diff [r_{1}, penc (x, pk (k), r_{2})]$ is replaced by $r_{1}$ to the system where it is replaced by $penc (x, pk (k), r_{2})$ . If the adversary cannot distinguish the two systems, they are said to be observationally equivalent. In this example, this means that he cannot distinguish a probabilistic encryption from random.

For both types of properties, Tamarin analyzes the reachability of attack states, which are defined by a given security property. It does so by exploring symbolic traces in a backward fashion.

3. Handling XOR

In the following, we explain how we deal with the AC properties of the XOR theory, and how we integrate it with the existing built-in and user-defined equational theories. Moreover, we show that the existing normal form conditions are insufficient. To address this, we propose a new normal form condition that eliminates redundant steps, and show its soundness. Finally we explain why we also had to adapt the adversary model for equivalence properties.

As explained above, one cannot handle the equational theory for exclusive-or, $E_{XOR}$ , within the user-defined theories of Tamarin due to the combination of its associativity and commutativity (AC) properties with its cancellation properties. To deal with this equational theory, we split it into two parts: (i) the convergent equations modeling the cancellation properties, and (ii) the axioms for associativity and commutativity, and then reason modulo the AC axioms. So, we define (i) $XOR$ to be the equational theory consisting of equations (1)–(3) oriented left to right, and (ii) $AC$ to be the equational theory consisting of equations (4) and (5). As $XOR$ has the required properties ( $AC$ -convergence and $AC$ -coherence, see [38] for details and how $XOR$ has these properties), we can define $t ↓_{XOR}$ as the normal form of term t with respect to $XOR, AC$ -rewriting and have $s =_{E_{XOR}} t$ iff $s ↓_{XOR} =_{AC} t ↓_{XOR}$ . We say that t is $↓_{XOR}$ -normal iff $t =_{AC} t ↓_{XOR}$ .

Tamarin already supports user-defined equational theories (without AC operators) and some built-in equational theories (with AC operators) such as the multiplication operation in the Diffie–Hellman equational theory [55], as well as bilinear pairing and multisets. To integrate the existing theories with XOR, we refer by $DHBPM$ to the rewriting part of equational theory $E_{DHBPM}$ for Diffie–Hellman exponentiation, bilinear pairing, and multisets as well as the user-defined convergent theory with the finite variant property as used in Tamarin, and let $ACC$ denote the underlying equational axioms of associativity and commutativity for multiplication, bilinear pairing, and multisets. Note that $E_{DHBPM}$ , in particular the user-defined part, is not allowed to use the function symbols from $E_{XOR}$ , so that the equational theories are disjoint. We now consider $ALL = XOR \cup DHBPM$ , ${AC}^{'} = AC \cup ACC$ and $E_{ALL} = E_{XOR} \cup E_{DHBPM}$ , i.e., the union of $E_{XOR}$ and the existing built-in equational theories in Tamarin.

Note that this is compatible with any user-defined equational theory as well. In a first step to enable automated analysis, we now switch from dependency graphs to dependency graphs modulo AC using the finite variant property. For a protocol P, we denote the variants of all protocol rules induced by the equational theory ${⌈ P ⌉}^{E}$ . The following lemma establishes a strong connection between both types of dependency graphs.

Lemma 2.
For all protocols P, $\begin{array}{l} {dgraphs}_{E_{ALL}} (P \cup MD) ↓_{ALL} =_{{AC}^{'}} {dg | dg \in {dgraphs}_{AC’} ({⌈ P \cup M D ⌉}^{E_{ALL}}) \land dg ↓_{ALL} -normal} \end{array}$
Proof.
By extension of Lemma 5 in [55]. The proof is analogous as the equational theory has the same properties. □

In a second step, we switch from dependency graphs modulo AC to normal dependency graphs next.
3.1. Normal dependency graphs

Fig. 3.

Message deduction graphs for pairing: the left represents a redundant dependency graph, the middle an impossible deduction with ordered $K$ -facts, and the right shows a shorter deduction with final conclusion equivalent to the left.

Even for simple convergent theories containing only the pairing function $⟨ \cdot, \cdot ⟩$ and the $fst$ and $snd$ operators, non-normalized dependency graphs are not sufficient to automate the analysis of traces. For example, consider the case where the adversary deduces the first element a of a pair $⟨ a, b ⟩$ by applying the function $fst (\cdot)$ , then pairs it with an element c, and then again deduces a, this time from the new pair, to next build the pair $⟨ a, d ⟩$ . This is visualized in the left-most graph of Fig. 3. (Note that the topmost rule is actually an instance of the function application rule for $fst (\cdot)$ where the conclusion $fst (⟨ a, b ⟩)$ is presented in the reduced form a, according to the equational theory.) This is a correct dependency graph, but redundant, as the steps containing c could have been skipped. As this can be resolved in just one step Tamarin uses normal dependency graphs that exclude such useless steps. This is necessary as otherwise automated analysis will easily loop.

Construction and deconstruction rules. To improve efficiency and avoid the aforementioned redundancy, Tamarin makes the equational theory explicit by dividing the adversary rules into two categories: construction rules and deconstruction rules. Deconstruction rules correspond to equations and are used by the adversary just after protocol rules to deduce messages from what has been sent on the network. Construction rules are, conversely, used to build messages from the adversary’s knowledge that are then sent on the network. To achieve this, adversary knowledge $K$ facts are equipped with an orientation, up and down, denoted $K_{}^{↑}$ and $K_{}^{↓}$ . Deconstruction rules have premises with both $K_{}^{↓}$ and $K_{}^{↑}$ facts (as, e.g., decrypting a ciphertext that was received requires knowing the key) and a conclusion with a $K_{}^{↓}$ fact. Construction rules, conversely, have premises with only $K_{}^{↑}$ facts and their conclusion is a $K_{}^{↑}$ fact as well. To match the purpose of construction and deconstruction rules, the new $Out$ rule has a $K_{}^{↓}$ fact as conclusion, while the $In$ rule has $K_{}^{↑}$ facts as premise. The transition from $K_{}^{↓}$ to $K_{}^{↑}$ is achieved by a special rule with label “Coerce”, see below, but no direct conversion from $K_{}^{↑}$ to $K_{}^{↓}$ is possible to prevent loops. This enforces deconstruction rules to be used before construction rules.

In the case of XOR, we have two deconstruction rules and one construction rule, which directly result from the variants of $x_{1} \oplus x_{2}$ . This results in normal deduction rules depicted in Fig. 4, including the usual pairing and unpairing operators.

Fig. 4.

Set of normal deduction rules ${ND}_{XOR}$ .

With such rules, the adversary avoids cases of redundancy as shown in Fig. 3. In the following we consider the normal deduction rules $ND$ , which include ${ND}_{XOR}$ , as well as the construction and deconstruction rules for Diffie–Hellman exponentiation, bilinear pairing, multisets, as well as the user-defined equational theory (see [34,55] for details on these rules).

Normal form conditions. We integrate the concept of normal message deduction with construction and deconstruction rules and dependency graphs, yielding (pre-)normal dependency graphs. (Pre-)normal dependency graphs enforce additional normal form conditions, called N1–N12 [34].

We also use an additional layer of ordering on $K$ facts, and give the ↓ a subscript d, respectively e, to annotate whether it was already used in a bilinear pairing, which is only allowed once.

Definition 2 (Adapted from [34]).

A pre-normal dependency graph for a set of protocol rules P is a dependency graph $dg$ such that $dg \in {dgraphs}_{AC’} ({⌈ P ⌉}_{insts}^{ALL} \cup ND)$ and the following conditions are satisfied:

The dependency graph $dg$ is $↓_{ALL}$ -normal.

There is no multiplication rule that has a premise fact of the form $K^{↑} (s * t)$ and all conclusion facts of the form $K^{x} (s * t)$ are conclusions of a multiplication rule.

If there are two conclusions c and $c^{'}$ with conclusion facts $K^{x} (m)$ and $K^{x^{'}} (m^{'})$ such that $m =_{{AC}^{'}} m^{'}$ and either $x = x^{'} = ↑$ , or $x = ↓ y$ and $x^{'} = ↓ y^{'}$ for $y, y^{'} \in {d, e}$ , then $c = c^{'}$ .

All conclusion facts $K^{↑} (f (t_{1}, \dots, t_{n}))$ where f is an invertible function symbol are conclusions of the construction rule for f.

If a node i has a conclusion $K^{↓ y} (m)$ for $y \in {d, e}$ and a node j has a conclusion $K^{↑} (m^{'})$ with $m =_{{AC}^{'}} m^{'}$ , then $i < j$ and either $root (m)$ is invertible or the node j is an instance of coerce.

There is no node $[K^{↓ d} (a), K^{↑} (b)] - [] \to K^{↓ e} (c \hat{} r)$ where c does not contain any fresh names and $nifactors (r) \subseteq_{{AC}^{'}} nifactors (b)$ .

There is no construction rule for ♯ that has a premise of the form $K^{↑} (s ♯ t)$ and all conclusion facts of the form $K^{↑} (s ♯ t)$ are conclusions of a construction rule for ♯.

The conclusion of a deconstruction rule for ♯ is never of the form $K^{↓ d} (s ♯ t)$ .

There is no node $[K^{↓ d} (a), K^{↑} (b)] - [] \to K^{↓ e} ([d] c)$ such that c does not contain any fresh names and $nifactors (d) \subseteq_{AC’} nifactors (b)$ .

There is no node i labeled with $[K^{↓ d} ([t_{1}] p), K^{↓ d} ([t_{2}] q)] - [] \to K^{↓ d} (\hat{e} (p, q) \hat{} c)$ such that there is a node j labeled with $[K^{↓ d} (\hat{e} (p, q) \hat{} c), K^{↑} (r)] - [] \to K^{↓ d} (\hat{e} (p, q) \hat{} s)$ , an edge $(i, 1) ↣ (j, 1)$ , $nifactors (t i) \subseteq_{{AC}^{'}} nifactors (r)$ for $i = 1$ or $i = 2$ , and $\hat{e} (p, q)$ does not contain any fresh names.

There is no node $[K^{↓ d} ([a] p), K^{↓ d} ([b] q)] - [] \to K^{↓ d} (\hat{e} (p, q) \hat{} (a * b))$ such that the send-nodes of the first and second premises are labeled with $r u_{1}$ and $r u_{2}$ and $fsyms (r u_{2}) <_{f s} fsyms (r u_{1})$ where $<_{f s}$ is a total order on sequences of fact symbols.

There is no chain of nodes repeatedly instantiating a rule of the form $K^{↓} (l |_{p}), K^{↑} (t_{1}), \dots, K^{↑} (t_{i}) - - [] \to K^{↓} (r)$ of length at least equal to the number of subterms of $l |_{p}$ , if $l |_{p}$ and r are unifiable.

Most of the conditions avoid redundancy and enforce that all terms are in normal form (N1). N2 and N6 are for the bilinear pairing theory $DH$ , N7 to N11 are for $BP$ . N3 avoids multiple deduction of the same term. N4 forbids deduction by coerce rule on invertible function symbols that instead must be created by construction. N5 enforces the ordering of $K_{}^{↓}$ before $K_{}^{↑}$ facts. N12 limits the length of derivation chains for certain rules to the maximum required number. We do not detail these conditions and their notations here as they are orthogonal to our work. For detailed explanations of these normal form conditions and the notations, see [34,54,55].

The existing normal form conditions are however insufficient to handle XOR, as illustrated by the following example.

Example 4.
Tamarin uses backwards constraint-solving to find normal dependency graphs representing the protocol executions. Suppose that during the constraint solving the adversary needs to compute a term $a \oplus b$ , or more precisely Tamarin encounters an unsolved $K^{↓} (a \oplus b)$ premise. Then Tamarin will check all possible ways for the adversary to compute this term: The premise can either be the result of a protocol output, or the result of a deconstruction rule for XOR. In the latter case, $K^{↓} (a \oplus b)$ can, for example, be the conclusion of a rule instance with premises $K^{↓} (a \oplus c)$ and $K^{↑} (c \oplus b)$ . Tamarin will then try to resolve the new premises, and again $K^{↓} (a \oplus c)$ can be the conclusion of a deconstruction rule with premises $K^{↓} (a \oplus d)$ and $K^{↑} (d \oplus c)$ , and so on, resulting in non-termination. This is illustrated in Fig. 5. Note that this is not prevented by any of the previous normal form conditions, as they are focused on handling the previous equational theories.

Fig. 5.
Example 4: infinite chain of deconstruction rules.

Such loops would occur in many cases when analyzing even simple protocols containing XOR. To prevent them, we introduce a new normal form condition, N13, which enforces that there is no chain of applications of XOR deconstruction rules.
Definition 3 (N13).

There is no chain of repeated instantiations of the deconstruction rules for XOR.

Intuitively, this does not limit the deducible terms for the adversary, as one can always cancel out all terms in a single step (i.e., using one deconstruction rule). This is formally stated and proven below.

Definition 4.
A normal dependency graph for a set of protocol rules P is a dependency graph $dg$ such that $dg \in dgraphs ({⌈ P ⌉}^{ALL} \cup ND)$ and the conditions N1–N13 are satisfied. We denote the set of all pre-normal dependency graphs (resp. normal dependency graphs) for P by $pdgraphs (P)$ (resp. $ndgraphs (P)$ ).

Let $\overline{tr}$ denote the subsequence, called observable trace, of all actions in a trace $tr$ that are not equal to ∅. We can now prove the main correctness theorem which states that the observable traces of the protocol are identical with the observable traces of the normal dependency graphs. This is sufficient to show soundness and completeness, as Tamarin generates all possible normal dependency graphs using constraint solving.
Theorem 1.
For all sets P of protocol rules, $\begin{matrix} \overline{trace (execs (P \cup MD))} ↓_{ALL} =_{{AC}^{'}} \overline{trace (ndgraphs (P))} . \end{matrix}$

Note that by relying on the observable trace we hide the adversary’s deduction steps on both sides (which differ slightly due to the normalized deduction), but ensure that security properties (defined on actions) are carried over correctly. This theorem shows that by ordering the $K$ -facts the adversary does not lose any power, and that we can simplify the deduction using the finite variant property. The proof, given below, is an extension of the proof of Theorem 1 in [34], where we need to add additional cases for the XOR rules. Normal form condition N13 can be ensured because of the boundedness property of XOR, which allows reaching any term’s normal form in at most two steps, one to cancel all duplicate terms, and another to cancel a possibly remaining single 0 if needed (in our deconstruction rules the latter case also corresponds to a single rule application).
3.1.1. Proof of Theorem 1 for XOR

To formally express the proof, we define some sets of messages, denoting notions of adversary knowledge over a dependency graph.

Definition 5.
We define the $known$ messages of a dependency graph $dg$ as well as the construction-, deconstruction- and combined-known messages for (pre-)normal dependency graphs $n d g$ : $\begin{matrix} known (dg) & = & {m | exists conclusion K (m) \in dg} \\ {known}^{↑} (n d g) & = & {m | exists conclusion K^{↑} (m) \in n d g} \\ {known}^{↓} (n d g) & = & {m | exists conclusion K^{↓} (m) \in n d g} \\ {known}^{↕} (n d g) & = & {known}^{↑} (n d g) \cup {known}^{↓} (n d g) \end{matrix}$

We define as $stfacts (dg)$ all state conclusion facts of a (pre-)normal dependency graph except for adversary knowledge facts $K, K_{}^{↑}, K_{}^{↓}$ . We define as the created messages $created (dg)$ all the fresh values that appear under $Fr$ facts in a (pre-)normal dependency graph.

Finally, we say that a (pre-)normal dependency graph $n d g^{'} = (I^{'}, D^{'})$ is a deduction extension of $n d g = (I, D)$ if I is a prefix of $I^{'}$ , $D \subseteq D^{'}$ , $trace (n d g) = trace (n d g^{'})$ , $stfacts (n d g) = stfacts (n d g^{'})$ , and $created (n d g) = created (n d g^{'})$ .

Note that if $t \in {known}^{↕} (n d g)$ , then there exists a deduction extension $n d g^{'}$ of $n d g$ such that $t \in {known}^{↑} (n d g^{'})$ using an instance of the $C OERCE$ rule if necessary.
Definition 6 (Factors).

We define the factors of a term t as follows: $\begin{matrix} factors (t) = \{\begin{matrix} {t_{1}, \dots, t_{n}} & if t =_{{AC}^{'}} t_{1} \oplus \dots \oplus t_{n} \\ \emptyset & otherwise \end{matrix} \end{matrix}$

Note that, ⊕ is a binary function symbol and ${AC}^{'}$ only modifies the order of the arguments of XOR, but never removes an argument. Therefore, $factors (t)$ is never a singleton set.

We can now show an intermediate lemma required for the proof of the correctness theorem, Theorem 1. The lemma simply states that if two terms are known by the adversary, he can also compute XOR of both terms while complying with all normal form conditions except N13 which will be treated directly in the proof of Theorem 1.

Lemma 3.
For all pre-normal dependency graphs $n d g$ with $t_{1} \in_{AC’} {known}^{↕} (n d g)$ and $t_{2} \in_{AC’} {known}^{↕} (n d g)$ there exists a deduction extension $n d g^{'}$ of $n d g$ such that $(t_{1} \oplus t_{2} ↓_{ALL}) \in_{{AC}^{'}} {known}^{↕} (n d g^{'})$ .
Proof.
If $(t_{1} \oplus t_{2} ↓_{ALL}) \in_{AC’} {known}^{↕} (n d g)$ then we trivially conclude with $n d g^{'} = n d g$ . In the following, we thus assume that $(t_{1} \oplus t_{2} ↓_{ALL}) \notin_{AC’} {known}^{↕} (n d g^{'})$ .

If $t_{1} =_{{AC}^{'}} t_{2}$ , then $t_{1} \oplus t_{2} ↓_{ALL} 0$ , and we extend $n d g$ with an instance of the constructor rule for 0. We now assume that $t_{1} \neq_{{AC}^{'}} t_{2}$ .

Let $f_{i} = factors (t_{i})$ and $n_{i} = | f_{i} |$ for $1 ⩽ i ⩽ 2$ . We proceed by induction on $k = n_{1} + n_{2}$ .

Base case. If $k = 0$ , then we have $n_{1} = n_{2} = 0$ , i.e., $f_{1} = f_{2} = \emptyset$ . Therefore, the facts $K^{x} (t_{1})$ and $K^{y} (t_{2})$ given by hypothesis were not conclusions of some variant of a XOR rule instance. We also have that $t_{1} \oplus t_{2} ↓_{ALL} =_{{AC}^{'}} t_{1} \oplus t_{2}$ . Indeed, $t_{1}$ and $t_{2}$ are different values in normal forms, have no ⊕ at top level and other symbols do not interact with XOR (⊕ neither appears in DHBPM nor in ACC). Potentially using some Coerce rules (depending on x and y), we can extend $n d g$ to produce facts $K^{↑} (t_{1})$ and $K^{↑} (t_{2})$ . We extend again the graph with an instance of the constructor rule for ⊕ with $K^{↑} (t_{1})$ and $K^{↑} (t_{2})$ as premises and $K^{↑} (t_{1} \oplus t_{2})$ as conclusion. All normal form conditions are satisfied. Note that N3 holds by assumption (i.e., $(t_{1} \oplus t_{2} ↓_{ALL}) \notin_{{AC}^{'}} {known}^{↕} (n d g^{'})$ ) and N5 holds because $n d g$ does not violate it.

Inductive case. Otherwise, $k > 0$ . There must be some i such that $n_{i} ⩾ 2$ . We suppose w.l.o.g. $n_{1} ⩾ n_{2}$ , hence $n_{1} ⩾ 2$ and $f_{1} \neq \emptyset$ .
If $f_{1} \cap f_{2} = \emptyset$ then $t_{1} \oplus t_{2} ↓_{ALL} =_{{AC}^{'}} t_{1} \oplus t_{2}$ (since $t_{1}$ and $t_{2}$ are normal forms). We extend $n d g$ with an instance of the constructor rule for ⊕ with $K^{↑} (t_{1})$ and $K^{↑} (t_{2})$ as premises and $K^{↑} (t_{1} \oplus t_{2})$ as conclusion. We assume in the following that $f_{1} \cap f_{2} \neq \emptyset$ . Note that $f_{1} ⊈ f_{2}$ since $f_{1} \neq f_{2}$ and $n_{1} ⩾ n_{2}$ .

If $f_{2} ⊈ f_{1}$ .

If $t_{1} \in_{{AC}^{'}} {known}^{↓} (n d g)$ , we can use an instance of the second deconstruction rule with $K^{↓} (t_{1})$ and $K^{↑} (t_{2})$ as premises and $K^{↓} (t_{1} \oplus t_{2} ↓_{ALL})$ as conclusion. In case $t_{2} \notin_{AC’} {known}^{↑} (n d g)$ , then $t_{2} \in_{{AC}^{'}} {known}^{↓} (n d g)$ and one can use a Coerce rule to add $K^{↑} (t_{2})$ to the graph.

If $t_{2} \in_{{AC}^{'}} {known}^{↓} (n d g)$ , we can use an instance of the second deconstruction rule with $K^{↓} (t_{2})$ and $K^{↑} (t_{1})$ as premises and $K^{↓} (t_{1} \oplus t_{2} ↓_{ALL})$ as conclusion. In case $t_{1} \notin_{AC’} {known}^{↑} (n d g)$ , then $t_{1} \in_{{AC}^{'}} {known}^{↓} (n d g)$ and one can use a Coerce rule to add $K^{↑} (t_{1})$ to the graph.

Otherwise, it holds that $t_{1} \notin_{{AC}^{'}} {known}^{↓} (n d g)$ and $t_{2} \notin_{{AC}^{'}} {known}^{↓} (n d g)$ . Therefore, we have $t_{1} \in_{{AC}^{'}} {known}^{↑} (n d g)$ and $t_{2} \in_{{AC}^{'}} {known}^{↑} (n d g)$ , and both $t_{1}$ and $t_{2}$ must be the conclusion of a constructor rule instance. Let $r_{1}$ and $r_{2}$ be the premises of the constructor rule instance for $t_{1}$ , and $s_{1}$ and $s_{2}$ be the premises of the constructor rule instance for $t_{2}$ , then we have that $factors (r_{1}) \cap factors (r_{2}) = \emptyset$ and $factors (s_{1}) \cap factors (s_{2}) = \emptyset$ . Indeed, otherwise, the application of the constructor on $r_{1}$ and $r_{2}$ (or $s_{1}$ and $s_{2}$ , respectively) would not be a valid normal form instantiation of the constructor rule (i.e., $r_{1} \oplus r_{2}$ or $s_{1} \oplus s_{2}$ , respectively, would not be $↓_{ALL}$ -normal). As $f_{1} \cap f_{2} \neq \emptyset$ , there exists i and j such that $factors (r_{i}) \cap factors (s_{j}) \neq \emptyset$ . By the induction hypothesis there exists a deduction extension $n d g^{'}$ such that $r_{i} \oplus s_{j} \in_{{AC}^{'}} {known}^{↕} (n d g^{'})$ . We have that $| factors (r_{i} \oplus s_{j}) | ⩽ | factors (r_{i}) | + | factors (s_{j}) | - 1$ , hence by applying the inductive hypothesis with $r_{3 - i}$ and then with $s_{3 - j}$ , we obtain a deduction extension $n d g^{″}$ of $n d g^{'}$ such that $r_{1} \oplus r_{2} \oplus s_{1} \oplus s_{2} =_{E_{ALL}} t_{1} \oplus t_{2} \in_{{AC}^{'}} {known}^{↕} (n d g^{″})$ .

If $f_{2} \subseteq f_{1}$ .

If $t_{1} \in_{{AC}^{'}} {known}^{↓} (n d g)$ , we can use an instance of the first deconstruction rule with $K^{↓} (t_{1})$ and $K^{↑} (t_{2})$ as premises and $K^{↓} (t_{1} \oplus t_{2} ↓_{ALL})$ as conclusion. In case $t_{2} \notin_{AC’} {known}^{↑} (n d g)$ , then $t_{2} \in_{{AC}^{'}} {known}^{↓} (n d g)$ and one can use a Coerce rule to add $K^{↑} (t_{2})$ to the graph.

If $t_{1} \notin_{{AC}^{'}} {known}^{↓} (n d g)$ , then $t_{1}$ must be the result of a constructor rule. Let $s_{1}$ and $s_{2}$ be the premises of this constructor rule. It holds that $factors (s_{1}) \cap factors (s_{2}) = \emptyset$ . Indeed, otherwise, the application of the constructor would not be a valid normal form instantiation of the constructor rule (i.e., $s_{1} \oplus s_{2}$ would not be $↓_{ALL}$ -normal). Since $f_{1} \cap f_{2} \neq \emptyset$ , there exists i such that $factors (s_{i}) \cap factors (t_{2}) \neq \emptyset$ . By induction hypothesis, there exists a deduction extension $n d g^{'}$ such that $s_{i} \oplus t_{2} \in_{E_{ALL}} {known}^{↕} (n d g^{'})$ . We have that $| factors (s_{i} \oplus t_{2}) | ⩽ n_{2} + | factors (s_{i}) | - 1$ , hence there exists a deduction extension $n d g^{″}$ of $n d g^{'}$ such that $s_{3 - i} \oplus s_{i} \oplus t_{2} =_{E_{ALL}} t_{1} \oplus t_{2} \in_{{AC}^{'}} {known}^{↕} (n d g^{″})$ .
□

We can now prove Theorem 1 by adapting the proof we find in [34]. The proof considers a dependency graph on which we add a rule instance and see if it is convertible into a possible rule instance from $ginst ({⌈ P \cup ND ⌉}_{insts}^{ALL} \cup {Fresh})$ to complete an equivalent normal dependency graph.
Proof of Theorem 1.
Relying on Lemmas 1, 2, 3 we shall prove that $\begin{array}{l} \overline{trace ({dg ∣ dg \in {dgraphs}_{{AC}^{'}} ({⌈ P \cup M D ⌉}^{E_{ALL}}) \land dg ↓_{ALL} -normal})} =_{{AC}^{'}} \overline{trace (ndgraphs (P))} \end{array}$ We prove both inclusions of the above by structural induction on (pre-) normal dependency graphs. Most cases can be treated as in [34].

$\subseteq_{{AC}^{'}}$ : We prove that, for all $dg \in {dgraphs}_{{AC}^{'}} ({⌈ P \cup MD ⌉}_{insts}^{ALL})$ with $dg ↓_{ALL} -normal$ , there is $n d g \in ndgraphs (P)$ such that: $\begin{array}{l} (1) & known (dg) & \subseteq_{{AC}^{'}} {known}^{↕} (n d g) \\ (2) & stfacts (dg) & \subseteq_{{AC}^{'}} stfacts (n d g) \\ (3) & created (dg) & =_{{AC}^{'}} created (n d g) \\ (4) & \overline{trace (dg)} & =_{{AC}^{'}} \overline{trace (n d g)} \end{array}$ Notice that the inclusion of (2) applies to multisets.

The four properties hold for $dg = ([], \emptyset)$ . Let $dg = (I, D) \in {dgraphs}_{{AC}^{'}} ({⌈ P \cup MD ⌉}_{insts}^{ALL})$ with $dg ↓_{ALL} -normal$ , and $n d g = (\tilde{I}, \tilde{D}) \in ndgraphs (P)$ such that (1)–(4) hold. Let $r i \in {ginst}_{{AC}^{'}} ({⌈ P \cup MD ⌉}_{insts}^{ALL} \cup {Fresh})$ such that ${dg}^{'} = (I \cdot r i, D ⨄ D^{'}) \in {dgraphs}_{{AC}^{'}} ({⌈ P \cup MD ⌉}_{insts}^{ALL})$ . We must show that there is a deduction extension $n d g^{'}$ of $n d g$ that satisfies (1)–(4) with respect to ${dg}^{'}$ .

We perform a case distinction on $r i$ :
for $r i \in {ginst}_{{AC}^{'}} ({⌈ P ⌉}_{insts}^{ALL} \cup {Fresh})$ , we can extend $n d g$ to $n d g^{'} = (\tilde{I} \cdot r i, \tilde{D} ⨄ {\tilde{D}}^{'})$ in accordance with conditions (2) and (3),

for $r i \in {Out (m) - [] \to K (m), K (m) - [K (m)] \to In (m), Fr (n) - [] \to K (n), - [] \to K (c)} \subset {ginst}_{ACC} ({⌈ MD ⌉}_{insts}^{R_{C S T^{'}}}$ , there are corresponding rules in $ND$ that can complete $\tilde{I}$ ,

for all variants of the XOR rule we can apply Lemma 3. In case the dependency graph violates N13, we have two consecutive instances of XOR deconstruction rules, which we can replace with one instance, as illustrated in Fig. 6. By Lemma 3, there exists a deduction extension to obtain $K^{↑} (t_{2} \oplus t_{4} ↓_{ALL})$ . Note that although the application of Lemma 3 can again introduce new instances that violate N13, we can apply the same technique again, which will terminate as there is only a finite number of known terms, and the application of the lemma does not duplicate terms.

Other rules only deal with the bilinear-pairing, Diffie–Hellman or user-defined theory, and the addition of XOR does not interfere with the original proof.

Fig. 6.
Merging multiple deconstruction rule instances.

$\supseteq_{{AC}^{'}}$ : For the other inclusion, we show, by an analogous way, that for all $n d g \in ndgraphs (P)$ , there is a $dg \in {dgraphs}_{{AC}^{'}} ({⌈ P \cup MD ⌉}_{insts}^{ALL})$ with $dg ↓_{ALL} -normal$ , such that: $\begin{array}{l} (1) & known (n d g) & \subseteq_{{AC}^{'}} {known}^{↕} (dg) \\ (2) & stfacts (n d g) & \subseteq_{{AC}^{'}} stfacts (dg) \\ (3) & created (n d g) & =_{{AC}^{'}} created (dg) \\ (4) & \overline{trace (n d g)} & =_{{AC}^{'}} \overline{trace (dg)} \end{array}$ It holds for $n d g = ([], \emptyset)$ . Let $n d g = (I, D) \in ndgraphs (P)$ , and $dg = (\tilde{I}, \tilde{D}) \in {dgraphs}_{{AC}^{'}} ({⌈ P \cup MD ⌉}_{insts}^{ALL})$ with $dg ↓_{ALL} -normal$ such that (1)–(4) hold. Let $r i \in {ginst}_{{AC}^{'}} ({⌈ P ⌉}_{insts}^{ALL} \cup ND \cup {Fresh})$ such that $n d g^{'} = (I \cdot r i, D ⨄ D^{'}) \in {ndgraphs}_{AC’} (P)$ . We must show that there is a deduction extension ${dg}^{'}$ of $dg$ that satisfies (1)–(4) with respect to $n d g^{'}$ . Note that there is no normal dependency graph violating N13 by definition, so no special care needs to be taken for that restriction in this direction. We still perform a case distinction on $r i$
for $r i \in {ginst}_{{AC}^{'}} ({⌈ P ⌉}_{insts}^{ALL} \cup {Fresh})$ : analogous to the other inclusion,

for $r i \in {ginst}_{{AC}^{'}} (ND)$ : there is a corresponding rule in ${⌈ MD ⌉}_{insts}^{ALL}$ for all variants of XOR rule instances $r i$ . For the others rules, we proceed as in the original proof.
□

We also show that our new constraint solving rule to ensure N13 is correct, and that N13 is sound and complete in equivalence mode using a similar argument.
3.1.2. Modified constraint-solving rules

We only added one constraint-solving rule that implements N13, as shown in Fig. 7. The proof of soundness and completeness of the constraint solving is then a straightforward extension of the proofs of [13, Lemma 6] and [49, Theorem 2]: It is easy to see that this rule does not create any new solutions, and it only removes solutions violating N13 as we only remove systems containing two chained instances of deconstruction rules for XOR.

Fig. 7.

New constraint-reduction rule. $Γ ⇝_{P} ⊥$ denotes that the constraint system Γ can be reduced to ⊥ (bottom); i and j define two rule instances $r i$ and $r i^{'}$ in the dependency graph; and $(i, 1) ⇢_{} (j, 1)$ denotes an edge in the graph between rule instances i and j.

3.2. Adversary model for equivalence properties

Tamarin verifies dependency graph equivalence, that is similar to diff-equivalence in ProVerif [18]. This notion requires that for any dependency graph in one protocol there is a corresponding (“mirrored”) dependency graph in the other protocol [13].

In doing so, Tamarin enforces a strict one-to-one mapping of rules: an instance of a rule can only be simulated using an instance of the same rule, modulo the equational theory. For protocol rules, this means that Tamarin allows one variant of a rule (modulo the equational theory) to be mirrored using a different variant of the same rule. For adversary rules, Tamarin is more conservative: a deconstruction rule instance can only be simulated by another deconstruction rule instance, and not by construction rule instances, although they are technically variants of the same function application rule. This is usually desired: e.g., in the case of signatures, an instance of the deconstruction rule for the signature verification function corresponds to a successfully verified signature. If a signature can be successfully verified in one protocol, then this must also be the case in the other protocol, otherwise there is no observational equivalence.

However, in the case of XOR, this mapping is too strict, as an adversary cannot know whether an application of XOR actually canceled out some terms or not. Consider the following toy protocol with only one rule that illustrates the problem: $\begin{matrix} Pr : Fr (r) - - [] \to Out (diff [r \oplus c, r \oplus d]) \end{matrix}$ where c and d are constant functions in the signature. The left and right instances of the bi-system should obviously be equivalent, as the adversary does not know the fresh value r (similar to a one-time pad encryption).

Fig. 8.

Dependency graph for an instance of the example protocol and its mirror.

Consider now the dependency graphs given in Fig. 8. The dependency graph on the left hand side corresponds to a protocol execution of the left bi-system. If we use Tamarin’s usual mirroring, this graph has no mirror, since in the right execution the rule at the bottom is not a valid instance of any deconstruction rule for XOR (cf. definition of ${ND}_{XOR}$ ), and Tamarin would thus claim an attack. However, the last rule still corresponds to an application of XOR, so the adversary should not see any difference, as long as he cannot distinguish the resulting terms.

To prevent these spurious attacks, we modified Tamarin to treat the XOR rules just like normal protocol rules, i.e., when mirroring an instance of an XOR construction or deconstruction rule, any instance corresponding to an application of the XOR operator is accepted (even if this does not strictly correspond to a standard construction or deconstruction rule as the ↑ and ↓ might be different), so long as it uses the same input and all other constraints still hold. Hence the dependency graph on the right of Fig. 8 is considered a valid mirror.

Note that Tamarin still verifies that all equalities from one side carry over to the other side, and vice versa. In particular, if we modify the protocol to also output the random value r, Tamarin reports an attack: the adversary can cancel out r, and compare the result with the public constants c or d.

3.2.1. Proof of soundness of equivalence mode for XOR

In [13] it is shown that dependency graph equivalence (Tamarin’s version of diff-equivalence) is a sound, but incomplete approximation of observational equivalence for multiset rewriting rules [13, Theorem 1]. This proof holds for any set of protocol and adversary rules, and thus also applies in our case. Then, in a second step, in the appendix of [13] it is shown that it is sufficient to consider only normalized graphs when checking for dependency graph equivalence [13, Theorem 3]. This result carries over to our case, there is only a syntactic change from $AC$ to ${AC}^{'}$ as we need to include XOR in the set of $AC$ symbols, but this does not change the rest of the proof.

We then only need to show soundness and completeness of our new normal form condition N13, i.e., to show that a bi-system is dependency graph equivalent if, and only if, it is dependency graph equivalent when only considering graphs respecting N13.

Theorem 2 (Soundness and Completeness of N13 w.r.t. Dependency Graph Equivalence).

Let S be a ∗-restricted protocol bi-system. S is dependency graph equivalent if, and only if, it is dependency graph equivalent when only considering graphs respecting N13.

Proof.
One direction (⇒) is trivial: each graph ensuring N13 is a valid graph, hence by assumption there is a valid mirror that also ensures N13 as this property is preserved by mirroring.

For the other direction (⇐), we need to show that even graphs that violate N13 have valid mirrors, assuming that all graphs ensuring N13 have a valid mirror.

Assume that there is a dependency graph $dg$ that does violate N13. Using the same approach as in the proof of Theorem 1 illustrated in Fig. 6, based on Lemma 3, we can turn $dg$ into a graph ${dg}^{'}$ that ensures N13.

By assumption there are the necessary valid mirrors for ${dg}^{'}$ . We then need to show that there are also the necessary valid mirrors for $dg$ . The only difference between $dg$ and ${dg}^{'}$ is part of the adversary deduction, where the adversary applied XOR deconstruction or construction rules. One can see the modifications as computing the same result, but applying the XOR operations on the terms in a different order. Because XOR is associative and commutative, the result remains the same. We can thus “undo” the modifications on the mirrors of ${dg}^{'}$ , i.e., compute the result as in $dg$ and not as in ${dg}^{'}$ , and obtain valid mirrors for $dg$ . This is possible in particular as we relaxed the mirroring to allow deconstruction rules to be mirrored using construction rules, and vice versa. □

4. Case studies

We first present a simple challenge-response protocol for illustration purposes (Section 4.1). We then present our first big case study LAK’06 [45], introduce security properties, and summarize our analysis results (Section 4.2). We present additional stateful RFID protocols in Sections 4.4, 4.5. We furthermore present our results on other non-stateful RFID protocols (Sections 4.3, 4.6), an eCash protocol (Section 4.7), and a version of the Needham–Schroeder–Lowe public key protocol with XOR (Section 4.8) after that. All RFID protocol case studies are taken from [63]. All our Tamarin models are freely available at [56]. Tamarin versions v1.4.0 and later contain the presented XOR extension. We present an overview of the results in Tables 1 and 2 in Section 4.9.

4.1. Introductory $CR \oplus$ example

We start with a toy example protocol to illustrate that a faithful model of XOR with support for AC and cancellation is necessary, as otherwise attacks can be missed. (Note that the attack we find on this example with Tamarin is the basis of an attack on the real LAK’06 case study that follows.) Consider the following basic challenge response protocol called CR:

	$A :$	knows $(k)$
	$B :$	knows $(k)$
	$A :$	fresh $(n a)$
CR1.	$A \to B :$	$n a$
CR2.	$B \to A :$	$⟨ h (n a, k, n b), n b ⟩$

Tamarin automatically proves both aliveness and recent-aliveness of the responder B, which is the protocol’s goal.

Consider now an extension of CR that uses ⊕, called

CR \oplus

	$A :$	knows $(k)$
	$B :$	knows $(k)$
	$A :$	fresh $(n a)$
CRx1.	$A \to B :$	$n a$
CRx2.	$B \to A :$	$⟨ h (n a \oplus k \oplus n b), n b ⟩$

Our model for this protocol is bounded to two agents, and Tamarin automatically proves aliveness of the responder B, but finds an attack on recent-aliveness, also automatically. Note that this attack is expected as an attacker can craft a correct response after having observed one real response. This attack uses the same hash value as the legitimate previous run,

h (n a \oplus k \oplus n b)

, but the attacker chooses the nonce

n b^{'} : = n a \oplus n b \oplus n a^{'}

where

n a

and

n b

are the values from the original run, and

n a^{'}

is the new challenge. This works because

n a^{'} \oplus k \oplus n b^{'} = n a^{'} \oplus k \oplus n a \oplus n b \oplus n a^{'} = k \oplus n a \oplus n b = n a \oplus k \oplus n b

and thus A accepts the old hash, as it expects

h (n a^{'} \oplus k \oplus n b^{'})

. This attack heavily relies on the cancellation property of XOR as seen in the above equality, where the duplicate

n a^{'}

is removed. Additionally, it also requires proper support for the AC property of the ⊕-operator. Without AC, one would have to define specific cancellation equations, e.g.,

X \oplus (Y \oplus (X \oplus Z)) = Y \oplus Z

, pick

n b^{'}

more carefully as

n b^{'} : = n a^{'} \oplus (n a \oplus n b)

and as result would then have

n a^{'} \oplus (k \oplus n b^{'}) = n a^{'} \oplus (k \oplus (n a^{'} \oplus (n a \oplus n b)) = k \oplus (n a \oplus n b)

which at least contains the same values, but still not in the same order.

4.2. LAK’06

Protocol description. LAK’06 [45] is an RFID protocol that aims at mutual authentication of a tag and reader while providing untraceability for the tag. In order to achieve untraceability, the protocol relies on a challenge-response mechanism based on a shared secret that is modified at the end of each session. We suppose that initially each tag has its own key k and the reader maintains a database containing those keys. To prevent desynchronization of the state k, the reader also stores the last successful key $k_{0}$ associated with each tag. Initially, $k^{init} = h (k_{0}^{init})$ where $h (\cdot)$ is some hash function. An Alice&Bob description of the protocol is depicted in Fig. 9(a).

The reader starts by challenging the tag (1.) with a fresh random $r_{0}$ , and the tag’s expected reply (2.) both (i) proves the knowledge of the secret k bound to the fresh value $r_{0}$ and (ii) challenges back the reader. Upon receiving that message, the reader is assured that the current key stored in the tag is k and thus updates its secrets: $k_{0}$ becomes the current key and k becomes the next key to be used: $h (k)$ . It then replies to the tag’s challenge proving it also knows the secret key k. When receiving that reply, the tag updates its key to $h (k)$ .

When all messages reach their recipients, tag and reader stay synchronized, storing the same key $k = h^{i} (k^{init})$ where i is the number of successful sessions (the reader additionally stores $k_{0} = h^{i - 1} (k^{init})$ ). However, if message 3. is lost or intercepted, the tag does not update while the reader has already done so. In that situation, the tag stores k and the reader stores $h (k)$ (as well as $k_{0} = k$ ). In order to recover from such desynchronized states, LAK’06 allows the reader to accept the tag’s replies based on the old key $k_{0}$ . This mechanism is depicted in Fig. 9(b) (reader accepts incoming message of the form 2′.). Note that the reader does not update keys in order to re-synchronize with the tag.

Fig. 9.

Alice&Bob description of LAK’06 [45].

Modeling in Tamarin. LAK’06 is a stateful protocol whose states are non-monotonic (i.e., if some tag stores k at some point, k will be replaced by another value later on). Additionally, we aim at modeling an unbounded number of sessions of the protocol in order to establish strong security guarantees. No tool other than Tamarin can handle both features, and we leverage its new capability of dealing with XOR theories to provide the first faithful modeling of the protocol1

[40] considers a stateless abstraction, [8] only considers a small number of sessions.

and first formal analysis of both reachability and equivalence properties.

Security properties. We are interested in analyzing secrecy, authentication, and untraceability properties.

Reachability properties. First, we would like to prove that, whenever a tag or a reader stores a key, then the attacker never learns the key (in the past or in the future). Formally, such a property is formalized in Tamarin using the formula defined below, where facts $Claim_Secret (a, k)$ are produced for each rule of agent a (some tag or reader) which accesses or stores a key k.

Definition 7.

Secrecy is modeled via the following formula: $\begin{matrix} \forall a t i . Claim_secret (a, t) @ i \Rightarrow \neg (\exists j . K (t) @ j) \end{matrix}$

Next, we define the non-injective agreement [48] property. We assume that the Tamarin model is equipped with facts $Claim_commit (a, b, ⟨ A, B, t ⟩)$ (i.e., an agent a of role A claims it has established agreement on data t with b whose role is B) and $Claim_running (b, a, ⟨ A, B, t ⟩)$ (i.e., an agent b of role B claims it tries to establish agreement on data t with a whose role is A).

Definition 8.

Non-injective agreement on data t of a role A towards a role B is modeled via the following formula: $\begin{matrix} \forall a b t i . Claim_commit (a, b, ⟨ A, B, t ⟩) @ i \Rightarrow (\exists j . Claim_running (b, a, ⟨ A, B, t ⟩) @ j) \end{matrix}$

Behavioral equivalence properties. We are interested in analyzing untraceability which is one of the key requirements of LAK’06. There are various notions of untraceability which have been defined in the symbolic model in various frameworks (see comparisons in [22,23]). We have chosen to analyze three notions of untraceability following three generic constructions: (symbolic) game-based unlinkability [23] (no relation to game-based computational proofs), which we call ${UK}_{1}$ in the rest of the paper, unlinkability as being checked in [8] ( ${UK}_{2}$ ), and strong unlinkability ( ${UK}_{3}$ ) following [40] (itself strengthening [4]). We informally define below those unlinkability properties as behavioral equivalences between two different systems involving tags and readers of different identities. Note that a tag and readers of same identity initially share the same key k, while agents of different identities initially have distinct keys k. We give identities to readers because we consider reader sessions that expect to interact with a tag of a specific identity.

Those constructions are unrelated in general [23], it seems that ${UK}_{3}$ is strictly stronger than the others [41] for realistic classes of protocols. Comparing the three notions is out the scope of this paper but being able to analyze all of them enables us to provide more fine-grained security guarantees.

Definition 9 (

{UK}_{1}

, informal).

${UK}_{1}$ compares two systems organized in two phases:

during the learning phase, the attacker can run one session for two tags and readers of identity ${id}_{1}$ and ${id}_{2}$ (the identity refers to the key a tag and a reader initially share). This phase is identical for the two systems being compared.

during the guessing phase, the attacker can run a tag of identity ${id}_{1}$ (resp. ${id}_{2}$ ) in the first (resp. second) system.

The property holds when the two systems are behaviorally equivalent.

The two phases shall be understood as weak phases [33] (also called stages [18]): no action from the learning phase can be executed once an action from the guessing phase has been executed. Intuitively, if the attacker can distinguish the two systems then he must have a criterion to guess which is the unknown tag in the guessing phase (i.e., ${id}_{1}$ in the first system, ${id}_{2}$ in the second system). Here, the attacker can take advantage of having interacted with tags and readers of identity ${id}_{1}$ and ${id}_{2}$ during the learning phase.

Definition 10 ( ${UK}_{2}$ , informal).

${UK}_{2}$ holds when the two following systems are behaviorally equivalent:

the first system is made of a tag of identity ${id}_{1}$ and a reader of identity either ${id}_{1}$ or ${id}_{2}$ (non-deterministic choice).

the second system is made of a tag of identity ${id}_{2}$ and a reader of identity either ${id}_{1}$ or ${id}_{2}$ (non-deterministic choice).

Additionally, for both systems, we assume that the attacker initially knows one full transcript of a past honest interaction between the tag and the reader of identity

{id}_{1}

Intuitively, if the attacker can distinguish the two systems then he is able to observe a link in the first system between the past transcript (whose identity is ${id}_{1}$ ) with data he can obtain from the tag ${id}_{1}$ while he doesn’t observe such a link in the second system (which has no tag of identity ${id}_{1}$ ).

Definition 11 ( ${UK}_{3}$ , informal).

${UK}_{3}$ holds when the two following systems are behaviorally equivalent:

the first system is made of a tag and a reader sharing the same identity that can perform two sessions each;

the second system is made of two different pairs of tag and reader that can only perform one session each.

The second system corresponds to an ideal scenario where there is nothing to link: no agent can be tracked because each agent plays at most one session. This is not the case for the first scenario where two sessions are considered for one single tag and one single reader. Intuitively, if the attacker cannot distinguish both systems then he has no way to track an agent over two sessions.

Note that for all unlinkability notions, we are considering finitely many agents and sessions only. For the case of strong unlinkability ( ${UK}_{3}$ ), this is due to a known lack of precision of diff-equivalence when it comes to verifying such strong properties [40,41]. Fortunately, for a bounded number of sessions only, one can overcome this limitation in Tamarin using a simplified swapping approach [19]. On the contrary, this is not a theoretical limitation for ${UK}_{1}$ and ${UK}_{2}$ (which is the case for other existing tools that could handle XOR) but rather a pragmatic approach: as proofs are getting highly complex when combining behavioral equivalence, XOR reasoning, and stateful protocols, verification requires either an excessive amount of resources or some manual work. We thus prefer to analyze more case studies but for slightly weaker notions of unlinkability.

Analysis.

Analysis of reachability properties. We model secrecy of stored keys (Definition 7) as well as the two non-injective agreement properties for both sides (Definition 8), for one pair of tag and reader that can play an unbounded number of sessions each.

We devise a dedicated oracle for the LAK’06 protocol to encode superior proof-search choices compared to the default heuristics. Oracles offer a light-weight tactics language to guide the proof search in Tamarin. This was necessary, as the proofs involve inductive reasoning to cope with the stateful nature of the LAK’06 protocol, unbounded number of sessions, and intricate and long message deductions for the equational theory including XOR. The oracle allows us to automatically complete very long and highly technical sub-proofs in order to focus the manual exploration on the high-level proof structure. We can thus semi-automatically prove secrecy of stored keys and non-injective agreement of the tag role towards the reader role and Tamarin automatically finds an attack on non-injective agreement of the reader towards the tag. The attack corresponds to the one described in [63] and works just like the one presented for $CR \oplus$ in Section 4.1.

Analysis of behavioral equivalence properties. We analyze ${UK}_{1}, {UK}_{2}$ , and ${UK}_{3}$ using diff-equivalence verification in Tamarin [13]. However, since we consider those properties for a bounded number of sessions only (1 or 2 sessions), we have not modeled the key update mechanism and used an abstraction where keys are chosen fresh for each session (e.g., as done in [40]). Thanks to those simplifications, we were able to obtain fully automatic proofs as described next.

For ${UK}_{2}$ (see Definition 10) we obtain a fully automatic proof.

We analyze ${UK}_{3}$ for four sessions in total, 2 sessions of tag and 2 sessions of reader (see Definition 11). Tamarin automatically finds an attack. While it was known that the property fails to hold [40], Tamarin finds a slightly different attack. Note that the protocol is claimed to be untraceable in [63] for a weaker notion of unlinkability. Strong unlinkability as being checked here may be considered too strong but [40,41] discuss how a variant of the attack found here constitutes a practical privacy breach.

We are not able to directly analyze ${UK}_{1}$ when taking readers into account during the learning phase. Indeed, for such a model, one needs a restriction2

²
Restrictions can be used in a Tamarin model to restrict considered executions to the ones that satisfy a specific property.

for modeling weak phase, that states that no action from the learning phase can be executed after an action from the guessing phase. Such a restriction is crucial for avoiding obvious false attacks. However, when dealing with both restrictions and diff-equivalence, Tamarin’s analysis frequently does not terminate, which is a known limitation. Therefore, in order to get rid of that restriction, we limit our analysis of weak unlinkability to tags only. For that weak model, Tamarin automatically proves that

{UK}_{1}

holds, without oracle.

4.3. CH’07

Fig. 10.

The CH’07 RFID authentication protocol.

Protocol description. CH’07 [30] was designed to be a challenge-response RFID authentication protocol that provides tag untraceability. We base our model on [63]. Figure 10 shows the protocol description.

The reader R and tag T share secrets k and $ID$ . The reader challenges the tag with a random bit string $r_{1}$ , modeled as a nonce. T generates a nonce $r_{2}$ and replies with a term derived from $h (r_{1} \oplus r_{2} \oplus k)$ , where h is a hash function, and the tag’s identifier $ID$ . The hash and $ID$ are used as input for a function $rot$ in which the bit string $ID$ is rotated by a value depending on the hash. We model $rot$ as a hash function, but note that a better approximation would be provided by the identity function. The term sent from the tag to the reader is the output of the $lh$ function which consists of the first half of its argument bitstring. We model $lh$ as a hash function.

The reader performs the same computation as the tag to identify the tag. If the tag can be identified, the reader replies with the output of the $rh$ function, which is the second half of the bitstring the reader computed. We model $rh$ as a hash function, too.

Analysis of reachability properties. We consider several authentication properties: recent aliveness of tag and reader as in [62,63], and non-injective agreement (Definition 8) of tag and reader, on different data items, namely on $⟨ k, r_{1}, r_{2} ⟩$ and on $k \oplus r_{1} \oplus r_{2}$ .

The protocol does not satisfy recent aliveness of tags, due to an impersonation attack [62,63]. The adversary can impersonate a tag to a reader after one interaction with a tag. We find this attack automatically using our Tamarin model. Recent aliveness of the reader R is satisfied and we find an automatic proof.

Agreement on $⟨ k, r_{1}, r_{2} ⟩$ is not satisfied for either role. In both cases, this is because the adversary can modify both the challenge and the response by an xor with a term x. The adversary’s modifications cancel out and both parties complete their protocol runs, but agreement is not satisfied on the nonces $r_{1}$ and $r_{2}$ . We again find the attacks automatically using Tamarin.

If we require agreement on the data $k \oplus r_{1} \oplus r_{2}$ instead, then both agreement claims are satisfied and Tamarin finds the proof automatically.

Analysis of behavioral equivalence. The protocol satisfies ${UK}_{1}$ and ${UK}_{2}$ (Definitions 9 and 10) and Tamarin finds a proof automatically. The protocol does not satisfy the property ${UK}_{3}$ (Definition 11) because the same reader responds to a replayed query with the same answer when the second time the attacker picks $r_{2}^{'} = r_{1}^{'} \oplus r_{1} \oplus r_{2}$ , similarly to the attack in Section 4.1. This allows the attacker to distinguish the two systems defining the ${UK}_{3}$ property: in the first system, the attacker will receive the same response from the RFID reader in both sessions while in the second system the attacker will receive different responses. Tamarin finds the attack automatically.

The interpretation of the attack is that it allows the adversary to test whether a reader is still accepting a given tag. If tags can expire or be removed from a system, then this attack allows the adversary to learn whether a previously observed tag has expired or whether it is still valid.

4.4. OTYT06

Fig. 11.

The OTYT’06 RFID authentication protocol.

Protocol Description. Similarly to CH’07, the OTYT’06 [50] RFID protocol aims at authenticating tags, which should remain untraceable for an adversary. We base our model on [63], see Fig. 11 for a protocol description.

The reader R and tag T share a secret key k that is supposed to be updated at the end of each session. The reader challenges the tag with $r 1$ . The tag is then supposed to prove a recent knowledge of k by computing and sending $h (k \oplus r 1)$ . The reader correctly authenticates the tag upon reception of this message and then updates the key to a fresh key $k 1$ . In order to let the tag updates its key accordingly, the reader sends $k \oplus k 1$ to the tag, who can then compute $(k \oplus k 1) \oplus k = k 1$ and update her key. The hash function h is modeled as a random oracle, as is standard.

Analysis of reachability properties. We consider several authentication properties: aliveness and recent aliveness of tag, aliveness of reader, non-injective agreement from the reader’s point of view on k and $r 1$ , and desynchronization resistance.

The protocol does satisfy aliveness and recent aliveness of tags [63]. However, the protocol is not desynchronization resistant [60] as tag proceeds with key update without authenticating the request. The tag never checks messages allegedly coming from the reader, hence reader aliveness does not hold either. Furthermore, the reader does not obtain non-injective agreement with the tag on $r 1$ . Indeed, based on a reader’s challenge $r 1$ , the adversary can make the tag update its key to $k \oplus r 1$ by sending $r 1$ as a third message (OTYT3 in Fig. 11) and then, in a new sessions, challenge the tag with 0, to which the tag will respond with $h ((k \oplus r 1) \oplus 0) = h (k \oplus r 1)$ . This message can be forwarded to the reader, who will authenticate the tag with $r 1$ as a challenge, while the tag saw 0 as a challenge. To the best of our knowledge, this attack was not previously reported. Using our Tamarin model, we automatically found this attack on non-injective agreement with the tag as well as the attacks on desynchronization resistance, and on aliveness of the reader. We had to limit the depth of the proof search for finding the desynchronization attack to prevent loops.

Aliveness of the tag was automatically established, as well as recent aliveness of the tag, but only for two sessions. This bound was necessary due to the complexity of such proofs for stateful protocols that fail to provide basic properties such as desynchronization resistance and mutual authentication, thus allowing all sorts of key updates.

Analysis of behavioral equivalence. Mainly due to a lack of reader authentication, tags are traceable. Essentially, the adversary can keep the tags’ (supposedly changing) key static by just sending a 0, leading to a static key and resulting in the same response to the same challenge (which can be adversary chosen as well). For this reason, OTYT’06 fails to satisfy either ${UK}_{1}$ , ${UK}_{2}$ , or ${UK}_{3}$ and Tamarin automatically found an attack for each property. Those attacks were found with respect to a simplified model with two sessions of the tag only, except for ${UK}_{3}$ for which we were able to model an unbounded number of tag sessions. The found attacks are also valid with respect to the full model.

4.5. LD07

Fig. 12.

The LD’07 RFID supply chain protocol.

Protocol description. LD’07 [46] is a protocol proposed for RFID systems in a supply chain setting. The protocol aims at mutual authentication between a tag and an authorized reader. Tags moving through the supply chain should remain untraceable for an adversary that is trying to link a tag before it has reached a supply chain partner’s facility to a tag that has left the supply chain partner’s facility.

A careful inspection shows that this protocol design is similar to and an improvement on the OTYT’06 protocol discussed in Section 4.4, although the protocols have been proposed independently. The LD’07 design improves over OTYT’06 in that tags do not accept a reader challenge equal to 0 in the first message and that the third protocol message contains an authenticator.

We base our model on [63], the protocol is shown in Fig. 12. Each tag is assigned a secret key $k_{0}$ that serves as its identifier and is known to every authorized reader in the supply chain. Tags move through the supply chain partners’ facilities in a given order. Every authorized RFID reader in the supply chain has its own secret access key $k_{i}$ for $i > 0$ and knows the access key $k_{i + 1}$ of the subsequent RFID reader in the supply chain.

The tag stores the term $α : = k_{0} \oplus k_{i}$ while the reader with access key $k_{i}$ is authorized to query and write to the tag. After authenticating a tag with a challenge-response protocol (messages LD1 and LD2 in Fig. 12) the reader rewrites the tag for the subsequent reader by sending $k_{i} \oplus k_{i + 1}$ and a hash value intended as an authenticator for the key update in message LD3a. When the tag receives a key-update message (LD3b), it verifies the key update value by comparing the hash value b to the hash of its stored term α xored with the received key update value a. If the values pass the check, the term α is updated to the value $a \oplus α = k_{0} \oplus k_{i + 1}$ authorizing the subsequent reader.

Analysis of reachability properties. We consider several authentication properties: aliveness and recent aliveness of the tag, recent aliveness of the reader, and non-injective agreement from the reader’s point of view on the tag’s key $k_{0}$ , the reader’s key $k_{i}$ , and the challenge r.

The protocol satisfies aliveness and recent aliveness of tags, but it does not satisfy recent aliveness of the reader [63]. In our model of LD’07, aliveness is automatically proven while the proof of recent aliveness is manually constructed and valid for two protocol sessions.

Moreover, we can show that the reader does not obtain non-injective agreement with the tag on r due to the following attack. The adversary challenges the tag with a nonce r and receives the answer $h (r \oplus α)$ . The adversary can then get the tag to update its key to $α \oplus r$ by sending $r, h (α \oplus r)$ as the third message LD3a. This desynchronizes the tag from its authorized reader. These attack steps have been first described in [61] as part of an extortion attack on supply chain partners. Next, when the reader challenges the tag with a fresh nonce $r^{'}$ , the adversary replaces this challenge with $r \oplus r^{'}$ and forwards it to the tag to which the tag responds with $h (r \oplus r^{'} \oplus α) = h (r^{'} \oplus α)$ . This message will be accepted by the reader which will authenticate the tag with $r^{'}$ as a challenge, while the tag received $r \oplus r^{'}$ as the challenge. Thus non-injective agreement does not hold.

Analysis of behavioral equivalence. LD’07 does not satisfy ${UK}_{1}$ because the tag’s response to a challenge is a function of the tag’s key and the challenge only. This allows the adversary to distinguish between different tags by challenging tags multiple times prior to their key update. We note that the LD’07 protocol was not intended to foil this type of traceability. The designers’ aim for this protocol was that an adversary cannot link the observation of a tag prior to an update to the observation of the same tag after it has been updated. This property is, however, not satisfied either as shown by the attack on the ${UK}_{2}$ .

For our ${UK}_{2}$ model of this protocol we reconstruct the attack described in [61]. The attacker observes one honest run of the tag and reader which ends with a tag update. The information the adversary learns is the challenge nonce r, the hash value $h (r \oplus α)$ and the update message $a : = k_{i} \oplus k_{i + 1}$ . The adversary then challenges a tag with the message $r \oplus a$ . If the tag answers with $h (r \oplus α)$ , the adversary knows to be communicating with the same tag that was observed prior to the update.

While the attack in the ${UK}_{2}$ model also demonstrates a violation of the ${UK}_{3}$ property, we construct a different attack in our ${UK}_{3}$ model where the adversary is allowed to actively interact with the tag. Instead of only observing the first session, the adversary now updates the tag in the same manner as described in the attack on non-injective agreement above. In the second session the adversary updates the tag again with the same key thus cancelling the previously made update. The adversary then challenges the tag as in the ${UK}_{2}$ attack and compares the tag’s answer to the output of the first session.

The ${UK}_{1}$ and ${UK}_{2}$ attacks were found with respect to a simplified model with two sessions of the tag only. The ${UK}_{3}$ attack was found with respect to a simplified model with no limit on the number of tag sessions. All attacks are also valid with respect to the full model.

4.6. KCL’07

KCL’07 [42] is an RFID protocol attempting to both authenticate the tag and to provide untraceability for the tag. It succeeds in providing the recent aliveness property for authentication, but untraceability does not hold. Figure 13 shows the protocol description.

Fig. 13.

The KCL’07 RFID authentication protocol.

Informally, the aliveness property is guaranteed due to the response including the hash of the challenge nonce $r 1$ together with the key k that is only used inside the hash and thus can never be learned by an attacker. Note that the reader cannot learn the value $r 2$ actually chosen by the tag, as a man-in-the-middle attacker can simply pick a random $r 3$ and XOR it to both elements of the pair the tag sends back to the reader. Then, the reader believes $r 2 \oplus r 3$ to be the chosen random value. The reader can only check that the application of XOR to both values results in $ID \oplus h (r 1, k)$ . Therefore, the random value $r 2$ is not relevant.

We thus apply a simplification in our model for the reader, which is that it receives just one term (the XOR of the elements of the pair output by the tag), while the tag sends the pair using $r 2$ . To be precise, the sent term is $⟨ id \oplus r 2, h (r 1, k) \oplus r 2 ⟩$ received as $⟨ idr 2, hashr 2 ⟩$ while in our model the reader simply receives X, interpreted as $idr 2 \oplus hashr 2$ .

The first property expected from this protocol is recent aliveness, which we prove automatically with Tamarin. As explained in Deursen and Radomirović [63] in this protocol the tag is not actually untraceable which can be seen by sending the same nonce twice to a tag, and applying ⊕ to the elements of the response pair, and comparing the results. For the same challenge $r 1$ , the results of applying XOR to the response for a given tag is always $ID \oplus h (r 1, k)$ . No reader is necessary for this attack.

Tamarin automatically finds attacks on ${UK}_{1}$ and ${UK}_{2}$ . For ${UK}_{3}$ , we construct the attack manually using Tamarin.

4.7. Chaum’s offline eCash protocol

Protocol Description. Chaum’s offline eCash [26] is a suite of three protocols that allows for anonymous, untraceable, electronic currencies to be spent offline, i.e., without the need to contact a bank during the payment. The protocols involve three parties, the customer C, the seller S, and the bank B and consist of the withdrawal protocol, where C withdraws eCash from the bank, the payment protocol, where C pays S, and the deposit protocol, where S deposits the received currency with B.

The protocol uses XOR as well as blind signatures, to ensure anonymity. The blind signatures require a non subterm-convergent equational theory, which illustrates that Tamarin is able to handle the combination of these two complex equational theories.

We model a simplified version of these protocols by combining them into one protocol consisting of three (weak) phases comprising withdrawal, payment, and deposit. We focus solely on the mechanism that provides anonymity as long as the customer does not double-spend a coin. We do not model the cut and choose procedure during withdrawal and instead assume that the customer generates well-formed coins.

The simplified protocol aims to provide anonymity to the customer as long as he does not double-spend a coin and is shown in Fig. 14. Messages eCash-1 and eCash-2 model the withdrawal phase, the next two messages model the payment phase, and the remaining messages model the deposit (redemption) phase of the protocol.

Fig. 14.

A simplified model of Chaum’s offline eCash protocol.

Fig. 15.

The simplified model of Chaum’s offline eCash protocol with dishonest seller and bank represented by the adversary-controlled environment E.

Analysis. In our Tamarin model, we consider seller and bank to be corrupted. This leads to a model where the customer interacts with the environment E that is controlled by the adversary and represents both S and B. The model is shown in Fig. 15. We model customer anonymity as secrecy of the customer’s identity C. Tamarin automatically verifies that an honest customer is anonymous and finds an attack on anonymity when the customer double spends.

4.8. NSLPK3xor

This is an insecure variant of the Needham–Schroeder–Lowe [47] (NSL) 3-message public-key protocol. The difference to the classical NSL protocol is the presence of an exclusive-or ⊕ instead of concatenation in message NSLx2. This idea is due to Chevalier et al. [29], and this protocol has previously been analyzed by Sasse et al. [53] using Maude-NPA.

	$A :$	knows $(s k (A), pk (B))$
	$B :$	knows $(s k (B), pk (A))$
	$A :$	fresh $(n a)$
NSLx1.	$A \to B :$	$enc (⟨ n a, A ⟩, pk (B))$
	$B :$	fresh $(n b)$
NSLx2.	$B \to A :$	$enc (⟨ n a, n b \oplus B ⟩, pk (A))$
NSLx3.	$A \to B :$	$enc (n b, pk (B))$

Our Tamarin theory models the case where there is only one key per agent and Tamarin automatically finds attacks on the secrecy of the two nonces as well as on the injective agreement property, as described in detail in [53].

4.9. Summary of experimental results

Table 1
Summary table of results – trace properties. Automation: A = automatic, A (BFS) = automatic with breadth-first search for attacks, O = oracle, O(BFS)-depth 12 = oracle with breadth-first search for attacks and depth bounded to 12, SM = semi-manual, M = manual. “BS” stands for “bounded sessions”. † means the time is for verifying the resulting stored proof. More details in Section 4.9. Properties starting with * are intermediate helping lemmas in the modular proofs

Protocol name Property Modifications Result Automation Runtime

CR-xor aliveness tag ✓ A 0.7s

recent aliveness tag χ A 1.3s

LAK06 helpingSecrecy ✓ A 0.4s

non-injective agreement tag ✓ A 22.0s

non-injective agreement reader χ A 1.3s

LAK06-state helpingUpdateKey ✓ O 21.1s

helpingStackHash ✓ A 19.6s

helpingSecrecy ✓ SM †31.6s

non-injective agreement tag ✓ SM †55.7s

non-injective agreement reader χ A (BFS) 1m38.7s

CH07 recent aliveness tag χ A 2.2s

recent aliveness reader ✓ A 1.1s

non-inj. agree. tag $(k \oplus r 1 \oplus r 2)$ ✓ A 1.1s

non-inj. agree. tag $(k, r 1, r 2)$ χ A 1.3s

non-inj. agree. reader $(k \oplus r 1 \oplus r 2)$ ✓ A 1.0s

non-inj. agree. reader $(k, r 1, r 2)$ χ A 1.1s

OTYT06 helping ✓ O 2m39.4s

aliveness tag ✓ A 0.7s

recent aliveness tag BS ✓ A 70m25.6s

non-injective agreement tag χ A (BFS) 16m39s

aliveness reader χ O 1.1s

desynch resistance χ O (BFS)-depth 12 1m20.1s

LD07 helping ✓ O 19.5s

aliveness tag ✓ A 1.5s

recent aliveness tag BS ✓ M †5m52.4s

non-injective agreement tag χ M †2.2s

recent aliveness reader χ O 3m22.1s

KCL07 recent aliveness tag XORed pair ✓ A 1.7s

Chaum Offline *coins No phases ✓ O 10.4s

anonymity No phases ✓ A 2.8s

anonymity of double spender No phases χ A 12.7s

NSL-xor nonce secrecy χ A 5.1s

injective agreement initiator χ A 1.4s

injective agreement responder χ A 4.0s

Protocol name	Property	Modifications	Result	Automation	Runtime
CR-xor	aliveness tag		✓	A	0.7s
	recent aliveness tag		χ	A	1.3s
LAK06	*helpingSecrecy		✓	A	0.4s
	non-injective agreement tag		✓	A	22.0s
	non-injective agreement reader		χ	A	1.3s
LAK06-state	*helpingUpdateKey		✓	O	21.1s
	*helpingStackHash		✓	A	19.6s
	*helpingSecrecy		✓	SM	†31.6s
	non-injective agreement tag		✓	SM	†55.7s
	non-injective agreement reader		χ	A (BFS)	1m38.7s
CH07	recent aliveness tag		χ	A	2.2s
	recent aliveness reader		✓	A	1.1s
	non-inj. agree. tag $(k \oplus r 1 \oplus r 2)$		✓	A	1.1s
	non-inj. agree. tag $(k, r 1, r 2)$		χ	A	1.3s
	non-inj. agree. reader $(k \oplus r 1 \oplus r 2)$		✓	A	1.0s
	non-inj. agree. reader $(k, r 1, r 2)$		χ	A	1.1s
OTYT06	helping		✓	O	2m39.4s
	aliveness tag		✓	A	0.7s
	recent aliveness tag	BS	✓	A	70m25.6s
	non-injective agreement tag		χ	A (BFS)	16m39s
	aliveness reader		χ	O	1.1s
	desynch resistance		χ	O (BFS)-depth 12	1m20.1s
LD07	helping		✓	O	19.5s
	aliveness tag		✓	A	1.5s
	recent aliveness tag	BS	✓	M	†5m52.4s
	non-injective agreement tag		χ	M	†2.2s
	recent aliveness reader		χ	O	3m22.1s
KCL07	recent aliveness tag	XORed pair	✓	A	1.7s
Chaum Offline	*coins	No phases	✓	O	10.4s
	anonymity	No phases	✓	A	2.8s
	anonymity of double spender	No phases	χ	A	12.7s
NSL-xor	nonce secrecy		χ	A	5.1s
	injective agreement initiator		χ	A	1.4s
	injective agreement responder		χ	A	4.0s

Table 2

Summary table of results – equivalence properties. Automation: A = automatic, A (BFS) = automatic with breadth-first search for attacks, M = manual. “BS” stands for “bounded sessions”. “TO” stands for “tag only”, i.e., no reader was modeled since an attack is already found. “A-EQlhs” means that the automatic proof was started in the subcase rule-equality, then LHS. † means the time is for verifying the resulting stored proof. More details in Section 4.9

Protocol name	Property	Modifications	Result	Automation	Runtime
LAK06	UK1 (tags only)	BS, stateless	✓	A	4m25.4s
	UK2	BS, stateless	✓	A	15m10.4s
	UK3	BS, stateless	χ	A	85m46.1s
CH07	UK1		✓	A	51.5s
	UK2		✓	A	12m16.6s
	UK3		χ	A	3m07.1s
OTYT06	UK1	BS, TO	χ	A-EQlhs	46.2s
	UK2	BS, TO	χ	A	8.1s
	UK3	TO	χ	A	27.7s
LD07	UK1	BS, TO	χ	A	47.2s
	UK2	BS, TO	χ	A	16.2s
	UK3	BS, TO	χ	M	†5s
KCL07	UK1	XORed pair	χ	A (BFS)	126m27.6s
	UK2	XORed pair	χ	A	1m02.6s
	UK3	XORed pair	χ	M	†2.1s

We present in Table 1 (trace properties) and in Table 2 (equivalence properties) a summary of the protocols we analyzed, the result obtained, the runtime required, as well as the level of automation achieved. All experiments are conducted on a server with 2 CPUs of type Intel^® Xeon^® CPU E5-2650 v4 @ 2.20 GHz (with 12 cores each), 256 GB of RAM, running Ubuntu 16.04.3, and we use 10 threads per experiment, running Tamarin v1.4.0.

All our theories are available at [56]. Note that all theories also contain a lemma showing that the protocol is actually executable, avoiding modeling mistakes, all of which are verified, but not listed in the table. We list what modifications we made on each case study, or other modeling limitations, in the Modifications column. Then we give the result, either ✓(the property is verified) or χ (the property does not hold – there is an attack).

For the automation level we show A for automated proofs or attacks, meaning using the standard heuristic and proof tree exploration. We show A (BFS) if the standard heuristic was used to find attacks, but using a breadth-first search of the proof tree (this is a common technique in Tamarin, as BFS is often quicker at finding attacks, but not for proofs). We write O when an oracle was used to automatically find the results, as described before, which can be combined with BFS. We use SM for a semi-manually achieved proof, which means a short human exploration of the state-space was conducted, and then the remainder of the proof is automatic using the oracle. There are cases where we manually constructed an attack or a proof, denoted M. Still, such manually constructed proofs and attacks are all machine-checked.

Note that we considered all RFID protocols from [63] which are in scope (i.e., that do not require further equational properties, such as, e.g., addition and its interaction with XOR), except for YPLRK05 [64]. YPLRK05 turned out to be surprisingly difficult to analyze for various reasons, notably the key update with XOR that is not desynchronization resistant and that leads to a plethora of cases and rule variants. More generally, we observed that analyzing simple but broken protocols such as OTYT06, LD07, CH07, YPLRK05 can be more involved than analyzing more complex protocols that provide strong, mutual authentication and desynchronization resistance properties [15,21], as the different attacks created more possibilities for the intruder to interact with the protocol in complex, unintended ways, which complicates the reasoning for the tool.

Another limit we encountered concerns equivalence properties for stateful protocols. In our examples we only encountered attacks for these protocols, but we conjecture that achieving proofs would be difficult due to the limitations of Tamarin’s equivalence mode.

5. Related work

Computational tools. In the computational model, XOR operations are common and supported by many tools, e.g., EasyCrypt [10] or CryptoVerif [17]. However, computational tools typically have a lesser degree of automation (e.g., EasyCrypt is mainly interactive), or are tailored to specific applications (e.g., [9,11]).

Symbolic tools. In the symbolic model, there are numerous verification tools for cryptographic protocols, some of which support XOR operations, for a bounded or an unbounded number of sessions.

Bounded number of sessions. In the case of a bounded number of sessions, AKiSs [8] and two solvers from the AVISPA [6] suite, Cl-AtSe [58] and OFMC [14], support XOR operations. AKiSs is designed to verify observational equivalence properties, while OFMC and Cl-AtSe are both limited to trace properties. These tools provide weaker guarantees than Tamarin, as they only consider a bounded number of sessions.

Unbounded number of sessions. Scyther [32] is restricted to a fixed set of cryptographic primitives and does not allow XOR operations. Moreover, it neither supports global mutable state nor verification of equivalence properties. The CPSA [39] tool is particularly amenable to the analysis of authentication and secrecy properties. It was used, in combination with the theorem prover PVS, to analyze stateful protocols [51]. However, like Scyther, it neither supports XOR nor the verification of equivalence properties.

ProVerif [20] supports user-defined equational theories, and allows for the verification of a rich variety of security properties. Moreover, the abstractions (based on a translation of applied pi calculus processes into Horn clauses) underlying the theory of ProVerif make it very efficient. However, these abstractions may also cause false attacks, which make the tool unsuitable to analyze stateful protocols. StatVerif [5], an extension of ProVerif, tries to overcome this shortcoming. However, the support for stateful protocols that can be effectively analyzed by StatVerif remains partial. For instance, only a fixed number of state cells may be declared and non-termination arises frequently. Moreover, only secrecy properties can be verified with StatVerif. The recent extension GSVerif [28] improves ProVerif’s handling of stateful protocols. However, the user-defined equational theories ProVerif can handle are insufficient to model XOR, thus GSVerif as well as StatVerif cannot deal with XOR. Another extension of ProVerif developed to support theories including XOR [44] is, however, limited to secrecy and simple authentication properties and also unsuitable for stateful protocols.

Maude-NPA [37] offers support for many equational theories, in particular XOR. Maude-NPA treats algebraic properties, such as associative-commutative operators, in a more generic way than Tamarin, which only offers support for built-in Diffie–Hellman and bilinear pairing theories, as well as multisets, and with the extension presented in this paper XOR operators. However, Maude-NPA does not support global mutable state nor protocols with else branches. Moreover, the verification of equivalence properties suffers from termination problems [52].

The Tamarin front-end SAPiC [43] has been successfully used to analyze stateful protocols given in an applied pi calculus extension. It directly benefits from our work.

Computational soundness. It is well-known that there cannot be a computational soundness proof for symbolic models of XOR [59]. We argue, however, that symbolic analysis including XOR is still useful in itself, not only because symbolic attacks still constitute valid attacks, but also due to the higher degree of automation that this approach provides over the computational approach. It allows for the analysis of complex real-world protocols that are difficult to handle manually, and which are the target of our work.

6. Conclusion

We have extended the Tamarin prover with equational theories including XOR, consequently expanding the class of protocols that can be faithfully modeled and analyzed using automatic verification tools. As Tamarin is sound and complete, we cannot hope for guaranteed termination since the underlying problem is undecidable. However, our new normal form conditions, heuristics, and use of light-weight tactics encoded as oracles allow for a good level of automation as demonstrated by our numerous case studies. These case studies as well as recent work [15,21] using our XOR implementation to analyze mobile network protocols indicate that Tamarin can now be used to tackle large-scale, real-world protocols with XOR.

As future work, an interesting challenge is to lift some of the limitations of equivalence proofs in Tamarin. For example, dealing with the combination of diff-equivalence and restrictions in a more effective way could enable additional case studies, including protocols using weak phases.

Moreover, many of the advanced case studies required manual intervention or specially designed oracles. Finding ways of improving automation in these cases is another direction for future work.

References

3GPP, 3G security; Security architecture, TS, 33.102, 3rd Generation Partnership Project (3GPP), http://www.3gpp.org/DynaReport/33102.htm.

3GPP, System Architecture Evolution (SAE), TR, 33.401, 3rd Generation Partnership Project (3GPP), http://www.3gpp.org/DynaReport/33401.htm.

3GPP, Security Architecture and Procedures for 5G System, TS, 33.501, 3rd Generation Partnership Project (3GPP), http://www.3gpp.org/DynaReport/33501.htm.

Arapinis,

Chothia,

Ritter and

Ryan, Analysing unlinkability and anonymity using the applied Pi calculus, in: Proceedings of the IEEE Computer Security Foundations Symposium, IEEE Comp. Soc. Press, 2010.

Arapinis,

Ritter and

Ryan, StatVerif: Verification of stateful processes, in: Proc. 24th IEEE Computer Security Foundations Symposium (CSF’11), IEEE Press, 2011, pp. 33–47.

Armando,

D.A.

Basin,

Boichut,

Chevalier,

Compagna,

Cuéllar,

P.H.

Drielsma,

P.-C.

Héam,

Kouchnarenko,

Mantovani,

Mödersheim,

von Oheimb,

Rusinowitch,

Santiago,

Turuani,

Viganò and

Vigneron, The AVISPA tool for the automated validation of Internet security protocols and applications, in: CAV, 2005, pp. 281–285.

Armando,

Carbone,

Compagna,

Cuellar and

Tobarra, Formal analysis of SAML 2.0 web browser single sign-on: Breaking the SAML-based single sign-on for Google apps, in: Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering, ACM, 2008, pp. 1–10.

Baelde,

Delaune,

Gazeau and

Kremer, Symbolic verification of privacy-type properties for security protocols with XOR, in: 30th IEEE Computer Security Foundations Symposium, CSF 2017, IEEE Computer Society, 2017, pp. 234–248. ISBN 978-1-5386-3217-8. doi:10.1109/CSF.2017.22.

Barthe,

J.M.

Crespo,

Grégoire,

Kunz,

Lakhnech,

Schmidt and

S.Z.

Béguelin, Fully automated analysis of padding-based encryption in the computational model, in: 2013 ACM SIGSAC Conference on Computer and Communications, Security, CCS’13, Berlin, Germany, November 4–8, 2013,

Sadeghi,

V.D.

Gligor and

Yung, eds, ACM, 2013, pp. 1247–1260. ISBN 978-1-4503-2477-9.

10.

Barthe,

Dupressoir,

Grégoire,

Kunz,

Schmidt and

Strub, EasyCrypt: A tutorial, in: Foundations of Security Analysis and Design VII – FOSAD 2012/2013 Tutorial Lectures,

Aldini,

Lopez and

Martinelli, eds, Lecture Notes in Computer Science, Vol. 8604, Springer, 2013, pp. 146–166. ISBN 978-3-319-10081-4. doi:10.1007/978-3-319-10082-1_6.

11.

Barthe,

Grégoire and

Schmidt, Automated proofs of pairing-based cryptography, in: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, Denver, CO, USA, October 12–6, 2015,

Ray,

Li and

Kruegel, eds, ACM, 2015, pp. 1156–1168. ISBN 978-1-4503-3832-5.

12.

Basin and

Cremers, Know your enemy: Compromising adversaries in protocol analysis, ACM Trans. Inf. Syst. Secur. 17(2) (2014), 7:1–7:31. doi:10.1145/2658996.

13.

Basin,

Dreier and

Sasse, Automated symbolic proofs of observational equivalence, in: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, ACM, 2015, pp. 1144–1155.

14.

Basin,

Mödersheim and

Viganò, OFMC: A symbolic model checker for security protocols, International Journal of Information Security 4(3) (2005), 181–208. doi:10.1007/s10207-004-0055-7.

15.

D.A.

Basin,

Dreier,

Hirschi,

Radomirovic,

Sasse and

Stettler, A formal analysis of 5G authentication, in: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15–19, 2018,

Lie,

Mannan,

Backes and

Wang, eds, ACM, 2018, pp. 1383–1396. ISBN 978-1-4503-5693-0. doi:10.1145/3243734.3243846.

16.

Bhargavan,

A.D.

Lavaud,

Fournet,

Pironti and

P.Y.

Strub, Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS, in: 2014 IEEE Symposium on Security and Privacy, IEEE, 2014, pp. 98–113. doi:10.1109/SP.2014.14.

17.

Blanchet, A computationally sound mechanized prover for security protocols, in: 2006 IEEE Symposium on Security and Privacy (S&P 2006), 21–24 May 2006, IEEE Computer Society, Berkeley, California, USA, 2006, pp. 140–154. ISBN 0-7695-2574-1.

18.

Blanchet,

Abadi and

Fournet, Automated verification of selected equivalences for security protocols, Journal of Logic and Algebraic Programming 75(1) (2008), 3–51. doi:10.1016/j.jlap.2007.06.002.

19.

Blanchet and

Smyth, Automated reasoning for equivalences in the applied pi calculus with barriers, in: Computer Security Foundations Symposium (CSF), 2016 IEEE 29th, IEEE, 2016, pp. 310–324. doi:10.1109/CSF.2016.29.

20.

Blanchet,

Smyth and

Cheval, Automatic Cryptographic Protocol Verifier, User Manual and Tutorial, 2016.

21.

Borgaonkar,

Hirschi,

Park and

Shaik, New privacy threat on 3G, 4G, and upcoming 5G AKA protocols, PoPETs 2019(3) (2019), 108–127.

22.

Brusó, Dissecting unlinkability, PhD thesis, Ph. D. dissertation, Technische Universiteit Eindhoven, 2014.

23.

Brusó,

Chatzikokolakis,

Etalle and

Den Hartog, Linking unlinkability, in: International Symposium on Trustworthy Global Computing, Springer, 2012, pp. 129–144.

24.

Chadha,

Cheval,

Ş.

Ciobâcă and

Kremer, Automated verification of equivalence properties of cryptographic protocols, ACM Trans. Comput. Log. 17(4) (2016), 23:1–23:32. doi:10.1145/2926715.

25.

Chaum, Blind signatures for untraceable payments, in: Advances in Cryptology: Proceedings of CRYPTO ’82, Plenum Press, 1982, pp. 199–203.

26.

Chaum,

Fiat and

Naor, Untraceable electronic cash, in: Advances in Cryptology: Proceedings of CRYPTO ’88, LNCS, Vol. 403, Springer, 1990, pp. 319–327. doi:10.1007/0-387-34799-2_25.

27.

Cheval,

Comon-Lundh and

Delaune, Trace equivalence decision: Negative tests and non-determinism, in: 18th Conference on Computer and Communications Security (CCS’11), ACM, Chicago, Illinois, USA, 2011.

28.

Cheval,

Cortier and

Turuani, A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif, in: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9–12, 2018, 2018, pp. 344–358. doi:10.1109/CSF.2018.00032.

29.

Chevalier,

Küsters,

Rusinowitch and

Turuani, An NP decision procedure for protocol insecurity with XOR, in: LICS, IEEE Computer Society, 2003, pp. 261–270. ISBN 0-7695-1884-2.

30.

H.-Y.

Chien and

C.-W.

Huang, A lightweight RFID protocol using substring, in: Embedded and Ubiquitous Computing (EUC), 2007, pp. 422–431. doi:10.1007/978-3-540-77092-3_37.

31.

Comon-Lundh and

Delaune, The finite variant property: How to get rid of some algebraic properties, in: Term Rewriting and Applications, 16th International Conference, RTA,

Giesl, ed., LNCS, Vol. 3467, Springer, 2005, pp. 294–307. ISBN 3-540-25596-6. doi:10.1007/978-3-540-32033-3_22.

32.

C.J.F.

Cremers, The Scyther Tool: Verification, falsification, and analysis of security protocols, in: 20th International Conference on Computer Aided Verification (CAV’08), LNCS, Vol. 5123, Springer, 2008, pp. 414–418. doi:10.1007/978-3-540-70545-1_38.

33.

Delaune,

M.D.

Ryan and

Smyth, Automatic verification of privacy properties in the applied pi-calculus, in: Proceedings 2nd Joint ITrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM’08), Springer, 2008.

34.

Dreier,

Duménil,

Kremer and

Sasse, Beyond subterm-convergent equational theories in automated verification of stateful protocols, in: Principles of Security and Trust – 6th International Conference, POST 2017, LNCS, Vol. 10204, Springer, 2017, pp. 117–140.

35.

Dreier,

Hirschi,

Radomirovic and

Sasse, Automated unbounded verification of stateful cryptographic protocols with exclusive OR, in: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9–12, 2018, IEEE Computer Society, 2018, pp. 359–373.

36.

Dreier,

Kassem and

Lafourcade, Formal Analysis of E-Cash Protocols, in: SECRYPT 2015 – Proceedings of the 12th International Conference on Security and Cryptography, SciTePress, 2015, pp. 65–75.

37.

Escobar,

Meadows and

Meseguer, Maude-NPA: Cryptographic protocol analysis modulo equational properties, in: Foundations of Security Analysis and Design V, LNCS, Vol. 5705, Springer, 2009, pp. 1–50. doi:10.1007/978-3-642-03829-7_1.

38.

Escobar,

Sasse and

Meseguer, Folding variant narrowing and optimal variant termination, Journal of Logic and Algebraic Programming 81(7–8) (2012), 898–928. doi:10.1016/j.jlap.2012.01.002.

39.

J.D.

Guttman and

J.D.

Ramsdell, CPSA: A cryptographic protocol shapes analyzer, 2009, http://hackage.haskell.org/package/cpsa.

40.

Hirschi,

Baelde and

Delaune, A method for verifying privacy-type properties: The unbounded case, in: IEEE Symposium on Security and Privacy, SP 2016, IEEE Computer Society, 2016, pp. 564–581. ISBN 978-1-5090-0824-7. doi:10.1109/SP.2016.40.

41.

Hirschi,

Baelde and

Delaune, A method for unbounded verification of privacy-type properties, Journal of Computer Security (2019), 1–66.

42.

I.J.

Kim,

E.Y.

Choi and

D.H.

Lee, Secure mobile RFID system against privacy and security problems, in: SecPerU 2007, 2007.

43.

Kremer and

Künnemann, Automated analysis of security protocols with global state, Journal of Computer Security 24(5) (2016), 583–616. doi:10.3233/JCS-160556.

44.

Küsters and

Truderung, Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach, in: Proceedings of the 2008 ACM Conference on Computer and Communications Security, CCS 2008, ACM, 2008, pp. 129–138. ISBN 978-1-59593-810-7.

45.

Lee,

Asano and

Kim, RFID mutual authentication scheme based on synchronized secret information, in: Symposium on Cryptography and Information Security, Hiroshima, Japan, 2006.

46.

Li and

Ding, Protecting RFID communications in supply chains, in: ASIACCS, 2007, pp. 234–241. doi:10.1145/1229285.1229318.

47.

Lowe, Breaking and fixing the Needham–Schroeder public-key protocol using FDR, in: TACAS, 1996, pp. 147–166.

48.

Lowe, A hierarchy of authentication specifications, in: 10th Computer Security Foundations Workshop (CSFW ’97), Rockport, Massachusetts, USA, June 10–12, 1997, IEEE Computer Society, 1997, pp. 31–44. doi:10.1109/CSFW.1997.596782.

49.

Meier,

Schmidt,

C.J.F.

Cremers and

Basin, The TAMARIN prover for the symbolic analysis of security protocols, in: CAV, LNCS, Vol. 8044, Springer, 2013, pp. 696–701.

50.

Osaka,

Takagi,

Yamazaki and

Takahashi, An efficient and secure RFID security method with ownership transfer, in: RFID Security, Springer, 2008, pp. 147–176. doi:10.1007/978-0-387-76481-8_7.

51.

J.D.

Ramsdell,

D.J.

Dougherty,

J.D.

Guttman and

P.D.

Rowe, A hybrid analysis for security protocols with state, in: Proc. 11th International Conference on Integrated Formal Methods (IFM’14), LNCS, Vol. 8739, Springer, 2014, pp. 272–287.

52.

Santiago,

Escobar,

Meadows and

Meseguer, A formal definition of protocol indistinguishability and its verification using maude-NPA, in: Security and Trust Management (STM) 2014, Springer, 2014, pp. 162–177.

53.

Sasse,

Escobar,

Meadows and

Meseguer, Protocol analysis modulo combination of theories: A case study in maude-NPA, in: STM, 2010, pp. 163–178.

54.

Schmidt, Formal Analysis of Key Exchange Protocols and Physical Protocols, PhD dissertation, ETH, Zurich, 2012.

55.

Schmidt,

Meier,

C.J.F.

Cremers and

Basin, Automated analysis of Diffie–Hellman protocols and advanced security properties, in: Computer Security Foundations Symposium (CSF), IEEE, 2012, pp. 78–94.

56.

Tamarin Models for Security Protocols with Exclusive OR, 2019, Accessed: 2019-11-04. https://github.com/tamarin-prover/tamarin-prover/tree/develop/examples/jcs19-xor.

57.

Tamarin website, Accessed: 2019-10-16, 2019, https://tamarin-prover.github.io/.

58.

Turuani, The CL-atse protocol analyser, in: Term Rewriting and Applications, 17th International Conference, RTA 2006, LNCS, Vol. 4098, Springer, 2006, pp. 277–286. ISBN 3-540-36834-5.

59.

Unruh, The impossibility of computationally sound XOR., IACR Cryptology ePrint Archive 2010 (2010), 389.

60.

van Deursen,

Mauw,

Radomirović and

Vullers, Secure ownership and ownership transfer in RFID systems, in: Proc. 14th European Symposium on Research in Computer Security (ESORICS’09), Lecture Notes in Computer Science, Vol. 5789, Springer, 2009, pp. 637–654.

61.

van Deursen and

Radomirović, Security of an RFID protocol for supply chains, in: Proc. 1st Workshop on Advances in RFID (AIR’08), IEEE Computer Society, 2008, pp. 568–573.

62.

van Deursen and

Radomirović, Algebraic attacks on RFID protocols, in: Information Security Theory and Practices. Smart Devices, Pervasive Systems, and Ubiquitous Networks (WISTP’09), Lecture Notes in Computer Science, Vol. 5746, Springer, 2009, pp. 38–51. doi:10.1007/978-3-642-03944-7_4.

63.

van Deursen and

Radomirović, Attacks on RFID Protocols (version 1.1), 2009, http://eprint.iacr.org/2008/310.

64.

Yang,

Park,

Lee,

Ren and

Kim, Mutual authentication protocol for low-cost RFID, in: Ecrypt, Graz, Austria, 2005.

Verification of stateful cryptographic protocols with exclusive OR

Abstract

Keywords

1. Introduction

2. Preliminaries

2.1. Messages represented as terms

Definition 1 (Dependency Graph).

2.3. Security property specification

Example 3 ([13], Ex. 10).

3. Handling XOR

Theorem 2 (Soundness and Completeness of N13 w.r.t. Dependency Graph Equivalence).

4.1. Introductory CR ⊕ example

4.2. LAK’06

Definition 10 ( UK 2 , informal).

Definition 11 ( UK 3 , informal).

2 Restrictions can be used in a Tamarin model to restrict considered executions to the ones that satisfy a specific property.

4.9. Summary of experimental results

6. Conclusion

References

4.1. Introductory $CR \oplus$ example

Definition 10 ( ${UK}_{2}$ , informal).

Definition 11 ( ${UK}_{3}$ , informal).

²
Restrictions can be used in a Tamarin model to restrict considered executions to the ones that satisfy a specific property.