Jannik Dreier
email: jannik.dreier@loria.fr

Lucca Hirschi
email: lucca.hirschi@inf.ethz.ch

Saša Radomirović
email: s.radomirovic@dundee.ac.uk

Ralf Sasse
email: ralf.sasse@inf.ethz.ch

Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR

operations are common in cryptographic protocols, in particular in RFID protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR.

The TAMARIN prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. In this paper, we improve the underlying theory and the tool to deal with an equational theory modeling XOR operations. The XOR theory can be freely combined with all equational theories previously supported, including user-defined equational theories. This makes TAMARIN the first tool 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.

I. 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 [START_REF] Chien | A lightweight RFID protocol using substring[END_REF], [START_REF] Lee | RFID mutual authentication scheme based on synchronized secret information[END_REF], [START_REF] Kim | Secure mobile RFID system against privacy and security problems[END_REF] and mobile communication protocols (3G [START_REF]3GPP: 3G security[END_REF], 4G/LTE [START_REF]3GPP: System Architecture Evolution (SAE)[END_REF], 5G [START_REF]3GPP: Security Architecture and Procedures for 5G System[END_REF]).

As illustrated by many attacks, e.g., [START_REF] Bhargavan | Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS[END_REF], [START_REF] Armando | Formal analysis of saml 2.0 web browser single sign-on: breaking the saml-based single sign-on for google apps[END_REF], [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF], security protocols are notoriously difficult to get right. Consequently, many tools for the automated analysis of security protocols have been developed, e.g., [START_REF] Armando | The AVISPA tool for the automated validation of internet security protocols and applications[END_REF], [START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF], [START_REF] Escobar | Maude-NPA: Cryptographic protocol analysis modulo equational properties[END_REF], [START_REF] Cremers | The Scyther Tool: Verification, falsification, and analysis of security protocols[END_REF], [START_REF] Guttman | CPSA: a cryptographic protocol shapes analyzer[END_REF], [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF]. 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 by extending the class of properties that can be verified to include, e.g., equivalence properties [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF], [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF], [START_REF] Cheval | Trace equivalence decision: Negative tests and non-determinism[END_REF], [START_REF] Santiago | A formal definition of protocol indistinguishability and its verification using Maude-NPA[END_REF], [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF], extending the adversary model with complex forms of compromise [START_REF] Basin | Know your enemy: Compromising adversaries in protocol analysis[END_REF], or extending the expressiveness of protocols, e.g., by allowing different sessions to update a global, mutable state [START_REF] Arapinis | StatVerif: Verification of stateful processes[END_REF], [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF].

Perhaps most significant is the support for user-specified equational theories allowing for the modeling of particular cryptographic primitives [START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF], [START_REF] Escobar | Maude-NPA: Cryptographic protocol analysis modulo equational properties[END_REF], [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF], [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF], [START_REF] Dreier | Beyond subtermconvergent equational theories in automated verification of stateful protocols[END_REF]. 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 section for a detailed discussion. The difficulty in faithfully modeling XOR is is due to the unique combination of algebraic properties that XOR satisfies, specifically (i) the associativity (x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z) and commutativity (x ⊕ y = y ⊕ x) properties and (ii) the cancellation properties (e.g., x⊕x = 0). Modeling XOR without one of the two properties provides only weak security guarantees since whole classes of attacks are missed.

The TAMARIN prover [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF], [START_REF] Tamarin Website | [END_REF] 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 [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF]), modeling cryptographic primitives by means of equational theories, and allowing protocols to maintain state information. The class of userspecified equational theories supported by the tool is the class of convergent equational theories that have the finite variant property [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF], 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. At the same time, TAMARIN supports AC symbols in some built-in theories such as Diffie-Hellman exponentiation, but 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 nontermination 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 when analyzing equivalence properties, the previous attacker model of TAMARIN is not suitable for XOR 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 in particular the RFID protocol LAK'06 [START_REF] Lee | RFID mutual authentication scheme based on synchronized secret information[END_REF], 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 machinechecked) 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 fully automatically analyze two further XOR-based RFID protocols, CH'07 [START_REF] Chien | A lightweight RFID protocol using substring[END_REF] and KCL'07 [START_REF] Kim | Secure mobile RFID system against privacy and security problems[END_REF] against similar properties. Furthermore we study a version of Needham-Schroeder-Lowe (NSL) with XOR and a challenge response protocol using XOR. We also analyze the off-line variant of Chaum's digital cash protocol [START_REF] Chaum | Blind signatures for untraceable payments[END_REF] which uses XOR and blind signatures. 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 [START_REF] Dreier | Formal analysis of e-cash protocols[END_REF], [START_REF] Dreier | Beyond subtermconvergent equational theories in automated verification of stateful protocols[END_REF] could not model XOR precisely and therefore provide weaker guarantees. Related work. In the computational model, XOR operations are common and supported by many tools, e.g., EasyCrypt [START_REF] Barthe | Easycrypt: A tutorial[END_REF] or CryptoVerif [START_REF] Blanchet | A computationally sound mechanized prover for security protocols[END_REF]. However, computational tools typically have a lesser degree of automation (e.g., EasyCrypt is mainly interactive), or are tailored to specific applications (e.g., [START_REF] Barthe | Fully automated analysis of padding-based encryption in the computational model[END_REF], [START_REF] Barthe | Automated proofs of pairingbased cryptography[END_REF]).

