Vincent Cheval

Raphaëlle Crubillé

Steve Kremer

Symbolic protocol verification with dice: process equivalences in the presence of probabilities

Keywords: Security protocols, symbolic verification, probabilistic process equivalences. ≤ tr ≤

Symbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need for randomized schedulers and exhibit a counterexample to a result in a previous work that relied on nonrandomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. In particular, when considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has-maybe surprisingly-a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity.

Introduction

Automated symbolic protocol verification, based on the seminal work of Dolev and Yao [START_REF] Dolev | On the security of public key protocols[END_REF], has nowadays reached a level of maturity enabling successful use on complex realworld security protocols, including TLS [START_REF] Bhargavan | Verified models and reference implementations for the tls 1.3 standard candidate[END_REF], [START_REF] Cremers | A comprehensive symbolic analysis of TLS 1.3[END_REF], Signal [START_REF] Cohn-Gordon | A formal security analysis of the signal messaging protocol[END_REF], authentication protocols of the 5G standard [START_REF] Basin | A formal analysis of 5g authentication[END_REF], or EMV's secure payment protocols [START_REF] Basin | The EMV standard: Break, fix, verify[END_REF] to name only a few. In the symbolic model, a non-deterministic, computationally unbounded attacker is assumed to have complete control of the network, being able to intercept any messages, and forge new ones. As a counterpart, cryptography is idealized and the attacker can only use predefined rules to manipulate messages that are represented by terms, e.g., expressed by an equation dec(enc(m, k), k) = m stating that a message m encrypted with k can be decrypted with the same key. This treatment of cryptography is in opposition to computational models where we assume a probabilistic polynomial time attacker, messages are represented by bitstrings and assumptions that an arbitrary such attacker has at most negligible probability of breaking a cryptographic primitive. Similarly, in the symbolic model, random values, such as keys or nonces, are chosen freshly from an infinite domain, rather than chosen randomly from a sufficiently large domain. These symbolic abstractions of cryptography and randomness have even been shown sound [START_REF] Cortier | A survey of symbolic methods in computational analysis of cryptographic systems[END_REF] (under rather strong assumptions) and significantly ease the automation of proofs. Hence, symbolic modeling of messages is arguably useful for formally analyzing cryptographic protocols.

However, the above-described abstractions of randomness only apply to the messages, and not to the control flow. Typical examples which crucially rely on randomized control flow are mechanisms for providing anonymity, such as the dining cryptographers protocol [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], mix-nets [START_REF]Untraceable electronic mail, return addresses, and digital pseudonyms[END_REF] or Crowds [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF]. In this paper, we will investigate indistinguishability properties, expressed as equivalences in a cryptographic process calculus, the applied π-calculus [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF], extended with a probabilistic choice operator. Typically, the testing equivalence expresses that two processes are equivalent if they exhibit the same behaviour when put in parallel with an arbitrary attacker process. Our work presents foundations for a model that (i) extends the scope of symbolic protocol analysis to probabilistic protocols, and (ii) allows to consider a probabilistic attacker (even on non-probabilistic protocols). In particular, when we consider purely concurrent processes-without probabilistic behavior-the equivalence we obtain is strictly stronger than the standard testing equivalence on such purely concurrent processes; in other terms, probabilistic adversaries are-for good reasons, as we will argue-more powerful in order to distinguish such processes than the purely concurrent adversaries considered in existing works and tools.

Our contributions. Our contributions can be split into three parts.

In a first part we introduce a probabilistic applied πcalculus and its semantics, which has similarities to [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF], with two major differences. (i) We express our semantics in terms of general non-deterministic probabilistic transition systems (NPLTS)-also called probabilistic automata in the literature-which allows us to benefit from a large body of existing results on these systems [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], [START_REF] Parma | Logical characterizations of bisimulations for discrete probabilistic systems[END_REF], [START_REF] Castiglioni | Trace and testing metrics on nondeterministic probabilistic processes[END_REF], [START_REF] Bonchi | The theory of traces for systems with nondeterminism and probability[END_REF], [START_REF] Deng | Testing finitary probabilistic processes[END_REF], [START_REF] Stoelinga | Alea jacta est: verification of probabilistic, real-time and parametric systems[END_REF], [START_REF] Eisentraut | Principles of markov automata[END_REF]. (ii) More importantly, we differ in the way non-determinism is resolved: unlike [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF] we allow for randomized schedulers-rather than choosing one particular non-deterministic choice, we allow the scheduler to choose an arbitrary distribution on the available non-deterministic choices.

Second, we define several notions of preorders and equivalences and study their relations. The main results are also summarized in Figure 1, focusing on preorders (with similar relations between corresponding equivalences). We show, in particular, that

• unlike in the purely non-deterministic case, the maytesting preorder (≤ may ) is strictly stronger than the trace equivalence preorder (≤ tr ) (Theorem 1); • simulation (≤ sim ) and observational pre-order (≤ obs ), respectively bisimilarity and observational equivalence, coincide for randomized schedulers (Theorem 2); • for non-randomized schedulers, these equivalences (≤ nr sim and ≤ nr obs ) do not coincide (Lemma 3), which provides a counter-example to one of the main results in [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF]. Third, a well-known phenomenon [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF], [START_REF] Alvim | Safe equivalences for security properties[END_REF] in process calculi that are both probabilistic and non-deterministic is the existence of some nonrealistic schedulers that are able to use the internal probabilistic choices done by an agent in order to schedule another agent's non-deterministic choices, i.e., the scheduler leaks the probabilistic choices. Therefore, we study two important subclasses of processes that avoid this phenomenon.

We first consider the classical class of non-probabilistic processes (denoted MP np ), as in the original applied πcalculus, but in the presence of probabilistic adversaries. We show that, if we additionally bound the number of sessions (denoted MP <∞,np ),

• may-testing with probabilistic adversaries coincides with the classical, purely possibilistic notion of similarity (Proposition 5 and Theorem 2). This also provides a contextual characterization of the notion of similarity which is reminiscent of [START_REF] Deng | Testing finitary probabilistic processes[END_REF] in the setting of CSP;

• verification of testing equivalence with probabilistic adversaries is co-NEXPTIME complete for a large class of cryptographic primitives, relying on results from [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF].

We next consider a class of purely probabilistic processes with a bounded number of sessions (denoted MP pp ), which is reminiscent of a probabilistic version of simple processes in [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF], [START_REF] Comon-Lundh | Computational soundness of observational equivalence[END_REF], and a slight generalization of the processes in [START_REF] Chadha | Verification of randomized security protocols[END_REF]. We show that trace equivalence as considered in [START_REF] Chadha | Verification of randomized security protocols[END_REF], is

• weaker than may-testing, but

• coincides with a version of may-testing with determinate attackers: attacker processes are restricted disallowing replication, parallel, and non-deterministic choice, but allowing probabilistic choices (Theorem 3). Finally, we briefly discuss how the algorithm for deciding trace equivalence in the DeepSec verifier [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF] could be adapted to this fully probabilistic case, providing a more general setting than Bauer et al. [START_REF] Bauer | Model checking indistinguishability of randomized security protocols[END_REF] who additionally bound the size of input messages.

A full version with detailed proofs is available at [START_REF] Cheval | Symbolic protocol verification with dice: process equivalences in the presence of probabilities (extended version)[END_REF].

Probabilistic Applied π-calculus

In this section we introduce the probabilistic applied πcalculus, a probabilistic variant of the applied π-calculus introduced by Goubault-Larrecq et al. [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF].

Message as terms

Atomic values such as keys and nonces are modelled by names. We assume an infinite set of such names N = {a, b, . . . , } and partition it into two disjoint infinite sets N pub and N priv . The set of private names N priv is a priori unknown to the attacker and models, e.g., honest keys in a protocol. The set of public names N pub models public values, known to the attacker. The distinction between public and private names is analogous to the distinction between free and bound names in the original applied pi calculus. We also define an infinite set of variables X . Finally, we consider a finite set of function symbols each equipped with their arity F = {f /n, g/m, . . .}. Function symbols model cryptographic operations, e.g., enc/2 is a binary symbol that could be used to model encryption. Terms are defined as names, variables, and function symbols applied to other terms. For instance, given two names a, k ∈ N , enc(a, k) represents the encryption of a with the key k. For any F ⊆ F, N ⊆ N and V ⊆ X , the set of terms built from N and V by applying function symbols in F is denoted by

T (F, N ∪ V).
We also suppose that terms are equipped with a binary relation . = that expresses that two terms evaluate to the same result, and a predicate Msg(•) that is intended to hold when evaluation succeeds. How . = and Msg(•) are precisely defined is not relevant for the results of this paper and we wish to capture several formalisms.

. = can for instance be defined by an equational theory, as in the applied πcalculus [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF] (where Msg(•) would evaluate to true on any term), by a constructor-destructor rewrite system, allowing evaluation to fail when a destructor application does not reduce, as in the DeepSec tool [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF], or a combination of these as in the ProVerif tool [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF].

Formally, we require that = m for any m, k modelling that decryption cancels out encryption when the same key k is used; one may also define Msg(dec(n, k)) as false to express that decryption fails if the ciphertext argument is not an encryption with the matching key.

