$\Pi_C^{\Phi_M, \Phi_N}(C_n) = A_{p-1}$, so there exists a thread $t'_i = (x^j[\bar{x}]Q, id'_i, E'_i)$ in $C_n$ with $\Pi_M^{\Phi_M}(id'_i) = id_i$ and $\Pi_N^{\Phi_M, \Phi_N} \circ E'_i = E_i$; thanks to Lem. 44, there also exists $Cont'_i \in \beta(Q, id'_i, E'_i)$ such that $\Pi_C^{\Phi_M, \Phi_N}(Cont'_i) = Cont_i$; thanks to the induction hypothesis, there exists a thread $t_c = (unsafe![c], id_c, E_c)$ in $C_n$, such that $\Pi_N^{\Phi_M, \Phi_N}(E_c(c)) = E_i(x)$; we first use the resource **repli** to replicate the thread $t_c$: we obtain a configuration $C_{n+1} = C_n \setminus \{t_c\} \cup \{t'_c; t''_c\}$ where $t'_c$ matches $(unsafe![c], id'_c, E'_c)$ and $t''_c$ matches $(unsafe![c], id''_c, E''_c)$ with $E'_c(c) = E''_c(c) = E_c(c)$; we then replicate the resource **spy**$_k$ by consuming the thread $t'_c$, and obtain the configuration $C_{n+2} = C_{n+1} \setminus \{t'_c\} \cup \{t_s\}$, where $t_s$ matches $(c?[y_1, ..., y_k](unsafe![y_1] | ... | unsafe![y_k]), id_s, E_s)$ with $E_s(c) = E_c(c)$; we have $\Pi_N^{\Phi_M, \Phi_N}(E_s(c)) = \Pi_N^{\Phi_M, \Phi_N}(E'_i(x))$; so thanks to Lem. 47.(3), we deduce that $E_s(c) = E'_i(x)$; thus we perform the communication between the thread $t'_i$ and $t_s$ to obtain the configuration $C_{n+3} = (C_{n+2} \setminus \{t_s; t'_i\}) \cup Cont'_i \cup \{t'_{u_i} | i \in [1; k]\}$, where each $t'_{u_i}$ matches $(unsafe![y_i], id'_i, E'_i)$ with $E'_i(y_i) = E'_i(x_i)$.

