David Baelde

Stéphanie Delaune

Charlie Jacomme

Adrien Koutsos

Solène Moreau

Solène Moreau An Interactive

An Interactive Prover for Protocol Verification in the Computational Model

Keywords: Security Protocols, Formal Methods, Observational Equivalence, Computational Security, Interactive Theorem Prover

établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

An Interactive Prover for Protocol Verification in the Computational Model David Baelde * , Stéphanie Delaune † , Charlie Jacomme ‡ , Adrien Koutsos § and Solène Moreau †

I. INTRODUCTION

Given the importance and difficulty of designing secure communication protocols, computer scientists have strived to provide solid mathematical foundations, formal methods and tools for the computer-aided verification of security protocols.

A successful approach in this line of research is to model cryptographic messages as formal terms subject to some equational theory representing attacker capabilities. Originally proposed by Dolev and Yao [START_REF] Dolev | On the security of public key protocols (extended abstract)[END_REF], this idea has been refined over the years, resulting in a variety of so-called symbolic models, based, e.g., on the applied pi-calculus [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF] or multiset rewriting [START_REF] Mitchell | Multiset rewriting and security protocol analysis[END_REF]. These models capture large classes of attackers and allow the automated verification of protocols. This has lead to tools such as PROVERIF [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF], TAMARIN [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF], DEEPSEC [START_REF] Cheval | The DEEPSEC prover[END_REF] and others [START_REF] Armando | The AVISPA tool for the automated validation of internet security protocols and applications[END_REF], [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF], [START_REF] Cortier | Equivalence properties by typing in cryptographic branching protocols[END_REF], [START_REF] Escobar | Maude-NPA: Cryptographic protocol analysis modulo equational properties[END_REF], which have

We would like to thank Bruno Blanchet and Benjamin Grégoire for their interactions and helpful guidance for using CRYPTOVERIF and EASYCRYPT. 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 agreement No 714955-POPSTAR), as well as from the French National Research Agency (ANR) under the project TECAP.

been used to prove the security of widely deployed protocols, e.g. [START_REF] Basin | A formal analysis of 5G authentication[END_REF], [START_REF] Bhargavan | Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF], [START_REF] Cremers | A comprehensive symbolic analysis of TLS 1.3[END_REF].

To discuss the general principle and limitations of the symbolic model, let us consider a simple protocol where a tag (role T ) with identity id carrying its own hashing key k is authenticated by a reader (role R) that has access to a database of legitimate pairs id, k : R → T : n T → R : id ⊕ H(n, k) In words, the reader sends a random number n and, when receiving a reply, verifies that there is some id, k in its database such that the reply is the identity id XORed with the hash of n using the key k. To verify that an attacker cannot impersonate a tag with data id 0 , k 0 , we need to check that the attacker cannot derive a message that the reader would accept, whatever knowledge they may have obtained from previous interactions. Assuming for simplicity two identities id 0 and id 1 , and that the attacker is only active during its last interaction, we have to verify that, for distinct names (n j ) 0≤j≤p , and for any i 1 , . . . , i p ∈ {0, 1}, there is no context C made of public function symbols such that:

C[n j , id ij ⊕ H(n j , k ij )] 1≤j≤p = E id 0 ⊕ H(n 0 , k 0 )
where = E is equality modulo a relevant equational theory. Rephrased like this, the problem may be solved using rewriting techniques such as unification, itself based on completion or variant computation [START_REF] Comon | The finite variant property: How to get rid of some algebraic properties[END_REF], [START_REF]Handbook of Automated Reasoning[END_REF]. However, the equational theory E would need to contain equations reflecting the algebraic properties of XOR which are typically problematic for these techniques. In fact, PROVERIF and DEEPSEC do not support XOR, and TAMARIN only provides limited support for it. Supporting primitives with rich algebraic properties (e.g., blind signatures, exponentiation, XOR) is probably the main challenge that these tools are currently facing.

An obvious limitation of the symbolic model is that it can only be used to find logical flaws in protocols, e.g. man-inthe-middle [START_REF] Lowe | An attack on the Needham-Schroeder public-key authentication protocol[END_REF] or reflection attacks [START_REF] Basin | Provably repairing the ISO/IEC 9798 standard for entity authentication[END_REF]. Indeed, security in the symbolic model is weaker than the cryptographer's standard security notion, based on a computational model where adversaries are arbitrary probabilistic polynomial-time (PTIME) Turing machines. As an illustration, nonces are modelled in the computational model as long bitstrings that are drawn uniformly at random. Two nonces correspond to the same probability distribution, and are thus indistinguishable, but the probability that two distinct nonces take the same value is negligible. The attacker may guess a bit of a nonce but has a negligible probability of guessing the whole nonce. In the symbolic model, distinct names are indistinguishable and are not equal modulo E, but the partial guessing of a nonce cannot be modelled: a name is either known or unknown to the attacker. Significant research efforts have been done to get the best of both worlds through the development of computational soundness results, but unfortunately they only apply under strong hypotheses, and have modularity issues [START_REF] Abadi | Reconciling two views of cryptography (the computational soundness of formal encryption)[END_REF], [START_REF] Cortier | A survey of symbolic methods in computational analysis of cryptographic systems[END_REF], [START_REF] Cortier | A composable computational soundness notion[END_REF].

In [START_REF] Bana | Towards unconditional soundness: Computationally complete symbolic attacker[END_REF], [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF], Bana and Comon have proposed a new approach to security proofs, which they call computationally complete symbolic attacker (CCSA). It relies on the symbolic setting of first-order logic, but avoids the limitations of the symbolic models mentioned above. Instead of modelling attacker capabilities using rules stating what the adversary can do, their method relies on the specification of what the attacker cannot do. Starting from the security properties of cryptographic primitives, they derive some axioms expressing which pairs of sequences of messages are indistinguishable. They show that their axioms are sound w.r.t. the interpretation of terms as probabilistic PTIME Turing machines. Therefore, a proof of a security property from these axioms implies security in the computational model under the initial cryptographic assumptions. This approach has been demonstrated on various protocols to obtain formal proofs of security [START_REF] Bana | Computationally complete symbolic attacker in action[END_REF], [START_REF] Bana | Formal analysis of vote privacy using computationally complete symbolic attacker[END_REF], [START_REF] Comon | Formal computational unlinkability proofs of RFID protocols[END_REF], [START_REF] Koutsos | The 5G-AKA authentication protocol privacy[END_REF], [START_REF] Scerri | Analysis of key wrapping APIs: Generic policies, computational security[END_REF]. Going back to our example, authentication would be expressed more abstractly as: EQ(att(frame), id 0 ⊕ H(n 0 , k 0 )) ∼ false, where frame def = n 1 , id i1 ⊕ H(n 1 , k i1 ), n 2 , id i2 ⊕ H(n 2 , k i2 ), . . . .

Here, the binary function symbol EQ is interpreted as bitstring equality, and ∼ as indistinguishability. The function symbol att stands for an arbitrary probabilistic PTIME computation performed by the attacker, taking past messages as input.

Intuitively, the overall statement expresses that there is a negligible probability that att(frame) yields a message that the reader would accept. It can be proved using just two axioms: first, we use the properties of XOR to obtain an equality between H(n 0 , k 0 ) and id 0 ⊕ att(frame); second, assuming that the keyed hash function satisfies existential unforgeability under chosen message attack (EUF-CMA), we conclude that this equality is false with overwhelming probability given that the message n 0 is fresh and has thus not been hashed in frame.

In contrast with the treatment of our example in the symbolic model, the CCSA approach yields a proof that is immediately relevant in the standard model of probabilistic PTIME machines and which relies on explicit and standard cryptographic assumptions. Finally, applying the axioms did not require complex rewriting techniques: we only had to verify a simple equality involving XOR, and never had to consider all possible contexts as in the symbolic model.

Two problems prevent a more widespread use of the CCSA approach. First, it is limited to bounded executions: given a protocol and a bound on its execution traces, one can derive a series of indistinguishability goals that need to be (separately) proved to guarantee the security of the protocol. Second, proofs are manual: proving a non-trivial goal in detail is tedious; proving all the goals resulting from all possible executions is not manageable. Works on decision procedures remain of limited use so far, as they are limited to trace properties [START_REF] Hubert Comon-Lundh | Tractable inference systems: An extension with a deducibility predicate[END_REF] (e.g. secrecy, authentication) or a very restrictive set of axioms [START_REF] Koutsos | Decidability of a sound set of inference rules for computational indistinguishability[END_REF].

Contributions: In this paper, we elaborate on the CCSA approach to solve these two problems. Our first contribution, presented in Sections III and IV, is a meta-logic over the base logic of Bana and Comon [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF]. In the base logic, one has to separately prove a family of indistinguishability goals, one for each possible protocol execution within a given bound. Formulas of our meta-logic express properties of all execution traces of a protocol, which allows to capture the family of base logic goals as a single formula. Security properties expressed in our meta-logic have the standard computational meaning, and provide guarantees for an arbitrary number of sessions that does not depend on the security parameter (this is discussed in detail in Section IV-C).

We then design proof systems for deriving security properties expressed as meta-logic formulas, in part by lifting base logic axioms. We consider both trace properties, which are useful to model authentication properties, and equivalence properties, which allow to express privacy properties such as anonymity and unlinkability. Our meta-logic enables useful interaction between the two kinds of properties. For instance, in several of our case studies, we establish unlinkability by proving en passant an authentication property. This second contribution is developed in Sections V and VI.

Our third contribution is the implementation of the interactive prover SQUIRREL [START_REF]The Squirrel Prover repository[END_REF], which allows to reason on protocols specified in an applied pi-calculus using our framework. Thanks to basic automation techniques coming from first-order logic, we have been able to carry out several case studies using this tool. These results, presented in Section VII, cover a variety of primitives (hashes, signatures, Diffie-Hellman exponentiation, encryption) and security properties (authentication, strong secrecy, unlinkability). Although this is not our primary goal, some of the proofs obtained here are firsts.

Related Work:

We have already discussed the limitations that are inherent to symbolic models, and now focus on tools which provide guarantees in the computational model. Several such systems exist, based on different approaches. For instance, CRYPTOVERIF [START_REF] Blanchet | A computationally sound mechanized prover for security protocols[END_REF] proofs are based on highlevel game transformations, EASYCRYPT [START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF] is built on a general-purpose probabilistic relational Hoare logic which can be used to formalize most pen-and-paper cryptographic proofs, and CRYPTHOL [START_REF] Basin | CryptHOL: Game-based proofs in higher-order logic[END_REF] goes even further by embedding the computational model in the proof assistant Isabelle/HOL. Finally, F [START_REF] Bhargavan | Everest: Towards a verified, drop-in replacement of HTTPS[END_REF] is a general-purpose program verification framework which can be used (via external arguments) to provide computational security guarantees. The various ap-proaches can be compared on several criteria [START_REF] Barbosa | SoK: Computeraided cryptography[END_REF]; we mention a few to highlight differences with our tool.

Like CRYPTOVERIF, our protocol specifications are given in the applied pi-calculus, although our language is less detailed and does not provide a link with implementations. The strongest tools for verifying implementations remain EASYCRYPT and, chiefly, F .

Unlike EASYCRYPT and CRYPTOVERIF, we only provide asymptotic security bounds. Our approach hides from the user all quantitative aspects such as probabilities and the security parameter and, on the surface, our tool is as simple as symbolic verification frameworks. In contrast, EASYCRYPT users often have to carry out probabilistic reasoning, and come up with complex security bounds, which can result in long proofs. Such aspects are automated in CRYPTOVERIF. In general, the current level of automation of our tool sits somewhere between EASYCRYPT and CRYPTOVERIF.

The most important difference between our tool and earlier ones is the associated proof methodology: CRYPTOVERIF relies on game transformations and EASYCRYPT performs Hoare-style proofs of programs, while we reason over execution traces of protocols. Our proofs are akin to TAMARIN's backward reachability analysis, driven e.g. by our unforgeability tactic. We give in Appendix E an in-depth comparison with EASYCRYPT and CRYPTOVERIF, based on the analysis of the Basic Hash protocol in the three tools.

II. OVERVIEW

In this section, we give an overview of our framework and tool, using as a running example the Basic Hash protocol. The SQUIRREL prover and our case studies can be found in [START_REF]The Squirrel Prover repository[END_REF].

Example 1. We consider the Basic Hash protocol as described in [START_REF] Brusò | Formal verification of privacy for RFID systems[END_REF], which is an RFID protocol involving multiple tags and readers. Each tag stores a secret key that is never updated, and the readers have access to a shared database containing all these keys. The protocol is as follows:

T → R : n, H(n, key) .

Here, n is a fresh name and key is the secret key. When receiving a message, the reader checks that it is a pair whose second component is a hash of the first component using one of the keys from the database. system (!j R: reader(j) | !i !j T: tag(i,j)).

Listing 1. Basic Hash protocol in SQUIRREL

Listing 1 shows a formal description of the Basic Hash protocol written in the input language of our tool, which is close to the classical applied pi-calculus. More specifically, we consider a scenario featuring several reader sessions with access to the database, and several tags where each tag can play multiple sessions. The try find instruction encodes the database lookup performed by the reader: the then branch is executed with some value of i for which the required condition holds, if any such i exists, otherwise the else branch is executed.

We now describe informally how to instantiate our framework to analyze this protocol -in practice, our tool performs this instantiation automatically from the applied pi-calculus specification. We consider a set of actions representing each step of the protocol: T[i, j] is the action performed by the j th session of tag i, R[j, i] represents the action of a reader session j when it has found a value i for which the second component of its input is a hash of its first component with key[i], and R1[j] represents the action of a reader session j when no such i can be found.