In the symbolic model, there are numerous verification tools for cryptographic protocols, some of which support XOR operations.

In the case of a bounded number of sessions, AKISS [START_REF] Baelde | Symbolic verification of privacy-type properties for security protocols with XOR[END_REF] and some solvers from the AVISPA [START_REF] Armando | The AVISPA tool for the automated validation of internet security protocols and applications[END_REF] suite (CL-ATSE [START_REF] Turuani | The cl-atse protocol analyser[END_REF] and OFMC [START_REF] Basin | Ofmc: A symbolic model checker for security protocols[END_REF]) support XOR operations. AKISS is designed to verify observational equivalence properties, while OFMC and CL-ATSE both are limited to trace properties. These tools provide weaker guarantees than TAMARIN, as they only consider a bounded number of sessions.

We will now discuss and compare our extension of TAMARIN with other tools for automated verification for an unbounded number of sessions.

SCYTHER [START_REF] Cremers | The Scyther Tool: Verification, falsification, and analysis of security protocols[END_REF] 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.

CPSA [START_REF] Guttman | CPSA: a cryptographic protocol shapes analyzer[END_REF] was designed for analyzing, essentially, authentication and secrecy properties. The tool was used, in combination with the theorem prover PVS, to analyze stateful protocols [START_REF] Ramsdell | A hybrid analysis for security protocols with state[END_REF]. However, like Scyther, it does neither support XOR nor the verification of equivalence properties. MAUDE-NPA [START_REF] Escobar | Maude-NPA: Cryptographic protocol analysis modulo equational properties[END_REF] 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 [START_REF] Santiago | A formal definition of protocol indistinguishability and its verification using Maude-NPA[END_REF].

PROVERIF [START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF] 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. An extension of PROVERIF (i.e., STATVERIF [START_REF] Arapinis | StatVerif: Verification of stateful processes[END_REF]) 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 user-defined equational theories PROVERIF can handle are insufficient to model XOR, but there is a different extension for PROVERIF to handle some theories including XOR [START_REF] Küsters | Reducing protocol analysis with XOR to the xor-free case in the horn theory based approach[END_REF]. However, this extension is limited to secrecy and simple authentication properties, and again unsuitable for stateful protocols.

The TAMARIN front-end SAPIC [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] has been successfully used to analyze stateful protocols given in an applied pi calculus extension. It directly benefits from our work.

Although there cannot be a computational soundness proof for symbolic models of XOR [START_REF] Unruh | The impossibility of computationally sound xor[END_REF], we argue that symbolic analysis is still useful in itself due to the higher grade of automation. This higher grade of automation allows the handling of more complex protocols, which are difficult to handle manually, and which are the goal of our work. Moreover, symbolic attacks still constitute valid attacks.

Outline. We present necessary preliminaries in Section II. Our extensions of the theory and tool are described in Section III. We evaluate the latter with the case studies shown in Section IV, and we also argue why one needs both AC and cancellation properties for faithfully modeling XOR. We give concluding remarks in Section V.

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

A. 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 ∈ 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(⋅, ⋅), checksign(⋅, ⋅), and pk(⋅) together with the equation checksign(sign(x, k), pk(k)) = x.

TAMARIN also requires that equational theories have the finite variant property (FVP) [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF]. For a theory with the FVP, for any term t, we can compute a finite set of terms t 1 , . . . , t n with the following property: For any substitution σ, there is an i ∈ {1, . . . , n} and substitution φ such that x ⊕ x = 0 (1)

x ⊕ 0 = x (2) x ⊕ x ⊕ y = y (3) x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z (4) x ⊕ y = y ⊕ x (5)
Fig. 1: Equational theory E XOR for XOR 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 [START_REF] Escobar | Folding variant narrowing and optimal variant termination[END_REF]. XOR operations are usually (see, e.g., [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF]) modeled using the equations given in Figure 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 [START_REF] Escobar | Folding variant narrowing and optimal variant termination[END_REF]). 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.

