David Baelde, Stéphanie Delaune, and Lucca Hirschi

# Partial Order Reduction for Security Protocols

David Baelde  LSV, ENS Cachan & CNRS
<EMAIL_ADDRESS>Stéphanie Delaune  LSV, ENS Cachan
& CNRS
<EMAIL_ADDRESS>Lucca Hirschi  LSV, ENS Cachan &
CNRS
<EMAIL_ADDRESS>
###### Abstract

Security protocols are concurrent processes that communicate using
cryptography with the aim of achieving various security properties. Recent
work on their formal verification has brought procedures and tools for
deciding trace equivalence properties (_e.g._ anonymity, unlinkability, vote
secrecy) for a bounded number of sessions. However, these procedures are based
on a naive symbolic exploration of all traces of the considered processes
which, unsurprisingly, greatly limits the scalability and practical impact of
the verification tools.

In this paper, we overcome this difficulty by developing partial order
reduction techniques for the verification of security protocols. We provide
reduced transition systems that optimally eliminate redundant traces, and
which are adequate for model-checking trace equivalence properties of
protocols by means of symbolic execution. We have implemented our reductions
in the tool Apte, and demonstrated that it achieves the expected speedup on
various protocols.

##  1 Introduction

Security protocols are concurrent processes that use various cryptographic
primitives in order to achieve security properties such as secrecy,
authentication, anonymity, unlinkability, _etc._ They involve a high level of
concurrency and are difficult to analyse by hand. Actually, many protocols
have been shown to be flawed several years after their publication (and
deployment). This has lead to a flurry of research on formal verification of
protocols.

A successful way of representing protocols is to use variants of the
$\pi$-calculus, whose labelled transition systems naturally express how a
protocol may interact with a (potentially malicious) environment whose
knowledge increases as more messages are exchanged over the network. Some
security properties (_e.g.,_ secrecy, authentication) are then described as
reachability properties, while others (_e.g.,_ unlinkability, anonymity) are
expressed as trace equivalence properties. In order to decide such properties,
a reasonable assumption is to bound the number of protocol sessions, thereby
limiting the length of execution traces. Even under this assumption,
infinitely many traces remain, since each input may be fed infinitely many
different messages. However, symbolic execution and dedicated constraint
solving procedures have been devised to provide decision procedures for
reachability [27, 15] and, more recently, equivalence properties [36, 11].
Unfortunately, the resulting tools, especially those for checking equivalence
(_e.g.,_ Apte [10], Spec [35]), have a very limited practical impact because
they scale very badly. This is not surprising since they treat concurrency in
a very naive way, exploring all possible symbolic interleavings of concurrent
actions.

_Contributions._ We develop partial order reduction (POR) techniques [31, 7,
24] for trace equivalence checking of security protocols. Our main challenge
is to do it in a way that is compatible with symbolic execution: we should
provide a reduction that is effective when messages remain unknown, but
leverages information about messages when it is inferred by the constraint
solver. We achieve this by refining interleaving semantics in two steps,
gradually eliminating redundant traces. The first refinement, called
_compression_ , uses the notion of polarity [3] to impose a simple strategy on
traces. It does not rely on data analysis at all and can easily be used as a
replacement for the usual semantics in verification algorithms. The second
one, called _reduction_ , takes data into account and achieves optimality in
eliminating redundant traces. In practice, the reduction step can be
implemented in an approximated fashion, through an extension of constraint
resolution procedures. We have done so in the tool Apte, showing that our
theoretical results do translate to significant practical optimisations.

_Outline._ We consider in Section 2 a rich process algebra for representing
security protocols. It supports arbitrary cryptographic primitives, and even
includes a replication operator suitable for modelling unbounded numbers of
sessions. Thus, we do not restrict to a particular fragment for which a
decision procedure exists, but show the full scope of our theoretical results.
We give in Section 3 an _annotated_ semantics that will facilitate the next
technical developments. We then define our _compressed_ semantics in Section 4
and the _reduced_ semantics in Section 5. In both sections, we first restrict
the transition system, then show that the restriction is adequate for checking
trace equivalence under some action-determinism condition. We finally discuss
how these results can be lifted to the symbolic setting in Section 6.
Specifically, we describe how we have implemented our techniques in Apte, and
we present experimental results showing that the optimisations are fully
effective in practice. We discuss related work in Section 7, and conclude in
Section 8. Complete proofs are given in appendices.

##  2 Model for security protocols

In this section we introduce our process algebra, which is a variant of the
applied $\pi$-calculus [1] that has been designed with the aim of modelling
cryptographic protocols. Processes can exchange complex messages, represented
by terms quotiented by some equational theory.

One of the key difficulties in the applied $\pi$-calculus is to model the
knowledge of the environment, seen as an attacker who listens to network
communication and may also inject messages. One has to make a distinction
between the content of a message (sent by the environment) and the way the
message has been created (from knowledge available to the environment). While
the distinction between messages and recipes came from security applications,
it is naturally of much broader interest, as it gives a precise, intentional
content to labelled transitions that we exploit to analyse data dependencies.

We study a process algebra that may seem quite restrictive: we forbid internal
communication and private channels. This is however reasonable when studying
security protocols faced with the usual omnipotent attacker. In such a
setting, we end up considering the worst-case scenario where any communication
has to be made via the environment.

###  2.1 Syntax

We assume a number of disjoint and infinite sets: a set $\mathcal{C}$ of
_channels_ , whose elements are denoted by $a$, $b$, $c$; a set $\mathcal{N}$
of _private names_ or _nonces_ , denoted by $n$ or $k$; a set $\mathcal{X}$ of
_variables_ , denoted by $x$, $y$, $z$ as usual; and a set $\mathcal{W}$ of
_handles_ , denoted by $w$ and used for referring to previously output terms.
Next, we consider a signature $\Sigma$ consisting of a finite set of function
symbols together with their arity. Terms over $S$, written $\mathcal{T}(S)$,
are inductively generated from $S$ and function symbols from $\Sigma$. When
$S\subseteq\mathcal{N}$, elements of $\mathcal{T}(S)$ are called _messages_.
When $S\subseteq\mathcal{W}$, they are called _recipes_ and written $M$, $N$.
Intuitively, recipes express how a message has been derived by the environment
from the messages obtained so far. Finally, we consider an equational theory
$\mathsf{E}$ over terms to assign a meaning to function symbols in $\Sigma$.

######  Example 2.1.

Let $\Sigma=\\{\mathsf{enc}/2,\mathsf{dec}/2,\mathsf{h}/1\\}$ and $\mathsf{E}$
be the equational theory induced by the equation
$\mathsf{dec}(\mathsf{enc}(x,y),y)=x$. Intuitively, the symbols $\mathsf{enc}$
and $\mathsf{dec}$ represent symmetric encryption and decryption, whereas
$\mathsf{h}$ is used to model a hash function. Now, assume that the
environment knows the key $k$ as well as the ciphertext $\mathsf{enc}(n,k)$,
and that these two messages are referred to by handles $w$ and $w^{\prime}$.
The environment may decrypt the ciphertext with the key $k$, apply the hash
function, and encrypt the result using $k$ to get the message
$m_{0}=\mathsf{enc}(\mathsf{h}(n),k)$. This computation is modelled using the
_recipe_ $M_{0}=\mathsf{enc}(\mathsf{h}(\mathsf{dec}(w^{\prime},w)),w)$.

######  Definition 2.2.

Processes are defined by the following syntax where $c,a\in\mathcal{C}$,
$x\in\mathcal{X}$, $u,v\in\mathcal{T}(\mathcal{N}\cup\mathcal{X})$, and
$\vv{c}$ (resp. $\vv{n}$) is a sequence of channels from $\mathcal{C}$ (resp.
names from $\mathcal{N}$).

$P,Q\;::=\;0\;\mid\;(P\leavevmode\nobreak\ |\leavevmode\nobreak\
Q)\;\mid\;\mathtt{in}(c,x).P\;\mid\;\mathtt{out}(c,u).P\;\mid\;\mathtt{if}\
u=v\ \mathtt{then}\ P\ \mathtt{else}\
Q\;\mid\;\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P$

The last construct combines replication with channel and name restriction:
$\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P$ may be read as
$!(\nu\vv{c}.\mathtt{out}(a,\vv{c}).\nu\vv{n}.P)$ in standard applied
$\pi$-calculus. Our goal with this compound construct is to support
replication in a way that is not fundamentally incompatible with the action-
determinism condition which we eventually impose on our processes. This is
achieved here by advertising on the public channel $a$ any new copy of the
replicated process. At the same time, we make public the new channels $\vv{c}$
on which the copy may operate — but not the new names $\vv{n}$. While it may
seem restrictive, this style is actually natural for security protocols where
the attacker knows exactly to whom he is sending a message and from whom he is
receiving, _e.g.,_ via IP addresses.

We shall only consider _ground_ processes, where each variable is bound by an
input. We denote by $\mathsf{fc}(P)$ and $\mathsf{bc}(P)$ the set of _free_
and _bound channels_ of $P$.

######  Example 2.3.

The process $P_{0}$ models an agent who sends the ciphertext
$\mathsf{enc}(n,k)$, and then waits for an input on $c$. In case the input has
the expected form, the constant $\mathsf{ok}$ is emitted.
$P_{0}=\mathtt{out}(c,\mathsf{enc}(n,k)).\mathtt{in}(c,x).\mathtt{if}\
\mathsf{dec}(x,k)=\mathsf{h}(n)\ \mathtt{then}\ \mathtt{out}(c,\mathsf{ok}).0\
\mathtt{else}\ 0$

The processes $P_{0}$ as well as $\mathbf{\large!}^{a}_{c,n}P_{0}$ are ground.
We have that $\mathsf{fc}(P_{0})=\\{c\\}$ and $\mathsf{bc}(P_{0})=\emptyset$
whereas $\mathsf{fc}(\mathbf{\large!}^{a}_{c,n}P_{0})=\\{a\\}$ and
$\mathsf{bc}(\mathbf{\large!}^{a}_{c,n}P_{0})=\\{c\\}$.

###  2.2 Semantics

We only consider processes that are _normal_ w.r.t. _internal reduction_
$\rightsquigarrow$ defined as follows:

$\begin{array}[]{c}\left.\begin{array}[]{ccc}\mathtt{if}\ u=v\ \mathtt{then}\
P\ \mathtt{else}\ Q\rightsquigarrow P\mbox{ \it when
}u=_{\mathsf{E}}v&&P\leavevmode\nobreak\ |\leavevmode\nobreak\
Q\,\rightsquigarrow\,P^{\prime}\leavevmode\nobreak\ |\leavevmode\nobreak\ Q\\\
\mathtt{if}\ u=v\ \mathtt{then}\ P\ \mathtt{else}\ Q\rightsquigarrow Q\mbox{
\it when }u\neq_{\mathsf{E}}v&&Q\leavevmode\nobreak\ |\leavevmode\nobreak\
P\,\rightsquigarrow\,Q\leavevmode\nobreak\ |\leavevmode\nobreak\
P^{\prime}\end{array}\right\\}\begin{array}[]{l}{\footnotesize{\it
when\,}P\rightsquigarrow P^{\prime}}\\\ \end{array}\\\\[5.69054pt]
\begin{array}[]{ccccc}(P_{1}\leavevmode\nobreak\ |\leavevmode\nobreak\
P_{2})\leavevmode\nobreak\ |\leavevmode\nobreak\
P_{3}\,\rightsquigarrow\,P_{1}\leavevmode\nobreak\ |\leavevmode\nobreak\
(P_{2}\leavevmode\nobreak\ |\leavevmode\nobreak\ P_{3})&&P\leavevmode\nobreak\
|\leavevmode\nobreak\ 0\rightsquigarrow P&&0\leavevmode\nobreak\
|\leavevmode\nobreak\ P\,\rightsquigarrow\,P\end{array}\end{array}$

Any process in normal form built from parallel composition can be uniquely
written as $P_{1}\leavevmode\nobreak\ |\leavevmode\nobreak\
(P_{2}\leavevmode\nobreak\ |\leavevmode\nobreak\ (\ldots\leavevmode\nobreak\
|\leavevmode\nobreak\ P_{n}))$ with $n\geq 2$, which we note
$\Pi_{i=1}^{n}P_{i}$, where each process $P_{i}$ is neither a parallel
composition nor the process $0$.

We now define our labelled transition system. It deals with _configurations_
(denoted by $A$, $B$) which are pairs $(\mathcal{P};\Phi)$ where $\mathcal{P}$
is a multiset of ground processes and $\Phi$, called the _frame_ , is a
substitution mapping handles to messages that have been made available to the
environment. Given a configuration $A$, $\Phi(A)$ denotes its second
component. Given a frame $\Phi$, $\mathrm{dom}(\Phi)$ denotes its domain.

$\begin{array}[]{lcl}\mbox{\sc
In}&&(\\{\mathtt{in}(c,x).Q\\}\uplus\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathtt{in}(c,M)$}}}$}}(\\{Q\\{{M\Phi}/{x}\\}\\}\uplus\mathcal{P};\Phi)\;\;\;\;\;\;\hfill{\mbox{$M\in\mathcal{T}(\mathrm{dom}(\Phi))$}}\\\\[5.69054pt]
\mbox{\sc
Out}&&(\\{\mathtt{out}(c,u).Q\\}\uplus\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathtt{out}(c,w)$}}}$}}(\\{Q\\}\uplus\mathcal{P};\Phi\cup\\{w\mapsto
u\\})\hfill\;\;\;\;{\mbox{$w\in\mathcal{W}$ fresh}}\\\\[5.69054pt] \mbox{\sc
Repl}&&(\\{\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P\\}\uplus\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{${\mathtt{sess}(a,\vv{c})}$}}}$}}(\\{P;\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P\\}\uplus\mathcal{P};\Phi)\hfill{\mbox{$\vv{c},\vv{n}$
fresh}}\\\\[5.69054pt] \mbox{\sc
Par}&&(\\{\Pi_{i=1}^{n}P_{i}\\}\uplus\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\tau$}}}$}}(\\{P_{1},\ldots,P_{n}\\}\uplus\mathcal{P};\Phi)\\\\[5.69054pt]
\mbox{\sc
Zero}&&(\\{0\\}\uplus\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\tau$}}}$}}(\mathcal{P};\Phi)\end{array}$

Rule In expresses that an input process may receive any message that the
environment can derive from the current frame. In rule Out, the frame is
enriched with a new message. The last two rules simply translate the parallel
structure of processes into the multiset structure of the configuration. As
explained above, rule Repl combines the replication of a process together with
the creation of new channels and nonces. The channels $\vv{c}$ are implicitly
made public, but the newly created names $\vv{n}$ remain private. Remark that
channels $\vv{c}$ and names $\vv{n}$ must be fresh, _i.e.,_ they do not appear
free in the original configuration. As usual, freshness conditions do not
block executions: it is always possible to rename bound channels $\vv{c}$ and
names $\vv{n}$ of a process $\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P$ before
applying Repl. We denote by $\mathsf{bc}(\mathsf{tr})$ the bound channels of a
trace $\mathsf{tr}$, _i.e.,_ all the channels that occur in second argument of
an action $\mathtt{sess}(a,\vv{c})$ in $\mathsf{tr}$, and we consider traces
where channels are bound at most once.

######  Example 2.4.

Going back to Example 2.3 with $\Phi_{0}=\\{w_{1}\mapsto k\\}$, we have that:
$(\\{\mathbf{\large!}^{a}_{c,n}P_{0}\\};\Phi_{0})\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathtt{sess}(a,c)$}}}$}}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathtt{out}(c,w_{2})$}}}$}}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathtt{in}(c,M_{0})$}}}$}}(\\{\mathtt{out}(c,\mathsf{ok}).0;\mathbf{\large!}^{a}_{c,n}P_{0}\\};\Phi)$
where $\Phi=\\{w_{1}\mapsto k,w_{2}\mapsto\mathsf{enc}(n,k)\\}$ and
$M_{0}=\mathsf{enc}(\mathsf{h}(\mathsf{dec}(w_{2},w_{1})),w_{1})$.

###  2.3 Equivalences

