**Proof.** Let $t \in \mathcal{T}(\mathcal{F}, \mathcal{N})$ such that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [t_{\mathcal{E}_i} \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I'} \vdash t$. We prove the result by induction on $|I'|$.

Base case $|I'| = 0$: Trivial.

Inductive case $|I'| > 0$: Let $k \in I'$, we do a case analysis on $k$.

- Case $k \in \mathcal{D}$: By Definition 36, we know that $t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k) \in \mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi)$. Thus, $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [t_{\mathcal{E}_i} \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I'} \vdash t$ implies that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [t_{\mathcal{E}_i} \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I' \setminus \{k\}} \vdash t$. By our inductive hypothesis on $I' \setminus \{k\}$, we deduce that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash t$.

- Case $k \in \mathcal{N}$: In such a case, $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [\mathcal{E}_i \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I'} \vdash t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k)$ implies $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [\mathcal{E}_i \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I} \vdash t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k)$. By Lemma 37, we know that for all names $a \in \mathrm{img}(\delta) \cap \mathrm{names}(t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k))$, for all term $u, u \in \mathrm{dom}(\delta)$ and $u\delta = a$ implies $\Phi \vdash u$. Thus, if we denote $A = \{a \in \mathrm{img}(\delta) \mid u \in \mathrm{dom}(\delta), u\delta = a, \Phi \vdash u\}$, we deduce that $\mathrm{names}(t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k)) \cap (\mathrm{img}(\delta) \setminus A) = \emptyset$. Therefore, by Lemma 39, $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [\mathcal{E}_i \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I} \vdash t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k)$ implies that $\Phi \vdash t_{\mathcal{E}_k} \Sigma_k$. This is a contradiction with the fact that $\Phi$ is a well formed frame for $\mathcal{S}$, $\mathcal{D}$, $\mathcal{N}$ and $\mathcal{H}$. Hence this case is impossible.

- Case $k \in \mathcal{H}$ and $(\mathcal{E}_k, \mathcal{F}_k)$ allows authentic channels: This case is similar to the case $k \in \mathcal{D}$ since $t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k) \in \mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi)$ by Definition 36.

