We have that:

$$N_2 \xrightarrow{m_1} \nu \tilde{u}, k'. (\kappa_1 : a\langle P \rangle) | (\kappa_2 : a(X) \triangleright Q) | m'_2 | k' : Q'\{P'/X\} | \\ \prod_{i \in I''} \kappa_i : \rho_i | \prod_{j \in J''} m_j$$

$$N_1 \xrightarrow{m_2} \nu \tilde{u}, k'. (\kappa_1 : a\langle P \rangle) | (\kappa_2 : a(X) \triangleright Q) | m'_2 | k' : Q'\{P'/X\} | \\ \prod_{i \in I''} \kappa_i : \rho_i | \prod_{j \in J''} m_j$$

as desired.

* $M \xrightarrow{m_1} N_1$ and $M \xrightarrow{m_2} N_2$, similar to the case above.

* $M \xrightarrow{m_1} N_1$ and $M \xrightarrow{m_2} N_2$, similar to the first case.

□

**Lemma 10 (Rearranging lemma).** Let $\sigma$ be a trace. There exist forward traces $\sigma'$ and $\sigma''$ such that $\sigma \asymp \sigma'_{\bullet}; \sigma''_{\bullet}$.

**PROOF.** The proof is by lexicographic induction on the length of $\sigma$ and on the distance between the beginning of $\sigma$ and the earliest pair of transitions in $\sigma$ of the form $t; t'_{\bullet}$ (where $t$ and $t'$ are forward). If there is no such pair we are done. If there is one, we have two possibilities: either $t$ and $t'$ are concurrent, or they are in conflict. In the first case, we can swap them by using Lemma 9, resulting in a later earliest contradicting pair, and by induction the result follows since swapping transitions keeps the total length constant. In the second case we have that there is a conflict on a tag $\kappa$. We have two cases: either the memory involved in the two transitions is the same or not. In the first case we have $t = t'$, and we can apply the Loop lemma removing $t; t'_{\bullet}$. Hence the total length of $\sigma$ decreases and again by induction the result follows. In the second case thanks to the property of well-formed configurations the only possible conflict is between the thread tag of a memory and a tag in the configuration part of the other memory. Assume a conflict between the thread tag of memory $m$ of transition $t$ and a tag in the configuration part of memory $m'$ of transition $t'_{\bullet}$. In this case $t$ has created a memory of the form $[\delta_1 : a\langle P \rangle | \gamma_1 : a(X) \triangleright Q; k_1]$ and a process $k_1 : R$. Thus from conditions 1 and 4 in the definition of well-formed
configuration this case never happens. Assume now the opposite case: a
conflict between the thread tag of memory $m'$ and a tag in the configuration
part of memory $m$. In this case transition $t'_•$ deletes a memory of the form
$[\delta_2 : a\langle P \rangle | \gamma_2 : a(X)\triangleright Q; k_2]$, but this requires having a process $k_2 : R$. Again
from conditions 1 and 4 this case never happens.
□

**Lemma 11 (Shortening lemma).** Let $\sigma_1, \sigma_2$ be coinitial and cofinal traces, with $\sigma_2$ forward. Then, there exists a forward trace $\sigma'_1$ of length at most that of $\sigma_1$ such that $\sigma'_1 \asymp \sigma_1$.

PROOF. We prove this lemma by induction on the length of $\sigma_1$. If $\sigma_1$ is a forward trace we are already done.

Otherwise by Lemma 10 we can write $\sigma_1$ as $\sigma_•; \sigma'$ (with $\sigma$ and $\sigma'$ forward). Let $t_•; t'$ be the only two successive transitions in $\sigma_1$ with opposite direction, with $m_1$ belonging to $t_•$. Since $m_1$ is removed by $t_•$ then $m_1$ has to be put back by another forward transition otherwise this difference will stay visible since $\sigma_2$ is a forward trace. Let $t_1$ be the earliest such transition in $\sigma_1$. Since it is able to put back $m_1$ it has to be the exact opposite of $t_•$, so $t_1 = t$. Now we can swap $t_1$ with all the transitions between $t_1$ and $t_•$, in order to obtain a trace in which $t_1$ and $t_•$ are adjacent. To do so we use the Square Lemma (Lemma 9), since all the transitions in between are concurrent. Assume in fact that there is a transition involving memory $m_2$ which is not concurrent to $t_1$, with $\lambda(m_1) = \{\delta_1, \gamma_1, k_1\}$, $\lambda(m_2) = \{\delta_2, \gamma_2, k_2\}$. Thanks to consistency conditions the only possible conflicts are (1) between $k_1$ and $\delta_2$ or between $k_1$ and $\gamma_2$ or (2) between $k_2$ and $\delta_1$ or $k_2$ and $\gamma_1$. The first case can never happen since $k_1$ is fresh (generated by the forward rule) and thus cannot coincide nor been a prefix of $\gamma_2$ or $\delta_2$. Similarly the second case can never happen since $k_2$ is fresh and thus cannot occur in $m_1$. When $t_•$ and $t$ are adjacent we can remove both of them using $\asymp$. The resulting trace is shorter, thus the thesis follows by inductive hypothesis.
□

**Theorem 1 (Causal consistency).** Let $\sigma_1$ and $\sigma_2$ be coinitial traces, then $\sigma_1 \asymp \sigma_2$ if and only if $\sigma_1$ and $\sigma_2$ are cofinal.

PROOF. By construction of $\asymp$, if $\sigma_1 \asymp \sigma_2$ then $\sigma_1$ and $\sigma_2$ must be coinitial and cofinal, so this direction of the theorem is verified. Now we have to prove that $\sigma_1$ and $\sigma_2$ being coinitial and cofinal implies that $\sigma_1 \asymp \sigma_2$. By Lemma 10 we know that the two traces can be written as composition of a backward
trace and a forward one. The proof is by lexicographic induction on the sum
of the lengths of $\sigma_1$ and $\sigma_2$ and on the distance between the end of $\sigma_1$ and
the earliest pair of transitions $t_1$ in $\sigma_1$ and $t_2$ in $\sigma_2$ which are not equal. If all
the transitions are equal then we are done. Otherwise we have to consider
three cases depending on the direction of the two transitions.

$t_1$ **forward and $t_2$ backward:** we have $\sigma_1 = \sigma_\bullet; t_1; \sigma'$ and $\sigma_2 = \sigma_\bullet; t_2; \sigma''$.
Moreover we know that $t_1; \sigma'$ is a forward trace, so we can apply the
Lemma 11 to the traces $t_1; \sigma'$ and $t_2; \sigma''$ (since $\sigma_1$ and $\sigma_2$ are coinitial
and cofinal by hypothesis, also $t_1; \sigma'$ and $t_2; \sigma''$ are coinitial and cofinal)
and we obtain that $t_2; \sigma''$ has a shorter equivalent forward trace and
so also $\sigma_2$ has a shorter equivalent forward trace. We can conclude by
induction.

$t_1$ **and $t_2$ forward:** by assumption the two transitions are different. If they
are not concurrent then they should conflict on a thread process $\kappa : P$
that they both consume and store in different memories. Since the two
traces are cofinal there should be $t'_2$ in $\sigma_2$ creating the same memory as
$t_1$. However no other process $\kappa : P$ is ever created in $\sigma_2$ thus this is not
possible. So we can assume that $t_1$ and $t_2$ are concurrent. Again let
$t'_2$ be the transition in $\sigma_2$ creating the same memory of $t_1$. We have to
prove that $t'_2$ is concurrent to all the previous transitions. This holds
since no previous transition can remove one of the processes needed
for triggering $t'_2$ and since forward transitions can never conflict on
$k$. Thus we can repetitively apply the Square Lemma to derive a trace
equivalent to $\sigma_2$ where $t_2$ and $t'_2$ are consecutive. We can apply a similar
transformation to $\sigma_1$. Now we can apply the Square Lemma to $t_1$ and
$t_2$ to have two traces of the same length as before but where the first
pair of different transitions is closer to the end. The thesis follows by
inductive hypothesis.

$t_1$ **and $t_2$ backward:** $t_1$ and $t_2$ cannot remove the same memory. Let $m_1$
be the memory removed by $t_1$. Since the two traces are cofinal, either
there is another transition in $\sigma_1$ putting back the memory or there is
a transition $t'_1$ in $\sigma_2$ removing the same memory. In the first case, $t_1$
is concurrent to all the backward transitions following it, but the ones
that consume processes generated by it. All the transitions of this kind
have to be undone by corresponding forward transitions (since they are
not possible in $\sigma_2$). Consider the last such transition: we can use the
Square Lemma to make it the last backward transition. The forward transition undoing it should be concurrent to all the previous forward transitions (the reason is the same as in the previous case). Thus we can use the Square Lemma to make it the first forward transition. Finally we can apply the simplification rule $t_{\bullet}; t \asymp \epsilon_{\text{target}(t)}$ to remove the two transitions, thus shortening the trace. The thesis follows by inductive hypothesis.

□

## Appendix B.2. Proofs of Section 3.2

### Appendix B.2.1. Labelled transition system semantics for $cho\pi$

In [21], Boreale and Sangiorgi do not define their causal $\pi$-calculus via a reduction semantics but with a labelled transition system. To show that our notion of causal process indeed corresponds to that of Boreale and Sangiorgi, we present here a labelled transition system semantics for $cho\pi$ directly adapted from [21] to our higher-order context. We then prove that the labelled transition system semantics and the reduction semantics for $cho\pi$ are in agreement.

The labelled transition system semantics of $cho\pi$ is given in Figure B.16, where $\alpha$ ranges over channel names $a$ and their complements of the form $\bar{a}$. The rules in Figure B.16 are a direct adaptation of the rules in [21] to the asynchronous higher-order $\pi$, with the use of concretions and abstractions, following Milner and Sangiorgi [15, 17]. A concretion takes the form $\nu\tilde{a}. \langle P \rangle A$, where $\tilde{a} \subseteq \mathbf{fn}(P)$. An abstraction takes the form $(X)A$. We use $C, D$ and their decorated variants to range over concretions, and $F, G$ and their decorated variants to range over abstractions. We call agent an abstraction, a concretion or a causal process, and by abuse of notation, we also use $A, B$ and their decorated variants to range over agents. The application operator $\bullet$ is defined by the following rule (where by convention $\tilde{a} \cap \mathbf{fn}(A) = \emptyset$):

$$ (X)A \bullet \nu\tilde{a}. \langle P \rangle B = \nu\tilde{a}. A^{\{P/X\}} | B $$

In addition, we define in Figure B.17 operations $\nu a. A$, $A | B$, $B | A$, and $K :: A$ for arbitrary agents $A$ and causal processes $B$. Finally, we define inductively the operation of substitution of a key $k$ by a set of keys $K$ in a
<figure><img src="image_15.png" /><figcaption>Figure B.16: Transition system rules for choπ</figcaption></figure>

causal process as follows:

$$ (K' \cup \{k\})^{K/\kappa} = K' \cup K \qquad \text{if } k \notin K' $$

$$ K'_{\{K/\kappa\}} = K' \qquad \text{if } k \notin K' $$

$$ P^{K/\kappa} = P $$

$$ (K' :: A)_{\{K/\kappa\}} = K'_{\{K/\kappa\}} :: A_{\{K/\kappa\}} $$

$$ (\nu a. A)_{\{K/\kappa\}} = \nu a. (A_{\{K/\kappa\}}) $$

$$ (A_1 | A_2)_{\{K/\kappa\}} = (A_1_{\{K/\kappa\}}) | (A_2_{\{K/\kappa\}}) $$

The agreement between the two semantics is given by the following result.

**Proposition 2.** $A \xrightarrow{\tau} A'$ if and only if $A \to A'$.
$$ \nu a. ((X)A) = (X)\nu a. A \qquad \nu a. (\nu \tilde{c}. \langle P \rangle A) = \nu a, \tilde{c}. \langle P \rangle A \quad \text{if } a \in \mathbf{fn}(P) $$

$$ \nu a. (\nu \tilde{c}. \langle P \rangle A) = \nu \tilde{c}. \langle P \rangle \nu a. A \quad \text{if } a \notin \mathbf{fn}(P) $$

$$ ((X)A) | B = (X)(A | B) \qquad B | ((X)A) = (X)(B | A) $$

$$ (\nu c. \langle P \rangle A) | B = \nu c. \langle P \rangle (A | B) \qquad B | (\nu c. \langle P \rangle A) = \nu c. \langle P \rangle (B | A) $$

$$ K :: ((X)A) = (X)K :: A \qquad K :: (\nu c. \langle P \rangle A) = \nu c. \langle P \rangle K :: A $$

<caption>Figure B.17: Operations on agents</caption>

The proof of this proposition is long but completely standard. We give details below.

Note that, thanks to the agreement with the reduction semantics, $A \downarrow_{K::\alpha}$ if and only if $A \xrightarrow{\alpha}_{K;k} A'$ for some $k, A'$.

### Appendix B.2.2. Proof of Proposition 2

We prove in this section the equivalence between the labelled transition system semantics and the reduction semantics for $cho\pi$. We start with a few additional notions used in the proofs.

We extend the structural congruence relation $\equiv$ to agents using the additional rules below (considering that rule E.α extends to agents as well):

$$ (\text{E-CNC}) \qquad \frac{P \equiv Q \qquad A \equiv B}{\nu \tilde{a}. \langle P \rangle A \equiv \nu \tilde{a}. \langle Q \rangle B} \qquad (\text{E-Abs}) \qquad \frac{A \equiv B}{(X)A \equiv (X)B} $$

An easy induction on the derivation of $A \equiv B$ gives us the following lemmas.

**Lemma 43.** For all agents A, B and process P, if $A \equiv B$ then $A^{\{P/X\}} \equiv B^{\{P/X\}}$.

**Lemma 44.** For all agents A, B, $A \equiv B$ implies $A^{\{K/k\}} \equiv B^{\{K/k\}}$.

Using Lemma 44, an easy induction on the structure of a causal process gives us the following lemma:
**Lemma 45.** For all causal processes $A, k \notin K$, $(K :: A)\{K \cup K' / k\} \equiv K :: A\{K' / k\}$.

**Lemma 46.** If $F \equiv F'$ and $C \equiv C'$, then $F \bullet C \equiv F' \bullet C'$.

**PROOF.** We must have $C = \nu\tilde{a} \cdot \langle P \rangle A_2$, $F = (X)A_1$, $C' = \nu\tilde{a} \cdot \langle P' \rangle A'_2$, $F' = (X)A'_1$, with $P \equiv P'$, $A_1 \equiv A'_1$ and $A_2 \equiv A'_2$. Now

$$ 
\begin{align*}
F \bullet C &= A_1\{P/X\} | A_2 && \text{definition of } \bullet \\
&\equiv A_1\{P'/X\} | A_2 && \text{congruence of } \equiv \\
&\equiv A'_1\{P'/X\} | A'_2 && \text{Lemma 43 and congruence of } \equiv \\
&= F' \bullet C' && \text{definition of } \bullet
\end{align*}
$$

□

**Lemma 47.** For all agents $F, C, K :: (F \bullet C) \equiv (K :: F) \bullet (K :: C)$

**PROOF.** Let $F = (X)A$ and $C = \nu\tilde{c} \cdot \langle P \rangle B$. We compute:

$$ 
\begin{align*}
K :: (F \bullet C) &= K :: \nu\tilde{c} \cdot A\{P/X\} | B \equiv \nu\tilde{c} \cdot K :: A\{P/X\} | K :: B \\
(K :: F) \bullet (K :: C) &= ((X)K :: A) \bullet (\nu\tilde{c} \cdot K :: B) = \nu\tilde{c} \cdot K :: A\{P/X\} | K :: B
\end{align*}
$$

□

An easy induction on the derivation of $A \xrightarrow{\alpha} A'$ gives us the following lemma:

**Lemma 48.** For any causal process $A$, and any keys $k, k'$, if $A \xrightarrow{\alpha} A'$, then $A \xrightarrow{\alpha} A'$.

We can then prove the main lemmas towards the agreement proposition:

**Lemma 49.** For all $A, A', B, \alpha, K, k$, if $A \xrightarrow{\alpha} A'$ and $B \equiv A$, then there exists $B' \equiv A'$ such that $B \xrightarrow{\alpha} B'$.

**PROOF.** The proof is lengthy but completely standard. It proceeds by induction on the derivation of $B \equiv A$. We just detail the non-classical cases arising from the rules in Figure 4.
* (E-PAR): in this case, $A = K' :: A_1 | A_2$ and $B = K' :: A_1 | K :: A_2$. $A \xrightarrow{\alpha}_{K;k} A'$ can only have been derived via (CAU), with $A_1 | A_2 \xrightarrow{\alpha}_{K'';k} A''$ and $K = K' \cup K'', A' = K' :: A''$. In turn, $A_1 | A_2 \xrightarrow{\alpha}_{K'';k} A''$ can only have been derived via (E-PARL) or (E-PARR). We check only the case (E-PARL) as the other is similar. We thus have $A_1 \xrightarrow{\alpha}_{K'';k} A'_1$ with $A'' = A'_1 | A_2$. Using rule (CAU), we now have $K' :: A_1 \xrightarrow{\alpha}_{K' \cup K'';k} K' :: A'_1$. Using rule (PARL), we obtain

$$B = K' :: A_1 | K' :: A_2 \xrightarrow{\alpha}_{K;k} K' :: A'_1 | K' :: A_2$$

By (E-PAR), we have $K' :: A'_1 | K' :: A_2 \equiv K' :: A'_1 | A_2 = A'$, and thus we have found $B' = K' :: A'_1 | K' :: A_2$, such that $B \xrightarrow{\alpha}_{K;k} B'$ and $B' \equiv A'$, as required.

* (E-CAU): in this case, $A = K_1 :: K_2 :: A_1$ and $B = K_1 \cup K_2 :: A_1$. $A \xrightarrow{\alpha}_{K;k} A'$ can only have been derived via (CAU), with $K_2 :: A_1 \xrightarrow{\alpha}_{K'_1;k} A'_1$ and $K = K_1 \cup K'_1$, $A' = K_1 :: A'_1$. In turn, the latter transition can only have been obtained via (CAU), with $A_1 \xrightarrow{\alpha}_{K'_2;k} A''_1$ and $K'_1 = K_2 \cup K'_2$, $A'_1 = K_2 :: A''_1$. Using (CAU) we get $K_1 \cup K_2 :: A_1 \xrightarrow{\alpha}_{K_1 \cup K_2 \cup K'_2;k} K_1 \cup K_2 :: A''_1$ and thus $B = K_1 \cup K_2 :: A_1 \xrightarrow{\alpha}_{K;k} K_1 \cup K_2 :: A''_1$. By rule (E-CAU), we have $K_1 \cup K_2 :: A''_1 \equiv K_1 :: K_2 :: A''_1 = A'$, and thus we have found $B' = K_1 \cup K_2 :: A''_1$ such that $B \xrightarrow{\alpha}_{K;k} B'$ and $B' \equiv A'$, as required.

* (E-RES): in this case, $A = K' :: \nu a. A_1$ and $B = \nu a. K' :: A_1$. $A \xrightarrow{\alpha}_{K;k} A'$ can only have been derived via (CAU), with $\nu a. A_1 \xrightarrow{\alpha}_{K'';k} A''$, $K = K' \cup K''$, and $A' = K' :: A''$. In turn, the latter transition can only have been derived via (RES), with $A_1 \xrightarrow{\alpha}_{K'';k} A'_1$, $a \neq \text{fn}(\alpha)$, and $A'' = \nu a. A'_1$. Using (CAU) we get $K' :: A_1 \xrightarrow{\alpha}_{K' \cup K'';k} K' :: A'_1$, and using (RES) we get $B = \nu a. K' :: A_1 \xrightarrow{\alpha}_{K;k} \nu a. K' :: A'_1$. By (E-RES) we get $\nu a. K' :: A'_1 \equiv K' :: \nu a. A'_1 = A'$, and thus we have found $B' = \nu a. K' :: A'_1$ such that $B \xrightarrow{\alpha}_{K;k} B'$ and $B' \equiv A'$, as required.
• (E-NIL): in this case, $A = \emptyset :: B$. $A \xrightarrow{\alpha}_{K;k}$ $A'$ can only have been derived via (CAU), with $B \xrightarrow{\alpha}_{K;k}$ $B'$ and $A' = \emptyset :: B'$. Now by (E-NIL) we have $A' \equiv B'$, as required.

□

**Lemma 50.** For all $A, A', B$, if $A \xrightarrow{\tau} A'$ and $A \equiv B$, then there exists $B' \equiv A'$ such that $B \xrightarrow{\tau} B'$.

**PROOF.** The proof proceeds by induction on the derivation of $A \equiv B$. Again, we give details only for the non-classical cases arising from the rules in Figure 4.

• (E.PAR): in this case, $A = K :: A_1 | A_2$ and $B = K :: A_1 | K :: A_2$. $A \xrightarrow{\tau} A'$ can only have been derived via (T-CAU), with $A_1 | A_2 \xrightarrow{\tau} A''$ and $A' = K :: A''$. In turn, the latter transition could only have been derived via (T-PARL), (T-PARR), (COML), or (COMR). We check the different cases:

- (T-PARL): in this case, we have $A_1 \xrightarrow{\tau} A'_1$, $A'' = A'_1 | A_2$, and $A' = K :: A'_1 | A_2$. Applying (T-CAU) and (T-PARL), we get $B \xrightarrow{\tau} K :: A'_1 | K :: A_2$. Now, by (E-CAU) $K :: A'_1 | K :: A_2 \equiv K :: A'_1 | A_2 = A'$, hence we have found $B' = K :: A'_1 | K :: A_2$ as required.

- (T-PARR): this case is similar to the (T-PARL) one.

- (COML): in this case, $A_1 \xrightarrow{\bar{a}}_{K_1;k} C$, $A_2 \xrightarrow{a}_{K_2;k} F$, $A'' = F^{\{K_1/k\}} \bullet C$, $k \notin \mathbf{fk}(A_1, A_2)$. Using (CAU) twice and (COML) we get $B \xrightarrow{\tau} B'$, with $B' = (K :: F \bullet K :: C)^{\{K \cup K_1/k\}}$. Now using Lemma 44 and Lemma 47, we get $B' \equiv (K :: F \bullet C)^{\{K \cup K_1/k\}}$ and by Lemma 45 (note that $k \notin K$ for $k$ must not be in $\mathbf{fk}(K :: A_1, K :: A_2)$ for applying (COML), a condition which can always be met thanks to Lemma 48) $B' \equiv K :: (F \bullet C)^{\{K_1/k\}} = A'$, as required.

- (COMR): this case is similar to the (COML) one.

• (E-CAU): in this case, $A = K_1 :: K_2 :: A_1$ and $B = K_1 \cup K_2 :: A_1$. $A \xrightarrow{\tau} A'$ can only have been derived via (T-CAU) twice, leading to
$A_1 \xrightarrow{\tau} A'_1$ and $A' = K_1 :: K_2 :: A'_1$. Now, applying (T-CAU) we get $B \xrightarrow{\tau} K_1 \cup K_2 :: A'_1$ and by (E-CAU) we get $B \equiv K_1 :: K_2 :: A'_1 = A'$, as required.

* (E-RES): the reasoning proceeds like above, exploiting (RES) and (E-RES).

* (E-NIL): immediate.

□

**Lemma 51.** For all causal processes A, the following properties hold:

1. If $A \xrightarrow{\bar{a}}_{K;k} \nu\tilde{c}. \langle P \rangle B$ then $A \equiv \nu\tilde{c}. (K :: a\langle P \rangle) | B$.

2. If $A \xrightarrow{a}_{K;k} F$ then $A \equiv \nu\tilde{c}. (K :: a(X) \triangleright Q) | B$ for some $\tilde{c}, Q, B$, and $F \equiv (X)\nu\tilde{c}. (K \cup \{k\} :: Q) | B$.

3. If $A \xrightarrow{\tau} A'$ then $A \equiv \nu\tilde{c}. (K_1 :: a\langle P \rangle) | (K_2 :: a(X) \triangleright Q) | B$ for some $\tilde{c}, K_1, K_2, a, P, Q, B$, and $A' \equiv \nu\tilde{c}. (K_1 \cup K_2 :: Q\{P/X\}) | B$.

**PROOF.** We prove property 1 by induction on the derivation of $A \xrightarrow{\bar{a}}_{K;k} C$, where $C = \nu\tilde{c}. \langle P \rangle B$ for some $\tilde{c}, P, B$.

* (OUT): in this case $A = a\langle P \rangle$, $K = \emptyset$ and $C = \langle P \rangle 0$, thus $A \equiv \emptyset :: a\langle P \rangle | 0$, as required.

* (CAU): in this case $A = K_1 :: A_1$, $K = K_1 \cup K_2$, $C = K_1 :: C_1$, and $A_1 \xrightarrow{\bar{a}}_{K_2;k} C_1$. Assume $C_1 = \nu\tilde{c}. \langle P \rangle B$, then $C = \nu\tilde{c}. \langle P \rangle K_1 :: B$. By induction assumption, we have $A_1 \equiv \nu\tilde{c}. (K_2 :: a\langle P \rangle) | B$. Thus $A = K_1 :: A_1 \equiv \nu\tilde{c}. (K_1 \cup K_2 :: a\langle P \rangle) | (K_1 :: B)$, as required.

* (PARL): in this case, $A = A_1 | A_2$, $A_1 \xrightarrow{\bar{a}}_{K;k} C_1$, and $C = C_1 | A_2$. Assume $C_1 = \nu\tilde{c}. \langle P \rangle B$, then $C = \nu\tilde{c}. \langle P \rangle (B | A_2)$. By induction assumption, we have $A_1 \equiv \nu\tilde{c}. K :: a\langle P \rangle | B$. Thus, $A = A_1 | A_2 \equiv \nu\tilde{c}. (K :: a\langle P \rangle) | (B | A_2)$, as required.

* (PARR): this case is similar to the (PARL) one.
• (RES): in this case, $A = \nu e. A_1$, $e \neq a$, $A_1 \xrightarrow{\overline{a}}_{K;k} C_1$, and $C = \nu e. C_1$. Assume $C_1 = \nu \tilde{c}. \langle P \rangle B$, then $C = \nu e. \nu \tilde{c}. \langle P \rangle B$. By induction assumption $A_1 \equiv \nu \tilde{c}. K :: a \langle P \rangle | B$. Thus $A = \nu e. A_1 \equiv \nu e, \tilde{c}. K :: a \langle P \rangle | B$. We now have two cases to consider, according to whether $e \in \mathbf{fn}(P)$ or not. If $e \in \mathbf{fn}(P)$, we have $C = \nu e, \tilde{c}. \langle P \rangle B$, and we are done. If not, we have $C = \nu \tilde{c}. \langle P \rangle \nu e. B$ and $A \equiv \nu \tilde{c}. K :: a \langle P \rangle | \nu e. B$, as required.

We prove property 2 by induction on the derivation of $A \xrightarrow{a} F$.

• (IN): in this case, $A = a(X) \triangleright Q$, $K = \emptyset$, and $F = \{k\} :: (X)Q$. Thus we have $A \equiv \emptyset :: a(X) \triangleright Q$ and $F \equiv \emptyset \cup \{k\} :: (X)Q$, as required.

• (CAU): in this case, $A = K_1 :: A_1$, $A_1 \xrightarrow{a}_{K_2;k} F_1$, $k = K_1 \cup K_2$, $F = K_1 :: F_1$. By induction assumption, we have $A_1 \equiv \nu \tilde{c}. (K_2 :: a(X) \triangleright Q) | B$ for some $\tilde{c}, Q, B$, and $F_1 \equiv (X)\nu \tilde{c}. (K_2 \cup \{k\} :: Q) | B$. Thus, $A \equiv \nu \tilde{c}. (K_1 \cup K_2 :: a(X) \triangleright Q) | (K_1 :: B)$, and $F \equiv (X)\nu \tilde{c}. (K_1 \cup K_2 \cup \{k\} :: Q) | (K_1 :: B)$ as required.

• (PARL): in this case, $A = A_1 | A_2$, $A_1 \xrightarrow{a} F_1$, $F = F_1 | A_2$. By induction assumption, we have $A_1 \equiv \nu \tilde{c}. (K :: a(X) \triangleright Q) | B$ for some $\tilde{c}, Q, B$, and $F_1 \equiv (X)\nu \tilde{c}. (K \cup \{k\} :: Q) | B$. Thus, $A \equiv \nu \tilde{c}. (K :: a(X) \triangleright Q) | (B | A_2)$, and $F \equiv (X)\nu \tilde{c}. (K \cup \{k\} :: Q) | (B | A_2)$ as required.

• (PARR): this case is handled as the (PARL) one.

• (RES): in this case $A = \nu e. A_1$, $e \neq a$, $A_1 \xrightarrow{a} F_1$, $F = \nu e. F_1$. By induction assumption, we have $A_1 \equiv \nu \tilde{c}. (K :: a(X) \triangleright Q) | B$ for some $\tilde{c}, Q, B$, and $F_1 \equiv (X)\nu \tilde{c}. (K \cup \{k\} :: Q) | B$. Thus, $A \equiv \nu e, \tilde{c}. (K :: a(X) \triangleright Q) | B$ for some $\tilde{c}, Q, B$, and $F \equiv (X)\nu e, \tilde{c}. (K \cup \{k\} :: Q) | B$, as required.

We prove property 3 by induction on the derivation of $A \xrightarrow{\tau} A'$.

• (T-CAU): in this case, $A = K :: A_1$, $A_1 \xrightarrow{\tau} A'_1$ and $A' = K :: A'_1$. By induction assumption $A_1 \equiv \nu \tilde{c}. K_1 :: a \langle P \rangle | K_2 :: a(X) \triangleright Q | B$, $A'_1 \equiv \nu \tilde{c}. K_1 \cup K_2 :: Q \{P/X\} | B$ for some $\tilde{c}, K_1, K_2, a, P, Q, B$. Thus

$$A \equiv \nu \tilde{c}. (K \cup K_1 :: a \langle P \rangle) | (K \cup K_2 :: a(X) \triangleright Q) | (K :: B)$$
and

$$A' \equiv \nu\tilde{c}. (K \cup K_1 \cup K_2 :: Q^{P/X}) | (K :: B)$$

as required.

* (T-RES), (T-PARL), (T-PARR): the proof is similar to the one of the (T-CAU) case.

* (COML): in this case, we have $A = A_1 | A_2, A_1 \xrightarrow{\bar{a}} C, A_2 \xrightarrow{a} F$, and $A' = F^{K_1/k} \bullet C$. Using property 1, we have $A_1 \equiv \nu\tilde{c}$. $K_1 :: a(P) | B_1$ for some $\tilde{c}, P, B_1$, and $C = \nu\tilde{c}. \langle P \rangle | B_1$ Using property 2, we have $A_2 \equiv \nu\tilde{c}. K_2 :: a(X) \triangleright Q | B_2$ for some $\tilde{c}, Q, B_2$, and $F \equiv \nu\tilde{c}. (K_2 \cup \{k\} :: Q) | B_2$. Thus,

$$A \equiv \nu\tilde{c}, \tilde{e}. (K_1 :: a(P)) | (K_2 :: a(X) \triangleright Q) | (B_1 | B_2)$$

and

$$A' \equiv \nu\tilde{c}, \tilde{e}. (((K_2 \cup \{k\} :: Q) | B_2)^{P/X} | B_1)^{K_1/k} \\ \equiv \nu\tilde{c}, \tilde{e}. (K_2 \cup K_1 :: Q^{P/X}) | (B_1 | B_2)$$

as required (noting that $X$ is not free in $B_2$ and that $k \notin \mathbf{fk}(B_1, B_2)$ for $k \notin \mathbf{fk}(A_1, A_2)$).

* (COMR): this case is proved like the (COML) one.

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

We can finally prove the agreement proposition itself:

**Proposition 2.** $A \xrightarrow{\tau} A'$ if and only if $A \to A'$.

**PROOF.** The *only if* part is a direct consequence of Lemma 51(3). For the *if* part, we reason by induction on the derivation of $A \to A'$:

* (C-RED): in this case, $A = K_1 :: a(P) | K_2 :: a(X) \triangleright Q$, and $A' = K_1 \cup K_2 : Q^{P/X}$. We can apply (OUT) followed by (CAU) to get $K_1 :: a(P) \xrightarrow{\bar{a}} \langle P \rangle K_1 :: 0$. We can apply (IN) followed by (CAU) to get $K_2 :: a(X) \triangleright Q \xrightarrow{a} (X) K_2 \cup \{k\} : Q$. Choosing $k$ such that $k \notin K_1 \cup K_2$, and applying (COML) we get:

$$A \xrightarrow{\tau} (K_2 \cup \{k\} : Q)^{P/X} \{K_1/k\} = K_2 \cup K_1 :: Q^{P/X}$$
• closure by $\equiv$: in this case, we have $A \equiv B$, $B \to B'$ and $B' \equiv A'$. By induction assumption, we have $B \xrightarrow{\tau} B'$. Now by Lemma 50, we have $A \xrightarrow{\tau} A''$ with $A'' \equiv B'$ and thus $A'' \equiv A'$, as required.

• closure by evaluation context: in this case we reason by induction on the form of evaluation context $\mathbb{E}$:

- $\mathbb{E} = \bullet$: this is the case (C-RED) above.

- $\mathbb{E} = \nu a. \mathbb{E}'$: in this case $A = \nu a. B$ and $A' = \nu a. B'$ for some $B, B'$ such that $B \to B'$. By induction assumption, $B \xrightarrow{\tau} B'' \equiv B'$. The thesis follows by applying rule T-RES since $\equiv$ is a congruence.

- $\mathbb{E} = \mathbb{E}' | B_P$ and symmetric: in this case $A = B | B_P$ and $A' = B' | B_P$ for some $B, B'$ such that $B \to B'$. By induction assumption, $B \xrightarrow{\tau} B'' \equiv B'$. The thesis follows by applying rule T-PARL since $\equiv$ is a congruence.

□

# Appendix C. Proofs of Section 4

## Appendix C.1. Proofs of Section 4.3

Before proving Lemma 13 below, which concerns configurations, we prove a corresponding result on processes.

**Lemma 52.** For all names $k$ and $\rho \in \pi$ processes $P, Q$, if $P \equiv Q$ then $\mathbf{nf}(|P|k) \equiv_{Ex} \mathbf{nf}(|Q|k)$.

**PROOF.** By induction on the derivation of $P \equiv Q$. The only interesting case is the base one, corresponding to the application of an axiom. We have a case analysis on the applied axiom. We consider just the most interesting cases.

$P | Q \equiv Q | P$. If either $P$ or $Q$ is congruent to 0, the thesis banally follows. Otherwise

$$ 
\begin{align*}
\mathbf{nf}(|P| | Q|k) &= \nu l, h. \mathbf{nf}(|P|l) | \mathbf{nf}(|Q|h) | \mathbf{nf}(\text{KillP} l h k) \\
&\equiv_{Ex} \nu l, h. \mathbf{nf}(|P|l) | \mathbf{nf}(|Q|h) | \mathbf{nf}(\text{KillP} h l k) \\
&= \mathbf{nf}(|Q| | P|k)
\end{align*}
$$

as desired, where we used axiom Ax.C.
$P | (Q | R) \equiv (P | Q) | R$. If at least one among $P$, $Q$ and $R$ is equivalent to
**0** the thesis banally follows. Otherwise

$$
\begin{align*}
\mathbf{nf}((\mathcal{P} | (\mathcal{Q} | \mathcal{R})\!)k) &= \\
&= \nu h, l, h', l'. \mathbf{nf}((\mathcal{P}\!)h) | \mathbf{nf}((\mathcal{Q}\!)h') | \mathbf{nf}((\mathcal{R}\!)l') | \mathbf{nf}(\mathbf{KillP} h l k) | \\
&\phantom{=} \mathbf{nf}(\mathbf{KillP} h' l' l) \\
&=_{\alpha} \nu h, l, h', l'. \mathbf{nf}((\mathcal{P}\!)h') | \mathbf{nf}((\mathcal{Q}\!)l') | \mathbf{nf}((\mathcal{R}\!)l) | \mathbf{nf}(\mathbf{KillP} h' h k) | \\
&\phantom{=} \mathbf{nf}(\mathbf{KillP} l' l h) \\
&\equiv_{\mathcal{E}x} \nu h, l, h', l'. \mathbf{nf}((\mathcal{P}\!)h') | \mathbf{nf}((\mathcal{Q}\!)l') | \mathbf{nf}((\mathcal{R}\!)l) | \mathbf{nf}(\mathbf{KillP} h' l' h) | \\
&\phantom{=} \mathbf{nf}(\mathbf{KillP} l h k) \\
&= \mathbf{nf}((\mathcal{P} | \mathcal{Q}) | \mathcal{R}\!)k
\end{align*}
$$

as desired, where we used axiom Ax.A.

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

**Lemma 13.** Let $M, N$ be closed consistent $\rho\circ\pi$ configurations. Then $M \equiv N$ implies $\mathbf{nf}((\mathcal{M})_\mathcal{I}) \equiv_{\mathcal{E}x} \mathbf{nf}((\mathcal{N})_\mathcal{I})$.

PROOF. By induction on the derivation of $M \equiv N$. The only interesting case is the base one, corresponding to the application of an axiom. If the axiom is applied to a process only, the thesis follows from Lemma 52 and from the observation that processes are always applied to keys. We show below the most interesting of the other cases:

$(\nu u. M) | N \equiv \nu u. (M | N)$. By definition:

$$
\begin{align*}
\mathbf{nf}((\nu u. M) | N)) &= \mathbf{nf}((\nu u. M)\!) | \mathbf{nf}((N)) \\
&= \mathbf{nf}(\nu u. (M)) | \mathbf{nf}((N)) \\
&= \nu u. \mathbf{nf}((M)) | \mathbf{nf}((N)) \\
&\equiv \mathbf{nf}(\nu u. (M | (N))) \\
&= \mathbf{nf}(\nu u. (M | N)) \\
&= \mathbf{nf}((\nu u. (M | N))\!)
\end{align*}
$$

$\kappa : \nu a. P \equiv \nu a. \kappa : P$. We distinguish two cases, depending on the form of $\kappa$.
If $\kappa = \langle h_i, \tilde{h} \rangle \cdot k$ then by definition:

$$
\begin{align*}
\mathrm{nf}(\langle\langle h_i, \tilde{h} \rangle\rangle \cdot k : \nu a. P|) &= \mathrm{nf}(\langle\langle \nu a. P \rangle\rangle h_i) | \mathrm{nf}(\mathrm{Kill}_{\langle h_i, \tilde{h} \rangle \cdot k}) \\
&= \nu a. \mathrm{nf}(\langle\langle P \rangle\rangle h_i) | \mathrm{nf}(\mathrm{Kill}_{\langle h_i, \tilde{h} \rangle \cdot k}) \\
&\equiv (\nu a. \mathrm{nf}(\langle\langle P \rangle\rangle h_i) | \mathrm{nf}(\mathrm{Kill}_{\langle h_i, \tilde{h} \rangle \cdot k}) \\
&= \nu a. \mathrm{nf}(\langle\langle h_i, \tilde{h} \rangle\rangle \cdot k : P|) \\
&= \mathrm{nf}(\langle\langle \nu a. \langle h_i, \tilde{h} \rangle \rangle \cdot k : P|)
\end{align*}
$$

The other case is simpler.

$k : \prod_{i=1}^{n} \tau_i \equiv \nu \tilde{h} \cdot \prod_{i=1}^{n} (\langle h_i, \tilde{h} \rangle \cdot k : \tau_i)$. We consider below the case $n > 2$, the case $n = 2$ is simpler. By definition:

$$
\begin{align*}
\mathrm{nf}(\langle k : \prod_{i=1}^{n} \tau_i \rangle) &= \mathrm{nf}(\langle \prod_{i=1}^{n} \tau_i \rangle k) = \\
&= \nu h_1, l_1 \cdot \mathrm{nf}(\langle \tau_1 \rangle h_1) \mid \mathrm{nf}(\langle \prod_{i=2}^{n} \tau_i \rangle l_1) \mid \mathrm{nf}(\mathrm{KillP} \ h_1 \ l_1 \ k) = \\
&= \nu h_1, h_2, l_1, l_2 \cdot \mathrm{nf}(\langle \tau_1 \rangle h_1) \mid \mathrm{nf}(\langle \tau_2 \rangle h_2) \mid \mathrm{nf}(\langle \prod_{i=3}^{n} \tau_i \rangle l_1) \mid \\
&\qquad \qquad \mathrm{nf}(\mathrm{KillP} \ h_1 \ l_1 \ k) \mid \mathrm{nf}(\mathrm{KillP} \ h_2 \ l_2 \ l_1) = \\
&= \nu \tilde{h}, \tilde{l} \cdot \prod_{i=1}^{n-1} \mathrm{nf}(\langle \tau_i \rangle h_i) \mid \mathrm{nf}(\langle \tau_n \rangle l_{n-1}) \mid \mathrm{nf}(\mathrm{KillP} \ h_1 \ l_1 \ k) \mid \\
&\qquad \qquad \prod_{i=2}^{n-1} \mathrm{nf}(\mathrm{KillP} \ h_i \ l_i \ l_{i-1})
\end{align*}
$$

Now by $\alpha$-converting the key of the last $\tau_n$ from $l_{n-1}$ to $h_n$ we obtain a term of the form

$$
\begin{align*}
& \nu \tilde{h}, \tilde{l} \cdot \prod_{i=1}^{n} \mathrm{nf}(\langle \tau_i \rangle h_i) \mid \mathrm{nf}(\mathrm{KillP} \ h_1 \ l_1 \ k) \mid \prod_{i=2}^{n-2} \mathrm{nf}(\mathrm{KillP} \ h_i \ l_i \ l_{i-1}) \mid \\
& \qquad \mathrm{nf}(\mathrm{KillP} \ h_{n-1} \ h_n \ l_{i-2}) = \\
& \qquad \mathrm{nf}(\langle \nu \tilde{h} \cdot \prod_{i=1}^{n} \langle h_i, \tilde{h} \rangle \cdot k : \tau_i \rangle)
\end{align*}
$$

Note that in this case we assumed that the $|\cdot|$ is right associative, in order to unroll the parallel composition from $\prod_{i=1}^n (\tau_i)$ to $(\tau_1) | \prod_{i=2}^n (\tau_i)$. $\square$
Before proving Lemma 14 below, we show a few auxiliary results.

First, we characterize the effect of reduction to normal form on a term of the form $C[P]$. To this end we define normal form on contexts, which also computes the substitution applied to the hole $\bullet$. To work with contexts with one hole only, we require that for all the higher-order applications $(X)P C_1[\bullet]$ either $P$ is linear or $P$ is already in normal form. In the first case the bullet is not replicated, and single-hole contexts are enough. In the second case, no inductive call is required.

**Definition 21 (Context normal form).** The context normal form function $nfc(C[\bullet])$ is defined as $nfc(C[\bullet], \emptyset)$, where the second parameter is used for computing the substitution applied to the bullet. The result is also a pair $(C'[\bullet], \sigma)$. The function $nfc(C[\bullet], \sigma)$ is defined as follows:

$$nfc(P | C_1[\bullet], \sigma) = nf(P) | C'[\bullet], \sigma' \quad \text{if } nfc(C_1[\bullet], \sigma) = C'[\bullet], \sigma'$$

$$nfc(v a. C_1[\bullet], \sigma) = v a. C'[\bullet], \sigma' \quad \text{if } nfc(C_1[\bullet], \sigma) = C'[\bullet], \sigma'$$

$$nfc((X)C_1[\bullet] P, \sigma) = C'[\bullet], \sigma' \quad \text{if } nfc(C_1\{P/X\}[\bullet], \sigma \cdot \{P/X\}) = C'[\bullet], \sigma'$$

$$nfc((X)P C_1[\bullet], \sigma) = C'[\bullet], \sigma' \quad \text{if } nfc(P\{C_1[\bullet]/X\}, \sigma) = C', \sigma' \text{ and } P \text{ is linear}$$

$$nfc((X)P C_1[\bullet], \sigma) = P\{C_1[\bullet]/X\}, \sigma \cdot \{C_1[\bullet]/X\} \quad \text{if } P \text{ is in normal form}$$

$$nfc((h)C_1[\bullet] l, \sigma) = C'[\bullet], \sigma' \quad \text{if } nfc(C_1\{l/h\}[\bullet], \sigma \cdot \{l/h\}) = C'[\bullet], \sigma'$$

$$nfc(a\langle C_1[\bullet] \rangle, \sigma) = a\langle C_1[\bullet] \rangle, \sigma$$

$$nfc(a(X) \triangleright C_1[\bullet], \sigma) = a(X) \triangleright C_1[\bullet], \sigma$$

$$nfc(\bullet, \sigma) = \bullet, \sigma$$

This definition enables the lemma below.

**Lemma 53.** If $nfc(C[\bullet], \emptyset) = C_1, \sigma$ then $nfc(C[\bullet], \sigma') = C_1, \sigma' \cdot \sigma$

The notions of normal form for processes and for contexts are compatible.

**Lemma 54.** $nf(C[P]) = C'[nf(P\sigma)]$ with $nfc(C[\bullet]) = C'[\bullet], \sigma$ if for each higher-order application $(X)Q C_1[\bullet]$ process $Q$ is either linear or in normal form.

**PROOF.** By structural induction on $C[\bullet]$. We show a few cases as examples:
• $\mathbb{C}[\bullet] = Q \mid \mathbb{C}_1[\bullet]$) we have that $\mathbf{nf}(Q \mid \mathbb{C}_1[P]) = \mathbf{nf}(Q) \mid \mathbf{nf}(\mathbb{C}_1[P])$. By inductive hypothesis we have that $\mathbf{nf}(\mathbb{C}_1[P]) = \mathbb{C}'_1[\mathbf{nf}(P\sigma)]$ with $\mathbf{nfc}(\mathbb{C}_1[P], \emptyset) = \mathbb{C}'_1, \sigma$, and we can conclude by noting that $\mathbf{nfc}(Q \mid \mathbb{C}_1[\bullet], \emptyset) = \mathbf{nf}(Q) \mid \mathbf{nfc}(\mathbb{C}_1[\bullet], \emptyset)$.

• $\mathbb{C}[\bullet] = (X)\mathbb{C}_1[\bullet]Q$ we have to show that $\mathbf{nf}((X)\mathbb{C}_1[P]Q) = \mathbb{C}'[\mathbf{nf}(P\sigma)]$ with $\mathbf{nfc}((X)\mathbb{C}_1[\bullet]Q, \emptyset) = \mathbb{C}', \sigma$. By definition, $\mathbf{nfc}((X)\mathbb{C}_1[\bullet]Q, \emptyset) = \mathbf{nfc}(\mathbb{C}_1[\bullet]\{Q/X\}, \{Q/X\})$. We have that $\mathbf{nf}(\mathbb{C}_1[P]\{Q/X\}) = \mathbf{nf}(\mathbb{C}_1\{Q/X\}[P\{Q/X\})) = \mathbb{C}''[\mathbf{nf}(P\{Q/X\}\sigma')]$ where $\mathbf{nfc}(\mathbb{C}_1\{Q/X\}[\bullet], \emptyset) = \mathbb{C}'', \sigma'$ and by using Lemma 53 $\mathbf{nfc}(\mathbb{C}_1\{Q/X\}[\bullet], \{Q/X\}) = \mathbb{C}'', \{Q/X\}\cdot\sigma'$. We have that $\mathbb{C}''$, $\sigma'\{Q/X\} = \mathbb{C}'$, $\sigma$. So $\mathbf{nf}((X)\mathbb{C}_1[P]Q) = \mathbb{C}'[\mathbf{nf}(P\sigma)]$ with $\mathbf{nfc}((X)\mathbb{C}_1[\bullet]Q, \emptyset) = \mathbb{C}', \sigma$, as desired.

• $\mathbb{C}[\bullet] = \mathbf{nf}((X)Q\mathbb{C}_1[\bullet])$ with $Q$ linear) we have that $\mathbf{nf}((X)Q\mathbb{C}_1[P]) = \mathbf{nf}(Q\{\mathbb{C}_1[P]/X\})$, but since $Q$ is linear we can write $Q\{\mathbb{C}_1[P]/X\} = \mathbb{C}_2[P]$, hence $\mathbf{nf}((X)Q\mathbb{C}_1[P]) = \mathbf{nf}(Q\{\mathbb{C}_1[P]/X\}) = \mathbf{nf}(\mathbb{C}_2[P])$. By inductive hypothesis we have that $\mathbf{nf}(\mathbb{C}_2[P]) = \mathbb{C}'_2[P\sigma]$ with $\mathbf{nfc}(\mathbb{C}_2[\bullet], \emptyset) = \mathbb{C}'_2, \sigma$, as desired.

• $\mathbb{C}[\bullet] = \mathbf{nf}((X)Q\mathbb{C}_1[\bullet])$ with $Q$ in normal form) we have that $\mathbf{nf}((X)Q\mathbb{C}_1[P]) = \mathbf{nf}(Q\{\mathbb{C}_1[P]/X\}) = Q\{\mathbb{C}_1[P]/X\}$ and $\mathbf{nfc}((X)Q\mathbb{C}_1[P], \emptyset) = \mathbb{C}'_1[\bullet], \sigma$ with $\mathbf{nfc}(Q\{\mathbb{C}_1[\bullet]/X\}, \emptyset) = Q\{\mathbb{C}_1[\bullet]/X\}, \emptyset$ and $\mathbb{C}'_1[\bullet] = Q\{\mathbb{C}_1[\bullet]/X\}$, and we can conclude by stating that $\mathbb{C}'_1[P\emptyset] = Q\{\mathbb{C}_1[P]/X\}$, as desired. Note that if $Q$ is in normal form then $\mathbf{nf}(Q\{P/X\}) = Q\{P/X\}$, since $X$ does not occur in evaluation contexts. $\square$

Substitutions preserve structural congruence $\equiv_{Ex}$.

**Lemma 55.** For any substitution $\sigma = \{^l/h\}$ or $\sigma = \{(P^l)/X\}$, if $M \equiv_{Ex} N$ then $M\sigma \equiv_{Ex} N\sigma$.

**PROOF.** The proof is trivial for name substitutions. For higher-order ones the proof is by induction on the derivation of $M \equiv_{Ex} N$, with a case analysis on the last applied axiom of $\equiv_{Ex}$. All the cases are easy. $\square$

**Lemma 14.** If $P$ and $Q$ are consistent $HO\pi^+$ processes and $P \equiv_{Ex} Q$ then $\mathbf{nf}(P) \equiv_{Ex} \mathbf{nf}(Q)$.
**PROOF.** Let us consider $P$ and $Q$ generated by the encoding of Figure 7 where instead of having **Trig** processes, we substitute them with their normal form. Thus we can apply Lemma 54. Let us consider one application of an axiom. We have that $P = \mathbb{C}[L]$ and $Q = \mathbb{C}[R]$ with $L \equiv_{Ex} R$ an axiom. By Lemma 54 we have that $\mathbf{nf}(\mathbb{C}[L]) = \mathbb{C}'[\mathbf{nf}(L\sigma)]$ with $\mathbf{nfc}(\mathbb{C}[\bullet], \emptyset) = \mathbb{C}'[\bullet], \sigma$, and the same with $\mathbf{nf}(\mathbb{C}[R]) = \mathbb{C}'[\mathbf{nf}(R\sigma)]$. By Lemma 55 we have that if $L \equiv_{Ex} R$ then $L\sigma \equiv_{Ex} R\sigma$. Also, $\mathbf{nf}(L\sigma) \equiv_{Ex} \mathbf{nf}(R\sigma)$ since $\equiv_{Ex}$ is closed under normal form. Finally, $\mathbb{C}'[\mathbf{nf}(L\sigma)] \equiv_{Ex} \mathbb{C}'[\mathbf{nf}(R\sigma)]$, as desired. $\square$

**Lemma 15.** If $\mathbf{nf}(P) \equiv_{Ex} \mathbf{nf}(P')$ then for each $Q \in \mathbf{addG}(P)$ there exists $Q' \in \mathbf{addG}(P')$ such that $\mathbf{nf}(Q) \equiv_{Ex} \mathbf{nf}(Q')$.

**PROOF.** By definition of **addG** we have that $P \equiv \mathbb{E}[0]$ and $P' \equiv \mathbb{E}'[0]$, with $Q \equiv \mathbb{E}[R]$. Let us choose $Q' \equiv \mathbb{E}'[R]$. By using Lemma 54 we have that $\mathbf{nf}(\mathbb{E}[R]) = \mathbb{E}_1[\mathbf{nf}(R\sigma)]$ and $\mathbf{nf}(\mathbb{E}'[R]) = \mathbb{E}_2[\mathbf{nf}(R\sigma')]$. Since all the processes added by the function **addG** are closed we have that $R\sigma = R\sigma' = R$ and $\mathbf{nf}(\mathbb{E}[R]) = \mathbb{E}_1[\mathbf{nf}(R)]$ and $\mathbf{nf}(\mathbb{E}'[R]) = \mathbb{E}_2[\mathbf{nf}(R)]$. By hypothesis we have that $\mathbf{nf}(\mathbb{E}[0]) \equiv_{Ex} \mathbf{nf}(\mathbb{E}'[0])$. We also have $\mathbb{E}_1[\mathbf{nf}(0\sigma)] = \mathbb{E}_1[0] \equiv_{Ex} \mathbb{E}_2[0] = \mathbb{E}_2[\mathbf{nf}(0\sigma')]$, and we can conclude by saying that also $\mathbb{E}_1[\mathbf{nf}(R)] \equiv_{Ex} \mathbb{E}_2[\mathbf{nf}(R)]$, that is $\mathbf{nf}(Q) \equiv_{Ex} \mathbf{nf}(Q')$, as desired. $\square$

**Lemma 16.** If $P$ is a consistent $\text{HO}\pi^+$ process and $P \equiv \mathbb{C}[l\langle R \rangle, \dots, l\langle R \rangle]$ with $l \in \mathcal{K}$ for some $n$-ary context $\mathbb{C}$ then $P \equiv \mathbb{C}'[l\langle R \rangle | S_1, \dots, l\langle R \rangle | S_n]$ for some $n$-ary context $\mathbb{C}'$ with, for each $i \in \{1, \dots, n\}$, $S_i = \text{Rew } l$ or $S_i = l(Z) \triangleright Z l$.

**PROOF.** By definition of consistency there exists a $\text{rho}\pi$ process $Q$ such that $(\nu k. k : Q) \Rightarrow P$. The proof is by induction on the number of steps in $\Rightarrow$. The base case is when $(\nu k. k : Q) = P$. The proof is easy by inspection on the rules defining the encoding, since all messages on key channels are created together with the corresponding **Rew** $l$.

In the inductive case we have that $(\nu k. k : Q) \Rightarrow P' \Rightarrow P$ with $P \equiv \mathbb{C}[l\langle R \rangle, \dots, l\langle R \rangle]$. For simplicity we consider just one instance of a message $l\langle R \rangle$ at the time. Note that messages cannot appear, but existing messages may be duplicated because of communications or applications. We proceed by case analysis on $P' \to P$. If the reduction does not involve the message $l\langle R \rangle$ nor the corresponding $S_i$ the thesis follows easily. If the message $l\langle R \rangle$ is inside a communicated message or the argument of an application, then
the corresponding $S_i$ is inside the same message or the same argument and they are deleted, moved, or replicated together. If the message is read, it disappears and nothing has to be proved. If the message is inside a trigger or in the body of an abstraction on a process then a substitution may be applied to it, but this has no effect on the corresponding $S_i$, and the thesis holds by inductive hypothesis. If the reduction is an application of an abstraction of the name $l$, then the same renaming is done on the corresponding *Rew* $l$, and the thesis holds by inductive hypothesis. If the reduction is the application of *Rew* $l$ we move from the first case of the thesis to the second one. If instead the reduction is the communication of $l(Z) \triangleright Z l$, this removes the corresponding message and nothing has to be proved (if it removes another message this means that there were two parallel messages on the same channel $l$, and we can simply exchange them in the correspondence). $\square$

**Lemma 17.**

If $P$ is a consistent $HO\pi^+$ process and $P \equiv \mathbb{C}[a\langle(\|Q\|), l\rangle, \dots, a\langle(\|Q\|), l\rangle]$ with $a \in \mathcal{N}$ for some $n$-ary context $\mathbb{C}$ then $P \equiv \mathbb{C}'[a\langle(\|Q\|), l\rangle | S_1, \dots, a\langle(\|Q\|), l\rangle | S_n]$ for some $n$-ary context $\mathbb{C}'$ with, for each $i \in \{1, \dots, n\}$, $S_i = (\text{KillM } a \ l)$ or $S_i = (a(X, \ \l) \triangleright \ l\langle(h)\text{Msg } a \ X \ h\rangle | \text{Rew } l)$.

**PROOF.** By inspection of the encoding of Figure 7 we note that a message of the form $a\langle(\|Q\|), l\rangle$ is only generated in the *Msg* process, together with the corresponding *KillM*. Also, interaction with the message is the only way to remove a *KillM*. The case analysis is similar to the one in Lemma 16. $\square$

**Lemma 18.** Let $P$ be a consistent $HO\pi^+$ process and $Q \in \text{addG}(P)$. If $\text{nf}(Q) \hookrightarrow Q'$ then there exists $P'$ such that $P \hookrightarrow_P^* P'$ with $Q' \in \text{addG}(P')$.

**PROOF.** The reduction $\text{nf}(Q) \hookrightarrow Q'$ is due to a communication since processes in normal form have no enabled applications.

We distinguish two cases: either the reduction $\hookrightarrow$ is due to the process $\text{nf}(P)$ only or it involves garbage added by **addG**.

Let us consider the first case. By definition we have $Q = \mathbb{E}[R]$ with $P \equiv \mathbb{E}[0]$ where $R$ is the garbage added by the function **addG**. The form of $Q$ is preserved by the $\text{nf}(\cdot)$ function, where all the applications are executed. Hence, $\text{nf}(Q) \equiv \mathbb{E}'[R']$ with $\text{nf}(P) = \mathbb{E}'[0]$. Since the reduction does not involve $R$ we have that $\mathbb{E}'[R] \hookrightarrow \mathbb{E}''[R] = Q'$, but also $\mathbb{E}'[0] \hookrightarrow \mathbb{E}''[0] = P'$. Moreover we have that $P \dashv_P^* \mathbb{E}'[0] \hookrightarrow \mathbb{E}''[0]$ and we are done.
In the second case, the only garbage processes that may interact with the context are either a (Rew l) process or a (KillM a l) process (the other garbage processes are inactive). If the administrative step is due to the applied form of (Rew l) then the context E contains a message on the channel l, that is nf(Q) = E[l(Z)▷Z l | R₁] ≡ E₁[l⟨S⟩ | l(Z)▷Z l | R₁] ↪→ E₁[(S l) | R₁] = Q'. But since P is consistent and since the process l(Z)▷Z l has been added by the addG function, by Lemma 16 we have that also P = E₁[l⟨S⟩] ≡ E₂[l⟨S⟩ | l(Z)▷Z l] ↪→ E₂[(S l)] = P'. We can conclude by noting that Q' ∈ nf(addG(P')). The other case is similar using Lemma 17 instead of Lemma 16. □

Appendix C.2. Proofs of Section 4.4

**Lemma 23.** For each closed rhoπ process P, ⟨P⟩k ↪→* ν̃u. k⟨⟨Q⟩⟩ | S with k /∈ ν̃u, S = ∏ Rᵢ, Rᵢ = Rew kᵢ or Rᵢ = νt. (a(X, h)|t▷R) and P ≡ ν̃u. Q.

PROOF. By induction on the structure of P. We show only the most inter-
esting cases:

$P = a(X) \triangleright P' : \text{let } Y = (X c)c\langle\langle (P')\rangle\rangle, \text{ we have that}$
$$
\begin{align*}
(\mathcal{P})k &= ((l)(\mathrm{Trig}\ Y\ a\ l))k \rightarrow \mathrm{Trig}\ Y\ a\ k \rightarrow \\
\nu t.\ (\bar{\mathfrak{t}}\ |\ (a(X,h)|t \triangleright R)\ |\ (\mathrm{Kill}\ T\ Y\ t\ k\ a))\rightarrow \\
\nu t.\ (\bar{\mathfrak{t}}\ |\ (a(X,h)|t \triangleright R)\ |\ (t \triangleright k\langle\langle (h)\mathrm{Trig}\ Y\ a\ h\rangle\rangle \mid \mathrm{Rew}\ k)) \leftrightarrow \\
\nu t.\ (a(X,h)|t \triangleright R)\ |\ k\langle\langle (h)\mathrm{Trig}\ Y\ a\ h\rangle\rangle \mid \mathrm{Rew}\ k \equiv \\
(\nu t.\ (a(X,h)|t \triangleright R))\ |\ k\langle\langle (h)\mathrm{Trig}\ Y\ a\ h\rangle\rangle \mid \mathrm{Rew}\ k = k\langle\langle (h)\mathrm{Trig}\ Y\ a\ h\rangle\rangle \mid S
\end{align*}
as desired.

