Bruno Blanchet
email: bruno.blanchet@inria.fr

ProVerif is an automatic symbolic protocol verifier. It supports a wide range of cryptographic primitives, defined by rewrite rules or by equations. It can prove various security properties: secrecy, authentication, and process equivalences, for an unbounded message space and an unbounded number of sessions. It takes as input a description of the protocol to verify in a dialect of the applied pi calculus, an extension of the pi calculus with cryptography. It automatically translates this protocol description into Horn clauses and determines whether the desired security properties hold by resolution on these clauses. This survey presents an overview of the research on ProVerif.

Introduction 1.Verifying security protocols

The verification of security protocols has been an active research area since the 1990s. This topic is interesting for several reasons. Security protocols are ubiquitous: they are used for e-commerce, wireless networks, credit cards, e-voting, among others. The design of security protocols is notoriously error-prone. This point can be illustrated by attacks found against many published protocols. For instance, a famous attack was discovered by [START_REF] Lowe | Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR[END_REF] against the Needham-Schroeder public-key protocol [START_REF] Needham | Using Encryption for Authentication in Large Networks of Computers[END_REF] 17 years after its publication. Attacks are also found against many protocols used in practice. Important examples are SSL (Secure Sockets Layer) and its successor TLS (Transport Layer Security), which are used for https:// connexions. The first version dates back to 1994, and since then many attacks were discovered, fixed versions were developed, and new attacks are still regularly discovered [START_REF] Beurdouche | A Messy State of the Union: Taming the Composite State Machines of TLS[END_REF][START_REF] Adrian | Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice[END_REF]. Moreover, security errors cannot be detected by functional testing, since they appear only in the presence of a malicious adversary. These errors can also have serious consequences. Hence, the formal verification or proof of protocols is particularly desirable.

Modeling security protocols

In order to verify protocols, two main models have been considered:

• In the symbolic model, often called Dolev-Yao model and due to Needham and[START_REF] Needham | Using Encryption for Authentication in Large Networks of Computers[END_REF][START_REF] Dolev | On the Security of Public Key Protocols[END_REF][START_REF] Dolev | On the Security of Public Key Protocols[END_REF], cryptographic primitives are considered as perfect blackboxes, modeled by function symbols in an algebra of terms, possibly with equations. Messages are terms on these primitives and the adversary can compute only using these primitives. This is the model usually considered by formal method practitioners.

• In contrast, in the computational model, messages are bitstrings, cryptographic primitives are functions from bitstrings to bitstrings, and the adversary is any probabilistic Turing machine. This is the model usually considered by cryptographers.

The symbolic model is an abstract model that makes it easier to build automatic verification tools, and many such tools exist: AVISPA [START_REF] Armando | The AVISPA tool for Automated Validation of Internet Security Protocols and Applications[END_REF], FDR [START_REF] Lowe | Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR[END_REF], Scyther [START_REF] Cremers | Unbounded verification, falsification, and characterization of security protocols by pattern refinement[END_REF], Tamarin [START_REF] Schmidt | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties[END_REF], for instance. The computational model is closer to the real execution of protocols, but the proofs are more difficult to automate; we refer the reader to (Blanchet, 2012a) and to Chapter 6 for some information on the mechanization of proofs in the computational model. Most often, the relations between cryptographic primitives given in the symbolic model also hold in the computational model. 1 In this case, an attack in the symbolic model directly leads to an attack in the computational model, and a practical attack. However, the converse is not true in general: a protocol may be proved secure in the symbolic model, and still be subject to attacks in the computational model. For this reason, the computational soundness approach was introduced: it proves general theorems showing that security in the symbolic model implies security in the computational model, modulo additional assumptions. However, since the two models do not coincide, this approach typically requires strong assumptions on the cryptographic primitives (for instance, encryption has to hide the length of the messages) and on the protocol (for instance, absence of key cycles, in which a key is encrypted under itself; correctly generated keys, even for the adversary). This approach was pioneered by [START_REF] Abadi | Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)[END_REF] This work triggered much research in this direction; we refer to [START_REF] Cortier | A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems[END_REF] for a survey.

Even though the computational model is closer to reality than the symbolic model, we stress that it is still a model. In particular, it does not take into account side channels, such as timing and power consumption, which may give additional information to an adversary and enable new attacks. Moreover, one often studies specifications of protocols. New attacks may appear when the protocol is implemented, either because the specification has not been faithfully implemented, or because the attacks rely on implementation details that do not appear at the specification level.

In this survey, we focus on the verification of specifications of protocols in the symbolic model. Even though it is fairly abstract, this level of verification is relevant in practice as it enables the discovery of many attacks.

Target security properties

Security protocols can aim at a wide variety of security goals. The main security properties can be classified into two categories, trace properties and equivalence properties. We define these categories and mention two particularly important examples: secrecy and authentication. These are two basic properties required by most security protocols. Some protocols, such as e-voting protocols [START_REF] Delaune | Verifying Privacy-type Properties of Electronic Voting Protocols[END_REF], require more complex and specific security properties, which we will not discuss.

Trace and equivalence properties

Trace properties are properties that can be defined on each execution trace (each run) of the protocol. The protocol satisfies such a property when it holds for all traces. For example, the fact that some states are unreachable is a trace property.

Equivalence properties mean that the adversary cannot distinguish two processes (that is, protocols). For instance, one of these processes can be the protocol under study, and the other one can be its specification. Then, the equivalence means that the protocol satisfies its specification. Therefore, equivalences can be used to model many subtle security properties. Several variants exist (observational equivalence, testing equivalence, trace equivalence) [START_REF] Abadi | A Calculus for Cryptographic Protocols: The Spi Calculus[END_REF]Abadi and Gordon, 1998;[START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF]. Observational equivalence provides compositional proofs: if a protocol P is equivalent to P , P can be replaced with P in a more complex protocol. However, the proof of equivalences is more difficult to automate than the proof of trace properties: equivalences cannot be expressed on a single trace, they require relations between traces (or processes).

Secrecy

Secrecy, or confidentiality, means that the adversary cannot obtain some information on data manipulated by the protocol. Secrecy can be formalized in two ways:

• Most often, secrecy means that the adversary cannot compute exactly the considered piece of data. In this survey, this property will simply be named secrecy, or when emphasis is needed, syntactic secrecy.

• Sometimes, one uses a stronger notion, strong secrecy, which means that the adversary cannot detect a change in the value of the secret [START_REF] Abadi | Secrecy by Typing in Security Protocols[END_REF][START_REF] Blanchet | Automatic Proof of Strong Secrecy for Security Protocols[END_REF]. In other words, the adversary has no information at all on the value of the secret.

The difference between syntactic secrecy and strong secrecy can be illustrated by a simple example: consider a piece of data for which the adversary knows half of the bits but not the other half. This piece of data is syntactically secret since the adversary cannot compute it entirely, but not strongly secret, since the adversary can see if one of the bits it knows changes. Syntactic secrecy cannot be used to express secrecy of data chosen among known constants. For instance, talking about syntactic secrecy of a boolean true or false does not make sense, because the adversary knows the constants true and false from the start. In this case, one has to use strong secrecy: the adversary must not be able to distinguish a protocol using the value true from the same protocol using the value false. These two notions are often equivalent [START_REF] Cortier | Relating two standard notions of secrecy[END_REF], for atomic data (data that cannot be split into several pieces, such as nonces, which are random numbers chosen independently at each run of the protocol) and for probabilistic cryptographic primitives. Syntactic secrecy is a trace property, while strong secrecy is an equivalence property.

Authentication

Authentication means that, if a participant A runs the protocol apparently with a participant B, then B runs the protocol apparently with A, and conversely. One often requires that A and B also share the same values of the parameters of the protocol. Authentication is generally formalized by correspondence properties [START_REF] Woo | A Semantic Model for Authentication Protocols[END_REF][START_REF] Lowe | A Hierarchy of Authentication Specifications[END_REF], of the form: if A executes a certain event e 1 (for instance, A terminates the protocol with B), then B has executed a certain event e 2 (for instance, B started a session of the protocol with A). There exist several variants of these properties. For instance, one may require that each execution of e 1 corresponds to a distinct execution of e 2 (injective correspondence) or, on the contrary, that if e 1 has been executed, then e 2 has been executed at least once (non-injective correspondence). The events e 1 and e 2 may also include more or fewer parameters depending on the desired property. These properties are trace properties.

Symbolic verification

Basically, to verify protocols in the symbolic model, one computes the set of terms (messages) that the adversary knows. If a message does not belong to this set, then this message is secret. The difficulty is that this set is infinite, for two reasons: the adversary can build terms of unbounded size, and the considered protocol can be executed any number of times. Several approaches can be considered to solve this problem:

• One can bound the size of messages and the number of executions of the protocols. In this case, the state space is finite, and one can apply standard model-checking techniques. This is the approach taken by FDR [START_REF] Lowe | Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR[END_REF] and by SATMC [START_REF] Armando | SATMC: a SATbased Model Checker for Security-critical Systems[END_REF], for instance.

• If we bound only the number of executions of the protocol, the state space is infinite, but under reasonable assumptions, one can show that the problem of security protocol verification is decidable: protocol insecurity is NP-complete [START_REF] Rusinowitch | Protocol Insecurity with Finite Number of Sessions is NP-complete[END_REF]. Basically, the non-deterministic Turing machine guesses an attack and polynomially checks that it is actually an attack against the protocol. There exist practical tools that can verify protocols in this case, using for instance constraint solving as in Cl-AtSe [START_REF] Turuani | The CL-Atse Protocol Analyser[END_REF] or extensions of model checking as in OFMC [START_REF] Basin | OFMC: A symbolic model checker for security protocols[END_REF].

• When the number of executions of the protocol is not bounded, the problem is undecidable [START_REF] Durgin | Multiset Rewriting and the Complexity of Bounded Security Protocols[END_REF] for a reasonable model of protocols. Hence, there exists no automatic tool that always terminates and solves this problem. However, there are several approaches that can tackle an undecidable problem:

-One can rely on help from the user. This is the approach taken for example by Isabelle [START_REF] Paulson | The Inductive Approach to Verifying Cryptographic Protocols[END_REF], which is an interactive theorem prover, Tamarin [START_REF] Schmidt | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties[END_REF], which just requires the user to give a few lemmas to help the tool, or Cryptyc [START_REF] Gordon | Types and Effects for Asymmetric Cryptographic Protocols[END_REF], which relies on typing with type annotations.

-One can have incomplete tools, which sometimes answer "I don't know" but succeed on many practical examples. For instance, one can use abstractions based on tree-automata to represent the knowledge of the adversary [START_REF] Monniaux | Abstracting Cryptographic Protocols with Tree Automata[END_REF][START_REF] Boichut | Validation of Prouvé protocols using the automatic tool TA4SP[END_REF].

-One can allow non-termination, as in Maude-NPA [START_REF] Meadows | The NRL Protocol Analyzer: An Overview[END_REF][START_REF] Escobar | A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties[END_REF].

The symbolic protocol verifier ProVerif represents protocols by Horn clauses, in the line of ideas by [START_REF] Weidenbach | Towards an Automatic Analysis of Security Protocols in First-Order Logic[END_REF]: Horn clauses are first order logical formulas, of the form

F 1 ∧ • • • ∧ F n ⇒ F ,
where F 1 , . . . , F n , F are facts. This representation introduces abstractions. It is still more precise than tree-automata because it keeps relational information on messages. However, using this approach, termination is not guaranteed in general.

Let us compare ProVerif with some other tools that verify protocol specifications in the symbolic model. AVISPA [START_REF] Armando | The AVISPA tool for Automated Validation of Internet Security Protocols and Applications[END_REF] is a platform that offers four different protocol verification back-ends: SATMC [START_REF] Armando | SATMC: a SATbased Model Checker for Security-critical Systems[END_REF] for bounded attack depth (which implies bounded sessions and messages), Cl-AtSe [START_REF] Turuani | The CL-Atse Protocol Analyser[END_REF] and OFMC [START_REF] Basin | OFMC: A symbolic model checker for security protocols[END_REF][START_REF] Mödersheim | The Open-source Fixed-point Model Checker for Symbolic Analysis of Security Protocols[END_REF] for bounded sessions, and TA4SP [START_REF] Boichut | Validation of Prouvé protocols using the automatic tool TA4SP[END_REF] for unbounded sessions.

