David Baelde

Alexandre Debant

Stéphanie Delaune

Proving Unlinkability using ProVerif through Desynchronised Bi-Processes

Unlinkability is a privacy property of crucial importance for several systems such as mobile phones or RFID chips. Analysing this security property is very complex, and highly error-prone. Therefore, formal verification with machine support is desirable. Unfortunately, existing techniques are not sufficient to directly apply verification tools to automatically prove unlinkability.

In this paper, we overcome this limitation by defining a simple transformation that will exploit some specific features of ProVerif. This transformation, together with some generic axioms, allows the tool to successfully conclude on several case studies. We have implemented our approach, effectively obtaining direct proofs of unlinkability on several protocols that were, until now, out of reach of automatic verification tools.

I. INTRODUCTION

RFID tags are popping up everywhere. They are present in credit cards enabling wireless payments, in wireless keys for opening cars, in e-passport for storing fingerprints and iris scans, in e-ticketing systems for public transport, amusement parks, etc. Citizens do not expect to be traceable just because they carry an e-passport or a credit card. Many applications blatantly ignore such concerns. As a famous and widespread example, contactless credit cards reveal card numbers in clear [START_REF] Basin | The EMV standard: Break, fix, verify[END_REF]. More interestingly, subtle tracing attacks may be found even when this security goal is explicitly taken into account. For instance, the BAC protocol for e-passports can be exploited to trace citizens [START_REF] Chothia | A traceability attack against e-passports[END_REF]. The attack relies on the possibility for an attacker to trace a passport by observing which error is obtained when replaying a particular message.

According to the ISO/IEC 15408-2 standard, a protocol is said to provide unlinkability when "a user may make multiple uses of [the protocol] without others being able to link these uses together". This is often defined as the fact that an attacker should not be able to distinguish a scenario in which the same agent (i.e., the user) is involved in many sessions from one that involves different agents in each session. Following this intuition, slightly different definitions have been proposed, e.g. [START_REF] Van Deursen | Untraceability of RFID protocols. In Information Security Theory and Practices. Smart Devices, Convergence and Next Generation Networks[END_REF], [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF], [START_REF] Brusò | Formal verification of privacy for RFID systems[END_REF], [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF]. A comparison between some of them may be found in [START_REF] Brusò | Linking unlinkability[END_REF]. In this work, we consider a variant of the definition originally proposed in [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF], and revisited in [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF] to make it more suitable to analyse RFID protocols manipulating a database. This definition follows the intuition that an attacker should not be able to distinguish between the real situation where multiple users (e.g. tags) are present and involved in possibly many sessions, and the ideal one in which each user is playing at most one session (in which case it is obviously impossible to link sessions).

Designing protocols which actually achieve the required security goals is well-known to be error-prone. A common good practice is to formally analyse protocols using symbolic techniques and tools, as has been done, e.g., for TLS 1.3 [START_REF] Cremers | A comprehensive symbolic analysis of TLS 1[END_REF], [START_REF] Bhargavan | Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF]. Aiming at machine support is really relevant since manual proofs are error-prone, tedious and hardly verifiable. Moreover, new protocols are developed quite frequently and need to be verified quickly. These symbolic techniques are mature for reachability properties like confidentiality or authentication, and some tools exist, e.g. Tamarin [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF] and ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF], to ease the verification process. This approach has been extended to deal with privacy properties that are usually expressed through equivalences [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF], [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF]. Nevertheless, verifying a security property in such a setting, and especially unlinkability as defined above, remains a difficult problem. Actually, ProVerif and Tamarin can only prove a restricted form of equivalence, namely diff-equivalence, which (in its standard form) is too limiting to prove unlinkability.

Various avenues have been explored to overcome this limitation and go beyond diff-equivalence, with varying degrees of success. To the best of our knowledge, none of these works is fully satisfactory. Some works rely on a notion of unlinkability expressed using two phases (a learning phase followed by a guessing phase) which is more amenable to automation, but may be weaker than expected. This is the approach followed in [START_REF] Dreier | Automated unbounded verification of stateful cryptographic protocols with exclusive OR[END_REF] where several RFID protocols using the XOR operator have been analysed. However, the security analysis in this work is performed in a restricted setting considering only a fixed number of agents and/or sessions (typically 1 or 2). Another line of works consists of establishing unlinkability using an indirect approach, e.g. [START_REF] Brusò | Formal verification of privacy for RFID systems[END_REF], [START_REF] Hirschi | A method for verifying privacytype properties: The unbounded case[END_REF], [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF]. In a nutshell, these works propose conditions that are more easily verified using existing tools, and show that these conditions imply the strongest notion of unlinkability. The latest paper in this line of work, [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF], tackles protocols involving a database. It provides an improved notion of unlinkability for these protocols and sufficient conditions that have enabled several first-time unlinkability proofs (as well as the discovery of some attacks). In the present paper, we shall consider the same class of protocols and the same notion of unlinkability. We will come back to [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF] in section V-C to compare its outcomes with the ones resulting from the new approach that we propose. Finally, a natural solution to overcome the limitations of diff-equivalence would be to use restrictions, that have been available in Tamarin for a long time. They allow the user to restrict the analysis to a subset of traces, those satisfying the formulas expressed by the restrictions. A rather simple idea would be to apply such a restriction on one side to express the fact that each user can play only once. Unfortunately, restrictions turned out to be incorrectly handled by Tamarin 1 which might introduce a lack of soundness. Recently, the use of restrictions has been formally justified, but for a very specific class (namely Type-0) only [START_REF] Paradzik | Conditional observational equivalence and off-line guessing attacks in multiset rewriting[END_REF]. This type of restrictions allows one to enforce protocol phases (used e.g. in the analysis performed in [START_REF] Dreier | Automated unbounded verification of stateful cryptographic protocols with exclusive OR[END_REF]) but cannot capture e.g. equality restrictions needed to model conditional branching. Therefore, the analyses performed in [START_REF] Paradzik | Conditional observational equivalence and off-line guessing attacks in multiset rewriting[END_REF] to establish unlinkability revisiting the models provided in [START_REF] Dreier | Automated unbounded verification of stateful cryptographic protocols with exclusive OR[END_REF] have been done considering simplified models (without conditional branching).

Our contributions. The general purpose of our work is to explore how the tool ProVerif can be used to verify unlinkability properties.

We first clarify how the introduction of restrictions in ProVerif [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF] can be used to prove meaningful equivalences. This is non-trivial because ProVerif only proves diffequivalence on bi-processes, and restrictions in that setting formally express properties of bi-executions, while equivalences are more naturally expressed between two independent processes. We identify a class of so-called diff-safe restrictions which, intuitively, have a consistent meaning for the bi-process and its projections. Although this new tool gives us more flexibility to encode security properties, it is still insufficient to model unlinkability.

We then turn to our main contribution. We design transformations of ProVerif models (i.e. bi-processes equipped with axioms and lemmas) which can turn an original model for which ProVerif fails into an equivalent model (in a sense that we make precise later) for which ProVerif succeeds in practice. These transformations are not specific to unlinkability, but we have designed them to tackle the key difficulties faced when trying to automatically verify that property. Our transformations make use of several features which are specific to ProVerif:

• Our first transformation relies on a recent extension of the notion of bi-process. Roughly, a bi-process combines two processes, which are declared equivalent if they can always evolve simultaneously, even for actions that are not observable by the attacker. We propose to dissociate the two processes that form the bi-process when executing some specific unobservable instructions on which the two processes may diverge. This is possible thanks to 1 https://github.com/tamarin-prover/tamarin-prover/issues/324

an extended kind of bi-process, first considered in [START_REF] Hirschi | A method for unbounded verification of privacy-type properties[END_REF] and officially introduced in ProVerif in 2020 with version 2.02. • This transformation alone is not sufficient for the tool to conclude on our case studies because of internal overapproximations. However, adding some generic axioms, as authorised by the latest version of ProVerif presented in [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF], improves the accuracy enough to successfully conclude on all our examples. We have implemented our approach in a tool and applied it on several case studies, obtaining in this way, for the first time, direct proofs of unlinkability for several protocols.

II. MODELLING PROTOCOLS

We recall first how cryptographic messages are modelled as terms in ProVerif. Building on this, we shall see how protocols are modelled as processes, and how protocol indistinguishability is formally expressed through process equivalences.

A. Term algebra

As usual in the symbolic setting, messages are modelled through a term algebra. We assume an infinite set N of names used to represent atomic data such as keys, or nonces, as well as an infinite set Σ 0 of constants used to represent atomic data known by the attacker; and two infinite and disjoint sets of variables X and W. Variables in X are used to refer e.g. to input messages, and variables in W, called handles, are used as pointers to messages learned by the attacker. We assume a finite signature Σ of function symbols with their arity partitioned into two disjoint subsets Σ c , and Σ d representing respectively the constructors, and destructors, and we denote Σ + c = Σ c Σ 0 , and Σ + = Σ Σ 0 . We note T (F, D) the set of terms built from elements of the set of atomic data D by applying function symbols in the signature F. We refer to elements of T (Σ + , N ∪ X ) as expressions and elements of T (Σ + c , N ∪ X ) as (constructor) terms. We define vars(M ) as the set of variables that occur in an expression M . A term (resp. an expression) is ground when it contains no variable. We finally define names(M ) as the set of names occurring in M . We will sometimes use names(M ) and vars(D) as vectors, meaning that we select an arbitrary ordering over these finite sets.