$P = \nu a. P'$ : we have that ⟨νa. P'⟩k = ((h)νa. ⟨P'⟩h)k → νa. ⟨P'⟩k. Now
by inductive hypothesis we know that ⟨P'⟩k ↪→* ν̃u. k⟨⟨Q⟩⟩ | S with
P' ≡ ν̃u. Q and since restriction is an evaluation context we have
νa. ⟨P'⟩k ↪→* νa. ν̃u. k⟨⟨Q⟩⟩ | S with νa. P' ≡ νa. ν̃u. Q, as desired.

$P = P_1 | P_2 : \text{ we have that}$
$$
\begin{align*}
(\mathcal{P})k &= ((l)(\mathbf{Par} (P_1) (P_2) l)k \rightarrow \mathbf{Par} (P_1) (P_2) k \rightarrow \\
\nu h, l. (P_1)h \mid (P_2)l \mid \mathbf{KillP} l h k \rightarrow \\
\nu h, l. (P_1)h \mid (P_2)l \mid (h(W)|l(Z) \triangleright k\langle\langle (h)\mathbf{Par} W Z h\rangle\rangle \mid \mathbf{Rew} k).
\end{align*}
$$
By inductive hypothesis we have that $\langle P_1 \rangle h \hookrightarrow^* \nu \tilde{u} \cdot h \langle \langle P'_1 \rangle \rangle | S_1$ with $P_1 \equiv \nu \tilde{u} \cdot P'_1$ and $\langle P_2 \rangle l \hookrightarrow^* \nu \tilde{v} \cdot l \langle \langle P'_2 \rangle \rangle | S_2$ with $P_2 \equiv \nu \tilde{v} \cdot P'_2$. Hence we have

$$
\begin{align*}
& \nu h, l. \langle P_1 \rangle h \mid \langle P_2 \rangle l \mid (h(W) \mid l(Z) \triangleright k \langle (h) \operatorname{Par} W Z h \rangle \mid \operatorname{Rew} k) \hookrightarrow^* \\
& \nu h, l, \tilde{u}, \tilde{v}. h \langle \langle P'_1 \rangle \rangle | S_1 \mid l \langle \langle P'_2 \rangle \rangle | S_2 \mid (h(W) \mid l(Z) \triangleright k \langle (h) \operatorname{Par} W Z h \rangle \mid \\
& \qquad \qquad \operatorname{Rew} k) \hookrightarrow \\
& \nu h, l, \tilde{u}, \tilde{v}. S_1 \mid S_2 \mid k \langle (h) \operatorname{Par} \langle \langle P'_1 \rangle \rangle \langle \langle P'_2 \rangle \rangle h \rangle \mid \operatorname{Rew} k \equiv \\
& \nu h, l, \tilde{u}, \tilde{v}. k \langle (h) \operatorname{Par} \langle \langle P'_1 \rangle \rangle \langle \langle P'_2 \rangle \rangle h \rangle \mid S
\end{align*}
$$

with $S = \text{Rew } k | S_1 | S_2$, and by garbage collecting names $h, l$ we have $P \equiv \nu \tilde{u}, \tilde{v}. (P'_1 | P'_2)$ as desired. $\square$

**Lemma 24.** For any consistent $HO\pi^+$ process $P$ the following conditions hold:

1. $P \not\equiv \mathbb{C}[l\langle P_1 \rangle | l\langle P_2 \rangle]$, with $l \in \mathcal{K}$.

2. $P \not\equiv \mathbb{C}[(\text{KillP } l_1 \ l_2 \ l_3) \mid (\text{KillP } l_4 \ l_5 \ l_6)]$, with $l_1, l_2, l_3, l_4, l_5, l_6 \in \mathcal{K}$ and $\{l_1, l_2\} \cap \{l_4, l_5\} \neq \emptyset$ or $l_3 = l_6$.

3. $P \not\equiv \mathbb{C}[(\text{KillP } l_1 \ l_2 \ l) \mid (\text{Mem } P \ a \ Q \ h \ l_3 \ k)]$, with $l, l_1, l_2, l_3, h, k \in \mathcal{K}$ and $l_1 = l_3$ or $l_2 = l_3$.

**PROOF.** By definition of consistency there is a $\text{rho}_\pi$ process $R$ such that $\langle \nu k. k : R \rangle \Rightarrow P$.

For condition 1 the proof is by structural induction on $R$, using as inductive hypothesis that messages are created only on the key channel passed to the process or on fresh key channels. In basic cases (**0** process, message or trigger), one message is created on the received channel, plus one if the **Rew** $l$ is executed, but this consumes a message on the same channel thus preserving the invariant. For restriction, the thesis follows by inductive hypothesis. For **Par**, two distinct fresh names are passed to the parallel processes, thus by inductive hypothesis their messages will not be on the same channel as the one created by the **KillP**. For **Trig**, a fresh name is passed to the continuation, thus by inductive hypothesis its messages will not conflict with the one created by the **KillT** or with the one created by the **Trig** in the **Mem**. Note that these last two messages cannot conflict since for them to be in parallel the token **t** is needed, and either **KillT** or the **Trig** may read it, but not both of them.
For condition 2, note that **KillP** is generated only by a **Par** process. The first two arguments are fresh, thus they cannot be used by another **KillP**. For the last argument, we can reason as above to show that at most one **KillP** for each name may be created.

For condition 3 we can see that both the channel used by the **Mem** and the ones used by **KillP** are fresh, thus they cannot coincide. □

Before proving Lemma 27 below we show a few auxiliary results.

**Lemma 56 (Input key invariant).** For each $\rho \in \Pi$ process $R$ and key $l$ we have:

1. $(R)l \not\Rightarrow \mathbb{E}[l(X) \triangleright P]$, unless the trigger has been generated by an application of **Rew** $l$.

2. $(R)l \not\Rightarrow \mathbb{E}[l(X)|l'(W) \triangleright P]$.

3. $(R)l \not\Rightarrow \mathbb{E}[l'(X) \triangleright P \mid l'(X) \triangleright Q]$ for each $l' \in K$ and $l' \neq l$, unless one of the triggers has been generated by an application of a **Rew** $l'$.

**PROOF.** We prove all the cases by showing that no such derivation with less than $n$ steps exists. The proof is by induction on $n$. All the base cases are trivial, since the starting term has no trigger in an evaluation context. Let us consider the different inductive cases.

1. We reason by contradiction. Suppose that $(R)l \Rightarrow \mathbb{E}[l(X) \triangleright P]$ in $n$ steps. By looking at the encoding in Figure 7 we note that a trigger on a key channel can only occur inside a **Mem** term. However the subject $k$ is generated fresh in the clause defining the **Trig** process, thus it cannot be $l$. This contradiction concludes the proof.

2. Suppose towards a contradiction that $(R)l \Rightarrow \mathbb{E}[l(X)|l'(Z) \triangleright P]$ in $n$ steps. By looking at the encoding we note that a trigger reading two messages can only be generated by a **KillP** process. However, the two names are generated fresh in the clause defining the **Par** process, against the hypothesis that one of them can be $l$.

3. We use the same proof strategy as in items 1 and 2. Triggers on keys $l' \in K$ with $l' \neq l$ may be generated only by **Mem** processes, but since the used key is fresh two triggers may not have the same key. □

Messages on channels $l \in K$ carry translations of processes with no toplevel restrictions.
**Lemma 57.** For each rhoπ process R, (R)l ⇒ ℂ[l⟨Q⟩] implies Q = (Q') where Q' has no toplevel restriction.

PROOF. We proceed by induction on the number of reductions in ⇒. The proof of the base case is by structural induction on R. We show a few cases as examples.

R = a⟨P⟩ : by definition

$$
\begin{align*}
(a\langle P \rangle)h = {}& (l)(\mathbf{Msg} a (\mathcal{P}) l)h = \\
& (l)((a X l)(a\langle X, l \rangle | (\mathbf{KillM} a l)) a (\mathcal{P}) l)h = \\
& (l)((a X l)(a\langle X, l \rangle | (((a l)a(X, \setminus l) \triangleright l \langle\langle (h)\mathbf{Msg} a X h \rangle| \\
& (\mathbf{Rew} l)) a l))a (\mathcal{P}) l)h
\end{align*}
$$

as desired since (h)Msg a X h = (a⟨X⟩).

R = νa. P : by definition (νa. P)h = (l)(νa. (P))h and we can conclude by inductive hypothesis on P.

R = P₁ | P₂ : by definition

$$
\begin{align*}
(P_1 | P_2)h &= (l)(\mathbf{Par} (P_1) (P_2) l)h = \\
&= (l)((((X Y l)\nu h, k. X h | Y k | (\mathbf{KillP} h k l)) (P_1) (P_2) l)h = \\
&= (l)((((X Y l)\nu h, k. X h | Y k | \\
&\qquad (((h k l)h(W)|k(Z) \triangleright l\langle\langle (l)(\mathbf{Par} W Z l)\rangle\rangle) h k l)) (P_1) (P_2) l)h
\end{align*}
$$

and we can conclude since (l)(Par W Z l) = (W | Z).

For the inductive case, either the message we are considering disappears, and
then there is nothing to prove, or the message remains in the context and
we can conclude by applying the inductive hypothesis. Note, in fact, that
higher order variables are always replaced by translations of rhoπ processes,
and that variables are never at top level inside the messages with subject l
above.
□

**Lemma 27.** If nf(*P*₁) ≡<sub>*Ex*</sub> nf(*P*₂) and nf(*P*₁) → *P*'<sub>1</sub> then nf(*P*₂) ⇒ nf(*P*'<sub>2</sub>) with nf(*P*''<sub>1</sub>) ≡<sub>*Ex*</sub> nf(*P*'<sub>2</sub>) and *P*''<sub>1</sub> ∈ addG(*P*'<sub>1</sub>). Furthermore, if → is forward then ⇒ *is* ⇒<sub>*f*</sub>, if → is backward then ⇒ *is* ⇒<sub>*b*</sub>, if → is administrative then ⇒ *is* ↪→*.
PROOF. By case analysis on the used axiom $P \equiv_{Ex} Q$ and on the structure of $nf(P_1)$. Since $nf(P_1)$ is in normal form, $\rightarrow$ is a communication. Hence we can express $nf(P_1)$ as an evaluation context $\mathbb{E}[a\langle R \rangle | a(X) \triangleright S]$ (the cases where the trigger has different forms are similar). We just consider a few interesting cases, the remaining ones are similar. The second part follows by noticing that in the proofs below the same trigger is used to mimic the reduction (possibly together with some administrative reductions).

$P | Q \equiv_{Ex} Q | P$. There are four places where the axiom could be applied: in the context, inside the message content, inside the trigger continuation, or to the context hole. We consider the second case as an example. We have that $nf(P_1)$ can be written as $\mathbb{E}[a\langle C[P | Q] \rangle | a(X) \triangleright S]$ and $nf(P_2)$ as $\mathbb{E}[a\langle C[Q | P] \rangle | a(X) \triangleright S]$. We have that $nf(P_1) \rightarrow \mathbb{E}[S\{C[P|Q]|_X\}]$ and $nf(P_2) \rightarrow \mathbb{E}[S\{C[Q|P]|_X\}]$, with $\mathbb{E}[S\{C[P|Q]|_X\}] \equiv_{Ex} \mathbb{E}[S\{C[Q|P]|_X\}]$, and we can conclude by applying Lemma 14.

**Ax.C.** We have that $nf(P_1) = \mathbb{E}[\mathbf{nf}(\mathbf{KillP} l h k)] = \mathbb{E}[(l(Z)|h(W)\triangleright k\langle(h)\mathbf{Par} Z W l \rangle | \mathbf{Rew} k)]$. If the communication is performed by the context $\mathbb{E}[\bullet]$ then the thesis banally follows. If the communication involves the hole, we should have in the context two messages of the form $l\langle P \rangle$ and $h\langle Q \rangle$, hence $\mathbb{E}[\mathbf{nf}(\mathbf{KillP} l h k)] \equiv \mathbb{E}'[l\langle P \rangle | h\langle Q \rangle | (l(Z)|h(W)\triangleright k\langle(h)\mathbf{Par} Z W l \rangle | \mathbf{Rew} k)] \rightarrow \mathbb{E}'[k\langle(h)\mathbf{Par} P Q h \rangle | \mathbf{Rew} k]$, and by expanding the definition of $\mathbf{Par}$ we have that

$$nf(P_1) \rightarrow \mathbb{E}'[k\langle(h)(\nu l_1, l_2. (P l_1) | (Q l_2) | \mathbf{KillP} l_1 l_2 h)\rangle | \mathbf{Rew} k] \equiv_{Ex} \mathbb{E}'[k\langle(h)(\nu l_1, l_2. (Q l_1) | (P l_2) | \mathbf{KillP} l_2 l_1 h)\rangle | \mathbf{Rew} k].$$

Since $nf(P_2) \rightarrow \mathbb{E}'[k\langle(h)(\nu l_1, l_2. (Q l_1) | (P l_2) | \mathbf{KillP} l_2 l_1 h)\rangle | \mathbf{Rew} k]$ the thesis follows.

**Ax.P.** We have $nf(P_1) = \mathbb{E}[l_1\langle(P)\rangle | l_2\langle(Q)\rangle | \mathbf{nf}(\mathbf{KillP} l_1 l_2 l)]$. The context can interact with the hole by reading messages on $l_1$ or $l_2$. By inspection of the encoding one can note that only processes generated by a **Rew**, by a **KillP**, or by a **Mem** can read this kind of messages. Let us consider the **Rew** case. We have that $nf(P_1) \equiv \mathbb{E}'[(l_1(Z) \triangleright Z l_1) | l_1\langle(P)\rangle | l_2\langle(Q)\rangle | \mathbf{nf}(\mathbf{KillP} l_1 l_2 l)] \rightarrow \mathbb{E}'[(P)l_1 | l_2\langle(Q)\rangle | \mathbf{nf}(\mathbf{KillP} l_1 l_2 l)] = P'$. Let us consider $P_2$. We also have that $nf(P_2) = \mathbb{E}[l\langle(h)\mathbf{Par} (P) (Q)\rangle | (l(Z) \triangleright Z l)]$. Thus, $nf(P_2) \leftrightarrow^* \mathbb{E}[\nu l_1, l_2. (P)l_1 | (Q)l_2 | (\mathbf{KillP} l_1 l_2 l)]$. Now, by using Lemma 23
we have that $\langle\!\langle Q\rangle\!\rangle l_2 \hookrightarrow^* \nu\tilde{u}_1 \cdot l_2\langle\!\langle Q\rangle\!\rangle | S_l$. Hence we have $\mathrm{nf}(P_2) \hookrightarrow^* \mathrm{E}[\nu\tilde{u}_1, l_1, l_2 \cdot (P)l_1 | l_2\langle\!\langle Q\rangle\!\rangle | (\mathrm{KillP} \ l_1 \ l_2 \ l) | S_l] \equiv \mathrm{E}'[\nu\tilde{u}_1, l_1, l_2 \cdot (P)l_1 | l_2\langle\!\langle Q\rangle\!\rangle | (\mathrm{KillP} \ l_1 \ l_2 \ l) | S_l | (l_1(Z) \triangleright Z \ l_1)] = P'_2$. Let $P''_1 = \mathrm{E}'[(P)l_1 | l_2\langle\!\langle Q\rangle\!\rangle | \mathrm{nf}(\mathrm{KillP} \ l_1 \ l_2 \ l)]$. We have that $\mathrm{nf}(P''_1) \equiv_{Ex} \mathrm{nf}(P'_2)$ and that $P'_1 \in \mathrm{addG}(P''_1)$, and we are done. The case of a $\mathrm{KillP}$ corresponds to a reduction inside the hole, since no other message on the same channel can exist thanks to condition 1 of Lemma 24, and no other $\mathrm{KillP}$ may read the same messages thanks to condition 2 of Lemma 24. In this case we have that $\mathrm{nf}(P_1) = \mathrm{E}[l_1\langle\!\langle P\rangle\!\rangle | l_2\langle\!\langle Q\rangle\!\rangle | (l_1(Z)|l_2(W) \triangleright (l)\mathrm{Par} \ Z \ W \ h | \mathrm{Rew} \ l)] \to \mathrm{E}[(l)\mathrm{Par} \ (P) \ (Q) \ h | \mathrm{Rew} \ l]$ and the thesis banally follows. The case of a $\mathrm{Mem}$ can never happen thanks to condition 3 of Lemma 24.

Reductions from the right member of the axiom are trivially matched since the left member reduces to the right one.

**Ax.A.** We have that $\mathrm{nf}(P_1) = \mathrm{E}[\nu l'. (l_1(Z)|l_2(W) \triangleright l'\langle\!\langle (h)\mathrm{Par} \ Z \ W \ h | \mathrm{Rew} \ l'\rangle\rangle) | (l'(Z')|l_3(W') \triangleright l\langle\!\langle (h)\mathrm{Par} \ Z' \ W' \ h | \mathrm{Rew} \ l\rangle\rangle]$. The hole may perform a communication only if there are two messages on $l_1, l_2$ in the context. In this case, we have that $\mathrm{nf}(P_1) \equiv \mathrm{E}'[\nu l'. l_1\langle\!\langle P\rangle\!\rangle | l_2\langle\!\langle Q\rangle\!\rangle | (l_1(Z)|l_2(W) \triangleright l'\langle\!\langle (h)\mathrm{Par} \ Z \ W \ h | \mathrm{Rew} \ l') | \mathrm{nf}(\mathrm{KillP} \ l' \ l_3 \ l)] \to \mathrm{E}'[\nu l'. l'\langle\!\langle (h)\mathrm{Par} \ P \ Q \ h | \mathrm{Rew} \ l' | \mathrm{nf}(\mathrm{KillP} \ l' \ l_3 \ l)] \equiv_{Ex} \mathrm{E}[\nu l'. l_1\langle\!\langle P\rangle\!\rangle | l_2\langle\!\langle Q\rangle\!\rangle | (l_1(Z)|l_2(W) \triangleright l'\langle\!\langle (h)\mathrm{Par} \ Z \ W \ h | \mathrm{Rew} \ l') | \mathrm{nf}(\mathrm{KillP} \ l' \ l_3 \ l)]$ using axiom AX.P, as desired.

**Ax.Adm.** By noting that the left member of the axiom can only perform a communication, reducing to the right member of the axiom. $\square$

**Lemma 28.** If $\mathrm{nf}(P_1) \equiv_{Ex} \mathrm{nf}(P_2)$ and $\mathrm{nf}(P_1) \Rightarrow P'_1$ then $\mathrm{nf}(P_2) \Rightarrow \mathrm{nf}(P'_2)$ with $\mathrm{nf}(P''_1) \equiv_{Ex} \mathrm{nf}(P'_2)$ and $P''_1 \in \mathrm{addG}(P'_1)$. Furthermore, if the first $\Rightarrow$ is $\Rightarrow_f$, $\Rightarrow_b$ or $\hookrightarrow^*$ then the second $\Rightarrow$ is of the same form.

**PROOF.** By induction on the length of the derivation $\mathrm{nf}(P_1) \Rightarrow P'_1$. In the base case ($n=0$) the proof is trivial. In the inductive case we have that $\mathrm{nf}(P_1) \Rightarrow P_1^{n-1} \to P'_1$ with $\mathrm{nf}(P_2) \Rightarrow \mathrm{nf}(P_2^{n-1})$ and $\mathrm{nf}(P_2^{n-1}) \equiv_{Ex} \mathrm{nf}(Q''_1)$ and $Q''_1 \in \mathrm{addG}(P_1^{n-1})$. Since $P_1^{n-1} \to P'_1$ then there exists $P'''_1 \in \mathrm{addG}(P'_1)$ such that $Q''_1 \to P'''_1$, and by Lemma 26 we have that $\mathrm{nf}(Q''_1) \to \mathrm{nf}(P'''_1)$. Since $\mathrm{nf}(Q''_1) \equiv_{Ex} \mathrm{nf}(P_2^{n-1})$ we can apply Lemma 27, and we have that $\mathrm{nf}(P_2^{n-1}) \Rightarrow \mathrm{nf}(P'_2)$ with $\mathrm{nf}(P'_2) \equiv_{Ex} \mathrm{nf}(Q)$ and $Q \in \mathrm{addG}(\mathrm{nf}(P'''_1))$. By
composing the garbage we have that there exists $P_1'' \in \mathbf{addG}(P_1')$ such that $\mathbf{nf}(P_1'') = \mathbf{nf}(Q)$. This concludes the proof of the first part. The second part follows from the second part of Lemma 27. □

Before proving Lemma 29 below we show some auxiliary results. In particular, we have to study where in a configuration a key may occur. We call $l$-process, denoted by $P_l$, a process of a specific form.

**Definition 22.** Let $Y = (X c)c\langle\langle(Q)\rangle\rangle$. An $l$-process is an $\text{HO}\pi^+$-process of one of the forms below, or obtained from them via one or more applications.

<table><tr><td>(|P|)l</td><td>l&lt;(|P|)&gt; | <b>Rev</b> l</td></tr><tr><td>Msg a (|Q|) l</td><td>Trig Y a l</td></tr><tr><td>Par (|P|) (|Q|) l</td><td>Kill P h k l</td></tr><tr><td>νc. (Y (|P|) c) | (c(Z) ▷ Z l) | (<b>Mem</b> Y a (|P|) l<sub>1</sub> l l<sub>2</sub>)</td><td>νu. (|P|)l</td></tr><tr><td>νc. c&lt;(|P|)&gt; | (c(Z) ▷ Z l) | (<b>Mem</b> Y a (|P|) l<sub>1</sub> l l<sub>2</sub>)</td><td>0</td></tr><tr><td><b>Mem</b> Y a (|P|) h k l</td><td><b>Mem</b> Y a (|P|) l k h</td></tr></table>

Essentially, each key $l$ occurs at most twice (apart from occurrences in **Rev**), once in an $l$-process and possibly once in a killer process or a memory process.

We call primitive context a context originated during the translation of a process.

**Definition 23.** A context $\mathcal{C}$ is called a primitive context if it is generated by:

$$ \mathcal{C} ::= \bullet \mid (l')\mathbf{Msg} a \mathcal{C} l' \mid (l')\mathbf{Trig} (X c)c\langle\langle\mathcal{C}\rangle\rangle a l' \mid (l')\nu a. (\mathcal{C} l') \mid \\ (l')\mathbf{Par} \mathcal{C} (|Q|) l' \mid (l')\mathbf{Par} (|P|) \mathcal{C} l' $$

**Lemma 58.** For any $\text{rho}\pi$ process $P$ and any $l \in \mathbf{n}(|P|) \cap \mathcal{K}$, we have $(|P|) = \mathcal{C}[(l)P_l]$ for some primitive context $\mathcal{C}$ and some $l$-process $P_l$.

**PROOF.** By structural induction on $P$. □

All the messages on channels $a \in \mathcal{N}$ carry a pair whose first element is the translation of a process.
**Lemma 59.** For any consistent $HO\pi^+$ process $P$, if $P \equiv \mathbb{E}[a\langle Q, h \rangle]$ with $a \in \mathcal{N}$ then $Q = (\mathcal{R})$.

**PROOF.** By definition of consistency there is a rho$\pi$ process $S$ such that $(\nu k. k : S) \Rightarrow P$. The proof is by induction on the number of steps in $\Rightarrow$. The base case is proved by inspection. The inductive case is easy. $\square$

We can now prove the invariant on the use of keys.

**Lemma 60.** For any consistent $HO\pi^+$ process $R$ and for any key $l$ occurring in $R$ one of the following statements holds:

1. $R \equiv \mathbb{E}[\nu l. R']$, with $R' \in \text{addG}(P_l | S)$ where $P_l$ is an $l$-process and $S$ is obtained from one of the following terms via 0 or more applications: $(\text{KillP} l l' h)$, $(\text{KillP} l' l h)$, $(\text{Mem } Y \text{ a } (\mathcal{P}) l_1 l l_2)$, **0**.

2. $R \equiv \mathbb{C}[\nu h. \mathbb{C}'[(l)P_l]h]$ where $P_l$ is an $l$-process and $\mathbb{C}'$ is generated from a primitive context via 0 or more applications.

3. $R \equiv \mathbb{C}[\nu l. ((h)P_h)l]$ where $P_h$ is an $h$-process.

4. $R \equiv \mathbb{C}[\nu l, c. (Y (\mathcal{Q}) c) | (c(Z) \triangleright Z l) | (\text{Mem } Y \text{ a } (\mathcal{Q}) h l k)]$ where $Y = ((X c)c(\langle \mathcal{P} \rangle))$.

**PROOF.** By definition of consistency there exists a rho$\pi$ process $P$ such that $(\nu k. k : P) \Rightarrow R$. The proof is by induction on the number $n$ of steps in $(\nu k. k : P) \Rightarrow R$.

For the base case ($n = 0$) we have that $(\nu k. k : P) = \nu k. (\mathcal{P})k$. By Lemma 58 we have that for any $l \in \mathbb{n}((\mathcal{P})) \cap \mathcal{K}$ we have $(\mathcal{P}) = \mathbb{C}'[(l)P_l]$, that is $\nu k. (\mathcal{P})k \equiv \nu k. \mathbb{C}'[(l)P_l]k$, and condition (2) holds.

In the inductive case we distinguish two possibilities: either name $l$ did not exist at the previous step, or it existed. By inspection of the encoding one can see that the first case may only happen when recursive definitions for `Par` or `Trig` are unfolded. In both the cases condition (1) is satisfied for new names, with $P_l = (\mathcal{P})l$ in the first case and $P_l = \nu c. c(\langle \mathcal{P} \rangle) | (c(Z) \triangleright Z l) | (\text{Mem } Y \text{ a } (\mathcal{P}) l_1 l l_2)$ in the second case.

For the second possibility we have a case analysis according to which condition holds before the additional step is done.

Let us consider the condition (1). Reductions involving only $\mathbb{E}$ leave the process in the same form. For other reductions we proceed by case analysis on the form of $P_l$ (we consider applied forms together with the form they
derive from). For simplicity we do not write `addG` if it does not change. Adding it is however straightforward.

If $P_l = (P_l)l$ we proceed by case analysis on the structure of $P$. If $P = 0$ then we have $\mathbb{E}[\nu l. P_l | S] \to \mathbb{E}[\nu l. l \langle \text{Nil} \rangle | \text{Rew } l | S]$, which satisfies again condition (1). Similarly, if $P = a \langle Q \rangle$ then $\mathbb{E}[\nu l. (a \langle Q \rangle) | S] \to \mathbb{E}[\nu l. \text{Msg } a (Q) | S]$, which satisfies again condition (1). The other cases are similar.

If $P_l = l \langle (P) \rangle$ | Rew $l$ then $\mathbb{E}[\nu l. l \langle (P) \rangle | \text{Rew } l | S]$ can perform several reductions. If Rew $l$ is applied, then we stay in the same case. If Rew $l$ is already in its applied form then $\mathbb{E}[\nu l. l \langle (P) \rangle | l(Z) \triangleright Z l | S] \to \mathbb{E}[\nu l. (P)l | S]$, which again satisfies the conditions. If the message on $l$ is read by $S$ then there are two cases: either it is read by a memory, or by a KillP. In the first case we have that:

$$ 
\begin{align*}
\mathbb{E}[\nu l. l \langle (P) \rangle | \text{Rew } l | (l(Z) \triangleright \text{Msg } a (Q) | l_1) | \text{Trig}(X c) c \langle (R) \rangle | a l_2) | S] &\to \\
\mathbb{E}[\nu l. \text{Rew } l | (\text{Msg } a (Q) | l_1) | (\text{Trig}(X c) c \langle (R) \rangle | a l_2) | S] &\equiv \\
\mathbb{E}'[\nu l. 0 | \text{Rew } l | S]
\end{align*}
$$

which satisfies again condition (1) since $\nu l. 0 | \text{Rew } l \in \text{addG}(\nu l. 0)$. If the message is read by a KillP then the context contains also a message on channel $h$ such that:

$$ 
\begin{align*}
\mathbb{E}[\nu l. l \langle (P) \rangle | \text{Rew } l | S] &\equiv \\
\mathbb{E}_1[\nu l. h \langle (Q) \rangle | l \langle (P) \rangle | (l(Z)|h(W) \triangleright k \langle (h)\text{Par } Z W h \rangle | \text{Rew } k) | S] &\to \\
\mathbb{E}_1[(\nu l. 0 | S) | k \langle (h)\text{Par } (Q) (P) h \rangle | \text{Rew } k] &\equiv \mathbb{E}_2[\nu l. 0 | S]
\end{align*}
$$

which satisfies again condition (1).

If $P_l = \text{Msg } a (Q) | l$ or $P_l = \text{Trig } Y a l$ we have a few cases. If $P_l$ reduces alone then it is simply applied, and its applied form is still an $l$-process. Note that neither $S$ nor the context can interact with such a $P_l$ before application.

Let us consider applied forms of $P_l = \text{Msg } a (Q) | l$. With one application we get $P_l = a \langle (Q), l \rangle | \text{KillM } a l$. In this case $\mathbb{E}[\nu l. P_l | S]$ can perform several reductions. If KillM is not in its applied form and it is applied, then the thesis banally follows. If KillM is in its applied form, then it can interact with the message. In this case, we have that

$$ 
\begin{align*}
\mathbb{E}[\nu l. a \langle (Q), l \rangle | (a(X, \setminus l) \triangleright l \langle (h)\text{Msg } a (Q) h \rangle | \text{Rew } l) | S] &\to \\
\mathbb{E}[\nu l. l \langle (h)\text{Msg } a (Q) h \rangle | (\text{Rew } l) | S]
\end{align*}
$$
and condition (1) still holds. If the message is read by the context, then it is read either by a **KillM** (in its applied form) or by a **Trig** (in its applied form). The first case has been treated just above. In the second case (we only need to consider the trigger, and the token $\bar{t}$ needed for its activation) we have that

$$ \mathbb{E}[\nu l. a \langle (Q), l \rangle | (\text{KillM } a l) | S] \equiv $$

$$ \mathbb{E}_1[\nu l. a \langle (Q), l \rangle | \bar{t} | (a(X, h)|t \triangleright \nu k, c. (((X c)c \langle (P) \rangle) X c) | (c(Z) \triangleright Z k) | (\text{Mem } Y a X h k l)) | (\text{KillM } a l) | S] \to $$

$$ \mathbb{E}_1[\nu l, k, c. (((X c)c \langle (P) \rangle) (Q) c) | (c(Z) \triangleright Z k) | (\text{Mem } Y a (P) l k l_1) | S] \equiv $$

$$ \mathbb{E}_2[\nu l. (\text{Mem } Y a (P) l k l_1) | S] $$

and condition (1) still holds.

Let us consider applied forms of $P_l = \text{Trig } Y a l$, i.e., $P_l = \nu t. \bar{t} | (a(X, h)|t \triangleright R) | (\text{KillT } Y t l a)$ where $R = \nu k, c. (Y X c) | (c(Z) \triangleright (Z k)) | (\text{Mem } Y a X h k l)$ and $Y = (X c)c \langle (Q) \rangle$. In this case $\mathbb{E}[\nu l. P_l | S]$ can perform several reductions. If the **KillT** is applied then the thesis banally follows. If the **KillT** is in its applied form then it can interact with $\bar{t}$:

$$ \mathbb{E}[\nu l, t. \bar{t} | (a(X, h)|t \triangleright_f R) | (t \triangleright l \langle (h) \text{Trig } Y a h \rangle) | \text{Rew } l) | S] \to $$

$$ \mathbb{E}[\nu l, t. (a(X, h)|t \triangleright_f R) | l \langle (h) \text{Trig } Y a h \rangle | \text{Rew } l | S] \equiv $$

$$ \mathbb{E}_1[\nu l. l \langle (h) \text{Trig } Y a h \rangle | \text{Rew } l | S] $$

as desired since $l \langle (h) \text{Trig } Y a h \rangle | \text{Rew } l \in \text{addG}((a(X) \triangleright Q))$. The only other possibility is that the trigger reads a message from the context. Thanks to Lemma 59 the message should be of the form $a \langle (P), l_1 \rangle$ for some $P$ and some $l_1$. Therefore,

$$ \mathbb{E}[\nu l, t. \bar{t} | (a(X, h)|t \triangleright_f R) | (\text{KillT } Y t l a) | S] \equiv $$

$$ \mathbb{E}_1[\nu l, t. \bar{t} | a \langle (P), l_1 \rangle | (a(X, h)|t \triangleright_f R) | (\text{KillT } Y t l a) | S] \to $$

$$ \mathbb{E}_1[\nu l, k, t, c. (((X c)c \langle (Q) \rangle) (P) c) | (c(Z) \triangleright Z k) | (\text{Mem } Y a (P) l_1 k l) | S] \equiv $$

$$ \mathbb{E}_2[\nu k. (((X c)c \langle (Q) \rangle) (P) c) | (c(Z) \triangleright Z k) | \nu l. (\text{Mem } Y a (P) l_1 k l) | S] \equiv $$

$$ \mathbb{E}_3[\nu l. (\text{Mem } Y a (P) l_1 k l) | S] $$

where condition (1) holds for name $l$. Note that condition (1) holds also for the new name $k$.

If $P_l = \text{Par} (P) (Q) l$ then we have that $\mathbb{E}[\nu l. (\text{Par} (P) (Q) l) | S] \to \mathbb{E}[\nu l, h, k. (P)h | (Q)k | (\text{KillP } h k l)]$, and we have that condition (1) is still satisfied by name $l$ and also by the new names $h$ and $k$.
If $P_l = \text{KillP} h k l$ and it reduces alone then it is applied, and condition (1) still holds. $P_l$ may interact with the context only if it is in its applied form and there are two messages, one on $h$ and one on $k$. Thanks to Lemma 57 they should contain translations of processes, thus:

$$ 
\begin{align*}
\mathbb{E}[\nu l. (h(W) | k(Z) \triangleright l \langle\langle (h)\mathbf{Par} W Z h \rangle | \mathbf{Rew} l)] &\equiv \\
\mathbb{E}_1[\nu l. (h(W) | k(Z) \triangleright l \langle\langle (h)\mathbf{Par} W Z h \rangle | \mathbf{Rew} l) | h(\langle\langle P \rangle\rangle) | k(\langle\langle Q \rangle\rangle)] &\hookrightarrow \\
\mathbb{E}[\nu l. l \langle\langle (h)\mathbf{Par} (\langle\langle P \rangle\rangle) (\langle\langle Q \rangle\rangle) h \rangle | \mathbf{Rew} l]
\end{align*}
$$

and condition (1) still holds.

If $P_l = \nu u. (\langle\langle P \rangle\rangle l$ then we can move the restriction into the context and reduce to the case $P_l = (\langle\langle P \rangle\rangle l$.

If $P_l = \nu c. (Y (\langle\langle P \rangle\rangle c) | (c(Z) \triangleright Z l) | (\text{Mem } Y a (\langle\langle P \rangle\rangle l_1 l l_2))]$ then $\mathbb{E}[\nu l. (P_l | S)]$ can perform two kinds of reductions. If the Mem process is applied then condition (1) is still satisfied. Since $c$ and $l$ are restricted, the only other possible reduction is the application of $Y = (X c)c(\langle\langle Q \rangle\rangle)$. Thus:

$$ 
\begin{align*}
\mathbb{E}[\nu l, c. (Y (\langle\langle P \rangle\rangle c) | (c(Z) \triangleright Z l) | (\text{Mem } Y a (\langle\langle P \rangle\rangle l_1 l l_2))] &\rightarrow \\
\mathbb{E}[\nu l, c. c(\langle\langle Q \rangle\rangle \{\langle\langle P \rangle\rangle / X\}) | (c(Z) \triangleright Z l) | (\text{Mem } Y a (\langle\langle P \rangle\rangle l_1 l l_2))]
\end{align*}
$$

and condition (1) still holds. The case where the memory is in its applied form is analogous.

If $P_l = \nu c. c(\langle\langle P \rangle\rangle) | (c(Z) \triangleright Z l) | (\text{Mem } Y a (\langle\langle P \rangle\rangle l_1 l l_2))$ and the Mem process is applied then condition (1) holds. Since $c$ and $l$ are restricted, the only possible communication is the internal one along $c$:

$$ 
\begin{align*}
\mathbb{E}[\nu l, c. c(\langle\langle P \rangle\rangle) | (c(Z) \triangleright Z l) | (\text{Mem } Y a (\langle\langle P \rangle\rangle l_1 l l_2))] &\hookrightarrow \\
\mathbb{E}[\nu l, c. (\langle\langle P \rangle\rangle l) | (\text{Mem } Y a (\langle\langle P \rangle\rangle l_1 l l_2))] &\equiv \\
\mathbb{E}[\nu l. (P_l | S)]
\end{align*}
$$

where condition (1) still holds. The case where the memory is in its applied form is analogous.

If $P_l = \text{Mem } Y a (\langle\langle P \rangle\rangle l k h$ and the Mem is applied, then the thesis banally follows. If the Mem process is already in its applied form, then it may only interact with the context via a message on $k$. Hence, we have

$$ 
\begin{align*}
\mathbb{E}[\nu l. k(Z) \triangleright_b (\text{Msg } a (\langle\langle P \rangle\rangle l) | (\text{Trig } Y a h))] &\equiv \\
\mathbb{E}_1[\nu l. k \langle\langle R \rangle\rangle | k(Z) \triangleright_b (\text{Msg } a (\langle\langle P \rangle\rangle l) | (\text{Trig } Y a h))] &\rightsquigarrow \\
\mathbb{E}_1[(\nu l. (\text{Msg } a (\langle\langle P \rangle\rangle l)) | \text{Trig } Y a h] &\equiv \\
\mathbb{E}_2[\nu l. (\text{Msg } a (\langle\langle P \rangle\rangle l))]
\end{align*}
$$
and condition (1) still holds.

The case $P_l = (\mathbf{Mem} Y a (\mathcal{P}) h k l)$ is similar.

Since $\mathbf{0}$ has no reduction, in the case $P_l = \mathbf{0}$ there is nothing to prove.

Let us consider conditions (2), (3) and (4). If the context evolves by itself, then they are still satisfied. For the hole to contribute, the only possibility is that the context is an evaluation context. For condition (2), we have a case analysis on the form of $\mathcal{C}'$. If $\mathcal{C}' = \bullet$, then $\mathcal{C}[\nu h. ((l)P_l)h] \to \mathcal{C}[\nu h. P_h]$, the name $l$ disappears and the thesis trivially holds. If $\mathcal{C}' = (l')\mathbf{Msg} a \mathcal{C}''[\bullet] l'$ then we have $\mathcal{C}[\nu h. ((l')\mathbf{Msg} a \mathcal{C}''[(l)P_l] l')h] \to \mathcal{C}[\nu h. \mathbf{Msg} a \mathcal{C}''[(l)P_l] h]$. Name $l$ disappears, thus the thesis holds trivially. Note that condition (2) holds for name $h$. The other cases for contexts in non-applied form are analogous.

Let us now consider contexts where the toplevel application has been performed. Again we have a case analysis on the form of the context. If the context has the form $\mathcal{C}[\nu h. \mathbf{Msg} a \mathcal{C}'[(l)P_l] h]$, then we have that $\mathcal{C}[\nu h. \mathbf{Msg} a \mathcal{C}'[(l)P_l] h] \to \mathcal{C}[\nu h. a \langle \mathcal{C}'[(l)P_l], h \rangle | \text{KillM} a h]$ and condition (2) still holds. The other cases are similar.

If condition (3) holds, we have that $\mathcal{C}[\nu l. ((h)P_h)l] \to \mathcal{C}[\nu l. P_l]$, and condition (1) holds for name $l$.

If condition (4) holds, we have that:

$$ \mathcal{C}[\nu l, c. (((X c)\langle\langle P \rangle\rangle)(Q) c) | (c(Z) \triangleright Z l) | (\mathbf{Mem} (X c)\langle\langle P \rangle\rangle) a (Q) h l k)] \to \\ \mathcal{C}[\nu l, c. c\langle\langle P \rangle\rangle\{\mathcal{Q}/X\}] | (c(Z) \triangleright Z l) | (\mathbf{Mem} (X c)\langle\langle P \rangle\rangle) a (Q) h l k)] = \\ \mathcal{C}[\nu l, c. c\langle\langle P\{Q/X\}\rangle\rangle] | (c(Z) \triangleright Z l) | (\mathbf{Mem} (X c)\langle\langle P \rangle\rangle) a (Q) h l k)] $$

by applying Lemma 21. Condition (1) holds for the name $l$. If the reduction involves the application of the Mem process, then condition (1) for name $l$ is still satisfied. $\square$

**Lemma 29.** For each consistent $\text{HO}\pi^+$ process $P$ if $P \hookrightarrow^* Q$ then there exist $Q'$ and $P'$ such that $Q \hookrightarrow^* Q'$, $P' \in \text{addG}(P)$ with $\text{nf}(P') \equiv_{E_x} \text{nf}(Q')$.

**PROOF.** By induction on the number $n$ of steps in $P \hookrightarrow^* Q$. In the base case ($n = 0$) the thesis banally follows. For the inductive case, consider the first step $P \hookrightarrow Q_1$ of $P \hookrightarrow^* Q$. There are two cases to distinguish: whether $\hookrightarrow$ is an application $\to$ or a non-labelled communication $\mapsto$. Let us consider the first case. We have that $P \to Q_1$ and $Q_1 \hookrightarrow^* Q$. By inductive hypothesis there exist $Q', Q'_1$ such that $Q \hookrightarrow^* Q'$, $Q'_1 \in \text{addG}(Q_1)$ and $\text{nf}(Q'_1) \equiv_{E_x} \text{nf}(Q')$. Since the added garbage does not forbid reductions we have that
there exists $P' \in \text{addG}(P)$ such that $P' \to Q'_1$. Thus $\text{nf}(P') = \text{nf}(Q'_1) \equiv_{Ex} \text{nf}(Q')$ as desired.

If the step is a non-labelled communication $\mapsto$ then we have three cases, corresponding to the three kinds of non-labelled trigger processes: a **Rew** process, a killer process and the trigger in the translation of the continuation of a rho$\pi$ trigger.

Let us consider the case of a **Rew** process. We have that $P \equiv \mathbb{E}[l\langle(\langle P_1\rangle)\rangle | l(Z) \triangleright Z l] \to \mathbb{E}[(\langle P_1\rangle)l]$. By using Lemma 23 and Lemma 16 we have that $(\langle P_1\rangle)l \mapsto^* l\langle(\langle P_2\rangle)\rangle | \text{Rew } l | S$ with $S$ a parallel composition of garbage processes. Thanks to Lemma 57, $P_1$ has no toplevel restrictions (since it was argument of a message), thus $P_2 = P_1$. So, we have that $\mathbb{E}[(\langle P_1\rangle)l] \mapsto^* \mathbb{E}[l\langle(\langle P_1\rangle)\rangle | \text{Rew } l | S] \in \text{addG}(P)$. Now from $\mathbb{E}[(\langle P_1\rangle)l] \mapsto^* Q$ we have that by inductive hypothesis $Q \mapsto^* Q'$ and there is $P' \in \text{addG}(\mathbb{E}[(\langle P_1\rangle)l])$ such that $\text{nf}(P') \equiv_{Ex} \text{nf}(Q')$. Since the garbage does not forbid reductions we have that there exists $P'' \in \text{addG}(\mathbb{E}[l\langle(\langle P_1\rangle)\rangle | \text{Rew } l | S])$ such that $P' \mapsto^* P''$. From Lemma 26 $\text{nf}(P') \mapsto^* \text{nf}(P'')$. Thanks to Lemma 27 from $\text{nf}(P') \equiv_{Ex} \text{nf}(Q')$ and $P' \mapsto^* P''$ we have that $\text{nf}(Q') \mapsto^* \text{nf}(Q'')$ with $P''' \in \text{addG}(P'')$ and $\text{nf}(P''') \equiv_{Ex} \text{nf}(Q'')$. By composing garbage we also have $P''' \in \text{addG}(P)$. The thesis follows.

Let us consider the case of a killer process. We have a few subcases, corresponding to the killer processes **KillM**, **KillP** and **KillT**. The main idea here is that the communication is undone by a **Rew**. Let us consider a **KillM** process. We have that $P \equiv \mathbb{E}[a\langle(\langle P_1\rangle), l\rangle | (a(X, \setminus l) \triangleright l\langle(h)\text{Msg } a X h\rangle | \text{Rew } l)]$ and $Q_1 = \mathbb{E}[\langle(h)\text{Msg } a(\langle P_1\rangle)h\rangle | \text{Rew } l]$. Then we have:

$$ Q_1 \to \mathbb{E}[l\langle(h)\text{Msg } a(\langle P_1\rangle)h\rangle | l(Z) \triangleright Z l] \mapsto \\ \mathbb{E}[(h)\text{Msg } a(\langle P_1\rangle)h]l \to^* \mathbb{E}[a\langle(\langle P_1\rangle), l\rangle | (\text{KillM } a l)] = Q' $$

with $\text{nf}(Q') = \text{nf}(P)$. Using the same approach of the **Rew** case, we can compose this result with the inductive hypothesis to get the thesis. Let us consider a **KillP** process. We have that $P \equiv \mathbb{E}[h\langle(\langle P_1\rangle)\rangle | l\langle(\langle Q\rangle)\rangle | (h(W)|l(Z) \triangleright k\langle(h)\text{ParW } Z h\rangle | \text{Rew } k)]$ and $Q_1 = \mathbb{E}[k\langle(h)\text{Par}(\langle P_1\rangle)(\langle Q\rangle)h\rangle | \text{Rew } k]$. Then we have:

$$ Q_1 \to \mathbb{E}[k\langle(h)\text{Par}(\langle P_1\rangle)(\langle Q\rangle)h\rangle | (k(Z) \triangleright Z k)] \to \\ \mathbb{E}[(h)\text{Par}(\langle P_1\rangle)(\langle Q\rangle)h]k \to \mathbb{E}[\nu h, l. (\langle P_1\rangle)l | (\langle Q\rangle)h | (\text{KillP } l h k)] $$

and by using Lemma 23 and Lemma 57 (to ensure that processes $P_1$ and $Q$
have no toplevel restrictions) we have:

$$ \begin{aligned} & \mathbb{E}[\nu h, l. (P_1)l | (Q)h | (\text{KillP } l h k)] \hookrightarrow^* \\ & \mathbb{E}[\nu h, l. l \langle (P_1) \rangle | S_1 | h \langle (Q) \rangle | S_2 | (\text{KillP } l h k)] = Q' \end{aligned} $$

To have a correspondence with $P$, we have to show that names $h$ and $l$ were restricted also in $P$, and with the same scope. By using Lemma 60 we have that $P \equiv \mathbb{E}_1[\nu l, h. P']$ for some $P' \in \text{addG}(h \langle (P_1) \rangle | l \langle (Q) \rangle | S)$ (where $S$ includes $(\text{KillP } l h k)$, $\text{Rew } l$ and $\text{Rew } h$), and

$$ \mathbf{nf}(\mathbb{E}_1[\nu l, h. P']) \equiv \mathbf{nf}(Q'') $$

for some $Q'' \in \text{addG}(Q')$ as desired.

If the communication is an internal communication in a trigger, we have that

$$ \begin{aligned} P &\equiv \mathbb{E}[\nu c. c \langle (P_1) \rangle | c(Z) \triangleright Z k] \hookrightarrow \\ \mathbb{E}[\nu c. (P_1)k] &\equiv_{Ex} \mathbb{E}[\nu c. c \langle (P_1) \rangle | c(Z) \triangleright Z k] \end{aligned} $$

as desired using axiom $\mathbf{AX.ADM.}$

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

## Appendix C.3. Proofs of Section 4.5

Before proving Lemma 30 we show that barbs are preserved by the encoding.

**Lemma 61.** For each consistent configuration $M$, if $M \downarrow_a$ then $\mathbf{nf}((M)) \downarrow_a$

**PROOF.** Easy, by definition of barbs and of the encoding.

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

**Lemma 30.** If $M \downarrow_a$ and $((M)) \hookrightarrow^* Q$ then $Q \hookrightarrow^* \downarrow_a$.

**PROOF.** By Lemma 61 we have that if $M \downarrow_a$ then $\mathbf{nf}((M)) \downarrow_a$. By definition of normal form we have that $((M)) \to_*^* \mathbf{nf}((M))$, and by hypothesis we have that $((M)) \to_*^* Q$. Using Lemma 26 we have that $\mathbf{nf}(M) \to_*^* Q'$ and $Q \to_*^* Q'$. Moreover, by Lemma 29 there exist $Q''$ and $P'$ such that $Q' \to_*^* Q''$, $P' \in \text{addG}(\mathbf{nf}((M)))$ and $\mathbf{nf}(P') \equiv_{Ex} \mathbf{nf}(Q'')$. Since $\text{addG}$ and $\equiv_{Ex}$ do not remove barbs we have $\mathbf{nf}(Q'') \downarrow_a$ as desired. The proof is graphically depicted in Figure C.18. $\square$

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

Before proving Lemma 31 below we prove some auxiliary results. Applications never remove barbs.
<figure><img src="image_21.png" /><figcaption>Figure C.18: Correspondence schema of barbs (numbers refer to Lemmas).</figcaption></figure>

**Lemma 62.** For any $HO\pi^+$ process $P$, if $P \downarrow_a$ and $P \to Q$, then also $Q \downarrow_a$.

**PROOF.** From the definition of $\downarrow_a$ and of $\to$. $\square$

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

Administrative steps do not add barbs.

**Lemma 63.** For each consistent configuration $M$, if $\langle M \rangle \hookrightarrow^* Q$ and $Q \downarrow_a$, then $\mathrm{nf}(\langle M \rangle) \downarrow_a$.

**PROOF.** By hypothesis $\langle M \rangle \hookrightarrow^* Q$ with $Q \downarrow_a$, and by definition $\langle M \rangle \to^* \mathrm{nf}(\langle M \rangle)$. By applying Lemma 26 we get $Q \to^* Q'$ and $\mathrm{nf}(\langle M \rangle) \to^* Q'$. Since $Q \downarrow_a$, and since applications ($\to$) do not remove barbs (by Lemma 62), we also have that $Q' \downarrow_a$. The above reasoning is depicted in Figure C.19.

We have to show that if $Q'$ has a barb then $\mathrm{nf}(\langle M \rangle)$ has the same barb. Since $M$ is consistent then $\mathrm{fn}(M) \cap K = \emptyset$ and also $\mathrm{fn}(Q) \cap K = \emptyset$ (by Lemma 22). Thus we have no need to consider barbs in $K$.

We proceed by case analysis on the administrative reduction $\hookrightarrow$. Since $Q'$ is generated from $\mathrm{nf}(\langle M \rangle)$ via administrative steps, then applications of the form (((X c)c\langle\langle P \rangle\rangle)\langle Q \rangle c) or communications of the form $c\langle\langle P \rangle\rangle | (c(Z) \triangleright Z l)$ are never enabled. Thus, only communications involving a killer or a *Rew* process may happen. A communication involving a killer does not add barbs (since $\mathrm{fn}(Q') \cap K = \emptyset$). A communication involving a *Rew* process does not add barbs since it produces an application. Similarly, all the applications involving killer, *Rew* and *Mem* processes do not add barbs. Nevertheless, other applications, such as the application of a *Msg* process,
<figure><img src="image_23.png" /><figcaption>Figure C.19: Barbs with respect to administrative steps (numbers refer to Lemmas).</figcaption></figure>

may create barbs. However, no such application is enabled in $nf(|M|)$. The only way they may become enabled is via a kill followed by a *Rew*. However, the created barb was already present in $nf(|M|)$ before the kill. This completes the proof. □

We now show that barbs of $nf(|M|)$ come from barbs of $M$.

**Lemma 64.** For each consistent configuration $M$, if $nf(|M|) \downarrow_a$ then $M \downarrow_a$.

**PROOF.** By structural induction on $M$. Note that only $\rho\sigma\pi$ names may be free, since all the names coming from $\rho\sigma\pi$ keys are bound (by Lemma 22). Since sub-terms of well-formed configurations are not well formed in general, we have to consider in the induction both well-formed configurations and their sub-terms. If $M = \kappa : P$, we proceed by structural induction on $P$ and by case analysis on $\kappa$. We will consider just the case in which $\kappa = k$, the other case with $\kappa = \langle h_i, \tilde{h} \rangle \cdot k$ is similar. If $P = 0$ then we have that $nf(|k : 0|) = k \langle \text{Nil} \rangle | \text{Rew } k$, but since $k \notin \mathcal{N}$ the process $nf(|k : 0|)$ does not show any relevant barb. If $P = a \langle Q \rangle$ then we have that $nf(|k : a \langle Q \rangle|) = a \langle |Q|, k \rangle | (a(X, \setminus k) \triangleright k \langle (h) \text{Msg } a |Q|, h \rangle | \text{Rew } k)$, which shows a barb on $a$. Since also $M \downarrow_a$, we are done. If $P = a(X) \triangleright Q$, we have that $nf(|k : a(X) \triangleright Q|) = \nu t. \bar{t} | (a(X, h)|t \triangleright R)| (t \triangleright S)$ (for some $R$ and $S$). Since $t$ is restricted then the entire process does not show any barb, and we are done. If $P = Q_1 | Q_2$, the tag $\kappa$ has to be a key, since we are dealing with well-formed configurations. So, we have that $nf(|k : (Q_1 | Q_2)|) = \nu h, l. nf(|Q_1|h)| nf(|Q_2|l)| (h(W)|l(Z) \triangleright S)$. The process may show a barb because of either $nf(|Q_1|h)$ or $nf(|Q_2|l)$ (or both). Let us suppose that it is because of $nf(|Q_1|h)$, that is $nf(|Q_1|h) \downarrow_a$. By definition of $|-|$ we have that $nf(|Q_1|h) = nf(|h : Q_1|)$ and hence $nf(|h : Q_1|) \downarrow_a$. Now, by applying the inductive hypothesis we have that $(h : Q_1) \downarrow_a$ and then also $k : (Q_1 | Q_2) \downarrow_a$, as desired. The other cases are similar.
If $M = 0$, we have that $\langle 0 \rangle = 0$ and the thesis banally follows. If $M = M_1 | M_2$ we have that $\mathbf{nf}(\langle M_1 | M_2 \rangle) = \mathbf{nf}(\langle M_1 \rangle | \langle M_2 \rangle) = \mathbf{nf}(\langle M_1 \rangle) | \mathbf{nf}(\langle M_2 \rangle)$ and we can conclude by applying the inductive hypothesis on $\mathbf{nf}(\langle M_1 \rangle)$ and $\mathbf{nf}(\langle M_2 \rangle)$. If $M = \nu u. M_1$ we have that $\mathbf{nf}(\langle \nu u. M_1 \rangle) = \nu u. \langle \mathbf{nf}(M_1) \rangle$ and we can conclude by applying the inductive hypothesis on $\langle \mathbf{nf}(M_1) \rangle$. If $M = [\kappa_1 : a\langle P \rangle | \kappa_2 : a(X) \triangleright Q; k]$, then $\mathbf{nf}(\langle M \rangle) = k(Z) \triangleright R$ (for some $R$), that shows no barbs and we can conclude. $\square$

**Lemma 31.** If $\langle M \rangle \hookrightarrowneq^* \downarrow_a$ then $M \downarrow_a$.

**PROOF.** By concatenating Lemma 63 and Lemma 64. $\square$

Before proving Lemma 33, which shows that the function **addG** has no impact on bfa barbed bisimilarity, we show the same result in isolation for the forms of garbage more tricky to deal with.

**Lemma 65.** Let $T_l$ be a process of the form $T_l = \mathbf{Rew} l$ or $T_l = (l(Z) \triangleright Z l)$. The relation $\mathcal{R} = \{(\mathbb{C}[T_l], \mathbb{C}[0])\}$ is a bfa barbed bisimulation.

**PROOF.** Let us start with barbs. Since $T_l$ does not show barbs, the barbs of $\mathbb{C}[T_l]$ and $\mathbb{C}[0]$ coincide.

Let us consider the reductions. If $\mathbb{C}[T_l]$ reduces then it is either because the context reduces by itself, or because $T_l$ reduces by itself or because of an interaction between the context and $T_l$. In the first case the reduction is banally matched by the process $\mathbb{C}[0]$. The second case implies that $T_l = \mathbf{Rew} l$ and $\mathbb{C}[\mathbf{Rew} l] \to \mathbb{C}[l(Z) \triangleright Z l]$. $\mathbb{C}[0]$ matches this step by staying idle. The third case implies that $T_l = (l(Z) \triangleright Z l)$ and the presence of a message in the context of the form $l\langle\langle P \rangle\rangle$. Hence, we have that $\mathbb{C}[(l(Z) \triangleright Z l)] \equiv \mathbb{C}'[l\langle\langle P \rangle\rangle | (l(Z) \triangleright Z l)]$ and $\mathbb{C}[0] \equiv \mathbb{C}'[l\langle\langle P \rangle\rangle]$. By Lemma 16 we know $\mathbb{C}'[l\langle\langle P \rangle\rangle] \equiv \mathbb{C}''[l\langle\langle P \rangle\rangle | T_l]$. Then on the other side we have that $\mathbb{C}'[l\langle\langle P \rangle\rangle | (l(Z) \triangleright Z l)] \equiv \mathbb{C}''[l\langle\langle P \rangle\rangle | (l(Z) \triangleright Z l) | T_l]$. Thus, the reduction $\mathbb{C}''[l\langle\langle P \rangle\rangle | (l(Z) \triangleright Z l) | T_l] \to \mathbb{C}''[\langle P \rangle l | T_l]$ can be matched on the right side by $\mathbb{C}''[l\langle\langle P \rangle\rangle | T_l] \hookrightarrowneq^* \mathbb{C}''[\langle P \rangle l]$, and we are still in the same relation since $\mathbb{C}''[\langle P \rangle l | T_l] \equiv \mathbb{C}'''[T_l]$ and $\mathbb{C}''[\langle P \rangle l] \equiv \mathbb{C}'''[0]$, as desired. $\square$

**Lemma 66.** Let $T(l, a)$ be a process of the form $T(l, a) = (\mathbf{KillM} a l)$ or $T(l, a) = (a(X, \setminus l) \triangleright l\langle\langle (h)Msg a X h \rangle | \mathbf{Rew} l)$. The relation $\mathcal{R} = \{(\mathbb{C}[T(l, a)], \mathbb{C}[0])\}$ is a bfa barbed bisimulation.
PROOF. Let us consider the barbs. Since a process of the form (KillM a l) or (a(X, \l) ▷ l⟨(h)Msg a X h⟩ | Rew l) does not show any barbs, then the barbs of C[T(l, a)] and C[0] coincide.

Let us consider the reductions. If the context evolves by itself, the reduction is banally matched. If T(l, a) = (KillM a l) then the only possible reduction is the application

$$C[(\text{KillM } a \\ l)] \to C[(a(X, \setminus l) \triangleright l \langle (h) \text{Msg } a X h \rangle | \text{Rew } l)]$$

which is matched by C[0] by staying idle. If in C[(a(X, \l)▷l⟨(h)Msg a X h⟩ | Rew l)] the hole process and the context interact, it is because there is a message of the form a⟨⟨P⟩⟩, l⟩ in the context. Hence

$$C[(a(X, \setminus l) \triangleright l \langle (h) \text{Msg } a X h \rangle | \text{Rew } l)] \equiv \\ C'[a(\langle P \rangle, l) | (a(X, \setminus l) \triangleright l \langle (h) \text{Msg } a X h \rangle | \text{Rew } l)]$$

This implies that also C[0] ≡ C'[a⟨⟨P⟩⟩, l]⟩, and by Lemma 17 we know that C'[a⟨⟨P⟩⟩, l]⟩ ≡ C''[a⟨⟨P⟩⟩, l] | S] with S = (KillM a l) or S = (a(X, \l) ▷ l⟨(h)Msg a X h⟩ | Rew l). Then

$$C'[a(\langle P \rangle, l) | (a(X, \setminus l) \triangleright l \langle (h) \text{Msg } a X h \rangle | \text{Rew } l)] \equiv \\ C''[a(\langle P \rangle, l) | (a(X, \setminus l) \triangleright l \langle (h) \text{Msg } a X h \rangle | \text{Rew } l) | S] \hookrightarrow \\ C'''[l \langle (h) \text{Msg } a (\langle P \rangle) h \rangle | \text{Rew } l) | S] \equiv C''''[S]$$

and on the other side we have that

$$C''[a(\langle P \rangle, l) | S] \hookrightarrow^* C''[l \langle (h) \text{Msg } a (\langle P \rangle) h \rangle | \text{Rew } l] \equiv C'''[0]$$

and we remain in the same relation, as desired. □

**Lemma 33.** For any consistent HOπ⁺ process P, the relation $R = \{(P, R) | R \in \text{addG}(P)\}$ is a bfa barbed bisimulation.

PROOF. From the definition of addG we know that P ≡ ν̃a. P', and R ≡ ν̃a. (P' | ν̃b. Q) with Q a parallel composition of processes as in Definition 17.

The proof is by induction on the number of parallel components inside Q. The base case Q = 0 reduces to the identity since we can can garbage collect via structural congruence names contained in b̃ (and structural congruence is a bfa barbed bisimulation by Lemma 34). In the inductive case, we do a case analysis on the last process Qn of the parallel composition.
$Q_n = \text{Rev } l$: by Lemma 65 we know that $\mathbb{C}[Q_n] \stackrel{\cdot}{=} \mathbb{C}[0]$. By choosing $\mathbb{C}[\bullet] = \nu\tilde{a}. (P' | \nu\tilde{b}. \bullet | \prod_{i=1..n-1} Q_i)$ we have that $\nu\tilde{a}. (P' | \nu\tilde{b}. \prod_{i=1..n} Q_i) \stackrel{\cdot}{=} \nu\tilde{a}. (P' | \nu\tilde{b}. \prod_{i=1..n-1} Q_i)$. By inductive hypothesis we have $\nu\tilde{a}. (P' | \nu\tilde{b}. \prod_{i=1..n-1} Q_i) \stackrel{\cdot}{=} \nu\tilde{a}. P'$ and by transitivity $\nu\tilde{a}. (P' | \nu\tilde{b}. \prod_{i=1..n} Q_i) \stackrel{\cdot}{=} \nu\tilde{a}. P'$. □