We are concerned with trace equivalence, which is used [8, 17] to model
anonymity, untraceability, strong secrecy, etc. Finer behavioural
equivalences, _e.g.,_ weak bisimulation, appear to be too strong with respect
to what an attacker can really observe. Intuitively, two configurations are
trace equivalent if the attacker cannot tell whether he is interacting with
one or the other. To make this formal, we introduce a notion of equivalence
between frames.

######  Definition 2.5.

Two frames $\Phi$ and $\Phi^{\prime}$ are in _static equivalence_ , written
$\Phi\sim\Phi^{\prime}$, when
$\mathrm{dom}(\Phi)=\mathrm{dom}(\Phi^{\prime})$, and:
$M\Phi=_{\mathsf{E}}N\Phi\;\Leftrightarrow\;M\Phi^{\prime}=_{\mathsf{E}}N\Phi^{\prime}\mbox{
for any terms $M,N\in\mathcal{T}(\mathrm{dom}(\Phi))$}.$

######  Example 2.6.

Continuing Example 2.4, consider $\Phi^{\prime}=\\{w_{1}\mapsto
k^{\prime},w_{2}\mapsto\mathsf{enc}(n,k)\\}$. The test
${\mathsf{enc}(\mathsf{dec}(w_{2},w_{1}),w_{1})=w_{2}}$ is true in $\Phi$ but
not in $\Phi^{\prime}$, thus $\Phi\not\sim\Phi^{\prime}$.

We then define $\mathsf{obs}(\mathsf{tr})$ to be the subsequence of
$\mathsf{tr}$ obtained by erasing $\tau$ actions.

######  Definition 2.7.

Let $A$ and $B$ be two configurations. We say that $A\sqsubseteq B$ when, for
any
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}A^{\prime}$
such that $\mathsf{bc}(\mathsf{tr})\cap\mathsf{fc}(B)=\emptyset$, there exists
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}^{\prime}$}}}$}}B^{\prime}$
such that $\mathsf{obs}(\mathsf{tr})=\mathsf{obs}(\mathsf{tr}^{\prime})$ and
${\Phi(A^{\prime})\sim\Phi(B^{\prime})}$. They are _trace equivalent_ ,
written $A\approx B$, when $A\sqsubseteq B$ and $B\sqsubseteq A$.

In order to lift our optimised semantics to trace equivalence, we will require
configurations to be action-deterministic. This common assumption in POR
techniques [7] is also reasonable in the context of security protocols, where
the attacker knows with whom he is communicating.

######  Definition 2.8.

A configuration $A$ is action-deterministic if whenever
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}(\mathcal{P};\Phi)$,
and $P,Q$ are two elements of $\mathcal{P}$, we have that $P$ and $Q$ cannot
perform an observable action of the same nature ($\mathtt{in}$,
$\mathtt{out}$, or $\mathtt{sess}$) on the same channel (_i.e.,_ if both
actions are of same nature, their first argument has to differ).

##  3 Annotated semantics

We shall now define an intermediate semantics whose transitions are equipped
with more informative actions. The annotated actions will notably feature
_labels_ $\ell\in\mathbb{N}^{*}$ indicating from which concurrent processes
they originate. A labelled action will be written $[\alpha]^{\ell}$ where
$\alpha$ is an action and $\ell$ is a label. Similarly, a labelled process
will be written $[P]^{\ell}$. When reasoning about trace equivalence between
two configurations, it will be crucial to maintain a consistent labelling
between configurations along the execution. In order to do so, we define
_skeletons of observable actions_ , which are of the form $\mathtt{in}_{c}$,
$\mathtt{out}_{c}$ or $!^{a}$ where $a,c\in\mathcal{C}$, and we assume a total
ordering over those skeletons, denoted $<$ with $\leq$ its reflexive closure.
Any process that is neither $0$ nor a parallel composition induces a skeleton
corresponding to its toplevel connective, and we denote it by
$\mathsf{sk}(P)$.

We define in Figure 1 the annotated semantics
$\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}$}}_{a}$
over configurations whose processes are labelled. In Par, note that
$\mathsf{sk}(P_{i})$ is well defined as $P_{i}$ cannot be a zero or a parallel
composition. Also note that the label of an action is always that of the
active process in that transition. More importantly, the annotated transition
system does not restrict the executions of a process but simply annotates them
with labels, and replaces $\tau$ actions by more descriptive actions.

$\begin{array}[]{l}\mbox{\sc
In/Out}\;\;(\\{[P]^{\ell}\\}\uplus\mathcal{P};\Phi)\xrightarrow{\;[\alpha]^{\ell}\;}_{a}(\\{[P^{\prime}]^{\ell}\\}\uplus\mathcal{P};\Phi^{\prime})(\\{P\\}\uplus\mathcal{P};\Phi)\xrightarrow{\;\alpha\;}(\\{P^{\prime}\\}\uplus\mathcal{P};\Phi^{\prime})\\\\[8.53581pt]
\mbox{\sc
Repl}\;\;(\\{[\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P_{0}]^{\ell}\\}\uplus\mathcal{P};\Phi)\xrightarrow{[\mathtt{sess}(a,\vv{c})]^{\ell}}_{a}(\\{[P_{0}]^{\ell\cdot
1},[\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P_{0}]^{\ell\cdot
2}\\}\uplus\mathcal{P};\Phi)\;\;\mbox{$\vv{c},\vv{n}$ fresh}\\\\[8.53581pt]
\mbox{\sc
Par}\;\;(\\{[\Pi_{i=1}^{n}P_{i}]^{\ell}\\}\uplus\mathcal{P};\Phi)\xrightarrow{[\mathtt{par}(\sigma_{\pi(1)};\ldots;\sigma_{\pi(n)})]^{\ell}}_{a}(\\{[P_{\pi(1)}]^{\ell\cdot
1},\ldots,[P_{\pi(n)}]^{\ell\cdot n}\\}\uplus\mathcal{P};\Phi)\\\\[2.84526pt]
\lx@intercol\hfil$\mbox{$\sigma_{i}=\mathsf{sk}(P_{i})$ and $\pi$ is a
permutation over $[1,...n]$ such that
<EMAIL_ADDRESS>\mbox{\sc Zero}\;\;\hskip
28.45274pt(\\{[0]^{\ell}\\}\uplus\mathcal{P};\Phi)\xrightarrow{[\mathtt{zero}]^{\ell}}_{a}(\mathcal{P};\Phi)\end{array}$

Figure 1: Annotated semantics

We now define how to extract sequential dependencies from labels, which will
allow us to analyse concurrency in a trace without referring to
configurations.

######  Definition 3.1.

Two labels are _dependent_ if one is a prefix of the other. We say that the
labelled actions $\alpha$ and $\beta$ are _sequentially dependent_ when their
labels are dependent, and _recipe dependent_ when
$\\{\alpha,\beta\\}=\\{[\mathtt{in}(c,M)]^{\ell},[\mathtt{out}(c^{\prime},w)]^{\ell^{\prime}}\\}$
with $w$ occurring in $M$. They are _dependent_ when they are either
sequentially or recipe dependent. Otherwise, they are _independent_.

######  Definition 3.2.

A configuration $(\mathcal{P};\Phi)$ is _well labelled_ if $\mathcal{P}$ is a
multiset of labelled processes such that two elements of $\mathcal{P}$ have
independent labels.

Obviously, any unlabelled configuration may be well labelled. Further, it is
easy to see that well labelling is preserved by
$\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}$}}_{a}$.
Thus, we shall implicitly assume to be working with well labelled
configurations in the rest of the paper. Under this assumption, we obtain the
following fundamental lemma.

######  Lemma 3.3.

Let $A$ be a (well labelled) configuration, $\alpha$ and $\beta$ be two
independent labelled actions. We have
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\alpha.\beta$}}}$}}_{a}A^{\prime}$
if, and only if,
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\beta.\alpha$}}}$}}_{a}A^{\prime}$.

#### Symmetries of trace equivalence.

We will see that, when checking $A\approx B$ for action-deterministic
configurations, it is sound to require that $B$ can perform all traces of $A$
in the annotated semantics (and the converse). In other words, labels and
detailed non-observable actions $\mathtt{zero}$ and
$\mathtt{par}(\sigma_{1}\ldots\sigma_{n})$ are actually relevant for trace
equivalence. Obviously, this can only hold if $A$ and $B$ are labelled
consistently. In order to express this, we extend $\mathsf{sk}(P)$ to parallel
and zero processes: we let their skeletons be the associated action in the
annotated semantics. Next, we define the labelled skeletons by
$\mathsf{skl}([P]^{\ell})=[\mathsf{sk}(P)]^{\ell}$. When checking for
equivalence of $A$ and $B$, we shall assume that
$\mathsf{skl}(A)=\mathsf{skl}(B)$, _i.e.,_ the configurations have the same
set of labelled skeletons. This technical condition is obviously not
restrictive in practice.

######  Example 3.4.

Let $A=(\\{[\mathtt{in}(a,x).((\mathtt{out}(b,m).P_{1})\leavevmode\nobreak\
|\leavevmode\nobreak\ P_{2})]^{0}\\};\Phi)$ with $P_{1}=\mathtt{in}(c,y).0$
and $P_{2}=\mathtt{in}(d,z).0$, and $B$ the configuration obtained from $A$ by
swapping $P_{1}$ and $P_{2}$. We have
$\mathsf{skl}(A)=\mathsf{skl}(B)=\\{[\mathtt{in}_{a}]^{0}\\}$. Consider the
following trace:
$\mathsf{tr}=[\mathtt{in}(a,\mathtt{ok})]^{0}.[\mathtt{par}(\\{\mathtt{out}_{b};\mathtt{in}_{d}\\})]^{0}.[\mathtt{out}(b,w)]^{0\cdot
1}.[\mathtt{in}(c,w)]^{0\cdot 1}.[\mathtt{in}(d,w)]^{0\cdot 2}$
Assuming $\mathtt{out}_{b}<\mathtt{in}_{d}$ and $\mathsf{ok}\in\Sigma$, we
have
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}A^{\prime}$.
However, there is no $B^{\prime}$ such that
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}B^{\prime}$,
for two reasons. First, $B$ cannot perform the second action since skeletons
of sub-processes of its parallel composition are
$\\{\mathtt{out}_{b};\mathtt{in}_{c}\\}$. Second, even if we ignored that
mismatch on a non-observable action, $B$ would not be able to perform the
action $\mathtt{in}(c,w)$ with the right label. Such mismatches can actually
be systematically used to show $A\not\approx B$, as shown next.

######  Lemma 3.5.

Let $A$ and $B$ be two action-deterministic configurations such that
${A\approx B}$ and $\mathsf{skl}(A)=\mathsf{skl}(B)$. For any execution
$A\xrightarrow{[\alpha_{1}]^{\ell_{1}}}_{a}A_{1}\xrightarrow{[\alpha_{2}]^{\ell_{2}}}_{a}\ldots\xrightarrow{[\alpha_{n}]^{\ell_{n}}}_{a}A_{n}$
with $\mathsf{bc}(\alpha_{1}.\ldots\alpha_{n})\cap\mathsf{fc}(B)=\emptyset$,
there exists an execution
$B\xrightarrow{[\alpha_{1}]^{\ell_{1}}}_{a}B_{1}\xrightarrow{[\alpha_{2}]^{\ell_{2}}}_{a}\ldots\xrightarrow{[\alpha_{n}]^{\ell_{n}}}_{a}B_{n}$
such that $\Phi(A_{i})\sim\Phi(B_{i})$ and
$\mathsf{skl}(A_{i})=\mathsf{skl}(B_{i})$ for any $1\leq i\leq n$.

##  4 Compression

Our first refinement of the semantics, which we call compression, is closely
related to focusing from proof theory [3]: we will assign a polarity to
processes and constrain the shape of executed traces based on those
polarities. This will provide a first significant reduction of the number of
traces to consider when checking reachability-based properties such as
secrecy, and more importantly, equivalence-based properties in the action-
deterministic case.

######  Definition 4.1.

A process $P$ is _positive_ if it is of the form $\mathtt{in}(c,x).Q$, and it
is _negative_ otherwise. A multiset of processes $\mathcal{P}$ is _initial_ if
it contains only positive or _replicated_ processes, _i.e.,_ of the form
$\mathbf{\large!}^{a}_{\vv{c},\vv{n}}Q$.

$\begin{array}[]{lcl}\mbox{\sc
Start/In}&&{(\mathcal{P}\uplus{\\{P\\}};\varnothing;\Phi)\xrightarrow{\;\mathtt{foc}(\mathtt{in}(c,M))\;}_{c}(\mathcal{P};P^{\prime};\Phi)\lx@proof@logical@and\mathcal{P}\text{
is
initial}(P;\Phi)\xrightarrow{\mathtt{in}(c,M)}_{a}(P^{\prime};\Phi)}\\\\[2.84526pt]
\mbox{\sc
Start/!}&&(\mathcal{P}\uplus{\\{\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P\\}};\varnothing;\Phi)\xrightarrow{\;\mathtt{foc}(\mathtt{sess}(a,\vv{c}))\;}_{c}(\mathcal{P}\uplus{\\{\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P\\}};Q;\Phi)\lx@proof@logical@and\mathcal{P}\text{
is
initial}(\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P;\Phi)\xrightarrow{\mathtt{sess}(a,\vv{c})}_{a}(\\{\mathbf{\large!}^{a}_{\vv{c},\vv{n}}P;Q\\};\Phi)\\\\[2.84526pt]
\mbox{\sc
Pos/In}&&(\mathcal{P};P;\Phi)\xrightarrow{\;\mathtt{in}(c,M)\;}_{c}(\mathcal{P};P^{\prime};\Phi)(P;\Phi)\xrightarrow{\mathtt{in}(c,M)}_{a}(P^{\prime};\Phi)\\\\[2.84526pt]
\mbox{{\sc
Neg}}&&(\mathcal{P}\uplus{\\{P\\}};\varnothing;\Phi)\xrightarrow{\;\alpha\;}_{c}(\mathcal{P}\uplus{\mathcal{P}^{\prime}};\varnothing;\Phi^{\prime})(P;\Phi)\xrightarrow{\alpha}_{a}(\mathcal{P}^{\prime};\Phi^{\prime})\\\\[2.84526pt]
\mbox{\sc
Release}&&{(\mathcal{P};[P]^{\ell};\Phi)\xrightarrow{\;[\mathtt{rel}]^{\ell}\;}_{c}(\mathcal{P}\uplus{\\{[P]^{\ell}\\}};\varnothing;\Phi)}\;\;\mbox{
when $P$\text{ is negative } }\end{array}$

Labels are implicitly set in the same way as in the annotated semantics. Neg
is made non-branching by imposing an arbitrary order on labelled skeletons of
available actions.

Figure 2: Compressed semantics

The compressed semantics (see Figure 2) is built upon the annotated semantics.
It constrains the traces to follow a particular strategy, alternating between
_negative_ and _positive_ phases. It uses enriched configurations of the form
$(\mathcal{P};F;\Phi)$ where $(\mathcal{P};\Phi)$ is a labelled configuration
and $F$ is either a process (signalling which process is under focus in the
positive phase) or $\varnothing$ (in the negative phase). The negative phase
lasts until the configuration is initial (_i.e.,_ unfocused with an initial
underlying multiset of processes) and in that phase we perform actions that
decompose negative non-replicated processes. This is done using the Neg rule,
in a completely deterministic way. When the configuration becomes initial, a
positive phase starts: we choose one process and start executing the actions
of that process (only inputs, possibly preceded by a new session) without the
ability to switch to another process of the multiset, until a negative
subprocess is released and we go back to the negative phase. The active
process in the positive phase is said to be _under focus_. Between any two
initial configurations, the compressed semantics executes a sequence of
actions, called _blocks_ , of the form
$\mathtt{foc}(\alpha).\mathsf{tr}^{+}.\mathtt{rel}.\mathsf{tr}^{-}$ where
$\mathsf{tr}^{+}$ is a (possibly empty) sequence of input actions, whereas
$\mathsf{tr}^{-}$ is a (possibly empty) sequence of $\mathtt{out}$,
$\mathtt{par}$, and $\mathtt{zero}$ actions. Note that, except for the choice
of recipes, the compressed semantics is completely non-branching when
executing a block. It may branch only when choosing which block to execute.