In order to provide a meaning to constructor symbols, we equip (constructor) terms with an equational theory. We assume a set E of equations over T (Σ c , X ) and we define = E as the smallest congruence containing E that is closed under substitutions and under bijective renaming. In addition, the semantics of destructor symbols is given by a set R of ordered rewriting rules of the form g(M 1 , . . . , M n ) → M 0 with M 0 , M 1 , . . . , M n ∈ T (Σ c , X ). A ground expression D can be rewritten in D if there is a position p in D, a rewrite rule g(M 1 , . . . , M n ) → M 0 and a substitution θ from variables to ground terms such that D| p = E g(M 1 θ, . . . , M n θ), and D = E D[M 0 θ] p , i.e. D in which the subterm at position p has been replaced by M 0 θ. In the case where more than one rule may be applied at position p, only the first such rule can be effectively used. Given a ground expression D, it may be possible to rewrite it (in an arbitrary number of steps) into a ground (constructor) term M : in that case, this term is noted D⇓, and we say that D evaluates to D⇓. We write D ⇓ when no such term exists, and say that the computation fails.

For modelling purposes, we split the signature Σ c Σ d into two parts, Σ pub and Σ priv . An attacker builds his own messages by applying public function symbols to terms he already knows, and which are available to him through variables in W. Formally, a computation done by the attacker is a recipe, i.e. a term in T (Σ + pub , W) where

Σ + pub = Σ pub Σ 0 . Example 1: We consider Σ c = { , proj 1 , proj 2 , h}, Σ d = ∅,
and we assume that all the function symbols are public. The symbol of arity 2 is used to model the pairing operator, and we have projection symbols proj 1 and proj 2 (both of arity 1) to access the components of a pair. The symbol h of arity 2 represents a keyed hash function. Given n T , k ∈ N , we have that n T , h(n T , k) is a term.

The standard equational theory E pair modelling the pairing operator contains the two following equations:

proj 1 ( x 1 , x 2 ) = x 1 , and proj 2 ( x 1 , x 2 ) = x 2 .
The informed reader will have noticed that we have chosen here to represent the projections using constructors with an appropriate equational theory. Another choice could have been to use destructors and rewriting rules (instead of equations). Both representations are possible in ProVerif. We made this choice to be consistent with the assumptions of the transformation presented in Section IV-C.

Example 2: To illustrate the notion of destructor symbols and ordered rewriting systems, we consider the signature Σ = Σ c ∪ Σ d such that Σ c = Σ c ∪{true, false} and Σ d = {eq} together with the rewriting rules eq(x, x) → true, and eq(x, y) → false, in this order (in addition to the equational theory E pair given in Example 1). We assume again that all these function symbols are public.

Let w ∈ W, and k 0 ∈ Σ 0 . We have that R = eq(h(proj 1 (w), k 0 ), proj 2 (w)) is a recipe, and D = R{w → n T , h(n T , k 0 ) }, i.e. R in which the occurrences of w are replaced by n T , h(n T , k 0 ) , is a ground expression such that D⇓ = true.

B. Process algebra

We consider two disjoint sets C pub and C priv of channel names. The channels in C pub are assumed to be public, whereas those in C priv are not. We denote C = C pub C priv . We also consider a set Σ e of event symbols and a set Σ t of table symbols. An event symbol evt of arity k may be applied to k terms to form an event evt(M 1 , . . . , M k ). We assume that all table symbols are of arity 1. Events will be used to record particular points in executions, while tables are used to store data across sessions.

Protocols will be modelled as processes using the grammar given in Figure 1. We will not comment on the standard constructs of this grammar (i.e. null process, name and channel

P, Q := 0 | new n; P | out(c, M ); P | new c priv ; P | in(c, x); P | let x = D in P else Q | event(e); P | insert tbl (M ); P | !P | get tbl (x) st. D in P else Q | (P | Q) | i : P In this figure, c ∈ C, M ∈ T (Σ + c , N ∪ X ) is a term, x ∈ X , n ∈ N , c priv ∈ C priv , tbl ∈ Σ t , D ∈ T (Σ + , N ∪ X ) is an
expression and e is an event.

Fig. 1. Grammar for processes restrictions, input, output, parallel composition, replication). The process insert tbl (M ); P inserts a record in the table tbl then runs P , and get tbl (x) st. D in P else Q looks for a record M in the table tbl such that the expression D evaluates to true when x is bound to M . When such a record is found, it runs P in which x has been replaced by M . Otherwise, it runs Q. The construct let x = D in P else Q combines a computation with a conditional: it attempts to evaluate D, executes P with x bound to the resulting message upon success, and Q otherwise. The construct i : P models that the process P must be executed in phase i only. Finally, the last construct simply records the event e before executing P .

The constructs in and let bind their variables x in their sub-processes P . The get construct binds x in D and P . The free variables fv(P ) of a process P are defined accordingly. A process P is closed when fv(P ) = ∅.

The operational semantics of processes is given by a labelled transition system over configurations (denoted by K) representing the current state of the process. Definition 1: A configuration is a tuple (P; Φ; S; i) with i ∈ N and such that:

• P is a multiset of closed processes; • Φ = {w 1 → M 1 , . . . , w n → M n } is a frame representing
the knowledge of the adversary, i.e. a substitution where w 1 , . . . , w n are handles and M 1 , . . . , M n are ground terms; • S is a set of elements of the form tbl (M ) with tbl ∈ Σ t , and M a ground term. This set S represents the content of all the tables. We may write P for the configuration ({0 : P }; ∅; ∅; 0), where we explicitly indicate that the process is intended to execute in phase 0.

The labelled transitions are defined using usual rules (see e.g. [START_REF] Cortier | Efficiently deciding equivalence for standard primitives and phases[END_REF], [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF]). Some rules are recalled in Figure 2 synchronous on private channels (rule IO). Regarding tables, the semantics is given by the rules INSERT, GET-THEN, and GET-ELSE. We also have rules for the other constructs, and some rules to deal with phases, e.g. MOVE and PHASE. An execution trace is a finite sequence:

K 0 1 -→ K 1 2 -→ . . . n -→ K n .
The associated sequence of observables of such a trace is the sequence 1 , . . . , n from which τ actions have been removed. Given a closed process P , we denote traces(P ) the set of execution traces from P . Given an integer j such that 0 ≤ j ≤ n, we denote T [j] the configuration K j , i.e the configuration at step j in trace T .

Example 3: For illustration purposes, we consider the Basic Hash protocol as described in [START_REF] Brusò | Formal verification of privacy for RFID systems[END_REF]. Each tag stores a secret key that is never updated, and the readers have access to a database containing all these keys. We have that:

T → R : n T , h(n T , k)
where n T is a fresh nonce and k is the secret key. When receiving a message, the reader checks that it is a pair whose second element is a hash of the first element of the pair with one of the keys from the database. The protocol can be modelled in our syntax as follows:

P BH = (0 : ! new k; insert keys(k); 1 : ! P T ) | (1 : ! P R )
where k, n T ∈ N , y, z ∈ X , ok, error ∈ Σ 0 , keys ∈ Σ t , and c R , c T ∈ C pub . Moreover, we have that:

• P R = in(c R , x);
get keys(y) st. D in out(c R , ok) else out(c R , error); • D = eq(proj 2 (x), h(proj 1 (x), y)); and

• P T = new n T ; out(c T , n T , h(n T , k) ).

C. Trace equivalence

We now define the notion of trace equivalence on which our definition of unlinkability is based. Intuitively, two processes are trace equivalent if for each trace of one process, there is an indistinguishable trace of the other process. To define this formally, we first introduce static equivalence between frames. Intuitively, an attacker can distinguish two frames Φ and Φ if there exists a test that fails in Φ and succeeds in Φ (or the contrary).

Definition 2: Two frames Φ and Φ are in static equivalence, written Φ ∼ s Φ , when dom(Φ) = dom(Φ ) and for any recipes R 1 and R 2 , we have that:

R 1 Φ⇓ = E R 2 Φ⇓, if, and only if, R 1 Φ ⇓ = E R 2 Φ ⇓. Example 4:
Continuing with the Basic Hash protocol, we consider the two following frames (n T , n T , k, k ∈ N ):

• Φ diff = {w 1 → n T , h(n T , k) ; w 2 → n T , h(n T , k ) }; and • Φ same = {w 1 → n T , h(n T , k) ; w 2 → n T , h(n T , k) }.
We have that Φ diff ∼ s Φ same . Intuitively, an attacker cannot distinguish two outputs from the same tag from two outputs performed by different tags.

We then extend the notion of equivalence to traces as follows: given two execution traces T and T leading respectively to configurations K = (P; Φ; S; i) and K = (P ; Φ ; S ; i ), we write T ∼ = T when i = i , T and T have the same sequence of observables, and Φ ∼ s Φ .

Finally, we define the notion of trace equivalence of two closed processes by considering all their execution traces.

Definition 3: Let P and P be two closed processes. We say that P and P are in trace equivalence, written P ≈ t P , when, for any execution trace T ∈ traces(P ), there exists T ∈ traces(P ) such that T ∼ = T , and conversely.

We rely on this notion of trace equivalence to model unlinkability following the definition originally proposed in [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF] and used in [START_REF] Filimonov | Breaking unlinkability of the ICAO 9303 standard for e-passports using bisimilarity[END_REF], [START_REF] Horne | Unlinkability of an improved key agreement protocol for EMV 2nd gen payments[END_REF] relying on a notion of equivalence stronger than the notion of trace equivalence. Actually, the notion of unlinkability we consider here is exactly the one studied in [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF]. The purpose of this work is not to provide a discussion on how to model unlinkability but to show how to overcome the limitations of the existing tools such ProVerif and Tamarin, and to show how to automate proofs of unlinkability in ProVerif relying on some recent advanced features added into the tool. Therefore, we simply illustrate the definition we will use here on the Basic Hash example.