Using the user syntax, we now express an authentication property on the Basic Hash protocol.

goal auth :

forall (i:index, j:index), cond@R(j,i) ⇒ exists (j':index), T(i,j') < R(j,i) && fst(input@R(j,i)) = fst(output@T(i,j')) && snd(input@R(j,i)) = snd(output@T(i,j')).

Listing 2. Reachability goal in SQUIRREL

Here cond@R[j, i] is a macro which stands for the executability condition of action R[j, i], where the reader recognizes a valid input message w.r.t. some key key[i]. Our authentication goal expresses that, whenever this condition holds, there must be some session j of tag i (the one using key[i]) that has been executed before R[j, i]. Moreover, the output of the tag's action coincides with the input of the reader's action. We may note that we express this correspondence on each projection. Indeed, for some implementations of the pairing primitive, the equality of projections does not imply the equality of pairs. This authentication goal can be proved in our tool using a succession of four tactics: simpl. expand cond@R(j,i). euf M0. exists j1.

The first tactic simply introduces variables i and j and the assumption cond@R[j, i] identified by M0. The second tactic expands this macro into its meaning, i.e.

snd(input@R[j, i]) = H(fst(input@R[j, i]), key[i]).
We then use the EUF-CMA assumption: the condition states that if snd(input@R[j, i]) is a valid hash of fst(input@R[j, i]), thus the term fst(input@R[j, i]) must be equal to a message that has previously been hashed, i.e. some m such that H(m, key[i]) appears in snd(input@R[j, i]) or fst(input@R[j, i]). Actually, input@R[j, i] refers to all messages outputted so far in the execution, and the only hashed messages outputted by the protocol with the key key[i] are the names n[i, j] (note that n is parametrized by i and j since it has been generated below the replications indexed by i and j). Therefore we deduce that there exists a tag's session j 1 occurring before the action R[j, i] such that n[i, j 1 ] = fst(input@R[j, i]). We conclude by instantiating the existential quantification over j by j 1 .

Our framework does not only provide a proof system for trace properties, but also allows to prove equivalence properties. For illustration purposes, let us consider the following unlinkability property for the Basic Hash protocol: we want to prove that a scenario where a tag with identity i can play many sessions is indistinguishable to a scenario where each tag with identity i can play only one session. To this end, we make use of bi-processes with diff terms (as done e.g. in PROVERIF [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF] or TAMARIN [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF]), and we replace in the protocol specification given in Listing 1 every key[i] with diff(key [i], key [i, j]). On the left side of the bi-process, the key is the same for all sessions of the tag with identity i, whereas on the right side each session j of the tag with identity i uses a new key.

We can then prove that the two projections of this biprocess are observationally equivalent. The proof proceeds by induction: we show that indistinguishability holds between the left and right-hand side's frames at any point of any trace, assuming that the same holds for the previous points. We then consider the three possible actions of the processes. For an action T[i, j], we use the PRF assumption on the hash function to replace the hashes of the fresh messages H(n[i, j], . . .) by fresh names; we can then conclude since indistinguishability is preserved by the addition of fresh names on both sides. For a reader's action R[j, i], we must show the equivalence (upto negligible probability) between the conditions of the action for the two projections of our bi-process. This is an immediate consequence of the previous authentication property (and its obvious converse) which holds for our two projections. The case of actions R1[j] is handled similarly.

III. MODELLING PROTOCOLS -SYNTAX

In this section, we introduce the syntax of our metalogic, which is an extension of the base logic of [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF] with timestamps, indices and macros, before describing how to use it to model protocols. Along this section, we illustrate our notions using the Basic Hash protocol introduced in Section II.

A. Meta-Logic

Syntactically, our meta-logic is a many-sorted first-order logic. Terms of the meta-logic (meta-terms) are of three possible sorts:

• terms of sort message represent bitstrings manipulated and exchanged by protocol's participants; • terms of sort timestamp represent time points in an execution trace of a protocol; • terms of sort index are used to identify unbounded collections of objects, e.g. sessions of a role or items in a database. We assume three infinite sets of variables: X (whose elements are noted x, y, z) for message variables; I (whose elements are noted i, j) for index variables; T (whose elements are noted τ ) for timestamp variables.

T := τ | init | a[i 1 , . . . , i k ] | pred(T ) t := x | n[i 1 , . . . , i k ] | f[i 1 , . . . , i k ](t 1 , . . . , t n ) | input@T | output@T | frame@T | if φ then t else t | find i suchthat φ in t else t A := t = t | i = i | T = T | T ≤ T | cond@T | exec@T φ := A | | ⊥ | φ ∧ φ | φ ∨ φ | φ ⇒ φ | ¬φ | ∀i.φ | ∃i.φ | ∀τ.φ | ∃τ.φ
We assume a set F of indexed function symbols (used to model encryptions, pairs, . . . ). Each of these symbols comes with an index arity as well as a message arity: if f ∈ F has index arity k and message arity n, then for all index variables i 1 , . . . , i k and meta-terms t 1 , . . . , t n , we have that

f[i 1 , . . . , i k ](t 1 , . . . , t n ) is a meta-term.
Example 2. Function symbols representing cryptographic primitives will have index arity 0, and a message arity depending on the kind of primitive. For instance, we use H of message arity 2 to model a keyed hash, •, • of message arity 2 to model concatenation, and fst (resp. snd) of message arity 1 to model the first (resp. second) projection. Function symbols representing identities (for example, a constant value associated to each tag) have 0 as message arity and 1 (or even more) as index arity.

We assume a set N of indexed name symbols (modelling random samplings of length η, the security parameter) and a set of indexed action symbols A (modelling specific timestamps). These indexed symbols only have an index arity: they cannot be applied to meta-terms.

Example 3. To model the Basic Hash protocol in our framework, we consider two names key, n ∈ N : key has index arity 1, and key[i] models the key associated to the tag i; n has index arity 2, and n[i, j] represents the name used by the session j of the tag i. Regarding actions symbols we let A be the set of three indexed action symbols: a T and a R of index arity 2 and a R1 of index arity 1. These action symbols correspond to what is called T, R, R1 in Section II. Definition 1. Given a meta-logic signature Σ = (F, N , A) and some sets of variables X , I and T , we give in Fig. 1 the syntax of meta-terms of sort message (noted t) and timestamp (noted T ), and the syntax of meta-formulas (noted φ). The only meta-terms of sort index are index variables.

For any meta-term t, we let st(t) and fv(t) be, resp., the set of subterms of t and the free variables of t of any sort.

Note that meta-terms and meta-formulas are mutually inductive, due to conditional and lookup constructs in terms. Lookups generalize conditionals: find i suchthat φ in t else t evaluates to t where indices i are bound to values such that φ holds if such values exist, and t otherwise. Again, this lookup construct can be computed thanks to the finiteness of the domain of interpretation of indices. The special timestamp constant init stands for the initial time point.

A key ingredient of our meta-logic are macros, which are used to refer to protocol executions. We have message macros input@T and output@T to refer to the input and output messages of the action executed at time T . The macro frame@T represents all the information available to the attacker at that time: essentially, it is the sequence of all output messages from the start of the protocol until time T . We also have boolean macros cond@T and exec@T which respectively encode the execution condition of the action at time T and the conjunction of all such conditions until time T .

B. Protocols as Sets of Actions

We model a protocol as a finite set of actions. Each action represents a basic step of the protocol where the attacker provides an input, a condition is checked, and finally an output is emitted. Formally, an action is defined by an action symbol identifying it, and an action description giving its semantics. Actions are indexed, allowing for unbounded executions. An action a[i 1 , . . . , i k ].(φ, o) models that o will be emitted provided that φ holds, but does not specify a failure case. Conditional branching may be modelled using two actions: one with the condition for the positive branch, and one with the negation of the condition for the negative branch. Alternatively, a single action with a trivial condition may be used, and an output term that performs the conditional branching. As we shall see, actions are chosen by the attacker, hence the second option gives less power to the attacker.

A protocol is a set of actions equipped with a dependency relation, which constrains the order of execution of actions. Definition 3. Given a finite set A of action symbols, a protocol P = (P A , <) over A is a finite set P A of actions, one for each action symbol, equipped with a partial order < over terms of the form a[ i] with a ∈ A. We require that:

• < is insensitive to the choice of specific index variables: Intuitively, an action can refer to its own input, and can otherwise only refer to timestamps corresponding to actions that occur strictly before it. We derive ≤ from < as usual: α ≤ β when α < β or α = β. Example 5. We model the Basic Hash protocol in our framework using a set of three actions with an empty dependency relation:

a[i 1 , . . . , i k ] < a [j 1 , . . . , j k ] iff a[σ(i 1 ), . . . , σ(i k )] < a [σ(
a T [i, j].
,

n[i, j], H(n[i, j], key[i]) a R [j, i]. snd(input@a R [j, i]) = H(fst(input@a R [j, i]), key[i]), ok a R1 [j]. ∀i. snd(input@a R1 [j]) = H(fst(input@a R1 [j]), key[i]) , error
We can instantiate the indices of an action by concrete values to yield concrete actions, which represent distinct copies of the original action. Definition 4. Given a set A of action symbols, a concrete action is an action symbol a ∈ A applied to k integers (where k is the index arity of a). The partial order of a protocol P = (P A , <) is lifted to concrete actions in the natural way: for any mapping σ :

I → N, a[σ(i 1 ), . . . , σ(i k )] < b[σ(j 1 ), . . . , σ(j l )] holds when a[i 1 , . . . , i k ] < b[j 1 , . . . , j l ].
Finally, for a given protocol, we can consider its possible interleavings, e.g. the possible sequences of actions that are compatible with its dependency relation. Definition 5. Given a protocol P = (P A , <), an interleaving is a sequence of concrete actions α 1 . . . α n in which no concrete action occurs twice, and such that, for every 1 ≤ i ≤ n, for every concrete action β such that β < α i , there exists 1 ≤ j < i such that β = α j .

The constraints on interleavings are necessary but insufficient conditions for a sequence of concrete actions to be executable. The actual executability of an interleaving will be a probabilistic notion, and will depend on the implementation of cryptographic primitives. It is addressed in the next section.

Example 6. Going back to the simple protocol introduced in Example 4, we have concrete actions a

[1], b[1], a[2], b[2], . . . with a[1] < b[1], a[2] < b[2], . . . indicating that, in each session, b has to occur after a. The sequence a[2] a[1] b[1] b[2] is an interleaving, but a[2] a[1] b[1] b[2] a[2], and b[2] a[1] b[1] a[2] are not.
Note that our notion of dependency ordering can be used to impose phase constraints: declaring a

[i] < b[j] imposes that, in all interleavings, any concrete actions a[k 1 ] is executed before all concrete actions b[k 2 ].
In the tool, such extra constraints can be specified with an axiom, as follows: [START_REF] Abadi | Reconciling two views of cryptography (the computational soundness of formal encryption)[END_REF][START_REF]IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques[END_REF], and a R1 [START_REF] Abadi | Reconciling two views of cryptography (the computational soundness of formal encryption)[END_REF] are concrete actions with no dependency. Some possible interleavings are:

axiom phase: forall(i,j:index), a(i) < b(j). Example 7. Continuing our running example, a T [1, 1], a T [1, 2], a T [2, 1], a R
1

) a T [1, 2] a R [3, 1]; 2) a T [1, 2] a R [3, 1] a R1 [3]; 3) a R [3, 1] a T [1, 2] a T [1, 3].
The first interleaving corresponds to an honest execution. First, a tag (with id 1) executes its action (for session id 2). Then, the reader (session id 3) executes its first action for i = 1, i.e. it recognizes a valid input w.r.t. key [START_REF]IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques[END_REF] of the tag with id 1.

The second interleaving does not correspond to any real execution since the conditions of actions a R [3, 1] and a R1 [START_REF] Abadi | Reconciling two views of cryptography (the computational soundness of formal encryption)[END_REF] could not be satisfied simulatenously.

The third interleaving is also not executable: it represents an execution in which the reader (session id 3) recognizes a valid input from tag 1 before any output from tag 1.

As mentioned before, our tool takes as input a protocol specification expressed in a fragment of the applied pi-calculus, and automatically translates it to a protocol according to Definition 3. The translation is rather straightforward but its description and the study of its semantic properties are outside the scope of this paper.

IV. SEMANTICS

The semantics of our meta-logic is given through a translation from the meta-logic to the base logic of [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF]. We recall the semantics of the base logic in Section IV-A before defining the translation in Section IV-B.

A. Base Logic

We briefly recall the key definitions of [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF], considering only the sort message, and a single attacker symbol att. We do not rely on the way [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF] encodes protocol equivalence into the logic (using a so-called folding operation) but only need the core logic for reasoning about computational indistinguishability of sequences of messages.

Syntax:

The base logic is a first-order logic, in which terms represent probabilistic PTIME Turing machines producing bitstrings, and a single predicate ∼ represents computational indistinguishability. A key idea of the CCSA approach is to use a special attacker function symbol att to represent the attacker's computations, which is left unspecified to model the fact that the attacker may perform any arbitrary probabilistic PTIME computation. The logic is parameterized by a set N B of name symbols, a set of variables X B , and a set of function symbols F B . Terms are generated from X B and N B using the unary function symbol att and the function symbols of F B . We assume that F B contains at least the following symbols, with the expected arities and usual notations:

• pairing _, _ , equality EQ(_, _); • constants empty, true and false;

• conditionals if _ then _ else _. We do not use a predicate symbol for equality in the base logic: EQ(u, v) is a term and we may write, for instance, EQ(true, EQ(u, v)). We allow ourselves to use the same notations for some constructs in the meta-logic and base logic, because our translation is homomorphic w.r.t. them.