- Case $k \in \mathcal{H}$ and $(\mathcal{E}_k, \mathcal{F}_k)$ does not allow authentic channels: In such a case, $(\mathcal{E}_k, \mathcal{F}_k)$ satisfies Property 4 of Definition 7. Thus, $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [\mathcal{E}_i \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I'} \vdash t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k)$ implies that either $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [t_{\mathcal{E}_i} \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I' \setminus \{k\}} \vdash t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k)$ or there exists $x \in \mathcal{X}_{\mathcal{E}_k}$ such that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [t_{\mathcal{E}_i} \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I' \setminus \{k\}} \vdash x \mathrm{Ap}_\delta(\Sigma_k)$. In the latter, by inductive hypothesis on $I \setminus \{k\}$, we would deduce that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash x \mathrm{Ap}_\delta(\Sigma_k)$ which is in contradiction with the fact that $\Phi$ is a well formed frame for $\mathcal{S}$, $\mathcal{D}$, $\mathcal{N}$ and $\mathcal{H}$. Hence we deduce that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [t_{\mathcal{E}_i} \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I' \setminus \{k\}} \vdash t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k)$. By applying our inductive hypothesis on $I' \setminus \{k\}$, we deduce that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash t_{\mathcal{E}_k} \mathrm{Ap}_\delta(\Sigma_k)$. Thus, $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [t_{\mathcal{E}_i} \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I'} \vdash t$ implies that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [t_{\mathcal{E}_i} \mathrm{Ap}_\delta(\Sigma_i)]_{i \in I' \setminus \{k\}} \vdash t$. By our inductive hypothesis on $I' \setminus \{k\}$, we deduce that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash t$.

◀

**Lemma 41.** Let $\mathcal{S}$ be a set of $\mathrm{tag}_A$-encapsulations. Let $\Phi$ be a frame. Let $\mathcal{D}$, $\mathcal{N}$, $\mathcal{H}$ be three disjoint sets such that $\mathcal{D} \cup \mathcal{N} \cup \mathcal{H} \subseteq \{1, \dots, |\Phi|\}$. Let $\delta$ be a $\mathrm{tag}_A$-mapping of $\Phi$. Assume that $\Phi$ is a well formed frame for $\mathcal{S}$, $\mathcal{D}$, $\mathcal{N}$ and $\mathcal{H}$. Let us denote $I = \mathcal{D} \cup \mathcal{N} \cup \mathcal{H}$. The following two properties hold:

- for all terms $t$, $\mathrm{names}(t) \cap \mathrm{img}(\delta) = \emptyset$ and $\Phi \vdash t$ imply $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash \mathrm{Ap}_\delta(t)$

- for all $i \in I$, for all positions $p$ of $\mathcal{E}_i$, if $\Phi \vdash_P \mathcal{E}_i(t^i, s_1^i, \dots, s_{\ell_i}^i)|_p$ then the term $\mathcal{E}_i \mathrm{Ap}_\delta(\Sigma_i)|_p$ is deducible from the frame $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [\mathcal{E}_k \mathrm{Ap}_\delta(\Sigma_k)]_{k \in I}$.

**Proof.** Let a term $t$ such that $\mathrm{names}(t) \cap \mathrm{img}(\delta) = \emptyset$ and $\Phi \vdash_P t$. Consider that $P$ is minimal. We will prove both properties by induction on $\mathcal{M}(P)$. In particular, for the second property, we will assume that $t = \mathcal{E}_i \Sigma_i|_p$ for some $i \in I$ and position $p$ of $\mathcal{E}_i$. Let us denote $\Phi = [w_1; \dots; w_n]$.

Base case $\mathcal{M}(P) = (0, 1)$: In such a case, $P = 0$ and so $t \in \mathcal{N}_D$ or $t \in \mathcal{F}_{\mathrm{cst}}$. Therefore, we deduce that $\mathrm{Ap}_\delta(t) = t$ and so $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash \mathrm{Ap}_\delta(t)$. Regarding the second property, if there exists $i \in I$ and a position $p$ of $\mathcal{E}_i$ such that $\mathcal{E}_i \Sigma_i|_p = t$ then either $\mathcal{E}_i|_p \in \mathcal{X} \cup \mathcal{F}_{\mathrm{cst}}$. In such a case, we deduce that $\mathcal{E}_i \mathrm{Ap}_\delta(\Sigma_i)|_p = t$ and so the result holds since $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash t$.

Base case $\mathcal{M}(P) = (i, 1)$: In such a case, $P = i$ and so $t = w_i$. We do a case analysis whether $i \in I$ or not.

**Case $i \notin I$:** By Definition 36, we know that there exists $j \le i$ such that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash_j \mathrm{Ap}_\delta(t)$. Thus the first property directly holds. Regarding the second property, assume that there exists $j \in I$ and
a position $p$ of $\mathcal{E}_j$ such that $t = \mathcal{E}_j \Sigma_j |_p$. By Lemma 34, we know that $\mathcal{E}_j \Sigma_j = C[u_1, \dots, u_m]$ where $C[\_]$ is a context built on $\{(\, )\} \cup \mathcal{F}_{\text{cst}}$ and for all $k \in \{1, \dots, m\}$, $u_k$ is either a $\text{tag}_A$-term of $\text{dom}(\delta)$ or $u_k \in \text{vars}(\mathcal{E}_i) \Sigma_i$ or a term of the form $f(v)$ for some $f \in \mathcal{F}_{\text{key}}$ and $v \in \mathcal{X}_{\mathcal{E}_i} \Sigma_i \cup \mathcal{F}_{\text{cst}}$. We know that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(t)$. Hence, for all $k \in \{1, \dots, m\}$, if $u_k$ is not a $\text{tag}_A$-term of $\text{dom}(\delta)$, it implies that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(u_k)$. If $u_k$ is a $\text{tag}_A$-term of $\text{dom}(\delta)$, we know by Definition 28 that there exists $P'$ such that $M(P') < (i, 1)$ and $\Phi \vdash_{P'} u_k$. Moreover, there exists a position $p'$ of $\mathcal{E}_j$ such that $u_k = \mathcal{E}_j \Sigma_j |_{p'}$ hence we can apply our inductive hypothesis on it which means that by combining both results, the result holds.

**Case $i \in I$:** In such case, by Lemma 34, we know that $\mathcal{E}_i \Sigma_i = C[u_1, \dots, u_m]$ where $C[\_]$ is a context built on $\{(\, )\} \cup \mathcal{F}_{\text{cst}}$ and for all $k \in \{1, \dots, m\}$, $u_k$ is either a $\text{tag}_A$-term of $\text{dom}(\delta)$ or $u_i \in \text{vars}(\mathcal{E}_i) \Sigma_i$ or a term of the form $f(v)$ for some $f \in \mathcal{F}_{\text{key}}$ and $v \in \mathcal{X}_{\mathcal{E}_i} \Sigma_i \cup \mathcal{F}_{\text{cst}}$. Since $t = w_i$, it implies that for all $k \in \{1, \dots, m\}$, $\Phi \vdash u_k$. But by Definition 7 and in particular by Property 1 using the empty frame, we can deduce that for all $k \in \{1, \dots, m\}$, $u_k$ is either a $\text{tag}_A$-term of $\text{dom}(\delta)$ or $u_k \in \{\text{t}_{\mathcal{E}_i} \Sigma_i\} \cup \mathcal{T}(\mathcal{F}_{\text{key}} \cup \mathcal{F}_{\text{cst}}, \emptyset)$. Moreover, by Property 4 of Definition 7 and by Definition 38, we deduce that $u_k$ can only be either a $\text{tag}_A$-term of $\text{dom}(\delta)$ or $u_k \in \mathcal{T}(\mathcal{F}_{\text{key}} \cup \mathcal{F}_{\text{cst}}, \emptyset)$ when $i \in D$ or when $(\mathcal{E}_i, F_i)$ does not allow authentic channels.

Furthermore, if $(\mathcal{E}_i, F_i)$ is an encapsulation allowing authentic channels, we know that by Definition 36 that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(t) = C[\text{Ap}_{\delta}(u_1), \dots, \text{Ap}_{\delta}(u_m)]$ and $\text{Ap}_{\delta}(u_1), \dots, \text{Ap}_{\delta}(u_m) \in \mathcal{N}_D \cup \{\text{t}_{\mathcal{E}_i} \text{Ap}_{\delta}(\Sigma_i)\} \cup \mathcal{T}(\mathcal{F}_{\text{key}} \cup \mathcal{F}_{\text{cst}}, \emptyset)$, we deduce that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(t)$.

Let us focus now on the second property. Assume that there exists $j \in I$ and a position $p$ of $\mathcal{E}_j$ such that $t = \mathcal{E}_j \Sigma_j |_p$. If $\mathcal{E}_j |_p \in \mathcal{X}$ then we have that $\text{Ap}_{\delta}(t) = \mathcal{E}_j \text{Ap}_{\delta}(\Sigma_j) |_p$. But we already proved that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(t)$ hence the result directly holds. If $\mathcal{E}_j |_p \notin \mathcal{X}$ then in such a case, $\mathcal{E}_j \Sigma_j |_p = \mathcal{E}_i \Sigma_i$ implies that $\mathcal{E}_j |_p$ is unifiable with $\mathcal{E}_i$. Let us consider the $\mathcal{E}_j |_p$. We know by definition that $\mathcal{E}_j |_p = C'[r_1, \dots, r_l]$ where $C'$ is built on pair for all $k \in \{1, \dots, l\}$, $r_k \in \mathcal{T}(\mathcal{F}_{\text{key}}, \mathcal{X})$ or $r_k$ is a $\text{tag}_A$-term. In the former, since $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(t)$, we deduce that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(r_k \Sigma_j)$. In the latter, if $q$ is the position of $r_k$ in $\mathcal{E}_j$ and $q$ is also a position of $\mathcal{E}_i$ different from a variable, then by Property 2 of Definition 5, we deduce that $\mathcal{E}_j \text{Ap}_{\delta}(\Sigma_j) |_{p,q} = \mathcal{E}_i \text{Ap}_{\delta}(\Sigma_i) |_q$. Therefore, we have that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \cdot [\mathcal{E}_k \text{Ap}_{\delta}(\Sigma_k)]_{k \in I} \vdash r_k \text{Ap}_{\delta}(\Sigma_j)$. Otherwise by Definition 28, we know that there exists a proof $Q$ such that $M(Q) < (i, 1)$ and $\Phi \vdash_Q r_k \Sigma_j$. Thus we can apply our inductive hypothesis on it which allows us to deduce that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \cdot [\mathcal{E}_k \text{Ap}_{\delta}(\Sigma_k)]_{k \in I} \vdash r_k \text{Ap}_{\delta}(\Sigma_j)$. And so the result holds.

**Inductive case $M(P) = (i, j)$ with $j > 1$:** Let us do a case analysis on the last rule of the proof.

Assume first that the last rule of the proof is an $f$-composition rule. Therefore, there exists $t_1, \dots, t_m$ and $ir$ such that $t = f(t_1, \dots, t_m)$, $P = \text{ir}(P_1, \dots, P_m)$ and for all $i \in \{1, \dots, m\}$, $\Phi \vdash_{P_i} t_i$. If $t \in \text{dom}(\delta)$ then $\text{Ap}_{\delta}(t) \in \mathcal{N}_D$ and so we directly have $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(t)$. Else $t \notin \text{dom}(\delta)$ and since for all $i \in \{1, \dots, m\}$, $M(P_i) < M(P)$ then by inductive hypothesis on all the $t_i$, we deduce that for all $i \in \{1, \dots, m\}$, $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(t_i)$. Moreover, thanks to $t \notin \text{dom}(\delta)$, we know that $\text{Ap}_{\delta}(t) = f(\text{Ap}_{\delta}(t_1), \dots, \text{Ap}_{\delta}(t_m))$. Hence we deduce that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(t)$. Consider now that there exists $r \in I$ and a position $p$ of $\mathcal{E}_r$ such that $t = \mathcal{E}_r \Sigma_r$. If $\mathcal{E}_r |_p \in \mathcal{X}$ then $\text{Ap}_{\delta}(t) = \mathcal{E}_r \text{Ap}_{\delta}(\Sigma_r) |_p$. Therefore, we directly have that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_{\delta}(t)$ as previously shown and so the result holds. If $\mathcal{E}_r |_p \notin \mathcal{X}$ then we can apply our inductive hypothesis on all $t_k$ with position $p \cdot k$ and so the result also holds.

Assume now that the last rule is an $f$-decomposition. Therefore, there exists $x \in \mathcal{X}$, $u_1, \dots, u_m, v_1, \dots, v_k \in \mathcal{T}(\mathcal{F}_{\text{key}}, \mathcal{X})$, a substitution $\sigma$ and some proofs $P', P_1, \dots, P_k$ such that:

- $t = x\sigma$

- $\text{vars}(v_1, \dots, v_k) \subseteq \{u_1, \dots, u_m\}$; and

- $P = \text{ir}(P', P_1, \dots, P_k)$; and
Φ ⊢<sub>P'</sub> f(x, u<sub>1</sub>, ..., u<sub>m</sub>)σ and for all r ∈ {1, ..., k}, Φ ⊢<sub>P<sub>r</sub></sub> v<sub>r</sub>σ.

Moreover, by minimality of P, we know that there exists i' ≤ i such that P is a successive sequence of applications of decomposition rules on w<sub>i'</sub>. We do a case analysis on f(x, u<sub>1</sub>, ..., u<sub>m</sub>)σ and i'.

Case f(x, u₁, ..., uₙ)σ ∈ dom(δ) and i' /∈ I: Since P is a successive sequence of applications of decomposition rules on wᵢ', we deduce that there exists a position p such that |wᵢ'|ₚ = f(x, u₁, ..., uₙ)σ and (i', 1) ≤ M(P') < (i, j). But by Definition 28, we know that either [w₁; ... ; wᵢ'-₁] ⊢ wᵢ'|ₚ or else p = p' · a · p'' such that [w₁; ... ; wᵢ'-₁] ⊢ wᵢ'|p'-a. Moreover, P being a successive sequence of applications of decomposition rules on wᵢ' implies that there exists P'' ∈ st(P) such that (i', 1) ≤ M(P'') and Φ ⊢<sub>P''</sub> wᵢ'|p'-a. Since we already know that [w₁; ... ; wᵢ'-₁] ⊢ wᵢ'|p'-a then there is a contradiction with the fact that P is minimal.

Case f(x, u₁, ..., uₙ)σ ∈ dom(δ), i' ∈ I and f(x, u₁, ..., uₙ)σ ∈ st(Σᵢ'): Similar to the previous case, meaning that we obtain a contradiction with the fact that P is minimal.

Case *t* ∈ dom(δ) and either *i*' /∈ I or *t* ∈ st(Σᵢ'): Similar to the previous case.

For the next cases, we need to look at different cases depending on the property we prove.
Moreover, we have to switch from one property to the other depending on the case.

**Property 1** *Case f(x, u₁, ..., uₙ)σ ∉ dom(δ): In such a case, we have Ap<sub>δ</sub>(f(xσ, u₁σ, ..., uₙσ)) = f(Ap<sub>δ</sub>(xσ), Ap<sub>δ</sub>(u₁σ), ..., Ap<sub>δ</sub>(uₙσ)). By our inductive hypothesis, we deduce Tr<sup>H,δ</sup><sub>D,N</sub>(Φ) ⊢ f(Ap<sub>δ</sub>(xσ), Ap<sub>δ</sub>(u₁σ), ..., Ap<sub>δ</sub>(uₙσ)) and for all i ∈ {1, ..., k}, Tr<sup>H,δ</sup><sub>D,N</sub>(Φ) ⊢ Ap<sub>δ</sub>(vᵢσ). But u₁σ, ..., uₙσ, v₁σ, ..., vₙσ ∈ T<sub>F<sub>key</sub></sub>(F<sub>X</sub>), hence we deduce that for all i, Ap<sub>δ</sub>(uᵢσ) = uᵢAp<sub>σ</sub>(σ) and Ap<sub>δ</sub>(vᵢσ) = vᵢAp<sub>σ</sub>(σ). This allows us to deduce that Tr<sup>H,δ</sup><sub>D,N</sub>(Φ) ⊢ Ap<sub>δ</sub>(xσ).*

**Property 2** *Case for all k ∈ I and all positions p of E<sub>k</sub>, E<sub>k</sub>Σ<sub>k</sub>|<sub>p</sub> ≠ f(x, u<sub>1</sub>, ..., u<sub>n</sub>)σ : In such a case, we deduce that i' /∈ I. However, we know that there exists k ∈ I and a position p of E<sub>k</sub> such that E<sub>k</sub>Σ<sub>k</sub>|<sub>p</sub> = t. Therefore, by Lemma 34, we deduce that t = C[u'<sub>1</sub>, ..., u'<sub>n'</sub>] such that for all r ∈ {1, ..., n'}, either u'<sub>r</sub> is a tag<sub>A</sub>-term or u'<sub>r</sub> ∈ vars(E<sub>k</sub>)Σ<sub>k</sub> or u'<sub>r</sub> is of the form f(v) for some f ∈ F<sub>key</sub> and some v ∈ X<sub>E<sub>k</sub></sub>Σ<sub>k</sub> ∪ F<sub>cst</sub>. From the previous case, we deduce that Tr<sup>H,δ</sup><sub>D,N</sub>(Φ) ⊢ Ap<sub>δ</sub>(t) and so for all r ∈ {1, ..., n'}, Tr<sup>H,δ</sup><sub>D,N</sub>(Φ) ⊢ Ap<sub>δ</sub>(u'<sub>r</sub>). But by Lemma 34, we know that E<sub>k</sub>Ap<sub>δ</sub>(Σ<sub>k</sub>)|<sub>p</sub> = C[v'<sub>1</sub>, ..., v'<sub>n'</sub>] such that for all r ∈ r ∈ {1, ..., n'}, if u'<sub>r</sub> is not a tag<sub>A</sub>-term then v'<sub>r</sub> = Ap<sub>δ</sub>(u'<sub>r</sub>). Moreover, if u'<sub>r</sub> is a tag<sub>A</sub>-term then by Definition 28, we know [w<sub>1</sub>; ... ; w<sub>i'-1</sub>] ⊢ u'<sub>r</sub>. We also know that there exists a position p' of E<sub>k</sub> such that E<sub>k</sub>Σ<sub>k</sub>|<sub>p'</sub> = u'<sub>r</sub>. Hence we can apply our inductive hypothesis on u'<sub>r</sub> and obtain that Tr<sup>H,δ</sup><sub>D,N</sub>(Φ) · [E<sub>k</sub>Ap<sub>δ</sub>(Σ<sub>k</sub>)]<sub>k∈I</sub> ⊢ E<sub>k</sub>Ap<sub>δ</sub>(Σ<sub>k</sub>)|<sub>p'</sub>. By combining the two cases (u'<sub>r</sub> being a tag<sub>A</sub>-term or not), we deduce that the term E<sub>k</sub>Ap<sub>δ</sub>(Σ<sub>k</sub>)|<sub>p</sub> is deducible from Tr<sup>H,δ</sup><sub>D,N</sub>(Φ) · [E<sub>k</sub>Ap<sub>δ</sub>(Σ<sub>k</sub>)]<sub>k∈I</sub>.*

**Property 2** *Case there exists k ∈ I and a position p of E<sub>k</sub> such that E<sub>k</sub>Σ<sub>k</sub>|<sub>p</sub> = f(x, u<sub>1</sub>, ..., u<sub>n</sub>)σ: We can apply our inductive hypothesis on f(x, u<sub>1</sub>, ..., u<sub>n</sub>)σ which allows us to deduce that E<sub>k</sub>Ap<sub>δ</sub>(Σ<sub>k</sub>)|<sub>p</sub> is deducible from Tr<sup>H,δ</sup><sub>D,N</sub>(Φ) · [E<sub>k</sub>Ap<sub>δ</sub>(Σ<sub>k</sub>)]<sub>k∈I</sub>. We show that we can apply the same rule ir. Let us look at the terms v<sub>1</sub>, ..., v<sub>m'</sub> and construct a new substitution σ'. For all r ∈ {1, ..., m'}, by Definition 5*

■ either v_r = g(x) for some x ∈ X, g ∈ F_key and for all r' ∈ {1, ..., n}, if x ∈ vars(u_{r'}) then u_{r'}σ ∈ vars(E_k)Σ_k ∪ F_cst. Therefore, for all r' ∈ {1, ..., n}, if x ∈ vars(u_{r'}) then E_kAp_δ(Σ_k)|_{p·(r'+1)} = Ap_δ(u_{r'})σ. Therefore, we define xσ' = Ap_δ(xσ). Note that in such a case, Ap_δ(v_rσ) = v_rσ'. Moreover, since Φ ⊢_{P_r} v_rσ then by our inductive hypothesis, we have that Tr_{I_D, I_H}^{δ, Φ}(⊢)Ap_δ(v_rσ) and so Tr_{D,N}^{H,δ}(Φ) ⊢ v_rσ'.

■ or v_r ∈ X and for all r' ∈ {1, ..., n}, if v_r ∈ vars(u_{r'}) then u_{r'}σ = v_rσ. In such a case, we define v_rσ' = E_k Ap_δ(Σ_k)|_{p·(r'+1)}. Note that since Φ ⊢_{P_r} v_rσ, we can apply our inductive hypothesis on v_rσ and the position p·(r' + 1) which indicates that the term v_rσ' is deducible from the frame Tr_{D,N}^{H,δ}(Φ) · [E_k Ap_δ(Σ_k)]_{k∈I}.
or $v_r \in X$ and there exists $r' \in \{1, \dots, n\}$ such that $v_r \in \text{vars}(u_{r'})$ and $u_{r'}\sigma = g(v)$ with $g \in \mathcal{F}_{\text{key}}$ and $v \in \mathcal{X}_{\mathcal{E}_k} \Sigma_k \cup \mathcal{F}_{\text{cst}}$. In such a case, we define $v_r\sigma' = \text{Ap}_{\delta}(v)$. Similarly to the first case, we deduce $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash v_r\sigma'$.

This allows us to conclude that $f(x, u_1, \dots, u_m)\sigma' = \mathcal{E}_k \text{Ap}_\delta(\Sigma_k)|_p$ and $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \cdot [\mathcal{E}_k \text{Ap}_\delta(\Sigma_k)]_{k \in I} \vdash v_r\sigma'$ for all $r \in \{1, \dots, m'\}$. Therefore, we conclude that $\mathcal{E}_k \text{Ap}_\delta(\Sigma_k)|_{p-1}$ is deducible from $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \cdot [\mathcal{E}_k \text{Ap}_\delta(\Sigma_k)]_{k \in I}$.

**Property 1** *Case f(x, u₁, ..., uₙ)σ ∈ dom(δ):* Considering all the different cases we went through, it implies that $i' \in I$ and there exists a position $p$ of $\mathcal{E}_{i'}$ such that $\mathcal{E}_{i'}\Sigma_{i'}|_p = t$. Therefore, by Lemma 34, we know that $t = C[d_1, \dots, d_k]$ where $C$ is a context built on $\{\langle\rangle\} \cup \mathcal{F}_{\text{cst}}$ and for all $r \in \{1, \dots, k\}$, $d_r$ is either a **tag**$_A$-term or $d_r \in \text{vars}(\mathcal{E}_{i'})\Sigma_{i'}$ or $d_r = g(v)$ with $g \in \mathcal{F}_{\text{key}}$ or $v \in \mathcal{X}_{\mathcal{E}_{i'}}\Sigma_{i'} \cup \mathcal{F}_{\text{cst}}$. By applying Property 2 on $t$, we deduce that for all $r \in \{1, \dots, k\}$, if $d_r$ is not a **tag**$_A$-term then $\text{Ap}_\delta(d_r)$ is deducible from $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \cdot [\mathcal{E}_k \text{Ap}_\delta(\Sigma_k)]_{k \in I}$. Let us consider the different cases:*

if $d_r \in \mathcal{T}(\mathcal{F}_{\text{key}} \cup \mathcal{F}_{\text{cst}}, \mathcal{X}_{\mathcal{E}_{i'}}\Sigma_{i'})$ then by Property 1 of Definition 7 and Lemma 40, we deduce that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_\delta(d_r)$.

if $d_r = \text{t}_{\mathcal{E}_{i'}}\Sigma_{i'}$ and $i' \in \mathbb{N}$ then this case is in fact impossible since $\Phi \vdash t$ implies $\Phi \vdash t^{i'}$ which is a contradiction with Definition 38.

if $d_r = \text{t}_{\mathcal{E}_{i'}}\Sigma_{i'}$ and $i' \in \mathbb{D}$ or $(\mathcal{E}_{i'}, \mathcal{F}_{i'})$ is an encapsulation allowing authentic channels, then by Definition 36, we know that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_\delta(d_r)$

if $d_r = \text{t}_{\mathcal{E}_{i'}}\Sigma_{i'}$ and $i' \in \mathbb{H}$ and $(\mathcal{E}_{i'}, \mathcal{F}_{i'})$ is an not encapsulation allowing authentic channels, then by Property 4 of Definition 7 and Lemma 40, either $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_\delta(d_r)$ or there exists $x \in \mathcal{X}_{\mathcal{E}_{i'}}$ such that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash x\text{Ap}_\delta(\Sigma_{i'})$. But the latter case contradicts our initial hypothesis given in Definition 38. Therefore, we deduce that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_\delta(d_r)$.

Lastly, for all $r \in \{1, \dots, k\}$, if $d_r$ is a **tag**$_A$-term then $\text{Ap}_\delta(d_r) \in \mathcal{N}_D$ and so we trivially have that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash d_r$. This allows us to conclude that $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash C[\text{Ap}_\delta(d_1), \dots, \text{Ap}_\delta(d_k)]$ and so $\text{Tr}_{\text{D,N}}^{\text{H},\delta}(\Phi) \vdash \text{Ap}_\delta(t)$. ◀

**Lemma 42.** *Let $S$ be a set of **tag**$_A$-encapsulations. Let $\Phi$ be a frame. Let $\mathbb{D}, \mathbb{N}, \mathbb{H}$ be three disjoint sets such that $\mathbb{D} \cup \mathbb{N} \cup \mathbb{H} \subseteq \{1, \dots, |\Phi|\}$. Let $\delta$ be a **tag**$_A$-mapping of $\Phi$. Assume that $\Phi$ is a well formed frame for $S$, $\mathbb{D}$, $\mathbb{N}$ and $\mathbb{H}$. Let us denote $I = \mathbb{D} \cup \mathbb{N} \cup \mathbb{H}$.*

For all $(\mathcal{E}, \mathcal{F}) \in S$, for all substitution $\Sigma$, for all position $p$ of $\mathcal{E}$, if $\Phi \vdash \mathcal{E}\Sigma|_p$ then there exists a context $C[\dots, \dots]$ and some terms $u_1, \dots, u_n$ such that $\mathcal{E}\Sigma|_p = C[u_1, \dots, u_n]$ and for all $i \in \{1, \dots, n\}$, $\Phi \vdash u_i$ and if $q$ is position of $u_i$ in $\mathcal{E}\Sigma|_p$ then $p \cdot q$ is a position of $\mathcal{E}$ and

either $\mathcal{E}|_{p,q} \in \mathcal{X}$;

or $\mathcal{E}|_{p,q} = f(x)$ with $f \in \mathcal{F}_{\text{key}}$ and $x \in \mathcal{X}_{\mathcal{E}} \cup \mathcal{F}_{\text{cst}}$;

or $\mathcal{E}|_{p,q}$ is a **tag**$_A$-tagged term and there exists $k \in I$ and a position $q'$ of $\mathcal{E}_k$ such that $\mathcal{E}_k|_{q'} \notin \mathcal{X}$ and $u_i = \mathcal{E}_k \Sigma_k|_{q'}$.

**Proof.** Let us denote $\Phi = [w_1; \dots; w_{|\Phi|}]$. Consider the minimal proof $P$ such that $\Phi \vdash_P \mathcal{E}\Sigma|_p$. We prove the result by induction on $\mathcal{M}(P)$.

*Base case* $P = (0, 1)$: In such a case, $\mathcal{E}\Sigma|_p \in \mathcal{N}_D \cup \mathcal{F}_{\text{cst}}$. Thus it necessarily implies that $\mathcal{E}|_p \in \mathcal{X}$. Hence the result holds with $C = \_.$

*Inductive case* $P = (i, j)$ and the last rule of $P$ is a decomposition: In such a case, we deduce that there exists $k \le i$ such that $\mathcal{E}\Sigma|_p \in \text{st}(w_k)$.

By Definition 5, we know that there exists a context $C[\dots, \dots]$ built on $\{\langle\rangle\} \cup \mathcal{F}_{\text{cst}}$ and some terms $v_1, \dots, v_n$ such that $\mathcal{E}|_p = C[v_1, \dots, v_n]$ and for all $i \in \{1, \dots, n\}$, either $v_i$ is a **tag**$_A$-term or
$v_i \in \mathcal{X}$ or $v_i = f(x)$ for some $f \in \mathcal{F}_{\text{key}}$ and $x \in \mathcal{X}_{\mathcal{E}} \cup \mathcal{F}_{\text{cst}}$. Therefore, for all $i \in \{1, \dots, n\}$, thanks to the fact that $C[\_, \dots, \_]$ is built on $\{(\, \cdot\, )\} \cup \mathcal{F}_{\text{cst}}$, we deduce that $\Phi \vdash v_i \Sigma$. If $v_i$ is a tag$_A$-tagged term then we do a small case analysis on $k$.

Case $k \in I$ and there exists a position $q'$ of $\mathcal{E}_k$ such that $\mathcal{E}_k|'q' \notin \mathcal{X}$ and $v_i = \mathcal{E}_k \Sigma_k|q'$: Trivial

Case $k \notin I$ or $\mathcal{E}_k|_{q'} \in \mathcal{X}$: In such a case, $v_i \Sigma$ being a tag$_A$-term implies thanks to Definition 28, we deduce that either there exist $k' \in I$ and a position $q''$ of $\mathcal{E}_{k'}$ different from a variable such that $v_i \Sigma = \mathcal{E}_{k'}|_{q''} \Sigma_k$ or $[w_1; \dots; w_{k-1}] \vdash v_i \Sigma$. In the former, the result directly holds. In the latter, we can apply our inductive hypothesis on $v_i \Sigma$ since $k-1 < i$ which allows us to deduce the existence of a context $C_i$ and terms $u_1^i, \dots, u_{n_i}^i$ satisfying the correct properties. In such a case, we can directly conclude with the context $C[C_1, \dots, C_n]$ where $C_k = \_\_$ in the case where $u_k$ is not a tag$_A$-tagged term else the context $C_k$ obtained through the inductive hypothesis.

Inductive case $P = (i, j)$ with the last rule of $P$ being a composition: In such a case, $\mathcal{E}\Sigma|_p = f(t_1, \dots, t_n)$ where for all $k \in \{1, \dots, n\}, \Phi \vdash t_k$. If $\mathcal{E}|_p \in \mathcal{X}$ the result directly holds. Else for all $k \in \{1, \dots, n\}, p \cdot k$ is a position $\mathcal{E}$. Therefore, we can apply our inductive hypothesis on $t_k$ and so we deduce the existence of a context $C_k$ and terms $u_1^k, \dots, u_{m_k}^k$ satisfying the correct properties. In such a case, we can directly conclude with the context $f[C_1, \dots, C_n]$ and the terms $u_1^1, \dots, u_{n_1}^1, \dots, u_{m_n}^n$. ◀

**Lemma 43.** Let $S$ be a set of tag$_A$-encapsulations. Let $\Phi$ be a frame. Let $D, N, H$ be three disjoint sets such that $I = D \cup N \cup H \subseteq \{1, \dots, |\Phi|\}$. Let $(\mathcal{E}, F) \in S$. Let $\Sigma$ be a ground substitution. Let $\delta$ be a tag$_A$-mapping of $\Phi \cdot [\mathcal{E}\Sigma]$. Assume that $\Phi$ is a well formed frame for $S, D, N$ and $H$.

If $\Phi \vdash \mathcal{E}\Sigma$ and $(\mathcal{E}, F)$ allows confidential channels then

- either there exists $k \in H$ such that $\mathcal{E}_k \sim \mathcal{E}$ and $\mathcal{E}_k \Sigma_k = \mathcal{E}\Sigma$;

- or $\text{Tr}_{D \cup N, \emptyset}^{H, \delta}(\Phi) \vdash \mathcal{E}_k \text{Ap}_\delta(\Sigma)$.

If $\Phi \vdash \mathcal{E}\Sigma$; and for all $i \in H$, either $X_{\mathcal{E}_i} \Sigma_i = X_{\mathcal{E}} \Sigma$ or $X_{\mathcal{E}_i} \Sigma_i \cap X_{\mathcal{E}} \Sigma = \emptyset$; and $(\mathcal{E}, F)$ does not allow confidential channels then

- if there exists $k \in H$ such that $X_{\mathcal{E}_k} \text{Ap}_\delta(\Sigma_k) = X_{\mathcal{E}} \text{Ap}_\delta(\Sigma)$ then there exist $k \in H$ such that $\mathcal{E}_k \sim \mathcal{E}$ and $\mathcal{E}_k \Sigma_k = \mathcal{E}\Sigma$;

- if for all $k \in H$, $X_{\mathcal{E}_k} \text{Ap}_\delta(\Sigma_k) \cap X_{\mathcal{E}} \text{Ap}_\delta(\Sigma) = \emptyset$ then $\text{Tr}_{D \cup N, \emptyset}^{H, \delta}(\Phi) \vdash \mathcal{E}_k \text{Ap}_\delta(\Sigma)$.

**Proof.** W.l.o.g. consider that the variable of $(\mathcal{E}, F)$ are disjoint from the variables of $(\mathcal{E}_k, F_k)$ for all $k \in I$. By Lemma 42, we know that there exists a context $C[\_, \dots, \_]$ and some terms $u_1, \dots, u_n$ such that $\mathcal{E}\Sigma = C[u_1, \dots, u_n]$ and for all $i \in \{1, \dots, n\}, \Phi \vdash u_i$ if $p$ is position of $u_i$ in $\mathcal{E}\Sigma$ then $p$ is a position of $\mathcal{E}$ and

- either $\mathcal{E}|_p \in \mathcal{X}$;

- or $\mathcal{E}|_p = f(x)$ with $f \in \mathcal{F}_{\text{key}}$ and $x \in \mathcal{X}_{\mathcal{E}} \cup \mathcal{F}_{\text{cst}}$;

- or $\mathcal{E}|_p$ is a tag$_A$-tagged term and there exists $k \in I$ and a position $q$ of $\mathcal{E}_k$ such that $\mathcal{E}_k|_q \notin \mathcal{X}$ and $u_i = \mathcal{E}_k \Sigma_k|_q$.

Let us first prove that $\text{Tr}_{D,N}^{H,\delta}(\Phi) \cdot [\mathcal{E}_k \text{Ap}_\delta(\Sigma_k)]_{k \in I} \vdash \mathcal{E} \text{Ap}_\delta(\Sigma)$. Let $i \in \{1, \dots, n\}$. Let us denote by $p$ is position of $u_i$ in $\mathcal{E}\Sigma$. If $\mathcal{E}|_p \in \mathcal{X}$ then by Lemma 41, $\Phi \vdash u_i$ implies that $\text{Tr}_{D,N}^{H,\delta}(\Phi) \vdash \text{Ap}_\delta(\mathcal{E}|_p \Sigma) = \mathcal{E}|_p \text{Ap}_\delta(\Sigma)$. Similarly, if $\mathcal{E}|_p = f(x)$ with $f \in \mathcal{F}_{\text{key}}$ and $x \in \mathcal{X}_{\mathcal{E}} \cup \mathcal{F}_{\text{cst}}$ then we deduce that $\text{Tr}_{D,N}^{H,\delta}(\Phi) \vdash \mathcal{E}|_p \text{Ap}_\delta(\Sigma)$.

Otherwise $\mathcal{E}|_p$ is a tag$_A$-tagged term and there exist $k \in I$ and a position $q$ of $\mathcal{E}_k$ such that $\mathcal{E}_k|_q \notin \mathcal{X}$ and $u_i = \mathcal{E}_k \Sigma_k|_q$. But $\mathcal{E}|_p \Sigma = \mathcal{E}_k|_q \Sigma_k$ implies that $\mathcal{E}|_p$ and $\mathcal{E}_k|_q$ are unifiable. Therefore, by Property 2 of Definition 7, we deduce that $\text{img}(\text{mgu}(\mathcal{E}_k|_q, \mathcal{E}|_p)) \subseteq \mathcal{X}$. Therefore, $\mathcal{E}_k|_q \Sigma_k = \mathcal{E}|_p \Sigma$ implies $\mathcal{E}_k|_q \text{Ap}_\delta(\Sigma_k) = \mathcal{E}|_p \text{Ap}_\delta(\Sigma)$. But we know that $\Phi \vdash \mathcal{E}|_p \Sigma$ and so $\Phi \vdash \mathcal{E}_k|_q \Sigma_k$. Hence by
Lemma 41, we deduce that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [\varepsilon_k \mathrm{Ap}_\delta(\Sigma_k)]_{k \in I} \vdash \varepsilon_k |_q \mathrm{Ap}_\delta(\Sigma_k)$. This allows us to deduce that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \cdot [\varepsilon_k \mathrm{Ap}_\delta(\Sigma_k)]_{k \in I} \vdash \varepsilon \mathrm{Ap}_\delta(\Sigma)$.

By applying Property 5 of Definition 7 and Lemma 40, we deduce that if $(\mathcal{E}, \mathcal{F})$ allows confidential channels then:

- either there exists $j \in I$ such that $\mathcal{E}_j \sim \mathcal{E}$ and $\mathcal{E}_j \mathrm{Ap}_\delta(\Sigma_j) = \mathcal{E} \mathrm{Ap}_\delta(\Sigma)$; If $j \in \mathcal{H}$ then the result holds. Else $j \in \mathcal{N} \cup \mathcal{D}$. But in both cases, $t_{\mathcal{E}} \mathrm{Ap}_\delta(\Sigma_j) \in \mathrm{Tr}_{\mathrm{D} \cup \mathcal{N}, \emptyset}^{\mathrm{H},\delta}(\Phi)$. Hence we deduce that $\mathrm{Tr}_{\mathrm{D} \cup \mathcal{N}, \emptyset}^{\mathrm{H},\delta}(\Phi) \vdash t_{\mathcal{E}} \mathrm{Ap}_\delta(\Sigma)$.

- or $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash t_{\mathcal{E}} \mathrm{Ap}_\delta(\Sigma)$ which implies $\mathrm{Tr}_{\mathrm{D} \cup \mathcal{N}, \emptyset}^{\mathrm{H},\delta}(\Phi) \vdash t_{\mathcal{E}} \mathrm{Ap}_\delta(\Sigma)$

This allows us to conclude when $(\mathcal{E}, \mathcal{F})$ allows confidential channels.

By applying Property 6 of Definition 7 and Lemma 40, we deduce that if $(\mathcal{E}, \mathcal{F})$ does not allow confidential channels then:

- either there exists $j \in I$ such that $\mathcal{E}_j \sim \mathcal{E}$ and $\mathcal{E}_j \mathrm{Ap}_\delta(\Sigma_j) = \mathcal{E} \mathrm{Ap}_\delta(\Sigma)$. Hence the result holds.

- or there exists $x \in X_\mathcal{E}$ such that $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash x \mathrm{Ap}_\delta(\Sigma)$ and $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash t_{\mathcal{E}} \mathrm{Ap}_\delta(\Sigma)$. Hence the result holds

- or there exists $j \in I$, $y \in X_\mathcal{E} \cap X_{\mathcal{E}_j}$, $x \in X_\mathcal{E}$ such that $y\Sigma = y\Sigma_j$, $t_{\mathcal{E}} \mathrm{Ap}_\delta(\Sigma) = t_{\mathcal{E}_j} \mathrm{Ap}_\delta(\Sigma_j)$ and $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash x \mathrm{Ap}_\delta(\Sigma)$. But by hypothesis, we know that for all $i \in \mathcal{H}$, either $X_{\mathcal{E}_i} \Sigma_i = X_\mathcal{E} \Sigma$ or $X_{\mathcal{E}_i} \Sigma_i \cap X_\mathcal{E} \Sigma = \emptyset$. In such a case, by Definition 38 and since $\mathrm{Tr}_{\mathrm{D},\mathrm{N}}^{\mathrm{H},\delta}(\Phi) \vdash x \mathrm{Ap}_\delta(\Sigma)$, we deduce that $j \notin \mathcal{H}$. Therefore, by definition of $\mathrm{Tr}_{\mathrm{D} \cup \mathcal{N}, \emptyset}^{\mathrm{H},\delta}(\Phi)$, we deduce that $\mathrm{Tr}_{\mathrm{D} \cup \mathcal{N}, \emptyset}^{\mathrm{H},\delta}(\Phi) \vdash t_{\mathcal{E}} \mathrm{Ap}_\delta(\Sigma)$.

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

## C.4 From the composed protocol to the abstract protocol (New)

The events added to a process $P$ when created an annotation $\tilde{P}$ under a mapping $\rho$ (Definition 9) contain sufficient information to express when $\tilde{P}$ is a secure channel establishment protocol (Definition 16). However, the channels in the events of $\tilde{P}$ are public since they are not restricted by any new operator. For the proof of Theorem 17, we need to link these public channels with the abstract channels actually restricted in the context of $Q$. Therefore, we consider below new events $\tilde{e}v_1, \dots, \tilde{e}v_n, \dots$ of arity 5 in which the last elements will be used to “store” the abstract channels actually restricted in the context of $Q$. Let us denote $\tilde{e}v = \{\tilde{e}v_1, \dots, \tilde{e}v_n, \dots\}$. Considering these new events, we also define a notion of process *secure* similar to Definition 16.

► **Definition 44.** Let $P$ be a closed process. We say that $P$ is secure when for all $(P, \emptyset, \emptyset, \stackrel{)}{\Rightarrow} e_1 \cdots e_m(P', \Phi', \mu', \theta')$, for all $i \in \{1, \dots, m\}$, if $e_i = \mathrm{ev}(c, ta, (s_1, \dots, s_\ell), (u_1, \dots, u_q), d)$ such that $\mathrm{ev} \in \tilde{e}v$ and all agents in $ta$ are honest then for all $k \in \{1, \dots, \ell\}$, $\Phi' \nvdash s_k$ and for all $k \in \{1, \dots, q\}$, $\Phi' \vdash u_k$. Moreover, for all $j \in \{1, \dots, m\}$, if $e_j = \mathrm{ev}'(c', ta', (s'_1, \dots, s'_{\ell'}), (u'_1, \dots, u'_{q'}), d')$ for some channel $c'$, $d'$, some tuple $ta'$ of agents and some tuples $(s'_1, \dots, s'_{\ell'})$ and $(u'_1, \dots, u'_{q'})$ of terms then

- either $ta \neq ta'$ or $c \neq c'$ or $\mathrm{ev} = \mathrm{ev}'$ implies $\forall k \in \{1, \dots, \ell\}, \forall k' \in \{1, \dots, \ell'\}, s_k \neq s_{k'}$

- or one of the two following properties is satisfied :

- $(s_1, \dots, s_\ell) = (s'_1, \dots, s'_{\ell'})$ and $(u_1, \dots, u_q) = (u'_1, \dots, u'_{q'})$.

- $\forall k \in \{1, \dots, \ell\}, \forall k' \in \{1, \dots, \ell'\}, s_k \neq s_{k'}$.

Note that the definition is almost identical of Definition 16. The only difference is that we consider events from $\tilde{e}v$ instead of the events $\{\mathrm{ev}_1, \dots, \mathrm{ev}_n, \dots\}$.

We also define a property on the trace linking the two channels of the events from $\tilde{e}v$.
**Definition 45.** Let $P$ be a closed process. We say that an execution $(P, \emptyset, \emptyset, \emptyset) \overset{e_1, \dots, e_m}{\implies} (P', \Phi', \mu', \theta')$ is well formed if for all $i, j \in \{1, \dots, m\}$, if $e_i = ev(c, ta, ts, tp, d)$, $e_j = ev'(c, ta, ts, tp, d')$, $ev, ev' \in \tilde{E}v$, the agents of $ta$ are honest, $ev \neq ev'$ and $d \neq d'$ for some $c, ta, ts, tp, d, d', ev, ev'$ then

- either there exists $i' < i$ such that $e_{i'} = ev(c, ta, ts, tp, d'')$ for some $d'' \neq d$;

- or there exists $j' < j$ such that $e_{j'} = ev'(c, tq, ts, tp, d'')$ for some $d'' \neq d'$.

**Lemma 46.** Let $S$ be a set of channels. Let $P = C[R_1, \dots, R_n]$ be a closed process such that:

- for all $i \in \{1, \dots, n\}$, if $c \in S$ appears in $R_i$ then it can only be inside an unique event $\tilde{e}v_i(d, ta, ts, tp, c)$ for some $d, ta, ts, tp$ where $A \in ta$, $A$ is the agent of $R_i$ and $new_{ta}$ $c$ is in $C$.

- there exists a bijective mapping $\gamma$ from $S$ to fresh channels for all $i \in \{1, \dots, n\}$, for all $\tilde{e}v_i(d, ta, ts, tp, c)$ in $R_i$, $c\gamma = d$.

For all $(P, \emptyset, \emptyset, \emptyset) \stackrel{tr}{\implies} (Q, \Phi, \mu, \theta)$, there exists $Q', \theta'$, $tr'$ such that $(P, \emptyset, \emptyset, \emptyset) \stackrel{tr'}{\implies} (Q', \Phi, \mu, \theta')$ and this configuration is well formed.

**Proof.** Consider $(P, \emptyset, \emptyset, \emptyset) \overset{e_1, \dots, e_n}{\implies} (Q, \Phi, \mu, \theta)$. Since the channels of $S$ only appear in the events of $P$, the choices of channels during the execution of the rule NEW-C do not affect the execution of the trace other than the value of the channels in $e_1 \dots e_n$. Let us create a partition $\psi_{j=1}^m I_j$ of $\{1, \dots, n\}$ such that for all $j \in \{1, \dots, m\}$, for all $k, k' \in I_j$, the fifth argument of $e_k'$ and $e_{k'}'$ have been instantiated by the same execution of the rule NEW-C, for all $k \in I_j$ for all $k \in I_{j'}$ with $j \neq j'$, the fifth argument of $e_k'$ and $e_{k'}'$ have been instantiated by two different execution of the rule NEW-C. This allows us to build recursively $\theta'$ on the $m$, i.e. on the order of execution of the rule NEW-C. Typically, when two events $(ev_i(d, ta, ts, tp, c)$ and $ev_j(d', ta', ts', tp', c')$) of the same partition, meaning $i \neq j$ satisfy $ta = ta'$ and $d = d'$ then we select the same channels if $(ts, tp) = (ts', tp')$. $\quad \blacksquare$

Let us denote by $T_t$ the set of tuples of terms.

**Definition 47.** Let $S$ be a set of tag$_A$-encapsulations. We say that $P$ is an initial process when for all instances $out_A(c, u)$ (resp. $in_A(c, u)$) in $P$,

- either $u$ is a fully tag$_B$-tagged term;

- or $c = c_{pub}$ and $u = \mathcal{E}\Sigma$ for some fully tag$_B$-tagged substitution $\Sigma$ and some encapsulation $(\mathcal{E}, \mathcal{F}) \in S$.

Let us denote by $channels_{O/I}(P)$ the set of channels appearing in an output or input of $P$. Note that $channels(P) \setminus channels_{O/I}(P)$ is not necessary empty since a channel $c$ can be declared by new $c$ in $P$ but never used in an output or input.

**Definition 48.** Let $S$ be a set of tag$_A$-encapsulations. Let $\Phi$ be an executed ground frame for $S$ and some $I$. Let $P$ be an initial process. Let $\alpha$ be a mapping from $S \times T_t$ to $Ch$. We say that $\alpha$ is a mapping of channels for $P$ (resp. $\Phi$) when $img(\alpha) \cap channels_{O/I}(P) = \emptyset$ and for all $(\mathcal{E}, \mathcal{F}) \in S$, for all substitution $\Sigma$, if $\mathcal{E}\Sigma$ is in $P$ (resp. for all $i \in I$, if $\mathcal{E}\Sigma = \mathcal{E}_i\Sigma_i$) then there exists $c \in Ch$ such that $((\mathcal{E}, \mathcal{F}), \chi_{\mathcal{E}\Sigma})\alpha = c$ and if $(\mathcal{E}, \mathcal{F})$ allows authentic (resp. confidential, secure) channels then $c \in Ch_a \cup Ch_p$ (resp. $Ch_c \cup Ch_p, Ch_s \cup Ch_p$).

We define the transformed process of $P$ w.r.t. $\alpha$, denoted $\text{Tr}_{\alpha}(P)$, as the process $P$ where we replace:

- all instances $out_{A_i}(c_{pub}, \mathcal{E}\Sigma)$ by $out_{A_i}(c, t_{\mathcal{E}}\Sigma)$

- all instances $in_{A_i}(c_{pub}, \mathcal{E}\Sigma)$ by $in_{A_i}(c, t_{\mathcal{E}}\Sigma)$

when $((\mathcal{E}, \mathcal{F}), \chi_{\mathcal{E}\Sigma})\alpha = c$ for some $\Sigma$ and $\mathcal{F}$.
**► Definition 49.** Let $\mathcal{S}$ be a set of tag$_A$-encapsulations. Let $\Phi$ be an ground executed frame for some set $I$. Let $P$ be an initial process. Let $\alpha$ (resp. $\beta$) be a mapping of channels for $P$ (resp. $\Phi$). Let $\sigma$ a substitution of closed terms. Let $tr$ be a sequence of closed events. We say that $P, \Phi, \alpha, \beta, tr$ and $\sigma$ have conforming events if

1. for all $i \in I$, there exist $c, d, ta, k$ such that $((\mathcal{E}_i, F_i), \chi_{\mathcal{E}_i \Sigma_i})\beta = d, \tilde{\mathcal{E}}v_k(c, ta, \chi_{\mathcal{E}_i \Sigma_i}, F_i \Sigma_i, d) \in tr$ and $d \notin Ch_p$ is equivalent to all agents in $ta$ are honest; and

2. for all roles $R = r_1...r_n$ of $P$, for all $i \in \{1, ..., n\}$, if $r_i = \text{out}_A(c_{pub}, \mathcal{E}\Sigma)$ (resp. $r_i = \text{in}_A(c_{pub}, \mathcal{E}\Sigma)$) for some agent $A$, some substitution $\Sigma$ and some encapsulation $(\mathcal{E}, F) \in \mathcal{S}$ then there exists $c, d, ta$ such that $((\mathcal{E}, F), \chi_{\mathcal{E}\Sigma})\alpha = d$ and:

- either there exist $j < i$ and $ev \in \tilde{\mathcal{E}}v$ such that $r_j = \text{event}_A(ev(c, ta, \chi_{\mathcal{E}\Sigma}, F\Sigma), d)$;

- or $ev(c, ta, \chi_{\mathcal{E}\Sigma}\sigma, F\Sigma\sigma, d) \in tr$ and $d \notin Ch_p$ is equivalent to all agents in $ta$ are honest.

When $tr$ and $\Phi$ are the empty sequence and $\sigma$ is the identity, we say that $P, \alpha$ have conforming events.

**► Definition 50.** Let $\mathcal{S}$ be a set of tag$_A$-encapsulations. Let $\Phi$ be a well formed frame for $\mathcal{S}$ and some $D, N$ and $H$. Let $\beta$ be a mapping of channels for $\Phi$. We define $\mu(\Phi, \beta)$ as a mapping from channels to sets of terms such that:

$$ \text{dom}(\mu(\Phi, \beta)) = \{c \notin Ch_p \mid i \in H \wedge ((\mathcal{E}_i, F_i), \chi_{\mathcal{E}_i \Sigma_i})\beta = c\}; \text{ and} $$

$$ \forall c \in \text{dom}(\mu(\Phi, \beta)), c\mu(\Phi, \beta) = \{\text{Ap}_{\delta}(t_{\mathcal{E}_i} \Sigma_i) \mid i \in H \wedge ((\mathcal{E}_i, F_i), \chi_{\mathcal{E}_i \Sigma_i})\beta = c\}. $$

**► Lemma 51.** Let $\mathcal{S}$ be a set of tag$_A$-tagged encapsulations allowing authentic, confidential and secure channels. Let $P_0$ be a closed initial process. Let $\alpha_0$ be a mapping of channels for $P_0$. Assume that $P_0, \alpha_0$ have conforming events. Assume that $(\text{Tr}_\alpha(P_0), \emptyset, \emptyset, \emptyset)$ is secure. For all well-formed execution $(P_0, \emptyset, \emptyset, \emptyset) \stackrel{tr}{\Rightarrow}_\sigma (P, \Phi, \mu, \theta)$, there exists an initial process $Q$, a mapping of channels $\alpha$ (resp. $\beta$) for $Q$ (resp. $\Phi$), and $\eta, \delta, D, N$ and $H$ such that:

$$ \text{Q}\sigma = P; \text{ and} $$

$$ \eta\sigma = \mu \text{ and } \eta \text{ only contains fully tag}_B\text{-terms; and} $$

$$ Q, \Phi, \alpha, \beta, tr \text{ and } \sigma \text{ have conforming events; and} $$

$$ \Phi \text{ is a well formed frame for } \mathcal{S}, D, N \text{ and } H; \text{ and} $$

$$ \sigma \text{ is an executed substitution for } \Phi; \text{ and} $$

$$ \delta \text{ is a tag}_A\text{-mapping of } \Phi \text{ and } \sigma; \text{ and} $$

$$ (\text{Tr}_\alpha(P_0), \emptyset, \emptyset, \emptyset) \stackrel{\text{Ap}_\delta(\text{tr})}{\Longrightarrow} \text{Ap}_\delta(\sigma) (\text{Tr}_\alpha(Q) \text{Ap}_\delta(\sigma), \text{Tr}_{D \cup N, \emptyset}^{H, \delta}(\Phi), \eta \text{Ap}_\delta(\sigma) \circ \mu(\Phi, \beta), \theta) $$

**Proof.** We do the proof by induction on the size of the trace $(P_0, \emptyset, id) \stackrel{tr}{\Rightarrow}_\sigma (P, \Phi, \mu)$:

*Base case:* The result trivially holds with $Q = P_0$, $\alpha = \alpha_0$, $\beta = id$, $\delta = id$, $D = N = H = \emptyset$.

*Inductive step:* In such case, we assume that there exist two processes $P_1$ and $P_2$, two substitutions $\sigma_1, \sigma_2$, two frames $\Phi_1, \Phi_2$ and two mapping $\mu_1, \mu_2$ such that $(P_0, \emptyset, id) \stackrel{tr_1}{\Rightarrow}_{\sigma_1} (P_1, \Phi_1, \mu_1) \stackrel{e}{\rightarrow}_{\sigma_2} (P_2, \Phi_2, \mu_2)$. By applying our inductive hypothesis on $(P_0, \emptyset, id) \stackrel{tr_1}{\Rightarrow}_{\sigma_1} (P_1, \Phi_1, \mu_1)$, we deduce that there exist an initial process $Q_1$, a mapping of channels $\alpha_1$ (resp. $\beta_1$) for $Q_1$ (resp. $\Phi_1$), and $\eta_1, \delta_1, D_1, N_1, H_1$ such that:

$$ Q_1\sigma_1 = P_1; \text{ and} $$

$$ \eta_1\sigma_1 = \mu_1 \text{ and } \eta_1 \text{ only contains fully tag}_B\text{-terms; and} $$

$$ Q_1, \Phi_1, \alpha_1, \beta_1, tr_1 \text{ and } \sigma_1 \text{ have conforming events; and} $$

$$ \Phi_1 \text{ is a well formed frame for } \mathcal{S}, D_1, N_1 \text{ and } H_1; \text{ and} $$
■ $\sigma_1$ is an executed substitution for $\Phi_1$; and

■ $\delta_1$ is a tag_A-mapping of $\Phi_1$ and $\sigma_1$; and

■ $(\mathrm{Tr}_\alpha(P_0), \emptyset, id) \overset{\mathrm{Ap}_{\delta_1}(tr_1)}{\implies} \sigma'_1 (\mathrm{Tr}_{\alpha_1}(Q_1)\sigma'_1, \mathrm{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1), \eta_1 \sigma'_1 \circ \mu(\Phi_1, \beta_1))$ with $\sigma'_1 = \mathrm{Ap}_{\delta_1}(\sigma_1)$.

We show the existence of an initial process $Q_2$, a mapping of channels $\alpha_2$ (resp. $\beta_2$) for $Q_2$ (resp. $\Phi_2$), and $\eta_2$, $\delta_2$, $D_2$, $N_2$ and $H_2$ satisfying the result with $(P_2, \Phi_2, \mu_2)$ by case analysis on the rule applying in $(P_1, \Phi_1, \mu_1) \stackrel{e}{\to} \sigma_2 (P_2, \Phi_2, \mu_2)$.

**Rule Out:** In such a case, $Q_1 = Q \mid \mathrm{out}_A(c, u).R_A$, $P_2 = Q\sigma_1 \mid R_A\sigma_1$, $\sigma_2 = \sigma_1$, $\Phi_2 = \Phi_1 \cdot [u\sigma_1]$ if $c \in Ch_p \cup Ch_a$ else $\Phi_2 = \Phi_1$, and $\mu_2 = \mathrm{rect}(c, u\sigma_1, \mu_1)$ if $c \notin Ch_p$ else $\mu_2 = \mu_1$. Let us first define $Q_2 = Q \mid R_A$. This allows us to deduce that $Q_2\sigma_2 = P_2$. Let us also define $tr_2 = tr_1$ and $\alpha_2 = \alpha_1$. Therefore, we deduce that $\mathrm{Tr}_{\alpha_2}(Q_2) = \mathrm{Tr}_{\alpha_1}(Q_1) \mid \mathrm{Tr}_{\alpha_1}(R_A)$.

By Definition 47, we know that either $u$ is a fully tag_B-tagged term and $c \notin \mathrm{img}(\alpha_1) \cup \mathrm{img}(\beta_1)$ or $u = \mathcal{E}\Sigma$ and $c = c_{pub} \in Ch_p$ where $\Sigma$ is a fully tag_B-tagged substitution and $(\mathcal{E}, \mathrm{F})$ is an encapsulation. We do a case analysis:

Case $u$ is a tag_B-tagged term and $c \notin \mathrm{img}(\alpha_1) \cup \mathrm{img}(\beta_1)$: In such a case, $\mathrm{Tr}_{\alpha_1}(Q_1) = \mathrm{Tr}_{\alpha_1}(Q) \mid \mathrm{out}_A(c, u).\mathrm{Tr}_{\alpha_1}(R_A)$. Since $u$ is a tag_B-tagged term, we deduce that $\mathrm{Ap}_{\delta_1}(u\sigma_1) = u\mathrm{Ap}_{\delta_1}(\sigma_1)$ thus if $\mu_2 = \mathrm{rect}(c, u\sigma_1, \mu_1)$ (when $c \notin Ch_p$) then we can define $\eta_2 = \mathrm{rect}(c, u, \eta_1)$ and obtain that $\mu_2 = \eta_2\sigma_1 = \eta_2\sigma_2$ and $\eta_2\mathrm{Ap}_{\delta_2}(\sigma_2) = \mathrm{rect}(c, u\mathrm{Ap}_{\delta_1}(\sigma_1), \eta_1\mathrm{Ap}_{\delta_1}(\sigma_1))$.

Consider $N_2$ and $D_2$ such that $N_2 \cup D_2 = N_1 \cup D_1$ and such that for all $i \in N_2$ (resp. $D_2$), $\Phi_2 \not\in t^i$ (resp. $\Phi_2 \vdash t^i$). Consider $H_2 = H_1$, $\delta_2 = \delta_1$ and $\beta_2 = \beta_1$. In such a case, if $\Phi_2 = \Phi_1 \cdot [u\sigma_1]$ (when $c \in Ch_p \cup Ch_a$) then we deduce that $\mathrm{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) = \mathrm{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1) \cdot [\mathrm{Ap}_{\delta_1}(u\sigma_1)] = \mathrm{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1) \cdot [u\mathrm{Ap}_{\delta_1}(\sigma_1)]$. This allows us to deduce that $\mu(\Phi_2, \beta_2) = \mu(\Phi_1, \beta_1)$ and so:

$$ (\mathrm{Tr}_{\alpha_1}(Q_1)\mathrm{Ap}_{\delta_1}(\sigma_1), \mathrm{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1), \eta_1\mathrm{Ap}_{\delta_1}(\sigma_1) \circ \mu(\Phi_1, \beta_1)) \to $$

$$ (\mathrm{Tr}_{\alpha_2}(Q_2)\mathrm{Ap}_{\delta_2}(\sigma_2), \mathrm{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2), \eta_2\mathrm{Ap}_{\delta_2}(\sigma_2) \circ \mu(\Phi_2, \beta_2)) $$

Moreover, since $\sigma_2 = \sigma_1$, $tr_1 = tr_2$, $\alpha_2 = \alpha_2$, $\beta_2 = \beta_1$, all outputs and inputs of $P_2$ are in $P_1$ and $N_2 \cup D_2 \cup H_2 = N_1 \cup D_1 \cup H_1$, we deduce that $P_2, \Phi_2, \alpha_2, \beta_2, tr_2$ and $\sigma_2$ have conforming events. Furthermore, we know that $\sigma_1$ is an executed substitution for $\Phi_1$ and $u$ is a tag_B-tagged term. Hence for all subterms of $u\sigma_1$ that are tag_A-tagged term, they are subterm of $\mathrm{img}(\sigma_1)$. Hence following Definitions 31 and 38, we deduce that $\Phi_2$ is a well formed frame for $S$, $D_2$, $N_2$ and $H_2$. We also directly have that $\sigma_2$ is an executed substitution for $\Phi_2$ since $\Phi_1$ is included in $\Phi_2$. Lastly, since $\delta_1$ is a tag_A-mapping of $\Phi_1$ and $\sigma_1$ then we know that all tag_A-tagged terms in $\mathrm{img}(\sigma_1)$ are in $\mathrm{dom}(\delta_1)$, thus so do the one in $u\sigma_1$. Hence we deduce that $\delta_2$ is a tag_A-mapping of $\Phi_2$ and $\sigma_2$. This allows us to conclude.

Case $u = \mathcal{E}\Sigma$ and $c = c_{pub} \in Ch_p$: In this case, by Definition 49, we deduce that there exists a channel $d$ such that $((\mathcal{E}, \mathrm{F}), X_{\mathcal{E}\Sigma}\sigma_1) = d$. Let us show that if $((\mathcal{E}, \mathrm{F}), X_{\mathcal{E}\Sigma}\sigma_1)\beta_1 = d'$ for some channel $d'$ and either $d \notin Ch_p$ or $d' \notin Ch_p$ then $d = d'$. By definition 48, we know that there exists $i \in H_1 \cup N_1 \cup D_1$ such that $(\mathcal{E}_i, F_i) = (\mathcal{E}, \mathrm{F}), X_{\mathcal{E}_i}\Sigma_i\sigma_1 = X_{\mathcal{E}\Sigma}\sigma_1$ and $((\mathcal{E}_i, F_i), X_{\mathcal{E}_i}\Sigma_i)\beta_1 = d'$. Therefore, by Definition 49, we know that there exists $ev' \in \tilde{\mathbb{E}}v, c'_0$ and $ta'$ such that $ev'(c'_0, ta', X_{\mathcal{E}_i}\Sigma_i\sigma_1, F_i\Sigma_i\sigma_1, d') \in tr_1$ and all agents in $ta'$ are honest is equivalent to $d' \notin Ch_p$. Moreover, with the same definition, we also know that there exists $ev \in \tilde{\mathbb{E}}v, c_0$ and $ta$ such that $ev(c_0, ta, X_{\mathcal{E}\Sigma}\sigma_1, F\Sigma\sigma_1, d) \in tr_1$ and all agents in $ta$ are honest is equivalent to $d \notin Ch_p$. But we know that $(\mathrm{Tr}_\alpha(P_0), \emptyset, id)$ is secure. Hence by our inductive hypothesis on $(\mathrm{Tr}_\alpha(P_0), \emptyset, id)$, if either $d \notin Ch_p$ or $d' \notin Ch_p$ then we deduce that all the agents in either $ta$ or $ta'$ are honest and thus since $X_{\mathcal{E}_i}\Sigma_i\sigma_1 = X_{\mathcal{E}\Sigma}\sigma_1$ we obtain by Definition 44 that $t_a = t'_a, c_0 = c'_0$ and $ev \neq ev'$. But we also know that the execution $(P_0, \emptyset, id) \stackrel{tr}{\Rightarrow} \sigma (P, \Phi, \mu)$ is well formed. Hence by Definition 45, we deduce that $d = d'$. So $X_{\mathcal{E}_i}\Sigma_i\sigma_1 = X_{\mathcal{E}\Sigma}\sigma_1$ implies that $d = d'$.
Therefore, let us define $\beta_2 = \beta_1 \circ ((\mathcal{E}, \mathcal{F}), \chi_{\mathcal{E}}\Sigma\sigma_1) \to d)$ if $d \notin Ch_p$ or if $((\mathcal{E}, \mathcal{F}), \chi_{\mathcal{E}}\Sigma\sigma_1) \notin \text{dom}(\beta_1)$. Otherwise, we define $\beta_2 = \beta_1$.

Moreover, $u = \mathcal{E}\Sigma$ and $c \in Ch_p$ imply $\text{Tr}_{\alpha_1}(Q_1) = \text{Tr}_{\alpha_1}(Q) | \text{out}_A(d, t_{\mathcal{E}}\Sigma).\text{Tr}_{\alpha_1}(R_A)$, $\Phi_2 = \Phi_1 \cdot [u\sigma_1]$ and $\mu_2 = \mu_1$. Therefore, by defining $\eta_2 = \eta_1$, we have that:

$$ (\text{Tr}_{\alpha_1}(Q_1)\text{Ap}_{\delta_1}(\sigma_1), \text{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1), \eta_1\text{Ap}_{\delta_1}(\sigma_1) \circ \mu(\Phi_1, \beta_1)) \\ \to \\ (\text{Tr}_{\alpha_2}(Q_2)\text{Ap}_{\delta_2}(\sigma_2), \Phi'_2, \mu'_2) $$

where $\Phi'_2 = \text{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1) \cdot [t_{\mathcal{E}}\Sigma\text{Ap}_{\delta_1}(\sigma_1)]$ if $d \in Ch_p \cup Ch_a$, else $\Phi'_2 = \text{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1)$; and where $\mu'_2 = \text{rect}(d, t_{\mathcal{E}}\Sigma\text{Ap}_{\delta_1}(\sigma_1), \eta_2\text{Ap}_{\delta_2}(\sigma_2) \circ \mu(\Phi_2, \beta_1))$ if $d \notin Ch_p$ else $\mu'_2 = \eta_2\text{Ap}_{\delta_2}(\sigma_2) \circ \mu(\Phi_1, \alpha_1)$. Note that $t_{\mathcal{E}}\Sigma$ is a tag$_B$-tagged term hence $t_{\mathcal{E}}\Sigma\text{Ap}_{\delta_1}(\sigma_1) = \text{Ap}_{\delta_1}(t_{\mathcal{E}}\Sigma\sigma_1)$. Moreover, we also directly have that $\sigma_2$ is an executed substitution for $\Phi_2$ since $\sigma_1$ is an executed substitution for $\Phi_1$ and $\Phi_1$ is included in $\Phi_2$. Furthermore, we know that $\Sigma$ is a fully tag$_B$-tagged substitution. Hence for all subterms of $\Sigma\sigma_1$ that are tag$_A$-tagged term, they are subterm of $\text{img}(\sigma_1)$. Hence following Definitions 31 and 28, we deduce that $\Phi_2$ is an executed frame for $S$ and $D_1 \cup N_1 \cup H_1 \cup \{|\Phi_1| + 1\}$. Note that by construction of $\beta_2$ and by Definition 49, we also deduce that $P_2, \Phi_2, \alpha_2, \beta_2, tr_2$ and $\sigma_2$ have conforming events. We do a small case analysis on $d$:

- Case $d \in Ch_p$: In such a case, we define $H_2 = H_1$ and $D_2, N_2$ such that $D_2 \cup N_2 = D_1 \cup N_1 \cup \{|\Phi_1|+1\}$ and for all $i \in N_2$ (resp. $D_2$), $\Phi_2 \nmid t_{\varepsilon_i}\Sigma_i$ (resp. $\Phi_2 \vdash t_{\varepsilon_i}\Sigma_i$). Since $\delta_1 = \delta_2$ and $\sigma_1 = \sigma_2$ then by Definition 36, we deduce that $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) = \text{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1) \cdot [\text{Ap}_{\delta_2}(t_{\mathcal{E}}\Sigma\sigma_2)] = \Phi'_2$. Moreover, since $d \in Ch_p$ then by Definition 50, we deduce that $\mu(\Phi_2, \beta_2) = \mu(\Phi_1, \beta_1)$. Hence we can conclude that $\mu'_2 = \eta_2\text{Ap}_{\delta_2}(\sigma_2) \circ \mu(\Phi_2, \beta_2)$. Lastly, since $H_2 = H_1$ and we already proved that $\Phi_2$ is an executed frame for $S$ and $D_2 \cup N_2 \cup H_2$, we deduce that $\Phi_2$ is a well formed frame for $S$, $D_2, N_2$ and $H_2$. This allows us to conclude.

- Case $d \notin Ch_p$: In such a case, we define $H_2 = H_1 \cup \{|\Phi_1| + 1\}$ and $D_2, N_2$ such that $D_2 \cup N_2 = D_1 \cup N_1$ and for all $i \in N_2$ (resp. $D_2$), $\Phi_2 \nmid t_{\varepsilon_i}\Sigma_i$ (resp. $\Phi_2 \vdash t_{\varepsilon_i}\Sigma_i$). By Definition 47, we know that $(\mathcal{E}, \mathcal{F})$ allows authentic (resp. confidential, secure) channels implies $d \in Ch_a$ (resp. $Ch_c, Ch_s$). Therefore, since $\delta_1 = \delta_2$ and $\sigma_1 = \sigma_2$ then by Definition 36, we deduce that $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) = \Phi'_2$. Let us now focus on $\mu'_2$. We know that $\mu'_2 = \text{rect}(d, t\text{Ap}_{\delta_1}(\sigma_1), \eta_2\text{Ap}_{\delta_2}(\sigma_2) \circ \mu(\Phi_1, \alpha_1))$. But if $d \notin \text{dom}(\mu_1)$ then we need to look at $\mu(\Phi_1, \alpha_1)$. Since we defined $\beta_2 = \beta_1 \circ ((\mathcal{E}, \mathcal{F}), \chi_{\mathcal{E}}\Sigma\sigma_1) \to d)$, $\Phi_2 = \Phi \cdot [\mathcal{E}\Sigma\sigma]$ and $H_2 = H_1 \cup \{|\Phi_1| + 1\}$, we deduce by definition that $\mu(\Phi_2, \beta_2) = \text{rect}(d, t_{\mathcal{E}}\Sigma\text{Ap}_{\delta_1}(\sigma), \mu(\Phi_1, \beta_1))$. Since $\mu_1 = \mu_2$, $\delta_2 = \delta_1$ and $\text{dom}(\mu_1) \cap \text{img}(\beta_2) = \emptyset$, we deduce that $\text{rect}(d, t_{\mathcal{E}}\Sigma\text{Ap}_{\delta_1}(\sigma_1), \eta_2\text{Ap}_{\delta_2}(\sigma_2) \circ \mu(\Phi_1, \beta_1)) = \eta_2\text{Ap}_{\delta_2}(\sigma_2) \circ \mu(\Phi_2, \beta_2) = \mu'_2$. It remains to prove that $\Phi_2$ is a well formed frame for $S$, $D_2$, $N_2$ and $H_2$. We already know that $\sigma_1$ is an executed substitution for $\Phi_1$ and $\Sigma$ does not contain tag$_A$-tagged term. Therefore, since $\Phi_2 = \Phi_1 \cdot [\mathcal{E}\Sigma\sigma_1]$ then we deduce that $\Phi_2$ is an executed frame for $D_2 \cup N_2 \cup H_2$. Let us prove that for all $v \in \chi_{\mathcal{E}}\Sigma\sigma_1$, $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) \nmid \text{Ap}_{\delta_2}(v)$ and $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) \vdash \text{FAp}_{\delta_2}(\Sigma\sigma_1)$. We know $(\text{Tr}_{\alpha}(P_0), \emptyset, id) \overset{\text{Ap}_{\delta_2}(tr_2)}{\implies} \text{Ap}_{\delta_2}(\sigma_2)$ ($\text{Tr}_{\alpha_2}(Q_2)\text{Ap}_{\delta_2}(\sigma_2), \text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2), \eta_2\text{Ap}_{\delta_2}(\sigma_2) \circ \mu(\Phi_2, \beta_2)$), $(\text{Tr}_{\alpha}(P_0), \emptyset, id)$ is secure and there exists ta such that $\text{ev}(d, ta, \chi_{\mathcal{E}}\Sigma\sigma_1, \mathcal{F}\Sigma\sigma_1) \in tr_1$ with all agents in ta are honest. Hence, applying Definition 44 allows us to conclude.

