Ivan Gazeau

Steve Kremer

Automated analysis of equivalence properties for security protocols using else branches

In this paper we present an extension of the AKISS protocol verification tool which allows to verify equivalence properties for protocols with else branches, i.e., disequality tests. While many protocols are represented as linear sequences or inputs, outputs and equality tests, the reality is often more complex. When verifying equivalence properties one needs to model precisely the error messages sent out when equality tests fail. While ignoring these branches may often be safe when studying trace properties this is not the case for equivalence properties, as for instance witnessed by an attack on the European electronic passport. One appealing feature of our approach is that our extension re-uses the saturation procedure which is at the heart of the verification procedure of AKISS as a black box, without need to modify it. As a result we obtain the first tool that is able verify equivalence properties for protocols that may use xor and else branches. We demonstrate the tool's effectiveness on several case studies, including the AKA protocol deployed in mobile telephony.

Introduction

Security protocols are communication protocols that rely on cryptographic primitives, e.g. encryption, or digital signatures to ensure security properties, e.g., confidentiality or authentication. Well-known examples of security protocols include TLS [START_REF] Dierks | The transport layer security (TLS) protocol version 1.1. RFC 4346[END_REF], Kerberos [START_REF] Neuman | The kerberos network authentication service (v5). RFC 4120[END_REF] and IKE [START_REF] Kaufman | Internet key exchange protocol version 2 (ikev2). RFC 7296[END_REF]. These protocols are extremely difficult to design as they must ensure the expected security property, even if the network is under control of an attacker: each message sent on the network can be intercepted by the attacker, each received message potentially originates from the attacker, and the attacker may manipulate all received data by applying functions on it. Moreover, as several sessions of the protocol may be executed concurrently, one must consider all possible interleavings, and the attacker may even participate in some of these sessions as a legitimate participant. As a result, a security proof by hand is extremely tricky as it would require to explore all of the possible cases.

A successful approach to discover weaknesses in such protocols, or show their absence is to use dedicated formal verification tools. A variety of tools for analysing protocols exist: ProVerif [START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF], Scyther [START_REF] Cremers | The Scyther Tool: Verification, falsification, and analysis of security protocols[END_REF], Maude-NPA [START_REF] Escobar | Maude-NPA: Cryptographic protocol analysis modulo equational properties[END_REF], Tamarin [START_REF] Schmidt | The TAMARIN prover for the symbolic analysis of security protocols[END_REF], AVISPA [START_REF] Armando | The AVISPA tool for the automated validation of internet security protocols and applications[END_REF], . . . These tools were generally initially developed for verifying trace properties of rather simple protocols. In the last years there has been a large body of works for extending these tools to handle more general properties and more complex protocols.

Most tools were designed for analysing trace properties: a protocol cannot reach a bad state, e.g., a state where the attacker knows a secret value. Many important security properties are however stated in terms of indistinguishability: can an attacker distinguish two protocols? For instance real-or-random secrecy states the indistinguishability of two protocols, one outputting at the end of the run the "real" secret, used within the protocol, while the other protocol outputs a freshly generated random secret. Similarly, unlinkability can be modeled by the adversary's inability to distinguish two sessions run by the same party form two sessions run by two different parties. More generally, strong flavours of secrecy [START_REF] Blanchet | Automatic proof of strong secrecy for security protocols[END_REF], anonymity and unlinkability [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF], as well as vote privacy [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF], are expressed as indistinguishability. This notion is naturally modelled in formal models through behavioural equivalences in cryptographic process calculi, such as the spi [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] and applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. During the last years, several specific tools for checking such equivalences have been developed [START_REF] Tiu | Automating open bisimulation checking for the spi-calculus[END_REF][START_REF] Cheval | Trace equivalence decision: Negative tests and non-determinism[END_REF][START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF], or existing tools have been extended to handle these properties [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF][START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF][START_REF] Santiago | A formal definition of protocol indistinguishability and its verification using Maude-NPA[END_REF].

Similarly, many tools were designed to verify protocols that have a simple, linear execution flow: many protocol specification languages allow several roles in parallel, each consisting of a sequence of input, or output actions with the possibility to check equality between parts of messages. More complex protocols do however require branching, and allow to react differently according to whether an equality test holds or not (rather than just halting if a test fails). As demonstrated by an attack on the European electronic passport [START_REF] Chothia | A traceability attack against e-passports[END_REF], taking into account the exact error message in case a test fails may be crucial: the fact that in some versions of the passport output different error messages allowed an attacker to trace a given passport. In this paper we will extend the AKISS tool with the ability to verify protocols that have else branches.

An overview of the AKISS tool. The AKISS tool [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF] is a verification tool for checking indistinguishability properties. More precisely, it verifies trace equivalence in a replication free (i.e., considering a bounded number of sessions) and positive (no else branches) fragment of the applied pi calculus. The tool allows a wide range of cryptographic primitives that are specified by the means of a user defined equational theory. The tool is correct for any equational theory that can be oriented into a convergent rewrite system which has the finite variant property and was shown to guarantee termination on any subterm convergent equational theory. This class of theories include classical cryptographic primitives such as encryption, signatures and hashes, but also non-interactive zero knowledge proofs. Moreover, even though termination is not guaranteed protocols relying on blind signatures or trapdoor commitments have been successfully analysed. In addition, a recent extension of AKISS provides support for protocols that use the exclusive or (xor) operation [START_REF] Baelde | Symbolic verification of privacy-type properties for security protocols with XOR[END_REF].