Syntax of the process calculus

The syntax for processes is defined as follows:

P, Q ::= processes 0 nil in(u, x); P output out(u, v); P input P | Q parallel composition !P replication new a; P restriction if u = v then P else Q conditional P + Q non-deterministic choice P + p Q probabilistic choice
where u, v ∈ T (F, N ∪ X ), x ∈ X , a ∈ N and p ∈]0; 1[. As usual, in examples we will omit trailing 0 processes and else 0 branches. A process P is closed when all variables in P are bound by an input.

Example 1. As an example, consider the process P :

(out(c, k) + 1 3 out(c, a)) | in(c, x); if x = k then out(c, ok) P consists of two parallel processes. The left process outputs on a channel c with probability 1 3 the name k and with probability 2 3 the name a. The right process inputs a value on channel c and binds this value to x. If x equals k then it outputs the constant ok.

We denote by SP the set of all processes in the probabilistic applied π-calculus, and by MP the set of all multisets over SP.

Operational semantics

We will now define the semantics of the probabilistic applied π-calculus. We opt for a different presentation of the semantics than Goubault-Larrecq et al. [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF] relying on existing formalisms for transition systems. Moreover, we allow for a more general class of schedulers. Notation 1. Let S be an arbitrary set. We denote by D(S) the set of all finitely supported probability distributions over S and by D ≤1 (S) the set of all sub-probability distributions over S (observe that D(S) ⊆ D ≤1 (S)). For p, q ≥ 0, and D, E two sub-distributions, we define the measure

(p • D + q • E)(x) = p • D(x) + q • E(x).
When q = 0, the resulting sub-distribution does not depend on E, and we simply write p

• D instead of p • D + 0 • E.
If D ∈ D(S), we denote by supp(D) the support of D, i.e., the set of all elements s ∈ S such that D(s) > 0.

If S ⊆ S, we define D(S ) = s∈S D(s). Finally, we denote by δ x the Dirac distribution on x.

The operational semantics of processes is defined by a relation between multisets of processes and probability distributions on multisets of processes, denoted P → τ µ. This relation is defined in Figure 2.

Remark 1. One may note that our calculus offers a nondeterministic choice operator that is resolved internally. This differs from the standard pi-calculus [START_REF] Milner | A calculus of mobile processes, I[END_REF] where the nondeterministic choice operator is resolved externally. Note that the original applied pi calculus [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF] does not contain non-deterministic choice.

In the following, we define the operational semantics of our calculus using well studied probabilistic systems. We choose the formalism of non-deterministic probabilistic labelled transition systems (NPLTS) used for instance in [START_REF] Bonchi | The theory of traces for systems with nondeterminism and probability[END_REF]. A NPLTS allows to represent states that allow both internal and external non-deterministic behavior. It can be noted that it coincides with the notion of simple probabilistic automata of Segala et al. [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. Definition 1. A NPLTS is a triple (S, A, trans), where

• S is a set of states,

P ∪ { {0} } → τ δ P P ∪ { {if u = v then P else Q} } → τ δ P∪{ {P } } if u . = v P ∪ { {if u = v then P else Q} } → τ δ P∪{ {Q} } if u . = v P ∪ { {out(u, t).P, in(v, x).Q} } → τ δ P∪{ {P,Q{x →t}} } if Msg(t) ∧ u . = v P ∪ { {P | Q} } → τ δ P∪{ {P,Q} } P ∪ { {!P } } → τ δ P∪{ {!P,P } } P ∪ { {new a; P } } → τ δ P∪{ {P { a /a}} }
where a ∈ N priv is fresh for each state in S, and each label in A, trans(s)(a) is a set of (finitely supported) distributions.

P ∪ { {P + Q} }) → τ δ P∪{ {P } } P ∪ { {P + Q} } → τ δ P∪{ {Q} } P ∪ { {P + p Q} } → τ p • δ P∪{ {P } } + (1 -p) • δ P∪{ {Q} }
The label τ is the internal action and the labels in A ext are the external actions. For s ∈ S, a ∈ A, we write s a -→ D when D ∈ trans(s, a).

In the remaining of this paper, we may define a NPLTS by only its transition function, i.e., we will say that trans : S → A → P(D(S)) is the NPLTS (S, A, trans).

We now express our operational semantics as a NPLTS without external actions, i.e., A ext = ∅. External actions will be used to express our labeled semantics in Section 4.1.

Definition 2. The operational semantics is the NPLTS N o = (MP, {τ }, trans o ) where for every s ∈ MP,

trans o (s)(τ ) = {D | s → τ D}.
Note that the states of the NPLTS N o contain all possible multisets of processes and how they are executed. Obviously, N o is thus an infinite transition system. In examples illustrating transitions of a multiset of processes P, we only show the relevant fragment of N o that contains P.

Example 2. The complete execution of the process P , introduced in Example 1 is given in Figure 3.

Behavioral equivalences

In this section we define probabilistic versions of two classical equivalences: may-testing and the stronger observational equivalence. In order to do so we first introduce the notion of resolution (also known as scheduler), i.e., how internal non-determinism is resolved, and the notion of barb, which models an observational action.

{ {P } } { {A, B} } τ { {out(c, k), B} } { {out(c, a), B} } 1/3 2/3 τ { {0, B 1 } } τ { {0, 0} } τ { {B 1 } } τ { {0} } τ τ ∅ τ { {0, B 2 } } τ { {B 2 } } τ { {0, B 3 } } τ { {B 3 } } τ τ A = out(c, k) + 1 3 out(c, a) B = in(c, x); if x = k then out(c, ok) B 1 = if a = k then out(c, ok) B 2 = if k = k then out(c, ok) B 3 = out(c, ok)

Resolving the internal non-determinism

Resolutions express how internal non-determinism of a NPLTS is resolved. Intuitively, resolving the nondeterminism means restricting the transition system by choosing for each state either one particular internal transition or leave the choice of a non-deterministic external action. The resulting transition system is called a Reactive Probabilistic Labelled Transition System (RPLTS) and has still external, but no internal, non-determinism. It can be noted that this model is equivalent to Labelled Markov Chains when extended with internal actions. Definition 3. A RPLTS is a triple (S, A, trans), where

• S is a set of states, • A = {τ } A ext a set of labels, and • trans : S → D(S) (A ext → D(S) ∪ { }) is a transition function that assigns to each state in S either a unique distribution for the label τ (the deterministic internal action); or a function mapping labels in A ext to a failure ( ) or a distribution over S (the non deterministic external actions). States s ∈ S such that trans(s) : A ext → D(S) ∪ { } are called external states, while the ones such that trans(s) : D(S) are called internal states. Given a RPLTS R, we denote by S ext (R) and S int (R) the sets of external and internal states of R respectively. For a more homogeneous notation, when s is an internal state, we sometimes write trans(s)(τ ) = D instead of trans(s) = D.

Remark 2. In the particular case of a NPLTS N with no external action, resolving the internal non-determinism results in a RPLTS without any non-determinism. This is the case of the operational semantics N o . Such a purely probabilistic system is typically equivalent to the notion of Markov Chain. By abuse of notation, the transition function

trans : S → D(S) (∅ → D(S) ∪ { })
of such RPLTS is rewritten as trans : S → D(S) { } as for any set X, the cardinality of the set (∅ → X) is 1.

Before defining the notion of resolution-or schedulers-, we need to introduce two classical notions in probabilistic models: the convex hull of a set of distributions and the probabilistic lifting of a function. Notation 2. Let S be a set of states. The convex hull of ∆ ⊆ D(S), denoted conv(∆), is the set of distributions D ∈ D(S) such that ∃α 1 , . . . , α n ∈ R.∃D 1 , . . . , D n ∈ ∆.

n i=1 α i = 1 and D = n i=1 α i • D i
Intuitively, rather than choosing one distribution in ∆, each element in conv(∆) corresponds to a distribution over the distributions in ∆. This will be useful for defining randomized schedulers.

Next, we lift functions to distributions: applying a function f to a distribution simply defines a new distribution that transfers, according to f , the probability weight of elements in the domain of f to its image, possibly summing these weights when f maps several inputs to a same output. Notation 3. Let S, S be two sets of states and f : S → S . We define the function f : D(S) → D(S ) to be the probabilistic lifting of f , where

f (D) = s∈S D(s) • δ f (s)
When obvious from context, we will overload the notation and write f instead of f . We now define resolutions for a NPLTS that allow to solve the internal, but not external, non-determinism: a resolution describes one of the possible ways of turning an NPLTS into a RPLTS. It means that for each state s, a resolution should choose whether s is an internal state or external state; in the first case, a unique post-transition distribution must be chosen; in the second case, for each external action a, the resolution must choose to either stop (i.e., trans(s) = ) or a unique distribution D such that s a -→ D (i.e., trans(s) = D). Due to the possible existence of cycles in the NPLTS, a scheduler that visit multiple times a certain state s must be able to choose differently how to resolve the non determinism every time it visits s. This leads to the notion of correspondence function. Given a NPLTS N we denote by R r (N) the set of randomized resolutions. Additionally, we denote R o r = R r (N o ). Figure 4 shows an example of a resolution from R o r for the process P from Example 2.

{ {P } } { {A, B} } τ { {out(c, k ), B} } { {out(c, a), B} } 1/3 2/3 τ { {0, B 1 } } τ { {0, 0} } { {B 1 } } { {0} } τ τ ∅ τ 1/4 3/4 τ { {0, B 2 } } τ { {B 2 } } τ { {B 3 } } τ

Computing the probability to reach a barb

The notion of barb is a classical way of expressing observables. Intuitively a state of N o , i.e., a multiset of processes, exhibits a barb c whenever an output on channel c is possible. Definition 5. For c ∈ N pub and P ∈ MP, we say that P exhibits barb c when there exists a process out(u, t).Q in P where c . = u and Msg(t). We denote by ↓ c the set of all multisets of processes that exhibit the barb c.

We next define the probability of reaching a state in a set of target states, in a fully probabilistic transition system, i.e., in a transition system where all non-determinism-internal or external-has already been resolved. We first define the probability of reaching such a state in at most n steps, and then we take the probability of reaching them eventually as the limit of the n-step reaching probabilities. Definition 6. Let R = (S, A, trans) be a RPLTS, T ⊆ S a set of states, and s an initial state. For every n ∈ N we define the probability of reaching T from s in at most n steps as:

RProb ≤0 R (s, T ) = 1 if s ∈ T 0 otherwise. RProb ≤n+1 R (s, T ) =          1 if s ∈ T 0 if s ∈ T ∧ s ∈ S ext (R) u∈supp(D) D(u) • RProb ≤n R (u, T ) if s ∈ T ∧ trans(s)(τ ) = D
We define the probability of reaching T from s as:

RProb R (s, T ) = lim n→+∞ RProb ≤n R (s, T ).
Note that, as RProb ≤n R (s, T ) is an increasing function in n we can replace the limit by the supremum on n ∈ N.

Given N = (S N , A, trans N ), we denote by RProb Rr(N) (s, T ) the probability:

sup RProb R (s , corr -1 (T )) (corr, R) ∈ R r (N), corr(s ) = s

Defining May Testing Equivalence

Intuitively, two processes are may-testing equivalent if they exhibit the same observations when executed in the presence of any attacker process. This models the inability of an arbitrary process to distinguish them. More formally, two multisets of processes P and Q are may testing equivalent when the attacker has the same probability over all schedulers to exhibit the barb c in both P and Q.

Definition 7 (May testing equivalence). Let P, Q ∈ MP. We say that P ≤ may Q iff:

∀Adv ∈ MP s.t. fn(Adv) ⊆ N pub . ∀c ∈ N pub . RProb R o r (P ∪ Adv, ↓ c) ≤ RProb R o r (Q ∪ Adv, ↓ c)
We say that P, Q are may testing equivalent, denoted P ≈ may Q, when P ≤ may Q and Q ≤ may P.

One could also consider a more fine-grained definition of may testing pre-order that guarantees the equality of probabilities between two schedulers rather than comparing the probabilities over all schedulers. Formally, this pre-order, denoted ≤ may , requires that for all resolutions (corr, R) ∈ R r (N) and state s of R such that corr(s) = P ∪ Adv, there exist a resolution (corr , R ) and a state s of R such that

corr (s ) = Q ∪ Adv and RProb R (s, corr -1 (↓ c)) = RProb R (s , corr -1 (↓ c))
However, the resulting relation is counter-intuitive and distinguishes processes

P := { {out(a, 0)} } and Q := { {out(a, 0) + 1 2 (out(a, 0) + 1 2 out(a, 0))} }.
Indeed, we can show that Q ≤ may P: for Adv = { {0} }, there exists a resolution (corr, R) such that

corr(s) = P ∪ Adv and RProb R (Q, ↓ a) = 1 2
but for every resolution (corr , R ) such that corr (s ) = Q ∪ Adv, RProb R (P, ↓ a) = 1.

Defining Observational Equivalence

In this section, we define observational preorders and equivalence which are stronger than may testing. When studying cryptographic protocols we suppose that internal actions are not observable and therefore only study weak equivalences hiding whether such internal actions take place or not. To define the observational preorder we need to introduce a weak relation for internal actions. In a purely non-deterministic system this simply corresponds to the reflexive, transitive closure τ -→ * . However, in our setting we need to compute the corresponding distributions. Definition 8. Let N be a NPLTS and D, E ∈ D ≤1 (S N ). We write

D τ = =⇒ Rr(N) E when there exists (corr, R) ∈ R r (N) and D , E ∈ D ≤1 (S R ) such that • corr(D ) = D, corr(E ) = E, supp(E ) ⊆ S ext (R), • ∀u ∈ S ext (R). E (u) = s ∈S R D (s )•RProb R (s , {u}).
To define the observational preorder, we additionally need to lift relations defined on a given set to relations on sub-distributions over this set. Definition 9 (Lifting of a relation). Let R be a binary relation on a discrete set S. We define the lifting of R to sub-distributions as the binary relation on D ≤1 (S), denoted R, defined as:

D R E when ∀S ⊆ S, D(S ) ≤ E(R(S ))
where R(S ) = {s ∈ S | s ∈ S ∧ s R s}.

Using these notions of weak transition and lifting of relations to sub-distributions we can define observational equivalence.

Definition 10. The observational preorder ≤ obs is the largest relation R on MP such that P R Q implies :

• ∀c ∈ N pub . RProb R o r (P, ↓ c) ≤ RProb R o r (Q, ↓ c); • if P τ = =⇒ R o r D and D ∈ D(S N o ) then Q τ = =⇒ R o r E, E ∈ D(S N o ) and D R E; • ∀ closed Adv ∈ MP such that fn(Adv) ⊆ N pub .
{Adv} ∪ P R {Adv} ∪ Q. The observational equivalence ≈ obs is defined by additionally requiring R to be symmetric.

Remark 3. Note that we slightly diverge from the original definition of observational equivalence [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF] where an

evaluation context C[ ] is of the form new n 1 ; . . . ; new n k ; ( | A)
In our definition we simply consider a parallel process, and no additional name restriction. However, we prove in the full version that these two definitions coincide. Intuitively, restricting names whose scope includes the adversarial process A corresponds to making previously public channels invisible to the attacker at later steps, hence it does not provide additional distinguishing power.

Labelled semantics and equivalences

As usual in π calculi, and in the applied π-calculus, we define a labelled semantics. The intent of the labels is to capture adversarial actions and avoid the universal quantification over processes in equivalence definitions.

Labelled semantics

A state in this labeled semantics is defined by associating a multiset of processes with a frame, modeling the adversary's knowledge. We consider a new set of variables AX = {ax 1 , ax 2 , . . .} distinct from X that will act as pointers to messages that were previously output. Definition 11. An extended process is a pair (P, φ), where P ∈ MP and φ is a ground substitution

{ax 1 → t 1 ; . . . ; ax n → t n } such that ax i ∈ AX , t i ∈ T (F, N ) and Msg(t i ) for 1 ≤ i ≤ n.
We denote by SP the set of all extended processes.

A recipe is a term from T (F, N pub ∪ AX } representing how an attacker can deduce a message. • trans ((P, φ))(a) = {D | (P, φ) → a D} where → a is defined in Figure 5.

Note that when we lift → τ to extended processes we suppose that the freshness requirement of a new name a in the (NEW) rule of Figure 2 also applies to the frame φ, i.e., a must not appear in φ.

Remark 4. It should be noted that we deal with static equivalence in a different way as done usually in the applied π-calculus, or implicitly in the probabilistic applied πcalculus [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF]: we encode static equivalence into the NPLTS N by a countable set of actions-all the tests (ξ

? = ζ)
and their negations-instead of just one action testing static equivalence. The motivation behind this choice is to be able to represent every action from the NPLTS by an elementary action of the adversary. As shown later, this choice has no effect on the definition of the simulation pre-orders or on bisimulation, but it leads to a slightly different notion of trace equivalence, that is closer to may testing equivalence.

Defining Trace Equivalence

We first define the probability of executing a trace for a given resolution. As we are interested in weak trace preorder (where internal actions cannot be observed), traces are sequences of external actions only. Our definition uses the previously introduced notation RProb R (s, {t}): recall that this denotes the probability of reaching state t from state s using only internal actions for some resolution (corr, R).

Definition 13. Let R = (S, {τ } A ext , trans) be a RPLTS. Let w ∈ A ext * be a trace, i.e., a finite word on the alphabet A ext . For all states s ∈ S, we define the probability of executing w starting from s in R as:

• Prob R (s, ) = 1 • Prob R (s, a.w) = t∈S trans(t)(a)=D RProb R (s, {t})• s ∈supp(D) D(s ) • Prob R (s , w)
Given a NPLTS N = (S, A, trans), we denote by Prob Rr(N) (s, w) the probability:

sup{Prob R (s , w) | (corr, R) ∈ R r (N), corr(s ) = s}
This allows us to define trace equivalence of (P, φ) and (P , φ ): intuitively any trace that can be executed in (P, φ) can be executed with at least the same probability in (P , φ ) and vice-versa. Definition 14 (trace equivalence). Let (P, φ), (P , φ ) ∈ SP . We say that (P, φ) ≤ tr (P , φ ) iff for all w ∈ A ext * , Prob Rr(N ) ((P, φ), w) ≤ Prob Rr(N ) ((P , φ ), w)

(P, φ) and (P , φ ) are trace equivalent, denoted (P, φ) ≈ tr (P , φ ), when (P, φ) ≤ tr (P , φ ) and (P , φ ) ≤ tr (P, φ).

Observe that in the NPLTS N o , even though s τ -→ D implies that D has finite support, it is possible to have

δ s τ = =⇒ R E,
where the sub-distribution E has infinite support.

Unlike, in the purely possibilistic case, in our probabilistic setting trace preorder is strictly weaker than the may testing preorder.

Theorem 1. Let P, Q ∈ MP be two processes.

P ≤ may Q ⇒ (P, ∅) ≤ tr (Q, ∅)
Moreover, processes P, Q ∈ MP defined in Figure 6 are such that (P, ∅) ≤ tr (Q, ∅) and P ≤ may Q.

Figure 6 witnesses that the implication is strict. P and Q output each 3 encrypted bits (in a non-deterministic order). P outputs twice the encryption of 0; Q twice the encryption of 1. The (randomized) encryption ensures that these three values are indeed indistinguishable. We give the adversary a single access to a decryption oracle P dec . Intuitively, trace equivalence holds, as the scheduler can ensure that matching encryptions are sent to P dec . However, may-testing does not hold: the attacker chooses uniformly at random one of the three encryptions to submit. The probability to hit 0 will be 2 3 in P and only 1 3 in Q. Observe that Theorem 1 holds for any processes and does not require them to be image-finite, contrary to usual results in the literature, e.g., [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF]. This discrepancy comes from our choice of labelled actions for static equivalence (see Remark 4): a trace cannot test directly static equivalence, but can only do a finite numbers of recipe tests. We believe this variant definition of trace equivalence to be of independent interest as it provides an exact characterization of may testing in the purely non-deterministic case.

Defining Bisimulation

In this section, we define simulations on probabilistic processes and corresponding equivalences. Our definition of simulation preorder is similar to the definition of randomized weak simulation preorder introduced by Segala and Lynch for probabilistic automata [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. We reuse the lifting of a relation and the weak relation for internal actions defined in Section 3.4 but applied to the NPLTS N . In particular, given an action a ∈ A ext and two distributions D, D ∈ D(S), we write

(P, φ) → τ (D, φ) if P → τ D ({ {in(u, x); P } } ∪ P, φ) → in(ξ,ζ) δ ({ {P { ζφ /x}} }∪P,φ) if u . = ξφ,
D a = =⇒ R r D when D τ = =⇒ R r E 1 , E 1 a -→ E 2 and E 2 τ = =⇒ R r D for some E 1 , E 2 and where R r denotes R r (N ). Here E 1 a -→ E 2 is the natural lifting of the transition function of N , i.e., E 2 = s E 1 (s) • D with s a -→ D. Definition 15. A relation R ⊆ (S N × S N ) is • a simulation if s 1 R s 2 implies that for all a ∈ A ext ∪ {τ }, D 1 ∈ D(S N ) if s 1 a -→ D 1 then s 2 a = =⇒ R r D 2 , D 2 ∈ D(S N )
and

D 1 R D 2
• a bisimulation if R is a simulation and R is symmetric. The simulation preorder, denoted ≤ sim , is the largest simulation and bisimilarity, denoted ≈ bi , is the largest bisimulation. We define similarity, denoted ≈ sim , as ≤ sim ∩ ≤ -1 sim . As usual in the field of (bi)simulation, it can be shown that ≤ sim , respectively ≈ bi , exists [START_REF] Eisentraut | Principles of markov automata[END_REF] and that it is a preorder, i.e., a reflexive and transitive relation, respectively an equivalence, i.e., a reflexive, symmetric and transitive relation [START_REF] Stoelinga | Alea jacta est: verification of probabilistic, real-time and parametric systems[END_REF].

The following proposition from [START_REF] Stoelinga | Alea jacta est: verification of probabilistic, real-time and parametric systems[END_REF] states that, as usual in the non-probabilistic case, the weak arrow a = =⇒ R r can replace the single arrow a -→ in the definition of simulation.

Proposition 1. Let R be the largest binary relation on S N such that s 1 R s 2 implies that for every a ∈ A ext ∪ {τ },

if s 1 a = =⇒ R r D 1 then s 2 a = =⇒ R r D 2 , D 2 ∈ D(S N )
and

D 1 R D 2
We have R = ≤ sim .

We now show that observational preorder and equivalence are exactly characterized by the simulation preorder and bisimilarity.

Theorem 2. Let P, Q two processes in MP.

P ≤ obs Q iff (P, ∅) ≤ sim (Q, ∅) and P ≈ obs Q iff (P, ∅) ≈ bi (Q, ∅)
Proof sketch. We here provide the main intuitions of the proof that P ≤ obs Q iff (P, ∅) ≤ sim (Q, ∅).

(⇒). To show that observational preorder implies simulation, we need to represent the frame of an extended process (P, φ) as a process: we output in parallel the terms ax i φ, with ax i ∈ dom(φ), on a public channel c i , distinct for each i and not occurring anywhere in (P, φ). Thus, we build the relation R such that

(P, φ) R(Q, φ ) if P ∪ { {out(c i , ax i φ); 0} } n i=1 ≤ obs Q ∪ { {out(c i , ax i φ ).0} } n i=1 with |dom(φ)| = |dom(φ )| = n and c 1 , . . . , c n ∈ N pub pairwise distinct and not occurring in P, Q, φ, φ .
As the public channels c i do not occur anywhere else, any internal transition on

P 1 = P ∪ { {out(c i , ax i φ); 0} } n i=1
must correspond to an internal transition on P; and similarly for Q.

For all visible actions, we rely on ≤ obs being closed by composition with an adversarial process. For example, when the action is the test ξ ? = ζ, we compose with the adversarial process that (i) reads the frame, (ii) applies the test, and (iii) outputs on a fresh public channel ok if the test succeeds:

Adv = in(c 1 , x i ); . . . ; in(c n , x n );
if ξρ = ζρ then out(ok, ok); 0 else 0 where x 1 , . . . , x n are fresh variables and ρ = { xi / axi } n i=1 . We then consider the transition

{ {Adv} } ∪ P 1 τ = =⇒ R o
r δ P∪out(ok,ok) and the fact that RProb Rr (P ∪ out(ok, ok), ↓ ok) = 1 to conclude. Indeed, for

{ {Adv} } ∪ Q ∪ { {out(c i , ax i φ ).0} } n i=1 τ = =⇒ r E to exist with δ P∪out(ok,ok) R E, { {Adv} } ∪ Q ∪ { {out(c i , ax i φ ); 0} } n
i=1 must also have passed the test ξρ = ζρ in the conditional branching. Hence ξφ = ζφ and so

(Q, φ ) ξ ? =ζ --→ δ (Q,φ ) .
When the visible action is an output or an input, the process is more complicated. The adversarial process starts by reading the frame as before and executing the action. The last part of the adversarial process consists in outputting again the frame so that we re-enter the relation R. Assume for instance the action in(ξ, ζ). By definition, P = P 1 ∪ { {in(c, x); P } } with ξφ . = c, (P, φ)

in(ξ,ζ) ----→ δ P1∪{ {P σ} } and σ = { ζφ / x }.
We consider the following adversarial process Adv:

Adv = in(c 1 , x i ); . . . ; in(c n , x n ); out(ξρ, ζρ); (out(ok, ok) + 0.5 (out(c 1 , x 1 ); 0 | out(c n , x n ); 0))
where c 1 , . . . , c n are fresh public names pairwise distinct not occurring anywhere else. We will conclude by considering the transition

{ {Adv} } ∪ P ∪ { {out(c i , ax i φ); 0} } n i=1 τ = =⇒ r D where D = 0.5 • δ P1∪{ {P { ζφ /x},out(ok,ok).0} } + 0.5 • δ P1∪{ {P {ζφ/x}} }∪{ {out(c i ,axiφ);0} } n i=1
Indeed, for

{ {Adv} } ∪ Q ∪ { {out(c i , ax i φ ); 0} } n i=1 τ = =⇒ r E to exist with D R E, { {Adv} } ∪ Q ∪ { {out(c i , ax i φ ); 0} } n i=1
must also have applied an internal transition executing the construct out(ξρ, ζρ) which allows for the labeled action in(ξ, ζ) to be executed on (Q, φ ).

(⇐). Showing that simulation implies observational preorder is more straightforward. We build a relation R such that P R Q when there exist two extended processes (P 1 , φ), (Q 1 , φ ) with compatible frames (i.e. dom(φ) = dom(φ )), a renaming ρ from N pub to N priv , and a multiset of adversarial processes P Att such that:

• names in img(ρ) do not occur in P 1 , φ, Q 1 and φ ;

• P = P 1 ρ ∪ P Att { axiφ / xi } n i=1 ρ; • Q = Q 1 ρ ∪ P Att { axiφ / xi } n i=1 ρ; • (P 1 , φ) ≤ sim (Q 1 , φ ).
The renaming ρ replaces the private names that are generated by the processes in P Att (through the construct new a; P ) with public names that are chosen fresh (i.e. not in P 1 , φ, Q 1 and φ ).

Randomized vs non-randomized schedulers

All our equivalence notions are based on randomized schedulers where the non-determinism is solved by picking a distribution from the convex hull of the available distributions. In the literature, more restrictive non-randomized schedulers have also been considered when defining observational equivalence and bisimilarity [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF]. A nonrandomized scheduler solves the non-determinism by choosing directly one of the available distributions. Formally, in Definition 4, instead of requiring that trans (s )(a) = D implies corr(D) ∈ conv(trans(corr(s ))(a)), a nonrandomized resolution requires that trans (s )(a) = D implies corr(D) ∈ trans(corr(s ))(a) and corr is injective on the support of D.

Denoting by R nr (N) the set of all non-randomized schedulers of N, we can naturally update the notions used to define behavioural equivalences to non-randomized schedulers. For instance, we denote by RProb Rnr(N) (s, T ) the probability of reaching T from s over all non randomized schedulers R nr (N). Similarly, Prob Rnr(N) (s, w) denotes the probability of executing the trace w from s over all schedulers from R nr (N). Updating the definitions results into may-testing and trace preorder for non-randomized schedulers, denoted ≤ nr may and ≤ nr tr respectively. We now show that ≤ may and ≤ tr do not depend on the whether schedulers are randomized or not (unlike simulation based notions as we will see below).

Lemma 1. May testing and trace preorders with randomized and non-randomized resolutions coincide:

≤ may = ≤ nr may and ≤ tr = ≤ nr tr Proof sketch. The core of the proof is the following fact: when we fix a randomized resolution R, an initial state s, and n ∈ N, it is possible to decompose the behaviour of R from state s and during the n first execution steps into a weighted family of non-randomized resolution (α i , R i ) i∈I (where the weight α i is a coefficient in [0, 1], in the sense that for every set of processes P, RProb ≤n R (s, P) = i∈I α i RProb ≤n Ri (s, P). The construction of this decomposition is defined inductively on n.

This result is of interest as it is often easier to manipulate non-randomized schedulers, and we expect automated verification to be more convenient as well.

When considering observational equivalence, simulation and bisimulation, non-randomized schedulers raise a number of issues. First, as highlighted for instance in [START_REF] Eisentraut | Principles of markov automata[END_REF], [START_REF] Deng | Axiomatisations and types for probabilistic and mobile processes[END_REF], when considering bisimulation or simulation on general NPLTSs, non-randomized resolutions result into relations that are not transitive. We show that even on the specific NPLTS N , simulation is not transitive.

Simulation for non-randomized scheduler is naturally defined by extending the notation D τ = =⇒ Rr(N) E to nonrandomized scheduler, denoted D τ = =⇒ Rnr(N) E: from Definition 8, we require (corr, R) to be in R nr (N) and additionally require an injectivity property on the correspondence function, i.e., corr is injective on the support of D . We denote the resulting simulation with non-randomized schedulers by ≤ nr sim (and similarly for ≤ nr obs , ≈ nr obs and ≈ nr bi ). Lemma 2. ≤ nr sim is not transitive. Proof sketch. Consider processes P = out(a, c) + 0.5 out(b, c) Q = (out(a, c) + 0.9 out(b, c)) + (out(a, c)

+ 0.1 out(b, c)) Q = if c = c then Q else 0 R = Q + 0.5 Q ({ {R} }, ∅) α ({ {Q} }, ∅) α ({ {Q } }, ∅)
s R s Q,1 s Q s Q,2 0
({ {P } }, ∅) ≤ nr sim ({ {R} }, ∅) ≤ nr sim ({ {Q} }, ∅) but ({ {P } }, ∅) ≤ nr sim ({ {Q} }, ∅)
The corresponding fragment of N is displayed in Figure 7a. We will show that

({ {P } }, ∅) ≤ nr sim ({ {R} }, ∅) and ({ {R} }, ∅) ≤ nr sim ({ {Q} }, ∅) but ({ {P } }, ∅) ≤ nr sim ({ {Q} }, ∅)
It is easy to see that ({ {Q} }, ∅) ≈ nr bi ({ {Q } }, ∅) and so

({ {R} }, ∅) ≤ nr sim ({ {Q} }, ∅). The difficult part of the proof of ({ {P } }, ∅) ≤ nr sim ({ {R} }, ∅) is to match ({ {P } }, ∅) τ -→ 0.5 • δ ({ {out(a,c)} },∅) + 0.5 • δ ({ {out(b,c)} },∅)
This is achieved by the scheduler displayed in Figure 7b. Finally, we prove

({ {P } }, ∅) ≤ nr sim ({ {R} }, ∅) by show- ing that the transition ({ {P } }, ∅) τ -→ 0.5 • δ ({ {out(a,c)} },∅) + 0.5 • δ ({ {out(b,c)} },∅) cannot be simulated in ({ {Q} }, ∅).
Note that the definitions of bisimilarity in [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF] rely on non-randomized schedulers. Even though this does not necessarily imply that their relation is not transitive (as they focus directly on the semantics of processes) we show in the next lemma that ≈ nr bi and ≈ nr obs do not coincide, hence disproving [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF]Theorem 2]. This reenforces our belief that it is preferable to use randomized schedulers in our definition. Lemma 3. There exist processes P, Q ∈ SP such that

• ({ {Q} }, ∅) ≈ bi ({ {P } }, ∅), • ({ {Q} }, ∅) ≈ nr bi ({ {P } }, ∅), and • { {Q} } ≤ nr obs { {P } }.
Proof sketch. We consider the following processes: Remark that we have cast the definitions of [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF] in our own framework. In the full version [START_REF] Cheval | Symbolic protocol verification with dice: process equivalences in the presence of probabilities (extended version)[END_REF] we show that processes P, Q in Lemma 3 can be adapted to obtain the counterpart of Lemma 3 in the exact framework of [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF]. The failure of the proof of [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF]Theorem 2] can be traced back to the auxilliary lemma [START_REF] Goubault-Larrecq | A probabilistic applied pi-calculus[END_REF]Lemma 3] that states that bisimilarity is closed under application of closing evaluation contexts. No proof of this lemma is however provided, and it is actually false: as shown in the proof of (our) Lemma 3, the extended processes ({ {Q} }, ∅) and ({ {P } }, ∅) defined there are bisimilar (with respect to non-randomized schedulers), but it is not the case of the extended processes ({ {Q | in(d, x).0} }, ∅) and ({ {P | in(d, x).0} }, ∅).

