On the semantics of communications when verifying equivalence properties

Abstract

Symbolic models for security protocol verification were pioneered by Dolev and Yao in their seminal work. Since then, although inspired by the same ideas, many variants of the original model were developed. In particular, a common assumption is that the attacker has complete control over the network and can therefore intercept any message. This assumption has been interpreted in slightly different ways depending on the particular models: either any protocol output is directly routed to the adversary, or communications may be among any two participants, including the attacker – the scheduling between which exact parties the communication happens is left to the attacker. This difference may seem unimportant at first glance and, depending on the verification tools, either one or the other semantics is implemented. We show that, unsurprisingly, they indeed coincide for reachability properties. However, for indistinguishability properties, we prove that these two interpretations lead to incomparable semantics. We also introduce and study a new semantics, where internal communications are allowed but messages are always eavesdropped by the attacker. This new semantics yields strictly stronger equivalence relations. Moreover, we identify two subclasses of protocols for which the three semantics coincide. Finally, we implemented verification of trace equivalence for each of the three semantics in the DeepSec tool and compare their performances on several classical examples.

Keywords

Cryptographic protocols symbolic models verification semantics equivalence properties

1. Introduction

Automated, symbolic analysis of security protocols, based on the seminal ideas of Dolev and Yao, comes in many variants. All of these models however share a few fundamental ideas:

messages are represented as abstract terms,

adversaries are computationally unbounded, but may manipulate messages only according to pre-defined rules (this is sometimes referred to as the perfect cryptography assumption), and

the adversary completely controls the network.

In this paper we will revisit this last assumption. Looking more precisely at different models we observe that this assumption may actually slightly differ among the models. The fact that the adversary controls the network is supposed to represent a worst case assumption.

In some models this assumption translates to the fact that every protocol output is sent to the adversary, and every protocol input is provided by the adversary. This is the case in the original Dolev Yao model and also in the models underlying several tools, such as AVISPA [8], Scyther [20], Tamarin [27], Millen and Shmatikov’s constraint solver [24], and the model used in Paulson’s inductive approach [25]. We will refer to this choice of semantics as the private semantics, as internal communications are only allowed on private channels.

Some other models, such as those based on process algebras, e.g. work based on CSP [26], the Spi [3] and applied pi calculus [1], but also the strand space model [28], consider a slightly different communication model: any two agents may communicate. Scheduling whether communication happens among two honest participants, or a honest participant and the attacker is under the attacker’s control. We will refer to this choice of semantics as the classical semantics, as it corresponds to what is generally used in process calculi.

When considering reachability properties, these two communication models indeed coincide: intuitively, any internal communication could go through the adversary who acts as a relay and increases his knowledge by the transmitted message. However, when considering indistinguishability properties, typically modelled as process equivalences, these communication models diverge. Interestingly, when forbidding internal communication, i.e., forcing all communication to be relayed by the attacker, we may weaken the attacker’s distinguishing power. This observation may seem counter-intuitive at first. However, executing a (non-observable) internal communication may enable actions that are otherwise only available after an observable input. These actions may then provide additional capabilities for simulating the other process.

In many recent work privacy properties have been modelled using process equivalences, see for instance [6,21,22]. The number of tools able to verify such properties is also increasing [12–14,16,18,29]. For instance, the AKISS [13] and SAT-EQUIV [18] tools do not allow any direct communication on public channels, while the APTE [14] and DeepSec [16] tools allow for internal communications. One motivation for disallowing direct communication is that it allows for more efficient verification (as less actions need to be considered and the number of interleavings to be considered is smaller).

Our contributions. We have formalised three semantics in the applied pi calculus which differ by the way communication is handled:

the classical semantics (as in the original applied pi calculus) allows both internal communication among honest participants and communication with the adversary;

the private semantics allows internal communication only on private channels while all communication on public channels is routed through the adversary;

the eavesdropping semantics which allows internal communication, but as a side-effect adds the transmitted message to the adversary’s knowledge.

For each of the new semantics we define may-testing and observational equivalences. We also define corresponding labelled semantics and trace equivalence and bisimulation relations (which may serve as proof techniques).

We show that, as expected, the three semantics coincide for reachability properties. For equivalence properties we show that the classical and private semantics yield incomparable equivalences, while the eavesdropping semantics yields strictly stronger equivalence relations than both other semantics. The results are summarized in Fig. 4.

An interesting question is whether these semantics coincide for specific subclasses of processes. We note that the processes that witness the differences in the semantics do not use replication, private channels, nor terms other than names, and no equational theory. Moreover, all except one of these examples only use trivial else branches (of the form $else 0$ ); the use of a non-trivial else branch can even be avoided by allowing a single free symbol.

We first study different notions of determinate processes: in the context of the applied pi calculus, Cheval et al. [15] have for instance shown that observational, testing, trace equivalence and labelled bisimulation coincide for this class of processes (for the classic semantics). We will show that this is actually the case for all semantics and show, among others that the private and eavesdropping semantics do coincide on these equivalences, and imply them for the classic semantics. We consider several specific subclasses of determinate processes when we bound the number of sessions. In particular, we show that all equivalences and semantics coincide for the class of strong action determinate processes. This class is of practical importance as this condition is checked in the AKISS and DeepSec tools to enable partial order reduction optimizations [10]. These optimizations provide spectacular speed-ups, but they were designed and shown correct only in the private semantics. Showing that all three semantics coincide for strong action determinate processes lifts the benefit of these optimizations to the other semantics. The results on subclasses of determinate processes are summarized in Fig. 8.

We also identify a syntactic class of processes, that we call I/O-unambiguous. For this class we forbid communication on private channels, communication of channel names and an output may not be sequentially followed by an input on the same channel directly, or with only conditionals in between. Note however that I/O-unambiguous processes, unlike most determinate processes, do allow outputs and inputs on the same channel in parallel. We show that for this class the eavesdropping semantics (which is the most strict relation) coincides with the private one (which is the most efficient for verification).

Finally, we extended the DeepSec tool to support verification of trace equivalence for the three semantics. Verifying existing protocols in the DeepSec example repository we verified that the results, fortunately, coincided for each of the semantics. We also made slight changes to the encodings, renaming some channels, to make them I/O-unambiguous. Interestingly, using different channels, significantly increased the performance of the tool. Finally, we also observed that, as expected, the private semantics yields more efficient verification. The results of our experiments are summarized in Section 5.

A preliminary version of this work appeared in [9]. In contrast to [9], this work contains full proofs of all results, new results for several subclasses of processes, giving a detailed comparison of the different semantics and equivalences, as well as an implementation of all three semantics in the DeepSec tool, together with an experimental evaluation.

Outline. In Section 2 we define the three semantics we consider. In Section 3 we present our main results on comparing these semantics. We present subclasses for which (some) semantics coincide in Section 4 and compare the performances when verifying protocols for different semantics using DeepSec in Section 5, before concluding in Section 6.

2. Model

The applied pi calculus [1] is a variant of the pi calculus that is specialised for modelling cryptographic protocols. Participants in a protocol are modelled as processes and the communication between them is modelled by message passing on channels. In this section, we describe the syntax and semantics of the applied pi calculus as well as the two new variants that we study in this paper.

2.1. Syntax

We consider an infinite set $N$ of names of base type and an infinite set $C h$ of names of channel type. We also consider an infinite set of variables $X$ of base type and channel type and a signature $F$ consisting of a finite set of function symbols. We rely on a sort system for terms. In particular, the sort base type differs from the sort channel type. Moreover, any function symbol can only be applied to and returns base type terms. We define terms as names, variables and function symbols applied to other terms. Given $N \subseteq N$ , $X \subseteq X$ and $F \subseteq F$ , we denote by $T (F, X, N)$ the sets of terms built from X and N by applying function symbols from F. We denote $v (t)$ the sets of variables occurring in t. We say that t is ground if $v (t) = \emptyset$ . We describe the behaviour of cryptographic primitives by the means of an equational theory $E$ that is a relation on terms closed under substitutions of terms for variables and closed under one-to-one renaming. Given two terms u and v, we write $u =_{E} v$ when u and v are equal modulo the equational theory.

In the original syntax of the applied pi calculus, there is no distinction between an output (resp. input) from a protocol participant and from the environment, also called the attacker. In this paper however, we will make this distinction in order to concisely present our new variants of the semantics. Therefore, we consider two process tags $ho$ and $at$ that respectively represent honest and attacker actions. The syntax of plain processes and extended processes is given in Fig. 1.

Fig. 1.

Syntax of processes.

The process ${out}^{θ} (c, u)$ represents the output by θ of the message u on the channel c. The process ${in}^{θ} (c, x)$ represents an input by θ on the channel c. The input message will instantiate the variable x. The process $eav (c, x)$ models the capability of the attacker to eavesdrop a communication on channel c. The process $! P$ represents the replication of the process P, i.e. unbounded number of copies of P. The process $P ∣ Q$ represents the parallel composition of P and Q. The process $ν n . P$ (resp. $ν x . A$ ) is the restriction of the name n in P (resp. variable x in A). The process $if u = v then P else Q$ is the conditional branching under the equality test $u = v$ . The process $ω c$ records that a private channel c has been opened, i.e., it has been sent on a public or previously opened channel. Finally, the substitution ${^{u} /_{x}}$ is an active substitution that replaces the variable x with the term u of base type.

We say that a process P (resp. extended process A) is an honest process (resp. honest extended process) when all inputs and outputs in P (resp. A) are tagged with $ho$ and when P (resp. A) does not contain eavesdropping processes and $ω c$ . We say that a process P (resp. extended process A) is an attacker process (resp. attacker extended process) when all inputs and outputs in P (resp. A) are tagged with $at$ .

As usual, names and variables have scopes which are delimited by restrictions, inputs and eavesdrops. We denote $fv (A), bv (A), fn (A), bn (A)$ the sets of free variables, bound variables, free names and bound names respectively in A. Moreover, we denote by $o c (A)$ the sets of terms c of channel type opened in A, i.e. that occurs in a process $ω c$ . We say that an extended process A is closed when all variables in A are either bound or defined by an active substitution in A. We define an evaluation context $C [_]$ as an extended process with a hole instead of an extended process. As for processes, we define an attacker evaluation context as an evaluation context where all outputs and inputs in the context are tagged with $at$ .

Note that our syntax without the eavesdropping process, opened channels and tags correspond exactly to the syntax of the original applied pi calculus.

Lastly, we consider the notion of frame that are extended processes built from 0, parallel composition, name and variable restrictions and active substitution. Given a frame φ, we consider the domain of φ, denoted $dom (φ)$ , as the set of free variables in φ that are defined by an active substitution in φ. Given an extended process A, we define the frame of A, denoted $ϕ (A)$ , as the process A where we replace all plain processes by 0. Finally, we write $dom (A)$ as syntactic sugar for $dom (ϕ (A))$ .

2.2. Operational semantics

In this section, we define the three semantics that we study in this paper, namely:

the classical semantics from the applied pi calculus, where internal communication can occur on both public and private channels;

the private semantics where internal communication can only occur on private channels; and

the eavesdropping semantics where the attacker is able to eavesdrop on a public channel.

We first define the structural equivalence between extended processes, denoted ≡, as the smallest equivalence relation on extended processes that is closed under renaming of names and variables, closed by application of evaluation contexts, that is associative and commutative w.r.t. ∣, and such that: $\begin{matrix} A & \equiv & A ∣ 0 & ! P & \equiv & ! P ∣ P & ν n .0 & \equiv & 0 \\ ν i . ν j . A & \equiv & ν j . ν i . A & ν x . {^{u} /_{x}} & \equiv & 0 & {^{u} /_{x}} ∣ A & \equiv & {^{u} /_{x}} ∣ A {^{u} /_{x}} \\ A ∣ ν i . B & \equiv & ν i . (A ∣ B) & when i \notin fv (A) \cup fn (A) & ω c \equiv ω c ∣ ω c \\ {^{u} /_{x}} & \equiv & {^{v} /_{x}} & when u =_{E} v \end{matrix}$