$Q_n = \text{KillM } a, l$: similar to the case above, using Lemma 66 instead of Lemma 65.

$Q_n = \nu t. (a(X, k)|t \triangleright Q)$: trivial, since the process cannot interact.

$Q_n = \nu c, t. (\text{KillT}((X)c(\mathbb{P}))) t l a$): trivial, since the process reduces to a process that cannot interact. □

Before proving Proposition 1 below, we prove some auxiliary results.

Each of the lemmas below shows that one of the axioms in $\equiv_{Ex}$ is correct with respect to bfa barbed bisimilarity (actually, the statement for axiom Ax.P is slightly weaker). We consider together each axiom $L \equiv_{Ax} R$ from $\equiv_{Ax}$ and its normal form $nf(L) \equiv_{Ex} nf(R)$, since this is obtained via applications. Below, we denote a multi-holes context as $\mathbb{C}$.

**Lemma 67.** Axiom Ax.C and its normal form are correct with respect to bfa barbed bisimilarity.

**PROOF.** We show that the relation $\mathcal{R}$ below is a bfa barbed bisimulation.

$$ \mathcal{R}_1 = \{((\text{KillP } l h k), (\text{KillP } h l k)) \mid h, l, k \in \mathcal{K}\} $$

$$ \mathcal{R}_2 = \{((a(X)|b(Y) \triangleright R), (b(Y)|a(X) \triangleright R)) \mid a, b \in \mathcal{N} \wedge X, Y \in \mathcal{V} \wedge R \in \mathcal{P}\} $$