P = out(d,

Well behaved subclasses of protocols

It is a well-known phenomenon that non-determinism and probabilistic choices do not interact well: a particular scheduler may for instance leak a secret probabilistic choice. Such schedulers are generally deemed unrealistic, and several papers aim at restricting schedulers, e.g., [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF], [START_REF] Alvim | Safe equivalences for security properties[END_REF]. We illustrate this phenomenon on the following example.

Example 3. Consider the processes

P := (in(c, x). if x = 0 then out(ok, 1) else out(bad, 1)) + 1 2 (in(c, x). if x = 0 then out(bad, 1) else out(ok, 1)) Q := in(c, x).(out(ok, 1) + 1 2 out(bad, 1))
One may, intuitively, consider that these two processes exhibit the same behaviour. Q takes an input and then with probability 1 2 decides to either output on ok or on bad. P on the other hand first choses a branch with probability 1 2 . Each branch performs an input and, depending on the input value, outputs either on ok or on bad. As the two branches make opposite choices on the output according to the input value, one might expect the probability to output on ok to be 1 2 .

({ {Q} }, ∅)

α(∅) ({ {P } }, ∅) α(∅) ({ {P } }, ∅) α(∅) 0.5 0.5 τ τ (P da , ∅) α(∅) τ (P a+ , φ) α(φ) out(d, ax 1 ) (P a , φ) α(φ) (∅, φ) α(φ) 0.1 0.9 τ (∅, φ ) out(a, ax 2 ) α(φ ) (P db , ∅) α(∅) τ (P b+ , φ) α(φ) out(d, ax 1 ) (P b , φ) α(φ) out(b, ax 2 ) 0.1 0.9 τ
For readability, α(φ) stands for all labels ξ ∼ ξ with ξ, ξ closed recipes such that ξφ ∼ ξ φ and ∼ ∈ { . =, . =}.

(a) The fragment of N corresponding to ({ {Q} }, ∅) and ({ {P } }, ∅)

P da = out(d, c);
(out(a, c) + 0.9 0) P db = out(d, c); (out(b, c) + 0.9 0)

P a+ = { {out(a, c) + 0.9 0} } P b+ = { {out(b, c) + 0.9 0} } P a = { {out(a, c)} } P b = { {out(b, c)} } φ = {ax 1 → c} φ = {ax 1 → c, ax 2 → c} { {Q; in(d, x).0} } { {P ; in(d, x).0} } { {P ; in(d, x).0} } 0.5 0.5 τ τ P da ∪ { {in(d, x).0} } τ P a+ τ P a ∅ 0.1 0.9 τ (P db ∪ { {in(d, x).0} } τ P b+ τ P b 0.1 0.9 τ (b) The fragment of N o corresponding to { {P ; in(d, x).0} } and { {Q; in(d, x).0} } Figure 8: Fragments of NPLTS showing ({ {Q} }, ∅) ≈ nr bi ({ {P } }, ∅) and { {Q} } ≤ nr obs { {P } }.
However, P and Q are not may testing equivalent and can be distinguished by the adversary Adv = { {out(c, 0) | out(c, 1)} }. Indeed, we can show that:

RProb R o r (P∪Adv, ↓ ok) = 1 RProb R o r (Q∪Adv, ↓ ok) = 1 2
Intuitively, this results from the fact that the resolution may leak the probabilistic choice through the non-deterministic choice of the attacker to output 0 or 1. The resolution chooses the attacker to output 0 in the first probabilistic branch of P and 1 in the second.

In this section we identify two subclasses of processes that avoid this problem. The first such subclass is that of non-probabilistic processes, i.e., without the + p operator (we denote by MP np all the multisets of such processes). This is the class of the original applied π-calculus which also enjoys good tool support. Figure 6 already illustrated that even on non-probabilistic processes, probabilistic adversaries have a stronger distinguishing power for the may testing equivalence. We formally characterize this distinguishing power when restricting protocols to a bounded number of sessions (denoted MP <∞,np ), i.e., considering processes without replication: for this subclass, may-testing coincides with similarity. We therefore inherit from [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF] the fact that deciding may-testing is coNEXP complete for a large class of cryptographic primitives.

The second subclass considers purely probabilistic processes with (nearly) no non-determinism. We show that trace equivalence in this class (as considered for instance in [START_REF] Chadha | Verification of randomized security protocols[END_REF]) corresponds to may-testing with a restricted, determinate adversary process. We also sketch how the algorithms of the DeepSec prover [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF] could be adapted to check trace equivalence in this probabilistic setting.

Non-probabilistic processes

May-testing with non-probabilistic adversaries and trace equivalence coincide. Our definitions of may testing and trace equivalence coincide with the classical definitions of the original, purely non-deterministic applied π-calculus when all processes are non probabilistic. As a first step, we observe that the weak operational semantics we defined in Section 4.3 is a conservative extension of the weak (nonprobabilistic) operational semantics: indeed, when considering non-probabilistic processes, all distributions in the (labeled) operational semantics are Dirac distributions. Notation 5. We write SP np for the set of all nonprobabibilistic extended processes We write -→ np , respectively a -→ np , for the one-step reduction relation we obtain when we restrict the NPLTS N o to MP np , respectively N to SP np . For P, Q ∈ MP np , we write P ⇒ np Q when there exists a sequence

P = P 0 - → np . . . - → np P n = Q. Lemma 4. Let P, Q ∈ MP np . P ⇒ np Q iff RProb Rnr(N o ) (P, {Q}) = 1
We look now at preorder relations between nonprobabilistic processes. We first recall formally how may testing, trace equivalence and bisimulation are defined for non-probabilistic processes (Definition 16 below). Those definitions are coherent with those from the literature, e.g [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF], (up to the difference on static equivalence, discussed in Remark 4). Notation 6. If b is a barb, we write P ⇓ b when there exists Q such that P ⇒ np Q, and Q ↓ b . For a ∈ A ext , we write (P, φ)

a = =⇒ np (Q, ψ) when (P, φ) τ -→ np . . . a -→ np . . . τ -→ np (Q, ψ). If α = a 1 , . . . , a n is a trace, we write (P, φ) α = =⇒ np (Q, ψ)
when there exists a sequence (P, φ)

a1 = =⇒ np . . . an = =⇒ np (Q, ψ).
Definition 16. We define the binary relations ≤ np may , ≤ np tr , ≤ np sim on MP np as follows:

• P ≤ np may Q when ∀Adv ∈ MP np s.t. fn(Adv) ⊆ N pub . ∀c ∈ N pub . Adv ∪ P ⇓ c implies Adv ∪ Q ⇓ c ; • (P, φ) ≤ np tr (Q, ψ) when for every trace α, (P, φ) α = =⇒ np (P , φ ) implies (Q, ψ) α = =⇒ np (Q , ψ ); • ≤ np
sim is the largest reflexive and transitive relation R such that (P, φ) R (Q, ψ) implies that for every a ∈ A ext ∪ {τ }, and (P, φ)

a -→ np (P , φ ), there exists (Q , ψ ) such that (Q, ψ) a = =⇒ np (Q , ψ ) and (P , φ ) R (Q , ψ ).
The preorders ≤ sim and ≤ tr -and the corresponding equivalence relations-are conservative extensions of ≤ np sim and ≤ np tr . As expected, the preorder ≤ may is not a conservative extension of ≤ np may , because of the additional expressive power of probabilistic adversaries. Nonetheless, we can recover ≤ np may when we restrict the adversaries in the definition of ≤ may to non-probabilistic adversaries.

Proposition 2. Let P, Q ∈ MP np .

• (P, ∅) ≤ np sim (Q, ∅) iff (P, ∅) ≤ sim (Q, ∅); • (P, ∅) ≤ np tr (Q, ∅) iff (P, ∅) ≤ tr (Q, ∅); • (P, ∅) ≤ np may (Q, ∅) iff ∀Adv ∈ MP np s.t. fn(Adv) ⊆ N pub . ∀c ∈ N pub . RProb Rnr(N o ) (P ∪ Adv, ↓ c) ≤ RProb Rnr(N o ) (Q ∪ Adv, ↓ c)
Proof sketch. For may-testing and trace preorder, the proof uses crucially the fact that it is enough to consider nonrandomized distributions (thanks to Lemma 1), and from there, we conclude using Lemma 4. Since it is not possible to consider only non-randomized schedulers in the definition of simulation, the proof of the first point in Proposition 2 is more subtle, and uses well-structured properties of the lifting of a relation from Definition 9. We need to show (1) that the (non-probabilistic) simulation ≤ np sim is a probabilistic simulation in the sense of Definition 15, and (2) that ≤ sim is also a non-probabilistic simulation in the sense of Definition 16.

• Suppose that P ≤ np sim Q for P, Q ∈ SP np . Let a ∈ A ext ∪ {τ }, D ∈ D(S N ) such that P a -→ r D.
Looking at the way we defined a -→ r (and since P is nonprobabilistic), we also see that P a -→ np P i for every P i is the support of D. From there, we obtain that for each i, there exists

Q i such that Q a = =⇒ np Q i , and P i ≤ np sim Q i . At that point, we build E = i D(P i ) • δ Q i ,
and we can see that Q a = =⇒ r E. Moreover, the structural properties of the lifting allows us to go from (∀i, P i ≤ np sim Q i ) to D ≤ np sim E. Hence, we have shown that ≤ np sim is indeed a probabilistic simulation in the sense of Definition 15.

• Suppose that P ≤ sim Q for P, Q ∈ SP np . Let a ∈ A ext ∪ {τ }, and P ∈ SP np such that P a -→ np P . This transition carries over to N , i.e., P a -→ r δ P . We obtain that there exists a distribution E such that Q a = =⇒ r E, and δ P ≤ sim E. But by structural property of the lifting, we have that P ≤ sim Q for every element Q in the support of E. Moreover, since Q is non-probabilistic, it holds that Q a = =⇒ np Q for every element Q in the support of E. Since E is a distribution, there exists at least one such element Q , thus we can conclude.

The following result indicates that may testing and trace equivalence coincide in non-probabilistic settings. In particular, we recover the fact that for the classical definitions in non-probabilistic settings, trace equivalence implies maytesting, as shown in [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF].

Proposition 3. Let P, Q ∈ MP np . (P, ∅) ≤ tr (Q, ∅) iff ∀Adv ∈ MP np s.t. fn(Adv) ⊆ N pub . ∀c ∈ N pub . RProb Rnr(N o ) (P ∪ Adv, ↓ c) ≤ RProb Rnr(N o ) (Q ∪ Adv, ↓ c)
May-testing and simulation coincide for bounded processes. We rely on a modal characterization of strong simulation on image finite labeled transition systems (LTS) by a Hennessy-Milner logic [START_REF] Hennessy | On observing nondeterminism and concurrency[END_REF] (HML).

We can rely on strong simulation as it is a well-known fact ( [START_REF] Amadio | Operational methods in semantics[END_REF]) that simulation for a LTS can be expressed as strong simulation on the corresponding weak LTS, that is, in our case all transitions (P, φ) A LTS is image finite when the LTS cannot infinitely branch from a state and a label. Therefore, as we consider only bounded processes and by denoting ≤ L ssim the strong simulation relation on a LTS L, we can build an image finite LTS L such that for all P, Q ∈ MP np :

(P, ∅) ≤ sim (Q, ∅) iff (P, ∅) ≤ L ssim (Q, ∅)
Our HML characterization consists in expressing strong simulation preorder by the means of satisfaction of logical formulas by the LTS. Definition 17. Let A be a countable set of actions. We define the set of logical formulas as:

F ∈ F := | a.F | F 1 ∧ F 2 ,
where a ∈ A

In our case, the set of actions corresponds to A ext that is indeed countable. The satisfaction of such formulas by a LTS is defined as follows.

Definition 18. Let L = (S, A, →) be a LTS. We say that L satisfies a formula F , written s |= F , if for all s ∈ S,

• s |= ;

• s |= a.F when s a -→ t and t |= F ;

• s |= F 1 ∧ F 2 when s |= F 1 and s |= F 2 .
The following proposition shows how to relate strong simulation with satisfiability of logical formulas.

Proposition 4 (HML caracterisation of simulation). For an image finite LTS L,

s ≤ L ssim t iff ∀F ∈ F. s |= F implies t |= F
In order to prove that simulation coincides with maytesting for bounded non-probabilistic processes, we show that we can emulate any logical formula by a probabilistic adversary: for all formulas F , we build a probabilistic adversary Adv c F such that for all bounded non-probabilistic extended processes (P, φ),

(P, ∅) |= F iff RProb Rr (P ∪ { {Adv c F } }, ↓ c) = 1
We illustrate the construction of Adv c F on a few selected formulas:

Adv c in(ξ,ζ).F = out(ξ, ζ).Adv c F Adv c (ξ ? =ζ).F = if ξ = ζ then Adv c F Adv c F1∧F2 = Adv c F1 + 1 2 Adv c F2 Adv c = out(c, c)
In particular, conjunction is encoded by probabilistic choice and on formula , the adversary process exhibits the barb c. The main result of this section follows almost directly.

Proposition 5. Let P, Q ∈ MP <∞,np .

(P, ∅) ≤ sim (Q, ∅) iff P ≤ may Q

Cheval et al. have shown [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF] that both deciding trace equivalence and bisimilarity is coNEXPTIME complete when cryptographic primitives are modelled by a subterm convergent destructor rewrite system and the number of sessions is bounded. (We refer the reader to [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF] for a precise definition of this class of rewrite systems.) The hardness proof reduces SUCCINT 3SAT to both trace equivalence and bisimilarity using a same encoding which also proves hardness of similarity. The coNEXPTIME decision procedure for bisimilarity can be directly adapted to the case of similarity, hence, we have the following result.

Corollary 1. Let P, Q ∈ MP <∞,np . Deciding P ≈ may Q is coNEXPTIME complete when . = is defined by a subterm convergent destructor rewrite system.

May-testing and simulation do not coincide for unbounded processes. We consider the following two simple LTS L 1 and L 2 , that are an asymetric variant of the LTSs used in [START_REF] Van Glabbeek | Bounded nondeterminism and the approximation induction principle in process algebra[END_REF] to show that the finitary HML does not characterize bisimulation. Though both L 1 and L 2 may produce an unbounded number of a transitions, the initial transition in L 2 decides on an arbitrary, but fixed number of a transitions in the rest of the execution. This in particular shows that L 2 does not simulate L 1 , i.e., L 1 ≤ sim L 2 .

In the applied π-calculus, L 1 can be represented by the process !out(c, a). Modeling L 2 is more complex: we non-deterministically choose an integer n ≥ 0, and output n + 1 times a. The non deterministic choice of n is realized through the following process that outputs the unary encoding h n (b) of n: Similarly to Q count (e), Q out (e) relies on a private d to increment b until reaching the value x read on e. It is easy to see that the process outputs x + 1 times a.

Q count (e) = new

Lemma 5. Let

Q = new e.(Q count (e) | Q out (e)).
We have:

(!out(c, a), ∅) ≤ N sim (Q, ∅) but !out(c, a) ≤ may Q

Purely probabilistic processes

At the opposite of the spectrum of purely non-nondeterministic processes, we study purely probabilistic processes with (nearly) no non-determinism. A similar class of processes has been considered in [START_REF] Chadha | Verification of randomized security protocols[END_REF], [START_REF] Bauer | Model checking indistinguishability of randomized security protocols[END_REF] to model various protocols relying on randomization (e.g., Crowds [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF], mixnet [START_REF]Untraceable electronic mail, return addresses, and digital pseudonyms[END_REF], electronic voting [START_REF] Chaum | A practical voterverifiable election scheme[END_REF]). They consider systems that are built as the parallel composition of independant agents, called roles, and where all communications are mediated by the adversary. Moreover, the internal behavior of each role is deterministic; the only non-determinism is controlled by the adversary-thus external-and consists in the adversary's choice for scheduling the communications. We model purely probabilistic processes as follows. Definition 19. A process is fully determinate if it does not contain the operators +, |, nor !. P = {P 1 , . . . , P n } ∈ MP is purely probabilistic when:

• each P i is fully determinate;

• there exist distinct public channels c 1 , . . . , c n ∈ N pub such that for all i ∈ {1, . . . , n}, all input and output actions in P i are on c i . The class of purely probabilistic multisets of processes is denoted by MP pp .

MP pp can also be seen as a probabilistic extension of the class of simple processes introduced in [START_REF] Cortier | A method for proving observational equivalence[END_REF] to show that trace equivalence coincides with observational equivalence for such processes.

Removing scheduling of τ -actions. In [START_REF] Chadha | Verification of randomized security protocols[END_REF], [START_REF] Bauer | Model checking indistinguishability of randomized security protocols[END_REF], the authors consider trace equivalence for a slightly restricted fragment of purely probabilistic processes. More precisely, all processes have exactly the same control structure which removes the necessity of scheduling honest τ -actions and allows to directly consider strong trace equivalence, as exactly the same τ -actions occur. In this work, we lift this restriction on the shape of the processes and show instead that the nondeterminism related to honest τ actions is inconsequential when deciding trace equivalence. Indeed, in a multiset of processes {P 1 , . . . , P n }, a τ action may be available simultaneously in multiple components. However, all such τ -action are in fact purely deterministic (e.g., conditional branching, probabilistic choice). Moreover, as the P i s do not contain parallel composition and all input and output occur on distinct channels c i , no internal communication between processes P i and P j is possible.

We show that to compute the probability of executing a trace w, we only need to consider a single maximal resolution on the NPLTS N . Such a resolution always executes an action when at least one is available. Formally, a resolution (corr, R) with R = (S, A, trans) on purely probabilistic processes is maximal when for all s ∈ S, if there exists corr(s) a -→ D in N for some a, D then trans(s)(a) = D for some D . Proposition 6. Let (P, φ) be an extended purely probabilistic process. For all maximal resolutions (corr, R) on N , for all s ∈ S(R) with corr(s) = (P, φ),

∀w ∈ A ext . Prob R (s, w) = Prob R r ((P, φ), w).
May-testing and trace equivalence coincide for fully determinate adversaries. As illustrated in Example 3, maytesting is strictly stronger than trace equivalence even on purely probabilistic processes due to the non-determinism in the adversarial process. However, by restricting the adversarial process to be fully determinate, we can show that may-testing and trace equivalence coincide. We define the resulting determinate may testing preorder, denoted ≤ d-may , exactly as in Definition 7 but additionally restrict the adversary process Adv to be a singleton { {A} } where A is fully determinate.

Theorem 3. Let

P, Q ∈ MP pp . P ≤ d-may Q iff (P, ∅) ≤ tr (Q, ∅)
Proof sketch. To prove that (P, ∅) ≤ d-may (Q, ∅) implies P ≤ tr Q we encode any trace w into a determinate adversary Adv c w where c is fresh. Adv c w is defined in a similar way as Adv The other implication is more difficult as the adversarial process Adv is allowed to use probabilistic choices which cannot be directly encoded in a trace. Instead, we show that any adversarial process Adv aiming to exhibit a barb c corresponds to a multiset of weighted traces Tr(Adv), built inductively on Adv. For instance, when Adv = Adv 1 + p Adv 2 and

Tr(Adv i ) = { {(p i k , w i k )} } ni k=1 for i = 1, 2 then Tr(Adv) = { {(p • p 1 k , w 1 k )} } n1 k=1 ∪ { {((1 -p) • p 2 k , w 2 k )} } n2 k=1
For other constructs, the set of weighted traces is built as expected, e. Intuitively, exhibiting the barb on c does not require any interaction with the adversary, or this interaction is correctly encoded in Tr(Adv). Using this property we easily conclude.

Towards deciding trace equivalence. As previous mentioned, Cheval et al. [START_REF] Cheval | Deepsec: Deciding equivalence properties in security protocols -theory and practice[END_REF] designed a decision procedure for trace equivalence when cryptographic primitives are modelled by a subterm convergent destructor rewrite system and a bounded number of sessions. This procedure is based on constraint solving techniques that represent in a finite symbolic tree the infinite set of all possible concrete executions of the processes and an arbitrary attacker. Intuitively, each node of this symbolic tree represents the state of the two processes after executing a trace tr. Due to nondeterminism, a node may contain several constraint systems corresponding to every possible interleaving allowing the execution of such trace tr. Deciding trace equivalence between processes A and B, in the original, non-probabilistic setting, requires to check that each node of the symbolic tree contains at leat one constraint system derived from process A and one from process B; or the node is empty. For purely probabilistic processes, as there is no nondeterminism, we can associate to each constraint system the probability of executing this trace, depending on the probabilistic choices taken during the execution of the processes. Thus, using the same constraint solving techniques, we can compute a symbolic tree representing the state of the processes after executing trace tr but where the constraint systems of a node correspond to the possible probabilistic choices. Deciding trace equivalence between processes A and B thus reduces to checking that in every node, the sum of the probabilities of the constraint systems derived from the process A is equal to the sum of the probabilities of the constraint systems derived from B.

Conclusion and future work

In this paper we introduced a framework to reason about indistinguishability properties, modelled as process equivalences, in symbolic models enhanced with probabilities. Defining such a framework turns out to rely on subtle technicalities such as the need for randomized schedulers, overseen in previous attempts. In addition to solving technical problems, we believe that randomized schedulers capture more faithfully the idea that one cannot predict how nondeterminism is resolved. Randomized schedulers generalize the idea that one distribution is chosen non-deterministically by allowing an arbitrary combination (in the convex hull) of the available distributions.

We define different, classical behavioral and labelled equivalences and show their precise relations. As usual in models mixing non-determinism and probabilities, the resulting equivalences may be considered as too strong: indeed arbitrary schedulers may leak the (private) probabilistic choices of the processes and give the attacker an unrealistically strong distinguishing power. Defining more restricted schedulers that are only allowed partial knowledge of the current state, such as in [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF], is orthogonal to our work. We however believe that our work provides a convenient framework for defining such more fine-grained notions of schedulers and consider this an interesting direction for future work.

We therefore study two classes of protocols where this problem is avoided. First, we study protocols that do not make probabilistic choices, but allow the adversary to do so. This class of non-probabilistic protocols corresponds to the classical setting and captures all major case studies performed in the context of symbolic models. Our results highlight that the classical notion of may-testing, considered rather intuitive as it models an arbitrary attacker running in parallel, does not take into account attackers that make probabilistic choices. Interestingly, when bounding the number of sessions, (non-probabilistic) similarity exactly captures such probabilistic attackers and offers an attractive target for automated analysis. Second, we study a class of fully probabilistic protocols, also considered in [START_REF] Chadha | Verification of randomized security protocols[END_REF], and show that trace equivalence on such protocols coincides with may testing in the presence of a (syntactic) class of determinate attackers. One may indeed argue that determinacy removes artificial non-deterministic choices that the attacker could exploit and that correspond to unrealistic behaviors. When protocols can be expressed in the class of purely probabilistic processes, from a formal analysis point, it seems appealing to do so as it also simplifies the analysis.

Our work paves the road towards several future work, in addition to exploring restricted schedulers mentioned above. We sketched a decision procedure in the DeepSec tool for the class of fully probabilistic adversaries. A thorough treatment of this idea and an implementation are a natural next step. Also, the insight that (purely possibilistic) similarity takes into account probabilistic adversaries (as it coincides with may testing) when the number of sessions is bounded and protocols are non-deterministic motivates adding support for (bi)similarity in a tool such as DeepSec (which currently only verifies trace equivalence). A different direction going beyond the subclasses considered in this paper is to investigate restrictions of the scheduler (building, e.g., on ideas from [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF], [START_REF] Alvim | Safe equivalences for security properties[END_REF]) in our framework to limit the adversary's power without restricting the class of protocols. Finally, a more prospective direction is the use of more quantitative equivalences, i.e., distances between processes, that might be interesting to compare different protocols that try to achieve a same property.

≤

  nr denotes a preorder with non-randomized schedulers.

Figure 1 :

 1 Figure 1: Summary of the relationship between preorders.

Figure 2 :

 2 Figure 2: Semantics of the calculus

Figure 3 :

 3 Figure 3: Semantics of the process P from Example 2

Definition 4 (

 4 [START_REF] Bonchi | The theory of traces for systems with nondeterminism and probability[END_REF]). A randomized resolution for a NPLTS N = (S, A, trans) is a pair (corr, R) where• R = (S , A, trans ) is a RPLTS, and • corr : S → S is the correspondence function such that for all states s ∈ S , trans (s )(a) = D implies corr(D) ∈ conv(trans(corr(s ))(a)).

Figure 4 :

 4 Figure 4: Example of a randomized resolution for process P from Example 2 where the correspondence function corr is the identity.

Notation 4 .

 4 If D is a distribution over MP, and φ a frame, we write (D, φ) for the distribution over extended processes defined as (D, φ) = P∈supp(D) D(P) • δ (P,φ) . We now define the NPLTS N for the labelled semantics. External actions model interactions with the attacker. Definition 12. The labelled semantics is the NPLTS N = (SP , {τ } ∪ A ext , trans ) where • A ext is the set of labels in(ξ, ζ), out(ξ, ax), (ξ ? = ζ) and (ξ ? = ζ) with ξ, ζ recipes and ax ∈ AX ;

Figure 5 :Figure 6 :

 56 Figure 5: Labelled semantics: definition of → a

  For readability, α stands for all labels (ξ ∼ ξ ), with closed recipes ξ, ξ such that ξ ∼ ξ (∼ ∈ { . =, . =}) andP ab (p) = { {out(a, c) + p out(b, c)} } (a)The fragment of N corresponding to ({ {Q} }, ∅) and ({ {R} }, ∅).

  The resolution for ({ {R} }, ∅)τ = =⇒R nr 0.5 • δ out(a,c) + 0.5 • δ out(b,c) .

Figure 7 :

 7 Figure 7: Fragments of N showing ({ {P } }, ∅) ≤ nr

  c); (out(a, c) + 0.9 0) + out(d, c); (out(b, c) + 0.9 0)P = if c = c then P else 0 Q = P + 1 2 P Both ({ {Q} }, ∅) ≈ nr bi ({ {P } }, ∅) and ({ {Q} }, ∅) ≈ nr bi ({ {P } }, ∅) are proved by showing that the binary relation R, defined as the reflexive, symmetric and transitive closure of {(({ {Q} }, ∅), ({ {P } }, ∅)), (({ {P } }, ∅), ({ {P } }, ∅))}, is a bisimulation (see Figure8a).To prove that { {Q} } ≤ nr obs { {P } }, we show that { {Q; in(d, x).0} } ≤ nr obs { {P ; in(d, x).0} }. In particular (see Figure8b), we build a non-randomized scheduler such that { {Q; in(d, x).0} } τ = =⇒ Rnr(N o ) D where D = 0.45 • δ Pa + 0.45•δ P b +0.

  ψ) are merged into a single transition.

  d.(out(d, b) | !in(d, x).(out(e, x) + out(d, h(x))))Channel d represents a memory cell initiated with a public name b (encoding 0). When reading on d the current value x, the process non deterministically chooses to increment x (updating the cell with h(x)) or to select the value x by outputting it on channel e.It remains to model the process that given an integer x, produces x + 1 outputs of a: Q out (e) = new d .in(e, x).(out(d , b) | !in(d , y).out(c, a).if x = y then 0 else out(d , h(y)))