Atomic formulas are of the form u 1 , . . . , u n ∼ v 1 , . . . , v n where n ≥ 0 and u 1 , . . . , u n , v 1 , . . . , v n are terms, and represent indistinguishabilities between two experiments.

Semantics: We are interested in the interpretation of formulas of the base logic in a specific class of first-order interpretations, called computational models. The domain of a computational model M is the set of PTIME Turing machines receiving as inputs the security parameter η in unary (1 η ) and a pair ρ = (ρ s , ρ r ) of random tapes (the complexity is w.r.t. the security parameter, not the random tapes). The tape ρ s is used to draw honestly generated random values, and is not directly accessible by the attacker, and ρ r is used for random values drawn by the attacker. The interpretation [[t]] of a term as a Turing machine is defined as follows.

• Each name n ∈ N B is interpreted as a machine that extracts a word of length η from ρ s , such that different names extract disjoint parts of the tape. • The symbols empty, true, false, EQ and if _ then _ else _ are interpreted in the expected way. E.g., for any terms

t 1 , t 2 , [[EQ(t 1 , t 2 )]] is the Turing machine that, on input (1 η , ρ), returns 1 if [[t 1 ]] and [[t 2 ]
] return the same result:

[[EQ(t 1 , t 2 )]](1 η , ρ) = 1 if [[t 1 ]](1 η , ρ) = [[t 2 ]](1 η , ρ) 0 otherwise
• The other function symbols in F B are interpreted as arbitrary PTIME Turing machines that do not access the random tapes. When studying a specific protocol, we restrict computational models according to the assumptions the protocol relies on: e.g. we may assume that a binary function symbol ⊕ is interpreted as exclusive or, that a binary function symbol H is interpreted as a PRF keyed hash function, . . . • The symbol att is interpreted as a PTIME Turing Machine that does not access the random tape ρ s , but has access to ρ r . Finally, the predicate ∼ is interpreted as computational indistinguishability (noted ≈), where d 1 , . . . , d n ≈ d 1 , . . . , d n when for any PTIME Turing machine A,

| Pr(ρ : A(d 1 (1 η , ρ), . . . , d n (1 η , ρ), ρ r ) = 1)- Pr(ρ : A(d 1 (1 η , ρ), . . . , d n (1 η , ρ), ρ r ) = 1) | is negligible in η.
We write M |= φ when the base formula φ is satisfied in the computational model M, and we say that φ is valid if it is satisfied in any computational model.

Example 8. Assume that n and m are two distinct names. The formulas n ∼ m and EQ(n, m) ∼ false are valid: indeed, the attacker cannot distinguish between two random samplings with the same distribution, and there is a negligible probability that two independent uniform samplings of length η coincide.

The if _ then _ else _ function symbol allows to define other boolean constructs. We write u

(u ∼ true) ⇒ (v ∼ true) (a) (u . ⇒ v) ∼ true (b)
Formula (a) is a logical consequence of (b): if both u .

⇒ v and u are true with overwhelming probability, then it must also be the case for v.

However, (a) does not generally imply (b). Consider a unary function symbol f and a model M where f is interpreted as the machine that returns the first bit of its argument. Then, for any arbitrary name n, the term f (n) is interpreted as the probabilistic computation returning 1 with probability 1 2 , and 0 otherwise. We have

M |= (f (n) ∼ true) hence formula (a) is satisfied in M when u := f (n), regardless of v. However, M |= (f (n) . ⇒ false) ∼ true.
In other words, f (n) is not true with overwhelming probability, but it is also not false with overwhelming probability.

B. Translation

Our translation from the meta-logic to the base logic, is parameterized by the protocol that the meta-logic is meant to describe. From now on, we assume some protocol P = (P A , <) built upon a set of actions A using function and name symbols from F and N . Therefore, we consider meta-logic terms and formulas over Σ = (F, N , A). Definition 6. Given a finite set D of integers, the base logic signature Σ D = (F B , N B ) contains exactly:

• a name symbol n k1,...,kp for every n ∈ N of index arity p, and every k 1 , . . . , k p ∈ D; • a function symbol f k1,...,kp of arity n for every f ∈ F of index arity p and message arity n, and every k 1 , . . . , k p ∈ D.

Example 10. In the Basic Hash protocol, n ∈ N is a name symbol of our meta-logic, of index arity 2. Let D = {1, 2}. We have

Σ D = (F B , N B ) with N B = {n 1,1 , n 1,2 , n 2,1 , n 2,2 }.
In other words, for this choice of concrete indices, we consider four different names in the base logic. Function symbols used to model primitives are all of index arity 0, thus we have a one to one correspondence between function symbols in F and those in F B , and we still write H, _, _ , fst, and snd.

We now define the structure that allows us to interpret metaterms and meta-formulas. The idea is that for each possible interleaving of the protocol, we can define a structure such that the macros at each timestamp correspond to their expected value for that interleaving. Definition 7. A trace model T (associated to a protocol P) is a tuple (D I , D T , < T , σ I , σ T ) such that:

• D I ⊆ N is a finite index domain; • < T is a total ordering on D T := {init} {a[k 1 , . . . , k n ] | a ∈ A, k 1 , . . . , k n ∈ D I }
such that init is minimal, and such that the sequence of elements of D T ordered by < T is an interleaving of P; • σ I : I → D I and σ T : T → D T are mappings that interpret index and timestamp variables as elements of their respective domains.

We include σ I and σ T to ease the presentation, which means that trace models provide an interpretation for all index and timestamp variables. This information is often irrelevant: when interpreting a formula, only the interpretation of its free variables will matter.

The total ordering < T yields a predecessor function pred T : D T → D T which maps init to itself and all other elements v ∈ D T to the largest v ∈ D T such that v < v.

Example 11. Continuing our running example, we consider D I = {1}, and the following total ordering:

init < a T [1, 1] < a R [1, 1] < a R1 [1] Therefore, we have that pred T (a R [1, 1]) = a T [1, 1].
The notion of trace model forces us to include both a R1 [START_REF]IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques[END_REF] and a R [START_REF]IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques[END_REF][START_REF]IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques[END_REF] even though their conditions are mutually exclusive. It is not a concern: what matters is that all real executions of the protocol are accounted for by some prefix of the complete interleaving induced by some trace model.

When T = (D I , D T , < T , σ I , σ T ) is a trace model and k ∈ D I , T{i → k} is the trace model identical to T in which σ I is updated to map i to k. We similarly define T{τ → v} when v ∈ D T .

We can now define, for each meta-term t and trace model T, the base logic term (t) T , and similarly for formulas. The complete definition is given in Appendix A, and we only present here its general principle. It is defined inductively on the structure of meta-terms and meta-formulas, translating each meta-logic construct by its counterpart in the base logic when it is available. Indexed function symbols are translated to their counterpart in Σ D I . For instance, names are translated as follows:

(n[i 1 , . . . , i p ]) T def = n σ I (i1),...,σ I (ip) .

Boolean constructs are translated to their dotted counterparts. Finally, lookup constructs are translated to nested conditionals:

(find i suchthat φ in t else t ) T def = if (φ) T{ i → k1} then (t) T{ i → k1} else if (φ) T{ i → k2} then (t) T{ i → k2} else . . . if (φ) T{ i → kp} then (t) T{ i → kp} else (t ) T cond init = exec init = true input init = frame init = output init = empty output a[ i ] = o cond a[ i ] = φ exec a[ i ] = cond@a[ i ] ∧ exec@pred(a[ i ]) frame a[ i ] = exec@a[ i ], if exec@a[ i ] then output@a[ i ] else empty, frame@pred(a[ i ]) input a[ i ] = att frame@pred(a[ i ])

∨ introduced previously:

(∀i.φ) T def =

.

∧ k∈D I (φ) T{i →k} (∀τ.φ) T def = . ∧ v∈D T (φ) T{τ →v}
and similarly for existential quantifications.

Finally, we also have to give a meaning to the macros input, output, frame, cond, and exec used in the meta-logic. We define in Fig. 2 the terms m init and {m a

[ i ] | a[ i ] ∈ P A }
for each of these macro symbols, and then have:

(m@T ) T def = (m init ) T if (T ) T = init (m a[ i ] ) T{ i → k} if (T ) T = a[ k ] and a[ i ] ∈ P A
Roughly, an output macro is replaced by the meta-term as specified by the protocol and it is then interpreted in the trace model to get a base term. The cond macro has a similar treatment and produces a base formula corresponding to the conditional of the action. The exec macro simply corresponds to the conjunction of all past conditions.

The translation of the frame gathers (using nested pairs) all the information available to the attacker at some execution point: for each past action, the attacker observes if the execution continues and, if that is the case, they obtain the output. Finally, in order to model the attacker's capabilities, the input macro is interpreted using the attacker symbol att, to which we pass the current frame.

Example 12. Considering the trace model T given in Example 11 with σ I (i) = σ I (j) = 1, we give below the interpretation of several meta-terms:

(output@a T [i, j]) T = n 1,1 , H(n 1,1 , key 1 ) def = t out (fst(output@a T [i, j])) T = fst(t out ) (input@a R [j, i]) T = att( true, if true then t out else empty, empty ) def = t in
Therefore the meta-formula expressing an authentication property in Listing 2 translates as follows in T:

snd(t in ) . = H(fst(t in ), key 1 ) . ⇒ true . ∧ fst(t in ) . = fst(t out ) . ∧ snd(t in ) . = snd(t out )
Note that the atom a T [i, j ] ≤ a R [j, i] has been replaced by true because it holds in T when i, j and j are (necessarily) interpreted as 1. If we had had a T [1, 1] > a R [START_REF]IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques[END_REF][START_REF]IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques[END_REF] in T we would have obtained false, making the conclusion of the implication unsatisfiable.

The base formula of the previous example corresponds to the translation of the meta-formula expressing authentication considering a single and very simple trace model. To provide a proof of our authentication property, we have to verify the validity of the base formula obtained with any trace model.

C. Validity

We say that a meta-formula φ is satisfied in T, M, written T, M |= P φ, or simply T, M |= φ when P is clear from the context, whenever M |= (φ) T ∼ true. Intuitively, it means that the formula φ is true with overwhelming probability on the trace T. Then, we say that φ is valid if it is satisfied in every T and M: intuitively, the formula φ is true with overwhelming probability for every executions of the associated protocol P.

In practice, this notion of validity is too strong: for instance, the authentication property of the Basic Hash protocol only holds if the hash satisfies some unforgeability assumption. Thus, we are interested in verifying the validity of metaformulas for restricted classes C of models. We will consider two types of restrictions. First, we may make some security assumptions on the interpretation of cryptographic primitives in M: e.g., when a hash function is declared in our prover, we assume that its interpretation satisfies the PRF assumption. Second, further assumptions can be made by adding axioms expressed as meta-formulas. An axiom φ will restrict the considered class C to those T and M such that M, σ |= (φ) T ∼ true for all semantic assignments σ mapping free message variables occurring in φ to probabilistic PTIME machines. Axioms are used, for example, to express properties of message lengths: len( x, y ) = plus(len(x), len(y)).

Note that our notion of validity differs from standard notion of security in the computational model. In our logic, if a formula φ is valid, it means that for any given trace and for any attacker interacting with the protocol along this trace, φ is false with negligible probability. In the computational model, one would rather expect that for any attacker interacting with the protocol and choosing a polynomial number of actions to execute, φ is false with negligible probability. In the former case, the advantage of the attacker may grow super-polynomially w.r.t. to the number of sessions, but not in the latter. We provide a contrived example showing the difference between the two notions in Appendix D. While weaker than concrete security bounds, we stress that this guarantee is stronger than symbolic guarantees for unbounded sessions. Furthermore, this limitation can be lifted using the composition result of [START_REF] Hubert Comon | Oracle simulation: a technique for protocol composition with long term shared secrets[END_REF], as done in some of our case studies (cf. Section VII).

NAMEINDEP n = m Γ, n[ i ] = m[ j ] φ NAMEEQ Γ, i1 = j1, . . . , i k = j k φ Γ, n[i1, . . . , i k ] = n[j1, . . . , j k ] φ ACTDEP when a[ j] < b[ i ] Γ, b[ i ] ≤ a[ j] φ ACTINDEP when a = b Γ, a[ i ] = b[ j ] φ ACTEQ Γ, i1 = j1, . . . , i k = j k φ Γ, a[i1, . . . , i k ] = b[j1, . . . , j k ] φ EXEC Γ, ∀τ ≤ τ.cond@τ φ Γ, exec@τ φ INIT Γ, τ = init ∧ τ ≤ pred(τ ) φ PRED Γ, τ = pred(τ ) ∨ τ = τ φ Γ, pred(τ ) ≤ τ ≤ τ φ
Fig. 3. Some rules of our sequent calculus for reachability.

Meta-formulas express properties of all execution traces of a protocol. Some security properties (e.g. strong secrecy, unlinkability) are better expressed as equivalences between two protocols. We accomodate such notions naturally in our framework since it is based on an indistinguishability predicate: this is presented in Section VI. Before that, we design in the next section a proof system that allows to derive valid meta-formulas (relatively to some classes of models).

V. REACHABILITY RULES

We now present our reachability sequent calculus, for some protocol P = (P A , <) fixed throughout the section. We now give our meta-logic reachability sequent calculus rules, and prove their soundness. We talk of validity (resp. soundness) without specifying the class C when it holds w.r.t. all models.

A. Basic Rules

Although our sequents have a probabilistic semantics, all rules of classical first-order sequent calculus are sound.

