**Measure 1: sizes of the processes** As first element of the measure, we compute a maximum on the sizes of the processes in the multisets $\mathcal{P}$, that is,

$$M_1(\Gamma) = \max_{(\mathcal{P}, C, C^e) \in \Gamma} \sum_{R \in \mathcal{P}} |R|_{\text{dag}} \qquad (\text{Meas. 1})$$

Notice that this stays unchanged for any simplification or case distinction rules but strictly decreases when applying the extended symbolic transitions.

**Measure 2: Number of constraint systems** The third element of the measure considers the number of extended symbolic processes in the set, i.e., $|\Gamma|$, that may increase only when applying a symbolic transition; however it strictly decreases when applying the simplification rules (VECT-SPLIT) and (VECT-RM-UNSAT). Moreover it also strictly decreases for the positive branch of Rule (SAT) when applied with the case 3 of its application conditions. In such a case, we consider a disequation $\psi$ and a mgs $\Sigma$ of $C_j^e$ that does not satisfy $\psi$, which will lead to at least one $S \in \Gamma$ being discarded by the simplification rule (VECT-RM-UNSAT).

$$M_2(\Gamma) = |\Gamma| \qquad (\text{Meas. 2})$$

**Measure 3: Number of terms not consequence** Given $C^e$ an extended symbolic constraint system, let us consider the following set representing the set of terms that are not consequence of $K(C^e)$ and $D(C^e)$:

$$\text{set}_K(C^e) = \{t \in T^1 | \forall \xi, (\xi, t) \notin \text{Conseq}(K(C^e) \cup D(C^e))\}$$

Typically it corresponds to the terms that are not deducible by the attacker but could potentially be (because the knowledge base is not saturated yet). In fact, when the simplification Rule (VECT-ADD-CONSEQ) is applied, i.e., when a deduction fact $\xi \vdash u$ is added to $K(C^e)$, the term $u$ is necessarily a subterm of the frame by the invariant $\text{Inv}_{wf}(C^e)$. Moreover by definition of Rule (VECT-ADD-CONSEQ) we know that $u$ is not already consequence, meaning that the size of $\text{set}_K(C^e)$ will strictly decrease. Finally the case distinction rules never increase the number of elements of $\text{set}_K(C^e)$: indeed they all consist of applying substitutions $\Sigma$ that are most general solutions of some systems having $K(C^e)$ as their knowledge base, hence their first-order terms are consequence by K-basis. All in all we choose the following component:

$$M_3(\Gamma) = \min_{(\mathcal{P}, C, C^e) \in \Gamma} |\text{set}_K(C^e)| \qquad (\text{Meas. 3})$$

**Measure 4: Number of unsolved extended constraint systems** We recall that the aim of Rule (SAT), case 1 of its application conditions, is to put extended constraint systems in solved form (that is, in a form where they trivially have $\mu^2$ as a unique mgs). If

$$M_4(\Gamma) = |\{(\mathcal{P}, C, C^e) \in \Gamma | C^e \text{ unsolved}\}| \qquad (\text{Meas. 4})$$
then this measure is strictly decreasing when applying the rule in question. Once a system has a unique mgs, instantiating its second variables does not change this fact and the other case distinction rules are therefore non-increasing w.r.t. this measure.

**Measure 5: Applicability of Rule REW** The next element represents the number of applications of Rule (REW) that are still possible. Typically, we consider all the parameters of the rule (REW) (the deduction facts from K, the rewrite rule, etc...) on which the rule would be applied with a most general solutions that does not already corresponds to a deduction fact in F. If C<sup>e</sup> is an extended constraint system we therefore consider set<sub>REW</sub>(C<sup>e</sup>) the set of tuples (ψ, ℓ → r, p, ψ<sub>0</sub>, Σ) that satisfy all the application conditions of Rule (REW), and

$$M_5(\Gamma) = \sum_{(\mathcal{P}, C, C^e) \in \Gamma} |\text{set}_{\text{REW}}(C^e)| \qquad (\text{Meas. 5})$$

By definition |set<sub>REW</sub>(C<sup>e</sup>)| strictly decreases for at least one (P, C, C<sup>e</sup>) ∈ Γ (and non-increasing for the others) when applying Rule (REW). Then let (P, C, C<sup>e</sup>) ∈ Γ: the other case distinction rules (SAT) and (EQ) do not increase |set<sub>REW</sub>(C<sup>e</sup>)|. Indeed if we consider one of their applications C<sup>e</sup> Σ'→ C<sup>e</sup>:Σ', we have

