# DeepSec: Deciding Equivalence Properties for Security Protocols — Improved theory and practice

**Received** Nov 14, 2022

**Revised** Dec 12, 2023

**Accepted** Jan 28, 2024

**Published** Mar 12, 2024

**Key words and phrases**

Verification, cryptographic protocols, process equivalences

Vincent Cheval<sup>a</sup> ☒ Ⓑ

Steve Kremer<sup>b</sup> ☒ Ⓑ

Itsaka Rakotonirina<sup>c</sup> ☒ Ⓑ

<sup>a</sup> University of Oxford, United Kingdom

<sup>b</sup> Inria Centre at Université de Lorraine, France

<sup>c</sup> MPI-SP, Germany

**ABSTRACT.** Automated verification has become an essential part in the security evaluation of cryptographic protocols. In this context privacy-type properties are often modelled by indistinguishability statements, expressed as behavioural equivalences in a process calculus. In this article we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of protocol sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives—those that can be represented by a subterm convergent destructor rewrite system. We also implemented the procedure in a new tool, DEEPSEC. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raising the scope of the protocols that can be analysed.

## 1. Introduction

The use of automated, formal methods has become indispensable for analysing complex security protocols, such as those for authentication, key exchange and secure channel establishment. Nowadays there exist mature, fully automated such analysers; among others AVISPA [9], PROVERIF [19], SCYTHER [46], TAMARIN [54] or Maude-NPA [58]. These tools are able to automatically verify full fledged models of widely deployed protocols and standards, such as

A preliminary version of this work appeared at IEEE Symposium on Security and Privacy (S&P) 2018 [31]. This work has been partly supported by the ANR Research and teaching chair in AI ASAP (ANR-20- CHIA-0024) with support from the region Grand Est and ANR France 2030 project SVP (ANR-22-PECY-0006).
the TLS protocol for secure connexion [17, 45], the Signal messaging protocol [53, 40], authentication protocols of the 5G standard [12], or deployed multi-factor authentication protocols [52]. Theory-wise, the tools operate in so-called symbolic models, rooted in the seminal work by Dolev and Yao [48]: the attacker has full control over the communication network, unbounded computational power, but cryptography is idealised. This model is well suited for finding attacks in the protocol logic, and tools have indeed been extremely effective in discovering this kind of flaw or proving their absence.

While most works investigate reachability properties, a later trend consists in adapting the tools—and the underlying theory—to the more complex indistinguishability properties. Such properties are generally modelled as a behavioural equivalence (bisimulation or trace equivalence) in a dedicated process calculus such as the spi calculus [4] or the applied pi calculus [1]. A typical example is real-or-random secrecy: after interacting with a protocol, an adversary is unable to distinguish the real secret used in the protocol from a random value. Privacy-type properties can also be expressed as such: anonymity may be modelled as the adversary's inability to distinguish two instances of a protocol executed by different agents; vote privacy [47] has been expressed as indistinguishability of the situations where the votes of two agents have been swapped or not; unlinkability [6] is seen as indistinguishability of two sessions, either both executed by the same agent A, or by two different agents A and B.

## Contributions

We significantly improve the theoretical understanding and the practical verification of equiva-
lences when the number of protocol sessions is bounded. We emphasise that even in this
setting, the system under study has an infinite state space due to the term algebra modelling
cryptographic primitives. Our work targets the wide class of cryptographic primitives that can
be represented by a subterm convergent rewriting system. Concretely, we provide:

1. tight complexity results for several equivalence relations: static equivalence, trace equivalence and labelled bisimilarity. In addition to the conference paper [31], we showcase the generality of our approach by providing, with a negligible proof overhead, a tight analysis of other security relations, namely similarity, simulation, and trace inclusion;

2. a novel procedure deciding all of the above mentioned security relations for a bounded number of sessions, for the class of cryptographic primitives modelled by a destructor subterm convergent rewrite system;

3. an implementation of our procedure for trace equivalence in a tool called DEEPSEC (DECiding Equivalence Properties for SECurity protocols), improved compared to its initial presentation in the conference paper [31].

We detail the three contributions below.
**Complexity** We provide the first complexity results for deciding trace equivalence and labelled bisimilarity in the applied pi calculus, without any syntactic or semantic restriction on the class of protocols (other than bounding the number of sessions), and for a large class of cryptographic primitives modelled as rewrite rules. As mentioned above, our results extend to several other security relations such as simulation. Let us also highlight one small, yet substantial difference with existing work: we do not consider cryptographic primitives (rewrite systems) as constants of the problem. As most modern verification tools allow for user-specified primitives [22, 54, 58, 24], our approach seems to better fit this reality. Typically, all existing procedures for static equivalence can only be claimed PTIME because of this difference and are actually exponential in the sizes of the signature or equational theory. Our complexity results are summarised in Table 1. All our lower bounds hold for subterm convergent rewrite systems and even for the positive fragment (without else branches). *En passant*, we present results for the pi calculus: although investigated in [23], complexity was unknown when restricted to a bounded number of sessions. Still, our main result is the coNEXP completeness (and in particular, the decidability) of trace equivalence and labelled bisimilarity for destructor subterm convergent rewrite systems.

<table><caption>**Table 1.** Summary of complexity results</caption><thead><tr><th></th><th>Pure pi calculus</th><th>Applied pi calculus<br>with destr. subterm convergent theory</th></tr></thead><tbody><tr><td>static equivalence</td><td>LOGSPACE</td><td>coNP complete</td></tr><tr><td>trace equivalence</td><td>Π<sub>2</sub> complete</td><td>coNEXP complete</td></tr><tr><td>labelled (bi)similarity</td><td>PSPACE complete</td><td>coNEXP complete</td></tr></tbody></table>

**Decision procedure** We present a novel procedure based on a symbolic semantics and constraint solving. Unlike most other work, our procedure decides equivalences *exactly*, i.e. without approximations. Moreover, it does not restrict the class of processes (except for replication), nor the use of else branches, and is correct for any cryptographic primitives that can be modelled by a subterm convergent destructor rewrite system (see Section 2 for more details). The design of the procedure did greatly benefit from our complexity study, and was developed in order to obtain tight complexity upper bounds. The theory is also more mature compared to the initial conference paper [31] which allowed some significant optimisations of the constraint solving procedure.

**Tool implementation** We implemented our procedure for trace equivalence in a tool, DEEPSEC. Its prototype has initially been presented in the conference paper [31] (and some implementation details in a tool paper [33]), but has significantly matured since then. In addition of the improvements at the level of the theoretical procedure, the low level implementation has been
more carefully engineered data-structure-wise. All in all, the DEEPSEC 2.0.0 release includes the
following new features:

- A significantly *reduced verification time* (several orders of magnitude on some examples).

- An *optional procedure exploiting the symmetries* that often arise in practical verification.
When used, this further reduces the verification time by orders of magnitude albeit for
occasionally introducing false attacks. In this article we rather focus on the main procedure;
details about this feature can be found in [32].

- An *improved user experience*. The html based pretty-print of the original prototype has been upgraded into a standalone graphical user interface. Verification queries and options can be managed directly from the interface and a simulator displays interactively equivalence proofs or attacks to better visualise the outcome of the analysis.

Naturally DEEPSEC still integrates already-present features such as multicore distribution and the partial order reductions presented in [10]. All in all this makes the tool more user friendly and scale well despite the high theoretical complexity of the problem (coNEXP). Installation guidelines can be found in the official website [35] together with a manual and a tutorial.

Through extensive benchmarks, we compare DEEPSEC to other tools limited to a bounded number of protocol sessions: APTE, SPEC, AKISS, SATEQUIV and our previous prototype (as presented in [31]). This prior version was already more efficient—by several orders of magnitude—than APTE, SPEC and AKISS, even though DEEPSEC covers a strictly larger class of protocols than APTE and SPEC. Besides, its performances were comparable to SATEQUIV, which still outperforms DEEPSEC when the number of parallel processes significantly increase. This gap in performance seems unavoidable as DEEPSEC operates on a much larger class of protocols (more primitives, else branches, no limitation to simple processes, termination guaranteed). Part of the benchmarks consists of classical authentication protocols and focuses on demonstrating scalability of the tool when augmenting the number of parallel protocol sessions. The other examples include more complex protocols, such as Abadi and Fournet's anonymous authentication protocol [3], the protocols implemented in the European passport [51], a model (without XOR) of the AKA protocol used in 3G mobile telephony, as well as the Prêt-à-Voter [57] and the Helios [5] e-voting protocols.

Related Work

The problem of analysing security protocols is undecidable in general but several decidable subclasses have been identified. While many complexity results are known for trace properties [49, 56], the case of behavioural equivalences remains mostly open. When the attacker is an eavesdropper and cannot interact with the protocol, the indistinguishability problem—*static equivalence*—has been shown PTIME for large classes of cryptographic primitives [2, 39, 42]. For active attackers, bounding the number of protocol sessions is often sufficient to
obtain decidability [56] and is of practical interest: most real-life attacks indeed only require a small number of sessions. In this context Baudet [14], and later Chevalier and Rusinowitch [36], showed that real-or-random secrecy was coNP for cryptographic primitives that can be modelled as subterm convergent rewrite systems, by checking whether two constraint systems admit the same set of solutions. These procedures do however not allow for else branches, nor do they verify trace equivalence in full generality. In [29], Cheval et al. have used Baudet's procedure as a black box to verify trace equivalence of *determinate* processes. This class of processes is however insufficient for most anonymity properties. Finally, decidability results for an unbounded number of sessions exist [38, 37], but with severe restrictions on processes and equational theories.

Tool support also exists for verifying equivalence properties. We start discussing tools that are limited to a bounded number of sessions. The SPEC tool [59, 60] verifies a sound symbolic bisimulation, but is restricted to particular cryptographic primitives (pairing, encryption, signatures and hash functions) and does not allow for else branches. In a similar setting, restricting to particular primitives, Cheval et al. [27] propose a procedure for deciding equivalence of constraint systems. This procedure can be used for deciding trace equivalence of determinate processes and has been implemented in the ADECS tool. The APTE tool [25] generalizes ADECS: it covers the same primitives but allows else branches and decides trace equivalence exactly. On the contrary, the AKISS tool [24] allows for user-defined cryptographic primitives. The procedure of this tool is correct for primitives modelled by an arbitrary convergent rewrite system that has the finite variant property [41], and termination is additionally guaranteed for subterm convergent rewrite systems. However, AKISS does only decide trace equivalence for a class of determinate processes; for other processes trace equivalence can be both over- and under-approximated. The recent SATEQUIV tool [43] uses a different approach: it relies on Graph Planning and SAT solving to verify trace equivalence, rather than a dedicated procedure. The tool is extremely efficient and several orders of magnitude faster than other tools. It does however not guarantee termination and is currently restricted to pairing and symmetric encryption and only considers a class of *simple processes* (a subclass of determinate processes) that satisfy a type-compliance condition. These restrictions severely limit its scope.

To mitigate the state explosion problem from which most of the above tools suffer, Baelde et al. [10] developed *partial order techniques* which avoid to explicitly consider all possible interleavings and which are compatible with a symbolic approach based on constrained solving. Substantial efficiency gains on practical examples have been illustrated through an implementation in the APTE tool. We also implemented these techniques in DEEPSEC. However, the techniques may only be applied on a class of *action-determinate* processes. This limitation has been overcome in a follow-up work by Baelde et al. [12]: while more general the new techniques also require additional, expensive computations resulting in less spectacular performance in-
crease than the initial work. Baelde et al. [12] have implemented their technique in a standalone
library, and plugged it into the APTE and DEEPSEC tools.

Other tools support verification of equivalence properties, even for an unbounded number
of sessions. This is the case of PROVERIF [20], TAMARIN [13] and Maude NPA [58] which all
allow for user-defined cryptographic primitives. However, given that the underlying prob-
lem is undecidable, these tools may not terminate. Moreover, they only approximate trace
equivalence by verifying the stronger *diff-equivalence*. This equivalence is too strong on many
examples. While some recent improvements on PROVERIF [26, 21] help covering more protocols,
general verification of trace equivalence is still out of scope. For instance, the verification by
Arapinis et al. [8] of unlinkability in the 3G mobile phone protocols required some “tricks”
and approximations of the protocol to avoid false attacks. In [44], Cortier et al. develop a
type system and automated type checker for verifying equivalences. While extremely efficient,
this tool only covers a fixed set of cryptographic primitives (the same as SPEC and APTE) and
verifies an approximated equivalence, similar to diff-equivalence. A different approach has
been taken by Hirschi et al. [50], identifying sufficient conditions provable by PROVERIF for
verifying unlinkability properties, implemented in the tool UKANO, a front-end to the PROVERIF
tool. UKANO does however not verify equivalence properties in general.

## Article Outline

We organize the article as follows. In Section 2 we present our formal model of cryptographic
protocols and the process equivalences used to express security properties. We also precisely
define the decision problems that we address in this article.

In Section 3 we provide an overview of our decision procedures. First, we define (sound and complete) symbolic semantics where we replace the infinite set of possible attacker inputs by a finite representation in the form of constraint systems. Second, we define the notion of a *partition tree*. The partition tree organizes all symbolic traces in a tree such that a node contains (a symbolic representation of) all statically equivalent processes that can be reached by a given trace. Third, we show how equivalences can be decided on such a partition tree. Next, we explain how to compute a partition tree *assuming* we can compute solutions to constraint systems. Finally, we discuss how the procedure for deciding trace equivalence has been implemented in the DEEPSEC tool and provide a performance evaluation.

In Section 4 we present a rule-based procedure to effectively solve constraint systems. This
requires the definition of *extended* constraint systems that store additional information and
the introduction of the new notion of *most general solutions*. Reminiscent of the notion of most
general unifiers, most general solutions are a set of solutions that guarantee that any solution
can be obtained from a most general solution by substituting atomic names by more complex
terms. After presenting all the rules of the procedure in detail we explain how to construct a
partition tree.
In Section 5 we give complexity results. To achieve upper bounds we prove termination of the constraint solving procedure and exponentially bound the number of rules and size. From these bounds we obtain that when two processes are not equivalent (for different notions of equivalence) there exists a witness of exponential size, yielding a coNEXP decision procedure for equivalence. Lower bounds are provided by reduction to the SUCCINCTSAT problem.

Finally we conclude the article in Section 6 and sketch some directions for future work.

## 2. Model

We first present our model of cryptographic protocols and use it to model the security of the Private Authentication Protocol as a running example [3]. Our framework is based on the applied pi calculus [1] and follows the tradition of symbolic models rooted in the seminal work of Dolev and Yao [48]. In these models, the low-level details of cryptography are abstracted by a term algebra describing the ideal behaviour of cryptographic primitives, whereas secret data such as cryptographic keys or nonces are represented by symbolic values called *names*.

### 2.1 Messages and cryptography

**Protocol messages** Cryptographic operations are modelled by a set $\mathcal{F}$ of symbols of fixed arity denoted $\mathcal{F} = \{f/n, g/m, \dots\}$, called a *signature*. In this article, it is always partitioned into:

- The infinite set of *constants* ($\mathcal{F}_0$) that are the functions of arity 0 of $\mathcal{F}$, thus modelling the public values of the protocol such as identities, IP addresses or public communication channels.

- The finite set of *constructors* ($\mathcal{F}_c$) modelling cryptographic operations used to build messages, typically encryption, signature, concatenation or hash.

- The finite set of *destructors* ($\mathcal{F}_d$) modelling inversions or operations that may fail depending on the structure of their argument, typically decryption, signature verification or projection.

**EXAMPLE 2.1.** The following signature captures most of the cryptographic primitives that are used in our examples and benchmarks. We will use them throughout Section 2 in examples.

<table><thead><tr><th></th><th>concatenation / pairs</th><th>symmetric encryption</th><th>asymmetric encryption</th><th>digital signature</th><th>one-way hash</th></tr></thead><tbody><tr><td>F<sub>c</sub></td><td>&lt;·, ·&gt;/2</td><td>senc/3</td><td>pk/1, aenc/3</td><td>vpk/1, sign/3</td><td>h/1</td></tr><tr><td>F<sub>d</sub></td><td>fst/1, snd/1</td><td>sdec/2</td><td>adec/2</td><td>verify/2</td><td>Ø</td></tr></tbody></table>

For example $aenc(m, r, pk(k))$ models a plaintext $m$ encrypted with public key $pk(k)$ and a randomness $r$. The corresponding decryption key would be $k$. A similar description can be made for symmetric encryption, except that the encryption and decryption keys are identical.
The model of hash functions contains no destructors on purpose, thus modelling an assumption that h is a random oracle, i.e., no identities can be derived from h. Notation-wise, we also often use a tuple notation $\langle x_1, \dots, x_n \rangle$ instead of the nested $n-1$ pairs $\langle x_1, \langle x_2, \dots \langle x_{n-1}, x_n \rangle \rangle \rangle$. ♦

A protocol message $m$ is then modelled by a term over this signature, i.e. $m$ is obtained by applying function symbols to other terms or names. The infinite set of names $\mathcal{N}$ can be seen as a symbolic abstraction of private values such as encryption keys or nonces. The set of names occurring in a term $t$ is written $\text{names}(t)$. In some models names are partitioned into public and private names, where the set of public names essentially plays the same role as $\mathcal{F}_0$. Since constants and public names have a similar role (and are even treated identically in our tool implementation) we decided to merge them into the single set $\mathcal{F}_0$ similarly to other formalisations, e.g. [37]. We write $\mathcal{T}(S)$, $S \subseteq \mathcal{F} \cup \mathcal{N}$, the set of terms built from functions, names, and constants of $S$.

**Specifying cryptographic assumptions** The behaviour of the primitives of the signature is modelled by a *rewriting system*. For that we assume an infinite set of variables $\mathcal{X} = \{x, y, z, \dots\}$ that may be used in terms, and write $\text{vars}(t)$ the set of variables occurring in a term $t$. Mappings $\sigma$ from variables to terms are called *substitutions* and are homomorphically extended to mappings from terms to terms implicitly. We use the postfix notation $t\sigma$ for $\sigma(t)$, and $\sigma\sigma'$ for the composition of substitution $\sigma' \circ \sigma$ (that is, $t\sigma\sigma' = (t\sigma)\sigma'$). We call the *domain* of $\sigma$ the set $\text{dom}(\sigma) = \{x \in \mathcal{X} \mid x\sigma \neq x\}$. For convenience we also use set notations, defining a substitution $\sigma$ such that $\text{dom}(\sigma) \subseteq \{x_1, \dots, x_n\}$ with the notation $\sigma = \{x_1 \mapsto \sigma(x_1), \dots, x_n \mapsto \sigma(x_n)\}$. Going further we may refer to the substitution $\sigma \cup \sigma'$ (provided $\sigma$ and $\sigma'$ coincide on $\text{dom}(\sigma) \cap \text{dom}(\sigma')$) or write $\sigma \subseteq \sigma'$ to mean that $\sigma'$ extends $\sigma$. A *rewriting system* $\mathcal{R}$ is then a finite binary relation on terms. All pairs of $\mathcal{R}$ are called *rewrite rules* and are assumed to be of the form

$$f(\ell_1, \dots, \ell_n) \to r \quad \text{for some } f/n \in \mathcal{F}_d \text{ and } \ell_1, \dots, \ell_n, r \in \mathcal{T}(\mathcal{F}_c \cup \mathcal{F}_0 \cup \mathcal{X})$$

Such rewriting systems are usually qualified as *constructor destructor* in the literature. By extension we also use notation $t \to s$ ("t rewrites to s") when $t$ and $s$ are related by the closure of $\mathcal{R}$ under application of substitution and term context. The reflexive transitive closure of this relation is written $\to^*$.

**EXAMPLE 2.2.** We give the rewrite rules for the primitives introduced in Example 2.1.

<table><tr><td><i>sym. encryption:</i></td><td>sdec(senc(x, y, z), z) &rarr; x</td></tr><tr><td><i>pairs:</i></td><td>fst(&lt;x, y&gt;) &rarr; x and snd(&lt;x, y&gt;) &rarr; y</td></tr><tr><td><i>asym. encryption:</i></td><td>adec(aenc(x, y, pk(z)), z) &rarr; x</td></tr><tr><td><i>signatures:</i></td><td>verify(sign(x, y, z), vpk(z)) &rarr; x</td></tr></table>
For example here one can decrypt (apply adec) a ciphertext aenc(x, y, pk(z)) with the corresponding key z to recover the plaintext x. The rule for signature verification is the opposite, recovering the signed message x using the public verification key vpk(z). The behaviour of these primitives is idealised by the absence of other rules, for example modelling an assumption that no information can be extracted from a ciphertext or a signature without access to the secret or verification keys. This idealisation can be partially lifted by adding more rewrite rules modelling specific imperfections of the cryptography. For example we can add the following new symbols and rewrite rules:

$$test\_aenc(aenc(x, y, pk(z))) \rightarrow ok \qquad get\_key(aenc(x, y, pk(z))) \rightarrow pk(z)$$

model two assumptions that 1. it is possible to distinguish a correctly encrypted message from a random bitstring, and 2. it is possible to retrieve the encryption key from the ciphertext itself (i.e. the scheme is not *key concealing*). Naturally even if a protocol is considered secure without these two rewrite rules, a security violation may arise upon adding them. It is therefore important to keep in mind the assumptions underlying the model when interpreting the result of an analysis. ♦

We observe that the rewrite rules introduced in the example above verify a classical property, *subterm convergence*, introduced in [2] and benefiting from several decidability results in the context of protocol analysis [2, 29]. It means that $\mathcal{R}$ is convergent (i.e. confluent and strongly terminating) and that its rules $\ell \rightarrow r$ verify that $r$ is either a strict subterm of $\ell$ or a *ground term* (i.e. a term without variables) in *normal form* (i.e. irreducible w.r.t. $\rightarrow$). The results of this article only apply to cryptographic primitives modelled by a constructor destructor subterm convergent rewriting systems. Imposing such restrictions is inevitable when aiming for decidability, since the problems we investigate are undecidable for arbitrary convergent rewriting systems [2].

In particular, by convergence, all terms $t \in \mathcal{T}(\mathcal{F} \cup \mathcal{N})$ have a unique normal form w.r.t. $\mathcal{R}$ that we will write $t\downarrow$. It is also common to identify messages whose destructors failed to be applied. For that we define a predicate msg on terms: we say that $t$ is a *message*, written $msg(t)$, when for all subterms $u$ of $t$, $u\downarrow$ does not contain any destructors. For example if $m, r \in \mathcal{F}_0$ and $k \neq k'$, adec(aenc(m, r, pk(k)), k) is a message but not $fst(\langle m, t \rangle)$ with $t = sdec(senc(m, r, k), k')$.
## 2.2 Protocols

**Processes** Security protocols are modelled by (plain) processes in a concurrent process calculus defined by the following grammar:

$$ 
\begin{array}{l@{\qquad}l}
P, Q := 0 & \text{null} \\
P | Q & \text{parallel} \\
\text{if } u = v \text{ then } P \text{ else } Q & \text{conditional} \\
\bar{u}\langle v \rangle.P & \text{output} \\
u(x).P & \text{input}
\end{array}
 $$

where $u, v$ are terms and $x \in \mathcal{X}$. Intuitively the 0 models a terminated process (and is often omitted for succinctness), a conditional if $u = v$ then $P$ else $Q$ executes either $P$ or $Q$ depending on whether the terms $u$ and $v$ are messages and have the same normal form, and $P | Q$ models two concurrent processes. Inter-process communications are performed with $u(x).P$ and $\bar{u}\langle v \rangle.P$ which are, respectively, inputs and outputs on a communication channel $u$. When $u$ is known to the attacker, for example when it belongs to $\mathcal{F}_0$, executing an output on $u$ adds it to the adversary's knowledge, whereas an input on $u$ is fetched from the adversary possibly forwarding a previously stored message, or computing a new message from previous outputs. Otherwise the communication is performed silently without adversarial interferences. The main difference with the calculus of [1] is the absence of replication, thus bounding the number of instructions of a process. This restriction does not make protocol analysis trivially decidable: although the number of instructions are finite, the number of their possible executions is not, since the attacker can fetch arbitrary messages to public inputs.

**EXAMPLE 2.3.** We define a process modelling the protocol for private authentication described in [3] as a running example through the article. Denoting by $sk_X, pk_X$ the secret and public keys of an agent $X$, and by $r_X$ fresh nonces, its control flow can be described as follows using an informal Alice-Bob notation:

$$ 
\begin{array}{l@{\qquad}l}
X \to B : \text{aenc}(\langle N_X, pk_X \rangle, r_X, pk_B) & \\
B \to X : \text{aenc}(\langle N_X, N_B, pk_B \rangle, r_A, pk_A) & \text{if } X = A \\
\text{aenc}(N_B, r_B, pk_B) & \text{if the decryption fails or } X \neq A
\end{array}
 $$

where $N_X, N_B$ are two freshly generated nonces. Here the agent $B$ accepts authentication requests from the agent $A$ but not from other parties. Among the security goals stated in [3] are

1. **Secrecy**: At the end of a successful instance of the protocol between $A$ and $B$, $N_A$ and $N_B$ are secrets (i.e. the attacker cannot get information about them).

2. **Anonymity**: The attacker cannot tell whether the protocol is run by $A$ and $B$ or other agents.
3. Private authentication: The attacker cannot tell whether B accepts connections from A or not.