In contrast, ProVerif focuses only on the case of unbounded sessions, and the Horn-clause abstraction it uses is more precise than the treeautomata abstraction of TA4SP, as mentioned above. SATMC supports basic cryptographic primitives that can be defined by rewrite rules. Cl-AtSe additionally supports exclusive or, Diffie-Hellman exponentiation (including equations of the multiplicative group modulo p), and associative concatenation. OFMC supports cryptographic primitives defined by finite equational theories (theories under which every term has a finite equivalence class) and subterm convergent theories (theories generated by rewrite rules that are convergent, that is, terminating and confluent, and whose right-hand side is either a subterm of the left-hand side or a constant). However, in order to guarantee termination, it bounds the number of instantiations of variables. TA4SP handles algebraic properties of exponentiation and exclusive or. ProVerif supports cryptographic primitives defined by rewrite rules and by equations that satisfy the finite variant property (Comon-Lundh and [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF],

Structure of ProVerif

The structure of ProVerif is represented in Figure 1.1. ProVerif takes as input a model of the protocol in an extension of the pi calculus with cryptography, similar to the applied pi calculus [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF][START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF] and detailed in the next chapter. It supports a wide variety of cryptographic primitives, modeled by rewrite rules or by equations. ProVerif also takes as input the security properties that we want to prove. It can verify various security properties, including secrecy, authentication, and some observational equivalence properties. It automatically translates this information into an internal representation by Horn clauses: the protocol is translated into a set of Horn clauses, and the security properties to prove are translated into derivability queries on these clauses. ProVerif uses an algorithm based on resolution with free selection to determine whether a fact is derivable from the clauses. If the fact is not derivable, then the desired security property is proved. If the fact is derivable, then there may be an attack against the considered property: the derivation may correspond to an attack, but it may also correspond to a "false attack", because the Horn clause representation makes some abstractions. These abstractions are key to the verification of an unbounded number of sessions of protocols.

Chapter 2 presents the protocol specification language of ProVerif. Chapter 3 explains how ProVerif verifies the desired security properties. Chapter 4 relates the protocol specification language of ProVerif to the applied pi calculus [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF][START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF]. Finally, Chapter 5 summarizes some applications of ProVerif and Chapter 6 concludes.

Comparison with previous surveys

Previous surveys on ProVerif [START_REF] Blanchet | Using Horn Clauses for Analyzing Security Protocols[END_REF][START_REF] Blanchet | Automatic Verification of Security Protocols in the Symbolic Model: the Verifier ProVerif[END_REF] focus only on secrecy. The general protocol verification survey Blanchet, 2012b also outlines the verification of secrecy in ProVerif. Previous journal papers present individual features of the tool: secrecy (Abadi and Blanchet, 2005a), correspondences [START_REF] Blanchet | Automatic Verification of Correspondences for Security Protocols[END_REF], and equivalences [START_REF] Blanchet | A Computationally Sound Mechanized Prover for Security Protocols[END_REF] Our habilitation thesis [START_REF] Blanchet | Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire[END_REF], in French, presents a general survey of ProVerif that includes secrecy, correspondences, and equivalences.

This survey is the first one to present all these features in English, in a common framework. Moreover, it includes features that never appeared in previous surveys: the extended destructors of [START_REF] Cheval | Proving More Observational Equivalences with ProVerif[END_REF], the proof of equivalences using swapping (Blanchet and Smyth, 2016), as well as the link with the applied pi calculus (Chapter 4), which was never published before.

The Protocol Specification Language

This chapter presents the protocol specification language used by ProVerif, by giving its syntax and semantics. Our presentation is based on earlier ones (Abadi and Blanchet, 2005a;[START_REF] Blanchet | Automatic Verification of Correspondences for Security Protocols[END_REF][START_REF] Blanchet | Automatic Verification of Security Protocols in the Symbolic Model: the Verifier ProVerif[END_REF], with some features added: extended destructors [START_REF] Cheval | Proving More Observational Equivalences with ProVerif[END_REF], support for equations and phases (Blanchet et al., 2008), enriched terms, pattern-matching, and table of keys (Blanchet et al., 2016).

Core language: syntax and informal semantics

Figure 2.1 gives the syntax of terms (data, messages), expressions (computations on terms), and processes (programs) of the input language of ProVerif. Terms are typed. The types T include channel for channels, bool for boolean values, and bitstring for bitstrings. The user may declare other types. ProVerif checks that processes given by the user are well-typed. This is helpful in order to detect mistakes in protocol specifications. However, by default, it ignores types for the verification of security properties. This behavior allows the adversary to bypass the type system, therefore enabling the detection of type-flaw

M, N ::= terms x, y, z variable a, b, c, k, s name f (M 1 , . . . , M n )
constructor application attacks [START_REF] Heather | How to Prevent Type Flaw Attacks on Security Protocols[END_REF]. For this reason, we remove types in the definition of the formal semantics and in the verification of security properties. If desired, ProVerif can also be configured to take into account types in the verification of security properties. We focus on the default configuration in this survey.

D ::= expressions M term h(D 1 , . . . , D n ) function application fail failure P, Q ::= processes 0 nil out(N, M ); P output in(N, x : T ); P input P | Q parallel composition !P replication new a : T ; P restriction let x : T = D in P else Q expression evaluation if M then P else Q conditional
The identifiers a, b, c, k, and similar ones range over names, and x, y, and z range over variables. Names represent atomic data, such as keys and nonces. Variables can be substituted by terms. Names and variables are declared with their type. The syntax also assumes a set of function symbols for constructors and destructors; we often use f for a constructor, g for a destructor, and h for a constructor or a destructor. Function symbols are declared with types: h(T 1 , . . . , T n ) : T means that the function h takes n arguments of types T 1 , . . . , T n respectively, and returns a result of type T .

Constructors are used to build terms. Therefore, terms are variables, names, and constructor applications of the form f (M 1 , . . . , M n ). For instance, symmetric encryption is typically represented by a constructor senc, and the term senc(c, k) represents the encryption of c under the key k. On the other hand, destructors do not appear in terms, but manipulate terms in expressions. They are functions on terms that processes can apply, via the expression evaluation construct. A destructor g is defined by a finite ordered list of rewrite rules def(g) of the form g(U 1 , . . . , U n ) → U where U 1 , . . . , U n , U are may-fail terms, that is, terms M , the constant fail, which represents the failure of a computation, or may-fail variables u. Hence, we have two kinds of variables: ordinary variables, or simply variables, which can be substituted by terms, and may-fail variables, which can be substituted by may-fail terms. In the rewrite rules, U 1 , . . . , U n , U do not contain names, and the variables of U also occur in U 1 , . . . , U n . The types of U 1 , . . . , U n must be the types of the arguments of g, and the type of U must be the type of the result of g. Destructors occur in expressions D, which evaluate either to a term M or to the special constant fail. To evaluate g(D 1 , . . . , D n ), we first evaluate D 1 , . . . , D n , which yields U 1 , . . . , U n , where each U i is either a term M or the constant fail. Then, we consider the first rewrite rule g(U 1 , . . . , U n ) → U in def(g). If there exists a substitution σ such that σU i = U i for all i ∈ {1, . . . , n}, then this rewrite rule applies and g(D 1 , . . . , D n ) evaluates to σU . Otherwise, the first rewrite rule does not apply, and we consider the second one, and so on. If no rewrite rule applies, the evaluation of g(D 1 , . . . , D n ) fails: it evaluates to the constant fail.

Using constructors and destructors, we can represent data structures, such as tuples, and cryptographic operations, for instance as follows: • senc(M, N ) is the symmetric (shared-key) encryption of the message M under the key N , where senc(bitstring, key) : bitstring is a constructor. The corresponding destructor sdec(bitstring, key) : bitstring is defined by sdec(senc(x, y), y) → x .

• tuple T 1 ,...,Tn (M 1 , . . . , M n ) is the tuple of the terms M 1 , . . . ,
Thus, sdec(M , N ) returns the decryption of M if M is a message encrypted under N . Otherwise, it fails.

• In order to represent asymmetric (public-key) encryption, we may use two constructors pk(skey) : pkey and aenc(bitstring, pkey) : bitstring, where skey is the type of secret keys and pkey is the type of public keys: pk(M ) builds a public key from a secret key M and aenc(M, N ) encrypts M under the public key N . The corresponding destructor adec(bitstring, skey) : bitstring is defined by adec(aenc(x, pk(y)), y) → x .

(2.1)

It decrypts the ciphertext aenc(x, pk(y)) using the secret key y corresponding to the public key pk(y) used to encrypt this ciphertext.

• Cryptographically, a secure asymmetric encryption scheme must be probabilistic. We can represent a probabilistic encryption scheme by adding a third argument to the constructor aenc to represent the randomness. This constructor becomes aenc(bitstring, pkey, rand) : bitstring and the rewrite rule for adec becomes adec(aenc(x, pk(y), z), y) → x .

(2.2)

For protocols that do not test equality of ciphertexts, for secrecy and authentication, one can use the simpler, deterministic model of encryption [START_REF] Cortier | Explicit Randomness is not Necessary when Modeling Probabilistic Encryption[END_REF]. However, for equivalence properties, or for protocols that test equality of ciphertexts, using probabilistic encryption does make a difference. Probabilistic versions can also be defined for symmetric encryption (above) and for digital signatures (below) (Blanchet et al., 2016, §4.2.5); we omit such models here. (2.4)

The destructor check verifies that the signature sign(x, y) is a correct signature under the secret key y, using the public key pk(y). When the signature is correct, it returns the message that was signed. The destructor getmess always returns the message that was signed. (This encoding of signatures assumes that the message that was signed can be recovered from the signature.)

• We may represent a one-way hash function by the constructor h(bitstring) : bitstring. There is no corresponding destructor; so we model that the term M cannot be retrieved from its hash h(M ).

• Boolean constants true : bool and false : bool are nullary constructors, and equality between terms may be defined as a destructor equal(T, T ) : bool with rewrite rules:

equal(x, x) → true , equal(x, y) → false . (2.5)
The second rewrite rule applies only when the first one does not apply, that is, when x = y. We will write M = N for equal(M, N ). Disequality as well as boolean operations (negation not, conjunction &&, disjunction ||) may also be defined as destructors. For instance, conjunction can be defined as a destructor and(bool, bool) : bool with rewrite rules:

and(true, u) → u , and(x, u) → false .

This destructor returns its second argument when its first argument is true, and false when its first argument is a term different from true. (We consider all boolean terms that are not true as false.)

The variable u is a may-fail variable, so that the rewrite rules apply even if the second argument fails. Therefore, and(false, fail) evaluates to false. Hence, and may not fail even if its second argument fails. Intuitively, the second argument need not be evaluated when the first argument is not true. If we replaced u with an ordinary variable y, and would fail when one of its arguments fails, corresponding to the intuition that we would evaluate both arguments before computing the conjunction. We write M && N for and(M, N ) for readability.

We can also define an if-then-else destructor ifthenelse(bool, T, T ) : T with rewrite rules:

ifthenelse(true, u, u ) → u , ifthenelse(x, u, u ) → u .
This destructor returns its second argument when its first argument is true. It returns its third argument when its first argument is a term different from true. Otherwise, that is, when its first argument fails, it fails. Similarly to the conjunction above, the variables u and u are may-fail variables, so that the rewrite rules apply even if the second or third argument fails. As a consequence, ifthenelse(true, M, fail) and ifthenelse(false, fail, M ) both evaluate to M . Hence, ifthenelse may not fail even if its second or third argument fails. Intuitively, the third argument need not be evaluated when the first argument is true, and the second argument need not be evaluated when the first argument is not true.

• Type-converter functions are unary functions, whose only goal is to convert a term from a type to another, so that it has the right type to be passed to other functions. Type-converter functions are declared with the annotation typeConverter so that ProVerif can recognize them. Since it ignores types for the verification of security properties, ProVerif removes type-converter functions at this stage.

For instance, we may define a type-converter function k2b(key) : bitstring, which converts terms from type key to type bitstring, so that keys can be encrypted or signed by the functions defined above. The inverse function b2k(bitstring) : key is defined by the rewrite rule b2k(k2b(x)) → x .

The function k2b always succeeds: all keys are bitstrings; while the function b2k succeeds only when its argument is of the form k2b(M ), that is, the terms k2b(M ) are the only terms of type bitstring that are keys and can be converted to type key.

Thus, destructors defined by rewrite rules support many of the operations common in security protocols. This way of specifying cryptographic primitives also has limitations, though: for example, modular exponentiation cannot be directly represented in this framework. To overcome this limitation, ProVerif supports equations, as explained in §2.5.1.

Most constructs of processes in the syntax of Figure 2.1 come from the pi calculus [START_REF] Milner | A Calculus of Mobile Processes, parts I and II[END_REF].

• The nil process 0 does nothing.

• The input process in(N, x : T ); P inputs a message on channel N , and executes P with x bound to the input message.

The output process out(N, M ); P outputs the message M on the channel N and then executes P .

Here, we use an arbitrary term N to represent a channel: N can be a name, a variable, or a constructor application. The calculus is monadic (in that the messages are terms rather than tuples of terms), but a polyadic calculus can be simulated since tuples are terms. It is also synchronous (in that a process P is executed after the output of a message). We may omit P when it is 0.

• The process P | Q is the parallel composition of P and Q.

• The replication !P represents an unbounded number of copies of P in parallel. It makes it possible to represent an unbounded number of executions of the protocol.

• The restriction new a : T ; P creates a new name a of type T , and then executes P . It can model the creation of a fresh key or nonce.

• The process let x : T = D in P else Q tries to evaluate D; if D evaluates to a term M , then x is bound to M and P is executed; if the evaluation of D fails, then Q is executed. The type T may be omitted when it can be determined from D, that is, when D is not fail.

• The conditional if M then P else Q executes P if M is true (or is a variable bound to true); it executes Q if M is different from true.
We may omit an else branch when it consists of 0.

The name a is bound in the process new a : T ; P . The variable x is bound in P in the processes in(N, x : T ); P and let x : T = D in P else Q. Processes are considered equal modulo renaming of bound names and variables. We write fn(P ) and fv(P ) for the sets of names and variables free in P , respectively. A process is closed if it has no free variables; it may have free names. The protocol to verify is represented by a closed process P 0 . Free names are declared with their type. They may be public or private: the adversary initially has access to the public free names, but not to the private ones. We write N pub for the set of public free names and N priv for the set of private free names, so we have fn(P 0 ) ⊆ N pub ∪ N priv . (One may declare free names not present in P 0 , but used for instance in security queries.) Similarly, function symbols may be public or private: the adversary has access to the public function symbols, but not to the private ones.

We write { M 1 / x 1 , . . . , Mn / xn } for the substitution that replaces x 1 , . . . , x n with M 1 , . . . , M n , respectively. When D is some term, expression, or process, we write D{ M 1 / x 1 , . . . , Mn / xn } for the result of applying this substitution to D, but we write σD when the substitution is simply denoted σ. Except when stated otherwise, substitutions always map variables (not names) to terms. Furthermore, substitutions never substitute fail or a may-fail variable for an ordinary variable.

The calculus of ProVerif resembles the applied pi calculus [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF][START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF]. Both calculi are extensions of the pi calculus with (fairly arbitrary) functions on terms. However, there are also important differences between these calculi. The first one is that ProVerif uses destructors in addition to the equational theories of the applied pi calculus, but does not support all equational theories. ( § 2.5.1 explains how ProVerif handles equations.) The second difference is that ProVerif has a built-in error-handling construct (the else branch of the expression evaluation), whereas in the applied pi calculus the errorhandling must be done "by hand". For instance, in ProVerif, the process let x = sdec(M, k) in P else out(c, error) outputs the error message when the decryption of M fails. In the applied pi calculus, decryption always succeeds, but may return junk, and one has to perform an additional test if one wants to check that M is a ciphertext under the key k.

Chapter 4 provides a more detailed comparison with the applied pi calculus.

An example of protocol

We use as a running example a simplified version of the Denning-Sacco key distribution protocol [START_REF] Denning | Timestamps in Key Distribution Protocols[END_REF], omitting certificates and timestamps:

Message 1. A → B : aenc(sign(k2b(k), ssk A ), pk B ) Message 2. B → A : senc(s, k)
This protocol is illustrated in Figure 2.2. It involves two principals A and B. The key ssk A is the secret, signature key of A and spk A its public, signature verification key. (We add an s prefix for signature keys to distinguish them from encryption keys.) The key sk B is the secret, decryption key of B and pk B its public, encryption key. The key k is a fresh session key created by A. A sends this key, signed with its private key ssk A , and encrypted under the public key of B, pk B . The key k is first converted to a bitstring by k2b, so that it has the right type for signing it. When B receives this message, B decrypts it and assumes, seeing the signature, that the key k has been generated by A. Then B sends a secret s encrypted under k. Only A should be able to decrypt the message and get the secret s. (The second message is not really part of the protocol; we use it to check if the key k can be used to exchange secrets between A and B. In fact, there is an attack against this protocol [START_REF] Abadi | Prudent Engineering Practice for Cryptographic Protocols[END_REF], so s will not remain secret. The attack is explained in Example 3. 2.) This protocol can be encoded by the following process:

B (Bob) A (Alice) senc(s, k) aenc(sign(k2b(k), ssk A ), pk B ) k fresh
P 0 = new
P B (sk B , spk A ) = ! in(c, y : bitstring); let y = adec(y, sk B ) in let x k = b2k(check(y , spk A )) in out(c, senc(s, x k ))
Such a process can be given as input to ProVerif. This process first creates the secret keys ssk A and sk B , computes the corresponding public keys spk A and pk B , and sends these keys on the public channel c, so that the adversary has these public keys. Then, it runs the processes P A and P B in parallel. These processes correspond respectively to the roles of A and B in the protocol. They both start with a replication, which makes it possible to model an unbounded number of sessions of the protocol.

The process P A executes the role of A: it creates a fresh key k, converts it to a bitstring by k2b, signs it with its secret key ssk A , then encrypts this message under pk B , and sends the obtained message on channel c. P A then expects the second message of the protocol on channel c, stores it in x and decrypts it. If decryption succeeds, the result (normally the secret s) is stored in z.

The process P B receives the first message of the protocol on channel c, stores it in y, decrypts it with sk B , and verifies the signature with spk A . If these verifications succeed, B believes that x k is a key shared between A and B, and it sends the secret s encrypted under x k . If the protocol is correct, s should remain secret. In this example, there are two free names, c and s; c is public and s is private, so N pub = {c} and N priv = {s}.

This model of the protocol is weak, because A and B talk only to each other: they do not interact with other, possibly dishonest participants. We can strengthen the model as follows. We replace the process P A with the following process: P A (ssk A , pk B ) = ! in(c, x pk B : pkey); new k : key; out (c, aenc(sign(k2b(k), ssk A ), x pk B )); in(c, x : bitstring); let z = sdec(x, k) in 0 This process P A first receives on the public channel c the key x pk B , which is the public key of A's interlocutor in the protocol. This message is not part of the protocol; it allows the adversary to choose with whom A is going to execute a session. In a standard session of the protocol, this key is pk B , but the adversary can also choose another key, for instance one of his own keys, so that A can interact with the adversary playing the role of a dishonest participant. Then P A executes the role of A as before, with the key x pk B instead of pk B . The process P B does not need to be modified because B sends the second message senc(s, k) only if its interlocutor is the honest participant A. (Otherwise, the secret would obviously be leaked.) Hence the signature is verified with the key spk A of A and not with an arbitrary key chosen by the adversary.

The above model still assumes for simplicity that A and B each play only one role of the protocol. One could easily write an even more general model in which they play both roles, or one could provide the adversary with an interface that allows it to dynamically create new protocol participants. We consider such a model in §2.5.5.

Core language: type system

Processes must be well-typed in the type system of Figure 2.3. For simplicity, all bound variables and names are renamed so that they are pairwise distinct and distinct from free names. The type system uses a type environment Γ that maps variables and names to their type. This type environment initially contains the types of the free names of the closed process under consideration. The type system defines three judgments: the judgment Γ M : T means that the term M is well-typed of type T in the type environment Γ; the judgment Γ D : T means that the expression D is well-typed of type T in the type environment Γ; and the judgment Γ P means that the process P is well-typed in the type environment Γ.

The typing rules are straightforward. The type of variables and names is obtained from the type environment Γ. Function applications h(D 1 , . . . , D n ) are well-typed when their arguments are well-typed, of the type expected by the function h, and the type of h(D 1 , . . . , D n ) is the type of the result of h. The constant fail can be of any type. The rules require that input and output channels be of type channel, that output messages be well-typed, and that conditions be of type bool.

Example 2.1. It is easy to see that the process P 0 of §2.2 is well-typed in the type environment Γ = c : channel, s : bitstring, that is, Γ P 0 .

As mentioned in §2.1, ProVerif checks that processes given by the user are well-typed, but it ignores types and removes type-converter functions for the verification of security properties.

Example 2.2. With types and type-converter functions removed, the process P 0 of §2.2 (version in which A may interact with dishonest participants) becomes:

P 0 = new ssk A ; new sk B ; let spk A = pk(ssk A ) in let pk B = pk(sk B ) in out(c, spk A ); out(c, pk B ); (P A (ssk A , pk B ) | P B (sk B , spk A )) Γ D : T Γ, x : T P Γ Q Γ let x : T = D in P else Q Γ M : bool Γ P Γ Q Γ if M then P else Q Figure 2.3: Type system P A (ssk A , pk B ) = ! in(c, x pk B ); new k; out(c, aenc(sign(k, ssk A ), x pk B )); in(c, x); let z = sdec(x, k) in 0 P B (sk B , spk A ) = ! in(c, y); let y = adec(y, sk B ) in let x k = check(y , spk A ) in out(c, senc(s, x k ))
ProVerif verifies this process when it is given the process of §2.2.

Core language: formal semantics

The formal semantics of this language is defined in Figure 2.4. The definition proceeds in two steps. First, we define the semantics of

M ⇓ M fail ⇓ fail h(D 1 , . . . , D n ) ⇓ σU j if and only if D 1 ⇓ U 1 , . . . , D n ⇓ U n , def(h) consists of the rewrite rules h(U i,1 , . . . , U i,n ) → U i for i ∈ {1, . . . , k}, σU j,1 = U 1 , . . . , σU j,n = U n , and for all i ≤ j, for all σ , σ U i,1 = U 1 , . . . , σ U i,n = U n . E, P ∪ { 0 } → E, P (Red Nil) E, P ∪ { P | Q } → E, P ∪ { P, Q } (Red Par) E, P ∪ { !P } → E, P ∪ { P, !P } (Red Repl) (N pub , N priv ), P ∪ { new a; P } → (N pub , N priv ∪ {a }), P ∪ { P { a / a } }
where a / ∈ N pub ∪ N priv (Red Res) To ease the definition of this relation, we associate to each constructor f of arity n a list of rewrite rules def(f ) that contains the identity rewrite rule

E, P ∪ { out(N, M ); Q, in(N, x); P } → E, P ∪ { Q, P { M / x } } (Red I/O) E, P ∪ { let x = D in P else Q } → E, P ∪ { P { M / x } } if D ⇓ M (Red Eval 1) E, P ∪ { let x = D in P else Q } → E, P ∪ { Q } if D ⇓ fail (Red Eval 2) E, P ∪ { if true then P else Q } → E, P ∪ { P } (Red Cond 1) E, P ∪ { if M then P else Q } → E, P ∪ { Q } if M = true (Red Cond 2)
f (x 1 , . . . , x n ) → f (x 1 , . . . , x n ) .
Furthermore, for each constructor or destructor h of arity n, we add the following rewrite rule as final rewrite rule of def(h): Second, we define the semantics of processes, by reduction of semantic configurations. A semantic configuration is a pair E, P where the environment E is a pair of two finite sets of names (N pub , N priv ) and P is a finite multiset of closed processes. The set N pub contains the public names, the set N priv contains the private names, and the multiset of processes P contains the processes currently running. 1 The configuration ({a 1 , . . . , a n }, {b 1 , . . . , b m }), {P 1 , . . . , P k } corresponds intuitively to the process new b 1 ; . . . new b m ; (P 1 | . . . | P k ). (Recall that types are ignored, so we need not type the names b 1 , . . . , b m .) A configuration (N pub , N priv ), P is valid when N pub and N priv are disjoint and fn(P) ⊆ N pub ∪ N priv . We only consider valid configurations. The reduction relation → on semantic configurations is defined in Figure 2.4. The reduction rules define the semantics of each language construct. The rule (Red Nil) removes processes 0, since they do nothing. The rule (Red Par) expands parallel compositions. The rule (Red Repl) creates an additional copy of a replicated process; since this rule can be applied again on the resulting configuration, it allows creating an unbounded number of copies of the replicated process. The rule (Red Res) creates a fresh name a , substitutes it for a, and adds it to the private names N priv . The fresh name a is required to occur neither in N priv , which contains the initial private free names as well as any fresh name created by a previous application of (Red Res), nor in N pub , which contains the public free names. The rule (Red I/O) allows communication between processes. The message M is sent by the output and received by the input in the variable x, provided the output and input channels are equal. The rules (Red Eval 1) and (Red Eval 2) define the semantics of expression evaluations. They evaluate D. In case of success, (Red Eval 1) runs P with the result M of the evaluation substituted for x. In case of failure, (Red Eval 2) runs Q. The rules (Red Cond 1) and (Red Cond 2) define the semantics of conditionals. When M is true, (Red Cond 1) runs P . When M is different from true, (Red Cond 2) runs Q.

h(u 1 , . . . , u n ) → fail , ( 2
The process P 0 , which represents the protocol to verify, is usually run in parallel with an adversary Q. In this case, the initial configuration is (N pub , N priv ), {P 0 , Q}.

Example 2.4. Let us consider the process P 0 of Example 2.2. This process cannot run alone since it sends messages on channel c without any process to receive them. Hence, we must run P 0 in parallel with an adversary Q. As an example, we consider the following adversary:

Q = in(c, x spk A ); in(c, x pk B ); out(c, x pk B ) ,
which receives the two public keys, and sends the B's public key to A, so that A runs a session with B. This system runs a correct session of the protocol between A and B as follows:

({c}, {s}), {P 0 , Q} There exist other approaches to define the semantics of such a language. We discuss one such approach in Chapter 4.

→ * E 1 , {out(c, pk(ssk A )); out(c, pk(sk B )); (P A (ssk A , pk(sk B )) | P B (sk B , pk(ssk A ))),

Extensions

This section presents the main extensions of the core language implemented in ProVerif, and gives their operational semantics, by extending the semantics given in §2.4.

Equations

In addition to cryptographic primitives defined by rewrite rules, ProVerif also supports primitives defined by equations. We consider an equational theory E that consists of a finite set of equations M = N between terms M , N without names and of the same type. Equality modulo the equational theory E is obtained from these equations by reflexive, symmetric, and transitive closure, closure under application of function symbols, and closure under substitution of terms for variables. We write M = E N an equality modulo E, and M = E N a disequality modulo E. We only consider non-trivial equational theories, that is, for each type T , there exist terms M and N of type T such that M = E N .

As an example, the Diffie-Hellman key agreement [START_REF] Diffie | New Directions in Cryptography[END_REF]) can be modeled using equations. The Diffie-Hellman key agreement relies on the following property of modular exponentiation: (g a ) b = (g b ) a = g ab in a cyclic multiplicative subgroup G of Z * p , where p is a large prime number and g is a generator of G, and on the assumption that it is difficult to compute g ab from g a and g b , without knowing the random numbers a and b (computational Diffie-Hellman assumption), or on the stronger assumption that it is difficult to distinguish g a , g b , g ab from g a , g b , g c without knowing the random numbers a, b, and c (decisional Diffie-Hellman assumption). These properties are exploited to establish a shared key between two participants A and B of a protocol: A chooses randomly a and sends g a to B; symmetrically, B chooses randomly b and sends g b to A. A can then compute (g b ) a , since it has a and receives g b , while B computes (g a ) b . These two values are equal, so they can be used to compute the shared key. The adversary, on the other hand, has g a and g b but not a and b so by the computational Diffie-Hellman assumption, it cannot compute the key. (This exchange resists passive attacks only; to resist active attacks, we need additional ingredients, for instance signatures.) We can model the Diffie-Hellman key agreement by the equation [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF][START_REF] Abadi | Just Fast Keying in the Pi Calculus[END_REF] exp(exp(g, x), y) = exp(exp(g, y), x)

(2.7)
where g : G is a constant and exp(G, Z) : G is modular exponentiation.

Obviously, this is a basic model: it models the main functional equation but misses many algebraic relations that exist in the group G.

We can also model a symmetric encryption scheme in which decryption always succeeds (but may return a meaningless message) by the equations

sdec(senc(x, y), y) = x senc(sdec(x, y), y) = x (2.8)
where senc(bitstring, key) : bitstring and sdec(bitstring, key) : bitstring are constructors. In this model, decryption always succeeds, because sdec(M, N ) is always a term, even when M is not of the form senc(M , N ). The first equation is standard; the second one avoids that the equality test senc(sdec(M, N ), N ) = M reveals that M is a ciphertext under N : in the presence of the second equation, this equality always holds, even when M is not a ciphertext under N . These equations are satisfied by block ciphers, which are bijective.

Equations allow one to model cryptographic primitives that cannot be modeled by destructors with rewrite rules. However, rewrite rules are easier to handle for ProVerif, so they should be preferred when they are sufficient to express the desired properties.

The formal semantics of the language is extended to equations as follows. We extend the evaluation of expressions by considering equality modulo E:

h(D 1 , . . . , D n ) ⇓ σU j if and only if D 1 ⇓ U 1 , . . . , D n ⇓ U n , def(h) consists of the rewrite rules h(U i,1 , . . . , U i,n ) → U i for i ∈ {1, . . . , k}, σU j,1 = E U 1 , . . . , σU j,n = E U n , and for all i ≤ j, for all σ , σ U i,1 = E U 1 , . . . , σ U i,n = E U n .
We also extend the reduction rules by considering equality modulo E:

E, P ∪ { out(N, M ); Q, in(N , x); P } → E, P ∪ { Q, P { M / x } } if N = E N (Red I/O ) E, P ∪ { if M then P else Q } → E, P ∪ { P } if M = E true (Red Cond 1 ) E, P ∪ { if M then P else Q } → E, P ∪ { Q } if M = E true (Red Cond 2 )
To handle equations, ProVerif translates them into a set of rewrite rules associated to constructors. For instance, the equations (2.8) are translated into the rewrite rules

senc(x, y) → senc(x, y) sdec(x, y) → sdec(x, y) senc(sdec(x, y), y) → x sdec(senc(x, y), y) → x (2.9) while the equation (2.7) is translated into exp(x, y) → exp(x, y) exp(exp(g, x), y) → exp(exp(g, y), x) (2.10)
Intuitively, these rewrite rules allow one, by applying them exactly once for each constructor, to obtain the various forms of the terms modulo the considered equational theory. 2 These forms are named variants, and since the number of rewrite rules must be finite, ProVerif only supports equational theories that have the finite variant property (Comon-Lundh and [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF]. Constructors are then evaluated similarly to destructors. The only difference is that the rewrite rules that come from equations are not ordered: all applicable rewrite rules are applied. With Abadi and Fournet, we have formally defined when a set of rewrite rules models an equational theory, and designed algorithms that translate equations into rewrite rules that model them (Blanchet et al., 2008, §5).

Then, each trace in the calculus with equational theory corresponds to a trace in the calculus with rewrite rules, and conversely (Blanchet et al., 2008, Lemma 1). 3 Hence, we reduce to the calculus with rewrite rules. The main advantage of this approach is that resolution can still use ordinary syntactic unification (instead of having to use unification modulo the equational theory), and therefore remains efficient: it avoids the explosion of the number of clauses that occurs when many unifiers modulo This approach still has limitations: associative operations, such as exclusive or, are not supported, because they would require an infinite number of rewrite rules. It may be possible to handle these operations using unification modulo the equational theory instead of syntactic unification, at the cost of a larger complexity. In the case of a bounded number of sessions, exclusive or is handled in [START_REF] Comon-Lundh | Intruder deductions, constraint solving and insecurity decision in presence of exclusive or[END_REF][START_REF] Chevalier | An NP decision procedure for protocol insecurity with XOR[END_REF] and a more complete theory of modular exponentiation is handled in [START_REF] Chevalier | Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents[END_REF]. A unification algorithm for modular exponentiation is presented in [START_REF] Meadows | A Unification Algorithm for the Group Diffie-Hellman Protocol[END_REF]. For an unbounded number of sessions, extensions of the Horn clause approach have been proposed. [START_REF] Küsters | Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach[END_REF] support exclusive or provided one of its two arguments is a constant in the clauses that model the protocol. [START_REF] Küsters | Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation[END_REF] support Diffie-Hellman key agreements with more detailed algebraic relations (including equations of the multiplicative group modulo p), provided the exponents are constants in the clauses that model the protocol. By extending that line of research, Pankova and Laud, 2012 support bilinear pairings, provided the exponents are constants in the clauses that model the protocol. These approaches proceed by transforming the initial clauses into richer clauses on which the standard resolution algorithm is applied. The tools Maude-NPA [START_REF] Meadows | The NRL Protocol Analyzer: An Overview[END_REF][START_REF] Escobar | A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties[END_REF] and Tamarin [START_REF] Schmidt | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties[END_REF] support equational theories that ProVerif does not support, at the cost of a more costly verification or by requiring user intervention. Maude-NPA supports equations defined by convergent rewrite rules plus associativity and commutativity [START_REF] Escobar | Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer[END_REF] (which includes Diffie-Hellman exponentiation and exclusive or), as well as homomorphic encryption [START_REF] Escobar | Protocol analysis in Maude-NPA using unification modulo homomorphic encryption[END_REF]. Tamarin supports subterm convergent equations, Diffie-Hellman exponentiation (including equations of the multiplicative group modulo p), bilinear pairings, and associative and commutative operators [START_REF] Schmidt | Automated Verification of Group Key Agreement Protocols[END_REF].

Enriched terms

ProVerif allows all occurrences of terms M in processes (input and output channels, output messages, and conditions) to be replaced with expressions D, which may contain destructors, hence the syntax of processes becomes:

P, Q ::= processes . . . out(D, D ); P output in(D, x : T ); P input if D then P else Q conditional
Each such expression D is evaluated; when the evaluation fails, the process does nothing; when it succeeds with result M , it executes the process with M instead of D. Hence the formal semantics can be defined as follows:

E, P ∪ { out(D , D); Q, in(D , x); P } → E, P ∪ { Q, P { M / x } } if D ⇓ M , D ⇓ M , D ⇓ M , and M = E M (Red I/O ) E, P ∪ { if D then P else Q } → E, P ∪ { P } if D ⇓ M and M = E true (Red Cond 1 ) E, P ∪ { if D then P else Q } → E, P ∪ { Q } if D ⇓ M and M = E true (Red Cond 2 )
Alternatively, processes with such expressions can easily be encoded into the core calculus by introducing additional expression evaluations. For instance, in(D, x : T ); P can be encoded as

let y = D in in(y, x : T ); P .
Furthermore, ProVerif allows expressions to contain some constructs from processes: restriction, expression evaluation, and conditional, so that the syntax of expressions is extended as follows:

D ::= expressions . . . new a : T ; D restriction let x : T = D in D else D expression evaluation if D then D else D conditional
Processes that contain such expressions are handled by transforming them into processes without such expressions, by moving restrictions, expression evaluations, and conditionals from expressions to processes.

Pattern-matching

We enrich the input and expression evaluation constructs with patternmatching as follows:

P, Q ::= processes . . . in(D, pat); P input let pat = D in P else Q expression evaluation
where patterns pat are defined by the following grammar:

pat ::= patterns x : T variable =D equality test f (pat 1 , . . . , pat n ) data constructor
The pattern x : T matches any term and stores it in variable x. The type T can be omitted when it can be inferred. The variables x inside a pattern must be pairwise distinct.

The pattern =D matches only terms that are equal to the result of the evaluation of D. When the evaluation of D fails, the patternmatching fails.

The pattern f (pat 1 , . . . , pat n ) matches terms of the form f (M 1 , . . . , M n ), when pat i matches M i for all i ≤ n. This pattern can be used only when f is data constructor. A data constructor is a constructor f of arity n that comes with associated destructors g i for i ∈ {1, . . . , n} defined by g i (f (x 1 , . . . , x n )) → x i . Data constructors are typically used for representing data structures. Tuples are examples of data constructors. Pattern-matching with data constructors allows one to extract the contents of the data structures. To be able to pattern-match on data constructors without considering the equational theory, we require that the equational theory satisfies the following condition: for all data constructors f ,

f (M 1 , . . . , M n ) = E M if and only if there exist M 1 , . . . , M n such that M = f (M 1 , . . . , M n ) and M i = E M i for all i ∈ {1, . . . , n}.
When the pattern-matching fails, the expression evaluation let pat = D in P else Q runs Q. For an input in(D, pat); P , the communication is executed even when the pattern-matching fails, but the receiver process does nothing after the input. In other words, in(D, pat); P is an abbreviation for in(D, x : T ); let pat = x in P else 0 where T is the type of the pattern pat.

Example 2.5. We consider again the protocol of §2.2. We may add the public key of B inside the first message, which becomes

Message 1. A → B : aenc(sign((pk B , k), ssk A ), pk B ) B (Bob) A (Alice) senc(s, k) aenc(sign((pk B , k), ssk A ), pk B ) k fresh Figure 2.5: Modified example of protocol
The modified protocol is illustrated in Figure 2.5. The processes P A and P B are then modified accordingly:

P A (ssk A , pk B ) = ! in(c, x pk B : pkey); new k : key; out(c, aenc(sign((x pk B , k), ssk A ), x pk B )); in(c, x : bitstring); let z = sdec(x, k) in 0 P B (sk B , spk A ) = ! in(c, y : bitstring); let y = adec(y, sk B ) in let (=pk(sk B ), x k : key) = check(y , spk A ) in out(c, senc(s, x k ))
The process P A signs the pair (x pk B , k). When P B verifies the signature, it uses pattern-matching to verify that the signed message is a pair whose first component is its own public key pk B = pk(sk B ), and to store the second component in the variable x k . Because of the overloading of tuples, the type of x k , namely key, must be explicitly mentioned, so that ProVerif knows that the pair (_, _) stands for tuple pkey,key (_, _).

Pattern-matching can be encoded into the core language using equality tests and the destructors associated to data constructors, as shown by the following example.

Example 2.6. The process P B of Example 2.5 can be encoded into the calculus without pattern-matching as follows:

P B (sk B , spk A ) = ! in(c, y : bitstring); let y = adec(y, sk B ) in let z = check(y , spk A ) in if 1th pkey,key (z) = pk(sk B ) then let x k = 2th pkey,key (z) in out(c, senc(s, x k ))
This process uses the extension of §2.5.2 to allow destructors in if 1th pkey,key (z) = pk(sk B ) then. It can be encoded in the core calculus as follows:

P B (sk B , spk A ) = ! in(c, y : bitstring); let y = adec(y, sk B ) in let z = check(y , spk A ) in let z = (1th pkey,key (z) = pk(sk B )) in if z then let x k = 2th pkey,key (z) in out(c, senc(s, x k ))
Obviously, the formal semantics of calculus can also be extended with pattern-matching as well as the following extensions described in this section. We omit these formal details for simplicity.

Phases

Some situations can be modeled with several phases or stages (Blanchet et al., 2008, §8). For instance, the protocol may run in a first phase, and a long-term key may be compromised in a later phase. One may hope that the secret messages exchanged in the first phase remain secret even after the compromise of the key. This property is named forward secrecy. Voting protocols may also include several phases, for instance a registration phase, a voting phase, and a tallying phase [START_REF] Kremer | Analysis of an Electronic Voting Protocol in the Applied Pi Calculus[END_REF]. ProVerif includes a phase construct to model such situations: P, Q ::= processes . . . phase n; P phase

The phase construct acts as a global synchronization. The processes initially run in phase 0. Then at some point, phase 1 starts. All processes that did not reach a phase n construct with n ≥ 1 are discarded, and processes that start with phase 1 run. Phases continue being incremented in the same way.

Example 2.7. The following process

P 0 = new ssk A : skey; (P | phase 1; out(c, ssk A )) ,
where P does not contain phases, models a protocol P that runs in phase 0, using the secret key ssk A . This key is then compromised in phase 1, by sending it on the public channel c.

Tables

Tables are often useful in the modeling of security protocols. For instance, an SSH client stores a list of names and keys of the servers it has contacted so far; this list can be modeled as a table. ProVerif supports specific constructs for modeling tables:

P, Q ::= processes . . . insert tbl(D 1 , . . . , D n ); P insertion in a table get tbl(pat 1 , . . . , pat n ) suchthat D in P else Q lookup in a table
The process insert tbl(D However, with such a protocol, the participants need to relate the keys (e.g. pk B ) to the identities (e.g. B). We establish this relation using certificates, in the same way as in the original Denning-Sacco key distribution protocol [START_REF] Denning | Timestamps in Key Distribution Protocols[END_REF]: we use sign((e, B, pk B ), ssk S ) as a certificate that pk B is the public encryption key of B and sign((s, A, spk A ), ssk S ) as a certificate that spk A is the public signature verification key of A, where ssk S is the signature key of a trusted certificate authority S (server). The protocol becomes: A ProVerif model for this protocol is shown in Figure 2.7. This model considers two participants Alice and Bob, which can play both roles A and B of the protocol. The process P 0 first generates the encryption and signature keys for Alice and Bob, and inserts them in a table keys, which contains triples (identity, encryption key, signature verification key) for each participant. It also generates the signature keys for the server S, and publishes all public keys by sending them on the public channel c. Finally, it runs the processes that model Alice, Bob, and

{s} k c A , c B , aenc(sign((B, k), ssk A ), pk B ) k fresh S (server) A, B c A , c B A (Alice) B (Bob)
P 0 = new ssk A : skey; let spk A = pk(ssk A ) in new sk A : skey; let pk A = pk(sk A ) in insert keys(Alice, pk A , spk A ); new ssk B : skey; let spk B = pk(ssk B ) in new sk B : skey; let pk B = pk(sk B ) in insert keys(Bob, pk B , spk B ); new ssk S : skey; let spk S = pk(ssk S ) in out(c, (pk A , spk A , pk B , spk B , spk S )); (P A (spk S , Alice, ssk A , spk A ) | P A (spk S , Bob, ssk B , spk B ) | P B (spk S , Bob, sk B , pk B ) | P B (spk S , Alice, sk A , pk A ) | P S (ssk S ) | P K ) P K = ! in(c, (h : host, pk : pkey, spk : pkey)); if h = Alice && h = Bob then insert keys(h, pk, spk) P S (ssk S ) = ! in(c, (h 1 : host, h 2 : host));
get keys(=h 1 , xx, spk 1 ) in get keys(=h 2 , pk 2 , yy) in out(c, (sign((s, h 1 , spk 1 ), ssk S ), sign((e, h 2 , pk 2 ), ssk S ))) S, as well as the process P K . This process allows the adversary to register its own keys for participants other than Alice and Bob by inserting these keys in the table keys. Therefore, the adversary can implement any number of dishonest participants to the protocol. The process P S for the server receives two participant names h 1 and h 2 , obtains their keys from the table keys, and outputs a certificate for the signature verification key of h 1 and one for the encryption key of h 2 . The process P A (spk S , A, ssk A , spk A ) models a participant A with secret signature key ssk A and public signature verification key spk A , running role A of the protocol. We suppose that the adversary sends the first message of the protocol himself. (This is possible since the participant names are public.) So this message does not appear explicitly in P A . The process P A receives message 2 containing the certificates, checks them, outputs message 3, and receives message 4. The process P B (spk S , B, sk B , pk B ) models a participant B with secret decryption key sk B and public encryption key pk B , running role B of the protocol. It receives message 3, checks the certificates, and when its interlocutor A is honest (that is, this interlocutor is Alice or Bob), it sends a secret s encrypted under the shared key x k as message 4. This message is only sent when the interlocutor is honest, because it is perfectly normal that the adversary can decrypt the last message when the interlocutor of B is dishonest, so the secrecy of s would not be preserved in this case.

P A (spk S , A, ssk A , spk A ) = ! in(c, (c A : bitstring, c B : bitstring)); if (s, A, spk A ) = check(c A , spk S ) then let (=e, B, pk B ) = check(c B , spk S ) in new k : key; out(c, (c A , c B , aenc(sign((B, k), ssk A ), pk B ))); in(c, x : bitstring); let z = sdec(x, k) in 0 P B (spk S , B, sk B , pk B ) = ! in(c, (c A : bitstring, c B : bitstring, y : bitstring)); if (e, B, pk B ) = check(c B , spk S ) then let (=s, A, spk A ) = check(c A , spk S ) in let y = adec(y, sk B ) in let (=B, x k : key) = check(y , spk A ) in if A = Alice || A = Bob then out(c, senc(s, x k ))
Tables can be encoded in the core calculus using private channels. ProVerif provides a specific construct as it is frequently used and it is probably easier to understand for users. This chapter presents the method used by ProVerif for verifying protocols. This method based on Horn clauses. The idea of using Horn clauses for verifying protocols was introduced by Weidenbach, 1999. We extended his work by defining a systematic translation from a formal model of protocols to clauses (while he built the clauses manually) and by proving properties other than secrecy. We first formalize the notion of an adversary, then deal with the various security properties verified by ProVerif, starting with the simplest one, secrecy, then considering more complex ones, correspondences and equivalences. The main reference for the proof of secrecy and correspondences in ProVerif is [START_REF] Blanchet | Automatic Verification of Correspondences for Security Protocols[END_REF] and for equivalences (Blanchet et al., 2008). For simplicity, this chapter only deals with the core calculus of §2.1. The results can be adapted to the extended calculus, and ProVerif supports that calculus.

Adversary

We assume that the protocol is executed in the presence of an adversary that intercept all messages, compute, and send all messages it has, following the Dolev-Yao model [START_REF] Dolev | On the Security of Public Key Protocols[END_REF]. In our calculus, an adversary can be represented by any process that has the set of public free names N pub in its initial knowledge. (Although the initial knowledge of the adversary contains only names in N pub , one can give any terms to the adversary by sending them on a channel in N pub .) Definition 3.1. Let N pub be a finite set of names. The closed process Q is an N pub -adversary if and only if fn(Q) ⊆ N pub and all function symbols in Q are public. (The process Q is not necessarily well-typed.)

Secrecy

This section deals with the verification of secrecy, the most basic security property. We first define secrecy formally, then explain how to verify it by translating the protocol into Horn clauses and using resolution on these clauses.

Definition

Intuitively, a process P preserves the secrecy of M when M cannot be output on a public channel, in a run of P with any adversary. Formally, we define that a trace outputs M as follows: Definition 3.2. We say that a trace Tr = (N pub , N priv ), P 0 → * E , P outputs M publicly if and only if Tr contains a reduction

E, P ∪ { out(N, M ); Q, in(N, x); P } → E, P ∪ { Q, P { M / x } } for some E, P, N , x, P , Q, with N ∈ N pub .
We can finally define secrecy: Definition 3.3. The closed process P 0 preserves the secrecy of the closed term M from N pub if and only if for some N priv disjoint from N pub such that fn(M ) ∪ fn(P 0 ) ⊆ N pub ∪ N priv , for any N pub -adversary Q, for any trace Tr = (N pub , N priv ), {P 0 , Q} → * E , P , the trace Tr does not output M publicly.

The choice of N priv does not matter, provided the conditions of Definition 3.3 are satisfied.

From the pi calculus to Horn clauses

Given a closed process P 0 in the language of Chapter 2 and a set of names N pub representing the initial knowledge of the adversary, ProVerif builds a set of Horn clauses, representing the protocol P 0 in parallel with any N pub -adversary. This translation was originally given in (Abadi and Blanchet, 2005a); we extend it to the richer destructors of [START_REF] Cheval | Proving More Observational Equivalences with ProVerif[END_REF]. We suppose that the bound names of P 0 are pairwise distinct and distinct from the free names and the names in N pub .

In these clauses, messages are represented by patterns p, defined by the following grammar:

p ::= patterns x, y, z, i variable a[p 1 , . . . , p n ] name f (p 1 , . . . , p n ) constructor application
Patterns are terms; we use the word patterns to distinguish them from terms of the process calculus. Patterns differ from those terms by the representation of names. We assign a pattern a[p 1 , . . . , p n ] to each name a of P 0 . We treat a as a function symbol, and write a[p 1 , . . . , p n ] rather than a(p 1 , . . . , p n ) only to distinguish functions that come from names from other functions. If a is a free name, then its pattern is a[ ]. To define the patterns of bound names, we first assign a distinct, fresh session identifier variable i to each replication of P 0 . (We will use a distinct value for i for each copy of the replicated process.) If a is bound by a restriction new a in P 0 , then its pattern takes as arguments the terms received as inputs and the session identifiers of replications above the restriction. For example, in the process !in(c, x); new a; P , each name created by new a is represented by a [i, x] where i is the session identifier for the replication and x is the message received as input in in(c, x).

Session identifiers enable us to distinguish names created in different copies of processes. Hence, each name created in the process calculus is represented by a different pattern in the Horn clauses. The evaluation of expressions may fail. We reflect that in the Horn clauses by introducing may-fail patterns, which can be the constant fail or a may-fail variable in addition to an ordinary pattern: As in messages and may-fail messages, a may-fail variable u can be instantiated by a pattern or fail, whereas a variable x cannot be instantiated by fail.

The clauses use facts defined by the following grammar:

F ::= facts attacker(mp) adversary knowledge message(p, p ) message on a channel ∀ v, (mp 1 , . . . , mp n ) = (mp 1 , . . . , mp n ) disequality
The fact attacker(mp) means that the adversary may have mp. The fact message(p, p ) means that the message p may appear on channel p. The fact ∀ v, (mp 1 , . . . , mp n ) = (mp 1 , . . . , mp n ) means that (mp 1 , . . . , mp n ) = (mp 1 , . . . , mp n ) for all values of variables in v, where v may contain variables as well as may-fail variables. We write v for a variable or a may-fail variable. We omit ∀ v when v contains no variable. We omit the parentheses around mp 1 , . . . , mp n and mp 1 , . . . , mp n when n = 1. We write mp as an abbreviation for (mp 1 , . . . , mp n ).

The clauses are of the form F 1 ∧ . . . ∧ F n ⇒ F , where F 1 , . . . , F n , F are facts. They comprise clauses for the adversary and clauses for the protocol, defined below. These clauses form the set R P 0 ,N pub ,N priv .

Clauses for the adversary

The abilities of the adversary are represented by the following clauses:

For each a ∈ N pub , attacker(a[ ]) (Init) attacker(b 0 [x]
) where b 0 occurs neither in P 0 nor in N pub ∪ N priv (Rn)

attacker(fail) (Rfail)
For each public function h, such that def(h) consists of the rewrite rules h(U i,1 , . . . , U i,n ) → U i for i ∈ {1, . . . , k}, the variables in these rewrite rules are renamed so that distinct rewrite rules use different variables, and

v i = fv(U i ) ∪ n l=1 fv(U i,l ), for each i ∈ {1, . . . , k}, attacker(U i,1 ) ∧ . . . ∧ attacker(U i,n ) ∧ j<i ∀ v j , (U i,1 , . . . , U i,n ) = (U j,1 , . . . , U j,n ) ⇒ attacker(U i ) (Rh) message(x,
∀ v j , (U i,1 , . . . , U i,n ) = (U j,1 , . . . , U j,n
). The rewrite rules in def(h) do not contain names, and terms without names are also patterns, so these clauses have the required format. When h is a constructor f of arity n, these clauses simplify into

attacker(x 1 ) ∧ . . . ∧ attacker(x n ) ⇒ attacker(f (x 1 , . . . , x n )) (Rf)
and when h is a destructor g with a single rewrite rule g(U 1 , . . . , U n ) → U , they simplify into

attacker(U 1 ) ∧ . . . ∧ attacker(U n ) ⇒ attacker(U ) (Rg)
(The clauses that conclude fail can be removed since they are subsumed by (Rfail).) Clause (Rl) means that the adversary can listen on all channels it has, and (Rs) that it can send all messages it has on all channels it has. When a message is sent on a channel, both the message and the channel cannot be fail, so x and y are ordinary variables.

Example 3.1. We suppose that public-key encryption is defined by (2.1).

The constructors senc, pk, aenc, and sign yield the following clauses:

attacker(m) ∧ attacker(k) ⇒ attacker(senc(m, k)) (senc) attacker(sk) ⇒ attacker(pk(sk)) (pk) attacker(m) ∧ attacker(pk) ⇒ attacker(aenc(m, pk)) (aenc) attacker(m) ∧ attacker(sk) ⇒ attacker(sign(m, sk)) (sign)
The corresponding destructors sdec, adec, check, and getmess yield the following clauses:

attacker(senc(m, k)) ∧ attacker(k) ⇒ attacker(m) (sdec) attacker(aenc(m, pk(sk))) ∧ attacker(sk) ⇒ attacker(m) (adec) attacker(sign(m, sk)) ∧ attacker(pk(sk)) ⇒ attacker(m) (check) attacker(sign(m, sk)) ⇒ attacker(m) (getmess)
For instance, the clause for sdec models that, when the adversary has the ciphertext senc(m, k) and the key k, then it can obtain the cleartext m by decryption. The clause for check is less general than the one for getmess since, in the former clause, the attacker additionally needs to know the key pk(sk); more formally, the clause for check is subsumed by the one for getmess, so it is discarded during the resolution algorithm (see "Elimination of subsumed clauses" in §3.2.3).

Clauses for the protocol

To translate the protocol into clauses, we first need to define evaluation on patterns expressions, defined by the following grammar:

Dp ::= pattern
mp ⇓ (mp, ∅, ) h(Dp 1 , . . . , Dp n ) ⇓ (σ u U i , σ u σ , σ u φ ∧ σ u φ) if (Dp 1 , . . . , Dp n ) ⇓ ((mp 1 , . . . , mp n ), σ , φ ),
σ u is a most general unifier of (mp 1 , U i,1 ), . . . , (mp n , U i,n ), and

φ = j<i ∀ v j , (mp 1 , . . . , mp n ) = (U j,1 , . . . , U j,n )
for some i ∈ {1, . . . , k}, where def(h) consists of the rewrite rules h(U i,1 , . . . , U i,n ) → U i for i ∈ {1, . . . , k}, the variables in these rewrite rules are renamed so that distinct rewrite rules use different variables, and

v i = fv(U i ) ∪ n l=1 fv(U i,l ) for all i ∈ {1, . . . , k}. (Dp 1 , . . . , Dp n ) ⇓ ((σ n mp 1 , . . . , σ n mp n-1 , mp n ), σ n σ, σ n φ ∧ φ n ) if (Dp 1 , . . . , Dp n-1 ) ⇓ ((mp 1 , . . . , mp n-1 ), σ, φ) and σDp n ⇓ (mp n , σ n , φ n )
The substitution ∅ is the identity. The formula denotes the empty conjunction, that is, a formula that always holds. The most general unifier of may-fail patterns is computed similarly to usual most general unifiers, even though specific cases hold due to may-fail variables and ordinary variables: there is no unifier of p and fail, for any pattern p (including variables x, because these variables can be instantiated only by messages); the most general unifier of u and mp is { mp / u }; the most general unifier of fail and fail is the identity; finally, the most general unifier of p and p is computed as usual.

The first rule of the definition ⇓ treats cases without destructors. The second one treats function application: it applies each rewrite rule of h. To apply the i-th rewrite rule, it evaluates the arguments of h to mp 1 , . . . , mp n , checks that the rewrite rule actually applies by unifying mp 1 , . . . , mp n with the arguments of h in the rewrite rule, and checks that all rewrite rules before the i-th do not apply thanks to the formula φ. Finally, the third rule treats the evaluation of a tuple.

The translation [[P ]

]ρsH of a process P is a set of clauses, where ρ is an environment that associates a pattern with each name and variable, s is a sequence of patterns, and H is a sequence of facts. We extend ρ as a substitution by ρ(h(M 1 , . . . , M n )) = h(ρ(M 1 ), . . . , ρ(M n )) and ρ(fail) = fail. The empty sequence is written ∅; the concatenation of a pattern p to the sequence s is written s, p; the concatenation of a fact F to the sequence H is written H ∧ F . Intuitively, H represents the hypothesis of the clauses, ρ represents the names and variables that are already associated with a pattern, and s represents the current values of session identifiers and inputs. The translation [[P ]]ρsH is defined as follows:

[[0]]ρsH = ∅ [[P | Q]]ρsH = [[P ]]ρsH ∪ [[Q]]ρsH [[!P ]]ρsH = [[P ]]ρ(s, i)H where i is a fresh variable [[new a; P ]]ρsH = [[P ]](ρ[a → a[s]])sH [[in(M, x); P ]]ρsH = [[P ]](ρ[x → x ])(s, x )(H ∧ message(ρ(M ), x ))
where x is a fresh variable

[[out(M, N ); P ]]ρsH = [[P ]]ρsH ∪ {H ⇒ message(ρ(M ), ρ(N ))} [[let x = D in P else Q]]ρsH = {[[P ]]((σρ)[x → p])(σs)(σH ∧ φ) | ρ(D) ⇓ (p, σ, φ)} ∪ {[[Q]](σρ)(σs)(σH ∧ φ) | ρ(D) ⇓ (fail, σ, φ)} [[if M then P else Q]]ρsH =              [[P ]](σρ)(σs)(σH) ∪ [[Q]]ρs(H ∧ ρ(M ) = true)
where σ is the most general unifier of ρ(M ) and true, when ρ(M ) and true unify [ [Q]]ρsH when ρ(M ) and true do not unify

The translation of a process is a set of Horn clauses that express that it may send certain messages.

• The nil process does nothing, so its translation is empty.

• The clauses for the parallel composition of processes P and Q are the union of clauses for P and Q.

• For the replication, we create a fresh session identifier i and add it to the sequence s. The replication is otherwise ignored, because all Horn clauses are applicable arbitrarily many times.

• For the restriction, we replace the restricted name a in question with the pattern a [s], where the sequence s contains the previous inputs and session identifiers.

• The sequence H is extended in the translation of an input, with the input in question. The sequence s is also extended with the received message.

• The translation of an output adds a clause, meaning that the output is triggered when all conditions in H are true.

• The translation of an expression evaluation is the union of the clauses for the cases where the evaluation succeeds and where the evaluation fails. In case of success, the variable x is bound to the result p in ρ. In both cases, ρ, s, and H are instantiated by σ and the formula φ is added to the hypothesis H, where ρ(D) ⇓ (mp, σ, φ).

• The translation of a conditional is also the union of the clauses for the cases where the condition is true and where it is not true. (In the second case of the definition, when ρ(M ) and true do not unify, the condition is never true, so the else branch is always executed.)

The clauses corresponding to the process P 0 are computed by

[[P 0 ]]ρ 0 ∅∅ where ρ 0 = {a → a[ ] | a ∈ fn(P 0 )}.

Results and example

We define the clauses corresponding to the process P 0 as:

R P 0 ,N pub ,N priv = [[P 0 ]]ρ 0 ∅∅ ∪ {attacker(a[ ]) | a ∈ N pub } ∪
{(Rn), (Rfail), (Rh), (Rl), (Rs)}

The following theorem allows one to prove secrecy using Horn clauses:

Theorem 3.1 (Soundness of the clauses). Let P 0 be a closed process and N pub be a set of names. Let M be a closed term and p be the pattern obtained from the term M by replacing all names a with a[ ]. Let N priv be a set of names disjoint from N pub and such that fn(P 0 ) ∪ fn(M ) ⊆ N pub ∪ N priv . If attacker(p) is not derivable from R P 0 ,N pub ,N priv , then P 0 preserves the secrecy of M from N pub .

The proof of this result relies on a type system to express the soundness of the clauses on P 0 , and on the subject reduction of this type system to show that soundness of the clauses is preserved during all executions of the process. This technique was introduced in (Abadi and Blanchet, 2005a) where a similar result is proved. (Abadi and Blanchet, 2005a) also shows an equivalence between an instance of a generic type system for proving secrecy properties of protocols and the Horn clause verification method. This instance is the most precise instance of this generic type system: if a secrecy property can be proved by any instance of this type system, then it can be proved by the Horn clause approach. To use Theorem 3.1, one needs to determine whether a fact is derivable from the clauses. This is done using a resolution algorithm described in §3. The fact attacker(s[ ]) is derivable from the clauses R P 0 ,N pub ,N priv . Hence the secrecy of s cannot be proved by Theorem 3.1 for this protocol. The derivation obtained by ProVerif is shown in Figure 3.1. This derivation corresponds to the following well-known attack [START_REF] Abadi | Prudent Engineering Practice for Cryptographic Protocols[END_REF]

F 2 = attacker(aenc(sign(k[i, pk(b 0 [x])], ssk A [ ]), pk(b 0 [x]))) F 2 F 1 by (Rg) for adec F 3 = attacker(sign(k[i, pk(b 0 [x])], ssk A [ ]) F 3 by (3.2) attacker(pk(sk B [ ]))
by (Rf) for aenc attacker (aenc(sign(k[i, pk(b

0 [x])], ssk A [ ]), pk(sk B [ ]))) by (3.4) F 4 = attacker(senc(s[ ], k[i, pk(b 0 [x])])) F 4 F 3 by (Rg) for getmess attacker(k[i, pk(b 0 [x])])
by (Rg) for sdec attacker(s[ ]) We can model the fixed version of the protocol, mentioned in Example 2.5, in a similar way, and compute the corresponding clauses. ProVerif then shows that attacker(s[ ]) is not derivable from these clauses. By Theorem 3.1, we obtain that the fixed protocol preserves the secrecy of s from {c}.

In the example above, we explained informally that the obtained derivation corresponds to an attack. [START_REF] Allamigeon | Reconstruction of Attacks against Cryptographic Protocols[END_REF] extended ProVerif so that it automatically reconstructs an attack from

aenc(sign(k, ssk A ), pk C ) aenc(sign(k, ssk A ), pk B ) senc(s, k) k fresh A (Alice) impersonating A (Alice) C (adversary) B (Bob) Figure 3.2: Attack a derivation.
The reconstructed attack is a trace of the process P 0 that outputs s publicly. The strategy for reconstructing this trace consists in executing the semantics of process P 0 , guided by the derivation: a reduction of the process is executed only if a clause in the derivation corresponds to this reduction. We showed the soundness and termination of this algorithm. We also gave a formal definition of this correspondence between clauses and reductions, by giving an explicit construction of a derivation from a trace of P 0 . We have then shown a partial completeness result for attack reconstruction: if all outputs in P 0 are of the form out(M, N ); P where M is a name in N pub not bound in P 0 or P = 0, and the derivation corresponds to a trace, then our algorithm succeeds in reconstructing a trace corresponding to the derivation. Moreover, with the same assumptions, our algorithm reconstructs a trace without backtracking. It is therefore very efficient in this case, and in practice it is generally very fast. We successfully tested this attack reconstruction algorithm on many protocols of the literature. To mention an extreme example, we could reconstruct an attack with 200 parallel sessions against the protocol f 200 g 200 [START_REF] Millen | A Necessarily Parallel Attack[END_REF]. (The protocol f n g n has an attack with n parallel sessions.)

In the example above, the obtained derivation corresponds to an attack. This is unfortunately not always the case, since Horn clauses introduce approximations. These approximations are useful in order to handle an infinite state space, but because of these approximations, ProVerif may sometimes find a derivation while secrecy is preserved. In this case, attack reconstruction fails, obviously. The case in which ProVerif finds a derivation but attack reconstruction fails corresponds to an "I do not know" answer. In all other cases, ProVerif gives a correct answer: either it finds no derivation and the desired property is proved, or attack reconstruction succeeds, and an attack against the property in question is found.

The main approximation done by ProVerif is that clauses can be applied any number of times, so the repetitions (or not) of actions are ignored. As a consequence, protocols with temporary secrets cannot be proved secure by ProVerif: when some value first needs to be kept secret and is revealed later in the protocol, the Horn clause model considers that this value can be reused in the beginning of the protocol, thus breaking the protocol. For instance, the process d,c)), in which actions are repeated, and which does not preserve the secrecy of s from {d}.

P 0 = new c; (out(c, s) | in(c,
An additional approximation occurs with outputs on private channels: for the output out(M, N ); P , the Horn clause representation considers that the process P can always be executed, as if the process was out(M, N ) | P , while in fact P can be executed only after sending N on channel M .

Resolution algorithm

The internal protocol representation is a set of Horn clauses, and our goal is to determine whether a given fact can be derived from these clauses or not. This is exactly the problem solved by Prolog systems. However, we cannot use such systems here, because they would not terminate. They use SLD-resolution [START_REF] Kowalski | Predicate Logic as Programming Language[END_REF], so for instance, with the goal attacker(s[ ]), the clause attacker(aenc(m, pk(sk))) ∧ attacker(sk) ⇒ attacker(m) leads to considering more and more complex facts attacker(aenc(. . . aenc(s[ ], pk(sk 1 )) . . . , pk(sk n ))

with an unbounded number of encryptions. We could of course limit arbitrarily the depth of terms to solve the problem, but we can do much better than that, by using another resolution strategy. We use resolution with free selection [START_REF] Bachmair | Resolution Theorem Proving[END_REF]. We could also use ordered resolution with selection, used by [START_REF] Weidenbach | Towards an Automatic Analysis of Security Protocols in First-Order Logic[END_REF] and implemented in SPASS (http://www.spass-prover.org/), which is similar but adds ordering constraints. An advantage of implementing our own resolution prover is that we can use domain-specific optimizations, described below, and extensions such as the one needed for proving correspondences ( §3.3).

Since a term is secret when a fact is not derivable from the clauses, soundness in terms of security (if the verifier claims that there is no attack, then there is no attack) corresponds to the completeness of the resolution algorithm in terms of logic programming (if the algorithm claims that a fact is not derivable, then it is not). The resolution algorithm that we use must therefore be complete.

Basic algorithm

A resolution step combines two clauses R = H ⇒ C and R = F ∧ H ⇒ C (where F is any hypothesis of R ) to infer R• F R = σH ∧σH ⇒ σC
where C and F are unifiable and σ is the most general unifier of C and F . Hence, the clause R • F R is the result of resolving R with R upon F ; it combines R and R , so that R is used in order to prove the hypothesis F of R . The resolution is guided by a selection function sel: sel(R) returns a hypothesis of R or the empty (meaning that the conclusion of R is selected), and the resolution step above is performed only when sel(R) = ∅ and sel(R ) = {F }, that is, the facts upon which we resolve, the conclusion of R and the hypothesis F of R , are selected. The saturation algorithm saturate(R 0 ) applies these resolution steps to R 0 until a fixpoint is reached, that is, no new clause is created. When the fixpoint is reached, saturate(R 0 ) returns the subset of the clauses R in the fixpoint such that sel(R) = ∅.

Resolution with free selection is sound and complete for any selection function, but the choice of this function considerably influences its speed (and its termination). The fact attacker(v) where v is a variable or a may-fail variable unifies with any fact attacker(p), so if attacker(v) is selected, the algorithm will almost never terminate. Therefore, we avoid selecting attacker(v). Furthermore, disequalities are treated by special simplification steps, shown below, so we never select them. A natural selection function is then:

sel 0 (H ⇒ C) =             

∅

if all elements of H are disequalities or of the form attacker(v), v variable or may-fail variable {F } where F is not a disequality,

F = attacker(v) and F ∈ H, otherwise

Optimizations

The resolution algorithm uses several optimizations, in order to speed up resolution. We mention the main optimizations in this section. Others are presented in [START_REF] Blanchet | Automatic Verification of Correspondences for Security Protocols[END_REF]. These optimizations are applied on the initial clauses and after each resolution step. The first three optimizations are standard, while the last two are domain-specific.

• Elimination of subsumed clauses. The clause • Elimination of duplicate hypotheses. Only one copy of duplicate hypotheses in a clause is kept.

H 1 ⇒ C 1 subsumes H 2 ⇒ C 2 if
• Elimination of tautologies. Tautologies (clauses whose conclusion is already present in the hypotheses) are removed.

• Elimination of hypotheses attacker(v). Hypotheses attacker(v), where the variable v does not occur elsewhere in the clause, are removed. Indeed, such an hypothesis is always satisfied for some value of v, for instance by (Rn).

• Decomposition of data constructors. For each data constructor f , the following clauses are generated:

attacker(x 1 ) ∧ . . . ∧ attacker(x n ) ⇒ attacker(f (x 1 , . . . , x n )) (Rf) attacker(f (x 1 , . . . , x n )) ⇒ attacker(x i ) (Rg)

Treatment of disequalities

The disequalities are simplified using the following transformations, adapted from (Blanchet et al., 2008), where the disequality predicate is written nounif:

• Elimination of free may-fail variables. Clauses of the form H ∧ ∀ v, (mp 1 , . . . , mp n ) = (mp 1 , . . . , mp n ) ⇒ C are transformed as follows.

When mp i or mp i is a may-fail variable u not in v, we replace the clause with two clauses

H ∧ ∀ v, (mp 1 , . . . , mp n ){ x / u } = (mp 1 , . . . , mp n ){ x / u } ⇒ C , H ∧ ∀ v, (mp 1 , . . . , mp n ){ fail / u } = (mp 1 , . . . , mp n ){ fail / u } ⇒ C ,
where x is an ordinary variable.

This transformation is repeated until all free may-fail variables have been removed from disequalities. It preserves the semantics of clauses because may-fail variables can be instantiated either with fail or with a pattern, while ordinary variables can be instantiated with a pattern. Otherwise, unify replaces the clause with

H ∧ ∀ v, (v 1 , . . . , v k ) = (σv 1 , . . . , σv k ) ⇒ C
where σ is the most general unifier of mp and mp and v 1 , . . . , v k are all variables affected by σ. In this unification, σ is built so that all variables in its domain and its image are variables of mp and mp , and the variables in its domain do not occur in its image.

Note that an instance of ∀ v, (v 1 , . . . , v k ) = (σv 1 , . . . , σv k ) holds if and only if the same instance of ∀ v, mp = mp does, because σ mp = σ mp if and only if σ (v 1 , . . . , v k ) = σ σ(v 1 , . . . , v k ), for all σ .

For instance, unify transforms the clause

H ∧ ∀z, (senc(x , y ), z ) = (senc(z, y), z) ⇒ C into H ∧ ∀z, (x , y , z ) = (z, y, z) ⇒ C (3.5)
• Elimination of elements of v. The transformation elimGVar transforms facts ∀ v, (mp 1 , . . . , mp n ) = (mp 1 , . . . , mp n ) in clauses obtained after unify, as follows:

1. When mp i = u ∈ v is a may-fail variable, it eliminates the pair mp i , mp i from the disequality and removes u from v.

2. When mp i = x ∈ v is a variable and mp i is a pattern, it eliminates the pair mp i , mp i from the disequality and removes x from v.

3. Otherwise, when mp i ∈ v, it swaps mp i and mp i everywhere in the disequality (mp 1 , . . . , mp n ) = (mp 1 , . . . , mp n ), then applies one of the first two cases.

The cases in which mp i is an ordinary variable and mp i = fail, or mp i is an ordinary variable and mp i = fail cannot happen by the previous application of unify.

We show that, in all cases, an instance of the initial disequality holds if and only if the same instance of the transformed disequality holds.

In Case 1, u does not occur elsewhere in the disequality by the previous application of unify, so for any substitution σ,

σ(∀ v, (mp 1 , . . . , mp n ) = (mp 1 , . . . , mp n )) is equivalent to σ(∀ v , (∀u, u = mp i ) ∨ (mp 1 , . . . , mp i-1 , mp i+1 , . . . , mp n ) = (mp 1 , . . . , mp i-1 , mp i+1 , . . . , mp n ))
which is equivalent to

σ(∀ v , (mp 1 , . . . , mp i-1 , mp i+1 , . . . , mp n ) = (mp 1 , . . . , mp i-1 , mp i+1 , . . . , mp n ))
since ∀u, u = σmp i is false for all σ.

In Case 2, ∀x, x = σmp i is false, so we can proceed as in Case 1.

In Case 3, swapping preserves the semantics of the disequality, since the unification constraints remain the same. Furthermore, swapping also preserves the property that mp i does not occur elsewhere.

For instance, elimGVar transforms Clause (3.5) into

H ∧ ∀z, (z, y , z ) = (x , y, x ) ⇒ C
by swapping z and x (Case 3), then transforms it into

H ∧ (y , z ) = (y, x ) ⇒ C
by Case 2.

• Detection of failed disequality. Clauses that contain the hypothesis ∀ v, () = () are removed.

Soundness

The soundness and completeness of this algorithm is justified by the following theorem:

Theorem 3.2. Let F be a closed fact. The fact F is derivable from R 0 if and only if it is derivable from saturate(R 0 ).

This theorem is a particular case of (Blanchet, 2009, Lemma 2), with the treatment of disequalities handled as in (Blanchet et al., 2008, Lemma 36). It shows that one can saturate the clauses by saturate without changing the set of derivable facts. One can then determine which instances of pred(p 1 , . . . , p n ) are derivable by the following computation:

solve P 0 ,N pub ,N priv (pred(p 1 , . . . , p n )) = {H ⇒ pred(p 1 , . . . , p n ) | H ⇒ pred (p 1 , . . . , p n ) ∈ saturate(R 0 )} ,
where pred is a new predicate and R 0 = R P 0 ,N pub ,N priv ∪ {pred(p 1 , . . . , p n ) ⇒ pred (p 1 , . . . , p n )}. Indeed, σpred(p 1 , . . . , p n ) is derivable from R P 0 ,N pub ,N priv if and only if σpred (p 1 , . . . , p n ) is derivable from R 0 , so by Theorem 3.2, if and only if σpred (p 1 , . . . , p n ) is derivable from saturate(R 0 ), so if and only if there exist a clause H ⇒ pred(p 1 , . . . , p n ) in solve P 0 ,N pub ,N priv (pred(p 1 , . . . , p n )) and a substitution σ such that σ pred(p 1 , . . . , p n ) = σpred(p 1 , . . . , p n ) and σ H is derivable from saturate(R 0 ). In particular, if solve P 0 ,N pub ,N priv (attacker(p)) = ∅, then attacker(p) is not derivable from R P 0 ,N pub ,N priv . Moreover, if the selection function is sel 0 and solve P 0 ,N pub ,N priv (attacker(p)) is non-empty, then at least one instance of attacker(p) is derivable. Indeed, in that case solve P 0 ,N pub ,N priv (attacker(p)) contains a clause R = H ⇒ attacker(σp) with sel 0 (R) = ∅, so the hypothesis H contains facts of the form attacker(x) and disequalities. Consider a substitution σ that maps each variable to b 0 [M ] for a distinct closed term M . Any fact σ attacker(x) is derivable by (Rn). Using invariants of the clauses and properties of the simplification of disequalities, we can show that for all disequalities F that occur in H, σ F holds. Hence σ H is derivable, so attacker(σ σp) is derivable.

Termination

In general, the resolution algorithm may not terminate. (The derivability problem is undecidable.) In practice, however, it terminates in most examples. [START_REF] Blanchet | Verification of Cryptographic Protocols: Tagging Enforces Termination[END_REF] have shown that it always terminates on a large and interesting class of protocols, the tagged protocols. They consider protocols that use as cryptographic primitives only public-key encryption and signatures with atomic keys, shared-key encryption, message authentication codes, and hash functions. Basically, a protocol is tagged when each application of a cryptographic primitive is marked with a distinct constant tag. It is easy to transform a protocol into a tagged protocol by adding tags. For instance, our running example of protocol can be transformed into a tagged protocol, by adding the tags c 0 , c 1 , c 2 to distinguish the encryptions and signature:

Message 1. A → B : aenc((c 1 , sign((c 0 , k), ssk A )), pk B ) Message 2. B → A : senc((c 2 , s), k)
Adding tags preserves the expected behavior of the protocol, that is, the attack-free executions are unchanged. In the presence of attacks, the tagged protocol may be more secure. Hence, tagging is a feature of good protocol design, as explained e.g. in [START_REF] Abadi | Prudent Engineering Practice for Cryptographic Protocols[END_REF]: the tags are checked when the messages are received; they facilitate the decoding of the received messages and prevent confusions between messages. More formally, tagging prevents type-flaw attacks [START_REF] Heather | How to Prevent Type Flaw Attacks on Security Protocols[END_REF], which occur when a message is taken for another message. Hence, the tagged protocol is potentially more secure than its untagged version, so, in other words, a proof of security for the tagged protocol does not imply the security of its untagged version.

We illustrate the effect of tagging on the Needham-Schroeder sharedkey protocol [START_REF] Needham | Using Encryption for Authentication in Large Networks of Computers[END_REF]. The algorithm does not terminate on its original version, which is untagged. It terminates after adding tags. This protocol contains the following messages:

Message 4. B → A : senc(b, k) Message 5. A → B : senc(b -1, k)
where b is a nonce. Representing b -1 using a function minusone(x) = x -1, the algorithm does not terminate. Indeed, the output of message 5 is represented by a clause of the form: H ∧ attacker(senc(x, y)) ⇒ attacker(senc(minusone(x), y))

where the hypothesis H describes other messages previously received by A. After some resolution steps, we obtain a clause of the form

attacker(senc(x, M k )) ⇒ attacker(senc(minusone(x), M k )) (Loop)
for some term M k that represents the key k.

The fact attacker(senc(minusone(M b ), M k )) is also derived for some term M b that represents the nonce b, so by resolution with (Loop), we derive: attacker(senc(minusone(minusone(M b )), M k )). This fact can again be resolved with (Loop), so that we obtain a cycle that derives attacker(senc(minusone n (M b ), M k )) for all n.

When tags are added, the clause (Loop) becomes: Other authors have proved related results: Ramanujam and Suresh, 2003 have shown that secrecy is decidable for tagged protocols. However, their tagging scheme is stronger since it forbids blind copies. A blind copy happens when a protocol participant sends back part of a message he received without looking at what is contained inside this part. On the other hand, they obtain a decidability result, while Blanchet and Podelski, 2005 obtain a termination result for an algorithm which is sound, efficient in practice, but approximate. [START_REF] Arapinis | Bounding Messages for Free in Security Protocols[END_REF] show that, for a class named "well-formed protocols", it is enough to consider well-typed attacks; this theorem allows them to extend the decidability result of [START_REF] Ramanujam | Tagging Makes Secrecy Decidable with Unbounded Nonces as Well[END_REF]Suresh, 2003, still forbidding blind copies. Comon-Lundh and[START_REF] Comon-Lundh | New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols[END_REF] show that an algorithm using ordered binary resolution, ordered factorization and splitting terminates on protocols that blindly copy at most one term in each message. In contrast, the result of [START_REF] Blanchet | Verification of Cryptographic Protocols: Tagging Enforces Termination[END_REF] puts no limit on the number of blind copies, but requires tagging.

attacker(senc((c 1 , x), M k )) ⇒ attacker(senc((c 2 , minusone(x)), M k )) (
For protocols that are not tagged, heuristics have been designed to adapt the selection function in order to obtain termination more often. We refer the reader to (Blanchet, 2009, §8.2) for more details.

It is also possible to obtain termination in all cases at the cost of additional abstractions. For instance, [START_REF] Goubault-Larrecq | Deciding H 1 by resolution[END_REF] shows that one can abstract the clauses into clauses in the decidable class H 1 , by losing some relational information on the messages.

Correspondences

Correspondences are properties of the form "if an event has been executed, then other events have been executed." Properties on the ordering of execution of events are also studied in other contexts, for instance in software verification to check that a file is always opened before being closed or that a lock is always acquired before being released. However, in the case of protocols, the events we want to relate are typically in different parallel processes, which complicates the proof.

To model correspondence properties, we introduce an additional construct in our process calculus, namely event(M ); P , which executes event M , then process P . The semantics of this construct is simply defined by

E, P ∪ { event(M ); P } → E, P ∪ { P } (Red Event)
The N pub -adversaries are restricted to processes that do not contain events (otherwise, no correspondence could be proved). We can then define the fact that a trace executes an event:

Definition 3.4. Let M be a closed term. We say that a trace Tr = E 0 , P 0 → * E , P executes event M if and only if it contains a reduction E, P ∪ { event(M ); P } → E, P ∪ { P } for some E, P, and P .

The correspondence event(M ) m j=1 l j k=1 event(M jk ) means intuitively that, if event M has been executed, then there exists j such that events M j1 , . . . , M jl j have been executed. More precisely, for any value of the variables of M , if event M has been executed, then there exists j and values of the variables of M j1 , . . . , M jl j that do not appear in M such that events M j1 , . . . , M jl j have been executed. The formal definition is as follows:

Definition 3.5. The closed process P 0 satisfies the correspondence

event(M ) m j=1 l j k=1 event(M jk )
against N pub -adversaries if and only if, for some N priv disjoint from N pub such that fn(P 0 ) ∪ fn(M ) ∪ j,k fn(M jk ) ⊆ N pub ∪ N priv , for any N pub -adversary Q, for any trace Tr = (N pub , N priv ), {P 0 , Q} → * E , P , for any substitution σ, if Tr executes event σM , then there exist σ and j ∈ {1, . . . , m} such that σ M = σM and, for all k ∈ {1, . . . , l j }, Tr executes event σ M jk .

Example 3.3. For example, we can modify the process P 0 of §2.2 by adding events as follows: out (c, aenc(sign(k2b(k)

P 0 = new
, ssk A ), x pk B )); in(c, x : bitstring); let z = sdec(x, k) in 0 P B (pk B , sk B , spk A ) = ! in(c, y : bitstring); let y = adec(y, sk B ) in let x k = b2k(check(y , spk A )) in event(e B (spk A , pk B , x k )); out(c, senc(s, x k ))
The event e A (spk A , x pk B , k) intuitively means that A started a session of the protocol between the participants with public keys spk A (that is, A) and x pk B , with the shared key k. Similarly, the event e B (spk A , pk B , x k ) means that B accepted the shared key k in a session between participants A and B. We can then try to show the correspondence event(e B (x, y, z))

event(e A (x, y, z)), which means that, if e B (x, y, z) has been executed, then e A (x, y, z) has also been executed.

In other words, if B thinks he runs a session of the protocol with A and the shared key z, then A thinks she runs a session of the protocol with B and the same key z. This is an authentication property.

As mentioned above, the Horn clause verification method overapproximates the actions that are executed: when attacker(p) is derivable from the clauses, the adversary may have p, that is, if attacker(p) is not derivable from the clauses, then the adversary cannot have p, but the converse is not true. Let us now consider the proof of a correspondence, for instance event(e 1 (x))

event(e 2 (x)), that is, we want to show that, if e 1 (x) has been executed, then e 2 (x) has been executed. In order to prove this correspondence, we can overapproximate the executions of event e 1 : if we prove the correspondence with this overapproximation, it will also hold in the exact semantics. So we can easily extend our analysis for secrecy with an additional predicate event, such that event(p) means that event p (more formally, event M with corresponding pattern p) may have been executed. We generate clauses message(p 1 , p 1 ) ∧ . . . ∧ message(p n , p n ) ⇒ event(p) when the process executes event p after receiving messages p 1 , . . . , p n on channels p 1 , . . . , p n respectively. However, such an overapproximation cannot be done for the event e 2 : if we prove the correspondence after overapproximating the execution of e 2 , we are not really sure that e 2 will be executed, so the correspondence may be wrong in the exact semantics. For instance, assuming c is public, the process in(c, x); event(e 1 (x)) | in(c, x ); event(e 2 (x )) may execute e 1 (x) and e 2 (x) for all x that the adversary has, but the correspondence event(e 1 (x))

event(e 2 (x)) does not hold for this process: there is a trace in which it executes e 1 (c) but does not execute e 2 (c). Therefore, we have to use a different method for treating e 2 .

We use the following idea: we fix the exact set Ev of allowed events e 2 (p) and, in order to prove event(e 1 (x))

event(e 2 (x)), we check that only events e 1 (p) for p such that e 2 (p) ∈ Ev can be executed. Therefore, if e 1 (M ) has been executed, then e 1 (p) has been executed with p the pattern corresponding to M , so e 2 (p) ∈ Ev has been executed, so e 2 (M ) has been executed, since a single term M corresponds to a given pattern p thanks to session identifiers, which allow us to distinguish the names created by the same restriction. If we prove this property for any value of Ev, we have proved the desired correspondence. So we introduce a predicate m-event (must event), such that m-event(p 0 ) is true if and only if p 0 ∈ Ev. We generate clauses message(p 1 , p 1 ) ∧ . . . ∧ message(p n , p n ) ∧ m-event(p 0 ) ⇒ message(p, p ) when the process outputs p on channel p after executing event p 0 and receiving messages p 1 , . . . , p n on channels p 1 , . . . , p n respectively. In other words, the output of p on channel p can be executed only when m-event(p 0 ) is true, that is, p 0 ∈ Ev.

More generally, we extend the computation of Horn clauses to events as follows:

[[event(M ); P ]]ρsH = [[P ]]ρs(H ∧ m-event(ρ(M ))) ∪ {H ∧ m-event(ρ(M )) ⇒ event(ρ(M ))}
We add the hypothesis m-event(ρ(M )) to H to express that P can be executed only if event M is allowed (which is useful for e 2 in the example above), and we add the clause H ∧ m-event(ρ(M )) ⇒ event(ρ(M )) to express that the event may be executed if H is true and the event is allowed (which is useful for e 1 in the example above).

In order to determine whether an event can be executed, we determine whether the corresponding fact is derivable from the clauses, by extending the previous resolution-based algorithm. Indeed, the resolution must be performed for an unknown value of Ev. So, basically, we keep m-event facts without trying to evaluate them (which we cannot do since Ev is unknown). To do that, we modify the selection function so that it never selects a fact of the form m-event(p). We do not know of an off-the-shelf first-order resolution prover that implements this feature, though it would probably not be difficult to add to existing provers. Letting F me = {m-event(p) | p ∈ Ev}, Theorem 3.2 becomes:

Theorem 3.3. Let F be a closed fact. The fact F is derivable from R 0 ∪ F me if and only if it is derivable from saturate(R 0 ) ∪ F me .
As for secrecy, we define R 0 = R P 0 ,N pub ,N priv ∪ {pred(p 1 , . . . , p n ) ⇒ pred (p 1 , . . . , p n )}. We have that σpred(p 1 , . . . , p n ) is derivable from R P 0 ,N pub ,N priv ∪ F me if and only if there exist a clause H ⇒ pred(p 1 , . . . , p n ) in solve P 0 ,N pub ,N priv (pred(p 1 , . . . , p n )) and a substitution σ such that σ pred(p 1 , . . . , p n ) = σpred(p 1 , . . . , p n ) and σ H is derivable from saturate(R 0 ) ∪ F me . Since no clause outside F me concludes m-event facts, the m-event facts in σ H must be in F me , which guarantees that the corresponding events have been executed. We can then show the following theorem: Theorem 3.4. Let P 0 be a closed process and N pub be a set of names. Let M , M jk (j ∈ {1, . . . , m}, k ∈ {1, . . . , l j }) be terms. Let p, p jk be the patterns obtained by replacing names a with patterns a[ ] in terms M , M jk respectively. Let N priv be a set of names disjoint from N pub such that fn(P 0 ) ∪ fn(M ) ∪ j,k fn(M jk ) ⊆ N pub ∪ N priv . Suppose that, for all clauses R ∈ solve P 0 ,N pub ,N priv (event(p)), there exist j ∈ {1, . . . , m}, σ and

H such that R = H ∧ m-event(σ p j1 ) ∧ . . . ∧ m-event(σ p jl j ) ⇒ event(σ p). Then P 0 satisfies the correspondence event(M ) m j=1 l j k=1 event(M jk ) against N pub -adversaries.
This result is a particular case of Blanchet, 2009, Theorem 4. Intuitively, if all clauses are of the form H ∧ m-event(σ p j1 ) ∧ . . . ∧ m-event(σ p jl j ) ⇒ event(σ p), then, in order to derive event(σ p), the facts m-event(σ p j1 ), . . . , m-event(σ p jl j ) must be true, so in order to execute event σ p, the events σ p j1 , . . . , σ p jl j must have been executed, which proves the desired correspondence.

Example 3.4. For the process P 0 of Example 3.3, the set of clauses solve P 0 ,N pub ,N priv (event(e B (x, y, z))) contains m-event(e A (pk(ssk

A [ ]), pk(y ), k[i, pk(y )])) ∧ attacker(y ) ⇒ event(e B (pk(ssk A [ ]), pk(sk B [ ]), k[i, pk(y )])) .
This clause prevents us from applying Theorem 3.4 to prove the correspondence event(e B (x, y, z))

event(e A (x, y, z)), because the fact m-event(e A (pk(ssk A [ ]), pk(y ), k[i, pk(y )])) contains pk(y ) instead of pk(sk B [ ]). This point corresponds again to the known attack against this protocol: A executes a session with C, which has secret key y and public key pk(y ), while B thinks he executes a session with A. In contrast, for the fixed version of the protocol with the public key of B added inside the signature as in Example 2.5,

solve P 0 ,N pub ,N priv (event(e B (x, y, z))) = {m-event(e A (pk(ssk A [ ]), pk(sk B [ ]), k[i, pk(sk B [ ])])) ⇒ event(e B (pk(ssk A [ ]), pk(sk B [ ]), k[i, pk(sk B [ ])]))} ,
so the desired correspondence is proved.

We extended these results to injective correspondences, that is, correspondences that additionally require that each execution of event M corresponds to a distinct execution of events M jk . The proof of injectivity relies on session identifiers to distinguish different executions of the same event. We also extended this work to nested correspondences, which can express constraints on the order in which events are executed (Blanchet, 2009, §7.2).

Attack reconstruction was also extended to non-injective and injective correspondences, and it reconstructs the attack of Example 3.4. The extension to injective correspondences presents an additional difficulty: the derivation corresponds to a single execution of event M while, to contradict injectivity, event M must be executed twice and an event M jk must be executed at most once. To solve this problem, we consider two copies of the derivation with variables renamed to distinct variables, and unify some events M jk between these two copies so that they correspond to a single event. After this unification, the two copies of the derivation contain the unified events M jk with the same session identifiers, but still contain event M with different session identifiers, because the derivation does not prove injectivity. We execute the attack reconstruction algorithm with these two copies of the derivation. That allows this algorithm to execute most actions (including event M ) twice, but not the unified events M jk , because they occur with the same session identifier in both copies of the derivation. We can then look for a trace that executes event M twice, while still executing the unified events M jk once.

Equivalences

The notion of process equivalence is the main reasoning tool introduced initially with the spi calculus [START_REF] Abadi | A Calculus for Cryptographic Protocols: The Spi Calculus[END_REF]Abadi and Gordon, 1998) and the applied pi calculus [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF][START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF], with manual proofs. Intuitively, two processes are equivalent when the adversary cannot distinguish them. Proving equivalences is more delicate than proving trace properties, because we need to consider relations between traces or semantic configurations, instead of a single trace. In general, equivalence is undecidable [START_REF] Hüttel | Deciding Framed Bisimilarity[END_REF][START_REF] Abadi | Deciding Knowledge in Security Protocols under Equational Theories[END_REF], so automated techniques are incomplete. For a bounded number of sessions, several tools can decide trace equivalence: SPEC [START_REF] Tiu | Automating Open Bisimulation Checking for the Spi Calculus[END_REF] for fixed primitives and without else branches, APTE [START_REF] Cheval | Trace Equivalence Decision: Negative Tests and Non-determinism[END_REF] for fixed primitives with else branches and non-determinism, and AKISS [START_REF] Chadha | Automated Verification of Equivalence Properties of Cryptographic Protocols[END_REF][START_REF] Ciobâcă | Automated Verification of Security Protocols with Applications to Electronic Voting[END_REF] for a wide variety of primitives and determinate processes, that is, processes whose execution is entirely determined by the adversary inputs. For an unbounded number of sessions, decision procedures exist for restricted classes of protocols: there is a decision procedure for trace equivalence for symmetric-key, type-compliant, acyclic protocols (Chrétien et al., 2015a), which is too complex for practical implementation, and for ping-pong protocols (Chrétien et al., 2015b), which is implemented in a tool. ProVerif also proves a restricted class of equivalences, explained below.

Next, we give a formal definition of observational equivalence. This definition, inspired by [START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF][START_REF] Arapinis | Stateful Applied Pi Calculus[END_REF], relies on the semantics with configurations while our previous work [START_REF] Blanchet | Automatic Proof of Strong Secrecy for Security Protocols[END_REF]Blanchet et al., 2008) uses a semantics closer to the applied pi calculus (see Chapter 4).

We consider configurations (N pub , N priv ), P as equal modulo any bijective renaming of names that leaves names in N pub unchanged. It is easy to see that such renamings commute with reduction, so all configurations in a trace are just transformed by such a renaming. Hence the semantics is not significantly altered. Allowing such renamings is helpful in order to define the application of a context to a configuration below. However, it would be problematic in our definition of correspondences, since names appear inside events and these names must not be modified between executions of several events that appear in a correspondence.

A configuration C = (N pub , N priv ), P can output on a channel N , denoted, C ↓ N , if there exists out(N, M ); P ∈ P with fn(N ) ⊆ N pub , for some term M and process P . For equivalences, the adversary is represented by an adversarial context. A context C[_] is a process with a hole, written _. Let adversarial contexts be contexts of the form new n;

(_ | Q) with fv(Q) = ∅ and all function symbols in Q are public. When C = (N pub , N priv ), P and C[_] = new n; (_ | Q) is an adversarial context, we define the application of context C[_] to the configuration C by C[C] = ((N pub ∪ fn(Q)) \ { n}, N priv ∪ { n}), P ∪ {Q},
after renaming the names in N priv so that N priv ∩ fn(Q) = ∅. The condition N priv ∩ fn(Q) = ∅ avoids clashes between the private names of the configuration C and the names of the adversary. To compute C [C], we add the process Q to the multiset P of processes of the configuration C, so that Q runs in parallel with these processes. The free names of Q are public, so we add them to N pub . Further, we apply the restriction new n by moving the names n from N pub to N priv . Definition 3.6 (Observational equivalence). Observational equivalence between configurations ≈ is the largest symmetric relation R between valid configurations such that C R C implies:

1. if C ↓ a , then C → * ↓ a , for all names a; 2. if C → C 1 , then C → * C 1 and C 1 R C 1 , for some C 1 . 3. C[C] R C[C ] for all adversarial contexts C[_].
We define observational equivalence on semantic configurations. Item 1 guarantees that, if a configuration C emits on a public channel, then so does C . Otherwise, an adversary could distinguish them immediately. Item 2 guarantees that this property is preserved by reduction, and Item 3 guarantees that it is preserved in the presence of an adversary. For proving observational equivalence in general, it is not enough to consider traces of one process, we need to relate the configurations of two processes together. For this reason, the proof of observational equivalence is difficult to automate, so ProVerif was designed to prove classes of equivalences that are easier to handle, but still interesting in practice.

The simplest class of equivalences that ProVerif verifies is strong secrecy (in the case without equational theory) [START_REF] Blanchet | Automatic Proof of Strong Secrecy for Security Protocols[END_REF]: strong secrecy means that the adversary cannot distinguish two versions of the protocol that use different values of the secret. This property is defined as follows:

Definition 3.7. The closed process P 0 preserves the strong secrecy of s with private names N priv if and only if for all closed terms M and N with (fn(M ) ∪ fn(N )) ∩ N priv = ∅, for some N pub disjoint from

N priv such that fn(P 0 ) ∪ fn(M ) ∪ fn(N ) ⊆ N pub ∪ N priv , we have (N pub , N priv ), P 0 { M / s } ≈ (N pub , N priv ), P 0 { N / s }.
To prove strong secrecy, ProVerif relies on a trace property: it shows that no test (destructor application, communication on a channel) that gives a different result for different values of the secret is reachable. This reachability property is encoded by Horn clauses, with an additional predicate used for testing whether a unification succeeds for some values of the secret and not for others.

Example 3.5. ProVerif cannot prove that the protocol of §2.2 preserves the strong secrecy of s. This is not surprising since it does not even preserve the secrecy of s. ProVerif proves that the fixed protocol of Example 2.5 preserves the strong secrecy of s: not only the adversary cannot compute s, but also it cannot distinguish when the value of s changes.

ProVerif can also verify a more general class of equivalences, whose proof is also more difficult: the equivalences between processes P and Q that differ only by the terms they contain (Blanchet et al., 2008). These equivalences are again proved by relying on a trace property, for a process that represents both P and Q. This idea extends the technique of [START_REF] Pottier | Information Flow Inference for ML[END_REF][START_REF] Pottier | A Simple View of Type-Secure Information Flow in the π-Calculus[END_REF] for information flow (without cryptography) to the case of security protocols.

ProVerif represents pairs of processes that differ only by the terms they contain as biprocesses. The grammar of biprocesses is an extension of the grammar of Figure 2.1, with the additional cases diff[M, M ] for terms and diff[D, D ] for expressions. The N pub -adversaries and the adversarial contexts do not contain diff. Given a biprocess P , we define two processes fst(P ) and snd(P ), as follows: fst(P ) is obtained by replacing all occurrences of diff[M, M ] with M and diff[D, D ] with D in P , and snd(P ) is obtained by replacing diff[M, M ] with M and diff[D, D ] with D in P . We define fst(M ), snd(M ), fst(D), and snd(D) similarly. We naturally extend fst and snd to multisets of processes, and to configurations by fst(E, P) = E, fst(P) and snd(E, P) = E, snd(P). Our goal is to show that the processes fst(P ) and snd(P ) are observationally equivalent.

Definition 3.8. The closed biprocess P 0 satisfies observational equivalence with private names N priv if and only if, for some N pub disjoint from N priv such that fn(P 0 ) ⊆ N pub ∪ N priv , we have that (N pub , N priv ), {fst(P 0 )} ≈ (N pub , N priv ), {snd(P 0 )}.

The semantics of biprocesses is defined as in Figure 2.4, except that the rules (Red I/O), (Red Eval 1), and (Red Eval 2) are as follows:

E, P ∪ { out(N, M ); Q, in(N , x); P } → E, P ∪ { Q, P {M/x} } if fst(N ) = fst(N ) and snd(N ) = snd(N ) (Red I/O) E, P ∪ { let x = D in P else Q } → E, P ∪ { P {diff[M, M ]/x} } if fst(D) ⇓ M and snd(D) ⇓ M (Red Eval 1) E, P ∪ { let x = D in P else Q } → E, P ∪ { Q } if fst(D) ⇓ fail and snd(D) ⇓ fail (Red Eval 2)
and the rules for the conditional are omitted because the conditional if M then P else Q can be encoded as an expression evaluation let x = istrue(M ) in P else Q, where x is a fresh variable and istrue(bool) : bool is a destructor defined by the rewrite rule istrue(true) → true. A biprocess P reduces by this semantics when its two components fst(P ) and snd(P ) reduce in the same way: a communication is executed when the channel is the same in the input and in the output for both components; an expression evaluation succeeds (resp. fails) when it succeeds (resp. fails) for both components. In particular, if C → C , then fst(C) → fst(C ) and snd(C) → snd (C ).

When the two components do not reduce in the same way, we say that the configuration C diverges, and we write C ↑ (vocabulary and notation from [START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF]):

E, P ∪ { out(N, M ); Q, in(N , x); P } ↑ if (fst(N ) = fst(N )) ⇔ (snd(N ) = snd(N )) (Div I/O) E, P ∪ { let x = D in P else Q } ↑ if fst(D) ⇓ fail ⇔ snd(D) ⇓ fail (Div Eval)
When the configuration C does not diverge, the two components always reduce in the same way, that is, the biprocess reduces. Formally, if C does not diverge and fst(C) → C 1 , then C → C and C 1 = fst(C ) for some C , and similarly for snd. If no reachable configuration diverges, then the two components of the considered biprocess P 0 always reduce in the same way. This property is formally defined as follows:

Definition 3.9. Let P 0 be a closed biprocess and N priv be a set of names.

The biprocess P 0 satisfies diff-equivalence with private names N priv if, for some N pub disjoint from N priv such that fn(P 0 ) ⊆ N pub ∪ N priv , for all N pub -adversaries Q, there exists no configuration C such that (N pub , N priv ), {P 0 , Q} → * C ↑.

Diff-equivalence implies observational equivalence, as shown by the following theorem: Theorem 3.5. Let P 0 be a closed biprocess and N priv be a set of names. If P 0 satisfies diff-equivalence with private names N priv , then P 0 satisfies observational equivalence with private names N priv .

Since the formalism is fairly different from the one used in our previous work (Blanchet et al., 2008), we provide a proof of this result in Appendix A. Diff-equivalence is a trace property on biprocesses. By Theorem 3.5, it suffices in order to obtain observational equivalence. It is however not necessary: for instance, if (N pub , N priv ), P ≈ (N pub , N priv ), P , then the biprocess if diff[true, false] then P else P satisfies observational equivalence with private names N priv , but Theorem 3.5 does not allow us to prove it (because this biprocess diverges immediately). The property on the traces of biprocesses is encoded into Horn clauses as before. However, in order to represent the semantics of biprocesses, we use facts attacker (p 1 , p 2 ) and message (p 1 , p 1 , p 2 , p 2 ), where components with index 1 correspond to fst(P ) and those with index 2 correspond to snd(P ), instead of attacker (p) and message (p, p ). The fact attacker (p 1 , p 2 ) means that, by the same actions, the adversary obtains p 1 by interacting with fst(P ) and p 2 by interacting with snd(P ). The fact message (p 1 , p 1 , p 2 , p 2 ) means that, by the same actions, fst(P ) sends message p 1 on channel p 1 while snd(P ) sends message p 2 on channel p 2 . We also use the fact input (p 1 , p 2 ) to express that an input on channel p 1 may be executed by fst(P ) while snd(P ) executes an input on p 2 . (This situation allows the adversary to test the equality of these channels with those used in an output.) We can then encode the desired trace property on biprocesses into clauses and prove it by resolution, which allows us to apply Theorem 3.5.

Example 3.6. We may consider the property that the secret s exchanged in our running example is indistinguishable from a fresh name, representing intuitively a fresh random value. This notion of secrecy is the symbolic analog of real-or-random secrecy in the computational model [START_REF] Abdalla | Password-Based Authenticated Key Exchange in the Three-Party Setting[END_REF]. This property can be verified in ProVerif by replacing the final output of the process P B of §2.2 with new r : bitstring; out(c, senc(diff[s, r], x k ))

The obtained process satisfies observational equivalence with private names {s} when the adversary cannot distinguish whether the output message contains the encryption of the secret s or of a fresh name r.

ProVerif finds an attack against diff-equivalence, both for the original version of the protocol (as expected given the attack of Example 3.2), and for the fixed version. Indeed, the fixed version is also subject to an attack against this equivalence: if the message from A to B is replayed, the first component sends the same encrypted message senc(s, k) twice, while the second component sends two distinct messages senc(r 1 , k) and senc(r 2 , k), with two distinct values of r.

A possible fix against this attack is to use a probabilistic symmetric encryption scheme, defined with a constructor senc(bitstring, pkey, rand), such that the encryption of message M under the key k is represented by senc(M, k, coins) where coins is a fresh name representing fresh random coins. Decryption is defined by the rewrite rule sdec(senc(x, y, z), y) → x .

The fixed protocol is obtained by replacing the final output of the process P B of Example 2.5 with new r : bitstring; new coins : rand; out(c, senc(diff[s, r], x k , coins))

The ciphertexts are then different even when they encrypt the same plaintext under the same key, and ProVerif proves that the obtained process satisfies observational equivalence with private names {s}. [START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF] shows the decidability of diff-equivalence for processes without replication, in a framework similar to ours. The protocol verifiers Maude-NPA [START_REF] Santiago | A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA[END_REF] and Tamarin [START_REF] Basin | Automated Symbolic Proofs of Observational Equivalence[END_REF] can also prove diff-equivalence.

An important application of diff-equivalence is the study of protocols that rely on weak secrets, such as passwords. These protocols are subject to guessing attacks, in which the adversary guesses the password (for instance by trying all words of a dictionary), and verifies that it has correctly guessed. This verification may be performed either on-line, by interacting with the protocol participants, which can simply be prevented by limiting the number of allowed attempts, or off-line, by computing on intercepted messages without interaction with the other participants.

Off-line guessing attacks can be modeled by combining observational equivalence, phases ( §2.5.4), and primitives defined by equations ( §2.5.1), since it is often necessary that the failure of decryption cannot be detected in order to protect oneself against such attacks.

In phase 0, the adversary interacts with the protocol, but the weak secret w is considered as unguessable. In phase 1, the adversary guesses a value of the weak secret, and tries to determine whether its guess is correct or not. The absence of off-line guessing attacks is characterized by an equivalence: the adversary cannot distinguish the weak secret w used in phase 0 from a fresh value w , so it cannot determine whether its guess is correct or not. Definition 3.10. Let P 0 be a closed process without phase prefix and N priv a set of names. We say that P 0 , with private names N priv , prevents off-line guessing attacks against w if new w; (phase 0; P 0 | phase 1; new w ; out(c, diff[w, w ])) satisfies observational equivalence with private names N priv .

ProVerif can prove that the protocols EKE [START_REF] Bellovin | Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks[END_REF] and Augmented EKE [START_REF] Bellovin | Augmented Encrypted Key Exchange: a Password-Based Protocol Secure Against Dictionary Attacks and Password File Compromise[END_REF] satisfy this property. This definition is in the line of work by [START_REF] Lowe | Analyzing Protocols Subject to Guessing Attacks[END_REF][START_REF] Cohen | Proving Protocols Safe from Guessing[END_REF][START_REF] Corin | Guess What? Here is a New Tool that Finds some New Guessing Attacks[END_REF][START_REF] Corin | Analysing Password Protocol Security Against Off-line Dictionary Attacks[END_REF][START_REF] Delaune | A Theory of Dictionary Attacks and its Complexity[END_REF][START_REF] Drielsma | A Formalization of Off-line Guessing for Security Protocol Analysis[END_REF][START_REF] Lowe | Analyzing Protocols Subject to Guessing Attacks[END_REF] uses the model checker FDR to handle a bounded number of sessions. [START_REF] Delaune | A Theory of Dictionary Attacks and its Complexity[END_REF] give a decision procedure in this case. [START_REF] Corin | Analysing Password Protocol Security Against Off-line Dictionary Attacks[END_REF] give a definition based on equivalence like ours but do not consider the first active phase and analyze a single session.

In order to prove observational equivalence, ProVerif requires that the considered processes differ only by their terms. As suggested by [START_REF] Cheval | Proving More Observational Equivalences with ProVerif[END_REF], this limitation can be partly overcome by encoding as many constructs as possible into terms. Conditionals can be encoded into terms using the destructor ifthenelse defined in §2.1, as shown in Example 3.7. Expression evaluations such as m), where the destructors catch-fail and not-caught-fail are defined by the rewrite rules catch-fail(x) → x not-caught-fail(caught-fail) → false catch-fail(fail) → caught-fail not-caught-fail(x) → true and caught-fail is a new constant. After transformation, if D succeeds, then x has the same value as before, and x = caught-fail, so not-caught-fail(x) = true and ifthenelse(not-caught-fail(

let x = D in out(c, M 1 ) else out(c, M 2 ) can be transformed into let x = catch-fail(D) in let m = ifthenelse(not-caught-fail(x), M 1 , M 2 ) in out(c,
x), M 1 , M 2 ) re- turns M 1 ; if D fails, then x = caught-fail, not-caught-fail(x) = false, and ifthenelse(not-caught-fail(x), M 1 , M 2 ) returns M 2 .
Example 3.7. As in [START_REF] Cheval | Proving More Observational Equivalences with ProVerif[END_REF], we consider a simplified version of the private authentication protocol by [START_REF] Abadi | Private authentication[END_REF] In this protocol, a participant A is willing to reveal its identity to a participant B, without revealing it to other participants. Using the pattern-matching extension of §2.5.3, the roles of A and B may be written in ProVerif as follows: where sk A and sk B are the private keys of A and B, respectively. A first sends to B a nonce a and its own public key pk(sk A ) encrypted with the public key of B, pk(sk B ). After receiving this message, B checks that the message is of the correct form and that it contains the public key of A. If so, B replies with the correct message composed of the nonce a he received, a freshly generated nonce b, and his own public key (pk(sk B )), all this encrypted with the public key of A. Otherwise, B replies with an error message, aenc(b, pk(sk B )). From the point of view of the adversary, this error message is indistinguishable from the correct one since the private keys sk A and sk B are unknown to the adversary, so the adversary should not be able to tell whether B is willing to talk to A or to another participant. Formally, this anonymity property holds when the process new sk A : skey; new sk A : skey; new sk B : skey; out(c, (pk

A(sk A , sk B ) =
(sk A ), pk(sk A ), pk(sk B ))); B(sk B , diff[sk A , sk A ])
satisfies observational equivalence with no private names. This process generates private keys, publishes the corresponding public keys, and runs B talking to A in the first component and to A in the second one. (A and A need not be explicitly modeled since the role of A uses only public keys, so it can be included in the adversary.)

ProVerif cannot prove this equivalence, because this process does not satisfy diff-equivalence. Suppose the adversary sends aenc((a, pk(sk A )), pk(sk B )) to B. Then xpk A = pk(sk A ), so the then branch of the test ( * ) is taken in B(sk B , sk A ), while the else branch is taken in B(sk B , sk A ).

The test ( * ) can be performed in a term, by transforming the process B(sk B , sk A ) into ProVerif proves diff-equivalence for the transformed process.

ProVerif includes an automatic process simplification procedure, which transforms conditionals and expression evaluations into terms when possible, as well as a merging procedure, which can merge two processes into a biprocess in order to prove observational equivalence, when the processes are sufficiently similar [START_REF] Cheval | Proving More Observational Equivalences with ProVerif[END_REF].

Another transformation useful for proving equivalence consists in swapping data between parallel processes at synchronization points. This transformation is particularly useful for e-voting protocols. Consider a process V (id A , v A ) that represents a voter id A voting v A . The voting protocol satisfies ballot secrecy when the process

V (id A , diff[v A , v B ]) | V (id B , diff[v B , v A ]) (3.6)
satisfies observational equivalence, which means that an adversary cannot distinguish when two voters swap their votes [START_REF] Delaune | Verifying Privacy-type Properties of Electronic Voting Protocols[END_REF].

In voting protocols, the voters often synchronize with each other, for instance because the protocol includes several stages, such as registration, voting, and tallying. To prove this equivalence, one often needs to swap the votes between the two voters at a synchronization point. This idea was introduced by [START_REF] Delaune | Automatic verification of privacy properties in the applied pi calculus[END_REF] and developed and formalized by Blanchet and Smyth, 2016. For instance, as in (Blanchet and Smyth, 2016), let us consider a toy protocol in which each voter first sends its identity on an anonymous channel to register, then sends its vote on an anonymous channel:

V (id A , v A ) = out(c, id A ); out(c, v A ) .
This protocol does not satisfy ballot secrecy because

V (id A , v A ) | V (id B , v B ) can output id A , v A , id B , v B on channel c in that order, while V (id A , v B ) | V (id B , v A ) cannot.
To solve this problem, the voters need to synchronize together after the registration. ProVerif represents the synchronization by the construct sync n, so the voting process becomes:

V (id A , v A ) = out(c, id A ); sync 1; out(c, v A ) . (3.7)
The synchronization construct sync n is similar to phase n except that it never drops processes that have not reached the synchronization yet. The number of processes that must synchronize is fixed from the beginning of the execution, and sync n blocks until that number of processes reach the synchronization sync n. For instance, consider the biprocess (3.6) where V is defined by (3.7), that is,

P 0 = out(c, id A ); sync 1; out(c, diff[v A , v B ]) | out(c, id B ); sync 1; out(c, diff[v B , v A ]) . (3.8)
The process P 0 contains two occurrences of sync 1, so sync 1 blocks until two processes reach sync 1. We refer the reader to (Blanchet and Smyth, 2016) for a formal semantics of synchronization.

The protocol P 0 satisfies ballot secrecy, but this property cannot be shown directly using diff-equivalence, because P 0 does not satisfy diffequivalence with no private names. Intuitively, diff-equivalence requires that the subprocesses of the parallel composition, namely, out(c, id A ); sync 1; out(c, diff[v A , v B ]) and out(c, id B ); sync 1; out(c, diff[v B , v A ]), each satisfy diff-equivalence, which is false, because out(c, v A ) is not equivalent to out(c, v B ). (Using the definition of diff-equivalence, we let

N priv = ∅, N pub = {c, id A , id B , v A , v B }, P 0 as in (3.8), and Q = in(c, x); in(c, y); in(c, x ); in(c, y ); let x = istrue(x = v A ) in out(c, v A ). The con- figuration (N pub , N priv ), {P 0 , Q} reduces into (N pub , N priv ), {let x = istrue(diff[v A , v B ] = v A ) in out(c, v A )} by receiving id A in x and id B in y, synchronizing, receiving diff[v A , v B ] in x and diff[v B , v A ]
in y , and removing 0 processes. The evaluation of istrue(diff[v A , v B ] = v A ) succeeds in the first component and fails in the second one, hence the obtained configuration diverges and the biprocess P 0 does not satisfy diff-equivalence.) To prove the equivalence, we need to swap the votes at the synchronization point in the second component of the biprocess, so that it becomes:

out(c, id A ); sync 1; out(c, diff[v A , v A ]) | out(c, id B ); sync 1; out(c, diff[v B , v B ])
which obviously satisfies diff-equivalence. Blanchet and Smyth, 2016 have designed, proved correct, and implemented a compiler that translates the synchronization construct into inputs and outputs and allows this swapping.

Usage heuristics

Several heuristics can help obtaining the best performance of ProVerif. Technical details on some of these heuristics can be found in (Blanchet et al., 2016, §6.3.1).

As mentioned in §2.5.1, using destructors when possible yields better performance than equations.

The precision and cost of the analysis can also be tuned by adjusting the arguments of patterns that represent names. By moving restrictions downwards in the syntax tree as far as possible, more inputs occur above restrictions, so the representation of the corresponding fresh names has more arguments. This transformation increases the precision and the cost of the analysis. Conversely, by moving restrictions upwards, the representation of the corresponding fresh names has fewer arguments, and the analysis is faster and less precise. ProVerif also allows the user to annotate restrictions with the variables that should occur in the internal representation of fresh names. (The session identifiers are always present. They are sufficient for soundness.) For the proof of equivalences, false attacks are sometimes due to names that have different arguments in the two components of the biprocess. In this case, making sure that matching names have the same arguments helps avoiding the false attack. This can be done by annotating the restrictions that create these names with the desired arguments.

When ProVerif does not terminate, tuning the selection function of the resolution algorithm may help. In particular, when ProVerif generates an unbounded number of clauses in which the selected fact is an instance of a fact F , one can tell ProVerif to avoid selecting a fact that matches F , by the declaration nounif F . ProVerif tries to detect some of these cases automatically, and to adjust the selection function accordingly, but sometimes manual declarations are still useful.

To share the work as much as possible, one can group several secrecy and correspondence queries together, in a single query declaration. ProVerif then generates a single set of Horn clauses for these queries, and saturates this set once. This is particularly beneficial when these queries use the same events. However, when queries use different events, it is often better to treat them separately, because the more events appear in a query, the more complex the generated clauses are, which can slow down ProVerif considerably. (Events that do not occur in the query are ignored when ProVerif generates the clauses.)

Finally, for the proof of equivalences, grouping all tests performed on a message in a single test can help avoiding false attacks. As a toy example, consider the biprocess

let x = diff[aenc(sign(a, sk A ), pk(sk B )), aenc(a, pk(sk A ))] in let y = adec(x, sk A ) in let z = check(y, pk(sk B )) in out(c, z)
This biprocess does not satisfy diff-equivalence with private names {a, sk A , sk B }, because the decryption adec(x, sk A ) fails in the first component (the keys do not match), while it succeeds in the second component. However, this biprocess satisfies observational equivalence, because the signature verification check(y, pk(sk B )) fails in the second component, so no component executes the output. ProVerif can prove the equivalence after grouping the decryption and the signature verification in one step:

let x = diff[aenc(sign(a, sk A ), pk(sk B )), aenc(a, pk(sk A ))] in let z = check(adec(x, sk A ), pk(sk B )) in out(c, z)
Indeed, this biprocess satisfies diff-equivalence because the combined decryption and signature verification fails in both components. In case a proof of equivalence fails, ProVerif performs an automatic process simplification that groups the tests [START_REF] Cheval | Proving More Observational Equivalences with ProVerif[END_REF]. However, grouping them manually in the initial process avoids the first failed proof attempt and yields better performance.

The input language of ProVerif is a dialect of the applied pi calculus introduced by [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF], and later updated by [START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF] In this chapter, we use the latter version. The applied pi calculus is an extension of the pi calculus with function symbols defined by an equational theory. It can be understood as a minimal core of the input language of ProVerif. This chapter formally relates the two languages.

The syntax of terms M of the applied pi calculus is the same as in ProVerif (Figure 2.1). The syntax of processes P of the applied pi calculus is given in Figure 4.1. Although the precise syntax of restrictions, inputs, and outputs differs, this calculus is very similar to the input language of ProVerif. More precisely, it matches a subset of the ProVerif language with equations ( §2.5.1) and enriched terms ( §2.5.2), with the following additional conditions: the only destructor is equal defined by (2.5), equal(M, N ) is written M = N , the expression in the conditional is always of the form M = N , and the destructor equal does not occur elsewhere; all function symbols are public; the expression evaluation construct is removed. The correspondence is formalized by the following encoding function, from ProVerif processes to applied pi processes: The applied pi calculus has a notion of extended processes, which additionally contain the current knowledge of the adversary, represented by substitutions. Extended processes are useful for proving observational equivalence manually, via the notion of labeled bisimilarity [START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF], but they are not necessary for relating the calculus to ProVerif, so we omit them here. We refer to processes as plain processes when we want to stress that they are not extended processes. The applied pi calculus has a sort system, which is similar to the type system of ProVerif. However, in the applied pi calculus, each variable and name comes with its own sort, so processes are not annotated with sorts. We write M : T when M is a term of sort T and P when the process P is well-sorted in the applied pi calculus. If the type of each function symbol in ProVerif is the same as its sort in the applied pi calculus and the type given to each variable and name in the type environment Γ and in the process P matches its sort in the applied pi calculus, then Γ M : T if and only if M : T , and Γ P if and only if [[P ]]. The untyped version of the applied pi calculus can be obtained by giving all terms the sort channel. In this chapter, we assume that either this untyped version of the applied pi calculus is used, or ProVerif is configured to take types into account in the verification of security properties.

[[0]] = 0 [[P | Q]] = [[P ]] | [[Q]] [[!P ]] = ![[P ]] [[new n : T ; P ]] = νn.[[P ]] [[if M = N then P else Q]] = if M = N then [[P ]] else [[Q]]
In contrast to the semantics of ProVerif, the operational semantics of the applied pi calculus is defined by a reduction relation → on processes. To prepare processes for reduction, we use a structural equivalence relation ≡. Formally, the semantics for plain processes is defined as follows (Abadi et al., 2016, §B.2). As usual, a context is a process with a hole. An evaluation context is a context whose hole is not under a replication, a conditional, an input, or an output. Structural equivalence ≡ is the smallest equivalence relation on processes closed by application of evaluation contexts such that Observational equivalence ( ≈) is the largest such relation.

As shown in §B.3, this definition is equivalent to (Abadi et al., 2016, Definition 4.1) for plain processes.

On the ProVerif side, the definition of C ↓ N needs to be adapted in the presence of equations, because the channel N is modulo the equational theory. We have (N pub , N priv ), P ↓ N if and only if there exists out(N , M ); P ∈ P with N = E N and fn(N ) ⊆ N pub , for some terms N , M and process P . We can then relate the equivalence used by ProVerif (Definition 3.6) and the equivalence of the applied pi calculus (Definition 4.1).

Proposition 4.2. Let C and C be valid configurations. If

C ≈ C , then [[C]] ≈ [[C ]].
This proposition shows that, if ProVerif proves an equivalence between processes in the language subset corresponding to the applied pi calculus, then the corresponding applied pi calculus processes are observationally equivalent.

The converse is less important in practice, since ProVerif proves diff-equivalence, which is stronger than ≈. Its proof requires encoding a ProVerif context into the applied pi calculus. In the proof in appendix, we provide this encoding for the core ProVerif language with equations and enriched terms. Pattern-matching and tables can be defined as an encoding in that subset of the ProVerif calculus, so the result extends to them. Phases would be more difficult to encode, though intuitively they do not give more power to the adversary when the considered protocol does not use them. For simplicity, the next proposition considers a ProVerif language without phases. This chapter outlines a number of applications and extensions of ProVerif.

Case studies

ProVerif can successfully prove secrecy and authentication properties for many protocols of the literature [START_REF] Blanchet | Automatic Verification of Correspondences for Security Protocols[END_REF]: no false attack is found in the 19 protocols tested in [START_REF] Blanchet | Automatic Verification of Correspondences for Security Protocols[END_REF]. It can also handle more substantial case studies:

• Abadi and Blanchet, 2005b verify a certified email protocol (Abadi et al., 2002). In this work, correspondence properties are used to prove that the receiver receives the message if and only if the sender has a receipt for the message, with simple manual arguments to take into account that the reception of sent messages is guaranteed. This protocol relies on a secure channel; one of the tested versions includes the SSH transport layer protocol in order to establish this channel.

• Abadi et al., 2007 study the JFK protocol (Just Fast Keying) by [START_REF] Aiello | Just Fast Keying: Key Agreement in a Hostile Internet[END_REF], which was one of the candidates to replace IKE as the key exchange protocol in IPSec. This work combines manual proofs and ProVerif to prove correspondences and equivalences.

• Blanchet and Chaudhuri, 2008 study the secure filesystem Plutus [START_REF] Kallahalla | Plutus: Scalable secure file sharing on untrusted storage[END_REF], discovering and fixing weaknesses of the initial system.

• ProVerif was also used for verifying a certified email web service [START_REF] Lux | WSEmail: Secure Internet Messaging Based on Web Services[END_REF], a certified mailing-list protocol [START_REF] Khurana | Certified Mailing Lists[END_REF]), e-voting protocols [START_REF] Kremer | Analysis of an Electronic Voting Protocol in the Applied Pi Calculus[END_REF]Backes et al., 2008a;[START_REF] Delaune | Verifying Privacy-type Properties of Electronic Voting Protocols[END_REF][START_REF] Cortier | A formal analysis of the Norwegian E-voting protocol[END_REF]), e-auction protocols [START_REF] Dreier | Formal Verification of e-Auction Protocols[END_REF], the ad-hoc routing protocol ARAN (Authenticated Routing for Adhoc Networks) [START_REF] Godskesen | Formal Verification of the ARAN Protocol Using the Applied Pi-calculus[END_REF], zero-knowledge protocols (Backes et al., 2008b;[START_REF] Backes | Symbolic Malleable Zero-Knowledge Proofs[END_REF], the Trusted Platform Module (TPM) [START_REF] Delaune | Formal analysis of protocols based on TPM state registers[END_REF], and the associated Direct Anonymous Attestation protocol (Backes et al., 2008b;[START_REF] Smyth | Formal analysis of privacy in Direct Anonymous Attestation schemes[END_REF], for instance.

ProVerif can also be used for verifying protocols in the computational model, via computational soundness results:

• [START_REF] Canetti | Universally Composable Symbolic Analysis of Mutual Authentication and Key Exchange Protocols[END_REF] show that, for a restricted class of protocols that use only public-key encryption, a proof in the Dolev-Yao model implies security in the computational model, in the universal composability framework.

• Backes et al., 2014 prove computational soundness for the equivalence properties shown by ProVerif. To achieve this result, they take advantage that ProVerif relies on a trace property on biprocesses in order to prove equivalence, so they can leverage computational soundness results for trace properties.

Extensions

Other authors also design and implement extensions of ProVerif:

• [START_REF] Küsters | Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach[END_REF][START_REF] Küsters | Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation[END_REF] extend ProVerif with support for exclusive or, and improve support for Diffie-Hellman key agreements. In the same line, Pankova and Laud, 2012 extend ProVerif with support for bilinear pairings (see also §2.5.1).

• StatVerif [START_REF] Arapinis | StatVerif: Verification of stateful processes[END_REF] [START_REF] Mödersheim | Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases[END_REF], then extended by providing a translation from an extension of the pi calculus [START_REF] Bruni | Set-Pi: Set Membership Pi-Calculus[END_REF].

• Chothia et al., 2015 provide an extension that avoids false attacks in protocols that first commit to a value, then later reveal it. This extension relies on the insertion of phase instructions, to avoid that ProVerif considers the revealed value as available to the adversary from the beginning of the protocol.

ProVerif as back-end

ProVerif is also used as a back-end for building other verification tools:

• [START_REF] Bhargavan | Verifying Policy-Based Security for Web Services[END_REF] use it to build the Web services verification tool TulaFale: Web services are protocols that send XML messages; TulaFale translates them into the input format of ProVerif and uses ProVerif to prove the desired security properties.

• [START_REF] Bhargavan | Verified interoperable implementations of security protocols[END_REF] use ProVerif for verifying implementations of protocols in F# (a functional language of the Microsoft .NET environment): a subset of F# large enough for expressing security protocols is translated into the input format of ProVerif. The TLS protocol [START_REF] Bhargavan | Cryptographically Verified Implementations for TLS[END_REF] and the TPM [START_REF] Mukhamedov | Towards a Verified Reference Implementation of a Trusted Platform Module[END_REF], in particular, were studied using this technique.

• The JavaSPI framework [START_REF] Avalle | The JavaSPI Framework for Security Protocol Implementation[END_REF] allows modeling security protocols in a subset of Java with annotations. These specifications can be verified with ProVerif via a Java-to-ProVerif converter and compiled into Java protocol implementations.

Conclusion

The protocol verifier ProVerif takes as input a description of the protocol to verify in an extension of the pi calculus with cryptography, as well as the security properties to prove. It may return three different answers: the property is true, the property is false with an attack (execution trace of the protocol), or "I do not know" with a derivation at the Horn clause level which does not correspond to a trace of the protocol.

Its main strengths are: it is fully automatic; it supports an unbounded number of sessions of the protocol; it allows the specification of many different cryptographic primitives by rewrite rules or by equations; and it can prove a wide variety of security properties, namely, secrecy, correspondences, and some equivalences.

It still has limitations: it may not terminate and it makes abstractions, which may lead to false attacks. These limitations are unavoidable because the verification of security protocols with an unbounded number of sessions is undecidable. In practice, ProVerif is still efficient and precise in many examples. A further limitation is the class of equational theories that it supports; in particular, it does not support associativity. The class of equivalences that it can prove is also limited. Some extensions, outlined in §5.2, tackle these limitations, and other verifiers make 92 different trade-offs. For instance, Maude-NPA [START_REF] Meadows | The NRL Protocol Analyzer: An Overview[END_REF][START_REF] Escobar | A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties[END_REF] and Tamarin [START_REF] Schmidt | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties[END_REF] support more equational theories, at the cost of a more costly verification or by requiring user intervention.

These limitations suggest areas for future work. For instance, we might improve the precision of the analysis to avoid false attacks, by adding more information into the clauses. We might support more equational theories, by implementing unification and resolution modulo associativity and commutativity. We might improve the support for mutable state, possibly by integrating StatVerif [START_REF] Arapinis | StatVerif: Verification of stateful processes[END_REF] and extending it. The proof of equivalences is also an area in which further research could be done, perhaps by combining manual and automatic proofs. For instance, a proof of observational equivalence could be decomposed into a family of static equivalences [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF] (equivalences between messages), proved automatically by ProVerif, and a manual bisimulation proof. On a more technical side, the user interface of ProVerif could be improved, for instance by displaying attacks graphically. The subsumption tests could be parallelized to improve performance on machines with multiple cores.

Finally, ProVerif verifies specifications of protocols in the symbolic model. One may go further in several directions. First, one may verify specifications of protocols in a more concrete model, such as the computational model, used by cryptographers. Several tools exist for verifying cryptographic primitives and protocols in this model, in particular, CertiCrypt [START_REF] Barthe | Formal Certification of Code-Based Cryptographic Proofs[END_REF][START_REF] Béguelin | Formally Certifying the Security of Digital Signature Schemes[END_REF] and its successor EasyCrypt [START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF]Barthe et al., 2014b), and CryptoVerif (Blanchet, 2008a). They are generally more delicate to use than symbolic protocol verifiers. We plan to modify ProVerif and CryptoVerif to make their input languages compatible, so that the same input file can be used to verify a protocol in both tools, to find attacks or obtain a symbolic proof in ProVerif, or obtain a computational proof in CryptoVerif. Second, instead of verifying specifications, one may verify runnable implementations of protocols. This verification is important because new attacks may appear in the implementation. Some tools for verifying implementations rely on ProVerif as a back-end (see §5.3).

There exist other approaches, by extracting models from implementations for other symbolic [START_REF] O'shea | Using Elyjah to Analyse Java Implementations of Cryptographic Protocols[END_REF] or computational [START_REF] Bhargavan | Crypto-Verifying Protocol Implementations in ML[END_REF][START_REF] Aizatulin | Computational Verification of C Protocol Implementations by Symbolic Execution[END_REF] verifiers, by generating implementations from models by compilation [START_REF] Song | AGVI-Automatic Generation, Verification, and Implementation of Security Protocols[END_REF][START_REF] Milicia | χ-Spaces: Programming Security Protocols[END_REF][START_REF] Pozza | Spi2Java: Automatic cryptographic protocol Java code generation from spi calculus[END_REF][START_REF] Pironti | Provably Correct Java Implementations of Spi Calculus Security Protocols Specifications[END_REF][START_REF] Almeida | Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations[END_REF][START_REF] Cadé | From Computationally-Proved Protocol Specifications to Implementations and Application to SSH[END_REF][START_REF] Cadé | Proved Generation of Implementations from Computationally Secure Protocol Specifications[END_REF], or by direct verification of the implementation, for instance by typing [START_REF] Bengtson | Refinement Types for Secure Implementations[END_REF][START_REF] Bhargavan | Modular Verification of Security Protocol Code by Typing[END_REF][START_REF] Swamy | Secure Distributed Programming with Value-dependent Types[END_REF][START_REF] Fournet | Modular Cryptographic Verification by Typing[END_REF][START_REF] Bhargavan | Implementing TLS with Verified Cryptographic Security[END_REF], by model-checking [START_REF] Chaki | ASPIER: An Automated Framework for Verifying Security Protocol Implementations[END_REF], or by the general-purpose C verifier VCC [START_REF] Dupressoir | Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols[END_REF]. Going even further, one may wish to take into account side-channels attacks, that is, physical attacks, which may rely for instance on timing, power consumption, or fault injection, and are not considered in the computational model. Taking such attacks into account in mechanized verification tools is still at its beginning (Barthe et al., 2014a).

C bad such that C 1 [. . . C k [C 1 ]] → * C bad ↑, since that would imply C 1 [. . . C k [C ]] → C 1 [. . . C k [C 1 ]] → * C bad ↑.
C bad such that C 1 [. . . C k [C ]] → * C bad ↑. Then C[C] = fst(C[C ]), C[C ] = snd(C[C ]), and for all adversarial contexts C 1 [_], . . . , C k [_], there exists no C bad such that C 1 [. . . C k [C[C ]]] → * C bad ↑, so C[C] R C[C ], using C[C ] instead of C .
Therefore, R ⊆ ≈. Let C = (N pub , N priv ), {P 0 }. To show that P 0 satisfies observational equivalence with private names N priv , it suffices to show that fst(C ) ≈ snd(C ), so it suffices to show that fst(C ) R snd(C ). To prove this property, we suppose that there exist adversarial contexts

C 1 [_], . . . , C k [_] such that C 1 [. . . C k [C ]
] → * ↑, and we derive a contradiction. To reach this contradiction, we build an N pub -adversary

Q from the context C 1 [. . . C k [_]], such that (N pub , N priv ), {P 0 , Q} → * ↑, which contradicts the hypothesis of the theorem. Let C i [_] = new n i ; (_ | Q i ) for all i ∈ {1, . . . , k}. We have C k [C ] = ((N pub ∪ fn(Q k )) \ { n k }, α k N priv ∪ { n k }), α k P ∪ {Q k } where α k is a bijective renaming of names in N priv to names not in fn(Q k ) that leaves names in N pub unchanged. Let N pub k+1 = N pub and for all i ∈ {1, . . . , k}, N pub i = (N pub i+1 ∪ fn(Q i )) \ { n i }. So we have C 1 [. . . C k [C ]] = (N pub 1 , α 1 (. . . (α k N priv ∪ { n k ) . . . ) ∪ n 1 ), {α 1 . . . α k P 0 , α 1 . . . α k-1 Q k , . . . , Q 1 } = (N pub 1 , α 1 . . . α k N priv ∪ k i=1 α 1 . . . α i-1 n i ), {α 1 . . . α k P 0 } ∪ {α 1 . . . α i-1 Q i | i ∈ {1, . . . , k} } ,
where α i is a bijective renaming of the names in α

i+1 . . . α k N priv ∪ k j=i+1 α i+1 . . . α j-1 n j to names not in fn(Q i ) that leaves names in N pub i+1 unchanged. So (α 1 . . . α k ) -1 C 1 [. . . C k [C ]] = ((α 1 . . . α k ) -1 N pub 1 , N priv ∪ k i=1 (α i . . . α k ) -1 n i ), {P 0 } ∪ {(α i . . . α k ) -1 Q i | i ∈ {1, . . . , k} } . We write k i=1 P i for P 1 | . . . | P k . Let Q = k i=1 (α i . . . α k ) -1 Q i , { n} = fn(Q ) \ N pub and Q = new n; Q . The process Q is an N pub - adversary. Moreover, let us show that { n} ∩ N priv = ∅. Suppose that a ∈ { n} ∩ N priv . Since N pub ∩ N priv = ∅, for some i ∈ {1, . . . , n}, a ∈ fn((α i . . . α k ) -1 Q i ) ∩ N priv , so α i . . . α k a ∈ fn(Q i ) ∩ α i . . . α k N priv . Since α i . . . α k a ∈ fn(Q i ), α i+1 . . . α k a / ∈ α i+1 . . . α k N priv , since α i renames names in α i+1 . . . α k N priv to names not in fn(Q i ). Therefore, α i . . . α k a / ∈ α i . . . α k N priv . Contradiction. Hence we have proved { n} ∩ N priv = ∅.
Moreover, we have the following property: if (N pub , N priv ), P → * ↑, then (N pub , N priv ), αP → * ↑, where N pub ∩ N priv = ∅, α is a bijective renaming, and fn(αP) ⊆ N pub ∪ N priv . This property is easy to prove by induction on the length of the trace. From this property and C 1 [. . . C k [C ]] → * ↑, we derive

(α 1 . . . α k ) -1 C 1 [. . . C k [C ]] → * ↑ , so (N pub , N priv ), {P 0 , Q} → * (N pub , N priv ∪ { n}), {P 0 } ∪ {(α i . . . α k ) -1 Q i | i ∈ {1, . . . , k} } → * ↑ .
This property contradicts the hypothesis of theorem. This contradiction allows us to conclude the proof.

B Proofs for Chapter 4

These proofs use the notations and definitions of [START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF]. In particular, they use the notion of extended processes A (Abadi et al., 2016, §2.1), with associated domain dom(A) (Abadi et al., 2016, §2.1), structural equivalence ≡ and reduction relation → (Abadi et al., 2016, §2.2); simple contexts [START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF]; partial normal forms, with associated structural equivalence

• ≡ and reduction relation → • (Abadi et al., 2016, §B.2); and the labeled semantics α -→ of (Abadi et al., 2016, §B.2). We show the following property by induction on the cardinal of I, using (Abadi et al., 2016, Lemma B.18(1)): P1. if i∈I P i is closed, α is νx.N x or N (M ) for some ground N and by induction on the cardinal of I. If |I| = 1, then the first case obviously holds. If |I| > 1, then i∈I P i = i∈I 1 P i | i∈I 2 P i for two disjoint non-empty sets I 1 and I 2 such that I = I 1 ∪ I 2 . By (Abadi et al., 2016, Lemma B.21(1)), one of the following four cases holds: ---→ P , and P ≡ νx.(P | A ) for some P , A , x, and ground term N .

In the first two cases, we conclude by induction hypothesis. In the last two cases, we conclude by P1.

By applying P2 to ). In the first case, we obtain Prop(E, P, P red , P ) with P red = {P i }, and in the second case, we obtain Prop(E, P, P red , P ) with P red = {P i , P j }.

As in [START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF], we define the size of processes by induction on the syntax, such that size(!P ) = 1 + 2 × size(P ) and, when P is not a replication, size(P ) is one plus the size of the immediate subprocesses of P . When P = {P 1 , . . . , P n } is a multiset of processes, we define size(P) = size(P 1 ) + • • • + size(P n ). Proof. Let E = (N pub , { a}) and P = {P 1 , . . . , P n }. By Lemma B.2, there exists P red such that Prop(E, P, P red , P ). We proceed by induction on size(P red ).

• Case P red = {P i }, [[P i ]] → P , and P ≡ ν a.(P | j =i [[P j ]]) for some i ∈ {1, . . . , n} and P . By (Abadi et al., 2016, Lemma B.21), we have the following cases:

By definition of [[•]], we have P

i = Q 1 | Q 2 , Q 1 = [[Q 1 ]], and Q 2 = [[Q 2 ]
] for some Q 1 and Q 2 . By (Red Par), E, P → E, P where P = P\{P i }∪{Q 1 , Q 2 }. We have Prop(E, P , P red , P ) with P red = {Q 1 } (case a), P red = {Q 2 } (symmetric of case a), or P red = {Q 1 , Q 2 } (case b and its symmetric), and size(P red ) < size(P red ) in all cases, so we conclude by induction hypothesis. We have P i = !Q and Q = [ [Q ]] for some Q . By (Red Repl) twice, E, P → * E, P where (Abadi et al., 2016, Lemma B.21), one of the following cases holds:

[[P

P = P ∪ {Q , Q }. Since Q | Q → Q , by
(a) Q → Q 1 and Q ≡ Q 1 | Q for some Q 1 , (b) Q N (x) ---→ A, Q νx.N x
-----→ B, and Q ≡ νx.(A | B) for some A, B, x, and ground term N , so we have Prop(E, P , P red , P ) with P red = {Q } (case a) or P red = {Q , Q } (case b), and size(P red ) < size(P red ) in all cases, so we conclude by induction hypothesis. and size(P red ) < size(P red ), so we conclude by induction hypothesis.

[[P

i ]] = if M = N then Q 1 else

[[P

i ]] = !Q, Q N (x)
---→ A , and P ≡ A | !Q for some Q and A . We have P i = !Q and Q = [ [Q ]] for some Q . By (Red Repl), E, P → E, P where P = P ∪ {Q }. We have Prop(E , P , P red , P ) with P red = {Q , P j } and size(P red ) < size(P red ), so we conclude by induction hypothesis.

[[P i

]] = N (x ).Q 1 , N = E N , and P ≡ Q 1 { x / x } for some Q 1 , N , and x . By (Abadi et al., 2016, Lemma B.18) applied to the transition

[[P k ]]) ≡ ν a, x.(Q 1 { x / x } | Q 2 | { M / x } | k =i,j [[P k ]]) P ≡ ν a.(Q 1 { M / x } | Q 2 | k =i,j

Figure 1 . 1 :

 11 Figure 1.1: Structure of ProVerif

Figure 2 . 1 :

 21 Figure 2.1: Syntax of the core language

Figure 2 . 2 :

 22 Figure 2.2: An example of protocol

Figure 2 . 4 :

 24 Figure 2.4: Operational semantics

Figure 2 . 6 :

 26 Figure 2.6: Protocol with certificates

Figure 2 . 7 :

 27 Figure 2.7: ProVerif example with tables

  against this protocol: Message 1. A → C : aenc(sign(k, ssk A ), pk C ) Message 1'. C(A) → B : aenc(sign(k, ssk A ), pk B ) Message 2. B → C(A) : senc(s, k) This attack is illustrated in Figure 3.2. In this attack, A runs the protocol with a dishonest principal C. This principal gets the first message of the protocol aenc(sign(k, ssk A ), pk C ), decrypts it and re-encrypts it under the public key of B. The obtained message aenc(sign(k, ssk A ), pk B ) corresponds exactly to the first message of a session between A and B. Then, C sends this message to B impersonating A. B replies with the secret s, intended for A, encrypted under k. C, having obtained the key k by the first message, can decrypt this message and obtain the secret s. The key sk C corresponds to b 0 [x] in the derivation of Figure 3.1, and is generated by the adversary using Clause (Rn). The key pk C corresponds to pk(b 0 [x]) and is computed by the application of Clause (Rf) by (Rn) F 1 = attacker(b 0 [x]) by (Rf) for pk attacker(pk(b 0 [x])) by (3.3)

Figure 3 . 1 :

 31 Figure 3.1: Derivation of attacker(s[ ])

  x); out(d, c)) preserves the secrecy of s from {d}, but ProVerif cannot prove it, because attacker(s[ ]) is derivable from the clauses (Rl), message(c[ ], s[ ]) and message(c[ ], x) ⇒ attacker(c[ ]), which are in R P 0 ,{d},{s} . (The fact message(d[ ], c[ ]) is equivalent to attacker(c[ ]) since d is a public channel.) The clauses do not take into account that the output out(c, s) must have been executed before the adversary obtains the channel c. (In this example, c is the temporary secret.) This example can also be understood by noticing that the generated clauses are the same as for the process P 0 = new c; (!out(c, s) | !in(c, x); out(

•

  Unification. The transformation unify transforms clauses of the form H ∧ ∀ v, mp = mp ⇒ C as follows. It tries to unify mp and mp . If this unification fails, then the clause becomes H ⇒ C, because ∀ v, mp = mp holds when σ mp = σ mp for all σ.

  NoLoop) and the previous loop disappears because c 2 does not unify with c 1 . The fact attacker(senc((c 2 , minusone(M b )), M k )) is derived, without yielding a loop.

  ssk A : skey; new sk B : skey; let spk A = pk(ssk A ) in let pk B = pk(sk B ) in out(c, spk A ); out(c, pk B ); (P A (spk A , ssk A ) | P B (pk B , sk B , spk A )) P A (spk A , ssk A ) = ! in(c, x pk B : pkey); new k : key; event(e A (spk A , x pk B , k));

  new a : rand; out(c, aenc((a, pk(sk A )), pk(sk B ))); in(c, x : bitstring) B(sk B , sk A ) = in(c, y : bitstring); new b : rand; let (xa : rand, xpk A : pkey) = adec(y, sk B ) in ( * ) if xpk A = pk(sk A ) then out(c, aenc((xa, b, pk(sk B )), pk(sk A ))) else out(c, aenc(b, pk(sk B ))) else out(c, aenc(b, pk(sk B )))

B

  (sk B , sk A ) = in(c, y : bitstring); new b : rand; let (xa : rand, xpk A : pkey) = adec(y, sk B ) in out(c, ifthenelse(equal(xpk A , pk(sk A )), aenc((xa, b, pk(sk B )), pk(sk A )), aenc(b, pk(sk B )))) else out(c, aenc(b, pk(sk B )))

[

  [in(N, x : T ); P ]] = N (x).[[P ]] [[out(N, M ); P ]] = N M .[[P ]]

  P | (Q | R) ≡ (P | Q) | R Par-C P | Q ≡ Q | P Repl !P ≡ P | !P New-0 νn.0 ≡ 0 New-C νn.νn .P ≡ νn .νn.P New-Par P | νn.Q ≡ νn.(P | Q) when n ∈ fn(P ) Rewrite P { M / x } ≡ P { N / x } when M = E N Rules Par-A, Par-C, and Par-0 express that parallel composition is associative, commutative, and has 0 as neutral element. Rule Repl allows one to create new copies of replicated processes (or to fold them back by applying Repl from right to left). The scope extrusion rule New-Par allows one to enlarge the scope of a restriction, for instance to make processes P and Q communicate. Rule Rewrite allows one to rewrite terms modulo the equational theory. The reduction relation → is the smallest relation on processes closed by ≡ and by 3. C[P ] R C[Q] for all closed evaluation contexts C[_].

Proposition 4. 3 .

 3 Let C and C be valid configurations. If [[C]] ≈ [[C ]], then C ≈ C .

2 .

 2 Suppose C R C and C → C 1 . Then there exists a configuration C such that C = fst(C ), C = snd(C ), and for all adversarial contexts C 1 [_], . . . , C k [_], there exists no C bad such that C 1 [. . . C k [C ]] → * C bad ↑. Since C does not diverge, we have C → C 1 and fst(C 1 ) = C 1 for some C 1 , by cases on the reductions. Then C = snd(C ) → snd(C 1 ). Let C 1 = snd(C 1 ). We have C → C 1 and C 1 R C 1 because C 1 = fst(C 1 ), C 1 = snd(C 1 ), and for all adversarial contexts C 1 [_], . . . , C k [_], there exists no

  3. Let C[_] be an adversarial context. Suppose C R C . There exists a configuration C such that C = fst(C ), C = snd(C ), and for all adversarial contexts C 1 [_], . . . , C k [_], there exists no

B. 1 1 Lemma B. 1 .

 111 Proof of Proposition 4.If E, P → E , P , then [[E, P]] ≡ [[E , P ]] or [[E, P]] → [[E , P ]].Proof. By cases on the applied reduction rule.• Case (Red Nil). We have P = P ∪ {0}. When P = ∅, we have [[E, P]] ≡ [[E , P ]] by Par-0. When P = ∅, we have [[E, P]] = [[E , P ]], so we also have [[E, P]] ≡ [[E , P ]]. • Case (Red Par). We have [[E, P]] ≡ [[E , P ]] by Par-A and Par-C.• Case (Red Repl). We have[[E, P]] ≡ [[E , P ]] by Repl.• Case (Red Res). We have[[E, P]] ≡ [[E , P ]] by New-Par.• Case (Red I/O ). Recall that the channels and output message do not contain destructors, so we haveE, P = E, P 0 ∪ { out(N, M ); Q, in(N , x); P } → E, P 0 ∪ { Q, P { M / x } } = E , Pwhere N = E N . By Rewrite, we can replace N with N in the input channel of the encoded process, so we have[[E, P]] → [[E , P ]] by Comm.• Case (Red Cond 1 ). We haveE, P = E, P 0 ∪ {if D then P else Q} → E, P 0 ∪ {P } = E , PwhereD ⇓ M and M = E true. Recall that all conditions are of the form D = (M = N ). Since D ⇓ M and M = E true, we have M = E N . By Rewrite, we can replace N with M in the condition of the encoded process, so we have [[E, P]] → [[E , P ]] by Then. • Case (Red Cond 2 ). We have E, P = E, P 0 ∪ {if D then P else Q} → E, P 0 ∪ {Q} = E , P where D ⇓ M and M = E true. Recall that all conditions are of the form D = (M = N ). Since D ⇓ M and M = E true, we have M = E N . The terms M and N are ground since configurations contain closed processes, so we have [[E, P]] → [[E , P ]] by Else. All cases may use Par-A and Par-C to reorganize parallel compositions and New-C to reorder restrictions. We write n i=1 P i for any parallel composition P 1 | • • • | P n modulo associativity and commutativity. We define the property Prop(E, P, P red , P ) by Prop(E, P, P red , P ) if and only if E = (N pub , { a}), P = {P 1 , . . . , P n }, and 1. P red = {P i }, [[P i ]] → P and P ≡ ν a.(P | j =i [[P j ]]) for some i ∈ {1, . . . , n} and P , or 2. P red = {P i , P j }, [[P i ]] N (x) ---→ P , [[P j ]] νx.N x -----→ A , and P ≡ ν a, x.((P | A ) | k =i,j [[P k ]]) for some i, j ∈ {1, . . . , n}, P , A , x, and ground term N . Intuitively, this property means that [[E, P]] → P by reducing the processes in P red . Lemma B.2. If [[E, P]] → P , then Prop(E, P, P red , P ) for some P red . Proof. Let E = (N pub , { a}) and P = {P 1 , . . . , P n }. We have ν a.([[P 1 ]] | • • • | [[P n ]]) → P . By (Abadi et al., 2016, Lemma B.21(2)), [[P 1 ]] | • • • | [[P n ]] → P and P ≡ ν a.P for some P .

N

  , then there exist i ∈ I and P such that P i α -→ P and P ≡ P | j∈I\{i} P j Next, we show the following property: P2. if i∈I P i is closed and i∈I P i → P , then either there exist i ∈ I and P such that P i → P and P ≡ P | j∈I\{i} [[P j ]], or there exist i, j ∈ I, P , A , x and a ground term N such that P i --→ A , and P ≡ νx.((P | A ) | k∈I\{i,j} P k ).

  n i=1 [[P i ]] → P , either there exist i ∈ {1, . . . , n} and P such that [[P i ]] → P and P ≡ P | j =i [[P j ]], or there exist i, j ∈ {1, . . . , n}, P , A , x, and a ground term N such that [[P i ]] --→ A , and P ≡ νx.((P | A ) | k =i,j [[P k ]]

Lemma B. 3 .

 3 If [[E, P]] → P , then E, P → * E , P and P ≡ [[E , P ]] for some E , P .

1 . 1 ,

 11 [[P i ]] = Q 1 | Q 2 for some Q 1 and Q 2 ,and one of the following cases holds:(a) Q 1 → Q 1 and P ≡ Q 1 | Q 2 for some Q --→ B, and P ≡ νx.(A | B) for some A, B, x, and ground term N , and two symmetric cases obtained by swapping Q 1 and Q 2 .

  i ]] = νn.Q, Q → Q , and P ≡ νn.Q for some n, Q, and Q .We haveP i = new n; Q and Q = [[Q ]] for some Q . By (Red Res), E, P → E , P where E = (N pub , {ã} ∪ {n }), P = P \ {P i } ∪ Q { n / n } , and n / ∈ N pub ∪ {ã}. We have [[Q { n / n }]] = Q{ n / n } → Q { n / n }. (We show by induction on the derivation of Q → Q that, if Q → Q , then σQ → σQwhere σ is a bijective renaming.) So we have Prop(E , P , P red , P ) with P red = Q { n / n } and size(P red ) < size(P red ), so we conclude by induction hypothesis.3. [[Pi ]] = !Q, Q | Q → Q, and P ≡ Q | !Q for some Q and Q .

  Q 2 and either M = E N and P ≡ Q 1 , or M = E N and P ≡ Q 2 , for some M , N , Q 1 , and Q 2 .

  [[P j ]]νx.N x -----→ A , we distinguish cases on [[P j ]]. The first three cases are similar to those for [[P i ]]. The last case is [[P j ]] = N M .Q 2 , N = E N , x / ∈ fv([[P j ]]), and A ≡ Q 2 | { M / x } for some N , M , and Q 2 . We have P i = in(N , x ); Q 1 and Q 1 = [[Q 1 ]] for some Q 1 . We also have P j = out(N , M ); Q 2 and Q 2 = [[Q 2 ]] for some Q 2 . By (Red I/O ), E, P → E, P where P = P \ {P i , P j } ∪ {Q 1 { M / x }, Q 2 } since N = E N . Therefore, [[E, P ]] = ν a.([[Q 1 { M / x }]] | [[Q 2 ]] | k =i,j [[P k ]]) = ν a.(Q 1 { M / x } | Q 2 | k =i,j [[P k ]]) .Moreover, P ≡ ν a, x.((P | A ) | k =i,j

[

  [P k ]]) since x does not occur free in Q 2 and P k for k = i, j since these are closed processes. So P ≡ [[E, P ]]. Proposition 4.1. If C → * C , then [[C]] → * ≡ [[C ]].Conversely, if [[C]] → * P , then C → * C and P ≡ [[C ]] for some C .Proof. This lemma is proved by reducing the context C ! by (Red Par), (Red Res), and (Red Repl). More formally, the proof proceeds by induction on the size of the replication context C ! [_].• If C ! [_] = _, the result is obvious.• If C ! [_] = P | C ! [_], then P = P 1 | P 1 with [[P 1 ]] = P and [[P 1 ]] = C ! [N M .Q]. We have (N pub , N priv ), P = (N pub , N priv ), P 0 ∪ {P 1 | P 1 } → (N pub , N priv ), P 0 ∪ {P 1 , P 1 } by (Red Par).We conclude by induction hypothesis with P 1 instead of P .• The case C ! [_] = C ! [_] | P is similar. • If C ! [_] = νb.C ! [_], then P = new b; P 1 with [[P 1 ]] = C ! [N M .Q].We have(N pub , N priv ), P =(N pub , N priv ), P 0 ∪ {new b; P 1 } →(N pub , N priv ∪ {b }), P 0 ∪ P 1 { b / b } for some b / ∈ N pub ∪ N priv by (Red Res). We have [[P 1 { b / b }]] = C ! { b / b }[N { b / b } M { b / b } .Q{ b / b }] and N { b / b } = E a since a = b because C ! does not bind a.We conclude by induction hypothesis with P 1 { b / b } instead of P .• If C ! [_] = !C ! [_], then P = !P 1 with [[P 1 ]] = C ! [N M .Q]. We have (N pub , N priv ), P = (N pub , N priv ), P 0 ∪ {!P 1 } → (N pub , N priv ), P 0 ∪ {!P1 , P 1 } by (Red Repl). We conclude by induction hypothesis with P 1 instead of P . Lemma B.6. Let E, P be a valid configuration. We have [[E, P]] ⇓ a if and only if E, P → * ↓ a . Proof. Suppose [[E, P]] ⇓ a . We have [[E, P]] → * ≡ C[a M .P ] for some M , P and evaluation context C[_] that does not bind a. By Proposition 4.1, E, P → * E , P and [[E , P ]] ≡ C[a M .P ] for some E , P . By Lemma B.4, [[E , P ]] = C ! [N M .P ] and N = E a for some N , M , P , and replication context C ! that does not bind a. Let E = (N pub , { a}) and P = {P 1 , . . . , P n }. We have [[E , P ]] = ν a.([[P 1 ]] | • • • | [[P n ]]). Then [[P i ]] = C ! [N M .P ] for some replication context C ! that does not Proof. We define a relation R between closed processes by P R Q if and only if P ≡ [[C]], Q ≡ [[C ]], and C ≈ C for some C and C . The relation R is symmetric. Let us show that it satisfies the three conditions of Definition 4.1: 1. If P R Q and P ⇓ a , then P ≡ [[C]], Q ≡ [[C ]], and C ≈ C for some C and C , so [[C]] ⇓ a , so by Lemma B.6, C → * ↓ a . Since C ≈ C , we have C → * ↓ a , so by Lemma B.6, [[C ]] ⇓ a , so Q ⇓ a . 2. Suppose P R Q, P → * P , and P is closed. We have P ≡ [[C]], Q ≡ [[C ]], and C ≈ C for some C and C . IfP = P , then Q → * Q and P R Q with Q = Q. Otherwise, [[C]] → * P , so by Proposition 4.1, C → * C 1 and P ≡ [[C 1 ]] for some C 1 . Hence C → * C 1 and C 1 ≈ C 1 for some C 1 . By Proposition 4.1, [[C ]] → * ≡ [[C 1 ]].If there is no reduction → in this trace, we defineQ = Q. We have Q → * Q . Moreover, P ≡ [[C 1 ]], C 1 ≈ C 1 , and Q = Q ≡ [[C ]] ≡ [[C 1 ]], so P R Q .If there is at least one reduction → in this trace, we defineQ = [[C 1 ]]. We have Q ≡ [[C ]] → * ≡ [[C 1 ]] = Q , so Q → * Q . Moreover, P ≡ [[C 1 ]], C 1 ≈ C 1 and Q = [[C 1 ]], so P R Q .3. Let us finally show that, if P R Q and C[_] is a closed evaluation context, then C[P ] R C[Q]. Up to structural equivalence ≡, the context C[_] can be decomposed into several closed contexts of the form ν n.(_ | Q), so it is enough to show the desired property for such contexts. For such a context C[_], there exists an ad-versarial context C [_] such that [[C [_]]] = C[_]. Since P R Q, we have P ≡ [[C]], Q ≡ [[C ]], and C ≈ C for some C and C . ThenC[P ] ≡ [[C ]][[[C]]] ≡ [[C [C]]] and C[Q] ≡ [[C ]][[[C ]]] ≡ [[C [C ]]] by Lemma B.7. Moreover, C[C] ≈ C [C ], so C[P ] R C[Q].Since ≈ is the largest such relation, we have R ⊆ ≈.If C ≈ C , then [[C]] R [[C ]], so [[C]] ≈ [[C ]].Lemma B.8. If P and Q are closed processes and P ≡ ≈ ≡ Q, then P ≈ Q.some context C i and substitution σ i , or P i = P i }. If (C, C ) ∈ gen(P, P ) and C → C 1 by a reduction that does not reduce processes P i with an empty context C i , then for some C 1 , C → C 1 by the same reduction rule and (C 1 , C 1 ) ∈ gen(P, P ). The symmetric property also holds, and gen(P, P ) is closed under application of adversarial contexts. Because of these properties, gen(P, P ) is a good starting point for building relations used for proving observational equivalence. We prove the following properties: P1. If fail occurs in D, then D ⇓ fail. If fail does not occur in D, then D ⇓ M for some term M . These properties are proved by induction on D. They come from the fact that equality is the only considered destructor, and it evaluates to fail if and only if one of its arguments evaluates to fail. P2. If P 0 is out(D, D ); P , in(D, x : T ); P , or if D then P else Q and fail occurs in D or D , then E, P ∪ {C[P 0 ]} ≈ E, P ∪ {C[0]}. This property is proved by defining a relation R between valid configurations by E, P ∪{σ 1 P 0 , . . . , σ n P 0 } R E, P when ((E, P), (E, P )) ∈ gen(P 0 , 0), and showing that R ∪ R -1 is symmetric and satisfies the three conditions of Definition 3.6. The main argument is that P 0 never reduces. P3. If fail occurs in D, then E, P ∪ {C[let x : T = D in P else Q]} ≈ E, P ∪ {C[Q]}. This property is proved by defining a relation R = gen(let x : T = D in P else Q, Q), and showing that R ∪ R -1 is symmetric and satisfies the three conditions of Definition 3.6. The main argument is that let x : T = D in P else Q reduces to Q since D ⇓ fail by P1. P4. We have E, P ∪ {C[if D then P else Q]} ≈ E, P ∪ {C[if D = true then P else Q]}. This property is proved by defining a relation R = gen(if D then P else Q, if D = true then P else Q), and showing that R ∪ R -1 is symmetric and satisfies the three conditions of Definition 3.6. The main argument is that if D then P else Q and if D = true then P else Q either both reduce to P or both reduce to Q, because D⇓M with M = E true if and only if (D = true)⇓M with M = E true.

  M n , where tuple T 1 ,...,Tn is a constructor that takes arguments of types T 1 , . . . , T n and returns a result of type bitstring, that is, the type declaration of tuple T

1 ,...,Tn is tuple T 1 ,...,Tn (T 1 , . . . , T n ) : bitstring. (We often abbreviate tuple T 1 ,...,Tn (M 1 , . . . , M n ) to (M 1 , . . . , M n ).)

The n projections are destructors ith T 1 ,...,Tn for i ∈ {1, . . . , n}, defined by ith T 1 ,...,Tn (tuple T 1 ,...,Tn (x 1 , . . . , x n )) → x i .

  ssk A : skey; new sk B : skey; let spk A = pk(ssk A ) in

	let pk B = pk(sk B ) in out(c, spk A ); out(c, pk B );
	(P A (ssk A , pk B ) | P B (sk B , spk A ))
	P A (ssk A , pk B ) = ! new k : key;
	out(c, aenc(sign(k2b(k), ssk A ), pk B ));
	in(c, x : bitstring); let z = sdec(x, k) in 0

  where the substitution σ collects instantiations of Dp obtained by unification and the formula φ collects the side conditions that express that certain rewrite rules of destructors do not apply. More formally, the relation Dp ⇓ (mp, σ, φ) specifies how instances of Dp evaluate: if Dp⇓ (mp, σ, φ), then for any substitution σ such that σ φ holds, we have σ σDp ⇓σ mp. There may be several (mp, σ, φ) such that Dp ⇓ (mp, σ, φ) in case several instances of Dp reduce in a different way. This relation is defined as follows:

		expression
	mp	may-fail pattern
	h(Dp 1 , . . . , Dp n )	function application
	Evaluation of open pattern expressions is defined as a relation Dp ⇓
	(mp, σ, φ),

  These clauses are of the form message(p 1 , p 1 ) ∧ . . . ∧ message(p n , p n ) ∧ φ ⇒ message(p, p ) when the process P 0 sends message p on channel p after receiving messages p 1 , . . . , p n on channels p 1 , . . . , p n respectively, provided the disequalities in φ hold. If c ∈ N

pub , ProVerif replaces all occurrences of message(c[ ], p) with attacker(p) in the clauses. Indeed, these facts are equivalent by the clauses (Rl) and (Rs).

  2.3. Let N pub = {c} be the initial knowledge of the adversary and N priv = {s} be the private free names. For the process P 0 of Example 2.2, the clauses [[P 0 ]]ρ 0 ∅∅ are, after replacing message(c[ ], p) ) correspond to the two outputs in P 0 itself, out(c, pk A ); out(c, pk B ). They express that the adversary has the public keys. Clause (3.3) corresponds to the output in P A : if the adversary has x pk B , it can send it to the first input of P A , and P A then replies with the message aenc(sign(k[i, x pk B ], ssk A [ ]), x pk B ), which the adversary intercepts. The second input of P A and the subsequent expression evaluation do not generate any clause, since no message is sent. Finally, Clause (3.4) corresponds to the output in P B : if the adversary obtains a message of the form aenc(sign(x m , ssk A [ ]), pk(sk B [ ])), it can send this message to P B . The decryption and signature verification succeed, so P B replies by sending s encrypted under x m , which the adversary intercepts.

	attacker(senc(s[ ], x m ))	(3.4)
	Clauses (3.1) and (3.2
	Example 3.2. with attacker(p):
	attacker(pk(ssk A [ ]))	(3.1)
	attacker(pk(sk B [ ]))	(3.2)

attacker(x pk

B ) ⇒ attacker(aenc(sign(k[i, x pk B ], ssk A [ ]), x pk B )) (3.3) attacker(aenc(sign(x m , ssk A [ ]), pk(sk B [ ]))) ⇒

  and only if there exists a substitution σ such that σH 1 ⊆ H 2 (multiset inclusion) and σC 1 = C 2 . All clauses subsumed by another clause of the current clause set are removed.

  is an extension of ProVerif with support for mutable state. It allows global mutable memory cells, which are encoded into Horn clauses by adding their current contents to the arguments of the predicates attacker and message. • Mödersheim, 2010; Bruni et al., 2015 provide another extension of ProVerif with support for state. They allow sets (such as databases of keys or access rights) where revocation is possible, so that the set of true facts does not increase monotonically. To achieve this result, they rely on a new abstraction of sets into terms in Horn clauses. This approach was first proposed at the Horn clause level

•

  [START_REF] Aizatulin | Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution[END_REF] use symbolic execution in order to extract ProVerif models from pre-existing protocol implementations in C. This technique currently analyzes a single execution path of the protocol, so it is limited to protocols without branching. An earlier related approach is that of Goubault-Larrecq and Parrennes, 2005: they also use the Horn clause method for analyzing implementations of protocols written in C. However, they translate protocols into clauses of the H 1 class and use the H 1 prover by Goubault-Larrecq, 2005 rather than ProVerif to prove secrecy properties of the protocol.

•

[START_REF] Bansal | Discovering Concrete Attacks on Website Authorization by Formal Analysis[END_REF][START_REF] Bansal | Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage[END_REF]

build the Web-spi library, which allows them to model web security mechanisms and protocols and verify them using ProVerif.

  1. i∈I 1 P i → P and P ≡ P | i∈I 2 P i for some P ; 2. i∈I 2 P i → P and P ≡ P | i∈I 1 P i for some P ; ) for some P , A , x, and ground term N ; 4. i∈I 1 P i νx.N x -----→ A , i∈I 2 P i N (x)

3. i∈I

1 P i N (x) ---→ P , i∈I 2 P i νx.N x

-----→ A , and P ≡ νx.(P | A

Sometimes, one may also overapproximate the capabilities of the adversary in the symbolic model.

(x : T ) ∈ Γ Γ x : T (a : T ) ∈ Γ Γ a : T f (T 1 , . . . , T n ) : T Γ M 1 : T 1 . . . Γ M n : T n Γ f (M 1 , . . . , M n ) : T h(T 1 , . . . , T n ) : T Γ D 1 : T 1 . . . Γ D n : T n Γ h(D 1 , . . . , D n ) : T Γ fail : T Γ N : channel Γ M : T Γ P Γ out(N, M ); P Γ N : channel Γ, x : T P Γ in(N, x : T ); P Γ 0 Γ P Γ Q Γ P | Q Γ P Γ !PΓ, a : T P Γ new a : T ; P

In(Blanchet,

2009), the environment E is simply a set of names, corresponding to N pub ∪ Npriv. Indeed, the distinction between public and private names is not essential for trace properties. It is useful for treating equivalences in §3.4.

The rewrite rules like sdec(x, y) → sdec(x, y) are necessary so that sdec always succeeds when its arguments succeed. Thanks to this rule, the evaluation of sdec(M, N ) succeeds and leaves this term unchanged when M is not of the form senc(M , N ).

3 More precisely, the disequality tests in D ⇓ U and (Red Cond 2 ) must still be performed modulo the equational theory, even in the calculus with rewrite rules. The impact on the performance of the resolution algorithm is limited because disequalities are less common than other facts and, when there are several unifiers modulo the equational theory in a disequality, that leads to several disequalities in a single clause, not to several clauses.

Acknowledgments

This survey borrows material from previous surveys (Blanchet, 2012b;Blanchet, 2014) and from my habilitation thesis (Blanchet, 2008b).

Much research on ProVerif has been done with co-authors: in alphabetical order, Martín Abadi, Xavier Allamigeon, Vincent Cheval, Cédric Fournet, Andreas Podelski, and Ben Smyth. I would like to thank them for their contributions. I also thank Ben Smyth for helpful comments on a draft of this survey.

application of evaluation contexts such that:

for any ground terms M and N such that M = E N Rule Comm performs communication between two processes. Rules Then and Else define the semantics of conditionals. This semantics is superficially very different from the semantics of ProVerif. However, we can still relate the two semantics formally. The encoding can be extended to configurations as follows:

[[(N pub , N priv ), P]] = ν a.([

where N priv = { a} and P = {P 1 , . . . , P n }. In particular, [[(N pub , N priv ), P]] = ν a.0 when P = ∅. The encoding of configurations is unique modulo ≡. More formally, [[(N pub , N priv ), P]] is a set of processes, containing all processes of the form ν a. Conversely, if [ [C]] → * P , then C → * C and P ≡ [ [C ]] for some C .

Next, we define observational equivalence in the applied pi calculus. We write P ⇓ a when P can send a message on name a, that is, when

Appendices

A

Proof of Theorem 3.5

Theorem 3.5. Let P 0 be a closed biprocess and N priv be a set of names.

If P 0 satisfies diff-equivalence with private names N priv , then P 0 satisfies observational equivalence with private names N priv . [C ] does not diverge, so fst(N 0 ) = fst(a) if and only if snd(N 0 ) = snd(a). Therefore, snd(N 0 ) = a, so C = snd(C ) = (N pub , N priv ), snd(P 0 ) with out(a, snd(M 0 )); snd(P 0 ) ∈ snd(P 0 ), so C ↓ a .

Proof

We have

and

If M = E N , then by (Red Cond 1 ), E, P → E, P where

) for some i, j ∈ {1, . . . , n}, P , A , x, and ground term N . By (Abadi et al., 2016, Lemma B.18) applied to the transition [

---→ P , we have the following cases: andA .

We have

] for some Q 1 and Q 2 . By (Red Par), E, P → E, P where P = P \ {P i } ∪ {Q 1 , Q 2 }. We have Prop(E, P , P red , P ) with P red = {Q 1 , P j } or P red = {Q 2 , P j } and size(P red ) < size(P red ), so we conclude by induction hypothesis.

[[P

---→ A , and P ≡ νn.A for some Q, A , and n that does not occur in N (x).

We have

----→ σA where σ is a bijective renaming.) So we have Prop(E , P , P red , P ) with

Proof. The first point is proved by induction on the number of steps of C → * C , using Lemma B.1. The second point is proved by induction on the number of steps of [ [C]] → * P , using Lemma B.3. Propositions 4.2 and4.3 Let replication contexts C ! [_] be plain contexts generated by the following grammar:

B.2 Proof of

We use replication contexts to characterize P ⇓ a without using structural equivalence, by the following lemma: bind a and P i ∈ P , and a / ∈ a. Since N = E a, we have a ∈ fn(N ). (Otherwise, we would have N { N / a } = E a{ N / a } for all N , since equality is preserved by substitution of terms for names because the equations do not contain names, so N = E N , which contradicts the assumption that the equational theory is non trivial.) So a ∈ fn(P i ), so a ∈ fn(P ). Since fn(P ) ⊆ N pub ∪ { a} and a / ∈ a, we have a ∈ N pub . By Lemma B.5, E , P → * E , P , N M .P = [ [Q]], and N = E a for some E = (N pub , N priv ), P , Q ∈ P , N , M , and P . Therefore Q = out(N , M ); Q ∈ P for some Q , N = E a, and a ∈ N pub , so E , P ↓ a , so E, P → * ↓ a .

Conversely, suppose E, P → * ↓ a . We have E, P → * E , P and E , P ↓ a for some E , P . So we have E = (N pub , { a}), a ∈ N pub , out(N, M ); Q ∈ P , and N = E a for some N pub , a, N , M , and

We define the encoding of contexts as the encoding of processes, with additionally [[_]] = _.

Lemma B.7. Let C[_] be an adversarial context. We have [[C [C] Proof. Since the contexts in Definition 3.6 may be any ProVerif adversarial contexts, we need to encode all ProVerif constructs into the subset already encoded by [[•]]. In this proof, we consider the core ProVerif language with equations and enriched terms. Pattern-matching and tables can be defined as an encoding into that subset, so the result extends to them. We do not consider phases. We define this encoding as follows: [P ] PV is the process obtained from P by performing the following replacements:

We define [C] PV similarly, and [E, P] PV = E, {[P ] PV | P ∈ P}.

We show that the encoding preserves observational equivalence. In the next properties, C denotes any context (any process with a hole, not only an adversarial context). We define gen(P, P ) = {((E, {P 1 , . . . , P n }), (E, {P 1 , . . . , P n })) | (E, {P 1 , . . . , P n }) and (E, {P 1 , . . . , P n }) are valid configurations, for all i ≤ n, P i = C i [σ i P ] and

Since ≈ is the largest such relation, we have

B.3 Relating definitions of observational equivalence

Let ≈ π be observational equivalence as defined in (Abadi et al., 2016, Definition 4.1). Let us show that, for plain processes, ≈ π is equal to ≈, defined in Definition 4.1. Lemma B.10. Let P be a plain process. If P ≡ A, then pnf(A) is a plain process and P ≡ pnf(A). If P → A, then pnf(A) is a plain process and P → pnf(A).

Proof. Suppose P ≡ A. By (Abadi et al., 2016, Lemma B.5), pnf(P )

• ≡ pnf(A). We have pnf(P ) = 0 | P ≡ P and dom(pnf(P )) = ∅. By Lemma B.9, we conclude that dom(pnf(A)) = ∅ and pnf(P ) ≡ pnf(A), so pnf(A) is a plain process and P ≡ pnf(A).

Suppose P → A. By (Abadi et al., 2016, Lemma B.8), pnf(P ) → • pnf(A). We have pnf(P ) = 0 | P ≡ P and dom(pnf(P )) = ∅. By Lemma B.9, we conclude that dom(pnf(A)) = ∅ and pnf(P ) → pnf(A), so pnf(A) is a plain process and P → pnf(A).

Lemma B.11. Let P and Q be closed processes and σ be a bijective renaming.

Proof. By induction on the derivations. Lemma B.12. Let P and Q be closed processes and σ be a bijective renaming.

The relation R is symmetric. Let us show that it satisfies the three properties of Definition 4.1:

Proofs for Chapter 4

Proof. The relation ≈ π restricted to closed plain processes is symmetric. Let us show that it satisfies the three conditions of Definition 4.1:

1. If P ≈ π Q and P ⇓ a , then by (Abadi et al., 2016, Lemmas B.9 and B.7

) is an evaluation context that does not bind a, so B ⇓ a . Since ≈ π is the largest such relation, R ⊆ ≈ π . In particular, if P ≈ Q, then P R Q, so P ≈ π Q.