* the computation sequence $C_n \xrightarrow{\ast_e} C_{n+2}$ does not involve any thread of $S_I$; by Lem. 45, we have $\Pi_C^{\Phi_M, \Phi_N}(C_{n+2}) = A_{p-1}$; we conclude that $\Pi_C^{\Phi_M, \Phi_N}(C_{n+3}) = A_p$; moreover $C_{n+2} \xrightarrow{i',j} C_{n+3}$ with $i' \notin L_I$; so $\Pi_{\tau(S_I, \Phi_M, \Phi_N)}(C_0...C_{n+2} \xrightarrow{(i',j)} C_{n+3}) = \tau'$.

* let $(u, id_u)$ be an unsafe name occurring in a state of $\tau$:

* in the case that $(u, id_u) = E_i(x)$, $t''_c$ is a thread of $C_{n+3}$ and matches $(unsafe![y], id, E)$ with $\Pi_N^{\Phi_M, \Phi_N}(E(y)) = E_i(x)$;

* in the case that $(u, id_u) = E_i(x_i)$, $t_{u_i}$ is a thread of $C_{n+3}$ and matches $(unsafe![y_i], id, E)$ which satisfies $\Pi_N^{\Phi_M, \Phi_N}(E(y_i)) = \Pi_N^{\Phi_M, \Phi_N}(E'_i(x_i))$; so $\Pi_N^{\Phi_M, \Phi_N}(E(y_i)) = E_i(x_i)$;

* otherwise there is necessarily a thread in $C_n$ which matches $(unsafe![y], id, E)$ with $\Pi_N^{\Phi_M, \Phi_N}(E(y)) = (x, id_x)$ and this thread is still in $C_{n+3}$.

(d) in the case that $(A_{p-1}, U_{p-1}, F_{p-1}) \overset{\lambda}{\rightleftharpoons} (A_p, U_p, F_p)$ is a spoilt communication: there is a thread $t_? = (y^?i[y_1, ..., y_k]P, id_?, E_?)$ with $E_?(y) \in U_{p-1}$ (we set $(u_0, id_0) = E_?(y)$), there is a channel name $(u_i, id_i) \in U_{p-1}$ for each $i \in [1; k]$, and a continuation $Cont_? \in \beta(P, id_?, E_?[y_i \mapsto (u_i, id_i)])$ such that $A_p = (A_{p-1} \setminus t_?) \cup Cont_?$, and $U_p = U_{p-1}$; moreover, we have $\Pi_C^{\Phi_M, \Phi_N}(C_n) = A_{p-1}$, so there exists a thread $t'_? = (y^?j[\bar{y}]P, id'_?, E'_?)$ in $C_n$ with $\Pi_M^{\Phi_M}(id'_?) = id_?$ and $\Pi_N^{\Phi_M, \Phi_N} \circ E'_? = E_?$; we first deal with the names that the context sends into the system $S_I$ for the first time: for each element $(u_i, id_i)$ of the set $\{(u_i, id_i) | i \in [1; k]\}$ that does not occur in any state of $\tau$, we create a new unsafe name using the resource **new**, as the result we get a fresh name $(channel, id_{chan_i})$ and, since $(u_i, id_i)$ is necessarily in $en$, we extend the definition of $\Phi_N$ with $\Phi_N(channel, id_{chan_i}) = (u_i, id_i)$; we obtain a state $C_{n+1}$ and an updated into map $\Phi_N$, such that
there exists a thread $t_{c_i} = (unsafe![c], id_{c_i}, E_{c_i})$ in the state $C_{n+1}$ such that $\Pi_{\mathcal{N}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(E_{c_i}(c)) = (u_i, id_i)$, for each $i \in [0; k]$; we then use the resource **repli** to replicate the threads $t_{c_i}$ until we obtain a configuration $C_{n+2} = (C_{n+1} \setminus \{t_{c_i} | i \in [0; k]\}) \cup \{t'_{c_i} | i \in [0; k]\} \cup \{t''_{c_i} | 0 \in [1; k]\}$ where $t'_{c_i}$ matches $(unsafe![c], id'_{c_i}, E'_{c_i})$ and $t''_{c_i}$ matches $(unsafe![c], id''_{c_i}, E''_{c_i})$ with $E'_{c_i}(c) = E''_{c_i}(c) = E_{c_i}(c)$ such that the threads $t'_{c_i}$ and $t''_{c_i}$ are all distinct from each other; we then replicate the resource **spoil$_k$** by consuming the thread $t'_{c_0}$, and obtain the configuration $C_{n+3} = (C_{n+2} \setminus \{t'_{c_0}\}) \cup \{t_s\}$, where $t_s$ matches $(unsafe?[x_1]...unsafe?[x_k]c![\bar{x}], id_s, E_s)$ with $E_s(c) = E_{c_0}(c)$; we then use successively the threads $t'_{c_i}$ to obtain a configuration $C_{n+4} = (C_{n+2} \setminus \{t'_{c_i} | i \in [0; k]\}) \cup \{t_m\}$, where $t_m$ matches $(x_0![\bar{x}], id_m, E_m)$ with $E_m(x_i) = E''_{c_i}(c)$, for each $i \in [0; k]$; moreover the thread $t'_? = (y?^j[\bar{y}]P, id'_?, E'_?)$ is in $C_{n+4}$ with $\Pi_{\mathcal{M}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(id'_?) = id_?, \Pi_{\mathcal{N}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}} \circ E'_? = E_?$, and $\Pi_{\mathcal{N}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(E''_{c_i}(c)) = (u_i, id_i)$, for each $i \in [1; k]$; thanks to Lem. 44, there also exists $Cont'_? \in \beta(P, id'_?, E'_? [y_i \mapsto E''_{c_i}(c)])$ such that $\Pi_{\mathcal{C}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(Cont'_?) = Cont_?; \text{ thus we perform the communication between the thread } t'_? \text{ and } t_m \text{ to obtain the configuration } C_{n+5} = C_{n+4} \setminus \{t'_?; t_m\} \cup Cont'_?.$

* the computation sequence $C_n \xrightarrow{\cdot_e} C_{n+4}$ does not involve thread of $S_I$, by Lem. 45, we have $\Pi_{\mathcal{C}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(C_{n+4}) = A_{p-1}$; then we conclude that $\Pi_{\mathcal{C}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(C_{n+5}) = A_p$; moreover $C_{n+4} \xrightarrow{i,j'} e C_{n+5}$ with $j' \notin \mathcal{L}_I$; so $\Pi_{\tau}(S_I, \Phi^{\mathcal{M}}, \Phi^{\mathcal{N}})(C_0...C_{n+4}) \xrightarrow{(i,j')} e C_{n+5}) = \tau'$.

* let $(u, id_u)$ be an unsafe name occurring in a state of $\tau$:

* in the case that $(u, id_u) = (u_i, id_i)$ with $i \in [0; k]$, $t''_{c_i}$ is a thread of $C_{n+5}$ and matches $(unsafe![c], id, E)$ with $\Pi_{\mathcal{N}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(E(c)) = (u_i, id_i)$;

* otherwise there is necessarily a thread in $C_n$ which matches $(unsafe![y], id, E)$ with $\Pi_{\mathcal{N}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(E(y)) = (x, id_x)$ and this thread is still in $C_{n+5}$.

(e) in the case that $(A_{p-1}, U_{p-1}, F_{p-1}) \stackrel{\lambda}{\rightleftharpoons} (A_p, U_p, F_p)$ is a spoilt replication: there is a thread $t_? = (*y?^i[y_1, ..., y_k]P, id_?, E_?)$ with $E_?(y) \in U_{p-1}$ (we set $(u_0, id_0) = E_?(y)$), there are several channel names $(u_i, id_i) \in U_{p-1}$, for $i \in [1; k]$, a marker $id_? \in F_{p-1}$ and a continuation $Cont_? \in \beta(P, N((i, 0), id_?, id_?), E_?[y_i \mapsto (u_i, id_i)])$, such that $A_p = A_{p-1} \cup Cont_?$, $U_p = U_{p-1}$ and $F_p = F_{p-1} \setminus \{id_?\}$; moreover, we have $\Pi_{\mathcal{C}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(C_n) = A_{p-1}$, so there exists a thread $t'_? = (*y?^j[\bar{y}]P, id'_?, E'_?)$ in $C_n$ with $\Pi_{\mathcal{M}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}}(id'_?) = id_? \text{ and } \Pi_{\mathcal{N}}^{\Phi^{\mathcal{M}}, \Phi^{\mathcal{N}}} \circ E'_? = E_?; \text{ we first deal with the names that the context sends into the system } S_I \text{ for the first time: for each element } (u_i, id_i) \text{ of the set } \{(u_i, id_i) | i \in [1; k]\} \text{ that does not occur in any state of } \tau, \text{ we create a new unsafe name using the resource new, as the result we get a fresh name } (channel, id_{chan_i}) \text{ and, since } (u_i, id_i) \text{ is necessarily in } en, \text{ we extend the definition of}$
$\Phi_N$ with $\Phi_N(channel, id_{chani}) = (u_i, id_i)$; we obtain a state $C_{n+1}$ and an updated into map $\Phi_N$, such that there exists a thread $t_{c_i} = (unsafe![c], id_{c_i}, E_{c_i})$ in the state $C_{n+1}$ such that $\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E_{c_i}(c)) = (u_i, id_i)$, for each $i \in [0; k]$; we then use the resource **repli** to replicate the threads $t_{c_i}$ until we obtain a configuration $C_{n+2} = (C_{n+1} \setminus \{t_{c_i} | i \in [0; k]\}) \cup \{t'_{c_i} | i \in [0; k]\} \cup \{t''_{c_i} | 0 \in [1; k]\}$ where $t'_{c_i}$ matches $(unsafe![c], id'_{c_i}, E'_{c_i})$ and $t''_{c_i}$ matches $(unsafe![c], id''_{c_i}, E''_{c_i})$ with $E'_{c_i}(c) = E''_{c_i}(c) = E_{c_i}(c)$, such that the threads $t'_{c_i}$ and $t''_{c_i}$ are all distinct from each other; we then replicate the resource **spoil**$_k$ by consuming the thread $t'_{c_0}$, and obtain the configuration $C_{n+3} = C_{n+2} \setminus \{t'_{c_0}\} \cup \{t_s\}$, where $t_s$ matches $(unsafe?[x_1]...unsafe?[x_k]c!|\bar{x}|, id_s, E_s)$ with $E_s(c) = E_{c_0}(c)$; we then use successively the threads $t'_{c_i}$ to obtain a configuration $C_{n+4} = (C_{n+2} \setminus \{t'_{c_i} | i \in [0; k]\}) \cup \{t_m\}$, where $t_m$ matches $(x_0!^{s_k}[\bar{x}], id_m, E_m)$ with $E_m(x_i) = E''_{c_i}(c)$, for all $i \in [0; k]$; by Prop. 4 it is the first time this syntactic component is tagged with the marker $id_m$; so we extend the definition of $\Phi_M$ with $\Phi_M(s_k, id_m) = id_l$; thus we have $\Pi_{\mathcal{M}}^{\Phi_M}(N((i, s_k), id'_?, id_m)) = N((i, 0), id_?, id_l)$; moreover the thread $t'_? = (y?^j[y]P, id'_?, E'_?)$ is in $C_{n+4}$ with $\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N} \circ E'_? = E_?$, and $\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E''_{c_i}(c)) = (u_i, id_i)$, for each $i \in [1; k]$; by Lem. 44, there also exists $Cont'_? \in \beta(P, N((i, s_k), id'_?, id_m), E'_?|\{y_i \mapsto E''_{c_i}(c)\})$ such that $\Pi_{\mathcal{C}}^{\Phi_M, \Phi_N}(Cont'_?) = Cont_?; thus we perform the communication between the thread $t'_?$ and $t_m$ to obtain the configuration $C_{n+5} = C_{n+4} \setminus \{t_m\} \cup Cont'_?.$

* the computation sequence $C_n \xrightarrow{e}^* C_{n+4}$ does not involves thread of $S_I$, by Lem. 45, we have $\Pi_{\mathcal{C}}^{\Phi_M, \Phi_N}(C_{n+4}) = A_{p-1}$; we conclude that $\Pi_{\mathcal{C}}^{\Phi_M, \Phi_N}(C_{n+5}) = A_p$; moreover $C_{n+4} \xrightarrow{i,j'} e C_{n+5}$ with $j' \notin \mathcal{L}_I$; so $\Pi_{\tau}(S_I, \Phi_M, \Phi_N)(C_0...C_{n+4} \xrightarrow{(i,j')} e C_{n+5}) = \tau'$.

* let $(u, id_u)$ be an unsafe name occurring in a state of $\tau$:

* in the case that $(u, id_u) = (c_i, id_{c_i}$, for $i \in [0; k]$, $t''_{c_i}$ is a thread of the state $C_{n+5}$ and matches $(unsafe![c], id, E)$ where $\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E(c)) = (u_i, id_i)$;

* otherwise there is necessarily a thread in $C_n$ which matches $(unsafe![y], id, E)$ with $\Pi_{\mathcal{N}}^{\Phi_M, \Phi_N}(E(y)) = (x, id_x)$ and this thread is still in $C_{n+5}$. $\square$

## E Abstract Interpretation framework

In this section we give the proof of Props. 27 and 28 which provide generic tools to compose abstractions.

**Proposition 27 (Product)** Let $(C_1^\sharp, \sqsubseteq_1^\sharp, \sqcup_1^\sharp, \perp_1^\sharp, \gamma_1, C_{0_1}^\sharp, \rightsquigarrow_1, \nabla_1)$ and $(C_2^\sharp, \sqsubseteq_2^\sharp, \sqcup_2^\sharp, \perp_2^\sharp, \gamma_2, C_{0_2}^\sharp, \rightsquigarrow_2, \nabla_2)$ be two abstractions.
The following tuple $(C^{\sharp}, \sqsubseteq^{\sharp}, \sqcup^{\sharp}, \perp^{\sharp}, \gamma, C_0^{\sharp}, \rightsquigarrow, \nabla)$ where

* $C^{\sharp} = C_1^{\sharp} \times C_2^{\sharp}$;

* $\sqsubseteq^{\sharp}, \sqcup^{\sharp}, \perp^{\sharp}$ and $\nabla$ are defined pair-wise;

* $\gamma : \begin{cases} C^{\sharp} \to \wp(\Sigma^* \times C) \\ (a_1^{\sharp}, a_2^{\sharp}) \mapsto \gamma_1(a_1^{\sharp}) \cap \gamma_2(a_2^{\sharp}) \end{cases}$

* $C_0^{\sharp} = (C_{01}^{\sharp}, C_{02}^{\sharp})$;

* $\rightsquigarrow$ is defined by:

$$ (a_1, a_2) \rightsquigarrow (b_1, b_2) \text{ if and only if } a_1 \rightsquigarrow_1 b_1 \text{ and } a_2 \rightsquigarrow_2 b_2 $$

is also an abstraction.

**PROOF.** The tuple $(C^{\sharp}, \sqsubseteq^{\sharp}, \sqcup^{\sharp}, \perp^{\sharp}, \gamma, C_0^{\sharp}, \rightsquigarrow, \nabla)$ satisfies Def. 24:

* Props. (1),(2),(3),(7) are usual properties of the Cartesian product;

* Prop. (4) is satisfied, since both $\gamma_1$ and $\gamma_2$ are monotonic;

* Prop. (5) holds because we have both $\gamma(C_0^{\sharp}) = \gamma_1(C_{01}^{\sharp}) \cap \gamma_2(C_{02}^{\sharp})$ and $\forall i \in \{1; 2\}, \{\varepsilon\} \times C_0^{\circ}(S) \subseteq \gamma_i(C_{0i}^{\sharp})$;

* Prop. (6) is satisfied:

let $C^{\sharp} = (a_1, a_2)$ be an abstract element in $C^{\sharp}$, $(u, C)$ be a concrete element which satisfies $(u, C) \in \gamma(C^{\sharp})$, $\lambda$ be a transition label in $\Sigma$ and $\overline{C}$ a concrete state such that $C \stackrel{\lambda}{\rightleftharpoons} \overline{C}$, we need to construct an abstract element $\overline{C}^{\sharp} \in C^{\sharp}$ such that $C^{\sharp} \rightsquigarrow \overline{C}^{\sharp}$ and $(u.\lambda, \overline{C}) \in \gamma(\overline{C}^{\sharp})$: in accordance with Def. 24.6, for all $i \in \{1; 2\}$, we can choose $b_i \in C_i^{\sharp}$, such that $a_i \rightsquigarrow_i b_i$ and $(u.\lambda, \overline{C}) \in \gamma(b_i)$; so, by definition of $\rightsquigarrow$, we have $(a_1, a_2) \rightsquigarrow (b_1, b_2)$ and, since $\gamma(b_1, b_2) = \gamma_1(b_1) \cap \gamma_2(b_2)$, we obtain that $(u.\lambda, \overline{C}) \in \gamma(b_1, b_2)$; so $(b_1, b_2)$ is a valid candidate. $\square$

**Proposition 28 (Reduction)** Let $(C^{\sharp}, \sqsubseteq^{\sharp}, \sqcup^{\sharp}, \perp^{\sharp}, \gamma, C_0^{\sharp}, \rightsquigarrow, \nabla)$ be an abstraction, and $\rho$ be a reduction operator$^{12}$ $\rho : C^{\sharp} \to C^{\sharp}$ which satisfies:

$$ \forall a^{\sharp} \in C^{\sharp}, \gamma(a^{\sharp}) \subseteq \gamma(\rho(a^{\sharp})). $$

The following tuple $(C^{\sharp}, \sqsubseteq^{\sharp}, \sqcup^{\sharp}, \perp^{\sharp}, \gamma, C_{0\rho}^{\sharp}, \rightsquigarrow, \nabla)$ where

* $C_{0\rho}^{\sharp} = \rho(C_0^{\sharp})$;

* $\rightsquigarrow_{\rho}$ is defined by:

$$ a \rightsquigarrow_{\rho} c \text{ if and only if there exists } b \in C^{\sharp}, \text{ such that } \rho(a) \rightsquigarrow b \text{ and } c = \rho(b) $$

is also an abstraction.

<footnote>$^{12}$ $\rho$ simplifies the properties obtained in the abstract domain.</footnote>
Furthermore, $\rho$ can also be used to simplify the final result of the abstract iteration.

**PROOF.** The tuple $(C^\sharp, \sqsubseteq^\sharp, \sqcup^\sharp, \perp^\sharp, \gamma, C_{0\rho}^\sharp, \rightsquigarrow_\rho, \nabla)$ satisfies Def. 24:

* Props. (1),(2),(3),(4),(7) hold because $(C^\sharp, \sqsubseteq^\sharp, \sqcup^\sharp, \perp^\sharp, \gamma, C_0^\sharp, \rightsquigarrow_\rho, \nabla)$ is an abstraction;

* Prop. (5) is satisfied because we have:

* $\{ (\varepsilon, c_0) \mid c_0 \in C_0(S) \} \subseteq \gamma(C_0^\sharp)$ (since $(C^\sharp, \sqsubseteq^\sharp, \sqcup^\sharp, \perp^\sharp, \gamma, C_0^\sharp, \rightsquigarrow_\rho, \nabla)$ is an abstraction),

* $\gamma(C_0^\sharp) \subseteq \gamma(\rho(C_0^\sharp))$ (by definition of $\rho$),

* $C_{0\rho}^\sharp = \rho(C_0^\sharp)$ (by definition of $C_{0\rho}^\sharp$),

so $\{\varepsilon\} \times C_0^o(S) \subseteq \gamma(C_0^\sharp) \subseteq \gamma(\rho(C_0^\sharp)) = \gamma(C_{0\rho}^\sharp)$;

* Prop. (6) is satisfied:

let $a$ be an element of $C^\sharp$, $(u, C)$ be a concrete element which satisfies $(u, C) \in \gamma(a)$, $\lambda$ be a transition label in $\Sigma$ and $\bar{C}$ a concrete state such that $C \stackrel{\lambda}{\rightleftharpoons} \bar{C}$, we need to construct an abstract element $\bar{b} \in C^\sharp$ such that $C^\sharp \rightsquigarrow_\rho \bar{b}$ and $(u.\lambda, \bar{C}) \in \gamma(\bar{b})$: we have $(u, C) \in \gamma(a) \subseteq \gamma(\rho(a))$ and $C \stackrel{\lambda}{\rightleftharpoons} \bar{C}$, so in accordance with Def. 24.6, we can choose $b \in C^\sharp$ such that $\rho(a) \stackrel{\lambda}{\rightsquigarrow} b$ and $(u.\lambda, \bar{C}) \in \gamma(b)$; then, by definition of $\stackrel{\lambda}{\rightsquigarrow}_\rho$, we have $a \stackrel{\lambda}{\rightsquigarrow}_\rho \rho(b)$, and, since $\gamma(b) \subseteq \gamma(\rho(b))$, we obtain that $(u.\lambda, \bar{C}) \in \gamma(\rho(b))$; so $\rho(b)$ is a valid candidate. $\square$

## F Control flow analysis

In this section we give the proof of Thm. 30 which establishes the soundness of our control flow analysis.

**Proposition 29** $\forall P \in \mathcal{P}, \forall id \in \gamma_1(id^\sharp), \forall E \in (fn(P) \to (\nu n(S) \times \mathcal{M}))$ such that $\forall m \in fn(P), \forall n \in \nu n(S), \forall id_n \in \mathcal{M}, [E(m) = (n, id_n) \implies (id, id_n) \in \gamma_2(E^\sharp(m, n))], we have:

$$ \Sigma^* \times (\beta(P, id, E) \times \{\emptyset\} \times \wp(\{t_n \mid n \in \mathbb{N}\})) \subseteq \gamma(\beta^\sharp(P, id^\sharp, E^\sharp)). $$

**PROOF.** By definition of $\gamma$ and since $x \in \emptyset$ implies anything, we only have to prove the following proposition Prop($P$): given $id^\sharp \in \mathrm{Id}_1^\sharp$ and $E^\sharp \in ((bn(S) \times \nu n(S)) \to \mathrm{Id}_2^\sharp)$, given a marker $id \in \mathcal{M}$ and an environment $E \in (fn(P) \to$
$(\nu n(S) \times \mathcal{M}))$ such that:

$$ \left\{ \begin{array}{l} \text{id} \in \gamma_1(id^\sharp) \\ \forall m \in \text{fn}(P), [E(m) = (n, id_m) \implies (id, id_m) \in \gamma_2(E^\sharp(m, n))] \end{array} \right. $$

then for any thread $(Q, id_Q, E_Q) \in \cup \beta(P, id, E)$, and any free name $x$ of $Q$, we have:

$$ \left\{ \begin{array}{l} \beta^\sharp(P, id^\sharp, E^\sharp) = (f, g) \\ E_Q(x) = (y, id_y) \end{array} \right. \implies (id_Q, id_x) \in \gamma_2(f(Q, x, y)) $$

for any sub-term $P \in \mathcal{P}$.

We prove $\forall P \in \mathcal{P}, \text{Prop}(P)$ by induction on the syntax of $P$: let $P \in \mathcal{P}$ be a sub-term, $id \in \gamma_1(id^\sharp)$ be a marker, $E \in (\text{fn}(P) \to (\nu n(S) \times \mathcal{M}))$ be an environment such that for all $m$ free names of $P$, for all $n \in \nu n(S)$, for all marker $id_n \in \mathcal{M}$, we have $[E(m) = (n, id_n) \implies (id, id_n) \in \gamma_2(E^\sharp(m, n))]$:

* if sub-term $P$ matches $\mathbf{0}$,

we have $\beta(P, id, E) = \emptyset$, so the property is trivial;

* if sub-term $P$ matches $aQ$,

we have $\beta(P, id, E) = \{\{aQ, id, E_{\text{fn}(aQ)}\}\}$, let $x$ be a free name of $aQ$, we denote $E(x) = (y, id_x)$ and $\beta^\sharp(P, id^\sharp, E^\sharp) = (f, g)$, by assumption we have $(id, id_x) \in \gamma_2(E^\sharp(x, y))$, besides we have $\beta^\sharp(P, id^\sharp, E^\sharp) = ([P, m, n] \mapsto E^\sharp(m, n), \forall m \in \text{fn}(P), n \in \nu n(S], \emptyset)$, so $f(aQ, x, y) = E^\sharp(x, y)$, and we obtain $(id, id_x) \in \gamma_2(f(aQ, x, y))$;

* if sub-term $P$ matches $(\nu n)Q$,

* we first prove that we can apply the induction hypothesis: we have $id \in \gamma_1(id^\sharp)$; let $m$ be a free name of $Q$; in the case that $m = n$ we have $E[n \mapsto (n, id)](m) = (n, id)$ and $(id, id) \in \gamma_2(E^\sharp[(n, n) \mapsto \text{dpush}(id^\sharp)](n, n))$; otherwise we denote $E[n \mapsto (n, id)](m)$ by $(o, id_m)$, since $E[n \mapsto (n, id)](m) = E(m)$, we have $E(m) = (o, id_m)$ and by assumption we get that $(id, id_m) \in \gamma_2(E^\sharp(m, o))$, then since $E^\sharp[(n, n) \mapsto \text{dpush}(id^\sharp)](m, o) = E^\sharp(m, o)$, we get that $(id, id_m) \in \gamma_2(E^\sharp[(n, n) \mapsto \text{dpush}(id^\sharp)](m, o))$; thus in both cases, the assertion $E[n \mapsto (n, id)](m) = (o, id_m)$ implies the fact that $(id, id_m) \in \gamma_2(E^\sharp[(n, n) \mapsto \text{dpush}(id^\sharp)](m, o))$;

* let $T_R = (R, id_R, E_R)$ be a thread in $\cup \beta((\nu n)Q, id, E)$, we have $\beta((\nu n)Q, id, E) = \beta(Q, id, E[n \mapsto (n, id)])$ so $T_R$ is also a thread in $\cup \beta(Q, id, E[n \mapsto (n, id)])$, so by the induction hypothesis, we obtain that for any free name $x$ of $R$, we have:

$$ \left\{ \begin{array}{l} \beta^\sharp(Q, id^\sharp, E^\sharp[(n, n) \mapsto \text{dpush}(id^\sharp)]) = (f', g') \\ E[n \mapsto (n, id_R)](x) = (y, id_y) \end{array} \right. \implies (id_R, id_x) \in \gamma_2(f'(R, x, y)); $$
then since $\beta^\sharp(Q, id^\sharp, E^\sharp[(n, n) \mapsto dpush(id^\sharp)]) = \beta^\sharp((\nu n)Q, id^\sharp, E^\sharp)$ we can conclude that for any free name $x$ of $R$, we have:

$$ \left\{ \begin{array}{l} \beta^\sharp((\nu n)Q, id^\sharp, E^\sharp) = (f', g') \\ E[n \mapsto (n, id_R)](x) = (y, id_y) \end{array} \right. \implies (id_R, id_x) \in \gamma_2(f'(R, x, y)). $$

• if sub-term $P$ matches $Q_1 | Q_2$ or with $Q_1 \oplus Q_2$,

• we first prove that we can apply the induction hypothesis on both $Q_1$ and $Q_2$: let $i$ be either 1 or 2: we have $id \in \gamma_1(id^\sharp)$; let $m$ be a free name in $Q_i$, we know that $m$ is also a free name in $P$ so by assumption we have $[E(m) = (n, id_m) \implies (id, id_m) \in \gamma_2(E^\sharp(m, n))]$;

• let $T = (R, id, E)$ be a thread in $\cup \beta(P, id, E)$, we know that $\cup \beta(P, id, E) = (\cup \beta(Q_1, id, E)) \cup (\cup \beta(Q_2, id, E))$, so $T$ is either a thread in $\cup \beta(Q_1, id, E)$, or a thread in $\cup \beta(Q_2, id, E)$, let us assume by symmetry that $T$ is a thread of $\cup \beta(Q_1, id, E)$; let $x$ be a free name of $R$, we know by the induction hypothesis that:

$$ \left\{ \begin{array}{l} \beta^\sharp(Q_1, id^\sharp, E) = (f', g') \\ E(x) = (y, id_y) \end{array} \right. \implies (id_R, id_x) \in \gamma_2(f'(R, x, y)); $$

then, since we have $\beta^\sharp(P, id^\sharp, E^\sharp) = \sqcup^\sharp\{\beta^\sharp(Q_1, id^\sharp, E^\sharp); \beta^\sharp(Q_2, id^\sharp, E^\sharp)\}$, we get that $\beta^\sharp(Q_1, id^\sharp, E) \sqsubseteq^\sharp \beta^\sharp(P, id^\sharp, E)$, so we conclude that:

$$ \left\{ \begin{array}{l} \beta^\sharp(P, id^\sharp, E^\sharp) = (f', g') \\ E(x) = (y, id_y) \end{array} \right. \implies (id_R, id_x) \in \gamma_2(f'(R, x, y)). $$

□

**Theorem 30** ($C^\sharp, \sqsubseteq^\sharp, \sqcup^\sharp, \perp^\sharp, \gamma, C_0^\sharp, \rightsquigarrow_{cfa}, \nabla$) is an abstraction.

**PROOF.** The tuple ($C^\sharp, \sqsubseteq^\sharp, \sqcup^\sharp, \perp^\sharp, \gamma, C_0^\sharp, \rightsquigarrow_{cfa}, \nabla$) satisfies Def. 24:

• Props. (1)(2)(3)(4)(7) follow from usual properties of both component-wise and pair-wise extension;

• Prop. (5) is satisfied: we denote $\beta^\sharp(S, \varepsilon^\sharp, [(n, ext) \mapsto \varepsilon^\sharp \bullet t^\sharp, \forall n \in fn(S)])$ by (f,g), let $E$ be an environment in $(fn(S) \to en)$ and $C$ be a configuration in $\beta(S, \varepsilon, E)$, we want to prove that $(\varepsilon, (C, en, \{t_n | n \in \mathbb{N}\})) \in \gamma(C_0^\sharp)$:

• we have $\varepsilon \in \gamma_1(\varepsilon^\sharp)$; let $m$ be a free name in $S$: by definition of $en$, there exists $i \in \mathbb{N}$ such that $E(m) = (ext, t_i)$; since $\{\varepsilon\} \times \{t_n | n \in \mathbb{N}\} \subseteq \gamma_2^\sharp(\varepsilon^\sharp \bullet t^\sharp)$, we obtain that $(\varepsilon, t_i) \in \gamma_2([n, ext) \mapsto \varepsilon^\sharp \bullet t^\sharp](m, ext))$; so by Prop. 29, we obtain that:

$$ \Sigma^* \times (\beta(S, \varepsilon, E) \times \{\emptyset\} \times \wp(\{t_n | n \in \mathbb{N}\})) \in \gamma((f, g)). $$
this proves that for all thread $(P, id_P, E_P)$ in $C$, for all free name $x$ in $P$ such that $E(x) = (y, id_x)$, we have $(id_P, id_x) \in \gamma_2(f(P, x, y))$;

• we have $en = \{ext\} \times \{t_n | n \in \mathbb{N}\}$, and for all $n$ in $\mathbb{N}$ we have $t_n \in \gamma_1(t^\sharp)$, so for all $(x, id) \in en$, we have $id \in \gamma_1([ext \mapsto t^\sharp](x))$, which means that $id \in \gamma_1(g(x))$;

• Prop. (6) is satisfied: let $C^\sharp = (f, g)$ be an abstract configuration, $(u, C)$ be in the concretization $\gamma(C^\sharp)$, $\lambda$ be a transition label and $\overline{C}$ be another configuration such that $C \overset{\lambda}{\rightleftharpoons} \overline{C}$, we must construct $\overline{C}^\sharp$ such that $(u.\lambda, \overline{C}) \in \gamma(\overline{C}^\sharp)$ and $C^\sharp \overset{\lambda}{\rightleftharpoons} \overline{C}^\sharp$.

(1) In the case that $C \overset{\lambda}{\rightleftharpoons} \overline{C}$ is a communication transition: we denote $C = (A, U, F)$; there exist two syntactic components $P_0$ and $Q_0$, such that $P_0$ matches $y?i[y]P$ and $Q_0$ matches $x!j[x]Q$, such that there exists two threads $(P_0, id_?, E_?)$ and $(Q_0, id_!, E_!)$ in $A$ with $E_?(y) = E_!(x)$, two continuations $Cont_? \in \beta(P, id_?, E_?[y_i \mapsto E_!(x_i)])$ and $Cont_! \in \beta(Q, id_!, E_!)$ such that $\overline{C}$ is $((A \setminus \{(P_0, id_?, E_?); (Q_0, id_!, E_!\}) \cup Cont_? \cup Cont_!, U, F)$; we denote $E_!(x) = (c, id_c)$, since $(u, C) \in \gamma(C^\sharp)$, we have $(id_?, id_c) \in \gamma_2(f(P_0, y, c))$ and $(id_!, id_c) \in \gamma_2(f(Q_0, x, c))$; then we can deduce that $(id_?, id_c, id_!, id_c) \in \gamma_4(\text{sync}(\{2, 4\}, f(P_0, y, c) \bullet f(Q_0, x, c)))$; since $\gamma_4$ is strict we obtain that $\sqcup_4 \{\text{sync}(\{2, 4\}, f(P_0, y, u) \bullet f(Q_0, x, u) \mid u \in \nu n(S))\} \neq \bot^\sharp_4$; so we can introduce $\overline{C}^\sharp = (f', g')$ such that $C^\sharp \overset{\lambda}{\rightleftharpoons} \overline{C}^\sharp$; we denote $\overline{C} = (\overline{A}, U, F)$, and introduce for each name $u \in \nu n(S)$, the abstract element $A(u) = \text{sync}(\{2, 4\}, f(P_0, y, u) \bullet f(Q_0, x, u))$, we also introduce two abstract markers $id_P^\sharp$ and $id_Q^\sharp$ and two abstract environments $E_P^\sharp$ and $E_Q^\sharp$ as follows:

$$ 
\begin{align*}
id_P^\sharp &= \bigsqcup_1 \{ \Pi_{(1)} (A(u)) \mid u \in \nu n(S) \}, \\
E_P^\sharp &= [(m, n) \mapsto \bigsqcup_2 \{ I_P(m, n, u) \mid u \in \nu n(S) \}, \forall m \in fn(P), n \in \nu n(S)]
\end{align*}
$$

where

$$ I_P(m, n, u) = \begin{cases} \Pi_{(1,6)} \text{sync}(\{3, 5\}, A(u) \bullet f(Q_0, x_i, n)) & \text{if } m = y_i \\ \Pi_{(1,6)} \text{sync}(\{1, 5\}, A(u) \bullet f(P_0, m, n)) & \text{otherwise.} \end{cases} $$

$$ 
\begin{align*}
id_Q^\sharp &= \bigsqcup_1 \{ \Pi_{(3)} (A(u)) \mid u \in \nu n(S) \}, \\
E_Q^\sharp &= [(m, n) \mapsto \bigsqcup_2 \{ I_Q(m, n, u) \mid u \in \nu n(S) \}, \forall m \in fn(Q), n \in \nu n(S)]
\end{align*}
$$

where $I_Q(m, n, u) = \{ \Pi_{(3,6)} \text{sync}(\{3, 5\}, A(u) \bullet f(Q_0, m, n))$.

We now prove that $(u.\lambda, \overline{C}) \in \gamma(\overline{C}^\sharp)$:

(a) let $T_R = (R, id_R, E_R)$ be a thread of $\overline{A}$, $x$ a free name of $R$ and $(y, id_x)$ such that $E_R(x) = (y, id_x)$, we need to prove that $(id_R, id_x) \in$
$\gamma_2(f'(R, x, y))$:

(i) if $T_R$ is a thread of $A$: we have $(u, C) \in \gamma(\overline{C})$, so $(id_R, id_x) \in \gamma_2(f(R, x, y))$, then $(f, g) \sqsubseteq (f', g')$ and $\gamma_2$ is monotonic, so $(id_R, id_x) \in \gamma_2(f'(R, x, y))$;

(ii) if $T_R$ is a thread of $\bigcup \beta(P, id_?, E_? [y_i \mapsto E_!(x_i)])$: we know that $(id_?, id_c, id_!, id_c) \in \gamma_4(A(c))$; this implies that $id_? \in \gamma_1(id_P^?)$; let us take $m$ be a free name in $P$, we denote $E_? [y_i \mapsto E_!(x_i)](m) = (n, id_n)$; in the case that $m$ matches $y_i$, we have $(n, id_n) = E_!(x_i)$; since $(Q_0, id_!, E_!)$ is a thread of $A$ and $(A, U, F) \in \gamma(f, g)$; we know that $(id_!, id_n) \in \gamma_2(f(Q_0, x_i, n))$ and $(id_?, id_c, id_!, id_c) \in \gamma_4(A(c))$, so $(id_?, id_c, id_!, id_c, id_n) \in \gamma_6(A(c) \bullet f(Q_0, x_i, n))$, then since $id_! = id_!$, we conclude that $(id_?, id_n) \in \gamma_2(E_P^?(m, n))$; in the other case, $m$ is a free name of $y?^i[y]P$; since $(P_0, id_?, E_?)$ is a thread of $A$, and $(A, U, F) \in \gamma(f, g)$, we obtain that $(id_?, id_n) \in \gamma_2(f(\lambda, m, n))$; then since $(id_P, id_c, id_Q, id_c) \in \gamma_4(A(c))$, we get that $(id_?, id_c, id_!, id_c, id_?, id_n) \in \gamma_6(A(c) \bullet f_{\text{can}}^?(P_0, m, n))$; then since $id_? = id_?$, we conclude that $(id_?, id_n) \in \gamma_2(E_P^?(m, n))$; so in any case, we have $(id_?, id_n) \in \gamma_2(E_P^?(m, n))$; we can then deduce from Prop. 29 that for any free name $m$ of $T_R$, $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

(iii) if $T_R$ is a thread of $\bigcup \beta(Q, id_!, E_!)$: we have $(id_?, id_u, id_!, id_c) \in \gamma_4(A(c))$, so $id_! \in \gamma_1(id_Q^?)$; let $m$ be a free name in $Q$, we denote $E_!(m) = (n, id_n)$; since $(Q_0, id_!, E_!)$ is a thread of $A$, and $(A, U, F) \in \gamma(f, g)$, we have $(id_!, id_n) \in \gamma_2(f(Q_0, m, n))$; then $(id_?, id_c, id_!, id_c, id_!, id_n) \in \gamma_6(A(c) \bullet f(Q_0, m, n))$; then since $id_! = id_!$, we conclude that $(id_!, id_n) \in \gamma_2(E_Q^?(m, n))$; then, we can deduce from Prop. 29 that for any free name $m$ of $T_R$, $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

so in any case, for any name $x$ free in $T_R$, we have $E_R = (y, id_y)$ implies that $(id_R, id_y) \in \gamma_2(f'(R, x, y))$;

(b) let $(x, id)$ be an element in $U$, we have $(A, U, F) \in \gamma((f, g))$ so $id \in \gamma_1(g(x))$, since $g = g'$ we obtain $id \in \gamma_1(g'(x))$.

So, in accordance with the definition of $\gamma$, we obtain that $(A', U, F) \in \gamma(\overline{C}^?)$.

(2) In the case that $C \stackrel{\lambda}{\hookrightarrow} \overline{C}$ is a resource replication: we denote $C = (A, U, F)$, there exist two syntactic components $P_0$ and $Q_0$, such that $P_0$ matches $*y?^i[y]P$ and $Q_0$ matches with $x!^j[\bar{x}]Q$, such that there exist two threads $(P_0, id_?, E_?)$ and $(Q_0, id_!, E_!)$ in $A$ with $E_?(y) = E_!(x)$, two continuations $Cont_? \in \beta(P, N((i, j), id_?, id_!), E_? [y_i \mapsto E_!(x_i)])$ and $Cont_! \in \beta(Q, id_!, E_!)$ such that $\overline{C}$ is $((A \setminus \{(Q_0, id_!, E_!\}) \cup Cont_? \cup Cont_!, U, F)$; we denote $E_!(x) = (c, id_c)$; since $(u, C) \in \gamma(C^?)$, we have $(id_?, id_c) \in \gamma_2(f(P_0, y, c))$ and $(id_!, id_c) \in \gamma_2(f(Q_0, x, c))$; so we can deduce that $(id_?, id_c, id_!, id_c) \in \gamma_4(\text{sync}(\{2, 4\}, f(P_0, y, c) \bullet f(Q_0, x, c)))$; since $\gamma_4$ is strict we obtain that $\sqcup_4(\text{sync}(\{2, 4\}, f(P_0, y, u) \bullet f(Q_0, x, u)) | u \in \nu n(S)) \neq \bot_4^?$; so we can
introduce $\overline{C}^{\sharp} = (f', g')$ such that $C^{\sharp} \stackrel{\lambda}{\rightsquigarrow} \overline{C}^{\sharp}$; we denote $\overline{C} = (\overline{A}, U, F)$, and introduce for each name $u \in \nu n(\mathcal{S})$, the abstract element $A(u) = \text{sync}(\{2, 4\}, f(P_0, y, u) \bullet f(Q_0, x, u))$, we also introduce two abstract mark- ers $id_P^{\sharp}$ and $id_Q^{\sharp}$ and two abstract environments $E_P^{\sharp}$ and $E_Q^{\sharp}$ as follows:

$$
\begin{align*}
id_P^{\sharp} &= \bigsqcup_1 \left\{ \prod_{(1)} (\text{push}(\prod_{(1,j)} (A(u)))) \mid u \in \nu n(\mathcal{S}) \right\}, \\
E_P^{\sharp} &= [(m, n) \mapsto \bigsqcup_2 \{ I_P(m, n, u) \mid u \in \nu n(\mathcal{S}) \}, \forall m \in \text{fn}(P), n \in \nu n(\mathcal{S})]
\end{align*}
$$

where

$$
I_P(m, n, u) = \begin{cases} \text{push}(\prod_{(i,j)} \text{sync}(\{3, 5\}, A(u) \bullet f(Q_0, x_i, n))) & \text{if } m = y_i \\ \text{push}(\prod_{(i,j)} \text{sync}(\{1, 5\}, A(u) \bullet f(P_0, m, n))) & \text{otherwise.} \end{cases}
$$

$$
\begin{align*}
id_Q^{\sharp} &= \bigsqcup_1 \{ \prod_{(3)} (A(u)) \mid u \in \nu n(\mathcal{S}) \}, \\
E_Q^{\sharp} &= [(m, n) \mapsto \bigsqcup_2 \{ I_Q(m, n, u) \mid u \in \nu n(\mathcal{S}) \}, \forall m \in \text{fn}(Q), n \in \nu n(\mathcal{S})]
\end{align*}
$$

$$
\text{where } I_Q(m, n, u) = \left\{ \prod_{(3,6)} \text{sync}(\{3, 5\}, A(u) \bullet f(Q_0, m, n)). \right\}
$$

We now prove that $(u.\lambda, \overline{C}) \in \gamma(\overline{C}^{\sharp})$:

(a) let $T_R = (R, id_R, E_R)$ be a thread of $\overline{A}$, $x$ a free name of $R$ and $(y, id_x)$ such that $E_R(x) = (y, id_x)$, we need to prove that $(id_R, id_x) \in \gamma_2(f'(R, x, y))$:

(i) if $T_R$ is a thread of $A$: we have $(u, C) \in \gamma(\overline{C})$, so $(id_R, id_x) \in \gamma_2(f(R, x, y))$, then $(f, g) \sqsubseteq (f', g')$ and $\gamma_2$ is monotonic, so $(id_R, id_x) \in \gamma_2(f'(R, x, y))$;

(ii) if $T_R$ is a thread of $\bigcup \beta(P, N((i, j), id_?, id_!), E_? [y_i \mapsto E_!(x_i)])$: we know that $(id_?, id_c, id_!, id_c) \in \gamma_4(A(c))$; so $(id_?, id_!, id_c) \in \gamma_3(\prod_{(1,3,4)} A(c))$ and $(N((i, j), id_?, id_!), id_c) \in \gamma_2(\text{push}(\prod_{(i,j)} (A(c))))$; then we conclude that $N((i, j), id_?, id_!) \in \gamma_1(id_P^{\sharp})$; let us take $m$ a free name in $P$, we denote $E_? [y_i \mapsto E_!(x_i)](m) = (n, id_n)$; in the case that $m$ matches $y_i$, we have $(n, id_n) = E_!(x_i)$, since $(Q_0, id_!, E_!)$ is a thread of $A$ and $(A, U, F) \in \gamma(f, g)$, we know that $(id_!, id_n) \in \gamma_2(f(Q_0, x_i, n))$; then since $(id_?, id_c, id_!, id_c) \in \gamma_4(A(c))$, we obtain that $(id_?, id_c, id_!, id_c, id_!, id_n) \in \gamma_6(A(c) \bullet f(Q_0, x_i, n))$; this way $(id_?, id_!, id_n) \in \gamma_3(\prod_{(1,3,6)} \text{sync}(\{3;5\}, A(c) \bullet f(Q_0, x_i, n)))$; so we can conclude that $(N((i, j), id_?, id_!), id_c) \in \gamma_2(E_P^{\sharp}(m, n))$; in the other case, $m$ is a free name of $*y?i[\overline{y}]P$; since $(P_0, id_?, E_?)$ is a thread of $A$, and $(A, U, F) \in \gamma(f, g)$, we get that $(id_?, id_n) \in \gamma_2(f(P_0, m, n))$; then since $(id_?, id_c, id_!, id_c) \in$
$\gamma_4(A(c))$, we obtain that $(id_?, id_c, id_!, id_c, id_?, id_n) \in \gamma_6(A(c) \bullet f(P_0, m, n))$; since $id_? = id_?$, we can deduce that $(id_?, id_!, id_n) \in \gamma_3(\prod_{(1,3,6)} (\text{sync}(\{1,5\}, A(c) \bullet f(P_0, m, n))));$ so we can conclude that $(N((i,j), id_?, id_!), id_c) \in \gamma_2(E_P^\sharp(m, n))$; so in any case, we have $(N((i,j), id_?, id_!), id_n) \in \gamma_2(E_P^\sharp(m, n))$; we can then deduce from Prop. 29 that for any free name $m$ of $T_R$, $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

(iii) if $T_R$ is a thread of $\cup \beta(Q, id_!, E_!)$: we have $(id_?, id_u, id_!, id_c) \in \gamma_4(A(c))$, so $id_! \in \gamma_1(id_Q^\sharp)$; let us take $m$ a free name in $Q$; we denote $E_!(m) = (n, id_n)$; since $(Q_0, id_!, E_!)$ is a thread of $A$, and $(A, U, F) \in \gamma(f, g)$, we have $(id_!, id_n) \in \gamma_2(f(Q_0, m, n))$; then $(id_?, id_c, id_!, id_c, id_!, id_n) \in \gamma_6(A(c) \bullet f(Q_0, m, n))$; then since $id_! = id_!$, we conclude that $(id_!, id_n) \in \gamma_2(E_Q^\sharp(m, n))$; we can then deduce from Prop. 29 that for any free name $m$ of $T_R$, $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

so in any case, for any name $x$ free in $T_R$, we have $E_R = (y, id_y)$ implies that $(id_R, id_y) \in \gamma_2(f'(R, x, y))$;

(b) let $(x, id)$ be an element in $U$, we have $(A, U, F) \in \gamma((f, g))$ so $id \in \gamma_1(g(x))$, since $g = g'$ we obtain $id \in \gamma_1(g'(x))$.

So in accordance with the definition of $\gamma$, we obtain that $(A', U, F) \in \overline{C}^\sharp$.

(3) In the case that $C \stackrel{\lambda}{\hookrightarrow} \overline{C}$ is a spied communication transition: we denote $C = (A, U, F)$, there exists a syntactic component $Q_0$, such that $Q_0$ matches $x^j[x_1, ..., x_n]Q$, such that there exists a thread $(Q_0, id_!, E_!)$ in $A$ with $E_!(x) \in U$ and a continuation $Cont_! \in \beta(Q, id_!, E_!)$ which satisfy $\overline{C} = ((A \setminus \{(Q_0, id_!, E_!\}) \cup Cont_!, U \cup \{E_!(x_i) | i \in [1; n]\}, F)$; we denote $E_!(x) = (c, id_c)$; since $(u, C) \in \gamma(C^\sharp)$, we have $(id_!, id_c) \in \gamma_2(f(Q_0, x, c))$ and $(id_c) \in \gamma_1(g(c))$; then $(id_!, id_c, id_c) \in \gamma_3(\text{sync}(\{2,3\}, f(Q_0, x, c) \bullet g(c)))$; since $\gamma_3$ is strict, we can conclude that $\bigcup_3 \{\text{sync}(\{2,3\}, f(Q_0, x, u) \bullet g(u)) | u \in \nu n(S)\} \neq \bigcup_3^\sharp$; so we can introduce $\overline{C}^\sharp = (f', g')$ such that $C^\sharp \stackrel{\lambda}{\rightsquigarrow} \overline{C}^\sharp$; we denote $\overline{C} = (\overline{A}, \overline{U}, \overline{F})$, and introduce for each name $u \in \nu n(S)$, the abstract element $A(u) = \text{sync}(\{2,3\}, f(Q_0, x, u) \bullet g(u))$, we also introduce an abstract marker $id_Q^\sharp$ and an abstract environment $E_Q^\sharp$ as follows:

$$id_Q^\sharp = \bigsqcup_1 \{\prod_{(1)} (A(u)) | u \in \nu n(S)\},$$

$$E_Q^\sharp = [(m, n) \mapsto \bigsqcup_2 \{I_Q(m, n, u) | u \in \nu n(S)\}, \forall m \in \text{fn}(Q), n \in \text{fn}(S)]$$

$$\text{where } I_Q(m, n, u) = \left\{ \prod_{(1,5)} \text{sync}(\{1,4\}, A(u) \bullet f(Q_0, m, n)) \right\}.$$

we now prove that $(u.\lambda, \overline{C}) \in \gamma(\overline{C}^\sharp)$:

(a) let $T_R = (R, id_R, E_R)$ be a thread of $\overline{A}$, $x$ be a free name in $R$, we denote $E_R(x) = (y, id_x)$, we need to prove that $(id_R, id_x) \in \gamma_2(f'(R, x, y))$:
(i) if $T_R$ is a thread of A: we have $(u, C) \in \gamma(\overline{C})$, so $(id_R, id_x) \in \gamma_2(f(R, x, y))$, then $(f, g) \sqsubseteq (f', g')$ and $\gamma_2$ is monotonic, so $(id_R, id_x) \in \gamma_2(f'(R, x, y))$;

(ii) if $T_R$ is a thread of $\cup \beta(Q, id_!, E_!)$: since $(id_!, id_c, id_c) \in \gamma_3(A(c))$, we have that $id_! \in \gamma_1(id_Q^!)$; let us take $m$ a free name in $Q$; we denote $E_!(m) = (n, id_n)$; since $(Q_0, id_!, E_!)$ is a thread of A, and $(A, U, F) \in \gamma(f, g)$, we obtain that $(id_!, id_n) \in \gamma_2(f(Q_0, m, n))$; then $(id_!, id_c, id_c, id_!, id_n) \in \gamma_5(A(c) \bullet f(Q_0, m, n))$; then since $id_! = id_1$, we conclude that $(id_!, id_n) \in \gamma_2(E_Q^!(m, n))$; we can then deduce from Prop. 29 that for any free name $m$ of $T_R$, $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

so in any case, for any name $m$ free in $T_R$, the fact $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

(b) let $(u, id)$ be an element in $\overline{U}$; we need to prove that $id \in \gamma_1(g(u))$:

(i) in the case that $(u, id) \in U$, we have $C \in \gamma(C^!)$, $C^! \sqsubseteq^! C^!$ and $\gamma$ is monotonic, then $C \in \gamma(\overline{C}^!)$ and $id \in \gamma_1(g'(u))$;

(ii) otherwise we have $(u, id) = E(x_k)$, so since $C \in \gamma(C^!)$, we obtain that $(id_!, id_c, id_c, id_!, id)$ in sync($\{(1, 4)\}$, $A(c) \bullet (f(Q_0, x_k, u))$), so $id \in \gamma_1(g'(u))$;

so in any case, for any $(u, id) \in \overline{U}$, we have $id \in \gamma_1(g'(u))$.

So in accordance with the definition of $\gamma$, we obtain that $(\overline{A}, \overline{U}, \overline{F}) \in \overline{C}^!$.

(4) In the case that $C \stackrel{\lambda}{\hookrightarrow} \overline{C}$ is a spoiled communication. We denote $C = (A, U, F)$, there exists a syntactic component $P_0$, such that $P_0$ matches $y?^i[\overline{y}]P$, such that there exists one thread $(P_0, id_?, E_?)$ in A with $E_?(y) \in U$, some elements $c_1, \dots, c_n$ in U and a continuation $Cont \in \beta(P, id_?, E_?)[y_i \mapsto c_i]$) that $\overline{C} = ((A \setminus \{(P_0, id_?, E_?)\}) \cup Cont, U, F)$; we denote $E_?(y) = (c, id_c)$; we have $(u, C) \in \gamma(C^!)$, so $(id_?, id_c) \in \gamma_2(f(P_0, y, c))$ and $(id_c) \in \gamma_1(g(c))$; then $(id_?, id_c, id_c) \in \gamma_3(\text{sync}(\{2, 3\}, f(P_0, y, c) \bullet g(c)))$; since $\gamma_3$ is strict we obtain that $\sqcup_3(\text{sync}(\{2, 3\}, f(P_0, y, c) \bullet g(c)) | u \in \nu n(\mathcal{S})) \neq \sqsubseteq_3^!)$; so we can introduce $\overline{C}^! = (f', g')$ such that $C^! \stackrel{\lambda}{\hookrightarrow} \overline{C}^!$; we denote $\overline{C} = (\overline{A}, U, F)$, and introduce for each name $u \in \nu n(\mathcal{S})$, the abstract element $A(u) = \text{sync}(\{2, 3\}, f(P_0, y, u) \bullet g(u))$, we also introduce an abstract marker $id_P^!$ and an abstract environment $E_P^!$ as follows:

$$id_P^! = \bigsqcup_1^{} \{ \Pi_{(1)} (A(u)) \mid u \in \nu n(\mathcal{S}) \},$$

$$E_P^! = [(m, n) \mapsto \bigsqcup_2^{} \{ I_P(m, n, u) \mid u \in \nu n(\mathcal{S}) \}, \forall m \in \text{fn}(P), n \in \nu n(\mathcal{S})]$$

where

$$I_P(m, n, u) = \begin{cases} id_P^! \bullet g(n) & \text{if } m = y_i \\ \Pi_{(1,5)} \text{sync}(\{1, 4\}, A(u) \bullet f(P_0, m, n)) & \text{otherwise.} \end{cases}$$

We now prove that $(u.\lambda, \overline{C}) \in \gamma(\overline{C}^!)$:
(a) let $T_R = (R, id_R, E_R)$ be a thread of $\overline{A}$, $x$ a free name of $R$ and $(y, id_x)$ such that $E_R(x) = (y, id_x)$, we need to prove that $(id_R, id_x) \in \gamma_2(f'(R, x, y))$:

(i) if $T_R$ is a thread of $A$: we have $(u, C) \in \gamma(\overline{C})$, so $(id_R, id_x) \in \gamma_2(f(R, x, y))$, then $(f, g) \subseteq (f', g')$ and $\gamma_2$ is monotonic, so $(id_R, id_x) \in \gamma_2(f'(R, x, y))$;

(ii) if $T_R$ is a thread of $\bigcup \beta(P, id_?, E_? [y_i \mapsto c_k])$: since $(id_?, id_c, id_c) \in \gamma_3(A(c))$, we deduce that $id_? \in \gamma_1(id_P^\sharp)$; let us take $m$ be a free name in $P$; we denote $E_? [y_i \mapsto E_l(x_i)](m) = (n, id_n)$; in the case that $m$ matches $y_i$, we have $(n, id_n) = c_i$; since $c_i \in U$ and $(A, U, F) \in \gamma(f, g)$, we know that $id_n \in \gamma_1(g(n))$; then since $id_? \in \gamma_1(id_P^\sharp)$, we get that $(id_?, id_n) \in \gamma_2(id_P^\sharp \bullet g(c))$; then we conclude that $(id_?, id_n) \in \gamma_2(E_P^\sharp(m, n))$; in the other case, $m$ is a free name of $y?^i[\overline{y}]P$; since $(P_0, id_?, E_?)$ is a thread of $A$, and $(A, U, F) \in \gamma(f, g)$, we obtain that $(id_?, id_n) \in \gamma_2(f(P_0, m, n))$; so, since $(id_?, id_c, id_c) \in \gamma_3(A(c))$, we have $(id_?, id_c, id_c, id_?, id_n) \in \gamma_5(A(c) \bullet (f(P_0, m, n)))$; then since $id_? = id_?$, we conclude that $(id_?, id_n) \in \gamma_2(E_P^\sharp(m, n))$; so in any case, we have $(id_?, id_n) \in \gamma_2(E_P^\sharp(m, n))$; we can then deduce from Prop. 29 that for any free name $m$ of $T_R$, $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

so in any case, for any name $m$ free in $T_R$, we have $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

(b) let $(x, id)$ be an element in $U$, we have $(A, U, F) \in \gamma((f, g))$ so $id \in \gamma_1(g(x))$, since $g = g'$ we obtain $id \in \gamma_1(g'(x))$.

So in accordance with the definition of $\gamma$, we obtain that $(A', U, F) \in \overline{C}^\sharp$.

(5) In the case that $C \stackrel{\lambda}{\hookrightarrow} \overline{C}$ is a spoiled resource replication. We denote $C = (A, U, F)$, there exists a syntactic component $P_0$, such that $P_0$ matches $*y?^i[\overline{y}]P$, such that there exists one thread $(P_0, id_?, E_?)$ in $A$ such that $E_?(y) \in U$, some elements $c_1, \dots, c_n$ in $U$, a fresh marker $id_! \in F$ and a continuation $Cont \in \beta(P, id_?, E_? [y_i \mapsto c_i])$ that $\overline{C} = ((C \setminus \{(P_0, id_?, E_?)\}) \cup Cont, U, F \setminus \{id_!\})$; we denote $E_?(y) = (c, id_c)$, since $(u, C) \in \gamma(C^\sharp)$, we have $(id_?, id_c) \in \gamma_2(f(P_0, y, c))$ and $(id_c) \in \gamma_1(g(c))$, so we deduce that $(id_?, id_c, id_c) \in \gamma_3.sync(\{2, 3\}, f(P_0, y, c) \bullet g(c)))$, and since $\gamma_3$ is strict we obtain that $\bigcup_3 sync(\{2, 3\}, f(P_0, y, c) \bullet g(c)) | u \in \nu n(S) \neq \perp_3^\sharp)$; so we can introduce $\overline{C}^\sharp = (f', g')$ such that $C^\sharp \stackrel{\lambda}{\rightsquigarrow} \overline{C}^\sharp$; we denote $\overline{C} = (\overline{A}, U, F)$, and introduce for each name $u \in \nu n(S)$, the abstract element $A(u) = sync(\{2, 3\}, f(P_0, y, u) \bullet g(u))$, we also introduce an abstract marker $id_P^\sharp$
and an abstract environment $E_P^\sharp$ as follows:

$$id_P^\sharp = \bigsqcup_1 \{ \prod_{(i,0)} (\text{push}((\prod_{(i,0)} (A(u))) \cdot t^\sharp \cdot \top_{\mathcal{M}}^\sharp)) | u \in \nu n(\mathcal{S}) \},$$

$$E_P^\sharp = [(m, n) \mapsto \bigsqcup_2 \{I_P(m, n, u) \mid u \in \nu n(\mathcal{S})\}, \forall m \in \text{fn}(P), n \in \nu n(\mathcal{S})]$$

where

$$I_P(m, n, u) = \begin{cases} id_P^\sharp \cdot g(n) & \text{if } m = y_i \\ \text{push}(\prod_{(i,0)} \text{sync}(\{1,4\}, A(u) \cdot f(P_0, m, n) \cdot t^\sharp)) & \text{otherwise.} \end{cases}$$

We now prove that $(u, \lambda, \bar{C}) \in \gamma(\bar{C}^\sharp)$:

(a) let $T_R = (R, id_R, E_R)$ be a thread of $\bar{A}$, $x$ a free name of $R$ and $(y, id_x)$ such that $E_R(x) = (y, id_x)$, we need to prove that $(id_R, id_x) \in \gamma_2(f'(R, x, y))$:

(i) if $T_R$ is a thread of $A$: we have $(u, C) \in \gamma(\bar{C})$, so $(id_R, id_x) \in \gamma_2(f'(R, x, y))$, then $(f, g) \sqsubseteq (f', g')$ and $\gamma_2$ is monotonic, so $(id_R, id_x) \in \gamma_2(f'(R, x, y))$;

(ii) if $T_R$ is a thread of $\bigcup \beta(P, N((i, 0), id_?, id_!))$, $E_? [y_i \mapsto c_k]$): we know that $(id_?, id_c, id_c) \in \gamma_3(A(c))$; so $id_? \in \gamma_1(\prod_{(1)}(A(c))$; moreover we have $id_! \in t^\sharp$; then for all $id \in \mathcal{M}$, we have $(id_?, id_!, id) \in \gamma_3(\prod_{(1)}(A(c)) \cdot t^\sharp \cdot \top_{\mathcal{M}}^\sharp)$; so $N((i, 0), id_?, id_!) \in \gamma_1(id_P^\sharp)$; let us take $m$ be a free name in $P$; we denote $E_? [y_i \mapsto E_!(x_i)](m) = (n, id_n)$; in the case that $m$ matches $y_i$, we have $(n, id_n) = c_i$; since $c_i \in U$ and $(A, U, F) \in \gamma(f, g)$, we know that $id_n \in \gamma_1(g(n))$; since $N((i, 0), id_?, id_!) \in \gamma_1(id_P^\sharp)$, we get that $(N((i, 0), id_?, id_!), id_n) \in \gamma_2(id_P^\sharp \cdot g(c))$; so $(N((i, 0), id_?, id_!), id_n) \in \gamma_2(E_P^\sharp(m, n))$; in the other case, $m$ is a free name of $y?^i[\bar{y}]P$; since $(P_0, id_?, E_?)$ is a thread of $A$, and $(A, U, F) \in \gamma(f, g)$; we obtain that $(id_?, id_n) \in \gamma_2(f(\lambda, m, n))$; since $(id_?, id_c, id_c) \in \gamma_3(A(c))$, we can deduce that $(id_?, id_c, id_c, id_?, id_n) \in \gamma_5(A(c) \cdot (f(P_0, m, n)))$; since $id_? = id_?$, we can conclude that $(N((i, 0), id_?, id_!), id_n) \in \gamma_2(E_P^\sharp(m, n))$; so in any case, we have $(N((i, 0), id_?, id_!), id_n) \in \gamma_2(E_P^\sharp(m, n))$; we can then deduce from Prop. 29 that for any free name $m$ of $T_R$, $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

so in any case, for any name $m$ free in $T_R$, we have $E_R = (n, id_n)$ implies that $(id_R, id_n) \in \gamma_2(f'(R, m, n))$;

(b) let $(x, id)$ be an element in $U$, we have $(A, U, F) \in \gamma((f, g))$ so $id \in \gamma_1(g(x))$, since $g = g'$ we obtain $id \in \gamma_1(g'(x))$.

So in accordance with the definition of $\gamma$, we obtain that $(A', U, F) \in \bar{C}^\sharp$.

□
G Occurrence counting abstraction

In this section we give the proof of Thm. 39 which establishes the soundness
of our occurrence counting analysis.

**Proposition 38** $\forall P \in \mathcal{P}, \forall id \in \mathcal{M}, \forall E \in (fn(P) \to (\nu n(\mathcal{S}) \times \mathcal{M}))$, we have $Cont \in \beta(P, id, E) \implies (\varepsilon, Cont) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(P))$.

**PROOF.** Prop. 38 is proved by induction on the syntax of P: let P be a sub-term in $\mathcal{P}$, id be a marker in $\mathcal{M}$, E be an environment in $(fn(P) \to (\nu n(\mathcal{S}) \times \mathcal{M}))$ and Cont be a continuation in $\beta(P, id, E)$:

* in the case that $P$ matches 0, we have $\beta(P, id, E) = \{\emptyset\}$; so $Cont = \emptyset$; then $\Pi_{\mathbb{N}^V}(\varepsilon, Cont) = (0)_{v \in V}$; since $(0)_{v \in V} \in \gamma_{\mathcal{N}_V}(0_{\mathcal{N}_V})$ and $\beta_{\mathcal{N}_V}(P) = (0)_{v \in V}$, we obtain that $(\varepsilon, \emptyset) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(P))$;

* in the case that $P$ matches $(\nu n)Q$, since $\beta(P, id, E) = \beta(Q, id, E[n \mapsto (n, id)])$, we have $(\varepsilon, Cont) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(Q))$ (by the induction hypothesis); since $\beta_{\mathcal{N}_V}(P) = \beta_{\mathcal{N}_V}(Q)$, we obtain that $(\varepsilon, Cont) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(P))$;

* in the case that $P$ matches $aQ$, we have $\beta(P, id, E) = \{( (P, id, E) )\}$; so $Cont = \{(P, id, E)\}$; then $\Pi_{\mathbb{N}^V}(\varepsilon, Cont) = (\delta_v^{aQ})_{v \in V}$; we obtain $(\varepsilon, Cont) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(aP))$, since $(\delta_v^{aQ})_{v \in V} \in \gamma_{\mathcal{N}_V}(1_{\mathcal{N}_V}(aP))$ and $\beta_{\mathcal{N}_V}(aP) = 1_{\mathcal{N}_V}(aP)$;

* in the case that $P$ matches $P_1 | P_2$, we have $\beta(P, id, E) = \{A_1 \cup A_2 | A_i \in \beta(P_i, id, E)\}$; let us take $(Cont_1, Cont_2) \in (\beta(P_1, id, E) \times \beta(P_2, id, E))$ such that $Cont = Cont_1 \cup Cont_2$, by the induction hypothesis, we have for any $i$ in the set $\{1; 2\}$, $(\varepsilon, Cont_i) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(P_i))$ (i.e. $\Pi_{\mathbb{N}^V}(\varepsilon, Cont_i) \in \gamma_{\mathcal{N}_V}(\beta_{\mathcal{N}_V}(P_i))$); moreover since $P \in \mathcal{P}$ is labelled with distinct labels, we have $Cont_1 \cap Cont_2 = \emptyset$; by applying Prop. 37, since $\Pi_{\mathbb{N}^V}(\varepsilon, Cont) = \Pi_{\mathbb{N}^V}(\varepsilon, Cont_1) + \Pi_{\mathbb{N}^V}(\varepsilon, Cont_2)$, we obtain $\Pi_{\mathbb{N}^V}(\varepsilon, Cont) \in \gamma_{\mathcal{N}_V}(\beta_{\mathcal{N}_V}(P_1) + \beta_{\mathcal{N}_V}(P_2))$; since $\beta_{\mathcal{N}_V}(P) = \beta_{\mathcal{N}_V}(P_1) + \beta_{\mathcal{N}_V}(P_2)$, we obtain $(\varepsilon, Cont) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(P))$.

* in the case that $P$ matches $P_1 \oplus P_2$, we have $\beta(P_1 \oplus P_2, id, E) = \beta(P_1, id, E) \cup \beta(P_2, id, E)$; so let us take $i$ in the set $\{1; 2\}$ such that $Cont \in \beta(P_i, id, E)$; by the induction hypothesis, we have $Cont \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(P_i))$; since $\beta_{\mathcal{N}_V}(P) = \beta_{\mathcal{N}_V}(P_1) \cup_{\mathcal{N}_V} \beta_{\mathcal{N}_V}(P_2)$, we get that $Cont \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\beta_{\mathcal{N}_V}(P))$. $\square$

**Theorem 39** $(\mathcal{N}_V, \sqsubseteq_{\mathcal{N}_V}, \cup_{\mathcal{N}_V}, \perp_{\mathcal{N}_V}, \gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V}, C_0^{\mathcal{N}_V}, \rightsquigarrow_{\mathcal{N}_V}, \nabla_{\mathcal{N}_V})$ is an abstraction.

**PROOF.** The tuple $(\mathcal{N}_V, \sqsubseteq_{\mathcal{N}_V}, \cup_{\mathcal{N}_V}, \perp_{\mathcal{N}_V}, \gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V}, C_0^{\mathcal{N}_V}, \rightsquigarrow_{\mathcal{N}_V}, \nabla_{\mathcal{N}_V})$ satisfies Def. 24:
• Props. (1)(2)(3)(7) are satisfied by our assumptions;

• Prop. (4) is satisfied since both $\gamma_{\mathbb{N}^V}$ and $\gamma_{\mathcal{N}_V}$ are monotonic;

• Prop. (5) is satisfied: we have $C_0^n(S) = \beta(S, \varepsilon, \emptyset)$ and $C_0^{\mathcal{N}_V} = \beta_{\mathcal{N}_V}(S)$, we conclude by Prop. 38 that $\{\varepsilon\} \times C_0^n(S) \subseteq C_0^{\mathcal{N}_V}$;

• Prop. (6) is satisfied: let $v^\sharp$ be an abstract configuration, $(u, C)$ be in the concretization $(\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(v^\sharp)$, $\lambda$ be a transition label and $\overline{C}$ be another configuration such that $C \stackrel{\lambda}{\rightleftharpoons} \overline{C}$, we must construct $\overline{C}^\sharp$ such that $(u.\lambda, \overline{C}) \in \gamma(\overline{C}^\sharp)$ and $C^\sharp \stackrel{\lambda}{\rightleftharpoons} \gamma_{\mathcal{N}_V}(\overline{C}^\sharp)$.

(1) in the case that $C \stackrel{\lambda}{\rightleftharpoons} \overline{C}$ is a communication transition: there exist two syntactic components $P_0$ and $Q_0$, such that $P_0$ matches with $y?^i[y]P$ and $Q_0$ matches with $x!^j[x]Q$, such that there exist two threads $(P_0, id_?, E_?)$ and $(Q_0, id_!, E_!)$ in $C$ with $E_?(y) = E_!(x)$, two continuations $Cont_? \in \beta(P, id_?, E_?[y_i \mapsto E_!(x_i)])$ and $Cont_! \in \beta(Q, id_!, E_!)$ such that $\overline{C}$ is $((C \setminus \{(P_0, id_?, E_?); (Q_0, id_!, E_!\}) \cup Cont_? \cup Cont_!)$; we have $(u, C) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(v^\sharp)$; so $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathcal{N}_V}(v^\sharp)$; then since $(P_0, id_?, E_?)$ and $(Q_0, id_!, E_!)$ are two threads of $C$, we have $(\Pi_{\mathbb{N}^V}(u, C))_{P_0} \ge 1$ and $(\Pi_{\mathbb{N}^V}(u, C))_{Q_0} \ge 1$; then $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathcal{N}_V}(\text{sync}_{\mathcal{N}_V}(\{i, j\}, v^\sharp))$; since $\gamma_{\mathcal{N}_V}$ is strict, we can conclude that $\text{sync}_{\mathcal{N}_V}(\{i, j\}, v^\sharp) \ne \perp_{\mathcal{N}_V}$; so we can introduce $\overline{v}^\sharp$ such that $C^\sharp \stackrel{\lambda}{\rightleftharpoons} \gamma_{\mathcal{N}_V}(\overline{C}^\sharp$; we now prove that $(u.\lambda, \overline{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\overline{v}^\sharp)$: we have $\overline{C} = ((C \setminus \{(P_0, id_?, E_?); (Q_0, id_!, E_!\}) \cup Cont_? \cup Cont_!)$; so $\Pi_{\mathbb{N}^V}(u.\lambda, \overline{C}) = \Pi_{\mathbb{N}^V}(u, C) - ((\delta_v^{P_0})_{v \in V} + (\delta_v^{Q_0})_{v \in V}) + \Pi_{\mathbb{N}^V}(\varepsilon, Cont_?) + \Pi_{\mathbb{N}^V}(\varepsilon, Cont_!) + (\delta_v^{\psi(\lambda)})_{v \in V}$; then we can deduce from Prop. 38 that $\Pi_{\mathbb{N}^V}(\varepsilon, Cont_?) \in \gamma_{\mathbb{N}^V}(\beta_{\mathcal{N}_V}(P))$ and that $\Pi_{\mathbb{N}^V}(\varepsilon, Cont_!) \in \gamma_{\mathbb{N}^V}(\beta_{\mathcal{N}_V}(Q))$; besides $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathcal{N}_V}(\text{sync}_{\mathcal{N}_V}(\{i, j\}, v^\sharp))$, so we conclude that $\Pi_{\mathbb{N}^V}(u.\lambda, \overline{C}) \in \gamma_{\mathcal{N}_V}(\text{sync}_{\mathcal{N}_V}(\{i, j\}, v^\sharp) - 1_{\mathcal{N}_V}(P_0) - 1_{\mathcal{N}_V}(Q_0) + 1_{\mathcal{N}_V}(\psi(\lambda)) + \beta_{\mathcal{N}_V}(P) + \beta_{\mathcal{N}_V}(Q))$; so $(u.\lambda, \overline{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\overline{v}^\sharp)$;

(2) in the case that $C \stackrel{\lambda}{\rightleftharpoons} \overline{C}$ is a resource replication: there exist two syntactic components $P_0$ and $Q_0$, such that $P_0$ matches $*y?^i[y]P$ and $Q_0$ matches with $x!^j[x]Q$, such that there exist two threads $(P_0, id_?, E_?)$ and $(Q_0, id_!, E_!)$ in $C$ with $E_?(y) = E_!(x)$, a marker $id_* \in \mathcal{M}$, two continuations $Cont_? \in \beta(P, id_*, E_?[y_i \mapsto E_!(x_i)])$ and $Cont_! \in \beta(Q, id_!, E_!)$ such that $\overline{C}$ is $((C \setminus \{(Q_0, id_!, E_!\}) \cup Cont_? \cup Cont_!)$; we have $(u, C) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(v^\sharp)$; so $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathcal{N}_V}(v^\sharp)$; then since $(P_0, id_?, E_?)$ and $(Q_0, id_!, E_!)$ are two threads of $C$, we have $(\Pi_{\mathbb{N}^V}(u, C))_{P_0} \ge 1$ and $(\Pi_{\mathbb{N}^V}(u, C))_{Q_0} \ge 1$; so we deduce that $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathcal{N}_V}(\text{sync}_{\mathcal{N}_V}(\{i, j\}, v^\sharp))$; since $\gamma_{\mathcal{N}_V}$ is strict, we get that $\text{sync}_{\mathcal{N}_V}(\{i, j\}, v^\sharp) \ne \perp_{\mathcal{N}_V}$; so we can introduce $\overline{v}^\sharp$ such that $C^\sharp \stackrel{\lambda}{\rightleftharpoons} \gamma_{\mathcal{N}_V}(\overline{C}^\sharp$; we now prove that $(u.\lambda, \overline{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\overline{v}^\sharp)$: we have $\overline{C} = ((C \setminus \{(Q_0, id_!, E_!\}) \cup Cont_? \cup Cont_!)$; so $\Pi_{\mathbb{N}^V}(u.\lambda, \overline{C}) = \Pi_{\mathbb{N}^V}(u, C) - (\delta_v^{Q_0})_{v \in V} + \Pi_{\mathbb{N}^V}(\varepsilon, Cont_?) + \Pi_{\mathbb{N}^V}(\varepsilon, Cont_!) + (\delta_v^{\psi(\lambda)})_{v \in V}$; then we deduce from Prop. 38 that $\Pi_{\mathbb{N}^V}(\varepsilon, Cont_?) \in \gamma_{\mathbb{N}^V}(\beta_{\mathcal{N}_V}(P))$ and that $\Pi_{\mathbb{N}^V}(\varepsilon, Cont_!)) \in \gamma_{\mathbb{N}^V}(\beta_{\mathcal{N}_V}(Q))$, we also have $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathcal{N}_V}(\text{sync}_{\mathcal{N}_V}(\{i, j\}, v^\sharp))$, and we conclude that $\Pi_{\mathbb{N}^V}(u.\lambda, \overline{C}) \in \gamma_{\mathcal{N}_V}(\text{sync}_{\mathcal{N}_V}(\{i, j\}, v^\sharp) - 1_{\mathcal{N}_V}(Q_0) + 1_{\mathcal{N}_V}(\psi(\lambda)) + \beta_{\mathcal{N}_V}(P) + \beta_{\mathcal{N}_V}(Q))$; so $(u.\lambda, \overline{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathcal{N}_V})(\overline{v}^\sharp)$;
(3) in the case that $C \stackrel{\lambda}{\rightleftarrows} \bar{C}$ is a spied communication: there exists one syntactic component $Q_0$, such that $Q_0$ matches $x!^j[\bar{x}]Q$, such that there exists one thread $(Q_0, id_!, E_!)$ in $C$, a continuation $Cont_! \in \beta(Q, id_!, E_!)$ such that $\bar{C}$ is $((C \setminus \{(Q_0, id_!, E_!\}) \cup Cont_!)$; we have $(u, C) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathbb{N}_V})(v^\sharp)$; so $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathbb{N}_V}(v^\sharp)$; and since $(Q_0, id_!, E_!)$ is a thread of $C$, we have $(\Pi_{\mathbb{N}^V}(u, C))_{Q_0} \ge 1$; then $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathbb{N}_V}(sync_{\mathbb{N}_V}(\{i\}, v^\sharp))$; since $\gamma_{\mathbb{N}_V}$ is strict, we can conclude that $sync_{\mathbb{N}_V}(\{i\}, v^\sharp) \ne \perp_{\mathbb{N}_V}$; so we can introduce $\bar{v}^\sharp$ such that $C^{\sharp} \stackrel{\lambda}{\rightsquigarrow}_{\mathbb{N}_V} \bar{C}^\sharp$; we now prove that $(u.\lambda, \bar{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathbb{N}_V})(\bar{v}^\sharp)$: we have $\bar{C} = ((C \setminus \{(Q_0, id_!, E_!\}) \cup Cont_!)$; so $\Pi_{\mathbb{N}^V}(u.\lambda, \bar{C}) = \Pi_{\mathbb{N}^V}(u, C) - (\delta_v^{Q_0})_{v \in V} + \Pi_{\mathbb{N}^V}(\varepsilon, Cont_!) + (\delta_v^{\psi(\lambda)})_{v \in V}$; then we can deduce from Prop. 38 that $\Pi_{\mathbb{N}^V}(\varepsilon, Cont_!) \in \gamma_{\mathbb{N}_V}(\beta_{\mathbb{N}_V}(Q))$; we also have $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathbb{N}_V}(sync_{\mathbb{N}_V}(\{i\}, v^\sharp))$; so $\Pi_{\mathbb{N}^V}(u.\lambda, \bar{C}) \in \gamma_{\mathbb{N}_V}(sync_{\mathbb{N}_V}(\{i\}, v^\sharp) - 1_{\mathbb{N}_V}(Q_0) + 1_{\mathbb{N}_V}(\psi(\lambda)) + \beta_{\mathbb{N}_V}(P))$; so we can conclude that $(u.\lambda, \bar{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathbb{N}_V})(\bar{v}^\sharp)$;

(4) in the case that $C \stackrel{\lambda}{\rightleftarrows} \bar{C}$ is a spoiled communication: there exists one syntactic component $P_0$, such that $P_0$ matches $y?^i[\bar{y}]P$ such that there exists one thread $(P_0, id_?, E_?)$ in $C$, and several tagged names $c_1, \dots, c_n \in \mathcal{N} \times \mathcal{M}$, a continuation $Cont_? \in \beta(P, id_?, E_?)[y_i \mapsto c_i]$ such that $\bar{C}$ is $((C \setminus \{(P_0, id_?, E_?)\} \cup Cont_?)$; we have $(u, C) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathbb{N}_V})(v^\sharp)$; so $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathbb{N}_V}(v^\sharp)$; then since $(P_0, id_?, E_?)$ is a thread of $C$, we have $(\Pi_{\mathbb{N}^V}(u, C))_{P_0} \ge 1$; then $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathbb{N}_V}(sync_{\mathbb{N}_V}(\{i\}, v^\sharp))$; since $\gamma_{\mathbb{N}_V}$ is strict, we can conclude that $sync_{\mathbb{N}_V}(\{i\}, v^\sharp) \ne \perp_{\mathbb{N}_V}$; so we can introduce $\bar{v}^\sharp$ such that $C^{\sharp} \stackrel{\lambda}{\rightsquigarrow}_{\mathbb{N}_V} \bar{C}^\sharp$; we now prove that $(u.\lambda, \bar{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathbb{N}_V})(\bar{v}^\sharp)$: we have $\bar{C} = ((C \setminus \{(P_0, id_?, E_?)\} \cup Cont_?)$; so $\Pi_{\mathbb{N}^V}(u.\lambda, \bar{C}) = \Pi_{\mathbb{N}^V}(u, C) - (\delta_v^{P_0})_{v \in V} + \Pi_{\mathbb{N}^V}(\varepsilon, Cont_?) + (\delta_v^{\psi(\lambda)})_{v \in V}$; we deduce from Prop. 38 that $\Pi_{\mathbb{N}^V}(\varepsilon, Cont_?) \in \gamma_{\mathbb{N}_V}(\beta_{\mathbb{N}_V}(P))$; we have already proved $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathbb{N}_V}(sync_{\mathbb{N}_V}(\{i\}, v^\sharp))$; so $\Pi_{\mathbb{N}^V}(u.\lambda, \bar{C}) \in \gamma_{\mathbb{N}_V}(sync_{\mathbb{N}_V}(\{i\}, v^\sharp) - 1_{\mathbb{N}_V}(P_0) + 1_{\mathbb{N}_V}(\psi(\lambda)) + \beta_{\mathbb{N}_V}(P))$; so we can conclude that $(u.\lambda, \bar{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathbb{N}_V})(\bar{v}^\sharp)$;

(5) in the case that $C \stackrel{\lambda}{\rightleftarrows} \bar{C}$ is a spoiled resource replication: there exists one syntactic component $P_0$, such that $P_0$ matches $*y?^i[\bar{y}]P$ such that there exists one thread $(P_0, id_?, E_?)$ in $C$, and several tagged names $c_1, \dots, c_n \in \mathcal{N} \times \mathcal{M}$, a marker $id_* \in \mathcal{M}$, and a continuation $Cont_? \in \beta(P, id_*, E_?)[y_i \mapsto c_i]$ such that $\bar{C}$ is $(C \cup Cont_?)$; we have $(u, C) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathbb{N}_V})(v^\sharp)$; so $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathbb{N}_V}(v^\sharp)$; and since $(P_0, id_?, E_?)$ is a thread of $C$, we have $(\Pi_{\mathbb{N}^V}(u, C))_{P_0} \ge 1$; then $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathbb{N}_V}(sync_{\mathbb{N}_V}(\{i\}, v^\sharp))$; since $\gamma_{\mathbb{N}_V}$ is strict, we can conclude that $sync_{\mathbb{N}_V}(\{i\}, v^\sharp) \ne \perp_{\mathbb{N}_V}$; so we can introduce $\bar{v}^\sharp$ such that $C^{\sharp} \stackrel{\lambda}{\rightsquigarrow}_{\mathbb{N}_V} \bar{C}^\sharp$; we now prove that $(u.\lambda, \bar{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathbb{N}_V})(\bar{v}^\sharp)$: we have $\bar{C} = (C \cup Cont_?)$; so $\Pi_{\mathbb{N}^V}(u.\lambda, \bar{C}) = \Pi_{\mathbb{N}^V}(u, C) + \Pi_{\mathbb{N}^V}(\varepsilon, Cont_?) + (\delta_v^{\psi(\lambda)})_{v \in V}$; we deduce from Prop. 38 that $\Pi_{\mathbb{N}^V}(\varepsilon, Cont_?) \in \gamma_{\mathbb{N}_V}(\beta_{\mathbb{N}_V}(P))$; we also have $\Pi_{\mathbb{N}^V}(u, C) \in \gamma_{\mathbb{N}_V}(sync_{\mathbb{N}_V}(\{i\}, v^\sharp))$; so we can conclude that $\Pi_{\mathbb{N}^V}(u.\lambda, \bar{C}) \in \gamma_{\mathbb{N}_V}(sync_{\mathbb{N}_V}(\{i\}, v^\sharp) + 1_{\mathbb{N}_V}(\psi(\lambda)) + \beta_{\mathbb{N}_V}(P))$; so $(u.\lambda, \bar{C}) \in (\gamma_{\mathbb{N}^V} \circ \gamma_{\mathbb{N}_V})(\bar{v}^\sharp)$. $\square$