A method for unbounded verification of privacy-type properties

Abstract

In this paper, we consider the problem of verifying anonymity and unlinkability in the symbolic model, where protocols are represented as processes in a variant of the applied pi calculus, notably used in the $ProVerif$ tool. Existing tools and techniques do not allow to verify directly these properties, expressed as behavioral equivalences. We propose a different approach: we design two conditions on protocols which are sufficient to ensure anonymity and unlinkability, and which can then be effectively checked automatically using $ProVerif$ . Our two conditions correspond to two broad classes of attacks on unlinkability, i.e. data and control-flow leaks. This theoretical result is general enough that it applies to a wide class of protocols based on a variety of cryptographic primitives. In particular, using our tool, $UKano$ , we provide the first formal security proofs of protocols such as BAC and PACE (e-passport), Hash-Lock (RFID authentication), etc. Our work has also lead to the discovery of new attacks, including one on the LAK protocol (RFID authentication) which was previously claimed to be unlinkable (in a weak sense).

Keywords

Formal verification security protocols symbolic model equivalence-based properties

1. Introduction

Security protocols aim at securing communications over various types of insecure networks (e.g. web, wireless devices) where dishonest users may listen to communications and interfere with them. A secure communication has a different meaning depending on the underlying application. It ranges from the confidentiality of data (medical files, secret keys, etc.) to, e.g. verifiability in electronic voting systems. Another example of a security notion is privacy. In this paper, we focus on two privacy-related properties, namely unlinkability (sometimes called untraceability), and anonymity. These two notions are informally defined in the ISO/IEC standard 15408 [41] as follows:

Unlinkability aims at ensuring that a user may make multiple uses of a service or resource without others being able to link these uses together.

Anonymity aims at ensuring that a user may use a service or resource without disclosing its identity.

Both are critical for instance for Radio-Frequency Identification Devices (RFID) and are thus extensively studied in that context (see, e.g. [52] for a survey of attacks on this type of protocols), but they are obviously not limited to it.

One extremely successful approach when designing and analyzing security protocols is the use of formal verification, i.e. the development of rigorous frameworks and techniques to analyze protocols. This approach has notably lead to the discovery of a flaw in the Single-Sign-On protocol used e.g. by Google Apps. It has been shown that a malicious application could very easily access to any other application (e.g. Gmail or Google Calendar) of their users [9]. This flaw has been found when analyzing the protocol using formal methods, abstracting messages by a term algebra and using the $Avantssar$ validation platform. Another example is a flaw on vote-privacy discovered during the formal and manual analysis of an electronic voting protocol [32]. All these results have been obtained using formal symbolic models, where most of the cryptographic details are ignored using abstract structures. The techniques used in symbolic models have become mature and several tools for protocol verification are nowadays available, e.g. the $Avantssar$ platform [8], the $Tamarin$ prover [45], and the $ProVerif$ tool [17].

Unfortunately, most of these results and tools focus on trace properties, that is, statements that something bad never occurs on any execution trace of a protocol. Secrecy and authentication are typical examples of trace properties: a data remains confidential if, for any execution, the attacker is not able to produce the data. However, privacy properties like unlinkability and anonymity are generally not defined as trace properties. Instead, they are usually defined as the fact that an observer cannot distinguish between two situations, which requires a notion of behavioural equivalence. Based on such a notion of equivalence, several definitions of privacy-type properties have been proposed (e.g. [5,21] for unlinkability, and [10,34] for vote-privacy). In this paper, we consider the well-established definitions of strong unlinkability and anonymity as defined in [5]. They have notably been used to establish privacy for various protocols either by hand or using ad hoc encodings (e.g. eHealth protocol [36], mobile telephony [6,7]). We provide a brief comparison with alternative definitions in Section 3.3.

Considering an unbounded number of sessions, the problem of deciding whether a protocol satisfies an equivalence property is undecidable even for a very limited fragment of protocols (see, e.g. [28]). Bounding the number of sessions suffices to retrieve decidability for standard primitives (see, e.g. [14,27]). However, analysing a protocol for a fixed (often low) number of sessions does not allow to prove security. Moreover, in the case of equivalence properties, existing tools scale badly and can only analyse protocols for a very limited number of sessions, typically 2 or 3. Another approach consists in implementing a procedure that is not guaranteed to terminate. This is in particular the case of $ProVerif$ , a well-established tool for checking security of protocols. $ProVerif$ is able to check a strong notion of equivalence (called diff-equivalence) between processes that share the same structure. Despite recent improvements on diff-equivalence checking [26] intended to prove unlinkability of the BAC protocol (used in e-passport), $ProVerif$ still cannot be used off-the-shelf to establish unlinkability properties, and therefore cannot conclude on most of the case studies presented in Section 6. Recently, similar approaches have been implemented in two other tools, namely $Tamarin$ [13] and $Maude - NPA$ [49]. They are based on a notion of diff-equivalence, and therefore suffer from the same drawbacks.

Our contribution. We believe that looking at trace equivalence of any pair of protocols is a too general problem and that much progress can be expected when one focuses on a few privacy goals and a class of protocols only (yet large and generic enough). We follow this different approach. We aim at proposing sufficient conditions that can be automatically checked, and that imply unlinkability and anonymity for a large class of security protocols. The success of our solution will be measured by confronting it to many real-world case studies.

More precisely, we identify a large class of 2-party protocols (simple else branches, arbitrary cryptographic primitives) and we devise two conditions called frame opacity and well-authentication that imply unlinkability and anonymity for an unbounded number of sessions. We show how these two conditions can be automatically checked using e.g. the $ProVerif$ tool, and we provide tool support for that. Using our tool $UKano$ (built on top of $ProVerif$ ), we have automatically analysed several protocols, among them the Basic Access Control (BAC) protocol as well as the Password Authenticated Connection Establishment (PACE) protocol that are both used in e-passports. We notably establish the first proof of unlinkability for ABCDH [3] and for the BAC protocol followed by the Passive Authentication (PA) and Active Authentication (AA) protocols. We also report on an attack that we found on the PACE protocol, and another one that we found on the LAK protocol [43] whereas it is claimed untraceable in [52]. It happens that our conditions are rather tight, and we believe that the overall methodology and proof method could be used for other classes of protocols and other privacy goals.

Our sufficient conditions. We now give an intuitive overview of our two sufficient conditions, namely frame opacity and well-authentication. In order to do this, assume that we want to design a mutual authentication protocol between a tag T and a reader R based on symmetric encryption, and we want this protocol to be unlinkable. We assume that k is a symmetric key shared between T and R.

A first attempt to design such a protocol is presented using Alice & Bob notation as follows ( $n_{R}$ is a fresh nonce): $\begin{array}{l} 1 . R \to T : n_{R} \\ 2 . T \to R : {n_{R}}_{k} \end{array}$ This first attempt based on a challenge-response scheme is actually linkable. Indeed, an active attacker who systematically intercepts the nonce $n_{R}$ and replaces it by a constant will be able to infer whether the same tag has been used in different sessions or not by comparing the answers he receives. Here, the tag is linkable because, for a certain behaviour (possibly malicious) of the attacker, some relations between messages leak information about the agents that are involved in the execution. Our first condition, namely frame opacity, actually checks that all outputted messages have only relations that only depend on what is already observable. Such relations can therefore not be exploited by the attacker to learn anything new about the involved agents.