The last two security goals explain in particular the decoy message aenc($N_B$, $r_B$, $pk_B$) that B sends upon decryption failure or connection refusal: thus from an outside observer there is no observable difference between the situations where B answers or not. The roles of X and B can be specified as follows in the applied pi calculus; each process takes as an argument its secret key s, the public key p of the agent it aims at communicating with, its fresh session nonces n, r and we write $t = \text{adec}(x, s)$:

$$X(s, p, n, r) = \bar{c}\langle\text{aenc}(\langle n, \text{pk}(s)\rangle, r, p)\rangle. \quad B(s, p, n, r) = c(x).$$
$$c(x) \qquad \begin{array}{l} \text{if } \text{snd}(t) = p \text{ then} \\ \qquad \bar{c}\langle\text{aenc}(\langle \text{fst}(t), n, \text{pk}(s)\rangle, r, p)\rangle \\ \text{else } \bar{c}\langle\text{aenc}(n, r, \text{pk}(s))\rangle \end{array}$$

where $c \in \mathcal{F}_0$. The security goals are formalised in Section 2.3. ♦

<figure><img src="image_1.png" /></figure>

**Attacker's knowledge** In the next paragraphs we formalise how processes may be executed in an active adversarial environment. The first step is to model the capabilities of the underlying attacker that spies on the communication network and actively interferes with communications. For that we refine the set of variables to $\mathcal{X} = \mathcal{X}^1 \uplus \mathcal{AX}$, thus introducing a new type of variables $\mathcal{AX} = \{ax_1, ax_2, ax_3, \dots\}$ called *axioms* that will serve as handles to make reference to attacker's observations. Concretely a term $\xi \in \mathcal{T}(\mathcal{F} \cup \mathcal{AX})$ is called a *recipe* and is intuitively an algorithm for the attacker to construct a term from their prior observations. For example upon observing the messages aenc($m, r, pk(k)$) and $k$ in this order, an attacker can use the recipe $\xi = \text{adec}(ax_1, ax_2)$ to retrieve $m$ although it has not been observed directly. We observe in particular that by definition a recipe cannot contain names, modelling that they are assumed to be private and as such cannot be used directly by the adversary.

On the other hand, the variables of $\mathcal{X}^1$, called *first-order variables* for distinction, stick to the initial role of variables—namely, being used as binders for protocol inputs. For this reason, we call a term $t \in \mathcal{T}(\mathcal{F} \cup \mathcal{N} \cup \mathcal{X}^1)$ a *protocol term*. However, we often more specifically consider *constructor terms* $\mathcal{T}(\mathcal{F}_c \cup \mathcal{F}_0 \cup \mathcal{N} \cup \mathcal{X}^1)$ that are protocol terms whose destructors have all been successfully computed, that is, reduced by a rewrite rule. We also write $\text{vars}^1(t) = \text{vars}(t) \cap \mathcal{X}^1$ the set of *first-order variables* of t. Using all these notions we define *extended processes*, representing a set of processes executed in parallel together with the knowledge aggregated by the attacker interacting with the protocol:

**DEFINITION 2.4.** An extended process is a pair $A = (\mathcal{P}, \Phi)$ with $\mathcal{P}$ a multiset of ground processes and $\Phi = \{ax_1 \mapsto u_1, \dots, ax_n \mapsto u_n\} = \Phi(A)$ is called a *frame* that is a substitution from axioms to ground constructor terms.
Formalising the example above, if the frame $\Phi = \{ax_1 \mapsto aenc(m, r, pk(k)), ax_2 \mapsto k\}$ models the attacker's observations during the execution of a protocol, the fact that $m$ can be retrieved with the recipe $\xi = adec(ax_1, ax_2)$ is expressed by the fact that $msg(\xi\Phi)$ and $\xi\Phi\downarrow = m$. A typical security problem is to decide, given a frame $\Phi$ and a term $t$, whether $t$ is deducible by the attacker from $\Phi$; that is, whether there exists a recipe $\xi$ such that $msg(\xi\Phi)$ and $\xi\Phi\downarrow = t\downarrow$.

**Operational semantics** We now formalise the semantics of processes. By manipulating extended processes this semantics carries the knowledge the attacker aggregates by spying on the communication outputs. Besides, in our constructor destructor setting we assume that the agents only send and accept meaningful messages, namely terms that verify the msg predicate. While this assumption is realistic for authenticated encryption for example, it may not hold for schemes with weaker security guarantees. In practice the semantics takes the form of a transition relation between extended processes labelled by so-called actions:

1. *Input actions* $\xi_c(\xi_t)$, where $\xi_c$ and $\xi_t$ are recipes, model an input from the attacker of a message (crafted using recipe $\xi_t$) on some channel (known to the attacker using recipe $\xi_c$)

2. *Output actions* $\bar{\xi}_c(\bar{\alpha}x_n)$, where $\bar{\xi}_c$ is a recipe, model an output on a channel (known by the attacker using recipe $\bar{\xi}_c$), recorded into the frame (at pointer $\bar{\alpha}x_n \in \mathcal{AX}$).

3. *Silent actions* $\tau$ that model actions that are unobservable by the attacker such as synchronous private communications or evaluation of a conditional.

We call $\mathcal{A}$ the alphabet of actions, and transitions are of the form $A \xrightarrow{a} B$, $a \in \mathcal{A}$. The transition relation is defined by the rules given in Figure 1. More generally:

**DEFINITION 2.5 (trace).** We write $A \xrightarrow{w} B$ when $A \xrightarrow{a_1} \dots \xrightarrow{a_n} B$ and $w \in \mathcal{A}^*$ is the word obtained after removing the $\tau$ actions from the word $a_1 \dots a_n$, and call such a sequence of transitions a trace. We also write $\tau \Rightarrow \tau^*$, i.e. the reflexive, transitive closure of $\tau$.

Apart from the absence of replication, this semantics aims at being as close as possible to the original semantics of the applied pi calculus [1] although using a different formalism, as it is also the semantics used by tools such as PROVERIF.

**EXAMPLE 2.6.** We now illustrate how our running example can be executed in the operational semantics. We let two agents of respective secret keys $sk_A, sk_B \in \mathcal{N}$. An instance of the protocol between $A$ and $B$ is thus modelled, using the notations of Example 2.3, by the process $P = \bar{A} | \bar{B}$ where, given fresh names $r_A, r_B$:

$$ \bar{A} = X(sk_A, pk(sk_B), N_A, r_A) $$

$$ \bar{B} = B(sk_B, pk(sk_A), N_B, r_B) $$
<figure><img src="image_2.png" /><figcaption>**Figure 1.** Semantics of the calculus</figcaption></figure>

In order to lighten the presentation we use the same notations as in Example 2.3 and name the three messages of the protocol as follows:

$$m_A = \text{aenc}(\langle N_A, \text{pk}(sk_A) \rangle, r_A, \text{pk}(sk_B))$$

$$m_B = \text{aenc}(\langle \text{fst}(t), N_B, \text{pk}(sk_B) \rangle, r_B, \text{pk}(sk_A))$$

$$m'_B = \text{aenc}(N_B, r_B, \text{pk}(sk_B))$$

We assume that the public keys pk(sk<sub>A</sub>) and pk(sk<sub>B</sub>) are known to the attacker, which can be modelled by an initial frame Φ<sub>0</sub> = {ax<sub>1</sub> ↦ pk(sk<sub>A</sub>), ax<sub>2</sub> ↦ pk(sk<sub>B</sub>)} . Another possibility is to prefix the process P with two outputs of pk(sk<sub>A</sub>) and pk(sk<sub>B</sub>) respectively, which will produce the frame Φ<sub>0</sub> after two applications of rule (Out). The normal execution of the process is the following sequence of reduction steps:

<figure><img src="image_3.png" /></figure>

In this execution the attacker only forwards messages, that is, each input action uses the last axiom added to the frame as a recipe. However the adversary may actively engage in the protocol, for example for guessing whether B accepts communications from a third agent C. For that they could generate fresh nonces N, R ∈ F<sub>0</sub> (attacker-generated nonces are modelled by fresh constants) and send the message m'<sub>A</sub> = aenc(⟨N, pk(sk<sub>C</sub>), R, pk(sk<sub>B</sub>)) to check how B
responds. Note that the message $m'_A$ can indeed be crafted by the attacker assuming $\Phi'_0 = \Phi_0 \cup \{ax_3 \mapsto pk(sk_c)\}$ as an initial frame. This scenario corresponds to the following sequence of transitions:

$$ (\{\!\{P\}\!\}, \Phi'_0) \xrightarrow{\tau} (\{\!\{\bar{A}, \bar{B}\}\!\}, \Phi'_0) \\ \qquad \underset{\bar{c}(\langle ax_4 \rangle)}{\overset{c(\mathrm{aenc}(\langle N, ax_3 \rangle, R, ax_2))}{\rightleftharpoons}} (\{\!\{\bar{A}, \bar{c}\langle m'_B \rangle\!\}, \Phi'_0) \\ \qquad \underset{\bar{c}(\langle ax_4 \rangle)}{\overset{\bar{c}\langle ax_4 \rangle}{\rightleftharpoons}} (\{\!\{\bar{A}, 0\}\!\}, \Phi'_0 \cup \{ax_4 \mapsto m'_B\}) $$

This does not leak information to the attacker, assuming they cannot distinguish the messages $m_B$ and $m'_B$. All in all, the set of traces of the process, i.e. the set of all possible sequences of reductions, characterises all possible executions of the protocol in an active adversarial environment. ♦

As a final note, let us observe that the original pi calculus [55] (referred as the *pure pi calculus* in this article) can be seen as a special case of our model. Indeed the fragment without replication is retrieved when $\mathcal{F}_c$, $\mathcal{F}_d$ and $\mathcal{R}$ are empty. This restriction makes the transition relation finitely branching up to bijective renaming of attacker-generated constants.

## 2.3 Security properties

**Against a passive attacker** We first define the notion of *static equivalence* that is often used to model security against a passive attacker in that it is only an equivalence of frames, i.e. it does not involve the operational semantics. It expresses that the knowledge obtained by eavesdropping in two different situations does not permit the attacker to distinguish them. For example no differences can be observed between $\{ax_1 \mapsto k\}$ and $\{ax_1 \mapsto k'\}$ if $k, k' \in \mathcal{N}$ because, intuitively, two fresh nonces look like random bitstrings from an external observer's point of view. However the situation is different with the frames

$$ \Phi = \{ax_1 \mapsto k, ax_2 \mapsto k\} \qquad \Psi = \{ax_1 \mapsto k', ax_2 \mapsto k\} \qquad \text{with } k \neq k' $$

Indeed, even if no differences can be made between $k$ and $k'$ in isolation, the attacker observed two identical messages in the first situation but two different messages in the second situation. In particular we say that the equality test "$ax_1 = ax_2$" distinguishes the two frames (because it holds in $\Phi$ but not in $\Psi$). Besides, in our constructor destructor algebra it is also possible to observe destructor failures. For example the following frames can be distinguished:

$$ \Phi = \{ax_1 \mapsto k, ax_2 \mapsto aenc(m, r, pk(k))\} \qquad \Psi = \{ax_1 \mapsto k', ax_2 \mapsto aenc(m, r, pk(k))\} $$

Indeed crafting the recipe $aenc(ax_2, ax_1)$ (i.e. decrypting the last observed message with the first one) succeeds in the first situation but triggers a decryption failure in the second. Static equivalence has been extensively studied in the literature (see e.g. [2, 39, 16, 42]). Formally:
**DEFINITION 2.7.** Two frames $\Phi$ and $\Psi$ of same domain are statically equivalent, written $\Phi \sim \Psi$, when for all recipes $\xi, \zeta$:

1. $msg(\xi\Phi)$ if and only if $msg(\xi\Psi)$

2. assuming $msg(\xi\Phi)$ and $msg(\zeta\Phi)$, $\xi\Phi\downarrow = \zeta\Phi\downarrow$ if and only if $\xi\Psi\downarrow = \zeta\Psi\downarrow$.

This definition is lifted to extended processes by writing $A \sim B$ instead of $\Phi(A) \sim \Phi(B)$.

**EXAMPLE 2.8.** The fact that the two frames

$$ \Phi = \{ax_1 \mapsto aenc(m, r, pk(k))\} \quad \Psi = \{ax_1 \mapsto k'\} \quad \text{with } m \in \mathcal{F}_0 \text{ and } k, k', r \in \mathcal{N} $$

are statically equivalent intuitively models that encryption makes messages unintelligible (in that the attacker cannot distinguish a ciphertext from a fresh nonce). Naturally this does not hold any more once the decryption key is revealed. Formally: $\Phi \cup \{ax_2 \mapsto k\} \not\supset \Psi \cup \{ax_2 \mapsto k\}$ as witnessed by the recipe $\xi = adec(ax_1, ax_2)$ whose computation succeeds in the first frame but triggers a decryption failure in the second. Without going to the extreme extent of revealing the key, the two situations are also distinguishable if we weaken the cryptographic assumptions on aenc. For example, recalling the considerations of Example 2.1, if we do not suppose the encryption scheme to be *key concealing* anymore by adding the rule

$$ \text{get\_key}(aenc(x, y, pk(z))) \to pk(z) $$

then $\Phi$ and $\Psi$ are distinguished by the recipe $\text{get\_key}(ax_1)$ whose destructor succeeds in $\Phi$ but fails in $\Psi$. The same fact would arise using the weaker rewrite rule

$$ \text{test\_aenc}(aenc(x, y, pk(z))) \to \text{ok} $$

that tests whether a bitstring is a ciphertext.

<figure><img src="image_4.png" /></figure>

**Against an active attacker** Dynamic extensions of static equivalence consider distinguishability for an attacker interacting actively with protocols. Consider for example a protocol modelled by a process $P$ manipulating a nonce $k$. A possible model of the secrecy of $k$ can be formalised by a non-interference statement: there is no observable difference in the behaviour of the protocol when $k$ is replaced by another term. In this article we study several relations modelling the underlying notion of indistinguishability. For completeness, we also present their associated pre-orders that can be useful modelling tools in situations where only inclusion relations are to be expressed.

**DEFINITION 2.9 (Trace equivalence).** If $A$ and $B$ are extended processes, we write $A \sqsubseteq_t B$ when for all traces $A \xrightarrow{\text{tr}} A'$, there exists a trace $B \xrightarrow{\text{tr}} B'$ such that $A' \sim B'$. We say that $A$ and $B$ are *trace equivalent*, written $A \approx_t B$, when $A \sqsubseteq_t B$ and $B \sqsubseteq_t A$.

**DEFINITION 2.10 (Simulation, (Bi)similarity).** A labelled simulation (or simply simulation) is a relation $\mathcal{R}$ such that for all extended processes $A, B, A \mathcal{R} B$ entails
1. $A \sim B$

2. for all transitions $A \xrightarrow{\alpha} A'$, there exists a trace $B \xrightarrow{\alpha} B'$ such that $A' \mathcal{R} B'$

We call $\sqsubseteq_s$ (simulation preorder) the largest simulation, and $\approx_s$ (labelled similarity, or simply similarity) the relation $\sqsubseteq_s \cap \sqsupseteq_s$. Bisimilarity $\approx_b$ is the largest symmetric simulation.

Note in particular that

$$ \approx_b \subset \approx_s \subset \approx_t $$

i.e. two bisimilar processes are always similar, and two similar processes are always trace equivalent. These equivalences are well established as means to express security properties [4, 1]. Trace equivalence has been studied intensively for security protocols [28, 7, 29, 31] while, for example, labelled bisimilarity is used as a characterisation for observational equivalence [1].

Each equivalence implies slightly different adversaries. As shown in [29], $\approx_t$ characterizes may-testing, i.e., equivalence in the presence of an arbitrary adversarial process running in parallel. $\approx_b$ characterizes observational equivalence [1] and considers a more adaptive adversary; $\approx_b$ was also introduced as a proof technique for may-testing in [4]. Finally, it was recently shown [30] that $\approx_s$ characterizes a may-testing equivalence in the presence of a probabilistic adversary, i.e. an adversarial process that is allowed to branch probabilistically.

**EXAMPLE 2.11.** We refer again to the processes modelling the Private Authentication protocol as described in Example 2.3. We let for instance the processes $P_a = B(sk_B, pk(sk_A), N_B, r_B)$ and $P_c = B(sk_B, pk(sk_C), N_B, r_B)$ modelling the role of $B$ accepting connections from $A$ and $C$, respectively. We want to verify whether an adversary would be able to distinguish the two situations. This could be modelled for example by

$$ (\{P_a\}, \Phi_0) \approx_t (\{P_c\}, \Phi_0) \quad \text{with} \quad \Phi_0 = \{\text{ax}_1 \mapsto \text{pk}(sk_A), \text{ax}_2 \mapsto \text{pk}(sk_B), \text{ax}_3 \mapsto \text{pk}(sk_C)\} $$

The initial frame $\Phi_0$ models that the attacker knows the public keys of all agents. It appears that this equivalence statement holds, the core argument being that for all messages $u_1, u_2, r_1, r_2$ and $pk_1, pk_2 \in \{\text{pk}(sk_A), \text{pk}(sk_B), \text{pk}(sk_C)\}$, the following frames are statically equivalent:

$$ \Phi_0 \cup \{\text{ax}_4 \mapsto \text{aenc}(u_1, r_1, pk_1)\} \qquad \Phi_0 \cup \{\text{ax}_4 \mapsto \text{aenc}(u_2, r_2, pk_2)\} $$

In particular this equivalence statement still holds if we weaken the cryptographic assumptions on aenc by assuming that a ciphertext is distinguishable from an arbitrary term, which is modelled by adding the rewrite rule test_aenc(aenc(x, y, pk(z))) $\rightarrow$ ok. However trace equivalence is violated if we add the rule get_key(aenc(x, y, pk(z))) $\rightarrow$ pk(z). A possible attack trace is, with $N, R \in \mathcal{F}_0$:

$$ (\{P_a\}, \Phi_0) \underset{\bar{c}\langle ax_4 \rangle}{\overset{c(aenc(\langle N, ax_1 \rangle, R, ax_2))}{\rightleftharpoons}} (\{\bar{c}\langle u \rangle\}, \Phi_0) \quad \text{with } u = \text{aenc}(\langle N, N_B, \text{pk}(sk_B) \rangle, r_B, \text{pk}(sk_A)) \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{with } \Phi = \Phi_0 \cup \{\text{ax}_4 \mapsto u\} $$
Indeed there is only one trace in the other process taking the same actions:

$$ (\{P_c\}, \Phi_0) \underset{\bar{c}\langle ax_4 \rangle}{\overset{c(aenc(\langle N, ax_1 \rangle, R, ax_2))}{\rightleftharpoons}} (\{\bar{c}\langle v \rangle\}, \Phi_0) \quad \text{with } v = aenc(N_B, r_B, \text{pk}(sk_B)) \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{with } \Psi = \Phi_0 \cup \{ax_4 \mapsto v\} $$

and $\Phi \nmid \Psi$ because the recipe $\xi = \text{get_key}(ax_4)$ is evaluated to $\text{pk}(sk_A)$ in $\Phi$ and to $\text{pk}(sk_B)$ in $\Psi$. That is, the recipes $\xi$ and $\zeta = ax_1$ are equal in $\Phi$ but not in $\Psi$. ♦

**In practice: security goals for Private Authentication** We now demonstrate in more details how equivalence properties can be used to model security in practical scenarios through a complete case study. We model the three security goals of the Private Authentication Protocol described in Example 2.3. For simplicity we present the simplest scenario of a single session of the protocol in this section (i.e. only one instance of the roles of A and B communicating in parallel). Of course a more extensive analysis needs to consider more parallel sessions. In the following we write $pk_X$ and $sk_X$ the public and private keys of an identity X and

$$ P(A, C, N_A, r_A, B, D, N_B, r_B) = X(sk_A, pk_C, N_A, r_A) | B(sk_B, pk_D, N_B, r_B) $$

the process that runs in parallel the roles of A attempting to initiate a communication with C and B accepting a connection from a unique identity D. We assume an initial frame $\Phi_0$ that contains the public keys of all identities involved in the process.

The security goals state that the protocol should conceal the identities of the participants (including C the recipient of A and D the connection accepted by B) and the values of the exchanged nonces. A possible formalisation is that there should not be any observable difference in $P(A, C, N_A, r_A, B, D, N_B, r_B)$ when replacing the identities by others and $N_A, N_B$ by any other value. That is, for all identities A, B, C, D, A', B', C', D', all terms $N_A, N_B, N'_A, N'_B$, and fresh names $r_A, r_B$,

$$ (\{P(A, C, N_A, r_A, B, D, N_B, r_B)\}, \Phi_0) \approx (\{P(A', C', N'_A, r_A, B', D', N'_B, r_B)\}, \Phi_0) $$

where $\approx$ is either $\approx_t$, $\approx_s$ or $\approx_b$ and $\Phi_0$ is a frame whose image contains the public keys of all identities involved. This models a form of non-interference property and has been called *strong secrecy* in [18].

## 2.4 Complexity and decision problems

So far we detailed how process equivalences can be used to model privacy preservation in security protocols. Our goal in this article is to present decidability and complexity results for static equivalence, trace equivalence and labelled bisimilarity.

**On sizes** Before going further we need to clarify the notion of size of the inputs since it plays a central role in complexity analyses. This is particularly important for our purpose since there
exist several conventions for representing terms. The tree size of term $t$ refers to its number of symbols and is written $|t|$. It corresponds to a classical representation of a term as a tree. On the other hand some of our complexity results are stated w.r.t. a succinct representation of terms as Directed Acyclic Graphs (DAG) with maximal sharing (which may be exponentially more concise). If $st(t)$ is the set of subterms of $t$, the DAG size of $t$ refers to the cardinality $|st(t)|$ and is written $|t|_{dag}$. This definition is lifted to sets and sequences of terms with the sharing common to all elements of the structure. The size of a signature $\mathcal{F}$ is the sum of the arities of the symbols of $\mathcal{F}$ (which is finite since $\mathcal{F}_c$ and $\mathcal{F}_d$ are finite) and the size of a rewrite system $\mathcal{R}$ is the sum of the sizes of the two hand sides of its rules. The size of a process is the sum of the number of operators of the process and of the sizes of all terms appearing in the process (in conditionals, channels, and output terms). We emphasise that

- A complexity upper bound stated w.r.t. the DAG size of the inputs is a stronger result than the same upper bound stated w.r.t. the tree size.

- On the contrary a complexity lower bound stated in DAG size is a weaker result than the corresponding result in tree size.

In this article we only address the strongest configurations: lower bounds in the tree representation of terms, upper bounds in DAG.

**Complexity classes** We now shortly remind some background about complexity, mainly introducing our notations. Given $f: \mathbb{N} \to \mathbb{N}$, we define $TIME(f)$ (resp. $SPACE(f)$) the class of problems decidable by a deterministic Turing machine running in time (resp. in space) at most $f(n)$ where $n$ is the size of the parameters of the problem. It is common to define the following classes:

$$ \text{LOGSPACE} = \bigcup_{p \in \mathbb{N}} \text{SPACE}(\log(n^p)) $$

$$ \text{PTIME} = \bigcup_{p \in \mathbb{N}} \text{TIME}(n^p) $$

$$ \text{PSPACE} = \bigcup_{p \in \mathbb{N}} \text{SPACE}(n^p) $$

$$ \text{EXPTIME} = \bigcup_{p \in \mathbb{N}} \text{TIME}(2^{n^p}) $$

One can define their non-deterministic counterparts NLOGSPACE (NL for short), NPTIME, NPSPACE and NEXPTIME. Given a (non-deterministic) class $C$, we call co-$C$ the class of problems whose negation is in $C$. From now on we often omit the suffix TIME in the name of time complexity classes for the sake of succinctness. Then it is known that:

$$ \text{LOGSPACE} \subseteq \text{NL} = \text{coNL} \subseteq \text{P} \subseteq \text{NP}, \text{coNP} \subseteq \text{PSPACE} = \text{NPSPACE} \subseteq \text{EXP} \subseteq \text{NEXP}, \text{coNEXP} $$

To define complete problems for complexity classes above PTIME we use classical *many-to-one polytime reductions*. We also mention the notion of *oracle reduction*, deciding a problem with a constant-time black box for another problem: the class of problems decidable in $C$ with an oracle for a problem $Q$ is noted $C^Q$. When $Q$ is complete for a class $\mathcal{D}$ w.r.t. a notion of reduction executable in $C$, we may write $C^\mathcal{D}$ instead; in particular $C^\mathcal{D} = C^{\text{co}\mathcal{D}}$. This kind of reduction is
needed to define the last complexity classes we will use in this article: the *polynomial hierarchy*, which is a collection of complexity classes between PTIME and PSPACE. Indeed the difference between NP and PSPACE lies in their capacity to express quantifier alternation; the usual complete problems considered for these two complexity classes are, given a boolean formula $\varphi$:

- SAT (NP complete): does $\exists x_1, \dots, x_n. \varphi(x_1, \dots, x_n)$ hold?

- QBF (PSPACE complete): does $\forall x_1, \exists y_1, \dots, \forall x_n, \exists y_n. \varphi(x_1, y_1, \dots, x_n, y_n)$ hold?

The polynomial hierarchy characterises all classes corresponding to intermediate alternations.

**DEFINITION 2.12.** The polynomial hierarchy PH consists of the classes $\Sigma_n$ defined by $\Sigma_0 = \text{PTIME}$ and $\Sigma_{i+1} = \text{NP}^{\Sigma_i}$. In particular, $\Sigma_1 = \text{NP}$. We also write $\Pi_i$ for $\text{co}\Sigma_i$.

**Problems studied in this article** We thus study the following decision problems:

**STATEQ:**

- **INPUT:** A rewriting system $\mathcal{R}$, two frames $\Phi$ and $\Psi$.

- **QUESTION:** $\Phi \sim \Psi$ for $\mathcal{R}$?

**TRACEEQ:**

- **INPUT:** A rewriting system $\mathcal{R}$, two processes $P$ and $Q$.

- **QUESTION:** $(\{P\}, \emptyset) \approx_t (\{Q\}, \emptyset)$ for $\mathcal{R}$?

We also consider TRACEINCL, SIMULATION, SIMILARITY, BISIMILARITY to be the analogue problems of TRACEEQ, replacing trace equivalence by the relations $\sqsubseteq_t$, $\sqsubseteq_s$, $\approx_s$, and $\approx_b$, respectively. As we explained previously these problems are undecidable in general and we need to put restrictions on the inputs, in addition to the restriction to a bounded number of sessions, which is inherent to our model. Typically our results all include the restriction (inherent to our model) to constructor destructor theories and bounded processes. When we say for example that “TRACEEQ is decidable for constructor destructor subterm convergent rewriting systems” it means that we are studying the following decision problem:

- **INPUT:** A constructor destructor subterm convergent rewriting system $\mathcal{R}$, two processes $P$ and $Q$.

- **QUESTION:** Are $P$ and $Q$ trace equivalent (for $\mathcal{R}$)?

The way we state the problem implies that complexity analyses need to account for the size of all inputs, including the rewriting system. However the treatment of this question is not uniform in the literature. Complexity analyses in [2, 15, 29] consider the rewriting system as a constant of the problem. For the example above this means considering, for each constructor destructor subterm convergent rewriting system $\mathcal{R}$, the following decision problem:

- **INPUT:** Two bounded processes $P$ and $Q$.

- **QUESTION:** Are $P$ and $Q$ trace equivalent (for $\mathcal{R}$)?
For this formulation of the problem, generic completeness results w.r.t. complexity classes are not possible in general because different complexities may arise for each rewriting system $\mathcal{R}$. This is for example the case in [2], where STATEQ is proven PTIME for any fixed subterm convergent rewriting system: the problem is indeed PTIME-hard for some of them [34] but also LOGSPACE for others as we prove it in this article. All existing procedures [2, 39, 42] are actually exponential in the size of the rewriting system. This is why we refer to this problem as *parametric equivalence* and say by opposition that *general equivalence* is the initial variant with the rewriting system considered as part of the input. We argue that the latter is more relevant today as the rewriting system can now be specified by the user in many automated tools. This motivated for example to prove in [34] that the complexity results of [15, 29] (stated in the parametric setting) were also valid in the general setting.

# 3. Structure of the decision procedure

We detail in this section our overall decision procedure for equivalence properties, intuitively reducing them to solving some forms of symbolic constraints. We express this through a novel notion of *partition tree* that crisply characterises equivalence proofs. We formalise in this section the main properties of this tree and describe how to derive an actual decision procedure from it; the constraint solving procedure necessary to generate the tree itself is then later detailed in Section 4.

## 3.1 The symbolic approach for decidability

Our decision procedures rely on a *symbolic semantics*, by opposition to the usual semantics of the calculus (recall Figure 1) that we will call the *concrete semantics* from now on. Specifically, rather than fetching concrete input terms from the active attacker, our symbolic semantics abstract these inputs and only record the constraints they should satisfy to execute the protocol. This thus provides a finite representation of the infinite set of actions potentially available to the attacker. For example let $c \in \mathcal{F}_0$, $h/1 \in \mathcal{F}_c$, $k \in \mathcal{N}$ and consider the process

$$P = \bar{c}\langle k \rangle . c(x). \text{ if } \text{fst}(x) = k \text{ then } \bar{c}\langle h(x) \rangle$$

The trace executing the output $h(x)$ will gather constraints that intuitively indicate that: 1. $x$ is a term deducible by the attacker from the frame $\{ax_1 \mapsto k\}$; and 2. $x = \langle k, y \rangle$ for some term $y$. A constraint solving algorithm, detailed in Section 4.2, can then be used to show that these constraints have a *solution*: the recipe $\xi = \langle ax_1, a \rangle$, $a \in \mathcal{F}_0$, can be used to compute the input term $x$ and satisfy the constraints, which justifies that the output of $h(x)$ is reachable. Similar approaches are common to decide reachability or equivalence properties of bounded
processes [15, 29]; our approach is however more widely applicable due to our absence of syntactic restrictions on processes.

**Formalising symbolic constraints** We first introduce a new type of variables, used in recipes:

**DEFINITION 3.1 (second-order terms).** We consider a partition of the set of (non-axiom) variables $\mathcal{X} \setminus \mathcal{AX} = \mathcal{X}^1 \uplus \mathcal{X}^2$. The elements of $\mathcal{X}^1$ are called *first-order variables* and correspond to those we used so far in terms (in processes, frames, rewrite rules). Those of $\mathcal{X}^2$ are called *second-order variables* and are used to represent an undefined recipe. A *first-order term* is an element of $\mathcal{T}(\mathcal{F} \cup \mathcal{F}_0 \cup \mathcal{N} \cup \mathcal{X}^1)$ and a *second-order term* is an element of $\mathcal{T}(\mathcal{F} \cup \mathcal{F}_0 \cup \mathcal{AX} \cup \mathcal{X}^2)$.

We now distinguish $vars^1(u) = vars(u) \cap \mathcal{X}^1$, $vars^2(u) = vars(u) \cap \mathcal{X}^2$, and $axioms(u) = vars(u) \cap \mathcal{AX}$. Note that we say that a second-order term $t$ is ground if $vars^2(t) = \emptyset$, i.e., $t$ may contain axioms. By definition, a recipe is therefore a ground second-order term. We also adapt the other notations of the term algebra to reflect the separation: $st^1, st^2, ...$

In practice, when executing an input instruction $c(x)$ in the symbolic semantics, $x$ will be associated to a fresh second-order variable written $X:i$, where $X \in \mathcal{X}^2$ will serve as a placeholder for the recipe used to compute $x$, and $i \in \mathbb{N}$ indicates that only the first $i$ axioms of the frame are available to compute the recipe in question. This is formalised by the following, natural extension of the notion of substitution:

**DEFINITION 3.2 (second-order substitutions).** We suppose a partition $\mathcal{X}^2 = \biguplus_{i \in \mathbb{N}} \mathcal{X}_{=i}^2$ where each class $\mathcal{X}_{=i}^2$ is infinite. We also write $\mathcal{X}_{\leq i}^2 = \bigcup_{j=0}^i \mathcal{X}_{=j}^2$. If $X$ is a second-order variable we may write $X:i$ to emphasise that $X \in \mathcal{X}_{=i}^2$ and say in this case that $X$ is of type $i$. A *second-order substitution* is then a substitution $\Sigma$ of domain $dom(\Sigma) \subseteq \mathcal{X}^2$ that *respects types*:

$$ \forall X:i \in dom(\Sigma), X\Sigma \in \mathcal{T}_i^2 \quad \text{where} \quad \mathcal{T}_i^2 = \mathcal{T}(\mathcal{F} \cup \mathcal{F}_0 \cup \mathcal{X}_{\leq i}^2 \cup \{\text{ax}_1, \dots, \text{ax}_i\}) $$

Altogether, we can then define the constraints that we use to characterise the possible values that an input term $x$ may take:

**DEFINITION 3.3 (atoms).** We consider the following three kinds of atoms:

1. *deduction fact* $\xi \vdash^? u$ where $u$ is a message in normal form and $\xi$ is a second-order term such that $\text{root}(\xi) \notin \mathcal{F}_c$;

2. *second-order equations* $\xi =^? \zeta$ where $\xi$ and $\zeta$ are two second-order terms;

3. *(first-order) equations* $u =^? v$ where $u$ and $v$ are two first-order terms (not necessarily messages).

The negation $\neg(\alpha =^? \beta)$ of an equation is written $\alpha \neq^? \beta$ and called a *disequation*.

**DEFINITION 3.4 (constraint).** An *atomic constraint* (or an *atomic formula*) is an atom that is either a deduction fact, a second-order equation, or a first-order equation $u =^? v$ where $u$ and $v$
are constructor terms. A *constraint* is then a first-order formula over atomic constraints, that is, either an atomic constraint, $\top$, $\bot$, or of the form $\varphi \wedge \psi, \varphi \vee \psi, \neg \varphi, \forall x. \varphi$, or $\forall X:n. \varphi$ for $\varphi, \psi$ constraints. Note that $\mathrm{vars}(\varphi)$ then refers to the *free variables* of the constraint $\varphi$.

A deduction fact $\xi \vdash? u$ indicates that term $u$ is deducible by the recipe $\xi$ and second-order equations $\xi =? \zeta$ are used to put restrictions on which recipes $\xi$ may be used to do so. For example $X:i \vdash? x$ states that the variable $x$ is to be replaced by a term deducible by the attacker using at most the $i$ first outputs of the frame; a constraint solving procedure may then impose that $\exists Y:i. X =? f(Y)$, i.e., that the underlying recipe should have a $f$ symbol at its root. Equations reflect the syntactic equalities that the first-order terms verify. Typically when executing if $fst(x) = t$ then *P* else *Q*, the positive branch will intuitively lead to the constraint $\exists y. x =? \langle t, y \rangle$ and the negative branch to $\forall y. x \neq? \langle t, y \rangle$.

**Constraint systems** Finally we define and give some properties of *constraint systems* that are used to collect the first-order constraints induced by a given execution of a process.

**DEFINITION 3.5 (constraint system).** A *constraint system* is a triple $C = (\Phi, D, E^1)$ whose elements are of the following form:

1. $\Phi = \{ax_1 \mapsto t_1, \dots, ax_n \mapsto t_n\}$ is a frame (not necessarily ground)

2. D is a set of constraints of the form $X \vdash? x$, with $X \in \mathcal{X}_{\le n}^2$, $x \in \mathcal{X}^1$. We also require the *origination property*: for all $i \in [1, n]$, for all $x \in \mathrm{vars}(t_i)$, there exists $X \in \mathcal{X}_{i-1}^2$ such that $(X \vdash? x) \in D$.

3. $E^1$ is a set of constraints of the form $u =? v$ or $\forall z_1 \dots \forall z_k. \bigvee_{j=1}^r u_j \neq? v_j$.

The components of $C$ are also written $\Phi(C)$, $D(C)$ and $E^1(C)$. The set $D$ contains all input binders $x$ that have been executed, each mapped to a second-order variable $X$ that will serve as a placeholder for the corresponding recipe. Next the origination property expresses that when reference is made to an input $x$ in an output $t_i$, this input should be computed only from the previous outputs $t_1, \dots, t_{i-1}$. This is a natural invariant preventing cyclic input-output dependencies, always satisfied in practice. Finally $E^1$ is a set of (dis)equalities imposed on the protocol messages by conditionals, among others. We will formalise in Section 3.3 the semantics of these constraints through a notion of *solution*.

**REMARK 3.6 (notational conventions).** We use several convenient notations throughout the article to lighten the presentation of constraints. First of all we do not make a difference between sets and conjunctions of constraints: for instance we may write $E^1 = \bigwedge_{i=1}^n \varphi_i$ instead of $E^1 = \{\varphi_i\}_{i=1}^n$ and conversely. We also interpret a substitution $\sigma$ as the set of equations $\mathcal{E} = \{x =? x\sigma | x \in \mathrm{dom}(\sigma)\}$.
## 3.2 (Most general) unifiers

We now recall some basics on term unification, a key concept in symbolic models that has some specificities in our context, in particular regarding second-order terms.

**Unification of first-order terms** Two first-order terms $u$ and $v$ are *unifiable* if there exists a substitution $\sigma$, called a *unifier*, such that $u\sigma = v\sigma$. For example the terms $u = \langle sdec(x, y), z \rangle$ and $v = \langle z_1, z_2 \rangle$ are unified by $\sigma = \{z_1 \mapsto sdec(x, y), z_2 \mapsto z\}$. The terms $u$ and $z'$ are unifiable as well using $\sigma = \{z' \mapsto u\}$, but the terms $u$ and $z$ are not. More generally, a unifier $\sigma$ of a set of equations $\mathcal{E} = \{u_i =? v_i\}_{i=1}^n$ is a unifier of $u_i$ and $v_i$ for all $i$. A classical characterisation of the set of unifiers of two terms is based on *most general unifiers*:

**DEFINITION 3.7 (most general unifier).** A unifier $\sigma$ of $\mathcal{E}$ is said to be a *most general* one if, for any $\theta$ unifier of $\mathcal{E}$, there exists $\tau$ such that $\theta = \sigma\tau$. In this case, we write $\sigma = \text{mgu}(\mathcal{E})$ (and it is unique up to variable renaming). When $\mathcal{E}$ is not unifiable, we write $\text{mgu}(\mathcal{E}) = \perp$.

A straightforward inductive procedure allows to decide whether $\mathcal{E}$ is unifiable and, if it is, to compute $\text{mgu}(\mathcal{E})$. We assume w.l.o.g. that this computation does not introduce variables, that is, if $\sigma = \text{mgu}(\mathcal{E})$ then $\text{dom}(\sigma) \cup \text{vars}(\text{img}(\sigma)) \subseteq \text{vars}(\mathcal{E})$. We also require that $\text{dom}(\sigma) \cap \text{vars}(\text{img}(\sigma)) = \emptyset$, that is, applying a mgu twice has no more effect than applying it once. Note as well that all unifiers are instances of the mgu but the converse is also true, that is, all instances of a mgu are unifiers. By convenience we also write $\text{mgu}(\mathcal{E})$ in the case where $\mathcal{E}$ contains disequations (typically when writing $\text{mgu}(\text{E}^1(\mathcal{C}))$): in this case only equations are taken into account and nothing ensures that the mgu satisfies the disequations of $\mathcal{E}$.

However mgu's are only syntactic: when taking the rewriting system $\mathcal{R}$ into account we say that $\sigma$ is a *unifier modulo theory of $\mathcal{E}$* when for all $(u =? v) \in \mathcal{E}$, $u\sigma \downarrow = v\sigma \downarrow$. A standard procedure based on narrowing (not detailed here) allows to compute *most general unifiers modulo $\mathcal{R}$* when $\mathcal{R}$ is subterm convergent among others [41]. However unlike the syntactic case they are not unique in general:

**DEFINITION 3.8 (most general unifier modulo theory).** We let $\mathcal{E}$ be a set of equations and $\mathcal{R}$ be a convergent rewriting system. A set of *most general unifiers modulo $\mathcal{R}$* is a set of substitutions $\text{mgu}_{\mathcal{R}}(\mathcal{E})$ that verifies the following properties:

1. for all $\sigma \in \text{mgu}_{\mathcal{R}}(\mathcal{E})$, $\sigma$ is a unifier of $\mathcal{E}$ modulo $\mathcal{R}$

2. for all $\theta$ unifier of $\mathcal{E}$ modulo $\mathcal{R}$, there exists $\sigma \in \text{mgu}_{\mathcal{R}}(\mathcal{E})$ and a substitution $\tau$ such that for all $x \in \text{vars}(\mathcal{E})$, $x\theta \downarrow = x\sigma\tau\downarrow$

Again we emphasise that equality modulo $\mathcal{R}$ only operates on valid messages, that is, if $\sigma \in \text{mgu}_{\mathcal{R}}(u =? v)$ then $u\sigma$ and $v\sigma$ verify the msg predicate. A typical use case we consider in the symbolic semantics is $\text{mgu}_{\mathcal{R}}(u =? u)$, which is the most general substitution $\sigma$ such that
msg(uσ) holds (if any). For example if $u = \text{adec}(x, y)$ we have $\text{mgu}_\mathcal{R}(u =? u) = \{\sigma\}$, where:

$$ \sigma = \{x \mapsto \text{aenc}(x', x_r, \text{pk}(y')); y \mapsto y'\} \qquad x', x_r, y' \in \mathcal{X} \text{ fresh} $$

This example also highlights that, unlike the syntactic case, computing mgu's modulo theory may require to introduce new variables. This also makes it possible to enforce that $\text{dom}(\sigma) \cap \text{vars}(\text{img}(\sigma)) = \emptyset$.

**Unification of second-order terms** Intuitively, the unification of two second-order terms $\xi$ and $\zeta$ modulo theory means that they deduce the same first-order term $u$ w.r.t. a given frame $\Phi$. This unusual kind of unification is performed as a part of our constraint solving algorithm using a dedicated kind of constraint written $\xi =?_{f} \zeta$, detailed in Section 4.1.1. However, even the computation of syntactic mgu's has some subtleties for second-order terms that we discuss below.

As in the first-order case, a syntactic unifier of $\xi$ and $\zeta$ is a second-order substitution $\Sigma$ such that $\xi\Sigma = \zeta\Sigma$. However, computing $\Sigma$ is not as simple as usual due to the variable types. Indeed, we recall that by definition, a second-order substitution has to respect types, that is, a variable $X:n$ cannot be mapped to a term containing axioms $ax_i$ or variables $Y:i$ if $i > n$. Say for instance we want to unify the two second-order terms $X:1$ and $f(Y:2)$: a regular computation of the mgu would yield the substitution $\Sigma = \{X \mapsto f(Y)\}$, which does not respect the type of $X$. In this case, one solution is to introduce a fresh variable $Z:1$ and to choose the following unifier:

$$ \text{mgu}(X =? f(Y)) = \{X \mapsto f(Z), Y \mapsto Z\} = \Sigma\{Y \mapsto Z\}. $$

Given a second-order term $\xi$, let us write $\#(\xi)$ the maximal type of second-order variables and axioms appearing in $\xi$, that is, the minimal type $i$ such that $\xi \in \mathcal{T}_i^2$. Formally,

$$ \#(\xi) = \min\{i \in \mathbb{N} \mid \xi \in \mathcal{T}_i^2\}. $$

The mgu of a conjunction of equations $\varphi$ is then computed inductively as follows:

$$ \text{mgu}(\top) = \top $$

$$ \text{mgu}(\varphi \wedge f(\xi_1, \dots, \xi_n) =? g(\zeta_1, \dots, \zeta_n)) = \begin{cases} \bot & \text{if } f \neq g \\ \text{mgu}(\varphi \wedge \bigwedge_{i=1}^n \xi_i =? \zeta_i) & \text{if } f = g \end{cases} \\ \text{mgu}(\varphi \wedge X:i =? \xi) = \begin{cases} \bot & \text{if } X \in \text{vars}^2(\xi) \text{ and } \xi \neq X \\ \bot & \text{else if } \exists ax_j \in \text{axioms}(\xi), j > i \\ \Sigma_0\Sigma & \text{else if } \xi \notin \mathcal{X}^2, Y:j \in \text{vars}^2(\xi), j > i, Z:i \text{ fresh and} \\ & \text{with } \Sigma_0 = \{Y \mapsto Z\} \text{ and } \Sigma = \text{mgu}(\varphi\Sigma_0 \wedge X:i =? \xi\Sigma_0) \\ \Sigma_0\Sigma & \text{else if } \#(\xi) \le i, \text{ with } \Sigma_0 = \{X \mapsto \xi\} \text{ and } \Sigma = \text{mgu}(\varphi\Sigma_0) \end{cases} $$
As before we extend this notation to arbitrary sets $\mathcal{E}$, that is, we may write $mgu(\mathcal{E})$ even if $\mathcal{E}$ contains disequations (which are then ignored during the computation). The correctness of this function is proved below.

**PROPOSITION 3.9 (correctness of second-order mgu's).** For all sets of second-order equations $\mathcal{E}$, the computation of $mgu(\mathcal{E})$ terminates. Besides we have that $mgu(\mathcal{E}) = \perp$ iff there exist no unifiers of $\mathcal{E}$. When $mgu(\mathcal{E}) \neq \perp$, we have that:

1. $mgu(\mathcal{E})$ is a second-order substitution, i.e., it respects types, and it is a unifier of $\mathcal{E}$;

2. for all unifiers $\Sigma$ of $\mathcal{E}$, there exists a second-order substitution $\Sigma_0$ such that $\Sigma = mgu(\mathcal{E})\Sigma_0$.

**PROOF.** We only prove the termination since all other properties can be proved separately by straightforward inductions on the definition of $mgu$. We let the partial ordering on second order variables $\ll$ given by the types, i.e. $X:i \ll Y:j$ iff $i \leq j$. Given a set of second-order equations $\mathcal{E}$ we then let

$$ \mu(\mathcal{E}) = (\text{vars}^2(\mathcal{E}), M(\mathcal{E}), F(\mathcal{E})) $$

where $M(\mathcal{E})$ is the multiset of variables of $\mathcal{E}$, i.e. multiplicity included, and $F(\mathcal{E})$ is the multiset of the sizes of the equations of $\mathcal{E}$ (where the size of $\xi =? \zeta$ is the number of function symbols in $\xi$ and $\zeta$). The first two components are ordered w.r.t. the multiset extension of $\ll$, and the third one w.r.t. the multiset extension of $\leq$. The overall tuple is ordered w.r.t. the lexicographic composition of the three components.

If we number from 1 to 7 the axioms defining $mgu$, we can show that $\mu$ decreases at each recursive call: (1), (2), (4) and (5) make no recursive calls; (3) preserves $\text{vars}^2$ and $M$, and makes $F$ decrease; (6) replaces all occurrences of $Y$ with $Z$ that has a lower type which makes $\text{vars}^2$ decrease. Regarding (7) two cases can arise: either $\xi = X$ or $X \notin \text{vars}^2(\xi)$. In the first case $\text{vars}^2$ is non increasing and $M$ is decreasing since two occurrences of $X$ are removed and the rest of the formula $\mathcal{E}$ is left unchanged. In the second case $\text{vars}^2$ is decreasing since all occurrences of $X$ are removed and no variables are added. ■

## 3.3 (Most general) solutions

**Solutions** Let us now formalise the semantics of constraints. Given a constraint $\varphi$, a frame $\Phi$ and second- and first-order substitutions $\Sigma$ and $\sigma$ we define the predicate $(\Phi, \Sigma, \sigma) \models \varphi$ by:

$$ (\Phi, \Sigma, \sigma) \models \xi \vdash^? u \quad \text{iff} \quad \xi\Sigma\Phi\sigma\downarrow = u\sigma\downarrow $$

$$ (\Phi, \Sigma, \sigma) \models \xi =? \zeta \quad \text{iff} \quad \xi\Sigma = \zeta\Sigma $$

$$ (\Phi, \Sigma, \sigma) \models u =? v \quad \text{iff} \quad u\sigma = v\sigma $$

$$ (\Phi, \Sigma, \sigma) \models \forall x. \varphi \quad \text{iff} \quad \text{for all first-order ground terms } t, (\Phi, \Sigma, \sigma) \models \varphi\{x \mapsto t\} $$

$$ (\Phi, \Sigma, \sigma) \models \forall X:n. \varphi \quad \text{iff} \quad \text{for all } \xi \in \mathcal{T}_n^2, (\Phi, \Sigma, \sigma) \models \varphi\{X \mapsto \xi\} $$

The definition is extended with logical connectives $\neg$, $\wedge$, $\vee$, ... in the natural way. By convention, writing $(\Phi, \Sigma, \sigma) \models \varphi$ implicitly assumes that, for all $x \in \text{vars}^1(\varphi)$ and $X \in \text{vars}^2(\varphi)$, $x\sigma$ and
$X\Sigma\Phi\sigma$ are ground. Intuitively the second-order substitution $\Sigma$ describes which recipes are used to deduce each input term appearing in $\varphi$, while $\sigma$ gives the actual values of these inputs.

**DEFINITION 3.10 (solution of a constraint system).** We say that $(\Sigma, \sigma)$ is a solution of $C$ if $dom(\Sigma) = vars^2(C)$, $dom(\sigma) = vars^1(C)$ and $(\Phi(C), \Sigma, \sigma) \models D(C) \wedge E^1(C)$. We call $\Sigma$ a second-order solution of $C$ and $\sigma$ its first-order solution. The set of solutions of $C$ is written $Sol(C)$.

The solutions of a constraint system $C$ indicate how the inputs of $C$ (i.e., $vars^1(D(C))$) can be computed while satisfying the constraints imposed by $E^1(C)$. Due to the origination property, the values the first-order solution $\sigma$ takes on $vars^1(D(C))$ is uniquely determined by which recipes are used to deduce terms, i.e., by the second-order solution $\Sigma$.

**EXAMPLE 3.11.** Consider again the example $P = \bar{c}\langle k \rangle$. $c(x)$. if $fst(x) = k$ then $\bar{c}\langle h(x) \rangle$. The traces performing the final output $h(x)$ are characterised by the constraint system

$$ \Phi(C) = \{ax_1 \mapsto k, ax_2 \mapsto h(x)\} \qquad D(C) = \{X \vdash^? x\} \qquad E^1(C) = \{x =? \langle k, y \rangle\} $$

where $X:1$ and $y$ are fresh second- and first-order variables, respectively. Observe in particular that the informal constraint "there exists a term $y$ such that $x = \langle k, y \rangle$" is not formalised using an explicit $\exists$ quantification but with a free variable $y$. All second-order solutions of $C$ are instances of $\Sigma_0 = \{X \mapsto \langle ax_1, Y \rangle\}$ where $Y:1$ is fresh, for example, $\Sigma = \{X \mapsto \langle ax_1, a \rangle\}$ with $a \in \mathcal{F}_0$. The corresponding first-order solution is then $\sigma = \{x \mapsto \langle k, a \rangle, y \mapsto a\}$. ♦

**Most general solutions** Similarly to mgu's, we now introduce a novel characterisation of solutions as instances of so-called most general solutions (mgs). The definition is parametrised with a predicate $\pi$ on second-order substitutions, writing $Sol^\pi(C) = \{(\Sigma, \sigma) \in Sol(C) | \pi(C) \text{ holds}\}$. Filtering solutions this way will essentially permit, during the decision procedure, to perform case analyses on the form of the solutions.

**DEFINITION 3.12 (most general solution).** A set of most general solutions of $C$ that satisfy $\pi$ is a set $mgs^\pi(C)$ of second-order substitutions such that:

1. for all $\Sigma_0 \in mgs^\pi(C)$, $dom(\Sigma_0) \subseteq vars^2(C)$, for all injections $\Sigma_1$ to fresh constants and of domain $dom(\Sigma_1) = vars^2(img(\Sigma_0), C) \setminus dom(\Sigma_0)$, $(\Sigma_0\Sigma_1, \sigma) \in Sol^\pi(C)$ for some $\sigma$.

2. for all $(\Sigma, \sigma) \in Sol^\pi(C)$, there exists $\Sigma_0 \in mgs^\pi(C)$ and $\Sigma_1$ such that $\Sigma = \Sigma_0\Sigma_1$.

We omit the predicate $\pi$ in the case where $\pi = \top$, i.e., $\pi(\Sigma)$ holds for any substitution.

The first condition of the definition states that a mgs $\Sigma_0$ is “almost” a solution of $C$: $\Sigma_0$ is allowed to be given in a minimal form that does not instantiate all variables of $vars^2(C)$, and that may not have a ground image; but we obtain a solution by replacing all pending variables by fresh names using $\Sigma_1$. The second condition states that all solutions are instances of a mgs.
**EXAMPLE 3.13.** In Example 3.11 we have mgs(C) = {Σ₀} and Sol(C) is the set of all ground instances of Σ₀. However in general the situation may be less ideal. For example a constraint system may have several most general solutions; a simple example being, with h/1 and k ∈ N:

$$ \Phi(C) = \{ax_1 \mapsto h(k), ax_2 \mapsto k\} \qquad D(C) = \{X: 2 \vdash^? x\} \qquad E^1(C) = \{x =? h(k)\} $$

The constraint system C expresses that an input x should be instantiated by h(k), potentially by using the two previous outputs h(k) and k. There are therefore two ways of computing x: either using ax₁ or h(ax₂), which is reflected as the fact that mgs(C) = {Σ₁, Σ₂} with

$$ \Sigma_1 = \{X \mapsto h(ax_2)\} \qquad \Sigma_2 = \{X \mapsto ax_1\} $$

Still, it is possible to obtain unique mgs' by performing a case analysis and restricting the solutions accordingly; typically here we have mgs<sup>πᵢ</sup>(C) = {Σᵢ} with

$$ \pi_1(\Sigma) \triangleq \exists X'. X =? h(X') \qquad \pi_2(\Sigma) \triangleq \forall X'. X \neq? h(X') $$

Another notable point is that some ground instances of a mgs may not be solutions themselves. Taking a ∈ F₀ a simple example is given by C = (Ø, X ⊢? x, x ≠? a) and mgs(C) = {id}: the substitution {X ↦ a} is a ground instance of the identity but not a solution (which does not contradict Item 1 of Definition 3.12 since although a is a constant, it is not fresh). ♦

We describe in Section 4.2 how to generate a finite set of most general solutions, at least in the context of our decision procedure.

## 3.4 Symbolic semantics

**Symbolic execution** We now describe formally our symbolic semantics. It shares some common ground with the concrete semantics of the calculus, except that a constraint system collects the execution's constraints. The semantics operates on so-called *symbolic processes* (P, C) where P is a multiset of (non-necessarily ground) plain processes and C is a constraint system. All free variables of P are bound by deductions facts, that is, for all x ∈ vars(P) there exists (X ⊢? x) ∈ D(C). The semantics then takes the form of a labelled transition system α →ₙ between symbolic processes, defined in Figure 2, where α ranges over the following alphabet of *symbolic actions*:

1. *symbolic input actions* X(Y) where X and Y are second-order variables, modelling public inputs as in the concrete semantics except that the attacker recipes are replaced by the two placeholders X, Y;

2. *symbolic output actions* X̄⟨axᵢ⟩ that follow the same logic;

3. the *unobservable action* τ which has the exact same role as in the concrete semantics.

Before we define the semantics let us explain how we handle conditionals. First of all we recall our convention to interpret substitutions as sets of equalities, that is, the positive branch
of “if $u = v$ then $P$ else $Q$” will add one mgu of $u$ and $v$ modulo theory to $E^1$. Regarding the negative branch, we want to add a constraint that is satisfied *iff* $u$ and $v$ are not equal modulo theory. We write it $\neg mgu_R(u =? v)$ and define it as follows:

$$ \neg mgu_R(u =? v) = \bigwedge_{\sigma \in mgu_R(u =? v)} \forall z_1, \dots, z_n. \bigvee_{x \in vars(u, v)} x \neq? x\sigma $$

where $\{z_1, \dots, z_n\} = vars(u\sigma, v\sigma) \setminus vars(u, v)$.

If $C = (\Phi, D, E^1)$, $\mu = mgu(E^1) \neq \perp$ and $n = |dom(\Phi)|$:

$$ (\{\text{if } u = v \text{ then } P \text{ else } Q\} \cup \mathcal{P}, C) \xrightarrow{\tau} S (\{P\} \cup \mathcal{P}, (\Phi, D, E^1 \wedge \sigma)) \qquad (\text{s-then}) \\ \text{if } \sigma \in mgu_R(u\mu =? v\mu) $$

$$ (\{\text{if } u = v \text{ then } P \text{ else } Q\} \cup \mathcal{P}, C) \xrightarrow{\tau} S (\{Q\} \cup \mathcal{P}, (\Phi, D, E^1 \wedge \neg mgu_R(u\mu =? v\mu))) \qquad (\text{s-else}) $$

$$ (\{u(x).P\} \cup \mathcal{P}, C) \xrightarrow{Y(X)} S (\{P\} \cup \mathcal{P}, (\Phi, D \wedge X \vdash? x \wedge Y \vdash? y, E^1 \wedge \sigma)) \qquad (\text{s-in}) \\ \text{if } Y:n, X:n \text{ and } y \text{ are fresh and } \sigma \in mgu_R(y =? u\mu) $$

$$ (\{\bar{u}\langle v\rangle.P\} \cup \mathcal{P}, C) \xrightarrow{\bar{Y}\langle ax_{n+1}\rangle} S (\{P\} \cup \mathcal{P}, (\Phi \cup \{ax_{n+1} \mapsto v\mu\sigma\downarrow\}, D \wedge Y \vdash? y, E^1 \wedge \sigma)) \qquad (\text{s-out}) \\ \text{if } Y:n \text{ and } y \text{ are fresh and } \sigma \in mgu_R(y =? u\mu \wedge v\mu =? v\mu) $$

$$ (\{\bar{u}\langle v\rangle.P, w(x).Q\} \cup \mathcal{P}, C) \xrightarrow{\tau} S (\{P, Q\{x \mapsto v\mu\sigma\}\} \cup \mathcal{P}, (\Phi, D, E^1 \wedge \sigma)) \qquad (\text{s-comm}) \\ \text{if } \sigma \in mgu_R(u\mu =? w\mu \wedge v\mu =? v\mu) $$

$$ (\{P | Q\} \cup \mathcal{P}, C) \xrightarrow{\tau} S (\{P, Q\} \cup \mathcal{P}, C) \qquad (\text{s-par}) $$

<caption>**Figure 2.** A symbolic semantics for the applied pi-calculus</caption>

The rule (s-IN) adds two deduction facts $X \vdash? x$ and $Y \vdash? y$ to $D$, modelling that the input term and communication channel should be deducible by the adversary; in particular the constraint $\sigma \in mgu_R(y =? u\mu)$ indicates that the term deduced by $Y$ is effectively the channel $u$. The rule (s-OUT) essentially follows the same logic, adding a fresh deduction fact and a constraint indicating that the channel is deducible. We assume an implicit alpha renaming of bound variables so that each appear only once in the process: this prevents reference conflicts in $D$ when applying the rule (s-IN). Let us also point out that several rules introduce constraints of the form $mgu_R(u, u)$: we recall that this substitution is not always $\top$, but is the most general substitution $\sigma$ ensuring that $u\sigma$ is a message. As in the concrete semantics, a *symbolic trace* is then a finite sequence of transitions

$$ (P_0, C_0) \xrightarrow{\alpha_1} \dots \xrightarrow{\alpha_n} S (P_n, C_n) $$
which may be referred to as $(\mathcal{P}_0, C_0) \stackrel{\text{tr}}{\Rightarrow}_s (\mathcal{P}_n, C_n)$ if tr is obtained by removing the $\tau$'s from the word $\alpha_1 \cdots \alpha_n$. For simplicity the plain process $P$ may be interpreted as the symbolic process $((\{P\}), (\emptyset, \top, \top))$.

**EXAMPLE 3.14.** We consider again the example of the private authentication protocol. We recall the process of the agent $B$ receiving the communication, writing $pk_X, sk_X$ instead of $pk(sk(X)), sk(X)$, and $t = \text{adec}(x, s)$:

$$ B(s, p, n, r) = c(x). $$
$$ \begin{array}{ll} \text{if } \text{snd}(t) = p & \text{then} \\ & \bar{c}\langle\text{aenc}(\langle\text{fst}(t), n, pk(s)\rangle, r, p)\rangle \\ \text{else } \bar{c}\langle\text{aenc}(n, r, pk(s))\rangle \end{array} $$

and use a frame $\Phi_0 = \{ax_1 \mapsto pk_A, ax_2 \mapsto pk_B, ax_3 \mapsto aenc(\langle N_A, pk_A\rangle, r_A, pk_B)\}$, containing public keys and the connection request sent by $A$. We give in Figure 3 a tree of all symbolic executions of $B$ (we only write the constraints added at each step).

<figure><img src="image_5.png" /><figcaption>**Figure 3.** Tree of all constraint systems reachable by executing $B$ symbolically</figcaption></figure>

Intuitively, the branch of the constraint system $C_1$ abstracts the set of concrete traces where $B$ accepts the connection, and the branch of $C_2$ those where $B$ refuses it. Typically in the traces of the branch $C_1$ the attacker forwards the message of $A$ or forges one pretending to be
A; this is formally expressed by the fact that mgs($C_1$) = {$\Sigma_0 \cup \Sigma_{fwd}$, $\Sigma_0 \cup \Sigma_{att}$} where:

$$ \Sigma_0 = \{Y \mapsto d, Z \mapsto d\} \quad \Sigma_{fwd} = \{X \mapsto ax_3\} \quad \Sigma_{att} = \{X \mapsto aenc(\langle x_1, ax_1 \rangle, x_3, ax_2)\} \quad \blackdiamond $$

**Soundness and completeness** Similar symbolic semantics have been developed in the context of protocol analysis [15, 29]. The general approach is to abstract the (infinite) set of concrete traces by the finite set of symbolic traces and to study the solutions of the resulting constraint systems. A typical example is that the following statements are equivalent:

1. Weak secrecy of the term $u$ in $P$: for all traces $P \xrightarrow{tr} (\mathcal{P}, \Phi)$, $u$ is not deducible from $\Phi$

2. for all symbolic traces $P \xrightarrow{tr} s (\mathcal{P}, C)$, the system $(\Phi(C), D(C) \wedge X \vdash^? x, E^1(C) \wedge x =? u)$ has no solution, where $X:n$ and $x$ are fresh, $n = |dom(\Phi)|$

(Recall that for notational convenience the plain process $P$ may be interpreted as the symbolic process ($(P)$, $(\emptyset, \top, \top)$).) This reduces weak secrecy (for a bounded number of sessions) to the decidability of whether a constraint system has a solution. Similar approaches have been developed in [15, 29] to decide equivalence properties for some classes of processes. They rely on a connection between the symbolic and concrete semantics, under the form of two properties: 1. soundness: applying to a symbolic trace a solution of its final constraint system leads to a concrete trace; and 2. completeness: all concrete traces are obtained by applying a solution to a symbolic one. They are formalised below, the proof following from a straightforward induction on the length of the traces.

**PROPOSITION 3.15 (soundness and completeness of the symbolic semantics).** Let $(\mathcal{P}, C)$ be a symbolic process. Then we have:

1. Soundness: for all symbolic traces $(\mathcal{P}, C) \xrightarrow{tr_s} s (Q, C')$ and $(\Sigma, \sigma) \in Sol(C')$, there exists a concrete trace of the form $(\mathcal{P}\sigma, \Phi(C)\sigma\downarrow) \xrightarrow{tr_s\Sigma} (Q\sigma, \Phi(C')\sigma\downarrow)$

2. Completeness: for all symbolic processes $(\mathcal{P}, C)$, $(\Sigma, \sigma) \in Sol(C)$, and for all concrete traces $(\mathcal{P}\sigma, \Phi(C)\sigma\downarrow) \xrightarrow{tr} (Q, \Phi)$, there exists a symbolic trace $(\mathcal{P}, C) \xrightarrow{tr'} s (Q', C')$ and $(\Sigma', \sigma') \in Sol(C')$ such that $\Sigma \subseteq \Sigma'$, $Q = Q'\sigma'$, $tr = tr'\Sigma'$ and $\Phi = \Phi(C')\sigma'\downarrow$.

## 3.5 The key tool: the partition tree

To decide trace equivalence and labelled bisimilarity, we introduce the novel notion of a *partition tree* of two bounded processes $P$ and $Q$. The point is to build a (finite) tree of all symbolic executions of $P$ and $Q$, grouping into the same nodes intermediary processes as follows:

1. All processes of a same node should have a *common, unique mgs*. Since one symbolic process alone may already have several most general solutions, the node is parametrised by a restricting predicate $\pi$ on second-order solutions (recall Example 3.13).

2. When applying the mgs of a node to all of the processes it contains (and instantiating the potential remaining variables by fresh distinct constants), the resulting frames are
statically equivalent. Conversely, all reachable symbolic processes that would verify this
property should be in the node as well.

A branch of this tree therefore represents the set of all equivalent traces of *P* and *Q* taking
a given sequence of visible actions. Taking profit of this observation we will show that whenever
*P* and *Q* are not trace equivalent or labelled bisimilar, a witness of non-equivalence can be
exhibited using the tree. Formally its nodes are modelled by *configurations* that consist of sets Γ
of symbolic processes sharing a unique mgs and statically equivalent solutions.

**DEFINITION 3.16 (configuration).** A *configuration* is a pair (Γ, π) where Γ is a set of symbolic processes and π a predicate on second-order substitutions. We also require that:

1. the predicate $\pi$ is defined on $\text{vars}^2(\Gamma)$, that is, for all $\Sigma$, $\pi(\Sigma)$ iff $\pi(\Sigma_{|\text{vars}^2(\Gamma)}})$;

2. for all ($\mathcal{P}$, $C$) ∈ Γ, |mgs$^\pi$(C)| = 1;

3. for all ($\mathcal{P}_1$, $C_1$), ($\mathcal{P}_2$, $C_2$) ∈ Γ, if ($\Sigma$, $\sigma_1$) ∈ $Sol^\pi(C_1)$ then there exists $\sigma_2$ such that ($\Sigma$, $\sigma_2$) ∈ $Sol^\pi(C_2)$ and $\Phi(C_1)\sigma_1 \sim \Phi(C_2)\sigma_2$.

The predicate $\pi$ can typically be described using second-order (dis)equations. We then consider trees with nodes labelled by configurations and edges by visible symbolic actions (i.e., not $\tau$). Given a node $n$ of such a tree, we write $\Gamma(n)$ and $\pi(n)$ the components of the corresponding configuration, and $n \xrightarrow{\alpha} n'$ to express that $n'$ is a child node of $n$ through an edge labelled by the symbolic action $\alpha$. By definition of a mgs, the points 2 and 3 of Definition 3.16 above ensure that all symbolic processes in $\Gamma(n)$ have the same set of second-order variables, written $\text{vars}^2(n)$, and a common and unique mgs, written $\text{mgs}(n)$.

**DEFINITION 3.17 (partition tree).** A *partition tree* of two bounded processes *P* and *Q* is a tree *T* whose nodes are labelled by configurations and edges by visible symbolic actions, and that verifies the following properties. First of all *P*, *Q* ∈ Γ(*root*(*T*)) and *π*(*root*(*T*)) = ⊥, where *root*(*T*) denotes the root node of the tree. Then for all nodes *n* of *T*, (*P*, *C*) ∈ Γ(*n*) and visible symbolic actions *α*:

1. *Closure by τ-transition:* if ($\mathcal{P}$, $C$) $\xrightarrow{\tau}$$_S$ ($\mathcal{P}'$, $C'$) and $Sol^{\pi(n)}(C') \neq \emptyset$ then ($\mathcal{P}'$, $C'$) ∈ $\Gamma(n)$.

2. All symbolic transitions are reflected in the tree: if (P, C) $\xrightarrow{\alpha}$<sub>s</sub> (P', C') and (Σ, σ) ∈ Sol<sup>π(n)</sup>(C') then there exists an edge n $\xrightarrow{\alpha}$ n' in T such that (P', C') ∈ Γ(n') and (Σ', σ) ∈ Sol<sup>π(n')</sup>(C') for some Σ' that coincides with Σ on vars<sup>2</sup>(n).

Moreover for all edges $n \xrightarrow{\alpha} n_c$ of $T$ and $(\mathcal{P}_c, \mathcal{C}_c) \in \Gamma(n_c)$:

3. *Predicates are refined along branches:* for all $\Sigma$, if $\Sigma$ verifies $\pi(n_c)$ then it verifies $\pi(n)$.

4. Nodes are maximal: if (Σ, σ) ∈ Sol^π(n)(C), (Σ_c, σ_c) ∈ Sol^π(n_c)(C_c) and Σ ⊆ Σ_c, then Γ(n_c) contains all symbolic processes (P', C') such that (P, C) ⇒_s (P', C') and, for some substitution σ', (Σ_c, σ') ∈ Sol(C') and Φ(C_c)σ_c ~ Φ(C')σ'.
The set of partition trees of P and Q is written PTree(P, Q).

The set PTree(P, Q) is infinite (at least because arbitrarily many processes can be put in the root configuration) but our decision procedures only require to construct one, arbitrary partition tree. The children $n'$ of a node $n$ represent the sets of processes, grouped w.r.t. static equivalence, reachable by one transition from a process of $n$. Item 2 ensures that all cases are covered, that is, for all symbolic transitions from $n$ and all solutions $\Sigma$, at least one child $n'$ should contain the resulting symbolic process. Note that we do not impose that $\Sigma$ verifies $\pi(n')$, but that there exists another solution $\Sigma'$ computing the same first-order terms that does. This more permissive approach will allow us, when generating partition-tree nodes in Section 4, to use families of predicates $\pi$ that only consider solutions of a certain form (which therefore requires to prove that any deducible term can be computed by a recipe of this form). Item 4 then formalises that the nodes are saturated under static equivalence: if $n'$ is a child of $n$ and a symbolic transition $A \stackrel{\alpha}{\Rightarrow}_s B$ from a process $A \in \Gamma(n)$ may result into a process statically equivalent to a process $C \in \Gamma(n')$ then $B$ should be in $\Gamma(n')$ as well.

**EXAMPLE 3.18.** Let us draw a partition tree corresponding to an anonymity analysis in the private authentication protocol, simplified for readability. We consider the following light version of the role of the process $B$ accepting a connection from an agent $X$, removing the identification nonces $N_A, N_B$ from the protocol and replacing the decoy message by a fresh name $r$:

$$B_X = c(x). \text{if } \text{adec}(x, sk_B) = pk_X \text{ then } \bar{c}\langle\text{aenc}(ok, r, pk_X)\rangle \text{ else } \bar{c}\langle r\rangle$$

We consider a 3-agent scenario $(A, B, C)$ where $A$ has already emitted $aenc(pk_A, r_A, pk_B)$ to initiate a communication with $B$. The security property we study is whether the identity of $B$'s accepted recipient remains anonymous. That is we want to prove $P \approx Q$ where

$$P = C[B_A] \quad Q = C[B_C] \quad C[R] = \bar{c}\langle pk_A \rangle \cdot \bar{c}\langle pk_B \rangle \cdot \bar{c}\langle pk_C \rangle \cdot \bar{c}\langle aenc(pk_A, r_A, pk_B) \rangle \cdot R$$

The partition tree in Figure 4 has been lightened for readability: if a node contains two symbolic processes $A_s, B_s$ such that $A_s \stackrel{\tau}{\Rightarrow}_s B_s$, then $A_s$ is omitted from the node (as it contains less constraints than $B_s$ anyway). The configuration at the root of the tree only contains $P$ and $Q$. After the four initial outputs of the context $C$, we reach the constraint system $C_0$ defined by:

$$\Phi(C_0) = \{ax_1 \mapsto pk_A, ax_2 \mapsto pk_B, ax_3 \mapsto pk_C, ax_4 \mapsto aenc(pk_A, r_A, pk_B)\}$$

$$D(C_0) = X_1 \vdash^? x_1 \wedge X_2 \vdash^? x_2 \wedge X_3 \vdash^? x_3 \wedge X_4 \vdash^? x_4$$

$$E^1(C_0) = x_1 =^? c \wedge x_2 =^? c \wedge x_3 =^? c \wedge x_4 =^? c$$

The next step is the first one inducing a non-trivial case analysis. This node has four children for the adversary to compute the input $c(x)$: $\pi_1$ forwards the message of $A$, $\pi_2$ forges a message
<figure><img src="image_6.png" /><figcaption>Figure 4. A simplified partition tree of P and Q</figcaption></figure>

pretending it is from A, $\pi_3$ forges a message pretending it is from C, $\pi_4$ any other case. The choice of these 4 cases is guided by the conditional if $adec(x, sk_B) = pk_X$ (where $X = A$ or $X = C$) that is evaluated on the input. Choice $\pi_1$ results in the positive branch in both $B_A$ and $B_C$, as it corresponds to an honest execution. Choice $\pi_2$ results in choosing the positive branch in $B_A$ and the negative branch in $B_C$, while $\pi_3$ does the opposite. Choice $\pi_4$ leads to the negative branch in all cases by construction (as it is the negation of the 3 previous cases).

More precisely we write $\Phi(C_{1,X}^{\text{pos}}) = \Phi(C_{1,X}^{\text{neg}}) = \Phi(C_0)$, $D(C_{1,X}^{\text{pos}}) = D(C_{1,X}^{\text{neg}}) = D(C_0) \wedge Y \vdash? y$ and

$$E^1(C_{1,X}^{\text{pos}}) = E^1(C_0) \wedge y =? c \wedge x =? aenc(pk_X, x', pk_B)$$

$$E^1(C_{1,X}^{\text{neg}}) = E^1(C_0) \wedge y =? c \wedge \forall x'. x \neq? aenc(pk_X, x', pk_B)$$

Then the final transitions simply execute the resulting outputs, i.e. $C_{2,X}^s$, $s \in \{\text{pos}, \text{neg}\}$, is obtained by adding $Z \vdash? z$ and $z =? c$ to $C_{1,X}^s$. Since a ciphertext is indistinguishable from a nonce, the two outputs always end up in the same nodes; that is, all leaves contain at least one process originated from P and at least one from Q, which is how we prove trace equivalence. The situation would be different with a rewrite rule such as $test_aenc(aenc(x, y, pk(z))) \rightarrow \text{ok}$; a partition tree of P and Q with this extended rewriting system can be found in Figure 5.

We highlighted the part differing from the previous tree. Essentially some leaf nodes have been split in two due to the enhanced capabilities of the adversary to disprove static equivalence, inducing a violation of trace equivalence. For example the leftmost leaf's mgs is

$$\{X \mapsto ax_4, X_1 \mapsto c, \dots, X_4 \mapsto c, Y \mapsto c, Z \mapsto c\}$$
<figure><img src="image_7.png" /><figcaption>**Figure 5.** Partition tree with the rewriting system extended with $test\_aenc(aenc(x, y, pk(z))) \to \text{ok}$</figcaption></figure>

which corresponds to an attack trace where the attacker forwards the message of A and observes whether the response of B is a ciphertext, which reveals whether B accepts connections from A or not. ♦

In the remaining of the section we formalise how to decide trace equivalence and labelled bisimilarity of two processes, given a partition tree and the mgs of each of its nodes. For that we will rely on the following notion of reduction, characterising symbolic traces viewed as branches of a partition tree:

**DEFINITION 3.19 (partition-tree trace).** Given a partition tree $T$ we write $(\mathcal{P}, C), n \xrightarrow{\alpha} T$ $(\mathcal{P}', C')$, $n'$ when:

1. $n$ and $n'$ are nodes of $T$ such that $(\mathcal{P}, C) \in \Gamma(n)$ and $(\mathcal{P}', C') \in \Gamma(n')$; and

2. if $\alpha = \tau$ then $n = n'$, otherwise $n \xrightarrow{\alpha} n'$ and $(\mathcal{P}, C) \xrightarrow{\alpha} S(\mathcal{P}', C')$.

For convenience this notion is to be understood up to alpha renaming of the variables of the symbolic action $\alpha$. We write $A_0^s, n_0 \stackrel{\text{tr}}{\Rightarrow} T A_p^s, n_p$ instead of $A_0^s, n_0 \xrightarrow{\alpha_1} T \cdots \xrightarrow{\alpha_p} T A_p^s, n_p$ if tr is the word obtained after removing $\tau$ symbols from $\alpha_1 \cdots \alpha_p$. If $P$ is a plain process we may also write $P \stackrel{\text{tr}}{\Rightarrow} T A_s, n$ instead of $(\{P\}, (\emptyset, \tau, \top)), \text{root}(T) \stackrel{\text{tr}}{\Rightarrow} T A_s, n$.

## 3.6 Decision procedures for equivalence

In this section, we assume that we managed to compute a partition tree $T \in \text{PTree}(P_1, P_2)$ (in particular, that there exists one). We then describe how to derive a decision procedure for trace equivalence and labelled bisimilarity from $T$.
**Trace equivalence** As hinted in our various examples, deciding trace equivalence can be reduced to an analogue notion of equivalence using the (finite) transition relation $\xrightarrow{\alpha}^T$ instead of the concrete semantics $\xrightarrow{\alpha}$. This is formalised by the following theorem:

**THEOREM 3.20 (partition-tree-based characterisation of trace equivalence).** Whenever $T \in PTree(P_1, P_2)$, the following points are equivalent:

1. $P_1 \sqsubseteq_t P_2$

2. for all partition-tree traces $P_1 \xrightarrow{\text{tr}}^T (\mathcal{P}_1, C_1)$, $n$, we have $P_2 \xrightarrow{\text{tr}}^T (\mathcal{P}_2, C_2)$, $n$

The proof of this result mostly follows from a combination of the soundness and completeness of the symbolic semantics, with two technical lemmas generalising the properties of the partition tree from edges to branches. The detailed statements and proofs can be found in Appendix A.1.

**Simulations** In the case of trace equivalence, a witness that $A \not\approx_t B$ was simply a trace of $A$ or $B$ that has no equivalent trace in the other process. The case of labelled bisimilarity is however more involved. Using vocabulary borrowed from game theory, the definition of bisimilarity can be seen as a *prover-disprover game*: at each state of the game the disprover chooses a transition from one of the two processes and the prover answers by choosing a transition of the same type from the other process (plus some potential $\tau$-transitions). The disprover wins the game if they manage to reach a state with non-statically-equivalent processes or if the prover cannot answer to one of the moves. A witness of non-equivalence is thus a winning strategy for the disprover. We formalise this below, recalling that if $\alpha$ is an action, we write $\bar{\alpha} = \alpha$ if $\alpha \neq \tau$ and $\bar{\alpha} = \varepsilon$ if $\alpha = \tau$.

**DEFINITION 3.21 (witnesses).** A witness of non-bisimilarity $w$ is a set of pairs $(A_0, A_1)$ verifying the following two conditions:

1. $A_0$ and $A_1$ are ground extended processes such that $A_0 \sim A_1$

2. there exists $b \in \{0, 1\}$ and a transition $A_b \xrightarrow{\alpha} A'_b$ such that for all traces $A_{1-b} \xrightarrow{\bar{\alpha}} A'_{1-b}$, either $A'_0 \not\approx A'_1$ or $(A'_0, A'_1) \in w$.

We say that in addition that $w$ is a witness of non-simulation if the above two conditions can always be satisfied with $b = 0$. We say that $w$ is a witness for $(A_0, A_1)$ if $(A_0, A_1) \in w$.

Note that the witness can be seen as a relation corresponding to the negation of the definition of bisimilarity (Definition 2.10) minus the static equivalence, i.e. $\not\approx_b \setminus \not\approx$.

**PROPOSITION 3.22 (witness-based characterisation of labelled bisimilarity).** If $A_0 \sim A_1$ then:

1. $A_0 \not\approx_b A_1$ iff there exists a witness of non-bisimilarity $w$ for $(A_0, A_1)$
2. $A_0 \not\subseteq_S A_1$ iff there exists a witness of non-simulation w for $(A_0, A_1)$

**PROOF.** We only give the proof in the case of $\approx_b$, as the proof for $\sqsubseteq_S$ is analogue. First, we observe that $A_0 \not\approx_b A_1$ iff there exists a binary relation $S$ on ground extended processes such that $A_0 S A_1$ and, for all $(B_0, B_1) \in S$, either 1. $B_0 \nrightarrow B_1$, or 2. there exists $b \in \{0, 1\}$ and a transition $B_b \xrightarrow{\alpha} B'_b$ such that for all traces $B_{1-b} \xrightarrow{\bar{\alpha}} B'_{1-b}, B'_0 S B'_1$. Let us call such a relation $S$ a labelled attack on $(A_0, A_1)$. Since processes are bounded there exist no infinite sequences of transitions and for all $A, B, A \not\approx_b B$ therefore straightforwardly rephrases to the existence of a labelled attack $S$ such that $A S B$. It then suffices to observe that

1. If $S$ is a labelled attack on $(A_0, A_1)$ then $S \setminus \not\approx$ is a witness for $(A_0, A_1)$.

2. If $w$ is a witness for $(A_0, A_1)$ then $w \cup \not\approx$ is a labelled attack on $(A_0, A_1)$.

<figure><img src="image_8.png" /></figure>

We now define a symbolic variant of the notion of witness that can be constructed within a partition tree $T$. In essence, a symbolic witness may be seen as a winning strategy for the disprover in a bisimulation game limited to the finite transition relation $\rightarrow_T$.

**DEFINITION 3.23 (symbolic witnesses).** A symbolic witness of non bisimilarity $w_S$ w.r.t. a partition tree $T$ is a finite tree whose nodes $N$ are labelled by tuples $(A_0, n)$ or $(A_0, A_1, n)$ with $n$ a node of $T$ and $A_0, A_1 \in \Gamma(n)$. We also require that if $N$ is labelled $(A_0, A_1, n)$, there exist $b \in \{0, 1\}$ and a transition $A_b, n \xrightarrow{\alpha} T A'_b, n'$ (possibly $\alpha = \tau$) such that:

1. If $A_{1-b}$ is not reducible by $\xrightarrow{\bar{\alpha}}_T$ then $N$ has a unique child labelled $(A'_b, n')$;

2. otherwise the children of $N$ are the nodes labelled $(A'_0, A'_1, n'), A_{1-b}, n \xrightarrow{\bar{\alpha}}_T A'_{1-b}, n'$.

We say that $w_S$ is a witness of non-simulation if the above two conditions can always be satisfied with $b=0$. We say that $w_S$ is a symbolic witness for $(A_0, A_1, n)$ when $\text{root}(w_S)$ is labelled by $(A_0, A_1, n)$.

However purely symbolic witnesses do not exhibit consistent proofs of non-equivalence in general. Indeed, while a concrete execution fixes the effective value of an input $x$ at the moment it is performed, a symbolic execution records constraints on $x$ all along the execution. Rephrasing, the symbolic semantics puts the prover at a disadvantage in the game, since they have to answer to the disprover's input actions without knowing the values of the input terms. Symbolic witnesses inducing invalid winning strategies for the disprover will be discarded by their absence of solutions in the following sense:

**DEFINITION 3.24 (solution of a symbolic witness).** Let $w_S$ be a symbolic witness. A solution of $w_S$ is a function $f_{sol}$ that maps nodes of $w_S$ to ground second-order substitutions such that for all nodes $N$ labelled $(A_0, n)$ or $(A_0, A_1, n)$,

1. for all $A_b = (\mathcal{P}, C), (f_{sol}(N), \sigma) \in \text{Sol}^{\pi(n)}(C)$ for some $\sigma$;
2. for all children nodes $N_1, N_2$ of $N$, $f_{sol}(N) \subseteq f_{sol}(N_1) = f_{sol}(N_2)$.

We denote $Sol(w_s)$ the set of solutions of $w_s$.

**THEOREM 3.25 (partition-tree-based characterisation of labelled bisimilarity).** If $T \in PTree(P_1, P_2)$:

1. $P_1 \approx_b P_2$ iff for all symbolic witnesses of non-bisimilarity $w_s$ for $(P_1, P_2, \text{root}(T))$, we have $Sol(w_s) = \emptyset$

2. $P_1 \sqsubseteq_s P_2$ iff for all symbolic witnesses of non-simulation $w_s$ for $(P_1, P_2, \text{root}(T))$, we have $Sol(w_s) = \emptyset$

The proof, although technical, simply connects the symbolic witnesses to concrete ones using the soundness and completeness of the symbolic semantics as well as the properties of the partition tree, following similar ideas as the analogue proof for trace equivalence. The detailed proof can be found in Appendix A.2.

Assuming one has computed a partition tree $T \in PTree(P_1, P_2)$ and the mgs of each of its nodes, since there are finitely-many possible symbolic witnesses, Theorem 3.25 yields a decision procedure for the labelled bisimilarity of $P_1$ and $P_2$ provided one can decide whether a given symbolic witness has a solution. For that we rely on a simple, bottom-up unification of the mgs' appearing in the witness; details can be found in Section 5.4 where we study more precisely the complexity of partition-tree-based decision procedures.

## 3.7 Generating partition trees (with a constraint-solving oracle)

In this section we detail the skeleton of the procedure for computing a partition tree of two plain processes $P_1$ and $P_2$. The description is modular in that most of the technical details, in particular the modelling of the node predicates and how we obtain the expected properties of the tree, are abstracted by a *constraint-solving oracle* that we detail in the next sections. This section should therefore be seen as the overview of the whole algorithm for deciding equivalence properties, which gives enough insight to discuss our implementation.

The algorithm generates the nodes of the tree top-down, that is, from the root to the leaves. We outline the procedure in Figure 6.

Let us now describe the algorithm to compute $T \in PTree(P_1, P_2)$ in more details, up to the technical developments detailed in the next sections.

1. First, we initiate a root containing $P_1$ and $P_2$ and saturate the configuration by $\tau$ transitions. That is, we consider the set of symbolic processes

$$ \Gamma(\text{root}(T)) = \{ (\mathcal{P}, C) \mid P_i \xrightarrow{\tau} s (\mathcal{P}, C), i \in \{1, 2\}, \text{Sol}(C) \neq \emptyset \} $$

Note that the constraint systems $C$ involved in this definition do not contain deduction facts, which makes the decision of the emptiness of $Sol(C)$ relatively straightforward.
<figure><img src="image_9.png" /><figcaption>Figure 6. Computing the subtree of a partition tree rooted in a node n</figcaption></figure>

Using the terminology of the later Section 4, using simplification rules permits to put the constraints into a simple form where the existence of a solution is trivial to decide.

2. Then let us assume we already constructed a node n of the tree using this algorithm, in particular the corresponding configuration $(\Gamma(n), \pi(n))$. To compute the children of n we first enumerate all symbolic transitions from processes of $\Gamma(n)$, separating input and output actions. That is, we compute the two sets

$$ \Gamma^{\text{in}} = \{ B \mid A \in \Gamma(n), A \underset{s}{\stackrel{Y(X)}{\rightleftharpoons}} B \} \qquad \Gamma^{\text{out}} = \{ B \mid A \in \Gamma(n), A \underset{s}{\stackrel{\bar{Y}\langle ax_p \rangle}{\rightleftharpoons}} B \} $$

3. $\Gamma^{\text{in}}$ and $\Gamma^{\text{out}}$ are two intermediary sets that do not satisfy yet the father-child properties of the partition tree. For that we use a constraint-solving algorithm detailed in Chapter 4 (simplification rules again, but also case distinction rules) that will partition $\Gamma^{\text{in}}$ and $\Gamma^{\text{out}}$ to gather symbolic processes with statically-equivalent solutions and remove those with no solutions. This constraint solving results into a sequence of configurations

$$ (\Gamma_1^{\text{in}}, \pi_1^{\text{in}}), \dots, (\Gamma_p^{\text{in}}, \pi_p^{\text{in}}) \qquad (\Gamma_1^{\text{out}}, \pi_1^{\text{out}}), \dots, (\Gamma_q^{\text{out}}, \pi_q^{\text{out}}) $$

that will label the children of n. The procedure is then carried out recursively from these child nodes until no more symbolic transitions are available.
In Section 4 we detail the missing parts of this procedure that take the form of constraint-solving rules, in the context of constructor-destructor subterm convergent theories. Note that the approach is modular in that the proofs we have carried so far are independent of the assumptions on the rewriting system: generalising the results of Section 4 will automatically result in the decidability of trace equivalence and labelled bisimilarity of bounded processes for the extended class of theories.

## 3.8 Implementation and performances

**The DeepSec prover** Building on the procedure's structure described above and the internal solver developed in the next sections, we have implemented a prototype in OCaml, called DEEPSEC (Deciding Equivalence Properties in SECURITY protocols). The user specifies a rewriting system (that is checked to be constructor-destructor and subterm convergent by the tool), two bounded processes, and the tool verifies whether they are trace equivalent. If not, a concrete attack trace is returned in a dedicated graphical interface; we refer to the DEEPSEC's website for development credits, tutorials and details on practical usage [35]:

https://deepsec-prover.github.io/

The tool's specification language implements the grammar presented in Section 2, including some syntax extensions for non-deterministic choice, private function symbols, a restricted form of patterned let bindings, as well as bounded replication $!^nP$ defined as $n$ parallel copies of $P$. These additional primitives should mostly be seen as syntactic sugar, although the native integration allowed specific optimisations compared to encodings within the initial calculus. The syntax and structure of DEEPSEC's input files are similar to the widely used PROVERIF tool [22] to make it easier for new users to discover and use it.

**Trace equivalence vs (bi)simulation** The tool currently only implements the trace equivalence procedure as it is rather efficient. Following Theorem 3.20, the procedure for checking trace equivalence between $P_1$ and $P_2$ consists in generating the partition tree and checking that each node contains symbolic constraint systems both from $P_1$ and $P_2$. As different branches of the partition tree are independent from one another, the implementation only requires to store in memory the current branch that is being verified, instead of the whole partition tree. On the other hand, the procedure for checking (bi)simulation both requires to compute and store in memory the full partition tree. In addition, the procedure also requires guessing a symbolic witness, which would be extremely inefficient. A natural follow up to our work would be to explore ways of effectively implementing the decision procedure for (bi)simulation that would avoid these two main hurdles.
**Partial order reductions** The tool also implements *partial order reductions (POR)*, an optimisa-
tion technique for protocol analysis developed by Baelde et al. [10]. The basic idea is to discard
part of the state space that is redundant but this optimisation is only sound when processes
are *action-determinate*, as defined in [10]. Although we omit here the definition of determinacy
for simplicity, let us mention that not using private channels and assigning a different channel
name to each parallel process is a simple, syntactic way to ensure this property. This is however
not always possible—typically when looking at some anonymity or unlinkability properties.
Typically, the private authentication protocol used as a running example can be modelled as a
determinate process, but not the Helios and BAC protocols (due to private channels or because
this introduces artificial violations of the equivalence property).

In practice, DEEPSEC automatically detects action-determinate processes and activates the POR, which drastically reduces the number of symbolic executions that need to be considered. We also go further and allow to verify a refined equivalence, *equivalence by session*, that allows to use similar POR techniques without the restriction to determinate processes. This contribution is however out of the scope of this article; details can be found in [32] and our experimental results presented below only include the base POR of [10].

**Distributing the computation** The main task of DEEPSEC is to generate a partition tree and, as we explained, this is done using a top-down approach. This task can be distributed as computing a given node of the tree can be done independently of its sibling nodes. However, some engineering is needed to avoid heavy communication overhead due to task scheduling. Indeed, the partition tree is not a balanced tree and we do not know in advance which branches will be larger than others. Because of this, we do not directly compute and return the children of each node in the most straightforward manner, but proceed in two steps:

1. We start with a breadth-first generation of the partition tree. The number of pending nodes will gradually grow until eventually exceeding a threshold parameter *n*.

2. Each available core focuses on one of these nodes, computes the whole subtree rooted in this node in a depth-first manner and, when this the task is completed, is assigned to a new node until none remain.

If some cores become idle for too long in Step 2 (because the number of cores exceeds the number of non-completed nodes), we perform a *new round*, that is, we interrupt the working nodes and restart this two-step procedure on incomplete nodes. Although doing so wastes some proof work, this improves performances for particularly unbalanced trees. Note that parallelisation is also supported by other automated analysers such as AKISS [24], but DEEPSEC goes one step further as it is able to distribute the computation not only on multiple cores of a given machine but also clusters of computers.
**Benchmarks** We performed extensive benchmarks to compare DEEPSEC against other tools that verify equivalence properties for a bounded number of sessions: AKISS [24], APTE [25], SATEQUIV [43] and SPEC [60]. Experiments are carried out on Intel Xeon 3.10GHz cores, with 40Go of memory. We distributed the computation on 20 cores for AKISS and DEEPSEC as they support parallelisation—unlike the others which therefore use a single core. The results are summarised in Table 2 with the following symbol conventions:

✓ analysis terminates and equivalence holds

⚡ analysis terminates and an attack is found

OM analysis aborted due to memory overflow (Out of Memory)

analysis aborted due to timeout (12 hours)

X the tool is not expressive enough to analyse the protocol

We first analysed strong secrecy and anonymity for several classical authentication protocols. The DEEPSEC tool clearly outperforms AKISS, APTE, and SPEC. The SATEQUIV tool becomes more efficient, when the number of sessions significantly increases.

To put more emphasis on the broad scope we also include analyses of unlinkability and anonymity properties for a number of other protocols. This includes the Private authentication protocol used as a running example, BAC [51] and the Helios voting protocol [5]. In addition we study a simplified version of the AKA protocol deployed in 3G telephony networks without XOR [8], the Passive Authentication protocol implemented in the European passport [51], as well as the Prêt-à-Voter protocol (PaV) [57]. Note that, while PaV is a priori in the scope of AKISS, it failed to produce a proof: AKISS only approximates trace equivalence of non-determinate processes and finds a false attack here. Finally we note that BAC, PaV and Helios protocols are not action-determinate and therefore do not benefit from the POR optimisation, which explains the much higher verification times when increasing the sessions. Nevertheless, as exemplified by some examples, attacks may be found very efficiently, as it generally does not require to explore the entire state space.

# 4. Generation of the partition tree

In the previous sections, we detailed how to use the partition tree to derive decision procedures for equivalence properties. We describe in this section a constraint solving procedure that may be used to generate one in practice.

## 4.1 Extended constraint systems

In order to carry out the constraint solving required to construct the partition tree, we extend constraint systems with components allowing to reason more finely about the *attacker's knowl-
<table><caption>**Table 2.** Performances of DeepSec (20 cores) against other protocol analysers</caption><thead><tr><th></th><th>Protocol (# of roles)</th><th>AKISS</th><th>APTE</th><th>SPEC</th><th>SATEQUIV</th><th>DEEPSEC</th></tr></thead><tbody><tr><td rowspan="10">Strong secrecy</td><td rowspan="6">Denning-Sacco</td><td>3</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td><td>✓ 11s</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>6</td><td>✓ &lt;1s</td><td>✓ 1s</td><td>OM</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>7</td><td>✓ 6s</td><td>✓ 3s</td><td></td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>10</td><td>OM</td><td>✓ 9m49</td><td>OM</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>12</td><td></td><td>OM</td><td>OM</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>29</td><td></td><td></td><td>OM</td><td>✓ &lt;1s</td><td>✓ 1s</td></tr><tr><td rowspan="6">Wide Mouth Frog</td><td>3</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td><td>✓ 5s</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>6</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td><td>✓1h11m</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>7</td><td>✓ &lt;1s</td><td>✓ 1s</td><td>OM</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>10</td><td>✓ 10s</td><td>✓ 3m35</td><td></td><td>✓ &lt;1s</td><td>✓ 1s</td></tr><tr><td>12</td><td>✓22m16s</td><td>OM</td><td></td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>14</td><td>OM</td><td></td><td></td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td rowspan="10">Anonymity</td><td rowspan="6">Yahalom-Lowe</td><td>3</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td><td>✓ 7s</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>6</td><td>✓ 2s</td><td>✓ 41s</td><td>OM</td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>7</td><td>✓ 42s</td><td>✓34m38s</td><td></td><td>✓ 1s</td><td>✓ &lt;1s</td></tr><tr><td>10</td><td>OM</td><td>OM</td><td></td><td>✓ 1s</td><td>✓ &lt;1s</td></tr><tr><td>12</td><td></td><td>OM</td><td></td><td>✓ 4s</td><td>✓ 2s</td></tr><tr><td>14</td><td></td><td></td><td></td><td>✓ 7s</td><td>✓ 2s</td></tr><tr><td rowspan="6">Private Authentication</td><td>10</td><td>OM</td><td>OM</td><td></td><td>✓ 12s</td><td>✓ 8s</td></tr><tr><td>12</td><td></td><td>OM</td><td></td><td></td><td></td></tr><tr><td>14</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>17</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>15</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>15</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td rowspan="10">Unlinkability</td><td rowspan="6">3G-AKA</td><td>4</td><td>✓ 1m35s</td><td>✓ 1h23m</td><td></td><td>✓ &lt;1s</td><td>✓ 2s</td></tr><tr><td>6</td><td>OM</td><td>OM</td><td></td><td>✓ &lt;1s</td><td>✓ 2s</td></tr><tr><td>4</td><td>✓ &lt;1s</td><td>✓ 1s</td><td></td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>6</td><td>✓ 2m15s</td><td>✓ 1m27s</td><td></td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>7</td><td>✓ 1h40m</td><td>✓ 1m44s</td><td></td><td>✓ &lt;1s</td><td>✓ 1s</td></tr><tr><td>9</td><td>OM</td><td>OM</td><td></td><td>✓ &lt;1s</td><td>✓ 9s</td></tr><tr><td rowspan="6">Passive Authentication</td><td>15</td><td></td><td>OM</td><td></td><td>✓ &lt;1s</td><td>✓ 15s</td></tr><tr><td>21</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td rowspan="2">BAC</td><td>4</td><td>OM</td><td>OM</td><td></td><td>✓ 1s</td><td>OM</td></tr><tr><td>6</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td rowspan="6">Prêt-à-Voter</td><td>6</td><td>OM</td><td>OM</td><td></td><td>✓ &lt;1s</td><td>✓ 2s</td></tr><tr><td>6</td><td>✓ 47s</td><td>OM</td><td></td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>10</td><td></td><td></td><td></td><td>✓ &lt;1s</td><td>✓ &lt;1s</td></tr><tr><td>11</td><td>OM</td><td>OM</td><td></td><td>✓ 7m 24s</td><td>✓ 1h 38m</td></tr><tr><td>12</td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>12</td><td></td><td></td><td></td><td></td><td></td></tr></tbody></table>
edge. The notion of solution of constraint system is also extended to capture their expected properties.

### 4.1.1 Knowledge base and formulas

**New constraints** From now on we assume the existence of a rewriting system $\mathcal{R}$ that is constructor-destructor and subterm convergent (we recall that the results of the previous sections did not rely on this assumption). All our definitions, lemmas and theorems will thus implicitly depend on this rewriting system. We introduce an extension of constraint systems with second-order constraints that serve key roles in the generation of the partition tree:

* Giving a finite representation of the deductive capabilities of the attacker.

This takes the form of a knowledge base $K$ which is a finite set of deduction facts. By relying on subterm convergence among others, our procedure will ensure that a term $u$ is deducible iff it can be deduced by applying constructor symbols to deduction facts of $K$, which makes deducibility easily decidable due to the constructor-destructor property. In particular we will only consider solutions that compute terms using entries of $K$ in this restricted manner.

* Giving a finite representation of the distinguishing capabilities of the attacker.

This takes the form of a set of formulas $F$ that is, in short, a finite representation of the term equalities that hold in the current frame. In particular static equivalence will be characterisable only from the formulas of $F$.

* Recording the constraints imposed on second-order solutions during the constraint solving.

When computing most general solutions or performing case analyses on the form of solutions, we track the resulting effect on second-order solutions in a set $E^2$ that is the second-order analogue of $E^1$. This is mostly how we model the predicates $\pi$ that appear in the configurations in partition trees (Definition 3.16).

More formally we consider, in addition to deduction facts and second-order equations, a new atomic second-order constraint, equality facts $\xi =_f^? \zeta$, $\xi$ and $\zeta$ second-order terms. Unlike second-order equations that model syntactic equalities, equality facts capture equalities modulo theory, that is, the fact that $\xi$ and $\zeta$ deduce the same first-order term. Concretely we extend the relation $\models$ (Section 3.3) with

$$ (\Phi, \Sigma, \sigma) \models \xi =_f^? \zeta \quad \text{iff} \quad \xi\Sigma\Phi\sigma\downarrow = \zeta\Sigma\Phi\sigma\downarrow $$

We now define the constraints that are typically put in the set $F$.

**DEFINITION 4.1 (deduction formula, equality formula).** A deduction (resp. equality) formula is a constraint of the form $\forall S. H \leftarrow (C_1 \wedge \dots \wedge C_n)$:

1. $S$ is a set of (both first-order and second-order) variables;
2. $H$ is a deduction fact (resp. an equality fact);

3. for all $i \in \{1, \dots, n\}$, $C_i$ is either a deduction fact of the form $X \vdash? t, X \in \mathcal{X}^2$, or a first-order syntactic equation $u =? v$.

A formula $\psi$ is called solved when it contains no hypotheses, i.e., $\psi = (\forall \emptyset. H \Leftarrow \top) = H$. Given a formula $\psi = \forall S. H \Leftarrow \varphi$, we denote by $\text{hyp}(\psi)$ the set of the syntactic equations appearing in the hypotheses $\varphi$, and by $\text{D}(\psi)$ the set of deduction facts in $\varphi$.

Intuitively, a formula captures a deduction or comparison that the attacker may perform and the premises $C_1, \dots, C_n$ express conditions under which this is possible. Typically if the attacker observed a ciphertext $\text{senc}(m, r, k)$ (bound to an axiom $ax$), we may express the deducibility of $m$ through the formula

$$ \forall X. \text{sdec}(ax, X) \vdash? m \Leftarrow X \vdash? k $$

Another example is the following formula that expresses the tautology that two recipes deducing the same term should be equal in the sense of an equality fact:

$$ \forall X, Y, z. X =?_f Y \Leftarrow (X \vdash? z \land Y \vdash? z) $$

This formula will serve as a generic placeholder when computing equality formulas during the constraint solving, that is, we will always add equality formulas obtained by substituting variables in the above formula. Although we consider arbitrary formulas such as the above two during the computation of the partition tree, note that only formulas of a certain shape will eventually be added in the set $F$ recording the attacker's distinguishing capabilities. We give more details about the invariants of the procedure in Appendix B.1, but we can mention for example that the formulas effectively recorded in $F$ will be of the form $H \Leftarrow \varphi$, i.e., there are no universally-quantified variables, and $\varphi$ only contains first-order equations.

**Extended constraint systems** We now formalise how we extend constraint systems to store the knowledge base, formulas, and to capture restrictions on the form of solutions.

**DEFINITION 4.2 (extended constraint system).** A tuple $C^e = (\Phi, D, E^1, E^2, K, F)$ is called an *extended constraint system* where:

1. $(\Phi, D, E^1)$ is a constraint system, although more general in that $D$ may contain constraints of the form $X \vdash? u$ or $\forall X. X \kappa? u$ where $u$ may be an arbitrary constructor term;

2. $E^2$ is a set of second-order equations and constraints of the form $\forall Y_1, \dots, Y_k. \bigvee_{j=1}^p \xi_j \neq? \zeta_j$

3. $K$ is a set of deduction facts;

4. $F$ is a set of deduction and equality formulas.

As explained earlier, the set $E^2$ gathers constraints to be satisfied by the second-order solutions of the system, $K$ is a finite representation of the attacker knowledge, and $F$ characterises
the attacker capabilities to deduce and compare terms modulo theory. In particular the set $E^2$ contains additional constraints to be satisfied by solutions while K and F are valid formulas that characterise potential attacker actions. For example, the (unsolved) deduction formulas in F reason about potentially deducible terms: when such formula contains premisses, the procedure will perform a case analysis to distinguish cases where the hypotheses hold or not, leading to solved or trivial formulas, respectively. When a solved deduction formula is obtained this way, we add it to the knowledge base K if u is not already deducible from it.

### 4.1.2 (Most general) solutions

We now define how the notion of solutions is lifted to extended constraint systems and how this embeds the predicates $\pi$ used in the definition of partition-tree configurations. The definition of a solution $(\Sigma, \sigma)$ of $C^e$ follows three guidelines: 1. it should be a solution in the usual sense and satisfy $E^2(C^e)$; 2. the set of formulas $F(C^e)$ plays no role in the definition of solutions: we will only prove invariants that this set verifies during our specific constraint-solving procedure (see Appendix B, Section B.1); and 3. all recipes used in the solution should have been constructed from the knowledge base $K(C^e)$, uniformly (that is, a same first-order term should not be deduced by different recipes in the solution). In particular this requires a notion of consequence, indicating that a recipe can be deduced from the knowledge base.

**DEFINITION 4.3 (consequence).** We define the set of consequences of a set of deduction facts $S$, denoted Conseq($S$), as the set of pairs $(C[\xi_1, \dots, \xi_n], C[u_1, \dots, u_n])$ where $C$ is a context built using $F_c \cup F_0$ and for all $i \in \{1, \dots, n\}$, $\xi_i \vdash^? u_i \in S$. We write $\xi \in \text{Conseq}(S)$ if $\exists t. (\xi, t) \in \text{Conseq}(S)$.

We recall that by definition a deduction fact never has a constructor function symbol at its root (Definition 3.4): in particular if $\xi \in \text{Conseq}(S)$, the context $C$ in the above definition is unique. Writing $\xi = C[\xi_1, \dots, \xi_n]$ it is therefore possible to define unambiguously the set of consequential subterms of $\xi$

$$st_c(\xi, S) = \{\xi|_p \mid p \text{ position of } C\}$$

If $R$ is a set of recipes we write $st_c(R, S) = \cup_{\xi \in R} st_c(\xi, S)$. From this we can define solutions of extended constraint systems.

**DEFINITION 4.4 (solution of an extended constraint system).** A pair of substitutions $(\Sigma, \sigma)$ is a solution of $(\Phi, D, E^1, E^2, K, F)$ if $(\Phi, \Sigma, \sigma) \models D \wedge E^1 \wedge E^2$ and the following two properties hold:

1. **K-Basis:** for all $\xi \in st^2(img(\Sigma) \cup K\Sigma)$, $msg(\xi\Phi\sigma)$ and $(\xi, \xi\Phi\sigma\downarrow) \in \text{Conseq}(K\Sigma\sigma)$

2. **Uniformity:** for all $\xi, \xi' \in st_c(img(\Sigma), K\Sigma)$, $\xi\Phi\sigma\downarrow = \xi'\Phi\sigma\downarrow$ implies $\xi = \xi'$.
The set of solutions of $C^e$ is written $Sol(C^e)$ and $C^e$ is satisfiable if $Sol(C^e) \neq \emptyset$. We will denote by $\perp$ an unsatisfiable extended constraint system. The notion of most general solution of $C^e$ is adapted in a straightforward way from the analogue for regular constraint systems.

Intuitively when computing a node $n$ of a partition tree, the extended constraint systems represent the predicate $\pi(n)$: it will be defined so that given $(\mathcal{P}, C) \in \Gamma(n)$ attached with $C^e$, we have $Sol^{\pi(n)}(C) = Sol(C^e)$ (up to domain restriction). We detail this in Sections 4.1.3 and 4.5.

**EXAMPLE 4.5.** Consider the extended constraint system $C^e$ defined by

$$ \Phi = \{ax_1 \mapsto \langle k, x \rangle\} \quad D = X:0 \vdash^? x \wedge Y:1 \vdash^? y \quad E^1 = y =? x \quad E^2 = \top \quad K = ax_1 \vdash^? \langle k, x \rangle \\ F = K \wedge \text{fst}(ax_1) \vdash^? k \wedge \text{snd}(ax_1) \vdash^? x \wedge X =? f \wedge \text{snd}(ax_1) $$

This system involves an adversarial input $x$ computable from an empty frame, which produces in response an output of $\langle k, x \rangle$ for some name $k$, and then the adversary inputs again $y = x$. The set $F$, although not impacting the notion of solution, characterises here all successful operations that the attacker may perform in this situation: applying destructors to the term bound to $ax_1$ and observe that $X$ and $\text{snd}(ax_1)$ deduce the same term.

We have for example $(\langle X, ax_1 \rangle, \langle x, \langle k, x \rangle \rangle) \in \text{Conseq}(K \cup D)$. However the knowledge base is not saturated in the sense that there are deducible terms $u$, for example $u = k$, such that there exist no recipes $\xi$ such that $(\xi, u) \in \text{Conseq}(K \cup D)$. In our procedure, the saturation is done by adding to $K$ all destructor applications that result into a non-consequence term. A saturated version of the constraint system would be

$$ C_s^e = C^e [K \mapsto K \wedge \text{fst}(ax_1) \vdash^? k] $$

Note that adding the deduction fact $\text{snd}(ax_1) \vdash^? x$ to the knowledge base is possible but redundant since $x$ is already deducible from $X$. The saturation ensures that for all $(\Sigma, \sigma)$ satisfying $D(C_s^e) \wedge E^1(C_s^e) \wedge E^2(C_s^e)$, there exists $\Sigma'$ such that $(\Sigma', \sigma) \in Sol(C_s^e)$, meaning that the requirement that solutions verify K-basis can always be satisfied (which is key for satisfying the requirement that all symbolic transitions are reflected in the partition tree, recall Item 2 of Definition 3.17). Let us then consider

$$ \Sigma = \{X \mapsto a, Y \mapsto \text{snd}(ax_1)\} \quad \Sigma' = \{X \mapsto a, Y \mapsto a\} \quad \sigma = \{x \mapsto a, y \mapsto a\} $$

Both $(\Sigma, \sigma)$ and $(\Sigma', \sigma)$ are solutions of the regular constraint system $(\Phi(C_s^e), D(C_s^e), E^1(C_s^e))$, but only $(\Sigma', \sigma)$ is a solution of $C^e$. This is because $\Sigma$ does not verify uniformity: two different recipes $a$ and $\text{snd}(ax_1)$ are used to deduce the same first-order term $a$. More generally we have $mgs(C_s^e) = \{Y \mapsto X\}$. To obtain this result, the constraint-solving procedure for computing mgs', detailed in Section 4.2, will observe that $X$ and $Y$ deduce the same term and should therefore be unified to satisfy uniformity. A second-order equation $X =? Y$ is thus added in $E^2$, whose mgu is then the expected most general solution. ♦
**REMARK 4.6 (uniformity and complexity).** In some sense enforcing that solutions are uniform ensures their minimality in terms of DAG size, by forcing identical recipes to be reused as much as possible when constructing the solution. This will be key for the complexity of our decision procedure, see Section 5.2.

### 4.1.3 Constraint Solving: the basics

Now we give details about the organisation of our constraint solver, detailed and proved correct in the next sections. As explained in Section 4.1.2, the goal of extended constraint system is to carry additional, structural information about solutions in a node $n$, thus playing the role of the predicate $\pi(n)$. More formally the procedure operates on:

**DEFINITION 4.7 (extended symbolic process, vector).** An *extended symbolic process* is a tuple $(\mathcal{P}, \mathcal{C}, \mathcal{C}^e)$ where $(\mathcal{P}, \mathcal{C})$ is a symbolic process and $\mathcal{C}^e$ an extended constraint system. We call a *vector* a set of sets of extended symbolic processes $\mathcal{S} = \{\Gamma_1, \dots, \Gamma_n\}$. Each set $\Gamma_i$ is called a *component* of $\mathcal{S}$.

An extended symbolic process $(\mathcal{P}, \mathcal{C}, \mathcal{C}^e)$ induces a predicate $\pi$ on the solutions of $(\mathcal{P}, \mathcal{C})$ defined as follows: if $(\Sigma, \sigma) \in \text{Sol}(\mathcal{C})$, then $\pi(\Sigma)$ holds *iff* there exists $(\Sigma', \sigma') \in \text{Sol}(\mathcal{C}^e)$ such that $\Sigma \subseteq \Sigma'$ and $\sigma \subseteq \sigma'$. In particular $\text{Sol}^\pi(\mathcal{C}) = \text{Sol}(\mathcal{C}^e)$ (up to domain restriction). However, we recall that, in the definition of the node of a partition tree (configurations, Definition 3.16), only *one* common predicate $\pi$ is used for all constraint systems $\mathcal{C}$ of the configuration $\Gamma$. For consistency, we therefore have to impose conditions ensuring that the predicates $\pi$ corresponding to each $\mathcal{C} \in \Gamma$ are all identical. Given a set of constraint systems $\Gamma$ such that this property is not verified, the goal of the constraint-solving procedure is thus to refine $\Gamma$ until obtaining a vector $\mathcal{S} = \{\Gamma_1, \dots, \Gamma_n\}$ such that

1. each component $\Gamma_i$ can be used to model a partition-tree node, that is, a predicate $\pi_i$ can be defined as above uniformly across all elements of $\Gamma_i$;

2. the underlying nodes verify the properties of the partition tree w.r.t. their father node $\Gamma$.

The procedure takes the form of various reduction relations that are used to refine a set of sets of extended symbolic processes, progressively, until reaching the final vector $\mathcal{S}$:

1. A set of rules to compute *most general solutions* (Section 4.2).

2. A set of *symbolic rules* (Section 4.3.1) that formalise how to apply symbolic transitions to extended symbolic processes.

3. Various sets of *simplification rules* (Sections 4.2.3, 4.3.2 and 4.3.3) that simplify vectors to remove unsatisfiable systems, or to split components that contain processes with non-statically-equivalent solutions.
4. A set of case distinction rules (Section 4.4) that refines the current vector based on case analyses to enforce the various properties of the partition tree (unique mgs in each component, maximal components w.r.t. static equivalence...).

The overall procedure organising the above sets of rules into a complete algorithm to compute a partition tree is then detailed in Section 4.5. This can therefore be seen as the detailed version of the outline provided in Section 3.7. The main arguments for proving the correctness of the computation are also provided in Section 4.5; note however that these are only arguments of partial correctness: the termination of the procedure is later justified in Section 5.2.

## 4.2 Constraint Solving: computing most general solutions

### 4.2.1 Applying solutions and unifiers

Because solutions $\Sigma$ may introduce new second-order variables, their applications to a constraint system or a formula is not straightforward. Let for example $C^e = (\Phi, D, E^1, E^2, K, F)$ where a variable $X:k$ is used to deduce a term $u$, i.e. $(X \vdash^? u) \in D$. Now say we want to consider the scenario where $u$ is computed using a constructor $f/3$ and an entry of the knowledge base $(\xi \vdash^? v) \in K$ as a first argument, that is, we want to apply to $C^e$:

$$ \Sigma = \{X \to f(\xi, X_1, X_2)\} \qquad X_1, X_2 \text{ fresh} $$

The raw application $C^e\Sigma$ has a flawed structure, in particular because the variables $X_1$ and $X_2$ would not be bound in the resulting system. To solve this issue we use a custom application mechanism that replaces $X \vdash^? u$ in $D$ by $X_1 \vdash^? x_1, X_2 \vdash^? x_2, x_1, x_2$ fresh, and we add the equality $u =? f(v, x_1, x_2)$ to $E^1$ to express the logical link between $X$ and $X\Sigma = f(\xi, X_1, X_2)$.

**DEFINITION 4.8 (application of a substitution to an extended constraint system).** Let $C^e = (\Phi, D, E^1, E^2, K, F)$ and $\Sigma$ be a substitution. We write $C^e:\Sigma$ the constraint system:

$$ (\Phi, D', E^1 \wedge E_\Sigma, E^2 \wedge \Sigma_{|vars^2(C^e)}, K\Sigma, F\Sigma) $$

where $D' = (D \setminus D_{dom}) \cup D_{fresh}$ with the sets of:

1. deduction facts removed by the application of $\Sigma$: $D_{dom} = \{Y \vdash^? u \in D \mid Y \in dom(\Sigma)\}$

2. binding facts: $D_{fresh} = \{Y \vdash^? y \mid Y \in vars^2(img(\Sigma_{|vars^2(C^e)})) \wedge vars^2(C^e), y \text{ fresh}\}$

3. linking equations: $E_\Sigma = \{u =? v \mid Y \vdash^? u \in D_{dom}, (Y\Sigma, v) \in Conseq(K\Sigma \cup D')\}$

By abuse of notation we may write $S:\Sigma$ for $(\mathcal{P}, C, C^e:\Sigma)$ if $S = (\mathcal{P}, C, C^e)$.

We will also use a similar mechanism for applying substitutions to formulas:

**DEFINITION 4.9 (application of a substitution to a formula).** Let $C^e = (\Phi, D, E^1, E^2, K, F)$, $\psi = \forall S. H \Leftarrow \varphi$ be a formula, and $\Sigma$ be a substitution. We denote $\psi:(\Sigma, C^e)$ (or $\psi:(\Sigma, S)$ by abuse
of notations if $S = (\mathcal{P}, C, C^e)$) the formula

$$ \forall S'. H\Sigma \leftarrow (D' \wedge \text{hyp}(\psi) \wedge E_\Sigma) $$

where $D' = (D(\psi) \setminus D_{dom}) \cup D_{fresh}$, $S' = (S \setminus dom(\Sigma)) \cup vars^1(D_{fresh})$ and:

1. $D_{dom} = \{Y \vdash^? u \in D(\psi) | Y \in dom(\Sigma)\}$

2. $D_{fresh} = \{Y \vdash^? y | Y \in vars^2(img(\Sigma)) \setminus vars^2(C, \psi), y \text{ fresh}\}$

3. $E_\Sigma = \{u =? v | Y \vdash^? u \in D_{dom}, (Y\Sigma, v) \in \text{Conseq}(K \cup D \cup D')\}$

### 4.2.2 Constraint-solving rules

**A complete example** By definition, the solutions of an extended constraint systems $C^e$ have to verify $K(C^e)$-basis, which means that in practice we only have to compute solutions constructed by applying constructors to the entries of the knowledge base and D. Besides due to the uniformity requirement we can always unify two recipes that deduce the same first-order term. Putting everything together the most general solutions of an extended constraint system can then be computed with a simple transition system. Let us detail a complete example to illustrate the mechanisms in play, before formalising the corresponding constraint-solving rules.

**EXAMPLE 4.10.** Given $k, r \in \mathcal{N}$, let us consider a situation where the attacker has observed the output of a hash $h(r)$, then inputs a term $x$, receives in response a ciphertext $aenc(k, r, x)$ encrypted with $x$, and finally inputs a term $y$ that should verify the equation $y =? \langle k, h(x) \rangle$. This is modelled by the frame $\Phi = \{ax_1 \mapsto h(r), ax_2 \mapsto aenc(k, r, x)\}$ and the constraints

$$ D = X:1 \vdash^? x \wedge Y:2 \vdash^? y $$

$$ E^1 = y =? \langle k, h(x) \rangle $$

At this point a saturated knowledge base should contain the two entries of the frame and one recipe indicating that decrypting $ax_2$ results in obtaining the name $k$.

$$ K = ax_1 \vdash^? h(r) \wedge ax_2 \vdash^? aenc(k, r, x) \wedge adec(ax_2, X) \vdash^? k $$

We consider that $E^2 = \top$ and we leave the set of formulas F unspecified since it has no influence on solutions. First of all some simplification rules will be applied to propagate the equations on $x$ and $y$ to the whole system; here it will apply $mgu(E^1)$ to D, resulting in

$$ D = X \vdash^? x \wedge Y \vdash^? \langle k, h(x) \rangle $$

The constraint-solving rules detailed in the remaining of this section consider all ways to compute recipes for $X$ and $Y$ from the knowledge base. For each of these recipes two cases arise: either 1. it is picked directly from the knowledge base; or 2. it starts with a constructor symbol. This will correspond to the constraint-solving rules (MGS-RES) and (MGS-CONS), respectively. Finally, to satisfy the uniformity property, the procedure unifies any second-order terms in the
system that deduce the same first-order term (Rule (MGS-CONSEQ)). We keep on refining the case analysis with these three rules, removing branches yielding contradictions, until no more rules are applicable. The resulting systems will either have no solutions, or be in a so-called solved form and have mgu(E²) as a unique mgs. Let us do it for our example:

### ▶ case 1: the recipe for Y has a constructor symbol at its root (only possible case)

The constructor in question is necessarily the pair. Therefore we let two fresh second-order variables $Y_1:2$, $Y_2:2$ and apply the substitution $\{Y \mapsto \langle Y_1, Y_2 \rangle\}$ to the system (in the sense of Definition 4.8). After simplification this leads to the updated second-order constraints:

$$D = X \vdash^? x \wedge Y_1 \vdash^? k \wedge Y_2 \vdash^? h(x) \qquad E^2 = Y =? \langle Y_1, Y_2 \rangle$$

### ▶ case 1.1: the recipe for $Y_1$ is $\mathrm{adec}(ax_2, X)$ from the knowledge base (only possible case)

We thus apply the substitution $\{Y_1 \mapsto \mathrm{adec}(ax_2, X)\}$, resulting in the updated constraints:

$$D = X \vdash^? x \wedge Y_2 \vdash^? h(x) \qquad E^2 = Y =? \langle \mathrm{adec}(ax_2, X), Y_2 \rangle \wedge Y_1 =? \mathrm{adec}(ax_2, X)$$

### ▶ case 1.1.1: the recipe for $Y_2$ is the entry $ax_1$ from the knowledge base

We therefore apply the substitution $\{Y_2 \mapsto ax_1\}$, resulting in the updated constraints:

$$D = X \vdash^? r \qquad E^2 = Y =? \langle \mathrm{adec}(ax_2, X), ax_1 \rangle \wedge Y_1 =? \mathrm{adec}(ax_2, X) \wedge Y_2 =? ax_1$$

However the constraints on $X$ are now unsatisfiable: the corresponding recipe can neither start with a constructor nor be an entry of the knowledge base. The constraints in this branch of the case analysis therefore have no solutions.

### ▶ case 1.1.2: the recipe for $Y_2$ has a constructor symbol at its root

The constructor in question is necessarily $h$. Similarly to case 1 we apply the substitution $\{Y_2 \mapsto h(Y_3)\}$ for some fresh variable $Y_3:2$ which results in the updated constraints:

$$D = X \vdash^? x \wedge Y_3 \vdash^? x \qquad E^2 = Y =? \langle \mathrm{adec}(ax_2, X), h(Y_3) \rangle \wedge Y_1 =? \mathrm{adec}(ax_2, X) \wedge Y_2 =? h(Y_3)$$

Then we observe that $X$ and $Y_3$ should be unified by uniformity because they deduce the same first-order term $x$. We have $\mathrm{mgu}(X =? Y_3) = \{Y_3 \mapsto X\}$ (we recall that $\{X \mapsto Y_3\}$ is not a valid second-order substitution because $Y_3$ has a strictly greater type than $X$) which, after application to the system, results in the updated constraints:

$$D = X \vdash^? x \qquad E^2 = Y =? \langle \mathrm{adec}(ax_2, X), h(X) \rangle \wedge Y_1 =? \mathrm{adec}(ax_2, X) \wedge Y_2 =? h(X) \wedge Y_3 =? X$$

This will be a typical example of system in solved form. Since we considered all cases and only this branch was successful we conclude that the overall system has a unique mgs which is $\mathrm{mgu}(E^2) = \{Y \mapsto \langle \mathrm{adec}(ax_2, X), h(X) \rangle\}$. ♦

<figure><img src="image_10.png" /></figure>
**Formalisation** We will formalise the simplification rules in the next section and focus here on the main three rules (MGS-CONSEQ), (MGS-RES) and (MGS-CONS) mentioned in the above example. For that we reason about a set $R(C^e)$ that represents all recipes that are already used to constraint the solutions of $C^e$:

$$R(C^e) = st_c(\mathrm{img}(\mathrm{mgu}(E^2(C^e)), K(C^e) \cup D(C^e)) \cup \mathrm{vars}^2(D(C^e)))$$

As we saw in the example, the mgs is gradually constructed “within $E^2$”, in the sense that after normalising $C^e$ with the transition system defined in this section, it will have $mgu(E^2)$ as a unique mgs. In particular an invariant of our transition system is that $\mathrm{img}(mgu(E^2(C^e)))$ is consequence of $K(C^e)$ and $D(C^e)$, hence the notation $R(C^e)$ is well defined. Formally speaking the transition system relies on three rules of the form

$$C^e \xrightarrow{\Sigma} C^e:\Sigma \qquad (\star)$$

for some substitution $\Sigma$ and under various conditions capturing the possible ways to satisfy the constraints of $C^e$. The uniformity property is expressed by applying $(\star)$ with

$$\begin{array}{l}
\Sigma = mgu(\xi =? \zeta) \text{ for some } \xi \in R(C^e) \cup \mathcal{F}_0, \zeta \in R(C^e), \text{ and provided} \\
\Sigma \neq \top, \Sigma \neq \bot, \text{ and } \exists u.(\xi, u), (\zeta, u) \in \mathrm{Conseq}(K(C^e) \cup D(C^e))
\end{array}
\qquad (\mathrm{MGS-CONSEQ})$$

The result is the unification in $C^e$ of the two second-order terms $\xi$ and $\zeta$ that deduce the same term $u$. It then remains to add rules that express how each term $u$, $(X \vdash^? u) \in D(C^e)$, can be constructed by the adversary from the knowledge base. When Rule (MGS-CONSEQ) is not applicable we thus apply $(\star)$ under one of the following two conditions. The first one expresses that $u$ is computed by directly using an entry from the knowledge base:

$$\begin{array}{l}
\Sigma = mgu(X =? \xi) \neq \bot \text{ where, for some } u \notin \mathcal{X}, \text{ there exist deduction facts} \\
(X \vdash^? u) \in D(C^e) \text{ and } (\xi \vdash^? v) \in K(C^e)
\end{array}
\qquad (\mathrm{MGS-RES})$$

Then the last rule expresses that the computation of $u$ starts by applying a constructor $f$:

$$\Sigma = \{X \to f(X_1, \dots, X_n)\} \text{ where } X_1:k, \dots, X_n:k \text{ are fresh, and there exists} \\
\text{a deduction fact } (X:k \vdash^? f(u_1, \dots, u_n)) \in D(C^e) \qquad (\mathrm{MGS-CONS})$$

As said above we always apply Rule (MGS-CONSEQ) in priority, that is, we add to the last two rules the condition that Rule (MGS-CONSEQ) cannot be applied. This will be crucial in particular when studying the complexity of the procedure in Section 5.2.

### 4.2.3 First set of simplification rules

To effectively compute most general solutions, the above three rules are applied repeatedly, but some simplification rules are also used in between. Their role is to put the constraint systems in a simpler form and in particular to detect the unsatisfiable systems. Other simplification rules,
serving different purposes, will be introduced later in the procedure. The rules here are of two kinds:

1. *simplification rules for formulas* that simply compute mgu and simplify the hypotheses of formulas; and

2. *simplification rules for mgs'* that apply mgu to the rest of the system, and detect unsatisfiability through contradictions or violations of uniformity.

**Simplification rules for formulas** We first introduce basic simplification rules for formulas that will be used even outside of the computation of most general solutions. We define five sets rules in Figure 7 that apply on constraints of $E^1$, $E^2$ and $F$.

<figure><img src="image_11.png" /><figcaption>**Figure 7.** Simplification rules on formulae</figcaption></figure>

We recall that, in the case of the simplification of second order disequations, the computation of mgu may introduce new variables to match arities (see Section 3.2), hence the need for the universal quantified variables $S'$. No rules are needed for second-order equations in the context of our decision procedure, since Rules (MGS-CONSEQ), (MGS-RES) and (MGS-CONS) already apply mgu to the entire system. The simplification rules are lifted to extended constraint systems $C^e$ in the natural way, by applying the simplifications to all formulas of $E^1(C^e)$, $E^2(C^e)$ and $F(C^e)$.
**Simplification rules for MGS** In addition of the rules of Figure 7 we define a couple of other rules specific to the computation of most general solutions. First of all the rule

$$ (\Phi, D, E^1 \wedge x =? u, E^2, K, F) \rightsquigarrow (\Phi\sigma, D\sigma, E^1\sigma \wedge x =? u, E^2, K\sigma, F\sigma) \quad (\text{MGS-UNIF}) $$

where $x \in vars^1(E^1, D, \Phi, K, F) \setminus vars(u)$ and $\sigma = \{x \mapsto u\}$, propagates first-order mgu in the whole system. We also consider the following rule discarding a system with no solutions

$$ C^e \rightsquigarrow \perp \quad (\text{MGS-UNSAT}) $$

where either of the following three conditions is satisfied:

1. $E^1 = \perp$

2. there exist $\xi, \zeta \in R(C^e)$ such that $(\xi, u), (\zeta, u) \in \text{Conseq}(K(C^e) \cup D(C^e))$ and, writing $\Sigma = \text{mgu}(\xi =? \zeta)$, either $\Sigma = \perp$ or $E^2\Sigma \rightsquigarrow \perp$ with the rules of Figure 7

3. there exist $(\forall X:i. X \kappa? u) \in D(C^e)$ and $\xi \in \mathcal{T}_i^2$ such that $(\xi, u) \in \text{Conseq}(K(C^e) \cup D(C^e))$

The first condition captures trivially unsatisfiable systems, the second one captures systems with no uniform solutions, and the third one exhibits a public channel that has been used for an internal communication (which is forbidden by the semantics). Since the whole set of simplification rules (Figure 7 and the above two) is convergent modulo renaming of variables, we denote $C_\xi$ a normal form of the extended constraint system $C$ w.r.t. $\rightsquigarrow$.

### 4.2.4 Overall procedure and correctness

**Description of the procedure** The point of the transition systems above is to transform an extended constraint system into a form where it has a unique mgs. More formally:

**DEFINITION 4.11 (solved extended constraint system).** An extended constraint system $C^e$ is in solved form if $C^e \neq \perp$, $C^e$ is irreducible w.r.t. $\rightsquigarrow$ and $\xrightarrow{\Sigma}$, and all deduction facts in $D(C^e)$ have variables as first-order terms.

Intuitively for such constraint systems, $\text{mgu}(E^2(C^e))$ is the unique mgs of $C^e$. Note however that this method for computing mgs' is only correct under some invariants of our overall procedure. Typically, since second-order equations are not handled by simplification rules, if $E^2$ contains two contradictory equations $X =? a \wedge X =? b$ for two constants $a \neq b$, our procedure would fail to detect the contradiction. If we define the reduction relation $\Rightarrow\Sigma$ as the reflexive transitive closure of the composition of relations $\xrightarrow{\sigma}\xi$, then under the invariants of the procedure we compute a set of most general solutions of $C^e$ as the set $\{\Sigma|_{vars^2(C^e)} | C^e \Rightarrow\Sigma C^{e'}, C^{e'} \text{ solved}\}$.

**REMARK 4.12 (notation for extended symbolic processes).** For convenience we often abuse notations and, if $S = (\mathcal{P}, C, C^e)$ is an extended symbolic process, we write $mgs(S)$ instead of $mgs(C^e)$ or say that $S$ is in solved form.
**Correctness arguments** As mentioned earlier this procedure is only correct under some additional properties verified all along Algorithm 1. For the sake of precision we make explicit mention to these two invariants, $Inv_{wf}(C^e)$ and $Inv_{sound}(C^e)$. They are formally defined in Appendix B.1 with a proof that they are preserved during the whole computation of the partition tree, but knowing their exact definition is not necessary to understand the results of this section. The core correctness arguments can be decomposed into following propositions, and are derived from the results proved in Appendix B.4. The first one states that when an extended constraint system cannot be reduced any more then its set of most general solutions is either empty or a singleton:

**PROPOSITION 4.13 (mgs of an irreducible system).** Let $C^e$ be an extended constraint system that is irreducible w.r.t. $\rightsquigarrow$ and $\xrightarrow{\Sigma}$, and such that the invariants $Inv_{wf}(C^e)$ and $Inv_{sound}(C^e)$ hold. Then

1. if $C^e$ is in solved form then mgs($C^e$) = {$mgu(E^2(C^e))$}

2. otherwise mgs($C^e$) = $\emptyset$

The second argument is that applying the mgs constraint-solving rules is correct w.r.t. the solutions of the initial system.

**PROPOSITION 4.14 (soundness of one step of the mgs constraint solving).** Let $C^e$ be an extended constraint system with $C^e = C^e_{\xi}$. If $C^e \xrightarrow{\Sigma} C^{e'}$ and $(\Sigma', \sigma) \in Sol(C^{e'})$ then $(\Sigma'_{|vars^2(C^e)}$, $\sigma_{|vars^1(C^e)}$) $\in Sol(C^e)$.

Finally the last argument formalises than all solutions can be expressed as a sequence of mgs constraint-solving transitions.

**PROPOSITION 4.15 (completeness of one step of the mgs constraint solving).** Let $C^e$ be an extended constraint system such that $C^e_{\xi} = C^e$ and the invariants $Inv_{wf}(C^e)$ and $Inv_{sound}(C^e)$ hold. We also assume that at least one mgs constraint-solving rule is applicable to $C^e$. Then for all $(\Sigma, \sigma) \in Sol(C^e)$, there exist a constraint-solving transition $C^e \xrightarrow{\Sigma_0} C^{e'}$ and $\Sigma \subseteq \Sigma'$, $\sigma \subseteq \sigma'$ such that $(\Sigma', \sigma') \in Sol(C^{e'})$.

Together these three results give the partial correctness of the procedure, that is, the correctness of the computation when it terminates. The termination is studied in Section 5.2:

**THEOREM 4.16 (partial correctness of mgs computation).** Let $C^e$ be an extended constraint system such that $Inv_{wf}(C^e)$ and $Inv_{sound}(C^e)$ hold. Then, assuming there exist no infinite sequences of $\xrightarrow{\Sigma}$ reductions from $C^e$, we have

$$mgs(C^e) = \{\Sigma_{|vars^2(C^e)} | C^e \xrightarrow{\Sigma} C^{e'}, C^{e'} \text{ solved}\}$$
**PROOF.** Since a set of mgs' of $C^e \frown \xi$ is also a set of mgs' of $C^e$, we assume without loss of generality that $C^e \frown \xi = C^e$. Let us write $S = \{\Sigma_{|vars^2(C^e)} | C^e \stackrel{\Sigma}{\Rightarrow} \frown \xi C^{e'}, C^{e'}$ solved\}$ and prove that $S$ is a set of mgs' of $C^e \frown \xi$. By the termination assumption, we can reason by well-founded induction on the reduction relation $\to \frown \xi$ from $C^e$. Using such an induction we can prove the two requirements of the definition, that is:

1. that all $\Sigma \in S$ are solutions of $C^e$ after replacing their second-order variables by fresh constants (base case: Proposition 4.13; inductive case: soundness, i.e., Proposition 4.14).

2. that all solutions of $C^e$ are instances of a substitution of $S$ (base case: Proposition 4.13 again; inductive case: completeness, i.e., Proposition 4.15). ■

## 4.3 Constraint Solving: symbolic and simplification rules

### 4.3.1 Symbolic rules

The symbolic rules simply apply the transitions of the symbolic semantics to extended symbolic processes, adding the corresponding constraints to both the symbolic process and the extended constraint system. In that sense most rules are close to identical to those of the symbolic semantics (Section 3.4). Typically the analogue of the rule (S-IN) is:

$$ (\{u(x).P\} \cup \mathcal{P}, C, C^e) \xrightarrow{Y(X)}_S (\{P\} \cup \mathcal{P}, \text{incr}(C), \text{incr}(C^e)) \qquad (\text{E-IN}) $$

where, if $\mathcal{D} \in \{C, C^e\}$, incr($\mathcal{D}$) = $\mathcal{D}$[D $\mapsto$ D $\wedge$ X $\vdash^?$ x $\wedge$ Y $\vdash^?$ y, E$^1$ $\mapsto$ E$^1$ $\wedge$ $\sigma$] with Y:n, X:n and y fresh (n size of the domain of the frame of C), and $\sigma \in \text{mgu}_R(y =? u\mu)$, $\mu = \text{mgu}(E^1(C)) \neq \perp$. The only rule that is not a trivial extension of the symbolic semantics is the one for outputs that puts a deduction fact in F to model the additional capability this offers to the attacker:

$$ (\{\bar{u}\langle v \rangle.P\} \cup \mathcal{P}, C, C^e) \xrightarrow{\bar{Y}\langle ax_{n+1} \rangle} _S (\{P\} \cup \mathcal{P}, \text{incr}(C), \text{incr}(C^e)[F \mapsto F \wedge ax_{n+1} \vdash? v\sigma\downarrow]) \quad (\text{E-OUT}) $$

where, if $\mathcal{D} \in \{C, C^e\}$, incr($\mathcal{D}$) = $\mathcal{D}$[$\Phi \mapsto \Phi \cup \{ax_{n+1} \mapsto v\mu\sigma\downarrow\}$, D $\mapsto$ D $\wedge$ Y $\vdash^?$ y, E$^1$ $\mapsto$ E$^1$ $\wedge$ $\sigma$] with Y:n and y fresh (n size of the domain of the frame of C), and $\sigma \in \text{mgu}_R(y =? u\mu \wedge v\mu =? v\mu)$, $\mu = \text{mgu}(E^1(C)) \neq \perp$. We omit the definition of the remaining rules corresponding to the other symbolic transitions, all being constructed similarly to (E-IN) by copying the new constraints of C into $C^e$.

### 4.3.2 Normalisation rules

We define a new set of simplification rules, called normalisation rules, that operate on extended constraint systems. Similarly to the simplification rules for most general solutions introduced in Section 4.2.3 they propagate first-order unifiers across the system and replace unsatisfiable systems by $\perp$. They also rely on the computation of mgs' of Section 4.2, for example to identify
and remove trivial constraints such as formulas with unsatisfiable hypotheses. They are defined in Figure 8 and commented below (in particular regarding the definition of $\approx_r$).

<figure><img src="image_12.png" /><figcaption>**Figure 8.** Normalisation rules on extended constraint systems</figcaption></figure>

We recall that we also write $C^e \rightsquigarrow C^{e'}$ if a constraint of $E^1(C^e)$, $E^2(C^e)$ or $F(C^e)$ can be simplified using one of the simplification rules on formulas (Figure 7). The relation $\rightsquigarrow$ can be lifted to sets of (sets of) extended constraint systems or symbolic processes in the natural way. Let us now comment on the rules of Figure 8. Rule (NORM-UNIF) uses the same rule as in the mgs constraint solving to propagate first-order unifiers to the whole system. The next three rules exploit the existence of a most general solution of the constraint system to simplify some constraints:

1. Rule (NORM-NO-MGS) checks whether the constraint system is unsatisfiable, i.e., does not have a most general solution, and in this case transforms it into $\perp$.

2. Rule (NORM-DISEQ) similarly removes a disequation $\forall \tilde{x}.\phi$ in $E^1$ when it does not effectively restrict the solutions: for that we require the constraint system not to have solutions that contradict the disequation.

3. Analogously Rule (NORM-FORMULA) removes a formula with unsatisfiable hypotheses. The fact that we only consider the equations among the hypotheses (recall that hyp$\psi$ omits the hypotheses of $\psi$ that are deduction facts) is due to an invariant of our procedure. We will indeed ensure that formulae are only added to the set F after all deduction facts have been removed from hypotheses by appropriate solving.

Finally Rule (NORM-DUPL) removes an unsolved deduction or equality formula $\psi$ from F when it is subsumed by another formula $\psi'$. This is formalised by the following notion of equivalence:

**DEFINITION 4.17 (head equivalence of formulas).** Let $\psi = H \Leftarrow \varphi$ and $\psi' = H' \Leftarrow \varphi'$ be two formulas. We say that $\psi$ and $\psi'$ are *head equivalent*, written $\psi \approx_r \psi'$, if for some $\xi, \zeta, u, u'$ either $H = H' = (\xi =_f \zeta)$, or $H = (\xi \vdash^u u)$ and $H' = (\xi \vdash^u u')$.
That is, two formulas are head equivalent if their heads have the same second-order terms (but may differ on their first-order terms), which means they model the same attacker action. In particular if $\psi \approx_r \psi'$ and $\psi'$ is solved (namely has no hypotheses any more) then the formula $\psi$ is already implied by $\psi'$ which is why Rule (NORM-DUPL) can remove it from F.

### 4.3.3 Vector-simplification rules

We now define simplification rules that focus on vector, thus called *vector-simplification rules*. They are described in Figure 9 and focus among other things on adding formulas and entries in the knowledge base. This has to be done concurrently on an entire vector component to ensure that the same attacker actions can be performed in all of its elements, that is, that they have statically-equivalent solutions. The rules assume that the constraint systems have been normalised by the normalisation rules (see Figure 8), and one of them uses our custom notation for applying a substitution $\Sigma$ to a formula (Section 4.2.1, Definition 4.9). Finally, for the sake of succinctness, if $S = (\mathcal{P}, C, C^e)$ is an extended symbolic process we refer as $\Phi(S)$, $E^1(S)$, $E^2(S)$, ... to the corresponding components of $C^e$.

Rule (VECT-RM-UNSAT) removes $\perp$ elements from the vector. Rule (VECT-SPLIT) splits a component whenever a common solution would yield statically inequivalent frames. More specifically, the rule separates the constraint systems in $\Gamma^+$ in which a given recipe always yields a message (resp. an equality always holds) from the constraint systems in $\Gamma^-$ in which the same recipe would never yield a message (resp. the same equality would never hold). This is characterised by the fact that a deduction (resp. equality) formula is solved in some constraint systems and not in the others. Rule (VECT-ADD-CONSEQ) adds a solved deduction formula from $F(S)$ to $K(S)$ when this formula is solved in the entire component $\Gamma$ and the new knowledge-base entries are not redundant with existing ones. Finally, when an equality fact $\xi =_f \zeta$ should hold in one constraint system, Rule (VECT-ADD-FORMULA) adds it to the entire component $\Gamma$ (with appropriate hypotheses). Observe that we use in this rule the placeholder formula $\psi = \forall X, Y, z. X =_f Y \Leftarrow (X \vdash z \wedge Y \vdash z)$, introduced in Section 4.1.1, stating that two recipes deducing the same term should verify an equality fact.

### 4.4 Constraint Solving: case distinction rules

Our case distinction rules take the form of a transition system on vectors $S$ of extended symbolic processes similarly to the vector-simplification rules. There are three different rules, each operating in a similar manner: given a vector $S \cup \{\Gamma\}$, all rules perform a transformation of the following form on one component $\Gamma$:

$$ S \cup \{\Gamma\} \rightarrow S \cup \{\Gamma^+, \Gamma^-\} \qquad (\star\star) $$
$$ \mathbb{S} \cup \{\Gamma \cup \{(\mathcal{P}, C, \perp)\}\} \rightsquigarrow \mathbb{S} \cup \{\Gamma\} \qquad (\text{VECT-RM-UNSAT}) $$

$$ \mathbb{S} \cup \{\Gamma\} \rightsquigarrow \mathbb{S} \cup \{\Gamma^+, \Gamma^-\} \qquad (\text{VECT-SPLIT}) $$

if $\Gamma^+, \Gamma^-$ is a partition of $\Gamma$ and there exists a formula $\psi$ such that

1. $\forall S \in \Gamma^+, \exists \psi' \in F(S), \psi \cong_r \psi'$ and $\psi'$ solved; and

2. $\forall S \in \Gamma^-, \forall \psi' \in F(S), \psi \neq_r \psi'$

$$ \mathbb{S} \cup \{\Gamma\} \rightsquigarrow \mathbb{S} \cup \{\{S[K \mapsto K \wedge \xi \vdash^? u_S] \mid S \in \Gamma\}\} \qquad (\text{VECT-ADD-CONSEQ}) $$

if for all $S \in \Gamma$, $S$ is solved, $\xi \vdash^? u_S \in F(S)$ and for all second-order term $\zeta$, $(\zeta, u_S) \notin \text{Conseq}(K(S) \cup D(S))$

$$ \mathbb{S} \cup \{\Gamma\} \rightsquigarrow \mathbb{S} \cup \{\{S[F \mapsto F \wedge \psi:(\Sigma, S)] \mid S \in \Gamma\}\} \qquad (\text{VECT-ADD-FORMULA}) $$

if $\psi = \forall X, Y, z. X =_f^? Y \Leftarrow (X \vdash^? z \wedge Y \vdash^? z)$ and $\Sigma = \{X \mapsto \xi, Y \mapsto \zeta\}$, and for all $S \in \Gamma$,

1. $S$ is solved

2. $F(S)$ contains a formula of the form $\xi \vdash^? u_S$. Besides, there should exist $S \in \Gamma$, such that $(\zeta, u_S) \in \text{Conseq}(K(S) \cup D(S))$.

3. for all $(\zeta_1 =_f^? \zeta_2 \Leftarrow \varphi) \in F(S), \zeta_1 \neq \xi$ and $\zeta_2 \neq \xi$

<caption>**Figure 9.** Vector-simplification rules for sets of sets of extended symbolic processes</caption>

where $\Gamma^+$ (the *positive branch*) is intuitively obtained by applying a mgs $\Sigma$ on each symbolic processes of $\Gamma$ and $\Gamma^-$ (the *negative branch*) by adding the formula $\neg\Sigma$ to each symbolic process $S \in \Gamma$, where

$$ \neg\Sigma = \forall S. \bigvee_{X \in \text{dom}(\Sigma)} X \neq^? X\Sigma \qquad \text{with } S = \text{vars}^2(\text{img}(\Sigma)) \setminus \text{vars}^2(\Gamma) $$

Intuitively this refines the component $\Gamma$ by considering the cases where $\Sigma$ is a solution or not. After that, normalising the refined components $\Gamma^+$ and $\Gamma^-$ with the simplification rules—in particular Rules (VECT-RM-UNSAT) and (VECT-SPLIT)—will discard impossibles cases and separate processes with newly-found non-statically-equivalent solutions. The three case distinction rules (SAT), (EQ) and (REW) are presented in the next sections by specifying how $\Gamma^+$ and $\Gamma^-$ are computed from $\Gamma$. They are applied using a particular strategy defined by the following ordering on rules (where $<$ means “has priority over”):

SAT < EQ < REW
Note that this ordering is mostly arbitrary: only the minimality of SAT will be needed in Section 5.2 for complexity. The other inequalities are only there to reduce the number of cases to be considered in proofs.

### 4.4.1 Rule Sat

The first rule focuses on satisfiability: its goal is to separate extended constraint systems of $\Gamma$ that do not have the same solutions. For example if we have $S = (\mathcal{P}, C, C^e) \in \Gamma$ and $\Sigma \in \text{mgs}(C^e)$, all other symbolic processes $S' \in \Gamma$ should also have a solution that is an instance of $\Sigma$ (and if not, the component $\Gamma$ should be split to separate $S$ and $S'$). In particular this ensures that when this rule cannot be applied any more, all extended constraint system in $\Gamma$ share a common, unique mgs (in particular they are in solved form). The same mechanism can be used to consider the solutions $\Sigma$ making trivial some disequations of $E^1$ or hypotheses of some formulas in $F$. In particular the normalisation rules defined earlier in Section 4.3.2 will then handle the now trivial or unsatisfiable constraints. All this can be formalised as an instance of (★★) with:

For all $\Sigma, \Gamma$,

$$ 
\begin{aligned}
\Gamma^+ &= \{S:\Sigma | S \in \Gamma\} \\
\Gamma^- &= \{S[E^2 \mapsto E^2 \wedge \neg\Sigma] | S \in \Gamma\}
\end{aligned} 
\qquad (\text{SAT})
$$

where there exists $S \in \Gamma$ such that either

1. $S$ not solved and $\Sigma \in \text{mgs}(S)$; or otherwise

2. there exists $\psi \in F(S)$ not solved and $\Sigma \in \text{mgs}(S[E^1 \mapsto E^1 \wedge \text{hyp}(\psi)])$; or

3. $E^1(S)$ contains a disequality $\psi = \forall \tilde{x}.\phi$ and $\Sigma \in \text{mgs}(S[E^1 \wedge \psi \mapsto E^1] \text{mgu}(\neg\phi))$.

### 4.4.2 Rule Eq

The second case distinction rule focuses on the static equivalence between solutions of extended constraint systems. More specifically, the rule (EQ) checks whether an entry $\xi_1 \vdash^? u_1$ of one knowledge base of $\Gamma$ can deduce the same term as another recipe $\xi_2$ consequence of $K$. The rule is formalised as an instance of (★★) with

For all $\Sigma, \Sigma_0, \Gamma$,

$$ 
\begin{aligned}
\Gamma^+ &= \{S:\Sigma[F \mapsto F \wedge \psi:(\Sigma_0\Sigma, S:\Sigma)] | S \in \Gamma\} \\
\Gamma^- &= \{S[E^2 \mapsto E^2 \wedge \neg\Sigma] | S \in \Gamma\}
\end{aligned} 
\qquad (\text{EQ})
$$

if there exist $S \in \Gamma$, such that $\Sigma \in \text{mgs}(S[E^1 \mapsto E^1 \wedge H_E, D \mapsto D \wedge H_D])$, where $H_E$ and $H_D$ are, respectively, the sets of equations and deduction facts of the hypotheses of $\psi:(\Sigma_0, S)$, and:

1. either $\Sigma_0 = \{X \to \xi_1, Y \to \xi_2\}$ for some $(\xi_1 \vdash^? u_1), (\xi_2 \vdash^? u_2) \in K(S)$ and for all $(H \Leftarrow \varphi) \in F(S), H \neq (\xi_1 =_f^? \xi_2)$; or
2. $\Sigma_0 = \{X \to \xi_1, Y \to f(X_1, \dots, X_n)\}$ for some $(\xi_1 \vdash^? u_1) \in K(S)$ and $f/n \in \mathcal{F}_c$ with $X_1:k, \dots, X_n:k$ fresh and for all $(\zeta_1 =^?_f \zeta_2 \Leftarrow \varphi) \in F(S)$, $\zeta_b = \xi_1$ implies $\mathrm{root}(\zeta_{1-b}) \neq f$. \\
where $k = |\mathrm{dom}(\Phi(S))|$ and $\psi = \forall X, Y, z. X =^?_f Y \Leftarrow (X \vdash^? z \wedge Y \vdash^? z)$ with $X:k, Y:k, z$ fresh variables.

Similarly to Rule (VECT-ADD-FORMULA) the rule uses the generic equality formula $\psi$ and the hypotheses of $\psi:(\Sigma_0, S)$ express that $X\Sigma_0$ and $Y\Sigma_0$ deduce the same term. Since a recipe consequence of K can either be coming from a deduction fact in K or be a recipe with a constructor symbol at its root, we consider the two cases 1 and 2 each with the appropriate instantiation $\Sigma_0$ of the placeholders $X$ and $Y$. The side requirements that head-equivalent formulas should not already be present in $F(S)$ are simply here for termination purpose, thus avoiding infinite aggregation of redundant formulas.

### 4.4.3 Rule Rew

The third case distinction rule focuses on saturating the knowledge base. For example when outputting a term $u$, the corresponding symbolic rule (E-OUT) will add a deduction fact $ax_n \vdash^? u$ to $F$; the rule (REW) will apply rewrite rules on $u$ to determine whether new messages can be learned by the attacker. Typically if $u = \langle u_1, u_2 \rangle$ the following actions will happen:

1. after $ax_n \vdash^? u$ has been added to $F$ by the symbolic rule (E-OUT), it will be copied to the knowledge base $K$ by the simplification rules (VECT-ADD-CONSEQ) (assuming $u$ is not already deducible from any knowledge base of the component)

2. after that, the case-distinction rule (REW) will add the two deduction facts $fst(ax_n) \vdash^? u_1$ and $snd(ax_n) \vdash^? u_2$ to $F$, which may in turn be transferred to $K$ as well.

More precisely, given a deduction fact $\xi_0 \vdash^? u_0$, the rule checks whether one may apply a rewrite rule $\ell \to r$ to $u_0$, which may require to first apply a context on $u_0$ (for example if $u_0 = h(a)$ and $\ell = f(g(h(x)))$). For that we introduce a notion of skeleton of $\ell$.

**DEFINITION 4.18 (rewriting skeleton).** Let $p$ be a position of a first-order term $\ell$. A skeleton for $(\ell, p)$ is a tuple $(\xi, t, D)$ such that $\xi \in \mathcal{T}(\mathcal{F} \cup \mathcal{F}_0 \cup \mathcal{X}^2)$, $t \in \mathcal{T}(\mathcal{F} \cup \mathcal{F}_0 \cup \mathcal{X}^1)$, $D$ is a set of deduction facts and

$$ (\mathrm{root}(\xi_{|q}), \mathrm{root}(t_{|q})) = \begin{cases} (\mathrm{root}(\ell_{|q}), \mathrm{root}(\ell_{|q})) & \text{for any strict prefix } q \text{ of } p \\ (X_q, x_q) & \text{for any other position } q \text{ of } \xi \end{cases} $$

where the set of variables $X_q$ (resp. $x_q$), $q$ a position of $\xi$ that is not strict prefix of $p$, are fresh pairwise distinct second-order (resp. first-order) variables, and $D$ is the set of all the deduction facts $X_q \vdash^? x_q$. The set of all such skeletons (which, notably, are all identical up to variable renaming but may therefore differ on the second-order-variable types) is written $\mathrm{Skel}(\ell, p)$.

For a skeleton $(\xi, t, D) \in \mathrm{Skel}(\ell, p)$, the recipe $\xi$ represents the context that the attacker will apply on top of the deduction fact $\xi_0 \vdash^? u_0$ at the position $p$ to obtain the left-hand side $\ell$.
The term $t$ represents the corresponding generic term on which the rewrite rule will be applied. Finally $D$ is the set of deduction facts linking the variables of $\xi$ and $t$.

Consider now a component $\Gamma$, a symbolic process $S \in \Gamma$, a deduction fact $(\xi_0 \vdash^? u_0) \in K(S)$, and a context $C$. The first role of Rule (REW) is to saturate the knowledge base, that is, to deduce the new term $C[u_0] \downarrow$ using $C[\xi_0]$. However after adding the new deduction fact $C[\xi_0] \vdash^? C[u_0] \downarrow$ to $F(S)$, a head-equivalent formula should be added to all other symbolic processes of $\Gamma$ whenever it is possible, so that the vector-simplification rule (VECT-SPLIT) (which separates processes with non-statically-equivalent solutions) only separates $S' \in \Gamma$ from $S$ if $C[\xi_0]$ yields a valid message in $S$ but not in $S'$. Yet the behaviour of a destructor symbol may be described by multiple rewrite rules: the rewrite rule used to normalise $C[u_0]$ may therefore not be the same as the one used to normalise the term deduced by $C[\xi_0]$ in $S'$. Because of this we have to add to $F(S')$ all formulas corresponding to using all possible rewrite rules. For that we consider the following set of generic formulas:

$$ \text{RewF}(\xi, \ell \to r, p) = \left\{ \forall S. \begin{array}{l} \xi \vdash^? r' \Leftarrow (D \wedge \text{mgu}(\ell' =? t)) \\ \phantom{\xi \vdash^? r' \Leftarrow (} \ell' \to r' \in \mathcal{R} \\ (\xi, t, D) \in \text{Skel}(\ell, p) \\ S = \text{vars}(D, \ell') \end{array} \right\} $$

Let us now give a complete example to illustrate all these notions. The goal is to detail what formulas will be added to $F$ by Rule (REW) on a concrete case as the actual definition of the rule is quite technical and hard to read—although the intuition behind it is rather simple.

**EXAMPLE 4.19.** Consider a rewriting system defined by a binary symbol $h$ and the two rewrite rules

$$ \text{getOther}(h(x, y), x) \to y \qquad \text{getOther}(h(x, y), y) \to x $$

These two rewrite rules give access to either argument of $h$ assuming the other one is known. Now consider a component $\Gamma$ containing two extended symbolic processes $S_1$ and $S_2$ with the respective frames, given $k, k', s, s' \in \mathcal{N}$:

$$ \Phi(S_1) = \{ax_1 \mapsto h(k, k'), ax_2 \mapsto k\} \qquad \Phi(S_2) = \{ax_1 \mapsto h(s, s'), ax_2 \mapsto s'\} $$

They are are statically equivalent, even if the recipe `getOther(ax1, ax2)` is not normalised using the same rewrite rule in $\Phi(S_1)$ and $\Phi(S_2)$. We assume that $K(S_1) = ax_1 \vdash^? h(k, k') \wedge ax_2 \vdash^? k$ and $K(S_2) = ax_1 \vdash^? h(s, s') \wedge ax_2 \vdash^? s'$. We describe the application of Rule (REW) that uses the rewrite rule $(\ell \to r) = (\text{getOther}(h(x, y), x) \to y)$ to deduce a new term in $S_1$ by putting $ax_1$ at the position of $h(x, y)$ in $\ell$, i.e., position 1. To begin the rule considers a skeleton $(\xi, t, D) \in \text{Skel}(\ell, 1)$:

$$ \xi = \text{getOther}(X_1, X_2) \qquad t = \text{getOther}(x_1, x_2) \qquad D = X_1 \vdash^? x_1 \wedge X_2 \vdash^? x_2 $$
The set RewF($\xi$, $\ell \to r$, 1) therefore contains the following two formulas (normalised by the simplification rules on formulae):

$$ \psi_1 = \forall X_1, X_2, x, y. \text{getOther}(X_1, X_2) \vdash^? y \Leftarrow (X_1 \vdash^? h(x, y) \land X_2 \vdash^? x) $$

$$ \psi_2 = \forall X_1, X_2, x, y. \text{getOther}(X_1, X_2) \vdash^? x \Leftarrow (X_1 \vdash^? h(x, y) \land X_2 \vdash^? y) $$

They are only generic formulas indicating that when the left side of a rewrite rule can be computed then the right side can be computed as well. Since our goal is to apply the rewrite rule $\ell \to r$ where the deduction fact $ax_1 \vdash^? h(k, k')$ is used to deduce the subterm $\ell|_1$, we have to replace the variable at position 1 in $\xi$, namely $X_1$, by $ax_1$ in these formulas. We do this by applying the substitution $\Sigma_0 = \{X_1 \mapsto ax_1\}$ to $\psi_1, \psi_2$ (in the sense defined in Section 4.2.1, again normalised by simplification rules):

$$ \psi_1:(\Sigma_0, S_1) = \forall X_2. \text{getOther}(ax_1, X_2) \vdash^? k' \Leftarrow X_2 \vdash^? k $$

$$ \psi_2:(\Sigma_0, S_1) = \forall X_2. \text{getOther}(ax_1, X_2) \vdash^? k \Leftarrow X_2 \vdash^? k' $$

Rule (REW) will then compute most general solutions to instantiate $X_2$ in a way that satisfies the hypotheses of these formulas. In the case of the first formula we have the unique solution $mgs(S_1[D \mapsto D \land X_2 \vdash^? k]) = \{\Sigma\}$ where $\Sigma = \{X_2 \mapsto ax_2\}$; the algorithm will therefore add the following deduction fact to $F(S_1)$:

$$ \psi_1:(\Sigma_0\Sigma, S_1:\Sigma) = \text{getOther}(ax_1, ax_2) \vdash^? k' $$

On the contrary, the algorithm could not have added the second formula: we have $mgs(S_1[D \mapsto D \land X_2 \vdash^? k']) = \emptyset$, meaning that no solutions satisfy its hypotheses. Then we are almost done: as explained earlier it only remains to add a head-equivalent formula to $F(S_2)$, if any, so that the vector-simplification rule (VECT-SPLIT) does not split $\Gamma$ if the recipe `getOther(ax_1, ax_2)` yields a valid message in both $S_1$ and $S_2$. That is, we should add to $F(S_2)$:

$$ \psi_1:(\Sigma_0\Sigma, S_2:\Sigma) = (\text{getOther}(ax_1, ax_2) \vdash^? s' \Leftarrow s' =? s) $$

$$ \psi_2:(\Sigma_0\Sigma, S_2:\Sigma) = (\text{getOther}(ax_1, ax_2) \vdash^? s \Leftarrow s' =? s') $$

This time the situation is reversed compared to $S_1$: the first formula has unsatisfiable hypotheses (and will therefore be discarded at the next round of normalisation rules by Rule (NORM-FORMULA)) and the second one will be simplified to `getOther(ax_1, ax_2) \vdash^? s`. This illustrates why we add one formula for each rewrite rule: should we have only considered $\psi_1$, we would have missed the head-equivalent formula `getOther(ax_1, ax_2) \vdash^? s` in $S_2$, resulting in the incorrect conclusion that $\Phi(S_1) \not\prec \Phi(S_2)$. ♦

Let us now formalise Rule (REW) in full generality. It can now be defined as an instance of (★) under the following conditions:
For all $\Sigma, \Gamma$,

$$ 
\begin{align*}
\Gamma^+ &= \{S:\Sigma[F \mapsto F \land \mathfrak{F}(S)] \mid S \in \Gamma\} \\
\Gamma^- &= \{S[E^2 \mapsto E^2 \land \neg\Sigma] \mid S \in \Gamma\}
\end{align*}
\qquad (REW) $$

if there exist $S \in \Gamma$, $\ell \to r \in \mathcal{R}$, $p$ position of $\ell$, $\xi \in \mathcal{T}(\mathfrak{F} \cup \mathcal{X}_{=k}^2)$ with $k = |\mathrm{dom}(\Phi(S))|$, $\psi_0 \in \mathrm{RewF}(\xi, \ell \to r, p)$, $(\xi_0 \vdash^2 u_0) \in \mathcal{K}(S)$, and a function $\mathfrak{F}$ from subsets of $\Gamma$ to constraints such that the following conditions are met:

1. $p \neq \varepsilon$ and $\ell_{|p} \notin \mathcal{X}^1$

2. $\Sigma_0 = \{\xi_{|p} \to \xi_0\}$ and $\Sigma \in \mathrm{mgs}(S[D \mapsto D \land D(\psi_1), E^1 \mapsto E^1 \land \mathrm{hyp}(\psi_1)])$ if $\psi_1 = \psi_0:(\Sigma_0, S)$

3. $\Sigma_1$ is an injection from $\mathrm{img}(\Sigma) \setminus \mathrm{vars}^2(\psi_1)$ to fresh constants, and for any such injection $\Sigma'_1$, we have $\psi_0:(\Sigma_0\Sigma\Sigma'_1, S:\Sigma) \notin \mathrm{F}(S)$

4. for all $S' \in \Gamma$, $\mathfrak{F}(S') = \{\psi:(\Sigma_0\Sigma\Sigma'_1, S':\Sigma) \mid \psi \in \mathrm{RewF}(\xi, \ell \to r, p)\}$

The conditions are rather technical but simply capture the steps of the example. Commenting the requirements of the rule, Item 1 ensures that the rewriting is not performed at a trivial position. Items 2 and 3 describe the formulas added to each symbolic process of $\Gamma$: just as in the example they are obtained by choosing one $S \in \Gamma$, computing a formula $\psi_0$ ($\psi_1$ in the example) corresponding to applying one given rewrite rule $\ell \to r$ in $S$, replacing the position $p$ of $\ell$ by an entry of $\mathcal{K}(S)$ by applying $\Sigma_0$ and computing a solution $\Sigma$ of the hypotheses of the resulting formula. Finally, in Item 4, all other symbolic processes $S' \in \Gamma$ receive the formulas of $\mathfrak{F}(S')$, each attempting to apply a rewrite rule to yield a valid message with the same recipe as in $\psi_0$.

Note that the computation of the mgs $\Sigma$ may leave some second-order variables $X_1, \dots, X_n$ unconstrained because they do not need to be instantiated in a particular way to obtain a solution. This is where Item 3 come into play, replacing these pending variables by fresh constants.

## 4.5 All in all: computing a partition tree

**Overall procedure** We make reference to the various constraint-solving relations defined in the previous sections using the following notations:

$\mathop{\mathrm{simpl}}\limits \rightsquigarrow$ : simplification rules on formulas
$\mathop{\mathrm{norm}}\limits \rightsquigarrow$ : normalisation rules

$\mathop{\mathrm{vect}}\limits \rightsquigarrow$ : vector-simplification rules

$\mathop{\mathrm{SAT}}\limits \longrightarrow$ : (SAT) case-distinction rule
$\mathop{\mathrm{EQ}}\limits \longrightarrow$ : (EQ) case-distinction rule

$\mathop{\mathrm{REW}}\limits \longrightarrow$ : (REW) case-distinction rule

All these transition relations are interpreted as binary relations on vectors. We recall that we call a *component* a set $\Gamma$ of extended symbolic processes and a *vector* a set $\mathcal{S}$ of components, and
that all $(\mathcal{P}, C, C^e) \in \Gamma$ induce a predicate $\pi$ on second-order solutions of C such that

$$ Sol^{\pi}(C) = \{(\Sigma|_{vars^2(C)}, \sigma|_{vars^1(C)}) | (\Sigma, \sigma) \in Sol(C^e)\} $$

We therefore propose in Algorithm 1 a procedure to compute the partition tree of two bounded plain processes, where the nodes are labelled by components instead of regular partition-tree configurations; in particular the proof of correctness of this algorithm has to justify that the above predicate $\pi$ can be defined uniformly across the entire nodes of the computed tree.

**Correctness arguments** To conclude we mention that the core arguments justifying that Algorithm 1 effectively generates a partition tree can be found in Appendix B.5. Technically, most of the theorem statements rely on a collection of invariants, with a proof of their preservation at each step of the procedure (called with “Inv” names such as $Inv_{wf}$, $Inv_{sound},...$).

# 5. Termination and complexity

## 5.1 Preliminaries

1. In Section 5.2 we prove that Algorithm 1 uses a finite number of constraint-solving rules to compute each branch of the partition tree. This proves the all considered security relations (trace equivalence and inclusion, simulation, (bi)similarity) to be decidable.

2. For complexity purposes we then refine this result in Section 5.3: we prove that Algorithm 1 applies at most an exponential number of rules and that the nodes of the resulting partition tree have most general solutions of exponential (DAG) size.

3. Relying on these bounds, we show that two processes are not equivalent iff there exists a non-equivalence witness of exponential size (as defined in Section 3.6). This shows the security relations to be decidable in coNEXP time.

4. Finally we show in Section 5.5 that the security relations are coNEXP hard. We also provide a complexity analysis in the pure pi-calculus. All in all:

**THEOREM 5.1 (complexity of equivalences).** For bounded processes, the problems TRACEEQ, TRACEINCL, SIMULATION, SIMILARITY, and BISIMILARITY are coNEXP complete for constructor-destructor subterm convergent theories. Besides, in the pure pi calculus, TRACEEQ and TRACEINCL are $\Pi_2$ complete, and SIMULATION, SIMILARITY and BISIMILARITY are PSPACE complete.

**Notations** We also introduce some notations that will be used in most incoming sections. We recall that we study complexity w.r.t. the DAG size of terms (which provides stronger results compared to complexity bounds w.r.t. the tree size of terms); in particular the DAG size of a substitution $\sigma$ is $|\sigma|_{dag} = |st(img(\sigma))|$, hence the many occurrences of subterm sets below.
// Application of simplification rules, as much as possible

**Procedure applySimpl($\mathcal{S}$: Vector): Vector =**
**if $\mathcal{S} \stackrel{\text{simpl}}{\rightleftharpoons} \mathcal{S}'$ then** return applySimpl($\mathcal{S}'$)
**else if $\mathcal{S} \stackrel{\text{norm}}{\rightleftharpoons} \mathcal{S}'$ then** return applySimpl($\mathcal{S}'$)
**else if $\mathcal{S} \stackrel{\text{vect}}{\rightleftharpoons} \mathcal{S}'$ then** return applySimpl($\mathcal{S}'$)
**else** return $\mathcal{S}$

// Application of case-distinction rules, with simplification rules in between

**Procedure applyCase($\mathcal{S}$: Vector): Vector =**
**if $\mathcal{S} \stackrel{\text{Sat}}{\rightleftharpoons} \mathcal{S}'$ then** return applyCase(applySimpl($\mathcal{S}'$))
**else if $\mathcal{S} \stackrel{\text{Eq}}{\rightleftharpoons} \mathcal{S}'$ then** return applyCase(applySimpl($\mathcal{S}'$))
**else if $\mathcal{S} \stackrel{\text{Rew}}{\rightleftharpoons} \mathcal{S}'$ then** return applyCase(applySimpl($\mathcal{S}'$))
**else** return $\mathcal{S}$