The three operational semantics of extended processes are defined by the structural equivalence and by three respective internal reductions, denoted $\to_{c}$ , $\to_{p}$ and $\to_{e}$ . These three reductions are the smallest relations on extended processes that are closed under application of evaluation context, structural equivalence and such that: $\begin{array}{l} \begin{matrix} if u = v then P else Q {\overset{τ}{\to}}_{s} P where u =_{E} v and s \in {c, p, e} & T HEN \\ if u = v then P else Q {\overset{τ}{\to}}_{s} Q & E LSE \\ where u, v ground, u \neq_{E} v and s \in {c, p, e} \\ {out}^{θ} (c, u) . P ∣ {in}^{θ^{'}} (c, x) . Q {\overset{τ}{\to}}_{c} P ∣ Q {^{u} /_{x}} & C OMM \end{matrix} \\ \begin{matrix} ν c . ({out}^{θ} (c, u) . P ∣ {in}^{θ^{'}} (c, x) . Q ∣ R) {\overset{τ}{\to}}_{s} ν c . (P ∣ Q {^{u} /_{x}} ∣ R) & C - P RIV \\ where c \notin o c (R) and s \in {p, e} \\ {out}^{θ} (c, u) . P ∣ {in}^{θ^{'}} (c, x) . Q {\overset{τ}{\to}}_{s} P ∣ Q {^{u} /_{x}} & C - E NV \\ at \in {θ, θ^{'}}, u is of base type and s \in {p, e} \\ {out}^{θ} (c, d) . P ∣ {in}^{θ^{'}} (c, x) . Q {\overset{τ}{\to}}_{s} P ∣ Q {^{d} /_{x}} ∣ ω d & C - O PEN \\ at \in {θ, θ^{'}}, d is of channel type and s \in {p, e} \\ {out}^{ho} (c, u) . P ∣ {in}^{ho} (c, x) . Q ∣ eav (c, y) . R {\overset{τ}{\to}}_{e} P ∣ Q {^{u} /_{x}} ∣ R {^{u} /_{y}} & C - E AV \\ where u is of base type \\ {out}^{ho} (c, d) . P ∣ {in}^{ho} (c, x) . Q ∣ eav (c, y) . R {\overset{τ}{\to}}_{e} P ∣ Q {^{d} /_{x}} ∣ R {^{d} /_{y}} ∣ ω d & C - OE AV \\ where d is of channel type \end{matrix} \end{array}$ We emphasise that the application of the rule is closed under application of arbitrary evaluation contexts. In particular the context may restrict channels, e.g. the rule C-Open may be used under the context $ν c ._$ resulting in a private channel c, but with the attacker input/output being in the scope of this restriction. It follows from the definition of evaluation contexts that the resulting processes are always well defined. We denote by $\Rightarrow_{s}$ the reflexive, transitive closure of ${\overset{τ}{\to}}_{s}$ for $s \in {c, p, e}$ . We note that the classical semantics ${\overset{τ}{\to}}_{c}$ is independent of the tags $θ, θ^{'}$ , the eavesdrop actions and the $ω c$ processes.

Example 1.
Consider the process $\begin{matrix} A = (ν d . {out}^{θ} (c, d) . {in}^{θ} (d, x) . P) ∣ ({in}^{θ^{'}} (c, y) . {out}^{θ^{'}} (y, t) . Q) \end{matrix}$ where d is a channel name and t a term of base type. Suppose $θ = θ^{'} = ho$ then we have that communication is only possible in the classical semantics (using twice the Comm rule): $\begin{matrix} A {\overset{τ}{\to}}_{c} & ν d . ({in}^{θ} (d, x) . P ∣ {out}^{θ^{'}} (d, t) . Q {^{d} /_{y}}) \\ {\overset{τ}{\to}}_{c} & ν d . (P {^{t} /_{x}} ∣ Q {^{d} /_{y}}) \end{matrix}$ while no transitions are available in the two other semantics. To enable communication in the eavesdropping semantics we need to explicitly add eavesdrop actions. Applying the rules C-OEav and C-Eav we have that $\begin{matrix} A ∣ eav (c, z_{1}) . eav (z_{1}, z_{2}) . R {\overset{τ}{\to}}_{e} & ν d . ({in}^{θ} (d, x) . P ∣ {out}^{θ^{'}} (d, t) . Q {^{d} /_{y}} \\ ∣ eav (d, z_{2}) . R {^{d} /_{z_{1}}} ∣ ω d) \\ {\overset{τ}{\to}}_{e} & ν d . (P {^{t} /_{x}} ∣ Q {^{d} /_{y}} ∣ R {^{d} /_{z_{1}}} {^{t} /_{z_{2}}} ∣ ω d) \end{matrix}$ We note that the first transition adds the information $ω d$ to indicate that d is now available to the environment.

Finally, if we consider that $at \in {θ, θ^{'}}$ then internal communication on a public channel is possible and, using rules C-Open and C-Env we obtain for $s \in {p, e}$ that $\begin{matrix} A {\overset{τ}{\to}}_{s} & ν d . ({in}^{θ} (d, x) . P ∣ {out}^{θ^{'}} (d, t) . Q {^{d} /_{y}} ∣ ω d) \\ {\overset{τ}{\to}}_{s} & ν d . (P {^{t} /_{x}} ∣ Q {^{d} /_{y}} ∣ ω d) \end{matrix}$

2.3. Reachability and behavioural equivalences

We are going to compare the relation between the three semantics for the two general kind of security properties, namely reachability properties encoding security properties such as secrecy, authentication, and equivalence properties encoding properties such as anonymity, unlinkability, strong secrecy, and receipt freeness. Intuitively, reachability properties encode that a process cannot reach some bad state. Equivalences define the fact that no attacker can distinguish two processes. This was originally defined by the (may)-testing equivalence [3] in the spi-calculus. An alternate equivalence, which was considered in the applied pi calculus [1], is observational equivalence.

Reachability properties can simply be encoded by verifying the capability of a process to perform an output on a given channel. We define $A ⇓_{c}^{s, θ}$ to hold when $A \Rightarrow_{s} C [{out}^{θ} (c, t) . P]$ for some evaluation context C that does not bind c, some term t and some plain process P, and $A ⇓_{c}^{s}$ to hold when $A ⇓_{c}^{s, θ}$ for some $θ \in {at, ho}$ . For example the secrecy of s in the process $ν s . A$ can be encoded by checking whether for all attacker plain process I, we have that $\begin{matrix} I ∣ ν s . (A ∣ {in}^{ho} (c, x) . if x = s then {out}^{ho} (bad, s)) {⇓̸}_{bad}^{s, ho} \end{matrix}$ where $bad \notin fn (A)$ .

Authentication properties are generally expressed as correspondence properties between events annotating processes, see e.g. [11]. A correspondence property between two events $begin$ and $end$ , denoted $begin \Leftarrow end$ , requires that the event $end$ is preceded by the event $begin$ on every trace. A possible encoding of this correspondence property consists in first replacing all instances of the events in A by outputs ${out}^{ho} (e v, begin)$ and ${out}^{ho} (e v, end)$ where $e v \notin fn (A) \cup bn (A)$ . This new process $A^{'}$ can then be put in parallel with a cell $Cell$ that reads on the channel $e v$ and stores any new value unless the value is $end$ and the current stored value in the cell is not $begin$ . In such a case, the cell will output on the channel $bad$ . The correspondance property can therefore be encoded by checking whether for all attacker plain process I, we have that $I ∣ ν e v . (A^{'} ∣ Cell) {⇓̸}_{bad}^{s, ho}$ .

We say that an attacker evaluation context $C [_]$ is $c$ -closing for an extended process A if $fv (C [A]) = \emptyset$ . For $s \in {p, e}$ , we say that $C [_]$ is s-closing for A if it is $c$ -closing for A, variables and names are bound only once in $C [_]$ and for all channels $c \in bn (C [_]) \cap fn (A)$ , if the scope of c includes $_$ then the scope of c also includes $ω c$ .

We next introduce the two main notions of behavioural equivalences: may testing and observational equivalence.

Definition 1 ((May-)Testing equivalences $\approx_{m}^{c}$ , $\approx_{m}^{p}$ , $\approx_{m}^{e}$ ).

Let $s \in {c, p, e}$ . Let A and B two closed honest extended processes such that $dom (A) = dom (B)$ . We say that $A \approx_{m}^{s} B$ if for all attacker evaluation contexts $C [_]$ s-closing for A and B, for all channels c, we have that $C [A] ⇓_{c}^{s}$ if and only if $C [B] ⇓_{c}^{s}$ .

Definition 2 (Observational equivalences $\approx_{o}^{c}$ , $\approx_{o}^{p}$ , $\approx_{o}^{e}$ ).

Let $s \in {c, p, e}$ . Let A and B two closed extended processes such that $dom (A) = dom (B)$ . We say that $A \approx_{o}^{s} B$ if $\approx_{o}^{s}$ is the largest equivalence relation such that:

$A ⇓_{c}^{s}$ implies $B ⇓_{c}^{s}$ ;

$A {\overset{τ}{\to}}_{s} A^{'}$ implies $B \Rightarrow ϵ_{s} B^{'}$ and $A^{'} \approx_{o}^{s} B^{'}$ for some $B^{'}$ ;

$C [A] \approx_{o}^{s} C [B]$ for all attacker evaluation contexts $C [_]$ s-closing for A and B.

For each of the semantics we have the usual relation between these two notions: observational equivalence implies testing equivalence.

Proposition 1.
$\approx_{o}^{s} ⊊ \approx_{m}^{s}$ for $s \in {c, e, p}$ .
Example 2.
Consider processes A and B of Fig. 2. Process A computes a value $h^{n} (a)$ to be output on channel c, where $h^{n} (a)$ denotes n applications of h and $h^{0} (a) = a$ . The value is initially a and A may choose to either output the current value, or update the current value by applying the free symbol h. B may choose non-deterministically to either behave as A or output the fresh name s. (The non-deterministic choice is encoded by a communication on the private channel e which may be received by either the process behaving as A or the process outputting s.)

We have that $A ≉_{o}^{s} B$ . The two processes can indeed be distinguished by the context $\begin{matrix} C [_] & \hat{=}_ & ∣ {out}^{at} (c_{a}, a) ∣! ({in}^{at} (c_{a}, x) . {out}^{at} (c_{a}, h (x)) \\ ∣ {in}^{at} (c_{a}, y) . {in}^{at} (c, z) . if y = z then {out}^{at} (c_{t}, h (x)) \end{matrix}$ Intuitively, when B outputs s the attacker context $C [_]$ can iterate the application of h the same number of times as would have done process A. Comparing the value computed by the adversary ( $h^{n} (a)$ ) and the honestly computed value (either $h^{n} (a)$ or s) the adversary distinguishes the two processes by outputting on the test channel $c_{t}$ .

However, we have that $A \approx_{m}^{s} B$ . Indeed, for any s-closing context $D [_]$ and all public channel $ch$ we have that $D [A] ⇓_{ch}^{s}$ if and only if $D [B] ⇓_{ch}^{s}$ . In particular for context $C [_]$ defined above we have that both $C [A] ⇓_{ch}^{s}$ and $C [B] ⇓_{ch}^{s}$ for $ch \in {c_{a}, c_{t}, c}$ . Unlike observational equivalence, may testing does not require to “mimic” the other process stepwise and we cannot force a process into a particular branch.

Fig. 2.
Processes A and B such that $A \approx_{m}^{s} B$ , but $A ≉_{o}^{s} B$ and $A ≉_{t}^{s} B$ for $s \in {c, e, p}$ .
2.4. Labelled semantics

The internal reduction semantics introduced in the previous section requires to reason about arbitrary contexts. Similar to the original applied pi calculus, we extend the three operational semantics by a labeled operational semantics which allows processes to directly interact with the (adversarial) environment: we define the relation ${\overset{ℓ}{\to}}_{c}$ , ${\overset{ℓ}{\to}}_{p}$ and ${\overset{ℓ}{\to}}_{e}$ where ℓ is part of the alphabet $A = {τ, out (c, d), eav (c, d), in (c, w), ν k . out (c, k), ν k . eav (c, k) ∣ c, d \in C h, k \in X \cup C h and w is a term of any sort}$ . The labeled rules are given in Fig. 3.

Fig. 3.

Labeled semantics.

Consider our alphabet of actions $A$ defined above. Given $w \in A^{*}$ , $s \in {c, p, e}$ and an extended process A, we say that $A {\overset{w}{\to}}_{s} A_{n}$ when $A {\overset{ℓ_{1}}{\to}}_{s} A_{1} {\overset{ℓ_{2}}{\to}}_{s} A_{2} {\overset{ℓ_{3}}{\to}}_{s} \dots {\overset{ℓ_{n}}{\to}}_{s} A_{n}$ for some extended processes $A_{1}, \dots, A_{n}$ and $w = ℓ_{1} \cdot \dots \cdot ℓ_{n}$ . By convention, we say that $A {\overset{ϵ}{\to}}_{s} A$ where ϵ is the empty word. Given $tr \in {(A ∖ {τ})}^{*}$ , we say that $A \Rightarrow {tr}_{s} A^{'}$ when there exists $w \in A^{*}$ such that $tr$ is the word w where we remove all τ actions and $A {\overset{w}{\to}}_{s} A^{'}$ .

Example 3.

Coming back to Example 1, we saw that $A {\overset{τ}{\to}}_{c} {\overset{τ}{\to}}_{c} ν d . (P {^{t} /_{x}} ∣ Q {^{d} /_{y}})$ and no τ-actions in the other two semantics were available. Instead of explicitly adding eavesdrop actions, we can apply the rules Eav-OCh and Eav-T and obtain that $\begin{matrix} A {\overset{ν d . eav (c, d)}{\to}}_{e} & {in}^{ho} (d, x) . P ∣ {out}^{ho} (d, t) . Q {^{d} /_{y}}) \\ {\overset{ν z . eav (d, z)}{\to}}_{e} & P {^{t} /_{x}} ∣ Q {^{d} /_{y}} ∣ {^{t} /_{z}} \end{matrix}$

We can now define both reachability and different equivalence properties in terms of these labelled semantics and relate them to the internal reduction. To define reachability properties in the labelled semantics, we define $A ⇊_{c}^{s}$ to hold when $A \Rightarrow tr A^{'}$ , $tr = {tr}_{1} out (c, t) {tr}_{2}$ and ${tr}_{1}$ does not bind c for some $tr, {tr}_{1}, {tr}_{2} \in {(A ∖ {τ})}^{*}$ , term t and extended process $A^{'}$ .

The following proposition states that any reachability property modelled in terms of $A ⇓_{c}^{s, θ}$ and universal quantification over processes, can also be expressed using $A ⇊_{c}^{s}$ without the need to quantify over processes.

Proposition 2.

For all closed honest plain processes A, for all $s \in {c, e, p}$ , $A ⇊_{c}^{s}$ iff there exists an attacker plain process $I^{s}$ such that $I^{s} ∣ A ⇓_{c}^{s, ho}$ .

Next, we define equivalence relations using our labelled semantics that may serve as proof techniques for the may testing relation. First we need to define an indistinguishability relation on frames, called static equivalence [1].

Definition 3 (Static equivalence ∼).

Two terms u and v are equal in the frame ϕ, written $(u =_{E} v) ϕ$ , if there exists $\tilde{n}$ and a substitution σ such that $ϕ \equiv ν \tilde{n} . σ$ , $\tilde{n} \cap (fn (u) \cup fn (v)) = \emptyset$ , and $u σ =_{E} v σ$ .

Two closed frames $ϕ_{1}$ and $ϕ_{2}$ are statically equivalent, written $ϕ_{1} \sim ϕ_{2}$ , when:

$dom (ϕ_{1}) = dom (ϕ_{2})$ , and

for all terms $u, v$ we have that: $(u =_{E} v) ϕ_{1}$ if and only if $(u =_{E} v) ϕ_{2}$ .

Example 4.
Consider the equational theory generated by the equation $dec (enc (x, y), y) = x$ . Then we have that $\begin{matrix} ν k . {^{enc (a, k)} /_{x_{1}}} & \sim & ν k . {^{enc (b, k)} /_{x_{1}}} \\ ν k . {^{enc (a, k)} /_{x_{1}},^{k} /_{x_{2}}} & ≁ & ν k . {^{enc (b, k)} /_{x_{1}},^{k} /_{x_{2}}} \\ ν k, a . {^{enc (a, k)} /_{x_{1}},^{k} /_{x_{2}}} & \sim & ν k, b . {^{enc (b, k)} /_{x_{1}},^{k} /_{x_{2}}} \end{matrix}$ Intutively, the first equivalence confirms that encryption hides the plaintext when the decryption key is unknown. The second equivalence does not hold as the test $(dec (x_{1}, x_{2}) =_{E} a)$ holds on the left hand side, but not on the right hand side. Finally, the third equivalence again holds as two restricted names are indistinguishable.

Now we are ready to define two classical equivalences on processes, based on the labelled semantics: trace equivalence and labelled bisimulation.
Definition 4 (Trace equivalences $\approx_{t}^{c}$ , $\approx_{t}^{p}$ , $\approx_{t}^{e}$ ).

Let $s \in {c, p, e}$ . Let A and B be two closed honest extended processes. We say that $A ⊑_{t}^{s} B$ if for all $A \Rightarrow {tr}_{s} A^{'}$ such that $bn (tr) \cap fn (B) = \emptyset$ , there exists $B^{'}$ such that $B \Rightarrow {tr}_{s} B^{'}$ and $ϕ (A^{'}) \sim ϕ (B^{'})$ . We say that $A \approx_{t}^{s} B$ when $A ⊑_{t}^{s} B$ and $B ⊑_{t}^{s} A$ .

Definition 5 (Labeled bisimulations $\approx_{ℓ}^{c}$ , $\approx_{ℓ}^{p}$ , $\approx_{ℓ}^{e}$ ).

Let $s \in {c, p, e}$ . Let A and B two closed honest extended processes such that $dom (A) = dom (B)$ . We say that $A \approx_{ℓ}^{s} B$ if $\approx_{ℓ}^{s}$ is the largest equivalence relation such that:

$ϕ (A) \sim ϕ (B)$

$A {\overset{τ}{\to}}_{s} A^{'}$ implies $B \Rightarrow ϵ_{s} B^{'}$ and $A^{'} \approx_{ℓ}^{s} B^{'}$ for some $B^{'}$ ,

$A {\overset{ℓ}{\to}}_{s} A^{'}$ and $bn (ℓ) \cap fn (B) = \emptyset$ implies $B \Rightarrow ℓ_{s} B^{'}$ and $A^{'} \approx_{ℓ}^{s} B^{'}$ for some $B^{'}$ .

We again have, as usual that labelled bisimulation implies trace equivalence.

Proposition 3.
$\approx_{ℓ}^{s} ⊊ \approx_{t}^{s}$ for $s \in {c, e, p}$ .

In [1] it is shown that $\approx_{o}^{c} = \approx_{ℓ}^{c}$ . We conjecture that for the new semantics $p$ and $e$ this same equivalence holds as well. Re-showing these results is beyond the scope of this paper, and we will mainly focus on testing/trace equivalence. As shown in [15], for the classical semantics trace equivalence implies may testing, while the converse does not hold in general. The two relations do however coincide on image-finite processes.
Definition 6.
Let A be a closed extended process. A is image-finite for the semantics $s \in {c, e, p}$ if for each trace $tr$ the set of equivalence classes ${ϕ (B) ∣ A \Rightarrow {tr}_{s} B} / \sim$ is finite.

Note that any replication-free process is necessarily image-finite as there are only a finite number of possible traces for any given sequence of labels $tr$ . The same relations among trace equivalence and may testing shown for the classical semantics hold also for the other semantics.
Theorem 1.
$\approx_{t}^{s} ⊊ \approx_{m}^{s}$ and $\approx_{t}^{s} = \approx_{m}^{s}$ on image-finite processes for $s \in {c, e, p}$ .

The proof of this result (for the classical semantics) is given in [15] and is easily adapted to the other semantics. To see that the implication is strict, we continue Example 2 on processes A and B defined in Fig. 2. We already noted that $A \approx_{m}^{s} B$ , but will now show that $A ≉_{t}^{s} B$ (for $s \in {c, e, p}$ ). All possible traces of A are of the form $A \Rightarrow {ν x . out (c, x)}_{s} A^{'}$ where $ϕ (A^{'}) = {^{h^{n} (a)} / x}$ for $n \in N$ . We easily see that $A ≉_{t}^{s} B$ as for any n we have that ${^{h^{n} (a)} /_{x}} ≁ {^{s} /_{x}}$ , by testing $x = h^{n} (a)$ . On the other hand, given an image-finite process, we can only have a finite number of different frames for a given trace, and therefore we can bound the context size that is necessary for distinguishing the processes.
3. Comparing the different semantics

In this section we state our results on comparing these semantics. Results on equivalence comparison are summarized in Fig. 4.

Fig. 4.

Overview of the results.

We first show that, as expected, all the semantics coincide for reachability properties.

Theorem 2.

For all ground, closed honest extended processes A, for all channels d, we have that $A ⇊_{d}^{p}$ iff $A ⇊_{d}^{c}$ iff $A ⇊_{d}^{e}$ .

The next result is, in our opinion, more surprising. As the private semantics force the adversary to observe all information, one might expect that his distinguishing power increases over the classical one. This intuition is however wrong: the classical and private trace equivalences, testing equivalence and labelled bisimulations appear to be incomparable.

Fig. 5.

Processes A and B such that $A \approx_{ℓ}^{p} B$ and $A ≉_{m}^{c} B$ .

Theorem 3.

$\approx_{r}^{p} ⊈ \approx_{r}^{c}$ and $\approx_{r}^{c} ⊈ \approx_{r}^{p}$ for $r \in {ℓ, t, m}$ .

Proof.

We show both statements separately.

$\approx_{r}^{p} ⊈ \approx_{r}^{c}$ . We first show that there exist A and B such that $A \approx_{ℓ}^{p} B$ , but $A ≉_{m}^{c} B$ . Note that, as $\approx_{ℓ}^{s} \subset \approx_{t}^{s} \subseteq \approx_{m}^{s}$ for $s \in {c, p}$ these processes demonstrate both that $\approx_{ℓ}^{p} ⊈ \approx_{ℓ}^{c}$ , $\approx_{t}^{p} ⊈ \approx_{t}^{c}$ and $\approx_{m}^{p} ⊈ \approx_{m}^{c}$ .

Consider processes A and B defined in Fig. 5. In short, the result follows from the fact that if A performs an internal communication on channel c followed by an output on d (from $P_{1}$ ), B has no choice other then performing the output on d in $P_{2}$ . In the private semantics, however, the internal communication will be split in an output followed by an input: after the output on c, the input ${in}^{ho} (c, x) . P_{2} (x)$ following the output becomes available. More precisely, to see that $A \approx_{ℓ}^{p} B$ we first observe that if $A {\overset{ν z . out (c, z)}{\to}}_{p} A^{'}$ then $B {\overset{ν z . out (c, z)}{\to}}_{p} B^{'}$ and $A^{'} \equiv B^{'}$ , and vice-versa. If $A {\overset{in (c, t)}{\to}}_{p} A^{'}$ then $B {\overset{in (c, t)}{\to}}_{p} B^{'}$ . As $t \notin {s_{1}, s_{2}}$ we have that $P_{1} (t) \approx_{ℓ}^{p} 0 \approx_{ℓ}^{p} P_{2} (t)$ . Finally, if $t \neq s_{2}$ we also have that $P_{1} (t) \approx_{ℓ}^{p} P_{2} (t)$ as in particular $P_{1} (s_{1}) \approx_{ℓ}^{p} P_{2} (s_{1})$ . Therefore, $\begin{matrix} ν s_{1} . ν s_{2} . ({out}^{ho} (c, s_{1}) . {in}^{ho} (c, x) . P_{1} (x)) \approx_{ℓ}^{p} ν s_{1} . ν s_{2} . ({out}^{ho} (c, s_{1}) . {in}^{ho} (c, x) . P_{2} (x)) \end{matrix}$ which allows us to conclude.

As A and B are image-finite, we have that $A \approx_{m}^{c} B$ if and only if $A \approx_{t}^{c} B$ . To see that $A ≉_{t}^{c} B$ we observe that A may perform the following transition sequence, starting with an internal communication on a public channel: $\begin{matrix} A {\overset{τ}{\to}}_{c} & ν s_{1} . ν s_{2} . (({in}^{ho} (c, x) . P_{1} (x)) ∣ (P_{2} (s_{1}))) \\ \Rightarrow {ν z . out (d, z)}_{c} & ν s_{1} . ν s_{2} . (({in}^{ho} (c, x) . P_{1} (x)) ∣ {^{s_{2}} /_{z}}) \\ {\overset{in (c, z)}{\to}}_{c} & ν s_{1} . ν s_{2} . (P_{1} (s_{2}) ∣ {^{s_{2}} /_{z}}) \end{matrix}$ In order to mimic the behaviour of A, B must perform the same sequence of observable transitions: $\begin{matrix} B \Rightarrow {ν z . out (d, z) in (c, z)}_{c} ν s_{1} . ν s_{2} . (P_{2} (s_{2}) ∣ {^{s_{2}} /_{z}}) \end{matrix}$ We conclude as $ν s_{1} . ν s_{2} . (P_{1} (s_{2}) ∣ {^{s_{2}} /_{z}}) \overset{ν z^{'} . out (e, z^{'})}{\to} ν s_{1} . ν s_{2} . ({^{s_{2}} /_{z}} ∣ {^{s_{2}} /_{z^{'}}})$ , but $ν s_{1} . ν s_{2} . (P_{2} (s_{2}) ∣ {^{s_{2}} /_{z}}) \overset{ν z^{'} . out (e, z^{'})}{↛}$ . This trace inequivalence has also been shown using DeepSec.

$\approx_{r}^{c} ⊈ \approx_{r}^{p}$ . To show that $\approx_{r}^{c} ⊈ \approx_{r}^{p}$ for $r \in {ℓ, t, m}$ we show that there exist processes A and B such that $A \approx_{ℓ}^{c} B$ and $A ≉_{m}^{p} B$ . As in the first part of the proof, note that, as $\approx_{ℓ}^{s} \subset \approx_{t}^{s} \subseteq \approx_{m}^{s}$ for $s \in {c, p}$ these processes demonstrate that $\approx_{ℓ}^{c} ⊈ \approx_{ℓ}^{p}$ , $\approx_{t}^{c} ⊈ \approx_{t}^{p}$ and $\approx_{m}^{c} ⊈ \approx_{m}^{p}$ .

Consider the processes A and B defined in Fig. 6. The proof crucially relies on the fact that B may perform an internal communication in the classical semantics to mimic A, which becomes visible in the attacker in the private semantics. To see that $A \approx_{ℓ}^{c} B$ we first observe that the only first possible action from A or B is an input. In particular, given a term t, there is a unique $B^{'}$ such that $B \overset{in (c, t)}{\to} B^{'}$ where $B^{'} = ν s . ({out}^{ho} (c, s) . {out}^{ho} (d, a) ∣ {in}^{ho} (c, y) . P (y))$ . However, if $A \overset{in (c, t)}{\to} A^{'}$ then either $A^{'} = B^{'}$ or $A^{'} = A^{″}$ with $A^{″} \hat{=} ν s . ({in}^{ho} (c, x) . {out}^{ho} (c, s) . {out}^{ho} (d, a) ∣ P (t))$ . Therefore, to complete the proof, we only need to find $B^{″}$ such that $B \Rightarrow in (c, t) B^{″}$ and $A^{″} \approx_{ℓ}^{c} B^{″}$ . Such a process can be obtained by applying an internal communication on $B^{'}$ , i.e. $B {\overset{in (c, t)}{\to}}_{c} B^{'} \overset{τ}{\to} ν s . ({out}^{ho} (d, a) ∣ P (s))$ . Note that $t \neq s$ since s is bound, meaning that $P (t) \approx_{ℓ}^{c} {out}^{ho} (d, a)$ . Moreover, $P (s) \approx_{ℓ}^{c} {in}^{ho} (c, x) . {out}^{ho} (c, s) . {out}^{ho} (d, a)$ . This allows us to conlude that $ν s . ({out}^{ho} (d, a) ∣ P (s)) \approx_{ℓ}^{c} A^{″}$ .

Again, as A and B are image-finite may and trace equivalence coincide. To see that $A ≉_{t}^{p} B$ we first observe that A may perform the following transition sequence: $\begin{matrix} A {\overset{in (c, t)}{\to}}_{p} A^{″} {\overset{τ}{\to}}_{p} & ν s . ({in}^{ho} (c, x) . {out}^{ho} (c, s) . {out}^{ho} (d, a) ∣ {out}^{ho} (d, a)) \\ {\overset{ν z . out (d, z)}{\to}}_{p} & ν s . ({in}^{ho} (c, x) . {out}^{ho} (c, s) . {out}^{ho} (d, a) ∣ {^{a} /_{z}}) \end{matrix}$ We conclude as $B {\overset{in (c, t)}{\to}}_{p} B^{'}$ but $B^{'} {\overset{ν z . out (d, z)}{↛}}_{p}$ . Violation of this trace equivalence has also been shown using the DeepSec tool. □

Fig. 6.

Processes A and B such that $A \approx_{ℓ}^{c} B$ and $A ≉_{m}^{p} B$ .

One may also note that the counter-example witnessing that equivalences in the private semantics do not imply equivalences in the classical semantics is minimal: it does not use function symbols, equational reasoning, private channels, replication nor else branches. The second part of the proof relies on the use of else branches. We can however refine this result in the case of labeled bisimulation to processes without else branches, the counter-example being the same processes A and B described in the proof but where we replace each ${out}^{ho} (d, a)$ by 0. In the case of trace equivalence, we can also produce a counter-example without else branches witnessing that trace equivalences in the classical semantics do no imply trace equivalences in the private semantics but provided that we rely on a function symbol h. In the Appendix, we describe in more details these processes and give the proofs of them being counter-examples.

Next, we show that the eavesdropping semantics yields strictly stronger bisimulations, trace and may testing equivalences: the eavesdropping semantics is actually strictly included in the intersection of the classic and private semantics.

Theorem 4.

$\approx_{t}^{e} ⊊ \approx_{t}^{p} \cap \approx_{t}^{c}$ .

Proof sketch.

We show the result in 3 steps: we show that (1) $\approx_{t}^{e} \subseteq \approx_{t}^{p}$ , (2) $\approx_{t}^{e} \subseteq \approx_{t}^{c}$ , and (3) that the implication is strict, i.e., there exist $A, B$ such that $A \approx_{t}^{p} B$ , $A \approx_{t}^{c} B$ and $A ≉_{t}^{e} B$ .

We first prove that $\approx_{t}^{e} \subseteq \approx_{t}^{p}$ . Suppose that $A \approx_{t}^{e} B$ . We need to show that for any $A^{'}$ such that $A \Rightarrow {tr}_{p} A^{'}$ there exists $B^{'}$ such that $B \Rightarrow {tr}_{p} B^{'}$ . It follows from the definition of the semantics that whenever $A \Rightarrow {tr}_{p} A^{'}$ then we also have $A \Rightarrow {tr}_{e} A^{'}$ as ${\overset{ℓ}{\to}}_{p} \subset {\overset{ℓ}{\to}}_{e}$ . As $A \approx_{t}^{e} B$ , we have that there exists $B^{'}$ , such that $B \Rightarrow {tr}_{e} B^{'}$ and $ϕ (A^{'}) \sim ϕ (B^{'})$ . As $tr$ does not contain labels of the form $eav (c, d)$ nor $ν y . e a v (c, y)$ and as no $C OMM - E AV$ are possible (A and B are honest processes) we also have that $B \Rightarrow {tr}_{p} B^{'}$ . Hence $A \approx_{t}^{p} B$ .

We next prove that $\approx_{t}^{e} \subseteq \approx_{t}^{c}$ . Similar to Item 1 we suppose that $A \approx_{t}^{e} B$ and $A \Rightarrow {tr}_{c}_{c} A_{c}^{'}$ . From the semantics, we obtain that $A \Rightarrow {tr}_{e}_{e} A_{e}^{'}$ , where

$ϕ (A_{c}^{'}) \subseteq ϕ (A_{e}^{'})$ , i.e., $dom (ϕ (A_{c}^{'})) \subseteq dom (ϕ (A_{e}^{'}))$ and the frames coincide on the common domain.

${tr}_{e}$ is constructed from ${tr}_{c}$ by replacing any τ action resulting from the $C OMM$ rule by an application of an eavesdrop rule ( $E AV - T$ , $E AV - C H$ , or $E AV - OC H$ ).

The proof is done by induction on the length of

{tr}_{c}

and the proof tree of each transition. As

A \approx_{t}^{e} B

we also have that

B \Rightarrow {tr}_{e}_{e} B_{e}^{'}

and

A_{e}^{'} \sim B_{e}^{'}

. We show by the definition of the semantics that

B \Rightarrow {tr}_{c}_{c} B_{c}^{'}

and

ϕ (B_{c}^{'}) \subseteq ϕ (B_{e}^{'})

(replacing each eavesdrop action by an internal communication). Due to the inclusions of the frames and

A_{e}^{'} \sim B_{e}^{'}

we also have that

A_{c}^{'} \sim B_{c}^{'}

Finally we show that the implication $\approx_{t}^{e} ⊊ \approx_{t}^{p} \cap \approx_{t}^{c}$ is strict, i.e., there exist A and B such that $A \approx_{ℓ}^{c} B$ (which implies $A \approx_{t}^{c} B$ ), $A \approx_{ℓ}^{p} B$ (which implies $A \approx_{t}^{p} B$ ) but $A ≉_{t}^{e} B$ .

Fig. 7.

Processes A and B such that $A \approx_{ℓ}^{c} B$ , $A \approx_{ℓ}^{p} B$ but $A ≉_{t}^{e} B$ .

Consider the processes A and B defined in Fig. 7. This example is a variant of the one given in Fig. 5. The difference is the addition of “ ${in}^{ho} (d, z) . if z = s_{1} then$ ” in processes $P_{1} (x)$ and $P_{2} (x)$ : this additional check is used to verify whether the adversary learned $s_{1}$ or not. The proofs that $A \approx_{ℓ}^{c} B$ and $A \approx_{ℓ}^{p} B$ follow the same lines as in Theorem 3. We just additionally observe that $ν s_{1} . ({in}^{ho} (d, z) . if z = s_{1} then {out}^{ho} (d, s_{2})) \approx_{ℓ}^{s} ν s_{1} . ({in}^{ho} (d, z) .0)$ for $s \in {c, p}$ .

The trace witnessing that $A ≉_{t}^{e} B$ is again similar to the one in Theorem 3, but starting with an eavesdrop transition which allows the attacker to learn $s_{1}$ , which in turn allows him to learn $s_{2}$ and distinguish $P_{1} (s_{2})$ from $P_{2} (s_{2})$ . These trace (in)equivalences have also been verified using DeepSec.

□

We note from the processes defined in Fig. 7 that the implications are strict even for processes that do not communicate on private channels, do not use replication, nor else branches and terms are simply names (no function symbols nor equational theories).

Theorem 5.

$\approx_{ℓ}^{e} ⊊ \approx_{ℓ}^{p} \cap \approx_{ℓ}^{c}$ .

Proof sketch.

The proof is structured in 3 steps, as in the proof of Theorem 4.

We first show that $\approx_{ℓ}^{e} \subseteq \approx_{ℓ}^{p}$ . Suppose $A \approx_{ℓ}^{e} B$ and let $R$ be the relation witnessing this equivalence. We will show that $R$ is also a labelled bisimulation in the private semantics. Suppose $A R B$ .

as $A \approx_{ℓ}^{e} B$ , we have that $ϕ (A) \sim ϕ (B)$ .

if $A {\overset{τ}{\to}}_{p} A^{'}$ then, as ${\overset{τ}{\to}}_{p} \subset {\overset{τ}{\to}}_{e}$ , $A {\overset{τ}{\to}}_{e} A^{'}$ . As $A \approx_{ℓ}^{e} B$ there exists $B^{'}$ such that $B \Rightarrow ϵ_{e} B^{'}$ and $A^{'} R B^{'}$ . As B is a honest process no $C OMM - E AV$ transition is possible, and hence $B \Rightarrow ϵ_{p} B^{'}$ .

if $A {\overset{ℓ}{\to}}_{p} A^{'}$ and $bn (ℓ) \cap fn (B) = \emptyset$ then we also have that $A {\overset{ℓ}{\to}}_{e} A^{'}$ (as ${\overset{ℓ}{\to}}_{p} \subset {\overset{ℓ}{\to}}_{e}$ and there exists $B^{'}$ such that $B \Rightarrow ℓ_{e} B^{'}$ and $A^{'} R B^{'}$ . As no $C OMM - E AV$ are possible and ℓ is not of the form $eav (c, d)$ nor $ν y . e a v (c, y)$ we have that $B \Rightarrow ℓ_{p} B^{'}$ .

We next show that $\approx_{ℓ}^{e} \subseteq \approx_{ℓ}^{c}$ . We will show that $\approx_{ℓ}^{e}$ is also a labelled bisimulation in the classical semantics. The proof relies on similar arguments as in Item 2 of the proof of Theorem 4 and the facts that

$ν \tilde{n} . (A^{'} ∣ {^{t} /_{x}}) \approx_{ℓ}^{e} ν \tilde{n} . (B^{'} ∣ {^{u} /_{x}})$ implies $ν \tilde{n} . A^{'} \approx_{ℓ}^{e} ν \tilde{n} . B^{'}$ ,

$A^{'} \approx_{ℓ}^{e} B^{'}$ implies $ν c . A^{'} \approx_{ℓ}^{e} ν c . B^{'}$

The first property is needed when an internal communication of a term or public channel is replaced by an eavesdrop action and an input. The second property handles the case when we replace the internal communication of a private channel by an application of the Eav-OCh rule and an input.

To show that the implication $\approx_{ℓ}^{e} ⊊ \approx_{ℓ}^{p} \cap \approx_{ℓ}^{c}$ is strict, we exhibit processes A and B such that $A \approx_{ℓ}^{c} B$ , $A \approx_{ℓ}^{p} B$ but $A ≉_{t}^{e} B$ (which implies $A ≉_{ℓ}^{e} B$ ). The processes defined in Fig. 7 witness this fact (cf the discussion of these processes in the proof of Theorem 4).

□

Again we note that the implications are strict, even for processes containing only public channels.

Theorem 6.

$\approx_{m}^{e} ⊊ \approx_{m}^{p} \cap \approx_{m}^{c}$ .

Proof sketch.

The proof is structured in 3 parts, as for Theorems 5 and 4.

We first prove that $\approx_{m}^{e} \subseteq \approx_{m}^{p}$ . Suppose that $A \approx_{m}^{e} B$ . Suppose that $A \approx_{m}^{e} B$ . We need to show that for all channel c, for all $C [_]$ attacker evaluation contexts $p$ -closing for A and B, $C [A] ⇓_{c}^{p}$ is equivalent to $C [B] ⇓_{c}^{p}$ . It follows from the definition of the private semantics that any process $eav (c, x) . P$ in $C [_]$ has the same behaviour as the process 0. Hence, we generate a context $C^{1} [_]$ by replacing in $C [_]$ any instance of $eav (c, x) . P$ by 0, and thus obtaining $C [A] ⇓_{c}^{p} \Leftrightarrow C^{'} [A] ⇓_{c}^{p}$ and $C [B] ⇓_{c}^{p} \Leftrightarrow C^{'} [B] ⇓_{c}^{p}$ . Notice that the definition of semantics gives us $\to_{p} \subseteq \to_{e}$ . Hence, $C^{'} [A] ⇓_{c}^{p}$ implies $C^{'} [A] ⇓_{c}^{e}$ and $C^{'} [B] ⇓_{c}^{p}$ implies $C^{'} [B] ⇓_{c}^{e}$ . Furthermore, since we built $C^{'} [_]$ to not contain any process of the form $eav (c, x) . P$ , we deduce that rules C-Eav and C-OEav can never be applied in a derivation of $C^{'} [A]$ or $C^{'} [B]$ . It implies that $C^{'} [A] ⇓_{c}^{p} \Leftrightarrow C^{'} [A] ⇓_{c}^{e}$ and $C^{'} [B] ⇓_{c}^{p} \Leftrightarrow C^{'} [B] ⇓_{c}^{e}$ . Thanks to $A \approx_{m}^{e} B$ , we know that $C^{'} [A] ⇓_{c}^{e} \Leftrightarrow C^{'} [B] ⇓_{c}^{e}$ and so we conclude that $C [A] ⇓_{c}^{p} \Leftrightarrow C [B] ⇓_{c}^{p}$ .

We next prove that $\approx_{m}^{e} \subseteq \approx_{m}^{c}$ . Similarly to Item 1, we consider a channel c and an attacker evaluation context $C [_]$ that is $c$ -closing for A and B. The main difficulty of this proof is to match the application of the rule Comm in the classical semantics with the rules C-Eav and C-OEac. However, $C [_]$ does not necessarily contain eavesdrop process $eav (d, x) ∣ ω c$ . Moreover, as mentioned in Item 1, a process $eav (d, x) . P$ has the same behavior as 0 in the classical semantics but can have a completely different behaviour in the eavesdropping semantics if P is not 0. Thus, we remove from $C [_]$ the eavesdrop processes, obtaining $C^{'} [_]$ . Then, we define a new context $C^{″} [_]$ based on $C^{'} [_]$ where will add harmless eavesdrop process $eav (d, y) .0$ . We first add in parallel the processes $! eav (a, y) ∣ ω a$ for all free channels a in $C^{'} [_], A$ and B. Moreover, since private channels can be opened, we also replace any process $ν d . P$ , ${in}^{at} (c, x) . P$ where $d, x$ are of channel type with $ν d . (P ∣! eav (d, y))$ and ${in}^{at} (c, x) . (P ∣! eav (x, y))$ . By induction of the derivations, we can show that $C [A] ⇓_{c}^{c} \Leftrightarrow C^{″} [A] ⇓_{c}^{e}$ and $C [B] ⇓_{c}^{c} \Leftrightarrow C^{″} [B] ⇓_{c}^{e}$ . Since $A \approx_{m}^{e} B$ , we deduce that $C^{″} [A] ⇓_{c}^{e} \Leftrightarrow C^{″} [B] ⇓_{c}^{e}$ and so $C [A] ⇓_{c}^{c} \Leftrightarrow C [B] ⇓_{c}^{c}$ .

Finally we show that the implication $\approx_{m}^{e} ⊊ \approx_{m}^{p} \cap \approx_{m}^{c}$ is strict, i.e., there exist processes A and B such that $A \approx_{m}^{c} B$ , $A \approx_{m}^{p} B$ but $A ≉_{m}^{e} B$ . The processes defined in Fig. 7 witness this fact. They already were witness of the strict inclusion $\approx_{t}^{e} ⊊ \approx_{t}^{p} \cap \approx_{t}^{c}$ (see proof of Theorem 4) and since A and B are image finite, we know from Theorem 1 that may and trace equivalences between A and B coincide.

□

4. Subclasses of processes for which (some of) the semantics coincide

As illustrated in previous sections, the presence of internal communications between public channels is the main issue when comparing the different semantics. Thus, the most natural class of processes on which the semantics coincide are processes where no internal communication on a public channel is possible.

Definition 7.
Let P be a closed honest process. P is internal communication free if and only for all $P \Rightarrow {tr}_{c} P^{'} {\overset{τ}{\to}}_{c} P^{″}$ , the τ action in $P^{'} {\overset{τ}{\to}}_{c} P^{″}$ is not the application of the rule Comm.

We denote by $ICF$ the set of internal communication free processes.
Lemma 1.
When restricted to $ICF$ , $\approx_{r}^{s_{1}} = \approx_{r}^{s_{2}}$ for $r \in {ℓ, o, m, t}$ and $s_{1}, s_{2} \in {c, p, e}$ .
Proof.
Immediate from the semantics. □

However, this class is very restrictive as it prevents any process of the form ${out}^{ho} (c, u) . P ∣ {in}^{ho} (c, x) . Q (x)$ . Therefore, we study in the rest of this section alternate classes of processes. The class of processes we study are mainly related to the notion of determinism: we first study the class of determinate processes, denoted $D$ , and then mainly restrict our attention to the case when the number of sessions is bounded. This is motivated by the fact that most tools able to verify these equivalences are restricted to a bounded number of sessions. We study three increasingly restrictive classes: (i) bounded determinate processes (denoted $BD$ ), (ii) action-determinate processes (denoted $AD$ ), and (iii) strong action determinate processes (denoted $SAD$ ). As the definition of determinism depends on the semantics, we may add the semantics as a parameter, e.g., we write $D (e)$ for the class of processes that are determinate in the eavesdrop semantics. Figure 8 provides an overview of the results of this section.

Finally, we also identify a new syntactic subclass of processes, called I/O-unambiguous and show relations among the equivalences for different semantics.

Fig. 8.
Summary of results for (bounded) determinate processes.
4.1. Determinate processes

4.1.1. Defining classes of determinate processes and their relations

In this section we define a subclass of determinate processes. These subclasses however depend on the semantics and therefore we also study the relations between these different subclasses. The notion of determinacy was defined in [15] for the classical semantics. It was shown that for determinate processes, observational and trace equivalence coincide. Intuitively, on determinate processes the attacker can determine, at each step of the execution, the position of the executed action in the process tree: this means that either the labels leading to the executed action differ, or, in case of two identical sequence of labels, the frames may be distinguished.

Definition 8 (Determinacy).

Let $s \in {c, p, e}$ . Let ≅ be an equivalence relation on closed honest extended processes. A closed honest extended process A is ≅-s-determinate if whenever $A \Rightarrow ℓ_{s} B$ , $A \Rightarrow ℓ_{s} B^{'}$ and $ϕ (B) \sim ϕ (B^{'})$ then $B ≅ B^{'}$ .

We denote by $D (s, ≅)$ the set of closed honest extended processes that are ≅-s-determinate.

It was shown in [15] that $D (c, \approx_{ℓ}^{c}) = D (c, \approx_{t}^{c})$ . We can show that this equality also holds in the private and eavesdrop semantics.

Lemma 2.
For all $s \in {c, p, e}$ , $D (s, \approx_{ℓ}^{s}) = D (s, \approx_{t}^{s})$ .
Proof.
The proof of [15, Lemma 2] literally holds for all semantics. □

Thanks to the previous lemma, we may simply consider the set of s-determinate processes, denoted $D (s)$ , as the set of closed honest extended processes that are $\approx_{ℓ}^{s}$ -s-determinate or $\approx_{t}^{s}$ -s-determinate coincide. It was also shown in [15] that when restricted to $c$ -determinate processes, we have that $\approx_{ℓ}^{c} = \approx_{t}^{c}$ . Once again, this result directly extends to $p$ -determinate and $e$ -determinate processes.
Lemma 3.
When restricted to $D (s)$ , $\approx_{ℓ}^{s} = \approx_{t}^{s}$ for $s \in {c, p, e}$ .
Proof.
The proof of [15, Theorem 2] literally holds for all semantics. □

The notion of determinacy depends on equivalences. Therefore one might expect the relations between determinate processes for different semantics to follow similar result as for the equivalences. However, we show that the sets of determinate processes coincide for eavesdrop and private semantics, while they are incomparable to the classic semantics Lemma 4.
$D (p) = D (e)$ , $D (c) ⊈ D (p)$ and $D (p) ⊈ D (c)$ .
Proof sketch.
We sketch the proof here. A more detailed version is available in Appendix F.

We start by showing that $D (p) ⊈ D (c)$ . Consider the process A displayed in Fig. 9a. $A \in D (c)$ since $A {\overset{τ}{\to}}_{c} {out}^{ho} (c, a)$ by the rule Comm and ${out}^{ho} (c, a) ≉_{ℓ}^{c} A$ . Moreover, $A \in D (p)$ since for all $tr$ , there is a unique $A^{'}$ such that $A \Rightarrow {tr}_{p} A^{'}$ . Hence $D (p) ⊈ D (c)$ .

We now show that $D (c) ⊈ D (p)$ . Consider the process B displayed in Fig. 9b. Intuitively, the use of the private channel s in B encodes a non determinist choice between the two processes P and Q. We can show that $P, Q \in D (c)$ which allows us to deduce that $B \in D (c)$ . However, $B \Rightarrow ε_{p} P$ , $B \Rightarrow ε_{p} Q$ and $P ≉_{t}^{p} Q$ imply $B \notin D (p)$ .

Let us show $D (e) \subseteq D (p)$ . Consider an honest closed process A such that $A \in D (e)$ . Let $A \Rightarrow {tr}_{p} A_{1}$ and $A \Rightarrow {tr}_{p} A_{2}$ . By definition of the semantics, $A \Rightarrow {tr}_{p} A_{i}$ implies $A \Rightarrow {tr}_{e} A_{i}$ , for $i = 1, 2$ . Since $A \in D (e)$ , we deduce $A_{1} \approx_{ℓ}^{e} A_{2}$ . By applying Theorem 5, we obtain $A_{1} \approx_{ℓ}^{p} A_{2}$ which concludes the proof of $D (e) \subseteq D (p)$ .

Finally, we need to show that $D (p) \subseteq D (e)$ . This part of the proof is detailed in Appendix F. □

4.1.2. Relations between semantics for determinate processes

We will now compare the equivalences when we restrict the processes to $D (s)$ for a given semantics s. We start with the subclass $D (p)$ (which coincides with $D (e)$ ).

Fig. 9.

Examples differentiating classical and private semantics for determinate processes.

Theorem 7.

When restricted to $D (p)$ , we have $\approx_{r_{1}}^{s_{1}} = \approx_{r_{2}}^{s_{2}} ⊊ \approx_{r_{3}}^{c}$ for $s_{1}, s_{2} \in {p, e}$ , $r_{1}, r_{2}, r_{3} \in {ℓ, t}$ .

The proof is given in Appendix F.

Next, we consider the subclass $D (c)$ . We show that even for this subclass of processes, the equivalences for the classical semantics are not included in the other ones.

Lemma 5.

When restricted to $D (c)$ , we have $\approx_{r}^{c} ⊈ \approx_{r}^{s}$ for $s \in {p, e}$ and $r \in {ℓ, t}$ .

Proof.

In the proof of Theorem 7 we showed that the processes P and Q displayed in Fig. 9 satisfy the following properties: $P, Q \in D (c)$ , $P \approx_{ℓ}^{c} Q$ and $P ≉_{t}^{p} Q$ . Note that we also have $P ≉_{t}^{e} Q$ . Hence P and Q allow us to prove that $\approx_{r}^{c} ⊈ \approx_{r}^{s}$ for $s \in {p, e}$ and $r \in {ℓ, t}$ . □

4.2. Determinacy for bounded processes

As many verification tools [13,14,16,18,29] consider a bounded number of sessions we study in this section, notions of determinacy when restricted to processes without replication. We also consider the notion of action-determinate which was introduced in [10] as a subclass of determinate processes that enable partial order reductions that significantly speed-up verification. Finally, we discuss the notion of strong action-determinate processes: this class was introduced in several tools, as this property can easily be checked syntactically. Interestingly, for this class of action-determinate processes, all notions of equivalences and semantics coincide.

4.2.1. Bounded determinate processes

We investigate in this section whether additional relations hold between the semantics when restricted to bounded processes, i.e., processes without replication. In particular we show that when restricted to such bounded processes, a $c$ -determinate P cannot have internal communication. However, we also show that even when restricted to bounded processes, $\approx_{ℓ}^{p}$ and $\approx_{ℓ}^{c}$ do not coincide.

We denote by $BD (s)$ the set of bounded processes in $D (s)$ for $s \in {p, c, e}$ .

Lemma 6.
$BD (c) ⊊ BD (p) = BD (e)$ and $BD (c) ⊊ ICF$ .
Proof.
Note that Lemma 4 directly gives us $BD (p) = BD (e)$ . Moreover, consider the process A displayed in Fig. 9a. We already showed in Lemma 4 that $A \in D (p)$ and $A \notin D (c)$ . Since A does not contain a replication, we deduce that $BD (p) ⊈ BD (c)$ .

Let us now show that $BD (c) \subseteq ICF$ . Let $A \in BD (c)$ . Assume by contradiction that $A \Rightarrow {tr}_{c} A_{1} {\overset{τ}{\to}}_{c} A_{2}$ where the transition $A_{1} {\overset{τ}{\to}}_{c} A_{2}$ is the application of the rule Comm. Hence $A_{1} \equiv ν \tilde{n} . ({out}^{ho} (c, u) . P ∣ {in}^{ho} (c, x) . Q ∣ R)$ and $A_{2} = ν \tilde{n} . (P ∣ Q {^{u} /_{x}} ∣ R)$ for some $c, u, P, Q$ . Since $A \in BD (c)$ , we deduce that $A_{1} \approx_{t}^{c} A_{2}$ . Consider the maximal trace ${tr}_{m}$ of $A_{1}$ (the trace ${tr}_{m}$ exists since A is bounded), i.e. $A_{1} \Rightarrow {tr}_{m}_{c} A_{1}^{'}$ . Since $A_{1} \approx_{t}^{c} A_{2}$ , the trace ${tr}_{m}$ is also maximal for $A_{2}$ with $A_{2} \Rightarrow {tr}_{m}_{c} A_{2}^{'}$ . But $A_{1} \Rightarrow {ν z . out (c, z) . in (c, z)}_{c} ν \tilde{n} . (P ∣ Q {^{u} /_{x}} ∣ R ∣ {^{u} /_{x}})$ . Since $A_{2} = ν \tilde{n} . (P ∣ Q {^{u} /_{x}} ∣ R)$ and $A_{2} \Rightarrow {tr}_{m}_{c} A_{2}^{'}$ , we deduce that $ν \tilde{n} . (P ∣ Q {^{u} /_{x}} ∣ R ∣ {^{u} /_{x}}) \Rightarrow {tr}_{m}_{c} A_{2}^{″}$ for some $A_{2}^{″}$ and so $ν z . out (c, z) . in (c, z) . {tr}_{m}$ is a trace of $A_{1}$ which contradicts the maximality of ${tr}_{m}$ . Hence $BD (c) \subseteq ICF$ .

To see that the inclusion $BD (c) ⊊ ICF$ is strict, observe that for the process $\begin{matrix} P \hat{=} {out}^{ho} (c, a) . {out}^{ho} (c, a_{1}) ∣ {out}^{ho} (c, a) . {out}^{ho} (c, a_{2}) \end{matrix}$ we have that $P \in ICF$ , but $P \notin BD (c)$ .

Finally, let us prove $BD (c) \subseteq BD (p)$ . Let $A \in BD (c)$ , $A \Rightarrow {tr}_{p} A_{1}$ and $A \Rightarrow {tr}_{p} A_{2}$ . Note that $A \Rightarrow {tr}_{p} A_{i}$ implies $A \Rightarrow {tr}_{c} A_{i}$ , for $i = 1, 2$ . As $A \in BD (c)$ , $A_{1} \approx_{ℓ}^{c} A_{2}$ . As $BD (c) \subseteq ICF$ , $A \in ICF$ and so $A_{1}, A_{2} \in ICF$ . By Lemma 1, we obtain $A_{1} \approx_{ℓ}^{p} A_{2}$ which allows us to conclude. □

In particular, as $BD (c) \subset ICF$ we directly have that all semantics coincide (Lemma 1), and by determinacy all equivalences coincide as well (Lemma 3).
Corollary 1.
When restricted to $BD (c)$ , we have that $\approx_{r_{1}}^{s_{1}} = \approx_{r_{2}}^{s_{2}}$ for $r_{1}, r_{2} \in {ℓ, o, m, t}$ and $s_{1}, s_{2} \in {c, p, e}$ .

Fig. 10.
$P \approx_{ℓ}^{c} Q$ but $P ≉_{t}^{p} Q$ .

We next investigate the relations when processes are restricted to the subclass $BD (p)$ (which coincides with $BD (e)$ ).
Theorem 8.
When restricted to $BD (p)$ , we have that $\approx_{r}^{p} = \approx_{r}^{e} ⊊ \approx_{r}^{c}$ for $r \in {ℓ, t}$ .

The proof is given in Appendix G.

Action-determinate. As mentioned above, the class of action determinate processes is of interest for verification tools since it supports partial order reduction techniques [10] which speed-up verification by several orders of magnitude. Such techniques have been implemented in several verification tools such as APTE, AKISS and DeepSec.
Definition 9.
Let P be a closed honest process. We say that P is action-determinate if $bn (P) \cap C h = \emptyset$ and for all $P \Rightarrow {tr}_{c} P^{'}$ , $P^{'} ≢ ν \tilde{k} . ({out}^{ho} (c, u_{1}) . Q_{1} ∣ {out}^{ho} (c, u_{2}) . Q_{2} | Q_{3})$ and $P^{'} ≢ ν \tilde{k} . ({in}^{ho} (c, x_{1}) . Q_{1} ∣ {in}^{ho} (c, x_{2}) . Q_{2} | Q_{3})$ for all $\tilde{k}, c, u_{1}, u_{2}, x_{1}, x_{2}, Q_{1}, Q_{2}, Q_{3}$ .

We define $AD$ to be the set of all action determinate processes.

Intuitively, a process is action determinate when there are never two similar available actions, i.e. two inputs or two outputs on the same channel. Note in particular that any (non-trivial) replicated process violates action-determinism.

We first show that the class of action determinate processes is strictly included in the class of determinate processes (for the private and, hence, eavesdropping semantics).
Lemma 7.
$AD ⊊ BD (p)$ .

The proof is give in Appendix H.

We can now show that the relations among equivalences that did hold for the subclass $BD (p)$ (Theorem 8) do also hold for the subclass $AD$ .
Theorem 9.
When restricted to $AD$ , we have that $\approx_{r}^{p} = \approx_{r}^{e} ⊊ \approx_{r}^{c}$ for $r \in {ℓ, t}$ .

Note that, while the equality and inclusion is a direct corollary of Theorem 8 and Lemma 7, the fact that the inclusion is strict needs to be shown. The proof is given in Appendix I.

Strong action determinate. In the context of automated verification, deciding whether a process is action-determinate is still rather costly as it basically requires to verify a reachability property. We therefore introduce a stronger and more syntactical notion of action determinate, which is actually implemented in the verification tools AKISS and DeepSec. Intuitively, while action determinate processes never reach a situation where two “similar” actions are available, strong action-determinate processes verify that such similar actions never appear in parallel, syntactically.

We first define the set of action skeletons $S = {out (c), in (c) ∣ c \in C h}$ .
Definition 10 (strong action determinate).

The set $S a (S)$ built on $S \subseteq S$ is the smallest set of honest processes such that ${^{u} /_{x}}, 0 \in S a (\emptyset)$ for all $u, x$ and such that if $P \in S a (S)$ and $Q \in S a (S^{'})$ then

${out}^{ho} (c, u) . P \in S a ({out (c)} \cup S)$ when $c \in C h$

${in}^{ho} (c, x) . P \in S a ({in (c)} \cup S)$ when $c \in C h$

$ν k; P \in S a (S)$ when ${in (k), out (k)} \cap S = \emptyset$

$if u = v then P else Q \in S a (S \cup S^{'})$

$S a (P ∣ Q) \in S a (S \cup S^{'})$ when $S \cap S^{'} = \emptyset$

We define the set of strong action determinate process as

SAD = ⋃_{S \subseteq S} S a (S)

As the name indicates, it is easy to see that any strong action determinate process is also an action determinate process.

Lemma 8.
$SAD ⊊ AD$ .
Proof.
The implication follows directly from the definition, as any strongly action determinate process forbids two identic skeletons in parallel. To see that the implication is strict we observe that, for $\begin{matrix} P \hat{=} ν k . ({out}^{ho} (c, k) ∣ {in}^{ho} (c, x) . if x = k then {out}^{ho} (c, a)) \end{matrix}$ we have that $P \in AD$ , but $P \notin SAD$ . □

While for action determinate processes we have that $\approx_{ℓ}^{p} ⊊ \approx_{ℓ}^{c}$ , we can show that for strong action determinate processes we actually have $\approx_{ℓ}^{c} \subseteq \approx_{ℓ}^{p}$ .
Theorem 10.
When restricted to $SAD$ , we have $\approx_{ℓ}^{c} \subseteq \approx_{ℓ}^{p}$ .

Proof of Theorem 10 can be found in Appendix J.

This implies the following corollary stating that for strong action determinate processes, all semantics and equivalences coincide. This is particularly interesting as the AKISS and DeepSec tools check this condition. Moreover, it means that partial-order reduction optimizations, developed and shown correct for the private semantics [10], are correctly applied by these tools, regardless of the chosen semantics.
Corollary 2.
When restricted to $SAD$ , we have that $\approx_{r_{1}}^{s_{1}} = \approx_{r_{2}}^{s_{2}}$ for $r_{1}, r_{2} \in {ℓ, o, m, t}$ and $s_{1}, s_{2} \in {c, p, e}$ .
4.3. I/O-unambiguous processes

Restricting processes to action-determinate processes may sometimes be too restrictive. For instance, when verifying unlinkability and anonymity properties, two outputs by different parties should not be distinguishable due to the channel name. We therefore introduce another class of processes, that we call I/O-unambiguous for which we also show that the different semantics (although not the different equivalences) do coincide.

Intuitively, an io-unambiguous process forbids an output and input on the same public channel to follow each other directly (or possibly with only conditionals in between). For instance, we forbid processes of the form ${out}^{θ} (c, t) . {in}^{θ} (c, x) . P$ , ${out}^{θ} (c, t) . ({in}^{θ} (c, x) . P ∣ Q)$ as well as ${out}^{θ} (c, t) . if t_{1} = t_{2} then P else {in}^{θ} (c, x) . Q$ . We however allow inputs and outputs on the same channel in parallel.

Definition 11.
We define an honest extended process A to be I/O-unambiguous when $ioua (A,_) = ⊤$ where $\begin{matrix} \begin{matrix} ioua (0, c) = ⊤ ioua ({^{u} /_{x}}, c) = ⊤ ioua (! P, c) = ioua (P, c) \\ ioua (A ∣ B, c) = ioua (A, c) \land ioua (B, c) ioua (ν x . A, c) = ioua (A, c) \end{matrix} \\ ioua (ν n . A, c) & = & \{\begin{matrix} ⊥ & if n \in C h \\ ioua (A, c) & otherwise \end{matrix} \\ ioua (if u = v then P else Q, c) & = & ioua (P, c) \land ioua (Q, c) \\ ioua ({out}^{θ} (d, u) . P, c) & = & \{\begin{matrix} ⊥ & if u is of channel type \\ ioua (P, d) & otherwise \end{matrix} \\ ioua ({in}^{θ} (d, x) . P, c) & = & \{\begin{matrix} ⊥ & if x is of channel type or d = c \\ ioua (P,_) & otherwise \end{matrix} \end{matrix}$

Note that an I/O-unambiguous process does not contain private channels and always input/output base-type terms. We also note that a simple way to enforce that processes are I/O-unambiguous is to use disjoint channel names for inputs and outputs (at least in the same parallel thread). Theorem 11.
When restricted to I/O-unambiguous processes, we have that $\approx_{r}^{p} = \approx_{r}^{e}$ but $\approx_{r}^{e} ⊊ \approx_{r}^{c}$ for $r \in {ℓ, t}$ .
Proof.
From Theorems 5 and 4, we already know that $\approx_{r}^{e} \subseteq \approx_{r}^{p}$ and $\approx_{r}^{e} \subseteq \approx_{r}^{c}$ . Hence, we only need to show that $\approx_{r}^{p} \subseteq \approx_{r}^{e}$ and $\approx_{r}^{p} ⊊ \approx_{r}^{c}$ . The latter is easily shown by noticing that the processes A and B in Fig. 6 are I/O-unambiguous. Thus, we focus on $\approx_{r}^{p} \subseteq \approx_{r}^{e}$ .

We start by proving that for all I/O-unambiguous processes A, for all $A \Rightarrow tr A^{'}$ , we have that $A^{'}$ is I/O-unambiguous. Note that structural equivalence preserves I/O-unambiguity, i.e. for all extended processes $A, B$ , for all channel name c, $A \equiv B$ implies $ioua (A, c) = ioua (B, c)$ . Hence, we assume w.l.o.g. that a name is bound at most once and the set of bound and free names are disjoint.

Second, we show that for all I/O-unambiguous processes A, for all $A \Rightarrow {ν z . out (c, z) . in (c, z)}_{p} A^{'}$ , we have that $\Rightarrow {ν z . eav (c, z)}_{e} A^{'}$ . To prove this property, denoted $P$ , let us assume w.l.o.g. that $A {\overset{ν z . out (c, z)}{\to}}_{p} A_{1} \to_{p}^{} A_{2} {\overset{in (c, z)}{\to}}_{p} A^{'}$ . The transition $A {\overset{ν z . out (c, z)}{\to}}_{p} A_{1}$ indicates that $A \equiv ν \tilde{n} . ({out}^{ho} (c, u) . P ∣ Q)$ and $A_{1} \equiv \tilde{n} . (P ∣ Q ∣ {^{u} /_{z}})$ for some $P, Q, \tilde{n}, c, u$ . Note that A is I/O-unambiguous, and hence $ioua (P, c) = ⊤$ .

As A is I/O-unambiguous implies that A does not contain private channels, we have that the rule applied in $A_{1} \to_{p}^{} A_{2}$ is either the rule Then or Else. Therefore, there exists $P^{'}$ and $Q^{'}$ such that $P \to_{p}^{} P^{'}$ , $Q \to_{p}^{} Q^{'}$ , $A_{n} \equiv ν \tilde{n} . (P^{'} ∣ Q^{'} ∣ {^{u} /_{x}})$ and $ioua (P^{'}, c) = ⊤$ . Hence, we deduce that there exists $Q_{1}, Q_{2}$ such that $Q^{'} \equiv ν \tilde{m} . ({in}^{.} (c, x) Q_{1} ∣ Q_{2})$ and $A^{'} \equiv ν \tilde{n} . ν \tilde{m} . (P^{'} ∣ Q_{1} {^{u} /_{x}} ∣ Q_{2})$ . We conclude the proof of this property by noticing that we can first apply on A the reduction rules of $Q \to_{p}^{} Q^{'}$ , then apply the rule C-Eav and finally apply the rules of $P \to_{p}^{} P^{'}$ .
To prove $\approx_{t}^{p} \subseteq \approx_{t}^{e}$ , we assume that A, B are two closed honest extended processes such that $A \approx_{t}^{p} B$ . For all $A \Rightarrow {tr}_{e} A^{'}$ , it follows from the semantics that $A \Rightarrow {tr}_{p}_{p} A^{'}$ where ${tr}_{p}$ is obtained by replacing in $tr$ each $ν z . eav (c, z)$ by $ν z . out (c, z) . in (c, z)$ . Since $A \approx_{t}^{p} B$ , there exists $B^{'}$ such that $B \Rightarrow {tr}_{p}_{p} B^{'}$ and $ϕ (A^{'}) \sim ϕ (B^{'})$ . Thanks to the property $P$ , we conclude that $B \Rightarrow {tr}_{e} B^{'}$ .

To prove $\approx_{ℓ}^{p} \subseteq \approx_{ℓ}^{e}$ , we assume that A, B are two closed honest extended processes such that $A \approx_{ℓ}^{p} B$ and let $R$ be the relation witnessing this equivalence. We will show that $R$ is also a labelled bisimulation in the eavesdropping semantics. Suppose $A R B$ .

as $A \approx_{ℓ}^{p} B$ , we have that $ϕ (A) \sim ϕ (B)$ .

if $A {\overset{τ}{\to}}_{e} A^{'}$ then, as A is honest, $A {\overset{τ}{\to}}_{p} A^{'}$ . As $A \approx_{ℓ}^{p} B$ there exists $B^{'}$ such that $B \Rightarrow ϵ_{p} B^{'}$ and $A^{'} R B^{'}$ . As ${\overset{τ}{\to}}_{p} \subset {\overset{τ}{\to}}_{e}$ , $B \Rightarrow ϵ_{e} B^{'}$

if $A {\overset{ℓ}{\to}}_{e} A^{'}$ then, as A is I/O-unambiguous, $A \Rightarrow {tr}_{e} A^{'}$ where $tr = ν z . out (c, z) . in (c, z)$ when $ℓ = ν z . eav (c, z)$ else $tr = ℓ$ . As $A \approx_{ℓ}^{p} B$ , there exists $B^{'}$ such that $B \Rightarrow {tr}_{p} B^{'}$ and $A^{'} R B^{'}$ . When $tr = ℓ$ , the definition of the semantics directly gives us $B \Rightarrow ℓ_{e} B^{'}$ . When $tr = ν z . out (c, z) . in (c, z)$ , the property $P$ gives us $B \Rightarrow ℓ_{e} B^{'}$ .
□

5. Different semantics in practice

As we have seen, in general, the three proposed semantics may yield different results. A conservative approach would consist in verifying always the eavesdropping semantics which is stronger than the two other ones, as shown before. However, this semantics seems also to be the least efficient one to verify. Moreover, partial-order reduction techniques that provide tremendous speed-ups were only developed for the private semantics.

We have implemented the three different semantics in the DeepSec tool. This allowed us to investigate the difference in results and performance between the semantics. In our experiments we considered several examples from DeepSec’s example repository. We rely on the existing modelling and do not describe these protocols, as these details are not important for the observations we wish to make. All benchmarks, summarized in Table 1, were carried out on a machine with 20 Intel Xeon 3.10 GHz cores and 50 Gb of memory. The implementation and the specification files are available at [17].

Table 1
Experimental results

Property/Protocol #roles Single channel I/O unambiguous $SAD$

$\approx_{t}^{p}$ $\approx_{t}^{e}$ $\approx_{t}^{c}$ $\approx_{t}^{p} = \approx_{t}^{e}$ $\approx_{t}^{c}$ $\approx_{t}^{p} = \approx_{t}^{e} = \approx_{t}^{c}$

Strong secrecy

Denning–Sacco 6 33 s 2 m 7 s 1 m 58 s 9 s 35 s <1 s

NSL 4 29 s 1 m 43 s 3 s 6 s <1 s

Wide Mouth Frog 9 12 m 16 s 34 m 43 s 20 m 1 s 24 s 58 s <1 s

Yahalom–Lowe 6 2 h 46 m 11 h 11 m 5 h 17 m 4 m 5 s 13 m 47 s <1 s

Anonymity

Passive Authentication 6 1 h 59 m 5 h 6 m 6 h 49 m 7 m 2 s 1 h 50 m <1 s

Private Authentication 4 9 s 9 s 11 s 1 s 2 s <1 s

Unlinkability

Passive Authentication 6 3 h 15 m 7 h 15 m 11 h 6 m 10 m 30 s 2 h 49 m <1 s

AKA 4 13 m 26 m 9 s 17 m 13 s 18 s 49 s <1 s

Vote privacy

Helios 10 10 m 9 s 19 m 10 s 14 m 50 s – – –

Scytl 3 2 m 47 s 5 m 9 s 5 m 14 s – – –

Property/Protocol	#roles	Single channel	I/O unambiguous	$SAD$
Strong secrecy
Denning–Sacco	6	33 s	2 m 7 s	1 m 58 s	9 s	35 s	<1 s
NSL	4	29 s	1 m	43 s	3 s	6 s	<1 s
Wide Mouth Frog	9	12 m 16 s	34 m 43 s	20 m 1 s	24 s	58 s	<1 s
Yahalom–Lowe	6	2 h 46 m	11 h 11 m	5 h 17 m	4 m 5 s	13 m 47 s	<1 s
Anonymity
Passive Authentication	6	1 h 59 m	5 h 6 m	6 h 49 m	7 m 2 s	1 h 50 m	<1 s
Private Authentication	4	9 s	9 s	11 s	1 s	2 s	<1 s
Unlinkability
Passive Authentication	6	3 h 15 m	7 h 15 m	11 h 6 m	10 m 30 s	2 h 49 m	<1 s
AKA	4	13 m	26 m 9 s	17 m 13 s	18 s	49 s	<1 s
Vote privacy
Helios	10	10 m 9 s	19 m 10 s	14 m 50 s	–	–	–
Scytl	3	2 m 47 s	5 m 9 s	5 m 14 s	–	–	–

The specifications we used for these experiments include verification of

strong secrecy in several classical authentication protocols (Denning–Sacco, Needham–Schroeder–Lowe (NSL), Wide Mouth Frog, and Yahalom–Lowe protocols);

anonymity of the Private Authentication protocol proposed by Abadi and Fournet [2];

anonymity and unlinkability of the passive authentication protocol implemented in the European Passport protocol [5,23];

unlinkability of the AKA protocol, deployed in 3G mobile telephony [7];

vote privacy in the Helios e-voting protocol [4], and the e-voting protocol proposed by Scytl for elections in the Swiss Neuchâtel canton [19].

For all these examples we found that the results were unchanged, independent of the semantics. However, as expected, performance was generally better for the private semantics, and much better for strong action determinate processes, as this class allows for powerful partial-order reductions. The existing protocol encodings generally used a single public channel. To enforce membership in a particular subclass we had to use different channel names. Surprisingly, the use of distinct channels to enforce I/O-unambiguity, significantly enhances the tool’s performance. We could not make the voting protocols I/O unambiguous and action determinate, because the encodings use private channels. In the absence of private channels using different channel names to enhance efficiency is tempting. One must however be careful as changing channel names changes the attacker’s observation and may change the result. Typically, a single channel name models that the attacker does a priori not know which process sent a given message. Binding the channel name to the identity allows the attacker to know which host sent a message, but not necessarily which of the possibly multiple processes, e.g. sessions, on the given host. However, this modelling is typically not adequate when checking anonymity, or unlinkability, as it reveals the sender’s identity. For such properties, it may be possible to use different channel names for each session, modelling that the adversary can distinguish different sessions, but not necessarily whether the same host executed one or several sessions. This is the encoding we used for verifying anonymity and unlinkability properties to enforce strong action determinism in the AKA and Passive Authentication protocols.

6. Conclusion

In this paper we investigated two families of Dolev–Yao models, depending on how the hypothesis that the attacker controls the network is reflected. While the two semantics coincide for reachability properties, they yield incomparable notions of behavioral equivalences, which have recently been extensively used to model privacy properties. The fact that forcing all communication to be routed through the attacker may diminish his distinguishing power may at first seem counter-intuitive. We also propose a third semantics, where internal communication among honest participants is permitted but leaks the message to the attacker. This new communication semantics entails strictly stronger equivalences than the two classical ones. We also identify several subclasses of protocols for which (some) semantics coincide. Finally, we implemented the three semantics in the DeepSec tool. Our experiments showed that the three semantics provide the same result on the case studies in the DeepSec example repository. However, the private semantics is slightly more efficient, as less interleavings have to be considered. Our results illustrate that behavioral equivalences are much more subtle than reachability properties and the need to carefully choose the precise attacker model.

Footnotes

Acknowledgments

We would like to thank Catherine Meadows and Stéphanie Delaune for interesting discussions, as well as the anonymous reviewers for their comments. This work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No 645865-SPOOC) and the ANR projects SEQUOIA ANR-14-CE28-0030-01 and TECAP ANR-17-CE39-0004-01.

Part of the work was carried out while the first author was a student at IIT Bombay during an internship at Inria Nancy Grand-Est.

Refining Theorem 3

We here give a more refined version of Theorem 3. In particular we show that the private and classical semantics are incomparable for trace equivalence and labelled bisimulation, even when restricted to processes that do not use else branches.

Proof of Proposition 2

Proof of Theorem 1

We start by restating the a proposition from [15] that was used to prove that trace equivalence implies may equivalence in the classical semantics. In order to prove the proposition for the semantics private and eavesdrop, we will first write exactly the proof of from [15] for the classical semantics and then highlight what changes are required to obtain the proofs for the private and eavesdropping semantics.

The previous lemma indicates that the trace equivalence are preserved by replacement of free names.

As for the previous proposition, the proof of Theorem 1 is taken from [15] for the classical semantics and we adapt it for the private and eavesdropping semantics. Theorem 1.

$\approx_{t}^{s} ⊊ \approx_{m}^{s}$ and $\approx_{t}^{s} = \approx_{m}^{s}$ on image-finite processes for $s \in {c, e, p}$ .

Proof.

We first prove that for all $s \in {c, p, e}$ , $\approx_{t}^{s} \subseteq \approx_{m}^{s}$ . Since we already proved in the body of the paper that there exists two closed honest extended processes such that $A \approx_{m}^{s} B$ but $A \approx_{t}^{s} B$ , we would thus obtain that $\approx_{t}^{s} ⊊ \approx_{m}^{s}$ .

Let $A, B$ be two closed extended processes such that $A \approx_{t}^{s} B$ . Let $C [_]$ be an evaluation context s-closing for A and B, and c be a channel name. We assume w.l.o.g. that $C [_] = ν \tilde{n} . (D_{1} ∣ ν \tilde{m} . (_∣ D_{2}))$ for some extended processes $D, D^{'}$ and for some sequences of names and variables $\tilde{n}$ , and $\tilde{m}$ . We assume w.l.o.g. that $\tilde{m} \cap (bn (A) \cup bv (A)) = \emptyset$ and $\tilde{m} \cap (bn (B) \cup bv (B)) = \emptyset$ .

Let $A_{2} = A {^{{\tilde{m}}^{'}} /_{\tilde{m}}}$ and $B_{2} = B {^{{\tilde{m}}^{'}} /_{\tilde{m}}}$ where $\tilde{m^{'}}$ is a sequence of fresh names and variables. Thanks to Lemma 10, we have that $A_{2} \approx_{t}^{s} B_{2}$ . Hence, by structural equivalence, there exists $C_{2} [_] = ν \tilde{k} . (D ∣_)$ such that $C [A] \equiv C_{2} [A_{2}]$ and $C [B] \equiv C_{2} [B_{2}]$ .

Assume now that $C [A] ⇓_{c}^{s}$ . This means that there exist a evaluation context $C_{1}$ that does not bind c, a term M, and a plain process P, $θ \in {at, ho}$ such that $C [A] \equiv C_{2} [A_{2}] \to_{s}^{*} C_{1} [{out}^{θ} (c, M) . P]$ . Applying Proposition 3 on $A_{2}$ , $B_{2}$ and $C_{2} [_]$ , we know that there exist a closed extended process $A_{2}^{'}$ , an evaluation context $C_{2}^{'} [_] = ν \tilde{r} . (E ∣_)$ s-closing for $A_{2}^{'}$ and $tr \in {(A \ {τ})}^{*}$ such that $C_{1} [{out}^{θ} (c, M) . P] \equiv C_{2} [A_{2}^{'}]$ , and $A_{2} \Rightarrow {tr}_{s} A_{2}^{'}$ , and for all closed extended process $B_{2}^{'}$ such that $B_{2} \Rightarrow {tr}_{s} B_{2}^{'}$ and $ϕ (B_{2}^{'}) \sim ϕ (A_{2}^{'})$ , we have that $C_{2} [B_{2}] \to_{s}^{*} C_{2}^{'} [B_{2}^{'}]$ . Moreover, we assume w.l.o.g. that $bn (() tr) \cap fn (() B_{2}) = \emptyset$ .

Since $C_{2}^{'} = ν \tilde{r} . (E |_)$ , we can deduce from $C_{1} [{out}^{θ} (c, M) . P] \equiv C_{2}^{'} [A_{2}^{'}]$ that the output ${out}^{θ} (c, M)$ comes from the process E when $θ = at$ or from $A_{2}^{'}$ when $θ = ho$ . We distinguish these two cases:

Case $θ = at$ : Since, we have that $A_{2} \approx_{t}^{s} B_{2}$ , we know that there exists $B_{2}^{'}$ such that $B_{2} \Rightarrow {tr}_{s} B_{2}^{'}$ and $ϕ (A_{2}^{'}) \sim ϕ (B_{2}^{'})$ . Therefore, we have that $C_{2} [B_{2}] \to_{s}^{*} C_{2}^{'} [B_{2}^{'}] \equiv ν \tilde{r} . (E ∣ B_{2}^{'})$ . But by hypothesis, we know that the output ${out}^{θ} (c, M)$ comes from E and $c \notin \tilde{r}$ . Hence we have that $C_{2} [B_{2}] ⇓_{c}^{s}$ , and since $C [B] \equiv C_{2} [B_{2}]$ , we conclude that $C [B] ⇓_{c}^{s}$ .

Case $θ = ho$ : Thus, we have that $A_{2}^{'} \equiv ν \tilde{v} . ({out}^{θ} (c, M) . P ∣ A_{3})$ with $c \notin \tilde{v}, \tilde{r}$ . Thus, we have that $A_{2}^{'} {\overset{ν z . out (c, z)}{\to}}_{s} ν \tilde{v} . (P ∣ A_{3} ∣ {^{M} /_{z}})$ where z is fresh (if M is a term of channel type, the transition is different but the proof can be done in a similar way.) Let $A^{″} = ν \tilde{v} . (P ∣ A_{3} ∣ {^{M} /_{z}})$ and ${tr}^{'} = tr \cdot ν z . out (c, z)$ , we have that $A_{2} \Rightarrow {tr}^{'}_{s} A^{″}$ . Since we have that $A_{2} \approx_{t}^{s} B_{2}$ , we have that there exists $B_{2}^{'}$ such that $B_{2} \Rightarrow {tr}^{'}_{s} B_{2}^{'}$ and $ϕ (A^{″}) \sim ϕ (B_{2}^{'})$ . Since internal reduction rules do not modify the frame (modulo structural equivalence), we can deduce w.l.o.g. that there exists $B^{'}$ such that $B_{2} \Rightarrow {tr}_{s} B^{'} {\overset{ν z . out (c, z)}{\to}}_{s} B_{2}^{'}$ . Therefore, we have that there exists a term N, an evaluation context $C_{3}$ and a process Q such that $B^{'} \equiv C_{3} [{out}^{ho} (c, N) . Q]$ and c is not bind by $C_{3}$ . Furthermore, we have that $ϕ (A_{2}^{'}) \sim ϕ (B^{'})$ which means that $C_{2} [B_{2}] \to_{s}^{*} C_{2}^{'} [B^{'}]$ , and thus $C_{2} [B_{2}] \to_{s}^{*} C_{2}^{'} [C_{3} [{out}^{ho} (c, N) . Q]]$ . Hence, we have that $C_{2} [B_{2}] ⇓_{c}^{s}$ , and since $C [B] \equiv C_{2} [B_{2}]$ , we conclude that $C [B] ⇓_{c}^{s}$ .

This conclude the proof of $\approx_{t}^{s} \subseteq \approx_{m}^{s}$ . It remains to prove that on imagine-finite processes, $\approx_{t}^{s} = \approx_{m}^{s}$ for all $s \in {c, e, p}$ . We first focus on $s = c$ .

Assume that $A ≉_{t}^{c} B$ . We assume w.l.o.g. that $A ⋢_{t}^{s} B$ . In such a case, there exists a witness for the non equivalence. This means that there exists $A^{'}, tr$ such that $bn (() tr) \cap fn (() B) = \emptyset$ , and for all $B^{'}$ , $B \Rightarrow {tr}_{c} B^{'}$ implies $ϕ (A^{'}) ≁ ϕ (B^{'})$ . Moreover, we assume that no name in $tr$ is bound twice (i.e. $ν a$ . cannot occur twice in $tr$ ) and bound names in $tr$ are distinct from free names that occur in A, B, and $tr$ .

We build an evaluation context $C_{c} [_]$ according to the trace $tr$ and also the tests that witness the fact that static equivalence does not hold. Let $S_{tr} = {ϕ (B^{'}) | B \Rightarrow {tr}_{c} B^{'}}$ . Since B is image-finite, we know that $S_{tr} / \sim$ is finite. Let ${ϕ_{1}, \dots, ϕ_{m}} = S / \sim$ . Note that m can be equal to 0 if there is no $B^{'}$ such that $B \Rightarrow {tr}_{c} B^{'}$ .

We know that ${1, \dots, m} = T^{+} ⊎ T^{-}$ with:

for each $i \in T^{+}$ , there exist two terms $M_{i}$ and $N_{i}$ such that $v (M_{i}) \cup v (N_{i}) \subseteq dom (ϕ (A^{'}))$ , $(M_{i} =_{E} N_{i}) ϕ (A^{'})$ , and $(M_{i} \neq_{E} N_{i}) ϕ_{i}$ ; and

for each $i \in T^{-}$ , there exist two terms $M_{i}$ and $N_{i}$ such that $v (M_{i}) \cup v (N_{i}) \subseteq dom (ϕ (A^{'}))$ , $(M_{i} \neq_{E} N_{i}) ϕ (A^{'})$ , and $(M_{i} =_{E} N_{i}) ϕ_{i}$ .

Let $bad$ be a fresh channel name that does not occur in A and B. Let $P_{1}, \dots, P_{m}, P_{m + 1}$ be the plain processes defined as follows:

$P_{m + 1} \hat{=} {out}^{at} (bad, bad) .0$

for $1 ⩽ i ⩽ m$ , we define $P_{i}$ as follows: $\begin{matrix} P_{i} \hat{=} if M_{i} = N_{i} then P_{i + 1} else 0 & when i \in T^{+} \\ P_{i} \hat{=} if M_{i} = N_{i} then 0 else P_{i + 1} & when i \in T^{-} \end{matrix}$

Let ${a_{1}, \dots, a_{k}}$ be channel names that occur free in A, B, and $tr$ . Let $X_{ch}^{0} = {x_{a_{1}}, \dots, x_{a_{k}}}$ be a set of variables of channel type, and $σ = {x_{a_{1}} \mapsto a_{1}, \dots, x_{a_{k}} \mapsto a_{k}}$ . Moreover, for all channel names ${d_{1}, \dots, d_{m}}$ that are bound in $tr$ , we also associate fresh variables $x_{d_{1}}, \dots, x_{d_{m}}$ .

We define $C_{c} [_]$ such that $C_{c} [_] = ν \tilde{z} . (Q_{c} (tr, X_{ch}^{0}) ∣_)$ where $\tilde{z} = dom (ϕ (A))$ and $Q_{c} (tr, X_{ch})$ is defined by recurrence on $tr$ as follows:

if $tr = ϵ$ then $Q_{c} (tr, X_{ch}) = P_{1}$ ;

if $tr = in (a, M) . {tr}^{'}$ then $Q_{c} (tr, X_{ch}) = {out}^{at} (x_{a} σ, M) . Q_{c} ({tr}^{'}, X_{ch})$ ;

if $tr = ν z . out (a, z) . {tr}^{'}$ and z is of base type then $Q_{c} (tr, X_{ch}) = {in}^{at} (x_{a} σ, x) . Q_{c} ({tr}^{'}, X_{ch})$

it $tr = out (a, c) . {tr}^{'}$ then $Q_{c} (tr, X_{ch}) = {in}^{at} (x_{a} σ, y) . if y = x_{c} σ then Q_{c} ({tr}^{'}, X_{ch}) else 0$ where y is fresh variable of channel type; and

if $tr = ν c . out (a, c)$ and c is of channel type then $Q_{c} (tr, X_{ch}) = {in}^{at} (x_{a} σ, x_{c}) . if x_{c} \in X_{ch} σ then 0 else Q_{c} ({tr}^{'}, X_{ch}^{'})$ where $X_{ch}^{'} = X_{ch} ⊎ {x_{c}}$ .

We use the conditional

if u \in {u_{1}, \dots, u_{k}} then 0 else P

as a shortcut for

\begin{matrix} if u = u_{1} then 0 else (if u = u_{2} then 0 else (\dots (if u = u_{k} then 0 else P) \dots)) . \end{matrix}

We can see that $C_{c} [A] ⇓_{bad}^{c}$ since $A \Rightarrow tr A^{'}$ and $ϕ (A^{'})$ satisfies by definition all the tests that are tested in $P_{1}, \dots, P_{m}$ . However, by construction of $C_{c} [_]$ , we have that $C_{c} [B] {⇓̸}_{bad}^{c}$ .

This conclude the proof for the case $s = c$ . The proof for $s = p$ and $e$ are very similar. We only need to slightly modify the context $C_{c} [_]$ . In fact since the possible labels in the private semantics are the same as in the original semantics, we have $C_{p} [_] = C_{c} [_]$ . However, for the eavesdropping semantics, we define $C_{e} [_]$ such that $C_{e} [_] = ν \tilde{z} . (Q_{e} (tr, X_{ch}^{0}) ∣_)$ where $\tilde{z} = dom (ϕ (A))$ and $Q_{e} (tr, X_{ch})$ is defined by recurrence on $tr$ as follows:

if $tr = ϵ$ then $Q_{e} (tr, X_{ch}) = P_{1}$ ;

if $tr = in (a, M) . {tr}^{'}$ then $Q_{e} (tr, X_{ch}) = {out}^{at} (x_{a} σ, M) . Q_{e} ({tr}^{'}, X_{ch})$ ;

if $tr = ν z . out (a, z) . {tr}^{'}$ and z is of base type then $Q_{e} (tr, X_{ch}) = {in}^{at} (x_{a} σ, z) . Q_{e} ({tr}^{'}, X_{ch})$

it $tr = out (a, c) . {tr}^{'}$ then $Q_{e} (tr, X_{ch}) = {in}^{at} (x_{a} σ, y) . if y = x_{c} σ then Q_{e} ({tr}^{'}, X_{ch}) else 0$ where y is fresh variable of channel type; and

if $tr = ν c . out (a, c)$ and c is of channel type then $Q_{e} (tr, X_{ch}) = {in}^{at} (x_{a} σ, x_{c}) . if x_{c} \in X_{ch} σ then 0 else Q_{e} ({tr}^{'}, X_{ch}^{'})$ where $X_{ch}^{'} = X_{ch} ⊎ {x_{c}}$ .

if $tr = eav (a, c) . {tr}^{'}$ with c of channel-type then $Q_{e} (tr, X_{ch}) = eav (x_{a} σ, y) . if y = x_{c} σ then Q_{e} ({tr}^{'}, X_{ch}) else 0$ where y is fresh variable of channel type;

if $tr = ν z . eav (a, z) . {tr}^{'}$ and z is of base type then $Q_{e} (tr, X_{ch}) = eav (x_{a} σ, z) . Q_{e} ({tr}^{'}, X_{ch})$

if $tr = ν c . eav (a, c) . {tr}^{'}$ and c is of channel type then $Q_{e} (tr, X_{ch}) = eav (x_{a} σ, x_{c}) . if x_{c} \in X_{ch} σ then 0 else Q_{e} ({tr}^{'}, X_{ch}^{'})$ where $X_{ch}^{'} = X_{ch} ⊎ {x_{c}}$ .

□

Proof of Theorem 6

In this section, we want to prove that $\approx_{m}^{e} ⊊ \approx_{m}^{p} \cap \approx_{m}^{c}$ . In order to show that $\approx_{m}^{e} ⊊ \approx_{m}^{c}$ , we need to build a transformation of context that would allows us to go from the classic semantics to eavesdropping semantics, and vice versa.

Notice that in the definition of structural equivalence $! A ∣! A$ is not equivalence to $! A$ even though they have the same behavior. In fact, for reachability, may equivalence, trace equivalence, observational equivalence and labeled bissimilar, using the structural equivalence coincides with using the structural equivalence augmented with the equality $! A ∣! A \equiv! A$ . As such in this section, we will consider the structural equivalence augmented with the equality $! A ∣! A \equiv! A$ .

In order to facilitate the readability of the proof, for a set S of names and variables, we will denote $P (S) = \prod_{a \in S \cap T_{ch}}! eav (a, y) ∣! eav (a, z)$ and $P_{o} (S) = \prod_{a \in S \cap T_{ch}}! eav (a, y) ∣! eav (a, z) ∣ ω a$ . Moreover, we will consider that $P (S) ∣ P (S) \equiv P (S)$ .

Hence, ${\overline{C}}_{S} [_]$ can now be written as $ν \tilde{n} . (\overline{D} ∣_∣ P_{o} (\tilde{n})) ∣ P_{o} (S)$ .

Note that from the definition, we have that for all A closed honest extended process, if $C [_] = ν \tilde{n} . (D ∣_)$ is $c$ -closing for A then ${\overline{C}}_{S} [_]$ is $e$ -closing for A for all S. Lemma 11.

Let A be an extended process and $ν \tilde{n}$ a sequence of names and variables. We have $\overline{ν \tilde{n} . A} \equiv ν \tilde{n} . (\overline{A} ∣ P (\tilde{n})$ .

Proof.

Direct from the definition. □

Lemma 12.

Let A be an closed honest extended process. Let $C [_] = ν \tilde{n} . (ν \tilde{m} . D ∣_)$ be an attacker evaluation context $c$ -closing for A such that D is named-cleaned and eavesdrop-free. Let S be a set of channel names such that $f c (C [A]) \subseteq S$ .

For all $C [A] \to_{c} A_{0}$ , there exist $A^{'}$ closed honest extended process, $C^{'} [_] = ν {\tilde{n}}^{'} . (ν {\tilde{m}}^{'} . D^{'} ∣_)$ an attacker evaluation context $c$ -closing for $A^{'}$ such that $D^{'}$ is name-cleaned and eavesdrop-free, $C^{'} [A^{'}] \equiv A_{0}$ and ${\overline{C}}_{S} [A] \to_{e} {\overline{C^{'}}}_{S} [A^{'}]$

For all ${\overline{C}}_{S} [A] \to_{e} A_{0}$ , there exist $A^{'}$ closed honest extended process, $C^{'} [_] = ν {\tilde{n}}^{'} . (ν {\tilde{m}}^{'} . D^{'} ∣_)$ an attacker evaluation context $c$ -closing for $A^{'}$ such that $D^{'}$ is name-cleaned and eavesdrop-free, ${\overline{C^{'}}}_{S} [A^{'}] \equiv A_{0}$ and $C [A] \to_{c} C^{'} [A^{'}]$

Proof.

We first start by proving the first property. Notice that by structural equivalence, we can always assume that the bound names and variables in $C [A]$ are only bound once and are distinct from the free names in S. Indeed, for all $C^{″} [_]$ , $A^{″}$ , if $C [A] \equiv C^{″} [A^{″}]$ only by renaming of bound names and variables then we obtain that ${\overline{C}}_{S} [A] \equiv {\overline{C^{″}}}_{S} [A^{″}]$ .

We do a case analysis on the internal rule applied.

Case 1.a, rule Then on D, i.e. $D = if u = v then D_{1} else D_{2} ∣ D_{3}$ and $A_{0} \equiv ν \tilde{n} . (D_{2} ∣ D_{3} ∣ A)$ : In such a case we have $\overline{D} \to_{e} \overline{D_{1}} ∣ \overline{D_{3}}$ and so $ν \tilde{m} . (\overline{D} ∣ P (\tilde{m})) \to_{e} ν \tilde{m} . (\overline{D_{1}} ∣ \overline{D_{3}} ∣ P (\tilde{m}))$ . By Lemma 11, we obtain that $\overline{ν \tilde{m} . D} \to \overline{ν \tilde{m} . (D_{1} ∣ D_{3})}$ . Let us denote $C^{'} [_] = ν \tilde{n} . (ν \tilde{m} . (D_{1} ∣ D_{3}) ∣_)$ and $A^{'} = A$ . Since ${\overline{C^{'}}}_{S} [_] = ν \tilde{n} . (\overline{ν \tilde{m} . (D_{1} ∣ D_{3})} ∣_∣ P_{o} (\tilde{n})) ∣ P_{o} (S)$ , we obtain that $A_{0} \equiv C^{'} [A^{'}]$ and ${\overline{C}}_{S} [A] \to_{e} {\overline{C^{'}}}_{S} [A^{'}]$ .

Case 1.b, rule Else on D: Similar to Case 1.a.

Case 2.a, rule Then on A, i.e. $A \equiv ν \tilde{r} . (if u = v then P_{1} else P_{2} ∣ P_{3})$ and $A_{0} \equiv C [ν \tilde{r} . (P_{1} ∣ P_{3})]$ : In such a case, let us denote $C^{'} [_] = C [_]$ and $A^{'} = ν \tilde{r} . (P_{1} ∣ P_{3})$ . Therefore, $C^{'} [A^{'}] = C [A^{'}] \equiv A_{0}$ . Note that $A \to_{e} A^{'}$ . Hence $C [A] \to_{e} C [A^{'}]$ and ${\overline{C}}_{S} [A] \to_{e} {\overline{C}}_{S} [A^{'}]$ . Thus the result holds.

Case 2.b, rule Else on A: Similar to Case 2.a.

Case 3, rule Comm on A, i.e. $A \equiv ν \tilde{r} . ({out}^{ho} (c, u) . P_{1} ∣ {in}^{ho} (c, x) . P_{2} ∣ P_{3})$ and $A_{0} \equiv C [ν \tilde{r} . (P_{1} ∣ P_{2} {^{u} /_{x}} ∣ P_{3})]$ : Note that even though $A \to_{c} ν \tilde{r} . (P_{1} ∣ P_{2} {^{u} /_{x}} ∣ P_{3})$ , we don’t necessarily have that $A \to_{e} ν \tilde{r} . (P_{1} ∣ P_{2} {^{u} /_{x}} ∣ P_{3})$ . We have to do a case analysis on u and c:

Case 3.a, $c \in \tilde{r}$ : In such a case, we know from A being an honest processes that $c \notin o c (P_{3})$ . Thus we can apply rule C-Priv to obtain that $A \to_{e} ν \tilde{r} . (P_{1} ∣ P_{2} {^{u} /_{x}} ∣ P_{3})$ . Hence, by denoting $C^{'} [_] = C [_]$ and $A^{'} = ν \tilde{r} . (P_{1} ∣ P_{2} {^{u} /_{x}} ∣ P_{3})$ , we obtain that $C^{'} [A^{'}] = C [A^{'}] \equiv A_{0}$ , $A \to_{e} A^{'}$ and so $C [A] \to_{e} C [A^{'}]$ and ${\overline{C}}_{S} [A] \to_{e} {\overline{C}}_{S} [A^{'}]$ . Therefore, the result holds.

Case 3.b, $c \notin \tilde{r}$ and u of base type: In such a case, ${out}^{ho} (c, u) . P_{1} ∣ {in}^{ho} (c, x) . P_{2} ∣ P_{3} ∣ eav (c, y) \to_{e} P_{1} ∣ P_{2} {^{u} /_{x}} ∣ P_{3}$ by the rule C-Eav. Let us denote $A^{'} = ν \tilde{r} . (P_{1} ∣ P_{2} {^{u} /_{x}} ∣ P_{3})$ . Since $c \notin \tilde{r}$ , we obtain that $A ∣ eav (c, y) \to_{e} A^{'}$ and so $A ∣! eav (c, y) \to_{e} A^{'} ∣! eav (c, y)$ . By noticing that c is either in $\tilde{n}$ or in $f c (C [A])$ and so in S, the structural equivalence gives us that ${\overline{C}}_{S} [A] \to_{e} {\overline{C}}_{S} [A^{'}]$ . Hence the result holds with $C^{'} [_] = C [_]$ .

Case 3.c, $c \notin \tilde{r}$ and u of channel type: This case is very similar to Case 3.b. Indeed, ${out}^{ho} (c, u) . P_{1} ∣ {in}^{ho} (c, x) . P_{2} ∣ P_{3} ∣ eav (c, z) \to_{e} P_{1} ∣ P_{2} {^{u} /_{x}} ∣ P_{3} ∣ ω c$ by the rule C-OEav. Let us denote $A^{'} = ν \tilde{r} . (P_{1} ∣ P_{2} {^{u} /_{x}} ∣ P_{3})$ . Since $c \notin \tilde{r}$ , we obtain that $A ∣ eav (c, z) \to_{e} A^{'} ∣ ω c$ and so $A ∣! eav (c, z) ∣ ω c \to_{e} A^{'} ∣! eav (c, z) ∣ ω c$ . By noticing that c is either in $\tilde{n}$ or in $f c (C [A])$ and so in S, the structural equivalence gives us that ${\overline{C}}_{S} [A] \to_{e} {\overline{C}}_{S} [A^{'}]$ . Hence the result holds with $C^{'} [_] = C [_]$ .

Case 4, rule Comm on D, i.e. $D = {out}^{at} (c, u) . D_{1} ∣ {in}^{at} (c, x) . D_{2} ∣ D_{3}$ and $A_{0} \equiv ν \tilde{n} . (ν \tilde{m} . (D_{1} ∣ D_{2} {^{u} /_{x}} ∣ D_{3}) ∣ A)$ : Let us do a case analysis on u:

Case 4.a, u is of base type: In such a case, we have ${out}^{at} (c, u) . \overline{D_{1}} ∣ {in}^{at} (c, x) . \overline{D_{2}} ∣ \overline{D_{3}} \to_{e} \overline{D_{1}} ∣ \overline{D_{2} {^{u} /_{x}}} ∣ \overline{D_{3}}$ by the rule C-Env. Hence, $ν \tilde{m} . ({out}^{at} (c, u) . \overline{D_{1}} ∣ {in}^{at} (c, x) . \overline{D_{2}} ∣ \overline{D_{3}} ∣ P (\tilde{m})) \to_{e} ν \tilde{m} . (\overline{D_{1}} ∣ \overline{D_{2} {^{u} /_{x}}} ∣ \overline{D_{3}} ∣ P (\tilde{m}))$ . Let us denote $D^{'} = (D_{1} ∣ D_{2} {^{u} /_{x}} ∣ D_{3})$ . By Lemma 11, we obtain that $\overline{ν \tilde{m} . D} \to_{e} \overline{ν \tilde{m} . D^{'}}$ . Hence, we deduce that $ν \tilde{n} . (\overline{ν \tilde{m} . D} ∣ A ∣ P_{o} (\tilde{n})) ∣ P_{o} (S) \to_{e} ν \tilde{n} . (\overline{ν \tilde{m} . D^{'}} ∣ A ∣ P_{o} (\tilde{n})) ∣ P_{o} (S)$ . Let us denote $C^{'} [_] = ν \tilde{n} . (ν \tilde{m} . D^{'} ∣_)$ and $A^{'} = A$ . We have $A_{0} \equiv C^{'} [A^{'}]$ and ${\overline{C}}_{S} [A] \to_{e} {\overline{C^{'}}}_{S} [A^{'}]$ . Hence the result holds.

Case 4.b, u is of channel type and $u \notin \tilde{m} \cup \tilde{n}$ : In such a case, $u \in fv (C [A]) \subseteq S$ and we have ${out}^{at} (c, u) . \overline{D_{1}} ∣ {in}^{at} (c, x) . (\overline{D_{2}} ∣ P (x)) ∣ \overline{D_{3}} \to_{e} \overline{D_{1}} ∣ \overline{D_{2} {^{u} /_{x}}} ∣ \overline{D_{3}} ∣ P (u) ∣ ω u$ by the rule C-Open. Since $u \notin \tilde{m}$ , we obtain that $ν \tilde{m} . ({out}^{at} (c, u) . \overline{D_{1}} ∣ {in}^{at} (c, x) . (\overline{D_{2}} ∣ P (x)) ∣ \overline{D_{3}} ∣ P (\tilde{m})) \to_{e} ν \tilde{m} . (\overline{D_{1}} ∣ \overline{D_{2} {^{u} /_{x}}} ∣ \overline{D_{3}} ∣ P (\tilde{m})) ∣ P_{o} (u)$ . Let us denote $D^{'} = (D_{1} ∣ D_{2} {^{u} /_{x}} ∣ D_{3})$ . By Lemma 11, we obtain that $\overline{ν \tilde{m} . D} \to_{e} \overline{ν \tilde{m} . D^{'}} ∣ P_{o} (u)$ . Moreover, since $u \notin \tilde{n}$ then $ν \tilde{n} . (\overline{ν \tilde{m} . D} ∣ A ∣ P_{o} (\tilde{n})) \to_{e} \tilde{n} . (\overline{ν \tilde{m} . D^{'}} ∣ A ∣ P_{o} (\tilde{n})) ∣ P_{o} (u)$ . Lastly, since $u \in S$ and $P_{o} (u) ∣ P_{o} (u) \equiv P_{o} (u)$ , we obtain that $ν \tilde{n} . (\overline{ν \tilde{m} . D} ∣ A ∣ P_{o} (\tilde{n})) ∣ P_{o} (S) \to_{e} \tilde{n} . (\overline{ν \tilde{m} . D^{'}} ∣ A ∣ P_{o} (\tilde{n})) ∣ P_{o} (S)$ . Therefore, the result holds with $A^{'} = A$ and $C^{'} [_] = ν \tilde{n} . (ν \tilde{m} . D^{'} ∣_)$ .

Case 4.c, u is of channel type and $u \in \tilde{n}$ : This case is similar to Case 4.b. Since $u \notin \tilde{m}$ , we can apply the same reasoning and obtain $\overline{ν \tilde{m} . D} \to_{e} \overline{ν \tilde{m} . D^{'}} ∣ P_{o} (u)$ where $D^{'} = (D_{1} ∣ D_{2} {^{u} /_{x}} ∣ D_{3})$ . Since $u \in \tilde{n}$ and $P_{o} (u) ∣ P_{o} (u) \equiv P_{o} (u)$ , we deduce that $ν \tilde{n} . (\overline{ν \tilde{m} . D} ∣ A ∣ P_{o} (\tilde{n})) \to_{e} ν \tilde{n} . (\overline{ν \tilde{m} . D^{'}} ∣ A ∣ P_{o} (\tilde{n}))$ . Therefore, we obtain that $ν \tilde{n} . (\overline{ν \tilde{m} . D} ∣ A ∣ P_{o} (\tilde{n})) ∣ P_{o} (S) \to_{e} ν \tilde{n} . (\overline{ν \tilde{m} . D^{'}} ∣ A ∣ P_{o} (\tilde{n})) ∣ P_{o} (S)$ and so the result holds with $A^{'} = A$ and $C^{'} [_] = ν \tilde{n} . (ν \tilde{m} . D^{'} ∣_)$ .

Case 4.d, u is of channel type and $u \in \tilde{m}$ : First of all, note that since $u \in \tilde{m}$ , $ν \tilde{m} . D \equiv ν u . ν {\tilde{m}}^{'} . D$ for some ${\tilde{m}}^{'}$ such that $u \notin {\tilde{m}}^{'}$ . Note that since u is bound, $u \notin fv (A) \cup fn (A)$ . Hence, by applying the same reasoning as in Case 4.b, we obtain that $\overline{ν {\tilde{m}}^{'} . D} \to_{e} \overline{ν {\tilde{m}}^{'} . D^{'}} ∣ P_{o} (u)$ where $D^{'} = (D_{1} ∣ D_{2} {^{u} /_{x}} ∣ D_{3})$ . Since $P (u) ∣ P_{o} (u) \equiv P (u) ∣ ω u ∣ P (u) \equiv P_{o} (u)$ , we deduce that $ν u . (\overline{ν {\tilde{m}}^{'} . D} ∣ P (u)) \to_{e} ν u . (\overline{ν {\tilde{m}}^{'} . D^{'}} ∣ P_{o} (u))$ . First, notice that $ν u . (\overline{ν {\tilde{m}}^{'} . D} ∣ P (u)) = \overline{ν u . ν {\tilde{m}}^{'} . D} = \overline{ν \tilde{m} . D}$ by Lemma 11. Second, since u does not appear in A, we deduce that $ν \tilde{n} . (\overline{ν \tilde{m} . D} ∣ A ∣ P_{o} (\tilde{n})) \to_{e} ν \tilde{n} . (ν u . (\overline{ν {\tilde{m}}^{'} . D^{'}} ∣ P_{o} (u)) ∣ A ∣ P_{o} (\tilde{n}) \equiv ν \tilde{n} . ν u . (\overline{ν {\tilde{m}}^{'} . D^{'}} ∣ A ∣ P_{o} (\tilde{n} \cup {u}))$ . Hence, if we denote ${\tilde{n}}^{'} = ν \tilde{n} . ν \tilde{u}$ then $ν \tilde{n} . (\overline{ν \tilde{m} . D} ∣ A ∣ P_{o} (\tilde{n})) \to_{e} ν {\tilde{n}}^{'} . (\overline{ν {\tilde{m}}^{'} . D^{'}} ∣ A ∣ P_{o} ({\tilde{n}}^{'}))$ . Therefore, by denoting $C^{'} [_] = ν {\tilde{n}}^{'} . (ν {\tilde{m}}^{'} . D^{'} ∣_{)}$ and $A^{'} = A$ , we deduce ${\overline{C}}_{S} [A] \to_{e} {\overline{C^{'}}}_{S} [A^{'}]$ . Thus the result holds.

Case 5, rule Comm between A (input) and D (output), i.e. $D = {out}^{at} (c, u) . D_{1} ∣ D_{2}$ , $A \equiv ν \tilde{r} . ({in}^{ho} (c, x) . P_{1} ∣ P_{2})$ and $A_{0} \equiv ν \tilde{n} . ν \tilde{m} . ν \tilde{r} . (D_{1} ∣ D_{2} ∣ P_{1} {^{u} /_{x}} ∣ P_{2})$ : Note that $c \notin \tilde{m} \cup \tilde{r}$ . Let us do a case analysis on u:

Case 5.a, u is of base type: In such a case, let us split $\tilde{r}$ and $\tilde{m}$ in ${\tilde{r}}_{b} . {\tilde{r}}_{c}$ and ${\tilde{m}}_{b} . {\tilde{m}}_{c}$ respectively, such that ${\tilde{r}}_{c}$ and ${\tilde{m}}_{c}$ are of channel type, and ${\tilde{r}}_{b}$ and ${\tilde{m}}_{b}$ are of base type. Since u is of base type, we deduce that $A_{0} \equiv ν \tilde{n} . ν {\tilde{m}}_{b} . ν {\tilde{r}}_{b} . (ν {\tilde{m}}_{c} . (D_{1} ∣ D_{2}) ∣ ν {\tilde{r}}_{c} . (P_{1} {^{u} /_{x}} ∣ P_{2}))$ . Note that ${out}^{at} (c, u) . \overline{D_{1}} ∣ \overline{D_{2}} ∣ {in}^{ho} (c, x) . P_{1} ∣ P_{2} \to_{e} \overline{D_{1}} ∣ \overline{D_{2}} ∣ P_{1} {^{u} /_{x}} ∣ P_{2}$ by the rule C-Env. Hence ${out}^{at} (c, u) . \overline{D_{1}} ∣ \overline{D_{2}} ∣ {in}^{ho} (c, x) . P_{1} ∣ P_{2} ∣ P (\tilde{m}) \to_{e} \overline{D_{1}} ∣ \overline{D_{2}} ∣ P_{1} {^{u} /_{x}} ∣ P_{2} ∣ P (\tilde{m})$ . Therefore, $ν \tilde{m} . ν \tilde{r} . ({out}^{at} (c, u) . \overline{D_{1}} ∣ \overline{D_{2}} ∣ {in}^{ho} (c, x) . P_{1} ∣ P_{2} ∣ P (\tilde{m})) \to_{e} ν \tilde{m} . ν \tilde{r} . (\overline{D_{1}} ∣ \overline{D_{2}} ∣ P_{1} {^{u} /_{x}} ∣ P_{2} ∣ P (\tilde{m}))$ . But $ν \tilde{m} . ν \tilde{r} . ({out}^{at} (c, u) . \overline{D_{1}} ∣ \overline{D_{2}} ∣ {in}^{ho} (c, x) . P_{1} ∣ P_{2} ∣ P (\tilde{m})) \equiv \overline{ν \tilde{m} . D} ∣ A$ thanks to Lemma 11 and since we assume that bound names and variables are bound once and distinct from free names and variables. Moreover, $ν \tilde{m} . ν \tilde{r} . (\overline{D_{1}} ∣ \overline{D_{2}} ∣ P_{1} {^{u} /_{x}} ∣ P_{2} ∣ P (\tilde{m})) \equiv ν {\tilde{m}}_{b} . ν {\tilde{r}}_{b} . (ν {\tilde{m}}_{c} . (\overline{D_{1}} ∣ \overline{D_{2}} ∣ P ({\tilde{m}}_{c})) ∣ ν {\tilde{r}}_{c} . (P_{1} {^{u} /_{x}} ∣ P_{2}))$ . Therefore, let us denote ${\tilde{n}}^{'} = \tilde{n} . {\tilde{m}}_{b} . {\tilde{r}}_{b}$ , $D^{'} = D_{1} ∣ D_{2}$ and $A^{'} = ν {\tilde{r}}_{c} . (P_{1} {^{u} /_{x}} ∣ P_{2})$ . Notice that ${\tilde{m}}_{b}$ and ${\tilde{r}}_{b}$ being of base type implies that $P_{o} (\tilde{n}) = P_{o} ({\tilde{n}}^{'})$ . Hence $ν \tilde{n} . (\overline{ν \tilde{m} . D} ∣ A ∣ P_{o} (\tilde{n})) ∣ P_{o} (S) \to_{e} ν {\tilde{n}}^{'} . (\overline{ν {\tilde{m}}_{c} . D^{'}} ∣ A^{'} ∣ P_{o} ({\tilde{n}}^{'})) ∣ P_{o} (S)$ . Hence, the result holds with $C^{'} [_] = ν {\tilde{n}}^{'} . (ν {\tilde{m}}_{c} . D^{'} ∣_)$ .

Case 5.b, u is of channel type and $u \notin \tilde{m} \cup \tilde{n}$ : Notice that in such a case $A_{0} \equiv ν \tilde{n} . (ν \tilde{m} . (D_{1} ∣ D_{2}) ∣ ν \tilde{r} . (P_{1} {^{u} /_{x}} ∣ P_{2}))$ . The rest of the proof follows a similar reasoning as in Case 4.b and the result will hold with $C^{'} [_] = ν \tilde{n} . (ν \tilde{m} . D^{'} ∣_)$ , $D^{'} = D_{1} ∣ D_{2}$ and $A^{'} = ν \tilde{r} . (P_{1} {^{u} /_{x}} ∣ P_{2})$ .

Case 5.c, u is of channel type and $u \in \tilde{n}$ : Notice that in such a case $A_{0} \equiv ν \tilde{n} . (ν \tilde{m} . (D_{1} ∣ D_{2}) ∣ ν \tilde{r} . (P_{1} {^{u} /_{x}} ∣ P_{2}))$ . The rest of the proof follows a similar reasoning as in Case 4.c and the result will hold with $C^{'} [_] = ν \tilde{n} . (ν \tilde{m} . D^{'} ∣_)$ , $D^{'} = D_{1} ∣ D_{2}$ and $A^{'} = ν \tilde{r} . (P_{1} {^{u} /_{x}} ∣ P_{2})$ .

Case 5.d, u is of channel type and $u \in \tilde{m}$ : Note that since $u \in \tilde{m}$ , $ν \tilde{m} . D \equiv ν u . ν {\tilde{m}}^{'} . D$ for some ${\tilde{m}}^{'}$ such that $u \notin {\tilde{m}}^{'}$ . Hence, $A_{0} \equiv ν \tilde{n} . ν u . (ν {\tilde{m}}^{'} . (D_{1} ∣ D_{2}) ∣ ν \tilde{r} . (P_{1} {^{u} /_{x}} ∣ P_{2}))$ . The rest of the proof follows a similar reasoning as in Case 4.d and the result will hold with $C^{'} [_] = ν {\tilde{n}}^{'} . (ν {\tilde{m}}^{'} . D^{'} ∣_)$ , $D^{'} = D_{1} ∣ D_{2}$ , $\tilde{n^{'}} = \tilde{n} . u$ and $A^{'} = ν \tilde{r} . (P_{1} {^{u} /_{x}} ∣ P_{2})$ .

Case 6, rule Comm between A (output) and D (input), i.e. $D = {in}^{at} (c, x) . D_{1} ∣ D_{2}$ , $A \equiv ν \tilde{r} . ({out}^{ho} (c, u) . P_{1} ∣ P_{2})$ and $A_{0} \equiv ν \tilde{n} . ν \tilde{m} . ν \tilde{r} . (D_{1} {^{u} /_{x}} ∣ D_{2} ∣ P_{1} ∣ P_{2})$ : Note that $c \notin \tilde{m} \cup \tilde{r}$ . Let us do a case analysis on u:

Case 6.a, u is of base type: In such a case, let us split $\tilde{r}$ and $\tilde{m}$ in ${\tilde{r}}_{b} . {\tilde{r}}_{c}$ and ${\tilde{m}}_{b} . {\tilde{m}}_{c}$ respectively, such that ${\tilde{r}}_{c}$ and ${\tilde{m}}_{c}$ are of channel type, and ${\tilde{r}}_{b}$ and ${\tilde{m}}_{b}$ are of base type. The rest of the proof follows a similar reasoning as in Case 5.a and the result holds with $C^{'} [_] = ν {\tilde{n}}^{'} . (ν {\tilde{m}}_{c} . D^{'} ∣_)$ , ${\tilde{n}}^{'} = \tilde{n} . {\tilde{m}}_{b} . {\tilde{r}}_{b}$ , $D^{'} = D_{1} {^{u} /_{x}} ∣ D_{2}$ and $A^{'} = ν {\tilde{r}}_{c} . (P_{1} ∣ P_{2})$ .

Case 6.b, u is of channel type and $u \notin \tilde{m} \cup \tilde{n}$ : Notice that in such a case $A_{0} \equiv ν \tilde{n} . (ν \tilde{m} . (D_{1} {^{u} /_{x}} ∣ D_{2}) ∣ ν \tilde{r} . (P_{1} ∣ P_{2}))$ . The rest of the proof follows a similar reasoning as in Case 4.b and the result will hold with $C^{'} [_] = ν \tilde{n} . (ν \tilde{m} . D^{'} ∣_)$ , $D^{'} = D_{1} {^{u} /_{x}} ∣ D_{2}$ and $A^{'} = ν \tilde{r} . (P_{1} ∣ P_{2})$ .

Case 6.c, u is of channel type and $u \in \tilde{n}$ : Notice that in such a case $A_{0} \equiv ν \tilde{n} . (ν \tilde{m} . (D_{1} ∣ D_{2}) ∣ ν \tilde{r} . (P_{1} {^{u} /_{x}} ∣ P_{2}))$ . The rest of the proof follows a similar reasoning as in Case 4.c and the result will hold with $C^{'} [_] = ν \tilde{n} . (ν \tilde{m} . D^{'} ∣_)$ , $D^{'} = D_{1} {^{u} /_{x}} ∣ D_{2}$ and $A^{'} = ν \tilde{r} . (P_{1} ∣ P_{2})$ .

Case 6.d, u is of channel type and $u \in \tilde{m}$ : Note that since $u \in \tilde{m}$ , $ν \tilde{m} . D \equiv ν u . ν {\tilde{m}}^{'} . D$ for some ${\tilde{m}}^{'}$ such that $u \notin {\tilde{m}}^{'}$ . Hence, $A_{0} \equiv ν \tilde{n} . ν u . (ν {\tilde{m}}^{'} . (D_{1} ∣ D_{2}) ∣ ν \tilde{r} . (P_{1} {^{u} /_{x}} ∣ P_{2}))$ . The rest of the proof follows a similar reasoning as in Case 4.d and the result will hold with $C^{'} [_] = ν {\tilde{n}}^{'} . (ν {\tilde{m}}^{'} . D^{'} ∣_)$ , $D^{'} = D_{1} {^{u} /_{x}} ∣ D_{2}$ , $\tilde{n^{'}} = \tilde{n} . u$ and $A^{'} = ν \tilde{r} . (P_{1} ∣ P_{2})$ .

This conclude the proof of the first property. The second property is in fact easy to prove: All rules in the eavesdropping semantics other than Then and Else will be mapped by the rule Comm in the classical semantics. One can notice that since we know that A and C do not contain eavesdrop processes and since the transformation from A to $\overline{A}$ and $C [_]$ to ${\overline{C}}_{S} [_]$ only adds processes of the form $eav (c, y) .0$ , the communication rules all becomes instances of the rule Comm. For instance, an application of rule C-Eav would result into the following $\begin{matrix} {out}^{ho} (c, u) . P ∣ {in}^{ho} (c, x) . Q ∣ eav (c, y) .0 {\overset{τ}{\to}}_{e} P ∣ Q {^{u} /_{x}} \end{matrix}$ which is typically the rule Comm when we remove the transformation and so the process $eav (c, y) .0$ . Lastly, since any instance of $ω d$ has no impact on the classical semantics, every rules thus corresponds to the rule Comm once the transformation removed. □

Corollary 3.

Theorem 6.

$\approx_{m}^{e} ⊊ \approx_{m}^{p} \cap \approx_{m}^{c}$ .

Proof.

Consider two closed honest extended process A and B. We assume $A \approx_{m}^{e} B$ . We first show that $A \approx_{m}^{c} B$ .

Let $C [_]$ be an attacker evaluation context $c$ -closing for A and B. Notice that in the classical semantics, a process $eav (c, x) . P$ as the same behaviour as the process 0. Hence, there exists $C^{1} [_]$ an attacker evaluation context eavesdrop-free and $c$ -closing for A and B such that for all c, $C [A] ⇓_{c}^{c} \Leftrightarrow C^{1} [A] ⇓_{c}^{c}$ and $C [B] ⇓_{c}^{c} \Leftrightarrow C^{1} [B] ⇓_{c}^{c}$ (1). Moreover, relying on the structural equivalence, we deduce that there exists $C^{2} = ν \tilde{n} . (ν \tilde{m} . D ∣ ν \tilde{r} . (_∣ E))$ attacker evaluation context eavesdrop-free and $c$ -closing for A and B such that D is named-cleaned, $C^{1} [A] \equiv C^{2} [A]$ and $C^{1} [B] \equiv C^{2} [B]$ . Lastly, by renaming $\tilde{r}$ through the structural equivalence, we deduce that there exist $A^{'}$ , $B^{'}$ two closed honest extended process and $C^{3} [_] = ν {\tilde{n}}^{'} . (ν {\tilde{m}}^{'} . (D^{'} ∣_))$ attacker evaluation context eavesdrop-free and $c$ -closing for A and B such that D is named-cleaned, $C^{2} [A] \equiv C^{3} [A^{'}]$ and $C^{2} [B] \equiv C^{3} [B^{'}]$ . Therefore, we have $C^{1} [A] \equiv C^{3} [A^{'}]$ and $C^{1} [B] \equiv C^{3} [B^{'}]$ . Lastly, let us denote $S = f c (C^{3} [A^{'}]) \cup f c (C^{3} [B^{'}])$ , relying on Lemma 11 and Definition 13, one can note that there exists $C^{4}$ attacker evaluation context $e$ -closing for A and B such that ${\overline{C^{3}}}_{S} [A^{'}] \equiv C^{4} [A]$ and ${\overline{C^{3}}}_{S} [B^{'}] \equiv C^{4} [B]$ .

We can conclude the proof as follows: Let $S = f c (C [A]) \cup f c (C [B])$ . For all channel c, $\begin{matrix} C [A] ⇓_{c}^{c} \\ iff & C^{1} [A] ⇓_{c}^{c} & by (1) \\ iff & C^{3} [A^{'}] ⇓_{c}^{c} & since C^{1} [A] \equiv C^{3} [A^{'}] \\ iff & {\overline{C^{3}}}_{S} [A^{'}] ⇓_{c}^{e} & by Corollary 3 \\ iff & C^{4} [A] ⇓_{c}^{e} & since {\overline{C^{3}}}_{S} [A^{'}] \equiv C^{4} [A] \\ iff & C^{4} [B] ⇓_{c}^{e} & since A \approx_{m}^{e} B \\ iff & {\overline{C^{3}}}_{S} [B^{'}] ⇓_{c}^{e} & since {\overline{C^{3}}}_{S} [B^{'}] \equiv C^{4} [B] \\ iff & C^{3} [B^{'}] ⇓_{c}^{c} & by Corollary 3 \\ iff & C^{1} [B] ⇓_{c}^{c} & since C^{1} [B] \equiv C^{3} [B^{'}] \\ iff & C [B] ⇓_{c}^{c} & by (1) \end{matrix}$

Let us now prove that $A \approx_{m}^{p} B$ . Let $C [_]$ be an attacker evaluation context $p$ -closing for A and B. As for the classical semantics, notice that in the private semantics, a process $eav (c, x) . P$ as the same behaviour as the process 0. Hence, there exists $C^{1} [_]$ an attacker evaluation context eavesdrop-free and $p$ -closing for A and B such that for all c, $C [A] ⇓_{c}^{p} \Leftrightarrow C^{1} [A] ⇓_{c}^{p}$ and $C [B] ⇓_{c}^{p} \Leftrightarrow C^{1} [B] ⇓_{c}^{p}$ . Moreover, notice that $\to_{p} \subseteq \to_{e}$ . Hence, for all c, $C^{1} [A] ⇓_{c}^{p}$ implies $C^{1} [A] ⇓_{c}^{e}$ and $C^{1} [B] ⇓_{c}^{p}$ implies $C^{1} [B] ⇓_{c}^{e}$ . Furthermore, since $C^{1} [_]$ is eavesdrop-free and $A, B$ are both honest, we deduce that rules C-Eav and C-OEav can never be applied in a derivation of $C^{1} [A]$ or $C^{1} [B]$ . Hence, we obtain that for all c, $C^{1} [A] ⇓_{c}^{p} \Leftrightarrow C^{1} [A] ⇓_{c}^{e}$ and $C^{1} [B] ⇓_{c}^{p} \Leftrightarrow C^{1} [B] ⇓_{c}^{e}$ . Lastly, $A \approx_{m}^{e} B$ implies that for all channel c, $C^{1} [A] ⇓_{c}^{e} \Leftrightarrow C^{1} [B] ⇓_{c}^{e}$ . We can conclude the proof by combining all these statements as follows: for all channel c, $\begin{matrix} C [A] ⇓_{c}^{p} \Leftrightarrow C^{1} [A] ⇓_{c}^{p} \Leftrightarrow C^{1} [A] ⇓_{c}^{e} \Leftrightarrow C^{1} [B] ⇓_{c}^{e} \Leftrightarrow C^{1} [B] ⇓_{c}^{p} \Leftrightarrow C [B] ⇓_{c}^{p} \end{matrix}$

We have concluded the proof of $\approx_{m}^{e} \subseteq \approx_{m}^{p} \cap \approx_{m}^{c}$ . Therefore, it remains to show that this inclusion is not strict. In Fig. 7, we have provided two processes A and B such that $A \approx_{ℓ}^{c} B$ , $A \approx_{ℓ}^{p} B$ but $A ≉_{t}^{e} B$ . Notice that these processes do not contain replication and so are imagine-finite. Thus, by Theorem 1, $A ≉_{t}^{e} B$ implies $A ≉_{m}^{e} B$ . Moreover, by Proposition 3, $A \approx_{ℓ}^{c} B$ and $A \approx_{ℓ}^{p} B$ implies $A \approx_{t}^{c} B$ , $A \approx_{t}^{p} B$ . Once again by Theorem 1, we deduce that $A \approx_{m}^{c} B$ , $A \approx_{m}^{p} B$ . Hence, we conclude that $\approx_{m}^{e} ⊊ \approx_{m}^{p} \cap \approx_{m}^{c}$ . □

Proof of Theorem 2

Proof of Theorem 7

The following theorem now follows directly from Lemmas 4 and 13. Theorem 7.

When restricted to $D (p)$ , we have $\approx_{r_{1}}^{s_{1}} = \approx_{r_{2}}^{s_{2}} ⊊ \approx_{r_{3}}^{c}$ for $s_{1}, s_{2} \in {p, e}$ , $r_{1}, r_{2}, r_{3} \in {ℓ, t}$ .

Proof of Theorem 8

Proof of Lemma 7

Proof of Theorem 9

Proof of Theorem 10

Proof of Theorem 11

References

Abadi and

Fournet, Mobile values, new names, and secure communication, in: 28th Symposium on Principles of Programming Languages (POPL’01),

H.R.

Nielson, ed., ACM, London, UK, 2001, pp. 104–115.

Abadi and

Fournet, Private authentication, Theor. Comput. Sci. 322(3) (2004), 427–476. doi:10.1016/j.tcs.2003.12.023.

Abadi and

A.D.

Gordon, A calculus for cryptographic protocols: The spi calculus, Inf. Comput. 148(1) (1999), 1–70. doi:10.1006/inco.1998.2740.

Adida, Helios: Web-based open-audit voting, in: 17th Conference on Security Symposium (SS’08), USENIX Association, 2008, pp. 335–348, http://dl.acm.org/citation.cfm?id=1496711.1496734 .

Arapinis,

Cheval and

Delaune, Verifying privacy-type properties in a modular way, in: Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF’12),

Cortier and

Zdancewic, eds, IEEE Computer Society Press, Cambridge Massachusetts, USA, 2012, pp. 95–109.

Arapinis,

Chothia,

Ritter and

Ryan, Analysing unlinkability and anonymity using the applied pi calculus, in: Proc. 23rd Computer Security Foundations Symposium (CSF’10), IEEE Computer Society Press, 2010, pp. 107–121.

Arapinis,

Mancini,

Ritter,

Ryan,

Golde,

Redon and

Borgaonkar, New privacy issues in mobile telephony: Fix and verification, in: 19th Conference on Computer and Communications Security (CCS’12), ACM Press, 2012, pp. 205–216.

Armando,

D.A.

Basin,

Boichut,

Chevalier,

Compagna,

Cuéllar,

P.H.

Drielsma,

P.-C.

Héam,

Kouchnarenko,

Mantovani,

Mödersheim,

von Oheimb,

Rusinowitch,

Santiago,

Turuani,

Viganò and

Vigneron, The AVISPA tool for the automated validation of Internet security protocols and applications, in: Proc. 17th International Conference on Computer Aided Verification (CAV’05), Lecture Notes in Computer Science, Springer, 2005, pp. 281–285.

Babel,

Cheval and

Kremer, On communication models when verifying equivalence properties, in: 6th International Conference on Principles of Security and Trust (POST’17), Lecture Notes in Computer Science, Vol. 10204, Springer, Uppsala, Sweden, 2017, pp. 141–163. doi:10.1007/978-3-662-54455-6.

10.

Baelde,

Delaune and

Hirschi, Partial order reduction for security protocols, in: Proceedings of the 26th International Conference on Concurrency Theory (CONCUR’15),

Aceto and

de Frutos-Escrig, eds, Leibniz International Proceedings in Informatics, Vol. 42, Leibniz-Zentrum für Informatik, Madrid, Spain, 2015, pp. 497–510, http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDH-concur15.pdf . doi:10.4230/LIPIcs.CONCUR.2015.497.

11.

Blanchet, Automatic verification of correspondences for security protocols, Journal of Computer Security 17(4) (2009), 363–434. doi:10.3233/JCS-2009-0339.

12.

Blanchet,

Abadi and

Fournet, Automated verification of selected equivalences for security protocols, Journal of Logic and Algebraic Programming 75(1) (2008), 3–51. doi:10.1016/j.jlap.2007.06.002.

13.

Chadha,

Cheval,

Ş.

Ciobâcă and

Kremer, Automated verification of equivalence properties of cryptographic protocol, ACM Transactions on Computational Logic 17(4) (2016), 1–32. doi:10.1145/2926715.

14.

Cheval,

Comon-Lundh and

Delaune, Trace equivalence decision: Negative tests and non-determinism, in: Proc. 18th ACM Conference on Computer and Communications Security (CCS’11), ACM, 2011.

15.

Cheval,

Cortier and

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

16.

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.

17.

Cheval,

Kremer and

Rakotonirina, DeepSec 1.1, 2019, https://github.com/DeepSec-prover/deepsec/tree/ae7a64e9023df242370b011dfa82a7586ac7a772.

18.

Cortier,

Delaune and

Dallon, SAT-Equiv: An efficient tool for equivalence properties, in: Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF’17), IEEE Computer Society Press, 2017, pp. 481–494. doi:10.1109/CSF.2017.15.

19.

Cortier,

Galindo and

Turuani, A formal analysis of the Neuchâtel e-voting protocol, in: IEEE European Symposium on Security and Privacy (EuroS&P), 2018.

20.

C.J.F.

Cremers, The Scyther Tool: Verification, falsification, and analysis of security protocols, in: Proc. 20th International Conference on Computer Aided Verification (CAV’08), Lecture Notes in Computer Science, Vol. 5123, Springer, 2008, pp. 414–418. doi:10.1007/978-3-540-70545-1_38.

21.

Delaune,

Kremer and

M.D.

Ryan, Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security 17(4) (2009), 435–487. doi:10.3233/JCS-2009-0340.

22.

Dong,

Jonker and

Pang, Analysis of a receipt-free auction protocol in the applied pi calculus, in: Proc. International Workshop on Formal Aspects in Security and Trust (FAST’10),

Etalle and

Guttman, eds, Pisa, Italy, 2010, To appear.

23.

P.T.

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

24.

J.K.

Millen and

Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, in: Proc. 8th Conference on Computer and Communications Security, ACM Press, 2001, pp. 166–175.

25.

L.C.

Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security 6(1/2) (1998), 85–128. doi:10.3233/JCS-1998-61-205.

26.

P.Y.A.

Ryan,

S.A.

Schneider,

Goldsmith,

Lowe and

A.W.

Roscoe, Modelling and Analysis of Security Protocols, Addison Wesley, 2000.

27.

Schmidt,

Meier,

Cremers and

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

28.

F.J.

Thayer Fabrega,

J.C.

Herzog and

J.D.

Guttman, Strand spaces: Proving security protocols correct, Journal of Computer Security 7(2/3) (1999), 191–230. doi:10.3233/JCS-1999-72-304.

29.

Tiu and

J.E.

Dawson, Automating open bisimulation checking for the spi calculus, in: Proc. 23rd Computer Security Foundations Symp. (CSF’10), IEEE Comp. Soc., 2010, pp. 307–321.

On the semantics of communications when verifying equivalence properties

Abstract

Keywords

1. Introduction

2. Model

2.1. Syntax

Definition 1 ((May-)Testing equivalences ≈ m c , ≈ m p , ≈ m e ).

Definition 2 (Observational equivalences ≈ o c , ≈ o p , ≈ o e ).

Definition 5 (Labeled bisimulations ≈ ℓ c , ≈ ℓ p , ≈ ℓ e ).

4.1.1. Defining classes of determinate processes and their relations

Definition 8 (Determinacy).

4.2.1. Bounded determinate processes

Footnotes

Acknowledgments

Refining Theorem 3

Proof of Proposition 2

Proof of Theorem 1

Proof of Theorem 6

Proof of Theorem 2

Proof of Theorem 7

Proof of Theorem 8

Proof of Lemma 7

Proof of Theorem 9

Proof of Theorem 10

Proof of Theorem 11

References

Definition 1 ((May-)Testing equivalences $\approx_{m}^{c}$ , $\approx_{m}^{p}$ , $\approx_{m}^{e}$ ).

Definition 2 (Observational equivalences $\approx_{o}^{c}$ , $\approx_{o}^{p}$ , $\approx_{o}^{e}$ ).

Definition 5 (Labeled bisimulations $\approx_{ℓ}^{c}$ , $\approx_{ℓ}^{p}$ , $\approx_{ℓ}^{e}$ ).