B. 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 , . . . , t n ) t i ∈ T ΣOp (V, N ), F ∈ Σ 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(⋅) converts multisets to sets by dropping the multiplicity. We use the superscript ♯ to denote operations on multisets, e.g., ∪ ♯ 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 ri = id ∶ l--[ a ]→r. We say its name is name(ri) = id, its premises are prems(ri) = l, its conclusions concs(ri) = r, and its actions acts(ri) = 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 → R ⊆ G ♯ × G ♯ × G ♯ , defined by the following step rule, where S is the current state (a multiset of facts):

ri = id ∶ l--[ a ]→r ∈ E ginsts(R) lfacts(l) ⊆ ♯ S pfacts(l) ⊆ S S set(a) → R ((S ∖ ♯ lfacts(l)) ∪ ♯ r)
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 ∈ 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 ∶ --[]→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 [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF].

We define an execution e of a protocol P as the alternating sequence of states and rule instances:

S 0 , (l 1 --[ a 1 ]→r 1 ), S 1 , . . . , S n-1 , (l n --[ a n ]→r n ), S n such that S 0 = ∅,
and that for all i ∈ {1, . . . , n} we have all (S i-1 , (l i --[ a i ]→r i ), S i ) are valid steps according to the step rule. We associate the trace trace(e) = [set(a 1 ), . . . , 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.

MD = { Out(x)--[]→K(x), K(x)--[ K(x) ]→In(x), Fr(x∶fr)--[]→K(x∶fr), []--[]→K(x∶pub) } ∪ { K(x 1 ), . . . , K(x n )--[]→K(f (x 1 , . . . , x n )) f ∈ Σ Op with arity n }
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 ∪ F resh, D ∈ N 2 × N 2
, and dg satisfies the conditions: DG1 For every edge (i, u) ↣ (j, v) ∈ D it holds that i ≤ j and the conclusion fact of (i, u) is syntactically equal to the premise fact of (j, v). DG2 Every premise of dg has exactly one incoming edge.

Rule instances

Fr(m) ri.1:

Fr(m) St(A, m) Out(m) ri.2: [Start(m)] Out(m) K(m) ri.3: K(m) In(m) ri.4: [K(m)] St(A, m) In(m) ri.5: [End(m)]
Trace States DG3 Every linear conclusion of dg has at most one outgoing edge. DG4 The Fresh instances are unique. We denote the set of all dependency graphs modulo E for R by dgraphs E (R).

S 0 = ∅ S 1 = {Fr(m)} S 2 = {St(A, m), Out(m)} S 3 = {St(A, m), K(m)} S 4 = {St(A, m), In(m), K(m)} S 5 = {K(m)}
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:

P basic = Fr(m) St(A, m) Out(m) [Start(m)], St(A, m) In(m) [End(m)]
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.

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 :

{trace(e) e ∈ exec(P ∪ MD)} = E {t t ∈ traces(dg), dg ∈ dgraphs E (P ∪ MD)}

C. 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 ≈ t 2 : t 1 and t 2 are equal in the equational theory;

• F @i: fact F ∈ 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 [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF] 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 T r we write T r ⊧ ∀ ϕ if tr ⊧ ϕ for any tr ∈ T r and T r ⊧ ∃ ϕ if tr ⊧ ϕ for some tr ∈ T r.

We specify unlinkability, anonymity, and more generally equivalence properties by use of diff -terms (defining bisystems, i.e., two systems differing only in some terms) and check their observational equivalence, see [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF].

Example 3 ([14], Ex. 10). An equational theory representing probabilistic encryption is pdec(penc(m, pk(k), r), k) = m. This equation gives rise to the decryption rule for probabilistic encryption for the adversary automatically generated by TAMARIN:

Dpenc ∶ K(penc(m, pk(k), r)), K(k)--[]→K(m) .
Consider now the following bi-system:

S = { GEN ∶ Fr(k)--[]→Key(k), Out(pk(k)), EN C ∶ Key(k), Fr(r 1 ), Fr(r 2 ), In(x)--[]→ Out(diff[r 1 , penc(x, pk(k), r 2 )]) } .
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.

III. 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 [START_REF] Arapinis | New privacy issues in mobile telephony: fix and verification[END_REF]. As XOR has the required properties (AC-convergence and AC-coherence, see [START_REF] Escobar | Folding variant narrowing and optimal variant termination[END_REF] for details and how XOR has these properties), we can define t↓ XOR as the normal form of term t with respect to XOR, ACrewriting and have s = EXOR 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 [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF], 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 ∪ DHBPM, AC' = AC ∪ ACC and E ALL = E XOR ∪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 ,

dgraphs EALL (P ∪ MD) ALL = AC' {dg dg ∈ dgraphs AC' (⌈P ∪ M D⌉ EALL ) ∧ dg ↓ ALL -normal}
Proof. By extension of Lemma 5 in [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF]. 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.

