Symbolic protocol verification with dice 1

Abstract

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 π-calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need for randomized schedulers and exhibit a counter-example to a result in a previous work that relied on non-randomized 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.

Keywords

Security protocols symbolic verification probabilistic process equivalences

1. Introduction

Automated symbolic protocol verification, based on the seminal work of Dolev and Yao [26], has nowadays reached a level of maturity enabling successful use on complex real-world security protocols, including TLS [7,23], Signal [19], authentication protocols of the 5G standard [4], or EMV’s secure payment protocols [5] 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 [22] (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 [14], mix-nets [13] or Crowds [32]. In this paper, we will investigate indistinguishability properties, expressed as equivalences in a cryptographic process calculus, the applied π-calculus [1], 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.

Fig. 1.

Summary of the relationship between preorders.

Our contributions. In a first part we introduce a probabilistic applied π-calculus and its semantics, which has similarities to [28], 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 [9,10,25,27,31,33,34]. (ii) More importantly, we differ in the way non-determinism is resolved: unlike [28] 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 Fig. 1, focusing on preorders (with similar relations between corresponding equivalences). We show, in particular, that

unlike in the purely non-deterministic case, the may-testing 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 ( $⩽_{sim}^{nr}$ and $⩽_{obs}^{nr}$ ) do not coincide (Lemma 4), which provides a counter-example to one of the main results in [28].

Third, a well-known phenomenon [2,12] 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}^{< \infty, 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 [25] 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 [18].

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 [16,20], and a slight generalization of the processes in [11]. We show that trace equivalence as considered in [11], is

weaker than may-testing, but

coincides with a version of may-testing with determinate attackers: attacker processes are restricted by disallowing replication, parallel, and non-deterministic choice, but allowing probabilistic choices (Theorem 3).

Next, we present an algorithm for deciding trace equivalence by extending the procedure of the DeepSec verifier [18]. Our procedure inherits some limitations (bounded number of sessions, the class of admissible rewrite systems) but provides a more general setting than Bauer et al. [6] who additionally bound the size of input messages. We have implemented our procedure in the open-source tool DeepSec available at [35].

Finally, we illustrate our framework by studying the Dining Cryptographers protocol. We notably provide a pen and paper proof that the protocol guarantees anonymity (expressed as may-testing equivalence). Using the DeepSec tool we also show that anonymity is not provided when coins are biased.

For readability, we often only provide proof sketches and omit some of the most technical proofs. A full version with more detailed proofs is available at [17].

2. 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. [28].

2.1. 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, \dots,}$ 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 π-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, \dots}$ . 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 \in N$ , $enc (a, k)$ represents the encryption of a with the key k. For any $F \subseteq F$ , $N \subseteq N$ and $V \subseteq X$ , the set of terms built from $N$ and $V$ by applying function symbols in $F$ is denoted by $T (F, N \cup 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 (\cdot)$ that is intended to hold when evaluation succeeds. How ≐ and $Msg (\cdot)$ 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 [1] (where $Msg (\cdot)$ 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 [18], or a combination of these as in the ProVerif tool [8].

Formally, we require that ≐ is symmetric, transitive, and closed under substitution of terms for names and variables, as well as application of function symbols. Moreover, for all $a, b \in N$ , $a = b$ if and only if $a ≐ b$ . $Msg (\cdot)$ 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 ≐ t$ .

For example, the ≐ relation could capture that $dec (enc (m, k), k) ≐ 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.

2.2. 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 \in T (F, N \cup X)

x \in X

a \in N

and

p \in] 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. We also denote by

fn (P)

the set of free names in P, i.e., the names not bound by a restriction, and by

n (P)

the set of all names occurring in P.

Example 1.
As an example, consider the process P: $\begin{matrix} (out (c, k) +_{\frac{1}{3}} out (c, a)) | in (c, x); if x = k then out (c, ok) \end{matrix}$ P consists of two parallel processes. The left process outputs on a channel c with probability $\frac{1}{3}$ the name k and with probability $\frac{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$ .
2.3. 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. [28] 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) \subseteq D^{⩽ 1} (S)$ ). For $p, q ⩾ 0$ , and sub-distributions D, E, we define the measure $\begin{matrix} (p \cdot D + q \cdot E) (x) = p \cdot D (x) + q \cdot E (x) . \end{matrix}$ When $q = 0$ , the resulting sub-distribution does not depend on E, and we simply write $p \cdot D$ instead of $p \cdot D + 0 \cdot E$ .

If $D \in D (S)$ , we denote by $supp (D)$ the support of D, i.e., the set of all elements $s \in S$ such that $D (s) > 0$ . If $S^{'} \subseteq S$ , we define $D (S^{'}) = \sum_{s \in 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 \to_{τ} μ$ . This relation is defined in Fig. 2.
Remark 1.
One may note that our calculus offers a non-deterministic choice operator that is resolved internally. This differs from the standard π-calculus [30] where the non-deterministic choice operator is resolved externally. Note that the original applied π-calculus [1] does not contain non-deterministic choice.

Fig. 2.
Semantics of the calculus.

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 [9]. 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. [33].
Definition 1.
A NPLTS is a triple $(S, A, trans)$ , where
$S$ is a set of states,

$A = {τ} ⊔ A_{ext}$ is a set of labels, and

$trans : S \to A \to P (D (S))$ is a transition function: for each state in $S$ , and each label in $A$ , $trans (s) (a)$ is a set of (finitely supported) distributions.
The label τ is the internal action and the labels in $A_{ext}$ are the external actions. For $s \in S$ , $a \in A$ , we write $s \overset{a}{\to} D$ when $D \in 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 \to A \to 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} = \emptyset$ . 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 \in MP$ , ${trans}^{o} (s) (τ) = {D | s \to_{τ} 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$ .

Fig. 3.
Semantics of the process P from Example 2.
Example 2.
The complete execution of the process P, introduced in Example 1 is given in Fig. 3.
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.

3.1. Resolving the internal non-determinism

Resolutions express how internal non-determinism of a NPLTS is resolved. Intuitively, resolving the non-determinism means, for each state, restricting the transition system either by choosing one particular internal transition, or else by leaving 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 \to D (S) ⊔ (A_{ext} \to D (S) \cup {⋆})$ 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 \in S$ such that $trans (s) : A_{ext} \to D (S) \cup {⋆}$ 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 $\begin{matrix} trans : S \to D (S) ⊔ (\emptyset \to D (S) \cup {⋆}) \end{matrix}$ of such RPLTS is rewritten as $\begin{matrix} trans : S \to D (S) ⊔ {⋆} \end{matrix}$ as for any set X, the cardinality of the set $(\emptyset \to 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 $Δ \subseteq D (S)$ , denoted $conv (Δ)$ , is the set of distributions $D \in D (S)$ such that $\begin{matrix} \exists α_{1}, \dots, α_{n} \in R . \exists D_{1}, \dots, D_{n} \in Δ . \sum_{i = 1}^{n} α_{i} = 1 and D = \sum_{i = 1}^{n} α_{i} \cdot D_{i} \end{matrix}$

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 \to S^{'}$ . We define the function $\overline{f} : D (S) \to D (S^{'})$ to be the probabilistic lifting of f, where $\begin{matrix} \overline{f} (D) = \sum_{s \in S} D (s) \cdot δ_{f (s)} \end{matrix}$

When obvious from context, we will overload the notation and write f instead of $\overline{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 \overset{a}{\to} D$ (i.e., $trans (s) = D$ ). Due to the possible existence of cycles in the NPLTS, a scheduler that visits 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.
Definition 4 ([9]).

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^{'} \to S$ is the correspondence function such that for all states $s^{'} \in S^{'}$ , ${trans}^{'} (s^{'}) (a) = D$ implies $corr (D) \in conv (trans (corr (s^{'})) (a))$ .

Given a NPLTS $N$ we denote by $R_{r} (N)$ the set of randomized resolutions. Additionally, we denote $R_{r}^{o} = R_{r} (N^{o})$ . Figure 4 shows an example of a resolution from $R_{r}^{o}$ for the process P from Example 2.

Fig. 4.

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