We give in Fig. 3 the rules we designed which are specific to security protocol analysis, and describe them below. Two different names are almost never equal (i.e. they are not equal except for a negligible number of samplings). This can be the case either because they have different head symbols (rule NAMEINDEP) or because they have the same head symbols but different indices (rule NAMEEQ). The rule ACTDEP states that actions must occur in the order imposed by the protocol, and ACTINDEP and ACTEQ express that two different actions 4. Some XOR rules of our sequent calculus for reachability. cannot occur at the same instant. The PRED rule states that there is no timestamp between pred(τ ) and τ , and EXEC states that if the trace is executable up to τ then the protocol conditions hold for any instant before τ . INIT says that if τ is not the initial timestamp, then τ cannot occur before the action preceding it.

⊕-NIL Γ t ⊕ t = 0 ⊕-SYM Γ t ⊕ t = t ⊕ t ⊕-ASSOC Γ t ⊕ (t ⊕ t ) = (t ⊕ t ) ⊕ t Fig.
We also have rules for expanding macros into their meaning. For instance, if P A contains the action a[ i ].(φ, o), we can derive Γ output@a[ i ] = o and Γ cond@a[ i ] ⇔ φ. All these rules are sound. Some of our rules are sound only under some computational assumptions. These assumptions can either be cryptographic assumptions (we give examples in the next section), or functional properties of the primitives. E.g, the rules ⊕-NIL, ⊕-SYM and ⊕-ASSOC of Fig. 4 state functional properties that ⊕ satisfies whenever it is interpreted as the XOR operator: these rules are obviously sound in any computational model where ⊕ is interpreted as XOR.

B. Advanced Rules

We now describe how we designed the most advanced rules of our reachability sequent calculus, which deal with cryptographic assumptions and probabilistic independence. We present here the rule for the EUF-CMA axiom. Another rule, NAMEFRESH, is presented in Fig. 8 of Appendix B.

a) Base logic rule: We recall the base logic EUF-CMA rule from [START_REF] Koutsos | The 5G-AKA authentication protocol privacy[END_REF]. Before starting, we introduce notations we use to describe syntactic side-conditions of rules. appearing in s or m. We formally define it next, as a simple elaboration of the rule EUF-MAC of [START_REF] Koutsos | The 5G-AKA authentication protocol privacy[END_REF] (a base logic sequent Γ φ is valid when (( .

∧ Γ)

.

⇒ φ) ∼ true is valid).

Definition 12. For any ground base terms s, u, m and name k, we let EUF-CMA be the rule:

Γ, . H(u,k)∈st(s,m) m . = u φ Γ, s . = H(m, k) φ when k H(_,•) s, m Example 14. If u is the term H(t 1 , k), H(t 2 , k), H(t 3 , k )
where k, k are names and s, t 0 , t 1 and t 2 are ground terms that do not use k and k , then we have an EUF-CMA instance:

Γ, (att(u)

. = t 1 ) . ∨ (att(u) . = t 2 ) φ Γ, s . = H(att(u), k) φ
Indeed, k appears only in hash positions in s and att(u), hence k H(_,•) s, att(u). Moreover, t 1 and t 2 are the only messages hashed by k (note that t 3 is hashed by a different key k ). b) Meta-logic rule: We now explain how to lift the base logic rule EUF-CMA to the meta-logic. We need to find a rule such that its translation in any trace model yields a valid instance of the base logic EUF-CMA rule. There are two obstacles to this. Assume our meta-logic rule is of the following form:

Γ, . H(u,k[ i ])∈ST(s,m) m . = u φ Γ, s . = H(m, k[ i ]) φ when SSC k[ i ] (s, m) (1)
Soundness requires that:

• if the meta-logic side-condition SSC k[ i ] (s, m) holds, then all translations of s and m must satisfy the base logic side-condition:

∀T, (k[ i ]) T H(_,•) (s) T , (m) T (2)
• the set of meta-terms ST(s, m) must be such that its translation in any trace model contains all hashes of the translation of s and m. That is, for every T:

H(u, (k[ i ]) T ) ∈ st((s) T , (m) T ) ⊆ (ST(s, m)) T (3)
Note that both obstacles are of the same nature, though there is an additional difficulty in the second condition: since the set on the left of (3) can be arbitrarily large (because the trace in T can be arbitrarily long), the set (ST(s, m)) T may be infinite (because of this, our final rule will slightly differ from the form proposed in (1)).

We start by focusing on the occurrence side condition H(_,•) . First, we naturally lift it to meta-terms, by requiring that the side-condition holds for the translation of the metaterms in any trace model. Definition 13. Let C be a template and u a meta-term with no message variables. For any name symbol n, we let n P C u hold whenever n k C (u) T P holds for any trace model T and k ⊆ D I (of length arity of n).

The base logic side-condition C is fully syntactic, and can easily be implemented. This is no longer the case with n P C u, as it requires to check a property on all translations of u. Therefore, instead of checking directly n P C u, we are going to check the property on the direct occurrences of n in u (i.e. n C u), and on the occurrences of n in any action of the protocol. The idea is that this must over-approximate all occurrences of n in any translation of u in a trace model T.

First, we adapt Definition 11 to meta-terms (base logic function symbols in a template C are seen as function symbols of index arity 0 of the meta-logic). Definition 14. Let C be a template, u a meta-term without message variables, and n be a name symbol. Then n C u holds whenever n appears in u only in subterms of the form C[ w , n[ i ]] for some w and indices i . Definition 15. Let C be a template, and n be a name symbol. We write

n C P when n C {φ, o | a[ i].(φ, o) ∈ P A }.
We give a sufficient condition to check that n P C u. Proposition 1. Let C be a template. For any name symbol n and meta-term u, if n C u and n C P then n P C u. Next, we need to over-approximate the (possibly infinite) set of all honest hashes that can appear in the translation of a meta-term, as stated in (3). As for P C , we look for all possible occurrences of H(u, k) either directly in (s, m), or in an action of P. In the latter case, we also construct a formula of the logic that characterizes the fact that the action must have happened before the moment where u was computed, which improves the precision. We capture this through some set st P (s, m), which is formally defined in Appendix B. Essentially, st P (s, m) is a set of triples (u, i, c) such that, for any T, any subterm of (s, m) T that is a hash is the interpretation of some (u) T{ i → k} such that c holds in T{ i → k}. Moreover, i are the new indices in u and c: fv(u, c) ⊆ fv(s, m) ∪ { i }.

We can now state the meta-logic version of the EUF-CMA rule given in Definition 12.

Proposition 2. The following rule is sound whenever H is interpreted as an EUF-CMA keyed hash-function:

Γ, (H(u,k[ j0 ]), i ,c)∈ st P (s,m) ∃ i .( j 0 = j ∧ c ∧ m = u) φ Γ, s = H(m, k[ j ]) φ when k H(_,•) P and k H(_,•) s, m.
Proof (sketch). It suffices to show that, for any trace model T, the translation of the rule in T is (up to some minor details) an instance of the base logic EUF-CMA rule.

Using Proposition 1, we know that k P H(_,•) t, m, hence k k H(_,•) (t, m) T for any k ⊆ D I : this guarantees that the side-condition of the base logic rule holds. Then, we show that the translation in T of the disjunction in the premise of the meta-rule covers all cases of the premise of the base logic EUF-CMA rule, using the fact that st P (s, m) correctly overapproximates the hashes in st((s, m) T ).

Example 15. We illustrate our rule on an example in the context of the Basic Hash protocol, as described in Example 5 (we factorize the quantification and the equality atom, which are shared by all three cases):

Γ, ∃i 0 , j 0 . i 0 = i ∧ (a T [i 0 , j 0 ] < τ ∧ n[i, j] = n[i 0 , j 0 ]) ∨ (a R [j 0 , i 0 ] < τ ∧ n[i, j] = fst(input@a R [j 0 , i 0 ])) ∨ (a R1 [j 0 ] < τ ∧ n[i, j] = fst(input@a R1 [j 0 ])) φ Γ, snd(input@τ ) = H(n[i, j], key[i]) φ
The rule does express that if a hash of n[i, j] has been obtained, this message must have been previously hashed. The three possible hashed messages detected by st P (s, m) are restricted to plausible situations: equalities i 0 = i ensure that the hashing key is key[i] and inequalities over timestamps (e.g. a T [i 0 , j 0 ] < τ ) ensure that the situation comes from an action that has been previously executed.

VI. EQUIVALENCE RULES

We now turn to proving equivalences. Ultimately, we are interested in proving observational equivalence between two protocols, as this allows to model several security properties such as strong secrecy, anonymity, or unlinkability. We first define the notion of observational equivalence, then define what are our equivalence sequents, and finally present our equivalence sequent calculus.

Intuitively, two protocols P 1 and P 2 are observationally equivalent when they offer the same set of actions for the attacker to execute and, for any sequence of actions that the attacker may decide to execute, the resulting frames with P 1 and P 2 are indistinguishable. In particular, the actions execute with the same probability on both sides, and the sequences of messages that are outputted are indistinguishable. We start by defining the notion of compatible protocols, capturing the idea that they offer the same set of actions.

Definition 16. Protocols P 1 = (P 1 A , < 1 ) and P 2 = (P 2 A , < 2 ) are compatible if they are based on the same set A of action names and have the same partial orders, i.e.

α < 1 α if, and only if, α < 2 α for all α and α .

Since the notion of trace model only depends on the underlying set of names and partial order, and not on the actual semantics of the protocol given by P A , we immediately have that two compatible protocols have the same trace models. Definition 17. Two protocols P 1 and P 2 are observationally equivalent if they are compatible and, for any trace model T, the base logic formula (frame@τ ) T P1 ∼ (frame@τ ) T P2 is valid. We need a notion of sequent for equivalences that allows us to express observational equivalences. More generally, we want to reason about indistinguishabilities between sequences of meta-level terms and formulas interpreted w.r.t. different protocols on each side of the equivalence. We also need hypotheses to enable proofs by induction. Definition 18. Let P 1 and P 2 be two compatible protocols. A meta-equivalence is an element of the form u ∼ v where u and v are sequences of meta-terms and meta-formulas of the same length and without message variables. The interpretation of a meta-equivalence in a trace model w.r.t. P 1 and P 2 is:

( u ∼ v) T P1,P2 def = ( u) T P1 ∼ ( v) T
P2 . An equivalence sequent for P 1 and P 2 is a judgment of the form ∆ P1,P2 E where E is a meta-equivalence and ∆ is a set of meta-equivalences. We may note ∆ E when P 1 , P 2 is clear from the context.

The sequent ∆ P1,P2 E is valid when T, M |= (E) T

P1,P2

for all T and M such that T, M |= (E ) T P1,P2 for each E ∈ ∆. We now present our equivalent calculus, for some compatible protocols P 1 and P 2 , fixed for the rest of this section.

A. Basic Rules

We present in Fig. 5 some basic inference rules for deriving equivalences, whose soundness does not depend on any cryptographic assumption. In these rules, we use the metavariable ξ to denote either a meta-term or a meta-formula.

All the rules but INDUCTION are obvious liftings of known axioms for deriving equivalences in the base logic (see e.g. [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF]). It is the case of rule REFL: if u is macro-free then its interpretations w.r.t. P 1 and P 2 are the same, thus our rule is, for each possible trace interpretation, an instance of the reflexivity rule of the base logic. It is also the case of rules ENRICH, DUP and FA. We also allow in our proof system variants of the FA rule such as FA-♦ which are still liftings of the base logic FA rule. Finally, rule EQUIV-TERM allows to replace some occurrences of a meta-term t by t on the left side of the equivalence provided that P1 t = t is derivable. We can similarly replace a meta-formula by an equivalent one using EQUIV-FORM. Obviously, the variants of these rules working on the right side of equivalences are also allowed.

The INDUCTION rule allows to prove an equivalence for any arbitrary timestamp τ by proving the equivalence when τ is init and, for each action a[ i ] of the protocol, when τ is a[ i ] assuming that the equivalence holds for pred([ i ]). Proofs of observational equivalence almost always start with this rule.

B. Advanced Rules

We now present some more advanced rules. The soundness arguments for these rules are postponed to Appendix C.

We show in Fig. 6 our rule FRESH. It is based on the base logic rule which states that adding fresh names on each side of an equivalence preserves its validity: indeed, these independent uniform random samplings do not bring any new information to the attacker. We lift this at the meta-level by overapproximating the freshness condition as meta-formulas: we have (n[ i ]) T P1 ∈ st(( u ) T P1 ) whenever (Fresh

n[ i ]
P1 ( u )) T P1 is true. Our proof system also features a rule expressing the information hiding capabilities of XOR, as well as rules corresponding to the cryptographic assumptions PRF, CCA 1 , ENC-KP, and DDH shown in Appendix C.

REFL u is macro-free ∆ u ∼ u ENRICH ∆ u , ξ ∼ v , ξ ∆ u ∼ v DUP ∆ u , ξ ∼ v , ξ ∆ u , ξ, ξ ∼ v , ξ , ξ AXIOM ∆, u ∼ v u ∼ v FA ∆ u , t1, . . . , tn ∼ v , t 1 , . . . , t n ∆ u , f[ i ](t1, . . . , tn) ∼ v , f[ i ](t 1 , . . . , t n ) FA-♦ ∆ u , φ, φ ∼ v , ψ, ψ ∆ u , φ♦φ ∼ v , ψ♦ψ where ♦ ∈ {∧, ∨, ⇒}
EQUIV-TERM Base logic rule:

P 1 t = t ∆ u {t → t } ∼ v ∆ u ∼ v EQUIV-FORM P 1 φ ⇔ φ ∆ u {φ → φ } ∼ v ∆ u ∼ v INDUCTION ∆ u ∼ v {τ → init} ∆, u ∼ v {τ → pred(a[ i ])} u ∼ v {τ → a[ i ]} a∈A, i ∈fv(∆, u , v ) ∆ u ∼ v τ ∈ fv(∆)
∆ u ∼ v ∆ u , n ∼ v , m where n ∈ st( u ), m ∈ st( v )
Meta-logic rule:

∆ u , if Fresh n[ i ] P1 ( u ) then empty else n[ i ] ∼ v , if Fresh m[ j ] P2 ( v ) then empty else m[ j ] ∆ u , n[ i ] ∼ v , m[ j ]
where Fresh Finally, our proof system includes a rule FA-DUP which allows to handle some cases where meta-formulas or metaterms could be dropped from an equivalence, but where this cannot be done using the FA and DUP rules because the justification for dropping the elements is not immediately apparent in the meta-logic. Formally, we define in Fig. 16 of Appendix C a set of honest meta-formulas Honest {T } for any timestamp T . The rule is then as follows:

n[ i ] P ( t ) def = (n[ i 0], j ,c)∈ st P ( t ) ∀ j . c ⇒ i = i 0
FA-DUP ∆ u , frame@T ∼ v , frame@T ∆ u , frame@T, exec@T ∧ φ ∼ v , frame@T, exec@T ∧ φ φ ∈ Honest {T }
Intuitively, we can remove φ when it can already be computed by the attacker using the information they obtained from a past execution. Our set Honest S captures a fragment that has this property. We typically use FA-DUP for formulas describing honest interactions between protocol participants, such as the right-hand side of the implication of Listing 2 which does belong to Honest {a R [j,i]} .

C. Implementation Details

Since we are interested in proving observational equivalence between protocols that are compatible and whose terms only differ in a few positions, we use the common technique of describing two protocols as a single bi-protocol using a special binary function symbol diff(•, •). We also present and manipulate meta-equivalences as bi-frames, i.e. as a single sequence of meta-terms and formulas featuring the diff(•, •) symbol. We have derived tactics from the rules presented before, adapting them to work conveniently using this presentation.

VII. CASE STUDIES

We have implemented the meta-logic inside an interactive protocol prover: SQUIRREL. This tool consists of about 10,000 lines of OCaml code, and is available at [START_REF]The Squirrel Prover repository[END_REF].

SQUIRREL accepts models written in a variant of the applied pi-calculus, as depicted in Listing 1, and allows to prove reachability and equivalence properties of the specified protocol. Proofs are interactive, using tactics. Automated tactics are available to reason over equalities and disequalities over terms (modulo e.g. the equations of XOR). Some tactics performing basic proof search and automated reasoning are implicitly applied at each step of the proof to simplify goals and close absurd ones. A strength of the tool is its modularity: extending the tool with new cryptographic primitives does not impact the core of the tool. It only requires to add new tactics and to prove their soundness inside the meta-logic.

We have used our tool to perform a number of case studies, proving different kind of properties (authentication, strong secrecy, anonymity, unlinkability) under various cryptographic assumptions (PRF, EUF-CMA, XOR, CCA 1 , ENC-KP, INT-CTXT, DDH). They are summarized in Table I.

For each protocol, we provide the number of lines of code (LoC), the cryptographic assumptions used, and the security properties studied. In all cases, SQUIRREL is able to conclude in less than one minute. Interestingly, most proofs follow the intuition of the pen-and-paper proofs, while some low-level reasoning is successfully abstracted away or automated.

A. RFID based protocols

Those case studies (Basic Hash [START_REF] Brusò | Formal verification of privacy for RFID systems[END_REF], Hash Lock [START_REF] Juels | Defining strong privacy for RFID[END_REF], LAK with pairs instead of XOR as in [START_REF] Hirschi | A method for unbounded verification of privacy-type properties[END_REF], MW [START_REF] Molnar | Privacy and security in library RFID: issues, practices, and architectures[END_REF] and Feldhofer [START_REF] Feldhofer | Strong authentication for RFID systems using the AES algorithm[END_REF]) are authentication protocols between identityspecific tags and a generic reader (having access to a shared database with authorized tags credentials). We used our tool to establish proofs of unlinkability using the notion defined in [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF], [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF]: an outside observer must not be able to distinguish between a system where each tag can play many sessions from a system where each tag can play at most one session.

These proofs follow the same global pattern: we use the induction tactic to reason on an arbitrary number of sessions, then at some point we use the equivalent tactic to transform the conditional of an action into an equivalent formula that can be removed with FA-DUP. The systematic use of authentication to establish unlinkability is reminiscent of the wellauthentication condition of [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF], [START_REF] Hirschi | A method for unbounded verification of privacy-type properties[END_REF].

In our framework, equivalence requires synchronized executions of the two protocols, but their databases need not have similar structures, as would be the case with the diffequivalence notions of PROVERIF or TAMARIN. This has allowed us to obtain proofs of unlinkability that are out-ofscope of these tools, cf. discussion about Basic Hash in [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF].

For LAK, MW and Feldhofer protocols, the last conditional of the protocol is not modelled. We managed to partially overcome this limitation for the MW protocol: in this proof, we enrich the frame with infinite sequences of messages that over-approximate what the attacker may learn during protocol executions, which eases the proof process. We cannot yet prove the indistinguishability of these sequences in the tool, because we lack a notion of induction over sequences of messages. This is left for future work.

B. Private authentication

We study the Private Authentication protocol as presented in [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF], where the authors give a (manual) proof of anonymity in the computational model for one session of the protocol. A protocol preserves anonymity if an attacker is not able to tell when a session of the protocol is initiated by one identity or by another. Using our tool, we were able to establish a mechanized proof of anonymity for this protocol, for an arbitrary number of sessions.

C. DDH based protocols

We first study a proof of strong secrecy of the shared key for the signed DDH protocol [START_REF]IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques[END_REF]. Similarly to RFID based protocols, we rely on the proof of authentication properties in the reachability prover to perform our proof of strong secrecy in the indistinguishability prover.

We also present two additional case studies for the signed DDH protocol [START_REF]IT Security techniques -Entity authentication -Part 3: Mechanisms using digital signature techniques[END_REF] and the SSH protocol [START_REF] Ylonen | The Secure Shell (SSH) Transport Layer Protocol[END_REF], where proofs are performed through the use of the composition framework developed for the CCSA model in [START_REF] Hubert Comon | Oracle simulation: a technique for protocol composition with long term shared secrets[END_REF]. The authors outline how to decompose a proof for those protocols into single session proofs, which consists in slightly modifying the hash function by giving more capacities to the attacker using oracles. With our tool, we were able to mechanize those proofs. Compared to the other case studies presented so far, those two hold for an unbounded number of sessions that may depend on the security parameter (this is given by the result in [START_REF] Hubert Comon | Oracle simulation: a technique for protocol composition with long term shared secrets[END_REF]), and not just for an arbitrary number of sessions.

VIII. CONCLUSION

We have designed a meta-logic on top of the CCSA logic of [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF], and proof systems for establishing reachability and equivalence properties in that language. We have shown that it yields a simple, high-level methodology for carrying out computer-assisted proofs of cryptographic protocols, providing asymptotic security guarantees in the computational model. This is supported by the implementation of the interactive prover SQUIRREL, and its use on various case studies.

As future work, we plan to enrich and optimize the proof automation, for instance by borrowing from the SMT techniques and tools. Our proof systems could also be enriched to benefit from equivalence reasoning in reachability goals, e.g. the PRF equivalence rule should allow to replace hashes by fresh names in reachability goals. We would like also to extend our framework to deal with protocols with states. Whereas handling protocols with states seems to be difficult in CRYPTOVERIF, our approach based on a reasoning over execution traces of protocols seems to be more suitable for this extension. We are working on it with the aim of mechanizing e.g. the proof of the modified AKA protocol of [START_REF] Koutsos | The 5G-AKA authentication protocol privacy[END_REF]. On a more theoretical level, we plan to address the formal semantics of our applied pi-calculus protocols, and the study of their translations to our internal representation as sets of actions. Finally, we plan to elaborate on our approach to provide truly unbounded security guarantees, instead of asymptotic security guarantees for each trace (with an asymptotic bound that may depend on the trace).

APPENDIX A SEMANTICS OF OUR META-LOGIC

Our translation from the meta-logic to the base logic, is parametrized by the protocol P = (P A , <) that the metalogic is meant to describe, as well as the trace model T under study. The general principle of this translation is presented in Section IV-B and we give below the complete definition of this translation. We start with the interpretation of meta-terms of sort index and timestamp:

(i) T P = σ I (i) (τ ) T P = σ T (τ ) (init) T P = init (a[i 1 , . . . , i p ]) T P = a σ I (i1),...,σ I (ip) (pred(T )) T P = pred T ((T ) T P )
Then, we give the interpretation of meta-terms of sort message. Remember that the interpretation of the macro terms m init and {m a

[ i ] | a[ i ] ∈ P A } are given in Fig. 2. Below, k 1 , . . . , k n is a complete enumeration of D | i| I in lexicographic order: 1 (n[i 1 , . . . , i p ]) T P = n σ I (i1),...,σ I (ip) (x) T P = x (f[i 1 , . . . , i p ](t 1 , . . . , t n )) T P = f σ I (i1),...,σ I (ip) (t 1 ) T P , . . . , (t n ) T P (m@T ) T =    (m init ) T if (T ) T = init (m a[ i ] ) T{ i → k} if (T ) T = a[ k ] and a[ i ] ∈ P A (if φ then t else t ) T P = if (φ) T P then (t) T P else (t ) T P (find i suchthat φ in t else t ) T P = if (φ) T{ i → k1} P then (t) T{ i → k1} P else . . . if (φ) T{ i → kp} P then (t) T{ i → kp} P else (t ) T P
The interpretation of meta-formulas is quite straightforward. For instance, we have that:

(φ ∧ φ ) T P = (φ) T P . ∧ (φ ) T P
Other boolean connectives are translated similarly. We let:

(i = i ) T P = true if σ I (i) = σ I (i ) false otherwise (T = T ) T P = true if (T ) T P = (T ) T P false otherwise (T ≤ T ) T P = true if (T ) T P ≤ (T ) T P false otherwise (t = t ) T P = (t) T P .

= (t ) T

P

Finally, as already explained, quantifications over indices and timestamps are translated to finite boolean expressions:

(∀i. φ) T P = . ∧ k∈D I (φ)
T{i →k} P (∃i. φ) T P =

.

∨ k∈D I (φ)

T{i →k} P (∀τ. φ) T P =

.

∧ v∈D T (φ)

T{τ →v} P (∃τ. φ) T P =

.

∨ v∈D T (φ)

T{τ →v} P
Overall, this translation is well-defined because our notion of protocol imposes that the condition and output message of an action α only refer to actions β < α, or to input@α (which itself can only refer to actions β < α). For instance, the translation of (output@T ) T is defined as the translation of a potentially large term (the output message at (T ) T ) but its translation can only rely on translations (m@T ) T for (T ) T < (T ) T or m = input and (T ) T = (T ) T .

APPENDIX B REACHABILITY SEQUENT CALCULUS

We present in this section the soundness proof of some of our reachability rules. We also give the definition of st P (_) which we omitted in the body and present rules of classical first-order sequent calculus in Fig. 7, and the rule NAMEFRESH in Fig. 8.

AXIOM Γ, φ φ CUT Γ φ Γ, φ ψ Γ ψ ∧-L Γ, φ, φ ψ Γ, φ ∧ φ ψ ∧-R Γ φ Γ φ Γ φ ∧ φ ¬-R Γ, φ ⊥ Γ ¬φ ¬-L Γ φ Γ, ¬φ ψ RAA Γ, ¬φ ⊥ Γ φ =-R Γ t = t =-L (Γ φ){x → t , x → t} t = t , Γ{x → t, x → t } φ{x → t, x → t } ∀-L Γ, φ{x → t} ψ Γ, ∀x.φ ψ ∀-R Γ φ Γ ∀x.φ
In ∀-R we require that x does not appear free in Γ. Base logic rule:

Γ, t = n φ
where n ∈ st(t)

Meta-logic rule: Proof. To prove the rules soundness, we only need to show that, if the premises are valid, then the conclusion is valid.

Γ, (n[ j], k,c)∈ st P (t) ∃ k.c ∧ i = j φ Γ, t = n[ i] φ
• For NAMEINDEP, this is because names of the metalogic with different head symbols are always translated as different names of the base logic. We conclude by using the base logic rule which states that EQ(n, m) ∼ false whenever n and m are distinct names (this is the rule EQINDEP of [START_REF] Comon | Formal computational unlinkability proofs of RFID protocols[END_REF]). • For NAMEEQ, if one of the equalities i 1 = j 1 , ..., i k = j k does not hold in T, then we know that (n[i 1 , . . . , i k ]) T and (n[j 1 , . . . , j k ]) T are distinct names of the base logic. Again, we conclude using the EQINDEP rule of [START_REF] Comon | Formal computational unlinkability proofs of RFID protocols[END_REF].

• For ACTDEP, if a[ j] < b[ i ] then (b[ i ] ≤ a[ j]) T is false,
because T must respect the protocol ordering <. • For ACTINDEP, we simply observe that if a and b are distinct symbols, then (a[ i ]) T cannot be equal to (b[ j ]) T . • Similarly for ACTEQ, we note that if there exists l such that i l and j l are distinct indices in T, then