Our second attempt takes the previous attack into account and randomises the tag’s response and should achieve mutual authentication by requiring that the reader must answer to the challenge $n_{T}$ . This protocol can be as follows: $\begin{array}{l} 1 . R \to T : n_{R} \\ 2 . T \to R : {n_{R}, n_{T}}_{k} \\ 3 . R \to T : {n_{T}}_{k} \end{array}$ Here, Alice & Bob notation shows its limit. It does not specify how the reader and the tag are supposed to check that the messages they received are of the expected form, and how they should react when the messages are not well formed. This has to be precisely defined, since unlinkability depends on it. For instance, assume the tag does not check that the message he receives at step 3 contains the nonce $n_{T}$ . We assume that it only checks that the received message is an encryption with its own key k, and it aborts the session otherwise. In such a flawed implementation, an active attacker can eavesdrop a message ${n_{T}}_{k}$ sent by R to a tag T, and try to inject this message at the third step of another session played by $T^{'}$ . The tag $T^{'}$ will react by either aborting or by continuing the execution of this protocol. Depending on the reaction of the tag, the attacker will be able to infer if T and $T^{'}$ are the same tag or not.

In this example, the attacker adopts a malicious behaviour that is not detected immediately by the tag who keeps executing the protocol. The fact that the tag passes successfully a conditional reveals crucial information about the agents that are involved in the execution. Our second condition, namely well-authentication, basically requires that when an execution deviates from the honest one, the agents that are involved cannot successfully pass a conditional, thus avoiding the leak of the binary information success/failure.

Our main theorem states that these two conditions, frame opacity and well-authentication, are actually sufficient to ensure both unlinkability and anonymity. This theorem is of interest as our two conditions are fundamentally simpler than the targeted properties: frame opacity can be expressed and established relying on diff-equivalence (without the aforementioned precision issue) and well-authentication is only a conjunction of reachability properties. In fact, they are both in the scope of existing automatic verification tools like $ProVerif$ and $Tamarin$ .

Some related work. The precision issue of diff-equivalence is well-known (acknowledged e.g. in [19,26,33,35]). So far, the main approach that has been developed to solve this issue consists in modifying the notion of diff-equivalence to get closer to trace equivalence. For instance, the swapping technique introduced in [35] and formally justified in [19] allows to relax constraints imposed by diff-equivalence in specific situations, namely in process algebras featuring a notion of phase, often used for modelling e-voting protocols. Besides, the limitation of the diff-equivalence w.r.t. conditional evaluations has been partially addressed in [26] by pushing away the evaluation of some conditionals into terms. Nevertheless, the problem remains in general and the limitation described above is not addressed by those works (incidentally, it is specifically acknowledged for the case of the BAC protocol in [26]). We have chosen to follow a novel approach in the same spirit as the one presented in [21]. However, [21] only considers a very restricted class of protocols (single-step protocols that only use hash functions), while we target more complex protocols.

This paper essentially subsumes the conference paper that has been published in 2016 [40]. Compared to that earlier work, we have greatly generalized the scope of our method and improved its mechanization. First, we consider more protocols, including protocols where one party has a single identity (e.g. DAA) as well as protocols where sessions are executed sequentially instead of concurrently (e.g. e-passport scenarios). Second, we consider a much more general notion of frame opacity, which enables the analysis of more protocols. As a result of these two improvements, we could apply our method to more case studies (e.g. DAA, ABCDH).

Outline. In Section 2, we present our model inspired from the applied pi calculus as well as the class of protocols we consider. We then introduce in Section 3 the notion of trace equivalence that we then use to formally define the two privacy properties we study in this paper: unlinkability and anonymity. Our two conditions (frame opacity and well-authentication) and our main theorem are presented in Section 4. Finally, we discuss how to mechanize the verification of our conditions in Section 5 and present our case studies in Section 6, before concluding in Section 8. A detailed proof of our main result is provided in Appendix.

2. Modelling protocols

We model security protocols using a process algebra inspired from the applied pi calculus [2]. More specifically, we consider a calculus close to the one which is used in the $ProVerif$ tool [18]. Participants are modeled as processes, and the communication between them is modeled by means of the exchange of messages that are represented by a term algebra.

2.1. Term algebra

We consider an infinite set $N$ of names which are used to represent keys and nonces, and two infinite and disjoint sets of variables, denoted $X$ and $W$ . Variables in $X$ will typically be used to refer to unknown parts of messages expected by participants, while variables in $W$ , called handles, will be used to store messages learned by the attacker. We assume a signature Σ, i.e. a set of function symbols together with their arity, split into constructor and destructor symbols, i.e. $Σ = Σ_{c} ⊔ Σ_{d}$ .

Given a signature $F$ and a set of initial data A, we denote by $T (F, A)$ the set of terms built from elements of A by applying function symbols in $F$ . Terms of $T (Σ_{c}, N \cup X)$ will be called constructor terms. We note $vars (u)$ the set of variables that occur in a term u. A message is a constructor term u that is ground, i.e. such that $vars (u) = \emptyset$ . We denote by $\overline{x}$ , $\overline{n}$ , $\overline{u}$ , $\overline{t}$ a (possibly empty) sequence of variables, names, messages, and terms respectively. We also sometimes write them $(n_{1}, n_{2}, \dots)$ or simply n (when the sequence is reduced to one element). Substitutions are denoted by σ, the domain of a substitution is written $dom (σ)$ , and the application of a substitution σ to a term u is written $u σ$ . The positions of a term are defined as usual.

Example 1.
Consider the following signature: $\begin{matrix} Σ = {enc, dec, ⟨ ⟩, {proj}_{1}, {proj}_{2}, \oplus, 0, eq, ok} . \end{matrix}$ The symbols $enc$ and $dec$ of arity 2 represent symmetric encryption and decryption. Pairing is modeled using $⟨ ⟩$ of arity 2, and projection functions ${proj}_{1}$ and ${proj}_{2}$ , both of arity 1. The function symbol ⊕ of arity 2 and the constant 0 are used to model the exclusive or operator. Finally, we consider the symbol $eq$ of arity 2 to model equality test, as well as the constant symbol $ok$ . This signature is split into two parts: $Σ_{c} = {enc, ⟨ ⟩, \oplus, 0, ok}$ , and $Σ_{d} = {dec, {proj}_{1}, {proj}_{2}, eq}$ .

As in the process calculus presented in [18], constructor terms are subject to an equational theory; this has proved very useful for modelling algebraic properties of cryptographic primitives (see e.g. [31] for a survey). Formally, we consider a congruence $=_{E}$ on $T (Σ_{c}, N \cup X)$ , generated from a set of equations $E$ over $T (Σ_{c}, X)$ . Thus, this congruence relation is closed under substitution and renaming. We assume that it is not degenerate, i.e. there exist u, v such that $u \neq_{E} v$ .
Example 2.
To reflect the algebraic properties of the exclusive or operator, we may consider the equational theory generated by the following equations: $\begin{matrix} x \oplus 0 = x x \oplus x = 0 x \oplus y = y \oplus x (x \oplus y) \oplus z = x \oplus (y \oplus z) \end{matrix}$ In such a case, we have that $enc (a \oplus (b \oplus a), k) =_{E} enc (b, k)$ .

We also give a meaning to destructor symbols through the notion of computation relation. As explained below, a computation relation may be derived from a rewriting system but we prefer to not commit to a specific construction, and therefore we introduce a generic notion of computation relation. Instead, we assume an arbitrary relation subject to a number of requirements, ensuring that the computation relation behaves naturally with respect to names, constructors, and the equational theory.
Definition 1.
A computation relation is a relation over $T (Σ, N) \times T (Σ_{c}, N)$ , denoted $⇓$ , that satisfies the following requirements:
if $n \in N$ , then $n ⇓ n$ ;

if $f \in Σ_{c}$ is a symbol of arity k, and $t_{1} ⇓ u_{1}, \dots, t_{k} ⇓ u_{k}$ , then $f (t_{1}, \dots, t_{k}) ⇓ f (u_{1}, \dots, u_{k})$ ;

if $t ⇓ u$ then $t ρ ⇓ u ρ$ for any bijective renaming ρ;

if $t^{'}$ is a context built from Σ and $N$ , $t ⇓ u$ , and $t^{'} [u] ⇓ v$ then $t^{'} [t] ⇓ v$ ;

if $t^{'}$ is a context built from Σ and $N$ , and $t_{1}$ , $t_{2}$ are constructor terms such that $t_{1} =_{E} t_{2}$ and $t^{'} [t_{1}] ⇓ u_{1}$ for some $u_{1}$ , then $t^{'} [t_{2}] ⇓ u_{2}$ for some $u_{2}$ such that $u_{1} =_{E} u_{2}$ ;

if $t ⇓ u_{1}$ then we have that $t ⇓ u_{2}$ if, and only if, $u_{1} =_{E} u_{2}$ .

The last requirement expresses that the relation $⇓$ associates, to any ground term t, at most one message up to the equational theory $E$ . When no such message exists, we say that the computation fails; this is noted $t ⇓ /$ . We may sometimes use directly $t ⇓$ as a message, when we know that the computation succeeds and the choice of representative is irrelevant.

A possible way to derive a computation relation is to consider an ordered set of rules of the form: $g (u_{1}, \dots, u_{n}) \to u$ where $g$ is a destructor, and $u, u_{1}, \dots, u_{n} \in T (Σ_{c}, X)$ . A ground term t can be rewritten into $t^{'}$ if there is a position p in t and a rule $g (u_{1}, \dots, u_{n}) \to u$ such that $t |_{p} = g (v_{1}, \dots, v_{n})$ and $v_{1} =_{E} u_{1} θ, \dots, v_{n} =_{E} u_{n} θ$ for some substitution θ, and $t^{'} = t {[u θ]}_{p}$ (i.e. t in which the subterm at position p has been replaced by $u θ$ ). Moreover, we assume that $u_{1} θ, \dots, u_{n} θ$ as well as $u θ$ are messages. In case there is more that one rule that can be applied at a given position p, we consider the one occurring first in the ordered set. We denote $\to^{}$ the reflexive and transitive closure of →, and $⇓$ the relation induced by →, i.e.* $t ⇓ u$ when $t \to^{} u^{'}$ and $u^{'} =_{E} u$ .

Proving that an ordered set rewriting rules as defined above induces a computation relation is beyond the scope of this paper but the interested reader will find such a proof in [39].
Example 3.
The properties of symbols in $Σ_{d}$ (Example 1) are reflected through the following rules: $\begin{matrix} dec (enc (x, y), y) \to x eq (x, x) \to ok {proj}_{i} (⟨ x_{1}, x_{2} ⟩) \to x_{i} for i \in {1, 2} \end{matrix}$ This rewriting system induces a computation relation. For instance, we have that: $\begin{matrix} dec (enc (c, a \oplus b), b \oplus a) ⇓ c, dec (enc (c, a \oplus b), b) ⇓ / and dec (a, b) \oplus dec (a, b) ⇓ / . \end{matrix}$
Example 4.
Ordered rewriting rules are expressive enough to define a destructor symbol $neq$ such that $neq (u, v) ⇓ yes$ if, and only if, u and v can be reduced to messages that are not equal modulo $E$ . It suffices to consider $neq (x, x) \to no$ and $neq (x, y) \to yes$ (in this order) with $yes, no \in Σ_{c}$ .

For modelling purposes, we split the signature Σ into two parts, namely $Σ_{pub}$ and $Σ_{priv}$ . An attacker builds his own messages by applying public function symbols to terms he already knows and that are available through variables in $W$ . Formally, a computation done by the attacker is a recipe, i.e.* a term in $T (Σ_{pub}, W)$ . Recipes will be denoted by R, M, N. Note that, although we do not give the attacker the ability to generate fresh names to use in recipes, we obtain essentially the same capability by assuming an infinite supply of public constants in $Σ_{c} \cap Σ_{pub}$ .
2.2. Process algebra

We now define the syntax and semantics of the process algebra we use to model security protocols. We consider a calculus close to the one which is used in the $ProVerif$ tool [18]. An important difference is that we only consider public channels. Our calculus also features, in addition to the usual replication (where an unbounded number of copies of a process are ran concurrently), a simple form of sequential composition and the associated repetition operation (where an unbounded number of copies of a process are ran sequentially, one after the other).

We consider a set $C$ of channel names that are assumed to be public. Protocols are modeled through processes using the following grammar: $\begin{matrix} P, Q & : = & 0 & null & ∣ & (P ∣ Q) & parallel & ∣ & ! P & replication \\ ∣ & in (c, x) . P & input & ∣ & new \overline{n} . P & restriction & ∣ & ! P & repetition \\ ∣ & out (c, u) . P & output & ∣ & let \overline{x} = \overline{t} in P else Q & evaluation & ∣ & P; Q & sequence \end{matrix}$ where $c \in C$ , $x \in X$ , $n \in N$ , $u \in T (Σ_{c}, N \cup X)$ , and $\overline{x}$ and $\overline{t}$ are two sequences of the same length, respectively over variables ( $X$ ) and terms ( $T (Σ, N \cup X)$ ).

We write $fv (P)$ for the set of free variables of P, i.e. the set of variables that are not bound by an input or a $let$ construct. A process P is ground if $fv (P) = \emptyset$ . Similarly, we write $fn (P)$ for the set of free names of P, i.e. the set of names that are not bound by a $new$ construct.

Most constructs are standard in process calculi. The process 0 does nothing and we sometimes omit it. The process $in (c, x) . P$ expects a message m on channel c and then behaves like $P {x \mapsto m}$ , i.e. P in which the (free) occurrences of x have been replaced by m. The process $out (c, u) . P$ emits u on channel c, and then behaves like P. The process $P ∣ Q$ runs P and Q in parallel. The process $new \overline{n} . P$ generates new names, binds it to $\overline{n}$ , and continues as P.

The special construct $let \overline{x} = \overline{t} in P else Q$ combines several standard constructions, allowing one to write computations and conditionals compactly. Such a process tries to evaluate the sequence of terms $\overline{t}$ and in case of success, i.e. when $\overline{t} ⇓ \overline{u}$ for some messages $\overline{u}$ , the process P in which $\overline{x}$ are replaced by $\overline{u}$ is executed; otherwise the process Q is executed. The goal of this construct is to avoid nested $let$ instructions to be able to define our class of protocols in a simple way later on. Note also that the $let$ instruction together with the $eq$ theory as defined in Example 3 can encode the usual conditional construction. Indeed, $let x = eq (u, v) in P else Q$ will execute P only if the computation succeeds on $eq (u, v)$ , that is only if $u ⇓ u^{'}$ , $v ⇓ v^{'}$ , and $u^{'} =_{E} v^{'}$ for some messages $u^{'}$ and $v^{'}$ . For brevity, we sometimes omit $else 0$ .

The process $! P$ executes P an arbitrary number of times (in parallel). The last two constructs correspond to sequential compositions. The process $(P; Q)$ behaves like P at first, and after the complete execution of P it behaves like Q. The process $! P$ executes P an arbitrary number of times in sequence, intuitively corresponding to $(P; P; P; \dots)$ . Such constructions are known to be problematic in process calculi. Our goal here is however quite modest: as will be visible in our operational semantics, our sequential composition is only meaningful for restricted processes. It could in fact be defined using recursion, but there is no point here to consider general recursion: our study is going to restrict to a simple class of protocols that would immediately exclude it.

Example 5.
We consider the RFID protocol due to Feldhofer et al. as described in [38] and which can be presented using Alice & Bob notation as follows: $\begin{array}{l} 1 . I \to R : n_{I} \\ 2 . R \to I : {n_{I}, n_{R}}_{k} \\ 3 . I \to R : {n_{R}, n_{I}}_{k} \end{array}$

The protocol is between an initiator I (the reader) and a responder R (the tag) that share a symmetric key k. We consider the term algebra introduced in Example 3. The protocol is modelled by the parallel composition of $P_{I}$ and $P_{R}$ , corresponding respectively to the roles I and R. $\begin{array}{l} P_{Fh} : = new k . (new n_{I} . P_{I} ∣ new n_{R} . P_{R}) \end{array}$ where $P_{I}$ and $P_{R}$ are defined as follows, with $u = dec (x_{1}, k)$ : $\begin{array}{l} \begin{matrix} P_{I} & : = & out (c_{I}, n_{I}) . \\ in (c_{I}, x_{1}) . \\ let x_{2}, x_{3} = eq (n_{I}, {proj}_{1} (u)), {proj}_{2} (u) in \\ out (c_{I}, enc (⟨ x_{3}, n_{I} ⟩, k)) \end{matrix} \begin{matrix} P_{R} & : = & in (c_{R}, y_{1}) . \\ out (c_{R}, enc (⟨ y_{1}, n_{R} ⟩, k)) . \\ in (c_{R}, y_{2}) . \\ let y_{3} = eq (y_{2}, enc (⟨ n_{R}, y_{1} ⟩, k)) in 0 \end{matrix} \end{array}$ We may note that there are potentially several ways to implement the last reader’s test. For instance, we may decide to replace the last line of the process $P_{R}$ by $let y_{3} = eq (⟨ n_{R}, y_{1} ⟩, dec (y_{2}, k)) in 0$ . This last check can also be simply removed. Alternatively, it could be followed by an observable action to make the outcome of the test manifest, e.g. the output of a public constant $open$ in case of success and $close$ in case of failure. This would be a reasonable model for many use cases, e.g. in access control scenarios a door may either open or remain close after the execution of the protocol.

The operational semantics of processes is given by a labelled transition system over configurations (denoted by K) which are pairs $(P; ϕ)$ where:

$P$ is a multiset of ground processes where null processes are implicitly removed;

$ϕ = {w_{1} \mapsto u_{1}, \dots, w_{n} \mapsto u_{n}}$ is a frame, i.e. a substitution where $w_{1}, \dots, w_{n}$ are variables in $W$ , and $u_{1}, \dots, u_{n}$ are messages.

We often write $P \cup P$ instead of ${P} \cup P$ . The terms in ϕ represent the messages that are known by the attacker. Given a configuration K, $ϕ (K)$ denotes its second component. Sometimes, we consider processes as configurations: in such cases, the corresponding frame is the empty set ∅.

Fig. 1.
Semantics for processes.

Fig. 2.
Sequence simplification rules.

The operational semantics of a process is given by the relation $\overset{α}{\to}$ defined as the least relation over configurations satisfying the rules in Fig. 1. The rules are mostly standard and correspond to the intuitive meaning given previously. Rule In allows the attacker to send on channel c a message as soon as it is the result of a computation done by applying public function symbols on messages that are in his current knowledge. Rule Out corresponds to the output of a term: the corresponding term is added to the frame of the current configuration, which means that the attacker gains access to it. Rule New corresponds to the generation of a fresh name. As is standard, the bound names $\overline{n}$ can be renamed to achieve freshness so that the rule can always fire. The Par rule simply splits parallel compositions. The Then and Else rules correspond to the evaluation of a sequence of terms $\overline{t} = t_{1}, \dots, t_{n}$ ; if this succeeds, i.e. if there exist messages $u_{1}, \dots u_{n}$ such that $t_{1} ⇓ u_{1}, \dots t_{n} ⇓ u_{n}$ then variables $\overline{x}$ are bound to those messages, and P is executed; otherwise the process will continue with Q. Rules Rep $-!$ and Rep $-!$ unfold replication and repetition operators. The latter gives rise to a sequential composition, whose execution will have to rely, via the Seq rule, on the simplification rules of Fig. 2. These rules only support a limited set of operators, hence a sequence $P; Q$ is only executable for a restricted class of processes P, notably excluding parallel compositions. This is not an issue for our simple needs; our purpose here is not to define a general (and notoriously problematic) notion of sequence.

We note that our semantics enjoys some expected properties. Reduction is stable by bijective renaming, thanks to Definition 1, item 3: if $K_{1} \overset{α}{\to} K_{2}$ then $K_{1} ρ \overset{α}{\to} K_{2} ρ$ where ρ is a bijection over $N$ , applied here to processes and frames. It is also compatible with our equational theory, thanks to Definition 1, items 5 and 6: if $K_{1} \overset{α}{\to} K_{2}$ then $K_{1}^{'} \overset{α}{\to} K_{2}^{'}$ for any $K_{1}^{'} =_{E} K_{1}$ and $K_{2}^{'} =_{E} K_{2}$ . By Definition 1, item 6, we also have that $\begin{matrix} (P; ϕ) \overset{in (c, R)}{\to} (P^{'}; ϕ) and R ϕ ⇓ =_{E} R^{'} ϕ ⇓ yield (P; ϕ) \overset{in (c, R^{'})}{\to} (P^{'}; ϕ) (modulo E). \end{matrix}$

As usual, the relation $\overset{α_{1} \dots α_{n}}{\to}$ between configurations (where $α_{1} \dots α_{n}$ is a trace, i.e. a sequence of actions) is defined as the (labelled) reflexive and transitive closure of $\overset{α}{\to}$ .
Definition 2.
Input and output actions are called observable, while all other are unobservable. Given a trace $tr$ we define $obs (tr)$ to be the sub-sequence of observable actions of $tr$ .

We generally refer to τ, $τ_{then}$ and $τ_{else}$ as unobservable actions. It will become clear later on why we make a distinction when a process evolves using $T HEN$ or $E LSE$ .
Example 6.
Continuing Example 5. We have that $P_{Fh} \overset{tr}{\to} (\emptyset; ϕ_{0})$ where:
$tr = τ . τ . τ . τ . out (c_{I}, w_{1}) . in (c_{R}, w_{1}) . out (c_{R}, w_{2}) . in (c_{I}, w_{2}) . τ_{then} . out (c_{I}, w_{3}) . in (c_{R}, w_{3}) . τ_{then}$ ;

$ϕ_{0} = {w_{1} \mapsto n_{I}^{'}, w_{2} \mapsto enc (⟨ n_{I}^{'}, n_{R}^{'} ⟩, k^{'}), w_{3} \mapsto enc (⟨ n_{R}^{'}, n_{I}^{'} ⟩, k^{'})}$ .
The names $k^{'}$ , $n_{I}^{'}$ and $n_{R}^{'}$ are fresh names. Actually, this execution corresponds to a normal execution of one session of the protocol.
2.3. A generic class of two-party protocols

We aim to propose sufficient conditions to ensure unlinkability and anonymity for a generic class of two-party protocols. In this section, we define formally the class of protocols we are interested in.

Roles. We consider two-party protocols that are therefore made of two roles called the initiator and responder role respectively. We assume a set $L$ of labels that will be used to name output actions in these roles, allowing us to identify outputs that are performed by a same syntactic output action. These labels have no effect on the semantics.

Definition 3.
An initiator role is a process that is obtained using the following grammar: $\begin{array}{l} P_{I} : = 0 ∣ ℓ : out (c, u) . P_{R} \end{array}$ where $c \in C$ , $u \in T (Σ_{c}, N \cup X)$ , $ℓ \in L$ , and $P_{R}$ is obtained from the grammar of responder roles: $\begin{array}{l} P_{R} : = 0 ∣ in (c, y) . let \overline{x} = \overline{t} in P_{I} else P_{fail} with P_{fail} = 0 ∣ ℓ : out (c^{'}, u^{'}) \end{array}$ where $c, c^{'} \in C$ , $y \in X$ , $\overline{x}$ (resp. $\overline{t}$ ) is a sequence of variables in $X$ (resp. terms in $T (Σ, N \cup X)$ ), $u^{'} \in T (Σ_{c}, N \cup X)$ , and $ℓ \in L$ .

Moreover, an initiator (resp. responder) role is assumed to be ground, i.e., contain no free variable, though it may contain free names.

Intuitively, a role describes the actions performed by an agent. A responder role consists of waiting for an input and, depending on the outcome of a number of tests, the process will continue by sending a message and possibly waiting for another input, or stop possibly outputting an error message. An initiator behaves similarly but begins with an output. The grammar forces to add a conditional after each input. This is not a real restriction as it is always possible to add trivial conditionals with empty $\overline{x}$ , and $\overline{t}$ .
Example 7.
Continuing our running example, $P_{I}$ (resp. $P_{R}$ ) as defined in Example 5 is an initiator (resp. responder) role, up to the addition of a trivial conditional in role $P_{R}$ and distinct labels $ℓ_{1}$ , $ℓ_{2}$ , and $ℓ_{3}$ to decorate output actions.

Then, a protocol notably consists of an initiator role and a responder role that can interact together producing an honest trace. Intuitively, an honest trace is a trace in which the attacker does not really interfere, and that allows the execution to progress without going into an $else$ branch, which would intuitively correspond to a way to abort the protocol.
Definition 4.
A trace $tr$ (i.e. a sequence of actions) is honest for a frame ϕ if $τ_{else} \notin tr$ and $obs (tr)$ is of the form $out (_, w_{0}) . in (_, R_{0}) . out (_, w_{1}) . in (_, R_{1}) . \dots$ for arbitrary channel names, and such that $R_{i} ϕ ⇓ w_{i} ϕ$ for any action $in (_, R_{i})$ occurring in $tr$ .

Identities and sessions. In addition to the pair of initiator and responder roles, more information is needed in order to meaningfully define a protocol. Among the names that occur in these two roles, we need to distinguish those that correspond to identity-specific, long-term data (e.g. k from Example 5), called identity parameters and denoted $\overline{k}$ below, and those which shall be freshly generated at each session (e.g. $n_{I}, n_{R}$ from Example 5), called session parameters and denoted ${\overline{n}}_{I}$ and ${\overline{n}}_{R}$ below. We will require that any free name of roles must be either a session or an identity parameter. When necessary, we model long-term data that is not identity-specific (i.e. uniform for all agents) as private constants (i.e. terms in $Σ_{c} \cap Σ_{priv}$ ). Depending on the protocol to be modelled, we shall see that either both the initiator and the responder or only one of those roles have identity parameters. The former case arises for protocols that involves different identities for each party while the latter concerns protocols whose only one party can be instantiated by different agents (see Examples 10, 11 below for a more detailed discussion).

We also need to know whether sessions (with the same identity parameters) can be executed concurrently or only sequentially. For instance, let us assume that the Feldhofer protocol is used in an access control scenario where all tags that are distributed to users have pairwise distinct identities. Assuming that tags cannot be cloned, it is probably more realistic to consider that a tag can be involved in at most one session at a particular time, i.e. a tag may run different sessions but only in sequence. Such a situation will also occur in the e-passport application where a same passport cannot be involved in two different sessions of the BAC protocol (resp. PACE protocol) concurrently. This is the purpose of the components $†_{I}$ and $†_{R}$ in the following definition. When one role has no identity parameter, we also consider both cases: whether the only identity instantiating this role may have concurrent sessions or only sequential sessions. Moreover, we require that the process $P_{Π}$ which models a single session of the protocol can produce an honest trace.
Definition 5.
A protocol Π is a tuple $(\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ where $\overline{k}$ , ${\overline{n}}_{I}$ , ${\overline{n}}_{R}$ are three disjoint sets of names, $I$ (resp. $R$ ) is an initiator (resp. responder) role such that $fn (I) \subseteq \overline{k} ⊔ {\overline{n}}_{I}$ , $fn (R) \subseteq \overline{k} ⊔ {\overline{n}}_{R}$ , and $†_{I}, †_{R} \in {!,!}$ . Labels of $I$ and $R$ must be pairwise distinct. Names $\overline{k}$ (resp. ${\overline{n}}_{I} ⊔ {\overline{n}}_{R}$ ) are called identity parameters (resp. session parameters).

Given a protocol Π, we define $P_{Π} : = new \overline{k} . (new {\overline{n}}_{I} . I ∣ new {\overline{n}}_{R} . R)$ and we assume that $P_{Π} \overset{{tr}_{h}}{\to} (\emptyset; ϕ_{h})$ for some frame $ϕ_{h}$ and some trace ${tr}_{h}$ that is honest for $ϕ_{h}$ .

Given a protocol Π, we also associate another process $M_{Π}$ that represents the situation where the protocol can be executed by an arbitrary number of identities, with the possibility of executing an arbitrary number of sessions for a given identity. The formal definition differs slightly depending on whether identity parameters occur in both roles or only in the role $I$ (resp. $R$ ).
Definition 6.
Given a protocol $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ , the process $M_{Π}$ is defined as follows:
If $\overline{k} \cap fn (I) \neq \emptyset$ and $\overline{k} \cap fn (R) \neq \emptyset$ , then $M_{Π} =! new \overline{k} . (†_{I} new {\overline{n}}_{I} . I ∣ †_{R} new {\overline{n}}_{R} . R)$ ;

If $\overline{k} \cap fn (I) = \emptyset$ and $\overline{k} \cap fn (R) \neq \emptyset$ , then $M_{Π} = †_{I} new {\overline{n}}_{I} . I ∣! new \overline{k} . †_{R} new {\overline{n}}_{R} . R$ .

For the sake of simplicity, in case identity parameters only occur in one role, we assume that this role is the responder role. The omitted case where identity parameters occur only in the initiator role is very much similar. In fact, swapping the initiator and responder roles can also be formally achieved by adding an exchange of a fresh nonce at the beginning of the protocol under consideration. Note that the case where both $\overline{k} \cap fn (I)$ and $\overline{k} \cap fn (R)$ are empty means that no identity parameters are involved and therefore there is no issue regarding privacy. As expected, in such a situation, our definitions of unlinkability and anonymity (see Definition 12 and Definition 10) will be trivially satisfied.
Example 8.
Let $Π_{Fh} = (k, n_{I}, n_{R},!,!, P_{I}, P_{R})$ with $P_{I}$ and $P_{R}$ as defined in Example 5 (up to the addition of a trivial conditional). Let $P_{Fh} = new k . (new n_{I} . P_{I} ∣ new n_{R} . P_{R})$ , ${tr}_{h} = tr$ (up to the addition of an action $τ_{then}$ ), and $ϕ_{h} = ϕ_{0}$ as defined in Example 6. They satisfy the requirements stated in Definition 5, and therefore $Π_{Fh}$ is a protocol according to our definition. For this protocol, the identity parameter k occurs both in the role $P_{I}$ and $P_{R}$ , and therefore we have that $M_{Π_{Fh}} =! new k . (! new n_{I} . P_{I} ∣! new n_{R} . P_{R})$ .
Example 9.
In order to illustrate our method and the use of the repetition operator, we introduce a toy protocol which, as we shall see later, satisfies unlinkability only when sessions of the initiator role are executed sequentially. Using Alice & Bob notation, this protocol can be described as follows: $\begin{array}{l} 1 . T \to R : n_{T} \\ 2 . R \to T : n_{R} \\ 3 . T \to R : mac (⟨ n_{R}, n_{T} ⟩, k) \\ 4 . R \to T : mac (⟨ n_{T}, n_{R} ⟩, k) \end{array}$

The protocol is between a tag T (the initiator) and a reader R (the responder) which share a symmetric key k. To avoid an obvious reflection attack (where $n_{T} = n_{R}$ ), we assume that the tag systematically checks that the first message it receives is not the one he sent initially.

To formalise such a protocol, we consider $\begin{matrix} Σ_{c} = {mac, ⟨ ⟩, ok, yes, no} and Σ_{d} = {{proj}_{1}, {proj}_{2}, eq, neq} . \end{matrix}$ All symbols of the signature are public: $ok$ , $yes$ , and $no$ have arity 0; ${proj}_{1}$ and ${proj}_{2}$ have arity 1; other function symbols have arity 2. The destructors ${proj}_{1}, {proj}_{2}, eq$ and $neq$ are defined as in Examples 3 and 4. The symbol $mac$ will be used to model message authentication code.

The processes modelling the initiator and the responder roles are as follows: $\begin{array}{l} \begin{matrix} P_{T}^{'} : = & out (c_{T}, n_{T}) . \\ in (c_{T}, x_{1}) . \\ let x_{test} = eq (yes, neq (x_{1}, n_{T})) in \\ out (c_{T}, mac (⟨ x_{1}, n_{T} ⟩, k)) . in (c_{T}, x_{2}) . \\ let x_{test}^{'} = eq (x_{2}, mac (⟨ n_{T}, x_{1} ⟩, k)) in 0 \end{matrix} \begin{matrix} P_{R}^{'} : = & in (c_{R}, y_{1}) . \\ out (c_{R}, n_{R}) . \\ in (c_{R}, y_{2}) . \\ let y_{test} = eq (y_{2}, mac (⟨ n_{R}, y_{1} ⟩, k)) in \\ out (c_{R}, mac (⟨ y_{1}, n_{R} ⟩, k)) . 0 \end{matrix} \end{array}$

We may note that different choices can be made. For instance, we may decide to replace the process 0 occurring in $P_{T}^{'}$ with $out (c_{T}, ok)$ to make the outcome of the test manifest. The tuple $Π_{Toy}^{!} = (k, (n_{T}), (n_{R}),!,!, P_{T}^{'}, P_{R}^{'})$ is a protocol according to Definition 5. For this protocol, we have again that k occurs both in the roles $P_{T}^{'}$ and $P_{R}^{'}$ , and therefore: $\begin{matrix} M_{Π_{Toy}^{!}} =! new k . (! new n_{T} . P_{T}^{'} ∣! new n_{R} . P_{R}^{'}) . \end{matrix}$

As a last example, we will consider one for which identity parameters only occur in one role. This example can be seen as a simplified version of the Direct Anonymous Attestation (DAA) sign protocol that will be detailed in Section 6.
Example 10.
We consider a simplified version of the protocol DAA sign (adapted from [50]). Note that a comprehensive analysis of the protocol DAA sign (as well as the protocol DAA join) will be conducted in Section 6. Before describing the protocol itself, we introduce the term algebra that will allow us to model the signature and zero knowledge proofs used in that protocol. We consider:
$Σ_{c} = {sign, zk, pk, ⟨ ⟩, tuple, ok, s k_{I}, error}$ , and

$Σ_{d} = {{check}_{sign}, {check}_{zk}, {public}_{zk}, {proj}_{1}, {proj}_{2}, {proj}_{1}^{4}, {proj}_{2}^{4}, {proj}_{3}^{4}, {proj}_{4}^{4}}$ .
We consider the computation relation induced by the empty set of equations, and the rules: $\begin{array}{l} {check}_{sign} (sign (x, y), pk (y)) \to x {proj}_{i} (⟨ y_{1}, y_{2} ⟩) \to y_{i} i \in {1, 2} \\ {check}_{zk} (zk (sign (⟨ x_{k}, x_{id} ⟩, z_{sk}), x_{k}, tuple (y_{1}, y_{2}, y_{3}, pk (z_{sk})))) \to ok \\ {public}_{zk} (zk (x, y, z)) \to z {proj}_{i}^{4} (tuple (y_{1}, y_{2}, y_{3}, y_{4})) \to y_{i} i \in {1, 2, 3, 4} \end{array}$

The protocol is between a client C (the responder) and a verifier V (the initiator). The client is willing to sign a message m using a credential issued by some issuer and then he has to convince V that the latter signature is genuine. The client C has a long-term secret key $k_{C}$ , an identity ${id}_{C}$ , and some credential ${cred}_{C} = sign (⟨ k_{C}, {id}_{C} ⟩, s k_{I})$ issued by some issuer I having $s k_{I}$ as a long-term signature key. Such a credential would be typically obtained once and for all through a protocol similar to DAA join. We give below an Alice & Bob description of the protocol: $\begin{array}{l} 1 . V \to C : n_{V} \\ 2 . C \to V : zk ({cred}_{C}, k_{C}, tuple (n_{V}, n_{C}, m, pk (s k_{I}))) \end{array}$ The verifier starts by challenging the client with a fresh nonce, the latter then sends a complex zero-knowledge proof bound to this challenge proving that he knows a credential from the expected issuer bound to the secret $k_{C}$ he knows. Before accepting this zero-knowledge proof, the verifier V (i) checks the validity of the zero-knowledge proof using the ${check}_{zk}$ operator, and (ii) verifies that this proof is bound to the challenge $n_{V}$ and to the public key of I using the ${public}_{zk}$ operator. The processes $P_{C}$ and $P_{V}$ are defined as follows: $\begin{array}{l} P_{V} : = & out (c_{V}, n_{V}) . \\ in (c_{V}, x_{1}) . \\ let x_{2}, x_{3}, x_{4} = \\ eq ({check}_{zk} (x_{1}), ok), eq ({proj}_{1}^{4} ({public}_{zk} (x_{1})), n_{V}), eq ({proj}_{4}^{4} ({public}_{zk} (x_{1})), pk (s k_{I})) in 0 \\ else out (c_{V}, error) \\ P_{C} : = & in (c_{R}, y_{1}) . \\ out (c_{R}, zk (sign (⟨ k_{C}, {id}_{C} ⟩, s k_{I}), k_{C}, tuple (y_{1}, n_{C}, m, pk (s k_{I})))) . \end{array}$

This protocol falls in our class, the two parties being the verifier $P_{V}$ and the client $P_{C}$ . The protocol DAA sign, and the simplified version we consider here, has been designed to provide privacy (i.e. unlinkability and anonymity as defined in Section 3) to users (i.e. clients) inside a group associated to a single issuer. In other words, the privacy set [47] that is typically considered is the set of users who obtained a credential from a single, given issuer. Therefore, as we are interested in modelling different clients having credentials signed by the same issuer, we model $s k_{I}$ as a private constant in $Σ_{c} \cap Σ_{priv}$ rather than as an identity parameter (we explore this different modelling choice in Example 11).

The tuple $Π_{DAA} = ((k_{C}, {id}_{C}), n_{V}, (n_{C}, m),!,!, P_{V}, P_{C})$ is a protocol according to our Definition 5. We have that $k_{C}$ or ${id}_{C}$ only occur in $P_{C}$ , and therefore following Definition 6, we have that: $\begin{matrix} M_{Π_{DAA}} = (! new n_{V} . P_{V}) ∣ (! new (k_{C}, {id}_{C}) .! new (n_{C}, m) . P_{C}) \end{matrix}$ This models infinitely many different clients who obtained credentials from a single issuer having the signature key $s k_{I}$ . Any of those clients may take part to infinitely many sessions of the protocol with any verifier associated to that issuer, which executes always the same role (he has no proper identity). We consider here a scenario where sessions can be executed concurrently (both for clients and verifiers). We shall see that our verification methods allows one to automatically prove that privacy is preserved in this scenario.
Example 11 (Continuing Example 10).

The flexibility of our notion of protocol allows for a subtly different scenario to be analyzed by considering $s k_{I}$ as being identity-specific (i.e. as an identity parameter) instead of being uniform for all identities (i.e. private constant). Privacy would then be considered between users associated to different issuers (the privacy set being all users); this is a stronger property that the protocol is not expected to meet. Indeed, a verifier sends ZK proofs whose public parts contain the public key of its credential issuer. We still consider the two parties $P_{V}$ and $P_{C}$ but we now model $s k_{I}$ as an identity parameter. Therefore, we remove $s k_{I}$ from $Σ_{c}$ defined in Example 10. The tuple $Π_{DAA} = ((s k_{I}, k_{C}, {id}_{C}), n_{V}, (n_{C}, m),!,!, P_{V}, P_{C})$ is a protocol according to our Definition 5. We have that $s k_{I}$ occurs both in $P_{C}$ and $P_{V}$ , and therefore following Definition 6, we have that: $\begin{matrix} M_{Π_{DAA}^{s k_{I}}} =! new (s k_{I}, k_{C}, {id}_{C}) . (! new n_{V} . P_{V} ∣! new (n_{C}, m) . P_{C}) \end{matrix}$ This models (i) infinitely many different clients who obtained pairwise different credentials from infinitely many issuers having pairwise different signature keys $s k_{I}$ , and, (ii) infinitely many different verifiers who check for credentials that have been signed by pairwise different issuers. Any of those clients and verifiers may take part to infinitely many sessions of the protocol. We consider here a scenario where users and verifiers sessions can be executed concurrently. Note however that only one user per group (associated to a single issuer) is considered. Relaxing this constraint would require a more generic notion of protocols with 3 parties (this limitation will be discussed in Section 7.1.2). Even for such a weaker scenario, we shall see that our verification methods allows one to find that privacy (unlinkability and anonymity) is already broken (see Fig. 3 and details in Section 6.6.2).

Fig. 3.

Summary of our running examples.

Discussion about shared and non-shared protocols. As mentioned earlier and shown in Definition 6, we distinguish two cases depending on whether (i) both roles use identity parameters (i.e. when $fn (I) \cap \overline{k} \neq \emptyset$ and $fn (R) \cap \overline{k} \neq \emptyset$ ) or (ii) only one role uses identity parameters (i.e. when $fn (I) \cap \overline{k} = \emptyset$ and $fn (R) \cap \overline{k} \neq \emptyset$ , the other case being symmetrical). The case (i) corresponds to the case where we should consider an arbitrary number of users for each role, whereas regarding case (ii) it is sufficient to consider an arbitrary number of users for role $R$ only. In addition to this distinction, note that there are two different kinds of protocols that lie in class (i):

The shared case when $fn (I) \cap fn (R) \neq \emptyset$ . In such a situation, roles $I$ and $R$ share names in $fn (I) \cap fn (R)$ . In practice, this shared knowledge may have been established in various ways such as by using prior protocols, using another communication channel (e.g. optical scan of a password as it is done with e-passports, use of PIN codes) or by retrieving the identity from a database that matches the first received message as it is often done with RFID protocols. For such protocols, it is expected that an initiator user and a responder user can communicate successfully producing an honest execution only if they have the same identity (i.e. they share the same names $\overline{k}$ ).

The non-shared case when $fn (I) \cap fn (R) = \emptyset$ . In such a case, both roles do not share any specific prior knowledge, and it is therefore expected that an initiator and a responder can communicate successfully producing an honest execution whatever their identities.

Unlinkability and anonymity will be uniformly expressed for the cases (i-a) and (i-b) but our sufficient conditions will slightly differ depending on the case under study.

3. Modelling security properties

This section is dedicated to the definition of the security properties we seek to verify on protocols: unlinkability and anonymity. Those properties are defined using the notion of trace equivalence which relates indistinguishable processes.

3.1. Trace equivalence

Intuitively, two configurations are trace equivalent if an attacker cannot tell whether he is interacting with one or the other. Before formally defining this notion, we first introduce a notion of equivalence between frames, called static equivalence.

Definition 7.
A frame ϕ is statically included in $ϕ^{'}$ when $dom (ϕ) = dom (ϕ^{'})$ , and
for any recipe R such that $R ϕ ⇓ u$ for some u, we have that $R ϕ^{'} ⇓ u^{'}$ for some $u^{'}$ ;

for any recipes $R_{1}, R_{2}$ such that $R_{1} ϕ ⇓ u_{1}$ , $R_{2} ϕ ⇓ u_{2}$ , and $u_{1} =_{E} u_{2}$ , we have that $R_{1} ϕ^{'} ⇓ =_{E} R_{2} ϕ^{'} ⇓$ , i.e. there exist $v_{1}, v_{2}$ such that $R_{1} ϕ^{'} ⇓ v_{1}$ , $R_{2} ϕ^{'} ⇓ v_{2}$ , and $v_{1} =_{E} v_{2}$ .
Two frames ϕ and $ϕ^{'}$ are in static equivalence, written $ϕ \sim ϕ^{'}$ , if the two static inclusions hold.

Intuitively, an attacker can distinguish two frames if he is able to perform some computation (or a test) that succeeds in ϕ and fails in $ϕ^{'}$ (or the converse).
Example 12.
Let $ϕ_{0}$ be the frame given in Example 6, we have that $ϕ_{0} ⊔ {w_{4} \mapsto k^{'}} ≁ ϕ_{0} ⊔ {w_{4} \mapsto k^{″}}$ . An attacker may observe a difference relying on the computation $R = dec (w_{2}, w_{4})$ .

Then, trace equivalence is the active counterpart of static equivalence, taking into account the fact that the attacker may interfere during the execution of the process. In order to define this, we first introduce $trace (K)$ for a configuration $K = (P; ϕ)$ : $\begin{matrix} trace (K) = {(tr, ϕ^{'}) | (P, ϕ) \overset{tr}{\to} (P^{'}; ϕ^{'}) for some configuration (P^{'}; ϕ^{'})} . \end{matrix}$ Definition 8.
Let K and $K^{'}$ be two configurations. We say that K is trace included in $K^{'}$ , written $K ⊑ K^{'}$ , when, for any $(tr, ϕ) \in trace (K)$ there exists $({tr}^{'}, ϕ^{'}) \in trace (K^{'})$ such that $obs ({tr}^{'}) = obs (tr)$ and $ϕ \sim ϕ^{'}$ . They are in trace equivalence, written $K \approx K^{'}$ , when $K ⊑ K^{'}$ and $K^{'} ⊑ K$ .
Example 13.
Resuming Example 8, we may be interested in checking whether the configurations $K = (! P_{Π_{Fh}}; \emptyset)$ and $K^{'} = (M_{Π_{Fh}}; \emptyset)$ are in trace equivalence. This equivalence models the fact that $Π_{Fh}$ is unlinkable: each session of the protocol appears to an attacker as if it has been initiated by a different tag, since a given tag can perform at most one session in the idealised scenario K. This equivalence actually holds. It is non-trivial, and cannot be established using existing verification tools such as $ProVerif$ or $Tamarin$ . The technique developed in this paper will notably allow one to establish it automatically.

3.2. Security properties under study

In this paper, we focus on two privacy-related properties, namely unlinkability and anonymity.

3.2.1. Unlinkability

According to the ISO/IEC standard 15408 [41], unlinkability aims at ensuring that a user may make multiple uses of a service or a resource without others being able to link these uses together. In terms of our modelling, a protocol preserves unlinkability if any two sessions of a same role look to an outsider as if they have been executed with different identity names. In other words, an ideal version of the protocol with respect to unlinkability, allows the roles $I$ and $R$ to be executed at most once for each identity names. An outside observer should then not be able to tell the difference between the original protocol and the ideal version of this protocol.

In order to precisely define this notion, we have to formally define this ideal version of a protocol Π. This ideal version, denoted $S_{Π}$ , represents an arbitrary number of agents that can at most execute one session each. Such a process is obtained from $M_{Π}$ by simply removing the symbols ! and $!$ that are in the scope of identity names. Indeed, those constructs enable each identity to execute an arbitrary number of sessions (respectively concurrently and sequentially). Formally, depending on whether identity names occur in both roles, or only in the responder role, this leads to slightly different definitions.

Definition 9.
Given a protocol $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ , the process $S_{Π}$ is defined as follows:
If $\overline{k} \cap fn (I) \neq \emptyset$ and $\overline{k} \cap fn (R) \neq \emptyset$ , then $S_{Π} : =! new \overline{k} . (new {\overline{n}}_{I} . I ∣ new {\overline{n}}_{R} . R)$ ;

If $\overline{k} \cap fn (I) = \emptyset$ and $\overline{k} \cap fn (R) \neq \emptyset$ , then $S_{Π} : = †_{I} new {\overline{n}}_{I} . I ∣! new \overline{k} . new {\overline{n}}_{R} . R$ .

Unlinkability is defined as a trace equivalence between $S_{Π}$ (where each identity can execute at most one session) and $M_{Π}$ (where each identity can execute an arbitrary number of sessions).
Definition 10.
A protocol $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ ensures unlinkability if $M_{Π} \approx S_{Π}$ .
Example 14.
Going back to our running example (Example 8), unlinkability is expressed through the equivalence given in Example 13 and recalled below: $\begin{matrix} ! new k . (! new n_{I} . P_{I} ∣! new n_{R} . P_{R}) \approx! new k . (new n_{I} . P_{I} ∣ new n_{R} . P_{R}) . \end{matrix}$

This intuitively represents the fact that the real situation where a tag and a reader may execute many sessions in parallel is indistinguishable from an idealized one where a given tag and a given reader can execute at most one session for each identity.

Although unlinkability of only one role (e.g. the tag for RFID protocols) is often considered in the literature (including [5]), we consider a stronger notion here since both roles are treated symmetrically. As illustrated through the case studies developed in Section 6 (see Sections 6.2 and 6.4), this is actually needed to not miss some practical attacks. Example 15.
We consider the variant of the toy protocol described in Example 9 where concurrent sessions are authorised for the initiator: $Π_{Toy}^{!} : = (k, (n_{T}), (n_{R}),!,!, P_{T}^{'}, P_{R}^{'})$ . We may be interested in checking unlinkability as in Example 14, i.e. whether the following equivalence holds or not: $\begin{matrix} ! new k . (! new n_{T} . P_{T}^{'} ∣! new n_{R} . P_{R}^{'}) \approx! new k . (new n_{T} . P_{T}^{'} ∣ new n_{R} . P_{R}^{'}) \end{matrix}$ Actually, this equivalence does not hold. When concurrent sessions are authorised, the following scenario is possible: two tags of the same identity can start a session. Then, the attacker just forwards messages from one tag to the other. They can thus complete the protocol. In particular, the mac-key verification stage goes well and the attacker observes that the last conditional of the two tags holds. Such a scenario (which is possible on the left-hand side of the equivalence) cannot be mimicked on the right-hand side (each tag can execute only once). Therefore we have a trace that can only be executed by the multiple sessions process: the equivalence does not hold.

However, we shall see that the original toy protocol of Example 9 (with sessions of the initiator running sequentially only) can be shown unlinkable using the technique developed in this paper. Formally, the following equivalence holds: $\begin{matrix} ! new k . (new n_{T} . P_{T}^{'} ∣ new n_{R} . P_{R}^{'}) \approx! new k . (! new n_{T} . P_{T}^{'} ∣! new n_{R} . P_{R}^{'}) \end{matrix}$

3.2.2. Anonymity

According to the ISO/IEC standard 15408 [41], anonymity aims at ensuring that a user may use a service or a resource without disclosing its identity. In terms of our modelling, a protocol preserves anonymity of some identities $\overline{id} \subseteq \overline{k}$ , if a session executed with some particular (public) identities $\overline{{id}_{0}}$ looks to an outsider as if it has been executed with different identity names. In other words, an outside observer should not be able to tell the difference between the original protocol and a version of the protocol where the attacker knows that specific roles $I$ and $R$ with identities ${id}_{0}$ (known by the attacker) are present.

Definition 11.
Given a protocol $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ , and $\overline{id} \subseteq \overline{k}$ , the process $M_{Π, \overline{id}}$ is defined as follows:
If $\overline{k} \cap fn (I) \neq \emptyset$ and $\overline{k} \cap fn (R) \neq \emptyset$ , then $M_{Π, \overline{id}} : = M_{Π} ∣ new \overline{k} . (†_{I} new {\overline{n}}_{I} . I_{0} ∣ †_{R} new {\overline{n}}_{R} . R_{0})$ .

If $\overline{k} \cap fn (I) = \emptyset$ and $\overline{k} \cap fn (R) \neq \emptyset$ , then $M_{Π, \overline{id}} : = M_{Π} ∣ new \overline{k} . †_{R} new {\overline{n}}_{R} . R_{0}$ ,
where $I_{0} = I {\overline{id} \mapsto \overline{{id}_{0}}}$ and $R_{0} = R {\overline{id} \mapsto \overline{{id}_{0}}}$ for some fresh public constants $\overline{{id}_{0}}$ .
Definition 12.
Let $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ , and $\overline{id} \subseteq \overline{k}$ . We say that Π ensures anonymity w.r.t. $\overline{id}$ if $M_{Π, \overline{id}} \approx M_{Π}$ .
Example 16.
Going back to Example 10, anonymity w.r.t. identity of the client (i.e. ${id}_{C}$ ) is expressed through the following equivalence: $\begin{array}{l} ! new n_{V} . P_{V} ∣ (! new (k_{C}, {id}_{C}) .! new (n_{C}, m) . P_{C}) ∣ (new (k_{C}, {id}_{C}) .! new (n_{C}, m) . P_{C} {{id}_{C} \mapsto i d_{0}}) \\ \approx! new n_{V} . P_{V} ∣ (! new (k_{C}, {id}_{C}) .! new (n_{C}, m) . P_{C}) \end{array}$ This intuitively represents the fact that the situation in which a specific client with some known identity $i d_{0}$ may execute some sessions is indistinguishable from a situation in which this client is not present at all. Therefore, if these two situations are indeed indistinguishable from the point of view of the attacker, it would mean that there is no way for the attacker to deduce whether a client with a specific identity is present or not.

3.3. Discussion

The notion of strong unlinkability that we consider is inspired by [5]. In this paper, the authors first propose a definition of weak unlinkability that is not expressed via a process equivalence, then they give a notion of strong unlinkability that implies the former notion and is expressed via a labelled bisimilarity. The authors argue that, compared to weak unlinkability, the strong variant is too constraining but has the advantage of being more amenable to verification. The first claim is based on an example protocol [5, Theorem 1] where a reader emits an observable “beep” when it sees the same tag twice, which breaks strong unlinkability but not weak unlinkability. Unlike the authors of [5], we do not consider this to be a spurious attack, but a potentially threatening linkability issue. The second claim is only substantiated by the fact that tools exist for automatically verifying bisimilarities. As discussed before, this is not sufficient. Moreover, there might be spurious attacks on strong unlinkability just because bisimilarity is a very restrictive equivalence: for this reason we would also consider that the strong unlinkability of [5] is too strong, and instead advocate for our variant based on trace equivalence.

We now show formally that, in the setting that we consider, our notion of unlinkability (Definition 10) indeed corresponds to the strong unlinkability of [5, Definition 12] where trace equivalence is required rather than bisimilarity. In this original formulation, strong unlinkability is a property of one specific role and not of the whole protocol. As a more technical difference, protocols in [5] may involve more than two roles, and agents may use private channels. In practice, this is used to communicate honest identities in setup phases, as is the case in their BAC case study. If we specialise the setting of [5] to two roles R and T (for Reader and Tag) which fall into the format of Definition 3 and do not use the distinguished private channel c, strong unlinkability of the tag role T corresponds to the following labelled bisimilarity: $\begin{array}{l} new c . ((! new \overline{k} .! out (c, \overline{k}) . new {\overline{n}}_{T} . T) ∣ (! in (c, \overline{k}) . new {\overline{n}}_{R} . R)) \\ (1) & \approx_{ℓ} new c . ((! new \overline{k} . out (c, \overline{k}) . new {\overline{n}}_{T} . T) ∣ (! in (c, \overline{k}) . new {\overline{n}}_{R} . R)) \end{array}$ As communications on channel c are private, equation (1) is equivalent to: $\begin{matrix} (2) & ! new \overline{k} . ((! new {\overline{n}}_{T} . T) ∣ (! new {\overline{n}}_{R} . R)) \approx_{ℓ}! new \overline{k} . ((new {\overline{n}}_{T} . T) ∣ (new {\overline{n}}_{R} . R)) \end{matrix}$ The key observation here is that, even though we had only removed replication for the tag role (on the right of equation (1)), replications are removed for both tags and readers in equation (2) because communications on c are linear (i.e. can be triggered only once). Thus, in this particular case, the only difference between strong unlinkability and our unlinkability is that we rely on trace equivalence rather than labelled bisimilarity.

Several other definitions of unlinkability have been proposed in the literature (see, e.g. [20,22] for a comparison). In particular, various game-based formulations have been considered, both in the computational and symbolic models. We first discuss the most common kind of games, called two-agents games in [22] and seen e.g. in [11,30,42]. As we shall see, these games can be accurately verified through diff-equivalence, but systematically miss some linkability attacks. We will not need any formal definition, but simply rely on the general idea behind these games, which run in two phases:

Learning phase: During this phase, the attacker can trigger an arbitrary number of sessions of the two roles (namely tag and reader) with the identity of his choice. This allows him to gain some knowledge. Eventually, the attacker chooses to end the learning phase and enter the second phase.

Guessing phase: The challenger chooses an identity x among two distinguished identities ${id}_{1}$ and ${id}_{2}$ . The attacker is allowed to interact again (an arbitrary number of times) with roles of x, or of identities other than ${id}_{1}$ and ${id}_{2}$ .

The attacker wins the game if he can infer whether x is

{id}_{1}

{id}_{2}

, i.e. if he is able to distinguish between these two scenarios. The following example shows that these two-agent games miss some linkability attacks, and do not imply unlinkability in our sense for this reason.

Example 17.
We consider a protocol between a tag T and a reader R sharing a symmetric key k. We consider that sessions can be executed in parallel, and we assume that T aborts in case the nonce $n_{R}$ he receives is equal to the nonce $n_{T}$ he sent previously (in the same session). $\begin{array}{l} 1 . T \to R : {n_{T}}_{k} \\ 2 . R \to T : {n_{R}}_{k} \\ 3 . T \to R : {n_{R} \oplus n_{T}}_{k} \end{array}$

We consider the term algebra introduced in Example 1, and the equational theory introduced in Example 2 with in addition the equation $dec (enc (x, y), y) = x$ . To show that the property formally stated in Definition 10 does not hold, consider the following scenario. $\begin{array}{l} 1 . T \to R : {n_{T}}_{k} \\ 1^{'} . T^{'} \to R : {n_{T}^{'}}_{k} \\ 2 . I (R) \to T : {n_{T}^{'}}_{k} \\ 2^{'} . I (R) \to T^{'} : {n_{T}}_{k} \\ 3 . T \to R : {n_{T}^{'} \oplus n_{T}}_{k} \\ 3^{'} . T^{'} \to R : {n_{T} \oplus n_{T}^{'}}_{k} \end{array}$

A same tag starts two sessions1
¹
This is possible if different physical tags share the same identity, as may be the case e.g. in access control scenarios. In such cases, two different physical tags may run sessions concurrently.

and therefore generates two nonces $n_{T}$ and $n_{T}^{'}$ . The attacker answers to these requests by sending back the two encrypted messages to the tag who will accept both of them, and sends on the network two messages that are actually equal (the exclusive or operator is commutative). Therefore the attacker observes a test, namely the equality between the last two messages, which has no counterpart in the single session scenario. Therefore, this protocol does not ensure unlinkability. In practice, this can be very harmful. Suppose, for example, that tags are distributed among distinct groups (e.g. for access control policies) sharing each the same key k. By interacting with two tags, the attacker would then be able to know if they belong to the same group and thus be able to trace groups.

The previous example illustrates a general phenomenon: two-agent games do not capture concurrent attacks. This is also seen with the protocol of Example 9, which suffers from the attack shown in Example 15, but is secure in the sense of two-agent games – this can actually be proved in $ProVerif$ because the protocol does not involve the exclusive-or primitive. Due to this general weakness, two-agent games do not adequately express unlinkability. They are however convenient for automation, as they can be directly and accurately expressed using the notions of diff-equivalence available in $ProVerif$ or $Tamarin$ . For instance, two-agent games have been used in [11] for unbounded sessions of the DAA protocols – although in this work the security property expressed in this way is called pseudonymity rather than unlinkability.

As pointed out in [22], three-agent games have also been considered where the challenge phase is changed as follows: the attacker chooses three tags $(a, a_{1}, a_{2})$ and must distinguish interactions with several tags including tags x and y with the same identity as a, and interactions with x and y having the respective identities of $a_{1}$ and $a_{2}$ . This allows to capture the attacks described above which the two-agent games missed. Three-agent games have successfully been used in [21] for automated verification of unlinkability, though only for a restrictive class of protocols and for bounded sessions only.

We suspect that three-agent games still miss some linkability attacks, though counter-example protocols are likely to be artificial. Further generalisations of these games could then be considered to obtain stronger security properties, and get closer to our notion of unlinkability. In any case, it is important to remark that this line of thought fundamentally relies on having a centralised reader since the attacker must distinguish between scenarios that differ only in the identities of some tags. This contrasts with our notion of unlinkability, which does not assume a centralised reader but treats symmetrically the tag and reader role, more generally called initiator and responder. Such a symmetric treatment is required to model unlinkability when the two parties share a dedicated channel or have an initial shared knowledge, e.g. in secure messaging protocols. We also argue that our definition has some value even when analysing protocols featuring centralised readers. In such cases, having reader roles expecting a specific identity seems artificial, but it can actually be seen as a way to model the successive states of a reader (e.g. in LAK, where the tags and reader evolve a common state almost in synchronisation) or a pre-established communication (e.g. in BAC or PACE, where an optical scan is performed to securely exchange a first secret). In any case, our analysis of the aforementioned protocols using our notion of unlinkability has revealed actual attacks that were previously unknown (see Section 6).
4. Our approach

We now define our two conditions, namely frame opacity and well-authentication, and our result which states that these conditions are sufficient to ensure unlinkability and anonymity as defined in Section 3. Before doing that, we shall introduce annotations in the semantics of our processes, in order to ease their analysis.

4.1. Annotations

We shall now define an annotated semantics whose transitions are equipped with more informative actions. The annotated actions will feature labels identifying which concurrent process has performed the action. This will allow us to identify which specific agent (with some specific identity and session names) performed some action.

Given a protocol $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ and $\overline{i d} \subseteq \overline{k}$ , consider any execution of $M_{Π, \overline{id}}$ , $M_{Π}$ or $S_{Π}$ . In such an execution, τ actions are solely used to create new agents (i.e. instantiations of $I$ and $R$ with new names or constants from ${id}_{0}$ ) by unfolding replications (i.e. !) or repetitions (i.e. $!$ ), breaking parallel compositions or choosing fresh session and identity parameters. Actions other than τ (that is, input, output and conditionals) are then only performed by the created agents. Formally, we say that an agent is either an instantiation of one of the two roles with some identity and session parameters, or its continuation after the execution of some actions. When $†_{A} =!$ , agents of role A are simply found at toplevel in the multiset of processes. When $†_{A} =!$ , they may be followed by another process. For instance, in traces of $M_{Π}$ when $†_{I} =!$ , newly created initiator agents occur on the left of the sequence in processes of the form: $\begin{matrix} I {\overline{k} \mapsto \overline{l}, {\overline{n}}_{I} \mapsto \overline{n}};! new \overline{m} . I {\overline{k} \mapsto \overline{l}, {\overline{n}}_{I} \mapsto \overline{m}} . \end{matrix}$

The previous remark allows us to define an annotated semantics for our processes of interest. We consider annotations of the form $A (\overline{k}, \overline{n})$ where $A \in {I, R}$ and $\overline{k}$ , $\overline{n}$ are sequences of names, or constants from $\overline{{id}_{0}}$ . Annotations are noted with the letter a, and the set of annotations is noted $A$ . We can then define an annotated semantics, where agents are decorated by such annotations, indicating their identity and session parameters. An agent P decorated with the annotation a is written $P [a]$ , and the actions it performs are also decorated with a, written $α [a]$ . Note that this includes $τ_{then}$ and $τ_{else}$ actions; in the annotated semantics, the only non-annotated action is τ. For instance, let us consider $M_{Π}$ in the annotated semantics when $†_{I} =!$ . Newly created initiator agents now appear as $I {\overline{k} \mapsto \overline{l}, {\overline{n}}_{I} \mapsto \overline{n}} [I (\overline{l}, \overline{n})];! new \overline{m} . I {\overline{k} \mapsto \overline{l}, {\overline{n}}_{I} \mapsto \overline{m}}$ ; they execute actions of the form $α [I (\overline{l}, \overline{n})]$ with $α \neq τ$ ; upon termination of the agent, unannotated τ actions can be executed to create a new agent annotated $I (\overline{l}, \overline{m})$ for fresh names $\overline{m}$ . We stress that agents having constants $\overline{{id}_{0}}$ as identity parameters shall be annotated with some $A (\overline{k}, \overline{n})$ where $\overline{{id}_{0}} \subseteq \overline{k}$ . Intuitively, in such a case, we keep in the annotation the information that the identity parameters $\overline{{id}_{0}}$ of that agent has been disclosed to the attacker.

Traces of the annotated semantics will be denoted by $ta$ . We assume2

²
This assumption only serves the purpose of uniquely identifying agents. The assumed session nonces do not have to occur in the corresponding roles, so this does not require to change the protocol under study.

that

{\overline{n}}_{I} \neq \emptyset

and

{\overline{n}}_{R} \neq \emptyset

, so that at any point in the execution of an annotated trace, an annotation a may not decorate more than one agent in the configuration. Thus, an annotated action may be uniquely traced back to the annotated process that performed it. We also assume that labels used to decorate output actions (i.e. elements of

L

) are added to the produced output actions so that we can refer to them when needed: output actions are thus of the form

ℓ : out (c, w) [a]

In annotated traces, τ actions are not really important. We sometimes need to reason up to these τ actions. Given two annotated trace $ta$ and ${ta}^{'}$ , we write $ta \overset{τ}{=} {ta}^{'}$ when both traces together with their annotations are equal up to some τ actions (but not $τ_{then}$ and $τ_{else}$ ). We write $K \overset{ta}{\Rightarrow} K^{'}$ when $K \overset{{ta}^{'}}{\to} K^{'}$ for some ${ta}^{'}$ such that $ta \overset{τ}{=} {ta}^{'}$ . Example 18.

Considering the protocol $Π_{Fh}$ defined in Example 8, process $S_{Π_{Fh}}$ can notably perform the execution seen in Example 6. The annotated execution has the trace $ta$ given below (up to some τ), where $k^{'}$ , $n_{I}^{'}$ and $n_{R}^{'}$ are fresh names, $a_{I} = I (k^{'}, n_{I}^{'})$ and $a_{R} = R (k^{'}, n_{R}^{'})$ : $\begin{array}{l} ta = & ℓ_{1} : out (c_{I}, w_{1}) [a_{I}] . in (c_{R}, w_{1}) [a_{R}] . τ_{then} [a_{R}] . \\ ℓ_{2} : out (c_{R}, w_{2}) [a_{R}] . in (c_{I}, w_{2}) [a_{I}] . τ_{then} [a_{I}] . \\ ℓ_{3} : out (c_{I}, w_{3}) [a_{I}] . in (c_{R}, w_{3}) [a_{R}] . τ_{then} [a_{R}] \end{array}$ After the initial τ actions, the annotated configuration is $({I σ_{I} [a_{I}], R σ_{R} [a_{R}], S_{Π}}; \emptyset)$ where $σ_{I} = {k \mapsto k^{'}, n_{I} \mapsto n_{I}^{'}}$ , and $σ_{R} = {k \mapsto k^{'}, n_{R} \mapsto n_{R}^{'}}$ . The structure is preserved for the rest of the execution with three processes in the multiset (until they become null). After $ta$ , the annotated configuration is $({S_{Π_{Fh}}}; ϕ_{0})$ where $ϕ_{0}$ has been defined in Example 6.

Example 19.

Going back to Example 16 and starting with $M_{Π, \overline{id}}$ , a possible annotated configuration obtained after some τ actions can be $K = (P; \emptyset)$ where $P$ is a multiset containing:

$P_{C} {k_{C} \mapsto k_{C}^{0}, {id}_{C} \mapsto {id}_{0}, n_{C} \mapsto n_{C}^{0}, m \mapsto m_{C}^{0}} [a_{C}^{0}]$ ;

$! new (n_{C}, m) . P_{C} {k_{C} \mapsto k_{C}^{0}, {id}_{C} \mapsto {id}_{0}}$ ;

$P_{V} {n_{V} \mapsto n_{V}^{1}} [a_{V}^{1}]$ ; and

$M_{Π_{DAA}}$ .

where

a_{V}^{1} = I (ϵ, n_{V}^{1})

and

a_{C}^{0} = R ((k_{C}^{0}, {id}_{0}), (n_{C}^{0}, m^{0}))

. We may note that the annotation

a_{V}^{1}

contains the empty sequence ϵ since the initiator role does not rely on identity names; and the annotation

a_{C}^{0}

contains

{id}_{0}

4.2. Frame opacity

In light of attacks based on leakage from messages where non-trivial relations between outputted messages are exploited by the attacker to trace an agent, our first condition will express that all relations the attacker can establish on output messages only depend on what is already observable by him and never depend on a priori hidden information such as identity names of specific agents. Therefore, such relations cannot be exploited by the attacker to learn anything new about the agents involved in the execution. We achieve this by requiring that any reachable frame must be indistinguishable from an idealised frame that only depends on data already observed in the execution, and not on the specific agents (and their names) of that execution.

As a first approximation, one might take the idealisation of a frame ${w_{1} \mapsto u_{1}, \dots, w_{l} \mapsto u_{n}}$ to be ${w_{1} \mapsto n_{1}, \dots, w_{l} \mapsto n_{l}}$ where the $n_{1}, \dots, n_{l}$ are distinct fresh names. It would then be very strong to require that frames obtained in arbitrary protocol executions are statically equivalent to their idealisation defined in this way. Although this would allow us to carry out our theoretical development, it would not be realistic since any protocol using, e.g. a pair, would fail to satisfy this condition. We thus need a notion of idealisation that retains part of the shape of messages, which a priori does not reveal anything sensitive to the attacker. We also want to allow outputs to depend on session names or previous inputs in ways that are observable, e.g. to cover the output of the signature of a previously inputted message.

Our idealised frames will be obtained by replacing each message, produced by an output of label ℓ, by a context that only depends on ℓ, whose holes are filled with fresh session names and (idealisations of) previously inputted messages. Intuitively, this is still enough to ensure that the attacker does not learn anything that is identity-specific. In order to formalise this notion, we assume two disjoint and countable subsets of variables: input variables $X^{i} = {x_{1}^{i}, x_{2}^{i}, \dots} \subseteq X$ , and name variables $X^{n} = {x_{1}^{n}, x_{2}^{n}, \dots} \subseteq X$ . We also consider a fixed but arbitrary idealisation operator $ideal (\cdot) : L \to T (Σ, X^{i} \cup X^{n})$ . Variables $x_{j}^{i}$ intuitively refers to the j-nth variable received by the agent of interest. Therefore, we assume that our idealisation operator satisfies the following: for all $ℓ \in L$ , we have that $ideal (ℓ) \cap X^{i} \subseteq {x_{1}^{i}, \dots, x_{k}^{i}}$ where k is the number of inputs preceding the output labelled ℓ.

Definition 13.
Let $fr : A \times X^{n} \to N$ be an injective function assigning names to each agent and name variable. We define the idealised frame associated to $ta$ , denoted $Φ_{ideal}^{fr} (ta)$ , inductively on the annotated trace $ta$ :
$Φ_{ideal}^{fr} (ϵ) = \emptyset$ and $Φ_{ideal}^{fr} (ta . α) = Φ_{ideal}^{fr} (ta)$ if α is not an output;

$Φ_{ideal}^{fr} (ta . (ℓ : out (c, w) [a])) = Φ_{ideal}^{fr} (ta) \cup {w \mapsto ideal (ℓ) σ^{i} σ^{n} ⇓}$ where

$σ^{n} (x_{j}^{n}) = fr (a, x_{j}^{n})$ when $x_{j}^{n} \in X^{n}$ , and

$σ^{i} (x_{j}^{i}) = R_{j} Φ_{ideal}^{fr} (ta)$ when $x_{j}^{i} \in X^{i}$ and $R_{j}$ is the recipe corresponding to the jth input of agent a in $ta$ .

We may note this notion is not necessarily well-defined, as $ideal (ℓ) σ^{i} σ^{n}$ may not compute to a message. Note also that well-definedness does not depend on the choice of the function $fr$ . Remark also that, by definition, $Φ_{ideal}^{fr} (ta)$ never depends on the specific identity names occurring in $ta$ . In particular, idealised frames do not depend on whether agents rely on the specific constants $\overline{{id}_{0}}$ or not.
Example 20.
Continuing Example 18, we consider the idealisation operator defined as follows: $ℓ_{1} \mapsto x_{1}^{n}, ℓ_{2} \mapsto x_{2}^{n}, ℓ_{3} \mapsto x_{3}^{n}$ . Let $fr$ be an injective function such that $fr (a_{I}, x_{j}^{n}) = n_{j}^{I}$ and $fr (a_{R}, x_{j}^{n}) = n_{j}^{R}$ . We have that $Φ_{ideal}^{fr} (ta) = {w_{1} \mapsto n_{1}^{I}, w_{2} \mapsto n_{2}^{R}, w_{3} \mapsto n_{3}^{I}}$ .

On the latter simple example, such an idealisation will be sufficient to establish that any reachable frame obtained through an execution of $M_{Π_{Fh}}$ is indistinguishable from its idealisation. However, as illustrated by the following two examples, we sometimes need to consider more complex idealisation operators.
Example 21.
Continuing Example 9, to establish our indistinguishability property, namely frame opacity defined below, we will consider: $\begin{matrix} ℓ_{1} \mapsto x_{1}^{n}, ℓ_{2} \mapsto x_{2}^{n}, ℓ_{3} \mapsto x_{3}^{n}, ℓ_{4} \mapsto x_{4}^{n} \end{matrix}$ assuming that the four outputs are labelled with $ℓ_{1}$ , $ℓ_{2}$ , $ℓ_{3}$ , and $ℓ_{4}$ respectively.
Example 22.
Regarding Example 10, we also need to define an idealisation that retains the shape of the second outputted message. Moreover, the idealisation of the second outputted message will depend on the nonce previously received. Assuming that the outputs are labelled with $ℓ_{1}$ and $ℓ_{2}$ respectively, we consider: $ℓ_{1} \mapsto x_{1}^{n}, ℓ_{2} \mapsto zk (sign (⟨ x_{2}^{n}, x_{3}^{n} ⟩, s k_{I}), x_{2}^{n}, tuple (x_{1}^{i}, x_{4}^{n}, x_{5}^{n}, pk (s k_{I})))$ . Note that such an idealisation would not work for Example 11; there $s k_{I}$ is an identity-parameter which, following Definition 13, cannot occur in $ideal (ℓ_{2})$ . It turns out that frame opacity cannot be established (for any heuristics considered by our tool UKano) for a good reason: unlinkability fails to hold for this variant. Essentially, this is because verifiers send ZK proofs whose the public parts contain the public key of their issuers.

The following proposition establishes that the particular choice of $fr$ in $Φ_{ideal}^{fr} (ta)$ is irrelevant with respect to static equivalence. We can thus note $Φ_{ideal} (ta) \sim ϕ$ instead of there exists $fr$ such that $Φ_{ideal}^{fr} (ta) \sim ϕ$ .
Proposition 1.
Let $Φ_{ideal}^{fr} (ta)$ (resp. $Φ_{ideal}^{f r^{'}} (ta)$ ) be the idealised frame associated to $ta$ relying on $fr$ (resp. $f r^{'}$ ). We have that $Φ_{ideal}^{fr} (ta) \sim Φ_{ideal}^{f r^{'}} (ta)$ .
Proof.
It is sufficient to observe that $Φ_{ideal}^{fr} (ta)$ and $Φ_{ideal}^{f r^{'}} (ta)$ are equal up to a bijective renaming of names. □

We can now formalise the notion of frame opacity as announced: it requires that all reachable frames must be statically equivalent to idealised frames.
Definition 14.
The protocol Π ensures frame opacity w.r.t. $ideal$ if for any execution $(M_{Π, \overline{id}}; \emptyset) \overset{ta}{\to} (Q; ϕ)$ we have that $Φ_{ideal} (ta)$ is defined and $Φ_{ideal} (ta) \sim ϕ$ .

There are many ways to choose the idealisation operator $ideal (\cdot)$ . We present below a syntactical construction that is sufficient to deal with almost all our case studies. This construction has been implemented as a heuristic to automatically build idealisation operators in the tool $UKano$ . The tool $UKano$ also provides other heuristics that generally lead to better performance but are less tight (i.e. they cannot always be used to establish frame opacity). We explain how $UKano$ verifies frame opacity and compare the different heuristics it can leverage in Section 6.

At first reading, it is possible to skip the rest of the section and directly go to Section 4.3 since proposed canonical constructions are just instantiations of our generic notion of idealisation.
4.2.1. Syntactical idealisation

Intuitively, this construction builds the idealisation operator by examining the initiator and responder roles as syntactically given in the protocol definition. The main idea is to consider (syntactical) outputted terms one by one, and to replace identity parameters, as well as variables bound by a let construct by pairwise distinct names variables, i.e. variables in $X^{n}$ .

Definition 15.
Let $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ be a protocol that uses input variables ${x_{1}^{i}, x_{2}^{i}, \dots} \subseteq X^{i}$ (in this order) for its two roles, and distinct variables from $X_{let}$ in let constructions. Let $σ : \overline{k} \cup \overline{n_{R}} \cup \overline{n_{I}} \cup X_{let} \to X^{n}$ be an injective renaming. The syntactical idealisation operator maps any $ℓ \in L$ occurring in an output action $ℓ : out (c, u)$ in $I$ or $R$ (for some c and some u) to $u σ$ .
Example 23.
Continuing Example 8, we first perform some renaming to satisfy the conditions imposed by the previous definition. We therefore replace $x_{1}$ by $x_{1}^{i}$ in role $I$ , and $y_{1}, y_{2}$ by $x_{1}^{i}, x_{2}^{i}$ in role $R$ . We assume that $x_{2}, x_{3}$ , and $y_{3}$ are elements of $X_{let}$ . We consider a renaming σ that maps $k, n_{I}, n_{R}, x_{2}, x_{3}, y_{3}$ to $x_{1}^{n}, \dots, x_{6}^{n}$ . We obtain the following idealisation operator: $\begin{matrix} ℓ_{1} \mapsto x_{2}^{n}; ℓ_{2} \mapsto enc (⟨ x_{1}^{i}, x_{3}^{n} ⟩, x_{1}^{n}); ℓ_{3} \mapsto enc (⟨ x_{5}^{n}, x_{2}^{n} ⟩, x_{1}^{n}) . \end{matrix}$

Considering $fr$ as defined in Example 20, i.e. such that $fr (a_{I}, x_{j}^{n}) = n_{j}^{I}$ and $fr (a_{R}, x_{j}^{n}) = n_{j}^{R}$ , and relying on the idealisation operator defined above, and $ta$ as given in Example 18, we have that: $Φ_{ideal}^{fr} (ta) = {w_{1} \mapsto n_{2}^{I}, w_{2} \mapsto enc (⟨ n_{2}^{I}, n_{3}^{R} ⟩, n_{1}^{R}), w_{3} \mapsto enc (⟨ n_{5}^{I}, n_{2}^{I} ⟩, n_{1}^{I})}$ . This idealisation is different from the one described in Example 20, but it also allows us to establish frame opacity.
Example 24.
Continuing Example 10, we consider a renaming σ that maps: $k_{C}$ , ${id}_{C}$ , $n_{V}$ , $n_{C}$ , m, $x_{2}$ , $x_{3}$ , $x_{4}$ , $y_{3}$ to $x_{1}^{n}, x_{2}^{n}, \dots, x_{9}^{n}$ . We obtain the following idealisation operator: $\begin{matrix} ℓ_{1} \mapsto x_{3}^{n}; ℓ_{2} \mapsto zk (sign (⟨ x_{1}^{n}, x_{2}^{n} ⟩, s k_{I}), x_{1}^{n}, tuple (x_{1}^{i}, x_{4}^{n}, x_{5}^{n}, pk (s k_{I}))); ℓ_{3} \mapsto error . \end{matrix}$ Such an idealisation operator is also suitable to establish frame opacity.

As illustrated by the previous examples, the syntactical idealisation is sufficient to conclude on most examples. Actually, using this canonical construction, we automatically build the idealisation operator and check frame opacity for all the examples we have introduced in the previous sections and for most of the case studies presented in Section 6.
4.2.2. Semantical idealisation

The previous construction is clearly purely syntactic and therefore closely connected to the way the roles of the protocol are written. Its main weakness lies in the way variables are bound by let constructions. Since there is no way to statically guess the shape of messages that will be instantiated for those variables, the previous technique replaces them by fresh session names. False negatives may result from such over-approximations. We may therefore prefer to build an idealisation operator looking at the messages outputted during a concrete execution. In such a case, we may simply retain part of the shape of messages, which a priori does not reveal anything sensitive to the attacker (e.g. pairs, lists). This can be formalised as follows:

Definition 16.
A symbol $f$ (of arity n) in Σ is transparent if it is a public constructor symbol that does not occur in $E$ and such that: for all $1 ⩽ i ⩽ n$ , there exists a recipe $R_{i} \in T (Σ_{pub}, {w})$ such that for any message $u = f (u_{1}, \dots, u_{n})$ , we have that $R_{i} {w \mapsto u} ⇓ v_{i}$ for some $v_{i}$ such that $v_{i} =_{E} u_{i}$ .
Example 25.
Considering the signature and the equational theory introduced in Example 1 and Example 2, the symbols $⟨ ⟩$ and $ok$ are the only ones that are transparent. Regarding the pairing operator, the recipes $R_{1} = {proj}_{1} (w)$ and $R_{2} = {proj}_{2} (w)$ satisfy the requirements.

Once the set $Σ_{t}$ of transparent functions is fixed, the idealisation associated to a label ℓ occurring in Π will be computed relying on a particular (but arbitrary) message u that has been outputted with this label ℓ during a concrete execution of $M_{Π}$ . The main idea is to go through transparent functions until getting stuck, and then replacing the remaining sub-terms using distinct name variables from $X^{n}$ .
Example 26.
Considering the protocol given in Example 8, the resulting idealisation associated to Π (considering messages in $ϕ_{0}$ as defined in Example 6) is: $ℓ_{1} \mapsto x_{1}^{n}; ℓ_{2} \mapsto x_{2}^{n}; ℓ_{3} \mapsto x_{3}^{n}$ . Even if this idealisation operators is quite different from the one presented in Example 23. it is also suitable to establish frame opacity.

In [40], the idealisation operator associated to Π was exclusively computed using this method. The technique is implemented in the tool $UKano$ , and yields simple idealisations for which frame opacity often holds and can be established quickly. However, it happens to be insufficient to establish frame opacity in presence of function symbols that are neither transparent nor totally opaque such as signatures. Indeed, a signature function symbol is not transparent according to our definition: an attacker can make the difference between a signature $sign (m, s k (A))$ and a random nonce. Therefore, replacing such a term by a fresh session name will never allow one to establish frame opacity. That is why we also defined other types of idealisations that produce more complex idealised messages but allow for a much better level of precision. In practice, our tool UKano has three different built-in heuristics for computing idealisations which span the range between precision (syntactical idealisation) and efficiency (semantical idealisation).
4.3. Well-authentication

Our second condition will prevent the attacker from obtaining some information about agents through the outcome of conditionals. To do so, we will essentially require that conditionals of $I$ and $R$ can only be executed successfully in honest, intended interactions. However, it is unnecessary to impose such a condition on conditionals that never leak any information, which are found in several security protocols. We characterise below a simple class of such conditionals, for which the attacker will always know the outcome of the conditional based on the past interaction.

Definition 17.
For a protocol Π, a conditional $let \overline{z} = \overline{t} in P else Q$ occurring in $A \in {I, R}$ is safe if $\overline{t} \in T (Σ_{pub}, {x_{1}, \dots, x_{n}} \cup {u_{1}, \dots, u_{m}})$ , where the $x_{i}$ are the variables bound by the previous inputs of that role, and $u_{i}$ are the messages used in the previous outputs of that role.
Example 27.
Consider the process $out (c, u) . in (c, x) . let z = neq (x, u) in P else Q$ . The conditional is used to ensure that the agent will not accept as input the message he sent at the previous step. Such a conditional is safe according to our definition.

Note that trivial conditionals required by the grammar of protocols (Definition 3) are safe and will thus not get in the way of our analysis. We can now formalise the notion of association, which expresses that two agents are having an honest, intended interaction, i.e. the attacker essentially did not interfere in their communications. For an annotated trace $ta$ and annotations a and $a^{'}$ , we denote by $ta |_{a, a^{'}}$ the subsequence of $ta$ that consists of actions of the form $α [a]$ or $α [a^{'}]$ .
Definition 18.
Given a protocol Π, two annotations $a_{1} = A_{1} ({\overline{k}}_{1}, {\overline{n}}_{1})$ and $a_{2} = A_{2} ({\overline{k}}_{2}, {\overline{n}}_{2})$ are associated in $(ta, ϕ)$ if:
they are dual, i.e. $A_{1} \neq A_{2}$ , and $\overline{k_{1}} = \overline{k_{2}}$ when $fn (R) \cap fn (I) \neq \emptyset$ (the shared case);

the interaction $ta |_{a_{1}, a_{2}}$ is honest for ϕ (see Definition 4).

Example 28.
Continuing Example 18, $I (k^{'}, n_{I}^{'})$ and $R (k^{'}, n_{R}^{'})$ are associated in $(ta, ϕ_{0})$ .

Finally, we can state our second condition.
Definition 19.
The protocol Π is well-authenticating if, for any $(M_{Π, \overline{id}}; \emptyset) \overset{ta . τ_{then} [a]}{\to} (P; ϕ)$ , either the last action corresponds to a safe conditional of $I$ or $R$ , or there exists $a^{'}$ such that:
The annotations a and $a^{'}$ are associated in $(ta, ϕ)$ ;

Moreover, when $fn (R) \cap fn (I) \neq \emptyset$ (the shared case), $a^{'}$ (resp. a) is only associated with a (resp. $a^{'}$ ) in $(ta, ϕ)$ .

Intuitively, this condition does not require anything for safe conditionals as we already know that they cannot leak new information to the attacker (he already knows their outcome). For unsafe conditionals, condition (i) requires that whenever an agent a evaluates them positively (i.e. he does not abort the protocol), it must be the case that this agent a is so far having an honest interaction with a dual agent $a^{'}$ . Indeed, as discussed in Introduction, it is crucial to avoid such unsafe conditionals to be evaluated positively when the attacker is interfering because this could leak crucial information. In the rest of the paper, when considering a protocol Π, we will say that a conditional in a process resulting from $M_{Π, \overline{id}}$ or $S_{Π}$ is safe when it corresponds to a safe conditional in $I$ or $R$ .

As illustrated in the following example, condition (ii) is needed to prevent from having executions where an annotation is associated to several annotations, which would break unlinkability in the shared case (i.e. when $fn (R) \cap fn (I) \neq \emptyset$ ).
Example 29.
We consider a protocol between an initiator and a responder that share a symmetric key k. The protocol can be described informally as follows: $\begin{array}{l} 1 . I \to R : {n_{I}}_{k} \\ 2 . R \to I : n_{R} \end{array}$

Assuming that the two outputs are labelled with $ℓ_{1}$ and $ℓ_{2}$ respectively, the idealisation operator $ℓ_{1} \mapsto x_{1}^{n}$ , $ℓ_{2} \mapsto x_{2}^{n}$ is suitable to establish frame opacity. We may note that the only conditional is the one performed by the responder role when receiving the ciphertext. He will check whether it is indeed an encryption with the expected key k. When an action $τ_{then} [R (k, n_{R})]$ occurs, it means that a ciphertext encrypted with k has been received by $R (k, n_{R})$ and since the key k is unknown by the attacker, such a ciphertext has been sent by a participant: this is necessarily a participant executing the initiator role with key k. Hence condition (i) of well-authentication holds (and can actually be formally proved). However, condition (ii) fails to hold since two responder roles may accept a same ciphertext ${n_{I}}_{k}$ and therefore be associated to the same agent acting as an initiator. This corresponds to an attack scenario w.r.t. our formal definition of unlinkability since such a trace will have no counterpart in $S_{Π}$ . More formally, the trace $tr = out (c_{I}, w_{0}) . in (c_{R}, w_{0}) . τ_{then} . out (c_{R}, w_{1}) . in (c_{R}, w_{0}) . τ_{then} . out (c_{R}, w_{2})$ will be executable starting from $M_{Π}$ and will allow one to reach $ϕ = {w_{0} \mapsto enc (n_{I}, k); w_{1} \mapsto n_{R}; w_{2} \mapsto n_{R}^{'}}$ . Starting from $S_{Π}$ the second action $τ_{then}$ will not be possible, and more importantly this will prevent the observable action $out (c_{R}, w_{2})$ to be triggered.

While the condition (i) of well-authentication is verifiable quite easily by expressing it as simple reachability properties (as explained in Section 5.2), the required condition (ii) for the shared-case is actually harder to express in existing tools. We therefore shall prove that, for the shared case, once condition (i) of well-authentication is known to hold, condition (ii) is a consequence of two simpler conditions that are easier to verify (as shown in Section 5.2.2). First, the first conditional of the responder role should be safe – remark that if this does not hold, similar attacks as the one discussed above may break unlinkability. Second, messages labelled by some ℓ outputted in honest interactions by different agents should always be different. Lemma 1.
Let $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ be a protocol such that $fn (I) \cap fn (R) \neq \emptyset$ (shared case) that satisfies condition (i) of well-authentication. Then well-authentication holds provided that:
the first conditional that occurs in $R$ is safe;

for any execution $(M_{Π, \overline{id}}; \emptyset) \overset{ta}{\to} (P; ϕ)$ , if ${ta}_{1} = ta |_{a_{1}, b_{1}}$ and ${ta}_{2} = ta |_{a_{2}, b_{2}}$ are honest with $a_{1} \neq a_{2}$ then for any $ℓ : out (c, w_{1}) [a_{1}] \in {ta}_{1}$ and $ℓ : out (c, w_{2}) [a_{2}] \in {ta}_{2}$ then $ϕ (w_{1}) \neq_{E} ϕ (w_{2})$ .

Proof.
Consider an execution $M_{Π, \overline{id}} \overset{ta . τ_{then} [a^{'}]}{\to} (P; ϕ)$ where two agents a and $a^{'}$ are associated and $a^{'}$ has performed the last $τ_{then}$ . If this test corresponds to a safe conditional, there is nothing to prove. Otherwise, we shall prove that a is only associated to $a^{'}$ , and vice versa.

Agent $a^{'}$ is only associated to a. Consider the last input of $a^{'}$ (the one just before $τ_{then} [a^{'}]$ ) and the output of a that occurs before this input of $a^{'}$ : $\begin{matrix} M_{Π, \overline{id}} \overset{ta . out (c, w_{ℓ}) [a] . {ta}^{'} . in (c^{'}, R) [a^{'}] . {ta}^{″} . τ_{then} [a^{'}]}{\to} (P; ϕ) \end{matrix}$ We have $R ϕ ⇓ ϕ (w_{ℓ})$ where $w_{ℓ}$ is labelled ℓ. Assume, for the sake of contradiction, that $a^{'}$ is associated to another agent $b \neq a$ . Then, we have $R ϕ ⇓ =_{E} ϕ (w_{ℓ}^{'})$ for some handle, and thus thanks to Item 6 of Definition 1, we have that $ϕ (w_{ℓ}) =_{E} ϕ (w_{ℓ}^{'})$ , for a handle $w_{ℓ}^{'}$ corresponding to some output of b labelled ℓ in the honest trace $ta |_{a^{'}, b}$ . This contradicts assumption (b).

Agent a is only associated to $a^{'}$ . Agent a must have performed an input in $ta$ : this is obvious if a is a responder, and follows from assumption (a) otherwise. Let $ℓ : out (c, w_{ℓ}) [a^{'}]$ be the output label (with annotation $a^{'}$ ) occurring in $ta$ just before the input of a mentioned above. The considered execution is thus of the following form: $\begin{matrix} M_{Π, \overline{id}} \overset{ta . out (c, w_{ℓ}) [a^{'}] . {ta}^{'} . in (c, R) [a] . {ta}^{″} . τ_{then} [a^{'}]}{\to} (P; ϕ) \end{matrix}$ We know that the message m, satisfying $R ϕ ⇓ m$ , which is inputted by a is equal (modulo $E$ ) to the previous output of $a^{'}$ , that is $ϕ (w_{ℓ})$ . As for the previous case, condition (b) implies that it cannot be equal to the output of another agent having an honest interaction in $ta$ , thus a is only associated to $a^{'}$ . □

4.4. Main result

Our main theorem establishes that the previous two conditions are sufficient to ensure unlinkability and anonymity.

Theorem 1.
Consider a protocol $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ and some identity names $\overline{i d} \subseteq \overline{k}$ . If the protocol ensures both well-authentication and frame opacity w.r.t. $\overline{i d}$ , then Π ensures unlinkability and anonymity w.r.t. $\overline{i d}$ .

Note that, when $\overline{i d} = \emptyset$ , we have that $M_{Π, \overline{i d}} \approx M_{Π}$ and our two conditions coincide on $M_{Π, \overline{i d}}$ and $M_{Π}$ . We thus have as a corollary that if $M_{Π}$ ensures well-authentication and frame opacity, then Π is unlinkable.

The proof of this theorem is detailed in Appendix B, and we explain in Section 5 how to check these two conditions in practice relying on existing verification tools. We apply our method on various case studies that are detailed in Section 6. Below, we only briefly summarize the result of the confrontation of our method to our various running examples, focusing on unlinkability.

We note ✓ for a condition automatically checked using $UKano$ and ✕ when the condition does not hold. For the analysis of the Toy protocol with $!$ , we do not rely on $UKano$ (which is based on $ProVerif$ ) since $ProVerif$ does not support the $!$ operator. We establish the well-authentication property using $Tamarin$ and frame opacity using $ProVerif$ by allowing sessions to run concurrently and thus doing a sound over-approximation of the protocol’s behaviors. Frame opacity has been established relying on the syntactical idealisation as well as the semantical one, except for Example 10. Indeed, as explained at the end of Section 4.2, the semantical idealisation is not suitable in this case.
5. Mechanization

We now discuss how to verify unlinkability and anonymity in practice, through the verification of our two conditions. More specifically, we describe how appropriate encodings allow one to verify frame opacity (Section 5.1) and well-authentication (Section 5.2), respectively through diff-equivalence and correspondence properties in $ProVerif$ .

We additionally provide a tool, called $UKano$ [51] (Section 5.3), which mechanises the encodings described in this section. Our tool takes as input a specification of a protocol in our class, computes encodings, and calls $ProVerif$ to automatically check our two conditions, and thus unlinkability and anonymity. As briefly mentioned in Section 4 and detailed in Section 6, $UKano$ concludes on many interesting case studies.

5.1. Frame opacity

We shall describe how to encode frame opacity using the diff-equivalence of $ProVerif$ [18]. In a nutshell, we will check this strong notion of equivalence between $M_{Π, \overline{id}}$ and a modified version of it that produces idealised outputs instead of real ones, in order to check static equivalence between all pairs of frames of the form $(Φ, Φ_{ideal} (ta))$ where $ta$ is executable by $M_{Π, \overline{id}}$ and Φ is the resulting frame. The main issue in implementing this idea arises from diff-equivalence being too strong regarding tests and computations of idealized terms. In [40], we had proposed a solution that avoided this problem by largely over-approximating the set of executable traces, which is sound but very imprecise. Moreover, this first solution is only adequate for the notion of idealization considered in [40], and not for the generalization proposed in the present paper. We describe below a simpler solution, that is much more precise and efficient, and can accommodate our generalized notion of idealization, at the cost of a slight extension of $ProVerif$ ’s diff-equivalence. We shall start with a brief reminder on diff-equivalence in $ProVerif$ , in order to describe how we extend it, before showing how this extension allows us to naturally encode frame opacity.

Diff-equivalence. Intuitively, diff-equivalence is obtained from trace equivalence by forcing the two processes (or configurations) being compared to follow the same execution. It has been introduced in [18] as a means to automatically verify observational equivalence in $ProVerif$ . This paper deals with the full process algebra supported by $ProVerif$ , which is more general but compatible with the process algebra of the present paper, the main difference being that we do not account for private channels. Processes of [18] are equipped with a reduction semantics, noted $P \to P^{'}$ . This allows to define observational equivalence, which implies trace equivalence in our sense. The key notion in [18] is that of a bi-process, that is a process in which some terms are replaced by bi-terms of the form $choice [u_{1}, u_{2}]$ . Given a bi-process P, its first projection $fst (P)$ is defined by taking the first component of all choice operators occurring in it. The second projection $snd (P)$ is defined analogously. Bi-processes are given a reduction semantics by taking the same rules as those for processes (which we do not recall) with three modified rules:3

³
We use our own notations here, taking advantage of the fact that our calculus is a simplification of the one used in [18]: in particular, channels are public constants and choice operators cannot be used in channel positions. We also use the notation $choice [\cdot, \cdot]$ as in the tool $ProVerif$ , rather than $diff [\cdot, \cdot]$ as in [18].

\begin{matrix} out (c, u) . Q ∣ in (c, x) . P \to Q ∣ P {x \mapsto u} & (Red I/O) \\ let \overline{x} = \overline{t} in P else Q \to P {\overline{x} \mapsto choice [{\overline{u}}_{1}, {\overline{u}}_{2}]} & if fst (\overline{t}) ⇓ {\overline{u}}_{1} and snd (\overline{t}) ⇓ {\overline{u}}_{2} & (Red Fun 1) \\ let \overline{x} = \overline{t} in P else Q \to Q & if fst (\overline{t}) ⇓̸ and snd (\overline{t}) ⇓̸ & (Red Fun 2) \end{matrix}

A bi-process execution step thus consists of strongly synchronized execution steps of its two projections. In particular, a conditional in a bi-process succeeds (resp. fails) if it succeeds (resp. fails) for both of its projections. Formally, we have that

P \to P^{'}

implies

fst (P) \to fst (P^{'})

and

snd (P) \to snd (P^{'})

. However, it could be that some execution step of

fst (P)

(resp.

snd (P)

) cannot be obtained in this way from an execution step of P. In fact, [18, Theorem 1] shows that the two projections of a bi-process P are observationally equivalent if, for all C, all reducts of

C [P]

are uniform in the following sense:

Definition 20 ([18]).

A bi-process P is uniform if for all reductions $fst (P) \to P_{1}$ , there exists $P^{'}$ such that $P \to P^{'}$ and $fst (P^{'}) = P_{1}$ , and symmetrically for $snd (P)$ .

From now on, we say that a bi-process is diff-equivalent when it satisfies the condition of [18, Theorem 1]. By extension, we say that the two projections of a bi-process are diff-equivalent when the bi-process is.

Diff-equivalence verification in $ProVerif$ . The next contribution of [18] is to show that diff-equivalence can be automatically verified in $ProVerif$ by adapting its Horn clause encoding and resolution algorithm to bi-processes. We will not recall the encoding and its modifications in detail here, but only present some key ideas at a high level. In the single-process case, a unary predicate $att (\cdot)$ is used to encode that the attacker knows some message. The attacker’s capabilities are expressed as Horn clauses involving this predicate, e.g. the ability to encrypt is translated as $\begin{matrix} \forall x \forall y . att (x) \land att (y) \Rightarrow att (enc (x, y)) . \end{matrix}$ Then, a process fragment of the form $in (c, x) . let y = dec (x, k) in out (c^{'}, t)$ , where t is a constructor term with free variable y, is encoded as $\begin{matrix} \forall y . att (enc (y, k)) \Rightarrow att (t) . \end{matrix}$ Note that the variable x does not appear in the clause, but has been refined into $enc (y, k)$ as part of the translation.

Consider now the analogue bi-process fragment $\begin{matrix} in (c, x) . let y = dec (x, k) in out (c^{'}, choice [t_{1}, t_{2}]) . \end{matrix}$ It corresponds to two processes, each of which may receive a message and attempt to decrypt it using k. Upon success, the processes output $t_{1}$ and $t_{2}$ respectively, relying on the value y obtained from the respective decryptions. In $ProVerif$ , this bi-process would translate into the Horn clause $\begin{matrix} \forall y_{1} \forall y_{2} . {att}^{'} (enc (y_{1}, k), enc (y_{2}, k)) \Rightarrow {att}^{'} (t_{1}^{'}, t_{2}^{'}) \end{matrix}$ where $t_{1}^{'}$ (resp. $t_{2}^{'}$ ) is $t_{1}$ (resp. $t_{2}$ ) in which all the occurrences of y have been replaced by $y_{1}$ (resp. $y_{2}$ ). This time, a binary predicate ${att}^{'} (\cdot, \cdot)$ is used to encode the attacker’s knowledge on each side of the bi-process run: the clause roughly says that if, at some point of the execution of the bi-process, the attacker can deduce (using the same derivation) a term of the form $enc (y_{1}, k)$ from the left frame and a term $enc (y_{2}, k)$ from the right frame, then he will learn $t_{1}$ on the left and $t_{2}$ on the right. The attacker’s capabilities are also modified to encode the effect of the attacker’s capabilities on each side of the bi-process run, e.g. for encryption: $\begin{matrix} \forall x_{1} \forall x_{2} \forall y_{1} \forall y_{2} . {att}^{'} (x_{1}, x_{2}) \land {att}^{'} (y_{1}, y_{2}) \Rightarrow {att}^{'} (enc (x_{1}, y_{1}), enc (x_{2}, y_{2})) . \end{matrix}$

An extension of bi-processes. In the original notion of bi-processes [18], the two sides of a bi-process are isolated and can execute independently. However, the Horn clause encoding of bi-processes that is used for verification in $ProVerif$ makes it easy to lift this restriction in a way that enables interesting new applications of diff-equivalence. Specifically, we introduce the possibility of binding two variables at once in a bi-process input, which we write $in (c, choice [x_{1}, x_{2}]) . P$ . For simplicity, we can consider that all inputs feature such choice variables, as the usual form $in (c, x) . P$ can be replaced by $in (c, choice [x_{1}, x_{2}]) . P {x \mapsto choice [x_{1}, x_{2}]}$ . The intuitive semantics of such a construct is that $x_{1}$ is bound to the message received on the left side of the bi-process run, while $x_{2}$ is bound to the message received on the right. Formally, we change the (Red I/O) rule as follows: $\begin{matrix} out (c, u) . Q ∣ in (c, choice [x_{1}, x_{2}]) . P \to Q ∣ P {x_{1} \mapsto fst (u), x_{2} \mapsto snd (u)} . \end{matrix}$ Crucially, each side of the bi-process will then have access to both $x_{1}$ and $x_{2}$ , allowing a form of communication between the two sides.

With this modification, [18, Theorem 1] does not hold anymore. In fact, $fst (P)$ and $snd (P)$ may not be ground processes when P uses choice variables in inputs, so that it does not even make sense to compare them for observational equivalence. More generally, we cannot talk in general of the projection of a bi-process execution: the fact that $P \to P^{'}$ implies $fst (P) \to fst (P^{'})$ becomes not only false but also ill-defined in general. However, the notion of uniformity is still meaningful, if properly adapted to be mathematically well-defined: a bi-process P is uniform if, whenever $fst (P)$ is ground, it is the case that for all reductions $fst (P) \to P_{1}$ there exists $P^{'}$ such that $P \to P^{'}$ and $fst (P^{'}) = P_{1}$ , and symmetrically for $snd (P)$ . Furthermore, we shall see that it can be useful in cases where at least one projection of the executions of a bi-process is well-defined, as will be the case with our encoding of the notion of frame opacity through (extended) diff-equivalence.

Besides the problem of the new meaning of diff-equivalence, an important question is whether extended diff-equivalence can be verified automatically, and how. We claim that it is straightforward, as the Horn clause encoding of bi-processes already features what is needed for adequately encoding extended bi-processes, namely the duplicated input variables seen in the above example – accordingly, we only had to modify a few tenth of lines of the $ProVerif$ tool to implement our extension. A formal justification of this claim would require to adapt the long technical development of [18], and is thus out of the scope of the present paper. We simply illustrate the idea here by getting back to our running example illustrating the various Horn clause encodings, considering now the process fragment $\begin{matrix} in (c, choice [x_{1}, x_{2}]) . let y = dec (x_{1}, k) in out (c^{'}, choice [t_{1}, t_{2}]) \end{matrix}$ where $t_{1}$ and $t_{2}$ are constructor terms with free variable y. This would be encoded as $\begin{matrix} \forall y_{1} \forall x_{2} . {att}^{'} (enc (y_{1}, k), x_{2}) \Rightarrow {att}^{'} (t_{1}^{'}, t_{2}^{'}) \end{matrix}$ where $t_{1}^{'}$ (resp. $t_{2}^{'}$ ) is $t_{1}$ (resp. $t_{2}$ ) in which all the occurrences of y have been replaced by $y_{1}$ . This time, $x_{2}$ is not refined since the bi-process does not attempt to deconstruct it, on either side. The clause expresses that if the attacker can derive a term $enc (y_{1}, k)$ on the left (regardless of what would be the corresponding term on the right) then he will learn $t_{1}^{'}$ on the left and $t_{2}^{'}$ on the right.

Encoding frame opacity through extended diff-equivalence. Using this extended notion of bi-process, we can now directly express frame opacity as the diff-equivalence of a bi-process. This bi-process will have $M_{Π, \overline{id}}$ as its first projection. Its second projection should replace each message output with its idealization, so that diff-equivalence of $P^{ideal}$ implies $Φ \sim Φ_{ideal} (ta)$ for any $ta$ that is executable by $M_{Π, \overline{id}}$ with Φ as the resulting frame. In itself, this can be achieved easily, as it suffices to create new names to use as values for $X^{n}$ variables and use appropriate input variables for the $X^{i}$ variables. The difficulty lies with tests (and computation failures) which need to be carefully used to obtain a correct encoding of frame opacity.

First, we need to ensure that any reduction of $M_{Π, \overline{id}}$ (in any context) can be obtained as the projection of a reduction of $P^{ideal}$ (in the same context). In other words, the second projection of any test should agree with its first projection, which corresponds to a normal execution of $M_{Π, \overline{id}}$ . This would not hold in general if we performed the same test on the idealizations which are computed in the second projection. We obtain the desired behaviour using our extension of bi-processes, by performing tests using only left-hand side input variables.

Second, we need to ensure that computation failures that occur while computing idealizations result in a diff-equivalence failure. This is necessary to obtain a match with frame opacity, which requires that idealizations are well-defined even when destructors are involved. Hence, when the bi-process computes idealized values in its second projection, a failsafe computation should happen in the first projection. Moreover, idealizations should be computed using the values of the input variables from the right side of the bi-process execution, in line with the definition of idealization, i.e. Definition 13.

Fig. 4.

Our running example (Feldhofer) using $ProVerif$ ’s syntax.

Before proving more formally that our translation is adequate, let us illustrate it on our running example, i.e. Example 8. We first give in Fig. 4 the description of the protocol in $ProVerif$ syntax. This syntax is actually very close to the one we introduced in Section 2. The main difference is the fact that $ProVerif$ relies on types, and here any name or variable is given the generic type bitstring. Next, we show in Fig. 5 the bi-process expressing frame opacity as described above, using the syntaxic idealisation (Section 4.2.1). Note that, when decrypting the first input of the initiator role, the variable x is used, corresponding to the left side of the bi-process execution. The variable xid, correspond to the right (idealized) side, is not used in that case because this input is not used in idealizations. However, the variable ynIid corresponding to an idealized input in the responder role is used in the first output. In this example, the idealisation operator does not contain any destructor, hence the computation of the idealisation can never fail. If destructors were present, they would be computed using $let$ constructs inside the right component of the $choice [\cdot, \cdot]$ operator4

⁴

This is not possible with the theoretical notion of bi-process, where $choice [\cdot, \cdot]$ operators can only contain terms, which cannot contain $let$ constructs. However, it is available in (vanilla) $ProVerif$ as syntactic sugar: it is equivalent to performing the $let$ outside the $choice [\cdot, \cdot]$ with a dummy first projection, which is exactly what we need.

in output, so that their failure would result in a non-equivalence.

We now conclude with a formal correctness argument.

Proposition 2.

Let $ideal$ be an idealisation operator, and note $P^{ideal}$ the corresponding encoding of a process P into a bi-process. Assume that, for all C and B such that $C [P^{ideal}] \to^{*} B$ , B is uniform. Then P satisfies frame opacity wrt. $ideal$ .

Proof.

Assume, by contradiction, that there exists an execution $(P; \emptyset) \overset{ta}{\to} (Q; Φ)$ with $Φ ≁ Φ_{ideal} (ta)$ . Then there exists a test $T = (let \overline{y} = \overline{u} in out (o, ok))$ with $fv (T) = fv (\overline{u}) \subseteq dom (Φ)$ such that $T Φ$ can perform an output (after the successful evaluation of its $let$ ) while $T Φ_{ideal} (ta)$ cannot. Further, we can construct in a standard way5

⁵

Define $C_{ta} [∙] = (∙ ∣ T_{ta})$ with $T_{ϵ} = T$ , $T_{τ . ta} = T_{ta}$ , $T_{out (c, w) . ta} = in (c, w) . T_{ta}$ and $T_{in (c, R) . ta} = out (c, R) . T_{ta}$ . In full details, the last case should include the creation of names that are used in R but not previously in the trace.

from

ta

a context

C_{ta}

such that

C_{ta} [P] \to^{*} T Φ

, with only communications and internal reductions of P in that reduction. Because of this, the reduction can be lifted to the idealized bi-process as follows, by definition of

P^{ideal}

\begin{matrix} C_{ta} [P^{ideal}] \to^{*} T^{'} = T {w \mapsto choice [Φ (w), Φ_{ideal} (ta) (w)]}_{w \in dom (Φ)} \end{matrix}

We have obtained our contradiction, since

T^{'}

is not uniform: indeed, the reduction step

fst (T^{'}) \to out (c, ok)

cannot be obtained as a projection of a reduction of

T^{'}

, which in fact cannot perform any reduction at all. □

Fig. 5.

$ProVerif$ file checking frame opacity generated by $UKano$ (Feldhofer).

Practical application. Our tool $UKano$ automatically constructs the bi-process described above from a description of the protocol, and calls the extension of $ProVerif$ in order to check frame opacity. Until this extension is integrated in the next release of $ProVerif$ , the source files of this slight extension of $ProVerif$ are distributed with $UKano$ [51]. Out tool does not require the user to input the idealisation function. Instead, a default idealisation is extracted from the protocol’s outputs. The user is informed about this idealisation, and if he wants to, he can bypass it using annotations or choose another heuristic to build idealisation operators. In practice, this is rarely necessary; we provide more details about this in Section 5.3. Also note that, although $ProVerif$ does not support the repetition operator $!$ , we can over-approximate the behaviours of protocols using it by replacing occurrences of $!$ with ! before checking frame opacity.

5.2. Well-authentication

We explain below how to check condition (i) of well-authentication (see Definition 19). Once that condition is established, together with frame opacity, we shall see that condition (ii) is actually a consequence of a simple assumption on the choice of idealisation, which is always guaranteed when using $UKano$ . This result is established relying on the sub-conditions that have been proved to be sufficient in Lemma 1.

5.2.1. Condition (i)

Condition (i) of well-authentication is basically a conjunction of reachability properties, which can be checked in $ProVerif$ using correspondence properties [1]. To each syntactical output $out (c, m_{0})$ of the initiator role, we associate an event, namely ${Iout}_{i} ({\overline{k}}_{I}, {\overline{n}}_{I}, {\overline{m}}_{I})$ which uniquely identifies the action. We have that:

${\overline{k}}_{I}$ are the identity parameters used in the intiator role;

${\overline{n}}_{I}$ are the sessions parameters; and

${\overline{m}}_{I}$ are the messages inputted and outputted so far in this role including $m_{0}$ .

Such an event is placed just before the action

out (c, m_{0})

. We proceed similarly for each syntactical input

in (c, m_{0})

putting the event

Ii n_{i} ({\overline{k}}_{I}, {\overline{n}}_{I}, {\overline{m}}_{I})

just after the corresponding input. Lastly, we also apply this transformation on the responder role using events of the form

Rou t_{i} ({\overline{k}}_{R}, {\overline{n}}_{R}, {\overline{m}}_{R})

and

Ri n_{i} ({\overline{k}}_{R}, {\overline{n}}_{R}, {\overline{m}}_{R})

. To be able to express condition (i) relying on events, we need to consider some events that will be triggered when conditional are passed successfully. Therefore, we add events of the form

Ites t_{i} ({\overline{k}}_{I}, {\overline{n}}_{I}, {\overline{m}}_{I})

(resp.

Rtes t_{i} ({\overline{k}}_{R}, {\overline{n}}_{R}, {\overline{m}}_{R})

) at the beginning of each

then

branch of the initiator (resp. responder) role.

For each conditional of the protocol, we first check if the simple syntactical definition of safe conditionals holds (see Definition 17). If it is the case we do nothing for this conditional. Otherwise, we need to check condition (i) of well-authentication. This condition can be easily expressed as a correspondence property relying on the events we have introduced. Let ${\overline{k}}_{I} = (k_{I}^{1}, \dots, k_{I}^{p})$ and ${\overline{k}}_{R} = (k_{R}^{1}, \dots, k_{R}^{q})$ . We denote ${\overline{x}}_{I} = (x_{k_{I}^{1}}, \dots, x_{k_{I}^{p}})$ and ${\overline{x}}_{R} = (x_{k_{R}^{1}}, \dots, x_{k_{R}^{q}})$ . Note that when ${\overline{k}}_{I} \cap {\overline{k}}_{R} \neq \emptyset$ (shared case), we have also that ${\overline{x}}_{I} \cap {\overline{x}}_{R} \neq \emptyset$ and the correspondence property (see below) will therefore allow us to express duality of the two underlying agents.

For instance, given a conditional of the initiator role tagged with event $Ites t_{i} ({\overline{k}}_{I}, {\overline{n}}_{I}, {\overline{m}}_{I})$ , we express as a correspondence property the fact that if the conditional is positively evaluated, then the involved agent must be associated to a dual agent as follows:

when the event $Ites t_{i} ({\overline{x}}_{I}, {\overline{y}}_{I}, (z_{1}, \dots, z_{ℓ}))$ is fired,

there must be a previous event $Ii n_{i} ({\overline{x}}_{I}, {\overline{y}}_{I}, (z_{1}, \dots, z_{ℓ}))$ (the one just before the conditional),

and a previous event $Rou t_{j} ({\overline{x}}_{R}, {\overline{y}}_{R}, (z_{1}, \dots, z_{ℓ}))$ (the one corresponding to the output that fed the input $Ii n_{i}$ in an honest execution),

and a previous event $Ri n_{j} ({\overline{x}}_{R}, {\overline{y}}_{R}, (z_{1}, \dots, z_{ℓ - 1}))$ (the one just before the output $Rou t_{j}$ ), etc.

Note that by using the same variables (

z_{1}, \dots, z_{ℓ}

) in both the intiator and responder roles, we express that the messages that are outputted and inputted are equal modulo the equational theory

E

. We provide in Fig. 6 the process obtained by applying the transformation on the Feldhofer protocol (Example 8). In Fig. 7, we show the

ProVerif

queries we have to consider to check condition (i) on the two conditionals.

Fig. 6.

Process modelling the Feldhofer protocol with events.

Fig. 7.

$ProVerif$ queries for checking condition (i) on the Feldhofer protocol.

Some practical considerations. In our tool, safe conditionals are not automatically identified. Actually, the tool lists all conditionals and tells which ones satisfy condition (i) of well-authentication. The user can thus easily get rid of the conditionals that he identifies as safe. Furthermore, the structure of the $ProVerif$ file produced by $UKano$ makes it easy for the user to remove the proof obligations corresponding to safe conditionals. To obtain more precise encodings once the translation in Horn clauses is performed by $ProVerif$ , we sometimes push the creation of session parameters (i.e. instructions of the form $new nI$ ). Therefore, in order to ensure the existence of at least one session parameter in each event, we systematically introduce a fresh session parameter sessI (resp. sessR) which is generated at the beginning of the initiator (resp. responder) role. Such parameters are systematically added in the events, and since they do not occur in the messages exchanged during the protocol execution, there is no need to push them.

Note that, for some examples, we also verified condition (i) of well-authentication using $Tamarin$ by encoding the queries described above as simple lemmas. In our case, one of the most important advantage of $Tamarin$ over $ProVerif$ is its capability to model the repetition operator $!$ and thus protocols for which a role executes its sessions in sequence. Relying on $Tamarin$ , we were thus able to verify condition (i) for protocols that ensure unlinkability when sessions are running sequentially but not when they are running concurrently, e.g. we automatically verified the toy example described in Example 9.

5.2.2. Condition (ii) – shared case

To verify Condition (ii) of well-authentication, we rely on Lemma 1 which provides two sufficient sub-conditions. Condition (a) of Lemma 1 can be checked manually; $UKano$ leaves it to the user. Condition (b) may in general be very difficult to verify. While it is surely possible to reduce the verification of this sub-condition to classical reachability properties verifiable in $ProVerif$ , we prefer to give a more direct verification technique.

Indeed, once frame opacity is known to hold, condition (b) actually follows immediately from simple properties of the idealisation function, since checking that honest outputs cannot be confused in executions of $M_{Π, \overline{id}}$ is equivalent to checking that they cannot be confused in idealised executions. Often, the idealisation function uses only function symbols that do not occur in $E$ and such that at least one session variable $x^{n} \in X^{n}$ occurs in $ideal (ℓ)$ for each honest output label ℓ. Checking that the idealisation function enjoys these properties is straightforward. Let us now show that it implies condition (b) of Lemma 1.

Proposition 3.
Let $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ be a protocol such that $fn (I) \cap fn (R) \neq \emptyset$ (shared case). Consider an idealisation operator $ideal (\cdot)$ such that, for any label $ℓ \in L$ occurring in the honest execution of Π, some name variable $x \in X^{n}$ appears in $ideal (ℓ)$ in a position only under symbols $f \in Σ_{c}$ that do not occur in equations of $E$ . If Π satisfies frame opacity for the idealised operator $ideal (\cdot)$ then condition (b) of Lemma 1 holds.
Proof.
Consider an execution $ta$ of $M_{Π, \overline{id}}$ where agent $a_{1}$ performs an output with label ℓ and handle $w_{1}$ , and agent $a_{2} \neq a_{1}$ performs another output with label ℓ and handle $w_{2}$ . We assume that ℓ occurs in the honest execution of Π and we note ϕ the resulting frame from the above execution. Assume, for the sake of contradiction, that $ϕ (w_{1}) =_{E} ϕ (w_{2})$ . Since the protocol ensures frame opacity for the idealised operator $ideal (\cdot)$ , we deduce that $Φ_{ideal}^{fr} (ta) (w_{1}) =_{E} Φ_{ideal}^{fr} (ta) (w_{2})$ . By hypothesis, some name variable $x_{1} \in X^{n}$ occurs in $ideal (ℓ)$ in a position which (even after a substitution) cannot be erased by the equational theory nor the computation relation. In other words we have that $fr (a_{1}, x^{n})$ occurs in $Φ_{ideal}^{fr} (ta) (w_{1})$ , and similarly $fr (a_{2}, x^{n})$ occurs in $Φ_{ideal}^{fr} (ta) (w_{2})$ , at the same position under non-malleable constructor symbols only. Since we have assumed (in Section 2.1) that our equational theory is non-degenerate, this implies that $fr (a_{1}, x^{n}) =_{E} fr (a_{2}, x^{n})$ and contradicts the injectivity of $fr$ . □

5.3. The tool $UKano$

As mentioned earlier, the tool $UKano$ [51] automatises the encodings described in this section. It takes as input a $ProVerif$ model specifying the protocol to be verified (and the identity names $\overline{id}$ ) and returns:

whether frame opacity could be established or not: in particular, it infers an idealisation operator that, when in the shared case, satisfies the assumptions of Proposition 3;

and the list of conditionals for which condition (i) of well-authentication holds.

If frame opacity holds and condition (i) of well-authentication holds for all conditionals – possibly with some exceptions for conditionals the user can identify as safe– then the tool concludes that the protocol given as input ensures unlinkability and anonymity w.r.t.

\overline{id}

. Note that the tool detects whether

fn (I) \cap fn (R) = \emptyset

or not and adapts the queries for verifying item (i) of well-authentication accordingly. Our tool uses heuristics to build idealised operators that always satisfy the assumptions of Proposition 3. Actually, three different heuristics have been implemented.

Syntaxic heuristic.

The syntaxic heuristic fully adopts the canonical syntactical construction from Section 4.2 (and displays a warning message when in the shared case, since all requirements are not met in this case). It can be enabled using the option –ideal-syntaxic.

Semantic heuristic.

The semantic heuristic (enabled with the option –ideal-semantic) follows the semantical construction from Section 4.2 with only tuples identified as transparent. Roughly, idealisation of a tuple is a tuple of idealisations of the corresponding sub-terms and idealisation of any other term is a fresh session variable in $X^{n}$ . Such an idealised operator is much less precise (i.e. may lead to more false negatives) but since idealised messages are much simpler, it allows better performance when it works.

Quasi-syntaxic heuristic.

This heuristic follows the canonical syntactical construction described in Section 4.2 except that sub-terms having a function symbol at top-level that is involved in the equational theory will be replaced by a fresh session name in order to comply with hypothesis of Proposition 3. This is the default heuristic in UKano.

Finally, the user can also define its own idealisations and the tool $UKano$ will check that assumptions of Proposition 3 are satisfied when in the shared case.

At a technical level, we built $UKano$ on top of $ProVerif$ . We only re-used the lexer, parser and AST of $ProVerif$ and build upon those a generator and translator of $ProVerif$ models implementing our sufficient conditions via the above encodings. This effort represents about 2k OCaml LoC. The official page of the tool $UKano$ with distributed releases of the tool can be found at http://projects.lsv.ens-cachan.fr/ukano/. We also distribute $ProVerif$ v1.97 modified for handling extended diff-equivalence (see Section 5.1). The difference between our modified version of $ProVerif$ v1.97 and the original one is about 60 lines of code.

6. Case studies

In this section we apply our verification method to several case studies. We rely on our tool $UKano$ to check whether the protocol under study satisfies frame opacity and well-authentication as defined in Section 4. We also discuss some variations of the protocols to examine how privacy is affected. Remind that if privacy can be established for concurrent sessions (i.e. $†_{I} = †_{R} =!$ ) then it implies privacy for all other scenarios as well, i.e. when $†_{I}, †_{R} \in {!,!}$ . We thus model protocols with concurrent sessions and discuss alternative scenarios only when attacks are found. The source code of our tool and material to reproduce results can be found at http://projects.lsv.ens-cachan.fr/ukano/.

All case studies discussed in this section except two (i.e. DAA in Section 6.4 and ABCDH in Section 6.5) have been automatically verified using our tool $UKano$ without any manual effort. We discuss little manual efforts needed to conclude for DAA and ABCDH in the dedicated sections. We used UKano v0.5 based on ProVerif v1.97 on a computer with following specifications:

OS: Linux 3.10-2-amd64 #1 SMP Debian 3.10.5-1x86_64 GNU/Linux

CPU / RAM: Intel(R) Xeon(R) CPU X5650 @ 2.67 GHz / 47GO

6.1. Hash–Lock protocol

We consider the Hash-Lock protocol as described in [42]. This is an RFID protocol that has been designed to achieve privacy even if no formal proof is given. We suppose that, initially, each tag has his own key k and the reader maintains a database containing those keys. The protocol relies on a hash function, denoted $h$ , and can be informally described as follows. $\begin{array}{l} Reader \to Tag : n_{R} \\ Tag \to Reader : n_{T}, h (n_{R}, n_{T}, k) \end{array}$

This protocol falls into our generic class of 2-party protocols in the shared case, and frame opacity and well-authentication can be automatically established in less than 0.01 second. We can therefore conclude that the protocol preserves unlinkability (note that anonymity does not make sense here). Actually, all implemented heuristics were able to successfully establish frame opacity automatically.

6.2. LAK protocol

We present an RFID protocol first introduced in [43], and we refer to the description given in [52]. To avoid traceability attacks, the main idea is to ask the tag to generate a nonce and to use it to send a different message at each session. We suppose that initially, each tag has his own key k and the reader maintains a database containing those keys. The protocol is informally described below ( $h$ models a hash function). In the original version (see e.g. [52]), in case of a successful execution, both parties update the key k with $h (k)$ (they always store the last two keys). Our framework does not allow one to model protocols that rely on a mutable state. Therefore, we consider here a version where the key is not updated at the end of a successful execution allowing the key k to be reused from one session to another. This protocol lies in the shared case since the identity name k is used by the reader and the tag. $\begin{array}{l} Reader \to Tag : r_{1} \\ Tag \to Reader : r_{2}, h (r_{1} \oplus r_{2} \oplus k) \\ Reader \to Tag : h (h (r_{1} \oplus r_{2} \oplus k) \oplus k \oplus r_{1}) \end{array}$

Actually, this protocol suffers from an authentication attack. The protocol does not allow the reader to authenticate the tag. This attack can be informally described as follows (and already exists on the original version of this protocol). By using algebraic properties of ⊕, an attacker can impersonate a tag by injecting previously eavesdropped messages. Below, $I (A)$ means that the attacker plays the role $A$ . $\begin{array}{l} I (Reader) \to Tag : r_{1} \\ Tag \to Reader : r_{2}, h (r_{1} \oplus r_{2} \oplus k) \\ Reader \to Tag : r_{1}^{'} \\ I (Tag) \to Reader : r_{2}^{I}, h (r_{1} \oplus r_{2} \oplus k) \\ Reader \to Tag : h (h (r_{1} \oplus r_{2} \oplus k) \oplus k \oplus r_{1}^{'}) \end{array}$ where $r_{2}^{I} = r_{1}^{'} \oplus r_{1} \oplus r_{2}$ , thus $h (r_{1} \oplus r_{2} \oplus k) =_{E} h (r_{1}^{'} \oplus r_{2}^{I} \oplus k)$ .

Due to this, the protocol does not satisfy our well-authentication requirement even with sessions in sequence for $Tag$ and $Reader$ . Indeed, the reader can end a session with a tag whereas the tag has not really participated to this session. In other words, the reader passes a test (which does not correspond to a safe conditional) with success, and therefore performs a $τ_{then}$ action whereas it has not interacted honestly with a tag. Actually, this trace can be turned into an attack against the unlinkability property (for any combination of $†_{I}, †_{R} \in {!,!}$ ). Indeed, by continuing the previous trace, the reader can send a new request to the tag generating a fresh nonce $r_{1}^{″}$ . The attacker $I (Tag)$ can again answer to this new request choosing his nonce $r_{2}^{″}$ accordingly, i.e. $r_{2}^{″} = r_{1}^{″} \oplus r_{1} \oplus r_{2}$ . This execution, involving two sessions of the reader talking to the same tag, cannot be mimicked in the single session scenario, and corresponds to an attack trace.

More importantly, this scenario can be seen as a traceability attack on the stateful version of the protocol leading to a practical attack. The attacker will first start a session with the targeted tag by sending it a nonce $r_{1}$ and storing its answer. Then, later on, he will interact with the reader as described in the second part of the attack scenario. Two situations may occur: either the interaction is successful meaning that the targeted tag has not been used since its last interaction with the attacker; or the interaction fails meaning that the key has been updated on the reader’s side, and thus the targeted tag has performed a session with the reader since its last interaction with the attacker. This attack shows that the reader may be the source of leaks exploited by the attacker to trace a tag. This is why we advocate for the strong notion of unlinkability we used, taking into account the reader and considering it as important as the tag.

We may note that the same protocol was declared untraceable in [52] due to the fact that they have in mind a weaker notion of unlinkability. Actually, their notion captures the intuitive notion that a tag is untraceable if for any execution in which two actions are performed by the same tag, there is another execution indistinguishable from the original one in which the actions have been performed by two different tags. We may note that in the attack scenario described above, the tag in itself does not leak anything but the reader does, explaining why this weak notion of untraceability missed this attack.

Now, to avoid the algebraic attack due to the properties of the xor operator, we may replace it by the pairing operator. The resulting protocol is a 2-party protocol that falls into our class, and for which frame opacity and well-authentication can be established (with concurrent sessions) using $UKano$ (any heuristic is suitable for that). Therefore, Theorem 1 allows us to conclude that it preserves unlinkability.

6.3. BAC protocol and some others

An e-passport is a paper passport with an RFID chip that stores the critical information printed on the passport. The International Civil Aviation Organization (ICAO) standard [48] specifies several protocols through which this information can be accessed. Before executing the Basic Access Control (BAC) protocol, the reader optically scans a weak secret from which it derives two keys $k_{E}$ and $k_{M}$ that are then shared between the passport and the reader. Then, the BAC protocol establishes a key seed from which two sessions keys are derived. The session keys are then used to prevent skimming and eavesdropping on subsequent communications.

In [5], two variants of the BAC protocol are described and analysed. We refer below to these two variants as the French version and the United Kingdom (U.K.) version. The U.K. version is claimed unlinkable (with no formal proof) whereas an attack is reported on the French version. We first give an informal description of the BAC protocol using Alice & Bob notation: $\begin{array}{l} Tag \to Reader : n_{T} \\ Reader \to Tag : {n_{R}, n_{T}, k_{R}}_{k_{E}}, mac ({n_{R}, n_{T}, k_{R}}_{k_{E}}, k_{M}) \\ Tag \to Reader : {n_{T}, n_{R}, k_{T}}_{k_{E}}, mac ({n_{T}, n_{R}, k_{T}}_{k_{E}}, k_{M}) \end{array}$

Then, to explain the difference between the two versions, we give a description of the passport’s role in Fig. 8.

Fig. 8.

Description of the passport’s role.

We do not model the $getChallenge$ constant message that is used to initiate the protocol but it is clear this message does not play any role regarding the security of the protocol. We consider the signature given in Example 1 augmented with a function symbol $mac$ of arity 2. This is a public constructor whose purpose is to model message authentication code, taking as arguments the message to authenticate and the mac key. There is no rewriting rule and no equation regarding this symbol. We also assume public constants to model error messages. The U.K. version of the protocol does not distinguish the two cases of failure, i.e. $erro r_{M a c}$ and $erro r_{N o n c e}$ are the same constant, whereas the French version does. The relevant point is the fact that, in case of failure, the French version sends a different error message indicating whether the failure occurs due to a problem when checking the mac, or when checking the nonce. This allows the attacker to exploit this conditional to learn if the mac key of a tag is the one used in a given message $⟨ m, mac (m, k) ⟩$ . Using this, he can very easily trace a tag T by first eavesdropping an honest interaction between the tag T and a reader.

The U.K. version of the BAC protocol is a 2-party protocol according to our definition. Note that since the two error messages are actually identical, we can merge the two $let$ instructions, and therefore satisfy our definition of being a responder role. Then, we automatically proved frame opacity and well-authentication using $UKano$ . It took less than 0.1 second independently of the chosen heuristic regarding frame opacity. Therefore, Theorem 1 allows us to conclude that unlinkability is indeed satisfied.

Regarding the French version of this protocol, it happens that the passport’s role is neither an initiator role, nor a responder role according to our formal definition. Indeed, our definition of a role, and therefore of a 2-party protocol does not allow to model two sequences of tests that will output different error messages in case of failure. As illustrated by the attack on the French version of the BAC protocol, imposing this syntactic condition is actually a good design principle w.r.t. unlinkability.

Once the BAC protocol has been successfully executed, the reader gains access to the information stored in the RFID tag through the Passive and Active Authentication protocols (PA and AA). They are respectively used to prove authenticity of the stored information and prevent cloning attacks, and may be executed in any order. A formal description of these protocols is available in [4]. These two protocols also fall into our class and our conditions can be checked automatically both for unlinkability and anonymity properties. We can also use our technique to analyse directly the three protocols together (i.e. the U.K. version of the BAC together with the PA and AA protocols in any order). We analysed both orders, i.e. BAC followed by PA, and then AA, as well as BAC following by AA, and then PA. We establish unlinkability and anonymity w.r.t. all private data stored in the RFID chip (name, picture, etc.). $UKano$ concludes within 1 second to establish both well-authentication and frame opacity (independently of the selected heuristic).

6.4. PACE protocol

The Password Authenticated Connection Establishment protocol (PACE) has been proposed by the German Federal Office for Information Security (BSI) to replace the BAC protocol. It has been studied in the literature [15,16,25] but to the best of our knowledge, no formal proofs about privacy have been given. Similarly to BAC, its purpose is to establish a secure channel based on an optically-scanned key k. This is done in four main steps (see Fig. 9):

The tag chooses a random number $s_{T}$ , encrypts it with the symmetric key k shared between the tag and the reader and sends the encrypted random number to the reader (message 1).

Both the tag and the reader perform a Diffie–Hellman exchange (messages 2 & 3), and derive G from $s_{T}$ and $g^{n_{R} n_{T}}$ .

The tag and the reader perform a Diffie–Hellman exchange based on the parameter G computed at the previous step (messages 5 & 6).

The tag and the reader derive a session key $k^{'}$ which is confirmed by exchanging and checking the authentication tokens (messages 8 & 9).

Moreover, at step 6, the reader is not supposed to accept as input a message which is equal to the previous message that it has just sent.

Fig. 9.

PACE in Alice & Bob notation.

To formalise such a protocol, we consider $Σ_{c} = {enc, dec, dh, mac, gen, g, ok}$ , and $Σ_{d} = {neq}$ .

Except $g$ and $ok$ which are public constants, all these function symbols are public constructor symbols of arity 2. The destructor $neq$ has already be defined in Example 4. The symbol $dh$ is used to model modular exponentiation whereas $mac$ will be used to model message authentication code. We consider the equational theory $E$ defined by the following equations: $\begin{matrix} dec (enc (x, y), y) = x dh (dh (x, y), z) = dh (dh (x, z), y) \end{matrix}$

Fig. 10.

Process $R_{PACE}$ .

We consider the process $R_{PACE}$ as described in Fig. 10. We do not detail the continuation $R^{'}$ and we omit trivial conditionals. The process modelling the role $I_{PACE}$ can be obtained in a similar way. Then, we consider $Π_{PACE} = (k, (s_{T}, n_{T}, n_{T}^{'}), (n_{R}, n_{R}^{'}),!,!, I_{PACE}, R_{PACE})$ which falls into our generic class of 2-party protocols. Unfortunately, $ProVerif$ cannot handle the equation above on the $dh$ operator (due to some termination issues). Instead of that single equation, we consider the following equational theory that is more suitable for $ProVerif$ : $\begin{matrix} dh (dh (g, y), z) = dh (dh (g, z), y) dh (dh (gen (x_{1}, x_{2}), y), z) = dh (dh (gen (x_{1}, x_{2}), z), y) \end{matrix}$

This is sufficient for the protocol to work properly but it obviously lacks equations that the attacker may exploit.

First, we would like to highlight an imprecision in the official specification that may lead to practical attacks on unlinkability. As the specification seems to not forbid it, we could have assumed that the decryption operation in $G = gen (dec (y_{1}, k), dh (y_{2}, n_{R}))$ is implemented in such a way that it may fail when the key k does not match with the key of the ciphertext $y_{1}$ . In that case, an attacker could eavesdrop a first message $c^{0} = enc (s_{T}^{0}, k^{0})$ of a certain tag $T^{0}$ and then, in a future session, it would let the reader optically scan a tag T but replace its challenge $enc (s_{T}, k)$ by $c^{0}$ and wait for an answer of the reader. If it answers, he learns that the decryption did not fail and thus $k = k^{0}$ : the tag T is actually $T^{0}$ . We discovered this attack using our method since, in our first attempt to model the protocol, we modelled $dec (\cdot, \cdot)$ as a destructor (that may fail) and the computation of G as an evaluation: $\begin{matrix} let G = gen (dec (y_{1}, k), dh (y_{2}, n_{R})) in [...] \end{matrix}$ In order to declare the protocol well-authenticating, this conditional computing G which is not safe has to satisfy our requirement (see Definition 19). However, as witnessed by the attack scenario described above (the reflection attack), the condition actually fails to hold. Incidentally, the same attack scenario shows that the protocol does not ensure unlinkability (this scenario cannot be observed when interacting with $S_{Π}$ ). Similarly to the attack on LAK, we highlight here the importance to take the reader into account and give it as much importance as the tag in the definition of unlinkability. Indeed, it is actually a leakage from the reader that allows an attacker to trace a specific tag.

Second, we now consider that decryption is a constructor, and thus cannot fail, an we report on an attack that we discovered using our method on some models of PACE found in the literature [15,16,25]. Indeed, in all those papers, the first conditional of the reader $\begin{matrix} let y_{test} = eq (yes, neq (y_{3}, dh (G, n_{R}^{'}))) in \end{matrix}$ is omitted. Then the resulting protocol is not well-authenticating. To see this, we simply have to consider a scenario where the attacker will send to the reader the message it has outputted at the previous step. Such an execution will allow the reader to execute its role until the end, and therefore execute $τ_{then}$ , but the resulting trace is not an honest one. Again, this scenario can be turned into an attack against unlinkability as explained next. As before, an attacker could eavesdrop a first message $c^{0} = enc (s_{T}^{0}, k^{0})$ of a certain tag $T^{0}$ . Then, in a future session, it would let the reader optically scan a tag T but replace its challenge $enc (s_{T}, k)$ by $c^{0}$ . Independently of whether k is equal to $k^{0}$ or not, the reader answers $g^{n_{R}}$ . The attacker then plays the two rounds of Diffie–Hellman by reusing messages from the reader (he actually performs a reflection attack). More precisely, he replies with $g^{n_{T}} = g^{n_{R}}$ , $G^{n_{T}^{'}} = G^{n_{R}^{'}}$ and $mac (G^{n_{R}^{'}}, k^{'}) = mac (G^{n_{T}^{'}}, k^{'})$ . The crucial point is that the attacker did not prove he knows k (whereas he is supposed to do so to generate G at step 4) thanks to the reflection attack that is not detected. Now, the attacker waits for the reader’s answer. If it is positive (the process $R^{'}$ is executed), he learns that $k = k^{0}$ : the tag T is actually the same as $T^{0}$ .

Third, we turn to PACE as properly understood from the official specification: when the latter test is present and the decryption may not fail. In that case, we report on a new attack. $UKano$ found that the last test of the reader violates well-authentication. This is the case for the following scenario: the message $enc (s_{T}, k)$ sent by a tag $T (k, n_{T})$ is fed to two readers $R (k, n_{R}^{1}), R (k, n_{R}^{2})$ of same identity name. Then, the attacker just forwards messages from one reader to the other. They can thus complete the two rounds of Diffie–Hellman (note that the test avoiding reflection attacks holds). More importantly, the mac-key verification phase (messages 8 and 9 from Fig. 9) goes well and the attacker observes that the last conditional of the two readers holds. This violates well-authentication but also unlinkability because the latter scenario cannot be observed at all in $S_{Π}$ : if the attacker makes two readers talk to each other in $S_{Π}$ they cannot complete a session because they must have different identity names. In practice, this flaw seems hard to exploit but it could be a real privacy concern: if a tag initiates multiple readers, an attacker may learn which ones it had initiated by forwarding messages from one to another. It does not seem to be realistic in the e-passport scenario, but could be harmful in other contexts. It seems that, in the e-passport context, a modelling with sequential sessions would be more realistic. We come back to such a modelling at the end of this section.

Further, we propose a simple fix to the above attack by adding tags avoiding confusions between reader’s messages and tag’s messages. It suffices to replace messages 8 and 9 from Fig. 9 by respectively $mac (⟨ c_{r}, G^{n_{T}^{'}} ⟩, k^{'})$ and $mac (⟨ c_{t}, G^{n_{R}^{'}} ⟩, k^{'})$ where $c_{r}, c_{t}$ are public constants, and adding the corresponding checks. Well-authentication can be automatically established using $UKano$ in around 1 minute. Frame opacity can be automatically established using any heuristic described in Section 5.3. Heuristics producing more complex idealisations (i.e. the syntaxic one) are less efficient. Nevertheless, the tool concludes in at most 16 seconds. We thus conclude that PACE with tags preserves unlinkability in the model considered here.

6.5. Attributed-based authentication scenario using ABCDH protocol

Most authentication protocols are identity-based: the user needs to provide his identity and prove to the service provider he is not trying to impersonate somebody else. However, in many contexts, the service provider just needs to know that the user has some non-identifying attributes (e.g. age, gender, country, membership). For instance, a liquor shop just needs to have the proof that the user has the right to buy liquors (i.e. that he is old enough) and does not need to know the full identity of the user (e.g. as it is currently done when showing ID cards). Attribute-based authentication protocols solve this problem and allow a user to prove to another user, within a secure channel, that he has some attributes without disclosing its identity.

We used our method to automatically establish unlinkability of a typical use case of such a protocol taking part to the IRMA project.6

⁶
For more information about IRMA (“I Reveal My Attributes”), see https://www.irmacard.org.

We analysed a use case of the protocol ABCDH as defined in [3]. This protocol allows a smartcard C to prove to some Verifier V that he has the required attributes. The protocol aims at fulfilling this goal without revealing the identity of C to V or to anyone else. One of its goal is also to avoid that any other smartcard

C^{'}

replays those attributes later on. The protocol should also ensure unlinkability of C. To the best of our knowledge, there was no prior formal analysis of that security property for this protocol.

The key ingredient of this protocol is attribute-based credential (ABC). It is a cryptographic container for attributes. In ABC, attributes are signed by some issuers and allow for selective disclosure (SD): it is possible to produce a zero-knowledge (ZK) proof revealing a subset of attributes signed by the issuer along with a proof that the selected disclosed attributes are actually in the credential. This non-interactive proof protocol can be bound to some fresh data to avoid replay attacks. We shall use the notation $SD (\overline{a_{i}}; n)$ to denote the selective disclosure of attributes $\overline{a_{i}}$ bound to n. Note that $SD (\emptyset; n)$ (no attribute is disclosed) still proves the existence of a credential. There are two majors ABC schemes: Microsoft U-Prove [46] and IBM’s Idemix [23]. We decided to model IBM’s scheme (since it is the one that is used in IRMA) following the formal model given in [24]. We may note that we consider here some privacy issues whereas the security analysis presented in [24] is dedicated to the analysis of some reachability properties. It involves complex cryptographic primitives (e.g. commitments, blind signature, ZK proofs) but $ProVerif$ can deal with them all. In this scheme, each user has a master secret never revealed to other parties. Issuers issue credentials bound to the master secret of users (note that users are known to issuers under pseudonyms). A SD consists in a ZK proof bound to n proving some knowledge: knowledge of the master secret, knowledge of a credential bound to the master secret, knowledge that the credential has been signed by the given organisation, knowledge that the credential contains some given attributes.

We analyse the ABCDH [3] using the model of SD from [24] used in the following scenario:

an organisation $O_{age}$ issues credentials about the age of majority;

an organisation $O_{check}$ issues credentials giving the right to check the age of majority;

a user C wants to watch a movie rated adult-only due to its violent contents; his has a credential from $O_{age}$ with the attribute adult;

a movie theatre V wants to verify whether the user has the right to watch this movie; it has a credential from $O_{check}$ with the attribute canCheckAdult.

The scheme is informally given in Fig. 11.

$n_{V}, n_{C}$ and n are fresh nonces. Functions $f_{1} / 1$ , $f_{2} / 1$ and $f_{3} / 2$ are independent hash functions; we thus model them as free constructor symbols. The construction $SD (\cdot; \cdot)$ is not modelled atomically and follows [24] but we do not describe here its details. We note however that when V (respectively C) sends a $SD (\cdot; \cdot)$ , the corresponding message we do not detail here contains an identity-parameter ${user}_{V}$ (respectively ${user}_{C}$ ).

Fig. 11.

ABCDH (where $s e e d = dh (dh (g, n_{C}), n_{V})$ and $k = f_{2} (s e e d)$ ).

This is a 2-party protocol that falls into our class. Actually, we have that ${user}_{V} \in fn (I) \cap \overline{k} \neq \emptyset$ and ${user}_{C} \in fn (R) \cap \overline{k} \neq \emptyset$ , but $fn (I) \cap fn (R) = \emptyset$ (non-shared case). The complete model of this protocol is quite complex and can be found in [51]. Frame Opacity can be automatically established using the syntaxic heuristic (see Section 5.3) in less than 40 seconds. The other heuristics were not enough precise to conclude (yielding negative results) showing the importance of having the choice between heuristics that are precise but less efficient and ones that are more efficient but less precise. Regarding well-authentication, due to the length of the protocol, the queries are also quite long. Because of the latter and the high complexity of the underlying term algebra, it required too much time for $ProVerif$ to terminate. We addressed this performance issue by soundly splitting up big queries into smaller ones. This way, we successfully established well-authentitcation for this protocol within 3 hours.

6.6. DAA join & DAA sign

A Trusted Platform Module (TPM) is a hardware device aiming at protecting cryptographic keys and at performing some cryptographic operations. Typically, a user may authenticate himself to a service provider relying on such a TPM. The main advantage is to physically separate the very sensitive data from the rest of the system. On the downside however, such devices may be used by malicious agents to breach users’ privacy by exploiting their TPMs. Direct Anonymous Attestation (DAA) protocols have been designed to let TPMs authenticate themselves whilst providing accountability and privacy.

In a nutshell, some issuers issue credentials representing membership to a group to the TPM using group signatures via the DAA join protocol. Those credentials are bound to the internal secret of the TPM that must remain unknown to the service provider. Then, when a TPM is willing to prove to a verifier its membership to a group, it uses the DAA sign protocol. We analysed the RSA-based DAA join and sign protocols as described in [50]. Both protocols rely on complex cryptographic primitives (e.g. blind signatures, commitments, and Zero Knowledge proofs) but $ProVerif$ can deal with them all. Note that the authors of [50] have automatically established a game-based version of unlinkability of the combination of DAA Join and DAA Sign using $ProVerif$ . We only provide an analysis of each protocol in isolation since the combination of the two protocols is a 3-party protocol.

6.6.1. DAA join

In the RSA-based DAA join protocol, the TPM starts by sending a credential request in the form of a commitment containing its internal secret, some session nonce and the public key of the issuer. The issuer then challenges the TPM with some fresh nonces encrypted asymmetrically with the public key of the TPM. After having received the expected TPM’s answer, the issuer sends a new nonce as second challenge. To this second challenge, the TPM needs to provide a ZK proof bound to this challenge proving that he knows the internal secret on which the previous commitment was bound. Finally, after verifying this proof, the issuer blindly signs the commitment allowing the TPM to extract the required credential.

Fig. 12.

DAA join.

We give in Fig. 12 an Alice & Bob description of the protocol between the TPM and the issuer. The message $z e t a_{I} = h ((0, b s n I))$ relies on $b s n I$ : using a fresh $b s n I$ allows to ensure that the session of DAA Join will be unlinkable from previous ones. The message $t s k = h ((h ((DAAseed, h (K I))), c n t, 0))$ combines the internal secret of the $TPM$ (i.e. $DAAseed$ ) with the public long-term key of the issuer (i.e. $K I$ ). The commit message $N_{I} = commit (z e t a_{I}, t s k)$ binds $z e t a_{I}$ with the internal secret while the commit message $U = clcommit (pk (s k_{I}), n_{v}, t s k)$ expresses a credential request for a signature key $s k_{I}$ . The goal of the $TPM$ will be to get the message U signed by the issuer. More precisely, the issuer will blindly sign the message U with the signature key $s k_{I}$ after making sure that the $TPM$ can decrypt challenges encrypted with its public key (step 2.) and that he can provide a fresh ZK proof showing he knows its internal secret binds in U and $N_{I}$ (step 5.). Finally, if all checks are successful, the issuer will blindly sign the credential request U (step 6.). We note $clsign ((U, r), s k_{I})$ the blind signature of a commitment U with signature key $s k_{I}$ and some random r. The function $penc$ denotes a randomized asymmetric encryption scheme. Note that $ZK (\cdot, \cdot)$ has two arguments: the first one should contain private data and the second one should contain public data. One can always extract public data from ZK proofs and one can check if both public and private data match as expected.

This protocol falls in our class and lies in the shared case7

⁷

Both roles share the identity name $s k_{TPM}$ (but note that the Issuer only uses $pk (s k_{TPM})$ ). Indeed, before executing the join protocol, the TPM and the issuer should establish a one-way authenticated channel that is not specified by the DAA scheme. Therefore, an Issuer session is associated to a single TPM’s identity it is expected to communicate with.

(i.e.

fn (I) \cap fn (R) = {s k_{TPM}}

UKano

automatically established frame opacity in less than 30 seconds using the syntaxic idealisation, and in less that 3 seconds when using the quasi-syntaxic heuristic. Note that the semantic one is not precise enough to allow one to conclude. Regarding well-authentication, we had to leverage the same splitting technique explained in Section 6.5 so that

UKano

could conclude in a reasonable amount of time (around 30 seconds).

6.6.2. DAA sign

Once a TPM has obtained such a credential, it may prove its membership using the DAA sign protocol. This protocol is played by a TPM and a verifier: the verifier starts by challenging the TPM with a fresh nonce (step 1.), the latter then sends a complex ZK proof bound to this nonce (step 2.). The latter ZK proof also proves that the TPM knows a credential from the expected issuer bound to a secret he knows (essentially a message $clsign ((U, r), s k_{I})$ received in a previous session of DAA join). The verifier accepts only if the ZK proof can be successfully checked (step 3.).

We give in Fig. 13 an Alice & Bob description of the protocol between a verifier and the TPM willing to sign a message m using its credential $c r e d = clsign ((U, r), s k_{I})$ he received from a past DAA join session. From its credential $c r e d$ , the TPM will compute a new credential dedicated to the current sign session: $c r e d^{'} = clcommit ((pk (s k_{I}), c r e d), n_{c})$ . Indeed, if the TPM had directly used $c r e d$ then two sessions of DAA sign would have been trivially linkable. The TPM also computes a commit of $t s k$ that was used to obtain the credential: $N_{V} = commit (t s k, z e t a_{V})$ where $z e t a_{V}$ is a fresh nonce.8

⁸
The protocol also specifies a mode that makes different signatures linkable by construction using $z e t a_{V} = h ((0, b s n V))$ . We focus on the other mode for which unlinkability is expected to hold.

Fig. 13.

DAA sign.

Similarly to Examples 10, 11, we distinguish two cases whether $s k_{I}$ is considered as a private constant or as an identity parameter. We recall that this choice critically impacts the privacy property that is modeled. Indeed, the privacy set [47] is considered to be (a) the set of users who obtained a credential from a given issuer in the former case, or, (b) the set of all users in the latter case.

(a) $s k_{I}$ as a private constant. This 2-party protocol falls in our class and lies in the non-shared case. Indeed, we model infinitely many different TPMs that may take part to the DAA sign protocol with any verifier whose role is always the same (he has no proper identity). We automatically analysed this protocol with $UKano$ and established both frame opacity and well-authentication in less than 4 seconds. Frame opacity has been established using a well-chosen idealisation adapted from the syntaxic heuristic.

(b) $s k_{I}$ as an identity parameter. This 2-party protocol falls in our class and lies in the shared case. Indeed, we model infinitely many different TPMs with credentials signed by pairwise different issuers that may take part to the DAA sign protocol with a verifier who is checking credential from the corresponding issuer.9

⁹

We discuss a more precise modelling and why it cannot be analyzed in our framework in 7.1.2.

We automatically analysed this protocol with

UKano

and we found that frame opacity is violated for any of

UKano

heuristic (note that the idealisation for the case (a) is not conform for (b)). By inspecting the attack trace returned by

UKano

, one can quickly rebuild an attack against unlinkability and anonymity. Indeed, the attack on frame opacity shows that an attacker can exploit the fact that the ZK proof contains in its public part the public key of the issuer (i.e.

pk (s k_{I}))

). A passive eavesdropper is thus able to learn the issuer that has signed the credential used in a ZK proof sent by a prover, hence breaking anonymity and unlinkability. This is not surprising as the privacy mechanism of DAA sign was intended to protect users’ privacy inside a certain group (associated with an issuer), which is a property we have checked, and which holds, with the variant (a).

6.6.3. Summary

We now summarise our results in Table 1. We only summarize results obtained regarding unlinkability and considering concurrent sessions. For each protocol, we mention the identity parameters of each role. Most of our case studies fall into the shared case with $fn (I) \cap fn (R) \neq \emptyset$ . We indicate the verification time in seconds to verify both conditions. When there is an attack, we give the time $ProVerif$ takes to show that one of the condition fails to hold. We note ✓ for a condition automatically checked using our tool $UKano$ and ✕ when the condition does not hold. Note that all positive results were established automatically using our tool $UKano$ (which is based on $ProVerif$ ) without any manual effort (except for the cases indicated by ✓^∗ for which little manual efforts were needed).

Table 1
Summary of our case studies regarding unlinkability with concurrent sessions

Protocol Identity parameters Frame opacity Well-auth. Unlink. Verification time

in role $I$ in role $R$

Hash-Lock k k ✓ ✓ safe <1s

Fixed LAK k k ✓ ✓ safe <1s

BAC $k_{E}, k_{M}$ $k_{E}, k_{M}$ ✓ ✓ safe <1s

BAC/PA/AA $k_{E}, k_{M}$ $k_{E}, k_{M}$ ✓ ✓ safe <1s

BAC/AA/PA $k_{E}, k_{M}$ $k_{E}, k_{M}$ ✓ ✓ safe <1s

PACE (faillible dec) k k − ✕ attack <30s

PACE (as in [16]) k k − ✕ attack <1m

PACE k k − ✕ attack <2m

PACE with tags k k ✓ ✓ safe <2m

ABCDH (irma) ${user}_{V}$ ${user}_{C}$ ✓ ✓^∗ safe <3h

DAA join $DAAseed, s k_{TPM}$ $s k_{TPM}$ ✓ ✓^∗ safe <5s

DAA sign (a) ∅ $DAAseed, c n t, r$ ✓^∗ ✓ safe <5s

DAA sign (b) $s k_{I}$ $s k_{I}, DAAseed, c n t, r$ ✕ ✓ attack <1s

Protocol	Identity parameters	Frame opacity	Well-auth.	Unlink.	Verification time
Hash-Lock	k	k	✓	✓	safe	<1s
Fixed LAK	k	k	✓	✓	safe	<1s
BAC	$k_{E}, k_{M}$	$k_{E}, k_{M}$	✓	✓	safe	<1s
BAC/PA/AA	$k_{E}, k_{M}$	$k_{E}, k_{M}$	✓	✓	safe	<1s
BAC/AA/PA	$k_{E}, k_{M}$	$k_{E}, k_{M}$	✓	✓	safe	<1s
PACE (faillible dec)	k	k	−	✕	attack	<30s
PACE (as in [16])	k	k	−	✕	attack	<1m
PACE	k	k	−	✕	attack	<2m
PACE with tags	k	k	✓	✓	safe	<2m
ABCDH (irma)	${user}_{V}$	${user}_{C}$	✓	✓^∗	safe	<3h
DAA join	$DAAseed, s k_{TPM}$	$s k_{TPM}$	✓	✓^∗	safe	<5s
DAA sign (a)	∅	$DAAseed, c n t, r$	✓^∗	✓	safe	<5s
DAA sign (b)	$s k_{I}$	$s k_{I}, DAAseed, c n t, r$	✕	✓	attack	<1s

7. Limitations of our approach

In this section, we would like to discuss some further limitations of our approach. We first explain some limitations that come from the approach itself in Section 7.1. In Section 7.2, we then discuss some limitations of our tool $UKano$ which inherits some of the limitations of the $ProVerif$ tool on which it is based.

7.1. Limitations of our Theorem 1

Our approach consists of providing two sufficient conditions under which anonymity (see Definition 12) and unlinkability (see Definition 10) are satisfied. These condtions, even if they are satisfied by many concrete examples, may not be fullfilled by some protocols that are nevertheless anonymous and unlinkable (see examples described in Section 7.1.1). We then discuss in Section 7.1.2 some limitations that come from the class of protocols we consider.

7.1.1. Tightness of our conditions

As illustrated by the toy protocols given in Examples 30 and 31, our conditions are sufficient but not necessary to ensure unlinkability or anonymity.

Example 30.
We suppose that, initially, each tag has its own key k and the reader maintains a database containing those keys. The protocol relies on symmetric encryption, and can be informally described as follows. $\begin{array}{l} Tag \to Reader : {id}_{k} \end{array}$

Once the reader receives the encryption, it opens it and checks the identity of the tag before accepting (or not) to grant access to the tag. This protocol falls into our generic class of 2-party protocols (shared case). Anonymity w.r.t. $id$ is satisfied but unlinkability is not: a given tag always sends the same message.

Regarding our conditions, frame opacity does not hold. Consider $\begin{matrix} ϕ = {w_{1} \mapsto {i d_{1}}_{k_{1}}, w_{2} \mapsto {i d_{1}}_{k_{1}}, w_{3} \mapsto {i d_{2}}_{k_{2}}} . \end{matrix}$ Such a frame can be obtained when executing the $M_{Π}$ process. The syntactical idealisation will rename both occurrences of $i d_{1}$ (resp. $k_{1}$ ) using different names whereas the semantical idealisation will idealise each output using a fresh names. In both cases, the resulting idealised frame is not statically equivalent to ϕ. Thus, frame opacity cannot be established using these idealisations. Actually, no idealisation will be able to idealise the two first outputs in the same way and the two last outputs in different way at the same time. This illustrates that frame opacity is a too strong condition when considering anonymity.

Regarding well-authentication, we can establish that such a condition does not hold as well. Still considering the execution leading to the frame ϕ above, we can then consider a reader that starts two sessions accepting twice $w_{1}$ as an input. It will then continue by executing its conditionals positively. The annotations of these two conditionals will be respectively $R ({k_{1}, {id}_{1}}, sid)$ and $R ({k_{1}, {id}_{1}}, {sid}^{'})$ . Therefore, condition (ii) of Definition 19 is not satisfied. These two conditionals are not safe and they are both associated to the same annotation (the one carried out by the output $w_{1}$ ). This does not break anonymity but simply shows that replaying messages is a scenario that allows an attacker to fool one party (here the reader) up to some point (here until the end).
Example 31.
In order to ensure unlinkability, we now suppose that the tag sends its identity accompanied with a freshly generated random number r. Therefore, we have that: $\begin{array}{l} Tag \to Reader : {⟨ r, id ⟩}_{k} . \end{array}$

This protocol falls into our generic class of 2-party protocols (shared case). The identity parameters of both roles are $id$ and k whereas r is the session parameter of role $I$ . As in the previous example, anonymity w.r.t. $id$ holds. Unlinkability should hold, assuming that the reader does not output any message indicating whether the test has been passed with success or not.

Actually, frame opacity can be established relying on either the syntaxical idealisation or the semantical one. The fresh random number inside each encryption allows one to ensure that all the ciphertexts are different. However, for the same reason as the one explained in the previous example, well-authentication does not hold: condition (ii) is not satisfied.

We recall that this can be considered as a false attack only if the protocol and the use case both enforce that the continuation of the protocol in case the test passes is always indistinguishable from the continuation in the other case; this is a strong assumption.

7.1.2. Class of protocols

Among the limitations coming from our definition of protocols, we first reconsider the DAA sign and PACE protocols to highlight some limitations of our approach.

Two parties only. Our notion of protocols only covers 2-party protocols. This obviously excludes important protocols with more than 2 parties such as secure group communication protocols [44], e-voting protocols [35], make mobile communication protocols [12], the combination of DAA join and DAA sign [35] that features 3 parties, etc.This also excludes scenarios where privacy is considered between group of entities. For instance for DAA sign (see Example 10 or Section 6.6.2), verifiers and clients may be associated to different issuers. Using our framework, one can analyze privacy between users in a single group (as in Example 10), or between groups but where each goup has only one user (as in Example 11). In the latter case, one would rather want to model privacy between groups where each group contains an unbounded number of users, but this is out of the scope of our approach. This is not surprinsing since such a scenario actually features three parties: clients, verifiers, issuers (forming groups); all with unbounded number of entities.

Honest trace. Now, we want to report on a potential limitation we discovered when analysing the PACE protocol using $Tamarin$ . Our initial aim was to investigate the scenario where sessions can be executed only sequentially. We have turned to $Tamarin$ since $ProVerif$ is not able to faithfully model such scenarios. We wrote a $Tamarin$ model encoding well-authentication and found surprisingly that this condition does not hold, even with the tagged version. This contrasts with the positive result obtained with $ProVerif$ . Actually, this comes from the fact that $Tamarin$ models Diffie–Hellman exponentiation in a more faithful way than $ProVerif$ . Some behaviours that were not possible in the $ProVerif$ model become possible, and it happens that well-authentication is not satisfied in such a model.

Indeed, the attacker can alter the Diffie–Hellman shares, as informally depicted in Fig. 14, without impacting the successive conditionals.

Fig. 14.

Example of successful but dishonest interaction (X can be any message).

This is problematic because successful tests will pass (independently of the message X) while such interactions are not honest according to our current definition of honest trace (see Definition 4). This problematic interaction is however not detected in $ProVerif$ , due to the lack of equations in the underlying equational theory: the final keys computed by both parties will be different, ${({(g^{n_{R}})}^{X})}^{n_{T}}$ for the tag and ${({(g^{n_{T}})}^{X})}^{n_{R}}$ for the reader. Therefore such an interaction cannot be completed sucessfully, and well-authentication will be established.

The failure of well-authentication described above does not yield a failure of unlinkability. It is thus a case where one might want to make well-authentication less restrictive. One direction for weakening it is to extend the notion of “honest trace associated to a protocol” (Definition 5): instead of a single honest trace we would associate to a protocol a set of symbolic traces that are, roughly, traces with (possibly) variables in recipes. For PACE, one may for instance use ${tr}_{h} = out (c_{I}, w_{1}) . in (c_{R}, dh (w_{1}, X)) . out (c_{R}, w_{2}) . in (c_{I}, dh (w_{2}, X)) . \dots$ in addition to the standard trace. However, in order to adapt our proof technique, we need to make sure that whatever the recipes chosen to fill in the variables (e.g. X in ${tr}_{h}$ ), the resulting concrete trace can be executed by the protocol and the produced frame always has the same idealisation. Remark that this is the case for ${tr}_{h}$ in the case of the PACE protocol.

In practice, this limitation on the well-authentication condition does not seem very important, as the issue is tied to the peculiar use of two Diffie–Hellman rounds in PACE and, expanding the discussion beyond privacy, the attack on well-authentication shows a potential weakness in that protocol. Indeed, Tag and Reader fail to establish an agreement on each other’s Diffie–Hellman shares from the first round (i.e. $g^{n_{R}}$ and $g^{n_{T}}$ ). Therefore, an attacker is able to manipulate those shares without being detected, which goes against best practices in protocol design. In contrast, the MAC messages 8 and 9 (see Fig. 9) allow the Tag and Reader to agree on each other’s Diffie–Hellman shares from the second round (i.e. $G^{n_{T}^{'}}$ and $G^{n_{R}^{'}}$ ) and on the shared key resulting from the first round (i.e. $g^{n_{R} n_{T}}$ in G). Adding $g^{n_{T}}$ (respectively $g^{n_{R}}$ ) to the first (respectively second) MAC message would fix this lack of agreement. We have formally verified with $Tamarin$ that PACE with this modification indeed satisfies well-authentication, thus providing an agreement on the full protocol transcript.

Stateless only. Our framework and our theorem only applies to stateless protocols (i.e. no mutable states persistent across sessions). This immediately excludes numerous real-world protocols such as secure messaging protocols [29], mobile communication protocols [12], etc.

7.2. Limitations of our tool

UKano

Our tool $UKano$ also suffers from some limitations. In particular, the heuristics we propose to build idealisation could be improved. For instance, in case of DAA sign, we were unable to establish frame opacity fully automatically: we had to propose a well-chosen idealisation adapted from the syntaxic heuristic. Note that, in general the syntaxic heuristic is a good choice but yields large messages that may cause some efficiency issues to $ProVerif$ . The semantical heuristic is less precise but much more efficient. In case of DAA sign, we make a trade-off betweeen these two choices to establish frame opacity. Regarding well-authentication, the resulting queries happen to be quite big and may also cause some troubles to $ProVerif$ . This can be adressed by soundly splitting the query (see Section 6.5) but this feature has not been implemented in $UKano$ .

Besides the limitations of our tool $UKano$ , we also inherit some of the limitations of the backend tool, i.e. $ProVerif$ . For instance, in terms of cryptographic primitives, we have seen that $ProVerif$ only consider a very abstract model for modular exponentiation, and does not allow one to model all the algebraic properties of the exclusive-or operator. We are also unable to faithfully model scenarios involving sequential compositions. This feature could be modeled in $ProVerif$ relying on private chanels but abstractions performed by $ProVerif$ when modeling private channels will not allow us to benefit from the extra information of that encoding. Of course, this limits the scope of our approach but progress made on existing verification tools will directly benefit to our approach as well. In particular, a natural extension for our tool $UKano$ would be to consider $Tamarin$ as a backend. This would bring precise support for sequential composition, a more faithful model for Diffie–Hellman exchange, and also the recent extension to deal with the exclusive-or operator [37].

8. Conclusion

We have identified two conditions, namely well-authentication and frame opacity, which imply anonymity and unlinkability for a wide class of protocols. Additionally, we have shown that these two conditions can be checked automatically using the tool $ProVerif$ , and we have mechanised their verification in our tool $UKano$ . This yields a new verification technique to check anonymity and unlinkability for an unbounded number of sessions. It has proved quite effective on various case studies. In particular, it has brought first-time unlinkability proofs for the BAC protocol (e-passport) and ABCDH protocol. Our case studies also illustrated that our methodology is useful to discover attacks against unlinkability and anonymity as illustrated by the new attacks we found on PACE and LAK.

In the future, we plan to improve the way our sufficient conditions are checked. For instance, we would like to let $UKano$ build idealisations in a cleverer way; notably in the choice of heuristics to adopt, and we are interested in other tools we may leverage as back-ends (e.g. $Tamarin$ ). We are also interested in simplifying further the verification of our conditions towards completely reducing the verification of equivalence-based properties to pure reachability verifications, which are known to be much simpler. Specifically, we believe that frame opacity could be verified via reachability and syntactical checks only. Obtaining such a result would certainly be useful, as it would allow us to use a richer toolset to verify case studies.

Based on limitations discussed in Section 7.1.2, we also identify a number of research problems aimed at generalizing the impact of our technique. We would like to investigate the extension of our main theorem to the case of protocols with states. This is certainly technically challenging, but would make it possible to model more protocols, or at least model them more faithfully. We are also interested in extending our method to protocols with more than 2 parties which are commonplace (e.g. the combination of DAA join and DAA sign is essentially a 3-party protocol).

Finally, we believe that the overall methodology developed in this paper (i.e. privacy via sufficient conditions) could be applied in other contexts where privacy is critical: e.g. e-voting, attribute-based credentials, blockchain technologies, transparent certificate authorities. In our opinion, the privacy via sufficient conditions approach also sheds light on the privacy notions themselves. Indeed, each sufficient condition helps to get a better grasp of necessary ingredients for preserving privacy. It might thus be interesting to translate such conditions into more comprehensive guidelines helping the design of new privacy-enhancing protocols.

Footnotes

Appendix

We provide in this appendix the proof of our main result (Theorem 1). Our main argument consists in showing that, for any execution of $M_{Π, \overline{id}}$ , there is an indistinguishable execution of $S_{Π}$ (the other direction being easy). This indistinguishable execution will be obtained by a modification of the involved agents. We will proceed via a renaming of agents applied to an abstraction of the given execution of $M_{Π, \overline{id}}$ . We then prove that the renamed executions can still be executed and produce an indistinguishable frame.

We fix a protocol $Π = (\overline{k}, {\overline{n}}_{I}, {\overline{n}}_{R}, †_{I}, †_{R}, I, R)$ , some identity names $\overline{id}$ and some fresh constants $\overline{{id}_{0}}$ yielding a process $M_{Π, \overline{id}}$ as defined in Section 3. We denote ${id}_{0}_{i}$ (resp ${id}_{i}$ , $k_{i}$ , and $k_{i}^{'}$ ) the ith element of the sequence $\overline{{id}_{0}}$ (resp. $\overline{id}$ , $\overline{k}$ , and $\overline{k^{'}}$ ). The construction of the proof will slightly differ depending on $†_{I}, †_{R}$ (sequential vs concurrent sessions) and whether $fn (I) \cap fn (R) = \emptyset$ or not (non-shared case vs shared case).

Abstraction of configurations

Instead of working with $M_{Π, \overline{id}}$ , $M_{Π}$ , and $S_{Π}$ , it will be more convenient to work with ground configurations. Intuitively, we will associate to each execution of $M_{Π, \overline{id}}$ , $M_{Π}$ , and $S_{Π}$ , a ground configuration that contains all agents involved in that execution, already correctly instantiated. By doing so, we are able to get rid of technical details such as unfolding replications and repetitions a necessary number of times, create necessary identity and session parameters, etc.These ground configurations are generated from sequences of annotations satisfying some requirements.

Control is determined by associations

We show in that section that the outcome of tests is entirely determined by associations. This will be useful to show that, if we modify an execution (by renaming agents) while preserving enough associations, then the control flow is left unchanged. Proposition 5.

We assume that Π satisfies item (i) of the well-authentication condition. Let $ta = {ta}_{0} . τ_{x} [a_{1}]$ with $τ_{x} \in {τ_{then}, τ_{else}}$ be a well-formed annotated trace such that $\begin{matrix} K (ta) \overset{{ta}_{0} . τ_{x} [a_{1}]}{\to} (P; ϕ) \end{matrix}$ and the last action (i.e. $τ_{x} [a_{1}]$ ) is performed by an unsafe conditional. We have that $τ_{x} = τ_{then}$ if, and only if, there exists $a_{2} \in A$ such that $a_{1}$ and $a_{2}$ are associated in $({ta}_{0}, ϕ)$ .

Proof.

(⇒) We start by applying Proposition 4 to obtain an execution $\begin{matrix} M_{Π, \overline{id}} \overset{{ta}_{0} . τ_{then} [a_{1}]}{\Rightarrow} (P^{'}; ϕ) and thus M_{Π, \overline{id}} \overset{{ta}_{0}^{*} . τ_{then} [a_{1}]}{\to} (P^{″}; ϕ) \end{matrix}$ for some ${ta}_{0}^{*} \overset{τ}{=} {ta}_{0}$ . As a consequence of well-authentication, item (i) applied on the above execution, we obtain that for some $a_{2} \in A$ , $a_{1}$ and $a_{2}$ are associated in $({ta}_{0}^{*}, ϕ)$ . Since ${ta}_{0} \overset{τ}{=} {ta}_{0}^{*}$ , they are also associated in $({ta}_{0}, ϕ)$ .

(⇐) For this other direction, we observe that (up to changes of recipes that do not affect the resulting messages) if two agents are associated in the above execution (starting with $K (ta)$ ), then they are executing the honest trace of Π modulo a renaming of parameters, thus the considered test must be successful. We thus assume that $a_{1} = A_{1} (\overline{k_{1}}, \overline{n_{1}})$ and $a_{2} = A_{2} (\overline{k_{2}}, \overline{n_{2}})$ are associated in $({ta}_{0}, ϕ)$ we shall prove that $τ_{x} = τ_{then}$ . By association, ${ta}_{0} |_{a_{1}, a_{2}}$ is honest: its observable actions are of the form $out (c_{1}, w_{1}) . in (c_{1}^{'}, M_{1}) \dots out (c_{n}, w_{n}) . in (c_{n}^{'}, M_{n})$ with possibly an extra output at the end, and are such that $M_{i} ϕ ⇓ =_{E} w_{i} ϕ$ for all $1 ⩽ i ⩽ n$ . Consider ${ta}^{'}$ obtained from ${ta}_{0}$ by replacing each recipe $M_{i}$ by $w_{i}$ . Since this change of recipes does not affect the resulting messages, the modified trace can still be executed by $K (ta)$ and yields the same configuration $(P; ϕ)$ . But now ${ta}^{'} |_{a_{1}, a_{2}}$ is a self-contained execution, i.e. if P and Q are the processes (possibly sub-processes) respectively annotated $a_{1}$ and $a_{2}$ in $K (ta)$ , we have: $\begin{matrix} ({P [a_{1}], Q [a_{2}]}; \emptyset) \overset{{ta}^{'} |_{a_{1}, a_{2}}}{\to} ({P^{'} [a_{1}], Q^{'} [a_{2}]}; ϕ^{'}) \overset{τ_{x} [a_{1}]}{\to} ({P^{″} [a_{1}], Q^{'} [a_{2}]}; ϕ^{'}) . \end{matrix}$ In the shared case (i.e. $fn (I) \cap fn (R) \neq \emptyset$ ), by definition of association, the identity parameters of $a_{1}$ are equal to those of $a_{2}$ . Otherwise, it holds that $fn (I) \cap fn (R) = \emptyset$ . In both cases, we thus have: $\begin{array}{l} ({new \overline{k} . (new {\overline{n}}_{I} . I | new {\overline{n}}_{R} . R)}; \emptyset) & \overset{τ^{*}}{\to} ({P [a_{1}], Q [a_{2}]}; \emptyset) \\ \overset{{ta}^{'} |_{a_{1}, a_{2}}}{\to} ({P^{'} [a_{1}], Q^{'} [a_{2}]}; ϕ^{'}) \\ \overset{τ_{x} [a_{1}]}{\to} ({P^{″} [a_{1}], Q^{'} [a_{2}]}; ϕ^{'}) . \end{array}$ In that execution, everything is deterministic (up to the equational theory) and thus the execution is actually a prefix of the honest execution of Π (from the process $P_{Π}$ defined in Definition 5), up to a bijective renaming of parameters (note that P and Q do not share session parameters). Remind that all tests must be positive in the honest execution (i.e. $τ_{else}$ does not occur in the honest execution). Therefore, $τ_{x} = τ_{then}$ concluding the proof. □

Invariance of frame idealisations

In general, a renaming of annotations can break executability: as illustrated in Example 33, mapping two dual annotations to annotations with different identities breaks the ability of the two underlying agents to communicate successfully. Moreover, even when executability is preserved, parameters change (so do names) and thus frames are modified. However, as stated next in Proposition 6, such renamings do not change idealised frames. We obtain the latter since we made sure that idealised frames only depend on what is already observable and not on specific identity or session parameters. In combination with frame opacity, this will imply (Proposition 7) that a renaming of annotations has no observable effect on the resulting real frames. Proposition 6.

Let $ta$ be an annotated trace such that $Φ_{ideal} (ta)$ is well-defined. Let ρ be a renaming of annotations. We have that $Φ_{ideal} (ta) \sim Φ_{ideal} (ta ρ)$ .

Proof.

Let $ta$ be an annotated trace such that $Φ_{ideal} (ta)$ is well-defined. Let ρ be a renaming of annotations. Let ${fr}_{1}$ be an arbitrary name assignment, and ${fr}_{2}$ be an injective function satisfying ${fr}_{2} (a ρ, x) = {fr}_{1} (a, x)$ . First, we show, by induction on $ta$ , that $Φ_{ideal}^{{fr}_{1}} (ta) = Φ_{ideal}^{{fr}_{2}} (ta ρ)$ . The only interesting case is when $ta = {ta}_{0} . (ℓ : out (c, w) [a])$ . In such a case, we have that: $\begin{matrix} Φ_{ideal}^{{fr}_{1}} ({ta}_{0} . (ℓ : out (c, w) [a])) = Φ_{ideal}^{{fr}_{1}} ({ta}_{0}) \cup {w \mapsto ideal (ℓ) σ_{1}^{i} σ_{1}^{n} ⇓} \end{matrix}$ with $σ_{1}^{n} (x_{j}^{n}) = {fr}_{1} (a, x_{j}^{n})$ and $σ_{1}^{i} (x_{j}^{i}) = R_{j} Φ_{ideal}^{{fr}_{1}} ({ta}_{0})$ where $R_{j}$ is the jth input of a in ${ta}_{0}$ . The idealised frame $Φ_{ideal}^{{fr}_{2}} (ta ρ)$ is defined similarly, i.e. $\begin{matrix} Φ_{ideal}^{{fr}_{2}} ({ta}_{0} ρ . (ℓ : out (c, w) [a ρ])) = Φ_{ideal}^{{fr}_{2}} ({ta}_{0} ρ) \cup {w \mapsto ideal (ℓ) σ_{2}^{i} σ_{2}^{n} ⇓} \end{matrix}$ with $σ_{2}^{n} (x_{j}^{n}) = {fr}_{2} (a ρ, x_{j}^{n})$ and $σ_{2}^{i} (x_{j}^{i}) = R_{j}^{ρ} Φ_{ideal}^{{fr}_{2}} ({ta}_{0} ρ)$ where $R_{j}^{ρ}$ is the jth input of $a ρ$ in ${ta}_{0} ρ$ . By induction hypothesis we know that $Φ_{ideal}^{{fr}_{1}} ({ta}_{0}) = Φ_{ideal}^{{fr}_{2}} ({ta}_{0} ρ)$ . Therefore, to conclude, it remains to show that $ideal (ℓ) σ_{1}^{i} σ_{1}^{n} = ideal (ℓ) σ_{2}^{i} σ_{2}^{n}$ . Actually, we have that $R_{j}^{ρ} = R_{j}$ , thus $σ_{1}^{i} (x_{j}^{i}) = σ_{2}^{i} (x_{j}^{i})$ , and $σ_{2}^{n} (x_{j}^{n}) = {fr}_{2} (a ρ, x_{j}^{n}) = {fr}_{1} (a, x_{j}^{n}) = σ_{1}^{n} (x_{j}^{n})$ .

We have shown that $Φ_{ideal}^{{fr}_{1}} (ta) = Φ_{ideal}^{{fr}_{2}} (ta ρ)$ and relying on Proposition 1, we easily deduce that $Φ_{ideal} (ta) \sim Φ_{ideal} (ta ρ)$ . □

Proposition 7.

We assume that Π satisfies frame opacity. Let ρ be a renaming of annotations and $ta$ be a well-formed annotated trace. If $K (ta) \overset{ta}{\Rightarrow} (P_{1}; ϕ_{1})$ and $K (ta ρ) \overset{ta ρ}{\Rightarrow} (P_{2}; ϕ_{2})$ , then we have that $ϕ_{1} \sim ϕ_{2}$ .

Proof.

We start by applying Proposition 4 on the two given executions to obtain two executions starting from $M_{Π, \overline{id}}$ :

$M_{Π, \overline{id}} \overset{{ta}^{*}}{\to} (P_{1}^{'}; ϕ_{1})$ with ${ta}^{*} \overset{τ}{=} ta$ ; and

$M_{Π, \overline{id}} \overset{{ta}_{ρ}^{*}}{\to} (P_{2}^{'}; ϕ_{2})$ with ${ta}_{ρ}^{*} \overset{τ}{=} ta ρ$ .

Relying on frame opacity, we know that

Φ_{ideal} ({ta}^{*})

(resp.

Φ_{ideal} ({ta}_{ρ}^{*})

) is well-defined and

Φ_{ideal} ({ta}^{*}) \sim ϕ_{1}

(resp.

Φ_{ideal} ({ta}_{ρ}^{*}) \sim ϕ_{2}

Note that, if ${ta}_{1}$ and ${ta}_{2}$ are two annotated traces such that ${ta}_{1} \overset{τ}{=} {ta}_{2}$ and ${fr}_{1}$ is a name assignment, then $Φ_{ideal}^{{fr}_{1}} ({ta}_{1}) = Φ_{ideal}^{{fr}_{1}} ({ta}_{2})$ . Thanks to this remark, we easily deduce that $Φ_{ideal} (ta) \sim Φ_{ideal} ({ta}^{*})$ and $Φ_{ideal} (ta ρ) = Φ_{ideal} ({ta}_{ρ}^{*})$ . Thanks to Proposition 6, we know that $Φ_{ideal} (ta) \sim Φ_{ideal} (ta ρ)$ and by transitivity of ∼, we conclude that $ϕ_{1} \sim ϕ_{2}$ . □

A sufficient condition for preserving executability

We can now state a key lemma (Lemma 2), identifying a class of renamings which yield indistinguishable executions. More precisely, this lemma shows that for renamings satisfying some requirements, if $K (ta)$ can execute an annotated trace $ta$ then $K (ta) ρ$ has an indistinguishable execution following the annotated trace $ta ρ$ . Remark that, in the conclusion, the renaming is applied after building the ground configuration ( $K (ta) ρ$ ) instead of building the ground configuration of the renamed trace ( $K (ta ρ)$ ). Both variants are a priori different. However, in the final proof and in order to leverage previous propositions, we will need to relate executions of $K (ta)$ with executions of $K (ta ρ)$ . The following easy proposition bridges this gap. We also state and prove a variant of Proposition 4, item (4) when ρ is applied after building the ground configuration.

Finally, after having defined the notion of connection between agents, we can state our key lemma. Definition 24.

Annotations a and $a^{'}$ are connected in $(ta, ϕ)$ if they are associated in $({ta}_{0}, ϕ)$ for some prefix ${ta}_{0}$ of $ta$ that contains at least one $τ_{then}$ action of an unsafe conditional annotated with either a or $a^{'}$ .

Lemma 2.

We assume that Π satisfies frame opacity and item (i) of well-authentication. Let $ta$ be a well-formed annotated trace such that $K (ta) \overset{ta}{\to} (P; ϕ)$ . Let ρ be a renaming of annotations. Moreover, when $fn (I) \cap fn (R) \neq \emptyset$ (shared case), we assume that for any annotations a, $a^{'}$ , it holds that a and $a^{'}$ are connected in $(ta, ϕ)$ , if, and only if, $ρ (a)$ and $ρ (a^{'})$ are dual.

We have that $K (ta) ρ \overset{ta ρ}{\to} (Q; ψ)$ for some ψ such that $ϕ \sim ψ$ .

Proof.

The ground configurations $K (ta)$ and $K (ta) ρ$ have the same shape: these processes only differ by their terms. Thus, we can put them together to form a bi-process,10

¹⁰

The bi-process considered here does not make use of the extension of diff-equivalence presented before: its inputs are of the form $in (c, x)$ and not $in (c, choice [x, y])$ .

i.e. a process in which terms are bi-terms of the form

choice (t_{1}, t_{2})

. Given a bi-process B, we denote

fst (B)

(resp.

snd (B)

) the process obtained from B by replacing any bi-term

choice [t_{1}, t_{2}]

t_{1}

(resp.

t_{2}

). Moreover, we write

B \overset{α [choice [a, a^{'}]]}{\to} B^{'}

to indicate that

fst (B)

executes α with annotation a and

snd (B)

performs α in the same way but with annotation

a^{'}

. More generally, we write

B \overset{choice [ta, {ta}^{'}]}{\to} B^{'}

to indicate that the bi-process B executes the trace

ta

on the left and

{ta}^{'}

on the right, where the two traces differ only in their annotations.

For the sake of simplicity, we decorate outputs of the biprocess obtained from $K (ta)$ and $K (ta) ρ$ with pairwise distinct handles from $W$ , and we assume that the handle that decorates an output will be used to store the output message when it will be executed. Lastly, we associate a vector of terms in $T (Σ_{pub}, W \cup X)$ to each safe conditional of the protocol: recall that $let \overline{z} = \overline{t} in P else Q$ is identified as a safe conditional only if there exists a sequence $\overline{R}$ of terms in $T (Σ_{pub}, W \cup X)$ such that $\overline{R} {w_{1} \mapsto u_{1}, \dots, w_{m} \mapsto u_{m}} = \overline{t}$ where $u_{i}$ are the messages used in outputs occurring before the conditional and $w_{i}$ is the handle associated to $u_{i}$ ; $\overline{R}$ is the vector of terms associated to the safe conditional. Note that $\overline{R}$ may contain variables from $X$ corresponding to inputs performed before the conditional, which will be instantiated by ground terms before the execution of the conditional. When executing a process with labels on conditionals, we assume that the execution of an input $in (c, x)$ with recipe $R_{i n}$ will instantiate the variable x occurring in the label of the conditional with $R_{i n}$ .

For any prefix $K (ta) \overset{{ta}_{0}}{\to} (P_{0}; ϕ_{0})$ of the execution $K (ta) \overset{ta}{\to} (P; ϕ)$ , we prove that there exists an execution $K (ta) ρ \overset{{ta}_{0} ρ}{\to} (Q_{0}; ψ_{0})$ such that:

$B \overset{choice [{ta}_{0}, {ta}_{0} ρ]}{\to} B_{0}$ with $fst (B_{0}) = (P_{0}; ϕ_{0})$ and $snd (B_{0}) = (Q_{0}; ψ_{0})$ .

Any bi-conditional $let \overline{z} = choice [{\overline{t}}_{l}, {\overline{t}}_{r}] in B_{P} else B_{Q}$ labeled with $\overline{R}$ is such that $\overline{R} = \overline{C} [R_{1}, \dots, R_{k}]$ with $\overline{C}$ a sequence of contexts built on $Σ_{pub}$ , and $R_{i} \in T (Σ_{pub}, W \cup X)$ is either a variable in $X$ or a $w \notin dom (ϕ_{0})$ or a recipe i.e. a term in $T (Σ_{pub}, dom (ϕ_{0}))$ . Moreover, assuming that $u ⇓ u$ for any constructor term (even if it contains some variables), we have that $\overline{C} [R_{1} ϕ_{0}^{+} ⇓, \dots, R_{k} ϕ_{0}^{+} ⇓] = {\overline{t}}_{l}$ and $\overline{C} [R_{1} ψ_{0}^{+} ⇓, \dots, R_{k} ψ_{0}^{+} ⇓] = {\overline{t}}_{r}$ where $ϕ_{0}^{+}$ (resp. $ψ_{0}^{+}$ ) is $ϕ_{0}$ (resp. $ψ_{0}$ ) extended with $w \mapsto u$ for each output $out (c, u)$ decorated with w preceding the conditional in $fst (B_{0})$ (resp. $snd (B_{0})$ ).

$ϕ_{0} \sim ψ_{0}$ ;

when $fn (I) \cap fn (R) = \emptyset$ (non-shared case), $ρ (a)$ and $ρ (a^{'})$ are associated in $({ta}_{0} ρ, ψ_{0})$ if, and only if, a and $a^{'}$ are associated in $({ta}_{0}, ϕ_{0})$ ;

when $fn (I) \cap fn (R) \neq \emptyset$ (shared case), $ρ (a)$ and $ρ (a^{'})$ are associated in $({ta}_{0} ρ, ψ_{0})$ if, and only if, a and $a^{'}$ are associated in $({ta}_{0}, ϕ_{0})$ and connected in $(ta, ϕ)$ .

We proceed by induction on the prefix ${ta}_{0}$ of $ta$ .

Case ${ta}_{0}$ is empty. In such a case, ${ta}_{0} ρ$ can obviously be executed. Condition (b) is trivial since both frames are empty. In order to check conditions (c₁) and (c₂), note that association coincides with duality for empty traces. We start by establishing condition (c₁). Being dual simply means being distinct roles, hence one obviously has that $ρ (a)$ and $ρ (a^{'})$ are dual if, and only if, a and $a^{'}$ are. This allows us to conclude for condition (c₁). Now, we establish condition (c₂). By hypothesis, we have that a and $a^{'}$ are connected in $(ta, ϕ)$ if, and only if, $ρ (a)$ and $ρ (a^{'})$ are dual, this allows us to conclude regarding one direction. Now, if $ρ (a)$ and $ρ (a^{'})$ are dual, then a and $a^{'}$ are dual too by definition of an agent renaming. Hence, we have the other direction. Condition (a) holds and condition (a′) holds since by definition of being safe, we have the expected $\overline{R}$ .

Case the prefix of $ta$ is of the form ${ta}_{0} . α$ . The action α may be an input, an output, a conditional (i.e. $τ_{then}$ or $τ_{else}$ ). By (a), we know that there is a process in $Q_{0}$ which is able to perform an action of the same nature. We consider separately the case where α is an input, an output or a conditional. In those cases α is necessarily annotated, say by a, and has been produced by a process annotated a in $P_{0}$ . By induction hypothesis we have $(P_{0}; ϕ_{0})$ and $(Q_{0}; ψ_{0})$ and the following executions $\begin{matrix} K (ta) \overset{{ta}_{0}}{\to} (P_{0}; ϕ_{0}) \overset{α [a]}{\to} (P_{0}^{'}; ϕ_{0}^{'}) and K (ta) ρ \overset{{ta}_{0} ρ}{\to} (Q_{0}; ψ_{0}) \end{matrix}$ satisfying all our invariants. Note that one has $({ta}_{0} . α [a]) ρ = ({ta}_{0} ρ) . α [ρ (a)]$ . Moreover, we have that $B \overset{choice [{ta}_{0}, {ta}_{0} ρ]}{\to} B_{0}$ with $fst (B_{0}) = (P_{0}; ϕ_{0})$ and $snd (B_{0}) = (Q_{0}; ψ_{0})$ . Now, we have to prove that there exists $B_{0}^{'}$ such that $B_{0} \overset{choice [α, α ρ]}{\to} B_{0}^{'}$ with $fst (B_{0}^{'}) = (P_{0}^{'}; ϕ_{0}^{'})$ .

Case where α is an output . We immediately have that $Q_{0}$ can perform $α [ρ (a)]$ , on the same channel and with the same handle. We now have to check our invariants for ${ta}_{0} . α [a]$ . Let $out (c, w) [a]$ be α. Conditions (a) is obviously preserved. Regarding condition (a′), it is easy to see that the result holds. The term that was added in $ϕ_{0}^{+}$ (resp. $ψ_{0}^{+}$ ) is now present in $ϕ_{0}^{'}$ (resp. $ψ_{0}^{'}$ ).

Conditions (c₁) and (c₂) follow from the fact that association is not affected by the execution of an output: $ρ (a)$ and $ρ (a^{'})$ are associated in $({ta}_{0} . α [a]) ρ$ if, and only if, they are associated in ${ta}_{0} ρ$ , and similarly without ρ. Finally, we shall prove (b): $ϕ_{0}^{'} \sim ψ_{0}^{'}$ where $ϕ_{0}^{'}$ (resp. $ψ_{0}^{'}$ ) is the resulting frame after the action $α [a]$ (resp. $α [a ρ]$ ). Applying Proposition 4 item (4) on the execution before renaming and Proposition 9 on the execution after renaming, one obtains $\begin{matrix} K ({ta}_{0} . α [a]) \overset{{ta}_{0} . α [a]}{\to} (P_{0}^{″}; ϕ_{0}^{'}) and K ({ta}_{0} . α [a]) ρ \overset{({ta}_{0} ρ) . α [a ρ]}{\to} (Q_{0}^{'}; ψ_{0}^{'}) . \end{matrix}$ We finally conclude $ϕ_{0}^{'} \sim ψ_{0}^{'}$ using Proposition 8 on the execution on the right and then Proposition 7.

Case where α is a conditional . We first need to make sure that the outcome of the test is the same for a and $a ρ$ . We let $τ_{x}$ (resp. $τ_{y}$ ) be the action produced by evaluating the conditional of a (resp. $a ρ$ ) and shall prove that $τ_{x} = τ_{y}$ . We distinguish two cases depending on whether the conditional has a label (i.e. has been identified as safe) or not.

If the conditional has a label $\overline{R}$ , since this conditional is now at toplevel, we know that $ϕ_{0}^{+} = ϕ_{0}$ and $ψ_{0}^{+} = ψ_{0}$ , and $\overline{R} = \overline{C} [R_{1}, \dots, R_{k}]$ only contains variables from $dom (ϕ_{0}) = dom (ψ_{0})$ . On the left, we have that the conditional will be evaluated to true iff ${\overline{t}}_{l} ⇓$ is a message, i.e. iff $\overline{C} [R_{1} ϕ_{0}^{+} ⇓, \dots, R_{k} ϕ_{0}^{+} ⇓] ⇓$ is a message, i.e. iff $\overline{C} [R_{1}, \dots, R_{k}] ϕ_{0} ⇓$ is a message and similarly on the right. Since $ϕ_{0} \sim ψ_{0}$ , this allows us to conclude that the two conditionals have the same outcome.

If the conditional is unsafe, we make use of Proposition 5 to show that the outcome of the conditional is the same on both sides. First, we deduce the following executions from Proposition 4 item (4) applied on the execution before renaming and Proposition 9 applied on the execution after renaming: $\begin{matrix} K ({ta}_{0} . τ_{x} [a]) \overset{{ta}_{0} . τ_{x} [a]}{\to} (P_{0}^{″}; ϕ_{0}) and K ({ta}_{0} . τ_{y} [a]) ρ \overset{({ta}_{0} ρ) . τ_{y} [a ρ]}{\to} (Q_{0}^{'}; ψ_{0}) . \end{matrix}$ To infer $τ_{x} = τ_{y}$ from Proposition 5, it remains to prove that a and $a^{'}$ are associated in $({ta}_{0}, ϕ_{0})$ if, and only if, $ρ (a)$ and $ρ (a^{'})$ are associated in $({ta}_{0} ρ, ψ_{0})$ . When $fn (I) \cap fn (R) = \emptyset$ (non-shared case), this is given by the invariant (c₁). Otherwise, when $fn (I) \cap fn (R) \neq \emptyset$ (shared case), (c₂) gives us that $ρ (a)$ and $ρ (a^{'})$ are associated in $({ta}_{0} ρ, ψ_{0})$ if, and only if, a and $a^{'}$ are associated in $({ta}_{0}, ϕ_{0})$ and connected in $(ta, ϕ)$ . Therefore, to conclude, it is actually sufficient to show that if a and $a^{'}$ are associated in $({ta}_{0}, ϕ_{0})$ then $ρ (a)$ and $ρ (a^{'})$ are associated in $({ta}_{0} ρ, ψ_{0})$ . Since a and $a^{'}$ are associated in $({ta}_{0}, ϕ_{0})$ , thanks to Proposition 5, we know that the outcome of the test will be positive (i.e. $τ_{x} = τ_{then}$ ), and thus a and $a^{'}$ are connected in $({ta}_{0} . τ_{τ_{then}}, ϕ_{0})$ , and therefore a and $a^{'}$ are also connected in $(ta, ϕ)$ . Thanks to (c₂) we have that $ρ (a)$ and $ρ (a^{'})$ are associated in $({ta}_{0} ρ, ψ_{0})$ , and we are done.

After the execution of this conditional producing

τ_{x} = τ_{y}

, condition (a) and (a′) obviously still hold since

τ_{x} = τ_{y}

implying that both agents go to the same branch of the conditional. Invariant (b) is trivial since frames have not changed. Conditions (c₁) and (c₂) are preserved because the association between a and

a^{'}

is preserved if, and only if, the outcome of the test is positive, which is the same before and after the renaming.

Case where $α = in (c, R_{i n})$ is an input . We immediately have that $Q_{0}$ can perform $α [ρ (a)]$ on the same channel and with the same recipe $R_{i n}$ (since $dom (ϕ_{0}) = dom (ψ_{0})$ follows from $ϕ_{0} \sim ψ_{0}$ ). Conditions (a) and (b) are obviously preserved. Let us establish Condition (a′). We consider a bi-conditional $let \overline{z} = choice [{\overline{t}}_{l}, {\overline{t}}_{r}] in B_{P} else B_{Q}$ labeled with $\overline{R}$ before executing α. Thus, we know that $(a^{'})$ holds, i.e. $\overline{R} = \overline{C} [R_{1}, \dots, R_{k}]$ such that $\overline{C} [R_{1} ϕ_{0}^{+} ⇓, \dots, R_{k} ϕ_{0}^{+} ⇓] = {\overline{t}}_{l}$ and $\overline{C} [R_{1} ψ_{0}^{+} ⇓, \dots, R_{k} ψ_{0}^{+} ⇓] = {\overline{t}}_{r}$ . After executing α, either this conditional is kept unchanged and the result trivially holds, or ${\overline{t}}_{l}$ becomes ${\overline{t}}_{l} {x \mapsto R_{i n} ϕ_{0} ⇓}$ and we have that the label of this conditional is now ${\overline{R}}^{'} = \overline{R} {x \mapsto R_{i n}}$ , and we have that $R_{i n} ϕ_{0} ⇓$ (and thus $R_{i n} ψ_{0} ⇓$ ) is a message. To conclude, it remains to show that $\overline{C} [R_{1} {x \mapsto R_{i n}} ϕ_{0}^{+} ⇓, \dots, R_{k} {x \mapsto R_{i n}} ϕ_{0}^{+} ⇓] = {\overline{t}}_{l} {x \mapsto R_{i n} ϕ_{0} ⇓}$ (and similarly for $ψ_{0}$ ). Either $R_{i} = x$ and we have that $R_{i} {x \mapsto R_{i n}} ϕ_{0}^{+} ⇓ = R_{i n} ϕ_{0} ⇓ = (R_{i} ϕ_{0}^{+} ⇓) {x \mapsto R_{i n} ϕ_{0} ⇓}$ . Otherwise, $R_{i}$ does not contain x, and we have that $R_{i} {x \mapsto R_{i n}} ϕ_{0}^{+} ⇓ = R_{i} ϕ_{0}^{+} ⇓ = (R_{i} ϕ_{0}^{+} ⇓) {x \mapsto R_{i n} ϕ_{0} ⇓}$ .

Thus, we have that $\overline{C} [R_{1} {x \mapsto R_{i n}} ϕ_{0}^{+} ⇓, \dots, R_{k} {x \mapsto R_{i n}} ϕ_{0}^{+} ⇓] = \overline{C} [(R_{1} ϕ_{0}^{+} ⇓) {x \mapsto R_{i n} ϕ_{0}}, \dots, (R_{k} ϕ_{0}^{+} ⇓) {x \mapsto R_{i n} ϕ_{0}}] = \overline{C} [R_{1} ϕ_{0}^{+} ⇓, \dots, R_{1} ϕ_{0}^{+} ⇓] {x \mapsto R_{i n} ϕ_{0} ⇓} = {\overline{t}}_{l} {x \mapsto R_{i n} ϕ_{0} ⇓}$ . This allows us to conclude.

Conditions (c₁) and (c₂) are preserved because honest interactions are preserved by the renaming, since $ϕ_{0} \sim ψ_{0}$ by invariant (b). We only detail one direction of (c₁), the other cases being similar. Assume that $ρ (a)$ and $ρ (a^{'})$ are associated in $(({ta}_{0} . α [a]) ρ, ψ_{0})$ . The renamed agents $ρ (a)$ and $ρ (a^{'})$ are also associated in $({ta}_{0} ρ, ϕ^{'})$ , thus a and $a^{'}$ are associated in $({ta}_{0}, ϕ^{'})$ . Now, because α did not break the association of $ρ (a)$ and $ρ (a^{'})$ in $({ta}_{0} ρ, ψ_{0})$ , it must be that the input message in $α = in (c, R_{i n})$ corresponds to the last output of $ρ (a^{'})$ in ${ta}_{0} ρ$ . Formally, if that last output corresponds to the handle w in $ψ_{0}$ , we have $R_{i n} ψ_{0} ⇓ =_{E} w ψ_{0}$ . But, because $ϕ_{0} \sim ψ_{0}$ by invariant (b), we then also have $M ϕ_{0} ⇓ =_{E} w ϕ_{0}$ and the association of a and $a^{'}$ in $({ta}_{0}, ϕ_{0})$ carries over to $({ta}_{0} . α [a], ϕ_{0})$ . □

Final proof

Thanks to Lemma 2, we can transform any execution of $M_{Π, \overline{id}}$ into an indistinguishable execution of $S_{Π}$ , provided that an appropriate renaming of annotations exists. In order to prove that such a renaming exists in Proposition 11, we show below that in the shared case, agents cannot be connected multiple times.

We are now able to prove our main theorem.

Acknowledgments

We would like to thank Bruno Blanchet for his valuable help regarding the mechanisation in ProVerif of our frame opacity condition. The extension of bi-processes in Section is due to him. We also thank Solène Moreau for her useful feedback on earlier versions of this paper. This work was conducted when Lucca Hirschi was working at LSV, ENS Paris-Saclay & Université Paris-Saclay, France and then at ETH Zurich, Switzerland. This work has received funding from the European Research Council (ERC) under the EU’s Horizon 2020 research and innovation program (grant agreement No 714955-POPSTAR) and the ANR project SEQUOIA ANR-14-CE28-0030-01.

References

Abadi and

Blanchet, Computer-assisted verification of a protocol for certified email, in: Static Analysis, Springer, 2003, pp. 316–335. doi:10.1007/3-540-44898-5_17.

Abadi and

Fournet, Mobile values, new names, and secure communication, in: Proceedings of POPL’01, ACM Press, 2001.

Alpár and

J.-H.

Hoepman, A secure channel for attribute-based credentials:[short paper], in: Proceedings of the 2013 ACM Workshop on Digital Identity Management, ACM, 2013, pp. 13–18. doi:10.1145/2517881.2517884.

Arapinis,

Cheval and

Delaune, Verifying privacy-type properties in a modular way, in: Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF’12), IEEE Computer Society Press, Cambridge Massachusetts, USA, 2012, pp. 95–109.

Arapinis,

Chothia,

Ritter and

Ryan, Analysing unlinkability and anonymity using the applied pi calculus, in: Proceedings of CSF’10, IEEE Comp. Soc. Press, 2010.

Arapinis,

Mancini,

Ritter,

Ryan,

Golde,

Redon and

Borgaonkar, New privacy issues in mobile telephony: Fix and verification, in: Proceedings of the ACM Conference on Computer and Communications Security, ACM, 2012, pp. 205–216.

Arapinis,

L.I.

Mancini,

Ritter and

Ryan, Privacy through pseudonymity in mobile telephony systems, in: NDSS, 2014.

Armando

et al., The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures, in: Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), Vol. 7214, Springer, 2012, pp. 267–282.

Armando,

Carbone,

Compagna,

Cuéllar and

M.L.

Tobarra, Formal analysis of SAML 2.0 web browser single sign-on: Breaking the SAML-based single sign-on for Google apps, in: Proc. 6th ACM Workshop on Formal Methods in Security Engineering (FMSE’08), ACM, 2008, pp. 1–10.

10.

Backes,

Hritcu and

Maffei, Automated verification of remote electronic voting protocols in the applied pi-calculus, in: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, 23–25 June, IEEE Computer Society, Pittsburgh, Pennsylvania, 2008, pp. 195–209. doi:10.1109/CSF.2008.26.

11.

Backes,

Maffei and

Unruh, Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol, in: Security and Privacy, SP 2008. IEEE Symposium on, IEEE, 2008, pp. 202–215.

12.

Basin,

Dreier,

Hirschi,

Radomirović,

Sasse and

Stettler, Formal analysis of 5G authentication, 2018, arXiv preprint arXiv:1806.10360.

13.

Basin,

Dreier and

Sasse, Automated symbolic proofs of observational equivalence, in: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, ACM, 2015, pp. 1144–1155.

14.

Baudet, Deciding security of protocols against off-line guessing attacks, in: Proc. 12th Conference on Computer and Communications Security, ACM, 2005.

15.

Bender,

Ö.

Dagdelen,

Fischlin and

Kügler, The pace aa protocol for machine readable travel documents, and its security, in: Financial Cryptography and Data Security, Springer, 2012, pp. 344–358. doi:10.1007/978-3-642-32946-3_25.

16.

Bender,

Fischlin and

Kügler, Security analysis of the pace key-agreement protocol, in: Information Security, Springer, 2009, pp. 33–48. doi:10.1007/978-3-642-04474-8_3.

17.

Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, in: Proceedings of CSFW’01, IEEE Comp. Soc. Press, 2001, pp. 82–96.

18.

Blanchet,

Abadi and

Fournet, Automated verification of selected equivalences for security protocols, Journal of Logic and Algebraic Programming (2008).

19.

Blanchet and

Smyth, Automated reasoning for equivalences in the applied pi calculus with barriers, in: Proc. 29th Computer Security Foundations Symposium, 2016.

20.

Brusó, Dissecting Unlinkability, PhD thesis, Technische Universiteit Eindhoven, 2014.

21.

Brusó,

Chatzikokolakis and

den Hartog, Formal verification of privacy for RFID systems, in: Proceedings of CSF’10, 2010.

22.

Brusó,

Chatzikokolakis,

Etalle and

Den Hartog, Linking unlinkability, in: Trustworthy Global Computing, Springer, 2012, pp. 129–144.

23.

Camenisch,

Lehmann and

Neven, Electronic identities need private credentials, IEEE Security & Privacy 10(1) (2012), 80–83. doi:10.1109/MSP.2012.7.

24.

Camenisch,

Mödersheim and

Sommer, A formal model of identity mixer, in: Formal Methods for Industrial Critical Systems, Springer, 2010, pp. 198–214. doi:10.1007/978-3-642-15898-8_13.

25.

Cheikhrouhou,

Stephan,

Ö.

Dagdelen,

Fischlin and

Ullmann, Merging the cryptographic security analysis and the algebraic-logic security proof of pace, in: Sicherheit, 2012, pp. 83–94.

26.

Cheval and

Blanchet, Proving more observational equivalences with ProVerif, in: Proc. 2nd Conference on Principles of Security and Trust, LNCS, Vol. 7796, Springer, 2013, pp. 226–246. doi:10.1007/978-3-642-36830-1_12.

27.

Cheval,

Comon-Lundh and

Delaune, Trace equivalence decision: Negative tests and non-determinism, in: Proceedings of CCS’11, ACM Press, 2011.

28.

Chrétien,

Cortier and

Delaune, From security protocols to pushdown automata, ACM Transactions on Computational Logic 1 (2015), 3.

29.

Cohn-Gordon,

Cremers,

Dowling,

Garratt and

Stebila, A formal security analysis of the signal messaging protocol, in: Security and Privacy (EuroS&P), 2017 IEEE European Symposium on, IEEE, 2017, pp. 451–466. doi:10.1109/EuroSP.2017.27.

30.

Comon and

Koutsos, Formal computational unlinkability proofs of rfid protocols, in: 2017 IEEE 30th Computer Security Foundations Symposium (CSF), 2017, pp. 100–114. doi:10.1109/CSF.2017.9.

31.

Cortier,

Delaune and

Lafourcade, A survey of algebraic properties used in cryptographic protocols, Journal of Computer Security 14(1) (2006), 1–43. doi:10.3233/JCS-2006-14101.

32.

Cortier and

Smyth, Attacking and fixing Helios: An analysis of ballot secrecy, Journal of Computer Security 21(1) (2013), 89–148. doi:10.3233/JCS-2012-0458.

33.

Delaune and

Hirschi, A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols, Journal of Logical and Algebraic Methods in Programming (2016).

34.

Delaune,

Kremer and

M.D.

Ryan, Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security 4 (2008).

35.

Delaune,

M.D.

Ryan and

Smyth, Automatic verification of privacy properties in the applied pi-calculus, in: Proceedings of the 2nd Joint ITrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM’08), IFIP Conference Proceedings, Vol. 263, Springer, 2008.

36.

Dong,

Jonker and

Pang, Formal analysis of privacy in an ehealth protocol, in: Computer Security–ESORICS 2012, Springer, 2012, pp. 325–342. doi:10.1007/978-3-642-33167-1_19.

37.

Dreier,

Hirschi,

Radomirovic and

Sasse, Automated unbounded verification of stateful cryptographic protocols with exclusive or, in: 31st IEEE Computer Security Foundations Symposium (CSF’2018), 2018.

38.

Feldhofer,

Dominikus and

Wolkerstorfer, Strong authentication for RFID systems using the AES algorithm, in: Cryptographic Hardware and Embedded Systems-CHES 2004, Springer, 2004, pp. 357–370. doi:10.1007/978-3-540-28632-5_26.

39.

Hirschi, Automated Verification of Privacy in Security Protocols: Back and Forth Between Theory & Practice, PhD thesis, École Normale Supérieure Paris-Saclay, 2017.

40.

Hirschi,

Baelde and

Delaune, A method for verifying privacy-type properties: The unbounded case, in: Proceedings of the 37th IEEE Symposium on Security and Privacy (S&P’16), IEEE Computer Society Press, San Jose, California, USA, 2016.

41.

Iso 15408-2: Common criteria for information technology security evaluation – part 2: Security functional components, 2009.

42.

Juels and

S.A.

Weis, Defining strong privacy for RFID, ACM Transactions on Information and System Security (TISSEC) 13(1) (2009), 7. doi:10.1145/1609956.1609963.

43.

Lee,

Asano and

Kim, RFID mutual authentication scheme based on synchronized secret information, in: Symposium on Cryptography and Information Security, 2006.

44.

Meadows, Formal methods for cryptographic protocol analysis: Emerging issues and trends, IEEE journal on selected areas in communications 21(1) (2003), 44–54. doi:10.1109/JSAC.2002.806125.

45.

Meier,

Schmidt,

Cremers and

Basin, The tamarin prover for the symbolic analysis of security protocols, in: Proc. 25th International Conference on Computer Aided Verification (CAV’13), LNCS, Vol. 8044, Springer, 2013, pp. 696–701.

46.

Paquin and

Zaverucha, U-prove cryptographic specification v1.1 (revision 3), December 2013.

47.

Pfitzmann and

Köhntopp, Anonymity, Unobservability, and Pseudonymity – a Proposal for Terminology. In Designing Privacy Enhancing Technologies, Springer, 2001, pp. 1–9.

48.

PKI for machine readable travel documents offering ICC read-only access, 2004, Technical report, International Civil Aviation Organization.

49.

Santiago,

Escobar,

Meadows and

Meseguer, A formal definition of protocol indistinguishability and its verification using maude-npa, in: Security and Trust Management, Springer, 2014, pp. 162–177.

50.

Smyth,

M.D.

Ryan and

Chen, Formal analysis of privacy in direct anonymous attestation schemes, Science of Computer Programming 111 (2015), 300–317. doi:10.1016/j.scico.2015.04.004.

51.

UKano tool and case studies. http://projects.lsv.ens-cachan.fr/ukano/. Accessed: 12-11-2018.

52.

Van Deursen and

Radomirovic, Attacks on RFID protocols, IACR Cryptology ePrint Archive 2008 (2008), 310.

A method for unbounded verification of privacy-type properties

Abstract

Keywords

1. Introduction

2. Modelling protocols

2.1. Term algebra

3.1. Trace equivalence

3.2.1. Unlinkability

4.1. Annotations

2 This assumption only serves the purpose of uniquely identifying agents. The assumed session nonces do not have to occur in the corresponding roles, so this does not require to change the protocol under study.

5.1. Frame opacity

5.2.1. Condition (i)

6. Case studies

6.1. Hash–Lock protocol

6.2. LAK protocol

6.3. BAC protocol and some others

6 For more information about IRMA (“I Reveal My Attributes”), see https://www.irmacard.org.

6.6.1. DAA join

8 The protocol also specifies a mode that makes different signatures linkable by construction using z e t a V = h ( ( 0 , b s n V ) ) . We focus on the other mode for which unlinkability is expected to hold.

7.1. Limitations of our Theorem 1

7.1.1. Tightness of our conditions

8. Conclusion

Footnotes

Appendix

Abstraction of configurations

Control is determined by associations

Invariance of frame idealisations

A sufficient condition for preserving executability

Final proof

Acknowledgments

References

²
This assumption only serves the purpose of uniquely identifying agents. The assumed session nonces do not have to occur in the corresponding roles, so this does not require to change the protocol under study.

⁶
For more information about IRMA (“I Reveal My Attributes”), see https://www.irmacard.org.

⁸
The protocol also specifies a mode that makes different signatures linkable by construction using $z e t a_{V} = h ((0, b s n V))$ . We focus on the other mode for which unlinkability is expected to hold.