In a nutshell, AKISS proceeds as follows. Protocols are translated into first-order Horn clauses. Next, the set of Horn clauses is saturated using a dedicated Horn clause resolution procedure. This saturated set of clauses provides a finite representation of all reachable states of the protocols, of the intruder knowledge and equality tests that hold on the protocol outputs. These equality tests are used by the adversary to distin-guish protocols, i.e., its aim is to find a test which holds on one protocol, but not the other. Next, AKISS uses this saturated set of Horn clauses to decide trace equivalence when the processes specifying the protocol are determinate (the precise definition of determinacy will be given in section 2). On general processes, AKISS may over-and under-approximate trace equivalence, as discussed in [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF].

Our contributions. Our main contribution is to extend the AKISS tool to allow more complex protocols which allow non trivial else branches. An interesting point of our approach is that we do not need to modify the saturation procedure of AKISS: we only need to saturate positive processes (in which disequality tests are ignored). The algorithm is based on the following simple observation: whenever a trace is not executable because of the failure of a disequality test t 1 = t 2 , the saturation of the process in which t 1 = t 2 is replaced by t 1 = t 2 computes all the traces that fail to execute on the original process (due to this particular disequality test). This test can then be confronted to the other process that we expect to be trace equivalent.

From a theoretical point, given that the saturation of AKISS was shown to terminate on any subterm convergent rewrite system our algorithm provides, en passant, a new decidability result for the class of subterm convergent equational theories for protocols with else branches, generalising the results of [START_REF] Baudet | Deciding security of protocols against off-line guessing attacks[END_REF][START_REF] Chevalier | Decidability of equivalence of symbolic derivations[END_REF] that do not allow else branches and the result of [START_REF] Cheval | Automating security analysis: symbolic equivalence of constraint systems[END_REF], which only applies to a particular equational theory. Moreover, the result is modular, in the sense that if we generalize the saturation procedure to other equational theories support for else branches comes for "for free". From a more practical point, we have implemented our new procedure in the AKISS tool and demonstrate its effectiveness on several case studies. Hence, we provide the first tool that is able to handle protocols that require both xor and else braches: in addition to previously analysed protocols, such as the private authentication protocol and the BAC protocol implemented in the European passport, this allows us to analyse protocols using xor, such as the AKA protocol [START_REF] Gpp | Technical specification group services and system aspects; 3G security; security architecture (release 9)[END_REF] used in 3G and 4G mobile telephony, as well as xor-based RFID protocols with key update (which requires an else branch for the modelling). A previous analysis of the AKA protocol with ProVerif replaced the use of xor with encryption [START_REF] Arapinis | New privacy issues in mobile telephony: fix and verification[END_REF]. Replacing xor by encryption may however miss attacks as it was shown by Ryan and Schneider in [START_REF] Ryan | An attack on a recursive authentication protocol. A cautionary tale[END_REF].

Related work. We consider two kinds of tools: those restricted to a bounded number of sessions (as in our work) and those that allow for an unbounded number of sessions. The first kind of tools includes the SPEC and APTE tools. SPEC [START_REF] Tiu | Automating open bisimulation checking for the spi-calculus[END_REF] allows to verify a symbolic bisimulation: it only supports a fixed equational theory (encryption, signature, hash and mac) and has no support for else branches. The APTE tool also supports a fixed equational theory (similar to SPEC), but allows else branches. Both tools are not restricted to determinate processes. Tools that allow protocol verification for an unbounded number of sessions include ProVerif, Maude NPA and Tamarin. Given that the underlying problem is undecidable when the number of sessions is not bounded, termination is not guaranteed. Each of these tools allows for else branches user-defined equational theories, but ProVerif and Tamarin do not include support for xor. While Maude NPA does support xor in principle, termination fails even on simple examples [START_REF] Santiago | A formal definition of protocol indistinguishability and its verification using Maude-NPA[END_REF]. We may also note that the support for else branches in Maude NPA is very recent [START_REF] Yang | Strand spaces with choice via a process algebra semantics[END_REF].

Finally, each of these three tools checks a more fine-grained relation that trace or observational equivalence, called diff-equivalence: this equivalence requires both processes to follow the same execution flow and is too fine-grained for some applications.

Full proofs, omitted because of lack of space, are available in [START_REF] Gazeau | Automated analysis of equivalence properties for security protocols using else branches (extended version)[END_REF].

A formal model for security protocols

In this section we introduce our formal language for modelling security protocols. Messages are modelled as terms and equipped with an equational theory, that models the algebraic properties of cryptographic primitives. The protocols themselves will be modelled in a process calculus similar to the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]: protocol participants are modelled as processes and their interaction through message passing.

Term algebra

Terms are built over the following atomic messages : the set of names N , that is partitioned into private names N prv and public names N pub ; the set of message variables X , denoted x, y, . . .; the set of parameters W = {w 1 , w 2 , . . .}. Private names are used to model fresh, secret values, such as nonces or cryptographic keys. Public names represent publically known values such as identifier and are available to the attacker. Parameters allow the adversary to refer to messages that were previously output.