(a[i 1 , . . . , i k ]) T cannot be equal to (b[j 1 , . . . , j k ]) T . • For EXEC, if τ ≤ τ in T,
then by a trivial induction we can show that (exec@τ ) T = . . .

. ∧ (cond@τ ) T . ∧ . . .

Therefore, if M |= (exec@τ ) T ∼ true then we have also that M |= (cond@τ ) T ∼ true. • INIT and PRED state properties of T w.r.t. the interpretation of init and pred(_).

A. Advanced Reachability Rules

First, we recall Proposition 1 and quickly sketch its proof.

Proposition. Let C be a template. For any name symbol n and meta-term u, if n C u and n C P then n P C u. Proof (sketch). We show this by induction over the size of (u) T . The proof uses the hypothesis n C P in the macro case, and n C u for the other cases.

We now focus on giving the definition of st P (_) which we omitted in the body. To do this, we need to define a happenbefore formula T 0 hb u, which characterizes the fact that some timestamp T 0 must have occurred before the meta-term u. First, we define this on macros (the base case). Definition 19. For every meta-terms T 0 , T of sort timestamp and macro m@T , we define:

T 0 hb m@T def = T 0 < T if m = input T 0 ≤ T otherwise
Our meta-logic has three index binders, ∃, ∀ and find _ suchthat _, which are respectively translated to disjunctions, conjunctions and nested if _ then _ else _ in a trace model. Therefore, the subterms of the translation of an index binder are:

• The subterms containing several whole disjuncts, conjuncts or conditionals. We do not need to overapproximate those: e.g. in the EUF-CMA example, we only care about subterms whose head symbol is H(_, _). • The union, over the number of concrete indices in the trace, of the subterms of, respectively, each disjunct, conjunct, or conditional. Hence, we need to keep track of bound indices. To do this, we let i-st(u) be the set of pairs (t, i) where t is a subterm of u, and i is the set of indices bound on the path from the root of u to t. 2 For example, if φ, t and t are meta-terms with no index binders and no message variables, then

i-st(find i suchthat φ in t else t ) = {(s, i) | s ∈ st(φ, t, t )}
Formally, we have that: Definition 20. For any meta-term u with no message variables, we let i-st(u) = i-st(∅ : u), where i-st(_ : _) is defined in Fig. 9.

i-st( i : u) = (u, i) ∪          i-st( i, j : ψ) if u = ∃j.ψ i-st( i, j : ψ) if u = ∀j.ψ i-st( i, j : t) ∪ i-st( i, j : φ) ∪ i-st( i : t ) if u = find j suchthat φ in t else t v∈mst(u) i-st( i : v) otherwise
Conventions: i are distinct index variables, and mst(u) are the maximal strict subterms of u. In all cases above, we require w.l.o.g. that the bound variable indices j and j are distinct and disjoint from i. Using this, we can extend the happen-before formula of Definition 19 to more than macros. The idea is that T 0 may happen before a timestamp in a meta-term u when some macro m@T appears in u, possibly under bound indices i, and for some value of these indices we have T 0 ≤ T . In particular, note that it does not matter if the binder is an existential or universal quantification, or a lookup. Formally: Definition 21. For every meta-term T 0 of sort timestamp and meta-term u with no message variables, we define the happenbefore meta-formula T 0 hb u:

T 0 hb u def = (m@T, i)∈i-st(u) ∃ i.(T 0 hb m@T )
where i and fv(T 0 ) must be distinct.

Finally, we can define the conditional subterms st P (u) of u. Definition 22. Let u be a meta-term with no message variables, we let the set of conditional subterms st P (u) be:

{(t, i, true) | (t, i) ∈ i-st(u)} ∪ a[ i].(_)∈P A ∪{init} {(t, ( i, j), a[ i] hb u) | (t, j) ∈ i-st(m a[ i] ), m ∈ M}
where i are distinct indices disjoint from fv(u), M is the set of macro symbols and m a[ i ] is given in Fig. 2.

The following (technical) lemma links the subterms of the translation of u that do not start with a conjunct, disjunct or conditional, to the elements of st P (u).

Lemma 1. For any meta-term u, the set st P (u) is finite. Moreover, for any trace model T = (D I , D T , < T , σ I , σ T ):

st((u) T P ) ∩ t | head(t) ∈ { . ∧, . ∨, if _ then _ else } ⊆ (t) T P | (t, i , c) ∈ st P (u), k ⊆ D I , T = T{ i → k }, ∀M, (T , M |= c)
where head(t) is the head symbol of t, if it exists.

Proof (sketch). The finiteness property is immediate. We prove the second point by induction over the size of (u) T P . The details are postponed to Appendix B-B.

In addition, we show the following proposition, which will be used in the proof of Lemma 1.

Proposition 4. Let a ∈ P A ∪ {init} of index arity p, φ a formula without message variables, and j a sequence of distinct index variables of length p. Then, for every T, M such that, for some k in the index domain of T:

T{i → k}, M |= a[ j] hb φ (4)
we have:

T, M |= a[ j] hb ∀i.φ (5)
whenever i does not appear in j.

Similar results hold for ∃i.φ and if φ then t else t ; we do not detail them. The proof is straightforward from the definition of hb .

Proof. By definition:

a[ j] hb φ def = (m@T, k)∈i-st(φ) ∃ k.a[ j] hb m@T Also: i-st(∀i.φ) = {(∀i.φ, ∅)} ∪ {(s, (i, k)) | (s, k) ∈ i-st(φ)}
Therefore, using the fact that i ∈ j: (m@T, k)∈i-st(φ) ∃ k.a[ j] hb m@T is satisfied in T. This is exactly ∃i.a[ j] hb φ. Hence, from Equ. (4) we deduce that Equ. (5) holds.

B. Proof of Lemma 1

We can now give the proof of Lemma 1. First, for every base or meta-term t, we let st (t) be the set of subterms of t that do not start with a conjunction, disjunction or conditional:

st (t) = st(t) ∩ s | head(s) ∈ { . ∧, . ∨, if _ then _ else _}
Moreover, for every u and T, we let S T u be the set on the right-hand side of the lemma.

S T u = (t) T P | (t, i , c) ∈ stP (u), k ⊆ DI, T = T{ i → k }, ∀M, (T , M |= c)
The finiteness property is immediate. We prove the second point by induction over the size of (u) T P , generalized over all parameters, and by a case analysis over u. We only present the input@T and ∀i.φ cases (the other cases are similar).

a) Case input@T : If u = input@T , then we know that:

st P (u) = {(u, ∅, true)} ∪ a[ i].(_)∈P A ∪{init} {(t, ( i, j), a[ i] < T ) | (t, j) ∈ i-st(m a[ i]
), m ∈ M} If (T ) T P = init, then (u) T P = empty, hence this is immediate. Assume (T ) T P = init, then:

(u) T P = att((frame@pred(T )) T P )

Take s ∈ st ((u) T P ). If s = (u) T P , we immediately get that s ∈ S T u (because (u, ∅, true) ∈ st P (u) and T, M |= true for any T, M). Assume s is not (u) T P , then s ∈ st ((frame@pred(T )) T P ). By induction hypothesis: st ((frame@pred(T )) T P ) ⊆ S T frame@pred(T )

Hence s ∈ S T frame@pred(T ) . To conclude this case, we prove that:

S T frame@pred(T ) ⊆ S T u
First, note that:

st P (frame@pred(T )) = {(frame@pred(T ), ∅, true)} ∪ a[ i ].(_)∈P A ∪{init} {(t, ( i, j), a[ i] ≤ pred(T )) | (t, j) ∈ i-st(m a[ i] ), m ∈ M

}

We have two cases:

• let (t, ( i, j), a[ i] ≤ pred(T )) in the set above, and let T = T{ i, j → k } for some k ⊆ D I . Assume that:

∀M, (T , M |= a[ i] ≤ pred(T ))
Then, since (T ) T is not init, 3 we know that:

∀M, (T , M |= a[ i] < T ) Hence (t) T P ∈ S T u . • for (frame@pred(T ), ∅, true), let a[ i ].(_) ∈ P A ∪ {init} and k ⊆ D I such that (pred(T )) T = a[ k ]. Let T = T{ i, j → k }, we know that: ∀M, (T , M |= a[ i] = pred(T ))
We conclude as in the previous case.

We know that (t) T ∈ S T φ , and we need to prove that (t) T ∈ S T ∀i.φ . Recall that st P (φ) is the set:

{(t, i, true) | (t, i) ∈ i-st(φ)} ∪ (7) a[ i ].(_)∈P A ∪{init} {(t, ( i, j), a[ i] hb φ) | (t, j) ∈ i-st(m a[ i] ), m ∈ M} (8)
If (t, j , c) is taken in the second component above (i.e. Equ. ( 8)), then j = j 0 , j 1 and there exists a such that:

c def = a[ j 0 ] hb φ and: ∀M, (T , M |= a[ j 0 ] hb φ) (9)
We know that (t, j , c) ∈ st P (∀i.φ), and Proposition 4 and Equ. [START_REF] Bana | Verification methods for the computationally complete symbolic attacker based on indistinguishability[END_REF] imply that:

∀M, (T{ j → k }, M |= a[ i] hb ∀i.φ)
Hence (t) T{ j → k } ∈ S T ∀i.φ . Since i does not appear in t, we have that (t) T{ j → k } is syntactically equal to (t) T{i →e}{ j → k } , which is exactly (t) T .

It only remains the case where (t, j , c) is taken in the first component (i.e. Equ. [START_REF] Bana | Computationally complete symbolic attacker in action[END_REF]). We start by observing that: i-st(∀i.φ) = {((i, k), s) | ( k, s) ∈ i-st(φ)} Hence (t, (i, j )) ∈ st P (∀i.φ). Since the condition is true, we have nothing else to check, and we know that t ∈ S T u .

C. Additional Cryptographic Rule

Finally, we present an additional cryptographic rule for an INT-CTXT symmetric encryption scheme [START_REF] Bellare | Authenticated encryption: Relations among notions and analysis of the generic composition paradigm[END_REF] (senc(•, •, •), sdec(•, •)). Here, senc(m, n, k) is the symmetric encryption of m using key k and randomness n, and sdec(c, k) is the decryption of the ciphertext c. The decryption of a ciphertext yields either a constant ⊥ c if it fails, or a message ok(m). In the latter case, c is said to be a valid ciphertext.

A symmetric encryption is INT-CTXT if it is computationally infeasible to produce a valid ciphertext not previously produced by the sender. We informally describe the security game played by an adversary A (see [START_REF] Bellare | Authenticated encryption: Relations among notions and analysis of the generic composition paradigm[END_REF] for a formal description): i) a fresh key k is randomly generated by the challenger; ii) we run the adversary A, while giving the adversary access The meta logic, given in Fig. 10, is similar to our EUF-CMA rule. Essentially, it states that if c is a valid ciphertext then it is equal to an encryption which took place before c. There is only one difficulty: encryptions can only be obtained through the encryption oracle in the INT-CTXT game, and this oracle samples a fresh encryption randomness at each call. Hence, for our rule to be valid for key k, we must ensure that all encryptions with key k use a valid encryption randomness (i.e. a name which can only appear at the encryption randomness position of the same plain-text). This is checked using the syntactic side-condition senc-rand P k (c) defined below. Definition 23. Let u a meta-term with no message variables. For any name symbol k, we let senc-rand P k (c) hold whenever, for any trace model T and l ⊆ D I (of length arity of k), for any: senc(m, r, k l ) ∈ (c) T then r is a name n p , and it only occurs in (c) T in the subterm senc(m, r, k l ).

b) Remarks: Finally, we have two remarks. First, [START_REF] Bellare | Authenticated encryption: Relations among notions and analysis of the generic composition paradigm[END_REF] only gives a ciphertext validity checking oracle, not a full decryption oracle. The two formulations are equivalent, as the only ciphertexts that can be decrypted to something different than ⊥ c are the one the adversary obtained by querying the encryption oracle. Consequently, the adversary can simulate the decryption oracle.

Second, we consider a randomized symmetric encryption scheme here. A similar cryptographic assumption and rule of our meta logic can be defined for deterministic symmetric encryptions (using unique initialisation vectors).

APPENDIX C EQUIVALENCE RULES

We present in this Section the remaining equivalence rules, and the soundness proofs missing from the body. a) XOR equivalence rule: The Fig. 11 defines our XOR-FRESH rule, which expresses the information hiding capabilities of XOR. Together with the rules of Section V, these are the only rules that we need to reason about protocols involving XOR. In a nutshell, the rule expresses that t ⊕ n[ i ] and n[ i ] are interpreted as the same probability distribution provided that n[ i ] is fresh (this guarantees the independence Base logic rule: of distributions) and that the distributions yield messages of the same length. In details, we rely on a base logic rule that differs from the one of [START_REF] Comon | Formal computational unlinkability proofs of RFID protocols[END_REF]. We first establish its soundness (see Proposition 6), and then lift it using the same overapproximation of the freshness condition as for FRESH.

∆ u ∼ v , if len(t) = len(n) then n else t ⊕ n ∆ u ∼ v , t ⊕ n where n ∈ st( v , t) Meta-logic rule: ∆ u ∼ v , if len(t) = len(n[ i ]) ∧ Fresh n[ i ] P2 ( v , t) then n[ i ] else t ⊕ n[ i ] ∆ u ∼ v , t ⊕ n[ i ]
b) Soundness: We now prove the soundness of our rules.

Proposition 5. Rule FRESH is sound.

Proof sketch. Consider an instance of the rule with a valid premise, and conclusion φ. Let us show that, for any T and M satisfying ∆, we also have T, M |= φ. Note that (Fresh

n[ i ] P1 ( u)) T
P1 is a boolean combination of constants true and false, and similarly for the other freshness formula.