###  4.1 Reachability

We now formalise the relationship between traces of the compressed and
annotated semantics. In order to do so, we translate between configuration and
enriched configuration as follows:
$\lceil{(\mathcal{P};\Phi)}\rceil=(\mathcal{P};\varnothing;\Phi)$,
$\lfloor{(\mathcal{P};\varnothing;\Phi)}\rfloor=(\mathcal{P};\Phi)$ and
$\lfloor{(\mathcal{P};P;\Phi)}\rfloor=(\mathcal{P}\uplus{\\{P}\\};\Phi)$.

Similarly, we map compressed traces to annotated ones:
$\lfloor{\epsilon}\rfloor=\epsilon$,
$\lfloor{\mathtt{foc}(\alpha).\mathsf{tr}}\rfloor=\alpha.\lfloor{\mathsf{tr}}\rfloor$,
$\lfloor{\mathtt{rel}.\mathsf{tr}}\rfloor=\lfloor{\mathsf{tr}}\rfloor$ and
$\lfloor{\alpha.\mathsf{tr}}\rfloor=\alpha.\lfloor{\mathsf{tr}}\rfloor$
otherwise.

We observe that we can map any execution in the compressed semantics to an
execution in the annotated semantics. Indeed, a compressed execution is simply
an annotated execution with some annotations (_i.e.,_ $\mathtt{foc}$ and
$\mathtt{rel}$) indicating the start of a positive/negative phase.

######  Lemma 4.2.

For any configurations $A$, $A^{\prime}$ and $\mathsf{tr}$,
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$
implies
$\lfloor{A}\rfloor\xrightarrow{\lfloor{\mathsf{tr}}\rfloor}_{a}\lfloor{A^{\prime}}\rfloor$.

Going in the opposite direction is more involved. In general, mapping
annotated executions to compressed ones requires to reorder actions.
Compressed executions also force negative actions to be performed
unconditionally, which we compensate by considering complete executions of a
configuration, _i.e.,_ executions after which no more action can be performed
except possibly the ones that consist in unfolding a replication (_i.e.,_ rule
Repl). Inspired by the positive trunk argument of [29], we show the following
lemma.

######  Lemma 4.3.

Let $A$, $A^{\prime}$ be two configurations and $\mathsf{tr}$ be such that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\;\mathsf{tr}\;$}}}$}}_{a}A^{\prime}$
is complete. There exists a trace $\mathsf{tr}_{c}$, such that
$\lfloor{\mathsf{tr}_{c}}\rfloor$ can be obtained from $\mathsf{tr}$ by
swapping independent labelled actions, and
$\lceil{A}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{c}$}}}$}}_{c}\lceil{A^{\prime}}\rceil$.

######  Proof 4.4 (Proof sketch).

We proceed by induction on the length of a complete execution starting from
$A$. If $A$ is not initial, then we need to execute some negative action using
Neg: this action must be present somewhere in the complete execution, and we
can permute it with preceding actions using Lemma 3.3. If $A$ is initial, we
analyse the prefix of input and session actions and we extract a subsequence
of that prefix that corresponds to a full positive phase.

###  4.2 Equivalence

We now define compressed trace equivalence ($\approx_{c}$) and prove that it
coincides with $\approx$.

######  Definition 4.5.

Let $A$ and $B$ be two configurations. We say that $A\sqsubseteq_{c}B$ when,
for any
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$
such that $\mathsf{bc}(\mathsf{tr})\cap\mathsf{fc}(B)=\varnothing$, there
exists
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}B^{\prime}$
such that $\Phi(A^{\prime})\sim\Phi(B^{\prime})$. They are _compressed trace
equivalent_ , denoted $A\approx_{c}B$, if $A\sqsubseteq_{c}B$ and
$B\sqsubseteq_{c}A$.

Compressed trace equivalence can be more efficiently checked than regular
trace equivalence. Obviously, it explores less interleavings by relying on
$\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}$}}_{c}$
rather than
$\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}$}}$.
It also requires that traces of one process can be played exactly by the
other, including details such as non-observable actions, labels, and focusing
annotations. The subtleties shown in Example 3.4 are crucial for the
completeness of compressed equivalence w.r.t. regular equivalence. Since the
compressed semantics forces to perform available outputs before _e.g._ input
actions, some non-equivalences are only detected thanks to the labels and
detailed non-observable actions of our annotated semantics.

######  Theorem 4.6.

Let $A$ and $B$ be two action-deterministic configurations with
$\mathsf{skl}(A)=\mathsf{skl}(B)$. We have $A\approx B$ if, and only if,
$\lceil{A}\rceil\approx_{c}\lceil{B}\rceil$.

######  Proof 4.7 (Proof sketch).

($\Rightarrow$) Consider an execution
$\lceil{A}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$.
Using Lemma 4.2, we get
${A}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\lfloor{\mathsf{tr}}\rfloor$}}}$}}_{a}\lfloor{A^{\prime}}\rfloor$.
Then, Lemma 3.5 yields
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\lfloor{\mathsf{tr}}\rfloor$}}}$}}_{a}B^{\prime}$
for some $B^{\prime}$ such that
$\Phi(\lfloor{A^{\prime}}\rfloor)\sim\Phi(B^{\prime})$ and labelled skeletons
are equal all along the executions. Relying on those skeletons, we show that
positive/negative phases are synchronised, and thus
$\lceil{B}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}B^{\prime\prime}$
for some $B^{\prime\prime}$ with
$\lfloor{B^{\prime\prime}}\rfloor=B^{\prime}$.
($\Leftarrow$) Consider an execution
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}A^{\prime}$.
We first observe that it suffices to consider only complete executions there.
This allows us to get a compressed execution
$\lceil{A}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{c}$}}}$}}_{c}\lceil{A^{\prime}}\rceil$
by Lemma 4.3. Since $\lceil{A}\rceil\approx_{c}\lceil{B}\rceil$, there exists
$B^{\prime}$ such that
$\lceil{B}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{c}$}}}$}}_{c}B^{\prime}$
with $\Phi(\lceil{A^{\prime}}\rceil)\sim\Phi(B^{\prime})$. Thus we have
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\lfloor{\mathsf{tr}_{c}}\rfloor$}}}$}}_{a}\lfloor{B^{\prime}}\rfloor$
but also
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}\lfloor{B^{\prime}}\rfloor$
thanks to Lemma 3.3.

_Improper blocks._ Note that blocks of the form
$\mathtt{foc}(\alpha).\mathsf{tr}^{+}.\mathtt{rel}.\mathtt{zero}$ do not bring
any new information to the attacker. While it would be incorrect to fully
ignore such _improper_ blocks, we can show that it is sufficient to consider
them at the end of traces. We can thus consider a further optimised compressed
trace equivalence that only checks for proper traces, _i.e.,_ ones that have
at most one improper block and only at the end of trace. We have also shown
that this optimised compressed trace equivalence actually coincides with
${\approx_{c}}$.

##  5 Reduction

Our compressed semantics cuts down interleavings by using a simple focused
strategy. However, this semantics does not analyse data dependency that happen
when an input depends on an output, and is thus unable to exploit the
independency of blocks to reduce interleavings. We tackle this problem now.

######  Definition 5.1.

Two blocks $b_{1}$ and $b_{2}$ are _independent_ , written
$b_{1}\mathrel{\text{\textbardbl}}b_{2}$, when all labelled actions
$\alpha_{1}\in b_{1}$ and $\alpha_{2}\in b_{2}$ are independent. Otherwise
they are _dependent_ , written $b_{1}\rightleftharpoons b_{2}$.

Obviously, Lemma 3.3 tells us that independent blocks can be permuted in a
trace without affecting the executability and the result of executing that
trace. But this notion is not very strong since it considers fixed recipes,
which are irrelevant (in the end, only the derived messages matter) and can
easily introduce spurious dependencies. Thus we define a stronger notion of
equivalence over traces, which allows permutations of independent blocks but
also changes of recipes that preserve messages. During these permutations, we
will also require that traces remain plausible, which is defined as follows:
$\mathsf{tr}$ is plausible if for any input $\mathtt{in}(c,M)$ such that
$\mathsf{tr}=\mathsf{tr}_{0}.\mathtt{in}(c,M).\mathsf{tr}_{2}$ then
$M\in\mathcal{T}(\mathcal{W})$ where $\mathcal{W}$ is the set of all handles
occurring in $\mathsf{tr}_{0}$. Given a block $b$, _i.e._ a sequence of the
form $\mathtt{foc}(\alpha).\mathsf{tr}^{+}.\mathtt{rel}.\mathsf{tr}^{-}$, we
denote by $b^{+}$ (resp. $b^{-}$) the part of $b$ corresponding to the
positive (resp. negative) phase, _i.e.,_ $b^{+}=\alpha.\mathsf{tr}^{+}$ (resp.
$b^{-}=\mathsf{tr}^{-}$). We note $(b_{1}=_{\mathsf{E}}b_{2})\Phi$ when
$b_{1}^{+}\Phi=_{\mathsf{E}}b_{2}^{+}\Phi$ and $b_{1}^{-}=b_{2}^{-}$.

######  Definition 5.2.

Given a frame $\Phi$, the relation $\equiv_{\Phi}$ is the smallest equivalence
over plausible compressed traces such that
$\mathsf{tr}.b_{1}.b_{2}.\mathsf{tr}^{\prime}\equiv_{\Phi}\mathsf{tr}.b_{2}.b_{1}.\mathsf{tr}^{\prime}$
when $b_{1}\mathrel{\mathrel{\text{\textbardbl}}}b_{2}$, and
$\mathsf{tr}.b_{1}.\mathsf{tr}^{\prime}\equiv_{\Phi}\mathsf{tr}.b_{2}.\mathsf{tr}^{\prime}$
when $(b_{1}=_{\mathsf{E}}b_{2})\Phi$.

######  Lemma 5.3.

Let $A$ and $A^{\prime}$ be two initial configurations such that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$.
We have that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}^{\prime}$}}}$}}_{c}A^{\prime}$
for any $\mathsf{tr}^{\prime}\equiv_{\Phi(A^{\prime})}\mathsf{tr}$.

We now turn to defining our reduced semantics, which is going to avoid the
redundancies identified above by only executing specific representatives in
equivalence classes modulo $\equiv_{\Phi}$. More precisely, we shall only
execute minimal traces according to some order, which we now introduce. We
assume an order ${\prec}$ on blocks that is insensitive to recipes, and such
that independent blocks are always strictly ordered in one way or the other.
We finally define ${\prec_{\mathsf{lex}}}$ on compressed traces as the
lexicographic extension of ${\prec}$ on blocks.

In order to incrementally build representatives that are minimal with respect
to ${\prec_{\mathsf{lex}}}$, we define a predicate that expresses whether a
block $b$ should be _authorised_ after a given trace $\mathsf{tr}$.
Intuitively, this is the case only when, for any block $b^{\prime}\succ b$ in
$\mathsf{tr}$, dependencies forbid to swap $b$ and $b^{\prime}$. We define
this with recipe dependencies first, then quantify over all recipes to capture
message dependencies.

######  Definition 5.4.

A block $b$ is authorised after $\mathsf{tr}$, noted
${\mathsf{tr}\triangleright b}$, when $\mathsf{tr}=\epsilon$; or
$\mathsf{tr}=\mathsf{tr}_{0}.b_{0}$ and either (i) $b\rightleftharpoons b_{0}$
or (ii) $b\mathrel{\text{\textbardbl}}b_{0}$, $b_{0}\prec b$, and
${\mathsf{tr}_{0}\triangleright b}$.

We finally define
$\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}$}}_{r}$
as the least relation such that:

$\begin{array}[]{llcll}\mbox{\sc
Init}&\hbox{\multirowsetup$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\epsilon$}}}$}}_{r}A\phantom{(\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{r}}$}&&\mbox{\sc
Block}&\hbox{\multirowsetup$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}.b$}}}$}}_{r}A^{\prime}\lx@proof@logical@and
A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{r}(\mathcal{P};\varnothing;\Phi)(\mathcal{P};\varnothing;\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$b$}}}$}}_{c}A^{\prime}$}\\\
&&&\end{array}$

Our reduced semantics only applies to initial configurations: otherwise, no
block can be performed. This is not restrictive since we can, without loss of
generality, pre-execute non-observable and output actions that may occur at
top level.

###  5.1 Reachability

An easy induction on the compressed trace $\mathsf{tr}$ allows us to map an
execution w.r.t. the reduced semantics to an execution w.r.t. the compressed
semantics.

######  Lemma 5.5.

For any configurations $A$ and $A^{\prime}$,
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{r}A^{\prime}$
implies
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$.

Next, we show that our reduced semantics only explores specific
representatives. Given a frame $\Phi$, a plausible trace $\mathsf{tr}$ is
$\Phi$-minimal if it is minimal111 Note that minimal traces are not unique,
since only labelled skeletons are taken into account when comparing actions.
However, the redundancy induced by the choice of recipes is not a concern in
practice as it does not arise with the current constraint-based techniques for
deciding trace equivalence.  in its equivalence class modulo $\equiv_{\Phi}$.

######  Lemma 5.6.

Let $A$ be an initial configuration and
$A^{\prime}=(\mathcal{P};\varnothing;\Phi)$ be a configuration such that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$.
We have that $\mathsf{tr}$ is $\Phi$-minimal if, and only if,
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{r}A^{\prime}$.

######  Proof 5.7 (Proof sketch).

In order to relate minimality and executability in the reduced semantics, let
us say that a trace is _bad_ if it is of the form $\mathsf{tr}.b_{0}\ldots
b_{n}.b^{\prime}.\mathsf{tr}^{\prime}$ where $n\geq 0$, there exists a block
$b^{\prime\prime}$ such that $(b^{\prime\prime}=_{\mathsf{E}}b^{\prime})\Phi$,
we have $b_{i}\mathrel{\text{\textbardbl}}b^{\prime\prime}$ for all $i$, and
$b_{i}\prec b^{\prime\prime}\prec b_{0}$ for all $i>0$. This pattern is
directly inspired by the characterisation of lexicographic normal forms by
Anisimov and Knuth in trace monoids [4]. We note that a trace that can be
executed in the compressed semantics can also be executed in the reduced
semantics if, and only if, it is not bad. Since the badness of a trace allows
to swap $b^{\prime}$ before $b_{0}$, and thus obtain a smaller trace in the
class $\equiv_{\Phi}$, we show that a bad trace cannot be $\Phi$-minimal (and
conversely).

###  5.2 Equivalence

The reduced semantics induces an equivalence $\approx_{r}$ that we define
similarly to the compressed one, and we then establish its soundness and
completeness w.r.t. $\approx_{c}$.

######  Definition 5.8.

Let $A$ and $B$ be two configurations. We say that $A\sqsubseteq_{r}B$ when,
for every
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{r}A^{\prime}$
such that $\mathsf{bc}(\mathsf{tr})\cap\mathsf{fc}(B)=\varnothing$, there
exists
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{r}B^{\prime}$
such that $\Phi(A^{\prime})\sim\Phi(B^{\prime})$. They are _reduced trace
equivalent_ , denoted $A\approx_{r}B$, if $A\sqsubseteq_{r}B$ and
$B\sqsubseteq_{r}A$.

######  Theorem 5.9.

Let $A$ and $B$ be two initial, action-deterministic configurations.
$A\approx_{c}B\mbox{ if, and only if, }A\approx_{r}B$

######  Proof 5.10 (Proof sketch).

We first prove that $\mathsf{tr}\equiv_{\Phi}\mathsf{tr}^{\prime}$ iff
$\mathsf{tr}\equiv_{\Psi}\mathsf{tr}^{\prime}$ when $\Phi\sim\Psi$.
($\Rightarrow$) This implication is then an easy consequence of Lemma 5.6.
($\Leftarrow$) We start by showing that it suffices to consider a complete
execution
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$.
Since $A^{\prime}$ is initial, by taking $\mathsf{tr}_{m}$ to be a
$\Phi(A^{\prime})$-minimal trace associated to $\mathsf{tr}$, we obtain a
reduced execution of $A$ leading to $A^{\prime}$. Using our hypothesis
$A\approx_{r}B$, we obtain that
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{m}$}}}$}}_{r}B^{\prime}$
with corresponding relations over frames. We finally conclude that
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}B^{\prime}$
using Lemma 5.3 and the result stated above.