We consider a signature Σ, i.e., a finite set of function symbols together with their arity. Function symbols of arity 0 are called constants. Given a signature Σ and a set of atoms A we denote by T (Σ, A) the set of terms, defined as the smallest set that contains A and is closed under application of function symbols. We denote by vars(t) the set of variables occurring in a term t. A substitution is a function from variables to terms, lifted to terms homomorphically. The application of a substitution σ to a term u is written uσ, and we denote dom(σ) its domain, i.e. dom(σ) = {x | σ(x) = x}. We denote the identity substitution whose domain is the empty set by ∅.

We equip the signature Σ with an equational theory E: an equational theory is defined by a set of equations M = N with M, N ∈ T (Σ, X ). The equational theory E induces an equivalence relation = E on terms: = E is the smallest equivalence on terms, which contains all equations M = N in E, is closed under application of function symbols and substitutions of variables by terms.

Example 1.

As an example we model the exclusive-or operator. Let Σ xor = {⊕, 0}, and the equational theory E xor defined by the following equations:

x ⊕ x = 0 x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z x ⊕ 0 = x x ⊕ y = y ⊕ x
Additional primitives, e.g. pairs, symmetric and asymmetric encryptions, signatures, hashes, etc, can be modelled by extending the signature and equational theory. andE + xor be defined by extending E xor with the following equations : proj 1 ( x, y ) = x, and proj 2 ( x, y ) = y.

Example 2. Let Σ + xor = Σ xor { •, • , proj 1 , proj 2 , h},
The symbol •, • models pairs and proj 1 and proj 2 projections of the first and second element. The unary symbol h models a cryptographic hash function. Let AU T N = SQN N ⊕ AK, M AC , then we have proj

1 (AU T N ) ⊕ AK = E SQN N .
As we build on the AKISS tool [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF][START_REF] Baelde | Symbolic verification of privacy-type properties for security protocols with XOR[END_REF] we suppose in the following that the signature and equational theory are an extension the theory of exclusive or, i.e., Σ is such that

Σ xor ⊆ Σ and E = E xor ∪ {M = N | M, N ∈ T (Σ Σ xor , X )}.
and that E can be oriented into a convergent rewrite system which has the finite variant property. This allows to model a wide range of cryptographic primitives, including symmetric and asymmetric encryption, digital signatures, hash functions and also zero knowledge proofs or blind signatures. We refer the reader to [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF] for the precise technical definitions, which are not crucial for this paper.

Process calculus

Syntax Let Ch be a set of public channel names. A protocol is a set of processes and a process is generated by the following grammar:

P, P , P 1 , P 2 ::= 0 null process in(c, x).P input out(c, t).P output [s = t].P test = [s = t].P test =
where x ∈ X , s, t ∈ T (Σ, N ∪ X ), and c ∈ Ch.

A receive action in(c, x) acts as a binding construct for the variable x and free and bound variables of processes are defined as usual. We also assume that each variable is bound at most once. A process is ground if it does not contain any free variables. For sake of conciseness, we sometimes omit the null process at the end of a process.

Following [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF], we only consider a minimalistic core calculus. Given that we only consider a bounded number of sessions (i.e., a process calculus without replication) and that we aim at verifying trace equivalence, parallel composition, denoted P Q can be added as syntactic sugar to denote the set of all interleavings at a cost of an exponential blow-up (see [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF]). Similarly, we can encode conditionals: a process

if t 1 = t 2 then P else Q can be encoded by the set {[t 1 = t 2 ].P, [t 1 = t 2 ]
.Q}. As usual we omit else Q when Q = 0 and sometimes write if t 1 = t 2 then P else Q for if t 1 = t 2 then Q else P . This will ease the specification of protocols and improve readability. A protocol typically consists of the set of all possible interleavings. Example 3. As an example consider a simplified version of the AKA protocol, which is vulnerable to replay attacks, depicted in Figure 1. The network (NS) and mobile station (MS) share a secret key k IM SI . NS generates a nonce r which it sends to MS together with f(k IM SI , r) where f models a message authentication code (MAC). MS verifies