It cannot be that the interpretation of one formula is equivalent to true and the other to false, as this would contradict the validity of the premise. If the two interpretations are false, the premise is equivalent to the conclusion, so we conclude trivially.

Otherwise, the two freshness formulas interpret to true. This implies that n σ I ( i ) is not a subterm of ( u ) T P1 , and correspondingly for m σ I ( j ) and v . The validity of the premise gives us

T, M |= ( u ) T P1 , empty ∼ ( v ) T P2 , empty, which implies T, M |= ( u ) T P1 ∼ ( v ) T P2 .
We can finally apply the FRESH rule of the base logic to obtain T, M |= φ as expected. Proposition 6. Rule XOR-FRESH is sound in all computational models where ⊕ is interpreted as XOR.

Proof. It suffices to show that the base logic rule is sound, then the lifting works as for FRESH. We express the advantage of an attacker on the indistinguishability game of the conclusion, where L is the random variable len(t) = len(n) and t is

Base logic Rule Meta-logic Rule ∆ u , C if HFresh k (t; u , C, t) then n else H(t, k) ∼ v ∆ u , C[H(t, k)] ∼ v ∆ u , C if HFresh k[ i ] P 1 (t; u , C, t) then n else H(t, k[ i ]) ∼ v ∆ u , C[H(t, k[ i ])] ∼ v when n ∈ st( u , C, t), k H(_,•) ( u , C, t) when n P 1 • st( u , C, t), k P 1 H(_,•) ( u , C, t)
and HFresh k (t; u For any set S of meta-terms of sort timestamp, define Honest S as the least set of meta-formulas and metaterms that contains atomic meta-formulas over indices and timestamps and is closed under function application, boolean connectives, and the following rules, where Q stands for any quantification over timestamp or index variables, and the quantified variable is assumed to be disjoint from the variables occurring in S: for any meta-term of meta-formula ξ ∈ Honest S for some set S containing T and such that4 (T ) T ≤ (T ) T for all T ∈ S.

) def = H(m,k)∈st( u ) m = t and HFresh k[ i ] P (t; u ) def = (H(m,k[ i 0 ]), j ,c)∈ st P ( u ) ∀ j . ( i = i0 ∧ c) ⇒ m = t
T ∈ S φ ∈ Honest S∪{T } (T ≤ T ⇒ φ) ∈ Honest S φ ∈ Honest S Q.φ ∈ Honest S T ∈ S φ ∈ Honest S∪{T } (T ≤ T ∧ φ) ∈ Honest S t, t ∈ Honest S (t = t ) ∈ Honest S T ∈ S or pred(T ) ∈ S input@T ∈ Honest S T ∈ S output@T ∈ Honest S
We proceed by structural induction on ξ.

• Assume ξ is of the form φ 1 ∧ φ 2 with φ 1 , φ 2 ∈ Honest S . By equational reasoning we can replace if (exec@T ) T P1 then (φ) T P1 else false by

(if (exec@T ) T P1 then (φ 1 ) T P1 else false) . ∧ (if (exec@T ) T P1 then (φ 2 ) T P1 else
false) and similarly on the other side. We conclude by the FA rule on . ∧ and induction hypotheses on φ 1 and φ 2 : we invoke the induction hypothesis on φ 1 with U and V , and then use the induction hypothesis on φ 2 with the sequence U (resp. V ) enriched with (frame@T ) T P1 , if (exec@T ) T P1 then (ξ) T P1 else false with i = 1 (resp. i = 2).

• The other boolean connectives cases (e.g. ∨), the case t = t and the case where ξ is a function application are identical to the φ 1 ∧ φ 2 case.

• Assume ξ is of the form T ≤ T ⇒ φ . There are two subcases:

-

If (T ) T ≤ (T ) T then (T ≤ T ⇒ φ ) T Pi is true . ⇒ (φ ) T
Pi for i ∈ {1, 2}. By equational reasoning on .

⇒ we can thus replace the interpretation of ξ by that of φ . Moreover, our condition on S extends to S ∪ {T }. We conclude by induction hypothesis on φ ∈ Honest S∪{T } . -Otherwise, each (T ≤ T ⇒ φ ) T Pi can be replaced by true and we conclude by FA on each if (exec@T ) T Pi then true else false, followed by FA on true and false, and DUP on exec@T .

• The case T ≤ T ∧ φ is similar to the second case above.

• Assume ξ is of the form Q.φ . By definition, (φ) T Pi is a boolean combination of (φ ) T Pi where T only differs from T in its semantic assignment for the quantified variable. Since this variable is assumed to not occur in S, the condition on S w.r.t. T also holds w.r.t. T , and the condition T w.r.t. T also holds w.r.t. T . We proceed as we did in the first case for a simple boolean combination, i.e. by pushing the conditional on exec@T underneath boolean connectives, using FA on boolean connectives and concluding by induction hypotheses on φ and T .

• If ξ is an atom over index or timestamp meta-terms, then the translation of ξ is independent of the protocol, i.e.

(ξ) T P1 = (ξ) T P2 , and is either true or false. We can thus conclude by induction hypothesis.

• Consider the case of a meta-term output@T for some T ∈ S. By hypothesis on S we have (T ) T ≤ (T ) T . Therefore, there exists some context C using fst and snd such that

EQ (if exec@T then output@T ) T Pi , C[(frame@T ) T Pi ]
∼ true.

Note that we omitted the else branch for conciseness, as it does not play a role. In other words, we have almost extracted (output@T ) T Pi from (frame@T ) T Pi . We now bridge the gap between the element in our sequence (i.e. an output) and what we can extract from the frame (i.e. an output under a conditional). Since T and T coincide except for the interpretation of variables that do not occur in T , we have (exec@T ) T Pi = (exec@T ) T Pi . Moreover, (exec@T ) T Pi is of the form (exec@T ) hand, EASYCRYPT does not have rules dedicated to cryptographic reasoning, but allows to carry out such reasoning using its lower-level, very expressive logics. As a direct consequence, proofs are considerably shorter in CRYPTOVERIF and SQUIRREL than in EASYCRYPT.

B. Quantitative Comparison

As a basic quantitative metric, we give in Table II the lines of code (LoC) needed to prove the authentication and unlinkability properties of the Basic Hash protocol in each tool, distinguishing the modelling and proof parts. We notice that SQUIRREL and CRYPTOVERIF have similar LoC values, with the difference that CRYPTOVERIF concludes automatically for the authentication proof. The EASYCRYPT development is sensibly longer, which was expected considering the fact that it is a general purpose proof assistant, relying on an expressive high-order logic.

We stress the fact that the LoC metric only gives a very rough idea of the modelling and proof efforts required to perform our case study analysis. For example, a large part of the EASYCRYPT development are low-level Hoare-logic proofs which, while being protracted, are elementary.

C. Qualitative comparison: modelling protocols

In CRYPTOVERIF, protocols are modelled using a variant of the applied-pi calculus. This language is similar to the input language of SQUIRREL. We note however that SQUIRREL can model trace restrictions, which can be used, for example, to model protocol phases (see Example 6). Phases and trace restrictions are not supported by CRYPTOVERIF.

EASYCRYPT has been mostly used for security analysis of cryptographic primitives. These are modelled using modules, which are simply lists of procedures. These procedures operate on a global memory and can perform random samplingsthey are stateful probabilistic programs. A key feature of the module system is its composability: a module F -a functor -can be parameterized by other modules by taking them as arguments. For example, an encryption schema can be defined w.r.t. an unspecified block permutation. The same mechanism can be used for protocols, modelling an input/output pair as a module procedure. Note however that when modelling a protocol in which an agent performs sequentially multiple pairs of input/output, the modelling becomes more complex, as we need to maintain in a global state the position of the agent in this sequence (this problem does not appear in Basic Hash, as each agent comprises only one input/output pair). D. Qualitative Comparison: modelling security properties a) Correspondence Properties: In CRYPTOVERIF, the processes of the protocol agents can be annotated by events. Crucially, events do not modify the agents behavior: they are only added to the execution trace of the protocol, where they can be used to express properties of the protocol.

Modelling correspondence properties in SQUIRREL is very similar, though we do not use events: we directly refer to the values of components of the protocol (e.g. nonces, messages) at various points of the protocol execution using timestamps.

Expressing correspondence properties in EASYCRYPT requires more work. For the Basic Hash protocol, we had to modify the protocol agents to add some bookkeeping of the events: essentially, events are manually logged into some global tables. Security properties are then expressed in the same way as in CRYPTOVERIF or SQUIRREL.

Contrarily to our timestamp approach where nothing is added, and to CRYPTOVERIF events that are just annotations leaving the protocol behavior unchanged, the EASYCRYPT modelling of correspondence properties has the drawback that it requires to modify the protocol to add the global tables of events: the protocol shown secure is not the original protocol. Of course, this problem can be solved by doing the modelling in several steps: i) define the original protocol; ii) define the protocol with events; and iii) show that the two protocols have the same behavior (except for the global tables). Nonetheless, this requires some additional work from the user.

Arguably, a minor advantage of our approach compared to CRYPTOVERIF is that it allows to have more concise protocol descriptions, as we do not need to modify the protocol specification itself. For example, new correspondence properties can be added to a development without changing the protocol.

b) Equivalence properties: CRYPTOVERIF models equivalence properties as the indistinguishability of two protocols (given as two distinct processes), whereas in SQUIRREL the two protocols have to be given in a bi-process.

EASYCRYPT models equivalences using relational probabilistic Hoare logic formulas (pRHL), which state that, assuming that the initial memories of the left and right programs satisfy some relational property (the pre-condition), the final memories satisfy some other relational property (the postcondition). This is a very expressive logic, which goes beyond bare equivalence: e.g., we can write a pRHL formula that (roughly) states that an event happened on the left program less often than on the right program.

E. Modelling: cryptographic assumptions

The analyses have been carried out using the same cryptographic assumptions: the keyed hash function is assumed EUF-CMA and PRF. Although the cryptographic assumptions are the same, their modelling differs.

CRYPTOVERIF offers a large panel of predefined cryptographic primitives: when modelling a protocol, a user has to import the appropriate cryptographic primitives and assumptions they need. Notably, these are modelled using a specification language, which let the user declares sets of indistinguishable oracles available to the adversary. While an experienced user can theoretically use this system to define their own cryptographic assumptions, we remark that some of the default assumptions have been modified in non-trivial ways, probably to use alternative equivalent formulations that are more powerful and can be used automatically by the tool. Consequently, adding complex new assumptions may be outof-reach of most users.

In EASYCRYPT, cryptographic assumptions are expressed through games, using the same programming language and module system than for protocols, and the user can define new cryptographic hypotheses if needed. Moreover, this can be done easily, as the language used to express assumptions is very close to the pseudo-code language used by cryptographers for paper proofs.

SQUIRREL cryptographic hypotheses are hard-coded in the prover, and adding now cryptographic hypothesis is not straightforward: it requires to do non-trivial syntactic checks, and to compute complex sets of subterms. E.g., for the EUF-CMA, we must compute the set of hashes appearing in a protocol execution for a given key, and the condition on the trace under which each of these hashes appears.

F. Security proofs

The main differences between CRYPTOVERIF and SQUIR-REL lie in the way proofs are handled. Each step of the proof is a transformation of a cryptographic game in CRYPTOVERIF, while in SQUIRREL the transformation is applied to formulas and frames. As a first consequence of this difference, CRYPTOVERIF does not handle states, while we are confident that SQUIRREL will be able to support stateful protocols. 7Both tools have basic proof steps dedicated to cryptographic reasoning: CRYPTOVERIF applies cryptographic assumptions by replacing a set of oracles by an indistinguishable set of oracles, while SQUIRREL has specialized inference rules.

EASYCRYPT proofs are done at two levels. First, the equivalence between two protocols (modelled as modules) can be shown using a probabilistic relational Hoare logic (pRHL). To complete such proofs, the user often has to come up with (relational) invariants of the programs, and to perform precise probabilistic reasoning. Then, such results can be composed using its ambient higher-order logic (e.g. a property shown for an arbitrary block permutation can be instantiated to a precise permutation, say AES). Among these three tools, EASYCRYPT is the only one that allows to prove high-level composition results (e.g. the Universal Composability framework has been formalized in EASYCRYPT [START_REF] Canetti | Easyuc: Using easycrypt to mechanize proofs of universally composable security[END_REF]). On the other hand, and in contrast with CRYPTOVERIF and SQUIRREL, EASYCRYPT does not have rules dedicated to cryptographic reasoning. Instead, its pRHL and higher-order logic are expressive enough to carry out cryptographic proofs directly -often at the cost of more details and work.

  hash H abstract ok : message abstract error : message name key : index → message channel c process tag(i,j:index) = new n; out(c, n, H(n,key[i]) ) process reader(j:index) = in(c,x); try find i such that snd(x)=H(fst(x),key[i]) in out(c,ok) else out(c,error)

Fig. 1 .

 1 Fig. 1. Syntax of meta-terms and meta-formulas

Definition 2 .

 2 An action a[i 1 , . . . , i k ].(φ, o) is formed from an action symbol a of index arity k, distinct indices i 1 , . . . , i k , a meta-logic formula φ and a meta-logic term o of sort message such that fv(φ, o) ⊆ {i 1 , . . . , i k }. The formula φ is the condition of the action, and o its output.

Example 4 .

 4 For illustration purposes, we consider a protocol made of two actionsa[i].( , ok) and b[i].( , input@a[i], input@b[i] ) with a[i] < b[i].Intuitively, this corresponds to multiple sessions indexed by i, where each session inputs an arbitrary message, outputs ok, then inputs another message before outputting the pair of the two messages it has received. Note that action b[i] is well-formed because a[i] < b[i] and b[i] only occurs in the action's components through input@b[i].