**Rule IN:** In such a case, $Q_1 = Q \mid \text{in}_A(c, v).R_A$, $\Phi_2 = \Phi_1$, $\mu_2 = \mu_1$ and there exists $\sigma$ such that $\text{dom}(\sigma) = \text{vars}(v\sigma_1)$ and either $v\sigma_1\sigma \in c\mu_1$ or else $c \in Ch_p \cup Ch_c$ and $\Phi_1 \vdash v\sigma_1\sigma$. Moreover, we have $P_2 = Q\sigma_1 \mid R_A\sigma_1\sigma$ and $\sigma_2 = \sigma_1\sigma$. Let us first define $Q_2 = Q \mid R_A$. In such a case, we deduce $Q_2\sigma_2 = P_2$.

Let us now define $\delta_2 = \delta_1 \cup \delta'$ where $\delta'$ is an injective mapping from tag$_A$-terms that are in $\sigma$ but not in $\sigma_1$ or $\Phi_1$ to fresh names of $N_D$. In such a case, we directly have that $\delta_2$ is a tag$_A$-mapping
of $\Phi_2$ and $\sigma_2$. Moreover, let us define $tr_2 = tr_1$, $D_2 = D_1$, $N_2 = N_1$, $H_2 = H_1$, $\alpha_2 = \alpha_1$, $\beta_2 = \beta_1$, $\eta_2 = \eta_1$. We directly have that $\Phi_2$ is a well formed frame for $\mathcal{S}$, $D_2$, $N_2$ and $H_2$. Since $\sigma_2 = \sigma_1\sigma$, then following Definition 49, we deduce that $Q_2$, $\Phi_2$, $\alpha_2$, $\beta_2$, $tr_2$ and $\sigma_2$ have conforming events. Moreover we also derive that $\eta_2\sigma_2 = \eta_1\sigma_1\sigma = \mu_1\sigma = \mu_1 = \mu_2$.

