<figure><img src="image_1.png" /></figure>

HAL
open science

# Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif

Bruno Blanchet

<figure><img src="image_2.png" /></figure>

## ► To cite this version:

Bruno Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends® in Privacy and Security, 2016, 1 (1-2), pp.1 - 135. 10.1561/3300000004. hal-01423760

HAL Id: hal-01423760

https://inria.hal.science/hal-01423760

Submitted on 31 Dec 2016

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.
Modeling and Verifying Security
Protocols with the Applied Pi
Calculus and ProVerif

**Suggested Citation:** Bruno Blanchet (2016), "Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif", : Vol. 1, No. 1, pp 1–135. DOI: 10.1561/3300000004.

Bruno Blanchet

INRIA Paris, France

Bruno.Blanchet@inria.fr

<footnote>This article may be used only for the purpose of research, teaching, and/or private study. Commercial use or systematic downloading (by robots or other automatic processes) is prohibited without explicit Publisher approval.</footnote>
# Contents

<table><tr><td>1</td><td>Introduction</td><td>2</td></tr><tr><td>1.1</td><td>Verifying security protocols</td><td>2</td></tr><tr><td>1.2</td><td>Structure of ProVerif</td><td>10</td></tr><tr><td>1.3</td><td>Comparison with previous surveys</td><td>11</td></tr><tr><td>2</td><td>The Protocol Specification Language</td><td>12</td></tr><tr><td>2.1</td><td>Core language: syntax and informal semantics</td><td>12</td></tr><tr><td>2.2</td><td>An example of protocol</td><td>20</td></tr><tr><td>2.3</td><td>Core language: type system</td><td>23</td></tr><tr><td>2.4</td><td>Core language: formal semantics</td><td>24</td></tr><tr><td>2.5</td><td>Extensions</td><td>29</td></tr><tr><td>3</td><td>Verifying Security Properties</td><td>42</td></tr><tr><td>3.1</td><td>Adversary</td><td>42</td></tr><tr><td>3.2</td><td>Secrecy</td><td>43</td></tr><tr><td>3.3</td><td>Correspondences</td><td>64</td></tr><tr><td>3.4</td><td>Equivalences</td><td>70</td></tr><tr><td>3.5</td><td>Usage heuristics</td><td>81</td></tr><tr><td>4</td><td>Link with the Applied Pi Calculus</td><td>83</td></tr></table>
<table><tr><td>5 Applications</td><td>88</td></tr><tr><td>5.1 Case studies</td><td>88</td></tr><tr><td>5.2 Extensions</td><td>89</td></tr><tr><td>5.3 ProVerif as back-end</td><td>90</td></tr><tr><td>6 Conclusion</td><td>92</td></tr><tr><td>Acknowledgments</td><td>95</td></tr><tr><td>Appendices</td><td>96</td></tr><tr><td>A Proof of Theorem 3.5</td><td>97</td></tr><tr><td>B Proofs for Chapter 4</td><td>100</td></tr><tr><td>B.1 Proof of Proposition 4.1</td><td>100</td></tr><tr><td>B.2 Proof of Propositions 4.2 and 4.3</td><td>107</td></tr><tr><td>B.3 Relating definitions of observational equivalence</td><td>114</td></tr><tr><td>References</td><td>118</td></tr></table>
# Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif

Bruno Blanchet¹

¹INRIA Paris, France; Bruno.Blanchet@inria.fr

## ABSTRACT

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

Introduction

1.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 net-
works, 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 Lowe, 1996 against the Needham-Schroeder
public-key protocol (Needham and Schroeder, 1978) 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 (Beurdouche et al., 2015; Adrian et al.,
2015). Moreover, security errors cannot be detected by functional test-
ing, 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.
1.1.1 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 Schroeder, 1978 and Dolev and Yao, 1983, 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 (Armando et al., 2005), FDR (Lowe, 1996), Scyther (Cremers, 2008), Tamarin (Schmidt et al., 2012), 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.<fnref n="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

<footnote n="1">¹Sometimes, one may also overapproximate the capabilities of the adversary in the symbolic model.</footnote>
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 Abadi and Rogaway, 2002. This work
triggered much research in this direction; we refer to (Cortier et al.,
2011) 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 proto-
cols 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.

1.1.2 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 (Delaune *et al.*, 2009), 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) (Abadi and Gordon, 1999; Abadi and Gordon, 1998; Abadi and Fournet, 2001). 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 (Abadi, 1999; Blanchet, 2004). 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 (Cortier *et al.*, 2007), 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 (Woo and Lam, 1993; Lowe, 1997), 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.

**1.1.3 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 (Lowe, 1996) and by SATMC (Armando et al., 2014), 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 (Rusinowitch and Turuani, 2003). 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 (Turuani, 2006) or extensions of model checking as in OFMC (Basin et al., 2005).

* When the number of executions of the protocol is not bounded, the problem is undecidable (Durgin et al., 2004) 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 (Paulson, 1998), which is an interactive theorem prover, Tamarin (Schmidt et al., 2012), which just requires the user to give a few lemmas to help the tool, or Cryptyc (Gordon and Jeffrey, 2004), 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 (Monniaux, 2003; Boichut et al., 2006).

- One can allow non-termination, as in Maude-NPA (Meadows, 1996; Escobar et al., 2006).

The symbolic protocol verifier ProVerif represents protocols by Horn clauses, in the line of ideas by Weidenbach, 1999: Horn clauses are first order logical formulas, of the form $F_1 \wedge \dots \wedge F_n \Rightarrow F$, where $F_1, \dots, 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 (Armando et al., 2005) is a platform that offers four different protocol verification back-ends: SATMC (Armando et al., 2014) for bounded attack depth (which implies bounded sessions and messages), Cl-AtSe (Turuani, 2006) and OFMC (Basin et al., 2005; Mödersheim and Viganò, 2009) for bounded sessions, and TA4SP (Boichut et al., 2006) 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 tree-automata 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 Delaune, 2005).
which excludes associativity. AVISPA focuses on trace properties, while
ProVerif can also verify some equivalence properties.

Maude-NPA (Meadows, 1996; Escobar et al., 2006) relies on narrow-
ing in rewrite systems. It is fully automatic and supports an unbounded
number of sessions, but in contrast to ProVerif, it does not make any
abstraction. Hence, it is sound and complete, but may not terminate. It
supports cryptographic primitives defined by convergent rewrite rules
plus associativity and commutativity (Escobar et al., 2007), as well as
homomorphic encryption (Escobar et al., 2011), while ProVerif does not
support associativity nor homomorphic encryption. It initially focused
on reachability properties and was recently extended to prove some
equivalences (Santiago et al., 2014), using the same idea as ProVerif
(see §3.4).

Scyther (Cremers, 2008) is fully automatic, always terminates, and
can provide three different results: verification for an unbounded number
of sessions, attack, or verification for a bounded number of sessions.
It supports only a fixed set of cryptographic primitives (symmetric
and asymmetric encryption and signatures). It proves secrecy and
authentication properties. A version named scyther-proof generates
Isabelle proofs of security of the verified protocols (Meier et al., 2010).

Tamarin (Schmidt *et al.*, 2012) verifies protocols for an unbounded
number of sessions, but often relies on the user to provide some lemmas
in order to guide the proof. It initially proved trace properties expressed
in temporal first-order logic, and was recently extended to prove some
equivalences (Basin *et al.*, 2015), using the same idea as ProVerif. It
supports cryptographic primitives defined by subterm convergent equa-
tions, Diffie-Hellman exponentiation, bilinear pairings, and associative
and commutative operators (Schmidt *et al.*, 2014). It also supports
mutable state and loops; the lemmas provided by the user basically give
loop invariants. Protocols in Tamarin are specified as multiset rewriting
systems; Kremer and Künnemann, 2014 wrote a translator from an
extension of the applied pi calculus with state.

The rest of this survey focuses on ProVerif. We refer the reader
to (Blanchet, 2012b) for a more complete survey of security protocol
verification.
<figure><img src="image_3.png" /><figcaption>Figure 1.1: Structure of ProVerif</figcaption></figure>

## 1.2 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 (Abadi and Fournet, 2001; Abadi et al., 2016) 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 (Abadi and Fournet, 2001; Abadi et al., 2016). Finally, Chapter 5 summarizes some applications of ProVerif and Chapter 6 concludes.

## 1.3 Comparison with previous surveys

Previous surveys on ProVerif (Blanchet, 2011; Blanchet, 2014) 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 (Blanchet, 2009), and equivalences Blanchet et al., 2008. Our habilitation thesis (Blanchet, 2008b), 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 (Cheval and Blanchet, 2013), 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; Blanchet, 2009; Blanchet, 2014), with some features added: extended destructors (Cheval and Blanchet, 2013), support for equations and phases (Blanchet et al., 2008), enriched terms, pattern-matching, and table of keys (Blanchet et al., 2016).

## 2.1 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
<table><caption>**Figure 2.1:** Syntax of the core language</caption><tr><td>M, N ::=</td><td>terms</td></tr><tr><td>x, y, z</td><td>variable</td></tr><tr><td>a, b, c, k, s</td><td>name</td></tr><tr><td>f(M<sub>1</sub>, ..., M<sub>n</sub>)</td><td>constructor application</td></tr><tr><td>D ::=</td><td>expressions</td></tr><tr><td>M</td><td>term</td></tr><tr><td>h(D<sub>1</sub>, ..., D<sub>n</sub>)</td><td>function application</td></tr><tr><td>fail</td><td>failure</td></tr><tr><td>P, Q ::=</td><td>processes</td></tr><tr><td>0</td><td>nil</td></tr><tr><td>out(N, M); P</td><td>output</td></tr><tr><td>in(N, x : T); P</td><td>input</td></tr><tr><td>P | Q</td><td>parallel composition</td></tr><tr><td>!P</td><td>replication</td></tr><tr><td>new a : T; P</td><td>restriction</td></tr><tr><td>let x : T = D in P else Q</td><td>expression evaluation</td></tr><tr><td>if M then P else Q</td><td>conditional</td></tr></table>

attacks (Heather *et al.*, 2000). 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.

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*<sub>1</sub>, ..., *T*<sub>*n*</sub>) : *T* means that the function *h* takes *n* arguments of types *T*<sub>1</sub>, ..., *T*<sub>*n*</sub> 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, \dots, 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, \dots, U_n) \rightarrow U$ where $U_1, \dots, 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, \dots, U_n, U$ do not contain names, and the variables of `U` also occur in $U_1, \dots, U_n$. The types of $U_1, \dots, 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, \dots, D_n)$, we first evaluate $D_1, \dots, D_n$, which yields $U_1, \dots, 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, \dots, U'_n) \rightarrow U'$ in `def(g)`. If there exists a substitution $\sigma$ such that $\sigma U'_i = U_i$ for all $i \in \{1, \dots, n\}$, then this rewrite rule applies and $g(D_1, \dots, D_n)$ evaluates to $\sigma 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, \dots, 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:

* `tuple<`$T_1, \dots, T_n$`(`$M_1, \dots, M_n$`) is the tuple of the terms $M_1, \dots, M_n$, where `tuple<`$T_1, \dots, T_n$`` is a constructor that takes arguments of types $T_1, \dots, T_n$ and returns a result of type `bitstring`, that is, the type declaration of `tuple<`$T_1, \dots, T_n$`` is `tuple<`$T_1, \dots, T_n$`(`$T_1, \dots, T_n$`) : `bitstring`. (We often abbreviate `tuple<`$T_1, \dots, T_n$`(`$M_1, \dots, M_n$`) to (`$M_1, \dots, M_n$`).) The `n` projections are destructors `ith<`$T_1, \dots, T_n$` for $i \in \{1, \dots, n\}$,
defined by

$$ ith_{T_1,...,T_n}(tuple_{T_1,...,T_n}(x_1,...,x_n)) \to x_i . $$

* 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) \to x . $$

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) \to x . \qquad (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) \to x . \qquad (2.2) $$

For protocols that do not test equality of ciphertexts, for secrecy and authentication, one can use the simpler, deterministic model of encryption (Cortier et al., 2006). 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.

* For digital signatures, we may use two constructors pk(skey) : pkey as above and sign(bitstring, skey) : bitstring, where sign(M, N) represents the message M signed with the signature key N. The corresponding destructors check(bitstring, pkey) : bitstring and getmess(bitstring) : bitstring are defined by:

$$ \check{check}(\text{sign}(x, y), \text{pk}(y)) \rightarrow x, \qquad (2.3) $$

$$ \check{getmess}(\text{sign}(x, y)) \rightarrow x. \qquad (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:

$$ \begin{aligned} \text{equal}(x, x) &\rightarrow \text{true}, \\ \text{equal}(x, y) &\rightarrow \text{false}. \end{aligned} \qquad (2.5) $$

The second rewrite rule applies only when the first one does not apply, that is, when $x \neq 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:

$$
\texttt{and}(\texttt{true}, u) \rightarrow u,
$$

$$
\texttt{and}(x, u) \rightarrow \texttt{false}.
$$

This destructor returns its second argument when its first argu-
ment 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 argu-
ment 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:

$$
\texttt{ifthenelse}(\texttt{true}, u, u') \rightarrow u,
$$

$$
\texttt{ifthenelse}(x, u, u') \rightarrow u'.
$$

This destructor returns its second argument when its first argu-
ment 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 evalu-
ated 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)) \rightarrow 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 (Milner et al., 1992).

* 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 \mid 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) \subseteq N_{pub} \cup 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, \dots, M_n/x_n\}$ for the substitution that replaces $x_1, \dots, x_n$ with $M_1, \dots, M_n$, respectively. When `D` is some term, expression, or process, we write $D\{M_1/x_1, \dots, M_n/x_n\}$ for the result of applying this substitution to `D`, but we write $\sigma D$ when the substitution is
simply denoted $\sigma$. 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 (Abadi and Fournet, 2001; Abadi et al., 2016). 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 error-handling 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.

## 2.2 An example of protocol