Example 5: Going back to our running example, unlinkability will be modelled as the following equivalence:

P BH ? ≈ t (0 : ! new k; insert keys(k); 1 : P T ) | (1 : ! P R )
This equivalence states that an attacker cannot distinguish the situation where many tags play multiple sessions from the situation where each tag can play only once. Note that the replication ! in front of process P T has been removed on the right hand side of the equivalence.

Tools like Tamarin or ProVerif cannot currently prove this equivalence, as observed in [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF]. We explain how ProVerif works and why it fails on our example in Section III. We then describe our approach to solve this issue in Section IV.

III. PROVING EQUIVALENCES USING PROVERIF

ProVerif can prove an equivalence between two processes P and Q that differ only by the terms and expressions they contain. In Section III-A, we explain this notion of bi-processes, and the notion of diff-equivalence that ProVerif considers. Then, we describe some features that have been recently introduced in ProVerif [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF] and on which our approach will rely.

A. Bi-processes and diff-equivalence

Two processes that only differ by terms and expressions can be given by a single process in which the special function symbol diff[•, •] is used. Intuitively, the first argument corresponds to the term used in the first process, whereas the second one is the term used in the second process. More formally, the grammar we consider for bi-processes is the same as the one introduced previously with the addition of diff[M, M ] for terms and the systematic use of diff[x, y] for variable bindings in let, get, and input commands. For instance an input biprocess is of the form in(c, diff[x, y]); P . The latter addition means that we do not consider ProVerif's standard bi-processes but their extension allowed by the allowDiffPatterns option.

When P is a bi-process we define fst(P ) as the process obtained by replacing any subterm diff[M, M ] by M in P . We define similarly fst(M ) when M is a bi-term, and define symmetrically snd(P ) and snd(M ). ProVerif's standard biprocesses, without diff operators on variable bindings, can equivalently be characterised in our setting as separated biprocesses. To formally define this notion, we assume given a partition X = X L X R for variables. Definition 4: A bi-process B is separated when its variable bindings are of the form diff[x L , x R ] with x L ∈ X L and x R ∈ X R , and all (bi)terms M occurring in B are such that vars(fst(M )) ⊆ X L and vars(snd(M )) ⊆ X R .

When a closed bi-process P is separated, fst(P ) and snd(P ) are closed processes too.

Example 6:

Let B = in(c, diff[x L , x R ]); out(c, x L , x R ).
We have that B is a closed bi-process since the variables x L and x R are bound by the input construct, but it is not separated. Indeed, we have that M = x L , x R occurs in B, and vars(fst

(M )) = vars(snd(M )) = {x L , x R }. Thus, we have neither vars(fst(M )) ⊆ X L nor vars(snd(M )) ⊆ X R . Moreover, fst(B) = in(c, x L ); out(c, x L , x R ) is not closed. Note that snd(B) is not closed as well.
The semantics of bi-processes is defined by a labelled transition system over bi-configurations of the form (P; Φ; S; i) where:

• P is a multiset of closed bi-processes,

• Φ is a substitution mapping variables to bi-terms called a bi-frame, • S is a bi-store, i.e. a set of items of the form tbl (M )

where tbl is a table identifier and M is a bi-term, and • i is an integer. This transition system over bi-configurations is actually an adaptation of the transition system for regular configurations. Some rules are given in Figure 3. When Φ is a bi-frame, we write Φ fst for the frame of domain dom(Φ) such that Φ fst (w) = fst(Φ(w)). For a bi-store S, we define S fst = {tbl (fst(M )) | tbl (M ) ∈ S}. We define similarly Φ snd and S snd . Note that, in this semantics, both sides of the biprocess have to progress in the same way. For instance, when executing a let instruction, the left and right processes have to progress in the same branch. When executing a get instruction, the left and right processes have to execute the same branch when they access to the same element.

For separated bi-processes, (P; Φ; S; i) -→ b (P ; Φ ; S ; i) implies (fst(P); Φ fst ; S fst ; i) -→ (fst(P ); Φ fst ; S fst ; i) and similarly for the second projection. This does not hold in general and, as illustrated by Example 6, it may not even make sense as the projections are not necessarily closed processes.

An execution trace of a bi-process is called a bi-execution trace. Given a bi-execution

T = K 0 1 -→ b K 1 2 -→ b . . . n -→ b K n
and an integer 0 ≤ j ≤ n, we denote by T [j] the biconfiguration at step j. As for processes, we may simply write B for the bi-configuration ({0 : B}; ∅; ∅; 0). The notion of convergence defined next captures the fact that the left and right processes always agree along a trace, in the sense that one of the above rules is always applicable unless both sides of the bi-process are blocked.

Definition 5: A bi-execution trace T converges, denoted T ↓↑, when for all steps j, T [j] = K = (P; Φ; S; i) implies:

1) if

(i : get tbl (diff[x L , x R ]) st. D in P else Q) ∈ P
then for all tbl (M ) ∈ S, we have that:

fst(D){x L → fst(M ), x R → snd(M )}⇓ = E true if, and only if, IN b ({i : in(c, diff[x L , x R ]); P } P; Φ; S; i) in(c,R) ----→ ({i : P {x L → M, x R → M }} P; Φ; S; i) if c ∈ C pub and RΦ fst ⇓ = E M and RΦ snd ⇓ = E M IO b ({i : in(c, diff[x L , x R ]); P } {i : out(c, M ); Q} P; Φ; S; i) τ -→ ({i : P {x L → fst(M ), x R → snd(M )}} {i : Q} P; Φ; S; i) if c ∈ C priv LET-THEN b ({i :let diff[x L , x R ] = D in P else Q} P; Φ; S; i) τ -→ b ({i :P {x L → fst(D)⇓, x R → snd(D)⇓}} P; Φ; S; i) LET-ELSE b ({i :let diff[x L , x R ] = D in P else Q} P; Φ; S; i) τ -→ b ({i :Q} P; Φ; S; i) if fst(D) ⇓ and snd(D) ⇓ GET-THEN b ({i :get tbl (diff[x L , x R ]) st. D in P else Q} P; Φ; S; i) τ -→ b ({i :P {x L → fst(M ), x R → snd(M )}} P; Φ; S; i) if there exists tbl (M ) ∈ S such that fst(D){x L → fst(M ), x R → snd(M )}⇓ = E true and snd(D){x L → fst(M ), x R → snd(M )}⇓ = E true GET-ELSE b ({i :get tbl (diff[x L , x R ]) st. D in P else Q} P; Φ; S; i) τ -→ b ({i :Q} P; Φ; S; i) if for all tbl (M ) ∈ S, fst(D){x L → fst(M ), x R → snd(M )} does not evaluate to true and snd(D){x L → fst(M ), x R → snd(M )} does not evaluate to true Fig. 3. Semantics for bi-processes snd(D){x L → fst(M ), x R → snd(M )}⇓ = E true; 2) (i :let diff[x L , x R ] = D in P else Q) ∈ P then fst(D) evaluates if, and only if, snd(D) evaluates; 3) fst(Φ) ∼ s snd(Φ).
We naturally extend this notion to sets of bi-traces: T ↓↑ if, and only if, T ↓↑ for all T ∈ T . We finally say that diffequivalence holds for a bi-process B when traces(B)↓↑.

In [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF], Blanchet et al. proved an important result for separated bi-processes: if traces(B) converges, i.e. traces(B)↓↑, then fst(B) is observationally equivalent to snd(B). In short, and because observational equivalence implies trace equivalence [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF], we have: if B is separated and traces(B)↓↑ then fst(B) ≈ t snd(B)

Example 7: Going back to our running example, we form the bi-process

B BH = (0 : ! new k L ; ! new k R ; insert keys(diff[k L , k R ]); 1 : B T ) | (1 : ! B R )
where

B T = P T {k → diff[k L , k R ]}, and B R is obtained from P R by changing x (resp. y) into diff[x L , x R ] (resp. diff[y L , y R ])
. This is a separated bi-process. We can recognise the two processes compared in Example 5 as the projections of our bi-process. Indeed, when considering the first projection fst(B BH ), and after having removed the name k R that is not used in the projected process, we get

(0 : ! new k L ; !insert keys(k L ); 1 : fst(B T )) | (1 : ! fst(B R )).
which corresponds to P BH in Example 3 (note that fst(B T ) =

P T {k → k L } and fst(B R ) = P R {k → k R }).
The unique difference is that the replication command is executed before the table insertion instead of before the process P T . This has no significant impact; there will just be many instances of the same key k L in the table. Similarly, when considering the second projection snd(B BH ), and after having removed the unused name k L , we get

(0 : ! ! new k R ; insert keys(k R ); 1 : snd(B T )) | (1 : ! snd(B R ))
which corresponds to the right-hand side process in Example 5. Semantically, the two consecutive replication operators are indeed equivalent to a single one.

In conclusion we have that fst(B BH ) represents the situation with multiple tags playing multiple sessions, while snd(B BH ) represents tags that play only once.

Unfortunately, the set traces(B BH ) of bi-execution traces is not convergent. Indeed, as explained in [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF], starting from B BH , we can reach a bi-configuration (P; Φ; S; i) such that P contains the bi-process

1 : get keys(diff[y L , y R ]) st. Dσ in . . . else . . .
where:

• σ = {x L → fst(M ), x R → snd(M )}, • M = n T , h(n T , diff[k L , k R 1 ]
) , and

• keys(diff[k L , k R 1 ]), keys(diff[k L , k R 2 ]) ∈ S. Considering the element keys(diff[k L , k R 2 ]
) ∈ S, we can see that item 1 of Definition 5 is not satisfied.