A. Normal dependency graphs

Even for simple convergent theories containing only the pairing function ⟨⋅, ⋅⟩ and the fst and snd operators, nonnormalized 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(⋅), then pairs it with an element c, and then again deduces a, this time from the new pair, to next

K(⟨a, b⟩) K(a) 1: K(a) K(c) K(⟨a, c⟩) 2: K(⟨a, c⟩) K(a) 3: K(a) K(d) K(⟨a, d⟩) 4: K ↑ (a) K ↑ (c) K ↑ (⟨a, c⟩) 1: K ↓ (⟨a, c⟩) K ↓ (a) 2: K ↓ (⟨a, b⟩) K ↓ (a) 1: K ↓ (a) K ↑ (a) 2: K ↑ (a) K ↑ (d) K ↑
(⟨a, d⟩)

3:

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.

build the pair ⟨a, d⟩. This is visualized in the left-most graph of Figure 3. (Note that the topmost rule is actually an instance of the function application rule for fst(⋅) 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 ⊕ x 2 . This results in normal deduction rules depicted in Figure 4, including the usual pairing and unpairing operators.

With such rules, the adversary avoids cases of redundancy

⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ Out(x) K ↓ (x) K ↑ (x) In(x) [K(x)] Coerce ∶ K ↓ (x) K ↑ (x)
Fr(x ∶ f r)

K ↑ (x ∶ f r) K ↑ (x ∶ pub)
Construction rules: Deconstruction rules:

K ↑ (x 1 ) K ↑ (x 2 ) K ↑ (⟨x 1 , x 2 ⟩) K ↓ (⟨x, y⟩) K ↓ (x) K ↓ (x 1 ⊕ x 2 ) K ↑ (x 2 ) K ↓ (x 1 ) K ↑ (0) K ↑ (x 1 ) K ↑ (x 2 ) K ↑ (x 1 ⊕ x 2 ) K ↓ (⟨x, y⟩) K ↓ (y) K ↓ (x 1 ⊕ x 2 ) K ↑ (x 2 ⊕ x 3 ) K ↓ (x 1 ⊕ x 3 ) ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭
Fig. 4: Set of normal deduction rules ND XOR as shown in Figure 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 userdefined equational theory (see [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF], [START_REF] Dreier | Beyond subtermconvergent equational theories in automated verification of stateful protocols[END_REF] 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 normal dependency graphs.

Normal dependency graphs enforce additional normal form conditions, called N1-N12 ( [START_REF] Dreier | Beyond subtermconvergent equational theories in automated verification of stateful protocols[END_REF], recalled in the technical report [START_REF] Dreier | Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (Extended Version)[END_REF]). These conditions help in avoiding other redundancies by, for example, prohibiting the adversary from deducing the same term multiple times.

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 ⊕ b, or more precisely TAMARIN encounters an unsolved K ↓ (a ⊕ 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⊕b) can, for example, be the conclusion of a rule instance with premises K ↓ (a ⊕ c) and K ↑ (c ⊕ b). TAMARIN will then try to resolve the new premises, and again K ↓ (a ⊕ c) can be the conclusion of a deconstruction rule with premises K ↓ (a⊕d) and K ↑ (d⊕c), and so on, resulting in nontermination. This is illustrated in Figure 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.

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 2 (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 3. A normal dependency graph for a set of protocol rules P is a dependency graph dg such that dg ∈ dgraphs(⌈P ⌉ ALL ∪ ND) and the conditions N1-N13 are satisfied. We denote the set of all normal dependency graphs for P with ndgraphs(P ).

Let 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, trace(execs(P ∪ MD)) ↓ ALL = AC' trace(ndgraphs(P )).

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 in the technical report [START_REF] Dreier | Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (Extended Version)[END_REF] is an extension of the proof of Theorem 1 in [START_REF] Dreier | Beyond subtermconvergent equational theories in automated verification of stateful protocols[END_REF], 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). We also show in the technical report [START_REF] Dreier | Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (Extended Version)[END_REF] that N13 is sound and complete in equivalence mode using a similar argument, and that our new constraint solving rule to ensure N13 is correct.

B. Adversary Model for Equivalence Properties

TAMARIN verifies dependency graph equivalence, that is similar to diff-equivalence in PROVERIF [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]. This notion requires that for any dependency graph in one protocol there Fr(r)

⋮ K ↓ (a ⊕ e) K ↑ (e ⊕ d) K ↓ (a ⊕ d) 3: K ↓ (a ⊕ d) K ↑ (d ⊕ c) K ↓ (a ⊕ c) 2: K ↓ (a ⊕ c) K ↑ (c ⊕ b) K ↓ (a ⊕ b) 1:
1:

Fr(r) Out(r ⊕ c) 2: Out(r ⊕ c) K ↓ (r ⊕ c) 3: K ↑ (c) 4: K ↓ (r ⊕ c) K ↑ (c) K ↓ (r)

5:

Fr(r)

1:

Fr(r) Out(r ⊕ d) 2: Out(r ⊕ d) K ↓ (r ⊕ d) 3: K ↑ (c) 4: K ↓ (r ⊕ d) K ↑ (c) K ↓ (r ⊕ d ⊕ c) 6:
Fig. 6: Dependency graph for an instance of the example protocol and its mirror.

is a corresponding ("mirrored") dependency graph in the other protocol [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF].

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:

P r ∶ Fr(r)--[]→Out(diff[r ⊕ c, r ⊕ d])
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).

Consider now the dependency graphs given in Figure 6. 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 N D 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 Figure 6 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.

IV. CASE STUDIES

We first present a simple challenge-response protocol for illustration purposes (Section IV-A). We then present our main case study LAK'06 [START_REF] Lee | RFID mutual authentication scheme based on synchronized secret information[END_REF], introduce security properties, and summarize our analysis results (Section IV-B). We present our results on other RFID protocols (Sections IV-C, IV-D), an eCash protocol (Section IV-E), and a version of the Needham-Schroeder-Lowe public key protocol with XOR (Section IV-F) after that. All our TAMARIN models are freely available in the TAMARIN repository [START_REF]Tamarin repository[END_REF] folder /examples/csf18-xor and TAMARIN as of v1.4.0 contains the presented XOR extension. We present an overview of the results in Figure 12 in Section IV-G.

A. Introductory CR⊕ 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(na) CR1. A → B∶ na CR2. B → A∶ ⟨h(na, k, nb), nb⟩
TAMARIN automatically proves both aliveness and recentaliveness of the responder B, which is the protocol's goal.

Consider now an extension of CR that uses ⊕, called CR⊕:

A∶ knows(k) B∶ knows(k) A∶ fresh(na) CRx1. A → B∶ na CRx2. B → A∶ ⟨h(na ⊕ k ⊕ nb), nb⟩
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(na ⊕ k ⊕ nb), but the attacker chooses the nonce nb ′ ∶= na ⊕ nb ⊕ na ′ where na and nb are the values from the original run, and na ′ is the new challenge. This works because na ′ ⊕k⊕nb ′ = na ′ ⊕k⊕na⊕nb⊕na ′ = k⊕na⊕nb = na⊕k⊕nb and thus A accepts the old hash, as it expects h(na ′ ⊕k ⊕nb ′ ). This attack heavily relies on the cancellation property of XOR as seen in the above equality, where the duplicate na ′ 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 ⊕ (Y ⊕ (X ⊕ Z)) = Y ⊕ Z, pick nb ′ more carefully as nb ′ ∶= na ′ ⊕ (na ⊕ nb) and as result would then have

na ′ ⊕ (k ⊕ nb ′ ) = na ′ ⊕ (k ⊕ (na ′ ⊕ (na ⊕ nb)) = k ⊕ (na ⊕ nb)
which at least contains the same values, but still not in the same order.

B. LAK'06

Protocol Description. LAK'06 [START_REF] Lee | RFID mutual authentication scheme based on synchronized secret information[END_REF] 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 init 0 ) where h(⋅) is some hash function. An Alice&Bob description of the protocol is depicted in Figure 7a.

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 Figure 7b (reader accepts incoming message of the form 2'.). Note that the reader does not update keys in order to re-synchronize with the tag. 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

R∶ knows(k, k0) T ∶ knows(k) R∶ fresh(r0) 1. R → T ∶ r 0 T ∶ fresh(r1) 2. T → R∶ r 1 , h(r 0 ⊕ r 1 ⊕ k) R∶ updates k 0 ∶= k R∶ updates k ∶= h(k) 3. R → T ∶ h(h(r 0 ⊕ r 1 ⊕ k) ⊕ k ⊕ r 0 ) T ∶ updates k ∶= h(k) (a) Core protocol R∶ knows(k, k0) T ∶ knows(k0) R∶ fresh(r0) 1. R → T ∶ r 0 T ∶ fresh(r1) 2'. T → R∶ r 1 , h(r 0 ⊕ r 1 ⊕ k 0 ) 3'. R → T ∶ h(h(r 0 ⊕ r 1 ⊕ k 0 ) ⊕ k 0 ⊕ r 0 ) T ∶ updates k ∶= h(k) (b) Re-synchronization mechanism
Fig. 7: Alice&Bob description of LAK'06 [START_REF] Lee | RFID mutual authentication scheme based on synchronized secret information[END_REF] we leverage its new capability of dealing with XOR theories to provide the first faithful modeling of the protocol 1 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 4. Secrecy is modeled via the following formula: ∀a t i. Claim secret(a, t)@i ⇒ ¬(∃j. K(t)@j)

Next, we define the non-injective agreement [START_REF] Lowe | A hierarchy of authentication specifications[END_REF] 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 5. Non-injective agreement on data t of a role A towards a role B is modeled via the following formula: ∀a b t i. Claim commit(a, b, ⟨A, B, t⟩)@i ⇒ (∃j. Claim running(b, a, ⟨A, B, t⟩)@j) 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 [START_REF] Brusó | Linking unlinkability[END_REF], [START_REF] Brusó | Dissecting unlinkability[END_REF]). We have chosen to analyze three notions of untraceability following three generic constructions: (symbolic) game-based unlinkability [START_REF] Brusó | Linking unlinkability[END_REF] (no relation to game-based computational proofs), which we call UK 1 in the rest of the paper, unlinkability as being checked in [START_REF] Baelde | Symbolic verification of privacy-type properties for security protocols with XOR[END_REF] (UK 2 ), and strong unlinkability (UK 3 ) following [START_REF] Hirschi | A method for verifying privacytype properties: The unbounded case[END_REF] (itself strengthening [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF]). 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 [START_REF] Brusó | Linking unlinkability[END_REF], it seems that UK 3 is strictly stronger than the others [START_REF] Hirschi | A method for unbounded verification of privacy-type properties[END_REF] 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 6 (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 [32] (also called stages [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]): 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 7 (UK 2 , informal). UK 2 holds when the two following systems are behaviorally equivalent:

1) 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). 2) 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 8 (UK 3 , informal). UK 3 holds when the two following systems are behaviorally equivalent:

1) the first system is made of a tag and a reader sharing the same identity that can perform two sessions each; 2) 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 [START_REF] Hirschi | A method for verifying privacytype properties: The unbounded case[END_REF], [START_REF] Hirschi | A method for unbounded verification of privacy-type properties[END_REF]. Fortunately, for a bounded number of sessions only, one can overcome this limitation in TAMARIN using a simplified swapping approach [START_REF] Blanchet | Automated reasoning for equivalences in the applied pi calculus with barriers[END_REF]. 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 4) as well as the two non-injective agreement properties for both sides (Definition 5), 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 subproofs in order to focus the manual exploration on the highlevel 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 [START_REF] Deursen | Attacks on RFID protocols (version 1.1)[END_REF] and works just like the one presented for CR⊕ in Section IV-A.

Analysis of behavioral equivalence properties. We analyze UK 1 , UK 2 , and UK 3 using diff-equivalence verification in TAMARIN [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF]. 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 [START_REF] Hirschi | A method for verifying privacytype properties: The unbounded case[END_REF]). Thanks to those simplifications, we were able to obtain fully automatic proofs as described next.

For UK 2 (see Definition 7) 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 8). TAMARIN automatically finds an attack. While it was known that the property fails to hold [START_REF] Hirschi | A method for verifying privacytype properties: The unbounded case[END_REF], TAMARIN finds a slightly different attack. Note that the protocol is claimed to be untraceable in [START_REF] Deursen | Attacks on RFID protocols (version 1.1)[END_REF] for a weaker notion of unlinkability. Strong unlinkability as being checked here may be considered too strong but [START_REF] Hirschi | A method for unbounded verification of privacy-type properties[END_REF], [START_REF] Hirschi | A method for verifying privacytype properties: The unbounded case[END_REF] 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 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.