MS kIMSI NS kIMSI nonce r XM AC ← f(kIMSI , r) r, XM AC M AC ← f(kIMSI , r) if M AC = XM AC then RES ← MAC FAIL else RES ← f2(kIMSI ,
N S = out(c, r, f(k IM SI , r) ).in(c, x).if x = f 2 (k IM SI , r) then out(c, RECOVER) M S = in(c, y). if y = f(k IM SI , r) then out(c, MAC FAIL) else out(c, f 2 (k IM SI , r))
If we skip the actions [x = f 2 (k IM SI , r)].out(c, RECOVER), the protocol corresponds to a set of 12 processes which include, for instance, the 4 following processes.

out(c, r, f(k IM SI , r) ).in(c, y).[y = f(k IM SI , r)].out(c, MAC FAIL).in(c, x) out(c, r, f(k IM SI , r) ).in(c, y).[y = f(k IM SI , r)].out(c, f 2 (k IM SI , r)).in(c, x) out(c, r, f(k IM SI , r) ).in(c, y).in(c, x).[y = f(k IM SI , r)].out(c, MAC FAIL) out(c, r, f(k IM SI , r) ).in(c, y).in(c, x).[y = f(k IM SI , r)].out(c, f 2 (k IM SI , r))
Note that since a test is an invisible action, there is no need to consider traces where a test does not strictly precede its following action. The correctness of this optimization is proven in [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF].

Semantics In order to define the operational semantics of our process calculus we define the notion of message deduction. Intuitively, message deduction models which new messages an intruder can construct from previously learnt messages. The messages output during a protocol execution are presented by a frame:

ϕ = {w 1 → t 1 , . . . , w → t }
A frame is a substitution dom(ϕ) = {w 1 , . . . , w }. An intruder may refer to the ith term through the parameter w i . Definition 1. Let ϕ be a frame, t ∈ T (Σ, N ) and R ∈ T (Σ, N pub ∪ dom(ϕ)). We say that t is deducible from ϕ using R, written ϕ R t, when Rϕ = E t.

Intuitively, an attacker can deduce new messages by applying function symbols in Σ to public names (in N pub ) and terms he already knows (those in ϕ). The term R is called a recipe.

A configuration is a pair (P, ϕ) where P is a ground process, and ϕ is a frame. The operational semantics is defined as a labelled transition relation on configurations -→ where is either an input, an output, or an unobservable action test defined as follows:

RECV (in(c, x).P, ϕ)

in(c,R) ----→ (P {x → t}, ϕ) if ϕ R t SEND (out(c, t).P, ϕ) out(c) ---→ (P, ϕ ∪ {w |ϕ|+1 → t}) TEST = ([s = t].P, ϕ) test --→ (P, ϕ) if s = E t TEST = ([s = t].P, ϕ) test --→ (P, ϕ) if s = E t
Intuitively, the labels have the following meaning:

-in(c, R) represents the input of a message sent by the attacker on channel c and the message is deduced using recipe R; -out(c) represents the output of a message on channel c (adding the message to the frame); -test represents the evaluation of a conditional (in the equational theory). -----→ (P , ϕ ), and similarly for = ⇒.

Trace equivalence

The fact that an attacker cannot distinguish two protocols will be modelled through trace equivalence. We first define the notion of a test which an attacker may apply on a frame to try to distinguish two processes.

Definition 2. Let ϕ be a frame and R 1 , R 2 be two terms in T (Σ, N pub ∪ dom(ϕ)).

The test R 1 ? = R 2 holds on frame ϕ, written (R 1 = R 2 )ϕ, if R 1 ϕ = E R 2 ϕ.
Trace equivalence of processes P and Q states that any test that holds on process P (after some execution) also holds on process Q after the same execution.

Definition 3 ([15]

). A protocol P is trace included in a protocol Q, denoted P Q, if whenever (P, ∅)

1,..., n = ==== ⇒ (P, ϕ) and (R 1 = R 2 )ϕ, then there exists a configuration

(Q , ϕ ) such that (Q, ∅) 1,..., n = ==== ⇒ (Q , ϕ ) and (R 1 = R 2 )
ϕ . We say that P and Q are equivalent, written P ≈ Q, if P Q and Q P.

This notion of equivalence does not coincide with the usual notion of trace equivalence as defined e.g. in [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF]. It is actually coarser and is therefore sound for finding attacks. However, it has been shown that the classical and above defined notions coincide for the class of determinate processes [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF].

Definition 4 ([15]

). We say that a protocol P is determinate if whenever (P, ∅) = R 2 , we have that:

(R 1 = R 2 )ϕ if, and only if (R 1 = R 2 )ϕ .
Determinacy of a protocol can be achieved through sufficient syntactic conditions, e.g. enforcing action-determinism [START_REF] Baelde | Partial order reduction for security protocols[END_REF]: all executions of an action determinate process ensure that we cannot reach a process P where the same action may lead to two different processes, e.g. we forbid the set of processes generated by (out(c, a).P 1 ) ((out(c, b).P 2 ) but allow (out(c 1 , a).P 1 ) ((out(c 2 , b).P 2 ). Action-determinism is automatically checked by AKISS. Whenever processes are not determinate, the above equivalence can be used to disprove trace equivalence, i.e., find attacks. The capability of AKISS to under approximate trace equivalence consists in finding a one-to-one mapping between each process of P and Q such that the pair of processes, which are determinate by construction, are equivalent. Such an approach is still possible with our procedure. In this paper we develop a procedure which checks trace equivalence on determinate processes and may be used for finding attacks on general processes.

Modelling using Horn clauses

Our decision procedure is based on a fully abstract modelling of a process in first-order Horn clauses which has initially been developed in [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF] and adapted to support the Xor operator in [START_REF] Baelde | Symbolic verification of privacy-type properties for security protocols with XOR[END_REF]. In this section we recall the main definitions and theorems of [START_REF] Baelde | Symbolic verification of privacy-type properties for security protocols with XOR[END_REF].

Predicates

We define the set of symbolic runs, denoted u, v, w, . . ., as the set of finite sequences of symbolic labels:

u, v, w := | , w with ∈ {in(c, t), out(c), test | t ∈ T (Σ, N ∪ X ), c ∈ Ch}
The empty sequence is denoted by . Intuitively, a symbolic run stands for a set of possible runs of the protocol. We denote u E v when u is a prefix (modulo E) of v.

(P0, ϕ0) |= r 1 ,..., n if (P0, ϕ0) L 1 --→ (P1, ϕ1) . . . Ln --→ (Pn, ϕn) such that i =E Liϕi-1 for all 1 ≤ i ≤ n (P0, ϕ0) |= k 1 ,..., n (R, t) if when (P0, ϕ0) L 1 --→ (P1, ϕ1) L 2 --→ . . . Ln --→ (Pn, ϕn) such that i =E Liϕi-1 for all 1 ≤ i ≤ n, then ϕn R t (P0, ϕ0) |= i 1 ,..., n (R, R ) if

Fig. 2: Semantics of atomic formulas

We assume a set Y of recipe variables disjoint from X , and we use capital letters X, Y, Z to range over Y. We assume that such variables may only be substituted by terms in T (Σ, N pub ∪ W ∪ Y).

We consider four kinds of predicates over which we construct the atomic formulas of our logic. Below, w denotes a symbolic run, R, R are terms in T (Σ, N pub ∪ W ∪ Y), and t is a term in T (Σ, N ∪X ). Informally, these predicates have the following meaning (see Figure 2 for the formal semantics).

r w holds when the run represented by w is executable; -k w (R, t) holds if whenever the run represented by w is executable, the message t can be constructed by the intruder using the recipe R; -i w (R, R ) holds if whenever the run w is executable, R and R are recipes for the same term; and ri w (R, R ) is a short form for the conjunction of the predicates r w and i w (R, R ).

A (ground) atomic formula is interpreted over a pair consisting of a process P and a frame ϕ, and we write (P, ϕ) |= f when the atomic formula f holds for (P, ϕ) or simply P |= f when ϕ is the empty frame. We consider first-order formulas built over the above atomic formulas and the usual connectives (conjunction, disjunction, negation, implication, existential and universal quantification). The semantics is defined as expected, but the domain of quantified variables depends on their type: variables in X may be mapped to any term in T (Σ, N ), while recipe variables in Y are mapped to recipes, i.e. terms in T (Σ, N pub ∪ W).

Statements and saturation

We now identify a subset of the formulas, which we call statements. Statements will take the form of Horn clauses, and we shall be mainly concerned with them.

Definition 5 ([15]

). A statement is a Horn clause of the form H ⇐ k u1 (X 1 , t 1 ), . . . , k un (X n , t n ) where:

-H ∈ {r u0 , k u0 (R, t), i u0 (R, R ), ri u0 (R, R )}; u 0 , u 1 , . . . , u n are symbolic runs such that u i E u 0 for any i ∈ {1, . . . , n}; t, t 1 , . . . , t n ∈ T (Σ, N ∪ X ); -R, R ∈ T (Σ, N pub ∪ W ∪ Y); and -X 1 , . . . , X n are distinct variables from Y.

Lastly, vars(t) ⊆ vars(t 1 , . . . , t n ) when H = k u0 (R, t).

In the definition above, we implicitly assume that all variables are universally quantified, i.e. all statements are ground. By abuse of language we sometimes call σ a grounding substitution for a statement H ⇐ B 1 , . . . , B n when σ is grounding for each of the atomic formulas H, B 1 , . . . , B n .

In [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF], the authors present a saturation-based procedure sat that given a ground process P produces a fully abstract set of solved statements sat(P ). The procedure starts by translating P and the equational theory into a finite set of statements. Then this set is saturated by applying Horn clause resolution rules. Finally, if the procedure terminates (which is guaranteed for subterm convergent equational theories), the set of solved statements K produced by the saturation procedure is a sound and complete abstraction of P : any statement that holds on the protocol P is a logical consequence of K. The notion of logical consequence is formalised through the (infinite) set H e (K).

Definition 6 ([8]

). Given a set K of statements, H(K) is the smallest set of ground facts that is closed under the rules of Figure 3. We define H e (K) to be the smallest set of ground facts containing H(K) and that is closed under the rules of Figure 4.

CONSEQ EXTEND f = H ⇐ B1, . . . , Bn ∈ K σ grounding for f B1σ ∈ H(K), . . . , Bnσ ∈ H(K) Hσ ∈ H(K) ku(R, t) ∈ H(K) kuv(R, t) ∈ H(K) Fig. 3: Rules of H(K) REFL iw(R, R) ∈ He(K) CONG iw(R1, R 1 ), . . . , iw(Rn, R n ) ∈ He(K) f ∈ Σ iw(f(R1, . . . Rn), f(R 1 , . . . R n )) ∈ He(K) EXT iu(R, R ) ∈ He(K) iuv(R, R ) ∈ He(K) EQ. CONSEQ. kw(R, t) ∈ H(K) iw(R, R ) ∈ He(K) kw(R , t) ∈ He(K)
Fig. 4: Rules of H e (K)

Theorem 1 ([8]). Let K = sat(P ) for some ground process P . We have that:

-P |= f for any f ∈ K ∪ H e (K); -If (P, ∅) L1,...,Ln ------→ (Q, ϕ) then 1. r L1ϕ,...,Lnϕ ∈ E H e (K); 2. if ϕ R t then k L1ϕ,...,Lnϕ (R, t) ∈ E H e (K); 3. if ϕ R t and ϕ R t, then i L1ϕ,...,Lnϕ (R, R ) ∈ E H e (K).

Algorithm

We first introduce a few notations and preliminary definitions. We start by introducing the recipe function: its goal is to associate a sequence of labels to a symbolic run and a positive process (in the labels we replace the input terms of the symbolic run by the recipes used to deduce them).

Definition 7. Given a positive process P and a symbolic run 1 , . . . , k we define a function rec P ( 1 . . . k ) = L 1 . . . L k where

L i = in(c, R) if i = in(c, t) and k 1... i-1 (R, t) ∈ H(sat(P ) ∪ K) i otherwise and K = {k (X i , x i ) | 1 ≤ i ≤ n, vars( 1 , . . . , k ) = {x 1 , . . . x n }, X 1 , . . . X n ∈
Y are pairwise distinct and fresh}.

Note that several functions may satisfy the specification of this definition. Here we consider any possible implementation of this specification, e.g., the one presented in [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF]. The complicated case is when the symbolic label is an input: in that case we need to retrieve the corresponding recipe in sat(P ). As the symbolic labels may not be closed we simply enhance sat(P ) with a recipe X for each variable x (the set K).

To check equivalence between processes we rely on the notion of reachable identity test written RId L1,...,L k (R, R ) where L 1 , . . . , L k are (not necessarily ground) labels and R, R (not necessarily ground) recipes. For a test t we denote by lbl(t) its sequence of labels L 1 , . . . , L k . For commodity reason, we also define a reachability test as: R L1,...,L k =RId L1,...,L k (0, 0).

Given a ground process P and a test t the predicate Ver P (t) checks whether t holds in P . We define Ver P (RId L1,...,L k )(R, R ) to hold when (P, ∅) L1σ,...,L k σ = ====== ⇒ (P , ϕ) and (Rσ = R σ)ϕ where σ is a bijection from vars(L 1 , . . . , L k , R, R ) to fresh names {c 1 , . . . , c n }. Finally the predicate is lifted to protocols and we write Ver P (t) for ∃P ∈ P. Ver P (t).

We note that when Ver P (t) holds and P is positive then Ver P (tσ) holds for any σ, as equality is stable by substitution. However, a disequality may hold when instantiated by distinct fresh names, while a different instantiation may make the test fail.

Next we define the process rm = (P ) which simply removes all inequality tests.

Definition 8. Let P be a process such that

P = P 1 .[t 1 = t 1 ].P 2 . . . . .[t m = t m ]
.P m+1 and P 1 .P 2 . . . . .P m+1 is positive. We define the process rm = (P ) =P 1 . . . . .P m+1 .

Given a process P we define the set of reachable identity tests Test RId (P ).

Test

RId (P ) = {RId L1,...,L k (R, R ) | ri 1 ,..., k (R, R ) ⇐ k u1 (X 1 , x 1 ), . . . , k un (X n , x n ) ∈ sat(rm = (P )), L 1 , . . . , L k = (rec P ( 1 , . . . , k ))σ where σ = {X j → X min{i|xi=xj } | 1 ≤ j ≤ k}, Ver P (RId L1,...,L k (R, R ))}
We also define reachability tests Test R (P ) for a process P :

Test R (P ) = {t | t ∈ Test RId (P ), ∃L 1 , . . . , L k , t = R L1,...,L k }
We note that we can only apply the sat function to positive processes. If P was already a positive process Ver P (t) would hold for each of the constructed tests because of the soundness of sat. However, in general, Ver rm = (P ) (t) may hold while Ver P (t) does not hold, which is why we explicitly test the validity of t in P .

In [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF] it is shown that given a positive ground process P and a positive determinate protocol Q, we have that

P t Q iff ∀t ∈ Test RId (P ). Ver Q (t)
which can be used to check trace inclusion between protocols (as P t Q iff ∀P ∈ P.P t Q) and trace equivalence (as P ≈ t Q iff P t Q and Q t P). This result does however not hold for processes with disequality tests.

Example 4. Let P = in(c, x).out(c, a) and Q = in(c, x).[x = a].out(c, a). We have that P ≈ t Q but all tests that hold on P also hold on Q (and vice-versa). In particular

R in(c,X).out(c) ∈ Test R (P ) holds in Q, as (Q, ∅) in(c,c1).out(c) ========⇒ (0, ϕ) for a fresh name c 1 .
Whenever a test holds on rm = (P ) but not on P , it must be that a disequality test in P did not hold. We therefore compute the complement of a process, which is the set of positive processes which transforms a disequality into an equality and removes remaining disequalities. Lastly, before explaining our algorithm we need to introduce the shrink operator on processes which is used in conjunction with the Inst operators on sequences of labels. Given a process P and a sequence of labels lbl we define a process that only executes instances of lbl (up to test actions which are ignored). In the following we suppose that variables in Y, X and names in N are totally ordered by an order < Y , < X resp. < N .

Definition 10. Let P be a process, lbl a sequence of labels, σ an increasing bijection from vars(lbl) ∩ Y to a set of fresh and pairwise distinct term variable in X , θ an increasing bijection from vars(lbl) ∩ Y to a set of fresh and pairwise distinct names in N , such that (P, ∅) L1θ,...,Lnθ = ====== ⇒ (P , ϕ). Let lbl 0 be the subsequence of lbl obtained by removing all test labels. We define shrink lbl (P ) as shr ∅ lbl0 (P ) where

-shr v lbl ([s ∼ t].P ) = [s ∼ t]
.shr v lbl (P ) for ∼∈ {=, =} -shr v out(c)•lbl (out(c, t).P ) = out(c, t).shr v lbl (P ), -shr v in(c,R)•lbl (in(c, x).P ) = in(c s , X 1 σ). . . . .in(c s , X n σ).in(c, x).[x = Rϕθ -1 σ].shr vars(R)∪v lblσ (P ) where vars(R) ∩ Y \ v = {X 1 , . . . , X n } and X i < X i+1 , -0 otherwise and c s is a dedicated channel not appearing in P .

Note that the function shrink depends on the chosen bijection but this only changes the process up to alpha renaming. Note that we cannot force an execution to contain an instance of a particular recipe R. The inserted test [x = Rϕσ] only ensures that the input of x is produced by some recipe R such that (Rσ = R )ϕ . We therefore additionally add inputs in(c s , x i ) which will allow us to retrieve instance Rθ of R that yields the same protocol message as R.

Definition 11. Let lbl, lbl be sequences of labels. If

in(lbl) = in(c s , R 1 1 ) . . . in(c s , R n1 1 ).in(c 1 , R 1 ). . . . .in(c s , R k 1 ) . . . in(c s , R n k k ).in(c k , R k ); in(lbl ) = in(c 1 , R 1 ). . . . .in(c k , R k ) and vars(R i ) \ j<i vars(R j ) = {X 1 i , . . . , X ni i } with X j i < X j+1 i then we define Inst(lbl, lbl ) = {X j i → R j i | 1 ≤ i ≤ k, 1 ≤ j ≤ n i }. Otherwise Inst(lbl, lbl ) = ⊥.
Example 5. Let P = in(c, x).out(c, 0) be a process and lbl = in(c, Y, 0 ), out(c) a sequence of labels. Consider two bijections σ = {Y → y} and θ = {Y → a}. The process shrink lbl (P ) = in(c s , y).in(c, x).[x = y, 0 ].out(c, 0) allows to identify the recipes Y such that (P, ϕ) lblσ --→ (P , ϕ ). Indeed, assume Test R (shrink lbl (P )) contains r = R in(cs,h(0)).in(c, h(0),0 .out(c) , then rτ = R in(c, h(0),0 .out(c) where τ = Inst(lbl, lbl(r)) is such that Ver rτ (P ) and lbl(rτ ) is an instance of l.

The algorithm Equiv for verifying trace equivalence on determinate processes is detailed in Algorithm 1.

Theorem 2. Let P and Q be two determinate protocols. Then we have that

P ≈ t Q iff Equiv(P ≈ t Q)
The algorithm proceeds as follows. For each P ∈ P we check whether all traces of P are included in Q. For this we compute the set Rid P of reachable identity tests that hold in P and that need to be checked on Q. We next pick a test rid from the set (and remove it from the set, denoted rid := pop(Rid P )) and check whether this test holds for some process Q in Q. If this is not the case we violate trace equivalence. Otherwise we need to perform additional checks: indeed even if the test rid holds, an instance of rid might not hold on Q but still hold in P . Consider the following simple example:

P = in(c, x).out(c, a) Q 1 = in(c, x).[x = a].out(c, a) Q = {Q 1 , Q 2 } Q 2 = in(c, x).[x = a].out(c, a)
5 Implementation and case studies 5.1 The AKISS tool

In addition to parallel composition P Q and conditionals AKISS also supports nondeterministic choice P ++ Q, sequences P :: Q and phases P > > Q, which are convenient for defining complex scenarios under which we analyse protocols. A sequence P :: Q contains all sequences of a trace of P followed by a trace of Q while the set of traces for a phase P > > Q contains all traces made of the beginning of a trace of P followed by a full trace of Q.

We model unlinkability for two sessions in each of the protocols below as follows:

P 1 A > > P 2 A ≈ P 1 A > > P 2 B
The attacker first interacts with a first session of protocol P executed by A, denoted P 1 A . Then, in a new phase he interacts with a second session of the protocol, which is either executed by A (process P 2 A ) or by B (process P 2 A ). The protocol P satisfies unlinkability if the two scenarios cannot be distinguished. Note that the use of the phase operator is preferable to the sequential composition, as an attacker may not be able to finish the first session completely before starting the second session.

The implementation of the tool and the files corresponding to our case studies are freely available at https://github.com/akiss/.

The AKA protocol

Unlike the simplified version of AKA described in Figure 1, the actual AKA protocol [START_REF] Gazeau | Automated analysis of equivalence properties for security protocols using else branches (extended version)[END_REF] provides a mechanism against replay attacks. In addition to the mac value, both the network and the mobile station store a counter SQN used as a timestamps: each time the network station starts a session with a same mobile station, it sends in addition to the random value and the mac an obfuscated message SQN ⊕ k IM SI containing the incremented value of the counter. The mobile stores the maximum value which has been received. If the received value is not strictly greater than this maximum, the mobile sends a synchronization error message. Otherwise it updates the stored value.

Unlinkability is modelled as explained above: in a first session a mobile station A interacts with the network station and in a second session either mobile A or mobile B interact with the network station. The AKISS tool does not allow for comparison of integer. Instead we just check that the sent value was not the same as a previous one. Therefore during the first phase, since there was no SQN value sent to the mobile there is no need to perform a check while in the second session of the mobile A (in the first scenario) we check that the new SQN value is distinct from the first time.

Using the AKISS tool we find the (previously known) attack consisting of observing the first phase and sending the network station's message of the first phase in the second one: if the second phase is with the same mobile station then it sends a synchronization error message while if its another mobile station it sends a mac error message. Running our tool on a 30 core Intel(R) Xeon(R) CPU E5-2687W v3 @ 3.10GHz, the attack is found in 3 minutes.

Unlinkability on some other protocols

We also analysed the Basic Access Control (BAC) protocol [START_REF]Machine readable travel documents[END_REF], the Private Authentication Protocol (PAP) [START_REF] Abadi | Private authentication[END_REF] and two RFID protocols [START_REF] Van Deursen | Attacks on RFID protocols[END_REF]: LAK and SLK.

All these protocols use else branches to send error messages except for the LAK RFID protocol. However, even though this protocol does not contain branches, the scenarios required for expressing unlinkability does requires the use of an else branch for the key update. Indeed, when a session succeeds, the key is updated for the next session, while the previous key is reused in case of failure. This results into an if then else structure. Finally, for the SLK and LAK protocols where both the tag and the reader update their data, the scenarios to consider for two sessions are the following. The roles with index u model the role with a preliminary update if test then R else R where R is R with updated values. As the update test is not defined before all inputs have been received, we introduce R a for each role R to be the process where the last input and the update test are missing (and moreover the construct R > > 0 allows the adversary to stop that instance of the role even earlier): in this case, the update will not happen anyway. Therefore, our scenario has four cases depending on whether the tag, the reader, both or none have reached the update test or not. The scenario where the instances of the tags corresponds to different tag is similar. Note that as we consider a different tag in the second session we do not need to worry whether T ag A was updated or not. The AKISS tool establishes the equivalence for PAP in 4s. It finds known attacks on BAC in 1m30, on SLK in 6s and in 7h for LAK. The much longer time for LAK is due to the particular use of xor which leads to complex unifiers.

Conclusion

In this paper we present an extension of AKISS which allows automated verification of protocols with else branches. An appealing aspect of our approach is that we do not modify the saturation procedure underlying the AKISS tool. As a result we obtain a new decidability result for the class of subterm convergent equational theories and an effective automated analysis tool. We have been able to analyse several protocols including the AKA protocol, and RFID protocols which require both support for xor and else branches.

  When = test we define = ⇒ to be test --→ * -→ test --→ * and we lift -→ and = ⇒ to sequences of actions. Given a protocol P, we write (P, ϕ) 1,..., n -----→ (P , ϕ ) if there exists P ∈ P such that (P, ϕ) 1,..., n

1

  ,..., n = ==== ⇒ (P, ϕ), and (P, ∅) 1 ,..., n = ==== ⇒ (P , ϕ ), then for any test R 1 ?

P

  same = ((T ag Aa Reader a ) > > (T ag A Reader)) ++ ((T ag A (Reader a > > 0)) :: (T ag Au Reader)) ++ (((T ag Aa > > 0) Reader) :: (T ag A Reader u )) ++ ((T ag A Reader) :: (T tag Au Reader u ))

  Pdiff = ((T ag A Reader a ) > > (T ag B Reader)) ++ (((T ag A > > 0) Reader) :: (T ag B Reader u ))

  there exists t such that (P0, ϕ0) |= k 1 ,..., n (R, t) and (P0, ϕ0) |= k 1 ,..., n (R , t) (P0, ϕ0) |= ri 1 ,..., n (R, R ) if (P0, ϕ0) |= r 1 ,..., n and (P0, ϕ0) |= i 1 ,...,

n (R, R )

  Definition 9. Let P be a process such that P = P 1 .[t 1 = t 1 ].P 2 . . . . .[t m = t m ].P m+1 and P 1 .P 2 . . . . .P m+1 is positive. We define the complement of P , comp(P ) to be the set {P 1 .P 2 . . . . .P i-1 .[t i = t i ].P i . . . . .P m .P m+1 |1 ≤ i ≤ m} We easily see that we have the following property. Lemma 1. Let P be a process and t a test. We have that Ver rm = (P ) (t) iff either Ver P (t) or Ver comp(P ) (t)

The research leading to these results has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreements No 645865-SPOOC), as well as from the French National Research Agency (ANR) under the project Sequoia.

Algorithm 1: Decision procedure for P ≈ t Q Function Check(P, Q)

Input: Process P , protocol Q Output: Boolean RidP := Test RId (P ); while RidP = ∅ do rid := pop(RidP ); Note that P ≈ t Q. Let rid = RId in(c,X).out(c) (a, a). This test holds in Q 1 . However, the more instantiated test RId in(c,a).out(c) (a, a) would not hold. (Note that the test may actually only fail because reachability is violated.) We therefore need to identify the instances of rid Q 1 that do not hold on Q 1 . The process shrink Q (lbl(rid)) defines the process that only verifies instances of rid. Computing its complement defines the processes that verify the instances of rid that are not verified by Q: in our example we would identify the test r = R in(c,a).out(c) , as computing the complement transforms

. Finally, we check whether r is verified by P . If this is the case, we add the more instantiated test RId in(c,a).out(c) (a, a) to the set Rid P of tests to be checked. We note that the fact that Q 1 does not verify r, but P does is not yet a violation of trace equivalence: another trace in Q may well verify the instantiated test.

In our example, indeed the process Q 2 verifies RId in(c,a).out(c) (a, a). Theorem 2 above ensures partial correctness, i.e., soundness and completeness. We now state that total correctness only depends on the termination of sat. Theorem 3. If procedure sat terminates then procedure Equiv terminates.

As it was shown in [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF], termination of sat is ensured for a wide class of subterm convergent equational theories. While sat may not terminate in general on other theories such as xor, or blind signatures, the tool does terminate in practice on a wide range of examples [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF][START_REF] Baelde | Symbolic verification of privacy-type properties for security protocols with XOR[END_REF] (and Theorem 2 ensures the correctness of the result).