Although Tamarin relies on a different approach to establish equivalences, a similar encoding adapted to the syntax of Tamarin will lead to the exact same issue (see file BasicHash-Tamarin.spthy in our repository).

B. Analysing bi-processes with restrictions, lemmas and axioms

An extension of ProVerif with restrictions, lemmas, and axioms has recently been introduced [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF]. We will see that these features (especially axioms) are actually useful to establish unlinkability.

We consider formulas and correspondence queries given by the grammar below, where e, e 1 , . . . , e n are events and M , N are (constructor) terms without diff operators:

ψ, ψ := true | false | event(e) | M = N | M = N | ψ ∧ ψ | ψ ∨ ψ ρ := event(e 1 ) ∧ . . . ∧ event(e n ) ⇒ ψ
Intuitively, a trace T satisfies the correspondence query ρ (noted T ρ) if whenever T contains instances of event(e i ) at τ i for each 1 ≤ i ≤ n, then T also satisfies ψ (for some instantiation of the variables that occur in ψ but not in the e i ) where each event in ψ is found in T at some step τ that occurs before some τ i . A closed process P satisfies ρ when T ρ for any T ∈ traces(P ).

This notion of correspondence queries is extended straightforwardly to bi-execution traces by considering that events contain bi-terms. The formal definition of satisfaction is actually the same as the one given above. We want to emphasise that this formal definition is different from the more natural one that would consist in checking satisfaction of each projection of the bi-restriction by the corresponding projection of the bi-trace. We first illustrate this on an example, and we will come back to this point in Section III-C.

Example 8: Consider the following bi-process B:

! new k L ; new k R ; ! new sid; event(e(sid, diff[k L , k R ])); out(c, diff[k L , k R ]).
Let ρ 2 be the following correspondence query:

event(e(diff[x 1 , x 2 ], diff[y 1 , y 2 ])) ∧ event(e(diff[x 1 , x 2 ], diff[y 1 , y 2 ])) ⇒ x 2 = x 2
We have that traces(B) ρ 2 . Indeed, consider

T = event(e(sid 1 , diff[k L , k R ])); event(e(sid 2 , diff[k L , k R ])).
We have that T ∈ traces(B) and T ρ 2 as sid 1 = sid 2 .

Correspondence queries may be used in several ways in the verification of a bi-process. We call restriction a correspondence query that is going to be used to restrict the set of bi-execution traces that we want to consider. We call axiom a correspondence query that holds for all bi-execution traces, and we call it a lemma when this fact should be verified by ProVerif instead of just being assumed. The next theorem sums up what it means to verify a bi-process in presence of axioms, lemmas and restrictions using ProVerif's semidecision procedure prove for equivalence queries -axioms and lemmas are similarly handled in this theorem, but in practice axioms would be trusted while lemmas would be verified.

Given a closed bi-process B and a set of restrictions R, we note traces R (B) = traces(B) ∩ {T | T ρ, ∀ρ ∈ R}. Moreover, we note fst(R) = {fst(ρ) | ρ ∈ R} and snd(R) = {snd(ρ) | ρ ∈ R}.

Example 9: Going back to Example 8, we have that:

fst(ρ 2 ) = event(e(x 1 , y 1 )) ∧ event(e(x 1 , y 1 )) ⇒ x 2 = x 2 snd(ρ 2 ) = event(e(x 2 , y 2 )) ∧ event(e(x 2 , y 2 )) ⇒ x 2 = x 2
It is important to note that we have snd(T ) snd(ρ 2 ) as expected but fst(T ) fst(ρ 2 ). Indeed, according to ProVerif semantics, variables that appear on the conclusion of a query (or lemma and restriction) and that are not introduced in its premises, are existentially quantified. This means that fst(ρ 2 ) is satisfied by any trace. We wanted to point out this (maybe unexpected) semantics feature of ProVerif to ease the understanding of some examples.

Theorem 1 ( [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF]): Let B be a closed bi-process, Ax, L, R be respectively sets of axioms, lemmas, and restrictions. If

• for all ∈ Ax ∪ L, we have that traces R (B)

; and • prove (B, Ax, L, R) returns true then traces R (B)↓↑.

This result has been stated and proved in [10, Theorem 1] for separated bi-processes only. We are confident that it remains true for the more general bi-processes that we obtain after the transformations presented in this paper. To justify this claim, it is not feasible to adapt the proofs of the technical report associated to [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF], which rely on a complex technical condition (called well-origination) that cannot be adapted without changing large proofs involving the inner workings of ProVerif's saturation procedure. However, the authors of [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF] have indicated in personal communication that they hope to lift these conditions completely in order to obtain results that would be easier to reuse in future developments, but also to justify some recent features of ProVerif that would, in turn, make it easy to justify the soundness of the verification procedure on our extended bi-processes. More details are available in appendix A.

Without restrictions and when B is separated, the conclusion of Theorem 1 could be fst(B) ≈ t snd(B). However, as already noted in [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF], with restrictions, it does not directly show trace equivalence (or observational equivalence) for traces satisfying their respective restrictions (obtained through projections). We illustrate this observation below through an example.

Example 10: Going back to our running example, a natural way to encode unlinkability would be to consider the (bi)process P BH as described in Example 3, and use a restriction to discard some traces on the right-hand side, enforcing that each tag executes only once. Applying this idea on the toy example developed in Example 8, we will consider the restriction ρ 2 which says that if two sessions of the same tag occur in a trace (on the right side of the bi-process), then this should be the same session. This is ensured by requiring that the session ids are the same, i.e. x 2 = x 2 .

When analysing an equivalence property, a restriction in ProVerif has to be seen as a bi-restriction, and will discard bi-traces. Therefore, such a restriction will also discard some behaviours on the left-hand side. Thus, our example restriction ρ 2 actually does not encode the unlinkability property we want: Considering the process B given in Example 8, it is relatively easy to see that traces(B)↓↑ (both sides of the bi-process are equal up to a renaming). Thus, we also have convergence for the restricted set of bi-traces, i.e. traces ρ2 (B)↓↑ while our process clearly does not satisfy unlinkability.

Regarding Tamarin, restrictions and lemmas are something that have been available for quite a long time. However, the soundness of the tool in presence of restrictions for equivalence properties has only been established recently [START_REF] Paradzik | Conditional observational equivalence and off-line guessing attacks in multiset rewriting[END_REF], and only for a specific type of restrictions which are actually not sufficient to write the restriction ρ 2 mentioned above.

C. Trace equivalence in presence of restrictions

In presence of restrictions, and when B is separated, we would like to be able to establish that traces R (B)↓↑ implies trace equivalence between fst(B) and snd(B) for traces satisfying their respective restrictions, i.e. traces fst(R) (fst(B)) ≈ t traces snd(R) (snd(B)).

We first illustrate through examples why such a result does not hold in general.

Example 11: Consider the following bi-process

B = event(e(diff[ok L , ok R ])); out(c, diff[bad L , bad R ])
and the restriction

ρ = event(e(diff[x L , x R ])) ⇒ x L = x R .
We have that traces ρ (B) contains only the empty bi-trace. However, fst(ρ) def = event(e(x L )) ⇒ x L = x R will not discard any traces on fst(B): recall that x R is quantified existentially because it only occurs in the conclusion of the clause. The same goes for snd(ρ) and snd(B). Therefore, we have that:

traces fst(ρ) (fst(B)) ≈ t traces snd(ρ) (snd(B))
Note that the restriction ρ applies in a symmetric way on fst(B) and snd(B) (a variable occurring free on the right, as x R , being quantified existentially). The issue here comes from the fact that this restriction discards more traces when considering the bi-process than its two projections individually. Concretely, a non-empty trace tr 1 of fst(B) trivially satisfies the restriction fst(ρ) but cannot be lifted to a bi-trace of B that satisfies ρ, i.e. there is no bi-trace tr ∈ traces ρ (B) such that fst(tr) = tr 1 . The same issue holds for traces of snd(B).

Example 12: Consider the bi-process

B = event(e(diff[ok L , ok R ], ok)); out(c, ok)
and the following restriction:

event(e(diff[ok R , ok R ], diff[x, x])) ⇒ x = ok
This restriction ρ will not discard any trace from traces(B) as any event e occurring in traces(B) will not have diff[ok R , ok R ] as first argument. Thus, we have that traces ρ (B)↓↑, and it is possible to lift any trace possible on the left to a bi-trace T satisfying the bi-restrictions. However, it is easy to see that the bi-trace

T = event(e(diff[ok L , ok R ], ok)); out(c, ok)
is such that snd(T ) snd(ρ), whereas fst(T ) fst(ρ), thus we have that:

traces fst(ρ) (fst(B)) ≈ t traces snd(ρ) (snd(B))
In the remaining of this section, we establish the expected result (see Proposition 1) for the class of restrictions that are diff-safe. First, as shown in Example 11, it is important to be able to lift a trace from the left-hand side and satisfying fst(R) to a bi-trace in traces R (B). Second, as shown in Example 12, we have also to ensure that this bi-trace will satisfy the restrictions on the right. This leads us to consider the following definition.

Definition 6: Let R be a set of bi-restrictions, and B a separated closed bi-process. We say that R is diff-safe w.r.t. B if for all T fst ∈ traces fst(R) (fst(B)), there exists T ∈ traces R (B) such that fst(T ) ∼ = T fst , and snd(T ) snd(ρ) for all ρ ∈ R, and conversely for traces in traces snd(R) (snd(B)).

We establish the following result. Proposition 1: Let B be a separated closed bi-process, and R be a set of restrictions that is diff-safe. If traces R (B)↓↑ then traces fst(R) (fst(B)) ≈ t traces snd(R) (snd(B)).