$$ \mathcal{R}' = \mathcal{R}_1 \cup \mathcal{R}_2 $$

$$ \mathcal{R} = \{(\mathbb{C}[P_1, \dots, P_n], \mathbb{C}[Q_1, \dots, Q_n]) \mid n \in \mathbb{N} \wedge \forall i \in \{1 \dots n\}. (P_i, Q_i) \in \mathcal{R}'\} $$

Let us consider the barbs. Since the context is the same on both the sides, and the processes in the holes show no barbs, the barbs coincide.

Let us consider reductions. We consider only challenges from the left, since the reasoning is analogous for challenges from the right. If the process $\mathbb{C}[P_1, \dots, P_n]$ does a reduction, it is because either the context evolves by itself, or one of the hole processes reduces by itself, or because of an interaction between the context and one hole (no interaction between holes is possible).
If the context performs a reduction by itself, that is $\mathbb{C}[P_1, .., P_n] \to \mathbb{C}'[P_1, .., P_m]$, then also $\mathbb{C}[Q_1, .., Q_n] \to \mathbb{C}'[Q_1, .., Q_m]$. Note that the number of holes may change because of the reduction.

Let us consider reductions in one hole. If $\mathbb{C}[P_1, .., (\text{KillP } l h k), .., P_n] \to \mathbb{C}[P_1, .., (h(W)|l(Z)\triangleright R), .., P_n]$ (for some $R$) then also $\mathbb{C}[Q_1, .., (\text{KillP } h l k), .., Q_n] \to \mathbb{C}[Q_1, .., (l(Z)|h(W)\triangleright R), .., Q_n]$ and we are still in the same relation.

Let us consider interactions between the context and one hole. For $\mathbb{C}[P_1, .., a(X)|b(Y)\triangleright R, .., P_n]$ to reduce, we need in the context two messages of the form $a\langle S_1 \rangle$ and $b\langle S_2 \rangle$. If so, we have that $\mathbb{C}[P_1, .., a(X)|b(Y)\triangleright R, .., P_n] \to \mathbb{C}'[P_1, .., R\{S_1,S_2/X,Y\}, .., P_m]$ and on the other side $\mathbb{C}[Q_1, .., b(Y)|a(X)\triangleright R, .., Q_n] \to \mathbb{C}'[Q_1, .., R\{S'_2,S'_1/X,Y,X\}, .., Q_m]$. Since identity is included in $\mathcal{R}$ (it suffices to consider a 0-ary context), and since $(S_i, S'_i) \in \mathcal{R}$ (since they are subterms) we have $(R\{S_1,S_2/X,Y\}, R\{S'_2,S'_1/Y,X\}) \in \mathcal{R}$, and also $(\mathbb{C}'[P_1, .., R\{S_1,S_2/X,Y\}, .., P_m], \mathbb{C}'[Q_1, .., R\{S'_2,S'_1/Y,X\}, .., Q_m]) \in \mathcal{R}$, as desired. $\square$

Before proving the lemma concerning axiom AX.P we prove as auxiliary result that the function addG does not introduce barbs.

**Lemma 68.** For any $HO\pi^+$ process $P$, if addG($P$) $\downarrow_a$ then $P \downarrow_a$.

**PROOF.** Easy, by looking at the definition of addG (Definition 17). $\square$

**Lemma 69.** *Applications of axiom AX.P and of its normal form to consistent $HO\pi^+$ processes are correct with respect to bfa barbed bisimilarity.*

**PROOF.** Note that the axiom AX.P alone is not correct, since the left term has barbs at $l_1$ and $l_2$ which are not matched by the right term. However, in consistent processes keys are always bound. We show below that applications of the axiom and of its normal form to consistent processes are always correct.

Thanks to Lemma 60 restrictions on $l_1$ and $l_2$ may occur only in processes of some forms. In particular, the only possibility is that for both $l_1$ and $l_2$ case (1) applies. Thus the process to which the axiom is applied is of the form $\mathbb{E}[\nu l_1, l_2. R']$ with $R' \in \text{addG}(R'')$ where $R''$ is obtained via zero or more applications from $l_1\langle (P) \rangle | l_2\langle (Q) \rangle | (\text{KillP } l_1 l_2 l_3)$. On the right side we can assume $l_1$ and $l_2$ do not occur.

Let $S(l_1, l_2, l_3)$ denote a process of one of the following forms:

$$S(l_1, l_2, l_3) = (\text{KillP } l_1 l_2 l_3)$$

$$S(l_1, l_2, l_3) = (l_1(Z)|l_2(W) \triangleright l_3 \langle (h)\text{Par } Z W h \rangle | \text{Rew } l)$$
Let $T_l$ be either a process of the form $T_l = \text{Rew } l$ or of the form $T_l = (l(Z) \triangleright Z l)$. Let us write $\text{addG}(P)$ for any process $Q \in \text{addG}(P)$. Let

$$
\begin{align*}
\mathcal{R}' &= \{(\nu l_1, l_2. \text{addG}(l_1\langle (P)\rangle | l_2\langle (Q)\rangle | S(l_1, l_2, l))), \\
&\qquad (\nu l_1, l_2. \text{addG}(l\langle (h)\text{Par } (P)\rangle (Q) | h) | T_l))\} \\
\mathcal{R} &= \{(\mathbb{C}[P_1, \dots, P_n], \mathbb{C}[Q_1, \dots, Q_n]) | (P_i, Q_i) \in \mathcal{R}' \wedge \\
&\qquad \mathbb{C}[P_1, \dots, P_n], \mathbb{C}[Q_1, \dots, Q_n] \text{ consistent}\}
\end{align*}
$$

We now prove that the relation $\mathcal{R}$ is a bfa barbed bisimulation. The thesis
will follow since in consistent processes all the contexts where the axiom can
be applied have this form.

Let us consider barbs. On both sides barbs shown by the contexts $\mathbb{C}$ are banally matched. The process $\nu l_1, l_2$. $\text{addG}(l_1\langle(P)\rangle | l_2\langle(Q)\rangle | S(l_1, l_2, l))$ does not show any barb, since $\text{addG}$ does not add any barb thanks to Lemma 68. On the other side, the process $\nu l_1, l_2$. $\text{addG}(l\langle(h)\text{Par } (P)\rangle (Q) | h) | T_l)$ shows only a barb at $l$. We have that:

$$
\begin{array}{l}
\nu l_1, l_2. \text{addG}(l_1 \langle (P) \rangle | l_2 \langle (Q) \rangle | S(l_1, l_2, l)) \hookrightarrow^* \\
\qquad \nu l_1, l_2. \text{addG}(l \langle (h) \text{Par } (P) \rangle (Q) | h) | \text{Rew } l)
\end{array}
$$

showing a barb at *l* as well.

Let us consider reductions. If $\mathbb{C}[P_1, \dots, P_n]$ reduces it is because the context reduces by itself or because of the hole processes. The first case is banally matched by the process $\mathbb{C}[Q_1, \dots, Q_n]$. In the second case, the process $\nu l_1, l_2$. $\text{addG}(l_1\langle(P)\rangle | l_2\langle(Q)\rangle | S(l_1, l_2, l))$ reduces. We have three cases: the processes added by $\text{addG}$ are not involved, the processes added by $\text{addG}$ reduce alone or they interact with the other processes. In the first case, if the reduction is the application of the process $S(l_1, l_2, l)$ then the right process can match the reduction by staying idle. If it is a communication on the channels $l_1$ and $l_2$ then we have that:

$$
\nu l_1, l_2. \text{addG}(l_1 \langle (P) \rangle | l_2 \langle (Q) \rangle | (l_1(W) | l_2(Z) \triangleright l \langle (h) \text{Par } (P) \rangle (Q) | h) | \text{Rew } l)) \to \\
\nu l_1, l_2. \text{addG}(l \langle (h) \text{Par } (P) \rangle (Q) | h) | \text{Rew } l))
$$