.∧Example 9 .

 9 v for if u then v else false, and define similarly u . ∨ v and u . ⇒ v. Finally, we write u .= v for EQ(u, v). Consider the following base logic formulas:

Fig. 2 .

 2 Fig. 2. Interpretation of macros, where a[ i].(φ, o) is an action of P A .

Definition 8 .

 8 A sequent Γ φ is formed from a set of metaformulas Γ and a meta-formula φ, both without message variables. The sequent Γ φ is valid w.r.t. a class of models C if (∧Γ) ⇒ φ is valid w.r.t. C. Definition 9. An inference rule Γ 1 φ 1 . . . Γ n φ n Γ φ is sound w.r.t. a class C when the conclusion is valid w.r.t. C whenever the premises are valid w.r.t. C.

Fig. 5 .

 5 Fig. 5. Generic inference rules for equivalences

Fig. 6 .

 6 Fig. 6. Rule FRESH.

Fig. 7 .

 7 Fig. 7. Standard Sequent Calculus for Reachability

Fig. 8 .Proposition 3 .

 83 Fig. 8. Rule NAMEFRESH.

Fig. 9 .

 9 Fig. 9. Subterms with bound index variables i-st( i : u).

  a[ j] hb ∀i.φ def = (m@T, k)∈i-st(φ) ∃i, k.a[ j] hb m@T which is satisfied in T if and only if: ∃i.

b)

  Case ∀i.φ: If u = ∀i.φ, then: (u) T = . ∧ e∈D I (φ) T{i →e} Since st ((u) T ) does not contain the subterms of (u) T that start with . ∧, we have that: st ((u) T ) = e∈D I st ((φ) T{i →e} ) Let e ∈ D I and T = T{i → e}. By induction hypothesis: st ((φ) T ) ⊆ S T φ To conclude, we show that S T φ ⊆ S T u . Le (t, j , c) ∈ st P (φ), k ⊆ D I and T = T { j → k } such that: ∀M, (T , M |= c)

ΓFig. 10 .

 10 Fig. 10. Rule INT-CTXT (meta logic)

Fig. 11 .

 11 Fig. 11. Rule XOR-FRESH (base and meta logic).

Fig. 15 .

 15 Fig. 15. Rule PRF (base and meta logic)

Fig. 16 .

 16 Fig. 16. Honest formulas used in rule FA-DUP.

  Definition 10. A template C[[] 1 , . . . , [] n , •] is a syntactic expression built using the hole variables ([] i ) 1≤i≤n , the special variable •, and applications of function symbols f ∈ F B (with the correct arity) such that • occurs exactly once in C. For any base terms t 1 , . . . , t n , t, we let C[t 1 , . . . , t n , t] be the base term obtained by substituting the hole variables and • by the terms t 1 , . . . , t n , t. When possible, we omit the hole variables and write C[_, •]. Definition 11. Let C[_, •] be a template, u a ground base term and n a name. Then n C u holds whenever n appears in u only in subterms of the form C[ w , n] for some w .

	Example 13. We give two examples:

• n • u states that n does not appear in u.• k H(_,•) u states that k appears only as a hash key in u.Roughly, the EUF-CMA rule states that if s is a valid hash of m, then m must be equal to some honestly hashed message

This is important to establish the soundness of some tactics, e.g. the one used to remove useless indices of the try find command.

This requires that binders in u use distinct variable names, and do not bind a free variable of u. This can be assumed w.l.o.g. through alpha-renaming.

Indeed, we know that (T ) T is not init, and T is T where we changed the interpretation of i . Since i is disjoint from fv(u) (this is guaranteed by st P ), we know that (T ) T = (T ) T .

We do not specify P 1 or P 2 here as they are irrelevant to the interpretation of timestamp meta-terms.

Of course, we also used existing case studies in the literature (e.g.[START_REF] Comon | Formal computational unlinkability proofs of RFID protocols[END_REF],[START_REF] Cortier | Machinechecked proofs of privacy for electronic voting protocols[END_REF],[START_REF] Lipp | A mechanised cryptographic proof of the wireguard virtual private network protocol[END_REF]), albeit not of the same protocol, to build a detailed description of how each tool operates.

See examples/{README.md, cryptoverif/, easycrypt/}

The CCSA approach can be naturally adapted to model and prove secure stateful protocols (e.g. see the manual case study of[START_REF] Koutsos | The 5G-AKA authentication protocol privacy[END_REF]).

CCA1

∆ P 1 ,P 2 u ∼ v, C[{zeroes(len(t))} r pk(k[ i ]) ] ∆ P 1 ,P 2 u ∼ v, C[{t} r pk(k[ i ]) ] when r P 2

• ( v , t, k[ i ], C), k P 2 pk(•),dec(_,•) ( v , t) and k P 2 pk(•) (C) Fig. [START_REF] Barbosa | SoK: Computeraided cryptography[END_REF]. Rule CCA 1 (meta logic)

ENC-KP if len(t) = len(n) then n else t ⊕ n:

The freshness condition n ∈ st( u , t) implies that the distributions v , t ⊕ n and v , n are the same, provided that L holds. Moreover, when ¬L, the terms t ⊕ n and t evaluate to the same result. We can thus rewrite our advantage as follows:

In other words the advantage is the same for the premise and conclusion, thus the rule is sound. c) Additional cryptographic rules: Our CCA 1 rule, shown in Fig. 12, uses the function symbol zeroes which is assumed to be interpreted, in all computational models, as the machine returning a string of 0 of the given length. Our meta-level rule can be obtained as a lifting of the base logic rule CCA s 1 of [START_REF] Koutsos | Preuves symboliques de propriétés d'indistinguabilité calculatoire[END_REF], using transitivity and function application rules to handle the context C. For this rule and the following ones, we extend Definition 11 to handle multiples matching patterns:

for some w. When t is a context we also impose that the terms w do not contain its hole variable -otherwise the syntactic side condition would not carry to the base logic rule after the application of function applications to get rid of the context.

We show in Fig. 13 our meta-logic rule for encryption key privacy [START_REF] Bellare | Key-privacy in public-key encryption[END_REF]. This rule is obtained as a lifting of a variant of the base logic ENC-KP axiom of [START_REF] Bana | A computationally complete symbolic attacker for equivalence properties[END_REF], relying on the IK-CCA notion instead of the IK-CPA notion of [START_REF] Bellare | Key-privacy in public-key encryption[END_REF].

Finally, Fig. 14 gives our lifting of the DDH rule from [START_REF] Bana | Verification methods for the computationally complete symbolic attacker based on indistinguishability[END_REF]. Remark that this last rule allows to directly close the goal when the sequent is a valid instance of a DDH game. In the tool, the rules for encryption support indexed names r, and incorporate a condition as in rule FRESH to guarantee freshness.

Finally, we define in Fig. 15 our rule PRF. Intuitively, the cryptographic assumption PRF allows us to replace the hash of

• ( u ) when P 2 is equal to P 1 in which all occurrences of ab have been replaced by c Fig. 14. Rule DDH (meta logic) some message by a new random value, provided that hashing key is well-used and that the message has not been hashed before. This is expressed in the base logic rule, which is a variant of the PRF rule of [START_REF] Comon | Formal computational unlinkability proofs of RFID protocols[END_REF], and then lifted to the metalogic using the same techniques as before.

d) The FA-DUP rule: We provide in Fig. 16 the definition of our sets Honest S of honest meta-formulas and metaterms. The rule FA-DUP assumes that frame@T is available on both sides of the equivalence. This entails that the attacker has output@T for any T such that T ≤ T ∧ exec@T holds. To ensure this condition, we impose that the formula φ occurs in a context where exec@T is known to hold, and our definition of Honest {T } guarantees (among other things) that subterms of φ of the form input@T are for timestamps T ≤ T . Proposition 7. Rule FA-DUP is sound.

Proof. In this argument, the computational model and ∆ do not play a role: we are simply showing that, for any trace model, our rule can be derived from base logic rules. Consider some trace model T, and assume that ( u , frame@T ) T P1 ∼ ( v , frame@T ) T P2 is a valid base logic formula. We show that

Using equational reasoning on .

∧, we can replace

and similarly on the other side. Then by FA and DUP on exec@T , we reduce our equivalence to proving the one where the last items of frames are replaced by if (exec@T ) T Pi then (φ) T Pi else false: in more detail, we observe that EQ (exec@T ) T Pi , (fst(fst(frame@T ))) T Pi ∼ true holds, which allows us to replace the first term by the second, to conclude by removing the applications of fst using FA and get rid of frame@T using DUP.

We will actually prove more generally that, for any sequences of base terms U and V such that U , (frame@T ) T P1 ∼ V , (frame@T ) T P2 , we have U , (frame@T ) T P1 , if (exec@T ) T P1 then (ξ) T P1 else false ∼ V , (frame@T ) T P2 , if (exec@T ) T P2 then (ξ) T P2 else false for any T that only differs from T for the semantic assignment of index and timestamp variables that do not occur in T , and Therefore (exec@T ) T Pi holds in the then branch of (exec@T ) T Pi . Putting everything together, we get:

∼ true.

We obtain our equivalence statement by performing the replacement permitted by this equality, and conclude by FA on the conditional, then on the fst and snd symbols in C. Finally, we remove exec@T and frame@T using DUP.

• Finally, if we have a meta-term input@T where either T ∈ S of pred(T ) ∈ S, we proceed roughly as in the previous case. First, we know that (input@T ) T Pi = att((frame@pred(T )) T Pi ). By hypothesis on T we have (pred(T )) T ≤ (T ) T . Moreover, (frame@pred(T )) T Pi is a subterm of (frame@T ) T Pi = (frame@T ) T Pi , which can be accessed using a number of applications of snd. We can thus replace (input@T ) T Pi by att(snd n ((frame@T ) T Pi )), which allows to conclude using FA and DUP.

APPENDIX D NUMBER OF SESSIONS DEPENDING ON η

We give here an example of two protocols P and P I that can be distinguished by an adversary which can interact q(η) times with the protocol, where q is a polynomial, but cannot be distinguished by an adversary which interacts k times with the protocol (where k is an arbitrary fixed integer, independent of η). The construction of P is as follows. First, the protocol samples uniformly at random a bitstring n of length η. Then, when queried with an integer input i, the protocol leaks bit(n, i) -the i th bit of the nonce n. Finally, the adversary wins the game if they can find n. The idealised protocol P I is identical to P , except that the adversary never wins:

else out(c 4 , false)

Clearly, there exists an adversary A that can distinguish between P and P I by interacting η+1 times with the protocol: this adversary queries all bits of n using η queries, and then sends n to the protocol. In that scenario, P returns true while P I returns false, which are trivial to distinguish. Of course, an adversary interacting at most k times with the protocol cannot learn more than k bits of n, and has a winning probability of at most 2 k-η . Such an adversary has a negligible probability of winning (w.r.t. η).

APPENDIX E COMPARISON WITH EXISTING TOOLS

To deepen the comparison between SQUIRREL, CRYP-TOVERIF and EASYCRYPT, we conducted a security analysis of the same protocol in the three tools. 5 More precisely, we modelled the Basic Hash protocol, and proved that it provides authentication and unlinkability. The corresponding SQUIRREL, CRYPTOVERIF and EASYCRYPT files can be found in the repository [START_REF]The Squirrel Prover repository[END_REF]. 6 We start by presenting the summary of the key findings of our comparison in Appendix E-A. This summary is based on the basic quantitative comparison of the three approaches in Appendix E-B, and an in-depth qualitative comparison conducted in Appendices E-C, to E-F, where we compare the three approaches on how protocols, security properties and cryptographic assumptions are modelled, and on how security proofs are carried out.

A. Summary of key findings

Generally, we conclude that CRYPTOVERIF and SQUIRREL operates at a similar level of details and expressivity, though they use different approaches, and proofs developments. On the other hand, EASYCRYPT is more expressive, at the cost of a higher level of details and modelling overhead.

a) Protocols: Protocols are modelled in very similar fashion in CRYPTOVERIF and SQUIRREL. Writing a protocol in EASYCRYPT may require a more involved modellingbecause it does not support directly protocols with sequences of inputs/outputs.

We note that CRYPTOVERIF does not support stateful protocols, while EASYCRYPT does. The CCSA approach on which SQUIRREL is based upon can naturally model stateful protocols [START_REF] Koutsos | The 5G-AKA authentication protocol privacy[END_REF] -such an extension is left as future work.

b) Security properties: From our case study, the three tools appeared equally capable of expressing all usual security properties, albeit using different approaches. However, we note that: i) native support for events or timestamps in CRYP-TOVERIF and SQUIRREL allows for more direct and simpler statements of correspondence properties; and ii) EASYCRYPT logic is more expressive, and allows to formalize more complex relational properties of protocols, and to internalize composition results and reasoning (though we did not much exploit this in our case study). c) Cryptographic assumptions: Adding new cryptographic assumptions in EASYCRYPT is easy, as it uses a very expressive logic. While CRYPTOVERIF provides a way to add new assumptions, doing it in a way that can be efficiently used by the tool probably requires a deep understanding of the tool. On the other side of the spectrum, we have SQUIRREL, where adding new hypotheses is not possible without in-depth knowledge of the tool. d) Proofs: Proofs in CRYPTOVERIF and SQUIRREL mostly focus on the security aspects, thanks to native support for cryptographic reasoning, although using different approaches: the former uses cryptographic game transformation, while the latter operates on the protocol traces. On the other