// Generates the subtree rooted on a node labelled by the component $\Gamma$

**Procedure generateSubtree($\Gamma$: Component): Tree =**
$\Gamma_{in} \leftarrow \{S' | S \stackrel{\Gamma(X)}{\rightleftharpoons} S', S \in \Gamma\}$
$\Gamma_{out} \leftarrow \{S' | S \stackrel{\Gamma(ax)}{\rightleftharpoons} S', S \in \Gamma\}$
**if $\Gamma_{in} = \Gamma_{out} = \emptyset$ then**
return a tree reduced to its root, labelled $\Gamma$
**else**
$\mathcal{S} \leftarrow$ applyCase(applySimpl($\{\Gamma_{in}, \Gamma_{out}\}$))
$T \leftarrow$ tree with root $\Gamma$ and children generateSubtree($\Gamma'$) for
each $\Gamma' \in \mathcal{S}$
return $T$

// Generates the root and then an entire partition tree of $P_1$ and $P_2$

**Procedure PTree($P_1, P_2$: Processes): Tree =**
$\Gamma_1 \leftarrow \{S | P_1 \stackrel{\varepsilon}{\rightleftharpoons} S\}$
$\Gamma_2 \leftarrow \{S | P_2 \stackrel{\varepsilon}{\rightleftharpoons} S\}$
$\{\Gamma\} \leftarrow$ applySimpl($\{\Gamma_1 \cup \Gamma_2\}$) // in the root, simplification rules never split the vector
return generateSubtree($\Gamma$)

**Algorithm 1.** Computation of the partition tree, with nodes labelled with components
Given an extended constraint system $C^e = (\Phi, D, E^1, E^2, K, F)$ we write

$$ \mu^1 = \text{mgu}(E^1) \qquad (\text{first-order mgu}) $$

$$ \mu^2 = \text{mgu}(E^2) \qquad (\text{second-order mgu}) $$

$$ T^1 = \text{st}^1(\text{img}(\Phi\mu^1), \text{img}(\mu^1), K\mu^1, D\mu^1) \qquad (\text{first-order terms}) $$

$$ T^2 = \text{st}^2(\text{img}(\mu^2), K, D) \qquad (\text{second-order terms}) $$

$$ R = \text{st}_c(\text{img}(\mu^2), K \cup D) \cup \text{vars}^2(D) \qquad (\text{solution recipes}) $$

When the extended constraint system is not clear from context we write explicitly $\mu^1(C^e)$, $\mu^2(C^e)$, $T^1(C^e)$,... Intuitively $\mu^i$ are the mgu's of the equations of $E[i]$ and we recall in particular that $mgs(C^e) = \{\mu^2\}$ when $C^e$ is solved (Section 4.2.4, Proposition 4.13). The other notations assume $\mu^1 \neq \perp$ (if $\mu^1 = \perp$, $C^e$ will be discarded by the normalisation rule (MGS-UNSAT) anyway). The sets $T^1$ and $T^2$ respectively represent the first-order and second-order terms appearing in the system, while $R \subseteq T^2$ models the set of recipes used to build the solution of $C^e$ (i.e., $\mu^2$) from $K \cup D$. We recall that it is the same set as the one used when defining the constraint-solving rules for most general solutions (Section 4.2.2).

**REMARK 5.2 (uniformity of second-order terms across components).** Due to an invariant of the procedure (Inv$_{str}$ formalised in Appendix B, Section B.1), we know that all extended constraint systems in a component $\Gamma$ have the same second-order structure. Here this means that $\mu^2(C_1^e) = \mu^2(C_2^e)$ and $T^2(C_1^e) = T^2(C_2^e)$ for any $(\mathcal{P}_1, C_1, C_1^e)$, $(\mathcal{P}_2, C_2, C_2^e) \in \Gamma$. For this reason we may write $\mu^2(\Gamma)$ or $T^2(\Gamma)$ instead of $\mu^2(C^e)$ or $T^2(C^e)$ for some arbitrary $(\mathcal{P}, C, C^e) \in \Gamma$.

## 5.2 Termination of the constraint solving

### 5.2.1 Termination of the computation of most general solutions

We first study the termination of the procedure for computing most general solutions provided in Section 4.2. The proof mostly relies on the following measure that characterises the set of first-order terms of an extended constraint system $C^e$ that are not used in $mgs(C^e)$, that is, that are not deduced by any recipe $\xi \in R(C^e)$:

$$ \text{unused}^1(C^e) = \{t \in T^1 \mid t \notin \mathcal{X}^1 \wedge \forall \xi \in R(C^e) \setminus \mathcal{X}^2, (\xi, t) \notin \text{Conseq}(K\mu^1 \cup D\mu^1)\} $$

The simplification rules for mgs do not affect this value (except if $C^e$ is replaced by $\perp$ by (MGS-UNSAT)). The application of (MGS-CONSEQ) will ensure that $\text{unused}^1$ is at least non-increasing, while (MGS-RES) and (MGS-CONS) make it strictly decreasing. We summarise this as the following proposition, proved in Appendix C; we recall that, similarly to the correctness arguments in Section 4, the statements makes reference to some procedure invariants formalised in Appendix B.1:
**PROPOSITION 5.3** (decrease of unused first-order terms during constraint solving). Let $C^e$ be an extended constraint system such that $C^e \not\approx = C^e$ and the invariants $\text{Inv}_{wf}(C^e)$ and $\text{Inv}_{sound}(C^e)$ hold. Then let $C^e \xrightarrow{\Sigma} \not\approx C^{e'} \neq \perp$. If this transition is derived with:

1. Rule (MGS-CONSEQ): $|\text{unused}^1(C^{e'})| \leq |\text{unused}^1(C^e)|$

2. Rules (MGS-RES) or (MGS-CONS): $|\text{unused}^1(C^{e'})| < |\text{unused}^1(C^e)|$

Using this proposition we can then easily prove the computation of the set of most general solutions to be terminating, and actually to give an upper bound on its cardinality:

**THEOREM 5.4** (termination for most general solutions). There exist no infinite sequences of transitions w.r.t. $\rightarrow \not\approx$. Besides if $C^e$ is an extended constraint system such that the invariants $\text{Inv}_{wf}(C^e)$ and $\text{Inv}_{sound}(C^e)$ hold, we have

$$|mgs(C^e)| \leq (|K(C^e)| + 1)^{|\text{unused}^1(C^e)|}$$

**PROOF.** First of all we observe that consecutive applications of Rule (MGS-CONSEQ) are terminating, since applying this rule strictly decrease the cardinality of the set $m(C^e)$ of parameters $(\xi, \zeta)$ the rule can be applied with. Combining this with Proposition 5.3 we obtain that if $C^e \xrightarrow{\Sigma} \not\approx C^{e'} \neq \perp$ then $C^e < C^{e'}$ w.r.t. the lexicographic composition of $\text{unused}^1$ and $m$.

Besides consecutive applications of Rule (MGS-CONSEQ) are also confluent by unicity of mgu's. For the same reason the applications of Rules (MGS-RES) or (MGS-CONS) can be performed on one deterministically-chosen deduction fact $(X \vdash^2 u) \in D$. We therefore obtain $mgs(C^e) = \{\Sigma_{|vars^2(C^e)|} | C^e \xrightarrow{\Sigma} \not\approx C^{e'}$ normalised, $C^{e'}$ solved\}$ where a reduction $C^e \xrightarrow{\Sigma} \not\approx C^{e'}$ is said to be normalised when all applications of Rule (MGS-CONSEQ) and the choice of deduction facts in Rules (MGS-RES) or (MGS-CONS) are done in a fixed, deterministic way. Since for any $C^e$, there are at most $|K(C^e)|$ normalised applications of Rule (MGS-RES) and 1 normalised application of Rule (MGS-CONS), we deduce by Proposition 5.3 that $|mgs(C^e)| \leq (|K(C^e)| + 1)^{|\text{unused}^1(C^e)|}$. ■

### 5.2.2 Termination of the computation of partition trees

To bound the number of rule applications in Algorithm 1 we define a well-founded measure that decreases after each case-distinction, simplification, normalisation and vector-simplification rules. More precisely the rule applications are always of the form

$$S \cup \{\Gamma\} \rightarrow S \cup \{\Gamma_1, \dots, \Gamma_p\} \qquad p \in \{1, 2\}$$

and we show that for all $i \in [1, p]$, $\Gamma > \Gamma_i$ w.r.t. to a well-founded measure on components (under the invariants of the procedure defined in Appendix B). This therefore bounds the number of rule applications to compute a given branch of the partition tree. The measure in question is a tuple of 9 integer components that is ordered w.r.t. the lexicographic ordering.