3.2. 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 \in N_{pub}$ and $P \in 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 \subseteq S$ a set of states, and s an initial state. For every $n \in N$ we define the probability of reaching $T$ from s in at most n steps as: $\begin{array}{c} {RProb}_{R}^{⩽ 0} (s, T) = \{\begin{array}{ll} 1 & if s \in T \\ 0 & otherwise . \end{array} \\ {RProb}_{R}^{⩽ n + 1} (s, T) = \{\begin{array}{ll} 1 & if s \in T \\ 0 & if s \notin T \land s \in S_{ext} (R) \\ \sum_{u \in supp (D)} D (u) \cdot {RProb}_{R}^{⩽ n} (u, T) \\ if s \notin T \land trans (s) (τ) = D \end{array} \end{array}$ We define the probability of reaching $T$ from s as: $\begin{matrix} {RProb}_{R} (s, T) = lim_{n \to + \infty} {RProb}_{R}^{⩽ n} (s, T) . \end{matrix}$

Note that, as ${RProb}_{R}^{⩽ n} (s, T)$ is an increasing function in n we can replace the limit by the supremum on $n \in N$ .

Given $N = (S_{N}, A, {trans}_{N})$ , we denote by ${RProb}_{R_{r} (N)} (s, T)$ the probability: $sup {{RProb}_{R} (s^{'}, {corr}^{- 1} (T)) | \begin{array}{c} (corr, R) \in R_{r} (N), \\ corr (s^{'}) = s \end{array}}$
3.3. 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 \in MP$ . We say that $P ⩽_{may} Q$ iff: $\begin{aligned} \forall Adv \in MP s.t. fn (Adv) \subseteq N_{pub} . \\ \forall c \in N_{pub} . \end{aligned} {RProb}_{R_{r}^{o}} (P \cup Adv, ↓ c) ⩽ {RProb}_{R_{r}^{o}} (Q \cup Adv, ↓ c)$

We say that $P$ , $Q$ are may testing equivalent, denoted $P \approx_{may}^{} Q$ , when $P ⩽_{may} Q$ and $Q ⩽_{may} P$ .

Remark 3.
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) \in R_{r} (N)$ and state s of R such that $corr (s) = P \cup Adv$ , there exist a resolution $({corr}^{'}, R^{'})$ and a state $s^{'}$ of $R^{'}$ such that ${corr}^{'} (s^{'}) = Q \cup Adv$ and $\begin{matrix} {RProb}_{R} (s, {corr}^{- 1} (↓ c)) = {RProb}_{R^{'}} (s^{'}, {corr}^{' - 1} (↓ c)) \end{matrix}$

However, the resulting relation is counter-intuitive and distinguishes processes $\begin{matrix} P : = {{out (a, 0)}} and Q : = {{out (a, 0) +_{\frac{1}{2}} (out (a, 0) +_{\frac{1}{2}} out (a, 0))}} . \end{matrix}$ Indeed, we can show that $Q ≰_{may}^{'} P$ : for $Adv = {{0}}$ , there exists a resolution $(corr, R)$ such that $\begin{matrix} corr (s) = P \cup Adv and {RProb}_{R} (Q, ↓ a) = \frac{1}{2} \end{matrix}$ but for every resolution $({corr}^{'}, R^{'})$ such that ${corr}^{'} (s^{'}) = Q \cup Adv$ , $\begin{matrix} {RProb}_{R^{'}} (P, ↓ a) = 1 . \end{matrix}$

3.4. 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 ${\overset{τ}{\to}}^{*}$ . However, in our setting we need to compute the corresponding distributions.

Definition 8.
Let $N$ be a NPLTS and $D, E \in D^{⩽ 1} (S_{N})$ .

We write $D {\overset{τ}{\Rightarrow}}_{R_{r} (N)} E$ when there exists $(corr, R) \in R_{r} (N)$ and $D^{'}, E^{'} \in D^{⩽ 1} (S_{R})$ such that
$corr (D^{'}) = D$ , $corr (E^{'}) = E$ , $supp (E^{'}) \subseteq S_{ext} (R)$ ,

$\forall u \in S_{ext} (R) . E^{'} (u) = \sum_{s^{'} \in S_{R}} D^{'} (s^{'}) \cdot {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 $\hat{R}$ , defined as: $\begin{matrix} D \hat{R} E when \forall S^{'} \subseteq S, D (S^{'}) ⩽ E (R (S^{'})) \end{matrix}$ where $R (S^{'}) = {s \in S | s^{'} \in S^{'} \land 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:
$\forall c \in N_{pub} . {RProb}_{R_{r}^{o}} (P, ↓ c) ⩽ {RProb}_{R_{r}^{o}} (Q, ↓ c)$ ;

if $P {\overset{τ}{\Rightarrow}}_{R_{r}^{o}} D$ and $D \in D (S_{N^{o}})$ then $Q {\overset{τ}{\Rightarrow}}_{R_{r}^{o}} E$ , $E \in D (S_{N^{o}})$ and $D \hat{R} E$ ;

∀ closed $Adv \in MP$ such that $fn (Adv) \subseteq N_{pub}$ . ${Adv} \cup P R {Adv} \cup Q$ .
The observational equivalence $\approx_{obs}^{}$ is defined by additionally requiring $R$ to be symmetric.
Remark 4.
Note that we slightly diverge from the original definition of observational equivalence [1] where an evaluation context $C [_]$ is of the form $\begin{matrix} new n_{1}; \dots; new n_{k}; (_| A) \end{matrix}$ In our definition we simply consider a parallel process, and no additional name restriction. However, we now show that these two definitions coincide. Intuitively, restricting names whose scope includes the adversarial process A does not provide additional distinguishing power and these names could as well be public. While this result is of independent interest, the reader may safely skip the remainder of this section without hindering their understanding of the rest of the paper.

Our distinction between private and public names enforces that all restricted names $n_{1}, \dots, n_{k}$ are in $N_{priv}$ . Applying an adversarial context with restriction in our formalism corresponds to applying a renaming from public to fresh private names. Hence, in our formalism the original observational equivalence can be defined as follows. Definition 11.
The original observational preorder $⩽_{ori}^{R}$ is the largest relation $R$ on $MP$ such that $P R Q$ implies:
for all $c \in N_{pub}$ , ${RProb}_{R} (P, ↓ c) ⩽ {RProb}_{R} (Q, ↓ c)$ ;

if $P {\overset{τ}{\Rightarrow}}_{r} D$ then $Q {\overset{τ}{\Rightarrow}}_{r} E$ and $D \hat{R} E$ ;

for all closed $Adv \in MP$ , for all renaming ρ, if $fn (Adv) \subseteq N_{pub}$ , $dom (ρ) \subseteq N_{pub}$ , $img (ρ) \subseteq N_{priv}$ and $img (ρ) \cap n (P, Q, Adv) = \emptyset$ then ${Adv ρ} \cup P ρ R {Adv ρ} \cup Q ρ$ .
The original observational equivalence $\approx_{ori}^{R}$ is defined by additionally requesting $R$ to be symmetric and in the second bullet point, by requesting both $D \hat{R} E$ and $E \hat{R} D$ to hold.

We now show that the two notions coincide. Intuitively, restricting names whose scope includes the adversarial process $Adv$ corresponds to making previously public channels invisible to the attacker at later steps, which does not provide additional distinguishing power. Lemma 1.
$⩽_{ori}^{R} = ⩽_{obs}^{R}$ and $\approx_{ori}^{R} = \approx_{obs}^{R}$ .
Proof.
Taking ρ to be the empty renaming, we have that $⩽_{ori}^{R} \subseteq ⩽_{obs}^{R}$ and $\approx_{ori}^{R} \subseteq \approx_{obs}^{R}$ .

Define the relation $R$ as $P R Q$ iff there exists $P^{'}$ , $Q^{'}$ and a renaming ρ such that $P = P^{'} ρ$ , $Q = Q^{'} ρ$ , $P^{'} ⩽_{obs}^{R} Q^{'}$ , $dom (ρ) \subseteq N_{pub}$ , $img (ρ) \subseteq N_{priv}$ and $img (ρ) \cap n (P^{'}, Q^{'}, Adv) = \emptyset$ .

As ≐ is closed under substitution of names by terms, we can show that $P ρ \to_{τ} D ρ$ iff $P \to_{τ} D$ . This can be propagate to schedulers, i.e. $(corr, R) \in R_{r}^{o}$ if and only if $(corr ρ, R) \in R_{r}^{o}$ . Hence, we derive that
${RProb}_{R_{r}^{o}} (P, T) = {RProb}_{R_{r}^{o}} (P ρ, T ρ)$

$D {\overset{τ}{\Rightarrow}}_{R_{r}^{o}} E$ if and only if $D ρ {\overset{τ}{\Rightarrow}}_{R_{r}^{o}} E ρ$
We now show that $R$ satisfies the three items in Definition 11:
Let $c \in N_{pub}$ . If $c \in dom (ρ)$ then c does neither occur in $P^{'} ρ$ nor in $Q^{'} ρ$ . Hence, ${RProb}_{R_{r}^{o}} (P^{'}, ↓ c) = 0 = {RProb}_{R_{r}^{o}} (Q^{'}, ↓ c)$ . Otherwise, $↓ c = ↓ c ρ \cup T$ where for all $P^{'} \in T$ , $fn (P^{'}) \cap dom (ρ) \neq \emptyset$ . Since, $P^{'} ρ$ and $Q^{'} ρ$ do not contain public names from $dom (ρ)$ , they can never reach states from $T$ . Hence, ${RProb}_{R_{r}^{o}} (P^{'} ρ, ↓ c) = {RProb}_{R_{r}^{o}} (P^{'} ρ, ↓ c ρ) = {RProb}_{R_{r}^{o}} (P^{'}, ↓ c)$ . Since $P^{'} ⩽_{obs}^{R} Q^{'}$ , we deduce that $\begin{matrix} {RProb}_{R_{r}^{o}} (P^{'}, ↓ c) ⩽ {RProb}_{R_{r}^{o}} (Q^{'}, ↓ c) ⩽ {RProb}_{R_{r}^{o}} (Q^{'} ρ, ↓ c ρ) ⩽ {RProb}_{R_{r}^{o}} (Q^{'}, ↓ c) \end{matrix}$

If $P ρ {\overset{τ}{\Rightarrow}}_{R_{r}^{o}} D ρ$ then $P^{'} {\overset{τ}{\Rightarrow}}_{R_{r}^{o}} D$ . By $P^{'} ⩽_{obs}^{R} Q^{'}$ , we have $Q^{'} {\overset{τ}{\Rightarrow}}_{R_{r}^{o}} E$ and $D \hat{⩽_{obs}^{R}} E$ . This implies that $D ρ \hat{R} E ρ$ with $Q^{'} ρ {\overset{τ}{\Rightarrow}}_{R_{r}^{o}} E ρ$ .

Let $Adv \in MP$ and $ρ^{'}$ be a renaming such that $fn (Adv) \subseteq N_{pub}$ , $dom (ρ^{'}) \subseteq N_{pub}$ , $img (ρ^{'}) \subseteq N_{priv}$ and $img (ρ^{'}) \cap n (P^{'} ρ, Q^{'} ρ) = \emptyset$ . Note that the domains of ρ and $ρ^{'}$ may not be disjoint. Similarly, the process $Adv$ may contain public names from $dom (ρ)$ .

Hence, let $ρ_{pub}$ be a renaming such that $dom (ρ_{pub}) = dom (ρ) \cap (dom (ρ^{'}) \cup fn (Adv))$ , $img (ρ_{pub}) \subseteq N_{pub} ∖ fn (P^{'}, Q^{'}, Adv)$ . Hence, we define $ρ_{1} = ρ ρ_{pub}^{- 1} ρ^{'}$ .

We have $P^{'} ρ_{1} = (P^{'} ρ) ρ^{'}$ since $img (ρ_{pub}) \subseteq N_{pub} ∖ fn (P^{'}, Q^{'}, Adv)$ . Moreover, as $dom (ρ_{pub}) = dom (ρ) \cap (dom (ρ^{'}) \cup fn (Adv))$ , we have that $\begin{matrix} (Adv ρ_{pub}) ρ = Adv ρ_{pub} ρ |_{dom (ρ) ∖ dom (ρ_{pub})} = Adv ρ |_{dom (ρ) ∖ dom (ρ_{pub})} ρ_{pub} = Adv ρ_{pub} \end{matrix}$ Therefore, $Adv ρ_{pub} ρ_{1} = Adv ρ_{pub} ρ_{pub}^{- 1} ρ^{'} = Adv ρ^{'}$ . This allows us to deduce that ${Adv ρ^{'}} \cup P^{'} ρ^{'} = ({Adv ρ_{pub}} \cup P^{'}) ρ_{1}$ . Similarly, we have ${Adv ρ^{'}} \cup Q^{'} ρ^{'} = ({Adv ρ_{pub}} \cup Q^{'}) ρ_{1}$ .

We know that $P^{'} ⩽_{obs}^{R} Q^{'}$ . Hence ${Adv ρ_{pub}} \cup P^{'} ⩽_{obs}^{R} {Adv ρ_{pub}} \cup Q^{'}$ which allows us to conclude that ${Adv ρ_{pub} ρ_{1}} \cup P^{'} ρ_{1} R {Adv ρ_{pub} ρ_{1}} \cup Q^{'} ρ_{1}$ and so ${Adv ρ^{'}} \cup P ρ^{'} R {Adv ρ^{'}} \cup Q ρ^{'}$ .
□

4. Labelled semantics and equivalences

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

4.1. 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}, \dots}$ distinct from $X$ that will act as pointers to messages that were previously output.

Definition 12.
An extended process is a pair $(P, ϕ)$ , where $P \in MP$ and ϕ is a ground substitution $\begin{matrix} {{ax}_{1} \mapsto t_{1}; \dots; {ax}_{n} \mapsto t_{n}} \end{matrix}$ such that ${ax}_{i} \in AX$ , $t_{i} \in 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} \cup AX}$ representing how an attacker can deduce a message.
Notation 4.
If D is a distribution over $MP$ , and ϕ a frame, we write $(D, ϕ)$ for the distribution over extended processes defined as $(D, ϕ) = \sum_{P \in supp (D)} D (P) \cdot δ_{(P, ϕ)}$ .

We now define the NPLTS $N^{ℓ}$ for the labelled semantics. External actions model interactions with the attacker.
Definition 13.
The labelled semantics is the NPLTS $N^{ℓ} = ({SP}_{ℓ}, {τ} \cup A_{ext}^{ℓ}, {trans}^{ℓ})$ where
$A_{ext}^{ℓ}$ is the set of labels $in (ξ, ζ)$ , $out (ξ, ax)$ , $(ξ \overset{?}{=} ζ)$ and with ξ, ζ recipes and $ax \in AX$ ;

${trans}^{ℓ} ((P, ϕ)) (a) = {D | (P, ϕ) \to_{a} D}$ where $\to_{a}$ is defined in Fig. 5.

Fig. 5.
Labelled semantics: definition of $\to_{a}$ .

Note that when we lift $\to_{τ}$ to extended processes we suppose that the freshness requirement of a new name $a^{'}$ in the (New) rule of Fig. 2 also applies to the frame ϕ, i.e., $a^{'}$ must not appear in ϕ.
Remark 5.
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 [28]: we encode static equivalence into the NPLTS $N^{ℓ}$ by a countable set of actions–all the tests $(ξ \overset{?}{=} ζ)$ 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.
4.2. 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 14.
Let $R = (S, {τ} ⊔ A_{ext}, trans)$ be a RPLTS. Let $w \in {A_{ext}}^{}$ be a trace, i.e., a finite word on the alphabet $A_{ext}$ . For all states $s \in S$ , we define the probability of executing w starting from s in R* as:
${Prob}_{R} (s, ϵ) = 1$

${Prob}_{R} (s, a . w) = \sum_{\begin{array}{c} t \in S \\ trans (t) (a) = D \end{array}} {RProb}_{R} (s, {t}) \cdot \sum_{s^{'} \in supp (D)} D (s^{'}) \cdot {Prob}_{R} (s^{'}, w)$

Given a NPLTS $N = (S, A, trans)$ , we denote by ${Prob}_{R_{r} (N)} (s, w)$ the probability: $\begin{matrix} sup {{Prob}_{R} (s^{'}, w) | (corr, R) \in R_{r} (N), corr (s^{'}) = s} \end{matrix}$

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 15 (trace equivalence).

Let $(P, ϕ)$ , $(P^{'}, ϕ^{'}) \in {SP}_{ℓ}$ . We say that $(P, ϕ) ⩽_{tr} (P^{'}, ϕ^{'})$ iff $\begin{matrix} for all w \in {A_{ext}^{ℓ}}^{*} . {Prob}_{R_{r} (N^{ℓ})} ((P, ϕ), w) ⩽ {Prob}_{R_{r} (N^{ℓ})} ((P^{'}, ϕ^{'}), w) \end{matrix}$ $(P, ϕ)$ and $(P^{'}, ϕ^{'})$ are trace equivalent, denoted $(P, ϕ) \approx_{tr}^{} (P^{'}, ϕ^{'})$ , iff $\begin{matrix} (P, ϕ) ⩽_{tr} (P^{'}, ϕ^{'}) and (P^{'}, ϕ^{'}) ⩽_{tr} (P, ϕ) . \end{matrix}$

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 \in MP$ be two processes. $\begin{matrix} P ⩽_{may} Q \Rightarrow (P, \emptyset) ⩽_{tr} (Q, \emptyset) \end{matrix}$ Moreover there exist processes $P, Q \in MP$ such that $\begin{matrix} (P, \emptyset) ⩽_{tr} (Q, \emptyset) and P ≰_{may} Q \end{matrix}$

Fig. 6.
$P$ , $Q$ such that $(P, \emptyset) ⩽_{tr} (Q, \emptyset) 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 $\frac{2}{3}$ in $P$ and only $\frac{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., [16]. This discrepancy comes from our choice of labelled actions for static equivalence (see Remark 5): 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.
4.3. Defining (bi)simulations

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 [33]. 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 \in A_{ext}^{ℓ}$ and two distributions $D, D^{'} \in D (S)$ , we write $D {\overset{a}{\Rightarrow}}_{R_{r}^{ℓ}} D^{'}$ when $D {\overset{τ}{\Rightarrow}}_{R_{r}^{ℓ}} E_{1}$ , $E_{1} \overset{a}{\to} E_{2}$ and $E_{2} {\overset{τ}{\Rightarrow}}_{R_{r}^{ℓ}} D^{'}$ for some $E_{1}$ , $E_{2}$ and where $R_{r}^{ℓ}$ denotes $R_{r} (N^{ℓ})$ . Here $E_{1} \overset{a}{\to} E_{2}$ is the natural lifting of the transition function of $N^{ℓ}$ , i.e., $E_{2} = \sum_{s} E_{1} (s) \cdot D$ with $s \overset{a}{\to} D$ .

Definition 16.
A relation $R \subseteq (S_{N^{ℓ}} \times S_{N^{ℓ}})$ is
a simulation if $s_{1} R s_{2}$ implies that for all $a \in A_{ext}^{ℓ} \cup {τ}$ , $D_{1} \in D (S_{N^{ℓ}})$ $\begin{matrix} if s_{1} \overset{a}{\to} D_{1} then s_{2} {\overset{a}{\Rightarrow}}_{R_{r}^{ℓ}} D_{2}, D_{2} \in D (S_{N^{ℓ}}) and D_{1} \hat{R} D_{2} \end{matrix}$

a bisimulation if R is a simulation and R is symmetric.
The simulation preorder, denoted $⩽_{sim}$ , is the largest simulation and bisimilarity, denoted $\approx_{bi}^{}$ , is the largest bisimulation. We define similarity, denoted $\approx_{sim}^{}$ , as $⩽_{sim} \cap ⩽_{sim}^{- 1}$ .

As usual in the field of (bi)simulation, it can be shown that $⩽_{sim}$ , respectively $\approx_{bi}^{}$ , exists [27] and that it is a pre-order, i.e., a reflexive and transitive relation, respectively an equivalence, i.e., a reflexive, symmetric and transitive relation [34].

The following proposition from [34] states that, as usual in the non-probabilistic case, the weak arrow ${\overset{a}{\Rightarrow}}_{R_{r}^{ℓ}}$ can replace the single arrow $\overset{a}{\to}$ 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 \in A_{ext} \cup {τ}$ , $\begin{matrix} if s_{1} {\overset{a}{\Rightarrow}}_{R_{r}^{ℓ}} D_{1} then s_{2} {\overset{a}{\Rightarrow}}_{R_{r}^{ℓ}} D_{2}, D_{2} \in D (S_{N^{ℓ}}) and D_{1} \hat{R} D_{2} \end{matrix}$ We have $R = ⩽_{sim}$ .
Remark 6.
Observe that our choice of labelled actions for static equivalence (see Remark 5) has no impact on the resulting simulation and bisimulation. Indeed, if two $N^{ℓ}$ -states $(P, ϕ)$ and $(Q, ψ)$ are in the simulation pre-order or bisimulation, then ϕ is statically equivalent to ψ. Indeed, for all $a \in {ξ \overset{?}{=} ζ, ξ \overset{?}{\neq} ζ}$ , $δ_{(P, ϕ)} \overset{a}{\to} δ_{(P, ϕ)}$ implies that $δ_{(Q, ψ)} {\overset{a}{\Rightarrow}}_{R_{r}^{ℓ}} D$ and $δ_{(P, ϕ)} \hat{⩽_{sim}} D$ . Since neither the a transition or τ transition modifies the frame, the former indicates that $δ_{(Q, ψ)} {\overset{τ}{\Rightarrow}}_{R_{r}^{ℓ}} E_{1}$ , $E_{1} \overset{a}{\to} E_{2}$ and $E_{2} {\overset{τ}{\Rightarrow}}_{R_{r}^{ℓ}} D$ , with for all $(Q^{'}, ψ^{'}) \in supp (E_{1})$ , $ψ = ψ^{'}$ . The former ensures that $supp (E_{1}) \neq \emptyset$ . Therefore, for all ξ, ζ, if $ξ \overset{?}{=} ζ$ or $ξ \overset{?}{\neq} ζ$ holds on ϕ then it also holds on ψ respectively. It implies that ϕ and ψ are statically equivalent.

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$ . $\begin{matrix} P ⩽_{obs} Q iff (P, \emptyset) ⩽_{sim} (Q, \emptyset) and P \approx_{obs}^{} Q iff (P, \emptyset) \approx_{bi}^{} (Q, \emptyset) \end{matrix}$
Proof sketch.
We here provide the main intuitions of the proof that $P ⩽_{obs} Q$ iff $(P, \emptyset) ⩽_{sim} (Q, \emptyset)$ .

(⇒). 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} \in 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 $\begin{matrix} (P, ϕ) R (Q, ϕ^{'}) if P \cup {{out (c_{i}, {ax}_{i} ϕ)}}_{i = 1}^{n} ⩽_{obs} Q \cup {{out (c_{i}, {ax}_{i} ϕ^{'})}}_{i = 1}^{n} \end{matrix}$ with $| dom (ϕ) | = | dom (ϕ^{'}) | = n$ and $c_{1}, \dots, c_{n} \in 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 $\begin{matrix} P_{1} = P \cup {{out (c_{i}, {ax}_{i} ϕ)}}_{i = 1}^{n} \end{matrix}$ 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 $ξ \overset{?}{=} ζ$ , 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: $\begin{matrix} Adv = in (c_{1}, x_{1}); \dots; in (c_{n}, x_{n}); if ξ ρ = ζ ρ then out (ok, ok) \end{matrix}$ where $x_{1}, \dots, x_{n}$ are fresh variables and $ρ = {{ax}_{i} \mapsto x_{i}}_{i = 1}^{n}$ . We then consider the transition $\begin{matrix} {{Adv}} \cup P_{1} {\overset{τ}{\Rightarrow}}_{R_{r}^{o}} δ_{P \cup out (ok, ok)} \end{matrix}$ and the fact that ${RProb}_{R_{r}} (P \cup out (ok, ok), ↓ ok) = 1$ to conclude. Indeed, for $\begin{matrix} {{Adv}} \cup Q \cup {{out (c_{i}, {ax}_{i} ϕ^{'}) .0}}_{i = 1}^{n} {\overset{τ}{\Rightarrow}}_{r} E \end{matrix}$ to exist with $δ_{P \cup out (ok, ok)} \hat{R} E$ , ${{Adv}} \cup Q \cup {{out (c_{i}, {ax}_{i} ϕ^{'}); 0}}_{i = 1}^{n}$ must also have passed the test $ξ ρ = ζ ρ$ in the conditional branching. Hence $ξ ϕ^{'} = ζ ϕ^{'}$ and so $(Q, ϕ^{'}) \overset{ξ \overset{?}{=} ζ}{\to} δ_{(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} \cup {{in (c, x); P}}$ with $ξ ϕ ≐ c$ , $(P, ϕ) \overset{in (ξ, ζ)}{\to} δ_{P_{1} \cup {{P σ}}}$ and $σ = {^{ζ ϕ} /_{x}}$ .

We consider the following adversarial process $Adv$ : $\begin{matrix} Adv = in (c_{1}, x_{1}); \dots; in (c_{n}, x_{n}); out (ξ ρ, ζ ρ); (out (ok, ok) +_{0.5} (out (c_{1}^{'}, x_{1}) | \dots | out (c_{n}^{'}, x_{n}))) \end{matrix}$ where $c_{1}^{'}, \dots, c_{n}^{'}$ are fresh public names pairwise distinct not occurring anywhere else. We will conclude by considering the transition $\begin{matrix} {{Adv}} \cup P \cup {{out (c_{i}, {ax}_{i} ϕ); 0}}_{i = 1}^{n} {\overset{τ}{\Rightarrow}}_{r} D \end{matrix}$ where $D = 0.5 \cdot δ_{P_{1} \cup {{P {^{ζ ϕ} /_{x}}, out (ok, ok)}}} + 0.5 \cdot δ_{P_{1} \cup {{P {ζ ϕ /_{x}}}} \cup {{out (c_{i}^{'}, {ax}_{i} ϕ); 0}}_{i = 1}^{n}}$ . Indeed, for $\begin{matrix} {{Adv}} \cup Q \cup {{out (c_{i}, {ax}_{i} ϕ^{'}); 0}}_{i = 1}^{n} {\overset{τ}{\Rightarrow}}_{r} E \end{matrix}$ to exist with $D \hat{R} E$ , ${{Adv}} \cup Q \cup {{out (c_{i}, {ax}_{i} ϕ^{'}); 0}}_{i = 1}^{n}$ 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} ρ \cup P_{Att} {^{{ax}_{i} ϕ} /_{x_{i}}}_{i = 1}^{n} ρ$ ;

$Q = Q_{1} ρ \cup P_{Att} {^{{ax}_{i} ϕ^{'}} /_{x_{i}}}_{i = 1}^{n} ρ$ ;

$(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 $ϕ^{'}$ ). □

4.4. 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 [28]. A non-randomized 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) \in conv (trans (corr (s^{'})) (a))$ , a non-randomized resolution requires that ${trans}^{'} (s^{'}) (a) = D$ implies $corr (D) \in 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}_{R_{nr} (N)} (s, T)$ the probability of reaching $T$ from s over all non randomized schedulers $R_{nr} (N)$ . Similarly, ${Prob}_{R_{nr} (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 $⩽_{may}^{nr}$ and $⩽_{tr}^{nr}$ 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 2.
May testing and trace preorders with randomized and non-randomized resolutions coincide: $\begin{matrix} ⩽_{may} = ⩽_{may}^{nr} and ⩽_{tr} = ⩽_{tr}^{nr} \end{matrix}$
Proof sketch.
The core of the proof is the following fact: when we fix a randomized resolution R, an initial state s, and $n \in 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 \in I}$ (where the weight $α_{i}$ is a coefficient in $[0, 1]$ , in the sense that for every set of processes $P$ , ${RProb}_{R}^{⩽ n} (s, P) = \sum_{i \in I} α_{i} {RProb}_{R_{i}}^{⩽ n} (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 [24,27], 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 {\overset{τ}{\Rightarrow}}_{R_{r} (N)} E$ to non-randomized scheduler, denoted $D {\overset{τ}{\Rightarrow}}_{R_{nr} (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 $⩽_{sim}^{nr}$ (and similarly for $⩽_{obs}^{nr}$ , $\approx_{obs}^{nr}$ and $\approx_{bi}^{nr}$ ).

Fig. 7.
Fragments of $N^{ℓ}$ showing $({{P}}, \emptyset) ⩽_{sim}^{nr} ({{R}}, \emptyset) ⩽_{sim}^{nr} ({{Q}}, \emptyset)$ but $({{P}}, \emptyset) ≰_{sim}^{nr} ({{Q}}, \emptyset)$ .
Lemma 3.
$⩽_{sim}^{nr}$ is not transitive.
Proof sketch.
Consider processes $\begin{array}{c} 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^{'} \end{array}$ The corresponding fragment of $N^{ℓ}$ is displayed in Fig. 7a. We will show that $\begin{matrix} ({{P}}, \emptyset) ⩽_{sim}^{nr} ({{R}}, \emptyset) and ({{R}}, \emptyset) ⩽_{sim}^{nr} ({{Q}}, \emptyset) but ({{P}}, \emptyset) ≰_{sim}^{nr} ({{Q}}, \emptyset) \end{matrix}$

It is easy to see that $({{Q}}, \emptyset) \approx_{bi}^{nr} ({{Q^{'}}}, \emptyset)$ and so $({{R}}, \emptyset) ⩽_{sim}^{nr} ({{Q}}, \emptyset)$ . The difficult part of the proof of $({{P}}, \emptyset) ⩽_{sim}^{nr} ({{R}}, \emptyset)$ is to match $\begin{matrix} ({{P}}, \emptyset) \overset{τ}{\to} 0.5 \cdot δ_{({{out (a, c)}}, \emptyset)} + 0.5 \cdot δ_{({{out (b, c)}}, \emptyset)} \end{matrix}$ This is achieved by the scheduler displayed in Fig. 7b.

Finally, we prove $({{P}}, \emptyset) ≰_{sim}^{nr} ({{R}}, \emptyset)$ by showing that the transition $({{P}}, \emptyset) \overset{τ}{\to} 0.5 \cdot δ_{({{out (a, c)}}, \emptyset)} + 0.5 \cdot δ_{({{out (b, c)}}, \emptyset)}$ cannot be simulated in $({{Q}}, \emptyset)$ . □

Note that the definitions of bisimilarity in [28] 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 $\approx_{bi}^{nr}$ and $\approx_{obs}^{nr}$ do not coincide, hence disproving [28, Theorem 2]. This reenforces our belief that it is preferable to use randomized schedulers in our definition.

Fig. 8.
Fragments of NPLTS showing $({{Q}}, \emptyset) \approx_{bi}^{nr} ({{P}}, \emptyset)$ and ${{Q}} ≰_{obs}^{nr} {{P}}$ .
Lemma 4.
There exist processes $P, Q \in SP$ such that
$({{Q}}, \emptyset) \approx_{bi}^{} ({{P}}, \emptyset)$ ,

$({{Q}}, \emptyset) \approx_{bi}^{nr} ({{P}}, \emptyset)$ , and

${{Q}} ≰_{obs}^{nr} {{P}}$ .

Proof sketch.
We consider the following processes: $\begin{array}{c} \begin{aligned} P & = out (d, c); (out (a, c) +_{0.9} 0) \\ + out (d, c); (out (b, c) +_{0.9} 0) \end{aligned} \\ P^{'} = if c = c then P else 0 \\ Q = P +_{\frac{1}{2}} P^{'} \end{array}$

Both $({{Q}}, \emptyset) \approx_{bi}^{nr} ({{P}}, \emptyset)$ and $({{Q}}, \emptyset) \approx_{bi}^{nr} ({{P}}, \emptyset)$ are proved by showing that the binary relation R, defined as the reflexive, symmetric and transitive closure of ${(({{Q}}, \emptyset), ({{P}}, \emptyset)), (({{P}}, \emptyset), ({{P^{'}}}, \emptyset))}$ , is a bisimulation (see Fig. 8a).

To prove that ${{Q}} ≰_{obs}^{nr} {{P}}$ , we show that ${{Q; in (d, x) .0}} ≰_{obs}^{nr} {{P; in (d, x) .0}}$ . In particular (see Fig. 8b), we build a non-randomized scheduler such that ${{Q; in (d, x) .0}} {\overset{τ}{\Rightarrow}}_{R_{nr} (N^{o})} D$ where $D = 0.45 \cdot δ_{P_{a}} + 0.45 \cdot δ_{P_{b}} + 0.1 \cdot δ_{\emptyset}$ . However, there is no distribution E such that ${{P; in (d, x) .0}} {\overset{τ}{\Rightarrow}}_{R_{nr} (N^{o})} E$ , and $D \hat{⩽_{obs}^{nr}} E$ . □

Remark that we have cast the definitions of [28] in our own framework. In the full version [17] we show that processes P, Q in Lemma 4 can be adapted to obtain the counterpart of Lemma 4 in the exact framework of [28]. The failure of the proof of [28, Theorem 2] can be traced back to the auxilliary lemma [28, 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 4, the extended processes $({{Q}}, \emptyset)$ and $({{P}}, \emptyset)$ 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}}, \emptyset)$ and $({{P | in (d, x) .0}}, \emptyset)$ .
5. 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., [2,12]. We illustrate this phenomenon on the following example.

Example 3.
Consider the processes $\begin{array}{c} \begin{aligned} P & : = (in (c, x) . if x = 0 then out (o k, 1) else out (b a d, 1)) \\ +_{\frac{1}{2}} (in (c, x) . if x = 0 then out (b a d, 1) else out (o k, 1)) \end{aligned} \\ Q : = in (c, x) . (out (o k, 1) +_{\frac{1}{2}} out (b a d, 1)) \end{array}$

One may, intuitively, consider that these two processes exhibit the same behaviour. Q takes an input and then with probability $\frac{1}{2}$ decides to either output on $ok$ or on $bad$ . P on the other hand first choses a branch with probability $\frac{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 $\frac{1}{2}$ .

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: $\begin{matrix} {RProb}_{R_{r}^{o}} (P \cup Adv, ↓ ok) = 1 {RProb}_{R_{r}^{o}} (Q \cup Adv, ↓ ok) = \frac{1}{2} \end{matrix}$ 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}^{< \infty, np}$ ), i.e., considering processes without replication: for this subclass, may-testing coincides with similarity. We therefore inherit from [18] 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 [11]) corresponds to may-testing with a restricted, determinate adversary process. We also sketch how the algorithms of the DeepSec prover [18] could be adapted to check trace equivalence in this probabilistic setting.
5.1. Non-probabilistic processes

5.1.1. 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 (non-probabilistic) 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 non-probabilistic extended processes. We write ${\overset{}{\to}}_{np}$ , respectively ${\overset{a}{\to}}_{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 \in {MP}^{np}$ , we write $P \Rightarrow_{np} Q$ when there exists a sequence $P = P_{0} {\overset{}{\to}}_{np} \dots {\overset{}{\to}}_{np} P_{n} = Q$ .
Lemma 5.
Let $P, Q \in {MP}^{np}$ . $\begin{matrix} P \Rightarrow_{np} Q iff {RProb}_{R_{nr} (N^{o})} (P, {Q}) = 1 \end{matrix}$

We look now at preorder relations between non-probabilistic processes. We first recall formally how may testing, trace equivalence and bisimulation are defined for non-probabilistic processes (Definition 17 below). Those definitions are coherent with those from the literature, e.g [16], (up to the difference on static equivalence, discussed in Remark 5).
Notation 6.
If b is a barb, we write $P ⇓_{b}$ when there exists $Q$ such that $P \Rightarrow_{np} Q$ , and $Q ↓_{b}$ . For $a \in A_{ext}^{ℓ}$ , we write $(P, ϕ) {\overset{a}{\Rightarrow}}_{np} (Q, ψ)$ when $(P, ϕ) {\overset{τ}{\to}}_{np} \dots {\overset{a}{\to}}_{np} \dots {\overset{τ}{\to}}_{np} (Q, ψ)$ . If $α = a_{1}, \dots, a_{n}$ is a trace, we write $(P, ϕ) {\overset{α}{\Rightarrow}}_{np} (Q, ψ)$ when there exists a sequence $(P, ϕ) {\overset{a_{1}}{\Rightarrow}}_{np} \dots {\overset{a_{n}}{\Rightarrow}}_{np} (Q, ψ)$ .
Definition 17.
We define the binary relations $⩽_{may}^{np}$ , $⩽_{tr}^{np}$ , $⩽_{sim}^{np}$ on ${MP}^{np}$ as follows:
$P ⩽_{may}^{np} Q$ when $\forall Adv \in {MP}^{np} s.t. fn (Adv) \subseteq N_{pub} . \forall c \in N_{pub}$ . $Adv \cup P ⇓_{c}$ implies $Adv \cup Q ⇓_{c}$ ;

$(P, ϕ) ⩽_{tr}^{np} (Q, ψ)$ when for every trace α, $(P, ϕ) {\overset{α}{\Rightarrow}}_{np} (P^{'}, ϕ^{'})$ implies $(Q, ψ) {\overset{α}{\Rightarrow}}_{np} (Q^{'}, ψ^{'})$ ;

$⩽_{sim}^{np}$ is the largest reflexive and transitive relation $R$ such that $(P, ϕ) R (Q, ψ)$ implies that for every $a \in A_{ext}^{ℓ} \cup {τ}$ , and $(P, ϕ) {\overset{a}{\to}}_{np} (P^{'}, ϕ^{'})$ , there exists $(Q^{'}, ψ^{'})$ such that $(Q, ψ) {\overset{a}{\Rightarrow}}_{np} (Q^{'}, ψ^{'})$ and $(P^{'}, ϕ^{'}) R (Q^{'}, ψ^{'})$ .

The preorders $⩽_{sim}$ and $⩽_{tr}$ –and the corresponding equivalence relations–are conservative extensions of $⩽_{sim}^{np}$ and $⩽_{tr}^{np}$ . As expected, the preorder $⩽_{may}$ is not a conservative extension of $⩽_{may}^{np}$ , because of the additional expressive power of probabilistic adversaries. Nonetheless, we can recover $⩽_{may}^{np}$ when we restrict the adversaries in the definition of $⩽_{may}$ to non-probabilistic adversaries.
Proposition 2.
Let $P, Q \in {MP}^{np}$ .
$(P, \emptyset) ⩽_{sim}^{np} (Q, \emptyset)$ iff $(P, \emptyset) ⩽_{sim} (Q, \emptyset)$ ;

$(P, \emptyset) ⩽_{tr}^{np} (Q, \emptyset)$ iff $(P, \emptyset) ⩽_{tr} (Q, \emptyset)$ ;

$(P, \emptyset) ⩽_{may}^{np} (Q, \emptyset)$ iff $\begin{array}{l} \forall Adv \in {MP}^{np} s.t. fn (Adv) \subseteq N_{pub} . \forall c \in N_{pub} . \\ {RProb}_{R_{nr} (N^{o})} (P \cup Adv, ↓ c) ⩽ {RProb}_{R_{nr} (N^{o})} (Q \cup Adv, ↓ c) \end{array}$

Proof sketch.
For may-testing and trace preorder, the proof uses crucially the fact that it is enough to consider non-randomized distributions (thanks to Lemma 2), and from there, we conclude using Lemma 5. 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 $⩽_{sim}^{np}$ is a probabilistic simulation in the sense of Definition 16, and (2) that $⩽_{sim}$ is also a non-probabilistic simulation in the sense of Definition 17.
Suppose that $P ⩽_{sim}^{np} Q$ for $P, Q \in {SP}_{ℓ}^{np}$ . Let $a \in A_{ext}^{ℓ} \cup {τ}$ , $D \in D (S_{N^{ℓ}})$ such that $P {\overset{a}{\to}}_{r} D$ . Looking at the way we defined ${\overset{a}{\to}}_{r}$ (and since $P$ is non-probabilistic), we also see that $P {\overset{a}{\to}}_{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 {\overset{a}{\Rightarrow}}_{np} Q_{i}^{'}$ , and $P_{i}^{'} ⩽_{sim}^{np} Q_{i}^{'}$ . At that point, we build $E = \sum_{i} D (P_{i}^{'}) \cdot δ_{Q_{i}^{'}}$ , and we can see that $Q {\overset{a}{\Rightarrow}}_{r} E$ . Moreover, the structural properties of the lifting allows us to go from $(\forall i, P_{i}^{'} ⩽_{sim}^{np} Q_{i}^{'})$ to $D \hat{⩽_{sim}^{np}} E$ . Hence, we have shown that $⩽_{sim}^{np}$ is indeed a probabilistic simulation in the sense of Definition 16.

Suppose that $P ⩽_{sim} Q$ for $P, Q \in {SP}_{ℓ}^{np}$ . Let $a \in A_{ext}^{ℓ} \cup {τ}$ , and $P^{'} \in {SP}_{ℓ}^{np}$ such that $P {\overset{a}{\to}}_{np} P^{'}$ . This transition carries over to $N^{ℓ}$ , i.e., $P {\overset{a}{\to}}_{r} δ_{P^{'}}$ . We obtain that there exists a distribution E such that $Q {\overset{a}{\Rightarrow}}_{r} E$ , and $δ_{P^{'}} \hat{⩽_{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 {\overset{a}{\Rightarrow}}_{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 may-testing, as shown in [16]. Proposition 3.
Let $P, Q \in {MP}^{np}$ . $(P, \emptyset) ⩽_{tr} (Q, \emptyset) iff \begin{array}{c} \forall Adv \in {MP}^{np} s.t. fn (Adv) \subseteq N_{pub} . \forall c \in N_{pub} . \\ {RProb}_{R_{nr} (N^{o})} (P \cup Adv, ↓ c) ⩽ {RProb}_{R_{nr} (N^{o})} (Q \cup Adv, ↓ c) \end{array}$

5.1.2. 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 [29] (HML).

We can rely on strong simulation as it is a well-known fact ([3]) that simulation for a LTS can be expressed as strong simulation on the corresponding weak LTS, that is, in our case all transitions $(P, ϕ) {\overset{τ}{\to}}^{*} \overset{a}{\to} {\overset{τ}{\to}}^{*} (Q, ψ)$ are merged into a single transition.

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 $⩽_{ssim}^{L}$ the strong simulation relation on a LTS $L$ , we can build an image finite LTS $L^{ℓ}$ such that for all $P, Q \in {MP}^{np}$ : $\begin{matrix} (P, \emptyset) ⩽_{sim} (Q, \emptyset) iff (P, \emptyset) ⩽_{ssim}^{L^{ℓ}} (Q, \emptyset) \end{matrix}$

Our HML characterization consists in expressing strong simulation preorder by the means of satisfaction of logical formulas by the LTS.

Definition 18.
Let $A$ be a countable set of actions. We define the set of logical formulas as: $\begin{matrix} F \in F : = ⊤ | a . F | F_{1} \land F_{2}, where a \in A \end{matrix}$

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 19.
Let $L = (S, A, \to)$ be a LTS. We say that $L$ satisfies a formula F, written $s ⊧ F$ , if for all $s \in S$ ,
$s ⊧ ⊤$ ;

$s ⊧ a . F$ when $s \overset{a}{\to} t$ and $t ⊧ F$ ;

$s ⊧ F_{1} \land 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 characterisation of simulation).

For an image finite LTS $L$ , $\begin{matrix} s ⩽_{ssim}^{L} t iff \forall F \in F . s ⊧ F implies t ⊧ F \end{matrix}$

In order to prove that simulation coincides with may-testing 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}_{F}^{c}$ such that for all bounded non-probabilistic extended processes $(P, ϕ)$ , $\begin{matrix} (P, \emptyset) ⊧ F iff {RProb}_{R_{r}} (P \cup {{{Adv}_{F}^{c}}}, ↓ c) = 1 \end{matrix}$ The construction of ${Adv}_{F}^{c}$ is defined as follows.

Definition 20.
Let F be a formula in $F$ , $ok \in N_{pub}$ such that $ok \notin fn (F)$ and $n \in N$ . We let ${{{Adv}_{F}^{c}}} = {Adv}_{F, 0}^{ok}$ and define ${Adv}_{F, n}^{ok}$ by induction on the syntax of F:
if $F = ⊤$ then ${Adv}_{F, n}^{ok} = out (ok, ok)$ .

if $F = in (ξ, ζ) . F^{'}$ then ${Adv}_{F, n}^{ok} = out (ξ, ζ); {Adv}_{F^{'}, n}^{ok}$ when ${vars}^{} (ξ, ζ) \subseteq {AX}_{n}$ and ${Adv}_{F, n}^{ok} = 0$ otherwise.

if $F = out (ξ, ax) . F^{'}$ then ${Adv}_{F, n}^{ok} = in (ξ, ax); {Adv}_{F^{'}, n + 1}^{ok}$ when $ax = {ax}_{n + 1}$ , ${vars}^{} (ξ) \subseteq {AX}_{n}$ and ${Adv}_{F, n}^{ok} = 0$ otherwise.

if $F = (ξ \overset{?}{=} ζ) . F^{'}$ then ${Adv}_{F, n}^{ok} = if ξ = ζ then {Adv}_{F^{'}, n}^{ok}$ when ${vars}^{} (ξ, ζ) \subseteq {AX}_{n}$ and ${Adv}_{F, n}^{ok} = 0$ otherwise.

if $F = (ξ \overset{?}{\neq} ζ) . F^{'}$ then ${Adv}_{F, n}^{ok} = if ξ = ζ then 0 else {Adv}_{F^{'}, n}^{ok}$ when ${vars}^{} (ξ, ζ) \subseteq {AX}_{n}$ and ${Adv}_{F, n}^{ok} = 0$ otherwise.

if $F = F_{1} \land F_{2}$ , then ${Adv}_{F, n}^{ok} = {Adv}_{F_{1}, n}^{ok} +_{\frac{1}{2}} {Adv}_{F_{2}, n}^{ok}$ .

In Definition 20, the integer n and the conditions on the variables of ξ, ζ ensure that the adversarial process ${Adv}_{F, n}^{ok}$ is closed (no free variables). This is not a restriction as $(P, \emptyset) ⊧ F$ implies that F satisfies these conditions. In particular, we note that 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 \in {MP}^{< \infty, np}$ . $\begin{matrix} (P, \emptyset) ⩽_{sim} (Q, \emptyset) iff P ⩽_{may} Q \end{matrix}$

Cheval et al. have shown [18] 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 [18] 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 \in {MP}^{< \infty, np}$ . Deciding $P \approx_{may}^{} Q$ is coNEXPTIME complete when ≐ is defined by a subterm convergent destructor rewrite system.

5.1.3. 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 [36] 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: $\begin{matrix} Q_{count} (e) = new d . (out (d, b) |! in (d, x) . (out (e, x) + out (d, h (x)))) \end{matrix}$ 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: $\begin{matrix} 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))) \end{matrix}$ 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.

Lemma 6.
Let $Q = new e . (Q_{count} (e) | Q_{out} (e))$ . We have: $\begin{matrix} (! out (c, a), \emptyset) ≰_{sim}^{N^{ℓ}} (Q, \emptyset) but! out (c, a) ⩽_{may} Q \end{matrix}$
Proof sketch.
$(! out (c, a), \emptyset) ≰_{sim}^{N^{ℓ}} (Q, \emptyset)$ is shown by relying on the same idea used to show $L_{1} ≰_{sim}^{} L_{2}$ . Before the first output on c, Q must produce a communication on e, hence fixing the value of x used in $Q_{out} (e)$ which bounds the number of following outputs on c by $x + 1$ . As $! out (c, a)$ may output on c an unbounded number of times, we conclude.

To prove that $! out (c, a) ⩽_{may} Q$ , we unfold the definition of ${RProb}_{R} ({{! out (c, a)}} \cup Adv, ↓ ch)$ and focus on ${RProb}_{R}^{⩽ n} (s, {corr}^{- 1} (↓ ch))$ where $(corr, R)$ is a resolution, $n \in N$ and $corr (s) = {{! out (c, a)}} \cup Adv$ . One can notice that by definition, the number of transitions from s in the computation of ${RProb}_{R}^{⩽ n} (s, {corr}_{R}^{- 1} (↓ ch))$ is bounded by n. Thus, the resolution $R$ may at most unfold n times the process $! out (c, a)$ . By denoting $P^{n} = \underset{n times}{\underset{︸}{out (c, a); \dots; out (c, a)}}$ , we can build a resolution whose probability to exhibit the barb $ch$ from ${{P^{n}}} \cup Adv$ is the same as ${RProb}_{R}^{⩽ n} (s, {corr}_{R}^{- 1} (↓ ch))$ . We then rely on $(P^{n}, \emptyset) ⩽_{sim} (Q, \emptyset)$ and Theorem 2 to conclude that ${RProb}_{R}^{⩽ n} (s, {corr}_{R}^{- 1} (↓ ch)) ⩽ {RProb}_{R} ({{Q}} \cup Adv, ↓ ch)$ which allows us to conclude. □

5.2. Purely probabilistic processes

At the opposite of the spectrum of purely non-deterministic processes, we study purely probabilistic processes with (nearly) no non-determinism. A similar class of processes has been considered in [6,11] to model various protocols relying on randomization (e.g., Crowds [32], mix-net [13], electronic voting [15]). They consider systems that are built as the parallel composition of independent 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 21.
A process is fully determinate if it does not contain the operators +, |, nor !.

$P = {P_{1}, \dots, P_{n}} \in MP$ is purely probabilistic when:
each $P_{i}$ is fully determinate;

there exist distinct public channels $c_{1}, \dots, c_{n} \in N_{pub}$ such that for all $i \in {1, \dots, 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 [21] to show that trace equivalence coincides with observational equivalence for such processes.
5.2.1. Removing scheduling of τ-actions

In [6,11], 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 non-determinism related to honest τ actions is inconsequential when deciding trace equivalence. Indeed, in a multiset of processes ${P_{1}, \dots, 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 \in S$ , if there exists $corr (s) \overset{a}{\to} 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 \in S (R)$ with $corr (s) = (P, ϕ)$ , $\begin{matrix} \forall w \in A_{ext}^{⋆} . {Prob}_{R} (s, w) = {Prob}_{R_{r}^{ℓ}} ((P, ϕ), w) . \end{matrix}$

5.2.2. May-testing and trace equivalence coincide for fully determinate adversaries

As illustrated in Example 3, may-testing 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 \in {MP}^{pp}$ . $\begin{matrix} P ⩽_{d - may} Q iff (P, \emptyset) ⩽_{tr} (Q, \emptyset) \end{matrix}$
Proof sketch.
To prove that $(P, \emptyset) ⩽_{d - may} (Q, \emptyset)$ implies $P ⩽_{tr} Q$ we encode any trace w into a determinate adversary ${Adv}_{w}^{c}$ where c is fresh. ${Adv}_{w}^{c}$ is defined in a similar way as ${Adv}_{F}^{c}$ (Section 5.1), e.g., $\begin{matrix} {Adv}_{in (ξ, ζ) . w^{'}}^{c} = out (ξ, ζ); {Adv}_{w^{'}}^{c} and {Adv}_{(ξ \overset{?}{=} ζ) . w^{'}}^{c} = if ξ = ζ then {Adv}_{w^{'}}^{c} \end{matrix}$ In particular, on the empty trace the adversary process exhibits the barb c: ${Adv}_{ε}^{c} = out (c, c)$ . We obtain that $\begin{matrix} {Prob}_{R_{r} (N^{ℓ})} ((P, \emptyset), w) = {RProb}_{R_{r}^{o}} (P \cup A_{dv}, ↓ c) \end{matrix}$

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 $\begin{matrix} Tr ({Adv}_{i}) = {{(p_{k}^{i}, w_{k}^{i})}}_{k = 1}^{n_{i}} for i = 1, 2 \end{matrix}$ then $\begin{matrix} Tr (Adv) = {{(p \cdot p_{k}^{1}, w_{k}^{1})}}_{k = 1}^{n_{1}} \cup {{((1 - p) \cdot p_{k}^{2}, w_{k}^{2})}}_{k = 1}^{n_{2}} \end{matrix}$ For other constructs, the set of weighted traces is built as expected, e.g., $Tr (0) = \emptyset$ 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})}}_{k = 1}^{n}$ ,

This construction yields the following property: $\begin{aligned} {RProb}_{R_{nr} (N^{o})} (P \cup Adv, ↓ c) \\ = {RProb}_{R_{nr} (N^{o})} (P, ↓ c) \\ + (1 - {RProb}_{R_{nr} (N^{o})} (P, ↓ c)) \cdot \sum_{(α, w) \in Tr (Adv)} α \cdot {Prob}_{R_{nr} (N^{ℓ})} ((P, \emptyset), w) \end{aligned}$ 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. □

6. Deciding trace equivalence and tool support

As previous mentioned, Cheval et al. [18] 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 the infinite set of all possible concrete executions of the processes and an arbitrary attacker as a finite symbolic tree, called the partition tree. Intuitively, each node of this symbolic tree represents the state of the two processes after executing a trace $tr$ . Due to non-determinism, a node may contain several constraint systems corresponding to every possible interleaving allowing the execution of a given 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 least one constraint system derived from process A and one from process B; or the node is empty.

We show how to extend this procedure in order to decide trace equivalence in a general setting where both probabilistic and non-determinism behavior may co-exist in the process. Obviously, we inherit the setting of a bounded number of sessions and cryptographic primitives modeled by a subterm convergent destructor rewrite system.

Following Lemma 2, proving $(P, ϕ) ⩽_{tr} (P^{'}, ϕ^{'})$ is equivalent to proving $(P, ϕ) ⩽_{tr}^{nr} (P^{'}, ϕ^{'})$ . Thus, by definition, we focus on the computation of ${Prob}_{R_{nr} (N^{ℓ})} ((P, ϕ), w)$ for all $w \in {A_{ext}^{ℓ}}^{*}$ . A main difficulty stems from the presence of universal quantification over resolutions. However, as $P$ is bounded, we can completely ignore resolutions and focus on the labelled semantics, as shown by the following property.

Lemma 7.
Let $(P, ϕ) \in {SP}_{ℓ}^{< \infty}$ . Let $a \in A_{ext}^{ℓ}$ . Let $w \in {A_{ext}^{ℓ}}^{}$ . $\begin{matrix} {Prob}_{R_{nr} (N^{ℓ})} ((P, ϕ), ϵ) = 1 {Prob}_{R_{nr} (N^{ℓ})} ((P, ϕ), a . w) = max (p_{1}, p_{2}) \end{matrix}$ where* $\begin{array}{c} p_{1} = max_{(P, ϕ) \to_{τ} D} \sum_{(P^{'}, ϕ^{'}) \in supp (D)} D ((P^{'}, ϕ^{'})) \cdot {Prob}_{R_{nr} (N^{ℓ})} ((P, ϕ), a . w) \\ p_{2} = max_{(P, ϕ) \to_{a} D} \sum_{(P^{'}, ϕ^{'}) \in supp (D)} D ((P^{'}, ϕ^{'})) \cdot {Prob}_{R_{nr} (N^{ℓ})} ((P, ϕ), w) \end{array}$

Note that this inductive definition is well founded as the size of the processes strictly decreases at each semantics step since there is no replication.

As mentioned above, partition trees [18] are a finite symbolic representation of the concrete executions of the two initial processes. Each node contains all reachable states of the two processes after executing some trace w. However, to compute the probability ${Prob}_{R_{nr} (N^{ℓ})} ((P, ϕ), w)$ , Lemma 7 also requires to know the different semantics steps that led to the process states after executing w. In other words, it requires the history of each extended processes. Therefore, to simplify the probability computation, we extended the labelled semantics by adding the history of transitions leading to the extended process. To further simplify, we assume that each input, output, probabilistic choice and non-deterministic choice are decorated with a label $ℓ \in L$ , denoted ${in}^{ℓ} (u, x); P$ , ${out}^{ℓ} (u, v); P$ and $P +_{p}^{ℓ} Q$ , $P +_{}^{ℓ} Q$ respectively. Additionally, we assume that all labels are distinct in the initial processes.
Definition 22.
We define history entries as elements from ${h_{1} (ℓ), h_{2} (ℓ, ℓ^{'}), h_{+} (ℓ, p, i), h_{c} (ℓ, i) | i \in {0, 1}, p \in] 0, 1 [, ℓ label}$ . A history, usually denoted $H$ , is a sequence of history entries.

Extended processes and the labelled semantics can naturally be extended to include history. In particular when $(P, ϕ) \to_{a} D$ and $(P^{'}, ϕ^{'}) \in supp (D)$ , we define $(P, ϕ, H) \overset{a}{\to} (P^{'}, ϕ^{'}, H^{'})$ where:
$H^{'} = H \cdot h_{+} (ℓ, p, 0)$ when $P = Q \cup {{P +_{p}^{ℓ} Q}}$ and $P^{'} = Q \cup {{P}}$ ;

$H^{'} = H \cdot h_{+} (ℓ, p, 1)$ when $P = Q \cup {{P +_{p}^{ℓ} Q}}$ and $P^{'} = Q \cup {{Q}}$ ;

$H^{'} = H \cdot h_{c} (ℓ, 0)$ when $P = Q \cup {{P +_{}^{ℓ} Q}}$ and $P^{'} = Q \cup {{P}}$ ;

$H^{'} = H \cdot h_{c} (ℓ, 1)$ when $P = Q \cup {{P +_{}^{ℓ} Q}}$ and $P^{'} = Q \cup {{Q}}$ ;

$H^{'} = H \cdot h_{2} (ℓ, ℓ^{'})$ when $P = Q \cup {{{out}^{ℓ} (u, t) . P, {in}^{ℓ^{'}} (v, x) . Q}}$ , $P^{'} = Q \cup {{P, Q {x \mapsto t}}}$ ;

$H^{'} = H \cdot h_{1} (ℓ)$ when $P = Q \cup {{{out}^{ℓ} (u, t) . P}}$ and $a = out (ξ, {ax}_{n})$ and $P^{'} = Q \cup {{P}}$ ;

$H^{'} = H \cdot h_{1} (ℓ)$ when $P = Q \cup {{{in}^{ℓ} (u, x) . P}}$ and $a = in (ξ, ζ)$ and $P^{'} = Q \cup {{P {x \mapsto ζ ϕ}}}$ ;

$H^{'} = H$ otherwise.
Given $w \in {A_{ext}^{ℓ}}^{}$ , we write $(P, ϕ, H) \overset{w}{\Rightarrow} (P^{'}, ϕ^{'}, H^{'})$ when $(P, ϕ, H) \overset{a_{1}}{\to} \dots \overset{a_{n}}{\to} (P^{'}, ϕ^{'}, H^{'})$ and w is $a_{1} \dots a_{n}$ with the τ labels removed.

Since labels occur at most once in the initial process, intuitively, two extended processes with a shared prefix executed the same semantics steps. In other words, if $\begin{matrix} (P, ϕ, H) \overset{w}{\Rightarrow} (P_{1}, ϕ_{1}, H_{0} \cdot H_{1}) and (P, ϕ, H) \overset{w}{\Rightarrow} (P_{2}, ϕ_{2}, H_{0} \cdot H_{2}) \end{matrix}$ then there exist $w_{0}$ , $w_{1}$ and an extended process $(P_{0}, ϕ_{0}, H_{0})$ such that $w = w_{0} w_{1}$ and

We now describe how we can compute the probability that $(P, ϕ)$ executes a trace w from the set of histories obtained after executing w, i.e. ${H^{'} | (P, ϕ, []) \overset{w}{\Rightarrow} (P^{'}, ϕ^{'}, H^{'})}$ where $[]$ denotes the empty sequence.
Definition 23.
Let S be a set of histories. We denote by $S_{| h} = {H^{'} | (h \cdot H^{'}) \in S}$ . We define $compute (S)$ inductively as follows:
$compute (\emptyset) = 0$

$compute ({[]}) = 1$ , i.e., if S is the singleton containing the empty sequence

otherwise $\begin{matrix} compute (S) = max \{\begin{array}{l} {max}_{ℓ} compute (S_{| h_{1} (ℓ)}) \\ {max}_{ℓ, ℓ^{'}} compute (S_{| h_{2} (ℓ, ℓ^{'})}) \\ {max}_{ℓ, i} compute (S_{| h_{c} (ℓ, i)}) \\ {max}_{ℓ, p} (p \cdot compute (S_{| h_{+} (ℓ, p, 0)}) + (1 - p) \cdot compute (S_{| h_{+} (ℓ, p, 1)})) \end{array} \end{matrix}$

The correspondence between ${Prob}_{R_{nr} (N^{ℓ})} ((P, ϕ), w)$ and the function $compute (\cdot)$ is given in the following lemma.
Lemma 8.
Let* $(P, ϕ)$ be an extended process, $w \in {A_{ext}^{ℓ}}^{}$ and* $S = {H^{'} | (P, ϕ, []) \overset{w}{\Rightarrow} (P^{'}, ϕ^{'}, H^{'})}$ . We have that ${Prob}_{R_{nr} (N^{ℓ})} ((P, ϕ), w) = compute (S)$ .

This lemma provides the core property that allows us to update the partition trees generated by the procedure in [18] as well as the test performed on each node of this partition tree to conclude trace preorder.
Theorem 4.
Let $P, Q \in {MP}^{< \infty}$ and ≐ be defined by a subterm convergent destructor rewrite system. Trace preorder $({{P}}, \emptyset) ⩽_{tr} ({{Q}}, \emptyset)$ is decidable.
Proof sketch.
First, we show that we can restrict the set of traces we need to verify. In particular, it suffices to look at traces $w \in {A_{ext}^{ℓ}}^{}$ that can be split in two parts: $w = w_{1} \cdot w_{2}$ where $w_{2}$ only consists of actions of the form $ξ ≐ ζ$ or , and $w_{1}$ of any other kind of actions. In other words, we can push* static equivalence tests towards the end of traces. Moreover, for all concrete traces $w_{1}$ not containing static equivalence tests, it suffices to check a finite number of concrete traces $w_{2}^{1}, \dots, w_{2}^{n}$ built only on static equivalence tests. To do this, we use a proof technique similar to the proof in [16] showing that trace equivalence and may testing coincide for processes with bounded number of sessions. Let us define the sets $S_{P} (w_{1}) = {(P^{'}, ϕ^{'}, H^{'}) | ({{P}}, \emptyset, []) \overset{w_{1}}{\Rightarrow} (P^{'}, ϕ^{'}, H^{'})}$ and $S_{Q} (w_{1}) = {(P^{'}, ϕ^{'}, H^{'}) | ({{Q}}, \emptyset, []) \overset{w_{1}}{\Rightarrow} (P^{'}, ϕ^{'}, H^{'})}$ . Since P and Q are bounded processes, $S_{P} (w_{1})$ , $S_{Q} (w_{1})$ and $(S_{P} (w_{1}) \cup S_{Q} (w_{1})) ∖_{\sim}$ are finite (here ∼ refers to static equivalence of frames). Therefore, for all $(P^{'}, ϕ^{'}, H^{'}) \in S_{P} (w_{1}) \cup S_{Q} (w_{1})$ , we can define a finite sequence of actions $w_{2}$ built only on actions of the form $ξ ≐ ζ$ or that exactly defines the equivalence class of $(P^{'}, ϕ^{'}, H^{'})$ in $(S_{P} \cup S_{Q}) ∖_{\sim}$ , i.e., for all $(P^{″}, ϕ^{″}, H^{″}) \in S_{P} (w_{1}) \cup S_{Q} (w_{1})$ , $ϕ^{'} \sim ϕ^{″}$ if and only if $(P^{″}, ϕ^{″}, H^{″}) \overset{w_{2}}{\Rightarrow} (P^{″}, ϕ^{″}, H^{″})$ . Thus, if we denote by W this set of traces sufficient for proving trace preorder, we have that $({{P}}, \emptyset) ⩽_{tr} ({{Q}}, \emptyset)$ if and only if for all $w \in W$ , ${Prob}_{R_{nr} (N^{ℓ})} (({{P}}, \emptyset), w) ⩽ {Prob}_{R_{nr} (N^{ℓ})} (({{Q}}, \emptyset), w)$ .

Second, similarly to how we augmented our labelled semantics with histories, we also augment the symbolic semantics used in [18] to generate partition trees with histories. As the addition of histories in symbolic extended processes does not impact in any way the generation of the partition trees, we can deduce from [18] that there exists a partition tree from P and Q, denoted $PTree (P, Q)$ . Thus, each node η of the partition tree will now contain a set $Γ (η)$ of symbolic processes of the form $(P_{c}, ϕ_{c}, C, H)$ where $(P_{c}, ϕ_{c})$ is an open extended processes, $C$ is a set of constraints and $H$ is a history. The set $Γ (η)$ can furthermore be divided into the sets of symbolic processes coming from P and from Q, respectively $Γ_{P} (η)$ and $Γ_{Q} (η)$ . If we denote by $H (S)$ the set of histories of the (symbolic) extended processes in S, our decision procedure consists in checking that for all nodes $η \in PTree (P, Q)$ , $compute (H (Γ_{P} (η))) ⩽ compute (H (Γ_{Q} (η)))$ .

To show that it indeed decides trace preorder, we recall that soundness of partition trees ensures that the nodes of the partition tree rooted by $({{P}}, \emptyset, [])$ and $({{Q}}, \emptyset, [])$ contain the symbolic processes representing all concrete extended processes reached after executing some trace w and that are statically equivalent. Moreover, completeness of partition trees ensures that for all concrete traces $w \in W$ , there exists a node in the partition tree such that if $({{P}}, \emptyset, []) \overset{w}{\Rightarrow} (P^{'}, ϕ^{'}, H^{'})$ or $({{Q}}, \emptyset, []) \overset{w}{\Rightarrow} (P^{'}, ϕ^{'}, H^{'})$ then $Γ (η)$ contains a symbolic process representing $(P^{'}, ϕ^{'}, H^{'})$ .

Formally, we show that:
Soundness: $\forall η \in PTree (P, Q)$ , $\exists w \in W$ s.t. $H (S_{P} (w)) = H (Γ_{P} (η))$ and $H (S_{Q} (w)) = H (Γ_{Q} (η))$

Completeness: $\forall w \in W$ , $\exists η \in PTree (P, Q)$ s.t. $H (S_{P} (w)) = H (Γ_{P} (η))$ and $H (S_{Q} (w)) = H (Γ_{Q} (η))$
Applying Lemma 8, we obtain that $\begin{array}{c} \forall w \in W, {Prob}_{R_{nr} (N^{ℓ})} (({{P}}, \emptyset), w) ⩽ {Prob}_{R_{nr} (N^{ℓ})} (({{Q}}, \emptyset), w) \\ if and only if \\ \forall η \in PTree (P, Q), compute (H (Γ_{P} (η))) ⩽ compute (H (Γ_{Q} (η))) \end{array}$ which allows us to conclude the proof. □

As a direct corollary we obtain that we can decide determinate may testing for purely probabilistic processes as it coincides with trace equivalence.
Corollary 2.
Let $P, Q \in {MP}^{pp}$ and ≐ be defined by a subterm convergent destructor rewrite system. Determinate may testing preorder $({{P}}, \emptyset) ⩽_{d - may} ({{Q}}, \emptyset)$ is decidable.

We have implemented the procedure described above in the DeepSec tool. The input language has been extended with a probabilistic choice operator $+_{p}$ where p is a real number in $] 0, 1 [$ . When trace equivalence between 2 processes is queried, the tool uses the above procedure for verification. The development is available on DeepSec’s official github repository at [35].

As we will see in Section 7, we can use DeepSec to show that the dining cryptographers protocol does not provide anonymity when coins are biased.
7. An example: Dining cryptographers

In this section, we illustrate our framework by proving anonymity of the well-known dining cryptographers protocol. This protocol has been designed to solve the following problem: three participants have a secret bit $b_{i} \in {0, 1}$ , such that at most one of these bits equals 1, i.e. the sum s of the three bits is either 0 or 1. The goal is to determine whether $s = 1$ while hiding any additional information of each $b_{i}$ ; in particular, if $s = 1$ , it must be impossible to identify for which i $b_{i} = 1$ . To do so, we suppose that each pair of participants ${a_{i}, a_{j}}$ has a private coin, that they can toss privately, i.e., only $a_{i}$ and $a_{j}$ can read the result. To solve the above described problem, participants proceed as follows:

each pair $(a_{i}, a_{j})$ of participants tosses its coin, and privately shares the result $c_{i, j}$ ;

each participant $a_{i}$ outputs their result $r_{i}$ , computed as the exclusive or (xor) of their secret bit $b_{i}$ , and the result of both their left and right coins;

each participant can compute s by doing the xor of all the three $r_{i}$ .

We suppose that the secret bits $b_{i}$ of each participant are determined by an assignment $B : {a_{1}, a_{2}, a_{3}} \to {0, 1}$ , and denote by ${DC}_{B}$ the process (defined below) modeling the protocol with the given assignment. As we are interested in anonymity we focus on the case where one secret bit is 1 and we denote by $W_{1}$ the set of 1-weighted assignment functions, that is those functions that assign map exactly one participant to 1. Then, the security property for the dining cryptographers protocol can be stated as $\begin{matrix} \forall B, B^{'} \in W_{1} . {DC}_{B} \approx_{may}^{} {DC}_{B^{'}} \end{matrix}$ that is no adversary should be able to distinguish the systems ${DC}_{B}$ and ${DC}_{B^{'}}$ whenever one of the secret bits equals 1.

Our contributions in this section are the following. First, we model the dining cryptographers protocol as a process ${DC}_{B}$ in the probabilistic applied π-calculus. Then we give a manual proof that (when coins are unbiased) ${DC}_{B}$ and ${DC}_{B^{'}}$ –where B, $B^{'}$ are assignment functions as above–are may-testing equivalent. Finally, we show, using the tool DeepSec, that when the coins are biased those systems are not trace equivalent, thus not may-testing equivalent (Theorem 1).

7.1. Dining cryptographers in the probabilistic applied π-calculus

We split the definition of ${DC}_{B}$ in several components. First, we model the fact that two adjacent participants can toss a coin, and privately share the result. We model this by the oracle process $O_{c_{l}, c_{r}}$ (indexed by channels $c_{l}$ , $c_{r}$ ): it performs a fair probabilistic choice, and sends the result in parallel on channel $c_{r}$ on its right, and channel $c_{l}$ on its left. $\begin{matrix} O_{c_{l}, c_{r}} : = (out (c_{l}, 0) | out (c_{r}, 0)) +_{1 / 2} (out (c_{l}, 1) | out (c_{r}, 1)) \end{matrix}$

We now define the process that models one agent $A_{c_{l}, c_{r}, c} (b)$ : it is indexed by three channels–(private) channels $c_{l}$ and $c_{r}$ for communicating with the oracle placed to its left, respectively to its right, and a (public) channel c for sending its final result. It also depends on the agent’s secret bit $b \in {0, 1}$ . $\begin{matrix} A_{c_{l}, c_{r}, c} (b) : = in (c_{r}, x_{r}); in (c_{l}, x_{l}); out (c, x_{l} \oplus x_{r} \oplus b) \end{matrix}$ where ⊕ models bitwise xor.

Notation 7.
We fix a set of public names $A = {a_{1}, a_{2}, a_{3}} \subseteq N_{pub}$ and we will identify each participant to their public channel $a_{i}$ .

Moreover, we define the set of oracles (or edges), that we note $E : = {{a_{i}, a_{j}} | i \neq j, a_{i}, a_{j} \in A}$ . Observe that $E$ has three elements, that we call $e_{1}$ , $e_{2}$ , $e_{3}$ for convenience.

We also fix a set of 6 private names $C = {c_{1}, \dots, c_{6}} \subseteq N_{priv}$ that will serve as the private channels between oracles and participants; each of the three participants has access to two oracles. We formalize the association between channels, oracles and participants by three functions $\begin{matrix} c : A \cup E \to C \times C e : C \to E a : C \to A \end{matrix}$ Function c associates to an agent or an edge the pair of channels (we denote by $c . l$ and $c . r$ the first and second projection of c respectively). Functions e and a associate to a channel, the corresponding agent, respectively edge.

Fig. 9.
Dining cryptographers: graph representation.

The overall system using these notations is depicted in Fig. 9. Given $B \in W_{1}$ we can now define the process ${DC}_{B}$ that puts in parallel three participants, and their three coin toss oracles. The agent channels used by the participants to communicate their final results are public. By contrast, the channels used to communicate with the oracles are hidden from the adversary, thus private and bound by $new$ . $\begin{matrix} {DC}_{B} : = new c_{1}, \dots, c_{6} (‖_{e \in E} O_{c_{l} (e), c_{r} (e)} | ‖_{a \in A} A_{c_{l} (a), c_{r} (a), a} (B (a))) \end{matrix}$

We can now formally state that the dining cryptographers protocol does ensure anonymity.
Theorem 5.
$\forall B, B^{'} \in W_{1} . {DC}_{B} \approx_{may}^{} {DC}_{B^{'}}$

In order to show Theorem 5, we are going to show use the labelled semantics and show a stronger result, i.e. that ${DC}_{B}$ and ${DC}_{B^{'}}$ are bisimilar.
7.2. Labelled semantics for the dining cryptographers protocol

The labelled semantics for our model of the dining cryptographers protocol is however complex: one of the reasons is that we do not enforce a particular order for the communications between the oracles $O_{i}$ and the participants $A_{i}$ . Thus, we have both probabilistic and non-deterministic concurrent behaviors. As a consequence, it is difficult to prove our equivalence result directly in the NPLTS $N^{ℓ}$ . To solve this problem, we define an auxiliary simplified NPLTS $N_{DC}$ , and show that:

$N_{DC}$ is bisimilar to $N^{ℓ}$ ;

for every $B, B^{'} \in W_{1}$ the $N_{DC}$ -states corresponding to ${DC}_{B}$ and ${DC}_{B^{'}}$ are bisimilar in $N_{DC}$ .

The main idea for the construction of the auxiliary NPLTS

N_{DC}

is that only relevant steps should appear. More precisely, we note that a run of the protocol should be entirely characterized by the oracles’ probabilistic choices, and the order in which participants output their results. By contrast, the order of internal communications between participants and oracles occur–on the private channels

c_{i}

–is irrelevant.

Definition 24.
We define sets of internal events Λ and external events $Λ^{ext}$ as: $\begin{matrix} Λ : = {e [\leftarrow b] | e \in E, b \in {0, 1}} Λ^{ext} : = {a [\to b] | a \in A, b \in {0, 1}} \end{matrix}$ The event $e [\leftarrow b]$ means that oracle $e \in E$ is sampling $b \in {0, 1}$ . The event $a [\to b]$ means that participant $a \in A$ is outputting b on their public channel. We call history a pair $h = (s, l)$ , where s is a set of internal events in Λ and l is a list of external events in $Λ^{ext}$ such that no participant $a \in A$ occurs twice in l. We denote by $H$ the set of all such h.
Notation 8.
To each history $h = (s, l)$ , we associate a frame $ϕ_{h} : = {{ax}_{1} = b_{1}, \dots {ax}_{n} = b_{n}}$ when $l = (a_{1} [\to b_{1}], \dots a_{n} [\to b_{n}])$ . Moreover, for $e \in E$ , and history $h = (s, l)$ , we write $e \in s$ when $e [\leftarrow b] \in s$ for some boolean b, and $e \notin h$ otherwise. We define similarly $a \in l$ and $a \notin l$ for $a \in A$ . We denote the empty history by $ϵ_{H} : = (\emptyset, ϵ)$ .

We are now ready to define our simplified NPLTS $N_{DC}$ . $N_{DC}$ has exactly the same set of actions as $N^{ℓ}$ , the NPLTS built from the labelled semantics. A state of $N_{DC}$ encapsulates information about both the (relevant) history, and the assignment function of secret bits $A \to {0, 1}$ . These information are enough to decide how a history is modified by an action. More precisely three kinds of actions can be enabled in a given state.

The first kind are actions of the form $(ξ \overset{?}{=} ζ)$ , that in $N^{ℓ}$ perform an equality test on the frame. In $N_{DC}$ the equality test is performed on $ϕ_{h}$ , the frame built unambiguously from the history as defined in Notation 8. The second kind of action is the internal action τ: in $N_{DC}$ τ-actions correspond to a step where an oracle, that does not already appear in the history, randomly samples a boolean b. After such a τ-action, which is inherently probabilistic, the information that this oracle has sampled b is added to the history. The last kind of actions are the (external) output actions: some participant $a \in A$ can output a result b – if no output by a is already recorded in the history – when the history contains the information of the boolean chosen by both oracles adjacent to a, and that moreover b is equal to the xor of these two booleans with the secret bit of a.
Definition 25.
We define a NPLTS $N_{DC} = (S_{DC}, A_{DC}, {trans}_{DC})$ where $S_{DC} : = {(h, B) | h \in H, B \in W_{1}}$ , $A_{DC} : = {τ} \cup A_{ext}^{ℓ}$ , and the transition function ${trans}_{DC}$ is defined as:

We now follow the road-map that we outlined in the beginning of the present section: first we show that we can replace the study of the labelled semantics for ${DC}_{B}$ by the study of $N_{DC}$ , by exhibiting a bisimilarity between those two NPLTSs (Proposition 7). Then, we show that the $N_{DC}$ states (corresponding to) ${DC}_{B}$ and ${DC}_{B^{'}}$ are bisimilar as soon as $B, B^{'} \in W_{1}$ (Proposition 8).
Proposition 7.
There exists an NPLTS bisimulation R on $N_{DC} \cup N^{ℓ}$ such that for every $B \in W_{1}$ , it holds that $(ϵ_{H}, B) R ({DC}_{B}, \emptyset)$ .
Proposition 8.
If $B, B^{'} \in W_{1}$ then the $N_{DC}$ -states $(ϵ_{H}, B)$ and $(ϵ_{H}, B^{'})$ are bisimilar.

From Propositions 7 and 8, we can show that the process ${DC}_{B}$ and ${DC}_{B^{'}}$ are equivalent for the labelled bisimulation from Definition 16 in Section 4. We state this result formally below.
Corollary 3 (Security for the dining cryptographers protocol).

If $B, B^{'} \in W_{1}$ then ${DC}_{B} \approx_{bi}^{} {DC}_{B^{'}}$ .

Proof.
Recall that by definition of $\approx_{bi}^{}$ , we need to show that the states $s_{B} : = ({DC}_{B}, \emptyset)$ and $s_{B^{'}} : = ({DC}_{B}^{'}, \emptyset)$ are bisimilar in $N^{ℓ}$ . Since we know by Proposition 8 that $t_{B} : = (ϵ_{H}, B)$ and $t_{B^{'}} = (ϵ_{H}, B^{'})$ are bisimilar in $N_{DC}$ , we also have $(t_{B}, t_{B^{'}}) \in (\sim_{N_{DC} \cup N^{ℓ}})$ (because $N^{ℓ}$ and $N_{DC}$ have disjoint state spaces). By Proposition 7, we also have that $t_{B} \sim_{N_{DC} \cup N^{ℓ}} s_{B}$ , and $t_{B^{'}} \sim_{N_{DC} \cup N^{ℓ}} s_{B^{'}}$ . Since $\sim_{N_{DC} \cup N^{ℓ}}$ is an equivalence relation, we can combine all this to obtain that $s_{B} \sim_{N_{DC} \cup N^{ℓ}} s_{B^{'}}$ . From here (again because $N^{ℓ}$ and $N_{DC}$ have disjoint state spaces), we conclude that $s_{B} \sim_{N^{ℓ}}, s_{B^{'}}$ . □

As an immediate consequence of Corollary 3, and since labelled bisimulation is stronger than may-testing equivalence, we obtain a proof of Theorem 5, i.e. that $\forall B, B^{'} \in W_{1}$ , ${DC}_{B} \approx_{may}^{} {DC}_{B^{'}}$ .
7.3. Analysis with DeepSec

We have analyzed the Dining Cryptographers protocol using our probabilistic extension of the DeepSec tool [35]. The encoding of processes ${DC}_{B}$ for $B \in W_{1}$ is straightforward and follows directly the modeling above. Although DeepSec does not support xor in general, we can easily encode the ternary version using 8 rewrite rules $xor (b_{1}, b_{2}, b_{3}) \to b$ for $b_{1}, b_{2}, b_{3} \in {0, 1}$ and $b = b 1 \oplus b_{2} \oplus b_{3}$ . Restricting to a ternary xor is not a loss of generality as the protocol does not take any input from the adversary and only honest users construct xor-terms.

As a first result we can show that $\begin{matrix} \forall B, B^{'} \in W_{1} . {DC}_{B} \approx_{tr}^{} {DC}_{B^{'}} \end{matrix}$ This result is actually not satisfactory, as trace equivalence is strictly weaker than may testing (which also motivated the pen and paper proof of the previous section). More interesting is the fact that we can show that anonymity is broken when we use a biased coin, i.e., we replace the probability 0.5 in the coin tossing oracle by a probability $p \neq 0.5$ . If we denote the modified process by ${DC}_{B}^{p}$ we can for instance show, using DeepSec, that, as expected,

where $B_{i}$ assigns $b_{i}$ to 1 and remaining bits to 0. Given that trace equivalence is strictly weaker than may-testing this implies that may testing does not hold either.

Given the rather small size of the processes DeepSec performs these verifications in about 1 second each.

8. 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, overlooked in previous attempts. In addition to solving technical problems, we believe that randomized schedulers capture more faithfully the idea that one cannot predict how non-determinism is resolved. Randomized schedulers generalize the idea that a schedulers chooses a particular distribution among the ones available 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 [12], 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 [11], 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.

We also show how deciding trace equivalence can be automated in the presence of probabilities. We propose a decision procedure that extends previous work by Cheval el al [18] and implement this procedure in the DeepSec tool. Hence, we provide tool support for proving determinate may-testing on the class of purely probabilistic processes when the number of sessions is bounded and cryptographic primitives are modeled as a subterm destructor rewrite system. On more general classes of processes, our tool can be used for attack finding: disproving trace equivalence implies that may testing (and all stronger equivalences) does not hold either, therefore violating security properties stated as an equivalence.

Finally, we illustrate our framework by studying the well-known Dining Cryptographers protocol. We model the protocol and its anonymity property in the probabilistic applied π-calculus. Then, we use our framework to prove that anonymity holds, and demonstrate DeepSec’s attack finding ability on a variant of the protocol that uses a biased coin.

Our work paves the road towards several future works, in addition to exploring restricted schedulers mentioned above. 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 [2,12]) 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.

Footnotes

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 with support from the region Grand Est and by France 2030 program managed by ANR (ANR-22-PECY-0006).

References

Abadi,

Blanchet and

Fournet, The applied pi calculus: Mobile values, new names, and secure communication, Journal of the ACM (JACM) (2017).

M.S.

Alvim,

M.E.

Andrés,

Palamidessi and

van Rossum, Safe equivalences for security properties, in: Theoretical Computer Science – 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010,

C.S.

Calude and

Sassone, eds, IFIP Advances in Information and Communication Technology, Vol. 323, Springer, 2010, pp. 55–70. doi:10.1007/978-3-642-15240-5_5.

Amadio, Operational methods in semantics, 2016.

D.A.

Basin,

Dreier,

Hirschi,

Radomirovic,

Sasse and

Stettler, A formal analysis of 5G authentication, in: ACM SIGSAC Conference on Computer and Communications Security (CCS’18),

Lie,

Mannan,

Backes and

Wang, eds, ACM, 2018, pp. 1383–1396. doi:10.1145/3243734.3243846.

D.A.

Basin,

Sasse and

Toro-Pozo, The EMV standard: Break, fix, verify, in: 42nd IEEE Symposium on Security and Privacy (S&P’21), IEEE, 2021, pp. 1766–1781. doi:10.1109/SP40001.2021.00037.

M.S.

Bauer,

Chadha,

A.P.

Sistla and

Viswanathan, Model checking indistinguishability of randomized security protocols, in: International Conference on Computer Aided Verification (CAV’18), Springer, 2018, pp. 117–135. doi:10.1007/978-3-319-96142-2_10.

Bhargavan,

Blanchet and

Kobeissi, Verified models and reference implementations for the TLS 1.3 standard candidate, in: IEEE Symposium on Security and Privacy (S&P’17), IEEE, 2017, pp. 483–502.

Blanchet, Modeling and verifying security protocols with the applied pi calculus and ProVerif, Foundations and Trends in Privacy and Security (2016).

Bonchi,

Sokolova and

Vignudelli, The theory of traces for systems with nondeterminism and probability, in: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), IEEE, 2019, pp. 1–14.

10.

Castiglioni, Trace and testing metrics on nondeterministic probabilistic processes, in: Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics and 15th Workshop on Structural Operational Semantics, (EXPRESS/SOS) 2018, Vol. 276, 2018, pp. 19–36.

11.

Chadha,

A.P.

Sistla and

Viswanathan, Verification of randomized security protocols, in: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’17), IEEE, 2017, pp. 1–12.

12.

Chatzikokolakis and

Palamidessi, Making random choices invisible to the scheduler, Inf. Comput.208(6) (2010), 694–715. doi:10.1016/j.ic.2009.06.006.

13.

Chaum, Untraceable electronic mail, return addresses, and digital pseudonyms, Commun. ACM24(2) (1981), 84–88. doi:10.1145/358549.358563.

14.

Chaum, The dining cryptographers problem: Unconditional sender and recipient untraceability, J. Cryptol.1(1) (1988), 65–75. doi:10.1007/BF00206326.

15.

Chaum,

P.Y.A.

Ryan and

S.A.

Schneider, A practical voter-verifiable election scheme, in: 10th European Symposium on Research in Computer Security (ESORICS’05),

S.D.C.

di sVimercati,

P.F.

Syverson and

Gollmann, eds, Lecture Notes in Computer Science, Vol. 3679, Springer, 2005, pp. 118–139. doi:10.1007/11555827_8.

16.

Cheval,

Cortier and

Delaune, Deciding equivalence-based properties using constraint solving, Theor. Comput. Sci.492 (2013), 1–39. doi:10.1016/j.tcs.2013.04.016.

17.

Cheval,

Crubillé and

Kremer, Symbolic protocol verification with dice: Process equivalences in the presence of probabilities (extended version), 2023, https://hal.inria.fr/hal-03683907/document.

18.

Cheval,

Kremer and

Rakotonirina, DEEPSEC: Deciding equivalence properties in security protocols – theory and practice, in: Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P’18), IEEE Computer Society Press, San Francisco, CA, USA, 2018, pp. 525–542. doi:10.1109/SP.2018.00033.

19.

Cohn-Gordon,

Cremers,

Dowling,

Garratt and

Stebila, A formal security analysis of the signal messaging protocol, Journal of Cryptology33(4) (2020), 1914–1983. doi:10.1007/s00145-020-09360-1.

20.

Comon-Lundh and

Cortier, Computational soundness of observational equivalence, in: ACM Conference on Computer and Communications Security (CCS’08),

Ning,

P.F.

Syverson and

Jha, eds, ACM, 2008, pp. 109–118. doi:10.1145/1455770.1455786.

21.

Cortier and

Delaune, A method for proving observational equivalence, in: 22nd IEEE Computer Security Foundations Symposium, (CSF’09), IEEE Computer Society, 2009, pp. 266–276. doi:10.1109/CSF.2009.9.

22.

Cortier,

Kremer and

Warinschi, A survey of symbolic methods in computational analysis of cryptographic systems, Journal of Automated Reasoning46(3–4) (2010), 225–259. doi:10.1007/s10817-010-9187-9.

23.

Cremers,

Horvat,

Hoyland,

Scott and

van der Merwe, A comprehensive symbolic analysis of TLS 1.3, in: ACM SIGSAC Conference on Computer and Communications Security (CCS’17), ACM, 2017, pp. 1773–1788.

24.

Deng, Axiomatisations and types for probabilistic and mobile processes, PhD thesis, École des Mines de Paris, 2005.

25.

Deng,

Van Glabbeek,

Hennessy and

Morgan, Testing finitary probabilistic processes, in: International Conference on Concurrency Theory, Springer, 2009, pp. 274–288.

26.

Dolev and

A.C.

Yao, On the security of public key protocols, IEEE Trans. Inf. Theory29(2) (1983), 198–207. doi:10.1109/TIT.1983.1056650.

27.

C.G.

Eisentraut, Principles of Markov automata, PhD thesis, Saarländische Universitäts-und Landesbibliothek, 2017.

28.

Goubault-Larrecq,

Palamidessi and

Troina, A probabilistic applied pi-calculus, in: Asian Symposium on Programming Languages and Systems, Springer, 2007, pp. 175–190. doi:10.1007/978-3-540-76637-7_12.

29.

Hennessy and

Milner, On observing nondeterminism and concurrency, in: Automata, Languages and Programming (ICALP’80),

de Bakker and

van Leeuwen, eds, Springer, 1980, pp. 299–309. doi:10.1007/3-540-10003-2_79.

30.

Milner,

Parrow and

Walker, A calculus of mobile processes, I, Inf. Comput.100(1) (1992), 1–40. doi:10.1016/0890-5401(92)90008-4.

31.

Parma and

Segala, Logical characterizations of bisimulations for discrete probabilistic systems, in: International Conference on Foundations of Software Science and Computational Structures, Springer, 2007, pp. 287–301.

32.

M.K.

Reiter and

A.D.

Rubin, Crowds: Anonymity for web transactions, ACM Trans. Inf. Syst. Secur.1(1) (1998), 66–92. doi:10.1145/290163.290168.

33.

Segala and

Lynch, Probabilistic simulations for probabilistic processes, Nordic Journal of Computing2(2) (1995), 250–273.

34.

Stoelinga, Alea jacta est: Verification of probabilistic, real-time and parametric systems, PhD thesis, University of Nijmegen, the Netherlands, 2002.

35.

The DeepSec tool, 2023, https://github.com/DeepSec-prover/deepsec/tree/probability.

36.

R.J.

van Glabbeek, Bounded nondeterminism and the approximation induction principle in process algebra, in: Annual Symposium on Theoretical Aspects of Computer Science, Springer, 1987, pp. 336–347.