We use as a running example a simplified version of the Denning-Sacco key distribution protocol (Denning and Sacco, 1981), omitting certificates and timestamps:

Message 1. $A \to B : aenc(\text{sign}(k2b(k), ssk_A), pk_B)$

Message 2. $B \to 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
<figure><img src="image_4.png" /><figcaption>**Figure 2.2:** An example of protocol</figcaption></figure>

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 (Abadi and Needham, 1996), so $s$ will not remain secret. The attack is explained in Example 3.2.)

This protocol can be encoded by the following process:

$$ 
\begin{align*}
P_0 &= \text{new ssk}_A : \text{skey}; \text{new sk}_B : \text{skey}; \text{let spk}_A = \text{pk}(\text{ssk}_A) \text{ in} \\
    &\quad \text{let pk}_B = \text{pk}(\text{sk}_B) \text{ in out}(c, \text{spk}_A); \text{out}(c, \text{pk}_B); \\
    &\quad (P_A(\text{ssk}_A, \text{pk}_B) | P_B(\text{sk}_B, \text{spk}_A))
\end{align*}
$$

$$ P_A(\text{ssk}_A, \text{pk}_B) = ! \text{ new } k : \text{key}; \\ \text{out}(c, \text{aenc}(\text{sign}(k2b(k), \text{ssk}_A), \text{pk}_B)); \\ \text{in}(c, x : \text{bitstring}); \text{let } z = \text{sdec}(x, k) \text{ in } 0 $$

$$ P_B(\text{sk}_B, \text{spk}_A) = ! \text{ in}(c, y : \text{bitstring}); \text{let } y' = \text{adec}(y, \text{sk}_B) \text{ in} \\ \text{let } x_k = \text{b2k}(\text{check}(y', \text{spk}_A)) \text{ in } \text{out}(c, \text{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) = ! \left( \begin{array}{l} \texttt{in}(c, x_{pk_B} : \texttt{pkey}); \texttt{new} \ k : \texttt{key}; \\ \texttt{out}(c, \texttt{aenc}(\texttt{sign}(k2b(k), ssk_A), x_{pk_B})); \\ \texttt{in}(c, x : \texttt{bitstring}); \text{let } z = \texttt{sdec}(x, k) \text{ in } \mathbf{0} \end{array} \right)$$

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.

### 2.3 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 $\Gamma$ 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 $\Gamma \vdash M : T$ means that the term $M$ is well-typed of type $T$ in the type environment $\Gamma$; the judgment $\Gamma \vdash D : T$ means that the expression $D$ is well-typed of type $T$ in the type environment $\Gamma$; and the judgment $\Gamma \vdash P$ means that the process $P$ is well-typed in the type environment $\Gamma$.

The typing rules are straightforward. The type of variables and names is obtained from the type environment $\Gamma$. Function applications $h(D_1, \dots, 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, \dots, 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 $\Gamma = c : channel, s : bitstring$, that is, $\Gamma \vdash 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 = \begin{array}{l} \texttt{new ssk}_A; \texttt{new sk}_B; \text{let spk}_A = \text{pk(ssk}_A) \text{ in let pk}_B = \text{pk(sk}_B) \text{ in} \\ \text{out}(c, \text{spk}_A); \text{out}(c, \text{pk}_B); (P_A(ssk_A, \text{pk}_B) | P_B(sk_B, \text{spk}_A)) \end{array}$$
<figure><img src="image_5.png" /><figcaption>**Figure 2.3: Type system**</figcaption></figure>

$$ P_A(ssk_A, pk_B) = ! \text{in}(c, x_{pk_B}); \text{new } k; $$
$$ \text{out}(c, \text{aenc}(\text{sign}(k, ssk_A), x_{pk_B})); \text{in}(c, x); \text{let } z = \text{sdec}(x, k) \text{ in } 0 $$
$$ P_B(sk_B, spk_A) = ! \text{in}(c, y); \text{let } y' = \text{adec}(y, sk_B) \text{ in} $$
$$ \text{let } x_k = \text{check}(y', spk_A) \text{ in } \text{out}(c, \text{senc}(s, x_k)) $$

ProVerif verifies this process when it is given the process of §2.2.

## 2.4 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 \Downarrow M$

fail $\Downarrow$ fail

$h(D_1, \dots, D_n) \Downarrow \sigma U'_j$ if and only if

$D_1 \Downarrow U_1, \dots, D_n \Downarrow U_n,$

def($h$) consists of the rewrite rules

$h(U'_{i,1}, \dots, U'_{i,n}) \to U'_i$ for $i \in \{1, \dots, k\},$

$\sigma U'_{j,1} = U_1, \dots, \sigma U'_{j,n} = U_n,$ and

for all $i \le j$, for all $\sigma'$, $\sigma' U'_{i,1} \ne U_1, \dots, \sigma' U'_{i,n} \ne U_n$.

$E, \mathcal{P} \cup \{0\} \to E, \mathcal{P}$ (Red Nil)

$E, \mathcal{P} \cup \{P \mid Q\} \to E, \mathcal{P} \cup \{P, Q\}$ (Red Par)

$E, \mathcal{P} \cup \{!P\} \to E, \mathcal{P} \cup \{P, !P\}$ (Red Repl)

($\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}$), $\mathcal{P} \cup \{\text{new } a; P\} \to (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}} \cup \{a'\})$, $\mathcal{P} \cup \{P^{a'/a}\}$

where $a' \notin \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$ (Red Res)

$E, \mathcal{P} \cup \{\text{out}(N, M); Q, \text{in}(N, x); P\} \to E, \mathcal{P} \cup \{Q, P^{M/x}\}$ (Red I/O)

$E, \mathcal{P} \cup \{\text{let } x = D \text{ in } P \text{ else } Q\} \to E, \mathcal{P} \cup \{P^{M/x}\}$
if $D \Downarrow M$ (Red Eval 1)

$E, \mathcal{P} \cup \{\text{let } x = D \text{ in } P \text{ else } Q\} \to E, \mathcal{P} \cup \{Q\}$ (Red Eval 2)
if $D \Downarrow \text{fail}$

$E, \mathcal{P} \cup \{\text{if true then } P \text{ else } Q\} \to E, \mathcal{P} \cup \{P\}$ (Red Cond 1)

$E, \mathcal{P} \cup \{\text{if } M \text{ then } P \text{ else } Q\} \to E, \mathcal{P} \cup \{Q\}$ (Red Cond 2)
if $M \ne \text{true}$

<caption>**Figure 2.4:** Operational semantics</caption>
expressions: the relation $D \Downarrow U$ means that the closed expression $D$ evaluates to the closed may-fail term $U$, which may be a closed term $M$ or the constant fail. 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

$$f(x_1, \dots, x_n) \rightarrow f(x_1, \dots, 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)$:

$$h(u_1, \dots, u_n) \rightarrow \text{fail}, \qquad (2.6)$$

where $u_1, \dots, u_n$ are may-fail variables. This rewrite rule expresses that the function $h$ returns fail when no other rewrite rule applies. In particular, constructors return fail when one of their argument fails. In Figure 2.4, the first two rules of the definition of $\Downarrow$ express that a closed term and fail evaluate to themselves; the third rule deals with function application. It first evaluates the arguments of the function $D_1, \dots, D_n$ to $U_1, \dots, U_n$ respectively. Then, it applies the $j$-th rewrite rule of $h$, $h(U'_{j,1}, \dots, U'_{j,n}) \rightarrow U'_j$, instantiated with the substitution $\sigma$, so $h(U_1, \dots, U_n) = h(\sigma U'_{j,1}, \dots, \sigma U'_{j,n})$ reduces into $\sigma U'_j$. The last line checks that the rewrite rules before the $j$-th cannot be applied.

**Example 2.3.** For instance, we have

$$\text{adec}(\text{aenc}(\text{sign}(k, ssk_A), \text{pk}(sk_B)), sk_B) \Downarrow \text{sign}(k, ssk_A)$$

by the rewrite rule (2.1). Hence

$$\text{check}(\text{adec}(\text{aenc}(\text{sign}(k, ssk_A), \text{pk}(sk_B)), sk_B), \text{pk}(ssk_A)) \Downarrow k$$

by the rewrite rule (2.3). On the other hand,

$$\text{adec}(\text{aenc}(\text{sign}(k, ssk_A), \text{pk}(sk_B)), ssk_A) \Downarrow \text{fail}$$

by the rewrite rule (2.6). (The rewrite rule (2.1) cannot be applied because the decryption key does not match the encryption key.) Hence,

$$\text{check}(\text{adec}(\text{aenc}(\text{sign}(k, ssk_A), \text{pk}(sk_B)), ssk_A), \text{pk}(ssk_A)) \Downarrow \text{fail}$$

by the rewrite rule (2.6) again.
Second, we define the semantics of processes, by reduction of semantic configurations. A semantic configuration is a pair $E, \mathcal{P}$ where the environment $E$ is a pair of two finite sets of names ($\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}$) and $\mathcal{P}$ is a finite multiset of closed processes. The set $\mathcal{N}_{\text{pub}}$ contains the public names, the set $\mathcal{N}_{\text{priv}}$ contains the private names, and the multiset of processes $\mathcal{P}$ contains the processes currently running.<fnref n="1" /> The configuration $(\{a_1, \dots, a_n\}, \{b_1, \dots, b_m\}), \{P_1, \dots, P_k\}$ corresponds intuitively to the process *new* $b_1; \dots; *new* b_m; (P_1 | \dots | P_k)$. (Recall that types are ignored, so we need not type the names $b_1, \dots, b_m$.) A configuration $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P}$ is valid when $\mathcal{N}_{\text{pub}}$ and $\mathcal{N}_{\text{priv}}$ are disjoint and $\mathcal{P} \subseteq \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$. We only consider valid configurations. The reduction relation $\rightarrow$ 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 $\mathcal{N}_{\text{priv}}$. The fresh name $a'$ is required to occur neither in $\mathcal{N}_{\text{priv}}$, which contains the initial private free names as well as any fresh name created by a previous application of (Red Res), nor in $\mathcal{N}_{\text{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$.