We now show that $\sigma_2$ is an executed substitution for $\Phi_2$. We know that either $v\sigma_2 \in c\eta_1\sigma_1$ or else $\Phi_1 \vdash v\sigma_2$. In the former case, since $\eta_1$ only contains fully $\mathbf{tag}_B$-terms, we deduce that all $\mathbf{tag}_A$-tagged subterms of $v\sigma_2$ is a subterm of $\sigma_1$ and so the result holds since $\sigma_1$ is an executed substitution for $\Phi_1 = \Phi_2$. In the latter case, $\Phi_1 \vdash v\sigma_2$ and Lemma 30 directly allow us to conclude.

Since $Q$ is an initial process, by Definition 47, we deduce that either $v$ is a fully $\mathbf{tag}_B$-tagged term and $c \notin \text{img}(\alpha_1) \cup \text{img}(\delta_1)$ or $v = \mathcal{E}\Sigma$ and $c = c_{pub} \in \text{Ch}_p$ where $\Sigma$ is a fully $\mathbf{tag}_B$-tagged substitution and $(\mathcal{E}, \mathcal{F})$ is an encapsulation. To prove the last property, we do a case analysis:

*Case v is a tag$_B$-tagged term and c $\notin$ img($\alpha_1$) $\cup$ img($\delta_1$):* Since $Q_1 = Q \mid \text{in}_A(c, v).R_A$ and $\alpha_1 = \alpha_2$, we deduce that $\text{Tr}_{\alpha_1}(Q_1) = \text{Tr}_{\alpha_2}(Q) \mid \text{in}_A(c, v).\text{Tr}_{\alpha_2}(R_A)$. But if $v\sigma_2 \in c\eta_1\sigma_1$ then $\mathbf{Ap}_{\delta_1}(v\sigma_1\sigma) \in \mathbf{Ap}_{\delta_1}(c\eta_1\sigma_1)$. But $v$ and $\eta_1$ only containing fully $\mathbf{tag}_B$-terms implies that $\mathbf{Ap}_{\delta_1}(v\sigma_1\sigma) = v\mathbf{Ap}_{\delta_1}(\sigma_1)\mathbf{Ap}_{\delta_1}(\sigma)$ and $\mathbf{Ap}_{\delta_1}(c\eta_1\sigma_1) = c\eta_1\mathbf{Ap}_{\delta_1}(\sigma_1)$. By definition of $\delta_2$, we have that $\mathbf{Ap}_{\delta_1}(\sigma) = \mathbf{Ap}_{\delta_2}(\sigma)$ and so by considering the substitution $\mathbf{Ap}_{\delta_2}(\sigma)$, we deduce that:

$$ \begin{array}{l} (\text{Tr}_{\alpha_1}(Q_1)\mathbf{Ap}_{\delta_1}(\sigma_1), \text{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1), \eta_1 \mathbf{Ap}_{\delta_1}(\sigma_1) \circ \mu(\Phi_1, \beta_1)) \\ \qquad \rightarrow \\ (\text{Tr}_{\alpha_2}(Q_2)\mathbf{Ap}_{\delta_2}(\sigma_2), \text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2), \eta_1 \mathbf{Ap}_{\delta_1}(\sigma_1) \circ \mu(\Phi_2, \beta_2)) \end{array} $$

The mapping $\eta_1 \mathbf{Ap}_{\delta_1}(\sigma_1)$ being ground, we have $\eta_1 \mathbf{Ap}_{\delta_1}(\sigma_1) = \eta_1 \mathbf{Ap}_{\delta_1}(\sigma_1) = \eta_1 \mathbf{Ap}_{\delta_2}(\sigma_1) \mathbf{Ap}_{\delta_2}(\sigma) = \eta_2 \mathbf{Ap}_{\delta_2}(\sigma_2)$. This allows us to conclude.

Let us now consider the case where $\Phi_1 \vdash v\sigma_2$. We know that $\delta_2 = \delta_1\delta'$, $\Phi_1 = \Phi_2$, $D_2 = D_1$, $N_2 = N_2$ and $H_2 = H_1$. Hence $\text{Tr}_{D_1 \cup N_1, \emptyset}^{H_1, \delta_1}(\Phi_1) = \text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2)$. By Lemma 41, we deduce that $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) \vdash \mathbf{Ap}_{\delta_2}(v\sigma_2)$. Once again since $v$ is a fully $\mathbf{tag}_B$-tagged term, we deduce that $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) \vdash v\mathbf{Ap}_{\delta_2}(\sigma_2)$. Therefore, by considering the substitution $\mathbf{Ap}_{\delta_2}(\sigma)$, the result holds.