_Improper blocks._ Similarly as we did for the compressed semantics in Section
4, we can further restrict ${\approx_{r}}$ to only check proper traces (see
Appendix D).

##  6 Application

We have developed two successive refinements of the concrete semantics of our
process algebra, eventually obtaining a reduced semantics that achieves an
optimal elimination of redundant interleavings. However, the practical
usability of these semantics in algorithms for checking the equivalence of
replication-free processes is far from immediate: indeed, all of our semantics
are still infinitely branching, because each input may be fed with arbitrary
messages. We now discuss how existing decision procedures based on symbolic
execution [27, 15, 36, 11] can be modified to decide our optimised
equivalences rather than the regular one, before presenting our implementation
and experimental results.

###  6.1 Symbolic execution

Our compressed semantics can easily be used as a replacement of the regular
one, in any tool whose algorithm is based on a forward exploration of the set
of possible traces. This modification is very lightweight, and already brings
a significant optimisation. In order to make use of our final, reduced
semantics, we need to enter into the details of constraint solving. In
addition to imposing the compressed strategy, symbolic execution should be
modified to generate _dependency constraints_ in order to reflect the data
dependencies imposed by our predicate ${\mathsf{tr}\triangleright b}$.
Actually, the generation of dependency constraints can be done in a similar
way as shown in [6] (even if the class of processes considered in [6] is more
restrictive). We simply illustrate the effect of these dependency constraints
on a simple example.

######  Example 6.1.

We consider roles $R_{i}:=\mathtt{in}(c_{i},x).\mathtt{if}\ x=\mathsf{ok}\
\mathtt{then}\ \mathtt{out}(c_{i},\mathsf{ok})$ where $\mathsf{ok}$ is a
public constant, and then consider a parallel composition of $n$ such
processes: $P_{n}:=\Pi_{i=1}^{n}R_{i}$. Thanks to compression, we will only
consider traces made of blocks, and obtained a first exponential reduction of
the state space. Now, assume that our order prioritizes blocks on $c_{i}$
w.r.t. those on $c_{j}$ when $i<j$, and consider a trace starting with
$\mathtt{in}(c_{j},\cdot).\mathtt{out}(c_{j},w_{j})$. Trying to continue the
exploration with an input action on $c_{i}$ with $i<j$, the dependency
constraint added will impose that the recipe $R_{i}$ used to feed the input on
$c_{i}$ makes use of the previous output to derive $\mathsf{ok}$. Actually,
this dependency constraint will impose more than that. Indeed, imposing that
$R_{i}$ has to use $w_{j}$ is not very restrictive since in this example there
are many ways to rely on $w_{j}$ to derive $\mathsf{ok}$, _e.g._
$R_{i}=\mathsf{dec}(\mathsf{enc}(\mathsf{ok},w_{j}),w_{j})$ or even
$R_{i}=w_{j}$.

Actually, according to our reduced semantics, this step will be possible only
if the message stored in $w_{j}$ is mandatory to derive the message expected
in input on channel $c_{i}$. In this example, the conditional imposes that the
recipe $R_{i}$ leads to the message $\mathsf{ok}$ (at least to pursue in the
then branch), and even if there are many ways to derive $\mathsf{ok}$, in any
case the content of $w_{j}$ is not mandatory for that. Thus, on this simple
example, all the traces where the action $\mathtt{in}(c_{j},\cdot)$ is
performed after the block on $c_{j}$ with $i<j$ will not be explored thanks to
our reduction technique.

The constraint solver is then modified in a non-invasive way: dependency
constraints are used to dismiss configurations when it becomes obvious that
they cannot be satisfied. The modified verification algorithm may explore
symbolic traces that do not correspond to $\Phi$-minimal representatives (when
dependency constraints cannot be shown to be infeasible) but we will see that
this approach allows us to obtain a very effective optimisation. Note that,
because we may over-approximate dependency constraints, we must ensure that
constraint resolution prunes executions in a symmetrical fashion for both
processes being checked for equivalence.

######  Remark 6.2.

A subtle point about compression is that it actually enhances reduction in a
symbolic setting. Consider the process
$P=\mathtt{in}(c,x).\mathtt{out}(c,n_{1}).\mathtt{out}(c,n_{2})$ in parallel
with $Q=\mathtt{in}(c^{\prime},x)$. If ${\prec}$ gives priority to $Q$, then
$Q$ can only be scheduled after $P$ if its input message requires the
knowledge of one of the nonces $n_{1}$ and $n_{2}$ revealed by $P$. Thus we
have two symbolic interleavings, one of which is subject to a dependency
constraint. Now, we could have applied the ideas of reduction directly on
actions rather than blocks but we would have obtained three symbolic
interleavings, reflecting the fact that if the input on $c^{\prime}$ depends
on only the first output nonce, it should be scheduled before the second
output.

###  6.2 Experimental results

The optimisations developed in the present paper have been implemented,
following the above approach, in the official version of the state of the art
tool Apte [12]. We now report on experimental results; sources and
instructions for reproduction are available [25]. We only show examples in
which equivalence holds, because the time spent on inequivalent processes is
too sensitive to the order in which the (depth-first) exploration is
performed.

_Toy example._ We consider again our simple example described in Section 6.1.
We ran Apte on $P_{n}\approx P_{n}$ for $n=1$ to $22$, on a single 2.67GHz
Xeon core (memory is not relevant). We performed our tests on the reference
version and the versions optimised with the compressed and reduced semantics
respectively. The results are shown on the left graph of Figure 3, in
logarithmic scale: it confirms that each optimisation brings an exponential
speedup, as predicted by our theoretical analysis.

Figure 3: Impact of optimisations on toy example (left) and Denning-Sacco
(right).

_Denning-Sacco protocol._ We ran a similar benchmark, checking that Denning-
Sacco ensures strong secrecy in various scenarios. The protocol has three
roles and we added processes playing those roles in turn, starting with three
processes in parallel. The results are plotted on Figure 3. The fact that we
add one role out of three at each step explains the irregular growth in
verification time. We still observe an exponential speedup for each
optimisation.

_Practical impact._ Finally, we illustrate how our optimisations make Apte
much more useful in practice for investigating interesting scenarios.
Verifying a single session of a protocol brings little assurance into its
security. In order to detect replay attacks and to allow the attacker to
compare messages that are exchanged, at least two sessions should be
considered. This means having at least four parallel processes for two-party
protocols, and six when a trusted third party is involved. This is actually
beyond what the unoptimised Apte can handle in a reasonable amount of time. We
show below how many parallel processes could be handled in $20$ hours by the
different versions of Apte on various use cases of protocols.

Protocol |  ref |  comp |  red | Protocol |  ref |  comp |  red
---|---|---|---|---|---|---|---
Needham Schroeder (3-party) |  4 |  6 |  7 | Denning-Sacco (3-party) |  5 |  9 |  10
Private Authent. (2-party) |  4 |  7 |  7 | WMF (3-party) |  6 |  12 |  13
Yahalom (3-party) |  4 |  5 |  5 | E-Passport PA (2-party) |  4 |  7 |  9

##  7 Related Work

The techniques we have presented borrow from standard ideas from concurrency
theory, trace theory and, perhaps more surprisingly, proof theory. Blending
all these ingredients, and adapting them to the demanding framework of
security protocols, we have come up with partial order reduction techniques
that can effectively be used in symbolic verification algorithms for
equivalence properties of security protocols. We now discuss related work, and
there is a lot of it given the huge success of POR techniques in various
application areas. We shall focus on the novel aspects of our approach, and
explain why such techniques have not been needed outside of security protocol
analysis. These observations are not new: as pointed out by Baier and Katoen
[7], “[POR] is mainly appropriate to control-intensive applications and less
suited for data-intensive applications”; Clarke _et al._ [13] also remark that
“In the domain of model checking of reactive systems, there are numerous
techniques for reducing the state space of the system. One such technique is
partial-order reduction. This technique does not directly apply to [security
protocol analysis] because we explicitly keep track of knowledge of various
agents, and our logic can refer to this knowledge in a meaningful way.”

We first compare our work with classical POR techniques. Then, we discuss more
specifically previous works that use POR in a symbolic execution setting, and
comment on previous work in the domain of security protocol analysis. We
conclude the section with some remarks on the relationship between our
optimized semantics and focused proof systems.

###  7.1 Classical POR

Partial order reduction techniques have proved very useful in the domain of
model checking concurrent programs. Given a Labelled Transition System (LTS)
and some property to check (_e.g.,_ a Linear Temporal Logic formula), the
basic idea of POR [31, 24, 7] is to only consider a reduced version of the
given LTS whose enable transitions of some states might be not exhaustive but
are such that this transformation does not affect the property. POR techniques
can be categorized in two groups [24]. First, the persistent set techniques
(_e.g.,_ stubborn sets, ample sets) where only a sufficiently representative
subset of available transitions is explored. Second, sleep set techniques
memoize past exploration and use this information along with available
transitions to disable some provably redundant transitions. Note that these
two kinds of techniques are compatible, and are indeed often combined to
obtain better reductions. Theoretical POR techniques apply to transition
systems which may not be explicitly available in practice, or whose explicit
computation may be too costly. In such cases, POR is often applied to an
approximation of the LTS that is obtained through static analysis. Another,
more recent approach is to use _dynamic POR_ [20, 34, 2] where the POR
arguments are applied based on information that is obtained during the
execution of the system.

Clearly, classical POR techniques would apply to our concrete LTS, but that
would not be practically useful since this LTS is wildly infinite, taking into
account all recipes that the attacker could build. Applying most classical POR
techniques to the LTS from which data would have been abstracted away would be
ineffective: any input would be dependent with any output (since the
attacker’s knowledge, increased by the output, may enable new input messages).
Our compression technique lies between these two extremes. It exploits a semi-
commutation property: outputs can be permuted before inputs, but not the
converse in general. Further, it exploits the fact that inputs do not increase
the attacker’s knowledge, and can thus be executed in a chained fashion, under
focus. The semi-commutation is reminiscent of the asymmetrical dependency
analysis enabled by the _conditional_ stubborn set technique [24], and the
execution of inputs under focus may be explained by means of sleep sets. While
it may be possible to formally derive our compressed semantics by
instantiating abstract POR techniques to our setting, we have not explored
this possibility in detail222 Although this would be an interesting question,
we do not expect that any improvement of compression would come out of it.
Indeed, compression can be argued to be maximal in terms of eliminating
redundant traces without analyzing data: for any compressed trace there is a
way to choose messages and modify tests to obtain a concrete execution which
does not belong to the equivalence class of any other compressed trace. . As
mentioned earlier, the compressed semantics is inspired from another
technique, namely focusing [3] from proof theory. Concerning our reduced
semantics, it may be seen as an application of the sleep set technique (or
even as a reformulation of Anisimov’s and Knuth’s characterization of
lexicographic normal forms) but the real contribution with this technique is
to have formulated it in such a way that it can be implemented without
requiring an _a priori_ knowledge of data dependencies: it allows us to
eliminate redundant traces on-the-fly as data (in)dependency is discovered by
the constraint resolution procedure (more on this in the next sections) — in
this sense, it may be viewed as a case of dynamic POR.

Narrowing the discussion a bit more, we now focus on the fact that our
techniques are designed for the verification of equivalence properties. This
requirement turns several seemingly trivial observations into subtle technical
problems. For instance, ideas akin to compression are often applied without
justification (_e.g.,_ in [32, 34, 30]) because they are obvious when one does
reachability rather than equivalence checking. To understand this, it is
important to distinguish between two very different ways of applying POR to
equivalence checking (independently of the precise equivalence under
consideration). The first approach is to reduce a system such that the reduced
system and the original systems are equivalent. In the second approach, one
only requires that two reduced systems are equivalent iff the original systems
are equivalent. The first approach seems to be more common in the POR
litterature (where one finds, _e.g.,_ reductions that preserve LTL-
satisfiability [7] or bisimilarity [26]) though there are instances of the
second approach (_e.g.,_ for Petri nets [23]). In the present work, we follow
the second approach: neither of our two reduction techniques preserves trace
equivalence. This allows stronger reductions but requires extra care: one has
to ensure that the independencies used in the reduction of one process are
also meaningful for the other processes; in other words, reduction has to be
symmetrical. This is the purpose of our annotated semantics and its “strong
symmetry lemma” (Lemma 3.5) but also, for the reduced semantics, of Lemma 5.6
and Proposition C.4. We come back to these two different approaches later,
when discussing specific POR techniques for security.

###  7.2 Infinite data and symbolic execution

Symbolic execution is often used to verify systems dealing with infinite data,
_e.g.,_ recipes and messages in security; integers, list, etc. in program
verification. In many works combining POR and symbolic executions (_e.g.,_
[32, 33, 34]) the detection of redundant explorations does not rely on the
data, and can thus be done trivially at the level of symbolic executions. In
such cases, POR and symbolic execution are orthogonal. For instance, in [32],
two actions are _data-dependent_ if one actions is a send action of some
message $m$ to some process $p$ and the other is a receive action of process
$p$. This is done independently of $m$, which is meaningful when one considers
internal reduction (as is the case that work) but would be too coarse when one
considers labelled transitions representing interactions with an environment
that may construct arbitrary recipes from previous outputs (as is the case in
our work). Due to this omnipotent attacker, POR techniques cannot be effective
in our setting unless they really take data into account. Further, due to the
infinite nature of data, and the dynamic extension of the attacker’s
knowledge, POR and symbolic execution must be integrated rather than
orthogonal. Our notion of independence and trace monoid are tailored to take
all this into account, including at the level of trace equivalence (cf. again
Lemma 5.6). And, although reduction is presented (Section 5) in the concrete
semantics, the crucial point is that the authorised predicate (Definition 5.4)
is implemented as a special _dependency_ constraint (Section 6) so that our
POR algorithm fundamentally relies on symbolic execution. We have not seen
such uses of POR outside of the security applications mentioned next [30, 6].

###  7.3 Security applications

The idea of applying POR to the verification of security protocols dates back,
at least, to the work of Clarke _et al._ [13, 14]. In this work, the authors
remark that traditional POR techniques cannot be directly applied to security
mainly because “[they] must keep track of knowledge of various agents” and
“[their] logic can refer to this knowledge in a meaningful way”. This led them
to define a notion of semi-invisible actions (output actions, that cannot be
swapped after inputs but only before them) and design a reduction that
prioritizes outputs and performs them in a fixed order. Compared to our work,
this reduction is much weaker (even weaker than compression only), only
handles a finite set of messages, and only focuses on reachability properties
checking.

In [19], the authors develop “state space reduction” techniques for the Maude-
NRL Protocol Analyzer (Maude-NPA). This tool proceeds by backwards
reachability analysis and treats at the same level the exploration of protocol
executions and attacker’s deductions. Several reductions techniques are
specific to this setting, and most are unrelated to partial order reduction in
general, and to our work in particular. We note that the lazy intruder
techniques from [19] should be compared to what is done in constraint
resolution procedures (_e.g.,_ the one used in Apte) rather than to our work.
A simple POR technique used in Maude-NPA is based on the observation that
inputs can be executed in priority in the backwards exploration, which
corresponds to the fact that we can execute outputs first in forward
explorations. We note again that this is only one aspect of the focused
strategy, and that it is not trivial to lift this observation from
reachability to trace equivalence. Finally, a “transition subsumption”
technique is described for Maude-NPA. While highly non-trivial due to the
technicalities of the model, this is essentially a tabling technique rather
than a partial order reduction. Though it does yield a significant state space
reduction (as shown in the experiments [19]) it falls short of exploiting
independencies fully, and has a potentially high computational cost (which is
not evaluated in the benchmarks of [19]).

In [21], Fokkink et al. model security protocols as labeled transition systems
whose states contain the control points of different agents as well as
previously outputted messages. They devise some POR technique for these
transition systems, where output actions are prioritized and performed in a
fixed order. In their work, the original and reduced systems are trace
equivalent modulo outputs (the same traces can be found after removing output
actions). The justification for their reduction would fail in our setting,
where we consider standard trace equivalence with observable outputs. More
importantly, their requirement that a reduced system should be equivalent to
the original one makes it impossible to swap input actions, and thus
reductions such as the execution under focus of our compressed semantics
cannot be used. The authors leave as future work the problem of combining
their algorithm with symbolic executions, in order to be able to lift the
restriction to a finite number of messages.