This step is matched by the right process by staying idle, since the process
in the *i*-th hole on the two sides become equal, and we can put them in
the context since the identity belongs to the relation (actually, processes
added by **addG** may be different, but they have no impact). The case where
processes inside addG reduce alone is banally matched. In the third case, since the process $\nu l_1, l_2$. addG($l_1 \langle (P) \rangle | l_2 \langle (Q) \rangle | S(l_1, l_2, l)$) is consistent then the only processes inside addG(-) able to interact are a $(l_1(Z) \triangleright Z l_1)$ and/or a $(l_2(Z) \triangleright Z l_2)$. The two cases are similar, so we consider just the first one. Assume

$$ \nu l_1, l_2. \text{addG}((l_1(Z) \triangleright Z l_1) | l_1 \langle (P) \rangle | l_2 \langle (Q) \rangle | S(l_1, l_2, l)) \hookrightarrow \\ \nu l_1, l_2. \text{addG}((\langle P \rangle l_1 | l_2 \langle (Q) \rangle | S(l_1, l_2, l)) $$

We have

$$ \nu l_1, l_2. \text{addG}(l \langle (h) \text{Par} (P) (Q) h \rangle | T_l) \hookrightarrow^* \\ \nu l_1, l_2. \text{addG}(\nu h, k. (P) h | (Q) k | (\text{KillP} h k l)) $$

Using Lemma 23:

$$ \nu l_1, l_2. \text{addG}(\nu h, k. (P) h | (Q) k | (\text{KillP} h k l)) \hookrightarrow^* \\ \nu l_1, l_2. \text{addG}(\nu h, k. (P) h | k \langle (Q) \rangle | (\text{KillP} h k l)) $$

since all the garbage can be moved to addG and since $Q$ does not contain restrictions thanks to Lemma 57. Now, using $\alpha$-conversion to swap names $l_1$ and $l_2$ with $h$ and $k$ and exploiting the fact that addG is closed under $\alpha$-conversion we get $\nu h, k$. addG($\nu l_1, l_2$. ($\langle P \rangle l_1 | l_2 \langle (Q) \rangle | (\text{KillP} l_1 l_2 l)$). Since $h, k$ are just used by the addG(-) context we can rewrite the process as $\nu l_1, l_2$. addG($\langle P \rangle l_1 | l_2 \langle (Q) \rangle | (\text{KillP} l_1 l_2 l)$), where the restriction on $k, h$ has been moved to the context.

Let us consider now the reductions of $C[Q_1, \dots, Q_n]$. We have three cases: the context reduces by itself, the hole reduces by itself or the hole and the context interact. The first case is trivial. In the second case, if the reduction is the application of $T_l$ then the step is matched by $C[P_1, \dots, P_n]$ by staying idle, and we are still in the same relation. If $T_l$ is already in its applied form then we have:

$$ \nu l_1, l_2. \text{addG}(l \langle (h) \text{Par} (P) (Q) h \rangle | l(Z) \triangleright Z l) \rightarrow \\ \nu l_1, l_2. \text{addG}(\text{Par} (P) (Q) l) $$

and on the other side we have that:

$$ \nu l_1, l_2. \text{addG}(l_1 \langle (P) \rangle | l_2 \langle (Q) \rangle | S(l_1, l_2, l)) \hookrightarrow^* \nu l_1, l_2. \text{addG}(\text{Par} (P) (Q) l) $$
and since the identity is contained in the relation, we are still in the same relation. In the last case, since we only consider consistent processes, thanks to Lemma 24 there are no two **KillP** processes waiting on the same channels. Thus the context may not interact with the hole, and this case will never happen. □

**Lemma 70.** *Axiom Ax.A and its normal form are correct with respect to bfa barbed bisimilarity.*

**PROOF.** Let $S(l_1, l_2, l_3)$ denote either a process of the form $S(l_1, l_2, l_3) = (\text{KillP } l_1 \ l_2 \ l_3)$ or of the form $S(l_1, l_2, l_3) = (l_1(Z)|l_2(W) \triangleright l_3 \langle (h)\text{Par } ZW h \rangle | \text{Rew } l_3)$. Let $T_l$ denote either a process of the form $T_l = \text{Rew } l$ or of the form $T_l = (l(Z) \triangleright Zl)$. Let $A(\langle\!\langle P \rangle\!\rangle, l)$ denote either a process of the form $A(\langle\!\langle P \rangle\!\rangle, l) = l\langle\!\langle\langle P \rangle\!\rangle$ or of the form $A(\langle\!\langle P \rangle\!\rangle, l) = \langle\!\langle P \rangle\!\rangle l$. A bfa barbed bisimulation containing axiom Ax.A and its normal form is quite large. For simplicity we consider a relation which is closed only under challenges from the left term. Extending the relation and the proof by considering the symmetric cases is a tedious but easy work. The considered relation is $\mathcal{R}$ in Figure C.20.

Let us consider the barbs. The processes of the form $T_l$, $S(l_1, l_2, l_3)$, $A(\langle\!\langle P \rangle\!\rangle, l)$ have at most barbs on channels $l \in \mathcal{K}$. However, all channels $l \in \mathcal{K}$ are restricted, thus no barb on this channel can be present. Also, function `addG(-)` does not add any barb thanks to Lemma 68. So the only barbs are those shown by the context $\mathbb{C}[\cdot]$. These barbs are trivially matched.

Let us now consider reductions. All the reductions performed by the context are banally matched. Also, since all the relations are closed under the applications of auxiliary processes such as $T_l$ or $S(l_1, l_2, l_3)$ we will not mention them. Let us consider the different relations.

In $\mathcal{R}_1$ the only possibility is that the process $S(l_1, l_2, l') = (l_1(Z)|l_2(W) \triangleright l'\langle\!\langle (h)\text{Par } ZW h \rangle\!\rangle | \text{Rew } l')$ interacts with two messages on $l_1$ and $l_2$ in the context. We can assume they are of the form $l_1\langle\!\langle\langle P \rangle\!\rangle$ and $l_2\langle\!\langle\langle Q \rangle\!\rangle$, thus the reduction leads to $\mathcal{R}_2$.

From $\mathcal{R}_2$ two reductions are possible: the process can interact with the context by reading a message on $l_3$ of the form $l_3\langle\!\langle\langle R \rangle\!\rangle$, or the message on $l'$ may interact with $T_{l'}$. In the first case we obtain $l\langle\!\langle (h)\text{Par } \langle\!\langle P \mid Q \rangle\!\rangle \langle\!\langle R \rangle\!\rangle h \rangle | T_l$. On the right side we obtain $T_l | l\langle\!\langle (h)\text{Par } \langle\!\langle P \rangle\!\rangle \langle\!\langle Q \mid R \rangle\!\rangle h \rangle$. We can move into the context the process $T_l$, which occurs on both the sides, and also the message context, the application context and the abstraction context going to $\mathcal{R}_6$. In the second case we go directly to $\mathcal{R}_3$.
$$
\mathcal{R}_1 = \{ (\nu l'. S(l_1, l_2, l') | S(l', l_3, l)), (\nu l'. S(l_1, l', l) | S(l_2, l_3, l')) | l_1, l_2, l, l' \in \mathcal{K} \}
$$

$$
\mathcal{R}_2 = \{ (\nu l'. l' \langle (h)\mathbf{Par} (\|P\|) (\|Q\|) h \rangle | T_{l'} | S(l', l_3, l)), \\
(\nu l_1, l_2. \mathbf{addG} (A(\|P\|), l_1) | A(\|Q\|), l_2) | \nu l'. S(l_1, l', l) | S(l_2, l_3, l')) \}
$$

$$
\mathcal{R}_3 = \{ (\nu l'. ((h)\mathbf{Par} (\|P\|) (\|Q\|) h)l' | T_{l'} | S(l', l_3, l)), \\
(\nu l_1, l_2. \mathbf{addG} (A(\|P\|), l_1) | A(\|Q\|), l_2) | \nu l'. S(l_1, l', l) | S(l_2, l_3, l')) \}
$$

$$
\mathcal{R}_4 = \{ (\nu l'. (\mathbf{Par} (\|P\|) (\|Q\|) l') | T_{l'} | S(l', l_3, l)), \\
(\nu l_1, l_2. \mathbf{addG} (A(\|P\|), l_1) | A(\|Q\|), l_2) | \nu l'. S(l_1, l', l) | S(l_2, l_3, l')) \}
$$

$$
\mathcal{R}_5 = \{ (\nu l', h_1, h_2. (\|P\|)h_1 | (\|Q\|)h_2 | S(h_1, h_2, l') | T_{l'} | S(l', l_3, l)), \\
(\nu l_1, l_2. \mathbf{addG} (A(\|P\|), l_1) | A(\|Q\|), l_2) | \nu l'. S(l_1, l', l) | S(l_2, l_3, l')) \}
$$

$$
\mathcal{R}_6 = \{ (\mathbf{Par} (\|P\| | \|Q\|) (\|R\|) l), (\mathbf{Par} (\|P\| | \|Q\| | \|R\|) l) \}
$$

$$
\mathcal{R}_7 = \{ (\nu l_1, l_2. (\|P\| | \|Q\|)l_1 | (\|R\|)l_2 | S(l_1, l_2, l)), \\
(\nu l_1, l_2. (\|P\|)l_1 | (\|Q\| | \|R\|)l_2 | S(l_1, l_2, l)) \}
$$

$$
\mathcal{R}_8 = \{ (\nu l_1. (\|P\| | \|Q\|)l_1 | S(l_1, l_2, l)), \\
(\nu l_1, l_3, l_4. (\|P\|)l_1 | (\|Q\|)l_3 | S(l_1, l_4, l) | S(l_3, l_2, l_4)) \}
$$

$$
\mathcal{R}' = \cup \mathcal{R}_i
$$

$$
\mathcal{R} = \{ (\mathbb{C}[P_1, \dots, P_n], \mathbb{C}[Q_1, \dots, Q_n]) \mid (P_i, Q_i) \in \mathcal{R}' \wedge \\
\qquad \qquad \mathbb{C}[P_1, \dots, P_n], \mathbb{C}[Q_1, \dots, Q_n] \text{ well formed} \}
$$

<caption>Figure C.20: Relation for Ax.A</caption>

In $\mathcal{R}_3$ the only possible reduction is the application of the $\mathbf{Par}$, leading to $\mathcal{R}_4$.

Also in $\mathcal{R}_4$ the only possible reduction is an application, leading to $\mathcal{R}_5$.

In $\mathcal{R}_5$ both $(\|P\|)h_1$ and $(\|Q\|)h_2$ may reduce by means of an application.
Note that the right process reduces to the left one. In fact, since processes
are consistent there exist in the term two Rew processes, one on $l_1$ and one
on $l_2$. Hence we have that

$$
\nu l_1, l_2. \mathbf{addG}(l_1 \langle (\|P\|) \rangle | l_2 \langle (\|Q\|) \rangle | (\mathbf{Rew} \, l_1) | \\
(\mathbf{Rew} \, l_2) | \nu l'. S(l_1, l', l) | S(l_2, l_3, l')) \hookrightarrow^* \\
\nu l_1, l_2. \mathbf{addG}((\|P\|)l_1 | (\|Q\|)l_2 | \nu l'. S(l_1, l', l) | S(l_2, l_3, l'))
$$

and by α-converting $l_1, l_2$ into $h_1, h_2$ we obtain $\nu h_1, h_2$. $\mathbf{addG}((\|P\|)h_1 | (\|Q\|)h_2|$
$\nu l'. S(h_1, l', l) \mid S(h_2, l_3, l')$). This last process is structural congruent to $\nu h_1, h_2$. $\mathbf{addG}(\langle P \rangle h_1 \mid \langle Q \rangle h_2) \mid \nu l'. S(h_1, l', l) \mid S(h_2, l_3, l')$. Since each process $R$ is bfa barbed bisimilar to $\mathbf{addG}(R)$ (by Lemma 33), we conclude by transitivity, noting that by removing the $\mathbf{addG}$ function we get back to the relation $\mathcal{R}_1$.

From $\mathcal{R}_6$ we can only move to $\mathcal{R}_7$ by applications.

From $\mathcal{R}_7$ there are two possible reductions, either the application of $\langle P \mid Q \rangle l_1$ or the application of $\langle R \rangle l_2$. In the first case we get back to the relation $\mathcal{R}_1$ (by using $\alpha$-conversion). In the second case we can execute on the right the application $\langle Q \mid R \rangle l_2$, and obtain a process of the form $\langle R \rangle l_2$ (using $\alpha$-conversion) also on the right. We can thus move these processes to the context, going to the relation $\mathcal{R}_8$.

From $\mathcal{R}_8$, the left process can only perform the application on $\langle P \mid Q \rangle$, and we get back to the relation $\mathcal{R}_1$ (the right process matches this challenge by a 0 steps computation). $\square$

**Lemma 71.** Axiom AX.ADM and its normal form are correct with respect to bfa barbed bisimilarity.

PROOF. Let

$$ \mathcal{R}' = \{ (\nu c. (c \langle P \rangle \mid c(Z) \triangleright Z k), \langle P \rangle k) \} $$

$$ \mathcal{R} = \{ (\mathcal{C}[P_1, \dots, P_n], \mathcal{C}[Q_1, \dots, Q_n]) \mid (P_i, Q_i) \in \mathcal{R}' \} $$

We now show that the relation $\mathcal{R}$ is a bfa barbed bisimulation.

All the challenges from the right process are easily matched, since the left process reduces to the right one via an administrative reduction.

The only barbs of the left term are in the context, thus they are easily matched. Similarly, reductions of the context are easily matched. Reductions in the hole reduce to the term on the right, thus we are in the same relation by removing one hole. $\square$

**Proposition 1.** The relation $\mathcal{R} = \{(P, Q) \mid P \equiv_{Ex} Q\}$ where $P, Q$ are consistent $HO\pi^+$ processes is a bfa barbed bisimulation.

PROOF. By definition $P \equiv_{Ex} Q$ iff there are $P_1, \dots, P_n$ such that $P \equiv_{Ex} P_1 \equiv_{Ex} \dots \equiv_{Ex} P_n \equiv_{Ex} Q$ where each equivalence is obtained by applying just one axiom. The proof is by induction on $n$. The base case is banally
verified. In the inductive case we proceed by case analysis on the last applied axiom.

Let us consider axiom AX.C. By inductive hypothesis we have that $P \equiv_{Ex} P_n$ implies that $P \dot{\approx}_c P_n$ and that $P_n \equiv_{Ex} Q$ using the axiom AX.C. By Lemma 67 we know that $P_n \equiv_{Ex} Q$ implies $P_n \dot{\approx}_c Q$, and by transitivity we have that also $P \dot{\approx}_c Q$.

The other cases are similar, using Lemma 69 for axiom AX.P, Lemma 70 for axiom AX.A, Lemma 71 for axiom AX.ADM and Lemma 34 for axioms in $\equiv_\pi$. □

## Appendix C.4. Proofs of Section 4.6

**Lemma 35.** If $nf(|M|) \to P$ then $M \to M'$ with $P \hookrightarrow P'$ and $nf(P') \equiv nf(Q')$ and $Q' \in \text{addG}(|M'|)$.

**PROOF.** By structural induction on $M$. If $M$ is a simple process such as 0, a message or a trigger there is nothing to verify since $nf(|M|) \not\equiv$.

In the inductive case, if $M$ is of the form $\nu a. M_1$ then by definition of $nf(\cdot)$ and $(|\cdot|)$ we have that $nf(|M|) = \nu a. nf(|M_1|)$ and by applying the inductive hypothesis on $nf(|M_1|)$ we have that $nf(|M_1|) \to P$ implies $M_1 \to M'_1$ with $P \hookrightarrow P'$ and $nf(P') = nf(Q')$ with $Q' \in \text{addG}(|M'_1|)$. If $\nu a. (|M_1|) \to \nu a. P$ then also $|M_1| \to P$ and using inductive hypothesis we obtain $\nu a. M_1 \to \nu a. M'_1$ with $\nu a. P \hookrightarrow \nu a. P'$ and since $nf(P') = nf(Q')$ with $Q' \in \text{addG}(|M'_1|)$ we also have that $\nu a. nf(P') = \nu a. nf(Q')$ that is $nf(\nu a. P') = nf(Q'')$ with $Q'' \in \text{addG}(|\nu a. M'_1|)$, as desired. The case of parallel context $M = M_1 | M_2$ also follows by inductive hypothesis if the reduction is done inside either $M_1$ or $M_2$. If both $M_1$ and $M_2$ contribute to the reduction then we can assume that there are a message in $M_1$ and a trigger in $M_2$ able to communicate. For the sake of brevity, we consider just the case in which both message and trigger are tagged by a key. The other cases are similar. We can write $M = M'_1 | k_1 : a\langle R \rangle | k_2 : a(X) \triangleright Q | M'_2$. Hence, we have

$$ \begin{aligned} & (|M'_1| | k_1 : a\langle R \rangle | k_2 : a(X) \triangleright Q | M'_2|) = \\ & (|M'_1|) | (|a\langle R \rangle|)k_1 | (|a(X) \triangleright Q|)k_2 | (|M'_2|) \end{aligned} $$
Let $Y = (X c)c\langle(\mathcal{Q})\rangle$, then we have that

$$
\begin{align*}
\mathrm{nf}((\mathcal{M})) &= \mathrm{nf}((M'_1)) \mid a\langle(\mathcal{R}), k_1\rangle \mid \mathrm{nf}(\mathrm{KillM} a k_1) \mid \\
&\qquad \nu t. t\mid (a(X, l)\mid t\triangleright_f \nu k, c. (Y X x) \mid (c(Z)\triangleright Z k) \mid (\mathrm{Mem} Y a X l k k_2)) \mid \\
&\qquad \mathrm{nf}(\mathrm{KillT} Y t k_2 a) \mid \mathrm{nf}((M'_2)) \twoheadrightarrow \\
\mathrm{nf}((M'_1)) &= \mathrm{nf}(\mathrm{KillM} a k_1) \mid \nu k, c, t. (Y (\mathcal{R}) c) \mid (c(Z)\triangleright Z k) \mid \\
&\qquad (\mathrm{Mem} Y a X l k k_2) \mid \mathrm{nf}(\mathrm{KillT} Y t k_2 a) \mid \mathrm{nf}((M'_2)) \hookrightarrow\twoheadleftarrow \\
\mathrm{nf}((M'_1)) &= \mathrm{nf}(\mathrm{KillM} a k_1) \mid \nu k, c, t. (\mathcal{Q})\{^{(\mathcal{R})}/_X\}k \mid (\mathrm{Mem} Y a (\mathcal{R}) k_1 k k_2) \mid \\
&\qquad \mathrm{nf}(\mathrm{KillT} Y t k_2 a) \mid \mathrm{nf}((M'_2))
\end{align*}
$$

By using Lemma 21 (Substitution Lemma) the process above is equal to:

$$
\begin{align*}
\mathrm{nf}((M'_1)) \mid \mathrm{nf}(\mathrm{KillM} a k_1) \mid \nu k, c, t. (\mathcal{Q}\{^{\mathcal{R}}/_X\})k \mid (\mathrm{Mem} Y a (\mathcal{R}) k_1 k k_2) \mid \\
\mathrm{nf}(\mathrm{KillT} Y t k_2 a) \mid \mathrm{nf}((M'_2)) = P
\end{align*}
$$

We have that $M \twoheadrightarrow M'$ with $M' = M'_1 \mid \nu k. k : Q^{\{R\}/_X} \mid M'_2$ and we
can easily see that $P \twoheadleftarrow^* \mathrm{nf}((M'_1)) \mid \mathrm{nf}(\mathrm{KillM} a k_1) \mid \nu k, c, t. (Q^{\{R\}/_X})k$
$\mid \mathrm{nf}(\mathrm{Mem} Y a (R) k_1 k k_2) \mid \mathrm{nf}(\mathrm{KillT} Y t k_2 a) \mid \mathrm{nf}((M'_2)) \equiv \mathrm{nf}(Q'')$ with
$Q'' \in \mathrm{addG}((M'))$, as desired. $\square$