*Case v = $\mathcal{E}\Sigma$ and c = $c_{pub} \in \text{Ch}_p$: In this case, by Definition 49, we deduce that there exists a channel $d$ such that $((\mathcal{E}, \mathcal{F}), X_{\mathcal{E}\Sigma})\alpha_1 = d$. Thus, we deduce that $\text{Tr}_{\alpha_1}(Q_1) = \text{Tr}_{\alpha_2}(Q_2) \mid \text{in}_A(d, t_{\mathcal{E}\Sigma}).\text{Tr}_{\alpha_2}(R_A)$. Moreover, since $c \in \text{Ch}_p$, we deduce that $c \notin \text{dom}(\mu_1)$ and $\Phi_1 \vdash v\sigma_1\sigma$. To conclude the result, we show that

- if $d \in \text{Ch}_p$ then $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) \vdash t_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2)$

- if $d \in \text{Ch}_c$ then $t_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2) \in d\mu(\Phi_2, \beta_2)$ or $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) \vdash t_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2)$

- if $d \in \text{Ch}_a \cup \text{Ch}_s$ then $t_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2) \in d\mu(\Phi_2, \beta_2)$.

But using the same reasoning as in the case of the rule Out with $(\text{Tr}_{\alpha_0}(P_0), \emptyset, id)$ being secure and the execution $(P_0, \emptyset, id) \stackrel{tr}{\Rightarrow}_{\sigma} (P, \Phi, \mu)$ being well-formed, we can deduce that if $d \in \text{Ch}_p$ then for all $k \in H$, $X_{\mathcal{E}k} \mathbf{Ap}_{\delta_2}(\Sigma_k) \cap X_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2) = \emptyset$. However, if $d \in \text{Ch}_c \cup \text{Ch}_a \cup \text{Ch}_s$ then there exists $k \in H$ such that $X_{\mathcal{E}k} \mathbf{Ap}_{\delta_2}(\Sigma_k) = X_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2)$. Moreover, we also know that $d \in \text{Ch}_c$ (resp. $\text{Ch}_a \cup \text{Ch}_s$) implies that $(\mathcal{E}, \mathcal{F})$ allows (resp. does not allow) confidential channels. Thus, by applying Lemma 43, we deduce that:

- if $d \in \text{Ch}_p$ then $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) \vdash t_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2)$.

- if $d \in \text{Ch}_c$ then either there exists $k \in H$ such that $\mathcal{E}_k \sim \mathcal{E}$ and $\mathcal{E}_k \mathbf{Ap}_{\delta_2}(\Sigma_k) = \mathcal{E}\Sigma \mathbf{Ap}_{\delta_2}(\sigma_2)$ or $\text{Tr}_{D_2 \cup N_2, \emptyset}^{H_2, \delta_2}(\Phi_2) \vdash t_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2)$. In the former case, by Definition 50, it implies that $t_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2) \in d\mu(\Phi_2, \beta_2)$ hence the result holds.

- if $d \in \text{Ch}_a \cup \text{Ch}_s$ then there exists $k \in H$ such that $\mathcal{E}_k \sim \mathcal{E}$ and $\mathcal{E}_k \mathbf{Ap}_{\delta_2}(\Sigma_k) = \mathcal{E}\Sigma \mathbf{Ap}_{\delta_2}(\sigma_2)$ and so as previously, it implies that $t_{\mathcal{E}\Sigma} \mathbf{Ap}_{\delta_2}(\sigma_2) \in d\mu(\Phi_2, \beta_2)$.
**Rule NEW-K:** In such a case, $Q_1 = Q \mid \text{new } x.R_A, \Phi_2 = \Phi_1, \mu_2 = \mu_1$ and $P_2 = Q\sigma_1 \mid R_A\sigma_1\{k/x\}$ where $k$ is a fresh name in $N_H$ if $A \in \mathcal{A}gt_H$ else $k \in N_D$. Therefore, the result trivially holds with $Q_2 = Q \mid R_A\{k/x\}, \Phi_2 = \Phi_1, \delta_2 = \delta_1, \eta_2 = \eta_1, D_2 = D_1, N_2 = N_1, H_2 = H_1, \beta_2 = \beta_1$ and $\alpha_2 = \{(\mathcal{E}, F), X_{\mathcal{E}}\Sigma\{k/x\}) \to c \mid ((\mathcal{E}, F), X_{\mathcal{E}}\Sigma)\alpha_1 = c\}$.