Cremers and Mauw proposed [16] a reduction technique based on the sleep set
idea. Basically, when their exploration algorithm chooses to explore a
specific action (an output or an input with its corresponding message), it
will also add all the other available actions that have priority over the
chosen one to the current sleep set. An action in this sleep set will never
been explored. In this work, only reachability property are considered, and
the reduction cannot be directly applied to trace equivalence checking. More
importantly, the technique can only handle a finite set of messages. The
authors identify as important future work the need to lift their method to the
symbolic setting.

Earlier work by Mödersheim et al. has shown how to combine POR technique with
symbolic semantics [30] in the context of reachability properties for security
protocols, which has led to high efficiency gains in the OFMC tool of the
AVISPA platform [5]. While their reduction is very limited, it brings some key
insight on how POR may be combined with symbolic execution. In a model where
actions are sequences of outputs followed by inputs, their reduction imposes a
_differentiation_ constraint on the interleavings of
$\mathtt{in}(c,x).\mathtt{out}(c,m)\leavevmode\nobreak\ |\leavevmode\nobreak\
\mathtt{in}(d,y).\mathtt{out}(d,m^{\prime})$. This constraint enforces that
the symbolic interleaving
${\mathtt{in}(d,M^{\prime}).\mathtt{out}(d,w^{\prime}).\mathtt{in}(c,M).\mathtt{out}(c,w)}$
should only be explored for instances of $M$ that depend on $w^{\prime}$. Our
reduced semantics constrains patterns of arbitrary size (instead of just size
2 diamond patterns as above) by means of the authorised predicate (Definition
5.4). Moreover, our POR technique has beed designed to be sound and complete
for trace equivalence checking as well.

In a previous work [6], we settled the general ideas for the POR techniques
presented in the present paper, but results were much weaker. That earlier
work only dealt with the restrictive class of _simple processes_ , which does
not feature nested parallel composition or replication, and made heavy use of
specific properties of processes of that class to define reductions and prove
them correct. In the present work, we show that our two reduction techniques
apply to a very large class of processes for reachability checking. For
equivalence checking, we only require the semantic condition of action-
determinism. Note that the results of the present paper are conservative over
those of [6]: the reductions of [6] are obtained as a particular case of the
results presented here in the case of simple processes. Finally, the present
work brings a solid implementation in the state of the art tool Apte [10],
whereas [6] did not present experimental results — it mentioned a preliminary
implementation, extending SPEC, which we abandoned since it was difficult to
justify and handled a more restricted class than APTE.

###  7.4 Relationship with focused proof systems

The reader familiar with focused proof systems [3] will have recognized the
strong similarities with our compressed semantics. The strategies are
structured in the same way, around positive and negative phases. More deeply,
the compressed semantics can actually be derived systematically from the
focused proof system of linear logic, through an encoding of our processes
into linear logic formulas (such that proof search corresponds to process
executions). There are several such encodings in the literature, see for
instance [28, 22, 18]. We do not provide here a fully worked-out encoding
appropriate for our protocols. It is not trivial, notably due to the need to
encode the attacker’s knowledge, and internal reductions of protocols — both
features require slight extensions of the usual linear logic framework. We
have thus chosen to only take the correspondence with linear logic as an
intuitive guide, and give a self-contained (and simple) proof of completeness
for our compressed semantics by adapting the positive trunk argument of [29].
Note that the strong analogies with proof theory only hold for reachability
results, _i.e.,_ up to Lemma 4.3. It is a contribution of this paper to
observe that focusing (compression) makes sense beyond reachability, at the
level of trace equivalence: Theorem 4.6 (stating that trace equivalence
coincides with compressed trace equivalence for action-deterministic
processes) has no analogue in the proof theoretical setting, where trace
equivalence itself is meaningless.

We motivated reduction by observing that (in)dependencies between blocks of
the compressed semantics should be exploited to eliminate redundant
interleavings. This same observation has been done in the context of linear
logic focusing, and lead to the idea of multi-focusing [9] where independent
synthetic connectives (the analogue of our blocks) are executed simultaneously
as much as possible. That work on multi-focusing is purely theoretical, and it
is unclear how multi-focusing could be applied effectively in proof search. It
would be interesting to consider whether the gradual construction of unique
representatives in our reduced semantics could be extended to the richer
setting of linear logic (where proof search branches, unlike process
executions).

##  8 Conclusion

We have developed two POR techniques that are adequate for verifying
reachability and trace equivalence properties of action-deterministic security
protocols. We have effectively implemented them in Apte, and shown that they
yield the expected, significant benefit.

We are considering several directions for future work. Regarding the
theoretical results presented here, the main question is whether we can get
rid of the action-determinism condition without degrading our reductions too
much. Regarding the practical application of our results, we can certainly go
further. We first note that our compression technique should be applicable and
useful in other verification tools, not necessarily based on symbolic
execution. Next, we could investigate the role of the particular choice of the
order $\prec$, to determine heuristics for maximising the practical impact of
reduction. Finally, we plan to adapt our treatment of replication to bounded
replication to obtain a first symmetry elimination scheme, which should
provide a significant optimisation when studying security protocols with
several sessions.

## References

  * [1] M. Abadi and C. Fournet.  Mobile values, new names, and secure communication.  In Proceedings of POPL’01. ACM Press, 2001.
  * [2] Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas.  Optimal dynamic partial order reduction.  ACM SIGPLAN Notices, 49(1):373–384, 2014.
  * [3] Jean-Marc Andreoli.  Logic programming with focusing proofs in linear logic.  J. Log. Comput., 2(3), 1992.
  * [4] A.V. Anisimov and D.E. Knuth.  Inhomogeneous sorting.  International Journal of Computer & Information Sciences, 8(4):255–260, 1979.
  * [5] A. Armando et al.  The AVISPA Tool for the automated validation of internet security protocols and applications.  In Proc. 17th Int. Conference on Computer Aided Verification (CAV’05), LNCS. Springer, 2005.
  * [6] David Baelde, Stéphanie Delaune, and Lucca Hirschi.  A reduced semantics for deciding trace equivalence using constraint systems.  In Proceedings of POST’14. Springer, 2014.
  * [7] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking (Representation and Mind Series).  The MIT Press, 2008.
  * [8] Mayla Bruso, K. Chatzikokolakis, and J. den Hartog.  Formal verification of privacy for RFID systems.  In Proceedings of CSF’10, 2010.
  * [9] Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin.  Canonical sequent proofs via multi-focusing.  In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and C.-H. Luke Ong, editors, Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy, volume 273 of IFIP, pages 383–396. Springer, 2008.
  * [10] Vincent Cheval.  Apte: an algorithm for proving trace equivalence.  In Proceedings TACAS’14. Springer, 2014.
  * [11] Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune.  Trace equivalence decision: Negative tests and non-determinism.  In Proceedings of CCS’11. ACM Press, 2011.
  * [12] Vincent Cheval and Lucca Hirschi.  sources of APTE, 2015.  Available at https://github.com/APTE/APTE.
  * [13] Edmund Clarke, Somesh Jha, and Will Marrero.  Partial order reductions for security protocol verification.  In Tools and Algorithms for the Construction and Analysis of Systems, pages 503–518. Springer, 2000.
  * [14] Edmund M. Clarke, Somesh Jha, and Wilfredo R. Marrero.  Efficient verification of security protocols using partial-order reductions.  International Journal on Software Tools for Technology Transfer, 4(2), 2003.
  * [15] H. Comon-Lundh, V. Cortier, and E. Zalinescu.  Deciding security properties for cryptographic protocols. Application to key cycles.  ACM Transactions on Computational Logic (TOCL), 11(4), 2010.
  * [16] Cas JF Cremers and Sjouke Mauw.  Checking secrecy by means of partial order reduction.  In System Analysis and Modeling. Springer, 2005.
  * [17] Stéphanie Delaune, Steve Kremer, and Mark D. Ryan.  Verifying privacy-type properties of electronic voting protocols: A taster.  In Towards Trustworthy Elections – New Directions in Electronic Voting, volume 6000. Springer, 2010.
  * [18] Yuxin Deng, Iliano Cervesato, and Robert J. Simmons.  Relating reasoning methodologies in linear logic and process algebra.  In LINEARITY, volume 101 of EPTCS, 2012.
  * [19] Santiago Escobar, Catherine Meadows, José Meseguer, and Sonia Santiago.  State space reduction in the maude-nrl protocol analyzer.  Inf. Comput., 238:157–186, 2014.
  * [20] Cormac Flanagan and Patrice Godefroid.  Dynamic partial-order reduction for model checking software.  In ACM Sigplan Notices, volume 40, pages 110–121. ACM, 2005.
  * [21] Wan Fokkink, Mohammad Torabi Dashti, and Anton Wijs.  Partial order reduction for branching security protocols.  In Proceedings of ACSD’10. IEEE, 2010.
  * [22] Deepak Garg and Frank Pfenning.  Type-directed concurrency.  In CONCUR, volume 3653 of Lecture Notes in Computer Science. Springer, 2005.
  * [23] Patrice Godefroid.  Using partial orders to improve automatic verification methods.  In Computer-Aided Verification, pages 176–185. Springer Berlin Heidelberg, 1991.
  * [24] Patrice Godefroid, J van Leeuwen, J Hartmanis, G Goos, and Pierre Wolper.  Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem, volume 1032.  Springer Heidelberg, 1996.
  * [25] Lucca Hirschi.  APTE with POR, 2015.  Available at http://www.lsv.ens-cachan.fr/~hirschi/apte_por.
  * [26] Michaela Huhn, Peter Niebert, and Heike Wehrheim.  Partial order reductions for bisimulation checking.  In Vikraman Arvind and Ramaswamy Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science, 18th Conference, Chennai, India, December 17-19, 1998, Proceedings, volume 1530 of Lecture Notes in Computer Science, pages 271–282. Springer, 1998.
  * [27] J. Millen and V. Shmatikov.  Constraint solving for bounded-process cryptographic protocol analysis.  In Proceedings of CCS’01. ACM Press, 2001.
  * [28] Dale Miller.  Encryption as an abstract data type.  Electr. Notes Theor. Comput. Sci., 84, 2003.
  * [29] Dale Miller and Alexis Saurin.  From proofs to focused proofs: A modular proof of focalization in linear logic.  In Proceedings of CSL’07, volume 4646. Springer, 2007.
  * [30] Sebastian Mödersheim, Luca Viganò, and David A. Basin.  Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols.  Journal of Computer Security, 18(4), 2010.
  * [31] Doron Peled.  Ten years of partial order reduction.  In Proceedings of CAV’98, volume 1427. Springer, 1998.
  * [32] Koushik Sen and Gul Agha.  Automated systematic testing of open distributed programs.  In Fundamental Approaches to Software Engineering, pages 339–356. Springer, 2006.
  * [33] Stephen F Siegel, Anastasia Mironova, George S Avrunin, and Lori A Clarke.  Using model checking with symbolic execution to verify parallel numerical programs.  In Proceedings of the 2006 international symposium on Software testing and analysis, pages 157–168. ACM, 2006.
  * [34] Samira Tasharofi, Rajesh K Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, and Gul Agha.  Transdpor: A novel dynamic partial-order reduction technique for testing actor programs.  In Formal Techniques for Distributed Systems, pages 219–234. Springer, 2012.
  * [35] Alwen Tiu.  Spec: http://users.cecs.anu.edu.au/~tiu/spec/, 2010.
  * [36] Alwen Tiu and Jeremy E. Dawson.  Automating open bisimulation checking for the spi calculus.  In Proceedings of CSF’10. IEEE Computer Society Press, 2010.

##  Appendix A Annotated semantics

###  A.1 Reachability

######  Proposition A.1.

Well labelling is preserved by
$\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}$}}_{a}$.

######  Proof A.2.

For all transitions except Par and Repl, the multiset of labels of the
resulting configuration is a subset of labels of the original configuration.
Thus, well labelling is obviously preserved in those cases.

Consider now a Par transition, represented below without the permutation,
which does not play a role here:

$([\\{\Pi_{i=1}^{n}P_{i}\\}]^{\ell}\\}\uplus\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\mathtt{par}(\sigma_{1},\ldots,\sigma_{n})]^{\ell}$}}}$}}(\\{[P_{1}]^{\ell\cdot
1},\ldots,[P_{n}]^{\ell\cdot n}\\}\uplus\mathcal{P};\Phi)$

We check that labels are pairwise independent. This is obviously the case for
the new labels $\ell\cdot i$. Let us now consider a label $\ell^{\prime}$ from
$\mathcal{P}$ and show that it is independent from any $\ell\cdot i$. It
cannot be equal to one of them (otherwise it would be a suffix of $\ell$,
which contradicts the well labelling of the initial configuration) and it
cannot be a strict prefix either (otherwise it would be a prefix of $\ell$
too). Finally, $\ell\cdot i$ cannot be a prefix of $\ell^{\prime}$ because
$\ell$ is not a prefix of $\ell^{\prime}$.

As far as labels are concerned, Repl transitions are a particular case of Par
where there are only two sub-processes. Thus Repl preserves well labelling.

######  Lemma (3.3).

Let $A$ be a (well labelled) configuration, $\alpha$ and $\beta$ be two
independent labelled actions. We have
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\alpha.\beta$}}}$}}_{a}A^{\prime}$
if, and only if,
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\beta.\alpha$}}}$}}_{a}A^{\prime}$.

######  Proof A.3.

By symmetry it is sufficient to show one implication. Assuming $\ell_{1}$ and
$\ell_{2}$ to be independent, we consider a transition labelled
$\alpha=[\alpha^{\prime}]^{\ell_{1}}$ followed by one labelled
$\beta=[\beta^{\prime}]^{\ell_{2}}$. We first observe that a transition
labelled $\ell_{1}$ can only generate new labels that are dependent with
$\ell_{1}$. Thus, $\ell_{2}$ must be present in the original configuration and
our execution is of the following form, where we write $P_{\alpha}$ (resp.
$P_{\beta}$) instead of $[P_{\alpha}]^{\ell_{1}}$ (resp.
$[P_{\beta}]^{\ell_{2}}$):

$A=(\mathcal{P}\uplus\\{P_{\alpha},P_{\beta}\\};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha]^{\ell_{1}}$}}}$}}(\mathcal{P}\uplus\mathcal{P}_{\alpha}\uplus\\{P_{\beta}\\};\Phi_{\alpha})\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\beta]^{\ell_{2}}$}}}$}}(\mathcal{P}\uplus\mathcal{P}_{\alpha}\uplus\mathcal{P}_{\beta};\Phi_{\beta})$

It remains to check that $\beta$ can be performed by $P_{\beta}$ in the
original configuration, and that doing so would not prevent the $\alpha$
transition to happen next. The only thing that could prevent $\beta$ from
being performed is that the frames $\Phi$ and $\Phi_{\alpha}$ may be
different, in the case where $\alpha$ is an input. In that case, the recipe
independence hypothesis guarantees that $\beta$ does not rely on the new
handle introduced by $\alpha$ and can thus be played with only $\Phi$.
Finally, performing $\alpha$ after $\beta$ is easy. We only detail the case
where $\beta=\mathtt{out}(c,w)$ and $\alpha$ is an input of recipe $M$. In
that case we have $\Phi_{\alpha}=\Phi$,
$\Phi_{\beta}=\Phi_{\alpha}\uplus\\{w\mapsto m\\}$, and
$M\in\mathcal{T}(\mathrm{dom}(\Phi))$. We observe that
$M\in\mathcal{T}(\mathrm{dom}(\Phi_{\beta}))$ and we construct the execution:

$A=(\mathcal{P}\uplus\\{[P_{\alpha}]^{\ell_{1}},[P_{\beta}]^{\ell_{2}}\\};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\beta]^{\ell_{2}}$}}}$}}(\mathcal{P}\uplus\mathcal{P}_{\beta}\uplus\\{[P_{\alpha}]^{\ell_{1}}\\};\Phi_{\beta})\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha]^{\ell_{1}}$}}}$}}(\mathcal{P}\uplus\mathcal{P}_{\alpha}\uplus\mathcal{P}_{\beta};\Phi_{\beta})$