C. CH'07

Protocol Description. CH'07 [START_REF] Chien | A lightweight RFID protocol using substring[END_REF] was designed to be a challenge-response RFID authentication protocol that provides tag untraceability. We base our model on [START_REF] Deursen | Attacks on RFID protocols (version 1.1)[END_REF]. Figure 8 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 ⊕ r 2 ⊕ 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 8: The CH'07 RFID authentication protocol. 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.

R∶ knows(k, ID) T ∶ knows(k, ID) R∶ fresh(r1) CH-1. R → T ∶ r1 T ∶ fresh(r2) CH-2. T → R∶ r2, lh(rot(ID, h(r1 ⊕ r2 ⊕ k))⊕ h(r1 ⊕ r2 ⊕ k)) CH-3. R → T ∶ rh(rot(ID, h(r1 ⊕ r2 ⊕ k))⊕ h(r1 ⊕ r2 ⊕ k)) Fig.
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 [START_REF] Deursen | Algebraic attacks on RFID protocols[END_REF], [START_REF] Deursen | Attacks on RFID protocols (version 1.1)[END_REF], and non-injective agreement (Definition 5) of tag and reader, on different data items, namely on ⟨k, r 1 , r 2 ⟩ and on k ⊕ r 1 ⊕ r 2 .

The protocol does not satisfy recent aliveness of tags, due to an impersonation attack [START_REF] Deursen | Algebraic attacks on RFID protocols[END_REF], [START_REF] Deursen | Attacks on RFID protocols (version 1.1)[END_REF]. 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 ⊕ r 1 ⊕ 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 6 and 7) and TAMARIN finds a proof automatically. The protocol does not satisfy the property UK 3 (Definition 8) because the same reader responds to a replayed query with the same answer when the second time the attacker picks r ′ 2 = r ′ 1 ⊕ r 1 ⊕ r 2 , similarly to the attack in Section IV-A. 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