Proof. We establish the result for one direction. The other one can be obtained in a similar way. Let T fst ∈ traces fst(R) (fst(B)). We have to establish the existence of T snd ∈ traces snd(R) (snd(B)) such that T fst ∼ = T snd .

By definition of diff-safe, we know that there exits T ∈ traces R (B) such that fst(T ) = T fst and snd(T ) snd(ρ) for all ρ ∈ R. Relying on the fact that traces R (B)↓↑, we deduce that fst(T ) ∼ = snd(T ). As T ∈ traces R (B), we know that snd(T ) ∈ traces(snd(B)), and since snd(T ) snd(ρ) for all ρ ∈ R, we deduce that snd(T ) ∈ traces snd(R) (snd(B)).

Deciding whether a set of restrictions is diff-safe is not an easy task. As a stepping stone towards a syntactic sufficient condition, we propose in the next lemma a useful characterisation that is used later on to identify some classes of birestrictions which are diff-safe.

Lemma 1: Let R be a set of bi-restrictions, and B be a separated closed bi-process such that traces R (B)↓↑, and such that for any ρ ∈ R and T ∈ traces(B), we have:

T ρ ⇔ fst(T ) fst(ρ) ⇔ snd(T ) snd(ρ)
We have that R is diff-safe w.r.t. B.

Proof. Let T fst ∈ traces fst(R) (fst(B)). We have to establish that there exists T ∈ traces R (B) such that fst(T ) ∼ = T fst , and snd(T ) snd(ρ) for all ρ ∈ R. We show this result by induction on the length of T fst . First, the result trivially holds for a trace of length 0. We now assume that T fst = T fst • α. Because the restriction satisfaction relation is prefix closed, i.e. T fst ρ implies T fst ρ, we have that T fst ∈ traces fst(R) (fst(B)). Applying the induction hypothesis, we deduce that there exists T ∈ traces R (B) such that fst(T ) ∼ = T fst , and snd(T ) snd(ρ) for all ρ ∈ R. We know that T ∈ traces(B), and we distinguish two cases:

• We have that there exists β such that T = T .β ∈ traces(B) with fst(β) = α. In such a case, relying on our hypothesis, and since fst(T ) fst(ρ) for all ρ ∈ R, we deduce that T ρ for all ρ ∈ R, and therefore T ∈ traces R (B). We have also that fst(T ) ∼ = T fst , and snd(T ) snd(ρ) relying on our hypothesis. This allows us to conclude.

• We have that there does not exist β such that T = T .β ∈ traces(B) and fst(β) = α meaning that T ∈ traces R (B) diverges which is not possible by hypothesis. This concludes the proof of the first direction, and the other direction can be done in a similar way.

Example 13: Going back to Example 8, the restriction ρ 2 does not satisfy the criterion given in Lemma 1. It is indeed easy to see that for some T ∈ traces(B), fst(T ) will satisfy fst(ρ 2 ) whereas snd(T ) will not satisfied snd(ρ 2 ). Actually, ρ 2 is not diff-safe. Consider the following bi-trace:

T = event(e(sid 1 , diff[k L , k R ])); out(c, diff[k L , k R ]); event(e(sid 2 , diff[k L , k R ])); out(c, diff[k L , k R ])
We have that T fst ∈ traces fst(ρ2) (B). The only bi-trace T 0 such that T 0 ∈ traces ρ2 (B) with fst(T 0 ) ∼ = T fst is actually T . However, it happens that snd(T ) ρ 2 .

In ProVerif, restrictions are actually bi-restrictions, and as we have seen in Proposition 1, a link between bi-restrictions and their projections has to be established to get the expected equivalence, i.e.

traces fst(R) (fst(B)) ≈ t traces snd(R) (snd(B)).
This way of considering restrictions (i.e. referring to their projections) is more in line with what is done in Tamarin. Even if restrictions have been available for quite a long time in Tamarin, the soundness of the procedure in presence of restrictions has only been established recently, and for Type-0 restrictions only [START_REF] Paradzik | Conditional observational equivalence and off-line guessing attacks in multiset rewriting[END_REF]. Intuitively, a Type-0 restriction is a Tamarin restriction that can be written relying solely on facts of arity 0. The idea behind this condition is to ensure that a restriction will apply in a symmetric way on both sides (on the dependency graph and also on its mirror). It may seem quite restrictive. However, it is important to note that, in Tamarin, any fact has a timestamp embedded in it. Therefore, Type-0 restrictions are expressive enough to enforce protocol phases or to model the fact that a certain action occurs only once:

OnlyOnce()@#i & OnlyOnce()@#j ⇒ #i = #j
Restrictions having a similar effect can also be written in ProVerif but restrictions with events of arity 0 are not sufficient for that.

Example 14: Let B be a bi-process (with no replication) containing several actions, e.g. out(c 1 , u 1 ), . . . , out(c n , u n ), and assume that we want to consider traces where at most one of these outputs is executed. The idea is to add new sid; event(OnlyOnce(sid)) before each output, and to consider the following restriction:

event(OnlyOnce(diff[x, x])) ∧ event(OnlyOnce(diff[y, y])) ⇒ x = y
It is easy to see that such a restriction ρ satisfies the hypothesis given in Lemma 1, and is thus diff-safe, allowing one to derive the expected result, i.e. traces ρ (B)↓↑ implies that traces fst(ρ) (fst(B)) ≈ t traces snd(ρ) (snd(B)). In other words, we get the soundness of ProVerif considering a more natural semantics for restrictions (we consider their respective projections).

Relying on diff-safe restrictions (or even simply the characterisation given in Lemma 1), we can also encode protocol phases (which is already a built-in mechanism in ProVerif). We believe that the criterion we provide with Lemma 1 to characterise diff-safe restrictions can be seen as the ProVerif counterpart of Type-0 restriction in the Tamarin setting. Thus, as done in [START_REF] Paradzik | Conditional observational equivalence and off-line guessing attacks in multiset rewriting[END_REF] for Tamarin, we have also established the soundness of ProVerif w.r.t. diff-safe restrictions considering a more natural semantics for restrictions. Indeed, for this class of bi-restrictions, we can reason on their projections avoiding the issues mentioned in Examples 11 and 12.

However, the class of diff-safe restrictions is too restrictive to encode unlinkability as done e.g. in Example 10 (see Example 13). We thus develop another approach in the following section using the allowDiffPatterns option and axioms of ProVerif.

IV. OUR APPROACH

As we have seen in Example 7, ProVerif is not able to conclude on the bi-process modelling our unlinkability property on the Basic Hash protocol, and diff-safe restrictions are too restrictive to encode this property. We thus propose another approach. We propose to transform such bi-processes so that diff-equivalence may be achieved (and verified with ProVerif) on the transformed bi-processes, and that this diffequivalence implies trace equivalence for the original process. We proceed in two steps:

1) We duplicate the get instructions to dissociate the process of the left and the one on the right. 2) We add some axioms to help ProVerif to reason on our bi-process. These axioms are used to improve the accuracy of the verification procedure by avoiding overapproximations. Before formally defining these two steps in Sections IV-B and IV-C, we illustrate the approach on our running example.

A. Going back to our running example On our running example, our transformations will only change the bi-process modelling the reader since it is the only one that features a get instruction. Instead of performing a get instruction to access one (bi)record in the keys table, it will perform two get instructions in a row to access two records in the keys table. This will allow one to choose two different records: one for the left and one for the right. Of course, the test performed remains the same and has to be satisfied by the element chosen on the left, and the one chosen on the right. We show the transformed bi-process in Figure 4, where the symbol _ represents irrelevant names for variables or public channels, and bad L and bad R are distinct public constants. The reader can ignore the added events at this stage. This transformation alone is not enough to allow ProVerif to conclude. We thus add some axioms that emphasise some properties that are necessarily satisfied, to make sure that these properties are not lost in the over-approximations performed in ProVerif's verification procedure. To this end, we make use of the three events introduced in the transformed bi-process: Inserted, FailL, and FailR. The first one indicates when an element is inserted in the table keys, whereas the two others will be used to track the outcome of lookups in that table: FailL indicates a failure of the get instruction regarding the left hand side of the process, whereas FailR indicates a failure of the get instruction w.r.t. the right process. Relying on these events, we state two axioms given in Figure 4.

Let us focus on the first one. In case the FailL event is executed with a value M , it means that there is no entry diff[N, N ] in the table allowing one to evaluate the expression eq(proj 2 (M ), h(proj 1 (M ), N )) to true. Otherwise, we should have chosen this entry to execute the then branch. Thus, it is safe to say that for any entry diff[N, N ] in the table keys, we have proj 2 (M ) = h(proj 1 (M ), N ). The same applies on the right. We may note that such an axiom is indeed satisfied since we know that insertions in the table can be done at the very beginning of the execution traces. This means that the element allowing one to perform the reasoning above can be assumed to be present before the execution of the FailL or FailR event. The validity of the axioms added by our transformation will be a consequence of Proposition 2.

B. Desynchronising the two parts of the bi-process

We now define the first step of the transformation informally described above.

Definition 7: Let B be a separated bi-process. We define T 1 (B) as follows:

• T 1 (get tbl (diff[x L , x R ]) st. D in B then else B else ) is
the following bi-process, where _ represents irrelevant names for variables or public channels, and bad = diff[bad L , bad R ] for two arbitrary distinct public constants bad L and bad R :

get tbl (diff[x L , _]) st. fst(D) in get tbl (diff[_, x R ]) st. snd(D) in T 1 (B then ) else out(_, bad) else get tbl (diff[_, x R ]) st. snd(D) in out(_, bad) else T 1 (B else )
• The transformation is homomorphic in all other cases: for instance, we define:

-T 1 (out(c, M ); B ) = out(c, M ); T 1 (B ), and -T 1 (in(c, diff[x L , x R ]); B ) = in(c, diff[x L , x R ]); T 1 (B ).
Note that, because B is separated, fst(D) cannot have x R as a free variable, which would render the above transformation semantically dubious. In the above definition, when fst(D) and snd(D) disagree, we use the bi-process out(_, diff[bad L , bad R ]) to signal that we want diffequivalence to fail. To conclude in more cases, a variant could slightly relax this, under the assumption that B then and B else have the same structure. We do not encounter this situation in our case studies, and we left this extension as future work.

We establish the following result so that the "equivalence is true" returned by ProVerif on T 1 (B 0 ) will allow one to conclude that trace equivalence holds between the two projections of B 0 , and thus our unlinkability property holds.

Theorem 2: Let B 0 be a separated closed bi-process such that T 1 (B 0 )↓↑. We have that fst(B 0 ) ≈ t snd(B 0 ). This theorem will be proved relying on two lemmas that we now introduce. In these lemmas, when T is a bi-execution trace of T 1 (B 0 ), we allow ourselves to write fst(T ) meaning that the first projection has been applied on each configuration of T . Note that this does not imply that fst(T ) is an execution of fst(T 1 (B 0 )) as T 1 (B 0 ) is not separated. Actually, we only use fst(T ) to assess its indistinguishability w.r,t. another trace (e.g., in T fst ∼ = fst(T )): we thus only care about the observables, and the first projection of the last frame of T . Since T 1 (B 0 ) duplicates the get instruction, to establish the connection between fst(B 0 ) and T 1 (B 0 ), it is easier to consider a notion of execution trace where the two get instructions corresponding to the same get instruction in the original bi-process B 0 are triggered in a row. We denote traces this notion of bi-execution trace.

Lemma 2: Let B 0 be a separated closed bi-process such that T 1 (B 0 )↓↑, and T fst ∈ traces(fst(B 0 )). There exists T ∈ traces(T 1 (B 0 )) such that T fst ∼ = fst(T ). A similar result holds for snd.

Proof. (Sketch) We will find T such that fst(T ) and T fst differ only on the duplicated τ actions corresponding to transformed get operations. Although the lemma is stated in terms of static equivalence, frames are actually equal. The convergence hypothesis guarantees that we avoid diff[bad L , bad R ] which can artificially appear in the traces of the transformed bi-process. Let B 0 be a separated closed bi-process such that T 1 (B 0 )↓↑, and T ∈ traces(T 1 (B 0 )). There exists T fst ∈ traces(fst(B 0 )) such that T fst ∼ = fst(T ). A similar result holds for snd.

in(c, diff[x L , x R ]); get keys(diff[y L , _]) st. eq(proj 2 (x L ), h(proj 1 (x L , y L ))) in get keys(diff[_, y R ]) st. eq(proj 2 (x R ), h(proj 1 (x R , y R ))) in out(c, ok) else event(FailR(x R )); out(_, diff[bad L , bad R ]) else event(FailL(x L )); get keys(diff[_, y R ]) st. eq(proj 2 (x R ), h(proj 1 (x R , y R ))) in out(_, diff[bad L , bad R ]) else out(c, error) event(FailL(x L )) ∧ event(Inserted(diff[y L , y R ])) ⇒ proj 2 (x L ) = h(proj 1 (x L ), y L ) event(FailR(x R )) ∧ event(Inserted(diff[y L , y R ])) ⇒ proj 2 (x R ) = h(proj 1 (x R ), y R )
Proof. (Sketch) The projected traces are simply obtained by de-duplicating the τ actions corresponding to get subprocesses. Again, the convergence hypothesis guarantees that we avoid diff[bad L , bad R ].

C. Refining the analysis in failure branches

We transform a model, i.e. a bi-process together with restrictions, axioms and lemmas, to a new model that is easier to verify by ProVerif. We first illustrate this transformation on a very simple toy example. On this simple example, ProVerif returns "observational equivalence cannot be proved", whereas it is relatively easy to see that the else branch cannot be taken (as there is an element in the table), and thus equivalence holds. Applying the transformation that we will formally present next will lead to the following bi-process:

event(Inserted(ok)); insert tbl (ok); get tbl (x) st. true in out(c, ok) else event(Fail()); out(c, diff[ok L , ok R ])
together with the following axiom:

event(Fail()) ∧ event(Inserted(diff[y L , y R ])) ⇒ false.
On this model, ProVerif is able to conclude that equivalence holds.

We now formally define this transformation.

Definition 8: We have that

(B, R, Ax, L) else (B , R, Ax ∪ {ax}, L)
when there exist a context C, two terms M 1 and M 2 without diff operators, and two processes P and Q such that:

• B is of the form:

C[get tbl (diff[x L , x R ]) st. eq(M 1 , M 2 ) in P else Q] • B is of the form: C[get tbl (diff[x L , x R ])st. eq(M 1 , M 2 ) in P else event(Fail( n, y)).Q]
where n = names({M 1 , M 2 }), y = vars({M 1 , M 2 }) \ {x L , x R }, and all operations insert tbl (M ) have been replaced by event(Inserted(M )).insert tbl (M ) • ax is of the form:

event(Fail( z, y)) ∧ event(Inserted(diff[x L , x R ])) ⇒ (M 1 = M 2 ){ n → z}
where Fail and Inserted are distinct events that do not occur in (B, R, Ax, L), and z is a vector of fresh variables of the same length as n.

Intuitively, the transformation instruments the process with events in order to express, in the added axiom, that we can only execute the else branch of the bi-process if no value inserted in tbl satisfies M 1 = M 2 . This makes sense even if x L and x R do not occur in eq(M 1 , M 2 ): in that case we are simply saying that we can only visit the else branch if either eq(M 1 , M 2 ) is false, or no value has even been inserted in the table.

The above intuition is not entirely exact, though. Indeed, the semantics of the axiom is that if at some point in the trace the events Fail and Inserted have happened (for some values of the free variables z, y, x L , x R ), then eq(M 1 , M 2 ) evaluates to true. The semantics of bi-processes enforces a weaker version of this statement, where the Inserted must happen before Fail. It is not possible to express such precise temporal properties in axioms with ProVerif but, as we shall see, we can live with this limitation.

The transformation can be iterated. Obviously, the insert events of several transformations relying on the same table can be merged. We justify next a single step of the transformation; the result extends naturally for iterations.

Proposition 2: Let (B, R, Ax, L), and (B , R, Ax , L) be two models such that (B, R, Ax, L) else (B , R, Ax , L). We have that Ax = Ax ∪ {ax} for some ax. Assuming that all insert instructions are performed in a phase that precedes the phase of the modified get instruction, we have:

traces R (B ) ax
Proof. Consider a bi-trace T ∈ traces R (B ), and assume that T ax. Then, for some substitution θ, we have Inserted(diff[x L , x R ])θ in the bi-trace, as well as Fail( z, y)θ, and (M 1 = E M 2 ){ n → z}θ is true. In other words, the execution of the get action, for the values given by θ, has stepped to the else branch, when there existed a bi-term diff[x L , x R ]θ in the table that satisfies the condition. This contradicts the semantics of bi-processes.

This result, together with Theorem 2 and Theorem 1, shows that if ProVerif concludes on the transformed model, then trace equivalence holds for the original one. More precisely, we have the following result.

Theorem 3: Let (B 0 , ∅, Ax, L) be a separated ProVerif model, and (B , ∅, Ax , L) be the model obtained after applying our two transformation, i.e. a model such that (T 1 (B 0 ), ∅, Ax, L) * else (B , ∅, Ax , L). Moreover, we assume that:

• for all ∈ Ax, we have that traces(B 0 ) ; • for all ∈ Ax, we have that traces(T 1 (B 0 )) ; • all insert instructions in B 0 are performed in a phase that precedes the phase of the get instructions transformed by else above; and • ProVerif establishes equivalence on the resulting model (B , ∅, Ax , L) i.e. returns "diff-equivalence is true" on this model. We conclude that fst(B 0 ) ≈ t snd(B 0 ).

Note that the two first items are there to justify the axioms already present in the original model (not the ones added by our transformation).

Proof. By Proposition 2, we have traces(B ) for any ∈ Ax \ Ax. By hypothesis, we have traces(T 1 (B 0 )) for any ∈ Ax, and this is also true for B since the events inserted in the last transformation are new. Moreover, we have no restriction here. By Theorem 1, we deduce that traces(B )↓↑, and we also have traces(T 1 (B 0 ))↓↑ since B and T 1 (B 0 ) are the same up to some events. We finally obtain fst(B 0 ) ≈ t snd(B 0 ) by Theorem 2.

V. CASE STUDIES

In this section, we explain how our approach can be used to analyse unlinkability on several existing protocols.

A. Implementation

In order to analyse our protocols of interest, we have developed a tool that implements the two transformations described in the previous section. This tool makes it easy to test our approach on various protocols, and avoids mistakes during transformations. It takes as input a ProVerif model containing a bi-process specifying the equivalence to be verified and returns another ProVerif file. If ProVerif concludes that diffequivalence holds on the output file then our result allows one to conclude that the left and right processes written in the input file are in trace equivalence.