###  A.2 Equivalence

######  Definition A.4.

Given a process $P$, we define the set of its enabled skeletons as

$\mathsf{enable}(P)=\begin{cases}\\{\mathsf{sk}(P)\\}&\text{if $P$ starts with
an observable action}\\\ \cup_{i}\\{\mathsf{sk}(P_{i})\\}&\text{if
$P=\Pi_{i}P_{i}$}\\\ \emptyset&\text{if $P=0$}\\\ \end{cases}$

We may consider skeletons, labelled skeletons and enabled skeletons of a
configuration by taking the set of the corresponding objects of all its
processes.

######  Property A.5.

For any configurations $A$, $A^{\prime}$ and non-observable action $\alpha$,
if
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\alpha$}}}$}}_{a}A^{\prime}$
or
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\tau$}}}$}}A^{\prime}$
then $\mathsf{enable}(A)=\mathsf{enable}(A^{\prime})$.

######  Property A.6.

Let $A$ be an action-deterministic configuration and $P$, $Q$ two of its
processes. We have that $\mathsf{enable}(P)\cap\mathsf{enable}(Q)=\emptyset$.

######  Lemma A.7.

Let $A$ be an action-deterministic configuration. If
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{1}$}}}$}}A_{1}$
and
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{2}$}}}$}}A_{2}$
for some traces $\mathsf{tr}_{1},\mathsf{tr}_{2}$ such that
$\mathsf{obs}(\mathsf{tr}_{1})=\mathsf{obs}(\mathsf{tr}_{2})$ then
$\mathsf{enable}(A_{1})=\mathsf{enable}(A_{2})$ and $\Phi(A_{1})=\Phi(A_{2})$.

######  Proof A.8.

We first prove a stronger result when the configurations $A_{1}$ and $A_{2}$
are _canonical_ , _i.e._ only contain processes that are neither $0$ nor a
parallel composition. Actually, in such a case, we prove that $A_{1}=A_{2}$.

To prove this intermediate result, we proceed by induction on
$\mathsf{obs}(\mathsf{tr}_{1})$. The base case is trivial. Let us show the
inductive case. We assume that
$\mathsf{tr}_{1}=\mathsf{tr}_{1}^{0}.\alpha.\mathsf{tr}^{-}_{1}$ with $\alpha$
an observable action and $\mathsf{tr}_{1}^{-}$ containing only non-observable
actions. Since $\mathsf{obs}(\mathsf{tr}_{1})=\mathsf{obs}(\mathsf{tr}_{2})$,
we have that $\mathsf{tr}_{2}=\mathsf{tr}_{2}^{0}.\alpha.\mathsf{tr}^{-}_{2}$
with $\mathsf{tr}_{2}^{-}$ containing only non-observable actions and
$\mathsf{obs}(\mathsf{tr}_{1}^{0})=\mathsf{obs}(\mathsf{tr}_{2}^{0})$. Our
given executions are thus of the form:

$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{1}^{0}$}}}$}}A^{0}_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\alpha.\mathsf{tr}_{1}^{-}$}}}$}}A_{1}\text{
and
}A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{2}^{0}$}}}$}}A^{0}_{2}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\alpha.\mathsf{tr}_{2}^{-}$}}}$}}A_{2}$

It may be the case that $A_{1}^{0}$ or $A_{2}^{0}$ are not canonical. The idea
is to reorder some non-observable actions. More precisely, we perform all
available non-observable actions of $A^{0}_{1}$ and $A^{0}_{2}$ before
performing $\alpha$. By doing this, we do not change the observable actions of
the different sub-traces and obtain

$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{1}^{0}.\mathsf{tr}_{3}^{-}$}}}$}}A^{\prime
0}_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\alpha.\mathsf{tr}^{\prime-}_{1}$}}}$}}A_{1}\text{
and
}A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{2}^{0}.\mathsf{tr}_{4}^{-}$}}}$}}A^{\prime
0}_{2}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\alpha.\mathsf{tr}^{\prime-}_{2}$}}}$}}A_{2}$

with $A^{\prime 0}_{1}$ and $A^{\prime 0}_{2}$ canonical. By inductive
hypothesis, we have that $A^{\prime 0}_{1}=A^{\prime 0}_{2}$. We now must show
$A_{1}=A_{2}$. By action-determinism of $A$, there is only one process $P$
that can perform $\alpha$ in $A^{\prime 0}_{1}(=A^{\prime 0}_{2})$. The
resulting process $P^{\prime}$ after performing $\alpha$ is thus the same in
the two executions. Since $A_{1}$ and $A_{2}$ are canonical and
$\mathsf{tr}^{\prime-}_{1}$ and $\mathsf{tr}^{\prime-}_{2}$ contain only non-
observable actions, $A_{1}=A_{2}$.

In order to be able to apply our previous result, we complete the executions
with all available non-observable actions:

$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{1}$}}}$}}A_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{1}^{-}$}}}$}}A_{1}^{\prime}$
and
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{2}$}}}$}}A_{2}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{1}^{-}$}}}$}}A_{2}^{\prime}$

such that $A_{1}$ and $A_{2}$ are canonical and $\mathsf{tr}^{-}_{1}$ and
$\mathsf{tr}^{-}_{2}$ contain only non-observable actions. We also have that:

  * •

$\Phi(A_{1})=\Phi(A^{\prime}_{1})$ and
$\mathsf{enable}(A_{1})=\mathsf{enable}(A^{\prime}_{1})$; and

  * •

$\Phi(A_{2})=\Phi(A^{\prime}_{2})$ and
$\mathsf{enable}(A_{2})=\mathsf{enable}(A^{\prime}_{2})$.

We now conclude thanks to our previous result, and obtain
$A^{\prime}_{1}=A^{\prime}_{2}$ implying the desired equalities.

######  Proposition A.9.

Let $A$ and $B$ be two action-deterministic configurations such that $A\approx
B$. If
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{A}$}}}$}}A^{\prime}$
and
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{B}$}}}$}}B^{\prime}$
with $\mathsf{obs}(\mathsf{tr}_{A})=\mathsf{obs}(\mathsf{tr}_{B})$ then
$\Phi(A^{\prime})\sim\Phi(B^{\prime})$ and
$\mathsf{enable}(A^{\prime})=\mathsf{enable}(B^{\prime})$.

######  Proof A.10.

By hypothesis, we know that $A\approx B$, and also that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{A}$}}}$}}A^{\prime}$.
Moreover, the freshness conditions on channels (_i.e.,_
$\mathsf{bc}(\mathsf{tr}_{A})\cap\mathsf{fc}(B)=\emptyset$) holds as $B$ is
able to perform $\mathsf{tr}_{B}$, and $\mathsf{tr}_{A}$ and $\mathsf{tr}_{B}$
share the same bound channels. Hence, we know that there exist
$\mathsf{tr}^{\prime}_{B}$ and $B^{\prime\prime}$ such that

$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}^{\prime}_{B}$}}}$}}B^{\prime\prime}$,
$\mathsf{obs}(\mathsf{tr}_{A})=\mathsf{obs}(\mathsf{tr}^{\prime}_{B})$, and
$\Phi(A^{\prime})\sim\Phi(B^{\prime\prime})$.

Now, since $B$ is an action-deterministic configuration, applying Lemma A.7 on
$\mathsf{tr}_{B}$ and $\mathsf{tr}^{\prime}_{B}$, we obtain that
$\mathsf{enable}(B^{\prime})=\mathsf{enable}(B^{\prime\prime})$ and
$\Phi(B^{\prime})=\Phi(B^{\prime\prime})$. This allows us to conclude that
$\Phi(A^{\prime})\sim\Phi(B^{\prime})$.

It remains to show that
$\mathsf{enable}(A^{\prime})=\mathsf{enable}(B^{\prime})$. By symmetry, we
only show one inclusion. Let $\alpha_{s}\in\mathsf{enable}(A^{\prime})$, we
shall show that $\alpha_{s}\in\mathsf{enable}(B^{\prime})$. We deduce from the
latter that there is a trace $\mathsf{tr}^{\prime}$ that is either $\alpha$ or
$\tau.\alpha$ (where $\alpha$ is an observable action whose the skeleton is
$\alpha_{s}$) such that

$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{A}$}}}$}}A^{\prime}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}^{\prime}$}}}$}}A_{0}$

for some $A_{0}$. Since $A\approx B$, we know that there exist
$\mathsf{tr}^{\prime}_{0}$, $\mathsf{tr}^{\prime}$, $B^{\prime}_{0}$, and
$B^{\prime}$ such that

$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}^{\prime}_{0}$}}}$}}B^{\prime}_{0}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}^{\prime}$}}}$}}B_{0}$

with $\Phi(A_{0})\sim\Phi(B_{0})$ and
$\mathsf{obs}(\mathsf{tr}_{A})=\mathsf{obs}(\mathsf{tr}_{0}^{\prime})$ and
$\mathsf{obs}(\mathsf{tr}^{\prime})=\alpha$. we have that
$\alpha\in\mathsf{enable}(B^{\prime}_{0})$. In particular, using Property A.5,
we have that $\alpha_{s}\in\mathsf{enable}(B^{\prime}_{0})$.

Now, since $B$ is an action-deterministic configuration, applying Lemma A.7 on
$\mathsf{tr}_{B}$ and $\mathsf{tr}^{\prime}_{0}$ we obtain
$\mathsf{enable}(B^{\prime})=\mathsf{enable}(B^{\prime}_{0})$, and thus
$\alpha_{s}\in\mathsf{enable}(B^{\prime})$.

######  Proposition A.11.

Let $A$ be an action-deterministic configuration and $P,Q$ two of its
processes. If $\mathsf{enable}(P)=\mathsf{enable}(Q)$ then
$\mathsf{sk}(P)=\mathsf{sk}(Q)$.

######  Proof A.12.

Let us show that $\mathsf{sk}(P)=\mathsf{sk}(Q)$. If $\mathsf{enable}(P)$ is
an empty set then $P=0$ and thus from $\mathsf{enable}(Q)=\emptyset$ we deduce
that $Q=0$ as well implying the required equality on skeletons. If
$\mathsf{enable}(P)$ is a singleton then it must be $\\{\mathsf{sk}(P)\\}$ —
we cannot be in the case where $P$ is a parallel composition, for in that case
there would be at least two skeletons in $\mathsf{enable}(P)$ by action-
determinism of $A$. The same goes with $Q$ thus we have
$\\{\mathsf{sk}(P)\\}=\\{\mathsf{sk}(Q)\\}$. Finally, if $\mathsf{enable}(P)$
contains at least two skeletons then it must be the case that $P$ is a
parallel composition of the form $\Pi_{i}P_{i}$ and
$\mathsf{enable}(P)=\cup_{i}\\{\mathsf{sk}(P_{i})\\}$. Similarly, $Q$ must be
of the form $\Pi_{i}Q_{i}$ and
$\mathsf{enable}(Q)=\cup_{i}\\{\mathsf{sk}(Q_{i})\\}$. Here, we make use of
action-determinism to obtain that the number of subprocesses in parallel is
the same as the cardinality of the sets of skeletons, and thus the same for
$P$ and $Q$: indeed, no two parallel subprocesses can have the same skeleton.
We conclude that $\mathsf{sk}(P)=\mathtt{par}(S)$ where $S$ is the ordered
sequence of skeletons from $\cup_{i}\\{\mathsf{sk}(P_{i})\\}$, and
$\mathsf{sk}(Q)=\mathtt{par}(S)$ where $S$ is the ordered sequence of
skeletons from
$\cup_{i}\\{\mathsf{sk}(Q_{i})\\}=\cup_{i}\\{\mathsf{sk}(P_{i})\\}$.

######  Lemma (3.5).

Let $A$ and $B$ be two action-deterministic configurations such that
${A\approx B}$ and $\mathsf{skl}(A)=\mathsf{skl}(B)$. For any execution
$A\xrightarrow{[\alpha_{1}]^{\ell_{1}}}_{a}A_{1}\xrightarrow{[\alpha_{2}]^{\ell_{2}}}_{a}\ldots\xrightarrow{[\alpha_{n}]^{\ell_{n}}}_{a}A_{n}$
with $\mathsf{bc}(\alpha_{1}.\ldots\alpha_{n})\cap\mathsf{fc}(B)=\emptyset$,
there exists an execution
$B\xrightarrow{[\alpha_{1}]^{\ell_{1}}}_{a}B_{1}\xrightarrow{[\alpha_{2}]^{\ell_{2}}}_{a}\ldots\xrightarrow{[\alpha_{n}]^{\ell_{n}}}_{a}B_{n}$
such that $\Phi(A_{i})\sim\Phi(B_{i})$ and
$\mathsf{skl}(A_{i})=\mathsf{skl}(B_{i})$ for any $1\leq i\leq n$.

######  Proof A.13.

We show this result by induction on the length of the derivation
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}A_{n}$.
The case where $\mathsf{tr}$ is empty (_i.e.,_ no action even a non-observable
one) is obvious. Assume that we have proved such a result for all the
executions of length $n$, and we want to establish the result for an execution
of length $n+1$.

Consider an execution of
$[\alpha_{1}]^{\ell_{1}}\ldots[\alpha_{n}]^{\ell_{n}}$ from $A$ to $A_{n}$,
followed by $[\alpha_{n+1}]^{\ell_{n+1}}$ towards $A_{n+1}$. By induction
hypothesis, we know that there exists an execution

$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha_{1}]^{\ell_{1}}$}}}$}}B_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha_{2}]^{\ell_{2}}$}}}$}}\ldots\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha_{n}]^{\ell_{n}}$}}}$}}B_{n}$

such that $\Phi(A_{n})\sim\Phi(B_{n})$ and
$\mathsf{skl}(A_{i})=\mathsf{skl}(B_{i})$ for any $1\leq i\leq n$. It remains
to establish that there exists $B_{n+1}$ such that $B_{n}$ can perform
$[\alpha_{n+1}]^{\ell_{n+1}}$ towards $B_{n+1}$,
$\Phi(A_{n+1})\sim\Phi(B_{n+1})$ and
$\mathsf{skl}(A_{n+1})=\mathsf{skl}(B_{n+1})$. We distinguish several cases
depending on the action $\alpha_{n+1}$.

_Case $\alpha_{n+1}=\mathtt{zero}$._ We have that
$[\mathtt{zero}]^{\ell_{n+1}}\in\mathsf{skl}(A_{n})$, and thus, since
$\mathsf{skl}(A_{n})=\mathsf{skl}(B_{n})$, we have also that
$[\mathtt{zero}]^{\ell_{n+1}}\in\mathsf{sk}(B_{n})$. We deduce that
$A_{n}=(\\{[0]^{\ell_{n+1}}\\}\uplus\mathcal{P}_{0};\Phi_{0})$, and
$B_{n}=(\\{[0]^{\ell_{n+1}}\\}\uplus\mathcal{Q}_{0};\Psi_{0})$ for some
$\mathcal{P}_{0}$, $\mathcal{Q}_{0}$, $\Phi_{0}$, and $\Psi_{0}$. Moreover,
since $\mathsf{skl}(A_{n})=\mathsf{skl}(B_{n})$, we deduce that
$\mathsf{skl}(\mathcal{P}_{0})=\mathsf{skl}(\mathcal{Q}_{0})$. Let
$B_{n+1}=(\mathcal{Q}_{0};\Psi_{0})$. We have that:

  * •

$B_{n}=(\\{[0]^{\ell_{n+1}}\\}\uplus\mathcal{Q}_{0};\Psi_{0})\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\mathtt{zero}]^{\ell_{n+1}}$}}}$}}(\mathcal{Q}_{0};\Psi_{0})=B_{n+1}$,

  * •

$\Phi(A_{n+1})=\Phi(A_{n})\sim\Phi(B_{n})=\Phi(B_{n+1})$, and

  * •

$\mathsf{skl}(A_{n+1})=\mathsf{skl}(\mathcal{P}_{0})=\mathsf{skl}(\mathcal{Q}_{0})=\mathsf{skl}(B_{n+1})$.