R∶ knows(k, ID) T ∶ knows(k, ID) R∶ fresh(r1) KCL-1. R → T ∶ r1
T ∶ fresh(r2) KCL-2. T → R∶ ⟨ID ⊕ r2, h(r1, k) ⊕ r2⟩ Fig. 9: The KCL'07 RFID authentication protocol. 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.

D. KCL'07

KCL'07 [START_REF] Kim | Secure mobile RFID system against privacy and security problems[END_REF] 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 9 shows the protocol description.

Informally, the aliveness property is guaranteed due to the response including the hash of the challenge nonce r1 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 r2 actually chosen by the tag, as a man-inthe-middle attacker can simply pick a random r3 and XOR it to both elements of the pair the tag sends back to the reader. Then, the reader believes r2 ⊕ r3 to be the chosen random value. The reader can only check that the application of XOR to both values results in ID ⊕h(r1, k). Therefore, the random value r2 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 r2. To be precise, the sent term is ⟨id ⊕ r2, h(r1, k) ⊕ r2⟩ received as ⟨idr2, hashr2⟩ while in our model the reader simply receives X, interpreted as idr2 ⊕ hashr2.

The first property expected from this protocol is recent aliveness, which we prove automatically with TAMARIN. As explained in Deursen and Radomirović [START_REF] Deursen | Attacks on RFID protocols (version 1.1)[END_REF] 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 r1, the results of applying XOR to the response for a given tag is always ID ⊕ h(r1, 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.

E. Chaum's Offline eCash Protocol

Protocol Description. Chaum's offline eCash [START_REF] Chaum | Untraceable electronic cash[END_REF] 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 eCash-1. C → B∶ blind(x ⊕ C, r), blind(x, r) eCash-2. B → C∶ sign(blind(x ⊕ C, r), skB), sign(blind(x, r), skB) eCash-3. S → C∶ z eCash-4. C → S∶ ⟨x ′ , sign(x ′ , skB)⟩ where x ′ =x if z =0 and x ′ = x ⊕ C otherwise eCash-5. S → B∶ ⟨x ′ , sign(x ′ , skB)⟩ eCash-6. B → S∶ x ′ eCash-7. S → B∶ ok/not ok Fig. 10: A simplified model of Chaum's offline eCash protocol. The protocol uses XOR as well as blind signatures, to ensure anonymity. The blind signatures require a non subtermconvergent equational theory, which illustrates that TAMARIN is able to handle the combination of these two complex equational theories.

eC-1. C → E∶ blind(x ⊕ C, r), blind(x, r) eC-2. E → C∶ sign(blind(x ′ , r), skB) where x ′ = x or x ′ = x ⊕ C eC-3. C → E∶ ⟨x ′ , sign(x ′ , skB)⟩
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 Figure 10. 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.

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 Figure 11. 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.

F. NSLPK3xor

This is an insecure variant of the Needham-Schroeder-Lowe [START_REF] Lowe | Breaking and fixing the Needham-Schroeder public-key protocol using FDR[END_REF] (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. [START_REF] Chevalier | An NP decision procedure for protocol insecurity with XOR[END_REF], and this protocol has previously been analyzed by Sasse et al. [START_REF] Sasse | Protocol analysis modulo combination of theories: A case study in Maude-NPA[END_REF] using MAUDE-NPA.

A∶ knows(sk(A), pk(B)) B∶ knows(sk(B), pk(A)) A∶ fresh(na) NSLx1. A → B∶ enc(⟨na, A⟩, pk(B))

B∶ fresh(nb) NSLx2. B → A∶ enc(⟨na, nb ⊕ B⟩, pk(A)) NSLx3. A → B∶ enc(nb, 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 [START_REF] Sasse | Protocol analysis modulo combination of theories: A case study in Maude-NPA[END_REF].

G. Summary of Experimental Results

We present in Figure 12 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(R) Xeon(R) CPU E5-2650 v4 @ 2.20GHz (with 12 cores each), 256GB of RAM, running Ubuntu 16.04.3, and we use 10 threads per experiment.

All our theories are available at [START_REF]Tamarin repository[END_REF], in the folder /examples/csf18-xor. 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. 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 is one case where we manually constructed an attack, denoted M.

V. 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 verifiers. 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 suggested by our numerous case studies. We believe that TAMARIN can now tackle large-scale real-life protocols with XOR.

As future work, we would like to study mobile telecommunication protocols that use XOR such as the AKA protocol [START_REF]3GPP: System Architecture Evolution (SAE)[END_REF] [1]. Previous analyses of this protocol [START_REF] Arapinis | New privacy issues in mobile telephony: fix and verification[END_REF], [START_REF] O'hanlon | Mobile subscriber wifi privacy[END_REF] were not able to model parts of the protocol making use of XOR, therefore providing guarantees that are too weak in our opinion. We would like to investigate the new perspectives opened by our extension in TAMARIN and faithfully analyze the AKA protocol as used in existing mobile networks (i.e., 3G [START_REF]3GPP: System Architecture Evolution (SAE)[END_REF] and 4G [START_REF]3GPP: 3G security[END_REF]) as well as in 5G that is being standardized [START_REF]3GPP: Security Architecture and Procedures for 5G System[END_REF].

On the theory side 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 could enable additional case studies, including protocols using weak phases.

Fig. 2 :

 2 Fig. 2: Example execution of (P basic ∪ MD).

Fig. 5 :

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

Fig. 11 :

 11 The simplified model of Chaum's offline eCash protocol with dishonest seller and bank represented by the adversary-controlled environment E. the deposit protocol, where S deposits the received currency with B.

Fig. 12 :

 12 Fig. 12: Summary Table of Results. Automation: A = automatic, A (BFS) = automatic with breadth-first search for attacks, O=oracle, SM=semi-manual, M=manual. † means the time is for verifying the resulting stored proof. More details in Section IV-G. 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
	NSL-xor	nonce secrecy		A	5.1s
		injective agreement initiator		A	1.4s
		injective agreement responder		A	4.0s
	CH07	recent aliveness tag		A	2.2s
		recent aliveness reader		A	1.1s
		non-inj. agree. tag (k ⊕ r1 ⊕ r2)		A	1.1s
		non-inj. agree. tag (k, r1, r2)		A	1.3s
		non-inj. agree. reader (k ⊕ r1 ⊕ r2)		A	1.0s
		non-inj. agree. reader (k, r1, r2)		A	1.1s
	Chaum Offline *coins	No phases	O	10.4s
		anonymity	No phases	A	2.8s
		anonymity of double spender	No phases	A	12.7s
	KCL07	recent aliveness tag	XORed pair	A	1.7s
	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)	1m 38.7s
	CH07	UK1		A	51.5s
		UK2		A	12m16.6s
		UK3		A	3m07.1s
	KCL07	UK1	XORed pair	A (BFS)	126m27.6s
		UK2	XORed pair	A	1m02.6s
		UK3	XORed pair	M	†2.1s
	LAK06	UK1 (tags only)	bounded sessions	A	4m25.4s
		UK2	bounded sessions	A	15m10.4s
		UK3	bounded sessions	A	85m46.1s

[START_REF] Hirschi | A method for verifying privacytype properties: The unbounded case[END_REF] considers a stateless abstraction,[START_REF] Baelde | Symbolic verification of privacy-type properties for security protocols with XOR[END_REF] only considers a small number of sessions.

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

ACKNOWLEDGEMENTS

We are grateful for the support from the ERC under the EUs Horizon 2020 research and innovation program (grant agree-ments No 645865-SPOOC) and the UK Engineering and Physical Sciences Research Council (EPSRC) grant EP/P013694/1.