$$\text{set}_{\text{REW}}(C^e: \Sigma') = \{(\psi \Sigma', \ell \to r, p, \psi_0, \Sigma \Sigma') | (\psi, \ell \to r, p, \psi_0, \Sigma) \in \text{set}_{\text{REW}}(C^e)\}.$$

Note however that |set<sub>REW</sub>(C<sup>e</sup>)| may increase by application of Rule (VECT-ADD-CONSEQ) since |K(C<sup>e</sup>)| will increase; yet the measure is already decreasing by the component M<sub>3</sub>.

**Measure 6: Number of unsolved deduction formulas** We recall that Rule (SAT), case 2 of its application conditions, applies a most general solution to remove the hypotheses of one formula ψ ∈ F(C<sup>e</sup>) for some (P, C, C<sup>e</sup>) ∈ Γ (the formula becomes solved in the positive branch, and is removed by (NORM-FORMULA) in the negative branch). This rule application is therefore strictly decreasing w.r.t. the measure

$$M_6(\Gamma) = |\{\psi \in F(C^e) | (\mathcal{P}, C, C^e) \in \Gamma, \psi \text{ unsolved deduction formula}\}| \qquad (\text{Meas. 6})$$

We only consider deduction formulas ψ for this component. In particular the only rule that may increase this measure (i.e., generate unsolved deduction formulas) is (REW) which is already decreasing w.r.t. the previous component of the measure.

**Measure 7: Applicability of Rule EQ** Similarly to the analogue component for Rule (REW), we now define the next component that bounds the maximal number of possible applications of Rule (EQ). The application conditions stipulate that it can be applied either

1. on two deduction facts of K(C<sub>i</sub><sup>e</sup>), or

2. on one deduction fact of K(C<sub>i</sub><sup>e</sup>) in combination with a construction function symbol.
Even if the application conditions also consider a mgs $\Sigma$, the number of applications of Rule (EQ) will not depend on their number; this is intuitively because after applying the rule with one arbitrary mgs $\Sigma$, the conditions forbid any later applications with identical parameters except $\Sigma$. Formally consider for example the case 1 (case (2) follows the same reasoning). The rule is applied on two deduction facts $(\xi_1 \vdash^? u_1)$, $(\xi_2 \vdash^? u_2) \in K(C^e)$. Thus, an equality formula with $\xi_1 \Sigma =^? \xi_2 \Sigma$ as head will be added in $F(C^e:\Sigma)$. However, in further applications of the rule, the condition that “for all $(H \leftarrow \varphi) \in F(C^e:\Sigma), H \neq (\xi_1 =^? \xi_2)$” will prevent a new application with the same (up to instantiation of $\Sigma$) deductions facts from $K(C^e:\Sigma)$.

We therefore conclude that the rule (EQ) can be applied only once per pair of deduction facts in $K$ and once per deduction fact in $K$ and function symbol in $\mathcal{F}_c$. If $C^e$ is an extended constraint system we therefore consider $\text{set}_{\text{EQ}}(C^e)$ the set of pairs $(\psi, \psi') \in K(C^e)^2$ or $(\psi, f) \in K \times \mathcal{F}_c$ that satisfy all the application conditions of the rule (EQ), and

$$M_7(\Gamma) = \sum_{(\mathcal{P}, C, C^e) \in \Gamma} |\text{set}_{\text{EQ}}(C^e)| \qquad (\text{Meas. 7})$$

**Measure 8: Number of unsolved equality formulas** We now introduce the analogue of Component 7 for equality formulas, that is,

$$M_8(\Gamma) = |\{\psi \in F(C^e) \mid (\mathcal{P}, C, C^e) \in \Gamma, \psi \text{ unsolved equality formula}\}| \qquad (\text{Meas. 8})$$

As before Rule (SAT) makes this measure decrease in the case 2 of its application conditions. On the contrary unsolved equality formulas can be generated by two rules: the case distinction rule (EQ) or the vector-simplification rule (VECT-ADD-FORMULA).

**Measure 9: Remaining most general solutions** So far, every time we showed that one of the previous element of the measure (strictly) decrease by application of a case distinction rule, we always focused on the positive branches of case-distinction rules. The negative branches on the contrary only add recipe disequations to the system, which does not increase any the previous components of the measure but strictly decreases the number of most general solutions we can compute for the same instance of the rule. For example, if $\Sigma \in \text{mgs}(C^e)$ then $|\text{mgs}(C^e)| > |\text{mgs}(C^e[E^2 \wedge \neg \Sigma])|$. Hence it suffices to consider the last component:

$$M_9(\Gamma) = \left| \left\{ \Sigma \mid \begin{array}{l} \text{there exists a case distinction rule applicable} \\ \text{from } C^e \text{ with parameter } \Sigma, (\mathcal{P}, C, C^e) \in \Gamma \end{array} \right\} \right| \qquad (\text{Meas. 9})$$

**Conclusion** This gives the termination of the algorithm for computing $T \in \text{PTree}(P, Q)$. We study more precisely the Components 1 to 9 of the measure in Appendix C and prove that they can all be bound by an exponential in $|P, Q, \mathcal{R}|_{\text{dag}}$ (with $\mathcal{R}$ the rewriting system, implicitly including the signature). Hence:
**THEOREM 5.5 (termination for partition trees).** For all P, Q plain processes, Algorithm 1 terminates with arguments P, Q. Moreover each branch of the resulting tree is generated by applying at most an exponential number (in $|P, Q, R|_{\text{dag}}$) of rules, not counting the negative branches of case distinction rules.

## 5.3 Bounding the size of most general solutions

### 5.3.1 Overall approach

**Objective** We now focus on the theoretical complexity of the decision problems TRACEEQ, BISIMILARITY, SIMULATION, ... Our goal for now is to prove that they are all decidable in coNEXP and the core argument to achieve this is to prove the theorem:

**THEOREM 5.6 (size of most general solutions).** If T is a partition tree of P, Q (w.r.t. a rewriting system $R$) generated by Algorithm 1, then for all nodes $n$ of T, $|mgs(n)|_{\text{dag}}$ is exponential in $|P, Q, R|_{\text{dag}}$.

We will detail in Section 5.4 how to derive a coNEXP decision procedure for equivalence properties by using this result. To bound the size of most general solutions we rely on the results previously established in Section 5.2.1: in the final partition tree $mgs(n) = \mu^2(\Gamma(n))$ and it therefore suffices to prove that for all nodes, $|\mu^2(\Gamma(n))|_{\text{dag}}$ is exponential in $|P, Q, R|_{\text{dag}}$. However we will instead study the easier-to-track bound:

$$|T^2(\Gamma(n))| \ge |\text{st}(\text{img}(\mu^2(\Gamma(n))))| = |\mu^2(\Gamma(n))|_{\text{dag}}$$

**Evolution of second-order terms** Let us now consider each constraint-solving rule and determine how $T^2$ evolves along the components along a branch of the partition tree.

1. **Symbolic rules:** only Rules (E-IN) and (E-OUT) increase the size of $T^2$ by adding at most two new second order variables.

2. **Simplification, normalisation, vector-simplification rules:** only Rule (VECT-ADD-CONSEQ) may increase the size of $T^2(\Gamma)$. Indeed, it transfers a deduction fact from F in K for each extended constraint systems in the current component $\Gamma$.

3. **Case distinction rules:** the positive branches of these rules increase the size of $T^2$ whereas the negative branches leave it unchanged.

It therefore suffices to prove the following result to obtain Theorem 5.6:

**PROPOSITION 5.7 (evolution of second-order terms in partition trees).** If $S \cup \{\Gamma\} \to S \cup S'$ where $S' = \{\Gamma'\}$ is obtained by Rule (VECT-ADD-CONSEQ) or $\Gamma' \in S'$ is the positive branch of a case distinction rule, then $|T^2(\Gamma')|_{\text{dag}} - |T^2(\Gamma)|_{\text{dag}}$ is bounded by a polynomial in $|P, Q, R|_{\text{dag}}$.

Indeed we recall that by Theorem 5.5, we already know that each branch of the partition tree is obtained after applying at most an exponential number of rules (negative branches of
case distinction rules excluded). Hence we obtain the expected exponential bound on $T^2$ when combined with the above proposition. The remaining of Section 5.3 is dedicated to its proof.

### 5.3.2 Bounding the increase of the second-order terms

When applying a mgs We first study the growth of $T^2(C^e)$ when applying a mgs to $C^e$, which means proving Theorem 5.6 in the case of Rule (SAT). Similarly to our previous results on most general solutions (Section 5.2.1), our bounds depend on $unused^1(C^e)$ the number of first-order terms of $C^e$ that are not already used in the solution, i.e., in $\mu^2$. We also recall that by Proposition 5.3, this measure is non-increasing when applying any of the mgs simplification and constraint-solving rules, and is even strictly decreasing in the case of Rule (MGS-RES) and (MGS-CONS). Let us now show that its growth is actually inverted compared to $T^2$, that is, how much $T^2$ increases can be bounded by how much $unused^1$ decreases:

**PROPOSITION 5.8 (evolution of second-order terms when applying mgs).** For all extended processes $C^e$ that verify the invariants $Inv_{wf}(C^e)$ and $Inv_{sound}(C^e)$, we have

$$ \forall \Sigma \in \text{mgs}(C^e), |T^2(C^e:\Sigma)| \le |T^2(C^e)| + |\mathcal{F}| \times (|\text{unused}^1(C^e)| - |\text{unused}^1(C^e:\Sigma)|) $$

**PROOF.** We assume $|\mathcal{F}| > 0$ by convention. It suffices to prove this property when replacing $C^e:\Sigma$ by $C^{e'}$ for $C^e \to C^{e'} \neq \perp$ obtained by a mgs simplification or constraint-solving rules. We perform a case analysis on the rule in question.

* case 1: simplification rule on formulas

The simplification rules on formulas only affect first-order terms and second-order equations and we therefore have $T^2(C^{e'}) = T^2(C^e)$.

* case 2: mgs simplification rule

We only need to consider Rule (MGS-UNIF). Since it only affects first-order terms, the reasoning is identical to the previous case.

* case 3: mgs constraint-solving rule

Rules (MGS-CONSEQ) and (MGS-RES) apply a second-order substitution $\Sigma = \text{mgu}(\xi =? \zeta)$ to $C^e$ for some $\xi, \zeta \in T^2(C^e)$. In particular we deduce that $|T^2(C^{e'})| \le |T^2(C^e)|$ and the conclusion thus follows from the fact that $\text{unused}^1(C^e) - \text{unused}^1(C^{e'}) \ge 0$ by Proposition 5.3. Finally the only rule that increases $T^2(C^e)$ is the last one, (MGS-CONS), that generates $n$ fresh second-order variables for some constructor symbol $f/n$. In particular $|T^2(C^{e'})| \le |T^2(C^e)| + n$, hence the result since $\text{unused}^1(C^e) - \text{unused}^1(C^{e'}) > 0$ by Proposition 5.3. ■

In particular we obtain Proposition 5.7 for Rule (SAT) case 1, provided we manage to prove that $\text{unused}^1(C^e)$ is bounded by a polynomial. We explain in Appendix C how to extend the argument to Rules (EQ), (REW) and (VECT-ADD-CONSEQ).
**Bound of unused terms** To conclude let us establish the polynomial bound on $|unused^1(C^e)|$. In order to do so we explore the relation between $C$ and $C^e$ in $(\mathcal{P}, C, C^e) \in \Gamma$. Intuitively $unused^1(C^e)$ always has less elements then $unused^1(C)$ because

1. the symbolic rules always add the same constraints to $C$ and $C^e$, ensuring that $unused^1(C^e)$ increases at most as much as $unused^1(C)$ by these rules

2. the other rules leave $C$ untouched and do not make $unused^1(C^e)$ increase.

**PROPOSITION 5.9 (approximation of unused terms).** For all $(\mathcal{P}, C, C^e) \in \Gamma$,

$$|unused^1(C^e)| \le |\Phi(C)\mu^1(C), \mu^1(C)|_{\text{dag}}$$

**PROOF.** Considering $C$ instead of $C^e$, we have the trivial approximation

$$|unused^1(C)| \le |T^1(C)| = \text{st}(\Phi(C)\mu^1(C), \mu^1(C)) = |\Phi(C)\mu^1(C), \mu^1(C)|_{\text{dag}}$$

It therefore suffices to prove that $|unused^1(C^e)| \le |unused^1(C)|$. For that we show that the inequality $|unused^1(C^e)| \le |unused^1(C)|$ is preserved when applying any of the constraint-solving rules.

► case 1: symbolic rules

These rules add the same constraints to $C^e$ and $C$ (up to an additional deduction fact added to $F(C^e)$ in the case of Rule (E-OUT), but this does not affect $unused^1(C^e)$). In particular since $E^2(C) = K(C) = \emptyset$, if we consider an instance $(\mathcal{P}, C, C^e) \xrightarrow{\alpha} S(\mathcal{P}', C', C^{e'})$ of a symbolic rule we therefore have

$$|unused^1(C^{e'})| - |unused^1(C^e)| \le |unused^1(C')| - |unused^1(C)|$$

which gives the expected result.

► case 2: simplification, normalisation, vector-simplification rules

By definition these rules only affect $C^e$ and leave $C$ untouched, hence the conclusion since these rules do not increase $unused^1(C^e)$.

► case 3: case distinction rules

Let us consider $\text{CompatSubs}(C^e)$ the set of substitutions $\Sigma$ such that the notation $C^e:\Sigma$ is well defined, that is, such that

1. if $\text{dom}(\Sigma) \subseteq \text{vars}^2(\text{D}(C^e))$

2. for all $X \in \text{dom}(\Sigma)$, there exists $t$ such that $(X\Sigma, t) \in \text{Conseq}(K(C^e) \cup D')$ where $D' = \{Y \vdash^? u \in D(C^e) | Y \notin \text{dom}(\Sigma)\} \cup D_{\text{fresh}}$ with

$$D_{\text{fresh}} = \{Y \vdash^? y | Y \in \text{vars}^2(\text{img}(\Sigma_{|\text{vars}^2(C^e)})) \setminus \text{vars}^2(C^e), y \text{ fresh}\}$$
This is intuitively the set of substitutions $\Sigma$ whose image is constructed from $\mathcal{K}(C^e)$, up to the new variables of $D_{fresh}$ introduced by $\Sigma$. In particular we have for all $\Sigma \in \text{CompatSubs}(C^e)$, $|\text{unused}^1(C^e:\Sigma)| \le |\text{unused}^1(C^e)|$ (which follows in more details from Proposition B.11 in Appendix B), hence the conclusion. ■

This relation allows to eventually reduce the problem to give a polynomial bound on $\Phi(C)$ and $\mu^1(C)$ which are only affected by symbolic rules (we recall that the other constraint-solving rules do not modify $C$). All in all this concludes the proof of the expected polynomial bound:

**COROLLARY 5.10 (polynomial evolution of second-order terms).** For all extended processes $C^e$ that verify the invariants $\text{Inv}_{wf}(C^e)$ and $\text{Inv}_{sound}(C^e)$, we have

$$ \forall \Sigma \in \text{mgs}(C^e), |T^2(C^e:\Sigma)| \le |T^2(C^e)| + 9 |P, Q, \mathcal{R}|_{\text{dag}}^3 $$

**PROOF.** We agree on the convention that $|P|_{\text{dag}}$, $|Q|_{\text{dag}}$ and $|\mathcal{R}|_{\text{dag}}$ are strictly positive. By Propositions 5.8 and 5.9, it suffices to prove that for all symbolic traces $P \xrightarrow{\text{tr}}_s (\mathcal{P}, C)$, we have that $|\Phi(C)\mu^1(C), \mu^1(C)|_{\text{dag}} \le 9 |P, \mathcal{R}|_{\text{dag}}^2$ (which, as we will see, is a very rough approximation). For that a quick induction on the length of tr allows to construct a set of $|\text{tr}|$ variables $Y = \{y_i\}_{i=1}^{|\text{tr}|}$ and finite set of equations S such that

1. $\mu^1(C) \in \text{mgu}_\mathcal{R}(S)$

2. for all $(u =? v) \in S$, $u$ (resp. $v$) is either a subterm of a term appearing in $P$ or a variable of $Y$

3. for all terms $u \in \text{img}(\Phi(C)\mu^1(C))$, there exists $u_0$ subterm of a term appearing in $P$ such that $u_0\mu^1(C) = u$

The variables of $Y$ model the fresh channel variables introduced when executing (S-IN) or (S-OUT) transitions, and the set of equations $S$ collects the equality tests performed during the trace and how each variable of $P$ is instantiated by $E^1$ (including by private communications). Independently from this, by induction on a straightforward algorithm to compute mgu modulo theory, we have if $\mathcal{R}$ is constructor-destructor subterm convergent

$$ \begin{aligned} |\text{st}(\sigma)| &\le |\text{st}(S)| + |\mathcal{R}|_{\text{dag}} \times |\{t \in \text{st}(S) \mid \text{root}(t) \in \mathcal{F}_d\}| \\ &\le 2|\text{st}(S)| \times |\mathcal{R}|_{\text{dag}} \end{aligned} \quad (\mathcal{E}) $$

Altogether we therefore obtain

$$ \begin{aligned} |\Phi(C)\mu^1(C), \mu^1(C)|_{\text{dag}} &\le |\text{st}(P)| + 2|\mu^1(C)|_{\text{dag}} && (\text{by 3}) \\ &\le |P|_{\text{dag}} + 4|\text{st}(S)| \times |\mathcal{R}|_{\text{dag}} && (\text{by 1 and } (\mathcal{E})) \\ &\le |P|_{\text{dag}} + 4(|P|_{\text{dag}} + |\text{tr}|) |\mathcal{R}|_{\text{dag}} && (\text{by 2}) \\ &\le 9|P, \mathcal{R}|_{\text{dag}}^2 && \blacksquare \end{aligned} $$
## 5.4 Complexity upper bounds for equivalence properties

### 5.4.1 Complexity of trace equivalence

The goal of this section is to prove the following theorem:

**THEOREM 5.11 (complexity of trace equivalence).** *TRACEEQ are coNEXP for bounded processes and constructor-destructor subterm convergent theories.*

The proof relies on the following arguments that were developed in previous sections:

1. *characterizing trace inclusion with partition trees:* Theorem 3.20

2. *existence of a mgs of exponential size:* Theorem 5.6

3. *soundness and completeness of the symbolic semantics:* see Proposition 3.15

Using these ingredients we prove the core property:

**PROPOSITION 5.12 (witness of non-trace equivalence of exponential size).** Let $P_1, P_2$ be two plain processes w.r.t. a constructor-destructor subterm convergent rewriting system $\mathcal{R}$. The following points are equivalent:

1. $P_1 \not\subseteq_t P_2$

2. there exists a trace $t : P_1 \xrightarrow{\text{tr}} A_1$ such that $|t|_{\text{dag}}$ is exponential in $|P, Q, \mathcal{R}|_{\text{dag}}$ and for all $P_2 \xrightarrow{\text{tr}} A_2, A_1 \neq A_2$.

**PROOF.** The proof of $2\Rightarrow 1$ is trivial and we therefore focus on $1\Rightarrow 2$. Let us assume that $P_1 \not\subseteq_t P_2$, and let $T \in \text{PTree}(P_1, P_2)$ the partition tree computed by Algorithm 1. By Theorem 3.20 we obtain a partition-tree trace $P_1 \xrightarrow{\text{tr}}_T (\mathcal{P}, C)$, $n$ such that there exist no traces of the form $P_2 \xrightarrow{\text{tr}}_T (\mathcal{P}', C')$, $n$. But by Theorem 5.6 we know that the (DAG) size of mgs($n$) is of exponential in $|P, Q, \mathcal{R}|_{\text{dag}}$, which gives a solution $(\Sigma, \sigma) \in \text{Sol}^{\pi(n)}(C)$ of exponential size as well by definition of a mgs.

Let us then consider the trace $t : P_1 \xrightarrow{\text{tr}\Sigma} (\mathcal{P}\sigma, \Phi(C)\sigma\downarrow)$ (that exists by soundness of the symbolic semantics) and show that it satisfies the conditions of 2. It is indeed of exponential DAG size. Besides assume by contradiction that there exists a trace $P_2 \xrightarrow{\text{tr}\Sigma} (Q, \Psi)$ such that $\Phi(C)\sigma \sim \Psi$. By using the completeness of the symbolic semantics and the properties of the partition tree (Lemma A.1), we would obtain a symbolic process $(\mathcal{P}', C')$ such that $P_2 \xrightarrow{\text{tr}}_T (\mathcal{P}', C')$, $n$, yielding a contradiction. ■

To obtain a decidability result we also use the following result on static equivalence from [2]:

**PROPOSITION 5.13 (witness of non-static equivalence of polynomial size).** If two frames $\Phi$ and $\Psi$ are not statically equivalent w.r.t. a subterm convergent rewriting system $\mathcal{R}$, there exist two recipes $\xi$ and $\zeta$ such that $|\xi, \zeta|_{\text{dag}}$ is polynomial in $|\Phi, \Psi, \mathcal{R}|_{\text{dag}}$, $\xi\Phi\downarrow=\zeta\Phi\downarrow$ and $\xi\Psi\downarrow\neq\zeta\Psi\downarrow$.
Wrapping everything together we obtain the following NEXP decision procedure for non-trace equivalence:

1. Given two processes $P_1, P_2$, guess an integer $i \in [1, 2]$ and a trace $P_1 \xrightarrow{\text{tr}} (\mathcal{P}, \Phi)$ of exponential size. In particular, although $|dom(\Phi)| \le |\text{tr}|$, the sizes of the terms in $img(\Phi)$ may be exponential as well.

2. For each of the exponentially-many traces of the form $t: P_2 \xrightarrow{\text{tr}} (Q, \Psi)$, guess two recipes $\xi_t, \zeta_t$ of exponential size.

3. if for one such trace $t$ we do not have $\xi_t \Phi \downarrow = \zeta_t \Phi \downarrow \Leftrightarrow \xi_t \Psi \downarrow = \zeta_t \Psi \downarrow$, conclude that $P_1 \not\approx_t P_2$.

### 5.4.2 Complexity of labelled bisimilarity

The goal of this section is to prove the following theorem:

**THEOREM 5.14 (complexity of labelled bisimilarity).** *BISIMILARITY is coNEXP for bounded processes and constructor-destructor subterm convergent theories.*

Similarly to trace equivalence we build on the results of the previous sections, this time using the characterisation of labelled bisimilarity based on symbolic witnesses (Theorem 3.25). Given a partition tree with most general solutions of exponential size, our goal is therefore to derive from it a symbolic witness of non-equivalence and a solution of this witness (Definition 3.24), both of exponential size as well.

**PROPOSITION 5.15 (witness of non-labelled bisimilarity of exponential size).** Let $P_1, P_2$ be two plain processes w.r.t. a constructor-destructor subterm convergent rewriting system $\mathcal{R}$. The following points are equivalent:

1. $P_1 \not\approx_b P_2$

2. there exists a witness $w$ for $(P_1, P_2)$ such that $|w|_{\text{dag}}$ is exponential in $|P, Q, \mathcal{R}|_{\text{dag}}$.

**PROOF.** The proof of $2 \Rightarrow 1$ is trivial and we therefore focus on $1 \Rightarrow 2$. Let us assume that $P_1 \not\approx_b P_2$, and let $T \in \text{PTree}(P_1, P_2)$ the partition tree computed by Algorithm 1. By Theorem 3.25 we obtain a symbolic witness $w_s$ for $(P_0, P_1, \text{root}(T))$ such that $\text{Sol}(w_s) \ne \emptyset$, and it suffices to prove that there exists a solution of $w_s$ of exponential size (where the size of a solution $f_{\text{sol}}$ is $\sum_{N \in \text{dom}(f_{\text{sol}})} |f_{\text{sol}}(N)|_{\text{dag}}$). More precisely we construct by induction on $w_s$ a function $f$ mapping the nodes of $w_s$ to second-order substitutions (not necessarily ground) such that:

1. $(f_{\text{mgs}}f) \in \text{Sol}(w_s)$, where $f_{\text{mgs}}(S, n) = \text{mgs}(n)$ and the notation $f = gh$ is defined by $f(N) = g(N)h(N)$ for all nodes $N$ of $w_s$

2. for all $f_{\text{sol}} \in \text{Sol}(w_s)$, there exists $f'$ such that $f_{\text{sol}} = f_{\text{mgs}}f f'$

In particular since $f_{\text{mgs}}$ is of exponential size by Theorem 5.6, it suffices to ensure that $f$ is of exponential size as well.
► case 1: $w_s$ is reduced to a leaf N.

Then it suffices to choose $f(N) = id$.

► case 2: $w_s$ has a root labelled $(S, n)$ and children $N_1, \dots, N_p$ labelled $(S_1, n'), \dots, (S_p, n')$

Let us write $S = \{A_0, A_1\}$ with, by definition, a symbolic trace $A_0 \xrightarrow{\alpha} S$ $A'_0$ such that each trace $A_1 \xrightarrow{\bar{\alpha}} S$ $A'_1$ corresponds to a child $S_i = \{A'_0, A'_1\}$. We apply the induction hypothesis to the children to obtain their respective functions $f_1, \dots, f_p$. We recall that $Sol(w_s) \neq \emptyset$ by hypothesis and that all solutions $f_{sol}$ verify $f_{sol}(N_1) = \dots = f_{sol}(N_p)$; thus, since by induction hypothesis all solutions of $w_s$ are instances of $f_{mgs}f_i$, we obtain:

$$mgu(mgs(n')f_1(N_1)\varrho_1 \wedge \dots \wedge mgs(n')f_p(N_p)\varrho_p) \neq \perp$$

for $\varrho_1, \dots, \varrho_p$ fresh variables renamings of $img(f_1(N_1)), \dots, img(f_p(N_p))$, respectively. In particular, assuming without loss of generality that all the $f_i(N_i)$ have the same domain $(vars^2(n') \setminus dom(mgs(n'))) \cup img(mgs(n'))$, we can write

$$\Sigma = mgu(f_1(N_1)\varrho_1 \wedge \dots \wedge f_p(N_p)\varrho_p) \neq \perp$$

Note that this $mgu$ is only polynomially bigger than each $f_i(N_i)$. Since $mgs(n')$ is an instance of $mgs(n)$, we also let $\Sigma_0$ such that $mgs(n') = mgs(n)\Sigma_0$. We then conclude the proof by defining $f$ as follows:

1. $f(root(w_s)) = (\Sigma_0\Sigma)|_{vars^2(n)}$

2. for all $i \in [1, p]$, for all nodes $N$ in the subtree of $w_s$ rooted in $N_i$, $f(N) = f_i\Sigma$.

## 5.5 Complexity lower bounds

We prove in this section the complexity lower bounds stated in Theorem 5.1.

### 5.5.1 Extensions of the calculus

We first introduce useful syntax extensions that can be encoded in the original calculus. We point out that that using these encodings does not affect the complexity of deciding the related decision problems, since they rely on polynomial-size encodings.

**Internal non-deterministic choice** A first classical operator is the non-deterministic choice: $P+Q$ is a process that can be executed either as $P$ or as $Q$. Its operational semantics can therefore be described by adding the following rule to those of Figure 1:

$$((P+Q) \cup \mathcal{P}, \Phi) \stackrel{\star}{\rightleftharpoons} ((R) \cup \mathcal{P}, \Phi) \quad \text{if } R \in \{P, Q\} \quad (\text{CHOICE})$$
This reduction can easily be encoded as an internal communication on a fresh private channel. We formalise it by a process transformation $[·]$:

$$[P+Q] \triangleq \bar{s}\langle s \rangle | s(x).[P] | s(y).[Q] \quad \text{where } s \in \mathcal{N} \text{ and } x, y \in \mathcal{X}^1 \text{ are fresh} \quad (1)$$

and all other cases of the syntax are handled as homomorphic extensions of $[·]$. As for the parallel operator we will sometimes use the big operator $\Sigma$ assuming right-associativity. The correctness of this translation with respect to $\approx_t$ and $\approx_b$ will be stated later on in this section.

We also introduce the Choose(x) construct which non-deterministically assigns either 0 or 1 to x. Choose(x).P silently reduces to either $P\{x \mapsto 0\}$ or $P\{x \mapsto 1\}$ and Choose($\vec{x}$).P is defined as Choose($x_1$).Choose($x_2$) ... Choose($x_n$).P where $\vec{x} = x_1, \dots, x_n$. Formally, we extend the operational semantics with the rule

$$(\mathcal{P} \cup \{\text{Choose}(x).P\}, \Phi) \xrightarrow{\varepsilon} (\mathcal{P} \cup \{P\{x \mapsto 0\}\}, \Phi) \quad (\text{CHOOSE-0})$$

$$(\mathcal{P} \cup \{\text{Choose}(x).P\}, \Phi) \xrightarrow{\varepsilon} (\mathcal{P} \cup \{P\{x \mapsto 1\}\}, \Phi) \quad (\text{CHOOSE-1})$$

and define

$$[\text{Choose}(y).P] \triangleq (\bar{d}\langle 0 \rangle + \bar{d}\langle 1 \rangle) | d(y).[P] \quad \text{with } d \in \mathcal{N} \text{ is fresh}$$

**Boolean circuits and formulae** Complete problems in complexity theory often involve boolean formulae (e.g., SAT or QBF). The ability to evaluate boolean formulae, or boolean circuits in general, within the applied $\pi$-calculus is therefore crucial. We can implement such a feature by the means of private channels and internal communication: each edge of a boolean circuit $\Gamma$ indeed mimics a channel transmitting a boolean over a network (Figure 10).

<figure><img src="image_13.png" /><figcaption>**Figure 10.** Simulation of an OR-gate within the applied $\pi$-calculus</figcaption></figure>

The essence of circuits lies in so-called *logical gates* which are boolean functions with at most two inputs. We consider the fan-out of gates to be possibly more than one in order to model the fact that wires of a gate can be split and connected to the input of different gates. Formally, we assume without loss of generality that the gate has at most two (identical) outputs, to be given as input to other gates. Logical gates usually range over the constants 0 and 1 and the predicates $\wedge$, $\vee$ and $\neg$ with the usual truth tables but we may use other common operators such as $=$. From that a *boolean circuit* is an acyclic graph of logical gates: each input (resp.
output) of a gate is either isolated or connected to a unique output (resp. input) of another gate, which defines the edges of this graph.

Such a circuit $\Gamma$ with $m$ isolated inputs and $n$ isolated outputs thus models a boolean function $\Gamma: \mathbb{B}^m \to \mathbb{B}^n$ (where $\mathbb{B} = \{0, 1\}$). We write $(c_1, c_2, g, c_3, c_4) \in \Gamma$ to state that $g: \mathbb{B}^2 \to \mathbb{B}$ is a gate of $\Gamma$ whose inputs are passed through edges $c_1$ and $c_2$ and whose output is sent to edges $c_3$ and $c_4$. This notation is naturally lifted to other in-outdegrees.

**Embedding into the calculus** The syntax of plain processes is now extended with the construction $x_1, \dots, x_n \leftarrow \Gamma(b_1, \dots, b_m).P$ where $\Gamma: \mathbb{B}^m \to \mathbb{B}^n$ is a circuit, $x_1, \dots, x_n$ variables and $b_1, \dots, b_m$ terms. We fix two distinct terms $0, 1 \in \mathcal{F}_0$ to model $\mathbb{B}$ within the calculus, and the labelled operational semantics is extended with the rule:

$$ (\mathcal{P} \cup \{\vec{x} \leftarrow \Gamma(\vec{b}).P\}, \Phi) \xrightarrow{\epsilon} (\mathcal{P} \cup \{P\{\vec{x} \mapsto \Gamma(\vec{b} \downarrow)\}\}, \Phi) \quad \text{if } \mathrm{msg}(\vec{b}) \text{ and } \vec{b} \downarrow \subseteq \mathbb{B} \quad (\text{VALUATE}) $$

Now we have to extend the definition of $[\cdot]$ (previous subsection) to handle the new operator. For simplicity we only consider the case where gates have two inputs and two outputs: handling lower arities is straightforward. If $(c_1, c_2, g, c_3, c_4) \in \Gamma$, we first define:

$$ [[c_1, c_2, g, c_3, c_4]] \triangleq c_1(x).c_2(y). \prod_{b, b' \in \mathbb{B}} \text{ if } x = b \text{ then if } y = b' \text{ then } (\overline{c_3\langle g(b, b') \rangle} | \overline{c_4\langle g(b, b') \rangle}) $$

where $c_1, c_2, c_3, c_4 \in \mathcal{N}$ (assuming that different circuits in a process do not share edges). To sum it up, we simply see circuit edges as private channels and simulate the logical flow of the gate. It is then easily extended:

$$ [[\vec{x} \leftarrow \Gamma(\vec{b}).P]] \triangleq \left( \prod_{k=1}^{m} \overline{c_{i_k}} \langle b_k \rangle \right) \mid \left( \prod_{(c_1, c_2, g, c_3, c_4) \in \Gamma} [[c_1, c_2, g, c_3, c_4]] \right) \mid c_{o_1}(x_1) \dots c_{o_n}(x_n). [[P]] $$

where $(c_{i_k})_{k=1}^m$ (resp. $(c_{o_k})_{k=1}^n$) are the isolated input (resp. output) edges of $\Gamma$. Note that when $b$ and $b'$ are fixed booleans, $g(b, b')$ denotes the boolean obtained from the truth table of $g$: we emphasise that $g$ is not a function symbol of the signature $\mathcal{F}$.

**REMARK 5.16 (simplifying assumption).** We assume that every input of a circuit goes through at least one gate and every circuit has at least one output. This is to avoid irrelevant side cases in proofs.

**Correctness of the translation** Now we dispose of an extended syntax and semantics as well as a mapping $[\cdot]$ removing the new constructors from a process. The correctness of this translation is proven in Appendix C:

**PROPOSITION 5.17 (correctness of the encodings).** Let $\approx_t^+$ and $\approx_b^+$ be the notions of trace equivalence and labelled bisimilarity over the extended calculus (the flag $+$ being omitted outside of
this lemma). For all extended processes $A = (\mathcal{P}, \Phi)$, the translation $[A] = (\llbracket \mathcal{P} \rrbracket, \Phi) = (\{\llbracket P \rrbracket \mid P \in \mathcal{P}\}, \Phi)$ can be computed in polynomial time, $A \approx_t^+ [A]$ and $A \approx_b^+ [A]$.

**REMARK 5.18 (stability of common fragments).** As the finite and pure fragments of the applied $\pi$-calculus are closed under $\llbracket \cdot \rrbracket$, sums and circuits can be safely used within any intersection of such fragments. The encoding does not use else branches either.

### 5.5.2 Lower bounds in the pure fragment

We now use the above tool to state our reductions, first, in the pure pi calculus.

**Trace equivalence** To show that trace equivalence is $\Pi_2$-hard we proceed by a reduction from $QBF_2$, that is, the problem of deciding, given $\varphi$ a boolean formula whose variables are partitioned into $\{\vec{x}\} \cup \{\vec{y}\}$, whether $\forall \vec{x}. \exists \vec{y}. \varphi(\vec{x}, \vec{y}) = 1$. Our goal is to thus to construct two processes $A$ and $B$ such that:

$$A \approx_t B \qquad \text{iff} \qquad \forall \vec{x}. \exists \vec{y}. \varphi(\vec{x}, \vec{y}) = 0 \qquad (2)$$

<figure><img src="image_14.png" /><figcaption>**Figure 11.** Schematic definition of $A$ and $B$</figcaption></figure>

Consider three distinct names $c, 0, 1 \in \mathcal{F}_0$ (the last two modelling booleans for the syntax extension of circuit evaluation, see Section 5.5.1). Processes $A$ and $B$ are depicted in Figure 11. Intuitively, the process $P(t)$ (where $t$ is a term which may depend on the variables bound by $P$) gets a valuation of $\vec{x}$ from the attacker, internally chooses a valuation of $\vec{y}$, computes the value of $\varphi(\vec{x}, \vec{y})$ using rule VALUATE, and outputs $t$. From that it is quite easy to see that $A$ and $B$ have the same set of traces *iff* for all valuation of $\vec{x}$, there exists a valuation of $\vec{y}$ such that $\varphi(\vec{x}, \vec{y}) = 0$. This reduction is formalised and proved in Appendix D.3.

**THEOREM 5.19.** In the pure pi-calculus, TRACEEQ and TRACEINCL are $\Pi_2$-hard for bounded positive processes.

Note that the hardness for TRACEINCL is directly implied by the hardness of TRACEEQ. This is evidenced by the reduction that, for all processes $P, Q, P \sqsubseteq_t Q \text{ iff } P + Q \approx_t Q$.
**Simulations** We now prove that labelled bisimilarity is PSPACE-hard for the positive pure pi calculus by reduction from QBF. This is more involved as QBF allows arbitrary quantifier alternation. Let $\varphi$ be a boolean formula whose variables are partitioned into $\{x_1, \dots, x_n\} \cup \{y_1, \dots, y_n\}$ for some $n \in \mathbb{N}$. We construct (in polynomial time in the size of $\varphi$ and $n$) two processes A and B such that:

$$A \approx_b B \quad \text{iff} \quad A \approx_s B \quad \text{iff} \quad \forall x_1 \exists y_1 \dots \forall x_n \exists y_n. \varphi(x_1, \dots, x_n, y_1, \dots, y_n) = 0 \quad (3)$$

Both QBF and labelled bisimilarity may be seen as bisimulation games: an attacker plays the $\exists$-quantifiers (selects a transition in a process) whereas a defender responds with the $\forall$-quantifiers (tries to find a similarly-labelled sequence of transitions in the other process). The role of A and B is to implement this intuitive connection: the attacker moves will be simulated by public inputs $c(x_i)$ and the defender responses by instructions Choose($z_i$). $c(y_i)$. The structure of A and B is then designed to constrain the moves of the two players so that the winning condition of the attacker is exactly $\exists x_1 \forall y_1 \dots \exists x_n \forall y_n. \varphi(\vec{x}, \vec{y}) = 1$.

<figure><img src="image_15.png" /><figcaption>**Figure 12.** Schematic definition of $A_i$ and $B_i$</figcaption></figure>

A and B are defined inductively by processes $A_i$, $B_i$ and $D_i$, depicted in Figure 12, structured in a way that, in a bisimulation game:

1. the attacker chooses the instance of $x_i$;

2. the defender chooses the instance of $z_i$ and can force the attacker to instantiate $y_i$ with the same value (the attacker not doing so allows for a trivial victory of the defender).

The intermediary processes Goto($A_i$) and Goto($B_i$) intuitively formalise value passing from one index to another, in order to avoid an exponential blowup when encoding $n$ nested tests. Their precise definition and the correctness of the reduction is formalised in Appendix D.3. As before, the hardness of the pre-order follows from the hardness of its symmetric closure.

**THEOREM 5.20.** In the pure pi-calculus, SIMULATION, SIMILARITY and BISIMILARITY are PSPACE-hard for bounded positive processes.
### 5.5.3 Reduction of SuccinctSAT to process equivalence

We now show that, when cryptographic primitives are modelled by a destructor subterm convergent rewrite system, TRACEEQ, TRACEINCL, SIMULATION, SIMILARITY and BISIMILARITY are coNEXP hard by reducing SuccinctSAT to process equivalence. Consider an instance of SUCCINCTSAT, Γ, with $m+2$ inputs and $n+1$ outputs and we design $\mathcal{F}$, $\mathcal{R}$ subterm destructor and A and B positive processes such that, for any equivalence relation $\approx \in \{\approx_s, \approx_t, \approx_b\}$, $A \not\approx B \text{ iff } [[\Gamma]]_\phi$ is satisfiable.

**Term algebra** Terms are built over the following signature:

<table><tr><td>$\mathcal{F} \triangleq 0, 1,$</td><td>(booleans $\mathbb{B}$)</td></tr><tr><td>Node/2, $\pi/2,$</td><td>(binary trees)</td></tr><tr><td>h/2,</td><td>(one-way binary hash)</td></tr><tr><td>h<sub>N</sub>/2, h<sub>\B</sub>/2, Test<sub>N</sub>/1, Test<sub>\B</sub>/1</td><td>(testable binary hashes)</td></tr></table>

We equip this term algebra with the rewriting system $E$ containing the following rules modelling subtree extraction (for binary trees) and argument testing (for hashes):

$$ \begin{array}{lclcl} \pi(\text{Node}(x, y), 0) \rightarrow x & \qquad & \pi(\text{Node}(x, y), 1) \rightarrow y & & \\ \text{Test}_N(\text{h}_N(\text{Node}(x, y), z)) \rightarrow 1 & & \text{Test}_B(\text{h}_B(0, z)) \rightarrow 1 & & \text{Test}_B(\text{h}_B(1, z)) \rightarrow 1 \end{array} $$

In particular $\mathcal{R}$ is subterm and destructor, the destructor symbols being $\pi$, Test$_N$ and Test$_B$. We will also use a shortcut for recursive subtree extraction: if $\ell$ is a finite sequence of first-order terms, the notation $t_{|\ell}$ is inductively defined by:

$$ t_{|\epsilon} \triangleq t $$

**Core of the reduction** Let us give the intuition behind the construction before diving into the formalism. Recall that we are studying a formula in CNF $[[\Gamma]]_\phi$ with $2^n$ variables and $2^m$ clauses. In particular, given a valuation of its $2^n$ variables, we can verify in non-deterministic polynomial time in $n, m$ that it falsifies $[[\Gamma]]_\phi$:

1. guess an integer $i \in [0, 2^m - 1]$ as a sequence of $m$ bits;

2. obtain the three literals of the $i^{th}$ clause of $[[\Gamma]]_\phi$ (requiring three runs of the circuit $\Gamma$) and verify that the valuation falsifies the disjunction of the three literals.

This non-deterministic verification is the essence our reduction. In the actual processes:

1. a process CheckTree($x$) checks that $x$ is a correct encoding of a valuation, that is, that $x$ is a complete binary tree of height $n$ whose leaves are booleans;

2. a process CheckSat($x$) implements the points 1. and 2. above.

All of this is then formulated as equivalence properties within A and B (see the intermediate lemmas in the next paragraph for details). Intuitively, we want to express the following
statement by equivalence properties: “for all term x, either x is not an encoding of a valuation or falsifies a clause of $[\Gamma]_\phi$”. A schematised definition is proposed in Figure 13.

<figure><img src="image_16.png" /><figcaption>Figure 13. Informal definition of A and B</figcaption></figure>

**Formal construction** Let us now define the processes depicted in Figure 13 properly; note that all the proofs about the correctness of this construction are relegated to Appendix C but we still state several intermediary lemmas in order to highlight the proof structure. But first of all, let us give a name to a frame which is at the core of our reduction:

$$ \Phi_0 = \{ax_1 \mapsto h(0, s), ax_2 \mapsto h(1, s)\} $$

$\Phi_0$ is reached after executing the central branch of B and everything is about knowing under which conditions a frame statically equivalent to $\Phi_0$ can be reached in A. Let us define the processes themselves now. We fix $s \in \mathcal{N}$ and define, if $x$ is a protocol term:

$$ \text{CheckTree}(x) \triangleq \sum_{i=0}^{n-1} \left( \begin{array}{l} \text{Choose}(p_1, \dots, p_i). \bar{c}\langle\text{h}_N(x_{|p_1\cdots p_i}, s)\rangle. \bar{c}\langle\text{h}(1, s)\rangle \\ + \text{Choose}(p_1, \dots, p_n). \bar{c}\langle\text{h}_B(x_{|p_1\cdots p_n}, s)\rangle. \bar{c}\langle\text{h}(1, s)\rangle \end{array} \right) $$

**PROPOSITION 5.21 (correctness of the tree checker).** Let $x$ be a message which is not a complete binary tree of height $n$ with boolean leaves. Then there exists a reduction $\text{CheckTree}(x) \stackrel{\epsilon}{\Rightarrow} (\{P\}, \emptyset)$ such that $P \approx_b \bar{c}\langle\text{h}(0, s)\rangle. \bar{c}\langle\text{h}(1, s)\rangle$.

Now let us move on to $\text{CheckSat}(x)$. This process binds a lot of variables:

1. $\vec{p} = p_1, \dots, p_m$ models the non-deterministic choice of a clause number in $[0, 2^m - 1]$;

2. $b_i, \ell_i, i \in [1, 3]$, where $\ell_i$ is a sequence of $n$ variables, model the literals of the clause chosen above ($b_i$ is the negation bit and $\ell_i$ the identifier of the variable);
3. v stores whether the chosen clause is satisfied by the valuation modelled by x.

$$
\begin{align*}
\text{CheckSat}(x) &\triangleq \text{Choose}(\vec{p}). \\
b_1, \ell_1 &\leftarrow \Gamma(\vec{p}, 0, 1). \\
b_2, \ell_2 &\leftarrow \Gamma(\vec{p}, 1, 0). \\
b_3, \ell_3 &\leftarrow \Gamma(\vec{p}, 1, 1). \\
v &\leftarrow (b_1 = x_{|\ell_1} \lor b_2 = x_{|\ell_2} \lor b_3 = x_{|\ell_3}). \\
\bar{c}\langle h(v, s) \rangle &\cdot \bar{c}\langle h(1, s) \rangle
\end{align*}
$$

**PROPOSITION 5.22 (correctness of the sat checker).** Let $x$ be a complete binary tree of height $n$ whose leaves are booleans, and $\text{val}_x$ be the valuation mapping the variable number $i$ of $[[\Gamma]]_\phi$ to $x_{|p_1 \cdots p_n} \in \mathbb{B}$ where $p_1 \cdots p_n$ is the binary representation of $i$ (i.e., $i = \sum_{k=1}^n p_k 2^{k-1}$). If $\text{val}_x$ does not satisfy $[[\Gamma]]_\phi$ then there exists $\text{CheckSat}(x) \stackrel{\epsilon}{\Rightarrow} P$ such that $P \approx_b \bar{c}\langle h(0, s) \rangle \cdot \bar{c}\langle h(1, s) \rangle$.

We can finally wrap up everything by defining A and B and stating the last part of the
correctness theorem. We recall that all the proofs can be found in Appendix C.

$$
\begin{align*}
A &\triangleq c(x).(\text{CheckSat}(x) + \text{CheckTree}(x)) \\
B &\triangleq c(x).(\text{CheckSat}(x) + \text{CheckTree}(x) + \bar{c}\langle\text{h}(0, s)\rangle \cdot \bar{c}\langle\text{h}(1, s)\rangle)
\end{align*}
$$

**PROPOSITION 5.23 (correctness of the reduction).** For any equivalence relation $\approx \in \{\approx_s, \approx_t, \approx_b\}$, $[[\Gamma]]_\phi$ is satisfiable iff $A \not\approx B$.

As a conclusion we obtain the coNEXP hardness of equivalence properties (and their
respective pre-orders as a consequence) for constructor-destructor subterm convergent theories.
This is stated by the theorem below, which additionally puts an emphasis on the fact that the
rewriting system used in our reduction is constant, that is, it does not depend on Γ.

**THEOREM 5.24 (hardness of equivalences).** There exists a fixed constructor-destructor subterm convergent rewriting system $\mathcal{R}$ such that the decision problems $\mathcal{R}$-TRACEEQ, $\mathcal{R}$-TRACEINCL, $\mathcal{R}$-SIMULATION, $\mathcal{R}$-SIMILARITY and $\mathcal{R}$-BISIMILARITY are coNEXP hard for bounded positive processes.

**6. Conclusion and future work**

In this article we have studied automated verification of equivalence properties, encompassing
both theoretical and practical aspects. We provide tight complexity results for static equivalence,
trace equivalence and labelled (bi)similarity (as well as their respective pre-orders), summarised
in Table 1. In particular we show that deciding trace equivalence and labelled (bi)similarity for
a bounded number of sessions is coNEXP complete for subterm convergent destructor rewrite
systems. Finally, we implement the procedure for deciding trace equivalence in the DEEPSEC
prototype. As demonstrated through an extensive benchmark (Table 2), our tool is broad in
scope and efficient compared to other tools.
Our work opens several directions for future work. It would be interesting to lift the restriction of subterm convergent equational theories to allow for more cryptographic primitives. Similarly, we plan to avoid the restriction to destructor rewrite systems to more general ones. Also, in recent work [30] it was shown that labelled similarity is the same relation as may testing equivalence in presence of a probabilistic adversary which motivates the extension of our implementation beyond trace equivalence. The presented procedure for (bi)similarity is however highly non-deterministic and a naive implementation would certainly be inefficient.

Finally, we also plan to extend the DEEPSEC tool with support for other types of properties. The extension provided in this article to simulation and other security relations shows the modularity of our core proof technique, the partition tree, for analysing security properties. For example, a simplified version of the tree could be used to verify more classical (and simpler) trace properties, which would significantly rise the scope and usability of DEEPSEC. More generally, since navigation within the tree already allows to verify the complex notion of bisimilarity, we expect that the technique should scale to hyperproperties in general. There are few formalisms and results for such properties in the context of security protocols, but hyperlogics fitting our symbolic model have recently been introduced [11]. They allow for example to model fine variants of equivalence relations to capture subtle hypotheses, and their combination to liveness or real-time properties. We expect that our proof techniques would allow to study the decidability and complexity of a large fragment of such logics.

## References

[1] Martín Abadi, Bruno Blanchet, and Cédric Fournet. The applied pi calculus: mobile values, new names, and secure communication. J. ACM, 65(1):1:1–1:41, 2018. DOI (2, 7, 10, 12, 16)

[2] Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367(1-2):2–32, 2006. DOI (4, 9, 14, 19, 20, 75)

[3] Martín Abadi and Cédric Fournet. Private authentication. Theor. Comput. Sci. 322(3):427–476, 2004. DOI (4, 7, 10)

[4] Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148(1):1–70, 1999. DOI (2, 16)

[5] Ben Adida. Helios: web-based open-audit voting. Proceedings of the 17th USENIX Security Symposium, July 28-August 1, 2008, San Jose, CA, USA, pages 335–348. USENIX Association, 2008. URL (4, 41)

[6] Myrto Arapinis, Tom Chothia, Eike Ritter, and Mark Ryan. Analysing unlinkability and anonymity using the applied pi calculus. Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, pages 107–121. IEEE Computer Society, 2010. DOI (2)

[7] Myrto Arapinis, Véronique Cortier, and Steve Kremer. When are three voters enough for privacy properties? Computer Security - ESORICS 2016 - 21st European Symposium on Research in Computer Security, Heraklion, Greece, September 26-30, 2016, Proceedings, Part II, volume 9879 of Lecture Notes in Computer Science, pages 241–260. Springer, 2016. DOI (16)

[8] Myrto Arapinis, Loretta Ilaria Mancini, Eike Ritter, Mark Ryan, Nico Golde, Kevin Redon, and Ravishankar Borgaonkar. New privacy issues in mobile telephony: fix and verification. the ACM Conference on Computer and Communications Security, CCS’12, Raleigh, NC, USA, October 16-18, 2012, pages 205–216. ACM, 2012. DOI (6, 41)
[9] Alessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, and Laurent Vigneron. The AVISPA tool for the automated validation of internet security protocols and applications. Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, volume 3576 of Lecture Notes in Computer Science, pages 281-285. Springer, 2005. DOI (1)

[10] David Baelde, Stéphanie Delaune, and Lucca Hirschi. Partial order reduction for security protocols. 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 497-510. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. DOI (4, 5, 40)

[11] Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, and Itsaka Rakotonirina. Tidy: symbolic verification of timed cryptographic protocols. Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022, pages 263-276. ACM, 2022. DOI (85)

[12] David A. Basin, Jannik Dreier, Lucca Hirschi, Sasa Radomirovic, Ralf Sasse, and Vincent Stettler. A formal analysis of 5g authentication. Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, pages 1383-1396. ACM, 2018. DOI (2, 5, 6)

[13] David A. Basin, Jannik Dreier, and Ralf Sasse. Automated symbolic proofs of observational equivalence. Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, Denver, CO, USA, October 12-16, 2015, pages 1144-1155. ACM, 2015. DOI (6)

[14] Mathieu Baudet. Deciding security of protocols against off-line guessing attacks. Proceedings of the 12th ACM Conference on Computer and Communications Security, CCS 2005, Alexandria, VA, USA, November 7-11, 2005, pages 16-25. ACM, 2005. DOI (5)

[15] Mathieu Baudet. Sécurité des protocoles cryptographiques : aspects logiques et calculatoires. (Security of cryptographic protocols : logical and computational aspects). PhD thesis, École normale supérieure de Cachan, France, 2007. URL (19-21, 30)

[16] Mathieu Baudet, Véronique Cortier, and Stéphanie Delaune. YAPA: A generic tool for computing intruder knowledge. ACM Trans. Comput. Log. 14(1):4:1-4:32, 2013. DOI (14)

[17] Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. Verified models and reference implementations for the TLS 1.3 standard candidate. 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, pages 483-502. IEEE Computer Society, 2017. DOI (2)

[18] Bruno Blanchet. Automatic proof of strong secrecy for security protocols. 2004 IEEE Symposium on Security and Privacy (S&P 2004), 9-12 May 2004, Berkeley, CA, USA, page 86. IEEE Computer Society, 2004. DOI (17)

[19] Bruno Blanchet. Modeling and verifying security protocols with the applied pi calculus and proverif. Found. Trends Priv. Secur. 1(1-2):1-135, 2016. DOI (1)

[20] Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated verification of selected equivalences for security protocols. J. Log. Algebraic Methods Program. 75(1):3-51, 2008. DOI (6)

[21] Bruno Blanchet and Ben Smyth. Automated reasoning for equivalences in the applied pi calculus with barriers. IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016, pages 310-324. IEEE Computer Society, 2016. DOI (6)

[22] Bruno Blanchet, Ben Smyth, Vincent Cheval, and Marc Sylvestre. Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. 2020. URL (3, 39)

[23] Michele Boreale and Luca Trevisan. A complexity analysis of bisimilarity for value-passing processes. Theor. Comput. Sci. 238(1-2):313-345, 2000. DOI (3)

[24] Rohit Chadha, Vincent Cheval, Ştefan Ciobăcă, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4):23, 2016. DOI (3, 5, 40, 41)

[25] Vincent Cheval. APTE: an algorithm for proving trace equivalence. Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pages 587-592. Springer, 2014. DOI (5, 41)

[26] Vincent Cheval and Bruno Blanchet. Proving more observational equivalences with proverif. Principles of Security and Trust - Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7796 of Lecture Notes in Computer Science, pages 226-246. Springer, 2013. DOI (6)
[27] Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune. Automating security analysis: symbolic equivalence of constraint systems. Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science, pages 412-426. Springer, 2010. DOI (5)

[28] Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune. Trace equivalence decision: negative tests and non-determinism. Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17-21, 2011, pages 321-330. ACM, 2011. DOI (16)

[29] Vincent Cheval, Véronique Cortier, and Stéphanie Delaune. Deciding equivalence-based properties using constraint solving. Theor. Comput. Sci. 492:1-39, 2013. DOI (5, 9, 16, 19-21, 30)

[30] Vincent Cheval, Raphaëlle Crubillé, and Steve Kremer. Symbolic protocol verification with dice: process equivalences in the presence of probabilities. 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022, pages 319-334. IEEE, 2022. DOI (16, 85)

[31] Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. DEEPSEC: deciding equivalence properties in security protocols theory and practice. 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA, pages 529-546. IEEE Computer Society, 2018. DOI (1-4, 16)

[32] Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. Exploiting symmetries when proving equivalence properties for security protocols. Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, pages 905-922. ACM, 2019. DOI (4, 40)

[33] Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. The DEEPSEC prover. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 28-36. Springer, 2018. DOI (3)

[34] Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols. Logic, Language, and Security - Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday, volume 12300 of Lecture Notes in Computer Science, pages 127-145. Springer, 2020. DOI (20)

[35] Vincent Cheval, Steve Kremer, Itsaka Rakotonirina, and Victor Yon. Deepsec official website. Installation, manual, tutorial, publications. URL (4, 39)

[36] Yannick Chevalier and Michaël Rusinowitch. Decidability of equivalence of symbolic derivations. J. Autom. Reason. 48(2):263-292, 2012. DOI (5)

[37] Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. Decidability of trace equivalence for protocols with nonces. IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July, 2015, pages 170-184. IEEE Computer Society, 2015. DOI (5, 8)

[38] Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. From security protocols to pushdown automata. ACM Trans. Comput. Log. 17(1):3, 2015. DOI (5)

[39] Ştefan Ciobâcă, Stéphanie Delaune, and Steve Kremer. Computing knowledge in security protocols under convergent equational theories. J. Autom. Reason. 48(2):219-262, 2012. DOI (4, 14, 20)

[40] Katriel Cohn-Gordon, Cas Cremers, Luke Garratt, Jon Millican, and Kevin Milner. On ends-to-ends encryption: asynchronous group messaging with strong security guarantees. Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, pages 1802-1819. ACM, 2018. DOI (2)

[41] Hubert Comon-Lundh and Stéphanie Delaune. The finite variant property: how to get rid of some algebraic properties. Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, pages 294-307. Springer, 2005. DOI (5, 23)

[42] Bruno Conchinha, David A. Basin, and Carlos Caleiro. FAST: an efficient decision procedure for deduction and static equivalence. Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs, pages 11-20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. DOI (4, 14, 20)

[43] Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. Sat-equiv: an efficient tool for equivalence properties. 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, August 21-25, 2017, pages 481-494. IEEE Computer Society, 2017. DOI (5, 41)

[44] Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. A type system for privacy properties. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, pages 409-423. ACM, 2017. DOI (6)

[45] Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. A comprehensive symbolic analysis of TLS 1.3. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, pages 1773-1788. ACM, 2017. DOI (2)
[46] Cas J. F. Cremers. The scyther tool: verification, falsification, and analysis of security protocols. Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, volume 5123 of Lecture Notes in Computer Science, pages 414-418. Springer, 2008. DOI (1)

[47] Stéphanie Delaune, Steve Kremer, and Mark Ryan. Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4):435-487, 2009. DOI (2)

[48] Danny Dolev and Andrew Chi-Chih Yao. On the security of public key protocols (extended abstract). 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981, pages 350-357. IEEE Computer Society, 1981. DOI (2, 7)

[49] Nancy A. Durgin, Patrick Lincoln, and John C. Mitchell. Multiset rewriting and the complexity of bounded security protocols. J. Comput. Secur. 12(2):247-311, 2004. DOI (4)

[50] Lucca Hirschi, David Baelde, and Stéphanie Delaune. A method for verifying privacy-type properties: the unbounded case. IEEE Symposium on Security and Privacy, SP 2016, San Jose, CA, USA, May 22-26, 2016, pages 564-581. IEEE Computer Society, 2016. DOI (6)

[51] PKI Task Force. PKI for machine readable travel documents offering ICC read-only access. Technical report, International Civil Aviation Organization, 2004. (4, 41)

[52] Charlie Jacomme and Steve Kremer. An extensive formal analysis of multi-factor authentication protocols. 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018, pages 1-15. IEEE Computer Society, 2018. DOI (2)

[53] Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017, Paris, France, April 26-28, 2017, pages 435-450. IEEE, 2017. DOI (2)

[54] Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. The TAMARIN prover for the symbolic analysis of security protocols. Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 696-701. Springer, 2013. DOI (1, 3)

[55] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Inf. Comput. 100(1):1-40, 1992. DOI (14)

[56] Michaël Rusinowitch and Mathieu Turuani. Protocol insecurity with a finite number of sessions, composed keys is np-complete. Theor. Comput. Sci. 299(1-3):451-475, 2003. DOI (4, 5)

[57] Peter Y. A. Ryan and Steve A. Schneider. Prêt à voter with re-encryption mixes. Computer Security - ESORICS 2006, 11th European Symposium on Research in Computer Security, Hamburg, Germany, September 18-20, 2006, Proceedings, volume 4189 of Lecture Notes in Computer Science, pages 313-326. Springer, 2006. DOI (4, 41)

[58] Sonia Santiago, Santiago Escobar, Catherine Meadows, and José Meseguer. A formal definition of protocol indistinguishability and its verification using Maude-NPA. Security and Trust Management - 10th International Workshop, STM 2014, Wroclaw, Poland, September 10-11, 2014. Proceedings, volume 8743 of Lecture Notes in Computer Science, pages 162-177. Springer, 2014. DOI (1, 3, 6)

[59] Alwen Tiu and Jeremy E. Dawson. Automating open bisimulation checking for the spi calculus. Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, pages 307-321. IEEE Computer Society, 2010. DOI (5)

[60] Alwen Tiu, Nam Nguyen, and Ross Horne. SPEC: an equivalence checker for security protocols. Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 87-95, 2016. DOI (5, 41)
# A. Decision procedures using partition trees

We detail in this appendix the technical proofs of correctness of the decision procedures for equivalences of Section 3.6, assuming a partition tree $T$ priorly constructed.

## A.1 Trace equivalence

We prove in this section the following theorem:

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

1. $P_1 \subseteq_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 theorem relies on two technical lemmas extending the properties of the partition tree edges to its branches, i.e., from $\xrightarrow{T}$ to $\xrightarrow{\text{tr}}_T$. For example we can generalise as follows the fact that the nodes of the tree are labelled by maximal configurations, i.e., Definition 3.17, Item 4:

**LEMMA A.1.** Assume that $(\mathcal{P}_1, C_1)$, $n \xrightarrow{\text{tr}}_T (\mathcal{P}'_1, C'_1)$, $n'$ and $(\mathcal{P}_2, C_2) \xrightarrow{\text{tr}}_S (\mathcal{P}'_2, C'_2)$ with $(\mathcal{P}_2, C_2) \in \Gamma(n)$. We also consider, for all $i \in \{1, 2\}$, a solution $(\Sigma', \sigma'_i) \in \text{Sol}^{\pi(n')}(C'_i)$ such that $\Phi(C'_1)\sigma'_1 \sim \Phi(C'_2)\sigma'_2$. Then we have $(\mathcal{P}_2, C_2)$, $n \xrightarrow{\text{tr}}_T (\mathcal{P}'_2, C'_2)$, $n'$.

**PROOF.** We proceed by induction on the length tr. The case $tr = \varepsilon$ follows from the saturation of nodes under $\tau$-transition (Definition 3.17, Item 1). Otherwise we let, with $tr = \alpha \cdot \tilde{\tau}$,

$$ (\mathcal{P}_1, C_1), n \xrightarrow{\alpha} T (\tilde{\mathcal{P}}_1, \tilde{C}_1), \tilde{n} \xrightarrow{\tilde{\tau}} T (\mathcal{P}'_1, C'_1), n' \qquad (\mathcal{P}_2, C_2) \xrightarrow{\alpha} S (\tilde{\mathcal{P}}_2, \tilde{C}_2) \xrightarrow{\tilde{\tau}} S (\mathcal{P}'_2, C'_2) $$

We also consider the restrictions $\Sigma = \Sigma'_{|\text{vars}^2(n)}$ and $\tilde{\Sigma} = \tilde{\Sigma}'_{|\text{vars}^2(\tilde{n})}$. In particular $\Sigma \subseteq \tilde{\Sigma}$ and there exist $\sigma_2, \tilde{\sigma}_1, \tilde{\sigma}_2$ such that

$$ (\Sigma, \sigma_2) \in \text{Sol}(C_2) \qquad (\tilde{\Sigma}, \tilde{\sigma}_1) \in \text{Sol}(\tilde{C}_1) \qquad (\tilde{\Sigma}, \tilde{\sigma}_2) \in \text{Sol}(\tilde{C}_2) $$

The hypothesis that $\Phi(C'_1)\sigma'_1 \sim \Phi(C'_2)\sigma'_2$ also implies that $\Phi(\tilde{C}_1)\tilde{\sigma}_1 \sim \Phi(\tilde{C}_2)\tilde{\sigma}_2$. Besides since predicates are refined along branches (Definition 3.17, Item 3) and are defined on the variables of their configurations (Definition 3.16, Item 1), we know that $\Sigma$ and $\tilde{\Sigma}$ verify $\pi(n)$ and $\pi(\tilde{n})$, respectively.

All in all we can use the maximality of the node $\tilde{n}$ (Definition 3.17, Item 4 applied to the edge $n \xrightarrow{\alpha} \tilde{n}$), which gives that $(\tilde{\mathcal{P}}_2, \tilde{C}_2) \in \Gamma(\tilde{n})$. Hence $(\mathcal{P}_2, C_2)$, $n \xrightarrow{\alpha} T (\tilde{\mathcal{P}}_2, \tilde{C}_2)$, $\tilde{n}$ by definition and the conclusion then follows from the induction hypothesis applied to the remaining of the traces. ■
Combined with the soundness and the completeness of the symbolic semantics, this permits to prove one direction of Theorem 3.20:

**PROOF OF THEOREM 3.20, 1⇒2.** Let us consider a trace $P_1 \underset{T}{\overset{\mathrm{tr}}{\Rightarrow}} (\mathcal{P}_1, C_1)$, $n$ and exhibit a trace $P_2 \underset{T}{\overset{\mathrm{tr}}{\Rightarrow}} (\mathcal{P}_2, C_2)$, $n$. We decompose the proof into the following steps:

1. By soundness of the symbolic semantics we obtain a trace $P_1 \underset{\Phi(C_1)\sigma_1\downarrow}{\overset{\mathrm{tr}\Sigma}{\Rightarrow}} (\mathcal{P}_1\sigma_1, \Phi(C_1)\sigma_1\downarrow)$ for an arbitrary solution $(\Sigma, \sigma_1) \in \mathrm{Sol}(C_1)$.

2. By hypothesis 1 there exists a concrete trace $P_2 \underset{\Phi(C_2)\sigma_2\downarrow}{\overset{\mathrm{tr}\Sigma}{\Rightarrow}} (\mathcal{P}, \Phi)$ such that $\Phi \sim \Phi(C_1)\sigma_1\downarrow$.

3. By completeness of the symbolic semantics we obtain a symbolic trace $P_2 \underset{\Phi(C_2)\sigma_2\downarrow}{\overset{\mathrm{tr}'}{\Rightarrow}} (\mathcal{P}_2, C_2)$ and $(\Sigma', \sigma_2) \in \mathrm{Sol}(C_2)$ such that $\mathrm{tr}\Sigma = \mathrm{tr}'\Sigma'$, $\mathcal{P}_2\sigma_2 = \mathcal{P}$ and $\Phi(C_2)\sigma_2\downarrow = \Phi$. Due to the form of symbolic actions, we know that there exists a second-order-variable renaming $\rho$ such that $\mathrm{tr} = \mathrm{tr}'\rho$; in particular $P_2 \underset{\Phi(C_2)\sigma_2\downarrow}{\overset{\mathrm{tr}}{\Rightarrow}} (\mathcal{P}_2, C_2\rho)$ and $(\Sigma, \sigma_2) \in \mathrm{Sol}(C_2\rho)$.

4. By Lemma A.1 we therefore obtain that $P_2 \underset{T}{\overset{\mathrm{tr}}{\Rightarrow}} (\mathcal{P}_2, C_2\rho)$, $n$, which gives the expected conclusion. ■

The second property of the partition tree we extend is the fact that symbolic transitions are reflected in the tree, i.e., Definition 3.17, Item 2:

**LEMMA A.2.** Let $n$ be a node of a partition tree $T$ and $(\mathcal{P}, C) \in \Gamma(n)$. If $(\mathcal{P}, C) \underset{\mathcal{P}'}{\overset{\mathrm{tr}}{\Rightarrow}} (\mathcal{P}', C')$ and $(\Sigma, \sigma) \in \mathrm{Sol}^{\pi(n)}(C')$ then there exist a node $n'$ and a substitution $\Sigma'$ such that $(\mathcal{P}, C), n \underset{T}{\overset{\mathrm{tr}}{\Rightarrow}} (\mathcal{P}', C')$, $n'$ and $(\Sigma', \sigma) \in \mathrm{Sol}^{\pi(n')}(C')$.

Note that unlike the definition of partition tree, we do not require that $\Sigma'$ coincides with $\Sigma$ on $\mathrm{vars}^2(n)$. This additional requirement would not make the lemma false but is unnecessary to prove Theorem 3.20. The lemma is proved by induction on tr below:

**PROOF.** We proceed by induction on the length of tr. If $\mathrm{tr} = \varepsilon$ it suffices to choose $n = n'$ and the conclusion immediately follows. Otherwise let us decompose the symbolic trace into

$$ (\mathcal{P}, C) \underset{\mathcal{P}'}{\overset{\mathrm{tr}}{\Rightarrow}} (\tilde{\mathcal{P}}, \tilde{C}) \underset{\mathcal{P}'}{\overset{\alpha}{\Rightarrow}} (\mathcal{P}', C') \qquad \mathrm{tr} = \mathrm{tr} \cdot \alpha $$

Note that $(\Sigma_{|\mathrm{vars}^2(\tilde{n})}, \sigma_{|\mathrm{vars}^1(\tilde{n})}) \in \mathrm{Sol}(\tilde{C})$, and $\Sigma_{|\mathrm{vars}^2(\tilde{n})}$ verifies $\pi(n)$ by definition of a configuration (since $\Sigma$ verifies it and has the same restriction to $\mathrm{vars}^2(\Gamma(n))$ as $\Sigma_{|\mathrm{vars}^2(\tilde{n})}$). By induction hypothesis we therefore obtain $\tilde{n}, \tilde{\Sigma}$ such that $(\mathcal{P}, C), n \underset{T}{\overset{\mathrm{tr}}{\Rightarrow}} (\tilde{\mathcal{P}}, \tilde{C}), \tilde{n}$ and $(\tilde{\Sigma}, \sigma_{|\mathrm{vars}^1(\tilde{n})}) \in \mathrm{Sol}^{\pi(\tilde{n})}(\tilde{C})$. Let us then consider the extension

$$ \tilde{\Sigma}^e = \tilde{\Sigma} \cup \Sigma_{|\mathrm{vars}^2(n') \setminus \mathrm{vars}^2(\tilde{n})} $$

To conclude the proof it suffices to apply the Item 2 of Definition 3.17 to the symbolic transition $(\tilde{\mathcal{P}}, \tilde{C}) \underset{\mathcal{P}'}{\overset{\alpha}{\Rightarrow}} (\mathcal{P}', C')$ and the solution $(\tilde{\Sigma}^e, \sigma)$; what remains to prove is therefore that we effectively have $(\tilde{\Sigma}^e, \sigma) \in \mathrm{Sol}^{\pi(\tilde{n})}(C')$. First of all we indeed have by construction $\mathrm{dom}(\tilde{\Sigma}^e) = \mathrm{vars}^2(C')$ and $\mathrm{dom}(\sigma) = \mathrm{vars}^1(C')$. We also know that $\tilde{\Sigma}^e$ satisfies the predicate $\pi(\tilde{n})$ because $\tilde{\Sigma} = \tilde{\Sigma}_{|\mathrm{vars}^2(\tilde{n})}^e$
satisfies it. The first-order solution $\sigma$ satisfies the constraints of $E^1(C')$ since $(\Sigma, \sigma) \in Sol(C')$ by hypothesis. Finally we let $\varphi \in D(C')$ and prove that $(\Phi(C'), \tilde{\Sigma}^e, \sigma) \models \varphi$:

* case 1: $\varphi = (X \vdash^? x) \in D(\tilde{C})$

The conclusion follows from the fact that $(\tilde{\Sigma}, \sigma|_{vars^1(\tilde{n})}) \in Sol(\tilde{C})$.

* case 2: $\varphi = (X \vdash^? x) \in D(C') \setminus D(\tilde{C})$

The conclusion follows from the fact that $(\Sigma, \sigma) \in Sol(C')$.

* case 3: $\varphi = \forall X. X \not? x$

We have to prove that $x\sigma$ is not deducible from the frame $\Phi(C')\sigma$, which is a consequence from the fact that $(\Sigma, \sigma) \in Sol(C')$. ■

Using again the soundness and completeness of the symbolic semantics, we can finally derive the other direction of Theorem 3.20.

**PROOF OF THEOREM 3.20, 2⇒1.** Let us consider a trace $P_1 \stackrel{\text{tr}}{\Rightarrow} (\mathcal{P}, \Phi)$ and exhibit a trace $P_2 \stackrel{\text{tr}}{\Rightarrow} (Q, \Psi)$ such that $\Phi \sim \Psi$. We decompose the proof into the following steps:

1. By completeness of the symbolic semantics we obtain a symbolic trace $P_1 \stackrel{\text{tr}_s}{\Rightarrow}_s (\mathcal{P}_1, C_1)$ and $(\Sigma, \sigma_1) \in Sol(C)$ such that $\text{tr}_s\Sigma = \text{tr}, \mathcal{P}_1\sigma_1 = \mathcal{P}$ and $\Phi(C_1)\sigma_1\downarrow = \Phi$.

2. By Lemma A.2 we then obtain a partition-tree trace $P_1 \stackrel{\text{tr}_s}{\Rightarrow}_T (\mathcal{P}_1, C_1)$, $n$ and $\Sigma'$ such that $(\Sigma', \sigma_1) \in Sol^{\pi(n)}(C_1)$.

3. By hypothesis 2 there also exists a partition-tree trace $P_2 \stackrel{\text{tr}_s}{\Rightarrow}_T (\mathcal{P}_2, C_2)$, $n$. By definition of a configuration we also know that there exists $\sigma_2$ such that $(\Sigma', \sigma_2) \in Sol^{\pi(n)}(C_2)$ and $\Phi(C_1)\sigma_1 \sim \Phi(C_2)\sigma_2$.

4. By soundness of the symbolic semantics applied to we then obtain a concrete trace $P_2 \stackrel{\text{tr}_s\Sigma'}{\Rightarrow} (Q, \Psi)$ with $Q = \mathcal{P}_2\sigma_2$ and $\Psi = \Phi(C_2)\sigma_2\downarrow \sim \Phi(C_1)\sigma_1\downarrow = \Phi$.

However we may have $\text{tr}_s\Sigma' \neq \text{tr}$ and, to conclude the proof, we prove that $P_2 \stackrel{\text{tr}}{\Rightarrow} (Q, \Psi)$ as well. For that it suffices to prove that $\text{tr}\Psi\downarrow = \text{tr}_s\Sigma'\Psi\downarrow$, that is, although the recipes or tr and $\text{tr}_s\Sigma'$ are different they produce the same first-order terms. Since $\Phi$ and $\Psi$ are statically equivalent, $\text{tr} = \text{tr}_s\Sigma$ and $\Phi = \Phi(C_1)\sigma_1\downarrow$, it suffices to prove that $\text{tr}_s\Sigma\Phi(C_1)\sigma\downarrow = \text{tr}_s\Sigma'\Phi(C_1)\sigma\downarrow$. Let $X \in \text{vars}^2(\text{tr}_s)$. A quick look at the rules of the symbolic semantics shows that there exists a deduction fact $(X \vdash^? x) \in D(C_1)$. In particular, since $(\Sigma, \sigma_1)$ and $(\Sigma', \sigma_1)$ are both solutions of $C_1$ we have $X\Sigma\Phi(C_1)\sigma_1\downarrow = x\sigma_1\downarrow = X\Sigma'\Phi(C_1)\sigma_1\downarrow$, hence the conclusion. ■

## A.2 Simulations

In this section, we now prove the main theorem at the basis of the decision procedure for simulations and its variants:
**THEOREM 3.25 (partition-tree-based characterisation of labelled bisimilarity).** If $T \in \text{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 $\text{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 $\text{Sol}(w_s) = \emptyset$

We only prove the case of labelled bisimilarity, as the proof for simulation is analogue. For that, we prove the following technical lemma by induction on the structure of the (symbolic) witness; this lemma is a stronger version of the theorem for the purpose of managing the induction invariant.

**LEMMA A.3.** Let $n$ be a node of a partition tree $T$ and $A_0, A_1 \in \Gamma(n)$. We let $A_i = (P_i, C_i)$ and $\Sigma, \sigma_0, \sigma_1$ such that $(\Sigma, \sigma_i) \in \text{Sol}^{\pi^{(n)}}(C_i)$. If $A_i^c = (P_i \sigma_i, \Phi(C_i) \sigma_i \downarrow)$, the following points are equivalent:

1. $A_0^c \not\approx_b A_1^c$

2. there exist a symbolic witness $w_s$ for $(A_0, A_1, n)$ and a solution $f_{\text{sol}} \in \text{Sol}(w_s)$ such that $f_{\text{sol}}(\text{root}(w_s)) = \Sigma$

To prove this lemma we first observe that, by definition of a configuration (Definition 3.16), $A_0^c \sim A_1^c$ because these two processes are obtained by instanciating two symbolic processes from a same node $n$ with a common solution $\Sigma$. We then prove the two directions separately.

**PROOF OF LEMMA A.3, 1 $\Rightarrow$ 2.**

We prove the result by induction on $|\mathcal{P}_0, \mathcal{P}_1|$. The conclusion is immediate if $|\mathcal{P}_0, \mathcal{P}_1| = 0$ as it yields a contradiction: the multisets $\mathcal{P}_0$ and $\mathcal{P}_1$ can only contain null processes and the fact that $A_0^c \sim A_1^c$ justifies that $A_0^c \approx_b A_1^c$. Otherwise we let by Proposition 3.22 a witness $w$ of $(A_0^c, A_1^c)$. Thus, by definition, there exist $b \in \{0, 1\}$ and a transition $A_b^c \xrightarrow{\alpha} A_b'^c = (Q, \Phi)$ such that for all traces $A_{1-b}^c \xrightarrow{\bar{\alpha}} A_{1-b}'^c$ such that $A_0'^c \sim A_0'^c$, we have $(A_0'^c, A_1'^c) \in \text{w}$ (and therefore $A_0'^c \not\approx_b A_1'^c$ by Proposition 3.22). Let us now construct a symbolic witness $w_s$ of $(A_0, A_1, n)$ and a suitable solution $f_{\text{sol}}$.

► case 1: $\alpha \neq \tau$

By completeness of the symbolic semantics (Proposition 3.15) applied to the transition $A_b^c \xrightarrow{\alpha} A_b'^c$, we let a symbolic transition $A_b \xrightarrow{\alpha_s} A_b' = (Q_s, C)$ and a solution $(\Sigma', \sigma') \in \text{Sol}(C)$ such that $\Sigma \subseteq \Sigma'$, $\alpha = \alpha_s \Sigma'$, $Q = Q_s \sigma'$ and $\Phi = \Phi(C) \sigma' \downarrow$. Note that by hypothesis $\Sigma$ verifies $\pi(n)$ and, therefore, so does its extension $\Sigma'$ (since by definition predicates are stable by domain extension, recall Definition 3.16). Then since the symbolic transition $A_b \xrightarrow{\alpha_s} A_b'$ is reflected in $T$ (in the sense of Definition 3.17, Item 2), we obtain a transition $A_b, n \xrightarrow{\alpha_s} T A_b'$, $n'$ and $\Sigma''$ such that $(\Sigma'', \sigma') \in \text{Sol}^{\pi^{(n')}}(C)$ and $\Sigma''|_{\text{vars}^2(n)} = \Sigma'|_{\text{vars}^2(n)} (= \Sigma)$.
► case 1a: there exist no $A'_{1-b}$ such that $A_{1-b}, n \stackrel{\alpha_s}{\Rightarrow_T} A'_{1-b}, n'$

Then we define $w_s$ to be the tree whose root is labelled $(A_0, A_1, n)$ and that has a unique child labelled $(A'_b, n')$. We then consider $f_{sol}$ mapping the child to $\Sigma''$ and the root to $\Sigma''_{|vars^2(n)} = \Sigma$, which is a solution of $w_s$.

► case 1b: otherwise

In this case we define $w_s$ as follows. Its root is labelled $(A_0, A_1, n)$ and its children are all the nodes labelled $(A'_0, A'_1, n')$, with $A_{1-b}, n \stackrel{\alpha_s}{\Rightarrow_T} A'_{1-b}, n'$. For each such node, as explained in the beginning of the proof we have $A'_0 \not\equiv_b A'_1$ which permits to apply the induction hypothesis with the solution $\Sigma''$. This gives a symbolic witness rooted in this node and $f_{sol}$ a solution mapping this node to $\Sigma''$. Let us write more explicitly these witnesses $w_s^1, \dots, w_s^p$ and $f_{sol}^1, \dots, f_{sol}^p$ the corresponding solutions. To conclude it then suffices to choose $w_s^1, \dots, w_s^p$ as the children of the root of $w_s$, and $f_{sol}$ maps the root of $w_s$ to $\Sigma''_{|vars^2(n)} = \Sigma$ and each node $n$ of $w_s^i$ to $f_{sol}^i(n)$.

► case 2: $\alpha = \tau$

Analogue to case 1 in the simpler case where $n = n'$ and $\Sigma = \Sigma' = \Sigma''$. Note also that the analogue of case 1a cannot arise. ■

PROOF OF LEMMA A.3, 2$\Rightarrow$1.

We construct a concrete witness $w$ of $(A_0^c, A_1^c)$ as follows:

$$ w = \left\{ \left( (\mathcal{P}_0\sigma_0, \Phi(C_0)\sigma_0\downarrow), (\mathcal{P}_1\sigma_1, \Phi(C_1)\sigma_1\downarrow) \right) \middle| \begin{array}{l} \text{$N$ node of $w_s$ labelled $((\mathcal{P}_0, C_0), (\mathcal{P}_1, C_1), n)$,} \\ \forall i \in \{0, 1\}, (f_{sol}(N), \sigma_i) \in \text{Sol}(C_i) \end{array} \right\} $$

The fact that all $(B_0, B_1) \in w$ verify $B_0 \sim B_1$ follows from Definition 3.16. Then let us consider $((\mathcal{P}_0\sigma_0, \Phi(C_0)\sigma_0\downarrow), (\mathcal{P}_1\sigma_1, \Phi(C_1)\sigma_1\downarrow)) \in w$ using the notations of the construction of $w$ above. By definition of a symbolic witness there exists $b \in \{0, 1\}$ and a transition $(\mathcal{P}_b, C_b), n \stackrel{\alpha}{\Rightarrow_T} (\mathcal{P}'_b, C'_b), n'$ such that:

► case 1: $N = \text{root}(w_s)$ has a unique child $N'$ labelled $\{(\mathcal{P}'_b, C'_b)\}, n'$

Then consider the concrete transition $(\mathcal{P}_b\sigma_b, \Phi(C_b)\sigma_b\downarrow) \xrightarrow{\alpha f_{sol}(N')} (\mathcal{P}'_b\sigma'_b, \Phi(C'_b)\sigma'_b\downarrow)$ obtained by soundness of the symbolic semantics (Proposition 3.15) where $(f_{sol}(N'), \sigma'_b) \in \text{Sol}^{\pi(n')}(C'_b)$. By completeness of the symbolic semantics (which is possible to apply since $f_{sol}(N) \subseteq f_{sol}(N')$ by definition of a solution of a symbolic witness) and maximality of the node $n'$ (Definition 3.17, Item 4), there cannot exist any concrete trace of the form

$$ (\mathcal{P}_{1-b}\sigma_{1-b}, \Phi(C_{1-b})\sigma_{1-b}\downarrow) \xrightarrow{\alpha f_{sol}(N')} (\mathcal{P}, \Phi) $$

such that $\Phi \sim \Phi(C'_b)\sigma'_b$, hence the conclusion.

► case 2: the children of $N = \text{root}(w_s)$ are all the nodes $N'$ labelled $((\mathcal{P}'_0, C'_0), (\mathcal{P}'_1, C'_1), n')$, where $(\mathcal{P}_{1-b}, C_{1-b}), n \stackrel{\alpha}{\Rightarrow_T} (\mathcal{P}'_{1-b}, C'_{1-b}), n'$ (and there is at least one such child)
Let $N'$ be an arbitrary child of $N$, labelled $((P'_0, C'_0), (P'_1, C'_1), n')$ with the above notations.
As in the previous case we consider the concrete transition obtained by soundness of the
symbolic semantics, $(P_b \sigma_b, \Phi(C_b) \sigma_b \downarrow) \xrightarrow{\alpha f_{sol}(N')} (P'_b \sigma'_b, \Phi(C'_b) \sigma'_b \downarrow)$. Then let us consider a trace of
the form

$$ (P_{1-b} \sigma_{1-b}, \Phi(C_{1-b}) \sigma_{1-b} \downarrow) \overset{\alpha f_{sol}(N')}{\rightleftharpoons} (P, \Phi) = A \qquad \Phi \sim \Phi(C'_b) \sigma'_b $$

Our goal is to prove that $(A, (P_b \sigma_b, \Phi(C_b) \sigma_b \downarrow)) \in w$. Using the completeness of the symbolic semantics and the maximality of $n'$ as in the previous case, we obtain a partition-tree trace $(P_{1-b}, C_{1-b}), n \stackrel{\alpha}{\Rightarrow}_T (P''_{1-b}, C''_{1-b}), n'$ and $(f_{sol}(N'), \sigma''_{1-b}) \in Sol^{\pi(n')}(C''_{1-b})$ with $P = P''_{1-b} \sigma''_{1-b}$ and $\Phi = \Phi(C''_{1-b}) \sigma''_{1-b} \downarrow$. By hypothesis there therefore exists a node $N''$, a child of $N$, labelled $((P'_b, C'_b), (P''_{1-b}, C''_{1-b}), n')$. The conclusion then follows from the fact that $f_{sol}(N') = f_{sol}(N'')$ by definition of a solution of a symbolic witness. ■

# B. Correctness of the generation of partition trees

## B.1 Invariants of the procedure

In this section we present some additional properties that are verified all along the procedure
by the nodes of the partition tree under construction. Such nodes are sets of extended symbolic
processes (i.e. tuples $(\mathcal{P}, C, C^e)$ with $\mathcal{P}$ a process, $C$ a constraint system and $C^e$ an extended
constraint system). Understanding the technical details of these invariants is not necessary to
understand the algorithm itself, however most of our subprocedure (e.g. the generation of most
general solutions) are only correct in their context.

**Invariant 1: Well-formedness** The first invariant is about the shape of the extended constraint
systems. Two important properties are that all equations of $E^1$ and $E^2$ are trivially satisfiable
(they are essentially of the form $x =^? u$ where $x$ appears nowhere else in the constraint system)
and that those of $E^2$ only use terms that can be constructed from the knowledge base (i.e. they
are consequences of $K \cup D$).

**DEFINITION B.1.** We define the predicate $Inv_{wf}$ on extended constraint systems as follows;
we have that $Inv_{wf}((\Phi, D, E^1, E^2, K, F))$ holds when

— Variables in K and F: $vars^2(K, F) \subseteq vars^2(D)$

— Equation: $mgu(E^i) \neq \perp, \text{dom}(mgu(E^i)) \cap vars^i(D) = \emptyset, vars^i(img(mgu(E^i))) \subseteq vars^i(D)$.

— Solution is consequence: $img(mgu(E^2)) \subseteq \text{Conseq}(K \cup D)$.

— Shape of K: For all $\psi = (\xi \vdash^? u) \in K, \psi \in F, u \notin \mathcal{X}^1, u \in st(\Phi)$ and $st(\xi) \subseteq \text{Conseq}(K \cup D)$.

— Shape of F: For all $\forall S. H \Leftarrow \varphi \in F(C), S$ is empty and $\varphi$ only contains syntactic equations as
hypothesis, i.e. no deduction facts. Moreover $sst^2(H) \subseteq \text{Conseq}(K \cup D)$, and if $H = \xi \vdash^? u$
then either $u \in st(\Phi)$ or there exists a recipe $\zeta$ such that $(\zeta, u) \in \text{Conseq}(K \cup D)$.
This invariant is lifted to sets of extended constraint systems in the natural way, i.e. $Inv_{wf}(S)$ holds iff for all $C \in S$, $Inv_{wf}(C)$ holds.

**Invariant 2: Formula soundness** The second invariant states that any substitution that satisfies the deduction facts of D and the equalities of $E^1$ also satisfies all formulas of $K \cup F$. This means that the procedure only adds correct formulas to the constraint system, sometimes under some hypothesis for the formulas of F.

**DEFINITION B.2.** We define the predicate $Inv_{sound}$ on extended constraint systems as follows; we have that $Inv_{sound}((\Phi, D, E^1, E^2, K, F))$ holds when for all $\psi \in K \cup F$, for all substitutions $\Sigma, \sigma$, if

$$ (\Phi, \Sigma, \sigma) \models D' \wedge E_{\underline{=} 1} \quad \text{with } D' = \{\psi' \in D | \text{vars}^2(\psi') \subseteq \text{vars}^2(\psi)\} $$

where $E_{\underline{=} 1}$ if the set of equations of $E^1$, then $(\Phi, \Sigma, \sigma) \models \psi$.

**Invariant 3: Formula completeness** Given a formula $\psi = H \Leftarrow \varphi$ in F, the soundness invariant above states that when some substitutions satisfy $\varphi$ then they also satisfy the head $H$. The next invariant can be seen as a kind of converse statement: when some substitutions satisfy the head $H$, there exists a formula $\psi' \in F$ (not necessarily the same) that has the same head and whose hypotheses are satisfied. This means that the procedure always covers all cases when generating the potential hypotheses of a given head $H$.

**DEFINITION B.3.** In this definition, we say that $(\Phi, \Sigma, \sigma)$ weakly satisfies a head $H$ when:

- if $H = \xi \vdash^? u$ then $\text{msg}(\xi\Sigma\Phi\sigma)$, i.e. the recipe $\xi$ leads to a valid message

- if $H = \xi =_f^? \zeta$ then $(\Phi, \Sigma, \sigma)$ satisfies $H$ in the usual sense, i.e. the recipes $\xi, \zeta$ lead to the same valid message.

Given a set of extended processes $\Gamma$, the predicate $Inv_{comp}(\Gamma)$ holds when for all $C_1^e, C_2^e \in \Gamma$, for all $(H \Leftarrow \varphi) \in F(C_1^e)$, for all $(\Sigma, \sigma) \in \text{Sol}(C_2^e)$, if $(\Phi(C_2^e), \Sigma, \sigma)$ weakly satisfies $H$ then there exists $(H' \Leftarrow \varphi') \in F(C_2^e)$ such that $H' \simeq_r H$ and $(\Phi(C_2^e), \Sigma, \sigma) \models \varphi'$.

**Invariant 4: Knowledge-base saturation** The next invariant states that the knowledge base $K$ is saturated, i.e. that we do not miss solutions by imposing that they are constructed from $K$ (see Definition 4.4).

**DEFINITION B.4.** We define the predicate $Inv_{satur}$ on extended constraint systems as follows. We have that $Inv_{satur}(C)$ holds when, considering the minimal $k$ such that $\text{vars}^2(D(C)) \subseteq \mathcal{X}_{\leq k}^2$, for all $f/n \in \mathcal{F}_d$, for all $(\xi_1, u_1), \dots, (\xi_n, u_n) \in \text{Conseq}(K(C))$ such that $\xi_1, \dots, \xi_n \in \mathcal{T}_k^2$, if $f(u_1, \dots, u_n) \downarrow$ is a constructor term then there is $\xi \in \mathcal{T}_k^2$ such that $(\xi, f(u_1, \dots, u_n) \downarrow) \in \text{Conseq}(K(C) \cup D(C))$.

**Invariant 5: Preservation of solutions** Finally the last invariant states that all the constraint solving performed on the additional data of extended constraint systems $(E^2, K, F)$ preserves the
solutions. That is, in an extended symbolic process $(\mathcal{P}, C, C^e)$, where $C$ is the constraint system obtained by only collecting constraints during the execution of the process $\mathcal{P}$ (i.e. without additional constraint solving), all solutions of $C^e$ are solutions of $C$.

**DEFINITION B.5.** We define the predicate $\text{Inv}_{\text{sol}}$ defined on extended symbolic processes where $\text{Inv}_{\text{sol}}((\mathcal{P}, C, C^e))$ holds when

- for all $i \in \mathbb{N}$, $\text{vars}^2(C) \subseteq \mathcal{X}_{\leq i}^2$ iff $\text{vars}^2(C^e) \subseteq \mathcal{X}_{\leq i}^2$.

- for all $(\Sigma, \sigma) \in \text{Sol}(C^e)$, $(\Sigma_{|\text{vars}^2(C)}, \sigma_{|\text{vars}^1(C)}) \in \text{Sol}(C)$.

We restrict the substitutions to the variables of $C$ since our extended constraint system may introduce new variables (e.g. by applying most general solutions) but all these variables are uniquely defined by the instantiation of the variables of $C$.

**Invariant 6: Component structure** Finally we state an invariant on components stating that all of their constraint systems have the same second-order structure. This invariant is preserved during the procedure by the fact that the constraint-solving rules that modify $\mathcal{K}$ or $\mathcal{E}^2$ are always applied to the entire components.

**DEFINITION B.6.** We define the predicate $\text{Inv}_{\text{str}}$ defined on sets of extended symbolic processes where $\text{Inv}_{\text{sol}}(\Gamma)$ holds when for all $(\mathcal{P}_1, C_1, C_1^e), (\mathcal{P}_2, C_2, C_2^e) \in \Gamma$,

- $\text{dom}(\Phi(C_1^e)) = \text{dom}(\Phi(C_2^e))$

- $\text{vars}^2(C_1^e) = \text{vars}^2(C_2^e)$

- $\{\xi \mid (\xi \vdash^? u) \in \mathcal{K}(C_1^e)\} = \{\xi \mid (\xi \vdash^? u) \in \mathcal{K}(C_2^e)\}$

**Overall invariant** As we mentioned, all invariants are lifted to sets of extended symbolic processes in the natural way if needed. We refer as

$$ \text{Inv}_{\text{all}}(\Gamma) = \text{Inv}_{\text{wf}}(\Gamma) \wedge \text{Inv}_{\text{sound}}(\Gamma) \wedge \text{Inv}_{\text{comp}}(\Gamma) \wedge \text{Inv}_{\text{satur}}(\Gamma) \wedge \text{Inv}_{\text{sol}}(\Gamma) \wedge \text{Inv}_{\text{str}}(\Gamma) $$

the invariant of the whole procedure on the nodes of the partition tree (i.e. sets of extended symbolic processes).

## B.2 Preservation of the invariants

In this section we prove that the invariants of the procedure stated in Section B.1 are preserved all along the procedure. First of all we prove the case of the case distinction rules:

**LEMMA B.7.** Let $\mathcal{S}$ be a set of extended symbolic processes such that $\text{Inv}_{\text{all}}(\mathcal{S})$. Let $\mathcal{S} \to \mathcal{S}'$ by applying one case distinction rule and then normalising the result with the simplification rules. We have that $\text{Inv}_{\text{all}}(\mathcal{S}')$.
For the proof we let $\Gamma' \in \mathcal{S}'$ and write $\Gamma \in \mathcal{S}$ the set from which $\Gamma'$ is originated, i.e. $\Gamma'$ is one of the sets obtained after applying one case distinction rule to $\Gamma$ (either the positive or the negative branch) and then normalising with the simplification rules.

**PROOF.** (Preservation of $\text{Inv}_{wf}$.) Let $C^{e'} = (\Phi, D, E^1, E^2, K, F)$ for some $(\mathcal{P}', C', C^{e'}) \in \Gamma'$. We consider each item of the definition of the predicate (Definition B.1) and show that $C^{e'}$ verifies them.

► property 1 (Variables in K and F): $\text{vars}^2(K, F) \subseteq \text{vars}^2(D)$.

We first observe that this property is preserved by all simplification rules: therefore it sufficies to prove that it is preserved by application of case distinction rules. For that we also observe that if $C^e$ is an extended constraint system verifying this property then for all second-oder substitutions $\Sigma$, $C^e:\Sigma$ verifies it as well (which is precisely why we consider this notation rather than a raw application $C^e\Sigma$). This is sufficient for getting the expected result for Rule (SAT). The case of the negative branches of Rules (REW) and (EQ) are trivial. Regarding their positive branches, we only treat the case of Rule (EQ) since the treatment of (REW) can be obtained by using a similar reasoning on each formulas added by the rule (the sets $F_0$ in the notations of Rule (REW)). The rule (EQ) does not introduce elements in K and the only second-oder variables introduced in F that are not trivially added to D are from recipes $\xi_1, \xi_2$ such that $\xi_1 \vdash^? u_1, \xi_2 \vdash^? u_2 \in K(C^e)$ for some $(\mathcal{P}, C, C^e) \in \Gamma$. In particular by hypothesis $\text{vars}^2(\xi_1, \xi_2) \subseteq \text{vars}^2(D(C^e)) \subseteq \text{vars}^2(D(C^{e'}))$, hence the conclusion.

► property 2 (first and second-order equations): we have $\text{mgu}(E^i) \neq \perp$, $\text{dom}(\text{mgu}(E^i)) \cap \text{vars}^i(D) = \emptyset$, and $\text{vars}^i(\text{img}(\text{mgu}(E^i))) \subseteq \text{vars}^i(D)$.

The fact that $\text{mgu}(E^i) \neq \perp$ is a direct consequence of the facts that $C^{e'} \neq \perp$ and that $C^{e'}$ is already normalised by the simplification rules of Figure 8, in particular Rules NORM-UNIF and the rules inherited from Figure 7. The remaining properties are simple invariants of the mgu's that are straightforward to verify.

► property 3 (Solution is consequence): $\text{img}(\text{mgu}(E^2)) \subseteq \text{Conseq}(K \cup D)$.

This property comes from the fact that $\text{mgu}(E^2)$ is only modified in the positive branches of the case distinction rules by applying a mgs $\Sigma$ to the extended constraint systems $C^e \in \Gamma$. A quick induction on the constraint solving relation for computing mgs $\rightsquigarrow$ show that $\text{img}(\Sigma) \subseteq \text{Conseq}(K(C^e) \cup D(C^e))$, hence the conclusion.

► property 4 (Shape of K): for all $\psi = (\xi \vdash^? u) \in K$, $\psi \in F$, $u \notin \mathcal{X}^1$, $u \in \text{st}(\Phi)$ and $\text{st}(\xi) \subseteq \text{Conseq}(K \cup D)$.

The only rule adding a deduction fact to K is the rule (VECT-ADD-CONSEQ); in particular this gives $\psi \in F$. The added deduction facts are of the form $\xi \vdash^? u$ where, for some $(\mathcal{P}, C, C^e) \in \Gamma$, $\xi \vdash^? u \in F(C^e)$ and $(\zeta, u) \notin \text{Conseq}(K(C^e) \cup D(C^e))$ for any recipe $\zeta$. The fact that $\xi \vdash^? u \in F(C^e)$
and $\text{Inv}_{wf}(\Gamma)$ (property 5) justify that $st(\xi) \subseteq \text{Conseq}(K \cup D)$; this justifies that $u \in st(\Phi)$ as well when taking into account that $u$ is not a consequence of $D(C^e)$ (in particular it cannot be a ground constructor term without names otherwise it would even be consequence of the empty set). Finally the property $u \notin \mathcal{X}^1$ also follows from $(\zeta, u)$ not being a consequence of $D(C^e)$.

► *property 5 (Shape of F):* For all $H \Leftarrow \varphi \in F(C^{e'})$, $\varphi$ only contains syntactic equations as hypothesis, i.e. no deduction facts. Moreover $sst^2(H) \subseteq \text{Conseq}(K \cup D)$, and if $H = \xi \vdash^? u$ then either $u \in st(\Phi)$ or there exists a recipe $\zeta$ such that $(\zeta, u) \in \text{Conseq}(K \cup D)$.

The property that the hypotheses of the formula only contain syntactic equations can be obtained by a straightforward inspection of each case-distinction and simplification rules. Note in particular that whenever a formula $\psi$ with deduction-fact hypotheses is considered (in Rules (REW) and (EQ)), they are applied to a substitution $\Sigma$ so that $\psi:(\Sigma, C^e)$ only has equations as hypotheses. As for the second part of property 5 we write 1. the property $sst^2(H) \subseteq \text{Conseq}(K \cup D)$ and 2. the rest (the property about the head terms of deduction formulas). We perform a case analysis on the rule that added the formula to $\Gamma'$.

- rule (VECT-ADD-FORMULA): the proof of 2 directly follows from $\text{Inv}_{wf}(\Gamma)$ since the rule does not add a deduction formula. Regarding 1, using the notations of the rule, the head of the formula is $\xi =_f^? \zeta$ where $\xi \vdash^? u \in F$ for some $u$, and $\zeta \in \text{Conseq}(K \cup D)$. In particular the conclusion follows from $\text{Inv}_{wf}(\Gamma)$ (property 4 for the subterms of $\xi$ and property 5 for the subterms of $\zeta$)

- rule (REW): we first prove 1. Using the notations of the rule, all non-root positions of the head of a formula of $F_0$ are either variables $X$ such that $D$ contains a deduction fact $X \vdash^? x$ (generated by the skeleton), a position of $\xi_0$, or a public function symbol (since the rewriting system is constructor, the left-hand sides $\ell$ of the rewrite rules only contain a destructor at their roots). In particular all strict subterms of $H$ are consequences of $K \cup D$. Now let us prove 2. By definition of the rule, $u$ is a constructor term in normal form obtained after applying one rewrite rule $\ell \to r$ at the root of $C[u_0]$ for some context $C$ (not containing names but possibly containing variables $x$ such that $X \vdash^? x \in D$ for some $X$). We recall that the rewriting system is constructor-destructor and subterm convergent, which leaves two cases. The first is that $r$ is a ground constructor term, and then $u = r$ is trivially a consequence of $K \cup D$ for the recipe $\zeta = r$. Otherwise $r$ is a subterm of $\ell$, meaning that $u$ is a subterm of $C[u_0]$. This implies that $u$ is either a subterm of $u_0$, a subterm of the context $C$, or a term of the form $C'[u_0]$ for some subcontext $C'$ of $C$. In all cases, since $u_0 \in st(\Phi)$ by $\text{Inv}_{wf}(\Gamma)$ (property 4), this gives the expected conclusion.

- rule (EQ): the proof of 2 follows from $\text{Inv}_{wf}(\Gamma)$ since the rule does not add a deduction formula. Regarding 1, this follows from $\text{Inv}_{wf}(\Gamma)$ (property 4). ■
**PROOF.** (Preservation of $Inv_{sound}$.) Let $C' = (\Phi, D, E^1, E^2, K, F)$ for some $(\mathcal{P}', C', C^{e'}) \in \Gamma', \psi \in K \cup F$, and $(\Sigma, \sigma)$ such that

$$ (\Phi, \Sigma, \sigma) \models \bigwedge_{\substack{\psi' \in D \\ \mathrm{vars}^2(\psi') \subseteq \mathrm{vars}^2(\psi)}} \psi' \wedge E_{\models}^1 $$

We have to prove that $(\Phi, \Sigma, \sigma) \models \psi$. Here we prove more precisely that the conclusion holds when applying one time any of the case-distinction or simplification rules. First of all we observe that this property is preserved by the application of a mgs to an extended constraint system. In particular this makes the conclusion immediate for all rules except the following:

- Rule (REW) (positive branch): using the notations of the rule and recalling $Inv_{sound}(\Gamma)$, the conclusion follows from the fact that if $\xi_0 \Sigma \Phi \sigma \downarrow = u_0 \downarrow$, $\ell \to r \in \mathcal{R}$ and $C[u] = \ell \sigma'$ for some substitution $\sigma'$, then $C[\xi_0] \Sigma \Phi \sigma \downarrow = r \sigma' \downarrow$.

- Rule (EQ) (positive branch): using the notations of the rule and recalling $Inv_{sound}(\Gamma)$, if $\psi$ is the formula added to F by this rule, we have $(\Phi, \Sigma, \sigma) \models \psi$ iff for some recipes $\xi_1, \xi_2$, if $\xi_1 \Sigma \Phi \sigma \downarrow = z$ and $\xi_2 \Sigma \Phi \sigma \downarrow = z$ then $\xi_1 \Sigma \Phi \sigma \downarrow = \xi_2 \Sigma \Phi \sigma \downarrow$. This naturally holds.

- Rule (VECT-ADD-CONSEQ): since the element added to K is originated from F, the conclusion follows from $Inv_{sound}(\Gamma)$.

- Rule (VECT-ADD-FORMULA): the reasoning is identical to the one for (EQ).

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

**PROOF.** (Preservation of $Inv_{comp}$.) Let $C_1^{e'}, C_2^{e'}$ for some $(\mathcal{P}'_1, C'_1, C_1^{e'})$, $(\mathcal{P}'_2, C'_2, C_2^{e'}) \in \Gamma', \psi = H \Leftarrow \varphi \in F(C_1^{e'})$ and $(\Sigma, \sigma) \in \mathrm{Sol}(C_2^{e'})$. We assume that $(\Phi(C_2^{e'}), \Sigma, \sigma)$ weakly satisfies H. We want to prove that there exists $\psi' = (H' \Leftarrow \varphi') \in F(C_2^{e'})$ such that $H' \simeq_r H$ and $(\Phi(C_2^{e'}), \Sigma, \sigma) \models \varphi'$. We prove the strengthened property stating that the invariant is preserved after the application of each case-distinction and simplification rules.

- Rules (NORM-UNIF), (NORM-NO-MGS), (NORM-DISEQ): the conclusion directly follows from $Inv_{comp}(\Gamma)$.

- Rule (NORM-FORMULA): by $Inv_{comp}(\Gamma)$ we let $\psi'_0 = (H'_0 \Leftarrow \varphi'_0) \in F(C_2^e)$ such that $H'_0 \simeq_r H$ and $(\Phi(C_2^e), \Sigma, \sigma) \models \varphi'_0$. The conclusion directly follows from this, except if $\psi'_0$ is the formula removed by the rule, i.e. if mgs$(C_2^e[E^1 \mapsto E^1 \wedge \varphi'_0]) = \emptyset$. However this would yield a contradiction with $(\Phi(C_2^e), \Sigma, \sigma) \models \varphi'_0$, hence the conclusion.

- Rule (NORM-DUPL): using the same notations as in the previous case, we let $\psi'_0$ by $Inv_{comp}(\Gamma)$ and the only non-trivial case is again the one where $\psi'_0$ is removed from $C_2^e$ by the rule. This means that there exists $\psi' \in F(C_2^{e'})$ solved such that $\psi' \simeq_r H'_0$, hence the conclusion since $\mathrm{hyp}(\psi') = \top$ and $H'_0 \simeq_r H$.

- Rules (VECT-RM-UNSAT) and (VECT-SPLIT): the conclusion follows from the $Inv_{comp}(\Gamma)$ since $\Gamma' \subseteq \Gamma$.

- Rule (VECT-ADD-CONSEQ): directly follows from $Inv_{comp}(\Gamma)$.
— Rule (VECT-ADD-FORMULA): Let us write

$$ \Gamma' = \{(\mathcal{P}, C, C^e [F \mapsto F \wedge \psi:(\Sigma, C^e)]) \mid (\mathcal{P}, C, C^e) \in \Gamma\} $$

with the notations and assumptions of the rule. If $i \in \{1, 2\}$ we write $S_i = (\mathcal{P}, C, C_i^e)$. The only case that does not directly follows from $\mathrm{Inv}_{\mathrm{comp}}(\Gamma)$ is the case where $\psi = \psi:(\Sigma, C_1^e)$. But since there exists a formula $\xi \vdash? u_{S_2} \in F(C_2^e)$ by hypothesis, we know by $\mathrm{Inv}_{\mathrm{sound}}(\Gamma)$ that $\xi\Phi(C_2^e)\Sigma\sigma_2\downarrow = u_{S_2}$. In particular since $(\Phi(C_2^e), \Sigma, \sigma_2)$ weakly satisfies $\xi =?_f \zeta$, we can write $u'_{S_2} = \zeta\Sigma\Phi(C_2^e)\sigma_i\downarrow$ and have $u_{S_2} = u_{S_2'}$. Since we also have by definition (after formula normalisation, see Figure 7)

$$ \psi:(\Sigma, C_2^e) = (\xi =?_f \zeta \Leftarrow u_{S_2} =? u_{S_2'}) $$

we obtain the expected conclusion.

— Any case-distinction rule (negative branch) or Rule (SAT): follows from $\mathrm{Inv}_{\mathrm{comp}}(\Gamma)$.

— Rule (REW) (positive branch): using the notations of the rule, the only case that does not directly follow from the assumption $\mathrm{Inv}_{\mathrm{comp}}(\Gamma)$ is the case where $\psi \in F_0$. The hypothesis $(\Phi(C_2^e), \Sigma, \sigma)$ weakly models the head of $\psi$ can then be rephrased as $\mathrm{msg}(\xi'\Sigma\Phi(C_2^e)\sigma)$ for some recipe $\xi' = C[\xi_0]$ such that $\mathrm{root}(C) \in \mathcal{F}_d$, by definition of $F_0$. Let us write $u = \xi_0\Sigma\Phi(C_2^e)\sigma\downarrow$. Since the rewriting system is constructor-destructor and $\mathrm{root}(C[u]) \in \mathcal{F}_d$, there exists at least one rewrite rule $\ell' \to r' \in \mathcal{R}$ such that $C[u]$ and $\ell'$ are unifiable. In particular it sufficies to choose $\psi'$ the formula of $F_0$ corresponding to picking this rule in the definition of $\mathrm{RewF}(\xi, \ell \to r, p)$.

— Rule (EQ) (positive branch): easily follows from $\mathrm{Inv}_{\mathrm{comp}}(\Gamma)$ since the rule only adds to each $(\mathcal{P}, C, C^e) \in \Gamma$ the same solved formula. ■

**PROOF.** (Preservation of $\mathrm{Inv}_{\mathrm{satur}}$.) Let $C' = (\Phi, D, E^1, E^2, K, F)$ for some $(\mathcal{P}', C', C^{e'}) \in \Gamma'$ and $k$ such that $\mathrm{vars}^2(D(C)) \subseteq \mathcal{X}_{\leq k}^2$. We also let $f/n \in \mathcal{F}_d$ and $(\xi_1, u_1), \dots, (\xi_n, u_n) \in \mathrm{Conseq}(K(C))$ such that $\xi_1, \dots, \xi_n \in \mathcal{T}_k^2$, and $f(u_1, \dots, u_n)\downarrow$ is a constructor term. We have to prove that there is $\xi \in \mathcal{T}_k^2$ such that $(\xi, f(u_1, \dots, u_n)\downarrow) \in \mathrm{Conseq}(K(C) \cup D(C))$. This can be justified by $\mathrm{Inv}_{\mathrm{wf}}(\Gamma)$ (in particular the item “shape of K”). Indeed, by definition the term $f(u_1, \dots, u_n)$ contains a single destructor, which is the symbol $f$ at its root. In particular if $f(u_1, \dots, u_n)\downarrow$ is indeed a constructor protocol term $u$, this has been obtained after applying a single rewriting rule at the root of $f(u_1, \dots, u_n)$ since the rewriting system is constructor-destructor. Therefore, by subterm convergence, $u$ is either a ground protocol term (without names, by definition of a rewrite rule) or a subterm of one of the $u_i$s. In the former case the conclusion is immediate, in the latter it follows from the invariant $\mathrm{Inv}_{\mathrm{wf}}$. ■

**PROOF.** (Preservation of $\mathrm{Inv}_{\mathrm{sol}}$.) The preservation of this invariant is straightforward: the case distinction and simplification rules only modify the extended constraint systems by 1. applying
a mgs, or 2. adding formulas to $E^1$, $E^2$, K,..., or 3. removing formulas from F, or 4. removing trivially-false disequations from $E^1$. In particular such operations restrict the set of solutions. ■

We can then extend this property to the whole procedure by proving the preservation by symbolic rules.

**LEMMA B.8.** Let $\Gamma$ be a set of extended symbolic processes such that $\text{Inv}_{\text{all}}(\{\Gamma\})$. We assume that no case-distinction or simplification rules can be applied to $\Gamma$. We then let

$$ \Gamma_{\text{in}} = \{(\mathcal{P}', C', C^{e'}) \mid (\mathcal{P}, C, C^e) \in \Gamma, (\mathcal{P}, C, C^e) \underset{s}{\overset{Y(X)}{\rightleftharpoons}} (\mathcal{P}', C', C^{e'})\} \\ \Gamma_{\text{out}} = \{(\mathcal{P}', C', C^{e'}) \mid (\mathcal{P}, C, C^e) \in \Gamma, (\mathcal{P}, C, C^e) \underset{s}{\overset{\bar{Z}\langle\text{ax}_{|\Phi(C^e)|+1}\rangle}{\rightleftharpoons}} (\mathcal{P}', C', C^{e'})\} $$

and the set of set of symbolic processes $\mathcal{S}$ obtained by normalising $\{\Gamma_{\text{in}}, \Gamma_{\text{out}}\}$ with the simplification rules. Then $\text{Inv}_{\text{all}}(\mathcal{S})$.

**PROOF.** Most invariants are either easily seen to be preserved by application of any symbolic or simplification rules, or are a straightforward consequence of the fact that no simplification rules can be applied to $\mathcal{S}$. The only substantial case is the Invariant 4 stating that the knowledge base is saturated. Let us then consider $(\mathcal{P}, C, C^e) \in \Gamma'$ for some $\Gamma' \in \mathcal{S}$ and we let $k$ the minimal index such that $\text{vars}^2(\text{D}(C)) \subseteq \mathcal{X}_{\le k}^2$. We then let $f/n \in \mathcal{F}_d$ and $(\xi_1, u_1), \dots, (\xi_n, u_n) \in \text{Conseq}(\mathcal{K}(C^e))$ such that $u\downarrow$, with $u = f(u_1, \dots, u_n)$ is a constructor term. We recall that no case-distinction rules can be applied to $\{\Gamma\}$, in particular (REW). But since the rewriting system is constructor-destructor, $f \in \mathcal{F}_d$, and $u\downarrow$ is a constructor term, this means that a rewrite rule is applicable at the root of $u$. We distinguish two cases.

► **case 1:** there exists a rule $\ell \to r$ applicable at the root of $u$, $i \in [1, n]$ and $p$ a position such that $\ell_{i \cdot p} \notin \mathcal{X}^1$ and $(\xi_{i \mid p} \vdash^? v) \in \mathcal{K}(C^e)$ for some $v$.

We consider the instance of Rule (REW) with the following parameters: the position $i \cdot p$, the rule $\ell \to r$, a recipe $\xi \in \mathcal{T}(\mathcal{F}, \mathcal{X}:|\Phi(C^e)|)$, the formula $\psi_0$ obtained by considering the rule $\ell \to r$ in RewF($\xi, \ell \to r, i \cdot p$), the deduction fact $\xi_{i \mid p} \vdash^? v$, $\Sigma_0 = \{\xi_{i \cdot p} \mapsto \xi_{i \mid p}\}$, and a mgs $\Sigma$ such that the head of $\psi_0:(\Sigma_0\Sigma, C^e:\Sigma)$ is of the form $\zeta \vdash^? u\downarrow$ for some recipe $\zeta$. Since this instance of the rule is not applicable by hypothesis, we deduce that there already exists a solved formula $\psi \in \text{F}(C^e)$ of the form $\zeta' \vdash^? u\downarrow$. Since no simplification rules are applicable neither, in particular (VECT-ADD-CONSEQ), we deduce that there exists a recipe $\xi'$ such that $(\xi', u\downarrow) \in \text{Conseq}(\mathcal{K}(C^e) \cup \text{D}(C^e))$.

► **case 2:** otherwise

We let $\ell \to r$ an arbitrary rewrite rule applicable at the root of $u$. By hypothesis for all positions $i \cdot p$ of $\ell$ that are not variables we know that $\xi_{i \mid p}$ is not the recipe of a deduction fact from $\mathcal{K}(C^e)$; since $\xi_i \in \text{Conseq}(\mathcal{K}(C^e))$, $\text{root}(\xi_{i \mid p})$ is therefore a constructor symbol. We rule
out the immediate case where $r$ is a ground term and only consider the one where $r$ is a strict subterm of $l$. Then, since the rewriting system is constructor-destructor, we can fix a ground constructor context $C$ such that $r = C[x_p, \dots, x_q]$ for $x_p, \dots, x_p$ the variables numbered $p$ to $q$ of $l$ (w.r.t. the lexicographic ordering on the positions of the term $l$). In particular the recipe $(C[\xi_p, \dots, \xi_q], u \downarrow) \in \text{Conseq}(K(C^e))$. ■

## B.3 Preliminary technical results

In this section we prove some low level technical results that will be useful during the incoming proofs.

**Preservation by application of substitutions** In this section, we show that applying substitution preserves in some cases the different notions we use in our algorithms, namely first-order and second-order equations, deduction and equality facts; and uniformity.

**LEMMA B.9.** Let $\psi$ be either a deduction fact, or an equality fact or a first-order equation or a second-order equation. For all ground frame $\Phi$, for all substitutions $\Sigma, \Sigma', \sigma, \sigma'$ if $dom(\Sigma) \cap dom(\Sigma') = \emptyset$ and $dom(\sigma) \cap dom(\sigma') = \emptyset$ then $(\Phi, \Sigma\Sigma', \sigma\sigma') \models \psi$ is equivalent to $(\Phi, \Sigma\Sigma', \sigma\sigma') \models \psi\Sigma\sigma$ and is equivalent to $(\Phi, \Sigma', \sigma') \models \psi\Sigma\sigma$.

**PROOF.** The proof of this lemma is done by case analysis on $\psi$.

**Case $u =? v$:** Consider $(\Phi, \Sigma\Sigma', \sigma\sigma') \models u =? v$. This is equivalent to $u\sigma\sigma' = v\sigma\sigma'$. Since $vars(\Sigma) \cap \chi^1 = \emptyset$, we deduce that $(\Phi, \Sigma\Sigma', \sigma\sigma') \models u =? v$ is equivalent to $u\Sigma\sigma\sigma' = v\Sigma\sigma\sigma'$. This is also equivalent to $u\Sigma\sigma\sigma\sigma' = v\Sigma\sigma\sigma\sigma'$ and so $(\Phi, \Sigma\Sigma', \sigma\sigma') \models u\Sigma\sigma =? v\Sigma\sigma$. Note that $u\Sigma\sigma\sigma' = v\Sigma\sigma\sigma'$ is also equivalent to $(\Phi, \Sigma', \sigma') \models u\Sigma\sigma =? v\Sigma\sigma$.

**Case $\xi =? \xi'$:** Similar to the previous case.

**Case $\xi \vdash? u$:** Consider $(\Phi, \Sigma\Sigma', \sigma\sigma') \models \xi \vdash? u$. It is equivalent to $\xi\Sigma\Sigma'\Phi \downarrow = u\sigma\sigma'$ and $msg(\xi\Sigma\Sigma'\Phi)$. But $(\xi \vdash? u)\Sigma\sigma = \xi\Sigma \vdash? u\sigma$. Moreover, by definition of substitution (in particular the acyclic property), we deduce that $\xi\Sigma\Sigma'\Phi = \xi\Sigma\Sigma\Sigma'\Phi$ and $u\sigma\sigma' = u\sigma\sigma\sigma'$. Hence, $msg(\xi\Sigma\Sigma'\Phi)$ is equivalent to $msg(\xi\Sigma\Sigma\Sigma'\Phi)$; and $\xi\Sigma\Sigma'\Phi \downarrow = u\sigma\sigma'$ is equivalent to $\xi\Sigma\Sigma\Sigma'\Phi \downarrow = u\sigma\sigma\sigma'$. Hence $(\Phi, \Sigma\Sigma', \sigma\sigma') \models \xi \vdash? u$ is equivalent to $(\Phi, \Sigma\Sigma', \sigma\sigma') \models \xi \vdash? u\Sigma\sigma$. Note that $msg(\xi\Sigma\Sigma'\Phi)$ and $\xi\Sigma\Sigma'\Phi \downarrow = u\sigma\sigma'$ are also equivalent to $(\Phi, \Sigma', \sigma') \models \xi\Sigma \vdash? u\sigma$.

**Case $\xi =?_f \xi'$:** Similar to previous case. ■

**Properties on consequence of set of deduction facts** This section contains some results about the consequence relation when modifying a set of deduction facts. The first lemma is about the application of substitutions.

**LEMMA B.10.** Let $S$ be a set of solved deduction facts. For all substitutions $\sigma$ of protocol terms, for all $(\xi, t) \in \text{Conseq}(S)$, $(\xi, t\sigma) \in \text{Conseq}(S\sigma)$.
**PROOF.** We know that $(\xi, t) \in \text{Conseq}(S)$ implies $\xi = C[\xi_1, \dots, \xi_n]$ and $t = C[t_1, \dots, t_n]$ for some public context $C$ and for all $i$, $(\xi_i \vdash^? t_i \in S$. Hence $(\xi_i \vdash^? t_i \sigma \in S\sigma$ which allows us to conclude. ■

**PROPOSITION B.11 (transitivity of consequences).** Let $S, S'$ be two sets of solved deduction facts. Let $\varphi = \{X_i \vdash^? u_i\}_{i=1}^n$ such that all $X_i$ are pairwise distinct, let $(\xi, t) \in \text{Conseq}(S \cup \varphi)$ and $\Sigma, \sigma$ be two substitutions. If for all $i \in [1, n]$, $(X_i\Sigma, u_i\sigma) \in \text{Conseq}(S\Sigma\sigma \cup S')$ then $(\xi\Sigma, t\sigma) \in \text{Conseq}(S\Sigma\sigma \cup S')$.

**PROOF.** We prove this result by induction on $|\xi|$. The base case ($|\xi| = 0$) is trivial as there are no terms of size 0 and we hence focus on the inductive step. We perform a case analysis on the hypothesis $(\xi, t) \in \text{Conseq}(S \cup \varphi)$.

► case 1: $\xi = t \in \mathcal{F}_0$

We directly have by definition that $(\xi\Sigma, t\sigma) \in \text{Conseq}(S\Sigma\sigma \cup S')$.

► case 2: there are $\xi_1, t_1, \dots, t_m, \xi_m$ and $f \in \mathcal{F}_c$ such that $\xi = f(\xi_1, \dots, \xi_m)$, $t = f(t_1, \dots, t_m)$ and for all $i \in [1, m]$, $(\xi_i, t_i) \in \text{Conseq}(S \cup \varphi)$

By induction hypothesis we know that for all $j \in [1, m]$, $(\xi_j\Sigma, t_j\sigma) \in \text{Conseq}(S\Sigma\sigma \cup S')$. Writing $\xi\Sigma = f(\xi_1\Sigma, \dots, \xi_m\Sigma)$ and $t\sigma = f(t_1\sigma, \dots, t_m\sigma)$, we conclude that $(\xi\Sigma, t\sigma) \in \text{Conseq}(S\Sigma\sigma \cup S')$.

► case 3: $\xi \vdash^? t \in S \cup \varphi$

If $(\xi \vdash^? t) \in S$ then $(\xi\Sigma \vdash^? t\sigma) \in S\Sigma\sigma$ and the result directly holds. Otherwise $\xi \vdash^? t \in \varphi$ and hence by hypothesis $(\xi\Sigma, t\sigma) \in \text{Conseq}(S\Sigma\sigma \cup S')$. ■

The previous lemma showed that a consequence $(\xi, t)$ is preserved when applying some substitution $\Sigma, \sigma$ under the right conditions. However, it is quite strong since we ensure that $\xi\Sigma$ is consequence with $t\sigma$. In some cases, we cannot guarantee that $\xi\Sigma$ is consequence with $t\sigma$ but with some other first-order term. This is the purpose of the next lemma.

**LEMMA B.12.** Let $S, S'$ be two sets of solved deduction facts. Let $\varphi = \{X_i \vdash^? u_i\}_{i=1}^n$ such that all $X_i$ are pairwise distinct. For all $\Sigma$, for all $\xi \in \text{Conseq}(S \cup \varphi)$, if for all $i \in \{1, \dots, n\}$, $X_i\Sigma \in \text{Conseq}(S\Sigma \cup S')$ then $\xi\Sigma \in \text{Conseq}(S\Sigma \cup S')$.

**PROOF.** We prove this result by induction on $|\xi|$. The base case ($|\xi| = 0$) being trivial as there is no term of size 0, we focus on the inductive step.

Since $\xi$ is consequence of $S \cup \varphi$, we know by definition that there exists $t$ such that one of the following conditions hold:

1. $\xi = t \in \mathcal{F}_0$

2. there exists $\xi_1, t_1, \dots, t_m, \xi_m$ and $f \in \mathcal{F}_c$ such that $\xi = f(\xi_1, \dots, \xi_m)$, $t = f(t_1, \dots, t_m)$ and for all $i \in \{1, \dots, m\}$, $(\xi_i, t_i)$ is consequence of $S \cup \varphi$.
3. there exists $t$ such that $\xi \vdash^? t \in S \cup \varphi$.

In case 1, we directly have by definition that $(\xi\Sigma, t)$ is a consequence of $S\Sigma \cup S'$. In case 2, by our inductive hypothesis on $\xi_1, \dots, \xi_m$, we have that for all $j \in \{1, \dots, m\}$, $\xi_j\Sigma$ is a consequence of $S\Sigma \cup S'$ hence there exists $t'_1, \dots, t'_m$ such that for all $j \in \{1, \dots, m\}$, $(\xi_j\Sigma, t'_j)$ is a consequence of $S\Sigma \cup S'$. With $\xi\Sigma = f(\xi_1\Sigma, \dots, \xi_m\Sigma)$ and $t' = f(t'_1, \dots, t'_m)$, we conclude that $(\xi\Sigma, t')$ is consequence of $S\Sigma \cup S'$. In case 3, if $\xi \vdash^? t \in S$ then $\xi\Sigma \vdash^? t \in S\Sigma$ and so the result directly holds. Else $\xi \vdash^? t \in \varphi$ and so by hypothesis $\xi\Sigma \in \text{Conseq}(S\Sigma \cup S')$. ■

In the next lemma, we show that when a recipe is consequence of the sets of solved deduction formulas $\mathbf{K}\Sigma\sigma$ where $(\Sigma, \sigma)$ is a solution of the constraint system, then all subterms of that recipe are also consequence of $\mathbf{K}\Sigma\sigma$. This property is in fact guaranteed by the fact that $\mathbf{K}$ contains itself recipes consequence of itself. This is an important property that allows us to generate solutions that satisfy the uniformity property.

**LEMMA B.13.** Let $C = (\Phi, D, E^1, E^2, K, F)$ be an extended constraint system such that $\text{Inv}_{wf}(C)$. For all $\xi \in \text{Conseq}(K \cup D)$, $\text{st}(\xi) \subseteq \text{Conseq}(K \cup D)$.

**PROOF.** Since $\xi \in \text{Conseq}(K \cup D)$, we know that $\xi = C[\xi_1, \dots, \xi_n]$ where $C$ is a public context and $\xi_1, \dots, \xi_n$ are recipes of deduction facts from $K$ or $D$. Hence since $\xi' \in \text{st}(\xi)$, we have that the position $p$ of $\xi'$ in $\xi$ is either a position of $C$ thus $\xi' \in \text{Conseq}(K \cup D)$ from the definition of consequence; or is a position of one of the $\xi_i$ and thus we conclude by the predicate $\text{Inv}_{wf}(C)$. ■

**LEMMA B.14.** Let $C = (\Phi, D, E^1, E^2, K, F)$ be an extended constraint system such that $\text{Inv}_{wf}(C)$. For all $(\Sigma, \sigma) \in \text{Sol}(C)$, for all $\xi \in \text{Conseq}(\mathbf{K}\Sigma\sigma)$, $\text{st}(\xi) \subseteq \text{Conseq}(\mathbf{K}\Sigma\sigma)$.

**LEMMA B.15.** Let $S$ be a set of ground deduction facts. Let $\Phi$ be a ground frame. Assume that for all $\psi \in S$, $\Phi \models \psi$. For all $(\xi, t) \in \text{Conseq}(S)$, $\Phi \models \xi \vdash^? t$.

**PROOF.** We prove this result by induction on $|\xi|$. The base case being trivial, we focus on the inductive step. Since $(\xi, t)$ is consequence of $S$ then one of the following properties holds:

1. $\xi = t \in \mathcal{F}_0$

2. there exist $\xi_1, t_1, \dots, \xi_n, t_n$ and $f \in \mathcal{F}_c$ such that $\xi = f(\xi_1, \dots, \xi_n)$, $t = f(t_1, \dots, t_n)$ and for all $i \in \{1, \dots, n\}$, $(\xi_i, t_i)$ is consequence of $S$

3. $\xi \vdash^? t \in S$.

In Case 1, the result trivially holds. In case two, a simple induction on $(\xi_1, t_1), \dots, (\xi_n, t_n)$ allows us to conclude. In case 3, we know by hypothesis that $\Phi \models \xi \vdash^? t$ hence the result holds

## B.4 Correctness of most general solutions

In this section we prove the correctness of the constraint solving procedure for computing mgs' in Section 4.2. We show that given an extended constraint system $C$, the Rules (MGS-CONSEQ),
(MGS-RES), (MGS-CONS), (MGS-UNSAT), and (MGS-UNIF) allow to compute the most general solutions of C.

**LEMMA B.16.** Let C be an extended constraint system such that $\text{Inv}_{\text{wf}}(C)$ and $\text{Inv}_{\text{sound}}(C)$. If any rule is applicable on C then for all $(\Sigma, \sigma) \in \text{Sol}(C)$, there exists C', $\Sigma'$ such that $C \Rightarrow \Sigma' C'$ and $(\Sigma\Sigma', \sigma) \in \text{Sol}(C')$.

**PROOF.** First, assume that there exist $\xi, \zeta \in R(C)^2$ and $u$ such that $\xi \neq \zeta$ and $(\xi, u), (\zeta, u) \in \text{Conseq}(K \cup D)$. By $\text{Inv}_{\text{sound}}(C)$ and Lemmas B.15 and Proposition B.11, we deduce that $\Phi\sigma \models \xi\Sigma \vdash^? u\sigma \wedge \zeta\Sigma \vdash^? u\sigma$. As such we have $\xi\Sigma\downarrow = u\sigma = \zeta\Sigma\downarrow$. However by definition of a solution it implies that $\xi\Sigma = \zeta\Sigma$. Thus there exists $\Sigma' = \text{mgu}(\xi =? \zeta)$ such that $\Sigma' \neq \emptyset$ and $\Sigma' \neq \bot$.

In such a case, let us show that $(\Sigma, \sigma) \in \text{Sol}(C')$ with $C \to C'$ by Rule (MGS-CONSEQ). We already know that $\Sigma \models E^2(C)$ and since $\xi\Sigma = \zeta\Sigma$ with $\Sigma' = \text{mgu}(\xi =? \zeta)$, we directly have that $\Sigma \models E^2(C)\Sigma' \wedge \Sigma'$. Moreover, $K(C)\Sigma = K(C)\Sigma'\Sigma$. Hence, the two bullets of the definition of solutions is trivially satisfied by that fact that $(\Sigma, \sigma) \in \text{Sol}(C)$. Therefore, we conclude that $(\Sigma, \sigma) \in \text{Sol}(C')$.

Let us now consider the case where our assumption do not hold. Thus since we assume that at least one rule is applicable on C, there exists $X \vdash^? u \in D(C)$ where $u \notin \mathcal{X}^1$. Let us do a case analysis on $X\Sigma$ since $X\Sigma \in \text{Conseq}(K\Sigma\sigma)$ by definition of a solution.

- either $X\Sigma \in \mathcal{F}_0$: in such a case, we have $C \to C'$ by Rule (MGS-CONSEQ) and we can prove similarly as in the previous case that $(\Sigma, \sigma) \in \text{Sol}(C')$;

- or $X\Sigma = f(\xi_1, \dots, \xi_n)$ where $\xi_i \in \text{Conseq}(K\Sigma\sigma)$ for all $i$: note that we know that $X\Sigma\Phi\sigma\downarrow = u\sigma$. Hence $u = f(u_1, \dots, u_n)$ for some $u_1, \dots, u_n$. We deduce that for all $i$, $\Phi\sigma \models \xi_i \vdash^? u_i\sigma$. Thus, by considering $\Sigma' = \{X_i \mapsto \xi_i\}_{i=1}^n$, we can conclude that $C \to C'$ by Rule (MGS-CONS) and $(\Sigma\Sigma', \sigma) \in \text{Sol}(C')$;

- or $X\Sigma \vdash^? u\sigma \in K\Sigma\sigma$ (since once again $X\Sigma\Phi\sigma\downarrow = u\sigma$): thus there exists $\xi \vdash^? v \in K$ such that $\xi\Sigma = X\Sigma$ and $u\sigma = v\sigma$. Hence $\text{mgu}\xi X$ exists and $\sigma \models u =? v$. Therefore, we can conclude that $C \to C'$ by Rule (MGS-RES) and $(\Sigma, \sigma) \in \text{Sol}(C')$. $\blacksquare$

**LEMMA B.17.** Let $C \neq \bot$ be an extended constraint system such that $C\xi = C$, $\text{Inv}_{\text{wf}}(C)$ and $\text{Inv}_{\text{sound}}(C)$. If $C \to \xi$ and $C$ is a solved extended constraint system then $\text{mgs}(C) = \{\text{mgu}(E^2)\}$.

**PROOF.** We know that for all $(\Sigma, \sigma) \in \text{Sol}(C)$, $\Sigma \models E^2(C)$ thus we directly obtain the existence of $\Sigma'$ such that $\Sigma = \text{mgu}(E^2)\Sigma'$. Consider now the second bullet point of the definition of most general solutions. We know that C is solved. Hence consider a fresh bijective renaming $\Sigma_1$ from $\text{vars}^2(\Sigma_0) \cup \text{vars}^2(C) \setminus \text{dom}(\Sigma_0)$ to $\mathcal{F}_0$. Let us define $\sigma_1 = \{x \mapsto X\Sigma_1 \mid x \vdash^? xD(C)\}$. Thanks to $\text{Inv}_{\text{wf}}(C)$, $\text{Inv}_{\text{sound}}(C)$ and Lemma B.14, B.12, and B.15 that $(\Phi\text{mgu}(E^1(C))\sigma_1, \text{mgu}(E^2)\Sigma_1, \text{mgu}(E^1(C))\sigma_1) \models D \wedge E^1 \wedge E^2$. Moreover, by Lemma B.14, we know that the first bullet of the definition of solution is satisfied. Finally, the second bullet is satisfied.
isfied otherwise Rule (MGS-UNSAT) would be applicable which contradict $C \not\approx = C$. Therefore, $(mgu(E^2)\Sigma_1, mgu(E^1(C))\sigma_1) \in \text{Sol}(C)$. We conclude that $mgs(C) = \{mgu(E^2)\}$. ■

**LEMMA B.18.** Let $C$ an extended constraint system such that $C \not\approx = C$, $\text{Inv}_{wf}(C)$ and $\text{Inv}_{sound}(C)$. If $C \to \not\approx$ and $C$ is not solved then $\text{Sol}(C) = \emptyset$.

**PROOF.** Since $C$ is not solved, we have two possibilities: Either (a) all deduction facts in $D$ are have variables as right hand term but not pairwise distinct. But in such a case Rule (MGS-CONSEQ) would be applicable which contradicts $C \to \not\approx$; or (b) there exists $(X \vdash^? u) \in D(C)$ such that $u \notin \mathcal{X}^1$. Since Rule (MGS-CONSEQ) is not applicable, we deduce that $u \notin \mathcal{F}_0$ and for all $\xi, \zeta \in R(C) \setminus \{X\}, (\xi, u) \notin \text{Conseq}(K \cup D)$. But rule Rule (MGS-CONS) is not applicable therefore, we deduce that $u \in \mathcal{N}$.

Assume now that $\text{Sol}(C) \neq \emptyset$ and so $(\Sigma, \sigma) \in \text{Sol}(C)$. Thus $X\Sigma\Phi\downarrow = u$. By definition of a solution, we know that $(X\Sigma, u) \in \text{Conseq}(K(C)\Sigma\sigma)$. Since $u \in \mathcal{N}$ it implies that there exists $(\xi \vdash^? v) \in K(C)$ such that $X\Sigma = \xi\Sigma$ and $u = v\sigma$. Note that by $\text{Inv}_{wf}(C)$, we also have that $v \notin \mathcal{X}^1$ and so $u = v$. In such a case, we obtain a contradiction with the fact the Rule (MGS-RES) is not applicable. ■

## B.5 Correctness of the partition tree

In this section we prove the correctness of the procedure generating the partition tree, using the invariants proved in Appendix B.1. Let us first start by noticing that the case distinction rules and simplification rules preserves the first order solutions of the extended constraint systems. This property is stated in the following lemma.

**LEMMA B.19.** Let $\mathcal{S}$ be a set of extended symbolic processes such that $\text{Inv}_{all}(\mathcal{S})$. Let $\mathcal{S} \to \mathcal{S}'$ by applying only case distinction or simplifications rules (i.e. no symbolic transitions). Then:

- Soundness:

for all $S \in \mathcal{S}$, for all $(\mathcal{P}, C, C^e) \in S$, for all $(\Sigma, \sigma) \in \text{Sol}(C^e)$, there exist $S' \in \mathcal{S}'$, $(\mathcal{P}, C, C^{e'}) \in S'$ and $(\Sigma', \sigma') \in \text{Sol}(C^{e'})$ such that $\sigma_{|vars^1(C)} = \sigma'_{|vars^1(C)}$

- Completeness:

for all $S' \in \mathcal{S}$, for all $(\mathcal{P}, C, C^{e'}) \in S'$, for all $(\Sigma', \sigma') \in \text{Sol}(C^{e'})$, there exist $S \in \mathcal{S}$, $(\mathcal{P}, C, C^e) \in S$ and $(\Sigma, \sigma) \in \text{Sol}(C^e)$ such that $\Sigma_{|vars^2(C)} = \Sigma'_{|vars^2(C)}$ and $\sigma_{|vars^1(C)} = \sigma'_{|vars^1(C)}$

**PROOF.** We do a case analysis on the rule applied.

► **case 1:** Normalisation rules (simplification rules of Figure 8)

First, let us notice the result directly hold for Rules NORM-UNIF, NORM-FORMULA, and NORM-DUPL. Indeed, Rule NORM-DISEQ does not modify constraints on recipe and preserves the constraints on protocol terms. Moreover, Rule NORM-FORMULA,NORM-DUPL affect F which
do not impact the solutions of the extended constraint system. For Rule NORM-NO-MGS, since $mgs(C^e) = \emptyset$, we have by definition of most general unifiers that $Sol(C^e) = \emptyset$ (otherwise the first bullet of the definition is contradicted). Hence the result holds since $Sol(\perp) = \emptyset$. Similarly, Rule NORM-FORMULA checks whether the disequations $\forall \tilde{x}.\phi$ is trivially true meaning that the rule preserves the solutions.

### ▶ case 2: Simplification rules on partitions of extended symbolic processes (Figure 9)

The rule VECT-RM-UNSAT only removes an extended symbolic process with an extended constraint systems having no solution hence the result holds. Rule VECT-SPLIT splits a set of $\mathbb{S}$ into two sets thus preserving the extended symbolic processes, and Rule VECT-ADD-FORMULA only adds element in $\mathbb{F}$ which do not impact the solutions of a constraint system. Therefore, for all these rules, the result hold. For Rule VECT-ADD-CONSEQ however, the result is not direct since the rule adds an element in the set $\mathbb{K}$ which has an impact on the solutions of a constraint system. However, we know from the application condition of the rule that the head protocol terms of the deduction facts added in $K_i$ are not consequence of $K_i \cup D_i$. But we also know that $\text{Inv}_{\text{satur}}(\mathbb{S})$ and $\text{Inv}_{\text{wf}}(\mathbb{S})$ hold hence it implies that the recipe $\xi$ (see Figure 9) contains $\text{ax}_{|\Phi_i|}$ and $\text{vars}^2(D_i) \cap \mathcal{X}_{\leq |\Phi_i|}^2 = \emptyset$. Hence, $\xi$ cannot appear in the second order solutions $C_i^e$ which allows us to conclude that the solutions are preserved.

### ▶ case 3: Case distinction rules

The case of case distinction rules is straightforward. Indeed, by definition all rules (SAT), (EQ) and (REW) always refine a set of extended symbolic process $\Gamma$ into $\Gamma_1, \Gamma_2$ where $\Gamma_1$ is obtained by applying a substitution $\Sigma$ to $\Gamma$, and $\Gamma_2$ by adding the constraint $\neg\Sigma$ to $\Gamma$. In particular this refinement preserves the solutions as expected. ■

Now we can show that the static equivalence is preserved by application of the case distinction and simplification rules.

**LEMMA B.20.** Let $\mathbb{S}$ be a set of extended symbolic processes such that $\text{Inv}_{\text{all}}(\mathbb{S})$. Let $\mathbb{S} \to \mathbb{S}'$ by applying only case distinction or simplifications rules (i.e. no symbolic transitions), $\Gamma \in \mathbb{S}$, $(\mathcal{P}_1, C_1, C_1^e), (\mathcal{P}_2, C_2, C_2^e) \in \Gamma$, $(\Sigma, \sigma_1) \in \text{Sol}(C_1^e)$ and $(\Sigma, \sigma_2) \in \text{Sol}(C_2^e)$ such that $\Phi(C_1)\sigma_1 \sim \Phi(C_2)\sigma_2$.

**PROOF.** Once again, let us consider the potential rule applied.

### ▶ case 1: Simplification rules

The only non trivial case is Rule VECT-SPLIT (the other ones do not refine the partition and the conclusion is therefore immediate). However by Lemma applied to $\mathbb{S}$ we know that if a deduction fact occurs in constraint systems $C_1^e$ but no recipe equivalent formula can be found in the constraint system $C_2^e$, then no solution of $C_2^e$ can satisfy the head of the formula.
Besides by $\mathrm{Inv}_{\mathrm{sound}}(\mathbb{S})$ we also know that all solutions of $C_1^e$ satisfy this deduction fact. Then since $(\Sigma, \sigma_1) \in \mathrm{Sol}(C_1^e)$, $(\Sigma, \sigma_2) \in \mathrm{Sol}(C_2^e)$ and $\Phi(C_1)\sigma_1 \sim \Phi(C_2)\sigma_2$, we obtain a contradiction. Therefore, $C_1^e$ and $C_2^e$ are necessarily in the same set of $\mathbb{S}'$.

### ▶ case 2: Case distinction rules

Note that for case distinction rules, the proof is simple since each rule create a partition of the second-order solutions with respect to some mgs $\Sigma_0$. Thus, assume w.l.o.g. that $(\Sigma', \sigma'_1) \in \mathrm{Sol}(C_1^{e'})$.

### ▶ case 2a: negative branch of the rule

First consider that $S'$ corresponds to branch in which we applied $\neg\Sigma_0$. In such a case, since we already know that $\Sigma'$ satisfies $\neg\Sigma_0$ and no other constraint is added, we directly obtain from $(\Sigma, \sigma_2) \in \mathrm{Sol}(C_2^e)$ that $(\Sigma', \sigma'_2) \in \mathrm{Sol}(C_2^{e'})$ (in this case, we even have $\sigma_2 = \sigma'_2$).

### ▶ case 2b: positive branch of the rule

Now consider that $S'$ corresponds to the branch in which we applied $\Sigma_0$. In such a case, the application of $\Sigma_0$ on $C_2^e$ regroups all the solution of $C_2^e$ that satisfies $\Sigma_0$. Since we know that $(\Sigma, \sigma_2) \in \mathrm{Sol}(C_2^e)$ and $\Sigma'_{|\mathrm{vars}^2(C_1)} = \Sigma_{|\mathrm{vars}^2(C_1)}$ which implies $\Sigma'_{|\mathrm{vars}^2(C_2)} = \Sigma_{|\mathrm{vars}^2(C_2)}$, the result holds. ■

The previous two lemmas allow us to obtain the soundness and completeness properties of the partition tree. Note that the monoticity of the second-order predicate is also proved by B.19 (Completeness part) since a solution of a child constraint system is also a solution of parent one. We now need to prove that all nodes of the partition tree are valid configurations. For that we prove properties on extended constraint systems such that no more case distinction rules are applicable.

**LEMMA B.21.** Let $\mathbb{S}$ be a set of sets of extended symbolic processes such that $\mathrm{Inv}_{\mathrm{all}}(\mathbb{S})$ and no instance of the rule (SAT) or normalisation rules (i.e. the simplification rules of Figure 8) are applicable. For all $S \in \mathbb{S}$, for all $(\mathcal{P}, C, C^e) \in S$, writing $C^e = (\Phi, D, E^1, E^2, K, F)$ we have that

1. $C^e$ is solved

2. all formulas $\psi \in F$ are solved

3. $E^1$ does not contain disequations

**PROOF.** First of all the non-applicability of Rule (SAT) case 1 gives that either $C^e$ is solved or $\mathrm{mgs}(C^e) = \emptyset$; due to normalisation rules not being applicable we deduce that $\mathrm{mgs}(C^e) \neq \emptyset$ meaning that $C^e$ is solved. Sinmilarly by the non applicability of case 2 we know that for all $\psi \in F$, either $\psi$ is solved or $\mathrm{mgs}(C^e[E^1 \mapsto E^1 \wedge \mathrm{hyp}(\psi)]) = \emptyset$. But since the normalisation rules are also not applicable, we know that $\mathrm{mgs}(C^e[E^1 \mapsto E^1 \wedge \mathrm{hyp}(\psi)]) \neq \emptyset$: therefore $\psi$ is solved. Finally the non applicability of case 3 and of the normalisation rules also gives us that $E^1$ is only composed of syntactic equations. ■
**LEMMA B.22.** Let $\mathcal{S}$ be a set of sets of extended symbolic processes such that $\text{Inv}_{\text{all}}(\mathcal{S})$ and no instance of the rule (SAT) or normalisation rules are applicable. For all $S \in \mathcal{S}$, for all $(\mathcal{P}, C, C^e) \in S$, $|\text{mgs}(C^e)| = 1$.

**PROOF.** Let us denote $C^e = (\Phi, D, E^1, E^2, K, F)$. By Lemma B.21 we know that $C^e$ is solved, that all formulas $\psi \in F$ are solved, and that $E^1$ only contain equations.

► **Step 1:** Construction of $(\Sigma, \sigma)$ such that $(\Phi, \Sigma, \sigma) \models D \wedge E^1 \wedge E^2$

Since $C^e$ is solved, we deduce that all deduction facts in $D = \{X_i \vdash^? x_i\}_{i=1}^n$ for some $n$ and pairwise distinct $x_i$s and $X_i$s. Consider now the substitutions $\Sigma_0 = \{X_i \rightarrow n_i\}_{i=1}^n$ and $\sigma_0 = \{x_i \rightarrow n_i\}_{i=1}^n$ where the $n_i$s are pairwise distincts public names, i.e. $n_i \in \mathcal{F}_0$. Since no more normalisation rules are applicable, we know that the disequations in $E^2$ not trivially unsatisfiable. Therefore by replacing the free variables of the disequations by names allow us to obtain that $\Sigma_0$ the disequations of $E^2$. By considering $\Sigma = \text{mgu}(E^2)\Sigma'$, we obtain that $\Sigma \models E^2$. Moreover we proved that $E^1$ does not contain any disequations, we directly obtain that $\text{mgu}(E^1)\sigma_0 \models E^1$. Therefore, by defining $\sigma = \text{mgu}(E^1)\sigma_0$, we obtain that $(\Phi, \Sigma, \sigma) \models D \wedge E^1 \wedge E^2$.

► **Step 2:** Proof that $(\Sigma, \sigma)$ is a solution

To prove that $(\Sigma, \sigma)$ is an actual solution of $C^e$ it remains to prove that it verifies the additional required two conditions: K-basis and uniformity. Let us first prove the K-basis, i.e. that for all $\xi \in \text{st}(\text{img}(\Sigma)) \cup \text{sst}^2(\mathcal{K}\Sigma)$, $\text{msg}(\xi\Phi\sigma)$ and $(\xi, \xi\Phi\sigma) \in \text{Conseq}(\mathcal{K}\Sigma\sigma)$. The case $\xi \in \text{sst}^2(\mathcal{K}\Sigma)$ directly follows from $\text{Inv}_{\text{wf}}(C^e)$. Let us therefore consider the case $\xi \in \text{st}(\text{img}(\Sigma))$. Since $\text{Inv}_{\text{wf}}(C^e)$ holds we have that $\text{img}(\text{mgu}(E^2)) \subseteq \text{Conseq}(\mathcal{K} \cup D)$; for the same reason we have that for all $\zeta \vdash^? u \in \mathcal{K}$, $\text{st}(\zeta) \subseteq \text{Conseq}(\mathcal{K} \cup D)$. Therefore by applying Lemma B.12, and by a quick induction on the size of the recipe in $\text{img}(\Sigma)$, we obtain that $\xi \in \text{Conseq}(\mathcal{K}\Sigma)$. Finally, by definition of consequence and since $\text{Inv}_{\text{sound}}(C^e)$ holds, we have $\text{msg}(\xi\Phi\sigma)$ hence the K-basis.

Let us now prove uniformity. We know that $C^e$ is solved which therefore means that for all recipes $\xi, \zeta \in \text{st}_c(\text{img}(\text{mgu}(E^2)), \mathcal{K} \cup D)^2 \cup (\mathcal{F}_0 \times \text{vars}^2(D))$, $(\xi, u), (\zeta, u) \in \text{Conseq}(\mathcal{K} \cup D)$ implies $\xi = \zeta$. Since $\Sigma = \text{mgu}(E^2)\Sigma_0$ we directly obtain that for all $\xi, \zeta \in \text{st}_c(\Sigma, \mathcal{K}\Sigma)$, $(\xi, u), (\zeta, u) \in \text{Conseq}(\mathcal{K}\Sigma)$ implies $\xi = \zeta$, which is exactly the uniformity.

► **Step 3:** Unicity of the solution

This step is rather straightforward: considering that $\Sigma = \text{mgu}(E^2)\Sigma_0$ and any other solutions $(\Sigma', \sigma') \in \text{Sol}(C^e)$ satisfy $\Sigma' \models E^2$, we deduce that $\text{mgs}(C^e) = \{\text{mgu}(E^2)\}$ and so $|\text{mgs}(C^e)| = 1$. ■

Let us now show that all extended constraint systems in the set have the same solutions and that they are statically equivalent.

**LEMMA B.23.** Let $\mathcal{S}$ be a set of extended symbolic processes such that $\text{Inv}_{\text{all}}(\mathcal{S})$ and no instances of the rules (SAT), (EQ) or (REW) or simplification rules are applicable. For all $S \in \mathcal{S}$, for all $(\mathcal{P}_1, C_1, C_1^e), (\mathcal{P}_2, C_2, C_2^e) \in S$, if $(\Sigma, \sigma_1) \in \text{Sol}(C_1^e)$ then $(\Sigma, \sigma_2) \in \text{Sol}(C_2^e)$ and $\Phi(C_1^e)\sigma_1 \sim \Phi(C_2^e)\sigma_2$.
**PROOF.** Since (SAT) and normalisation rules are not applicable, we know by Lemma B.21 that all extended constraint systems $C^e \in S$ have a particular form, that is 1. all deduction facts in $D(C^e)$ have pairwise distinct variables as right hand side; and 2. $E^1(C^e)$ only contain syntactic equations. Moreover, we know that all extended constraint systems have the same structure. Therefore, if $(\Sigma, \sigma_1) \in \text{Sol}(C_1^e)$, we deduce that $\Sigma \models E^2(C_1^e)$ and for all $\xi \in \text{st}(\text{img}(\Sigma))$, $\xi \in \text{Conseq}(\mathbf{K}(C_1^e)\Sigma)$, meaning that $\Sigma \models E^2(C_2^e)$ and $\xi \in \text{Conseq}(\mathbf{K}(C_2^e)\Sigma)$. Since the first order solutions are always completely defined by the second-order substitutions, we can build $\sigma'_2$ such that for all $X \vdash^? x \in D(C_2^e)$, $X\Sigma(\Phi(C_2^e)\sigma'_2) \downarrow = x\sigma'_2$. Moreover, since $\text{Inv}_{\text{sound}}(C_1^e)$ and $\text{Inv}_{\text{sound}}(C_2^e)$ both hold and since for all $\xi \in \text{st}(\text{img}(\Sigma))$, $\xi \in \text{Conseq}(\mathbf{K}(C_2^e)\Sigma)$, we deduce that for all $\xi \in \text{st}(\text{img}(\Sigma))$, $\text{msg}(\xi\Phi(C_2^e)\sigma'_2)$. Note that we also need to satisfy the syntactic equations in $E^1$. However thanks to $\text{Inv}_{\text{wf}}(C_2^e)$ holding, we know that $\text{dom}(\text{mgu}(E^1(C_2^e))) \cap \text{vars}^1(D(C_2^e)) = \emptyset$. Thus, we can build $\sigma_2 = \text{mgu}(E^1(C_2^e))\sigma'_2$ and obtain that $(\Sigma, \sigma_2) \models D(C_2^e) \wedge E^1(C_2^e) \wedge E^2(C_2^e)$. Note that by origination property of an extended constraint system, we have $\Phi(C_2^e)\sigma'_2 = \Phi(C_2^e)\sigma_2$. Therefore, since we already prove that for all $\xi \in \text{st}(\text{img}(\Sigma))$, $\text{msg}(\xi\Phi(C_2^e)\sigma'_2)$ and $\xi \in \text{Conseq}(\mathbf{K}(C_2^e)\Sigma)$, it only remains to prove the second bullet point of Definition the definition of solutions extended constraint system to obtain that $(\Sigma, \sigma_2) \in \text{Sol}(C_2^e)$.

To prove this it suffices to prove that $\Phi(C_1^e)\sigma_1 \sim \Phi(C_2^e)\sigma_2$: the conclusion will then follow since $(\Sigma, \sigma_1) \in \text{Sol}(C_1^e)$. Therefore we let recipes $\xi, \xi'$ and show that:

(i) $\text{msg}(\xi\Phi(C_1^e)\sigma_1) \text{ iff } \text{msg}(\xi\Phi(C_2^e)\sigma_2)$

(ii) if $\text{msg}(\xi\Phi(C_1^e)\sigma_1), \xi'\Phi(C_1^e)\sigma_1)$ then $\xi\Phi(C_1^e)\sigma_1 \downarrow = \xi'\Phi(C_1^e)\sigma_1 \downarrow \text{ iff } \xi\Phi(C_2^e)\sigma_2 \downarrow = \xi'\Phi(C_2^e)\sigma_2 \downarrow$.

We prove this by lexicographic induction on $(N(\xi, \xi'), \max(|\xi|, |\xi'|))$ where $N(\xi, \xi')$ is the number of subterms $\zeta \in \text{st}(\xi, \xi')$ such that $\zeta \notin \text{Conseq}(\mathbf{K}(C_1^e)\Sigma)$ (recall that since $C_1^e$ and $C_2^e$ have the same structure, we have $\zeta \in \text{Conseq}(\mathbf{K}(C_1^e)\Sigma)$ iff $\zeta \in \text{Conseq}(\mathbf{K}(C_2^e)\Sigma)$).

► case 1: $N(\xi, \xi') = 0$ and $\max(|\xi|, |\xi'|) = 0$

Impossible since there exist no terms of size 0.

► case 2: $N(\xi, \xi') > 0$

► subgoal 2a: Proof of (i)

Assume $\text{msg}(\xi\Phi(C_1^e)\sigma_1)$. Let us also assume by contradiction that $\neg\text{msg}(\xi\Phi(C_2^e)\sigma_2)$. Since we know that $N(\xi, \xi') > 0$, there exists $\zeta \in \text{st}(\xi, \xi')$ such that $\zeta \notin \text{Conseq}(\mathbf{K}(C_1^e))$. Without loss of generality we can consider that $\zeta \in \text{st}(\xi)$ (otherwise we can apply our inductive hypothesis on $\xi$ twice since $N(\xi, \xi')$ would be equal to 0 and so we would obtain a contradiction). Moreover, let us consider $\zeta$ such that $|\zeta|$ is minimal. Therefore, by definition of consequence, we deduce that $\zeta = g(\zeta_1, \dots, \zeta_n)$ with $g \in \mathcal{F}_d$ and for all $i \in \{1, \dots, n\}$, $\zeta_i \in \text{Conseq}(\mathbf{K}(C_1^e))$. Since $\text{msg}(\xi\Phi(C_1^e)\sigma_1)$ we also deduce that $g(\zeta_1, \dots, \zeta_n)\Phi(C_1^e)\sigma_1 \downarrow$ is a protocol term. Therefore, there exist a rewrite rule $g(\ell_1, \dots, \ell_n) \rightarrow r$ and a substitution $\gamma$ such that $\ell_i\gamma = \zeta_i\Phi(C_1^e)\sigma_1\downarrow$ for all $i = 1 \dots n$.
Recall that the rule (REW) is not applicable on $C_1^e$ and $C_2^e$. Therefore we can show that provided $\neg msg(\xi\Phi(C_2^e)\sigma_2)$ and $g(\zeta_1, \dots, \zeta_n)\Phi(C_1^e)\sigma_1\downarrow$ is a protocol term then we necessarily have that there exists $\zeta'_1, \dots, \zeta'_n$ and $u$ such that $g(\zeta'_1, \dots, \zeta'_n) \vdash^? u_1 \in F(C_1^e)$ and $\zeta'_i\Sigma\Phi(C_1^e)\sigma_1\downarrow= \zeta_i\Phi(C_1^e)\sigma_1\downarrow$. Moreover, since the normalisation rules are also not applicable (in particular Rule VECT-SPLIT), we deduce that there exists $u_2$ such that $g(\zeta'_1, \dots, \zeta'_n) \vdash^? u_2 \in F(C_2^e)$. By $\text{Inv}_{wf}(C_1^e)$, we know that for all $i \in \{1, \dots, n\}$, $\zeta'_i \in \text{Conseq}(K(C_1^e) \cup D(C_1^e))$ and so $\zeta'_i\Sigma \in \text{Conseq}(K(C_1^e)\Sigma)$. Moreover, by hypothesis on $\zeta_i$, we know that $\zeta_i \in \text{Conseq}(K(C_1^e)\Sigma)$. Thus, by applying our inductive hypothesis, we obtain that $\zeta_i\Phi(C_2^e)\sigma_2\downarrow= \zeta'_i\Sigma\Phi(C_2^e)\sigma_2\downarrow$. Moreover, by $\text{Inv}_{sound}(C_2^e)$, we know that $g(\zeta'_1, \dots, \zeta'_n)\Sigma\Phi(C_2^e)\sigma_2\downarrow= u_2\sigma_2$ which is a protocol term. We conclude that $g(\zeta_1, \dots, \zeta_n)\Sigma\Phi(C_2^e)\sigma_2\downarrow$ is a protocol term and thus $msg(\xi\Phi(C_2^e)\sigma_2)$ gives us a contradiction.

► subgoal 2b: Proof of (ii)

Assume now that $\xi\Phi(C_1^e)\sigma_1\downarrow= \xi'\Phi(C_1^e)\sigma_1\downarrow$, $msg(\xi\Phi(C_1^e)\sigma_1)$ and $msg(\xi'\Phi(C_1^e)\sigma_1)$. Let us once again take the smallest $\zeta \in st(\xi, \xi')$ such that $\zeta \notin \text{Conseq}(K(C_1^e))$. We already proved above that there exist $u_1, u_2, g, \zeta'_1, \dots, \zeta'_n, \zeta_1, \dots, \zeta_n$ such that:

- $\zeta = g(\zeta_1, \dots, \zeta_n)$

- $g(\zeta'_1, \dots, \zeta'_n) \vdash^? u_1 \in F(C_1^e)$

- $g(\zeta'_1, \dots, \zeta'_n) \vdash^? u_2 \in F(C_2^e)$

- for all $i \in \{1, \dots, n\}$, $\zeta_i\Phi(C_2^e)\sigma_2\downarrow= \zeta'_i\Sigma\Phi(C_2^e)\sigma_2\downarrow$ and $\zeta_i\Phi(C_1^e)\sigma_1\downarrow= \zeta'_i\Sigma\Phi(C_1^e)\sigma_1\downarrow$.

By $\text{Inv}_{satur}(C_1^e)$, we know that there exists $\beta$ such that $(\beta, u_1) \in \text{Conseq}(K(C_1^e) \cup D(C_1^e))$. However the normalisation Rule VECT-ADD-FORMULA is not applicable on the set of extended symbolic processes. Thus, we deduce that there exists $\beta'$ such that $(\beta', u_1) \in \text{Conseq}(K(C_1^e) \cup D(C_1^e))$ and $g(\zeta'_1, \dots, \zeta'_n) =^? \beta' \in F(C_1^e)$. Once again due to the normalisation Rule VECT-SPLIT, we obtain that $g(\zeta'_1, \dots, \zeta'_n) =^? \beta' \in F(C_2^e)$. But $\text{Inv}_{sound}(C_2^e)$ and $\text{Inv}_{sound}(C_1^e)$ hold meaning that $(\Phi(C_2^e)\sigma_2, \Sigma, \sigma_2) \models g(\zeta'_1, \dots, \zeta'_n) =^? \beta'$ and $(\Phi(C_1^e)\sigma_1, \Sigma, \sigma_1) \models g(\zeta'_1, \dots, \zeta'_n) =^? \beta'$.

Note that if $p$ is the position of $\zeta$ in $\xi$ then we have $N(\xi[\beta'\Sigma]_p, \xi') < N(\xi, \xi')$. Thus by applying our inductive hypothesis, we obtain that $(\Phi(C_2^e)\sigma_2, \Sigma, \sigma_2) \models \xi[\beta'\Sigma]_p =^? \xi'$. Since $(\Phi(C_2^e)\sigma_2, \Sigma, \sigma_2) \models g(\zeta'_1, \dots, \zeta'_n) =^? \beta'$ and $(\Phi(C_2^e)\sigma_2, \Sigma, \sigma_2) \models g(\zeta'_1, \dots, \zeta'_n) =^? g(\zeta_1, \dots, \zeta_n)$, we conclude that $(\Phi(C_2^e)\sigma_2, \Sigma, \sigma_2) \models \xi =^? \xi'$.

► case 3: $N(\xi, \xi') = 0$ and $\max(|\xi|, |\xi'|) > 0$

In such a case, we know that $\xi, \xi' \in \text{Conseq}(K(C_1^e)\Sigma)$ and $\xi, \xi' \in \text{Conseq}(K(C_2^e)\Sigma)$. By definition of consequence and by $\text{Inv}_{sound}(C_1^e)$ and $\text{Inv}_{sound}(C_2^e)$, we directly obtain that $msg(\xi\Phi(C_1^e)\sigma_1)$ and $msg(\xi\Phi(C_2^e)\sigma_2)$ (same thing for $\xi'$). Now assume that $(\Phi(C_1^e)\sigma_1, \Sigma, \sigma_1) \models \xi =^? \xi'$. Since both $\xi, \xi'$ are consequences of $K(C_1^e)\Sigma$, we deduce that:

- either $\xi = f(\xi_1, \dots, \xi_n)$ and $\xi' = f(\xi'_1, \dots, \xi'_n)$ with $f \in \mathcal{F}_c$ and $(\Phi(C_1^e)\sigma_1, \Sigma, \sigma_1) \models \xi_i =^? \xi'_i$ for all $i$. Therefore, we can apply our inductive hypothesis on the $(\xi_i, \xi'_i)$s to conclude.
— or $\xi\Sigma, \xi'\Sigma \in K(C_1^e)\Sigma$: Since we know that the rule (EQ) is not applicable, it implies that
$\xi =_f^? \xi' \in F(C_1^e)$ and so $\xi =_f^? \xi' \in F(C_2^e)$ thanks to the normalisation Rule VECT-SPLIT. Since
$\mathrm{Inv}_{\mathrm{sound}}(C_2^e)$ holds, we can conclude that $(\Phi(C_2^e)\sigma_2, \Sigma, \sigma_2) \models \xi =_f^? \xi'$.

— or $\xi\Sigma \in K(C_1^e)\Sigma$ and $\xi' = f(\xi'_1, \dots, \xi'_n)$ with $f \in \mathcal{F}_c$; Once again since the rule (EQ) is not applicable, we deduce that there exists $\zeta'_1, \dots, \zeta'_n$ such that $\xi =_f^? f(\zeta'_1, \dots, \zeta'_n) \in F(C_1^e)$. Note from $\mathrm{Inv}_{\mathrm{sound}}(C_1^e)$ that in such a case, $(\Phi(C_1^e)\sigma_1, \Sigma, \sigma_1) \models \xi =_f^? f(\zeta'_1, \dots, \zeta'_n)$ meaning that $(\Phi(C_1^e)\sigma_1, \Sigma, \sigma_1) \models \xi'_i =_f^? \zeta'_i$ for all $i \in \{1, \dots, n\}$. Since $|\xi'_i\Phi(C_1^e)\sigma_1\rangle \downarrow < |\xi\Phi(C_1^e)\sigma_1\rangle \downarrow |$, we can apply our inductive hypothesis on all $(\xi'_i, \zeta'_i)$ meaning that $(\Phi(C_2^e)\sigma_2, \Sigma, \sigma_2) \models f(\zeta'_1, \dots, \zeta'_n) =_f^? \xi'$. However, by the rule VECT-SPLIT not being applicable, $\xi =_f^? f(\zeta_1, \dots, \zeta'_n) \in F(C_1^e)$ implies $\xi =_f^? f(\zeta'_1, \dots, \zeta'_n) \in F(C_2^e)$ and so by $\mathrm{Inv}_{\mathrm{sound}}(C_2^e)$, we obtain that $(\Phi(C_2^e)\sigma_2, \Sigma, \sigma_2) \models \xi =_f^? f(\zeta'_1, \dots, \zeta'_n)$ which allows us to conclude that $(\Phi(C_2^e)\sigma_2, \Sigma, \sigma_2) \models \xi =_f^? \xi'$. ■

**C. Termination proof**

**C.1 For mgs**

The termination of the computation of most general solutions mostly relied on the following
result, yet to be proved:

**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 $\mathrm{Inv}_{wf}(C^e)$ and $\mathrm{Inv}_{sound}(C^e)$*
*hold. Then let $C^e \xrightarrow{\Sigma} C^{e'} \neq \perp$. If this transition is derived with:*

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

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

**PROOF.** Consider first the simplification rule (MGS-UNIF) and the ones from Figure 7. They typically apply protocol term substitutions on the constraint system (they also effect recipe disequations that are irrelevant in *unused*¹(*C*⁵)). Note that the applied substitution is always generated from terms already in the constraint system. As such *μ*¹(*C*⁵↓) = *μ*¹(*C*⁵) and so *Φ*(*C*⁵↓)·*μ*¹(*C*⁵↓) = *Φ*(*C*⁵)·*μ*¹(*C*⁵), *K*(*C*⁵↓)·*μ*¹(*C*⁵↓) = *K*(*C*⁵)·*μ*¹(*C*⁵) and *D*(*C*⁵↓)·*μ*¹(*C*⁵↓) = *D*(*C*⁵)·*μ*¹(*C*⁵). Thus, we directly obtain that |unused¹(*C*⁵↓)| ≤ |unused¹(*C*⁵)|.

Let us look at Rules (MGS-CONSEQ), (MGS-CONS) and (MGS-RES) and let us consider $C^e \xrightarrow{\Sigma} C^{e'}$.
The rule (MGS-CONSEQ) does not modify the protocol terms of the constraint systems by apply
a recipe substitution. However, we show an invariant on the constraint systems that any
$\xi, \zeta \in st_c(C^e)$ are consequence of $K \cup D$ as well as any of their subterms (see Definition B.1
in Appendix). Thus, we deduce from the definition of $st_c(C^e)$ that $st_c(C^e)\Sigma \subseteq st_c(C^{e'})$. To
conclude that $|unused^1(C^{e'})| \le |unused^1(C^e)|$, we rely on the technical Proposition B.11; in other
words, if $(\xi, t) \in \mathrm{Conseq}(K(C^e)\mu^1(C^e) \cup D(C^e)\mu^1(C^e))$ then $(\xi\Sigma, t) \in \mathrm{Conseq}(K(C^{e'})\mu^1(C^{e'}) \cup
D(C^{e'})\mu^1(C^{e'}))$. Since $st_c(C^e)\Sigma \subseteq st_c(C^{e'})$, we conclude that $|unused^1(C^{e'})| \le |unused^1(C^e)|$.
Applying the same reasoning for the rule (MGS-RES), we can also show that $unused^1(C'^e) \le unused^1(C^e)$. However, we can even show that this inequality is strict. Indeed, using the same the notation in the rule (MGS-RES), this rule is only applied if $C^e = C^e \downarrow$ and for all $\xi \in st_c(C^e) \setminus \{X\}$, $(\xi, u) \notin \text{Conseq}(K \cup D)$. Note that $C^e = C^e \downarrow$ implies that $K\mu^1 = K$ and $D\mu^1 = D$. Moreover, it also implies that $u \in unused^1 C^e$. However, in $C'^e$, we have that $(\xi, u\mu_1(C'^e)) \in \text{Conseq}(K(C'^e)\mu^1(C'^e) \cup D(C'^e)\mu^1(C'^e))$. Moreover, we show another invariant on the constraint system (see Definition B.1 in Appendix) that ensures us that $X \in st_c(C^e)$ and so $\xi \in st_c(C'^e)$. Hence, we obtain that $u\mu^1(C'^e) \notin unused^1(C'^e)$ allowing us to conclude that $unused^1(C'^e) < unused^1(C^e)$. By applying the same reasoning, we can also show that $unused^1(C'^e) < unused^1(C^e)$ when the rule (MGS-CONS) is applied. ■

## C.2 Exponential measure

Another argument left pending is that each component of the measure except the last one can be bounded by an exponential in the DAG size of the parameters of the problem. We give a bound for each of them, in particular relying on the bound on $unused^1$ proved in the body of the article.

1. $M_1(\Gamma) \le |P, Q|_{\text{dag}}$: by definition.

2. $M_2(\Gamma) \le (|P|_{\text{dag}} |E|_{\text{dag}})^{|P|_{\text{dag}}} + (|Q|_{\text{dag}} |E|_{\text{dag}})^{|Q|_{\text{dag}}}$:

The measure corresponds to the number of symbolic transitions possible from $P$ and $Q$ for a given symbolic trace, hence the bound. Notice that the part $|E|_{\text{dag}}^{|P|_{\text{dag}}}$ is due to the computation of the most general unifiers modulo $E$ in the symbolic transitions.

3. $M_3(\Gamma) \le 9 |P, Q, E|_{\text{dag}}^3$:

It suffices to observe that $\text{set}_K(C^e) \le unused^1(C^e)$ and to use the bound proved in the body of the article.

4. $M_4(\Gamma) \le M_2(\Gamma)$:

5. $M_5(\Gamma) \le M_2(\Gamma) \times |E|_{\text{dag}}^{|E|_{\text{dag}}} \times (18 |P, Q, E|_{\text{dag}})^{27|P, Q, E|_{\text{dag}}^3}$:

Bounding the size of $|\text{set}_{\text{REW}}(C^e)|$ can easily be done: the number of $\psi \in K$ possible is bounded by $|K|$, itself bounded by $|\text{set}_K(C^e)|$. The number of rewrite rules, position $p$ and $\psi_0 \in \text{RewF}(\xi, \ell \to r, p)$ only depends on the rewrite systems and can be bounded by $|E|_{\text{dag}}^{|E|_{\text{dag}}}$.
Note that the exponential comes mainly from the number of possible positions in $\ell$. We already know that the number of most general solutions is bounded by $(|K(C^e)| + 1)^{unused^1(C^e)}$.
Combining with all previous results, and with the rough approximation $9|P, Q, E|_{\text{dag}}^3 + 1 \le 18|P, Q, E|_{\text{dag}}^3$, we obtain the above bound.

6. $M_6(\Gamma) \le |E| \times M_2(\Gamma):$
To bound this number, we need to recall that we always apply the case distinction rules with the priority ordering (SAT) < (REW). Thus, when we apply a rule (REW), there is no unsolved deduction formula in any of the extended constraint systems (otherwise we should have applied the rule (SAT)). It means this measure is bounded by the number of deduction formulas produced by one instance of (REW). By definition, we know that $|\text{RewF}(\xi, \ell \to r, p)| \le |\mathcal{R}|$ (one formula per rewrite rule). Thus, the rule (REW) generates at most $|E| \times M_2(\Gamma)$ deduction formulas.

7. $M_7(\Gamma) \le M_2(\Gamma) \times 2^{|E|_{\text{dag}} (|P, Q|_{\text{dag}})^2 (1 + |E|_{\text{dag}})^2}$:

The application conditions stipulate that the rule can be applied either (a) on two deduction facts of $\kappa(C_i^e)$, or (b) on one deduction fact of $\kappa(C_i^e)$ in combination with a construction function symbol.

Note that even though the rule also consider the existence of a most general solution $\Sigma \in \text{mgs}(C_i^e[E^1 \mapsto E^1 \wedge \text{hyp}(\psi:(\Sigma_0, C_i^e))])$, the number of applications of the rule (EQ) will not depend on the number of possible most general solutions. Indeed, consider the case (a) where the rule is applied on two deduction fact $(\xi_1 \vdash^? u_1), (\xi_2 \vdash^? u_2) \in \kappa(C_i^e)$. Thus, an equality formula with $\xi_1\Sigma =^?_f \xi_2\Sigma$ as head will be added in $F(C_i^e:\Sigma)$. However, in the application conditions of the rule, we also require that for all $(\forall S. H \Leftarrow \varphi) \in F(C_i^e)$, $H \ne (\xi_1 =^?_f \xi_2)$. Thus, a new application of the rule (EQ) on $C_i^e:\Sigma$ with the same (up to instantiation of $\Sigma$) deductions facts from $\kappa(C_i^e:\Sigma)$ will be prevented.

The same situation occurs in case (b) with the condition for all $(\forall S. \zeta_1 =^?_f \zeta_2 \Leftarrow \varphi) \in F(C_i^e)$, $\zeta_1 = \xi_1$ implies $\text{root}(\zeta_2) \ne \text{f}$. We therefore conclude that the rule (EQ) can be applied only once per pair of deduction facts in $\kappa$ and once per deduction fact in $\kappa$ and function symbol in $\mathcal{F}_c$.

8. $M_8(\Gamma) \le M_2(\Gamma):$

Unsolved equality formulas can be generated by two rules: the case distinction rule (EQ) or the simplification Rule VECT-ADD-FORMULA. However, once again because of the priority order (SAT) < (EQ), the two rules cannot be triggered simultaneously and the rule (EQ) is only triggered when there is no unsolved equality formulas. Note that due to the condition $\forall i.\forall (\forall S. \zeta_1 =^?_f \zeta_2 \Leftarrow \varphi) \in F_i, \zeta_1 \ne \xi$ or $\zeta_2 \ne \xi$ in Rule VECT-ADD-FORMULA, two instances of the Rule VECT-ADD-FORMULA with different recipes $\zeta$ (e.g. if $u_1$ can be deducible with two different recipes) cannot be applied sequentially. Thus, at any given moment, there is at most one unsolved equality formula per extended constraint system of $\Gamma$, hence the bound.

### C.3 Bounding the increase of second order terms

In Section 5.3, Proposition 5.8, we gave a bound on the increase of the size of most general solutions when applying the rule (SAT). We give here the arguments to extend to the other
case distinction rules. For that it suffices to generalise this property to a more general set of substitution Σ:

**DEFINITION C.1.** Let $C^e$ be an extended constraint system. Let $\Sigma$ be a second-order substitution. We say that $\Sigma \in \text{CompatSubs}(C^e)$ if $\text{dom}(\Sigma) \subseteq \text{vars}^2(\text{D}(C^e))$ and for all $X \in \text{dom}(\Sigma)$, $X\Sigma \in \text{Conseq}(\text{K}(C^e) \cup D' \cup D_\Sigma)$ where $D' = \{X \vdash^? u \in \text{D}(C^e) \mid X \notin \text{dom}(\Sigma)\}$ and $D_\Sigma = \{X \vdash^? x \mid x \text{ fresh and } X \in \text{vars}^2(\Sigma) \setminus \text{vars}^2(C^e)\}$.

Intuitively, $\text{CompatSubs}(C^e)$ represents the recipe substitutions $\Sigma$ that can be applied be applied to the constraint system $C^e$, i.e. $C^e:\Sigma$, and such that the recipes in the of $\Sigma$ would be consequence of $C^e:\Sigma$. Note that $\text{mgs}(C^e) \subseteq \text{CompatSubs}(C^e)$.

By applying Proposition B.11, we can show that:

$$ \text{for all } \Sigma \in \text{CompatSubs}(C^e), |\text{unused}^1(C^e:\Sigma)| \le |\text{unused}^1(C^e)| \quad (4) $$

Note that in a set of symbolic processes two extended constraint systems $C_1^e, C_2^e$ always have the same *recipe structure* (Invariant $\text{Inv}_{\text{str}}$), i.e. $|\Phi(C_1^e)| = |\Phi(C_2^e)|$, $\text{vars}^2(C_1^e) = \text{vars}^2(C_2^e)$ and $\{\xi \mid (\xi \vdash^? u) \in \text{K}(C_1^e)\} = \{\xi \mid (\xi \vdash^? u) \in \text{K}(C_2^e)\}$. Thus, we deduce that $\text{CompatSubs}(C_1^e) = \text{CompatSubs}(C_2^e)$. Therefore, we can conclude that for any simplification and case distinction rules, $|\text{unused}^1(C^e)|$ never increase for all extended constraint systems in a set of extended symbolic processes.

# D. Proofs of complexity lower bounds

## D.1 Advanced winning strategies

Before starting the proofs, we present some characterizations of observational (in)equivalence in order to make the incoming proofs easier to handle.

**REMARK D.1.** The results of this section (D.1) also apply to the extended semantics of Section 5.5.1.

**For the defender** The transitions of the semantics which are deterministic and silent are not essential to equivalence proofs as they do not interfere substantially with them. We introduce below a refined proof technique to rule them out.

**DEFINITION D.2 (simplification).** A multiset of closed plain processes $\mathcal{S}$ is silent in an extended process $(\mathcal{P}, \Phi)$ when for all transitions $(\mathcal{P} \cup \mathcal{S}, \Phi) \xrightarrow{\alpha} (\mathcal{Q}, \Phi')$, it holds that $\mathcal{Q} = \mathcal{P}' \cup \mathcal{S}$ with $(\mathcal{P}, \Phi) \xrightarrow{\alpha} (\mathcal{P}', \Phi')$ and $\mathcal{S}$ silent in $(\mathcal{P}', \Phi')$. Then we define $\rightsquigarrow$ (simplification relation) the relation
on extended processes defined by the following inference rules:

$$ \frac{\mathbb{S} \text{ silent in } (\mathcal{P}, \Phi)}{(\mathcal{P} \cup \mathbb{S}, \Phi) \rightsquigarrow (\mathcal{P}, \Phi)} [(S - \text{sil})] $$

$$ \frac{c \in \mathcal{N} \quad \text{msgt} \quad c \notin \text{names}\mathcal{P}, \Phi}{(\mathcal{P} \cup \{\overline{c}\langle t \rangle.P, c(x).Q\}), \Phi) \rightsquigarrow (\mathcal{P} \cup \{P, Q\{x \mapsto t\}\}, \Phi)} [(S - \text{comm})] $$

$$ \frac{A \xrightarrow{\tau} B \text{ by rules NULL, PAR, THEN, ELSE}}{A \rightsquigarrow B} [(S - \text{npte})] $$

In other words, we write $A \rightsquigarrow B$ when $B$ is obtained from $A$ by removing some silent process or applying a deterministic (in the sense of the confluence lemma below) instance of the transition relation $\xrightarrow{\tau}$. We call $\rightsquigarrow_{pi}$ the restriction of $\rightsquigarrow$ to the rule simplification. Their reflexive transitive closures are denoted $\rightsquigarrow_{\star}$ and $\rightsquigarrow_{\star pi}$ respectively as usual.

**LEMMA D.3.** If $A \rightsquigarrow B$ (by some rule $\varrho_{sil}$ of the definition of $\rightsquigarrow$) and $A \xrightarrow{\alpha} C$ (by some rule $\varrho_c$ of the semantics), then either $B = C$ and $\alpha = \rightsquigarrow_{\star}$, or there exists $D$ such that $C \rightsquigarrow D$ (by rule $\varrho_{sil}$) and $B \xrightarrow{\alpha} D$ (by rule $\varrho_c$).

**PROOF.** We make a case analysis on the rule used to obtain the reduction $A \rightsquigarrow B$:

— case 1 : by rule simplification:

Then we write $A = (\mathcal{P} \cup \mathbb{S}, \Phi)$, $B = (\mathcal{P}, \Phi)$. By definition of silent processes, the reduction $A \xrightarrow{\alpha} C$ hence gives $C = (\mathcal{P}' \cup \mathbb{S}, \Phi')$ where $(\mathcal{P}, \Phi) \xrightarrow{\alpha} (\mathcal{P}', \Phi') = D$ and $\mathbb{S}$ silent in $D$. In particular $D$ gives the expected conclusion.

— case 2 : by rule simplification or simplification:

Then either $B = C$ and the conclusion is immediate, or $B \neq C$ and a quick analysis of the rules of the semantics gives $\mathcal{P}, Q_B, Q'_B, Q_C, Q'_C, \Phi, \Phi'$ such that:

$$ \begin{array}{l@{\qquad}l@{\qquad}l} A = (\{Q_B, Q_C\} \cup \mathcal{P}, \Phi) & B = (\{Q'_B, Q_C\} \cup \mathcal{P}, \Phi) & C = (\{Q_B, Q'_C\} \cup \mathcal{P}, \Phi') \\ (\{Q_B\}, \Phi) \rightsquigarrow (\{Q'_B\}, \Phi) & (\{Q_C\}, \Phi) \xrightarrow{\alpha} (\{Q'_C\}, \Phi') & \end{array} $$

and we conclude by choosing $D = (\{Q'_B, Q'_C\} \cup \mathcal{P}, \Phi')$. ■

**COROLLARY D.4.** If $A \rightsquigarrow B$ and $A \xrightarrow{\alpha} C$ then either $B \rightsquigarrow C$ and $\alpha = \rightsquigarrow_{\star}$, or there exists $D$ such that $C \rightsquigarrow D$ and $B \xrightarrow{\alpha} D$. ■

**PROOF.** By a straightforward induction on the number of steps of the reduction $A \rightsquigarrow B$. ■

**COROLLARY D.5.** $\rightsquigarrow_{pi}$ is convergent.
**PROOF.** The termination of $\rightsquigarrow_{\pi_i}$ follows from the termination of the whole calculus. As for the local confluence (which sufficies by Newmann's lemma), we observe that by Lemma D.3, if $A \rightsquigarrow_{\pi_i} B$ and $A \rightsquigarrow_{\pi_i} C$ then either $B = C$, or there is $D$ such that $B \rightsquigarrow_{\pi_i} D$ and $C \rightsquigarrow_{\pi_i} D$: in particular, $B \overset{\star}{\rightsquigarrow}_{\pi_i} E$ and $C \overset{\star}{\rightsquigarrow}_{\pi_i} E$ for some $E \in \{C, D\}$. ■

In particular, all extended processes $A$ have a unique normal form w.r.t. $\rightsquigarrow_{\pi_i}$ which will be written $A_{\downarrow\pi_i}$. This notation is lifted to multiset of processes, writing $\mathcal{P}_{\downarrow\pi_i}$ (which is consistent since $\rightsquigarrow_{\pi_i}$ does not modify the frame). With all of this, we eventually gathered all the ingredients to introduce our characterization of bisimilarity:

**DEFINITION D.6 (bisimulation up to $\rightsquigarrow$).** A symmetric relation $\mathcal{R}$ on extended processes is then said to be bisimulation up to $\rightsquigarrow$, or a bisimulation up to simplification, when:

— $\mathcal{R} \subseteq \sim$;

— for all extended processes $A, B$ such that $A \mathcal{R} B$, and for all transitions $A \xrightarrow{\alpha} A'$, there exists $B \xrightarrow{\alpha} B'$ such that $A' \overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow} B'$.

**PROPOSITION D.7.** For all extended processes $A$ and $B$, $A \approx_b B$ iff there exists a bisimulation up to simplification $\mathcal{R}$ such that $A \overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow} B$.

**PROOF.** The forward implication follows from the fact that $\approx_b$ is a bisimulation up to simplification (by reflexivity of $\rightsquigarrow$). For the converse, let us consider $\mathcal{R}$ a bisimulation up to $\rightsquigarrow$ and prove that it is contained in $\approx_b$. In order to do that, it sufficies to show that:

— $\overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow}$ is symmetric;

— $(\overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow}) \subseteq \sim$;

— for all extended processes $A, B$ such that $A \overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow} B$, if $A \xrightarrow{\alpha} A'$ then there exists $B \xrightarrow{\alpha} B'$ such that $A' \overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow} B'$.

These three properties indeed justify that $(\overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow}) \subseteq \approx_b$ by definition, hence the expected conclusion as $\mathcal{R} \subseteq \overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow}$ by reflexivity of $\rightsquigarrow$. Yet it appears that the first two points directly follows from the properties of $\mathcal{R}$ and the reflexivity of $\rightsquigarrow$, and we thus only need to prove the third point. Let us therefore consider the following hypotheses and notations:

$$A \overset{\star}{\rightsquigarrow} C \mathcal{R} D \overset{\star}{\rightsquigarrow} B$$

$$A \xrightarrow{\alpha} A'$$

and let us exhibit $B'$ such that $B \xrightarrow{\alpha} B'$ and $A' \overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow} B'$. Let us consider the two cases induced by the application of Corollary D.4:

— **case 1 :** $A' \overset{\star}{\rightsquigarrow} C$ and $\alpha = \rightsquigarrow$

Then we can choose $B' = B$.

— **case 2 :** there exists $C'$ such that $A' \overset{\star}{\rightsquigarrow} C'$ and $C \xrightarrow{\alpha} C'$

Consequently, since $\mathcal{R}$ is a bisimulation up to simplification, there is $D'$ such that $D \xrightarrow{\alpha} D'$ and $C' \overset{\star}{\rightsquigarrow} \mathcal{R} \overset{\star}{\rightsquigarrow} D'$. Then we remark that for all extended processes $B_1, B_2, B_3$:
— a transition $B_1 \rightsquigarrow B_2$ with rules simplification or simplification implies $B_1 \xrightarrow{\tau} B_2$;

— if $B_1 \rightsquigarrow B_2$ with rule simplification and $B_2 \xrightarrow{\beta} B_3$, then $B_1 \xrightarrow{\beta} \rightsquigarrow B_3$.

In particular since $B \underset{\sim}{\overset{\star}{\rightleftharpoons}} D \stackrel{\alpha}{\Rightarrow} D'$, we have $B \stackrel{\alpha}{\Rightarrow} D'' \underset{\sim}{\overset{\star}{\rightleftharpoons}} D'$ for some $D''$. Hence the conclusion by choosing $B' = D''$. ■

**For the attacker** When taking the negation of labelled bisimilarity, we essentially obtain a set of rules for a game whose states are pairs of processes (A, B): an attacker selects a transition and a defender answers by selecting an equivalently-labelled sequence of transitions in the other process.

**DEFINITION D.8 (labelled attack).** A relation $S$ on extended processes is called a labelled attack when for all A, B such that $A \in S B$, it holds that:

1. either: $A \not\supseteq B$

2. or: $\exists A \xrightarrow{\alpha \text{ tr}} A'$, $\forall B \xrightarrow{\alpha \text{ tr}} B'$, $A' S B'$

3. or: $\exists B \xrightarrow{\alpha \text{ tr}} B'$, $\forall A \xrightarrow{\alpha \text{ tr}} A'$, $A' S B'$

Note that labelled attacks are not the direct translation of the above intuition since they allow the attacker to choose several transitions in a row; this intuitively entails no loss of generality since it is equivalent to the attacker selecting some transitions non-adaptatively (i.e. independently of the answer of the defender). Here is the formal statement of correctness:

**PROPOSITION D.9.** For all extended processes A and B, $A \not\supseteq_b B$ if there exists a labelled attack $S$ such that $A \in S B$.

**PROOF.** The forward implication is immediate since $\not\supseteq_b$ is a labelled attack (we can even choose $\text{tr} = \varepsilon$ everytime). Let then $S$ be a labelled attack such that $A \in S B$ and let us prove that $S \subseteq \not\supseteq_b$. More precisely, we prove that $S \subseteq S' \subseteq \not\supseteq_b$ for some relation $S'$. We will construct $S'$ in such a way that for all A, B extended processes, $A \in S' B$ entails:

(i) either: $A \not\supseteq B$;

(ii) or: $\exists A \xrightarrow{\alpha} A'$, $\forall B \xrightarrow{\alpha} B'$, $A' S B'$;

(iii) or: $\exists B \xrightarrow{\alpha} B'$, $\forall A \xrightarrow{\alpha} A'$, $A' S B'$

The inclusion $S' \subseteq \not\supseteq_b$ is indeed clear if this property is verified, hence the expected conclusion provided such a relation $S'$. We concretely define it as the smallest relation on extended
processes saturated by the following inference rules:

$$ \frac{A S B}{A S' B}[(\text{Axiom})] $$

$$ \frac{A S' B \quad A \xrightarrow{\alpha} A' \xrightarrow{\alpha' \quad \text{tr}} A'' \quad \forall B \quad \alpha.\alpha'.\text{tr} \implies B'', A'' S' B'' \quad B \xrightarrow{\alpha} B' \quad [(\text{Dec} - L)]}{A' S' B'} $$

$$ \frac{A S' B \quad B \xrightarrow{\alpha} B' \xrightarrow{\alpha' \quad \text{tr}} B'' \quad \forall A \quad \alpha.\alpha'.\text{tr} \implies A'', A'' S' B'' \quad A \xrightarrow{\alpha} A' \quad [(\text{Dec} - R)]}{A' S' B'} $$

In particular, note that $S \subseteq S'$ thanks to the rule For the attacker. As for the two other rules For the attacker and For the attacker, they intuitively decompose sequences $\xrightarrow{\alpha \text{ tr}}$ into atomic transitions in order to switch from points 2. or 3. of Definition D.8 to points (ii) or (iii).

Let then A and B be two extended processes such that $A S' B$. We consider a proof-tree of $A S' B$ in the inference system above and perform a case analysis on the rule at its root:

- case 1 For the attacker: $A S B$.

As $S$ is a labelled attack, we apply the case analysis of Definition D.8:

- case 1.a : $A \neq B$.

Then (i) is satisfied.

- case 1.b : there exists $A \xrightarrow{\alpha} A' \xrightarrow{\alpha'.\text{tr}} A''$ such that $A'' S B''$ for all $B \xrightarrow{\alpha.\text{tr}} B''$.

In particular, keeping in mind that $S \subseteq S'$ due to the rule For the attacker, we have $A'' S' B''$ for all $B \xrightarrow{\alpha.\text{tr}} B''$. Let us then show that the transition $A \xrightarrow{\alpha} A'$ satisfies (ii). We therefore have to show that $A' S' B'$ for all $B \xrightarrow{\alpha} B'$. If $A' = A''$ then the result follows from the hypothesis. Otherwise let us write $A \xrightarrow{\alpha} A' \xrightarrow{\alpha'.\text{tr}'} A''$ where $\alpha'.\text{tr}' = \text{tr}$ and the rule For the attacker justifies that $A' S' B'$ for all $B \xrightarrow{\alpha} B'$.

- case 1.c : there exists $B \xrightarrow{\alpha} B' \xrightarrow{\alpha'.\text{tr}} B''$ such that $B'' S A''$ for all $A \xrightarrow{\alpha.\text{tr}} A''$.

Analogous, targeting (iii) instead of (ii) and replacing For the attacker by For the attacker.

- case 2 For the attacker: there are $A_0, A_1, A_2, B_0, B_2, \alpha, \alpha', \text{tr}$, such that $A_0 S' B_0, B_0 \xrightarrow{\alpha} B, A_0 \xrightarrow{\alpha} A \xrightarrow{\alpha'} A_1 \xrightarrow{\text{tr}} A_2$, and $\forall B_0 \xrightarrow{\alpha.\alpha'.\text{tr}} B_2, A_2 S' B_2$.

Let us show that the transition $A \xrightarrow{\alpha'} A_1$ satisfies (ii). We therefore have to show that $A_1 S' B_1$ for all $B \xrightarrow{\alpha'} B_1$. If $A_1 = A_2$ then the result follows from the hypothesis. Otherwise we write $A \xrightarrow{\alpha'} A_1 \xrightarrow{\alpha'' \text{ tr}'} A_2$ where $\alpha'' \text{ tr}' = \text{tr}$ and the rule For the attacker justifies that $A_1 S' B_1$ for all $B \xrightarrow{\alpha} B_1$.

- case 3 For the attacker: Analogous to case 2.
## D.2 Correctness of the encodings (Section 5.5.1)

Now we prove that the translation $[\cdot]$ of the extended semantics is correct:

**LEMMA D.10.** Let $\approx_t^+$ and $\approx_b^+$ be the notions of trace equivalence and labelled bisimilarity over the extended calculus (the flag $+$ being omitted outside of this lemma). For all extended processes $A = (\mathcal{P}, \Phi)$, the translation $[[A]] = ([\mathcal{P}], \Phi) = (\{[[P]] \mid P \in \mathcal{P}\}, \Phi)$ can be computed in polynomial time, $A \approx_t^+ [[A]]$ and $A \approx_b^+ [[A]]$.

But first of all, a (trivial) observation about the free variables of a translated process:

**LEMMA D.11.** For all plain processes $P$ and all first-order substitution $\sigma$, $[[P\sigma]] = [[P]]\sigma$.

We will use this lemma implicitly in the remaining of this section. Besides, as we have the inclusion of relations $\approx_b \subseteq \approx_t$, we only need to prove the observational-equivalence statement of Lemma D.10. We recall that we use notations $A_{\downarrow pi}$ and $\mathcal{P}_{\downarrow pi}$ to refer to normal forms w.r.t. $\rightsquigarrow_{pi}$ (see Corollary D.5).

**PROPOSITION D.12.** We consider $\mathcal{R}$ the symmetric closure of:

$$ \{(C, [[C]]_{\downarrow pi}) \mid C \text{ extended process such that } C = C_{\downarrow pi}\} $$

$\mathcal{R}$ is a bisimulation up to simplification.

**PROOF.** $\mathcal{R}$ is symmetric by definition and is trivially included in $\sim$. Let then $(A, B) \in \mathcal{R}$ and $A \xrightarrow{\alpha} A'$ and let us exhibit $B'$ such that $B \xrightarrow{\alpha} B'$ and $A' \mathcal{R} B'$. We perform a case analysis on the rule triggering the transition $A \xrightarrow{\alpha} A'$:

— case 1 (rules NULL, PAR, THEN, ELSE):

This case cannot arise as $A$ is in normal form w.r.t. $\rightsquigarrow_{pi}$ by definition of $\mathcal{R}$.

— case 2 (rule IN): $\alpha = \xi(\zeta)$ for some $\xi, \zeta \in \mathcal{T}(\mathcal{F}, \mathcal{F}_0 \cup \text{dom}\Phi)$ and:

$$ A = (\mathcal{P} \cup \{\{u(x).P\}, \Phi\}) \quad \text{with msgu, msg} \xi \Phi \text{ and } \xi \Phi \downarrow = u \downarrow $$

$$ A' = (\mathcal{P} \cup \{\{P\{x \mapsto \zeta \Phi \downarrow\}\}, \Phi\}) \quad \text{with msg} \zeta \Phi $$

Then, by a case analysis on the hypothesis $A \mathcal{R} B$:

— case 2.a : $B = [[A]]_{\downarrow pi}$

Then we can write:

$$ B = ([\mathcal{P}]_{\downarrow pi} \cup \{u(x).[[P]]\}, \Phi) $$

and we conclude by remarking that $B \xrightarrow{\xi(\zeta)} B' = ([\mathcal{P}]_{\downarrow pi} \cup \{[[P]]\{x \mapsto \zeta \Phi \downarrow\}\}, \Phi)$ and:

$$ A' \rightsquigarrow A'_{\downarrow pi} \mathcal{R} [[A'_{\downarrow pi}]]_{\downarrow pi} = [[A')]_{\downarrow pi} = ([\mathcal{P}]_{\downarrow pi} \cup \{[[P]]\{x \mapsto \zeta \Phi \downarrow\}\})_{\downarrow pi}, \Phi) \rightsquigarrow B' $$
— case 2.b : $A = [[B]]_{\downarrow pi}$ (and $B = B_{\downarrow pi}$)

Note that $u = \xi\Phi\downarrow$ cannot be one of the names introduced by the translation $[[\cdot]]$: these names can indeed not appear in $\Phi$ since they are chosen private and fresh and since the semantics cannot introduce new private names. In particular we can write:

$$B = (Q \cup \{u(x).Q\}, \Phi) \quad \text{with } [[Q]] = P \text{ and } [[Q]]_{\downarrow pi} = \mathcal{P}$$

and we conclude by writing $B \xrightarrow{\xi(\zeta)} B' = (Q \cup \{Q\{x \mapsto \zeta\Phi\downarrow\}\}, \Phi)$ and:

$$A' \overset{\star}{\rightleftharpoons} ([Q]_{\downarrow pi} \cup \{[[Q]\{x \mapsto \zeta\Phi\downarrow\}]\}_{\downarrow pi}, \Phi) = [B']_{\downarrow pi} = [[B'_{\downarrow pi}]_{\downarrow pi} \mathcal{R} B'_{\downarrow pi}] \overset{\star}{\rightleftharpoons} B'$$

— case 3 (rule OUT): $\alpha = \bar{\xi}\langle ax_n \rangle$ for some $\xi, \in \mathcal{T}(F, F_0 \cup dom\Phi)$, $ax_n \in \mathcal{AX}$ and:

$$A = (\mathcal{P} \cup \{\bar{u}\langle t \rangle.P\}, \Phi) \quad \text{with } msgu, msgt, msg\xi\Phi \text{ and } \xi\Phi\downarrow = u\downarrow$$

$$A' = (\mathcal{P} \cup \{P\}, \Phi') \quad \text{where } \Phi' = \Phi \cup \{ax_n \mapsto t\} \text{ and } n = |\Phi| + 1$$

Then, by a case analysis on the hypothesis $A \mathcal{R} B$:

— case 3.a : $B = [[A]]_{\downarrow pi}$

Then we can write:

$$B = ([\mathcal{P}]_{\downarrow pi} \cup \{\bar{u}\langle t \rangle. [P]\}, \Phi)$$

and we conclude by remarking that $B \xrightarrow{\bar{\xi}\langle ax_n \rangle} B' = ([\mathcal{P}]_{\downarrow pi} \cup \{[[P]\}\}, \Phi)$ and:

$$A' \overset{\star}{\rightleftharpoons} A'_{\downarrow pi} \mathcal{R} [[A'_{\downarrow pi}]_{\downarrow pi}] = [A']_{\downarrow pi} = ([\mathcal{P}]_{\downarrow pi} \cup \{[[P]\}\}_{\downarrow pi}, \Phi) \overset{\star}{\rightleftharpoons} B'$$

— case 3.b : $A = [[B]]_{\downarrow pi}$ (and $B = B_{\downarrow pi}$)

For the same reason as in case 2.b, we can write:

$$B = (Q \cup \{\bar{u}\langle t \rangle.Q\}, \Phi) \quad \text{with } [[Q]] = P \text{ and } [[Q]]_{\downarrow pi} = \mathcal{P}$$

and we conclude by writing $B \xrightarrow{\bar{\xi}\langle ax_n \rangle} B' = (Q \cup \{Q\}, \Phi)$ and:

$$A' \overset{\star}{\rightleftharpoons} ([Q]_{\downarrow pi} \cup \{[[Q]\}\}_{\downarrow pi}, \Phi) = [B']_{\downarrow pi} = [[B'_{\downarrow pi}]_{\downarrow pi} \mathcal{R} B'_{\downarrow pi}] \overset{\star}{\rightleftharpoons} B'$$

— case 4 (rule (COMM)): $\alpha = \overset{\star}{\rightleftharpoons}$ and:

$$A = (\mathcal{P} \cup \{\bar{u}\langle t \rangle.P, v(x).Q\}, \Phi) \quad \text{with } msgu, msgv, msgt \text{ and } u\downarrow = v\downarrow$$

$$A' = (\mathcal{P} \cup \{P, Q\{x \mapsto t\}\}, \Phi)$$

Then, by a case analysis on the hypothesis $A \mathcal{R} B$:

— case 4.a : $B = [[A]]_{\downarrow pi}$
Then we can write:

$$B = (\llbracket \mathcal{P} \rrbracket_{\downarrow \pi_i} \cup \{\bar{u}\langle t \rangle . \llbracket P \rrbracket, v(x) . \llbracket Q \rrbracket\}, \Phi)$$

and we conclude by remarking that $B \xrightarrow{\tau} B' = (\llbracket \mathcal{P} \rrbracket_{\downarrow \pi_i} \cup \{\llbracket P \rrbracket, \llbracket Q \rrbracket \{x \mapsto t\}\}, \Phi)$ and:

$$A' \overset{\star}{\rightleftharpoons} A'_{\downarrow \pi_i} \mathcal{R} \llbracket A'_{\downarrow \pi_i} \rrbracket_{\downarrow \pi_i} = \llbracket A' \rrbracket_{\downarrow \pi_i} = (\llbracket \mathcal{P} \rrbracket_{\downarrow \pi_i} \cup \{\llbracket P \rrbracket_{\downarrow \pi_i}, \llbracket Q \rrbracket \{x \mapsto t\}_{\downarrow \pi_i}\}, \Phi) \overset{\star}{\rightleftharpoons} B'$$

— case 4.b : $A = \llbracket B \rrbracket_{\downarrow \pi_i}$ (and $B = B_{\downarrow \pi_i}$) and a term $w$ such that $w \downarrow = u \downarrow$ appears in $B$ (syntactically)

In particular $\downarrow u$ is not a fresh name introduced by the translation $\llbracket \cdot \rrbracket$ and we can therefore write:

$$B = (\mathcal{P}' \cup \{\bar{u}\langle t \rangle . P', v(x) . Q'\}, \Phi) \quad \text{with} \quad \llbracket \mathcal{P}' \rrbracket_{\downarrow \pi_i} = \mathcal{P}, \llbracket P' \rrbracket = P \text{ and } \llbracket Q' \rrbracket = Q$$

and we conclude by writing $B \xrightarrow{\tau} B' = (\mathcal{P}' \cup \{P', Q'\{x \mapsto t\}\}, \Phi)$ and:

$$A' \overset{\star}{\rightleftharpoons} (\llbracket \mathcal{P}' \rrbracket_{\downarrow \pi_i} \cup \{\llbracket P' \rrbracket_{\downarrow \pi_i}, \llbracket Q' \rrbracket \{x \mapsto t\}_{\downarrow \pi_i}\}, \Phi) = \llbracket B' \rrbracket_{\downarrow \pi_i} = \llbracket B'_{\downarrow \pi_i} \rrbracket_{\downarrow \pi_i} \mathcal{R} B'_{\downarrow \pi_i} \overset{\star}{\rightleftharpoons} B'$$

— case 4.c : $A = \llbracket B \rrbracket_{\downarrow \pi_i}$ (and $B = B_{\downarrow \pi_i}$) and there exists no term $w$ appearing in $B$ such that $w \downarrow = u \downarrow$ (syntactically)

Then $u$ is a fresh name introduced by $\llbracket \cdot \rrbracket$. We consider the two disjoint cases where it was introduced for the translation of a sum or a circuit:

— If $u \in \mathcal{N}$ is a fresh name generated in order to translate a sum of $B$, or rephrased more formally:

$$B = (Q \cup \{P' + Q'\}, \Phi)$$

$$A = (\llbracket Q \rrbracket_{\downarrow \pi_i} \cup \{\bar{u}\langle u \rangle, u(x) . \llbracket P' \rrbracket, u(x) . \llbracket Q' \rrbracket\}, \Phi) \quad \text{where } x \in \mathcal{X}^1 \text{ but } x \notin \text{vars} P', Q'$$

$$A' = (\llbracket Q \rrbracket_{\downarrow \pi_i} \cup \{\llbracket R \rrbracket, u(x) . \llbracket S \rrbracket\}, \Phi) \quad \text{where } R, S \in \{P', Q'\}, R \neq S$$

We let $B' = (Q \cup \{R\}, \Phi)$ and remark that $B \xrightarrow{\tau} B'$ by the rule CHOICE (if $R = P'$ and $S = Q'$, or $R = Q'$ and $S = P'$). Besides, let us observe that the name $u$ does not appear in $\llbracket Q \rrbracket_{\downarrow \pi_i}$, $\llbracket R \rrbracket$ nor $\Phi$ by construction of $\llbracket \cdot \rrbracket$ and that $u(x)$. $\llbracket S \rrbracket$ is therefore easily seen to be silent in $A'' = (\llbracket Q \rrbracket_{\downarrow \pi_i} \cup \{\llbracket R \rrbracket\}, \Phi)$. In particular it entails that $A' \rightsquigarrow A''$ by the rule simplification which gives the conclusion:

$$A' \rightsquigarrow A'' \overset{\star}{\rightleftharpoons} (\llbracket Q \rrbracket_{\downarrow \pi_i} \cup \{\llbracket R \rrbracket\}_{\downarrow \pi_i}, \Phi) = \llbracket B' \rrbracket_{\downarrow \pi_i} = \llbracket B'_{\downarrow \pi_i} \rrbracket_{\downarrow \pi_i} \mathcal{R} B'_{\downarrow \pi_i} \overset{\star}{\rightleftharpoons} B'$$

— $u \in \mathcal{N}$ is a fresh name generated in order to translate a Choose($x$): this case can be handle analogously to the previous one.
— If $u \in \mathcal{N}$ is a fresh name generated in order to translate a circuit of $B$, or formally:

$$B = (Q \cup \{\vec{x} \leftarrow \Gamma(\vec{b}).P'\}, \Phi)$$

$$A = (\llbracket Q \rrbracket_{\downarrow pi} \cup \{\llbracket \vec{x} \leftarrow \Gamma(\vec{b}).P' \rrbracket\}, \Phi)$$

We call $(c_i)_i$ the private fresh names introduced by the translation $\llbracket \vec{x} \leftarrow \Gamma(\vec{b}).P' \rrbracket$, stressing that none of them appears in $\llbracket Q \rrbracket_{\downarrow pi}$, $\llbracket P' \rrbracket$ nor $\Phi$. Here $u \in \{c_i\}_i$ and we can therefore write:

$$A' = (\llbracket Q \rrbracket_{\downarrow pi} \cup \{\llbracket Q' \rrbracket, \Phi\}) \quad \text{where} \quad (\{\llbracket \vec{x} \leftarrow \Gamma(\vec{b}).P' \rrbracket\}, \Phi) \xrightarrow{\alpha} (\{\llbracket Q' \rrbracket, \Phi\})$$

If the sequence $\vec{b}$ contains a term which is not a message or does not reduce to a boolean, then one easily obtain that $(\{\llbracket Q' \rrbracket, \Phi\}) \overset{\star}{\rightleftharpoons}_{pi} (\mathbb{S}, \Phi)$ where $\mathbb{S}$ is silent in $(\llbracket Q \rrbracket_{\downarrow pi}, \Phi)$ (for that we assume, w.l.o.g. that each input of $\Gamma$ goes through at least one gate). Hence since $\{\vec{x} \leftarrow \Gamma(\vec{b}).P'\}$ is also silent in $(Q, \Phi)$, we conclude with $B' = (Q, \Phi)$.

Otherwise assume that $\text{msg}\vec{b}$ and $\vec{b} \downarrow \subseteq \mathbb{B}$. Then one easily obtain by induction on the number of gates of $\Gamma$ that $(\{\llbracket Q' \rrbracket, \Phi\}) \overset{\star}{\rightleftharpoons}_{pi} (\{\llbracket P' \rrbracket\} \{\vec{x} \mapsto \Gamma(\vec{b})\}\}, \Phi)$ and we conclude by choosing $B' = (Q \cup \{\llbracket P'\{\vec{x} \mapsto \Gamma(\vec{b})\}\}, \Phi\}$.

— case 5 (rules CHOICE, CHOOSE-0, CHOOSE-1 or VALUATE):

The arguments of each of these cases are analogous to priorly-met subcases. ■

In particular note that $A \overset{\star}{\rightleftharpoons} A_{\downarrow pi} \mathcal{R} \llbracket A_{\downarrow pi} \rrbracket_{\downarrow pi} = \llbracket A \rrbracket_{\downarrow pi} \overset{\star}{\rightleftharpoons} \llbracket A \rrbracket$ for all extended processes $A$, hence Lemma D.10.

## D.3 Reductions in the pure calculus

We now formalise and prove the correctness of the reductions intuited in Section 5.5.2.

**For trace equivalence** We define the processes $P(t)$, $A$ and $B$ as follows.

$$P(t) \triangleq c(\vec{x}). \text{Choose}(\vec{y}). v \leftarrow \varphi(\vec{x}, \vec{y}). \bar{c}\langle t \rangle$$

$$A \triangleq P(v) + P(1)$$

$$B \triangleq P(0) + P(1)$$

**PROPOSITION D.13 (Reduction for trace equivalence).** $A \approx_t B \text{ iff } \forall \vec{x}. \exists \vec{y}. \varphi(\vec{x}, \vec{y}) = 0$.

**PROOF.** We do the proof by double implication.

⇒ Suppose that $A \not\approx_t B$. By a quick case analysis, we obtain $B \xrightarrow{\varepsilon} (\{\llbracket P(0) \rrbracket, \emptyset\}) \xrightarrow{\text{tr}} (\emptyset, \{\text{ax}_1 \mapsto 0\})$ where $\text{tr} = c(\vec{t}).\bar{c}\langle\text{ax}_1\rangle$ for some messages $\vec{t}$, such that for all reduction $A \xrightarrow{\text{tr}} (C, \Phi)$ the frames $\{\text{ax}_1 \mapsto 0\}$ and $\Phi$ are not statically equivalent. In particular, for all $\vec{y} \subseteq \mathbb{B}$, by choosing $\Phi = \{\text{ax}_1 \mapsto \varphi(\vec{t}, \vec{y})\}$ reachable from $A$, we obtain $\varphi(\vec{t}, \vec{y}) \neq 0$, hence the result.
\Leftrightarrow\text{Conversely, suppose that exists exists } \vec{x} \subseteq \mathbb{B} \text{ such that } \varphi(\vec{x}, \vec{y}) = 1 \text{ for all } \vec{y} \subseteq \mathbb{B}. \text{ Then the trace } B \stackrel{\varepsilon}{\Rightarrow} (\emptyset, \{\text{ax}_1 \mapsto 0\}) \text{ cannot be matched in } A \text{ and therefore } A \not\models_t B. \blacksquare

**For simulations** We recall that a graphical depiction of the processes has been provided in Section 5.5.2. We fix a family of private channels $(c_p)_p \subseteq \mathcal{N}$ indexed by processes $P$ which will be used to simulate instructions $\text{Goto } \langle P \rangle$. We use a shortcut $\overline{d\langle \vec{t}^p \rangle}$ for an indexed sequence of terms $(t_i)_i$ to denote the sequence of outputs:

$$ \overline{d\langle \vec{t}^p \rangle} \triangleq \overline{d\langle t_1 \rangle} \dots \overline{d\langle t_p \rangle} $$

and a similar notation for sequences of inputs. Then the Goto feature is implemented as follows, allowing for passing and receiving program states through parallel processes:

$$ \begin{array}{l@{\qquad}l} \text{Goto } \langle A_i \rangle & \triangleq \overline{c_{A_i}} \langle \vec{x}^i, \vec{y}^i \rangle & \text{Goto } \langle B_i \rangle \triangleq \overline{c_{B_i}} \langle \vec{x}^i, \vec{y}^i \rangle \\ \text{GetEnv } \langle A_i \rangle . P \triangleq c_{A_i} (\vec{x}^i, \vec{y}^i) & & \text{GetEnv } \langle B_i \rangle . P \triangleq c_{B_i} (\vec{x}^i, \vec{y}^i) \end{array} $$

Formally the processes $A_i$, $B_i$ and $D_i$ are defined below. We stress out that $A$ and $B$ are closed (as required) but that $A_i$, $B_i$ and $D_i$ are not in general. Fixing a public channel $c \in \mathcal{F}_0$, we write:

$$ \begin{align*} \forall i \le n, A_i &\triangleq c(x_i). x_i \leftarrow x_i. D_i \\ \forall i \le n, B_i &\triangleq c(x_i). x_i \leftarrow x_i. (D_i + (c(y_i). y_i \leftarrow y_i. \text{Goto } \langle B_{i+1} \rangle)) \\ A_{n+1} &\triangleq v \leftarrow \varphi(\vec{x}, \vec{y}). \overline{c}\langle v \rangle \\ B_{n+1} &\triangleq \overline{c}\langle 0 \rangle \\ D_i &\triangleq \text{Choose}(z_i). c(y_i). r_i \leftarrow (y_i = z_i). \\ &\quad ((\text{if } r_i = 1 \text{ then } \text{Goto } \langle A_{i+1} \rangle) \\ &\quad \mid (\text{if } r_i = 0 \text{ then } c(y_i). y_i \leftarrow y_i. \text{Goto } \langle B_{i+1} \rangle)) \end{align*} $$

As in the reduction for trace equivalence, the Choose($\alpha$) simulates non-deterministic choice among $\mathbb{B}$; the construction $\alpha \leftarrow \alpha$, which may seem useless, encodes the test $\alpha \in \mathbb{B}$. Finally, we define $A$ and $B$ by putting the auxiliary processes in parallel and connecting the Goto's to the getEnv's:

$$ A \triangleq A_1 | C \qquad B \triangleq B_1 | C \qquad C \triangleq \prod_{i=2}^{n+1} (\text{GetEnv } \langle A_i \rangle . A_i) \mid \prod_{i=2}^{n+1} (\text{GetEnv } \langle B_i \rangle . B_i) $$

$A$ and $B$ can be computed in time $O(n^2 + |\varphi|)$ in a straightforward way. The formal proof of the reduction is detailed below.

**PROPOSITION D.14 (Correctness of the reduction).** The following statements are equivalent:
1. $A \approx_b B$

2. $A \approx_s B$

3. $\forall x_1 \exists y_1 \dots \forall x_n \exists y_n. \varphi(x_1, \dots, x_n, y_1, \dots, y_n) = 0$

**PROOF.** We recall that, again, our proof uses the advanced winning strategy framework presented in Section D.1.

1) $\Rightarrow$ 2) Follows from the inclusion $\approx_b \subset \approx_s$.

3) $\Rightarrow$ 1) Suppose that $\forall x_1 \exists y_1 \dots \forall x_n \exists y_n. \varphi(x_1, \dots, x_n, y_1, \dots, y_n) = 1$. For convenience we use a notation for subprocess extraction: is $\ell$ is a position of a process $C$, then the subprocess of $C$ at position $\ell$ (which may not be closed) is denoted by $C|_\ell$. Then writing in addition:

$$C_i = \prod_{j=i+1}^{n+1} (\text{GetEnv} \langle A_j \rangle . A_j) \mid \prod_{j=i+1}^{n+1} (\text{GetEnv} \langle B_j \rangle . B_j)$$

we define $\mathcal{R}$ the smallest reflexive symmetric relation on closed extended processes such that:

1. $(A_i | C_i)(\vec{x}^{i-1}, \vec{y}^{i-1}) \mathcal{R} (B_i | C_i)(\vec{x}^{i-1}, \vec{y}^{i-1})$ if $\forall x_i \exists y_i \dots \forall x_n \exists y_n, \varphi(\vec{x}, \vec{y})$.

2. $(A_{i|\ell} | C_i)(\vec{x}^i, \vec{y}^{i-1}) \mathcal{R} (B_{i|\ell} | C_i)(\vec{x}^{i-1}, \vec{y}^{i-1})$ if $\ell \in \{0, 0.0\}$ and $\exists y_i \dots \forall x_n \exists y_n, \varphi(\vec{x}, \vec{y})$.

3. $(B_{i|0.0.1.\ell} | C_i)(\vec{x}^i, \vec{y}^i) \mathcal{R} (D_{i|0.\ell} | C_i)(\vec{x}^i, \vec{y}^i)$ if $\ell \in \{\varepsilon, 0\}$ and $\forall x_{i+1} \exists y_{i+1} \dots \forall x_n \exists y_n, \varphi(\vec{x}, \vec{y})$.

Then one can verify that $\mathcal{R}$ is a bisimulation up to $\rightsquigarrow$, and $A \mathcal{R} B$ by hypothesis, hence the $A \approx_b B$.

2) $\Rightarrow$ 3) By contraposition, if we suppose that $\exists x_1 \forall y_1 \dots \exists x_n \forall y_n. \varphi(x_1, \dots, x_n, y_1, \dots, y_n) = 1$, then one can define a labelled attack $\mathcal{S}$ (valid against simulation) such that $B \mathcal{S} A$. We omit the concrete construction as it is analogous to that of $\mathcal{R}$ above; all in all this gives the conclusion $A \not\approx_s B$. ■

## D.4 Reduction in the full calculus

Before concretely proving the pending lemmas, let us introduce some notations and prove intermediary results about static equivalence. We fix a private nonce $s \in \mathcal{N}$ and define the following frames given a protocol term $t$:

$$\Phi_t = \{ax_1 \mapsto h(t, s), ax_2 \mapsto h(1, s)\}$$

$$\Phi_t^N = \{ax_1 \mapsto h_N(t, s), ax_2 \mapsto h(1, s)\}$$

$$\Phi_t^B = \{ax_1 \mapsto h_B(t, s), ax_2 \mapsto h(1, s)\}$$
One shall observe that the whole deal with our reduction is about which instances of these three frames are reachable in which conditions. Hence first we prove a lemma investigating the static equivalence between some of them:

**LEMMA D.15.** Let $t$ be a message in normal form ($t = t\downarrow$). The following properties hold:

(i) $\Phi_t \sim \Phi_0$ iff $t \neq 1$

(ii) $\Phi_t^N \sim \Phi_0$ iff $\text{root}(t) \neq \text{Node}$

(iii) $\Phi_t^B \sim \Phi_0$ iff $t \notin B$

**PROOF.** We prove the three equivalences together by double implication.

(⇒) We prove the three properties by contraposition. We naturally proceed by exhibiting ground recipes $\xi$, $\zeta$ witnessing the non-static-equivalence goal:

• (i) We assume $t = 1$ and we choose $\xi = ax_1$ and $\zeta = ax_2$: the conclusion follows from $\xi\Phi_t\downarrow = h(1, s) = \zeta\Phi_t\downarrow$ and $\xi\Phi_0\downarrow = h(0, s) \neq h(1, s) = \zeta\Phi_0\downarrow$.

• (ii) We assume $t = \text{Node}(t_1, t_2)$ and we choose $\xi = \text{TestNode}(ax_1)$: the conclusion follows from $\text{msg}\xi\Phi_t^N$ and $\neg\text{msg}\xi\Phi_0^N$.

• (iii) We assume $t \in \{0, 1\}$ and we choose $\xi = \text{TestBool}(ax_1)$: the conclusion follows from $\text{msg}\xi\Phi_t^B$ and $\neg\text{msg}\xi\Phi_0^B$.

($\Leftarrow$) The key point is an observation about rewriting critical pairs (not specific to $\mathcal{R}$):

if: $u$ is a term;

if: $\sigma$ is a substitution such that for any $m \in \text{img}(\sigma)$ there exists no rule $\ell \to r$ of $\mathcal{R}$ such that $m$ is unifiable with a subterm $u \in st\ell - \mathcal{X}$;

then: for any rewriting sequence $u\sigma \to^* s$, it holds that $s = u'\sigma$ for some $u \to^* u'$ (where $u'$ is in normal form iff $s$ is in normal form. In particular $(u\sigma)\downarrow = (u\downarrow)\sigma$).

One shall note that any frame $\Phi$ investigated by the lemma ($\Phi_t$ when $t \neq 1$, $\Phi_t^N$ when $\text{roott} \neq \text{Node}$ and $\Phi_t^B$ when $t \notin B$) verifies the second hypothesis. As a consequence, if $\xi$ is a ground recipe such that axioms $\xi \subseteq \text{dom}(\Phi)$, then $\text{msg}\xi\Phi$ iff $\text{msg}\xi\Phi_0$ (iff $\forall \zeta \in st\xi$, $\zeta\downarrow \in \mathcal{T}(F_c, F_0 \cup \mathcal{AX})$). This settles the first item of the definition of static equivalence. As for the second item, let us fix two ground recipes $\xi, \zeta$ such that $\text{msg}\xi\Phi$ and $\text{msg}\xi\Phi_0$. Let us then prove that $\xi\Phi\downarrow = \zeta\Phi\downarrow$ iff $\xi\Phi_0\downarrow = \zeta\Phi_0\downarrow$ by induction on $(\xi\downarrow, \zeta\downarrow)$. Note that we will intensively (and implicitly) use the fact that $\xi\Phi\downarrow = (\xi\downarrow)\Phi$ (same for $\zeta$ and/or $\Phi_0$).

• **case 1**: $\xi\downarrow = f(\xi_1, \dots, \xi_n)$ and $\zeta\downarrow = f(\zeta_1, \dots, \zeta_p)$ with $f, g \in F_c$.

If $f = g$ then the result follows from induction hypothesis and if $f \neq g$ the conclusion is immediate $(\xi\Phi\downarrow \neq \zeta\Phi\downarrow$ and $\xi\Phi_0\downarrow \neq \zeta\Phi_0\downarrow)$.

• **case 2**: $\xi\downarrow \in \mathcal{AX}$ and $\zeta\downarrow \in \mathcal{AX}$.

If $\xi = \zeta$ the conclusion is immediate and so is it when $\xi \neq \zeta$ since $\Phi(ax_1) \neq \Phi(ax_2)$ and $\Phi_0(ax_1) \neq \Phi_0(ax_2)$.

• **case 3**: $\xi\downarrow \in \mathcal{AX}$ and $\zeta\downarrow = f(\zeta_1, \dots, \zeta_p)$ with $f \in F_c$.
We argue that $\xi\Phi\downarrow \neq \zeta\Phi\downarrow$ and $\xi\Phi_0\downarrow \neq \zeta\Phi_0\downarrow$. Either of the two equalities being verified would indeed imply that $s \in \{\zeta_2\Phi, \zeta_2\Phi_0\}$: this is impossible as $\zeta_2$ is a ground recipe in normal form and $s \in \mathcal{N}$ (one easily shows that $\zeta_2\Phi$ and $\zeta_2\Phi_0$ are either public names, constants, or terms of height 1 or more).

As $msg\xi\Phi$ and $msg\xi\Phi_0$, the preliminary observation justifies that $\xi\downarrow$ and $\zeta\downarrow$ function symbols are all constructor. In particular no other cases than the three above need to be considered, which concludes the proof. ■

With this lemma in mind, the proofs of Propositions 5.21 and 5.22 become quite straight-forward:

**PROPOSITION 5.21 (correctness of the tree checker).** Let $x$ be a message which is not a complete binary tree of height $n$ with boolean leaves. Then there exists a reduction $CheckTree(x) \stackrel{\epsilon}{\Rightarrow} (\{P\}, \emptyset)$ such that $P \approx_b \bar{c}\langle h(0, s) \rangle \cdot \bar{c}\langle h(1, s) \rangle$.

**PROOF.** Let $x$ be a message which is not a complete binary tree of height $n$ whose leaves are booleans.

**case 1:** there exists a position $\vec{\pi} \in \mathbb{B}^*$ such that $|\vec{\pi}| = i \in [0, n-1]$ and $\mathrm{rootx}_{|\vec{\pi}|} \neq \mathrm{Node}$. The result follows from Lemma D.15 after writing the following sequence of transitions:

$$ \begin{align*} \mathrm{CheckTree}(x) &\stackrel{\epsilon}{\Rightarrow} \mathrm{Choose}(p_1, \dots, p_i) \cdot \bar{c}\langle h_N(x_{|p_1\dots p_i}, s) \rangle \cdot \bar{c}\langle h(1, s) \rangle \\ &\stackrel{\epsilon}{\Rightarrow} \bar{c}\langle h_N(x_{|\vec{\pi}|}, s) \rangle \cdot \bar{c}\langle h(1, s) \rangle \end{align*} $$

**case 2:** there exists a position $\vec{\pi} \in \mathbb{B}^n$ such that $x_{|\vec{\pi}|} \notin \mathbb{B}$.

The result follows from Lemma D.15 after writing the following sequence of transitions:

$$ \begin{align*} \mathrm{CheckTree}(x) &\stackrel{\epsilon}{\Rightarrow} \mathrm{Choose}(p_1, \dots, p_n) \cdot \bar{c}\langle h_N(x_{|p_1\dots p_n}, s) \rangle \cdot \bar{c}\langle h(1, s) \rangle \\ &\stackrel{\epsilon}{\Rightarrow} \bar{c}\langle h_{\mathbb{B}}(x_{|\vec{\pi}|}, s) \rangle \cdot \bar{c}\langle h(1, s) \rangle \end{align*} $$

**PROPOSITION 5.22 (correctness of the sat checker).** Let $x$ be a complete binary tree of height $n$ whose leaves are booleans, and $\mathrm{val}_x$ be the valuation mapping the variable number $i$ of $[[\Gamma]]_\phi$ to $x_{|p_1\dots p_n} \in \mathbb{B}$ where $p_1 \dots p_n$ is the binary representation of $i$ (i.e., $i = \sum_{k=1}^n p_k 2^{k-1}$). If $\mathrm{val}_x$ does not satisfy $[[\Gamma]]_\phi$ then there exists $\mathrm{CheckSat}(x) \stackrel{\epsilon}{\Rightarrow} P$ such that $P \approx_b \bar{c}\langle h(0, s) \rangle \cdot \bar{c}\langle h(1, s) \rangle$.

**PROOF.** Let $x$ be a complete binary tree of height $n$ whose leaves are booleans, that is to say, a message such that $x_{|\vec{p}} \in \mathbb{B}$ for all $\vec{p} \in \mathbb{B}^n$. Naming $x_0, \dots, x_{2^n-1}$ the variables of $[[\Gamma]]_\phi$ in this order, $\mathrm{val}_x$ refers to the valuation mapping $x_i$ to $x_{|\vec{p}}$ where $\vec{p}$ is the binary representation of $i$ (of size $n$ with padding head 0's).