_Case $\alpha_{n+1}=\mathtt{par}(S)$ for some sequence
$S=(\beta_{1},\ldots,\beta_{k})$._ Note that this sequence is ordered
according to our order $<$ over skeletons (_i.e.,_
$\beta_{1}<\ldots<\beta_{k}$) and $\beta_{i}$’s are pairwise distinct by
action-determinism of $A$. We have
$[\mathtt{par}(S)]^{\ell_{n+1}}\in\mathsf{skl}(A_{n})$, and thus, since
$\mathsf{skl}(A_{n})=\mathsf{skl}(B_{n})$, we have also that
$[\mathtt{par}(S)]^{\ell_{n+1}}\in\mathsf{skl}(B_{n})$.
$A_{n}=(\\{[\Pi_{i=1}^{k}P_{i}]^{\ell_{n+1}}\\}\uplus\mathcal{P}_{0};\Phi_{0})$,
$\uplus_{i=1}^{k}\mathsf{sk}(P_{i})=\\{\beta_{1},\ldots,\beta_{k}\\}$ and
$B_{n}=(\\{[\Pi_{i=1}^{k}Q_{i}]^{\ell_{n+1}}\\}\uplus\mathcal{Q}_{0};\Psi_{0})$
for some $P_{i}$, $Q_{i}$, $\mathcal{P}_{0}$, $\mathcal{Q}_{0}$, $\Phi_{0}$,
and $\Psi_{0}$. Further, we have

$A_{n+1}=(\uplus_{i=1}^{k}\\{[P_{\pi(i)}]^{\ell_{n+1}i}\\}\uplus\mathcal{P}_{0};\Phi_{0})$

for some permutation $\pi$ over $[1;k]$ such that
$\mathsf{sk}(P_{\pi(i)})=\beta_{i}$ for all $i$. Moreover, since
$\mathsf{skl}(A_{n})=\mathsf{skl}(B_{n})$, we deduce that
$\mathsf{skl}(\mathcal{P}_{0})=\mathsf{skl}(\mathcal{Q}_{0})$, and

$\\{\mathsf{sk}(P_{i})\leavevmode\nobreak\ |\leavevmode\nobreak\ 1\leq i\leq
k\\}=\\{\mathsf{sk}(Q_{i})\leavevmode\nobreak\ |\leavevmode\nobreak\ 1\leq
i\leq k\\}=\\{\beta_{1},\ldots,\beta_{k}\\}$

Remark that, since $P_{i}$ (resp. $Q_{i}$) cannot be a zero or a parallel we
have that $\mathsf{enable}(P_{i})=\\{\mathsf{sk}(P_{i})\\}$ (resp.
$\mathsf{enable}(Q_{i})=\\{\mathsf{sk}(Q_{i})\\}$) and those sets are
singletons. Moreover, by action-determinism of $A$ and $B$ we know that all
those singletons are pairwise disjoint. From this, we conclude that there
exists a permutation $\pi^{\prime}$ over $[1;k]$ such that

$\forall i,\
\mathsf{sk}(Q_{\pi^{\prime}(i)})=\beta_{i}=\mathsf{sk}(P_{\pi(i)})$

and thus

$\forall i,\
\mathsf{skl}([Q_{\pi^{\prime}(i)}]^{\ell_{n+1}i})=\mathsf{skl}([P_{\pi(i)}]^{\ell_{n+1}i})$

We can finally let $B_{n+1}$ be
$(\uplus_{i=1}^{k}\\{[Q_{\pi^{\prime}(i)}]^{\ell_{n+1}i}\\}\uplus\mathcal{Q}_{0};\Psi_{0})$
and we have:

  * •

$B_{n}=(\\{[\Pi_{i=1}^{k}Q_{i}]^{\ell_{n+1}}\\}\uplus\mathcal{Q}_{0};\Psi_{0})\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\mathtt{par}(S)]^{\ell_{n+1}}$}}}$}}(\uplus_{i=1}^{k}\\{[Q_{\pi^{\prime}(i)}]^{\ell_{n+1}i}\\}\uplus\mathcal{Q}_{0};\Psi_{0})=B_{n+1}$,

  * •

$\Phi(A_{n+1})=\Phi(A_{n})\sim\Phi(B_{n})=\Phi(B_{n+1})$, and

  * •

$\mathsf{skl}(A_{n+1})=\mathsf{skl}(\mathcal{P}_{0})\;\uplus\;\biguplus_{i=1}^{k}\mathsf{skl}([P_{\pi(i)}]^{\ell_{n+1}i})$
$\mathsf{skl}(A_{n+1})$
$=\mathsf{skl}(\mathcal{Q}_{0})\;\uplus\;\biguplus_{i=1}^{k}\mathsf{skl}([Q_{\pi^{\prime}(i)}]^{\ell_{n+1}i})=\mathsf{skl}(B_{n+1})$.

_Case $\alpha_{n+1}=\mathtt{in}(c,M)$ for some $c$, and $M$ with
$M\in\mathcal{T}(\mathrm{dom}(\Phi(A_{n}))$._ We have that
$[\mathtt{in}_{c}]^{\ell_{n+1}}\in\mathsf{skl}(A_{n})$, and thus, since
$\mathsf{skl}(A_{n})=\mathsf{skl}(B_{n})$, we have
$[\mathtt{in}_{c}]^{\ell_{n+1}}\in\mathsf{skl}(B_{n})$. We deduce that
$A_{n}=(\\{[\mathtt{in}(c,x_{A}).P]^{\ell_{n+1}}\\}\uplus\mathcal{P}_{0};\Phi_{0})$,
and
$B_{n}=(\\{[\mathtt{in}(c,x_{B}).Q]^{\ell_{n+1}}\\}\uplus\mathcal{Q}_{0};\Psi_{0})$
for some $x_{A}$, $x_{B}$, $P$, $Q$, $\mathcal{P}_{0}$, $\mathcal{Q}_{0}$,
$\Phi_{0}$, and $\Psi_{0}$. Since $A\approx B$ and thus
$\mathrm{dom}(\Phi(A))=\mathrm{dom}(\Phi(B))$, we have that
$\mathrm{dom}(\Phi_{0})=\mathrm{dom}(\Psi_{0})$. Moreover, since
$\mathsf{skl}(A_{n})=\mathsf{skl}(B_{n})$, we deduce that
$\mathsf{skl}(\mathcal{P}_{0})=\mathsf{skl}(\mathcal{Q}_{0})$. Let
$B_{n+1}=([Q\\{{u_{B}}/{x_{B}}\\}]^{\ell_{n+1}}\uplus\mathcal{Q}_{0};\Psi_{0})$
where $u_{B}=M\Psi_{0}$. We have that:

  * •

$B_{n}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\mathtt{in}(c,M)]^{\ell_{n+1}}$}}}$}}B_{n+1}$,
and

  * •

$\Phi(A_{n+1})=\Phi(A_{n})\sim\Phi(B_{n})=\Phi(B_{n+1})$.

It remains to show that $\mathsf{skl}(A_{n+1})=\mathsf{skl}(B_{n+1})$. Since
we have that $\mathsf{skl}(\mathcal{P}_{0})=\mathsf{skl}(\mathcal{Q}_{0})$,
and the label of the new subprocess is the same (namely, $\ell_{n+1}$) on both
sides, we only need to show that:

$\mathsf{sk}(P\\{M\Phi_{0}/x_{A}\\})=\mathsf{sk}(Q\\{M\Psi_{0}/x_{B}\\})$

In order to improve the readability, we will note
$P^{\prime}=P\\{M\Phi_{0}/x_{A}\\}$ and $Q^{\prime}=Q\\{M\Psi_{0}/x_{B}\\}$.
We have that $A$ and $B$ are two action-deterministic configurations such that
$A\approx B$. Moreover, they perform the same trace, respectively towards
$A_{n+1}$ and $B_{n+1}$. Thus, thanks to Proposition A.9, we deduce that
$\mathsf{enable}(A_{n+1})=\mathsf{enable}(B_{n+1})$. Moreover, our hypothesis
$\mathsf{skl}(\mathcal{P}_{0})=\mathsf{skl}(\mathcal{Q}_{0})$ implies that
$\mathsf{enable}(\mathcal{P}_{0})=\mathsf{enable}(\mathcal{Q}_{0})$, and thus
we deduce that $\mathsf{enable}(P^{\prime})=\mathsf{enable}(Q^{\prime})$
(recall that by action-determinism, unions of the form
$\mathsf{enable}(A_{n+1})=\mathsf{enable}(\mathcal{P}_{0})\cup\mathsf{enable}(P^{\prime})$
are actually disjoint unions). We conclude using Proposition A.11.

_Case $\alpha_{n+1}=\mathtt{out}(c,w)$ for some $c$ and some $w$ with
$w\not\in\mathrm{dom}(\Phi(A_{n}))$._ This case is similar to the previous
one. However, during such a step, the frame of each configuration is enriched,
and thus the fact that $\Phi(A_{n+1})\sim\Phi(B_{n+1})$ is now a consequence
of Proposition A.9.

_Case $\alpha_{n+1}=\mathtt{sess}(a,\vv{c})$ for some $a$, and some $\vv{c}$._
Firstly, we show for later that $\vv{c}$ are fresh in $B_{n}$. Indeed, we
deduce from
$\mathsf{bc}(\alpha_{1}.\ldots\alpha_{n+1})\cap\mathsf{fc}(B)=\emptyset$ that
$\vv{c}$ are fresh in $B$ and we know that free channels of $B_{n}$ are
included in $\mathsf{fc}(B)\cup\mathsf{bc}(\alpha_{1}.\ldots\alpha_{n})$.
Thereby, if there was a channel $c_{i}\in\vv{c}\cap\mathsf{fc}(B_{n})$ it
would be in $\mathsf{bc}(\alpha_{1}.\ldots\alpha_{n})$ but this is forbidden
because of the freshness condition (in the current trace) over channels,
_i.e.,_ new channels cannot be introduced twice (once in
$\alpha_{1}.\ldots\alpha_{n}$ and once in $\alpha_{n+1}$).

As before, we obtain

$A_{n}=(\\{[\mathbf{\large!}^{a}_{\vv{c},\vv{n_{P}}}P]^{\ell_{n+1}}\\}\uplus\mathcal{P}_{0};\Phi_{0})\quad\mbox{and}\quad
B_{n}=(\\{[\mathbf{\large!}^{a}_{\vv{c},\vv{n_{Q}}}Q]^{\ell_{n+1}}\\}\uplus\mathcal{Q}_{0};\Psi_{0})$

for some $P$, $Q$, $\mathcal{P}_{0}$, $\mathcal{Q}_{0}$, $\Phi_{0}$, and
$\Psi_{0}$. Moreover, since $\mathsf{skl}(A_{n})=\mathsf{skl}(B_{n})$, we
deduce that $\mathsf{skl}(\mathcal{P}_{0})=\mathsf{skl}(\mathcal{Q}_{0})$.

We have

$A_{n+1}=(\\{[P]^{\ell_{n+1}1},[\mathbf{\large!}^{a}_{\vv{c},\vv{n_{P}}}P]^{\ell_{n+1}2}\\}\uplus\mathcal{P}_{0};\Phi_{0})$

Accordingly, let us pose

$B_{n+1}=(\\{[Q]^{\ell_{n+1}1},[\mathbf{\large!}^{a}_{\vv{c},\vv{n_{Q}}}Q]^{\ell_{n+1}2}\\}\uplus\mathcal{Q}_{0};\Psi_{0})$

We have that:

  * •

$B_{n}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\mathtt{sess}(a,\vv{c})]^{\ell_{n+1}}$}}}$}}B_{n+1}$;
and

  * •

$\Phi(A_{n+1})=\Phi(A_{n})\sim\Phi(B_{n})=\Phi(B_{n+1})$.

It remains to show that $\mathsf{skl}(A_{n+1})=\mathsf{skl}(B_{n+1})$. Since
we have that $\mathsf{skl}(\mathcal{P}_{0})=\mathsf{skl}(\mathcal{Q}_{0})$,
and since the labels of corresponding subprocesses are the same on both sides,
we only need to show that:

  * •

$\mathsf{sk}(P)=\mathsf{sk}(Q)$ and

  * •

$\mathsf{sk}(\mathbf{\large!}^{a}_{\vv{c},\vv{n_{P}}}P)=\mathsf{sk}(\mathbf{\large!}^{a}_{\vv{c},\vv{n_{Q}}}Q)$

As in the previous case, thanks to Proposition A.9, we know that
$\mathsf{enable}(A_{n+1})=\mathsf{enable}(B_{n+1})$, and we deduce that
$\mathsf{enable}(P)=\mathsf{enable}(Q)$ and
$\mathsf{enable}(\mathbf{\large!}^{a}_{\vv{c},\vv{n_{P}}}P)=\mathsf{enable}(\mathbf{\large!}^{a}_{\vv{c},\vv{n_{Q}}}Q)$,
which allows us to conclude using Proposition A.11.

Finally, we can define the annotated trace equivalence and show that, for
action-deterministic configurations, it coincides with trace equivalence.

######  Definition A.14.

Let $A$ and $B$ be two configurations. We have that $A\sqsubseteq_{a}B$ if,
for every $A^{\prime}$ such that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}A^{\prime}$
with $\mathsf{bc}(\mathsf{tr})\cap\mathsf{fc}(B)=\emptyset$, then there exists
$B^{\prime}$ such that
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}B^{\prime}$,
and $\Phi\sim\Psi$. They are in _annotated trace equivalence_ , denoted
$A\approx_{a}B$, if $A\sqsubseteq_{a}B$ and $B\sqsubseteq_{a}A$.

######  Lemma A.15.

Let $A$ and $B$ be two action-deterministic configurations such that
$\mathsf{skl}(A)=\mathsf{skl}(B)$.

$A\approx B\text{ if, and only if, }A\approx_{a}B$

######  Proof A.16.

Firstly, $A\approx_{a}B$ trivially implies $A\approx B$. For the other
direction, we use Lemma 3.5 to conclude.

##  Appendix B Compression

###  B.1 Reachability

######  Lemma (4.3).

Let $A$, $A^{\prime}$ be two configurations and $\mathsf{tr}$ be such that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\;\mathsf{tr}\;$}}}$}}_{a}A^{\prime}$
is complete. There exists a trace $\mathsf{tr}_{c}$, such that
$\lfloor{\mathsf{tr}_{c}}\rfloor$ can be obtained from $\mathsf{tr}$ by
swapping independent labelled actions, and
$\lceil{A}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{c}$}}}$}}_{c}\lceil{A^{\prime}}\rceil$.

######  Proof B.1.

Let $A=(\mathcal{P};\Phi)$ be a configuration and
$(\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}A^{\prime}$
a complete execution. We proceed by induction on the length of $\mathsf{tr}$,
distinguishing two cases.

_Case 1._ We first consider the case where there is at least one process in
$\mathcal{P}$ that is negative and non-replicated. Since we are considering a
complete execution, at least one negative action $\alpha$ is performed on this
process in $\mathsf{tr}$. This action may be an output, the decomposition of a
parallel composition, or the removal of a zero. If there are more than one
such action, we choose the one that can be performed using Neg, _i.e.,_ the
one that is minimal according to our arbitrary order on labelled skeletons.
Since our action can be performed initially by our process, and by well-
labelling, the label of the action is independent with all labels of
previously executed actions in $\mathsf{tr}$. Moreover, there cannot be any
second-order dependency between $\alpha$ and one of those actions. Indeed, if
$\alpha$ is an output, no input performed before $\alpha$ is able to use the
handle of $\alpha$. It can thus be swapped before all the others by using
Lemma 3.3, obtaining an execution of trace $\alpha.\mathsf{tr}^{\prime}$
ending in the same configuration $A^{\prime}$. The rule Neg can be performed
in the compressed semantics to trigger the action $\alpha$, and by induction
hypothesis on $\mathsf{tr}^{\prime}$ we can complete our compressed execution
towards $A^{\prime}$.