In practice, we implemented a ProVerif front-end tool to automatically apply our two transformations (≈ 2k OCaml LoC). It takes as input a description of the protocol as presented in Example 7 and outputs a new ProVerif model in which the two parts of the bi-process have been desynchronised and the axioms corresponding to else branches have been added. ProVerif can then be ran on this transformed model to automatically prove the security of the protocol. The source code of our tool and material to reproduce results can be found at [START_REF] Debant | Proving Unlinkability using ProVerif through Desynchronized Bi-Processes[END_REF]. This includes ProVerif models for our case studies but also the generated files corresponding to their transformations: the reader may thus inspect the effect of our transformation without running our tool.

B. Results

We first study four examples: Basic Hash (used as a running example), Hash-Lock, Feldhofer, and a variant of the LAK protocol (LAK-v1). All these examples are described, e.g., in [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF]. They are similar in the sense that they involve monotonic states, i.e. states that are never updated. On all these examples, it was already well-known that ProVerif is unable to conclude on the model encoding unlinkability relying on standard bi-process and diff-equivalence. Using our tool, we obtain a file on which ProVerif is able to conclude in a few seconds, thus we conclude that these protocols ensure unlinkability by Theorem 3. A detailed description of how our transformations work on the Basic Hash protocol is given in Section IV-A.

We then consider a fixed version of the OSK protocol, described as OSK-v2 in [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF]. The protocol can be described informally as follows:

T → R : g(h(k T )) T updates k T with h(k T )
Here, g and h are two hash functions. Each tag has a secret key k T , whose initial value is stored in the reader's database. The tag updates its key by applying the h function symbol at each session on its current key. The reader expects a message of the form g(h n (x)) for some database entry x (h n means that h is applied n times). This check is modelled relying on a private destructor retrievekey(•) allowing one to extract k from a term of the form h(n, k) used to model h n (k). As usual in ProVerif, we encode the state of the tag using a private channel. To avoid false attacks, we rely on some axioms to improve precision in the manipulation of private channels. This is done following the approach developed in GSVerif [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF] for trace-based properties. Extending the approach of [START_REF] Cheval | A little more conversation, a little less action, a lot more satisfaction: Global states in proverif[END_REF] for equivalence properties is beyond the scope of this paper, but on this particular example, it is easy to be convinced that these axioms are valid, and thus our encoding correct. Despite this and the addition of a lemma to help regarding termination, ProVerif is not able to establish that the equivalence holds. However, ProVerif concludes successfully on the transformed model (produced by our tool) hence unlinkability holds for OSK-v2 by Theorem 3.

C. Comparison with earlier work

In [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF], Baelde et. al. develop an approach to tackle the same class of protocols as the one we consider here, and using the same definition for unlinkability. It is thus natural to compare in more details this work with the present one.

First, we note that all the results presented above are consistent with the security analyses performed in [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF] where unlinkability has been established relying on three sufficient conditions proved using the tool Tamarin.

Second, the verification technique proposed by [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF], based on sufficient conditions, is at a high-level independent of the verification tool, whereas our work is specific to ProVerif. Moreover, the sufficient conditions themselves can provide some insight as to what makes unlinkability hold, or fail.

However, in practice, verifying the sufficient conditions of [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF] has proved very difficult, and the authors of that paper could only obtain semi-automated Tamarin proofs. In general, we thus reckon that this verification technique will require more effort than our direct approach. In each of the case studies of [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF], two different models had to be designed to verify the three sufficient conditions. Each time, several lemmas have to be written corresponding to the various conditions (between two and four depending on the protocol) and, in some cases, several intermediate lemmas are needed to help Tamarin prove the conditions.

In particular, regarding OSK-v2, the security analysis conducted in [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF] has only been possible thanks to several simplifications and using some modelling tricks. For instance, one of the sufficient conditions has been established discarding the reader role, and the attacker was not given the power to apply a hash function on some terms.

Overall, our approach brings an interesting complement to the technique of [START_REF] Baelde | A method for proving unlinkability of stateful protocols[END_REF], which can significantly ease the verification effort when ProVerif is applicable.

VI. CONCLUSION

We have shown that unlinkability can be automatically proved in ProVerif, by applying two generic transformations on the standard bi-process expressing unlinkability. Our approach significantly improves over existing automated proofs, avoiding several over-approximations as well as manual work. It builds on several specific features of ProVerif. In particular, we make crucial use of extended bi-processes with diff operators on bound variables, that have seen only limited use so far (and which would not make sense in e.g. Tamarin). More generally, we make use of the recent addition of axioms, lemmas and restrictions in ProVerif, and we provide a better understanding of how restrictions can be used to prove equivalences.

It would be natural to extend our theoretical development as well as our tool to generalise our second transformation beyond equality tests between constructor terms. To deal with arbitrary terms D, a more involved transformation which essentially consists in computing the variants of an expression to get rid of destructor symbols will be necessary [START_REF] Comon-Lundh | The finite variant property: How to get rid of some algebraic properties[END_REF]. In light of the usefulness and simplicity of our approach, a promising perspective would be to integrate it by default in ProVerif, but this requires the addition of temporal constraints in correspondence queries. Meanwhile, this work introduces a new approach which is not specific to unlinkability. We develop in [START_REF] Debant | Proving Unlinkability using ProVerif through Desynchronized Bi-Processes[END_REF] an example (actually a toy protocol provided in [START_REF] Hirschi | A method for unbounded verification of privacy-type properties[END_REF]) which demonstrates that our approach can be used to prove anonymity properties. We think that a similar approach could have been used in [START_REF] Bhargavan | A symbolic analysis of privacy for tls 1.3 with encrypted client hello[END_REF] to overcome ProVerif limitations when manipulating lookup tables for anonymity properties. It appears as an alternative to the encoding used in [START_REF] Bhargavan | A symbolic analysis of privacy for tls 1.3 with encrypted client hello[END_REF] (and detailed in [START_REF] Bhargavan | Handshake Privacy for TLS 1.3[END_REF] -Section 5.4.3). Their encoding is based on the use of restrictions which have to be manipulated with a lot of care when analysing equivalence-based properties.

Our contribution in this paper, namely relaxing diffequivalence to be able to prove unlinkability in ProVerif, does not address other difficult aspects that might arise in this task. Handling the tag's mutable state in the OSK-v2 case study has proved difficult, but there is hope that advances with GSVerif will soon solve this issue. It is also natural to consider protocols with state updates on the reader's side, i.e. updates of database entries. Although such operations are not directly supported in ProVerif, there is hope to model them naturally enough using restrictions -which calls for a (slight) generalisation of our results. can back-translate this to bi-processes, obtaining for instance a bi-process that is rigorously equivalent to the previous one for ProVerif's translation (and which we make equivalent as a bi-process by providing it with the suitable semantics):

in(c, diff[x L , x R ]); if diff[x L , x R ] = cst then out(c, diff[x L , x R ]) else out(c, m)
More interestingly, we can modify our process to only perform the test on the left projection, as we do in our first transformation:

in(c, diff[x L , x R ]); if x L = cst then out(c, diff[x L , x R ]) else out(c, m)

The generated clauses would now become:

att (cst, x R ) ⇒ att (cst, x R ) att (x L , x R ) ∧ x L = cst ⇒ att (fst(m), snd(m))
Note that the clause deriving bad has disappeared since the test x L = cst cannot succeed on one projection only, since it does not contain diff operators anymore. Also note that the second clause above is simply obtained from the second clause of the first bi-process by dropping the atom corresponding to the right projection of the original conditional.

The fact that [10, Lemma 1] remains true for extended bi-processes simply stems from the fact that the semantics of extended bi-processes (as presented in this paper) are adequately captured by this simple extension of the translation process, which is the one currently implemented in ProVerif. b) Soundness of the saturation procedure: As it is, [10, Theorem 3] relies on the assumption that clauses satisfy a so-called well-origination condition. The condition notably imposes that, if a clause concludes with att (m, n), then the variables in m (resp. n) are introduced in some hypothesis of the clause. The definition is actually unclear in the case of clauses corresponding to biprocesses and, due to the complexity of the proofs, we could not determine how to clarify it.

The authors of [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF] have indicated in personal communication that they expect to lift this technical condition completely in the future, which would almost immediately justify our use of extended biprocesses. Their goal is obviously to clarify and generalise the result, but also to justify an option that is currently available in ProVerif (under the name maxHyps) which allows the saturation procedure to drop hypotheses in large clauses in order to achieve termination more easily. This perspective would provide much more reasonable ways to justify ProVerif's soundness when used on (a class of) nonseparated bi-processes. In fact, the justification of maxHyps would automatically allow the clauses resulting from the biprocesses used in our transformations: as in the example above, our bi-processes only exploit "unilateral conditionals", and their clauses are obtained from the clauses of standard bi-processes by dropping the unwanted projection of some conditionals.

B. Proofs of Section IV

Given a multiset P of bi-processes, we define T 1 (P) the multiset of all transformed elements of P. We extend this notion to bi-configurations as follows: T 1 (K) = (T 1 (P); Φ; S; i) when K = (P; Φ; S; i). Similarly, we extend the notion fst and snd to multiset of processes and to configurations as follows: fst(K) = (fst(P); Φ fst ; S fst ; i) when K = (P; Φ; S; i), and similarly for snd.

Lemma 2: Let B 0 be a separated closed bi-process such that T 1 (B 0 )↓↑, and T fst ∈ traces(fst(B 0 )). There exists T ∈ traces(T 1 (B 0 )) such that T fst ∼ = fst(T ). A similar result holds for snd.

Proof. We prove the result for fst, the case of snd being symmetric. We start by establishing the following claim.