<footnote n="1">¹In (Blanchet, 2009), the environment $E$ is simply a set of names, corresponding to $\mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$. Indeed, the distinction between public and private names is not essential for trace properties. It is useful for treating equivalences in §3.4.</footnote>
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 $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{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 = \text{in}(c, x_{\text{spk}_A}); \text{in}(c, x_{\text{pk}_B}); \text{out}(c, x_{\text{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:

$$
\begin{align*}
& (\{c\}, \{s\}), \{P_0, Q\} \\
\rightarrow &^* E_1, \{\text{out}(c, \text{pk}(ssk_A)); \text{out}(c, \text{pk}(sk_B)); \\
& \qquad (P_A(ssk_A, \text{pk}(sk_B)) | P_B(sk_B, \text{pk}(ssk_A)), Q)\} \\
& \qquad \text{by (Red Res) twice and (Red Eval 1) twice} \\
\rightarrow &^* E_1, \{P_A(ssk_A, \text{pk}(sk_B)), P_B(sk_B, \text{pk}(ssk_A)), \\
& \qquad \text{out}(c, \text{pk}(sk_B))\} \text{ by (Red I/O) twice and (Red Par)} \\
\rightarrow &^* E_1, \mathcal{P} \cup \{P'_A, P'_B, \text{out}(c, \text{pk}(sk_B))\} \text{ by (Red Repl) twice}
\end{align*}
$$

where

$$
\begin{align*}
E_1 &= (\{c\}, \{s, ssk_A, sk_B\}) \\
\mathcal{P} &= \{P_A(ssk_A, \text{pk}(sk_B)), P_B(sk_B, \text{pk}(ssk_A))\} \\
P'_A &= \text{in}(c, x_{pk_B}); \text{new } k; \text{out}(c, \text{aenc}(\text{sign}(k, ssk_A), x_{pk_B})); P''_A \\
P''_A &= \text{in}(c, x); \text{let } z = \text{sdec}(x, k) \text{ in } \mathbf{0} \\
P'_B &= \text{in}(c, y); \text{let } y' = \text{adec}(y, sk_B) \text{ in} \\
& \phantom{=} \quad \text{let } x_k = \text{check}(y', \text{pk}(ssk_A)) \text{ in } \text{out}(c, \text{senc}(s, x_k)).
\end{align*}
$$

By (Red I/O), $P'_A$ reduces with $\text{out}(c, \text{pk}(sk_B))$; by (Red Nil), we remove
the omitted final $\mathbf{0}$. With $E_2 = (\{c\}, \{s, ssk_A, sk_B, k\})$, we obtain

$$
E_1, \mathcal{P} \cup \{\text{new } k; \text{out}(c, \text{aenc}(\text{sign}(k, ssk_A), \text{pk}(sk_B))); P_A'' \cup P_B''\}
$$
$$ \rightarrow E_2, \mathcal{P} \cup \{\text{out}(c, \text{aenc}(\text{sign}(k, ssk_A), \text{pk}(sk_B))); P_A'', P_B'\} $$
by (Red Res) (A creates the fresh key $k$)

$$ \rightarrow E_2, \mathcal{P} \cup \{P_A'', \\ \text{let } y' = \text{adec}(\text{aenc}(\text{sign}(k, ssk_A), \text{pk}(sk_B)), sk_B) \text{ in} \\ \text{let } x_k = \text{check}(y', \text{pk}(ssk_A)) \text{ in } \text{out}(c, \text{senc}(s, x_k))\} $$
by (Red I/O) (A sends message 1 to B)

$$ \rightarrow^* E_2, \mathcal{P} \cup \{P_A'', \text{out}(c, \text{senc}(s, k))\} $$
by (Red Eval 1) twice

$$ \rightarrow E_2, \mathcal{P} \cup \{\text{let } z = \text{sdec}(\text{senc}(s, k), k) \text{ in } \mathbf{0}, \mathbf{0}\} $$
by (Red I/O) (B sends message 2 to A)

$$ \rightarrow E_2, \mathcal{P} \cup \{\mathbf{0}, \mathbf{0}\} $$
by (Red Eval 1)

$$ \rightarrow^* E_2, \mathcal{P} $$
by (Red Nil) twice

There exist other approaches to define the semantics of such a language. We discuss one such approach in Chapter 4.

## 2.5 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.

### 2.5.1 Equations

In addition to cryptographic primitives defined by rewrite rules, ProVerif also supports primitives defined by equations. We consider an equational theory $\mathcal{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 $\mathcal{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 =_{\mathcal{E}} N$ an equality modulo $\mathcal{E}$, and $M \neq_{\mathcal{E}} N$ a disequality modulo $\mathcal{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 \neq_{\mathcal{E}} N$.

As an example, the Diffie-Hellman key agreement (Diffie and Hellman, 1976) 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 $\mathbb{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 (Abadi and Fournet, 2001; Abadi et al., 2007)

$$ \exp(\exp(g, x), y) = \exp(\exp(g, y), x) \qquad (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

$$ \begin{aligned} \text{sdec}(\text{senc}(x, y), y) &= x \\ \text{senc}(\text{sdec}(x, y), y) &= x \end{aligned} \qquad (2.8) $$

where $\text{senc}(\text{bitstring}, \text{key}) : \text{bitstring}$ and $\text{sdec}(\text{bitstring}, \text{key}) : \text{bitstring}$ are constructors. In this model, decryption always succeeds, because $\text{sdec}(M, N)$ is always a term, even when $M$ is not of the form $\text{senc}(M', N)$. The first equation is standard; the second one avoids that the equality test $\text{senc}(\text{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 $\mathcal{E}$:

$h(D_1, \dots, D_n) \triangleq \sigma U'_j$ if and only if

$D_1 \triangleq U_1, \dots, D_n \triangleq U_n,$

def($h$) consists of the rewrite rules

$h(U'_{i,1}, \dots, U'_{i,n}) \rightarrow U'_i$ for $i \in \{1, \dots, k\},$

$\sigma U'_{j,1} = \mathcal{E} U_1, \dots, \sigma U'_{j,n} = \mathcal{E} U_n,$ and

for all $i \le j$, for all $\sigma'$, $\sigma' U'_{i,1} \ne \mathcal{E} U_1, \dots, \sigma' U'_{i,n} \ne \mathcal{E} U_n$.

We also extend the reduction rules by considering equality modulo $\mathcal{E}$:

$$ E, \mathcal{P} \cup \{ \text{out}(N, M); Q, \text{in}(N', x); P \} \rightarrow E, \mathcal{P} \cup \{ Q, P\{M/x\} \} \quad \text{(Red I/O')} $$

$$ E, \mathcal{P} \cup \{ \text{if } M \text{ then } P \text{ else } Q \} \rightarrow E, \mathcal{P} \cup \{ P \} \quad \text{(Red Cond 1')} $$

$$ E, \mathcal{P} \cup \{ \text{if } M \text{ then } P \text{ else } Q \} \rightarrow E, \mathcal{P} \cup \{ Q \} \quad \text{(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

$$ \begin{aligned} \text{senc}(x, y) &\rightarrow \text{senc}(x, y) & \text{sdec}(x, y) &\rightarrow \text{sdec}(x, y) \\ \text{senc}(\text{sdec}(x, y), y) &\rightarrow x & \text{sdec}(\text{senc}(x, y), y) &\rightarrow x \end{aligned} \quad (2.9) $$

while the equation (2.7) is translated into

$$ \exp(x, y) \rightarrow \exp(x, y) \qquad \exp(\exp(g, x), y) \rightarrow \exp(\exp(g, y), x) \quad (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.<fnref n="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 Delaune, 2005). 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).<fnref n="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 (Comon-Lundh and Shmatikov, 2003; Chevalier et al., 2005) and a more complete theory of modular exponentiation is handled in (Chevalier et al., 2003). A unification algorithm for modular exponentiation is presented in (Meadows and Narendran, 2002). For an unbounded number of sessions, extensions of the Horn clause

<footnote n="2">²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)`.</footnote>

<footnote n="3">³More precisely, the disequality tests in $D \Downarrow 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.</footnote>
approach have been proposed. Küsters and Truderung, 2008 support exclusive or provided one of its two arguments is a constant in the clauses that model the protocol. Küsters and Truderung, 2009 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 (Meadows, 1996; Escobar et al., 2006) and Tamarin (Schmidt et al., 2012) 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 (Escobar et al., 2007) (which includes Diffie-Hellman exponentiation and exclusive or), as well as homomorphic encryption (Escobar et al., 2011). Tamarin supports subterm convergent equations, Diffie-Hellman exponentiation (including equations of the multiplicative group modulo $p$), bilinear pairings, and associative and commutative operators (Schmidt et al., 2014).

### 2.5.2 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 ::= \begin{array}{l} \text{...} \\ \text{out}(D, D'); P \\ \text{in}(D, x : T); P \\ \text{if } D \text{ then } P \text{ else } Q \end{array} \qquad \begin{array}{l} \text{processes} \\ \text{output} \\ \text{input} \\ \text{conditional} \end{array} $$

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, \mathcal{P} \cup \{ \text{out}(D', D); Q, \text{in}(D'', x); P \} \to E, \mathcal{P} \cup \{ Q, P\{M/x\} \} $$
$$ \text{if } D \Downarrow M, D' \Downarrow M', D'' \Downarrow M'', \text{ and } M' =_{\mathcal{E}} M'' \quad \text{(Red I/O'')} $$

$$ E, \mathcal{P} \cup \{ \text{if } D \text{ then } P \text{ else } Q \} \to E, \mathcal{P} \cup \{ P \} $$
$$ \text{if } D \Downarrow M \text{ and } M =_{\mathcal{E}} \text{true} \quad \text{(Red Cond 1'')} $$

$$ E, \mathcal{P} \cup \{ \text{if } D \text{ then } P \text{ else } Q \} \to E, \mathcal{P} \cup \{ Q \} $$
$$ \text{if } D \Downarrow M \text{ and } M \neq_{\mathcal{E}} \text{true} \quad \text{(Red Cond 2'')} $$

Alternatively, processes with such expressions can easily be encoded into the core calculus by introducing additional expression evaluations. For instance, $\text{in}(D, x : T); P$ can be encoded as

$$ \text{let } y = D \text{ in } \text{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 ::= \text{ 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.

### 2.5.3 Pattern-matching

We enrich the input and expression evaluation constructs with pattern-matching as follows:

$$ P, Q ::= \text{ processes} $$

...

$\text{in}(D, pat); P$ input

let $pat = D$ in $P$ else $Q$ expression evaluation
where patterns *pat* are defined by the following grammar:

<table><tr><td><i>pat</i> ::=</td><td>patterns</td></tr><tr><td><i>x</i> : <i>T</i></td><td>variable</td></tr><tr><td><i>=D</i></td><td>equality test</td></tr><tr><td><i>f</i>(<i>pat</i><sub>1</sub>, ..., <i>pat</i><sub>n</sub>)</td><td>data constructor</td></tr></table>

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 pattern-matching fails.

The pattern *f*(*pat*<sub>1</sub>, ..., *pat*<sub>*n*</sub>) matches terms of the form *f*(*M*<sub>1</sub>, ..., *M*<sub>*n*</sub>), when *pat*<sub>*i*</sub> matches *M*<sub>*i*</sub> for all *i* ≤ *n*. This pattern can be used only when *f* is *data constructor*. A *data constructor* is a constructor *f* of a type *n* that comes with associated destructors *g*<sub>*i*</sub> for *i* ∈ {1, ..., *n*} defined by *g*<sub>*i*</sub>(*f*(*x*<sub>1</sub>, ..., *x*<sub>*n*</sub>)) → *x*<sub>*i*</sub>. 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*<sub>1</sub>, ..., *M*<sub>*n*</sub>) =<sub>ε</sub> *M'* if and only if there exist *M*'<sub>1</sub>, ..., *M*'<sub>*n*</sub> such that *M'* = *f*(*M*'<sub>1</sub>, ..., *M*'<sub>*n*</sub>) and *M*<sub>*i*</sub> =<sub>ε</sub> *M*'<sub>*i*</sub> 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 \to B : aenc(\text{sign}((pk_B, k), ssk_A), pk_B)$
<figure><img src="image_6.png" /><figcaption>**Figure 2.5:** Modified example of protocol</figcaption></figure>

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) = ! \text{ in}(c, x_{pk_B} : \text{pkey}); \text{ new } k : \text{key};$$

$$\text{out}(c, \text{aenc}(\text{sign}((x_{pk_B}, k), ssk_A), x_{pk_B}));$$

$$\text{in}(c, x : \text{bitstring}); \text{let } z = \text{sdec}(x, k) \text{ in } \mathbf{0}$$

$$P_B(sk_B, spk_A) = ! \text{ in}(c, y : \text{bitstring}); \text{let } y' = \text{adec}(y, sk_B) \text{ in}$$

$$\text{let } (=\text{pk}(sk_B), x_k : \text{key}) = \text{check}(y', spk_A) \text{ in } \text{out}(c, \text{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 = \text{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) = ! \text{ in}(c, y : \text{bitstring}); \text{let } y' = \text{adec}(y, sk_B) \text{ in} \\ \text{let } z = \text{check}(y', spk_A) \text{ in if } \text{1th}_{\text{pkey,key}}(z) = \text{pk}(sk_B) \text{ then} \\ \text{let } x_k = \text{2th}_{\text{pkey,key}}(z) \text{ in } \text{out}(c, \text{senc}(s, x_k))$$

This process uses the extension of §2.5.2 to allow destructors in if $\text{1th}_{\text{pkey,key}}(z) = \text{pk}(sk_B)$ then. It can be encoded in the core calculus as
follows:

$$
\begin{align*}
P_B(sk_B, spk_A) = &! \text{in}(c, y : \text{bitstring}); \text{let } y' = \text{adec}(y, sk_B) \text{ in} \\
&\text{let } z = \text{check}(y', spk_A) \text{ in } \text{let } z' = (\text{th}_{\text{pkey},\text{key}}(z) = \text{pk}(sk_B)) \text{ in} \\
&\text{if } z' \text{ then let } x_k = 2\text{th}_{\text{pkey},\text{key}}(z) \text{ in } \text{out}(c, \text{senc}(s, x_k))
\end{align*}
$$

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.

2.5.4 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 (Kremer and Ryan, 2005). ProVerif includes a phase construct to model such situations:

$$
\begin{array}{ll}
P, Q ::= & \text{processes} \\
\dots & \\
\text{phase } n; P & \text{phase}
\end{array}
$$

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 = \text{new ssk}_A : \text{skey}; (P \mid \text{phase } 1; \text{out}(c, \text{ssk}_A)),
$$

where *P* does not contain phases, models a protocol *P* that runs in phase 0, using the secret key *ssk*<sub>A</sub>. This key is then compromised in phase 1, by sending it on the public channel *c*.
### 2.5.5 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:

$$ 
\begin{array}{ll}
P, Q ::= & \text{processes} \\
\dots & \\
\text{insert } tbl(D_1, \dots, D_n); P & \text{insertion in a table} \\
\text{get } tbl.pat_1, \dots, pat_n) & \text{suchthat } D \text{ in } P \text{ else } Q \\
& \text{lookup in a table}
\end{array}
$$

The process `insert tbl(D₁, ..., Dₙ)`; `P` inserts the record `(M₁, ..., Mₙ)` in the table `tbl`, where `D₁, ..., Dₙ` evaluate to `M₁, ..., Mₙ` respectively, then runs `P`. The process `get tbl.pat₁, ..., patₙ)` suchthat `D` in `P` else `Q` looks for a record `(M₁, ..., Mₙ)` in the table `tbl` that matches the patterns `(pat₁, ..., patₙ)` and such that the condition `D` evaluates to `true`. When such a record is found, it runs `P` with the variables of `pat₁, ..., patₙ` bound to the corresponding values. Otherwise, it runs `Q`. The condition `suchthat D` can be omitted when `D` is `true`. The branch `else Q` can be omitted when `Q` is `0`.

**Example 2.8.** We consider again the protocol of §2.2. Instead of adding the public key of `B` to the first message, as in Example 2.5, we may add the name of `B`. The first message would then become

Message 1. $A \rightarrow B : \text{aenc}(\text{sign}((B, k), ssk_A), pk_B)$.

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 (Denning and Sacco, 1981): 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:
<figure><img src="image_7.png" /><figcaption>**Figure 2.6: Protocol with certificates**</figcaption></figure>

Message 1. $A \to S: A, B$

Message 2. $S \to A: c_A, c_B$

Message 3. $A \to B: c_A, c_B, \text{aenc}(\text{sign}((B, k), ssk_A), pk_B)$

Message 4. $B \to A: \text{senc}(s, k)$

where $c_A = \text{sign}((s, A, spk_A), ssk_S)$ and $c_B = \text{sign}((e, B, pk_B), ssk_S)$. This protocol is illustrated in Figure 2.6. A first asks the server for the certificate for its own signature key $spk_A$ and for the encryption key $pk_B$ of B. The second certificate allows A to obtain the key $pk_B$. Then it sends the message $\text{aenc}(\text{sign}((B, k), ssk_A), pk_B)$ with the certificates to B. B uses $c_A$ to obtain A's signature verification key $spk_A$. It decrypts and verifies the signature as before; it additionally verifies that B is the first component of the signed message.

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
$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$)))

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 (=, 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 (=, 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$))

<caption>**Figure 2.7:** ProVerif example with tables</caption>
$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.

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 pro-
tocols. 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 (Blanchet,
2009) 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.

3.1 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 (Dolev and Yao, 1983). In our calculus,
an adversary can be represented by any process that has the set of public free names $\mathcal{N}_{\text{pub}}$ in its initial knowledge. (Although the initial knowledge of the adversary contains only names in $\mathcal{N}_{\text{pub}}$, one can give any terms to the adversary by sending them on a channel in $\mathcal{N}_{\text{pub}}$.)

**Definition 3.1.** Let $\mathcal{N}_{\text{pub}}$ be a finite set of names. The closed process $Q$ is an $\mathcal{N}_{\text{pub}}$-adversary if and only if $fn(Q) \subseteq \mathcal{N}_{\text{pub}}$ and all function symbols in $Q$ are public. (The process $Q$ is not necessarily well-typed.)

## 3.2 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.

### 3.2.1 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 = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P}_0 \to^* E', \mathcal{P}'$ outputs $M$ publicly if and only if $Tr$ contains a reduction $E, \mathcal{P} \cup \{\text{out}(N, M); Q, \text{in}(N, x); P \} \to E, \mathcal{P} \cup \{Q, P\{M/x\}\}$ for some $E, \mathcal{P}, N, x, P, Q$, with $N \in \mathcal{N}_{\text{pub}}$.

We can finally define secrecy:

**Definition 3.3.** The closed process $P_0$ preserves the secrecy of the closed term $M$ from $\mathcal{N}_{\text{pub}}$ if and only if for some $\mathcal{N}_{\text{priv}}$ disjoint from $\mathcal{N}_{\text{pub}}$ such that $fn(M) \cup fn(P_0) \subseteq \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$, for any $\mathcal{N}_{\text{pub}}$-adversary $Q$, for any trace $Tr = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \{P_0, Q\} \to^* E', \mathcal{P}'$, the trace $Tr$ does not output $M$ publicly.

The choice of $\mathcal{N}_{\text{priv}}$ does not matter, provided the conditions of Definition 3.3 are satisfied.
### 3.2.2 From the pi calculus to Horn clauses

Given a closed process $P_0$ in the language of Chapter 2 and a set of names $\mathcal{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 $\mathcal{N}_{pub}$-adversary. This translation was originally given in (Abadi and Blanchet, 2005a); we extend it to the richer destructors of (Cheval and Blanchet, 2013). We suppose that the bound names of $P_0$ are pairwise distinct and distinct from the free names and the names in $\mathcal{N}_{pub}$.

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

$$ p ::= \begin{array}{ll} x, y, z, i & \text{patterns} \\ a[p_1, \dots, p_n] & \text{variable} \\ f(p_1, \dots, p_n) & \text{name} \\ & \text{constructor application} \end{array} $$

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, \dots, p_n]$ to each name $a$ of $P_0$. We treat $a$ as a function symbol, and write $a[p_1, \dots, p_n]$ rather than $a(p_1, \dots, p_n)$ only to distinguish functions that come from names from other functions. If $a$ is a free name, then its pattern is $a[\cdot]$. 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 $!\text{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 $\text{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:
<table><tr><td>mp ::=</td><td>may-fail pattern</td></tr><tr><td>p</td><td>pattern</td></tr><tr><td>u</td><td>may-fail variable</td></tr><tr><td>fail</td><td>failure</td></tr></table>

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:

<table><tr><td>F ::=</td><td>facts</td></tr><tr><td>attacker(<i>mp</i>)</td><td>adversary knowledge</td></tr><tr><td>message(<i>p</i>, <i>p'</i>)</td><td>message on a channel</td></tr><tr><td>∀<i>v</i>, (<i>mp</i><sub>1</sub>, ..., <i>mp</i><sub>n</sub>) ≠ (<i>mp</i>'<sub>1</sub>, ..., <i>mp</i>'<sub>n</sub>)</td><td>disequality</td></tr></table>

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*<sub>1</sub>, ..., *mp*<sub>n</sub>) ≠ (*mp*'<sub>1</sub>, ..., *mp*'<sub>n</sub>) means that (*mp*<sub>1</sub>, ..., *mp*<sub>n</sub>) ≠ (*mp*'<sub>1</sub>, ..., *mp*'<sub>n</sub>) 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*<sub>1</sub>, ..., *mp*<sub>n</sub> and *mp*'<sub>1</sub>, ..., *mp*'<sub>n</sub> when *n* = 1. We write *mp* as an abbreviation for (*mp*<sub>1</sub>, ..., *mp*<sub>n</sub>).

The clauses are of the form $F_1 \wedge \dots \wedge F_n \Rightarrow F$, where $F_1, \dots, F_n, F$ are facts. They comprise clauses for the adversary and clauses for the protocol, defined below. These clauses form the set $\mathcal{R}_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}}$.

### Clauses for the adversary

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

For each $a \in \mathcal{N}_{\text{pub}}$, **attacker**($a$[]) (Init)

**attacker**($b_0[x]$) where $b_0$ occurs neither in $P_0$ nor in $\mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$ (Rn)

**attacker**(*fail*) (Rfail)
For each public function $h$, such that $\text{def}(h)$ consists of the rewrite rules $h(U_{i,1}, \dots, U_{i,n}) \to U_i$ for $i \in \{1, \dots, k\}$, the variables in these rewrite rules are renamed so that distinct rewrite rules use different variables, and $\tilde{v}_i = fv(U_i) \cup \bigcup_{l=1}^n fv(U_{i,l})$,

for each $i \in \{1, \dots, k\}$,

$$ \text{attacker}(U_{i,1}) \wedge \dots \wedge \text{attacker}(U_{i,n}) \wedge $$

$$ \bigwedge_{j<i} \forall \tilde{v}_j, (U_{i,1}, \dots, U_{i,n}) \neq (U_{j,1}, \dots, U_{j,n}) \Rightarrow \text{attacker}(U_i) \qquad (\text{Rh}) $$

$$ \text{message}(x, y) \wedge \text{attacker}(x) \Rightarrow \text{attacker}(y) \qquad (\text{Rl}) $$

$$ \text{attacker}(x) \wedge \text{attacker}(y) \Rightarrow \text{message}(x, y) \qquad (\text{Rs}) $$

Clause (Init) represents the initial knowledge of the adversary. Clause (Rn) means that the adversary can generate an unbounded number of new names; these names are represented by patterns of the form $b_0[x]$. Clause (Rfail) means that the adversary has the special constant fail. Clauses (Rh) mean that the adversary can apply all public functions to all terms it has: if it has an instance of $U_{i,1}, \dots, U_{i,n}$, it can compute the corresponding instance of $U_i$ by applying the rewrite rule $h(U_{i,1}, \dots, U_{i,n}) \to U_i$, provided no previous rewrite rule applies, which is checked by $\bigwedge_{j<i} \forall \tilde{v}_j, (U_{i,1}, \dots, U_{i,n}) \neq (U_{j,1}, \dots, U_{j,n})$. The rewrite rules in $\text{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

$$ \text{attacker}(x_1) \wedge \dots \wedge \text{attacker}(x_n) \Rightarrow \text{attacker}(f(x_1, \dots, x_n)) \qquad (\text{Rf}) $$

and when $h$ is a destructor $g$ with a single rewrite rule $g(U_1, \dots, U_n) \to U$, they simplify into

$$ \text{attacker}(U_1) \wedge \dots \wedge \text{attacker}(U_n) \Rightarrow \text{attacker}(U) \qquad (\text{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:

$$ \text{attacker}(m) \wedge \text{attacker}(k) \Rightarrow \text{attacker}(\text{senc}(m, k)) \qquad (\text{senc}) $$

$$ \text{attacker}(sk) \Rightarrow \text{attacker}(\text{pk}(sk)) \qquad (\text{pk}) $$

$$ \text{attacker}(m) \wedge \text{attacker}(pk) \Rightarrow \text{attacker}(\text{aenc}(m, pk)) \qquad (\text{aenc}) $$

$$ \text{attacker}(m) \wedge \text{attacker}(sk) \Rightarrow \text{attacker}(\text{sign}(m, sk)) \qquad (\text{sign}) $$

The corresponding destructors sdec, adec, check, and getmess yield the following clauses:

$$ \text{attacker}(\text{senc}(m, k)) \wedge \text{attacker}(k) \Rightarrow \text{attacker}(m) \qquad (\text{sdec}) $$

$$ \text{attacker}(\text{aenc}(m, pk(sk))) \wedge \text{attacker}(sk) \Rightarrow \text{attacker}(m) \qquad (\text{adec}) $$

$$ \text{attacker}(\text{sign}(m, sk)) \wedge \text{attacker}(\text{pk}(sk)) \Rightarrow \text{attacker}(m) \qquad (\text{check}) $$

$$ \text{attacker}(\text{sign}(m, sk)) \Rightarrow \text{attacker}(m) \qquad (\text{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:

<table><tr><td>Dp ::=</td><td>pattern expression</td></tr><tr><td>mp</td><td>may-fail pattern</td></tr><tr><td>h(Dp<sub>1</sub>, ..., Dp<sub>n</sub>)</td><td>function application</td></tr></table>

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

$$mp \Downarrow'(mp, \emptyset, \top)$$

$h(Dp_1, \dots, Dp_n) \Downarrow' (\sigma_u U_i, \sigma_u \sigma', \sigma_u \phi' \wedge \sigma_u \phi)$
if $(Dp_1, \dots, Dp_n) \Downarrow' ((mp_1, \dots, mp_n), \sigma', \phi')$,
$\sigma_u$ is a most general unifier of $(mp_1, U_{i,1}), \dots, (mp_n, U_{i,n})$, and
$\phi = \bigwedge_{j<i} \forall \tilde{v}_j, (mp_1, \dots, mp_n) \neq (U_{j,1}, \dots, U_{j,n})$
for some $i \in \{1, \dots, k\}$,

where $def(h)$ consists of the rewrite rules $h(U_{i,1}, \dots, U_{i,n}) \rightarrow U_i$ for $i \in \{1, \dots, k\}$, the variables in these rewrite rules are renamed so that distinct rewrite rules use different variables, and

$$\tilde{v}_i = fv(U_i) \cup \bigcup_{l=1}^{n} fv(U_{i,l}) \text{ for all } i \in \{1, \dots, k\}.$$

$(Dp_1, \dots, Dp_n) \Downarrow' ((\sigma_n mp_1, \dots, \sigma_n mp_{n-1}, mp_n), \sigma_n \sigma, \sigma_n \phi \wedge \phi_n)$
if $(Dp_1, \dots, Dp_{n-1}) \Downarrow' ((mp_1, \dots, mp_{n-1}), \sigma, \phi)$
and $\sigma Dp_n \Downarrow' (mp_n, \sigma_n, \phi_n)$

The substitution $\emptyset$ is the identity. The formula $\top$ 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 $\Downarrow'$ 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, \dots, mp_n$, checks that the rewrite rule actually applies by unifying $mp_1, \dots, 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 $\phi$. Finally, the third rule treats the evaluation of a tuple.
The translation $[[P]]\rho sH$ of a process $P$ is a set of clauses, where $\rho$ 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 $\rho$ as a substitution by $\rho(h(M_1, \dots, M_n)) = h(\rho(M_1), \dots, \rho(M_n))$ and $\rho(\mathbf{fail}) = \mathbf{fail}$. The empty sequence is written $\emptyset$; 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 \land F$. Intuitively, $H$ represents the hypothesis of the clauses, $\rho$ 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]]\rho sH$ is defined as follows:

$$ 
\begin{align*}
& [[0]]\rho sH = \emptyset \\
& [[P \mid Q]]\rho sH = [[P]]\rho sH \cup [[Q]]\rho sH \\
& [[!P]]\rho sH = [[P]]\rho(s, i)H \text{ where } i \text{ is a fresh variable} \\
& [[\mathbf{new} \; a; P]]\rho sH = [[P]](\rho[a \mapsto a[s]])sH \\
& [[\mathbf{in}(M, x); P]]\rho sH = [[P]](\rho[x \mapsto x'])(s, x')(H \land \mathbf{message}(\rho(M), x')) \\
& \qquad \text{where } x' \text{ is a fresh variable}
\end{align*}
$$

$$ [[\mathbf{out}(M, N); P]]\rho sH = [[P]]\rho sH \cup \{H \Rightarrow \mathbf{message}(\rho(M), \rho(N))\} $$

$$ 
\begin{align*}
& [[\mathbf{let} \ x = D \ \mathbf{in} \ P \ \mathbf{else} \ Q]]\rho sH = \\
& \quad \cup \{[[P]]((\sigma\rho)[x \mapsto p])(\sigma s)(\sigma H \land \phi) \mid \rho(D) \Downarrow' (p, \sigma, \phi)\} \\
& \quad \cup \{[[Q]](\sigma\rho)(\sigma s)(\sigma H \land \phi) \mid \rho(D) \Downarrow' (\mathbf{fail}, \sigma, \phi)\}
\end{align*}
$$

$$ 
\begin{array}{l}
[[\mathbf{if} \ M \ \mathbf{then} \ P \ \mathbf{else} \ Q]]\rho sH = \\
\quad \begin{cases}
[[P]](\sigma\rho)(\sigma s)(\sigma H) \cup [[Q]]\rho s(H \land \rho(M) \neq \mathbf{true}) & \\
\quad \text{where } \sigma \text{ is the most general unifier of } \rho(M) \text{ and } \mathbf{true}, & \\
\quad \text{when } \rho(M) \text{ and } \mathbf{true} \text{ unify} & \\
\quad [[Q]]\rho sH & \text{when } \rho(M) \text{ and } \mathbf{true} \text{ do not unify}
\end{cases}
\end{array}
$$

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 $\rho$. In both cases, $\rho$, $s$, and $H$ are instantiated by $\sigma$ and the formula $\phi$ is added to the hypothesis $H$, where $\rho(D) \Downarrow' (mp, \sigma, \phi)$.

* 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 $\rho(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]]_{\rho_0} \emptyset \emptyset$ where $\rho_0 = \{a \mapsto a[] \mid a \in fn(P_0)\}$. These clauses are of the form $\mathbf{message}(p_1, p'_1) \wedge \dots \wedge \mathbf{message}(p_n, p'_n) \wedge \phi \Rightarrow \mathbf{message}(p, p')$ when the process $P_0$ sends message $p'$ on channel $p$ after receiving messages $p'_1, \dots, p'_n$ on channels $p_1, \dots, p_n$ respectively, provided the disequalities in $\phi$ hold. If $c \in \mathcal{N}_{\text{pub}}$, ProVerif replaces all occurrences of $\mathbf{message}(c[], p)$ with $\text{attacker}(p)$ in the clauses. Indeed, these facts are equivalent by the clauses (Rl) and (Rs).
Results and example

We define the clauses corresponding to the process $P_0$ as:

$$ \mathcal{R}_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} = [P_0]_{\rho_0 \emptyset \emptyset} \cup \{\text{attacker}(a[\cdot]) \mid a \in \mathcal{N}_{\text{pub}}\} \cup \\ \{\text{(Rn)}, \text{(Rfail)}, \text{(Rh)}, \text{(Rl)}, \text{(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 $\mathcal{N}_{\text{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[\cdot]$. Let $\mathcal{N}_{\text{priv}}$ be a set of names disjoint from $\mathcal{N}_{\text{pub}}$ and such that $\text{fn}(P_0) \cup \text{fn}(M) \subseteq \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$. If $\text{attacker}(p)$ is not derivable from $\mathcal{R}_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}}$, then $P_0$ preserves the secrecy of $M$ from $\mathcal{N}_{\text{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.2.3.

**Example 3.2.** Let $\mathcal{N}_{\text{pub}} = \{c\}$ be the initial knowledge of the adversary and $\mathcal{N}_{\text{priv}} = \{s\}$ be the private free names. For the process $P_0$ of Example 2.2, the clauses $[P_0]_{\rho_0 \emptyset \emptyset}$ are, after replacing $\text{message}(c[\cdot], p)$ with $\text{attacker}(p)$:

$$ \text{attacker}(\text{pk}(\text{ssk}_A[\cdot])) \qquad (3.1) $$

$$ \text{attacker}(\text{pk}(\text{sk}_B[\cdot])) \qquad (3.2) $$

$$ \text{attacker}(x_{pk_B}) \Rightarrow \qquad (3.3) $$

$$ \text{attacker}(\text{aenc}(\text{sign}(k[i, x_{pk_B}], \text{ssk}_A[\cdot], x_{pk_B}))) $$
$$ \begin{aligned} \text{attacker}(\text{aenc}(\text{sign}(x_m, ssk_A[]), \text{pk}(sk_B[]))) \Rightarrow \\ \text{attacker}(\text{senc}(s[], x_m)) \end{aligned} \qquad (3.4) $$

Clauses (3.1) and (3.2) 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 $\text{aenc}(\text{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 $\text{aenc}(\text{sign}(x_m, ssk_A[]), \text{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.

The fact $\text{attacker}(s[])$ is derivable from the clauses $R_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{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 (Abadi and Needham, 1996) against this protocol:

Message 1. $A \to C$: $\text{aenc}(\text{sign}(k, ssk_A), pk_C)$

Message 1: $C(A) \to B$: $\text{aenc}(\text{sign}(k, ssk_A), pk_B)$

Message 2. $B \to C(A)$: $\text{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 $\text{aenc}(\text{sign}(k, ssk_A), pk_C)$, decrypts it and re-encrypts it under the public key of $B$. The obtained message $\text{aenc}(\text{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 $\text{pk}(b_0[x])$ and is computed by the application of Clause (Rf)
$$ \frac{\frac{F_1 = \text{attacker}(b_0[x])}{\text{attacker}(pk(b_0[x]))} \text{ by (Rn)} \text{ by (Rf) for pk}}{F_2 = \text{attacker}(\text{aenc}(\text{sign}(k[i, pk(b_0[x])], ssk_A[]), pk(b_0[x])))} \text{ by (3.3)} $$

$$ \frac{F_2 \quad F_1}{F_3 = \text{attacker}(\text{sign}(k[i, pk(b_0[x])], ssk_A[]))} \text{ by (Rg) for adec} $$

$$ \frac{F_3 \quad \text{attacker}(pk(sk_B[])) \text{ by (3.2)}}{\text{attacker}(\text{aenc}(\text{sign}(k[i, pk(b_0[x])], ssk_A[]), pk(sk_B[])))} \text{ by (Rf) for aenc} \\ F_4 = \text{attacker}(\text{senc}(s[], k[i, pk(b_0[x])))) \text{ by (3.4)} $$

$$ \frac{F_4 \quad \frac{F_3}{\text{attacker}(k[i, pk(b_0[x])])} \text{ by (Rg) for getmess}}{\text{attacker}(s[])}} \text{ by (Rg) for sdec} $$

<caption>Figure 3.1: Derivation of attacker(s[])</caption>

for pk. The output of Message 1 corresponds to the application of Clause (3.3); then the adversary computes Message 1' by applying destructor adec to decrypt it and constructor aenc to reencrypt it under pk<sub>B</sub> = pk(sk<sub>B</sub>[]), corresponding to Clauses (Rg) for adec and (Rf) for aenc of the derivation. The input of Message 1' and the output of Message 2 corresponds to Clause (3.4). Finally, the adversary computes k (represented in the derivation by k[i, pk(b<sub>0</sub>[x])]) using Clause (Rg) for getmess and decrypts Message 2 by Clause (Rg) for sdec.

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. Allamigeon and Blanchet, 2005 extended ProVerif so that it automatically reconstructs an attack from
<figure><img src="image_8.png" /><figcaption>Figure 3.2: Attack</figcaption></figure>

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 $\text{out}(M, N)$; $P$ where $M$ is a name in $\mathcal{N}_{\text{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}$ (Millen, 1999). (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 can- not 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 $P_0 = \text{new } c; (\text{out}(c, s) | \text{in}(c, x); \text{out}(d, c))$ preserves the secrecy of $s$ from $\{d\}$, but ProVerif cannot prove it, because **attacker**($s$[]) is derivable from the clauses (Rl), $\text{message}(c[], s[])$ and $\text{message}(c[], x) \Rightarrow \text{attacker}(c[])$, which are in $\mathcal{R}_{P_0, \{d\}, \{s\}}$. (The fact $\text{message}(d[], c[])$ is equivalent to **attacker**($c$[]) since $d$ is a public channel.) The clauses do not take into account that the output $\text{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 gen- erated clauses are the same as for the process $P'_0 = \text{new } c; (!\text{out}(c, s) | \text{in}(c, x); \text{out}(d, c))$, in which actions are repeated, and which does not preserve the secrecy of $s$ from $\{d\}$.

An additional approximation occurs with outputs on private chan- nels: for the output $\text{out}(M, N)$; $P$, the Horn clause representation con- siders that the process $P$ can always be executed, as if the process was $\text{out}(M, N) | P$, while in fact $P$ can be executed only after sending $N$ on channel $M$.

### 3.2.3 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 (Kowalski, 1974), so for instance,
with the goal `attacker(s[])`, the clause

$$ \text{attacker}(\text{aenc}(m, \text{pk}(sk))) \wedge \text{attacker}(sk) \Rightarrow \text{attacker}(m) $$

leads to considering more and more complex facts

$$ \text{attacker}(\text{aenc}(\dots, \text{aenc}(s[], \text{pk}(sk_1)), \dots, \text{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 (Bachmair and Ganzinger, 2001). We could also use ordered resolution with selection, used by Weidenbach, 1999 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 \Rightarrow C$ and $R' = F \wedge H' \Rightarrow C'$ (where $F$ is any hypothesis of $R'$) to infer $R \circ_F R' = \sigma H \wedge \sigma H' \Rightarrow \sigma C'$ where $C$ and $F$ are unifiable and $\sigma$ is the most general unifier of $C$ and $F$. Hence, the clause $R \circ_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) = \emptyset` 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₀)` 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) = \emptyset$.

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 \Rightarrow C) = \left\{ \begin{array}{ll} \emptyset & \text{if all elements of } H \text{ are disequalities or of the} \\ & \text{form attacker}(v), v \text{ variable or may-fail variable} \\ \{F\} & \text{where } F \text{ is not a disequality,} \\ & F \neq \text{attacker}(v) \text{ and } F \in H, \text{ otherwise} \end{array} \right. $$

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 (Blanchet, 2009). 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 $H_1 \Rightarrow C_1$ subsumes $H_2 \Rightarrow C_2$ if and only if there exists a substitution $\sigma$ such that $\sigma H_1 \subseteq H_2$ (multiset inclusion) and $\sigma C_1 = C_2$. All clauses subsumed by another clause of the current clause set are removed.

* *Elimination of duplicate hypotheses.* Only one copy of duplicate hypotheses in a clause is kept.

* *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:

$$ \mathit{attacker}(x_1) \wedge \dots \wedge \mathit{attacker}(x_n) \Rightarrow \mathit{attacker}(f(x_1, \dots, x_n)) \quad (\mathit{Rf}) $$

$$ \mathit{attacker}(f(x_1, \dots, x_n)) \Rightarrow \mathit{attacker}(x_i) \quad (\mathit{Rg}) $$

Therefore, $\mathit{attacker}(f(p_1, \dots, p_n))$ is derivable if and only if $\forall i \in \{1, \dots, n\}$, $\mathit{attacker}(p_i)$ is derivable. When a fact of the form $\mathit{attacker}(f(p_1, \dots, p_n))$ is met, it is replaced with $\mathit{attacker}(p_1) \wedge \dots \wedge \mathit{attacker}(p_n)$. If this replacement is done in the conclusion of a clause $H \Rightarrow \mathit{attacker}(f(p_1, \dots, p_n))$, n clauses are created: $H \Rightarrow \mathit{attacker}(p_i)$ for each $i \in \{1, \dots, n\}$. This replacement is of course done recursively: if $p_i$ itself is a data constructor application, it is replaced again. The clauses (Rf) and (Rg) for data constructors are left unchanged.

## 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 \wedge \forall \tilde{v}, (mp_1, \dots, mp_n) \neq (mp'_1, \dots, mp'_n) \Rightarrow C$ are transformed as follows.

When $mp_i$ or $mp'_i$ is a may-fail variable $u$ not in $\tilde{v}$, we replace the clause with two clauses

$$ H \wedge \forall \tilde{v}, (mp_1, \dots, mp_n) \{x/u\} \neq (mp'_1, \dots, mp'_n) \{x/u\} \Rightarrow C, $$

$$ H \wedge \forall \tilde{v}, (mp_1, \dots, mp_n) \{\text{fail}/u\} \neq (mp'_1, \dots, mp'_n) \{\text{fail}/u\} \Rightarrow 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.

*   **Unification.** The transformation **unify** transforms clauses of the form $H \wedge \forall \tilde{v}, \overline{mp} \neq \overline{mp}' \Rightarrow C$ as follows. It tries to unify $\overline{mp}$ and $\overline{mp}'$. If this unification fails, then the clause becomes $H \Rightarrow C$, because $\forall \tilde{v}, \overline{mp} \neq \overline{mp}'$ holds when $\sigma \overline{mp} \neq \sigma \overline{mp}'$ for all $\sigma$. Otherwise, **unify** replaces the clause with

$$H \wedge \forall \tilde{v}, (v_1, \dots, v_k) \neq (\sigma v_1, \dots, \sigma v_k) \Rightarrow C$$

where $\sigma$ is the most general unifier of $\overline{mp}$ and $\overline{mp}'$ and $v_1, \dots, v_k$ are all variables affected by $\sigma$. In this unification, $\sigma$ is built so that all variables in its domain and its image are variables of $\overline{mp}$ and $\overline{mp}'$, and the variables in its domain do not occur in its image. Note that an instance of $\forall \tilde{v}, (v_1, \dots, v_k) \neq (\sigma v_1, \dots, \sigma v_k)$ holds if and only if the same instance of $\forall \tilde{v}, \overline{mp} \neq \overline{mp}'$ does, because $\sigma' \overline{mp} = \sigma' \overline{mp}'$ if and only if $\sigma'(v_1, \dots, v_k) = \sigma' \sigma(v_1, \dots, v_k)$, for all $\sigma'$.

For instance, **unify** transforms the clause

$$H \wedge \forall z, (\text{senc}(x', y'), z') \neq (\text{senc}(z, y), z) \Rightarrow C$$

into

$$H \wedge \forall z, (x', y', z') \neq (z, y, z) \Rightarrow C \qquad (3.5)$$

*   **Elimination of elements of $\tilde{v}$.** The transformation **elimGVar** transforms facts $\forall \tilde{v}, (mp_1, \dots, mp_n) \neq (mp'_1, \dots, mp'_n)$ in clauses obtained after **unify**, as follows:

1.  When $mp_i = u \in \tilde{v}$ is a may-fail variable, it eliminates the pair $mp_i, mp'_i$ from the disequality and removes $u$ from $\tilde{v}$.

2.  When $mp_i = x \in \tilde{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 $\tilde{v}$.
3. Otherwise, when $mp'_i \in \tilde{v}$, it swaps $mp_i$ and $mp'_i$ everywhere in the disequality $(mp_1, \dots, mp_n) \neq (mp'_1, \dots, mp'_n)$, then applies one of the first two cases.

The cases in which $mp_i$ is an ordinary variable and $mp'_i = \mathbf{fail}$, or $mp'_i$ is an ordinary variable and $mp_i = \mathbf{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 $\sigma$,

$$ \sigma(\forall \tilde{v}, (mp_1, \dots, mp_n) \neq (mp'_1, \dots, mp'_n)) $$

is equivalent to

$$ \sigma(\forall \tilde{v}', (\forall u, u \neq mp'_i) \lor (mp_1, \dots, mp_{i-1}, mp_{i+1}, \dots, mp_n) \neq (mp'_1, \dots, mp'_{i-1}, mp'_{i+1}, \dots, mp'_n)) $$

which is equivalent to

$$ \sigma(\forall \tilde{v}', (mp_1, \dots, mp_{i-1}, mp_{i+1}, \dots, mp_n) \neq (mp'_1, \dots, mp'_{i-1}, mp'_{i+1}, \dots, mp'_n)) $$

since $\forall u, u \neq \sigma mp'_i$ is false for all $\sigma$.

In Case 2, $\forall x, x \neq \sigma 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 \land \forall z, (z, y', z') \neq (x', y, x') \Rightarrow C $$

by swapping $z$ and $x'$ (Case 3), then transforms it into

$$ H \land (y', z') \neq (y, x') \Rightarrow C $$

by Case 2.
* Detection of failed disequity. Clauses that contain the hypothesis $\forall \tilde{v}, () \neq ()$ 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 $\mathcal{R}_0$ if and only if it is derivable from saturate($\mathcal{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, \dots, p_n)$ are derivable by the following computation:

$$ \text{solve}_{\mathcal{P}_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} (pred(p_1, \dots, p_n)) = \\ \{H \Rightarrow pred(p'_1, \dots, p'_n) \mid H \Rightarrow pred'(p'_1, \dots, p'_n) \in \text{saturate}(\mathcal{R}_0)\}, $$

where $pred'$ is a new predicate and $\mathcal{R}_0 = \mathcal{R}_{\mathcal{P}_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} \cup \{pred(p_1, \dots, p_n) \Rightarrow pred'(p_1, \dots, p_n)\}$. Indeed, $\sigma pred(p_1, \dots, p_n)$ is derivable from $\mathcal{R}_{\mathcal{P}_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}}$ if and only if $\sigma pred'(p_1, \dots, p_n)$ is derivable from $\mathcal{R}_0$, so by Theorem 3.2, if and only if $\sigma pred'(p_1, \dots, p_n)$ is derivable from saturate($\mathcal{R}_0$), so if and only if there exist a clause $H \Rightarrow pred(p'_1, \dots, p'_n)$ in $\text{solve}_{\mathcal{P}_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} (pred(p_1, \dots, p_n))$ and a substitution $\sigma'$ such that $\sigma' pred(p'_1, \dots, p'_n) = \sigma pred(p_1, \dots, p_n)$ and $\sigma' H$ is derivable from saturate($\mathcal{R}_0$). In particular, if $\text{solve}_{\mathcal{P}_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} (\text{attacker}(p)) = \emptyset$, then attacker($p$) is not derivable from $\mathcal{R}_{\mathcal{P}_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}}$. Moreover, if the selection function is $sel_0$ and $\text{solve}_{\mathcal{P}_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} (\text{attacker}(p))$ is non-empty, then at least one instance of attacker($p$) is derivable. Indeed, in that case $\text{solve}_{\mathcal{P}_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} (\text{attacker}(p))$ contains a clause $R = H \Rightarrow \text{attacker}(\sigma p)$ with $sel_0(R) = \emptyset$, so the hypothesis $H$ contains facts of the form attacker($x$) and disequalities. Consider a substitution $\sigma'$ that maps each variable to $b_0[M]$ for a distinct closed term $M$. Any fact $\sigma' \text{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$, $\sigma' F$ holds. Hence $\sigma' H$ is derivable, so $\text{attacker}(\sigma' \sigma 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.

Blanchet and Podelski, 2005 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 \to B : aenc((c_1, \text{sign}((c_0, k), ssk_A)), pk_B)$

Message 2. $B \to A : \text{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 (Abadi and Needham, 1996): 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 (Heather et al., 2000), 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 shared-key protocol (Needham and Schroeder, 1978). 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 \to A : \text{senc}(b, k)$

Message 5. $A \to B : \text{senc}(b-1, k)$
where $b$ is a nonce. Representing $b-1$ using a function $\text{minusone}(x) = x-1$, the algorithm does not terminate. Indeed, the output of message 5 is represented by a clause of the form:

$$H \wedge \text{attacker}(\text{senc}(x, y)) \Rightarrow \text{attacker}(\text{senc}(\text{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

$$\text{attacker}(\text{senc}(x, M_k)) \Rightarrow \text{attacker}(\text{senc}(\text{minusone}(x), M_k)) \quad (\text{Loop})$$

for some term $M_k$ that represents the key $k$.

The fact $\text{attacker}(\text{senc}(\text{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: $\text{attacker}(\text{senc}(\text{minusone}(\text{minusone}(M_b)), M_k))$. This fact can again be resolved with (Loop), so that we obtain a cycle that derives $\text{attacker}(\text{senc}(\text{minusone}^n(M_b), M_k))$ for all $n$.

When tags are added, the clause (Loop) becomes:

$$\text{attacker}(\text{senc}((c_1, x), M_k)) \Rightarrow \text{attacker}(\text{senc}((c_2, \text{minusone}(x)), M_k)) \quad (\text{NoLoop})$$

and the previous loop disappears because $c_2$ does not unify with $c_1$. The fact $\text{attacker}(\text{senc}((c_2, \text{minusone}(M_b)), M_k))$ is derived, without yielding a loop.

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. Arapinis and Duflot, 2007 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 Ramanujam and Suresh, 2003, still forbidding blind copies. Comon-Lundh and Cortier, 2003 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 Blanchet and Podelski, 2005 puts no limit on the number of blind copies, but requires tagging.

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, Goubault-Larrecq, 2005 shows that one can abstract the clauses into clauses in the decidable class $\mathcal{H}_1$, by losing some relational information on the messages.

## 3.3 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, \mathcal{P} \cup \{\text{event}(M); P\} \to E, \mathcal{P} \cup \{P\} \qquad (\text{Red Event})$$

The $\mathcal{N}_{\text{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, \mathcal{P}_0 \to^* E', \mathcal{P}'$ executes event `M` if and only if it contains a reduction $E, \mathcal{P} \cup \{\text{event}(M); P\} \to E, \mathcal{P} \cup \{P\}$ for some $E, \mathcal{P}$, and $P$.

The correspondence `event(M) \rightsquigarrow \bigvee_{j=1}^{m} \bigwedge_{k=1}^{l_j} event(M_{jk})` means intuitively that, if event `M` has been executed, then there exists `j` such that events $M_{j1}, \dots, 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}, \dots, M_{jl_j}$ that do not appear in $M$ such that events $M_{j1}, \dots, M_{jl_j}$ have been executed. The formal definition is as follows:

**Definition 3.5.** The closed process $P_0$ satisfies the correspondence

$$ \text{event}(M) \rightsquigarrow \bigvee_{j=1}^{m} \bigwedge_{k=1}^{l_j} \text{event}(M_{jk}) $$

against $\mathcal{N}_{\text{pub}}$-adversaries if and only if, for some $\mathcal{N}_{\text{priv}}$ disjoint from $\mathcal{N}_{\text{pub}}$ such that $\text{fn}(P_0) \cup \text{fn}(M) \cup \bigcup_{j,k} \text{fn}(M_{jk}) \subseteq \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$, for any $\mathcal{N}_{\text{pub}}$-adversary $Q$, for any trace $\text{Tr} = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \{P_0, Q\} \to^* E', P'$, for any substitution $\sigma$, if $\text{Tr}$ executes event $\sigma M$, then there exist $\sigma'$ and $j \in \{1, \dots, m\}$ such that $\sigma'M = \sigma M$ and, for all $k \in \{1, \dots, l_j\}$, $\text{Tr}$ executes event $\sigma'M_{jk}$.

**Example 3.3.** For example, we can modify the process $P_0$ of §2.2 by adding events as follows:

$$
\begin{align*}
P_0 &= \text{new ssk}_A : \text{skey}; \text{new sk}_B : \text{skey}; \text{let spk}_A = \text{pk}(ssk_A) \text{ in} \\
    &\quad \text{let pk}_B = \text{pk}(sk_B) \text{ in out}(c, spk_A); \text{out}(c, pk_B); \\
    &\quad (P_A(spk_A, ssk_A) | P_B(pk_B, sk_B, spk_A)) \\
P_A(spk_A, ssk_A) &= \! \text{in}(c, x_{pk_B} : \text{pkey}); \text{new k : key}; \\
    &\quad \text{event}(e_A(spk_A, x_{pk_B}, k)); \\
    &\quad \text{out}(c, \text{aenc}(\text{sign}(k2b(k), ssk_A), x_{pk_B})); \\
    &\quad \text{in}(c, x : \text{bitstring}); \text{let } z = \text{sdec}(x, k) \text{ in } 0 \\
P_B(pk_B, sk_B, spk_A) &= \! \text{in}(c, y : \text{bitstring}); \text{let } y' = \text{adec}(y, sk_B) \text{ in} \\
    &\quad \text{let } x_k = \text{b2k}(\text{check}(y', spk_A)) \text{ in} \\
    &\quad \text{event}(e_B(spk_A, pk_B, x_k)); \text{out}(c, \text{senc}(s, x_k))
\end{align*}
$$

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 $\text{event}(e_B(x, y, z)) \rightsquigarrow \text{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 $\text{event}(e_1(x)) \rightsquigarrow \text{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 $\text{event}(p)$ means that event $p$ (more formally, event $M$ with corresponding pattern $p$) may have been executed. We generate clauses $\text{message}(p_1, p'_1) \wedge \dots \wedge \text{message}(p_n, p'_n) \Rightarrow \text{event}(p)$ when the process executes event $p$ after receiving messages $p'_1, \dots, p'_n$ on channels $p_1, \dots, 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

$$ \texttt{in}(c, x); \text{event}(e_1(x)) \mid \texttt{in}(c, x'); \text{event}(e_2(x')) $$

may execute $e_1(x)$ and $e_2(x)$ for all $x$ that the adversary has, but the correspondence $\text{event}(e_1(x)) \rightsquigarrow \text{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 $\text{event}(e_1(x)) \rightsquigarrow \text{event}(e_2(x))$, we check that only events $e_1(p)$ for $p$ such that $e_2(p) \in 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) \in 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*₀) is true if and only if *p*₀ ∈ *Ev*. We generate clauses **message**(*p*₁, *p*₁') ∧ ... ∧ **message**(*p*ₙ, *p*ₙ') ∧ **m-event**(*p*₀) ⇒ **message**(*p*, *p*') when the process outputs *p*' on channel *p* after executing event *p*₀ and receiving messages *p*₁', ..., *p*ₙ' on channels *p*₁, ..., *p*ₙ respectively. In other words, the output of *p*' on channel *p* can be executed only when **m-event**(*p*₀) is true, that is, *p*₀ ∈ *Ev*.

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

$$ \llbracket \mathit{event}(M); P \rrbracket \rho s H = \llbracket P \rrbracket \rho s (H \wedge \mathit{m-event}(\rho(M))) \cup \\ \{H \wedge \mathit{m-event}(\rho(M)) \Rightarrow \mathit{event}(\rho(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*₂ 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*₁ 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 $\mathcal{F}_{\text{me}} = \{\text{m-event}(*p) | *p \in Ev\}$, Theorem 3.2 becomes:

**Theorem 3.3.** Let $F$ be a closed fact. The fact $F$ is derivable from $\mathcal{R}_0 \cup \mathcal{F}_{\text{me}}$ if and only if it is derivable from **saturate**($\mathcal{R}_0$) $\cup$ $\mathcal{F}_{\text{me}}$.

As for secrecy, we define $\mathcal{R}_0 = \mathcal{R}_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} \cup \{\text{pred}(p_1, \dots, p_n) \Rightarrow \text{pred}'(p_1, \dots, p_n)\}$. We have that $\sigma\text{pred}(p_1, \dots, p_n)$ is derivable from
$\mathcal{R}_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} \cup \mathcal{F}_{\text{me}}$ if and only if there exist a clause $H \Rightarrow \text{pred}(p'_1, \dots, p'_n)$ in $\text{solve}_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}}(\text{pred}(p_1, \dots, p_n))$ and a substitution $\sigma'$ such that $\sigma'\text{pred}(p'_1, \dots, p'_n) = \sigma\text{pred}(p_1, \dots, p_n)$ and $\sigma' H$ is derivable from $\text{saturate}(\mathcal{R}_0) \cup \mathcal{F}_{\text{me}}$. Since no clause outside $\mathcal{F}_{\text{me}}$ concludes m-event facts, the m-event facts in $\sigma' H$ must be in $\mathcal{F}_{\text{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 $\mathcal{N}_{\text{pub}}$ be a set of names. Let $M, M_{jk}$ ($j \in \{1, \dots, m\}, k \in \{1, \dots, 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 $\mathcal{N}_{\text{priv}}$ be a set of names disjoint from $\mathcal{N}_{\text{pub}}$ such that $\text{fn}(P_0) \cup \text{fn}(M) \cup \bigcup_{j,k} \text{fn}(M_{jk}) \subseteq \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$. Suppose that, for all clauses $R \in \text{solve}_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}}(\text{event}(p))$, there exist $j \in \{1, \dots, m\}$, $\sigma'$ and $H$ such that $R = H \wedge \text{m-event}(\sigma'p_{j1}) \wedge \dots \wedge \text{m-event}(\sigma'p_{jl_j}) \Rightarrow \text{event}(\sigma'p)$. Then $P_0$ satisfies the correspondence $\text{event}(M) \rightsquigarrow \bigvee_{j=1}^m \bigwedge_{k=1}^{l_j} \text{event}(M_{jk})$ against $\mathcal{N}_{\text{pub}}$-adversaries.

This result is a particular case of Blanchet, 2009, Theorem 4. Intuitively, if all clauses are of the form $H \wedge \text{m-event}(\sigma'p_{j1}) \wedge \dots \wedge \text{m-event}(\sigma'p_{jl_j}) \Rightarrow \text{event}(\sigma'p)$, then, in order to derive $\text{event}(\sigma'p)$, the facts $\text{m-event}(\sigma'p_{j1}), \dots, \text{m-event}(\sigma'p_{jl_j})$ must be true, so in order to execute event $\sigma'p$, the events $\sigma'p_{j1}, \dots, \sigma'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 $\text{solve}_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}}(\text{event}(e_B(x, y, z)))$ contains

$$ \begin{aligned} & \text{m-event}(e_A(\text{pk}(\text{ssk}_A[]), \text{pk}(y'), k[i, \text{pk}(y')])) \wedge \text{attacker}(y') \\ & \Rightarrow \text{event}(e_B(\text{pk}(\text{ssk}_A[]), \text{pk}(sk_B[]), k[i, \text{pk}(y')])) . \end{aligned} $$

This clause prevents us from applying Theorem 3.4 to prove the correspondence $\text{event}(e_B(x, y, z)) \rightsquigarrow \text{event}(e_A(x, y, z))$, because the fact $\text{m-event}(e_A(\text{pk}(\text{ssk}_A[]), \text{pk}(y'), k[i, \text{pk}(y')]))$ contains $\text{pk}(y')$ instead of $\text{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 $\text{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,

$$ \text{solve}_{P_0, \mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}} (\text{event}(e_B(x, y, z))) = \\ \{\text{m-event}(e_A(\text{pk}(ssk_A[])), \text{pk}(sk_B[]), k[i, \text{pk}(sk_B[]))) \Rightarrow \\ \text{event}(e_B(\text{pk}(ssk_A[])), \text{pk}(sk_B[]), k[i, \text{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.
## 3.4 Equivalences

The notion of process equivalence is the main reasoning tool introduced initially with the spi calculus (Abadi and Gordon, 1999; Abadi and Gordon, 1998) and the applied pi calculus (Abadi and Fournet, 2001; Abadi et al., 2016), 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 (Hüttel, 2003; Abadi and Cortier, 2006), so automated techniques are incomplete. For a bounded number of sessions, several tools can decide trace equivalence: SPEC (Tiu and Dawson, 2010) for fixed primitives and without else branches, APTE (Cheval et al., 2011) for fixed primitives with else branches and non-determinism, and AKISS (Chadha et al., 2012; Ciobâcă, 2011) 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 Baudet, 2007 and Arapinis et al., 2014, relies on the semantics with configurations while our previous work (Blanchet, 2004; Blanchet et al., 2008) uses a semantics closer to the applied pi calculus (see Chapter 4).

We consider configurations $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\mathcal{P}$ as equal modulo any bijective renaming of names that leaves names in $\mathcal{N}_{\text{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 $\mathcal{C} = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P}$ can output on a channel $N$, denoted, $\mathcal{C} \downarrow_N$, if there exists $\text{out}(N, M); P \in \mathcal{P}$ with $\text{fn}(N) \subseteq \mathcal{N}_{\text{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 $\text{new } \tilde{n}; (\_ | Q)$ with $\text{fv}(Q) = \emptyset$ and all function symbols in $Q$ are public. When $\mathcal{C} = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P}$ and $C[\_] = \text{new } \tilde{n}; (\_ | Q)$ is an adversarial context, we define the application of context $C[\_]$ to the configuration $\mathcal{C}$ by $C[\mathcal{C}] = ((\mathcal{N}_{\text{pub}} \cup \text{fn}(Q)) \setminus \{\tilde{n}\}, \mathcal{N}_{\text{priv}} \cup \{\tilde{n}\}), \mathcal{P} \cup \{Q\}$, after renaming the names in $\mathcal{N}_{\text{priv}}$ so that $\mathcal{N}_{\text{priv}} \cap \text{fn}(Q) = \emptyset$. The condition $\mathcal{N}_{\text{priv}} \cap \text{fn}(Q) = \emptyset$ avoids clashes between the private names of the configuration $\mathcal{C}$ and the names of the adversary. To compute $C[\mathcal{C}]$, we add the process $Q$ to the multiset $\mathcal{P}$ of processes of the configuration $\mathcal{C}$, so that $Q$ runs in parallel with these processes. The free names of $Q$ are public, so we add them to $\mathcal{N}_{\text{pub}}$. Further, we apply the restriction $\text{new } \tilde{n}$ by moving the names $\tilde{n}$ from $\mathcal{N}_{\text{pub}}$ to $\mathcal{N}_{\text{priv}}$.

**Definition 3.6 (Observational equivalence).** *Observational equivalence* between configurations $\approx$ is the largest symmetric relation $\mathcal{R}$ between valid configurations such that $\mathcal{C} \mathcal{R} \mathcal{C}'$ implies:

1. if $\mathcal{C} \downarrow_a$, then $\mathcal{C}' \to^* \downarrow_a$, for all names $a$;

2. if $\mathcal{C} \to \mathcal{C}_1$, then $\mathcal{C}' \to^* \mathcal{C}'_1$ and $\mathcal{C}_1 \mathcal{R} \mathcal{C}'_1$, for some $\mathcal{C}'_1$.

3. $\mathcal{C}[\mathcal{C}] \mathcal{R} \mathcal{C}[\mathcal{C}']$ for all adversarial contexts $\mathcal{C}[\_]$.

We define observational equivalence on semantic configurations. Item 1 guarantees that, if a configuration $\mathcal{C}$ emits on a public channel, then so does $\mathcal{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) (Blanchet, 2004): 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 $\mathcal{N}_{\text{priv}}$ if and only if for all closed terms $M$ and $N$ with $(fn(M) \cup fn(N)) \cap \mathcal{N}_{\text{priv}} = \emptyset$, for some $\mathcal{N}_{\text{pub}}$ disjoint from $\mathcal{N}_{\text{priv}}$ such that $fn(P_0) \cup fn(M) \cup fn(N) \subseteq \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$, we have $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), P_0\{M/s\} \approx (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{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 (Pottier and Simonet, 2002; Pottier, 2002) 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 $\text{diff}[M, M']$ for terms and $\text{diff}[D, D']$ for expressions. The $\mathcal{N}_{\text{pub}}$-adversaries and the adversarial contexts do not contain $\text{diff}$. Given a biprocess $P$, we define two processes $\text{fst}(P)$ and $\text{snd}(P)$, as follows: $\text{fst}(P)$ is obtained by replacing all occurrences of $\text{diff}[M, M']$ with $M$ and $\text{diff}[D, D']$ with $D$ in $P$, and $\text{snd}(P)$ is obtained by replacing $\text{diff}[M, M']$ with $M'$ and $\text{diff}[D, D']$ with $D'$ in $P$. We define $\text{fst}(M)$, $\text{snd}(M)$, $\text{fst}(D)$, and $\text{snd}(D)$ similarly. We naturally extend $\text{fst}$ and $\text{snd}$ to multisets of processes, and to configurations by $\text{fst}(E, \mathcal{P}) = E, \text{fst}(\mathcal{P})$ and $\text{snd}(E, \mathcal{P}) = E, \text{snd}(\mathcal{P})$. Our goal is to show that the processes $\text{fst}(P)$ and $\text{snd}(P)$ are observationally equivalent.

**Definition 3.8.** The closed biprocess $P_0$ satisfies observational equivalence with private names $\mathcal{N}_{\text{priv}}$ if and only if, for some $\mathcal{N}_{\text{pub}}$ disjoint from $\mathcal{N}_{\text{priv}}$ such that $\text{fn}(P_0) \subseteq \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$, we have that $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\{\text{fst}(P_0)\} \approx (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\{\text{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, \mathcal{P} \cup \{ \text{out}(N, M); Q, \text{in}(N', x); P \} \rightarrow E, \mathcal{P} \cup \{ Q, P\{M/x\} \} $$
$$ \text{if } \text{fst}(N) = \text{fst}(N') \text{ and } \text{snd}(N) = \text{snd}(N') \qquad \text{(Red I/O)} $$

$$ E, \mathcal{P} \cup \{ \text{let } x = D \text{ in } P \text{ else } Q \} \rightarrow E, \mathcal{P} \cup \{ P\{\text{diff}[M, M']/x\} \} $$
$$ \text{if } \text{fst}(D) \Downarrow M \text{ and } \text{snd}(D) \Downarrow M' \qquad \text{(Red Eval 1)} $$

$$ E, \mathcal{P} \cup \{ \text{let } x = D \text{ in } P \text{ else } Q \} \rightarrow E, \mathcal{P} \cup \{ Q \} $$
$$ \text{if } \text{fst}(D) \Downarrow \text{fail} \text{ and } \text{snd}(D) \Downarrow \text{fail} \qquad \text{(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 = \text{istrue}(M)$ in $P$ else $Q$, where $x$ is a fresh variable and $\text{istrue}(\text{bool}) : \text{bool}$ is a destructor defined by the rewrite rule $\text{istrue}(\text{true}) \rightarrow \text{true}$. A biprocess $P$ reduces by this semantics when its two components $\text{fst}(P)$ and $\text{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 \rightarrow C'$, then $\text{fst}(C) \rightarrow \text{fst}(C')$ and $\text{snd}(C) \rightarrow \text{snd}(C')$.
When the two components do not reduce in the same way, we say that the configuration $\mathcal{C}$ diverges, and we write $\mathcal{C} \uparrow$ (vocabulary and notation from (Baudet, 2007)):

$$ E, \mathcal{P} \cup \{ \text{out}(N, M); Q, \text{in}(N', x); P \} \uparrow \qquad (\text{Div I/O}) \\ \text{if } (\text{fst}(N) = \text{fst}(N')) \not\iff (\text{snd}(N) = \text{snd}(N')) $$

$$ E, \mathcal{P} \cup \{ \text{let } x = D \text{ in } P \text{ else } Q \} \uparrow \qquad (\text{Div Eval}) \\ \text{if } \text{fst}(D) \downarrow \text{fail} \not\iff \text{snd}(D) \downarrow \text{fail} $$

When the configuration $\mathcal{C}$ does not diverge, the two components always reduce in the same way, that is, the biprocess reduces. Formally, if $\mathcal{C}$ does not diverge and $\text{fst}(\mathcal{C}) \to \mathcal{C}_1$, then $\mathcal{C} \to \mathcal{C}'$ and $\mathcal{C}_1 = \text{fst}(\mathcal{C}')$ for some $\mathcal{C}'$, and similarly for $\text{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 $\mathcal{N}_{\text{priv}}$ be a set of names. The biprocess $P_0$ satisfies *diff-equivalence* with private names $\mathcal{N}_{\text{priv}}$ if, for some $\mathcal{N}_{\text{pub}}$ disjoint from $\mathcal{N}_{\text{priv}}$ such that $\text{fn}(P_0) \subseteq \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$, for all $\mathcal{N}_{\text{pub}}$-adversaries $Q$, there exists no configuration $\mathcal{C}$ such that $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \{P_0, Q\} \to^* \mathcal{C} \uparrow$.

Diff-equivalence implies observational equivalence, as shown by the following theorem:

**Theorem 3.5.** Let $P_0$ be a closed biprocess and $\mathcal{N}_{\text{priv}}$ be a set of names. If $P_0$ satisfies *diff-equivalence* with private names $\mathcal{N}_{\text{priv}}$, then $P_0$ satisfies observational equivalence with private names $\mathcal{N}_{\text{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 $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), P \approx (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), P'$, then the biprocess if *diff*[true, false] then $P$ else $P'$ satisfies observational equivalence with private names $\mathcal{N}_{\text{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*₁, *p*₂) and **message'**(*p*₁, *p*'_₁, *p*₂, *p*'_₂'), where com-
ponents 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*₁, *p*₂) means that, by the same actions, the adversary
obtains *p*₁ by interacting with **fst**(*P*) and *p*₂ by interacting with **snd**(*P*).
The fact **message'**(*p*₁, *p*'_₁, *p*₂, *p*'_₂') means that, by the same actions, **fst**(*P*)
sends message *p*'_₁ on channel *p*₁ while **snd**(*P*) sends message *p*'_₂ on chan-
nel *p*₂. We also use the fact **input'**(*p*₁, *p*₂) to express that an input on
channel *p*₁ may be executed by **fst**(*P*) while **snd**(*P*) executes an input
on *p*₂. (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 (Abdalla *et al.*, 2005). This property can be verified in ProVerif by replacing the final output of the process *P*<sub>B</sub> of §2.2 with

$$
\texttt{new } r \texttt{ : bitstring; out}(c, \texttt{senc}(\texttt{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*₁, *k*) and
**senc**(*r*₂, *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) \rightarrow x.$$

The fixed protocol is obtained by replacing the final output of the process $P_B$ of Example 2.5 with

$$\text{new } r : \text{bitstring}; \text{new } \textit{coins} : \text{rand}; \text{out}(c, \text{senc}(\text{diff}[s, r], x_k, \text{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\}$.

Baudet, 2007 shows the decidability of diff-equivalence for processes without replication, in a framework similar to ours. The protocol verifiers Maude-NPA (Santiago et al., 2014) and Tamarin (Basin et al., 2015) 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_{\text{priv}}$ a set of names. We say that $P_0$, with private names $N_{\text{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_{\text{priv}}$.

ProVerif can prove that the protocols EKE (Bellovin and Merritt, 1992) and Augmented EKE (Bellovin and Merritt, 1993) satisfy this property. This definition is in the line of work by Lowe, 2002; Cohen, 2002; Corin et al., 2003; Corin et al., 2004; Delaune and Jacquemard, 2004; Drielsma et al., 2005. Lowe, 2002 uses the model checker FDR to handle a bounded number of sessions. Delaune and Jacquemard, 2004 give a decision procedure in this case. Corin et al., 2004 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 Cheval and Blanchet, 2013, 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 `let x = D in out(c, M₁) else out(c, M₂)` can be transformed into `let x = catch-fail(D)` in `let m = ifthenelse(not-caught-fail(x), M₁, M₂)` in `out(c, m)`, where the destructors `catch-fail` and `not-caught-fail` are defined by the rewrite rules

$$ \begin{array}{l@{\qquad}l} \text{catch-fail}(x) & \rightarrow x & \text{not-caught-fail}(\text{caught-fail}) \rightarrow \text{false} \\ \text{catch-fail(fail)} & \rightarrow \text{caught-fail} & \text{not-caught-fail}(x) \rightarrow \text{true} \end{array} $$

and `caught-fail` is a new constant. After transformation, if $D$ succeeds, then $x$ has the same value as before, and $x \neq \text{caught-fail}$, so `not-caught-fail(x) = true` and `ifthenelse(not-caught-fail(x), M₁, M₂)` returns $M₁$; if $D$ fails, then $x = \text{caught-fail}$, `not-caught-fail(x) = false`, and `ifthenelse(not-caught-fail(x), M₁, M₂)` returns $M₂$.

**Example 3.7.** As in (Cheval and Blanchet, 2013), we consider a simplified version of the private authentication protocol by Abadi and Fournet, 2004. 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:

$$
\begin{align*}
A(sk_A, sk_B) &= \begin{array}{@{}l@{}} \texttt{new } a : \texttt{rand;} \\ \texttt{out}(c, \texttt{aenc}((a, \texttt{pk}(sk_A)), \texttt{pk}(sk_B))); \end{array} \\
\texttt{in}(c, x : \texttt{bitstring})
\end{align*}
$$

$$
\begin{align*}
B(sk_B, sk_A) &= \begin{array}{@{}l@{}}
    \texttt{in}(c, y : \texttt{bitstring}); \texttt{new } b : \texttt{rand}; \\
    \quad \texttt{let } (xa : \texttt{rand}, xpk}_A : \texttt{pkey}) = \texttt{adec}(y, sk_B) \texttt{ in} \\
    \quad (*) \quad \begin{array}{@{}l@{}}
        \texttt{if } xpk}_A = \texttt{pk}(sk_A) \texttt{ then} \\
        \qquad \texttt{out}(c, \texttt{aenc}((xa, b, \texttt{pk}(sk_B)), \texttt{pk}(sk_A))); \\
        \qquad \texttt{else } \texttt{out}(c, \texttt{aenc}(b, \texttt{pk}(sk_B))); \\
        \qquad \texttt{else } \texttt{out}(c, \texttt{aenc}(b, \texttt{pk}(sk_B))); \end{array}
    \end{array}
\end{align*}
$$

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

$$
\begin{align*}
& \texttt{new sk}_A : \texttt{skey}; \texttt{new sk}'_A : \texttt{skey}; \texttt{new sk}_B : \texttt{skey}; \\
& \texttt{out}(c, (\texttt{pk}(sk}_A), (\texttt{pk}(sk}'_A), (\texttt{pk}(sk}_B)); B(sk}_B, \texttt{diff}[sk}_A, sk}'_A]
\end{align*}
$$

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 $\text{aenc}((a, \text{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

$$ 
\begin{aligned}
B'(sk_B, sk_A) = & \text{in}(c, y : \text{bitstring}); \text{new } b : \text{rand}; \\
& \text{let } (xa : \text{rand}, xpk_A : \text{pkey}) = \text{adec}(y, sk_B) \text{ in} \\
& \quad \text{out}(c, \text{ifthenelse}(\text{equal}(xpk_A, \text{pk}(sk_A)), \\
& \quad \quad \text{aenc}((xa, b, \text{pk}(sk_B)), \text{pk}(sk_A)), \\
& \quad \quad \text{aenc}(b, \text{pk}(sk_B)))) \\
& \quad \text{else } \text{out}(c, \text{aenc}(b, \text{pk}(sk_B)))
\end{aligned}
$$

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 (Cheval and Blanchet, 2013).

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, \text{diff}[v_A, v_B]) | V(id_B, \text{diff}[v_B, v_A]) \quad (3.6) $$

satisfies observational equivalence, which means that an adversary cannot distinguish when two voters swap their votes (Delaune et al., 2009). 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 Delaune et al., 2008 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) = \text{out}(c, id_A); \text{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) = \text{out}(c, id_A); \text{sync } 1; \text{out}(c, v_A). \qquad (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 = \text{out}(c, id_A); \text{sync } 1; \text{out}(c, \text{diff}[v_A, v_B]) \\ | \text{out}(c, id_B); \text{sync } 1; \text{out}(c, \text{diff}[v_B, v_A]). \qquad (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 diff-equivalence 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_{\text{priv}} = \emptyset$, $N_{\text{pub}} = \{c, id_A, id_B, v_A, v_B\}$, $P_0$ as in (3.8), and $Q = \text{in}(c, x)$; $\text{in}(c, y)$; $\text{in}(c, x')$; $\text{in}(c, y')$; let $x'' = \text{istrue}(x' = v_A)$ in out($c$, $v_A$). The configuration ($N_{\text{pub}}, N_{\text{priv}}$), $\{P_0, Q\}$ reduces into ($N_{\text{pub}}, N_{\text{priv}}$), $\{\text{let } x'' = \text{istrue}(\text{diff}[v_A, v_B] = v_A) \text{ 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 $\text{istrue}(\text{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:

$$
\begin{array}{l}
\mathit{out}(c, \mathit{id}_A); \mathit{sync} \ 1; \mathit{out}(c, \mathit{diff}[v_A, v_A]) \\
\mid \\
\mathit{out}(c, \mathit{id}_B); \mathit{sync} \ 1; \mathit{out}(c, \mathit{diff}[v_B, v_B])
\end{array}
$$

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.

3.5 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

$$ \begin{aligned} \text{let } x &= \text{diff}[\text{aenc}(\text{sign}(a, sk_A), \text{pk}(sk_B)), \text{aenc}(a, \text{pk}(sk_A))] \text{ in} \\ \text{let } y &= \text{adec}(x, sk_A) \text{ in } \text{let } z = \text{check}(y, \text{pk}(sk_B)) \text{ in } \text{out}(c, z) \end{aligned} $$

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:

$$ \begin{aligned} \text{let } x &= \text{diff}[\text{aenc}(\text{sign}(a, sk_A), \text{pk}(sk_B)), \text{aenc}(a, \text{pk}(sk_A))] \text{ in} \\ \text{let } z &= \text{check}(\text{adec}(x, sk_A), \text{pk}(sk_B)) \text{ in } \text{out}(c, z) \end{aligned} $$

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 (Cheval and Blanchet, 2013). However, grouping them manually in the initial process avoids the first failed proof attempt and yields better performance.
Link with the Applied Pi Calculus

The input language of ProVerif is a dialect of the applied pi calculus introduced by Abadi and Fournet, 2001, and later updated by Abadi et al., 2016. 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
<table><caption>**Figure 4.1:** Syntax of the applied pi calculus</caption><tr><td>P, Q, R ::=</td><td>processes (or plain processes)</td></tr><tr><td>0</td><td>null process</td></tr><tr><td>P | Q</td><td>parallel composition</td></tr><tr><td>!P</td><td>replication</td></tr><tr><td>vn.P</td><td>name restriction ("new")</td></tr><tr><td>if M = N then P else Q</td><td>conditional</td></tr><tr><td>N(x).P</td><td>message input</td></tr><tr><td>N&#773;⟨M⟩.P</td><td>message output</td></tr></table>

processes:

```
[[0]] = 0
[[P | Q]] = [[P]] | [[Q]]
[[!P]] = ![[P]]
[[new n : T; P]] = vn.[[P]]
[[if M = N then P else Q]] = if M = N then [[P]] else [[Q]]
[[in(N, x : T); P]] = N(x).[[P]]
[[out(N, M); P]] = N&#773;⟨M⟩.[[P]]
```

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 (Abadi et al., 2016), 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 $\vdash M : T$ when $M$ is a term of sort $T$ and $\vdash 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 $\Gamma$ and in the process $P$ matches its sort in the applied pi calculus, then $\Gamma \vdash M : T$ if and only if $\vdash M : T$, and $\Gamma \vdash P$ if and only if $\vdash [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.

In contrast to the semantics of ProVerif, the operational semantics of the applied pi calculus is defined by a reduction relation $\rightarrow_{\diamond}$ on processes. To prepare processes for reduction, we use a structural equivalence relation $\cong$. 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 $\cong$ is the smallest equivalence relation on processes closed by application of evaluation contexts such that

PAR-0 $P | 0 \cong P$
PAR-A $P | (Q | R) \cong (P | Q) | R$
PAR-C $P | Q \cong Q | P$
REPL !P $\cong P | !P$
NEW-0 $\nu n. 0 \cong 0$
NEW-C $\nu n. \nu n'. P \cong \nu n'. \nu n. P$
NEW-PAR $P | \nu n. Q \cong \nu n. (P | Q)$ when $n \notin \mathit{fn}(P)$
REWRITE $P^{M/x} \cong P^{N/x}$ when $M =_{\varepsilon} 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 $\rightarrow_{\diamond}$ is the smallest relation on processes closed by $\cong$ and by
application of evaluation contexts such that:

COMM $\overline{N}\langle M \rangle.P | N(x).Q \to_{\diamond} P | Q^{M/x}$

THEN if $M = M$ then $P$ else $Q \to_{\diamond} P$

ELSE if $M = N$ then $P$ else $Q \to_{\diamond} Q$
for any ground terms $M$ and $N$ such that $M \neq_{\epsilon} 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:

$$ \llbracket (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P} \rrbracket = \nu \tilde{a}. (\llbracket P_1 \rrbracket | \dots | \llbracket P_n \rrbracket) $$

where $\mathcal{N}_{\text{priv}} = \{\tilde{a}\}$ and $\mathcal{P} = \{P_1, \dots, P_n\}$. In particular, $\llbracket (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P} \rrbracket = \nu \tilde{a}.0$ when $\mathcal{P} = \emptyset$. The encoding of configurations is unique modulo $\hat{=}$. More formally, $\llbracket (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P} \rrbracket$ is a set of processes, containing all processes of the form $\nu \tilde{a}. (\llbracket P_1 \rrbracket | \dots | \llbracket P_n \rrbracket)$ with any ordering of $\tilde{a}$ and any parallel composition of $\llbracket P_1 \rrbracket, \dots, \llbracket P_n \rrbracket$ modulo associativity and commutativity. The results below hold for any element of $\llbracket \mathcal{C} \rrbracket$.

The next proposition formally relates the two semantics. It is proved in Appendix B, together with the other results of this chapter.

**Proposition 4.1.** If $C \to^{*} C'$, then $\llbracket C \rrbracket \to_{\diamond} \hat{=} \llbracket C' \rrbracket$.

Conversely, if $\llbracket C \rrbracket \to_{\diamond} \hat{*} P'$, then $C \to^{*} C'$ and $P' \hat{=} \llbracket C' \rrbracket$ for some $C'$.

Next, we define observational equivalence in the applied pi calculus. We write $P \downarrow_{a}^{\diamond}$ when $P$ can send a message on name $a$, that is, when $P \to_{\diamond} \hat{=} C[\bar{a}\langle M \rangle.Q]$ for some evaluation context $C[\_]$ that does not bind $a$.

**Definition 4.1.** An observational bisimulation is a symmetric relation $\mathcal{R}$ between closed processes such that $P \mathcal{R} Q$ implies:

1. if $P \downarrow_{a}^{\diamond}$, then $Q \downarrow_{a}^{\diamond}$;

2. if $P \to_{\diamond} \hat{*} P'$ and $P'$ is closed, then $Q \to_{\diamond} \hat{*} Q'$ and $P' \mathcal{R} Q'$ for some $Q'$;
3. $C[P] \mathcal{R} C[Q]$ for all closed evaluation contexts $C[\_].$

Observational equivalence ($\hat{\approx}$) 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 \downarrow_N$ needs to be adapted in the presence of equations, because the channel $N$ is modulo the equational theory. We have ($\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}$), $P \downarrow_N$ if and only if there exists $\text{out}(N', M)$; $P \in \mathcal{P}$ with $N =_{\mathcal{E}} N'$ and $\text{fn}(N) \subseteq \mathcal{N}_{\text{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 \approx C'$, then $[[C]] \stackrel{\approx}{=} [[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 $\approx$. 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.

**Proposition 4.3.** Let $C$ and $C'$ be valid configurations. If $[[C]] \stackrel{\approx}{=} [[C']]$,
then $C \approx C'$.
This chapter outlines a number of applications and extensions of
ProVerif.

5.1 Case studies

ProVerif can successfully prove secrecy and authentication properties
for many protocols of the literature (Blanchet, 2009): no false attack is
found in the 19 protocols tested in (Blanchet, 2009). 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 Aiello et al., 2004, 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 equiva-
lences.

* Blanchet and Chaudhuri, 2008 study the secure filesystem Plutus (Kallahalla et al., 2003), discovering and fixing weaknesses of the initial system.

* ProVerif was also used for verifying a certified email web service (Lux et al., 2005), a certified mailing-list protocol (Khurana and Hahm, 2006), e-voting protocols (Kremer and Ryan, 2005; Backes et al., 2008a; Delaune et al., 2009; Cortier and Wiedling, 2012), e-auction protocols (Dreier et al., 2013), the ad-hoc routing protocol ARAN (*Authenticated Routing for Adhoc Networks*) (Godskesen, 2006), zero-knowledge protocols (Backes et al., 2008b; Backes et al., 2015), the Trusted Platform Module (TPM) (Delaune et al., 2011), and the associated Direct Anonymous Attestation protocol (Backes et al., 2008b; Smyth et al., 2015), for instance.

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

* Canetti and Herzog, 2006 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 equiva-
lence properties shown by ProVerif. To achieve this result, they
take advantage that ProVerif relies on a trace property on bipro-
cesses in order to prove equivalence, so they can leverage compu-
tational soundness results for trace properties.

5.2 Extensions

Other authors also design and implement extensions of ProVerif:
* Küsters and Truderung, 2008; Küsters and Truderung, 2009 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 (Arapinis et al., 2011) 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 (Mödersheim, 2010), then extended by providing a translation from an extension of the pi calculus (Bruni et al., 2015).

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

## 5.3 ProVerif as back-end

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

* Bhargavan et al., 2004 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.

* Bhargavan et al., 2006 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 (Bhargavan et al., 2008) and the TPM (Mukhamedov
et al., 2013), in particular, were studied using this technique.

* The JavaSPI framework (Avalle et al., 2011) 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.

* Aizatulin et al., 2011 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.

* Bansal et al., 2012; Bansal et al., 2013 build the Web-spi library, which allows them to model web security mechanisms and protocols and verify them using ProVerif.
## 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