**Rule NEW-C:** In such a case, $Q_1 = Q \mid \text{new } c.Q', \Phi_2 = \Phi_1, \mu_2 = \mu_1$ and $P_2 = Q\sigma_1 \mid R_A\sigma_1\{c'/c\}$ where $c'$ is name in $Ch_a$ (resp. $Ch_c, Ch_s$) if $c \in Ch_a$ (resp. $Ch_c, Ch_s$) and for all $I \in \mathcal{A}gt_D, c \in ch_I(Q')$ else $c' \in Ch_p$. Therefore, the result trivially holds with $Q_2 = Q \mid R_A\{c'/c\}, \Phi_2 = \Phi_1, \delta_2 = \delta_1, \eta_2 = \eta_1, D_2 = D_1, N_2 = N_1, H_2 = H_1, \beta_2 = \beta_1$ and $\alpha_2 = \alpha_1\{c'/c\}$.

**Rule REPL:** In such a case, $Q_1 = Q \mid !Q'$ where $dom(\sigma_1) \cap vars(Q') = \emptyset, \Phi_2 = \Phi_1, \mu_2 = \mu_1$ and $P_2 = Q\sigma_1 \mid !Q' \mid Q\rho$ where $\rho$ is a fresh renaming of variables in $Q'$. We also know that the variables in $Q_1$ are bound once. Therefore, the result trivially holds with $Q_2 = Q \mid !Q' \mid Q\rho, \Phi_2 = \Phi_1, \delta_2 = \delta_1, \eta_2 = \eta_1, D_2 = D_1, N_2 = N_1, H_2 = H_1, \beta_2 = \beta_1$ and $\alpha_2 = \alpha_1 \circ ((\mathcal{E}, F), X_{\mathcal{E}}\Sigma\rho) \to c \mid ((\mathcal{E}, F), X_{\mathcal{E}}\Sigma)\alpha_1 = c$ and $vars(img(\Sigma)) \cap dom(\rho) \neq \emptyset$.

**Other rules:** Trivial.

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

Let $S$ be a set of channels. We say that two processes $P$ and $Q$ are composable under $S$ and $C'$ if $P = C[R_1, \dots, R_n], Q = C'[R'_1, \dots, R'_n]$ and $C[\_] = C'[\_]\upharpoonright_S$ for some contexts $C[\_], C'[\_]$ and for some roles $R_i, R'_i$ of the same agent, for $i = 1 \dots n$.

**Theorem 17.** Let $\mathbf{tag}_A$ and $\mathbf{tag}_B$ be two disjoint sets of tags. Let $S_e$ be a set of $\mathbf{tag}_A$-encapsulation allowing authentic, confidential, and secure channels. Let $\rho$ be a mapping from channels to $T_{\mathcal{A}g_1} \times S_e$. Let $P$ and $Q$ be two closed executable composable $\mathbf{tag}_B$-processes under $\rho$ such that $P$ and $Q$ do not share names and $\mathbf{fa}(P) = \mathbf{fa}(Q) = \emptyset$. Let $\tilde{P}$ be an annotation of $P$ under $\rho$. If $\tilde{P}$ is secure and $Q$ preserves secrecy then $\tilde{P}^\rho Q$ preserves secrecy as well.

**Proof.** Since $P$ and $Q$ are composable under $\rho$, let us denote $P = C[R_1, \dots, R_n]$ and $Q = C'[R'_1, \dots, R'_n]$. Moreover, following Definition 13, let us denote $\tilde{P}^\rho Q = C_0[R_1.R''_1, \dots, R_n.R''_n]$ where $C_0 = C^{C,C'}\upharpoonright_S$ and $R''_1, \dots, R''_n$ are defined as described in Definition 13 with $\tilde{P} = C[R_1 ev_1(c_1, ta_1, ts_1, tp_1), \dots, \tilde{R}_n ev_n(c_n, ta_n, ts_n, tp_n)]$.

Let us consider $\tilde{C}, C_1$ two contexts such that $\tilde{C}$ and $C'$ are composable; and $\tilde{C}|_{\upharpoonright_S} = C$. Let us denote $C_1 = C^{\tilde{C},C'}$. Note that $C_0 = C_1|_{\upharpoonright_S}$. Lastly, let us define $\gamma$ a bijective mapping from $S$ to fresh channels of same kind, that is $c\theta \in Ch_a$ (resp. $Ch_c, Ch_s$) is equivalent to $c \in Ch_a$ (resp. $Ch_c, Ch_s$).

We denote by $P_0 = C_1[\tilde{R}_1.R''_1, \dots, \tilde{R}_n.R''_n]$. We first show that for all execution $(\tilde{P}^\rho Q, \emptyset, \emptyset, \emptyset) \stackrel{tr}{\Rightarrow} (P', \Phi, \mu)\theta$ there exists $P''$ and $tr'$ such that $(P_0, \emptyset, \emptyset, \emptyset) \stackrel{tr'}{\Rightarrow} (P'', \Phi, \mu)\theta$ is a well-formed execution and $tr$ is the trace $tr'$ where we removed the events of the form $ev(c, ta, ts, tp, d)$ with $ev \in \tilde{E}v$.

By construction, the differences between $P_0$ and $\tilde{P}^\rho Q$ lie the addition of some channel declarations in $C_0$ and the some events. But the declared channels are not used in any output or input of $R_i$ and $R''_i$. Thus, we trivially have that for all execution $(\tilde{P}^\rho Q, \emptyset, \emptyset, \emptyset) \stackrel{tr}{\Rightarrow} (P', \Phi, \mu)\theta$ there exists $P''$ and $tr'$ such that $(P_0, \emptyset, \emptyset, \emptyset) \stackrel{tr'}{\Rightarrow} (P'', \Phi, \mu, \theta)$ and $tr$ is the trace $tr'$ where we removed the events of the form $ev(c, ta, ts, tp, d)$ with $ev \in \tilde{E}v$. The existence of a well-formed execution is then given by Lemma 46.

We now show that $P_0$ is an initial process and that there exists $\alpha_0$ a mapping of channels for $P_0$ such that $\text{Tr}_{\alpha_0}(P_0) = C_1[\tilde{R}_1.R'_1, \dots, \tilde{R}_n.R'_n]$. We already know that $P$ and $Q$ are fully $\mathbf{tag}_B$-tagged processes. Moreover, by Definition 13, we know that for all $i \in \{1, \dots, n\}, R''_i$ is the process $R'_i$ where some instances of $\mathbf{out}_A(c, u)$ (resp. $\text{in}_A(c, u)$) are replaced by $\mathbf{out}_A(c_{pub}, \mathcal{E}\sigma)$ (resp. $\text{in}_A(c_{pub}, \mathcal{E}\sigma)$) when $c\rho = (ta, (\mathcal{E}, F))$ and $\mathbf{event}_A(\tilde{e}v_i(d, ta, X_{\mathcal{E}}\sigma, F\sigma, c))$ is in $\tilde{R}_i$ for some substitution $\sigma$. By Definition 47, we deduce that $P_0$ is initial.
Moreover, let us define $\alpha_0$ such mapping such that for all $i \in \{1, \dots, n\}$, for all instances of $\text{out}_A(c, u)$ (resp. $\text{in}_A(c, u)$) in $R'_i$, if $\text{event}_A(\text{ev}_i(d, ta, X_E\sigma, F\sigma, c))$ is in $\tilde{R}_i$ and $c\rho = (ta, (\mathcal{E}, F))$ for some $ta, c, (\mathcal{E}, F)$ then $((\mathcal{E}, F), X_E\sigma)\alpha_0 = c$. Since by Definition 9, $c\rho = (ta, (\mathcal{E}, F))$ implies that $c \in Ch_a$ (resp. $Ch_c, Ch_s$) is equivalent to $(\mathcal{E}, F)$ allows authentic (resp. confidential, secure) channels. Therefore, we can deduce from Definition 48 that $\alpha_0$ is a mapping of channels for $P_0$. Lastly, following Definition 48 and Definition 13, we directly obtain that $\text{Tr}_{\alpha_0}(P_0) = C_1[\tilde{R}_1.R'_1, \dots, \tilde{R}_n.R'_n]$.

Let us now prove that $(\text{Tr}_{\alpha_0}(P_0), \emptyset, \emptyset, \emptyset)$ is secure. We know that $\tilde{P}$ is secure. But the properties of Definition 16 are all reachability properties which are preserved by parallel composition. Hence, we have that $(\tilde{P} | Q, \emptyset, \emptyset, \emptyset) = (C[\tilde{R}_1, \dots, \tilde{R}_n] | C'[R'_1, \dots, R'_n], \emptyset, \emptyset, \emptyset)$ is secure. But we know that $P$ and $Q$ do not share any names and channels$(C_1) \cap channels(R_1, \dots, R_n) \cap channels(R'_1, \dots, R'_n) = \emptyset$. Thus, a simple induction allows us to prove that $(C_1[\tilde{R}_1.R'_1, \dots, \tilde{R}_n.R'_n], \emptyset, id, =)(\text{Tr}_{\alpha_0}(P_0), \emptyset, \emptyset)\emptyset$ is secure.

With the same reasoning as above, we can prove that $(C_1[\tilde{R}_1.R'_1, \dots, \tilde{R}_n.R'_n], \emptyset, \emptyset, \emptyset) = (\text{Tr}_{\alpha_0}(P_0), \emptyset, \emptyset, \emptyset)$ preserves the secrecy of some term $t$ shared by some agents $A_1, \dots, A_n$. We now show that $(P_0, \emptyset, id)$ also preserves the secrecy of $t$ shared by $A_1, \dots, A_n$.

Let $(P_0, \emptyset, \emptyset, \emptyset) \stackrel{tr}{\Rightarrow}_{\sigma} (P', \Phi, \mu)\theta$ a well formed execution, and agent $B$ and an event $\text{Sec}(t', (A'_1, \dots, A'_n))$ such that $(B, \text{Sec}(t', (A'_1, \dots, A'_n))) \in \text{tr}$ and $\Phi \vdash t'$. By Lemma 51, we deduce that there exists an initial process $U$, a mapping of channels $\alpha$ (resp. $\beta$) for $U$ (resp. $\Phi$), and $\eta, \delta, D, N$ and $H$ such that:

- $U\sigma = P$; and

- $\eta\sigma = \mu$ and $\eta$ only contains fully $\text{tag}_B$-terms; and

- $U, \Phi, \alpha, \beta, \text{tr}$ and $\sigma$ have conforming events; and

- $\Phi$ is a well formed frame for $S_e, D, N$ and $H$; and

- $\sigma$ is an executed substitution for $\Phi$; and

- $\delta$ is a $\text{tag}_A$-mapping of $\Phi$ and $\sigma$; and

- $(\text{Tr}_{\alpha}(P_0), \emptyset, \emptyset, \emptyset) \stackrel{A_{p_{\delta}}(tr)}{\Longrightarrow} A_{p_{\delta}}(\sigma) (\text{Tr}_{\alpha}(U)A_{p_{\delta}}(\sigma), \text{Tr}_{D \cup N, \emptyset}^{H, \delta}(\Phi), \eta A_{p_{\delta}}(\sigma) \circ \mu(\Phi, \beta), \theta)$

But $(B, \text{Sec}(t', (A'_1, \dots, A'_n))) \in \text{tr}$ implies that $(B, \text{Sec}(A_{p_{\delta}}(t'), (A'_1, \dots, A'_n))) \in A_{p_{\delta}}(\text{tr})$. Moreover, by Lemma 41 and Definition 36, $\Phi \vdash t'$ implies that $\text{Tr}_{D \cup N, \emptyset}^{H, \delta}(\Phi) \vdash A_{p_{\delta}}(t')$. This is a contradiction with the fact that $(\text{Tr}_{\alpha_0}(P_0), \emptyset, \emptyset, \emptyset)$ also preserves the secrecy of $t$ shared by $A_1, \dots, A_n$. Therefore, $(P_0, \emptyset, \emptyset, \emptyset)$ indeed preserves the secrecy of $t$ shared by $A_1, \dots, A_n$.

Note that in $P_0$ the channels $\text{channels}(C_1) \setminus \text{channels}(C)$ do not appear in any $\tilde{R}_i.R''_i$, for $i = 1..n$. As such, removing them still preserves the secrecy of $t$ shared by $A_1, \dots, A_n$. Lastly, for all $i \in \{1, \dots, n\}$, the difference between $\tilde{R}_i$ and $R_i$ is the addition of some event $\text{ev}$ that are different from the event $\text{Sec}$, removing them also preserves secrecy meaning that $C[R_1.R''_1, \dots, R_n.R''_n] = \tilde{P}^{\prec} Q$ preserves the secrecy of $t$ shared by $A_1, \dots, A_n$. This allows us to conclude. $\quad$