=

  c F (Section 5.1), e.g., Adv c in(ξ,ζ).w = out(ξ, ζ); Adv c w and Adv c if ξ = ζ then Adv c w In particular, on the empty trace the adversary process exhibits the barb c: Adv c ε = out(c, c). We obtain that Prob Rr(N ) ((P, ∅), w) = RProb R o r (P ∪ A dv , ↓ c)

  g., Tr(0) = ∅ and Tr(new a; Adv ) = Tr(Adv ). For outputs or inputs, we additionally test if the channel corresponds to the barb c, i.e., when Adv = out(ξ, ζ); Adv and Tr(Adv ) = { {(p k , w k )} } n k=1 , Tr(Adv) = { {(p k , (ξ ? = c).in(ξ, ζ).w k )} } n k=1 ∪ { {(1, ξ ? = c)} } This construction yields the following property: RProb Rnr(N o ) (P ∪ Adv, ↓ c) = RProb Rnr(N o ) (P, ↓ c) + (1 -RProb Rnr(N o ) (P, ↓ c))• (α,w)∈Tr(Adv) α • Prob Rnr(N ) ((P, ∅), w)

  . = is symmetric, transitive, and closed under substitution of names and variables by other terms and application of function symbols. Moreover, for all a, b ∈ N , a = b if and only if a . = b. Msg(•) is supposed to hold on any names, be closed under renamings and t 1 . = t 2 implies that Msg(t 1 ) and Msg(t 2 ). Finally, we require that

	Msg(t) implies t For example, the . = t. dec(enc(m, k), k) .	. = relation could capture that

  Msg(ζφ) and vars(ξ, ζ) ⊆ dom(φ) ({ {out(u, t); P } } ∪ P, φ) → out(ξ,axn+1) δ ({ {P } }∪P,φ{axn+1 →t}) if u . = ξφ, Msg(t), vars(ξ) ⊆ dom(φ) and |φ| = n (P, φ) → (ξ∼ζ) δ (P,φ) if vars(ξ, ζ) ⊆ dom(φ) and ξφ ∼ ζφ where ∼ ∈ { .

	=,	. =}

  1•δ ∅ . However, there is no distribution E such that { {P ; in(d, x).0} }

τ = =⇒ Rnr(N o ) E, and D ≤ nr obs E.

Acknowledgments. We thank Alwen Tiu and the anonymous reviewers for their helpful comments and suggestions. This work has been partly supported by the ANR Research and teaching chair in AI ASAP and by ANR TECAP (decision number ANR-17-CE39-0004-03).