Claim. Let K 0 be a separated bi-configuration, and K = T 1 (K 0 ) such that K↓↑. If fst(K 0 ) α -→ K L for some α and some K L , then there exist a separated bi-configuration K 0 and K such that K ↓↑, K = T 1 (K 0 ), and fst(K 0 ) = K L . Moreover, either this step corresponds to the execution of a get instruction, and we have that α = τ , and K τ τ -→ K (with the execution of two get instructions in a row); otherwise we have that K α -→ K .

Note that the result stated above allows us to prove the statement in the lemma by induction on the length of the execution trace T fst . Now, it remains to establish this claim. We do a case analysis depending on the rule used to perform fst(K 0 ) α -→ K L .

Case IN. In such a case, we have that:

• K 0 = ({i :in(c, diff[x L , x R ]); P } ∪ P; Φ; S; i); • α = in(c, R) for some recipe R such that RΦ fst ⇓ = E M , and RΦ snd ⇓ = E M ; • K L = ({i :fst(P ){x L → M }} ∪ fst(P); Φ fst ; S fst ; i); and • K = T 1 (K 0 ) = ({i :in(c, diff[x L , x R ]); T 1 (P )} ∪ T 1 (P); Φ; S; i). We consider the two following bi-configurations:

• K 0 = ({i :P {x L → M, x R → M }} ∪ P; Φ; S; i); and • K = ({i :T 1 (P ){x L → M, x R → M }} ∪ T 1 (P); Φ; S; i). Since K 0 is separated, we have that K 0 is separated too, and we have that fst(K 0 ) = K L . Relying on the fact that our transformation is compatible with the substitution of difffree terms, i.e., T (Bσ) = T (B)σ for all bi-process B and substitution σ which do not introduce terms with diff operators, we deduce that T 1 (K 0 ) = K . Then, it is easy to see that K in(c,R) ----→ K , and thus K ↓↑.

Most of the cases can be done in a similar way. We focus now on the more interesting cases, i.e. the ones corresponding to get instructions.

Case GET-T. In such a case, we have that α = τ , and:

• K 0 = ({i :get tbl (diff[x L , x R ]) st. D in B then else B else } ∪ P; Φ; S; i);

Fig. 4 .

 4 Fig. 4. Transformed reader bi-process for Basic Hash

Example 15 :

 15 Consider the following bi-process B: insert tbl (ok); get tbl (x) st. true in out(c, ok) else out(c, diff[ok L , ok R ])

  ({i : P {x → M }} P; Φ; S; i) if c ∈ C pub and there exists a recipe R such that RΦ⇓ = E M

	IN ----→ IO ({i : in(c, x); P } P; Φ; S; i) in(c,R) ({i : in(c, x); P } {i : out(c, M ); Q} P; Φ; S; i)
				τ -→ ({i : P {x → M }} {i : Q} P; Φ; S; i) if c ∈ C priv
	INSERT	({i : insert tbl (M ); P } P Φ S; i)	τ -→ ({i : P } P; Φ; S ∪ {tbl (M )}; i)
	GET-THEN ({i : get tbl (x) st. D in P else Q} P; Φ; S; i)	τ -→ ({i : P {x → M }} P; Φ; S; i)
		if there exists M such that tbl (M ) ∈ S, and D{x → M } evaluates to true
	GET-ELSE ({i : get tbl (x) st. D in P else Q} P; Φ, S; i)	τ -→ ({i : Q} P; Φ; S; i)
		if for any M such that tbl (M ) ∈ S, D{x → M } does not evaluate to true
	MOVE	(P; Φ; S; i)	phase (i+1) -------→ (P; Φ; S; i + 1)
	PHASE	({i : i : P } ∪ P; Φ; S; i)	τ -→ ({i : P } ∪ P; Φ; S; i)
			Fig. 2. Semantics for processes (selected rules)
				. An
				adversary can send any message of their knowledge on a
				public channel through the IN rule, while communications are

This work received funding from the ANR Chair AI ASAP (ANR-20-CHIA-0024) and the France 2030 program managed by the French National Research Agency under grant agreement No. ANR-22-PECY-0006.

APPENDIX

A. On the soundness of ProVerif for non-separated biprocesses Theorem 1 is established in [START_REF] Blanchet | Proverif with lemmas, induction, fast subsumption, and much more[END_REF] for separated bi-processes. We outline the argument next, referring to results in the technical report associated to that paper. In order to verify diff-equivalence, ProVerif first translates the definition of cryptographic primitives and the initial bi-process into a set of Horn clauses. It is shown in [10, Lemma 11] that if the bi-process admits non-convergent traces, then there exists a logical derivation of some bad atom using the Horn clauses. Then, [10, Theorem 3] justifies that the derivability of bad would be detected by the saturation step of ProVerif's algorithm.

The first step in this reasoning easily carries over to nonseparated bi-processes. In fact, the generalised bi-processes made available by the allowDiffPatterns option are nothing more than a back-translation: mechanisms already available in ProVerif clauses are added to bi-processes, with a semantics that naturally follows the Horn clause semantics. We briefly explain this point below, referring the reader to [23, §5.1] for a more detailed discussion, and to [10, §4.3.2] for a full definition of the translation. a) Translating bi-processes into Horn clauses: Clauses in ProVerif use an atomic proposition att (m L , m R ) to express the fact that the attacker can compute m L using some recipe after executing some trace with the left projection of the biprocess, and would compute m R using the same recipe after executing the same trace against the right projection. In terms of bi-executions, this simply means that some recipe yields diff[m L , m R ] when applied to the bi-frame obtained after executing the trace on the bi-process.

Consider for example the following separated bi-process, where cst is an arbitrary constant:

The translation would notably produce the following clauses for that bi-process (we assume that m does not contain occurrences of x, but may contain diff operators):

The first clause encodes the execution of our bi-process when the conditional succeeds on both projections; it brings no new knowledge to the attacker. The second one corresponds to the case where the conditional fails in both projections. The last one corresponds to a non-convergence case, where the conditional passes on the left but not on the right.

As is visible in this example, input variables are duplicated during the translation into their left and right counterparts. We

where M L is such that tbl (M L ) ∈ S fst , and fst(D){x L → M L }⇓ = E true;

• K = T 1 (K 0 ) = ({i :B } ∪ T 1 (P); Φ; S; i) where:

Note that the first element exists since we know that tbl (M L ) ∈ S fst . Regarding the second one, we know that it exists relying on our hypothesis K↓↑. Therefore, we consider the two following bi-configurations:

T 1 (P); Φ; S; i). Since K 0 is separated, we have that K 0 is separated too, and we have that fst(K 0 ) = K L . Relying on the fact that our transformation is compatible with substitution, we deduce that T 1 (K 0 ) = K . Then, it is easy to see that K τ τ -→ K , and thus K ↓↑.

The case of the rule GET-E can be done in a similar way. This allows us to conclude.

Lemma 3: Let B 0 be a separated closed bi-process such that T 1 (B 0 )↓↑, and T ∈ traces(T 1 (B 0 )). There exists T fst ∈ traces(fst(B 0 )) such that T fst ∼ = fst(T ). A similar result holds for snd.

Proof. We prove the result for fst, starting with the following claim.

Claim. Let K 0 be a separated bi-configuration, K = T 1 (K 0 ) such that K↓↑. If K α -→ K for some α and some K with a rule different from GET-T and GET-E, then there exists K 0 a separated bi-configuration such that K = T 1 (K 0 ), and fst(K 0 ) α -→ fst(K 0 ). A similar result holds when considering K τ τ -→ K corresponding to the execution of two get instructions in a row. In such a case, we have that fst(K 0 ) τ -→ fst(K 0 ).

Note that the result stated above allows us to prove the statement in the lemma by induction on the length of the execution trace T . Now, it remains to establish this claim. We do a case analysis on the rule(s) used to perform K -→ K . Case IN. In such a case, we have that:

and

We consider the following bi-configuration:

Since K 0 is separated, we have that K 0 is separated too. Since K α -→ K and K↓↑, we have that K ↓↑. Relying on the fact that our transformation is compatible with substitution, we deduce that K = T 1 (K 0 ). Then, it is easy to see that fst(K 0 ) α -→ fst(K 0 ). Most of the cases can be done in a similar way. We focus now on the most interesting ones, corresponding to the execution of two get instructions in a row.We simply consider the most interesting cases, corresponding to the execution of two get instructions in a row. Case GET-T followed by GET-T. In such a case, we have that:

T 1 (P); Φ; S; i). We consider the following bi-configuration:

Since K 0 is separated, we have that K 0 is separated too. Since K τ τ -→ K , and K↓↑, we have that K ↓↑. Relying on the fact that our transformation is compatible with substitution, we deduce that K = T 1 (K 0 ). Then, it is easy to see that fst(K 0 ) τ -→ fst(K 0 ). Case GET-T followed by GET-E. In such a case, we have that

It is easy to see that K diverges, and thus K diverges too, contradicting our hypothesis.

The other cases GET-E followed by GET-E, and GET-E followed by GET-T can be done in a similar way. This allows us to conclude.

Theorem 2: Let B 0 be a separated closed bi-process such that T 1 (B 0 )↓↑. We have that fst(B 0 ) ≈ t snd(B 0 ).

Proof. Let T fst ∈ traces(fst(B 0 )). By Lemma 2, we know that there exists T ∈ traces(T 1 (B 0 )) such T fst ∼ = fst(T ). Then, relying on Lemma 3 (considering the case snd), we know that there exists T snd ∈ traces(snd(B 0 )) such that T snd ∼ = snd(T ). Moreover, since T ∈ traces(T 1 (B 0 )) and T 1 (B 0 )↓↑, we have that fst(T ) ∼ = snd(T ). This allows us to conclude that T fst ∼ = fst(T ) ∼ = snd(T ) ∼ = T snd . Hence, the result.