_Case 2._ Otherwise, when $\mathcal{P}$ contains only positive or replicated
processes, we must choose one process to focus on, start a positive phase and
execute all its actions until we can finally release the focus. As long as all
processes are positive or replicated, only input or session actions can be
performed. In either case, the action yields a new process (the continuation
of the input, or the new session) which may be negative or positive. We define
the _positive prefix_ of our execution as the prefix of actions for which all
but the last transition yield a positive process. It is guaranteed to exist
because $A^{\prime}$ contains only negative processes.

The positive prefix is composed only of input and replication actions. Because
session actions are performed by negative processes, and no new negative
process is created in the positive prefix, session actions can be permuted at
the beginning of the prefix thanks to Lemma 3.3. Thus, we assume without loss
of generality that the prefix is composed of session actions, followed by
input actions: we write
$\mathsf{tr}=\mathsf{tr}_{!}.\mathsf{tr}_{\mathrm{in}}.\mathsf{tr}_{0}$. In
the portion of the execution where inputs of $\mathsf{tr}_{\mathrm{in}}$ are
performed, there is an obvious bijective mapping between the processes of any
configuration and its successor, allowing us to follow execution threads, and
to freely permute inputs pertaining to different threads. Such permutations
are made possible by Lemma 3.3. Indeed, they concern actions that are (i)
sequentially independent (_i.e.,_ labels are independent) since two different
threads involve actions performed by processes in parallel and (ii) recipe
independent since there is no output action in $\mathsf{tr}_{\mathrm{in}}$.

The last action of the positive prefix releases a negative process $P^{-}$.
Let $P$ be its antecedent (trough its corresponding thread) in the
configuration obtained after the execution of $\mathsf{tr}_{!}$. We have that:

$A=(\mathcal{P};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{!}$}}}$}}_{a}(\mathcal{P}_{1}\uplus\\{P\\};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{\mathrm{in}}$}}}$}}_{a}(\mathcal{P}_{2}\uplus\\{P^{-}\\};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{0}$}}}$}}_{a}A^{\prime}$

Now we can write $\mathcal{P}=\mathcal{P}_{0}\uplus\\{P_{\mathsf{f}}\\}$ where
$P_{\mathsf{f}}$ is either $P$ or a replicated process that gives rise to $P$
in one transition. By permuting actions pertaining to $P_{\mathsf{f}}$ before
all others thanks to Lemma 3.3 and previous remarks, we obtain an execution of
the form

$A=(\mathcal{P}_{0}\uplus\\{P_{\mathsf{f}}\\};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{1}$}}}$}}_{a}(\mathcal{P}^{\prime}_{0}\uplus\\{P^{-}\\};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{2}$}}}$}}_{a}(\mathcal{P}_{2}\uplus\\{P^{-}\\};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{0}$}}}$}}_{a}A^{\prime}$

where $\mathsf{tr}_{1}.\mathsf{tr}_{2}.\mathsf{tr}_{0}$ is a permutation of
$\mathsf{tr}$ of independent labelled actions,
$\mathsf{tr}_{1}=[\alpha]^{\ell}.\mathsf{tr}^{\prime}_{1}$, and
$\mathcal{P}^{\prime}_{0}=\mathcal{P}_{0}$ when $P_{\mathsf{f}}=P$, and
$\mathcal{P}^{\prime}_{0}=\mathcal{P}_{0}\uplus\\{P_{\mathsf{f}}\\}$
otherwise.

In the compressed semantics, if we initiate a focus on $P_{\mathsf{f}}$ we can
execute the actions of $\mathsf{tr}_{1}$ and release the focus when reaching
$P^{-}$, _i.e.,_ we have that (where $\ell^{\prime}$ is the label of $P^{-}$):

$(\mathcal{P};\varnothing;\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\mathtt{foc}(\alpha)]^{\ell}$}}}$}}_{c}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}^{\prime}_{1}$}}}$}}_{c}(\mathcal{P}^{\prime}_{0};P^{-};\Phi)\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\mathtt{rel}]^{\ell^{\prime}}$}}}$}}_{c}(\mathcal{P}^{\prime}_{0}\uplus\\{P^{-}\\};\varnothing;\Phi).$

We can conclude by induction hypothesis on $\mathsf{tr}_{2}.\mathsf{tr}_{0}$.

###  B.2 Equivalence

We prove below the two implications of Theorem 4.6, dealing first with
soundness and then with the more involved completeness result.

######  Lemma B.2 (Soundness).

Let $A$ and $B$ be action-deterministic configurations such that
$\mathsf{skl}(A)=\mathsf{skl}(B)$. We have that $A\approx B$ implies
$\lceil{A}\rceil\approx_{c}\lceil{B}\rceil$.

######  Proof B.3.

By symmetry it suffices to show
$\lceil{A}\rceil\sqsubseteq_{c}\lceil{B}\rceil$. Consider an execution
$\lceil{A}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$
such that $\mathsf{bc}(\mathsf{tr})\cap\mathsf{fc}(B)=\emptyset$. Thanks to
Lemma 4.2, we know that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\lfloor{\mathsf{tr}}\rfloor$}}}$}}_{a}\lfloor{A^{\prime}}\rfloor$.
Let
$\lfloor{\mathsf{tr}}\rfloor=[\alpha_{1}]^{\ell_{1}}\ldots[\alpha_{n}]^{\ell_{n}}$,
and we denote $A_{1},\ldots,A_{n}$ the intermediate configurations that are
reached during this execution. We have that:

$A_{0}=A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha_{1}]^{\ell_{1}}$}}}$}}_{a}A_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha_{2}]^{\ell_{2}}$}}}$}}_{a}\ldots\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha_{n}]^{\ell_{n}}$}}}$}}_{a}A_{n}=(\mathcal{P};\Phi_{A}).$

Applying Lemma 3.5, we deduce that $B$ can perform a very similar execution
(same labels, same actions), _i.e.,_

$B_{0}=B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha_{1}]^{\ell_{1}}$}}}$}}_{a}B_{1}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha_{2}]^{\ell_{2}}$}}}$}}_{a}\ldots\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$[\alpha_{n}]^{\ell_{n}}$}}}$}}_{a}B_{n}=(\mathcal{Q};\Phi_{B}).$

with $\Phi(A_{i})\sim\Phi(B_{i})$ and
$\mathsf{skl}(A_{i})=\mathsf{skl}(B_{i})$ for $0\leq i\leq n$.

Due to this strong symmetry, we are sure that $\lceil{B}\rceil$ will be able
to do this execution in the compressed semantics. In particular, the fact that
a given configuration $B_{i}$ can start a positive phase or has to release the
focus is determined by the set $\mathsf{skl}(B_{i})=\mathsf{skl}(A_{i})$ and
the fact that it can keep the focus on a specific process while performing
positive actions can be deduce from labels of $\mathsf{tr}$. Finally, we have
shown that if $A_{i}$ can execute an action $\alpha$ using Neg rule then
$B_{i}$ can as well. The only missing part is about the fact that Neg has been
made non-branching using an arbitrary order on labelled skeletons. Let say we
can use Neg only for actions whose skeleton is minimal among others skeletons
of available, negative actions. Using
$\mathsf{skl}(A_{i})=\mathsf{skl}(B_{i})$, we easily show that this is
symmetric for $A_{i}$ and $B_{i}$. This way, we obtain an execution
$\lceil{B}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}B^{\prime}$
with $\lfloor{B^{\prime}}\rfloor=B_{n}$. Finally, we have
$\Phi(B^{\prime})=\Phi_{B}\sim\Phi_{A}=\Phi(A^{\prime})$.

######  Lemma B.4.

Let $A$ and $B$ be two action-deterministic configurations such that
$A\approx_{c}B$. If
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$
and
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}B^{\prime}$
for a labelled trace $\mathsf{tr}$ then $A^{\prime}\approx_{c}B^{\prime}$.

######  Proof B.5.

We assume $A\approx_{c}B$,
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$
and
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}B^{\prime}$
for a labelled trace $\mathsf{tr}=\alpha_{1}.\ldots\alpha_{n}$. We shall prove
$A^{\prime}\approx_{c}B^{\prime}$. By symmetry, we show one inclusion.
Consider an execution
$A^{\prime}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{2}$}}}$}}_{c}A_{2}$
such that $\mathsf{bc}(\mathsf{tr}_{2})\cap\mathsf{fc}(B^{\prime})=\emptyset$.
Let us construct an execution
$B^{\prime}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{2}$}}}$}}_{c}B_{2}$
such that $\Phi(A_{2})\sim\Phi(B_{2})$. Firstly, remark that since
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}B^{\prime}$,
we have that $\mathsf{bc}(\mathsf{tr})\cap\mathsf{fc}(B)=\emptyset$. In order
to exploit our hypothesis $A\approx_{c}B$, we shall prove that
$\mathsf{bc}(\mathsf{tr}.\mathsf{tr}_{2})\cap\mathsf{fc}(B)=\emptyset$. All
that remains to show is
$\mathsf{bc}(\mathsf{tr}_{2})\cap(\mathsf{fc}(B)\backslash\mathsf{fc}(B^{\prime}))=\emptyset$.
This is implied by the fact that channels in
$\mathsf{fc}(B)\backslash\mathsf{fc}(B^{\prime})$ must occur in $\mathsf{tr}$
as bound channels and, because of the execution
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}.\mathsf{tr}_{2}$}}}$}}_{c}A_{2}$,
those channels cannot appear in the set $\mathsf{bc}(\mathsf{tr}_{2})$.

We have that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}.\mathsf{tr}_{2}$}}}$}}_{c}A_{2}$
and thus by hypothesis,
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}.\mathsf{tr}_{2}$}}}$}}_{c}B_{2}$
with $\Phi(B_{2})\sim\Phi(A_{2})$. Since there can be at most one process in
$B$ that has a label that matches the label of $\alpha_{1}$, there is at most
one configuration $B_{1}$ that satisfies
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\alpha_{1}$}}}$}}_{c}B_{1}$.
By iteration, we obtain the unicity of the configuration $B^{\prime}$
satisfying
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}B^{\prime}$.
We thus have obtained the required execution
$B^{\prime}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{2}$}}}$}}_{c}B_{2}$.

######  Lemma B.6.

Let $A$ and $B$ be two action-deterministic configurations. If for any
complete execution
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}A^{\prime}$
with $\mathsf{bc}(\mathsf{tr})\cap\mathsf{fc}(B)=\emptyset$, there exists a
trace $\mathsf{tr}^{\prime}$ and an execution
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}^{\prime}$}}}$}}_{a}B^{\prime}$
such that $\Phi(A^{\prime})\sim\Phi(B^{\prime})$, then $A\sqsubseteq_{a}B$.

######  Proof B.7.

Let
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{0}$}}}$}}_{a}A_{0}$
be an execution of $A$ with
$\mathsf{bc}(\mathsf{tr}_{0})\cap\mathsf{fc}(B)=\emptyset$. Firstly, we
complete the latter execution in an arbitrary way
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{0}.\mathsf{tr}_{1}$}}}$}}_{a}A^{\prime}$
such that any process of $A^{\prime}$ is replicated and
$\mathsf{bc}(\mathsf{tr}_{0}.\mathsf{tr}_{1})\cap\mathsf{fc}(B)=\emptyset$ (it
suffices to choose fresh channels for $B$ as well). By hypothesis, there
exists an execution
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{0}.\mathsf{tr}_{1}$}}}$}}_{a}B^{\prime}$
such that $\Phi(A^{\prime})\sim\Phi(B^{\prime})$. The latter execution of $B$
is thus of the form
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{0}$}}}$}}_{a}B_{0}\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{1}$}}}$}}_{a}B^{\prime}$.
It remains to show that $\Phi(A_{0})\sim\Phi(B_{0})$. For the sake of
contradiction, we assume that $\Phi(B_{0})\sim\Phi(A_{0})$ does not hold. In
other words, there is a test of equality over $\mathrm{dom}(\Phi(B_{0}))$ that
holds for $\Phi(A_{0})$ and does not for $\Phi(B_{0})$ (or the converse).
Since
$\mathrm{dom}(\Phi(B_{0}))\subseteq\mathrm{dom}(\Phi(B^{\prime}))=\mathrm{dom}(\Phi(A^{\prime}))$,
this same test can be used to conclude that
$\Phi(A^{\prime})\sim\Phi(B^{\prime})$ does not hold as well leading to an
absurd conclusion.

######  Lemma B.8 (Completeness).

Let $A$ and $B$ be two action-deterministic configurations satisfying
$\mathsf{skl}(A)=\mathsf{skl}(B)$. Then
$\lceil{A}\rceil\approx_{c}\lceil{B}\rceil$ implies $A\approx B$.

######  Proof B.9.

Assume $\lfloor{A}\rfloor\approx_{c}\lfloor{B}\rfloor$, thanks to Lemma A.15,
it suffices to show $A\approx_{a}B$. Let us show the following intermediate
result: for any complete execution
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}A^{\prime}$
such that $\mathsf{bc}(\mathsf{tr})\cap\mathsf{fc}(B)=\emptyset$, there is an
execution
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}B^{\prime}$
such that $\Phi(A^{\prime})\sim\Phi(B^{\prime})$. Thanks to Lemma B.6 and by
symmetry of $\approx_{a}$, this intermediate result implies the required
conclusion $A\approx_{a}B$.

Let
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}A^{\prime}$
be a complete execution with
$\mathsf{bc}(\mathsf{tr})\cap\mathsf{fc}(B)=\emptyset$. We thus have that
$A^{\prime}$ is initial. Applying the Lemma 4.3, we obtain a trace
$\mathsf{tr}_{c}$ such that
$\lceil{A}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{c}$}}}$}}_{c}\lceil{A^{\prime}}\rceil$
and $\lfloor{\mathsf{tr}_{c}}\rfloor$ can be obtained from $\mathsf{tr}$ by
swapping independent actions. Since we have
$\lceil{A}\rceil\approx_{c}\lceil{B}\rceil$, we deduce that
$\lceil{B}\rceil\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}_{c}$}}}$}}_{c}\lceil{B^{\prime}}\rceil$
with $\Phi(A^{\prime})\sim\Phi(B^{\prime})$. Lemma 4.2 gives us
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\lfloor{\mathsf{tr}_{c}}\rfloor$}}}$}}_{a}B^{\prime}$.
We can now apply Lemma 3.3 to obtain
$B\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{a}B^{\prime}$
and conclude.

##  Appendix C Reduction

###  C.1 Reachability

######  Lemma (5.3).

Let $A$ and $A^{\prime}$ be two initial configurations such that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}$}}}$}}_{c}A^{\prime}$.
We have that
$A\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\mathsf{tr}^{\prime}$}}}$}}_{c}A^{\prime}$
for any $\mathsf{tr}^{\prime}\equiv_{\Phi(A^{\prime})}\mathsf{tr}$.

######  Proof C.1.

Thanks to Lemma 4.2, we have that
$\lfloor{A}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\lfloor{\mathsf{tr}}\rfloor$}}}$}}_{a}(\mathcal{P};\Phi)$.
We first prove that $\mathsf{tr}^{\prime}$ can be performed using
$\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}$}}_{a}$.
For this, it suffices to establish the implication for each of the two
generators of $\equiv_{\Phi}$. The first case is given by Lemma 3.3. The
second one is a common property of (derivatives of) the applied $\pi$-calculus
that follows from a simple observation of the transition rules. Finally, we
must prove that $\mathsf{tr}^{\prime}$ can be played using
$\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$$}}}$}}_{c}$.
Thanks to initiality of $A$ and $(\mathcal{P};\varnothing;\Phi)$ we know that
each block of $\mathsf{tr}$ starts when the configuration is initial and after
performing it we get another initial configuration. This is still true in
$\lfloor{A}\rfloor\mathrel{\raisebox{-0.5pt}[5.0pt]{$\xrightarrow{\raisebox{-1.2pt}[2.0pt][1.0pt]{\scalebox{0.7}{$\lfloor{\mathsf{tr}^{\prime}}\rfloor$}}}$}}_{a}(\mathcal{P};\Phi)$.
Finally, labels of blocks of $\mathsf{tr}^{\prime}$ ensures that a single
process is used in a positive part of any block. Having proving those two
facts, we can easily show that each block of $\mathsf{tr}^{\prime}$ can be
performed using