Secure refinements of communication channels

Vincent Cheval, Véronique Cortier, Eric Le Morvan

► To cite this version:

Vincent Cheval, Véronique Cortier, Eric Le Morvan. Secure refinements of communication channels. FSTTCS 2015, Dec 2015, Bangalore, India. hal-01238094

HAL Id: hal-01238094

https://inria.hal.science/hal-01238094

Submitted on 4 Dec 2015

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
# Secure refinements of communication channels

Vincent Cheval¹,³, Véronique Cortier², and Eric le Morvan²

1 School of Computing, University of Kent, UK

2 LORIA, CNRS, France

3 LORIA, INRIA, France

## Abstract

It is a common practice to design a protocol (say $Q$) assuming some secure channels. Then the secure channels are implemented using any standard protocol, e.g. TLS. In this paper, we study when such a practice is indeed secure.

We provide a characterization of both confidential and authenticated channels. As an application, we study several protocols of the literature including TLS and BAC protocols. Thanks to our result, we can consider a larger number of sessions when analyzing complex protocols resulting from explicit implementation of the secure channels of some more abstract protocol $Q$.

## 1 Introduction

When designing a protocol, it is common to assume a secure, confidential, or authentic channel. Authentic channels may be read but not written in. Symmetrically, confidential channels may be written in but not read. Secure channels are both authentic and confidential. For example, payment protocols like 3D-secure are supposed to be run over a secure channel such as TLS. Similarly, many services such as public key registration assume an authenticated channel. How to implement these secure channels is left unspecified and, intuitively, the security of a payment protocol should not depend on the particular choice of implementation of its secure channels. A typical example of a popular and generic realization of a secure channel is TLS. For authentication, one usually relies on a password-based authentication or on previously established keys (used e.g. for signature or MACs). Is it safe to use these protocols in any context? What is a secure or authenticated channel? This paper aims at characterizing channels that have security properties. For example, assume $Q$ is a secure protocol (e.g. a payment protocol) that requires a secure channel. Which properties should a protocol $P$ achieve in order to securely realize the secure channels of $Q$? These properties should of course be independent of $Q$ since $P$ and $Q$ are typically designed in totally independent contexts. In the remaining of this introduction, $Q$ will refer to the “main” protocol while $P$ will refer to a protocol realizing secure channels (for several notions of security).

**Our contributions.** Our first contribution is a characterization of both secure, confidential, and authenticated channels. We actually characterize what it means for a channel to be readable or not, and writable or not. Then the realization of a secure channel typically proceeds in two phases. First, some values are established by the protocol $P$, for example short-term symmetric keys or MAC keys. Quite unsurprisingly, we show that these values need to be secret and appropriately shared. Then the messages of $Q$ are transported or encapsulated using the values established by $P$. For example, the messages of $Q$ may be encrypted with a key established by $P$. We provide a characterization of secure encapsulations both for secure, confidential, and authentic channels. A key feature of our characterization is that it is independent of $P$ and $Q$, which allows for a modular analysis. We show that standard encapsulations (e.g. typical use of encryption, signatures, or MACs) enjoy the requested properties.

Our second and main contribution is to show how to securely compose protocols. Intuitively, our main result guarantees that whenever $P$ is a secure key exchange protocol and $\mathcal{E}$ is a secure

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

licensed under Creative Commons License CC-BY

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

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
encapsulation then $P \cdot \mathcal{E} Q$ is as secure as $Q$ where $P \cdot \mathcal{E} Q$ denotes the protocol obtained from $Q$ by
implementing its secure channels using $P$ and $\mathcal{E}$.

The interest of our result is twofolds. First, it provides foundational grounds to a common practice where protocols are typically designed and studied independently and then combined. We show that such a practice is actually secure under reasonably light assumptions: primitives shared between $P$, $\mathcal{E}$, and $Q$ should be tagged as proposed in [4]. Tagging is a standard practice that avoids message confusion. Second, our result provides a technique for analyzing a complex protocol: it is sufficient to analyse its components to deduce security of the whole protocol. To express and prove our result, we have developed a framework, an extension of the applied-pi calculus [2], that allows to easily talk about protocols roles and sessions, a missing aspect in the applied-pi calculus.

To illustrate our approach, we show that TLS is a secure implementation of secure channels. Similarly we show that the BAC protocol [1] is also a secure implementation of a secure channel and may be safely used with the Passive Authentication (PA) protocol as prescribed for the biometric passport [1]. Using the CL-Atse tool [18], we analyse several combined protocols. Thanks to our combination result, it is possible to analyse protocols in isolation instead of their combination, which allows to consider a larger number of sessions.

**Related work.** One seminal work on composition is the one of Guttman and Thayer [13]. They show that two protocols can be composed without one damaging the security of the other as soon as they are “independent”. However, this independence notion needs to be checked for any protocol execution and cannot be statically checked at the protocol specification level. Later, Guttman [11] provides a criterion on the specification of $P$ and $Q$ such that $P$ can be safely composed with $Q$. Intuitively, $Q$ should not break some invariant satisfied by $P$ and conversely. While the work of [11] focuses on authentication and secrecy properties, [12] more generally devises a framework for defining protocol goals and designing, step by step, protocols that fulfill them. In [10], the strand space model is used in a modular way, to analyse protocols components by components. The disjunction criteria cannot be checked statically. All these approaches provide a framework that allows to reason modularly when analysing the combination of two protocols $P$ and $Q$, typically expressing invariants satisfied by $P$ that are shown sufficient to prove security of $Q$. This simplifies the proof of $P$ combined with $Q$ but requires the knowledge of both protocols. Compared to our work, we propose a criteria for a protocol $P$ to securely implement a secure channel, independently of the protocol $Q$ that will use it (provided primitives are tagged).

Under tagging assumptions similar to ours, it was already shown that $P$ and $Q$ can be safely run in parallel even if they share long-term keys [7]. In passing, we generalize this result to the case where long-term keys may be used as payload. [6] explains when two protocols may be used sequentially, with $Q$ using data established by $P$. The main difference with our work is that messages may not be transformed when composing protocols. Therefore, [7, 6] cannot be used to (securely) implement abstract channels. Note also that [6] may not consider compromised sessions, that is sessions between honest and dishonest agents. The problem we address here is referred to as *sequential composition* in [16], where the messages of $Q$ are used as payloads in the composed protocol $P \cdot \mathcal{E} Q$. [16] provides a nice exposition of the generic problem of a protocol $Q$ using a protocol $P$ as sub-protocol and lists sufficient (semantical) conditions for combining two protocols. These conditions require again the knowledge of both $P$ and $Q$.

Datta et al. (e.g. [8]) have also studied secure protocol composition in a broader sense: protocols can be composed in parallel, sequentially or protocols may use other protocols as components. However, they do not provide any syntactic conditions for a protocol $P$ to be safely executed in parallel with other protocols. For any protocol $P'$ that might be executed in parallel, they have to prove that the two protocols $P$ and $P'$ satisfy each other invariants. Their approach is thus rather designed for component based design of protocols.
## 2 Model

Our model is inspired from the applied-pi calculus [2], extended to an explicit notion of roles.

### 2.1 Messages

Messages are modeled using a typed term algebra. We assume an infinite set of names $N = N_D \uplus N_H$ of base type and a set $Ch$ of names of channel type. The set $N_H$ (resp. $N_D$) represents the names accessible by honest (resp. dishonest) agents. We also consider an infinite set of variables $X$ and a finite signature $\mathcal{F}$ of function symbols operating and returning terms of base type. More precisely, we consider $\mathcal{F} = \mathcal{F}_c \uplus \mathcal{F}_{cst} \uplus \mathcal{F}_{key}$ where $\mathcal{F}_{cst}$ contains only constants, all functions in $\mathcal{F}_{key}$ are unary, and $\mathcal{F}_c = \{\langle \rangle/2, f_1/n_1, \dots, f_k/n_k\}$ contains the binary function symbol $\langle \rangle$ used to denote concatenation and other function symbols $f_i$ of arity $n_i$. Terms are defined as names, variables and function symbols applied to other terms. The set of terms built from $N \subseteq N \cup Ch$, $X \subseteq X$ and by applying the function symbols in $\mathcal{F} \subseteq \mathcal{F}$ is denoted by $\mathcal{T}(\mathcal{F}, N \cup X)$. We denote by $st(t)$ the set of subterms of $t$. We denote by $vars(t)$ (resp. $names(t)$) the set of variables (resp. names) in $t$. When $vars(t) = \emptyset$, we say that $t$ is ground. To represent events that may occur during a protocol execution, we assume an infinite signature $\mathcal{E}v$ distinct from $\mathcal{F}$. We say that a term $e(t_1, \dots, t_n)$ with $e \in \mathcal{E}v$ and $t_1, \dots, t_n \in \mathcal{T}(\mathcal{F}, N \cup X)$ is an event.

**Example 1.** A standard signature to represent encryption and signature is $\mathcal{F}_{std}$, the signature built from a finite set of constants, functions $\mathcal{F}_{std} = \{\text{senc}/2, \text{aenc}/2, \text{sign}/2, \text{h}/1, \langle\rangle/2\}$ and $\mathcal{F}_{kstd} = \{\text{pk}/1, \text{vk}/1\}$. The function symbol senc (resp. aenc) represents the symmetric (resp. asymmetric) encryption. We denote by pk(s) the public key associated s. The function symbol sign represents the digital signature where vk(s) is the verification associated to s. We write $\langle u, v \rangle$ as syntactic sugar for $\langle\rangle(u, v)$.

We model the algebraic properties of the cryptographic primitives by a set of inference rules $\mathcal{I}$ composed of composition and decomposition rule described as follows:

$$ \frac{x_1 \quad \dots \quad x_k}{f(x_1, \dots, x_k)} \text{ f-comp} \quad \frac{\langle x_1, x_2 \rangle}{x_1} \quad \frac{\langle x_1, x_2 \rangle}{x_2} \quad \frac{f(x, u_1, \dots, u_n)}{x} \quad \frac{v_1 \quad \dots \quad v_m}{x} \text{ f-decomp} $$

where for all $j \in \{1, \dots, n\}$, for all $k \in \{1, \dots, m\}$, $u_j, v_k \in \mathcal{T}(\mathcal{F}_{key}, X)$ and $vars(v_1, \dots, v_k) \subseteq \{u_1, \dots, u_n, x\}$. For each $f \in \mathcal{F}$, the set $\mathcal{I}$ contains a unique f-comp rule and there is no f-decomp rule when $f \in \mathcal{F}_{key}$. Given a set or sequence of terms $S$ and a term $t$, the deducibility relation is inductively defined as follows. The term $t$ is deducible from $S$, denoted $S \vdash t$, when $t \in S \cup \mathcal{F}_{cst} \cup N_D$ or there exists a substitution $\sigma$ and an inference rule in $\mathcal{I}$ with premises $u_1, \dots, u_n$ and conclusion $u$ such that $t = u\sigma$ and for all $i \in \{1, \dots, n\}$, $S \vdash u_i\sigma$.

**Example 2.** Continuing Example 1, we define the set $\mathcal{I}_{std}$ of decomposition rules as follows.

$$ \frac{\text{senc}(x, y)}{x} \quad \frac{y}{x} \quad \frac{\text{aenc}(x, \text{pk}(y))}{x} \quad \frac{y}{x} \quad \frac{\text{sign}(x, y)}{x} \quad \frac{\text{vk}(y)}{x} \quad \frac{\langle x, y \rangle}{x} \quad \frac{\langle x, y \rangle}{y} $$

We have that $\text{senc}(\langle a, c \rangle, k), k \vdash a$ but $\text{aenc}(\langle a, c \rangle, \text{pk}(k)), \text{pk}(k) \nvdash a$.

### 2.2 Agents

In standard process algebra (e.g. [2]), the notion of agents is usually implicit. Typically, a process that models the behavior of the different honest agents is a single process where all agents are implicitly represented. However, to model protocol composition, we need to explain how to compose each role and thus we need to talk about each agent separately. Therefore, we explicit the presence of agents
4 Secure refinements of communication channels

in our model. Interestingly, our model may also be used to specify semi-honest agents which may
directly communicate with the attacker during the protocol execution, still hiding some secrets from
him. We consider an infinite set of agents $\mathcal{A}_{gt} = \{A, B, \dots\} = \mathcal{A}_{gt_H} \uplus \mathcal{A}_{gt_D}$ where $\mathcal{A}_{gt_H}$ and $\mathcal{A}_{gt_D}$
represent respectively honest and dishonest agents. Each agent possesses private data such as keys.
Therefore, we consider $\mathcal{N}_{\mathcal{A}_{gt}}$ a subset of $\mathcal{N}$ as an infinite partition $\mathcal{N}_{\mathcal{A}_{gt}} = \uplus_{A \in \mathcal{A}_{gt}} \mathcal{N}_A$ where $\mathcal{N}_A$
intuitively are the names accessible by the agent $A$. By convention, $k[A]$ denotes a name in $\mathcal{N}_A$.

2.3 Protocols

In the spirit of [2], we model protocols through a process algebra. We represent explicitly confiden-
tial, secure, and authenticated channels. Formally, we partition the set of channels into three infinite
sets $Ch = Ch_a \uplus Ch_c \uplus Ch_s \uplus Ch_p$ where $Ch_a, Ch_c, Ch_s, Ch_p$ respectively represent the sets of authen-
ticated, confidential, secure and public channels. The syntax of our calculus is as follows:

Roles of agent A

$$
R_A, R'_A := 0 \mid \mathrm{out}_A(c, u).R_A \mid \mathrm{in}_A(c, v).R_A \mid \mathrm{new} \ k.R_A \mid \mathrm{event}_A(ev).R_A
$$

Channel and agent declarations

$$
C, C' := R_A \mid new_{ta} c.C \mid C \mid C'
$$

Processes

$$
P, Q := C \mid P \mid Q \mid !P \mid \mathbf{ag}(A, \mathcal{A}, \mathcal{K}_{pub}, \mathcal{K}_{prv}).P
$$

where $c \in Ch$, $A \in \mathcal{A}_{gt}$, $ta$ is the tuple of agents in $C$ such that $c$ occurs in their role, $k$ is name, $u$ and $v$ are terms, $ev$ is an event, $\mathcal{K}_{pub}$ and $\mathcal{K}_{prv}$ are sets of ground terms with $\mathit{names}(\mathcal{K}_{pub}) \subseteq \mathcal{N}_A$, $\mathit{names}(\mathcal{K}_{prv}) \subseteq \mathcal{N}_{\mathcal{A}_{gt}}$ and $\mathcal{A} \subseteq \mathcal{A}_{gt}$.

The behavior of an agent A is described in a role $R_A$ that consists of a sequence of inputs, outputs, creations of names and emissions of events. The role $out_A(c, u).R_A$ outputs the term $u$ on the channel $c$ and then behaves like $R_A$. The role $in_A(c, v).R_A$ inputs a message from channel $c$ and expects it to be an instance of $v$. The role $new \ k.R_A$ generates a fresh name $k$. Processes express how the roles of different agents are combined. The process $new_{ta} c$ allocates an abstract channel to the agents in $ta$. The process $P \mid Q$ expresses the parallel execution of $P$ and $Q$. The process $!P$ represents the replication of $P$. The process $ag(A, \mathcal{A}, \mathcal{K}_{pub}, \mathcal{K}_{prv}).P$ selects a new agent $A$ amongst $\mathcal{A}$. The set $\mathcal{K}_{pub}$ typically indicates the public keys of $A$ while $\mathcal{K}_{prv}$ contains the (secret) long term keys known by $A$. The variables in a role are uniquely bound by the first input in which they appear. The channels are bound by the operators new . The agents in a process are also bound by agent creation. In a protocol, we assume that a name or variable is syntactically bound only once. A variable (resp. agent, channel) that is not bound in $P$ is free. We denote by $fa(P)$, $ba(P)$, $fv(P)$, $bv(P)$, $fn(P)$ and $bn(P)$ the sets of free and bound agents, variables and names in $P$ respectively. We say that $P$ is closed when $fv(P) = \emptyset$. Given a process $P$ and an agent $A$, we denote by $\mathit{names}_A(P)$ and $ch_A(P)$ the sets of names, channels that occur in the roles of $A$ in $P$.

A role is executable if it only outputs terms that may be deduced from its inputs, the generated
values (nonces and keys), and the long-term keys used in the role.

► **Definition 3.** Let $R_A = r_1 \dots r_n$ be a role of an agent $A$. We say that $R_A$ is *executable* when for all $i \in \{1, \dots, n\}$, if $r_i = \text{out}_A(c, u)$ then $\text{names}(r_1, \dots, r_i) \cup S \vdash u$ where $S = \{v \mid j < i \wedge (r_j = \text{in}_A(d, v) \lor r_j = \text{new } v)\}$. A process $P$ is executable when all the roles in $P$ are executable.

The state of a protocol during its execution is represented by a configuration $(P, \Phi, \mu, \theta)$ where $P$
is a closed process, $\Phi$ is a sequence of ground terms representing the knowledge of the attacker, $\mu$ is
a mapping from channels to sets of terms representing the messages sent over non-public channels
and $\theta$ is a mapping from triplets of channel, agent, tuple of agents to sets of channels. The semantics
$$ (P | \text{out}_A(c, u).R_A, \Phi, \mu, \theta) \rightarrow (P | R_A, \Phi', \mu', \theta) \quad \text{where } \Phi' = \Phi \text{ if } c \in Ch_c \cup Ch_s \\ \text{else } \Phi' = \Phi \cdot [u] \text{ and } \mu' = \text{rect}(c, u, \mu) \text{ if } c \notin Ch_p \text{ else } \mu' = \mu \quad \text{OUT} $$

$$ (P | \text{in}_A(c, v).R_A, \Phi, \mu, \theta) \rightarrow (P | R_A \sigma, \Phi, \mu, \theta) \quad \text{if there exists } \sigma \text{ such that} \\ \text{dom}(\sigma) = \text{vars}(v) \text{ and either } v \sigma \in c \mu \text{ or else } c \in Ch_p \cup Ch_c \text{ and } \Phi \vdash v \sigma \quad \text{IN} $$

$$ (P | \text{new } k.R_A, \Phi, \mu, \theta) \rightarrow (P | R_A \{k' / k\}, \Phi, \mu, \theta) \quad \text{NEW-K} \\ \text{with } k' \text{ fresh in } N_H \text{ if } A \in \mathcal{A}gt_H \text{ else } k' \in N_D $$

$$ (P | \text{new}_{ta} c.C[R_{A_1}, \dots, R_{A_n}], \Phi, \mu, \theta) \rightarrow (P | [R'_{A_1}, \dots, R'_{A_n}], \Phi, \mu, \theta') \quad \text{NEW-C} \\ \forall i, R'_{A_i} = R_{A_i} \text{ if } c \notin ch(R_{A_i}) \text{ else } R'_{A_i} = R_{A_i} \{c_{A_i} / c\} \text{ with } c_{A_i} \in Ch_p \text{ if } ta \cap \mathcal{A}gt_D \neq \emptyset \text{ else} \\ c_{A_i} \in S \cup \bigcup_{B \in ta} \theta(c, B, ta) \setminus \theta(c, A_i, ta) \text{ and } S \subseteq Ch_a \text{ fresh (resp. } Ch_c, Ch_s) \text{ if } c \in Ch_a \\ (\text{resp. } Ch_c, Ch_s). \text{ Moreover, } \theta = \theta' \text{ if } ta \cap \mathcal{A}gt_D \neq \emptyset \text{ else } \theta' = \text{recc}((c_A, A)_{A \in ta}, ta, c, \theta). $$

$$ (P | !Q, \Phi, \mu, \theta) \rightarrow (P | !Q | Q\rho, \Phi, \mu, \theta) \quad \text{with } \rho \text{ a fresh renaming of } \text{vars}(Q) \quad \text{REPL} $$

$$ (P | \text{event}_A(ev).R, \Phi, \mu, \theta) \xrightarrow{ev} (P | R, \Phi, \mu, \theta) \quad \text{EVENT} $$

$$ (P | \text{ag}(A, \mathcal{A}, \mathcal{K}_{pub}, \mathcal{K}_{prv}).Q, \Phi, \mu, \theta) \rightarrow (P | Q\sigma, \Phi \cdot S, \mu, \theta) \quad \text{AGENT} \\ \text{with } \sigma = \{A' / A\}, A' \notin fa(Q), S = \mathcal{K}_{pub}\sigma \text{ if } A' \in \mathcal{A} \cap \mathcal{A}gt_H \text{ else } S = \mathcal{K}_{pub}\sigma \cdot \mathcal{K}_{prv}\sigma $$

<caption>Figure 1 Semantics of configuration</caption>

is given in Figure 1. The rule OUT indicates that the attacker obtains messages on public or authenticated channels. In this rule, rect(c, t, μ) is the mapping μ' where t was recorded as being sent over c. Formally, μ'(c') = μ(c') for any c' ≠ c and μ'(c) = μ(c) ∪ {t}. With rule IN the attacker can inject on c any message that he can deduce from his knowledge when c is a public or confidential channel. He can also relay any message that was previously sent on c. The rule NEW-K generates a fresh name of N_H or N_D depending on whether the agent A is honest or not. The rule NEW-C allocates to the role of an agent a channel possibly fresh or that has already been used by other roles in different sessions. In this rule, recc(S, ta, c, θ) is the mapping θ in which we record the channels allocated to the agents. Formally, θ'(c', A', ta') = θ(c', A', ta') for any A' /∈ ta' or (c', ta') ≠ (c, ta), and θ'(c, A, ta) = θ(c, A, ta) ∪ {d} for any (d, A) ∈ S. The rule AGENT selects an agent from A and adds Kpub to the knowledge of the attacker. Additionally, if the agent is dishonest, the rules adds Kprv. When (P, Φ, μ, θ) e1 → ... → eN → (P', Φ', μ', θ'), we write (P, Φ, μ, θ) e1...eN ⇄ (P', Φ', μ', θ').

**► Example 4.** An electronic passport is a paper passport containing a RFID chip that stores most of the information printed on the passport. The protocols used to access these private data are specified in the International Civil Aviation Organization standard [1]. Before exchanging any private data, an electronic passport and a reader must establish session keys through a key-exchange protocol, called Basic Access Control (BAC), that prevents eavesdropping on further communication. The BAC protocol relies on two keys ke and km that are printed on the passport and thus can be obtained by the reader through optical scanning. We described below the BAC protocol, between a passport (P) and a reader (R). We assume encrypted messages to be tagged with a. The use of tagging will be explained later on.

$$ R \rightarrow P : \text{challenge} $$

$$ P \rightarrow R : n_P $$

$$ R \rightarrow P : \langle \text{senc}(\langle a, n_R, n_P, k_R \rangle, ke), \text{mac}(\langle a, \text{senc}(\langle a, n_R, n_P, k_R \rangle, ke) \rangle, km) \rangle $$

$$ P \rightarrow R : \langle \text{senc}(\langle a, n_P, n_R, k_P \rangle, ke), \text{mac}(\langle a, \text{senc}(\langle a, n_P, n_R, k_P \rangle, ke) \rangle, km) \rangle $$

After receiving a challenge command from the reader, the passport generates a fresh name $n_P$ that
will be used to verify the authenticity of the messages he will receive later on. Upon receiving $n_P$, the reader generates two nonces $n_R$, $k_R$ and sends back to the passport all three nonces encrypted with the key $k_e$ and a mac with the key $k_m$. The nonce $n_R$ has also an authenticity purpose whereas $k_R$ will be the reader's contribution to the session keys. The passport then checks the mac using $k_m$ and the cipher by decrypting it using $k_e$ and verifying the presence of $n_P$ in the plain text. If all verifications succeed, the passport generates a nonce $k_P$, the passport's contribution to the session keys, and sends it to the reader. At the end of the protocol, both reader and passport know $k_R$ and $k_P$ that they use to generate two session keys $f_1(k_R, k_P)$ and $f_2(k_R, k_P)$. In our syntax, the roles of the reader ($R_R$) and of the passport ($R_P$) can be expressed as follows.

$$R_P = \begin{aligned} & \text{in}_P(c, \text{challenge}).\text{new } n_P.\text{out}_P(c, n_P).\text{in}_P(c, \langle M, \text{mac}(\langle a, M \rangle, km[P]) \rangle). \\ & \quad \text{new } k_P.\text{out}_P(c, \langle N, \text{mac}(\langle a, N \rangle, km[P]) \rangle).0 \end{aligned}$$

$$R_R = \begin{aligned} & \text{out}_R(c, \text{challenge}).\text{in}_R(c, z).\text{new } k_R.\text{new } n_R.\text{out}_R(c, \langle U, \text{mac}(\langle a, U \rangle, km[P]) \rangle). \\ & \quad \text{in}_R(c, \langle V, \text{mac}(\langle a, V \rangle, km[P]) \rangle).0 \end{aligned}$$

with $c \in Ch_p$, $M = \text{senc}(\langle a, x, n_P, y \rangle, ke[P])$, $N = \text{senc}(\langle a, n_P, x, k_P \rangle, ke[P])$, $U = \text{senc}(\langle a, n_R, z, k_R \rangle, ke[P])$ and $V = \text{senc}(\langle a, z, n_R, w \rangle, ke[P])$. An honest reader communicating with unbounded number of passports, possibly dishonest, can be modeled in our calculus as the process:

$$BAC = \text{ag}(R, \{R\}, \emptyset, \emptyset).!\text{ag}(P, \mathcal{P}, \emptyset, \{ke[P], km[P]\}).(R_P | R_R)$$

where $\mathcal{P}$ is an infinite set of agents containing honest and dishonest agents and $R \notin \mathcal{P}$. The following trace would correspond to the execution of a session with a dishonest passport $l$ and a session of an honest one $A$ both in $\mathcal{P}$.

$$\begin{aligned} (BAC, \emptyset, \emptyset, \emptyset) & \to^* (BAC \mid \text{ag}(P, \mathcal{P}, \emptyset, \{ke[P], km[P]\}).(R_P | R_R), \emptyset, \emptyset, \emptyset) \\ & \to (BAC \mid R_P \sigma_A \mid R_R \sigma_A, \emptyset, \emptyset, \emptyset) \\ & \to^* (BAC \mid R_P \sigma_A \mid R_R \sigma_A \mid R_P \sigma_I \mid R_R \sigma_I, [ke[l], km[l]], \emptyset, \emptyset) \\ & \to (BAC \mid R_P \sigma_A \mid R_R \sigma_A \mid R_P \sigma_I \mid Q, [ke[l], km[l], \text{challenge}], \emptyset, \emptyset) \\ & \to^* \dots \end{aligned}$$

where $P\sigma_A = A$, $P\sigma_I = l$ and $\sigma_A, \sigma_I$ also are fresh renaming of bound variables and names and $R_R\sigma_I = \text{out}_I(c, \text{challenge}).Q$. By convention the empty mapping $\mu = \emptyset$ (resp. $\theta = \emptyset$) denotes the mapping that maps any argument to the emptyset: $\mu(c) = \emptyset$ (resp. $\theta(c, A, ta) = \emptyset$) for any $c, A, ta$.

# 3 Composition

In the previous section, we have defined an abstract notion of confidential, secure, and authenticated channels. In practice, such channels are realized through cryptographic means. Agents first execute some key establishment protocol in order to generate secret session keys. Then they encapsulate the messages supposedly sent over a channel using these session keys. A standard case for secure channels consists in using session keys to encrypt subsequent messages. How to encrypt the message is defined by the encapsulation. In Section 3.1, we provide a generic definition of encapsulations and identify properties needed for encapsulations to allow for authentication, confidential, and secure channels. We continue in Section 3.2 by characterizing the composition of a key establishment protocol with a process using abstract channels.

## 3.1 Encapsulation

For our composition result, we tag encapsulations and processes. These tags are used to distinguish the parts of a message that correspond to encapsulations from the ones coming from processes. Formally, a tag is a constant from $\mathcal{F}_{\text{cst}}$, hence known to the attacker. Given a set $\text{Tag} \subseteq \mathcal{F}_{\text{cst}}$, we say that a term $t$ is a Tag-term when for all $t' \in st(t)$, if $t' = f(t_1, \dots, t_n)$ for some $f \in \mathcal{F}_c\setminus\{\langle \rangle\}$ and some
terms $t_1, \dots, t_n$ then $t_1 = \langle a, u \rangle$ for some term $u$ and $a \in \text{Tag}$.

**► Definition 5.** A Tag-encapsulation is a pair $(\mathcal{E}, \mathcal{F})$ where $\mathcal{E}$ is a Tag-term of $\mathcal{T}(\mathcal{F}, \mathcal{X})$ and $\mathcal{F} \subseteq \mathcal{T}(\mathcal{F}_{\mathcal{key}}, \mathcal{X})$ such that $\text{vars}(\mathcal{E}) = \{x, x_1, \dots, x_n\}, \{\mathcal{E}, x_1, \dots, x_n\} \vdash \mathcal{X}$ and for all $t \in \text{st}(\mathcal{E})$,

- if $t = f(v)$ with $f \in \mathcal{F}_{\mathcal{key}}$ then $v \in \{x_1, \dots, x_n\} \cup \mathcal{F}_{\text{cst}}$

- if $t = f(w, t_1, \dots, t_n)$ and there exists a $f$-decomposition rule with $f(x, u_1, \dots, u_n), v_1, \dots, v_m$ as premises then for all $j \in \{1, \dots, m\}$, for all $i \in \{1, \dots, n\}$, $v_j = g(y)$ and $y \in \text{vars}(u_i)$ implies $t_i \in \{x_1, \dots, x_n\} \cup \mathcal{F}_{\text{cst}}$. Intuitively, if a $f$-decomposition rule may be applied to a subterm of an encapsulation using a non atomic key $g(t_i)$ then $t_i$ must be a variable or a constant.

We denote $x$ by $t_{\mathcal{E}}$ and $(x_1, \dots, x_n)$ by $X_{\mathcal{E}}$. Given two encapsulations $(\mathcal{E}, \mathcal{F})$ and $(\mathcal{E}', \mathcal{F}')$, we write $\mathcal{E} \sim \mathcal{E}'$ when there exists a renaming $\rho$ such that $\mathcal{E}\rho = \mathcal{E}'$, $\mathcal{F}\rho = \mathcal{F}'$, $t_{\mathcal{E}}\rho = t_{\mathcal{E}'}$ and $X_{\mathcal{E}}\rho = X_{\mathcal{E}'}$. We denote by $\mathcal{E}(t, t_1, \dots, t_n)$ the term obtained from $\mathcal{E}$ by substituting $x$ by $t$ and $x_i$ by $t_i$.

In an encapsulation $(\mathcal{E}, \mathcal{F})$, the variable $t_{\mathcal{E}}$ will be instantiated by the message sent on the channel implemented by the encapsulation whereas the variables in $X_{\mathcal{E}}$ will be instantiated by the session keys. Note that $\{\mathcal{E}, x_1, \dots, x_n\} \vdash \mathcal{X}$ indicates that an encapsulated messages may always be retrieved using the session keys. The terms in $\mathcal{F}$ represent the public keys that can be used to deduce the term encapsulated or to generate an encapsulation with a new message without revealing the session keys.

**► Example 6.** In Example 4, we described how the session keys $f_1(k_R, k_P)$ and $f_2(k_R, k_P)$ are established in the BAC protocol. The ICAO standard states that in any other protocol executed after BAC, the messages exchanged should be of the form $\langle u, \text{mac}(\langle b, u \rangle, f_1(k_R, k_P)) \rangle$ with $u = \text{senc}(\langle b, M \rangle, f_2(k_R, k_P))$ for some data $M$ and tag $b$. This represents in fact the encapsulation of $M$ with the session keys $f_1(k_R, k_P)$ and $f_2(k_R, k_P)$. In our formalism, the encapsulation is defined as $(\mathcal{E}_{\text{BAC}}, \emptyset)$ where $\mathcal{E}_{\text{BAC}} = \langle t, \text{mac}(\langle b, t \rangle, x_2) \rangle$ with $t = \text{senc}(\langle b, x \rangle, x_1)$, $t_{\mathcal{E}_{\text{BAC}}} = x$ and $X_{\mathcal{E}_{\text{BAC}}} = (x_1, x_2)$.

We use tags to distinguish the encapsulations from the messages actually sent over the network. However, a process can implement different types of channels using different encapsulations with the same tags. We need to ensure that the security of an encapsulation is not compromised when used with other encapsulations. Therefore, to state the different properties that encapsulations must satisfy, we consider a set of encapsulations and not only a unique one.

These conditions are easily met by standard encapsulations.

**► Definition 7.** Let $S_e = S_a \mathbin{\triangleright} S_c \mathbin{\triangleright} S_s$ be a set of Tag-encapsulations. We say that $S_e$ allows authentic, confidential and secure channels if the following properties are satisfied: Let $(\mathcal{E}_1, F_1), \dots, (\mathcal{E}_n, F_n) \in S_e$. Assume that the variables in $\mathcal{E}_1, \dots, \mathcal{E}_n$ are disjoint. Let $\sigma$ be a ground substitution such that $\text{dom}(\sigma) = \text{vars}(\mathcal{E}_1, \dots, \mathcal{E}_n)$ and let $\Phi$ be a ground frame such that $\text{Tag} \cap \text{st}(\sigma, \Phi) = \emptyset$. Let $I$ be the set of $i \in \{1, \dots, n\}$ such that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash t_{\mathcal{E}_i} \sigma$.

1. For all $i \in \{1, \dots, n\}, \forall u \in \mathcal{T}(\mathcal{F}_{\mathcal{key}}, X_{\mathcal{E}_i} \sigma)$, if $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash u$ then $\Phi \cdot [t_{\mathcal{E}_k} \sigma]_{k \in I} \vdash u$.

2. For all $i, i' \in \{1, \dots, n\}, \forall u \in \text{st}(\mathcal{E}_i) \setminus X, \forall v \in \text{st}(\mathcal{E}_{i'}) \setminus X$, if $u$ and $v$ are unifiable and $\text{root}(u) \neq \{\langle \rangle\}$ then $\text{img}(\text{mgu}(u, v)) \subset X$.

Moreover, an encapsulation is *authentic*, that is $(\mathcal{E}_i, F_i) \in S_a$ if it satisfies the properties **[Can read]** and **[Cannot write]**. An encapsulation is *confidential*, that is $(\mathcal{E}_i, F_i) \in S_c$ if it satisfies the properties **[Cannot read]** and **[Can write]**. Finally, an encapsulation is *secure*, that is $(\mathcal{E}_i, F_i) \in S_c$ if it satisfies the properties **[Cannot read]** and **[Cannot write]**.

For all ground substitution $\sigma'$ such that $\text{Tag} \cap \text{st}(\sigma') = \emptyset$, if we denote $J = I - i$ then

3. **[Can read]** $[\mathcal{E}_i] \vdash F_i \vdash t_{\mathcal{E}_i}$

4. **[Cannot read]** $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash t_{\mathcal{E}_i} \sigma$ implies $\Phi \cdot [t_{\mathcal{E}_k} \sigma]_{k \in J} \vdash t_{\mathcal{E}_i} \sigma \lor \exists x \in X_{\mathcal{E}_i} \cdot \Phi \cdot [t_{\mathcal{E}_k} \sigma]_{k \in J} \vdash x \sigma$
5. [Can write] $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash \mathcal{E}_i \sigma'$ is equivalent to $\varphi \lor (\Phi \cdot [t_{\mathcal{E}_k} \sigma]_{k \in I} \vdash t_{\mathcal{E}_i} \sigma' \land \Phi \cdot [t_{\mathcal{E}_k} \sigma]_{k \in I} \vdash F_i \sigma')$

6. [Cannot write] $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash \mathcal{E}_i \sigma'$ implies either $\varphi$ or the following property:

$$ \exists x \in \mathcal{X}_{\mathcal{E}_i} . \Phi' \vdash x \sigma' \land ((\exists j \in N . t_{\mathcal{E}_i} \sigma' = t_{\mathcal{E}_j} \sigma \land \mathcal{X}_{\mathcal{E}_i} \sigma' \cap \mathcal{X}_{\mathcal{E}_j} \sigma \neq \emptyset) \lor \Phi' \vdash t_{\mathcal{E}_i} \sigma') $$

where $\varphi = \exists j \in N.(\mathcal{E}_i \sim \mathcal{E}_j \land \mathcal{E}_i \sigma' = \mathcal{E}_j \sigma)$, $N = \{1, \dots, n\}$ and $\Phi' = \Phi \cdot [t_{\mathcal{E}_k} \sigma]_{k \in I}$.

The set $S_a$ (resp. $S_c$, $S_s$) represents the sets of encapsulations that can be used to implement authentic (resp. confidential, secure) channels. Property 1 indicates that the session keys or their associated public keys cannot be retrieved directly from an encapsulation. Different encapsulations may use for instance the same encryption scheme. However, Property 2 prevents a part of an encapsulation to be mistaken as session key for another encapsulation. Properties 3 to 6 model the access control of an encapsulation. In particular, the term $t_E$ of an encapsulation allowing reading access can be derived from the encapsulation $\mathcal{E}$ and its public keys $F$ (Property 3). On the other hand, the term $t_E$ of an encapsulation not allowing reading access should not be derived from the encapsulation without knowing the session keys $\mathcal{X}_E$ (Property 4). Property 5 indicates that an encapsulation allowing writing access can be deduced only if it was already sent on the network (expressed by formula $\varphi$) or by generating it from its public keys $F$ and the term $t_E$ encapsulated. Lastly, Property 6 models that an encapsulation not allowing writing access cannot be generated by an attacker unless already given or unless some of the session keys in $\mathcal{X}_E$ are known. In the latter, Property 6 also states that when the term $t_E$ is not known to the attacker then he must have extracted it from encapsulations previously received.

Most common encapsulations satisfy the requested properties.

**▶ Theorem 8.** *The following encapsulations are:*

**authentic:** $\mathcal{E}_{\text{sign}} = \text{sign}(\langle a_{\mathcal{E}_{\text{sign}}}, x \rangle, x_1)$ and $\mathcal{E}_{\text{mac}} = \langle x, h(\langle a_{\mathcal{E}_{\text{mac}}}, x, x_1 \rangle) \rangle$;

**confidential:** $\mathcal{E}_{\text{aenc}} = \text{aenc}(\langle a_{\mathcal{E}_{\text{aenc}}}, x \rangle, \text{pk}(x_1))$;

**secure:** $\mathcal{E}_{\text{TLS}} = \text{senc}(\langle a_{\mathcal{E}_{\text{TLS}}}, x \rangle, x_1)$, $\mathcal{E}_{\text{BAC}} = \langle t, \text{mac}(\langle a_{\mathcal{E}_{\text{BAC}}}, t \rangle, x_2) \rangle$ with $t = \text{senc}(\langle a_{\mathcal{E}_{\text{BAC}}}, x \rangle, x_1)$, and $\mathcal{E}_{\text{signcrypt}} = \text{sign}(\langle a_{\mathcal{E}_{\text{signcrypt}}}, a_{\text{enc}}(\langle a_{\mathcal{E}_{\text{signcrypt}}}, x \rangle, \text{pk}(x_1)) \rangle, x_2)$.

where $a_{\mathcal{E}_{\text{sign}}}, a_{\mathcal{E}_{\text{mac}}}, a_{\mathcal{E}_{\text{aenc}}}, a_{\mathcal{E}_{\text{TLS}}}, a_{\mathcal{E}_{\text{BAC}}}, a_{\mathcal{E}_{\text{signcrypt}}}$ are constants.

Moreover, the set $\{(\mathcal{E}_{\text{sign}}, \{\text{vk}(x_1)\}), (\mathcal{E}_{\text{mac}}, \emptyset), (\mathcal{E}_{\text{aenc}}, \{\text{pk}(x_1)\}), (\mathcal{E}_{\text{TLS}}, \emptyset), (\mathcal{E}_{\text{BAC}}, \emptyset), (\mathcal{E}_{\text{signcrypt}}, \emptyset)\}$ allows for authentic, confidential and secure channels.

The proof of Theorem 8 is available in Appendix B. In the rest of this paper, we assume the existence of a set of encapsulations $S_e$ allowing authentic, secure and confidential channels.

## 3.2 Composition of protocols

Encapsulations use session keys, which are established by a key exchange protocol. To express the requested property of this protocol, we need to annotate it with events that specify which keys are established for which channels and agents. Considering a context of channel and agent declarations $C$ and a set of channels $S$, we denote by $C|_S$ the context $C$ where all new$_{ta}$ $c$ with $c \in S$ are removed. We denote by $T_{\mathcal{A}_{gt}}$ the set of tuples of agents. We consider special events $\mathcal{Ev} = \{\mathcal{ev}_1, \mathcal{ev}_2, \dots \in \mathcal{Ev}\}$.

**Definition 9.** Let $P = C[R_1, \dots, R_n]$ be a process with $C$ an agent and channel declaration context such that $R_1, \dots, R_n$ are roles of agents $A_1, \dots, A_n$ respectively. Let $S$ be a set of channels such that channels($C$) $\cap S = \emptyset$. Let $\rho$ be a mapping from $S$ to $T_{\mathcal{A}_{gt}} \times S_e$. We say that a process $\tilde{P}$ is an annotation of $P$ under $\rho$ if $\tilde{P} = C[R'_1, \dots, R'_n]$ where for all $i \in \{1, \dots, n\}$,

$$ R'_{i} = R_{i} \cdot \text{event}_{A_{i}}(\text{ev}_{i}(c_{1}, ta_{1}, ts_{1}, tp_{1})). \dots \cdot \text{event}_{A_{i}}(\text{ev}_{i}(c_{m}, ta_{m}, ts_{m}, tp_{m})) $$

where $\{c_1, \dots, c_m\} = \{c \in \text{dom}(\rho) \mid c\rho = (ta, (\mathcal{E}, F)) \land A_i \in \text{st}(ta)\}$ and $\forall j \in \{1, \dots, m\}, c_j\rho = (ta_j, (\mathcal{E}, F)), ts_j = (u_1, \dots, u_{|\mathcal{X}_E|}), tp = F(u_1, \dots, u_{|\mathcal{X}_E|})$ for some $(\mathcal{E}, F)$ and terms $u_1, \dots, u_{|\mathcal{X}_E|}$ such that if $c \in Ch_a$ (resp. $Ch_c, Ch_s$) then $(\mathcal{E}, F)$ allows authentic (resp. confidential, secure) channels.
At the end of each role $R_i$, we add the events $ev_i$ for the channels $c_1, \dots, c_m$ that the agent is supposed to establish. Events $ev_i(c, ta, ts, tp)$ are composed of four elements: a channel $c$ that the agent wants to instantiate, a tuple of agents $ta$ indicating who is sharing the channel $c$, a tuple of session keys $ts$ that will be used in the encapsulation $(\mathcal{E}, \mathcal{F})$ to implement $c$, and lastly a tuple $tp$ of public keys associated to the session keys and $\mathcal{F}$. Typically, we will require that the session keys in $ts$ remain secret for honest agents while the public keys are indeed public.

**► Example 10.** Continuing Example 4 and thanks to Theorem 8, the encapsulation $(\mathcal{E}_{BAC}, \emptyset)$ provides the passport and reader with a secure channel, denoted $c_s \in Ch_s$, once BAC has been executed. The fact that BAC is supposed to establish a secure channel for $P$ and $R$ is expressed by the mapping $\rho = \{c_s \to ((P, R), (\mathcal{E}, \emptyset))\}$. The corresponding annotation of BAC under $\rho$ is as follows:

$$ B\tilde{A}C = C_{BAC}[R_P event_P(ev_1(c_s, (P, R), (f_1(y, k_P), f_2(y, k_P)))) | R_R event_R(ev_2(c_s, (P, R), (f_1(k_R, w), f_2(k_R, w))))] $$

where $C_{BAC}[\_] = ag(R, \{R\}, \emptyset, \emptyset).!ag(P, \mathcal{P}, \emptyset, \{ke[P], km[P], data[P]\}).$. Note that the session keys are different and reflect the respective views on the session keys of the passport and the reader.

**► Definition 11.** Let $C$ and $C'$ be two channel and agent declaration contexts. We say that $C$ and $C'$ are composable if there exist contexts $C_1, C_2, C'_1, C'_2$ such that $C_1$ and $C'_1$ are sequences of agent declarations with $ba(C_1) \cap ba(C'_1) = \emptyset$, $C = C_1[C_2]$, $C'_1 = C'_1[C'_2]$ and $C_2, C'_2$ only differ from the content of $K_{pub}, K_{prv}$ in the instances of $ag(A, A, K_{pub}, K_{prv})$.

We define their composition, denoted $C^{C,C'}$, as the context $C_1[C'_1[C_3]]$ with $C_3$ being the context $C_2$ where all instances of $ag(A, A, K_{pub}, K_{prv})$ are replaced by $ag(A, A, K_{pub} \cup K_{pub'}, K_{prv} \cup K_{prv'})$ and $ag(A, A, K_{pub'}, K_{prv'})$ is in $C'_2$.

The composability of the channel and agent declaration contexts ensures that the roles of the process $Q$ can be sequentially composed with the roles of the process $P$. For instance, they should have similar replications, agent declarations or even channel declarations. However, we do not require that an agent in $P$ and $Q$ to have the same private $(K_{prv})$ or public $(K_{pub})$ data. We also allow an agent to be declared in one context but not in the other one if declared upfront.

**► Example 12.** One of the protocols that are executed after BAC is the Passive Authentication protocol which provides an authentication mechanism proving that the content of the RFID chip is authentic. In fact the ICAO standard also indicates that the chip must contain a signature by the Document Signer authority (D) of a hash of the private data $data[P]$, $sod \stackrel{def}{=} \text{sign}(\langle a, h(\langle a, data[P] \rangle)\rangle, sk[D])$. During the Passive Authentication protocol, after receiving on the secure channel a challenge from the reader, the passport sends back this signature that is checked by the reader.

$R \to_{sec} P : \text{read}$

$P \to_{sec} R : \langle data, \text{sign}(\langle a, h(\langle a, data \rangle)\rangle, sk) \rangle$

where $sk$ is the signing key of the Document Signer authority. In our calculus, the roles of the reader $(Q_R)$ and of the passport $(Q_P)$ can be described as follows:

$Q_P = \text{in}_P(c_s, \text{read}).\text{out}_P(c_s, \langle data[P], sod \rangle)$

$Q_R = \text{out}_R(c_s, \text{read}).\text{in}_R(c_s, \langle x', \text{sign}(\langle a, h(\langle a, x' \rangle)\rangle, sk[D]) \rangle)$

The complete representation of the system is given by $PA = C_{PA}[\text{new } c_s.(Q_P | Q_R)]$ where $C_{PA}$ is the following context:

$C_{PA} = ag(D, \{D\}, \{vk(sk[D])\}, \{sk[D]\}).ag(R, \{R\}, \emptyset, \emptyset).!ag(P, \mathcal{P}, \emptyset, \{data[P]\}).$

Continuing Example 10, $C_{PA}$ and $C_{BAC}$ are composable and $C^{C_{PA},C_{BAC}}$ is the context:

$C^{C_{PA},C_{BAC}} = ag(D, \{D\}, \{vk(sk[D])\}, \{sk[D]\}).ag(R, \{R\}, \emptyset, \emptyset).!ag(P, \mathcal{P}, \emptyset, \{ke[P], km[P], data[P]\}).$

Let $S$ be a set of channels. Let $\rho$ be a mapping from $S$ to $T_{\mathcal{A}_{gt}} \times S_e$. We say that two processes $P$ and $Q$ are *composable under* $\rho$ if $P = C[R_1, \dots, R_n]$, $Q = C'[R'_1, \dots, R'_n]$ where $R_i, R'_i$ are roles of the
same agent $A_i$ for $i = 1...n$, $C$ and $C'|_S$ are composable and for all $c \in \text{dom}(\rho)$, if $c\rho = (ta, (\mathcal{E}, F))$ then for all $i \in \{1, ..., n\}$, $c \in \text{ch}_{A_i}(Q)$ is equivalent to $A_i \in ta$. This reflects the fact that agents using channel $c$ should be explicitly listed as authorized agents for $c$.

The composability between $P$ and $Q$ ensures that the agents in $Q$ sharing abstract authentic, confidential and secure channels are correctly represented in $\rho$.

**Definition 13.** Let $S$ be a set of channels. Let $\rho$ be a mapping from $S$ to $T_{\mathcal{A}_{gt}} \times S_e$. Let $P = C[R_1, ..., R_n]$ and $Q = C'[R'_1, ..., R'_n]$ two closed composable processes under $\rho$.

For all $\tilde{P} = C[\tilde{R}_1, ..., \tilde{R}_n]$ annotations of $P$ under $\rho$, the implementation of $Q$ by $\tilde{P}$ through $\rho$, denoted $\tilde{P}^{\rho}$, is the process $C_0[R_1.R_1'',...,R_n.R_n'']$ where $C_0 = C^{C,C'|_S}$ and for all $i \in \{1, ..., n\}$, $R_i''$ is defined as $R_i'$ where all instances of $\text{out}_A(c, u)$ (resp. $\text{in}_A(c, u)$) are replaced by $\text{out}_A(c_{pub}, \mathcal{E}\sigma)$ (resp. $\text{in}_A(c_{pub}, \mathcal{E}\sigma)$) when $c\rho = (ta, (\mathcal{E}, F))$, $t_{\mathcal{E}}\sigma = u$ and $\text{event}_A(\text{ev}_i(c, ta, \chi_{\mathcal{E}}\sigma, F\sigma))$ is in $\tilde{R}_i$ for some substitution $\sigma$.

**Example 14.** Continuing Example 12, the implementation of $PA$ by $\tilde{BAC}$ through $\rho$ is thus the process $\tilde{BAC}^{\rho} PA = C^{C_{PA}, C_{BAC}}[R_P.Q'_P | R_R.Q'_R]$ where $Q'_P$ and $Q'_R$ are defined as follows:

$$ 
\begin{aligned}
Q'_P &= \text{in}_P(c_{pub}, \mathcal{E}_{BAC}(\text{read}, K_1, K_2)).\text{out}_P(c_{pub}, \mathcal{E}_{BAC}(\langle\text{data}[P], \text{sod}\rangle, K_1, K_2)) \\
Q'_R &= \text{out}_R(c_{pub}, \mathcal{E}_{BAC}(\text{read}, K'_1, K'_2)).\text{in}_R(c_{pub}, \mathcal{E}_{BAC}(\langle x, \text{sign}(\langle a, h(\langle a, x\rangle), sk[D]\rangle), \mathcal{K}'_1, \mathcal{K}'_2))
\end{aligned}
$$

with $K_1 = f_1(y, k_P)$, $K_2 = f_2(y, k_P)$, $K'_1 = f_1(k_R, w)$, $K'_2 = f_2(k_P, w)$. Note that the ICAO standard describes in fact the Passive Authentication protocol as the process $C[Q'_P | Q'_R]$ (without tags). Thanks to our result, we may study the simpler process $C[\text{new } c_s.(Q_P | Q_R)]$.

## 4 Security property

It is easy to state secrecy in our formalism, using a special event $\text{Sec} \in \mathcal{E}v$: any term occurring in a $\text{Sec}$ event should remain secret unless the corresponding session involves a dishonest agent.

**Definition 15.** Let $Q$ be closed process containing some events of the form $\text{Sec}(t, (A_1, ..., A_n))$ where $t$ is a term and $A_1, ..., A_n$ are some agents. Let $\Phi$ be a closed frame. We say that $Q$ preserves secrecy if for all $(Q, \emptyset, \emptyset, \emptyset) \stackrel{\text{ev}_1...\text{ev}_n}{\implies} (Q', \Phi', \mu', \theta')$, for all $i \in \{1, ..., n\}$, if $\text{ev}_i = \text{Sec}(t', (A'_1, ..., A'_n))$ for some $t'$ and some honest agents $A'_1, ..., A'_n$ then $\Phi' \not\equiv t'$.

We may also specify the properties requested from a key exchange protocol $P$: $P$ should preserve the secrecy of the session keys occurring in its events and should ensure that the associated public keys are public. Moreover, $P$ also needs to ensure that a session key cannot be used to implement two different channels and that honest agents sharing a channel will share the same session keys for this channel. In such a case, we say that $P$ is a *secure channel establishment protocol*.

**Definition 16.** Let $P = C[R_1, ..., R_n]$ be a closed process. Let $\tilde{P}$ be an annotation of $P$ under some mapping $\rho$. We say that $\tilde{P}$ is a *secure channel establishment protocol* when for all $(\tilde{P}, \emptyset, \emptyset, \emptyset) \stackrel{e_1...e_n}{\implies} (P', \Phi', \mu', \theta')$, for all $i \in \{1, ..., m\}$, if $e_i = \text{ev}(c, ta, (s_1, ..., s_\ell), (u_1, ..., u_q))$ such that $\text{ev} \in \text{Ev}$, all agents in $ta$ are honest then for all $k \in \{1, ..., \ell\}$, $\Phi' \not\equiv s_k$ and for all $k \in \{1, ..., q\}$, $\Phi' \vdash u_k$. Moreover, for all $j \in \{1, ..., m\}$, if $\text{ev}_j = \text{ev}'(c', ta', (s'_1, ..., s'_{\ell'}), (u'_1, ..., u'_{q'}))$ for some $\text{ev}' \in \text{Ev}$, some channel $c'$, some tuple $ta'$ of agents and some tuples $(s'_1, ..., s'_{\ell'})$ and $(u'_1, ..., u'_{q'})$ of terms then

- either $ta \neq ta'$ or $c \neq c'$ or $\text{ev} = \text{ev}'$ implies $\forall k \in \{1, ..., \ell\}, \forall k' \in \{1, ..., \ell'\}, s_k \neq s'_{k'}$

- or one of the two following properties is satisfied :

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

- $\forall k \in \{1, ..., \ell\}, \forall k' \in \{1, ..., \ell'\}, s_k \neq s'_{k'}$.
The first item indicates that the session keys used for a channel between some honest agents are necessarily different from session keys used for a different channel between any kind of agents, whether they are honest, dishonest or a mix of both. The second item requires that for matching channels and sets of agents, either the session keys perfectly match or they are all different.

We are now ready to state our main result: if $P$ is a secure channel establishment protocol and if $Q$ preserves secrecy using some secure, confidential, or authentic channels, then $Q$ may safely use $P$ to implement its channels. The proof of Theorem 17 is available in a companion report [5].

**Theorem 17.** Let $\mathit{tag}_A$ and $\mathit{tag}_B$ be two disjoint sets of tags. Let $S_e$ be a set of $\mathit{tag}_A$-encapsulation allowing authentic, confidential, and secure channels. Let $\rho$ be a mapping from channels to $T_{\mathcal{A}_{gt}} \times S_e$. Let $P$ and $Q$ be two closed executable composable $\mathit{tag}_B$-processes under $\rho$ such that $P$ and $Q$ do not share names and $\mathit{fa}(P) = \mathit{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} \perp Q$ preserves secrecy as well.

For simplicity, we prove secure composition w.r.t. secrecy properties but we believe that our result could be easily extended to trace properties.

**Sketch of proof.** The proof first relies on that fact that the reachability properties are preserved by disjoint parallel composition. In particular, the process $\tilde{P} | Q$ is a secure channel establishment protocol and preserves secrecy. The rest of the proof consists in showing that any trace of $\tilde{P} \perp Q$ is also a trace of $\tilde{P} | Q$ with a frame that induces a similar attacker knowledge. More specifically, properties from Definition 7 ensure that $\mathit{tag}_B$-terms generated by the attacker or obtained from the encapsulations in $\tilde{P} \perp Q$ do not give any relevant knowledge to the attacker and can be replaced by fresh names. This allows us to obtain a trace without $\mathit{tag}_B$-terms and so without encapsulations. Lastly, since $\tilde{P} | Q$ is a secure channel establishment protocol, we can always match two encapsulations having same session keys with the corresponding abstract channel in $\tilde{P} | Q$. $\blacksquare$

**Example 18.** Continuing Example 14, the annotation under $\rho$ of the Basic Access Control $\mathcal{B} \tilde{A} C$ is secure and the Passive Authentication $C_{PA}[\mathit{new }c_s.(Q_p.\mathit{event}_P(\mathit{Sec}(data[P], (P, R))) | Q_R)]$ preserves secrecy (of the private data). Hence, thanks to Theorems 8 and 17, the implementation of $PA$ by $\mathcal{B} \tilde{A} C$ through $\rho$, $C^{C_{PA},C_{BAC}}[R_p.Q'_p.\mathit{event}_P(\mathit{Sec}(data[P], (P, R))) | R_R.Q'_R]$, preserves secrecy.

# 5 Case studies

We show that our approach can be applied to deployed protocols such as the biometric passport or TLS applied to 3D-secure. As an application, we show that the automatic analysis through the CL-Atse tool can be significantly speed up when the number of sessions goes higher.

## 5.1 Biometric passport

Our running example is the combination of the Basic Access Control (BAC) protocol with the Passive Authentication (PA) protocol from the electronic passports. Actually, PA is not the only protocol executed after BAC. Another authentication mechanism is used to prevent cloning of the passport chip. This protocol, called *Active Authentication protocol* (AA), also uses the same session keys and encapsulations than PA. Using the CL-Atse tool [18], we show for different scenarios that BAC is a secure channel establishment protocol and that PA and AA both preserve secrecy. Thanks to our main result, this yields security of the combined protocol, where BAC implements the secure channel of PA and AA. For comparison purpose, we also analyze directly the combined protocol with CL-Atse. These analysis are reported in Section 5.3.
## 5.2 TLS and 3D-secure

Our results also apply to other complex systems. We study the Visa 3D-secure protocol [17] used by several websites for internet banking and that relies on secure channels implemented by the well known TLS protocol. The Visa 3D secure protocol is an authenticated payment method between a card holder and a merchant during an electronic payment. This protocol aims to ensure authentication of the card holder as well as confirmation that the card holder is authorized by his bank to make the payment. Lastly, the protocol also aims to ensure the secrecy of the card holder's banking information, the payment amount and other data.

The protocol involves four types of participants: a card holder (C), a merchant (M), a centralized structure called Visa Directory Servers (DS) and the card issuer's servers called Access Control Servers (ACS). The main role of the Visa Directory Servers is to transfer card holder's information between the Access Control Servers and the merchant. In itself, the 3D secure protocol is already a complex protocol with multiple exchanges of messages. But the protocol also requires most messages to be exchanged through a TLS channel. More specifically, messages of the 3D secure protocol shall be encrypted with a symmetric session key previously established with TLS. In our model, this means that the messages are encapsulated by ($\mathcal{E}_{TLS}, \emptyset$), as defined in Theorem 8.

The well known TLS protocol [15, 9] aims at establishing a secure channel between a client and a server. Using the CL-Atse tool, we show that TLS (Basic TLS handshake, in the RSA mode) is indeed a secure channel establishment protocol.

Note that for one session of the Visa 3D secure protocol yields four sessions of the TLS protocol: one channel between C and M, between C and ACS, between ACS and DS and finally between M and DS. This renders the verification of even one session of 3D secure protocol with the channels implemented by TLS a complex task (more than thirty five messages exchanged per session).

## 5.3 Analysis with CL-Atse

We applied the automatic verification tool CL-Atse [18] on a Dell T1700 computer (16 Go RAM, 3.40 GHz CPU). The corresponding time of analysis are displayed below.

<table><thead><tr><th colspan="2"></th><th colspan="8">Computation time (in seconds, timeout set to 24 hours)</th></tr><tr><th colspan="2">protocols</th><th colspan="2">TLS & 3D secure</th><th colspan="2">BAC & PA</th><th colspan="2">BAC & AA</th><th colspan="2">BAC & PA & AA</th></tr><tr><th colspan="2">complete system (C) or<br>separated analysis (S)</th><th>S</th><th>C</th><th>S</th><th>C</th><th>S</th><th>C</th><th>S</th><th>C</th></tr></thead><tbody><tr><th rowspan="3">number of<br>sessions<br>considered</th><th>1</th><td>0.2</td><td>0.1</td><td>0.7</td><td>0.1</td><td>0.7</td><td>0.1</td><td>0.7</td><td>0.2</td></tr><tr><th>2</th><td>1350</td><td>time out</td><td>6.2</td><td>1.6</td><td>6.2</td><td>1.6</td><td>6.5</td><td>43156</td></tr><tr><th>3</th><td>time out</td><td>time out</td><td>9133</td><td>time out</td><td>9133</td><td>time out</td><td>9185</td><td>time out</td></tr></tbody></table>

Amongst the tools able to verify security protocols for a bounded number of sessions, CL-Atse is well known and considered to be one of the fastest. However, in the case of the 3D-secure protocol, the tool already fails to verify one session with all channels implemented as we reached a time out set to 24 hours of computation. Thus, to obtain meaningful results with the 3D-secure protocol, we considered the case where only the channel between the card holder and the merchant is implemented. Already in this case, we can see a clear benefit from analyzing separately 3D-secure and TLS when considering two sessions. Indeed, the verification can be performed under 25 minutes when analysing the protocols separately whereas the tool was reaching a time out when considering the complete system. We obtain similar results with the Basic Access Control protocol, the Active Authentication protocol and the Passive Authentication protocol. Note that for verification tools handling unbounded number of sessions (e.g. ProVerif [3], Tamarin [14]), the gain in time would probably be less significant since these tools do not systematically explore all interleavings.
# 6 Conclusion

We have shown how to securely compose a protocol with the implementation of its channels. We have provided a characterization for the three most common types of channels: secure, confidential, and authentic channels. We plan to consider other types of communication channels like anonymous channels. This will certainly require to extend our approach to equivalence properties.

Our composition result holds for a class of primitives that encompasses all standard cryptographic primitives. We plan to extend it to a larger class of primitives, including in particular exclusive or or homomorphic encryption.

Our result assumes a light tagging of the primitives, to ensure that an encapsulation cannot be confused with a message coming from the protocols. While tagging is reasonable, it is not often done in practice. On the other hand standard protocols typically enjoy some non unifiability properties that prevent such confusion. We believe that our result could be extended to a general notion of non unifiability of the terms, without having to require explicit tagging.

## Acknowledgments:

The research leading to these results has received funding from the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement n° 258865, project ProSecure.

## References

1. Machine readable travel document. Technical Report 9303, International Civil Aviation Organization, 2008.

2. M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In *Proc. of the 28th ACM Symposium on Principles of Programming Languages (POPL'01)*, pages 104–115, January 2001.

3. B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In *Proc. CSFW'01*, 2001.

4. B. Blanchet and A. Podelski. Verification of cryptographic protocols: Tagging enforces termination. In A. Gordon, editor, *Foundations of Software Science and Computation Structures (FoSSaCS'03)*, volume 2620 of LNCS, April 2003.

5. V. Cheval, V. Cortier, and E. Le-Morvan. secure refinements of communication channels. research report RR-8790, Inria, eric.le-morvan@inria.fr, 2015.

6. Ş. Ciobâčă and V. Cortier. Protocol composition for arbitrary primitives. In *Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10)*, pages 322–336, Edinburgh, Scotland, UK, July 2010. IEEE Computer Society Press.

7. V. Cortier and S. Delaune. Safely composing security protocols. *Formal Methods in System Design*, 34(1):1–36, Feb. 2009.

8. A. Datta, A. Derek, J. C. Mitchell, and A. Roy. Protocol composition logic (PCL). *Electr. Notes Theoretical Computer Science*, 172:311–358, 2007.

9. T. Dierks and E. Rescorla. The transport layer security (tls) protocol version 1.2 (rfc 5246). Technical report, IETF, 2008.

10. T. Gibson-Robinson, A. Kamil, and G. Lowe. Verifying layered security protocols. *Journal of Computer Security*, 23(3), 2015.

11. J. D. Guttman. Authentication tests and disjoint encryption: a design method for security protocols. *Journal of Computer Security*, 12(3–4):409–433, 2004.

12. J. D. Guttman. Establishing and preserving protocol security goals. *Journal of Computer Security*, 22(2):203–267, 2004.
14 Secure refinements of communication channels

13 J. D. Guttman and F. J. Thayer. Protocol independence through disjoint encryption. In Proc. 13th Computer Security Foundations Workshop (CSFW'00), pages 24–34. IEEE Comp. Soc. Press, 2000.

14 S. Meier, B. Schmidt, C. Cremers, and D. Basin. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In N. Sharygina and H. Veith, editors, Computer Aided Verification, 25th International Conference, CAV 2013, Princeton, USA, Proc., volume 8044 of Lecture Notes in Computer Science, pages 696–701. Springer, 2013.

15 C. Meyer and J. Schwenk. Lessons learned from previous ssl/tls attacks : A brief chronology of attacks and weaknesses. In IACR Cryptology ePrint, 2013.

16 S. Moedersheim and L. Viganò. Sufficient conditions for vertical composition of security protocols. In ASIACCS, pages 435–446, 2014.

17 V. Pasupathinathan, J. Pieprzyk, H. Wang, and J. Y. Cho. Formal analysis of card-based payment systems in mobile services. In Fourth Australian information security workshop, conferences in research and practise in information security, pages 213–220, 2006.

18 M. Turuani. The CL-Atse Protocol Analyser. In Term Rewriting and Applications - Proc. of RTA, volume 4098 of Lecture Notes in Computer Science, pages 277–286, Seattle, WA, USA, 2006.
# A Modelization of other protocols

## A.1 TLS and 3D secure

### A.1.1 TLS

TLS is the protocol that is most often used when an application needs a secure channel to communicate on a public network. In a TLS session between a client C and a server S, C and S start by doing a handshake: C sends a message containing a constant `helloC` along with his name, a session number `id` and a fresh nonce `n_C`. The server then answers a constant `helloS` along with the same session number `id`, another fresh nonce `n_S` and its signed public encryption key. After that, C runs the key exchange step by encrypting with S's public key a message containing a randomly generated value `pms` along with the two previous nonces `n_C` and `n_S`, S checks that `n_C` and `n_S` are in the message he received and if so C and S build the session key `keygen(pms, n_S, n_C)`. The two last steps consist in C and S sending each other respectively the hashes `finishC` and `finishS` encrypted by `keygen(pms, n_S, n_C)`: they contain all the values that were transmitted during the session, furthermore `finishC` and `finishS` contain respectively the labels client and server so that they can not be confused. `finishC` and `finishS` enable C and S to check that they agree upon what has been transmitted during the session. The session key `keygen(pms, n_S, n_C)` provided by TLS will be used to implement the channels in other protocols

Here is diagram showing how a TLS session works with $t_{TLS}$ a tag:

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

In our models, the roles of the client ($R_C$) and of the server ($R_S$) are as follows, with $c \in Ch_p$:

$R_C$ = new $n_C$.new id.out_c(c, (helloC, name[C], n_C, id)).in_c(c, (helloS, x, id)).
in_c(c, sign((t_{TLS}, name[S], u), sk[S])).new pms.out_c(c, aenc((t_{TLS}, pms), u)).
out_c(c, senc((t_{TLS}, finishC_1), keygen(pms, n_C, x))).
in_c(c, senc((t_{TLS}, finishS_1), keygen(pms, n_C, x))).0

$R_S$ = in_s(c, (helloC, v, w, y)).new n_S.out_s(c, (helloS, n_S, y)).
out_s(c, sign((t_{TLS}, name[S], pk(priv[S]), sk[S]))).
in_s(c, aenc((t_{TLS}, z), pk(priv[S]))).in_s(c, senc((t_{TLS}, finishC_2), keygen(z, w, n_S))).
out_s(c, senc((t_{TLS}, finishS_2), keygen(z, w, n_S))).0

where

finishC_1 = h((keygen(pms, n_C, x), name[C], name[S], n_C, x, Id, client))

finishS_1 = h((keygen(pms, n_C, x), name[C], name[S], n_C, x, Id, server))

finishC_2 = h((keygen(z, w, n_S), v, name[C], name[S], w, n_S, y, client))

finishS_2 = h((keygen(z, w, n_S), v, name[C], name[S], w, n_S, y, server))

The session key provided by TLS is `keygen(z, w, n_S)` for $R_S$ and `keygen(pms, n_C, x)` for $R_C$.
### A.1.2 3D secure

An informal description of a 3D-secure session between a client C, a merchant M, a directory server DS and an access control server ACS is provided below.

C →sec M : <pan[C], expiry[C]>
M →sec DS : <pan[C], password[M], infoM>
DS →sec ACS : <pan[C], infoM>
ACS →sec DS : <panok, acctid, url[ACS], proto>
DS →sec M : <panok, acctid, url[ACS], proto>
M →sec C : sign(<t3D, infoM, publicM, expiry[C], transInfo>, skVISA[M])
C →sec ACS : sign(<t3D, infoM, publicM, expiry[C], transInfo>, skVISA[M])
ACS →sec C : <name[M], payInfo, panshort[C], expiry[C]>
ACS →outofband C : pam[C]
C →sec ACS : password[C]
ACS →sec C : sign(<t3D, infoM, xid, payInfo, panshort[C], status, otherInfo>, skVISA[ACS])
C →sec M : sign(<t3D, infoM, xid, payInfo, panshort[C], status, otherInfo>, skVISA[ACS])
M →sec C : sign(<t3D, status>, skVISA[M])

where infoM = <macqbin, id[M]>, publicM = <name[M], url[M]>, transInfo = <xid, pdate, pamnt, acctid>, payInfo = <pamnt, pdate> and otherInfo = <date, cavv, eci, cavvalg>. The specification of the 3D-secure protocol is not public, the semantics of some of the data (e.g. cavv, eci, cavvalg) are unspecified even in [17]. That is why in the protocol we model them as nonces.

A 3D-secure session starts when C sends to M a purchase request containing her primary account number pan[C] and the expiration date expiry[C] of the card. Then M forwards to DS pan[C] along with M's identifiers infoM and password[M] shared only by M and DS : M asks for confirmation about C's banking account. DS transmits to ACS the identifiers of M along with pan[C] so that ACS certifies the existence of the bank account of C. Upon successful verification, ACS sends confirmation panok to DS along with its own url url[ACS] and some other information to be forwarded to M. M then sends to C a signed copy of M's own information infoM and publicM along with the identifiers transInfo regarding the transaction, furthermore it makes C initiate a communication with ACS thanks to his knowledge of url[ACS]. C forwards M's signed message to ACS so that ACS checks C. ACS sends back to C a summary of the transaction (M's identity, payInfo and panshort[C]). ACS also sends a personnal assurance message pam[C] at some point that C uses to determine the password password[C] that she has to give to authentify herself to ACS. The nature of pam[C] is not specified, usually it consists in a secret code sent to C's mobile phone that has to be sent back, or it can be a password matrix given to C when she gets her credit card, in that case C just has to send the password contained in a case specified by ACS. In the end, ACS gives C a signed message containing all the data necessary to conclude the transaction. That certified message is then forwarded to M and finally M signs with his own signing key the status of the transaction between C and M.

We notice that the signing key sk involved in TLS is different from the ones involved in 3D secure, which models the fact that signing keys in 3D secure are provided by VISA that is in charge of credit cards, thus that signing key has no reason to be involved in TLS. Consequently TLS and 3D secure do not share names, which is a prerequisite of our result.

### A.1.3 Composition between TLS and 3D secure

Channels in 3D secure have to be implemented between all the users that have to speak together, namely C and M, M and DS, DS and ACS, ACS and C. Thus if 3D secure is to be composed with
TLS, we need to instanciate it with all the agents that will later share secure channels in 3D secure. However given that the CL-Atse tool can not analyse 4 TLS sessions within a reasonable time (24 hours), we had to restrict the composition to only one channel implementation between C and M. Consequently we model the case where there is only one honest Access Directory Server ACS, one honest Directory Server DS and one honest merchant M speaking with an unbounded number of clients, possibly dishonest. The four roles of 3D-secure are denoted by $R'_C$, $R'_M$, $R'_DS$, and $R'_ACS$. Thus 3D secure can be modeled by the following process:

$$3D = C_{3D}[\text{new } c_s^{ca_1} . \text{new } c_s^{ca_2} . \text{new } c_s^{cm} . \text{new } c_s^{ma} . \text{new } c_s^{ad} . (R'_C | R'_M | R'_ACS | R'_DS)]$$

where

$$C_{3D}[\_] = \text{ag}(M, \{M\}, \mathcal{K}_{pub}^M, \mathcal{K}_{prv}^M) \cdot \text{ag}(ACS, \{ACS\}, \emptyset, \mathcal{K}_{prv}^{ACS}) \cdot \text{ag}(DS, \{DS\}, \emptyset, \emptyset) \cdot \text{ag}(C, \mathcal{P}, \emptyset, \mathcal{K}_{prv}^C) \cdot \_ \\ \text{with the sets } \mathcal{K}_{pub}^M = \{\text{id}[M], \text{name}[M]\}, \mathcal{K}_{prv}^M = \{\text{password}[M], \text{sk}_{VISA}[M], \text{url}[M]\}, \mathcal{K}_{prv}^C = \{\text{pan}[C], \text{expiry}[C], \text{pam}[C], \text{password}[C]\} \text{ and } \mathcal{K}_{prv}^{ACS} = \{\text{sk}_{VISA}[ACS], \text{url}[ACS]\}.$$

Since we implement only the secure channel between C and M, the complete representation of the system is the process $TLS = \text{ag}(M, \{M\}, \mathcal{K}_{pub}^M, \mathcal{K}_{prv}^M) \cdot \text{ag}(C, \mathcal{P}, \mathcal{K}_{pub}^C, \emptyset) \cdot (R_C | R_S)$ where $\mathcal{P}$ is an infinite set of agents containing honest and dishonest agents such that $M \notin \mathcal{P}$ and $\mathcal{K}_{pub}^M = \{\text{pk}(\text{priv}[M]), \text{vk}(\text{sk}[M]), \text{name}[M]\}, \mathcal{K}_{prv}^M = \{\text{priv}[M], \text{sk}[M]\}, \mathcal{K}_{pub}^C = \{\text{name}[C]\}$.

As previously mentioned, the 3D-secure protocol specifies that all the exchanged messages should be done on secure channels implemented by TLS, except the out of bound channel used by the issuer's Access Control Servers. More specifically, they require that all messages of the 3D secure protocol must be encrypted with a symmetric session key previously established with TLS. In our model, it means that the messages are encapsulated by $(\mathcal{E}_{TLS}, \emptyset)$, as defined in Theorem 8. Moreover as explained in Section 5, the session keys provided by TLS are keygen($z, w, n_S$) and keygen($pms, n_C, x$) for the card holder and merchant respectively. Therefore, by defining the mapping $\rho = \{c_S^{cm} \rightarrow ((C, M), (\mathcal{E}_{TLS}, \emptyset))\}$, an annotation of TLS under $\rho$ is the following process:

$$T\tilde{L}S = C_{TLS}[R_C \cdot \text{event}_C(\text{ev}(c_S^{cm}, (C, M), k_{CM}^1)) | R_S \cdot \text{event}_M(\text{ev}(c_S^{cm}, (C, M), k_{CM}^2))]$$

where $C_{TLS}[\_] = \text{ag}(M, \{M\}, \mathcal{K}_{pub}^M, \mathcal{K}_{prv}^M) \cdot \text{ag}(C, \mathcal{P}, \mathcal{K}_{pub}^C, \emptyset) \cdot \_ \cdot k_{CM}^1 = \text{keygen}(pms, n_C, x)$ and $k_{CM}^2 = \text{keygen}(z, w, n_S)$. Therefore, the implementation of 3D by $T\tilde{L}S$ through $\rho$ is the process:

$$T\tilde{L}S . \rho 3D = C^{C_{TLS}, C_{3D}}[(\text{new } c_S^{ca_1} . \text{new } c_S^{ca_2} . \text{new } c_S^{cm} . \text{new } c_S^{ma} . \text{new } c_S^{ad} . (R_C . R'_C) | (R_S . R'_M) | R'_ACS | R'_DS)]$$

where

$$C^{C_{TLS}, C_{3D}}[\_] = \text{ag}(M, \{M\}, \mathcal{K}_{pub}^M \cup \mathcal{K}_{pub}^{\prime M}, \mathcal{K}_{prv}^M \cup \mathcal{K}_{prv}^{\prime M}) \cdot \text{ag}(ACS, \{ACS\}, \mathcal{K}_{pub}^{ACS}, \mathcal{K}_{prv}^{ACS}) \cdot \text{ag}(DS, \{DS\}, \emptyset, \emptyset) \cdot \text{ag}(C, \mathcal{P}, \mathcal{K}_{pub}^C, \mathcal{K}_{prv}^C \cup \mathcal{K}_{prv}^{\prime C}) \cdot \_$$

Our result now enables us to conclude that if

$$C_{3D}[(\text{new } c_S^{ca_1} . \text{new } c_S^{ca_2} . \text{new } c_S^{cm} . \text{new } c_S^{ma} . \text{new } c_S^{ad} . (R'_C \cdot \text{event}_C(\text{Sec}(\text{pan}[C], (C, M, ACS, DS)))) | R'_M | R'_ACS | R'_DS))]$$

preserves secrecy (in that instance, the secrecy of $pan[C]$) and if $T\tilde{L}S$ is secure, then the implementation of the process 3D by $T\tilde{L}S$ through $\rho$ preserves secrecy. Furthermore we can also look at the secrecy of other data such as $pam[C]$ expressed as follows.

$$C_{3D}[(\text{new } c_S^{ca_1} . \text{new } c_S^{ca_2} . \text{new } c_S^{cm} . \text{new } c_S^{ma} . \text{new } c_S^{ad} . (R'_C \cdot \text{event}_C(\text{Sec}(\text{pam}[C], (C, ACS)))) | R'_M | R'_ACS | R'_DS))]$$

Note that the secrecy of $pam[C]$ only concerns the agents C and ACS whereas the secrecy of $pan[C]$ is between C, M, ACS, DS. Our model allows us to verify the secrecy of $pam[C]$ even when M or DS can be dishonest.
## A.2 Active Authentication protocol

The aim of the Active Authentication protocol (AA) is to prevent cloning of the passport chip. For that purpose the protocol relies on a signing key $sk[P]$ that is registered in a tempered resistant memory and cannot be read or copied. A certificate of the verification key $vk(sk[P])$ provided by the Document Signer authority mentioned in Example 12 is in fact contained in the data of the passport. For sake of simplicity, we represented these data in Example 12 as a name $data[P]$ since their exact value was irrelevant for the implementation of the Passive Authentication protocol by the Basic Access Control protocol. In reality, the data stored in the chip is organized in data groups ($dg_1$ up to $dg_{19}$), some of them containing the passport holder's name, picture, etc. In particular, the certificate of the verification key $vk(sk[P])$, that is $sign(vk(sk[P]), sk[D])$, is stored in the data group $dg_{15}$. Thus, by replacing, in the Passive Authentication presented in Example 12, the name $data[P]$ by the tuple of data groups, we can see that a reader would then be able to obtain from $d_{15}$ the verification key $vk(sk[P])$ after the execution of the protocol.

A session of the Active Authentication protocol is as follows: R sends to P a nonce $n_R$ that P has to send back along with a nonce $n_P$ after having them signed with $sk[P]$. In our study we consider the case where AA is a-tagged, although it is not the case in practice.

$$ 
\begin{aligned}
R & \to_{sec} P : \langle \text{init}, n_R \rangle \\
P & \to_{sec} R : \text{sign}(\langle a, n_P, n_R \rangle, sk[P])
\end{aligned}
$$

The AA roles of the reader ($Q_R$) and of the passport ($Q_P$) on $c_s \in Ch_s$ can be expressed as below in our formalism :

$$ 
\begin{aligned}
Q_R &= \text{new } n_R.\text{out}_R(c_s, \langle \text{init}, n_R \rangle).\text{in}_R(c_s, \text{sign}(\langle a, x', n_R \rangle, sk[P])) \\
Q_P &= \text{in}_P(c_s, \langle \text{init}, y' \rangle).\text{new } n_P.\text{out}_P(c_s, \text{sign}(\langle a, n_P, y' \rangle, sk[P]))
\end{aligned}
$$

We model the case where one honest reader speaks with an unbounded number of honest and dishonest passports. Thus AA can be modeled as a whole by $AA = C_{AA}[\text{new } c_s.(Q_R | Q_P)]$ where

$$ C_{AA} = \text{ag}(D, \{D\}, vk(sk[D]), sk[D]).\text{ag}(R, \{R\}, \emptyset, \emptyset).!\text{ag}(P, P, \emptyset, \{sk[P]\}).\_ $$

where $P$ is an infinite set of agents containing honest and dishonest agents and $R, D \notin P$.

We study the composition between the Basic Access Control (BAC) and AA. As explained in the section 2.3, in the a-tagged BAC protocol the role of the passport ($R_P$) and the role of the reader ($R_R$) can be modeled as shown below, with $c \in Ch_p$, $M = \text{senc}(\langle a, x, n_P, y \rangle, ke[P])$, $N = \text{senc}(\langle a, n_P, x, k_P \rangle, ke[P])$, $U = \text{senc}(\langle a, n_R, z, k_R \rangle, ke[P])$ and $V = \text{senc}(\langle a, z, n_R, w \rangle, ke[P])$ :

$$ 
\begin{aligned}
R_P &= \text{in}_P(c, \text{challenge}).\text{new } n_P.\text{out}_P(c, n_P).\text{in}_P(c, \langle M, \text{mac}(\langle a, M \rangle, km[P]) \rangle). \\
    & \quad \text{new } k_P.\text{out}_P(c, \langle N, \text{mac}(\langle a, N \rangle, km[P]) \rangle).0
\end{aligned}
$$

$$ 
\begin{aligned}
R_R &= \text{out}_R(c, \text{challenge}).\text{in}_R(c, z).\text{new } k_R.\text{new } n_R.\text{out}_R(c, \langle U, \text{mac}(\langle a, U \rangle, km[P]) \rangle). \\
    & \quad \text{in}_R(c, \langle V, \text{mac}(\langle a, V \rangle, km[P]) \rangle).0
\end{aligned}
$$

Hence an honest reader communicating with an unbounded number of passports that are either honest or dishonest can be modeled by :

$$ BAC = \text{ag}(R, \{R\}, \emptyset, \emptyset).!\text{ag}(P, P, \emptyset, \{ke[P], km[P]\}).(R_P | R_R) $$

As written in section 3.1, the BAC protocol is meant to generate two session keys per role ($f_1(y, k_P)$ and $f_2(y, k_P)$ for $R_P$, $f_1(k_R, w)$ and $f_2(k_R, w)$ for $R_R$), and the messages sent in AA are all encapsulated by $(\mathcal{E}_{BAC}, \emptyset)$ where $\mathcal{E}_{BAC} = \langle t, \text{mac}(\langle a_{\mathcal{E}_{BAC}}, t \rangle, x_2) \rangle$ with $t = \text{senc}(\langle a_{\mathcal{E}_{BAC}}, x \rangle, x_1)$, $t_{\mathcal{E}_{BAC}} = x$ and $X_{\mathcal{E}_{BAC}} = (x_1, x_2)$. By theorem 8, the encapsulation $(\mathcal{E}_{BAC}, \emptyset)$ implements secure channels.
The fact that BAC aims at establishing a secure channel for P and R is translated in our model by using the mapping $\rho = \{c_s \to ((P, R), (\mathcal{E}_{BAC}, \emptyset))\}$ and the associated annotation of BAC under $\rho$:

$$B\tilde{A}C = C_{BAC}[R_P.event_P(ev(c_s, (P, R), (f_1(y, k_P), f_2(y, k_P)))) | R_R.event_R(ev(c_s, (P, R), (f_1(k_R, w), f_2(k_R, w))))]$$

where $C_{BAC}[\_] = \text{ag}(R, \{R\}, \emptyset, \emptyset).!\text{ag}(P, \mathcal{P}, \emptyset, \{ke[P], km[P]\}).\_.$

Hence the two contexts $C_{BAC}$ and $C_{AA}$ can be composed into the new context

$$C^{C_{AA}, C_{BAC}} = \text{ag}(D, \{D\}, \text{vk}(sk[D]), sk[D]).\text{ag}(R, \{R\}, \emptyset, \emptyset).!\text{ag}(P, \mathcal{P}, \emptyset, \{ke[P], km[P], sk[P]\}).\_$$

And now we can write the process $B\tilde{A}C \circ \rho PA = C^{C_{AA}, C_{BAC}}[R_P.Q'_P | R_R.Q'_R]$ where $Q'_P$ and $Q'_R$ are defined as follows:

$$Q'_P = \begin{cases} \text{in}_P(c_{pub}, \mathcal{E}_{BAC}(\langle \text{init}, y' \rangle, K_1, K_2)). & \\ \text{new } n_P.\text{out}_P(c_{pub}, \mathcal{E}_{BAC}(\text{sign}(\langle a, n_P, y' \rangle, sk[P]), K_1, K_2)) & \end{cases}$$

$$Q'_R = \begin{cases} \text{new } n_R.\text{out}_R(c_{pub}, \mathcal{E}_{BAC}(\langle \text{init}, n_R \rangle, K'_1, K'_2)). & \\ \text{in}_R(c_{pub}, \mathcal{E}_{BAC}(\text{sign}(\langle a, x', n_P \rangle, sk[P]), K'_1, K'_2)) & \end{cases}$$

with $K_1 = f_1(y, k_P)$, $K_2 = f_2(y, k_P)$, $K'_1 = f_1(k_R, w)$, $K'_2 = f_2(k_P, w)$.

Our result enables us for instance to conclude that if the annotation under $\rho$ of the Basic Access Control $B\tilde{A}C$ is secure and if the Active Authentication

$$C_{AA}[\text{new } c_s.(Q_R | Q_P.event_P(\text{Sec}(sk[P], (P))))]$$

preserves secrecy, then

$$C^{C_{AA}, C_{BAC}}[R_P.Q'_P.event_P(\text{Sec}(sk[P], (P)))) | R_R.Q'_R]$$

also preserves secrecy.

## B Secure encapsulations

For our proofs, we will need to discuss about the deduction proof of $\Phi \vdash t$. As such, we will denote by $\Phi \vdash_P t$ the deduction of $\Phi \vdash t$ with an associated proof $P$. We write $\Phi \vdash_i t$ when $t$ is the $i$-th element of $\Phi$. We write $\Phi \vdash_t$ when $t \in \mathcal{N}_D \cup \mathcal{F}_{cst}$. When an inference rule $ir$ is applied on premises $\Phi \vdash_{P_1} u_1, \dots, \Phi \vdash_{P_n} u_n$ to obtain the term $u$, we write $\Phi \vdash_{ir(P_1, \dots, P_n)} u$. Note that given a proof $P$ and a frame $\Phi$, there exists a unique $t$ such that $\Phi \vdash_P t$.

Given as a proof $P$ can be seen as a term, we write $\mathcal{M}(P) = (n, m)$ the pair of integer where $n = \max\{i \in st(P) \cap \mathcal{N}\}$ if $st(P) \cap \mathcal{N} \neq \emptyset$ else $n = 0$; and $m = |P|$ where $|P|$ is the number of symbols in $P$. We also consider the lexicographic order on pairs of integers. Given $\Phi$ and $t$, we say that a proof $P$ of $\Phi \vdash t$ is minimal for $\mathcal{M}$ if for all $P'$, $\Phi \vdash_{P'} t$ implies $\mathcal{M}(P) \leq \mathcal{M}(P')$. We also consider sometimes minimal proof $P$ for $|P|$ instead of $\mathcal{M}(P)$.

Lastly we say that a proof $P$ is a successive sequence of applications of decomposition rule on the $i$-th element of $\Phi$ when there exists $n \in \mathcal{N}$ such that $P = \text{ir}_n(\dots \text{ir}_1(i, P_1, \dots, P_m) \dots, P'_1, \dots, P'_{m'})$ and each $\text{ir}_k$ is a decomposition rule for $k = 1 \dots n$.

We denote by $st_<(t)$ the set of strict subterms of $t$. We naturally extend this notion to frames.

**Lemma 19.** Let $\Phi$ be a frame. Let $t \in \mathcal{T}(\mathcal{F}, \mathcal{N} \cup \mathcal{X})$ such that $\Phi \vdash t$. For all $P$ minimal proofs for $|P|$ of $\Phi \vdash t$, for all $P' \in st(P)$, for all terms $t'$, if $\Phi \vdash_{P'} t'$ then

■ root($t'$) $\notin \mathcal{F}_{key}$ and root($P$) is a composition rule imply $t' \in st(\Phi) \cup st(t)$;
■ root(t') / ∈ Fkey and root(P) is a decomposition rule imply t' ∈ st(Φ);

■ t' = f(u) for some term u and f ∈ Fkey implies u ∈ st< (Φ) ∪ st< (t).

**Proof.** We show the result by induction on M(P).

Base case $|P| = 1$: In such a case, $t \in \mathcal{N}_D \cup \mathcal{F}_{\text{cst}}$ or $t \in \Phi$. In the former, $\text{root}(t) \notin \mathcal{F}_{\text{key}}$ and $\text{root}(P)$ is neither a composition rule nor a decomposition rule. Hence the result directly holds. In the latter, $t \in \Phi$ and $\text{root}(P)$ is neither a composition rule nor a decomposition rule. Therefore, if $t = f(u)$ for some term $u$ and $f \in \mathcal{F}_{\text{key}}$ then we directly have that $u \in \text{st}_<(\Phi)$. Hence the result holds.

Induction case $|P| > 1$: Otherwise root(P) is an inference rule. Therefore, we have :

$$ \frac{t_1 \quad \dots \quad t_n}{t} $$

with $P = \text{ir}(P_1, \dots, P_n)$ and for all $k \in \{1, \dots, n\}$, $\Phi \vdash_{P_k} t_k$. Applying the inductive hypothesis we can deduce that for all $k \in \{1, \dots, n\}$, for all $P' \in \text{st}(P_k)$, for all $t'$, if $\Phi \vdash_{P'} t'$ then:

■ root(t') / ∈ Fkey and root(P_k) is a composition rule imply t' ∈ st(Φ) ∪ st(t_k);

■ root(t') / ∈ Fkey and root(P_k) is a decomposition rule imply t' ∈ st(Φ);

■ t' = f(u) for some term u and f ∈ Fkey implies u ∈ st< (Φ) ∪ st< (t_k).

Let $P' \in \text{st}(P)$ and let $t'$ be a term such that $\Phi \vdash_{P'} t'$. Let us do a case analysis on whether ir is a decomposition or a composition rule.

■ Case ir is a composition rule: In such a case, there exists a function symbol f such that $t = f(t_1, \dots, t_n)$, implying that for all $k \in \{1, \dots, n\}$, $st(\Phi) \cup st(t_k) \subseteq st(\Phi) \cup st(t)$ and $st_<(\Phi) \cup st_<(t_k) \subseteq st_<(\Phi) \cup st_<(t)$. Hence, if $P' \in \text{st}(P_k)$ for some $k \in \{1, \dots, n\}$ the result directly holds given our inductive hypothesis. Consider now $P' = P$ and so $t' = t$. In such a case, if $\text{root}(t) \notin \mathcal{F}_{\text{key}}$ then we directly have that $t \in \text{st}(t)$ else $t = f(u)$ with $f \in \mathcal{F}_{\text{key}}$ and $u \in \text{st}_<(t)$. Therefore the result holds.

■ Case ir is a decomposition rule: Otherwise $t_1 = f(t_1, u_1, \dots, u_m)$ for some term $u_1, \dots, u_m$ and $f \notin \mathcal{F}_{\text{key}}$. Since $P$ is minimal, we deduce that either $\text{root}(P_1)$ is a decomposition rule or $P = t_1$ meaning that $t_1 \in \Phi$ (otherwise there would exist $P'_1 \in \text{st}(P_1)$ such that $\Phi \vdash_{P'_1} t$ and $|P'_1| < |P|$). Let us first focus on $P' \in \text{st}(P_1)$. If $\text{root}(t') \notin \mathcal{F}_{\text{key}}$ then by our inductive hypothesis and knowing that ir is a decomposition rule, we obtain that $t' \in \text{st}(\Phi)$. In particular when $P' = P_1$ we deduce that $f(t_1, u_1, \dots, u_m) \in \text{st}(\Phi)$. Moreover, if $t' = g(u)$ with $g \in \mathcal{F}_{\text{key}}$ then $u \in \text{st}_<(\Phi) \cup \text{st}_<(f(t_1, u_1, \dots, u_m))$. Since $f(t_1, u_1, \dots, u_m) \in \text{st}(\Phi)$, $u \in \text{st}_<(f(t_1, u_1, \dots, u_m))$ implies $u \in \text{st}_<(\Phi)$. Hence the result holds.

Note that $f(t_1, u_1, \dots, u_m) \in \text{st}(\Phi)$ allows us to directly prove that $t \in \text{st}(\Phi)$ hence the result holds in the case $P' = P$ and $t' = t$.

Let us now focus on the case where $P' \in \text{st}(P_k)$ for some $k \in \{2, \dots, n\}$. By our inductive hypothesis, we know that $\text{root}(t') \notin \mathcal{F}_{\text{key}}$ implies $t' \in \text{st}(\Phi) \cup \text{st}(t_k)$. But from the definition of a decomposition rule, we know that for all $k \in \{2, \dots, n\}$, either $t_k \in \text{st}_<(f(t_1, u_1, \dots, u_m))$ or $\text{root}(t_k) \in \mathcal{F}_{\text{key}}$ and $\text{st}_<(t_k) \subseteq \text{st}_<(f(t_1, u_1, \dots, u_m))$. In the former, since $f(t_1, u_1, \dots, u_m) \in \text{st}(\Phi)$ then we directly deduce that $t' \in \text{st}(\Phi)$. In the latter, since $\text{root}(t') \notin \mathcal{F}_{\text{key}}$ and $\text{root}(t_k) \in \mathcal{F}_{\text{key}}$ then $t' \in \text{st}(t_k)$ implies $t' \in \text{st}_<(t_k)$ and so $t' \in \text{st}_<(f(t_1, u_1, \dots, u_m)) \subseteq \text{st}(\Phi)$.

If $t' = g(u)$ with $g \in \mathcal{F}_{\text{key}}$ then by our inductive hypothesis, $u \in \text{st}_<(\Phi) \cup \text{st}_<(t_k)$. But we have already shown that $\text{st}_<(t_k) \subseteq \text{st}_<(f(t_1, u_1, \dots, u_m))$ and $f(t_1, u_1, \dots, u_m) \in \text{st}(\Phi)$. Hence we deduce that $u \in \text{st}_<(t_k)$ implies that $u \in \text{st}_<(\Phi)$ which allows us to conclude.

◀
## B.1 BAC encapsulation

**Lemma 20.** Let $\mathcal{A}_{\mathcal{E}_{\text{BAC}}} \in \text{Tag}$. Let $\mathcal{E}_{\text{BAC}} = \langle t, h(\langle \mathcal{a}_{\mathcal{E}_{\text{BAC}}}, \langle t, z \rangle \rangle) \rangle$ with $t = \text{senc}(\langle \mathcal{a}, x \rangle, y)$, $t_{\mathcal{E}_{\text{BAC}}} = x$ and $X_{\mathcal{E}_{\text{BAC}}} = (y, z)$. We have that $(\mathcal{E}_{\text{BAC}}, \emptyset)$ is a $\{\mathcal{a}_{\mathcal{E}_{\text{BAC}}}\}$-tagged encapsulation and $S = \{(\mathcal{E}_{\text{BAC}}, \emptyset)\}$ allows secure channels.

**Proof.** Let $(\mathcal{E}_1, \emptyset), \dots, (\mathcal{E}_n, \emptyset) \in S$ such that the variables of $\mathcal{E}_1, \dots, \mathcal{E}_n$ are disjoints. Since $S = \{(\mathcal{E}_{\text{BAC}}, \emptyset)\}$, we have that $\mathcal{E}_i \sim \mathcal{E}_j$ for all $i, j \in \{1, \dots, n\}$. For all $i \in \{1, \dots, n\}$, we will denote $t_{\mathcal{E}_i} = x_i$ and $X_{\mathcal{E}_i} = (y_i, z_i)$. Let $\sigma$ be a ground substitution such that $\text{dom}(\sigma) \subseteq \text{vars}(\mathcal{E}_1, \dots, \mathcal{E}_n)$ and let $\Phi$ be a ground frame such that $\mathcal{A}_{\mathcal{E}_{\text{BAC}}} \notin \text{st}(\sigma, \Phi)$. Finally, let $I = \{i \in \{1, \dots, n\} \mid \Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash x_i \sigma\}$. We show that for all $i \in \{1, \dots, n\}$, Properties 1, 2, 4 and 6 of Definition 7 hold.

**Property 1:** Let $i \in \{1, \dots, n\}$. Let $t \in \mathcal{T}(\mathcal{F}_{\text{key}}, \{y_i \sigma, z_i \sigma\})$ such that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_P t$. Assume that $P$ is minimal for $|P|$. We do a case analysis on $|P|$. If $|P| = 1$ then either $t \in \mathcal{N}_D \cup \mathcal{F}_{\text{cst}}$ or $t \in \Phi$ or $t = \mathcal{E}_k \sigma$ for some $k \in \{1, \dots, n\}$. But $\mathcal{A}_{\mathcal{E}_{\text{BAC}}} \notin \text{st}(t)$. Hence, we deduce that $t \in \mathcal{N}_D \cup \mathcal{F}_{\text{cst}}$ or $t \in \Phi$. Therefore, $\Phi \vdash t$ and so $\Phi \cdot [x_k \sigma]_{k \in I} \vdash t$.

Otherwise, $|P| > 1$. Let us assume that there exist $j \in \{1, \dots, n\}$ and $P' \in \text{st}(P)$ such that $P' = |\Phi| + j$. Since $|P| > 1$, we deduce that there exist ir, $P''$, $P_1, \dots, P_m$, $\ell \in \{1, \dots, m\}$ such that $P'' = \text{ir}(P_1, \dots, P_m) \in \text{st}(P)$ and $P_\ell = P'$. Let us denote $t''$ the term $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_{P''} t''$. By Lemma 19, we deduce that either $t'' \in \text{st}(\Phi) \cup \text{st}(\mathcal{E}_k \sigma)_{k=1}^n \cup \text{st}(t)$ or $t'' = g(u)$ for some $g \in \mathcal{F}_{\text{key}}$ and $u \in \text{st}_< (\Phi) \cup \text{st}_< (\mathcal{E}_k \sigma)_{k=1}^n \cup \text{st}_< (t)$. Since $\mathcal{A}_{\mathcal{E}_{\text{BAC}}} \notin \text{st}(t, \sigma, \Phi)$, $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_{P'} \mathcal{E}_j \sigma$ and all $\mathcal{E}_1, \dots, \mathcal{E}_n$ are equal after variable renaming, we deduce that in both cases, ir cannot be a composition rule. Since ir is a decomposition rule, we in fact have $P'' = \text{ir}(P')$ where ir is one of the pair decomposition. Moreover, either $t'' = h(\langle \mathcal{a}_{\mathcal{E}_{\text{BAC}}}, \langle u, z_i \sigma \rangle \rangle)$ where $u = \text{senc}(\langle \mathcal{a}_{\mathcal{E}_{\text{BAC}}}, x_i \sigma \rangle, y_i \sigma)$ or $t'' = u$. Once again since $\mathcal{A}_{\mathcal{E}_{\text{BAC}}} \notin \text{st}(t)$, we deduce that $P'' \neq P$. Thus, there exists $Q = \text{ir}'(Q_1, \dots, Q_\ell)$ and $\ell' \in \{1, \dots, \ell\}$ such that $Q \in \text{st}(P)$ and $Q_{\ell'} = P''$.

By the Lemma 19, we can easily show that $ir'$ cannot be a composition rule for some $g \notin \mathcal{F}_{\text{key}}$ since if would imply that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_Q \mathcal{E}_r \sigma$ for some $r$ which would contradict our hypothesis on the minimality of $|P|$. We also show that $ir'$ cannot be a composition rule for some $g \in \mathcal{F}_{\text{key}}$. In such a case, it would imply that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_Q g(t'')$. But since $\mathcal{A}_{\mathcal{E}_{\text{BAC}}} \in \text{st}(t'')$, then $Q \neq P$ and so there must be another inference rule $ir''$ applied on $Q$ in $P$. Once again, by Lemma 19, $ir''$ cannot be a composition rule for any function symbol since it would imply that $g(t'') \in \text{st}(\Phi) \cup \text{st}([\mathcal{E}_k \sigma]_{k=1}^n) \cup \text{st}(t)$ but $\mathcal{E}_{\text{BAC}}$ does not contain function symbol from $\mathcal{F}_{\text{key}}$ and $\mathcal{A}_{\mathcal{E}_{\text{BAC}}} \notin \text{st}(t, \sigma, \Phi)$. Moreover, $ir''$ cannot be a decomposition rule either since the only rule involving a function symbol $g \in \mathcal{F}_{\text{key}}$ as argument is the signature decomposition which would imply that there exists a term $v$ and a proof $R \in \text{st}(P)$ such that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_R \text{sign}(v, t'')$. Once again, this is prevented by Lemma 19. Therefore, we can conclude that $ir'$ cannot be a composition rule for some $g \in \mathcal{F}_{\text{key}}$.

Thus, $ir'$ is a decomposition rule. Note that once again thanks to Lemma 19 and the fact that $\mathcal{A}_{\mathcal{E}_{\text{BAC}}} \notin \text{st}(t, \sigma, \Phi)$, we can deduce that $j' = 1$ meaning that $t''$ is not used as a key in the decomposition rule $ir'$. But there is no decomposition rule for $h$, thus $t'' = \text{senc}(\langle \mathcal{a}, x_j \sigma \rangle, y_j \sigma)$, $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_{Q_2} y_j \sigma$. This allows us to deduce that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_Q \langle \mathcal{a}_{\mathcal{E}_{\text{BAC}}}, x_j \sigma \rangle$. But $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash \langle \mathcal{a}_{\mathcal{E}_{\text{BAC}}}, x_j \sigma \rangle$ also imply that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash x_j \sigma$ and so $j \in I$. Therefore, $\Phi \cdot [x_k \sigma]_{k \in I} \vdash \langle \mathcal{a}_{\mathcal{E}_{\text{BAC}}}, x_j \sigma \rangle$.

We have just shown that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$, a proof $Q_j$ and a term $u$ such that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_{P|_{p'_j}} u$ and $\Phi \cdot [x_k \sigma]_{k \in I} \vdash_{Q_j} u$. Therefore, by replacing all instances of $P|_{p'_j}$ in $P$ by $Q_j$, we obtain that a proof $P'$ such that $\Phi \cdot [x_k \sigma]_{k \in I} \vdash_{P'} t$. This allows us to conclude.

**Property 2:** Let $u \in \text{st}(\mathcal{E}_i) \setminus \mathcal{X}$ and $v \in \text{st}(\mathcal{E}_j) \setminus \mathcal{X}$ such that $u$ and $v$ are unifiable and $\text{root}(u) \neq \langle \cdot \rangle$. By definition of $\mathcal{E}_{\text{BAC}}$, $u, v$ unifiable implies that there exists a position $p$ of $\mathcal{E}_{\text{BAC}}$ such that $u = \mathcal{E}_i|_p$ and $v = \mathcal{E}_j|_p$. Since $\mathcal{E}_i \sim \mathcal{E}_j$ then the result holds.
**Property 4:** Let $i \in \{1, \dots, n\}$. Consider a minimal proof $P$ for $|P|$ such that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_P x_i \sigma$. We do a case analysis on $|P|$. If $|P| = 1$ then either $x_i \sigma \in \mathcal{N}_D \cup \mathcal{F}_{cst}$ or $x_i \sigma \in \Phi$ or $x_i \sigma = \mathcal{E}_k \sigma$ for some $k \in \{1, \dots, n\}$. But $\mathcal{a}_{\mathcal{EBAC}} \notin st(x_i \sigma)$. Hence, we deduce that $x_i \sigma \in \mathcal{N}_D \cup \mathcal{F}_{cst}$ or $x_i \sigma \in \Phi$. Therefore, $\Phi \vdash x_i \sigma$ and so $\Phi \cdot [x_k \sigma]_{k \in I} \vdash x_i \sigma$.

Otherwise, $|P| > 1$. Following exactly the proof of Property 1 (replacing $t$ by $x_i \sigma$), we deduce that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$, a proof $Q_j$ such that $P|_{p'_j} = \text{ir}_1(\text{ir}_2(|\Phi|+j), Q_j)$, $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_P |P|_{p'_j} \langle \mathcal{a}_{\mathcal{EBAC}}, x_j \sigma \rangle$ and $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_Q y_j \sigma$ where $\text{ir}_1$ is the decomposition rule of senc and $\text{ir}_2$ is the first decomposition rule of $\langle \cdot \rangle$. Let us look at the proof $Q_j$. Since $\mathcal{a}_{\mathcal{EBAC}} \notin st(y_j \sigma)$, we can deduce by minimality of $|P|$ that $|\Phi| + j \notin Q_j$ (otherwise, using the same reasoning, it would imply that there exists a proof $Q'_j \in st(Q_j)$ deducing $y_i \sigma$). Thus, $\Phi \cdot [\mathcal{E}_k \sigma]_{k \in \{1, \dots, n\}-j} \vdash_Q y_j \sigma$. Let $I' = \{i \in \{1, \dots, n\}-j \mid \Phi \cdot [\mathcal{E}_k \sigma]_{k \in \{1, \dots, n\}-j} \vdash x_i \sigma\}$. Note that $I' \subseteq I - j$. By applying Property 1 on $y_j \sigma$ with $[\mathcal{E}_k \sigma]_{k \in \{1, \dots, n\}-j}$ and $I'$, we deduce that $\Phi \cdot [x_k \sigma]_{k \in I'} \vdash y_j \sigma$.

Therefore, we have proven that if $|\Phi| + i \in st(P)$ then $\Phi \cdot [x_k \sigma]_{k \in I-i} \vdash y_j \sigma$. Otherwise, if for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, $P|_{p_j} = |\Phi| + j$ implies that $i \neq j$ then we also have proven that $\Phi \cdot [x_k \sigma]_{k \in I-i} \vdash x_j \sigma$ using the same replacement of proofs as in the proof of Property 1. Hence, the result holds.

**Property 6:** Let $i \in \{1, \dots, n\}$. Let $\sigma'$ some ground substitution such that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash \mathcal{E}_i \sigma'$ and $\mathcal{a}_{\mathcal{EBAC}} \notin st(\sigma')$, if we denote $J = I - i$ then. Consider a proof $P$ minimal for $|P|$ such that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_P \mathcal{E}_i \sigma'$. If $|P| = 1$ then it implies that $\mathcal{E}_i \sigma' \in [\mathcal{E}_k \sigma]_{k=1}^n$ due to the fact that $\mathcal{a}_{\mathcal{EBAC}} \notin st(\Phi)$. Therefore, there exists $k \in \{1, \dots, n\}$ such that $\mathcal{E}_i \sigma' = \mathcal{E}_k \sigma$. Since we already know that $\mathcal{E}_i \sim \mathcal{E}_k$ then the result holds.

Otherwise $|P| > 1$. In such a case $P = \text{ir}(P_1, \dots, P_n)$. We do a case analysis on ir.

- Case ir is a decomposition rule: By Lemma 19, we deduce that $\mathcal{E}_i \sigma' \in st(\Phi) \cup st([\mathcal{E}_k \sigma]_{k=1}^n)$. But since $\mathcal{a}_{\mathcal{EBAC}} \notin st(\Phi) \cup st(\sigma)$, then we deduce that $\mathcal{E}_i \sigma' \in [\mathcal{E}_k \sigma]_{k=1}^n$ which contradicts the minimality of $|P|$.

- Case ir is a composition rule: In such a case, we have $P = \text{ir}(P_1, P_2)$ and $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_P u$ and $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_P h(\langle \mathcal{a}_{\mathcal{EBAC}}, \langle u, z_i \sigma' \rangle \rangle)$ with $u = \text{senc}(\langle \mathcal{a}_{\mathcal{EBAC}}, x_i \sigma' \rangle, y_i \sigma')$. Let us first focus on $P_2$. If the last rule of $P_2$ starts by a decomposition rule, then by Lemma 19, we deduce that $h(\langle \mathcal{a}_{\mathcal{EBAC}}, \langle u, z_i \sigma' \rangle \rangle) \in st([\mathcal{E}_k \sigma]_{k=1}^n)$ which would then imply that there exists $k \in \{1, \dots, n\}$ such that $h(\langle \mathcal{a}_{\mathcal{EBAC}}, \langle u, z_i \sigma' \rangle \rangle) = h(\langle \mathcal{a}_{\mathcal{EBAC}}, \langle v, z_k \sigma \rangle \rangle)$ with $v = \text{senc}(\langle \mathcal{a}_{\mathcal{EBAC}}, x_k \sigma \rangle, y_k \sigma)$. Therefore, $x_k \sigma = x_i \sigma'$ and so $\mathcal{E}_i \sigma' = \mathcal{E}_k \sigma$ which contradicts our hypothesis on the minimality of $|P|$. Therefore, the last rule of $P_2$ is necessarily a composition rule, implying that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash z_i \sigma'$. Following the same proof of Property 1 (replacing $t$ by $z_i \sigma'$), we deduce that $\Phi \cdot [\mathcal{t}_{\mathcal{E}_k \sigma}]_{k \in I} \vdash z_i \sigma'$. Let us now consider $P_1$. If $P_1$ starts by a decomposition rule, then by Lemma 19, we deduce that $\text{senc}(\langle \mathcal{a}_{\mathcal{EBAC}}, x_i \sigma' \rangle, y_i \sigma') \in st([\mathcal{E}_k \sigma]_{k=1}^n)$. Thus, it implies that there exists $j \in \{1, \dots, n\}$ such that $x_i \sigma' = x_j \sigma$ and $y_i \sigma' = y_j \sigma$ meaning that $X_{\mathcal{E}_i \sigma'} \cap X_{\mathcal{E}_j \sigma} \neq \emptyset$. Hence the result holds. If on the other hand, $P_1$ starts by a composition rule then we directly have that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash x_i \sigma'$. Once again by following the same proof as in Property 1 (replacing $t$ by $x_i \sigma'$), we deduce that $\Phi \cdot [\mathcal{t}_{\mathcal{E}_k \sigma}]_{k \in I} \vdash x_i \sigma'$.

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

## B.2 TLS encapsulation

**Lemma 21.** Let $\mathcal{a}_{\mathcal{TLS}} \in \text{Tag}$. Let $\mathcal{E}_{\text{TLS}} = \text{senc}(\langle \mathcal{a}_{\mathcal{TLS}}, x \rangle, y)$, $\mathcal{t}_{\mathcal{E}_{\text{TLS}}} = x$ and $X_{\mathcal{E}_{\text{TLS}}} = y$. We have that $(\mathcal{E}_{\text{TLS}}, \emptyset)$ is a $\{\mathcal{a}_{\mathcal{TLS}}\}$-tagged encapsulation and $S = \{(\mathcal{E}_{\text{TLS}}, \emptyset)\}$ allows secure channels.

**Proof.** Let $(\mathcal{E}_1, \emptyset), \dots, (\mathcal{E}_n, \emptyset) \in S$ such that the variables of $\mathcal{E}_1, \dots, \mathcal{E}_n$ are disjoints. Since $S = \{(\mathcal{E}_{\text{TLS}}, \emptyset)\}$, we have that $\mathcal{E}_i \sim \mathcal{E}_j$ for all $i, j \in \{1, \dots, n\}$. For all $i \in \{1, \dots, n\}$, we will denote $\mathcal{t}_{\mathcal{E}_i} = x_i$
and $X_{\varepsilon_i} = y_i$. Let $\sigma$ be a ground substitution such that $dom(\sigma) \subseteq vars(\varepsilon_1, \dots, \varepsilon_n)$ and let $\Phi$ be a ground frame such that $a_{\varepsilon\text{TLS}} \notin st(\sigma, \Phi)$. Finally, let $I = \{i \in \{1, \dots, n\} \mid \Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash x_i\sigma\}$. We show that for all $i \in \{1, \dots, n\}$, Properties 1, 2, 4 and 6 of Definition 7 hold.

**Property 1:** Let $i \in \{1, \dots, n\}$. Let $t \in \mathcal{T}(\mathcal{F}_{key}, \{y_i\sigma\})$ such that $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash_P t$. Assume that $P$ is minimal for $|P|$. We do a case analysis on $|P|$. If $|P| = 1$ then either $t \in \mathcal{N}_D \cup \mathcal{F}_{cst}$ or $t \in \Phi$ or $t = \varepsilon_k\sigma$ for some $k \in \{1, \dots, n\}$. But $a_{\varepsilon\text{TLS}} \notin st(t)$. Hence, we deduce that $t \in \mathcal{N}_D \cup \mathcal{F}_{cst}$ or $t \in \Phi$. Therefore, $\Phi \vdash t$ and so $\Phi \cdot [x_k\sigma]_{k \in I} \vdash t$.

Otherwise, $|P| > 1$. Let us assume that there exists $j \in \{1, \dots, n\}$ and $P' \in st(P)$ such that $P' = |\Phi| + j$. Since $|P| > 1$, we deduce that there exists ir, $P'', P_1, \dots, P_m$, $\ell \in \{1, \dots, m\}$ such that $P'' = \text{ir}(P_1, \dots, P_m) \in st(P)$ and $P_\ell = P'$. Let us denote $t''$ the term $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash_{P''} t''$. By Lemma 19, we deduce that either $t'' \in st(\Phi) \cup st(\varepsilon_k\sigma)_{k=1}^n \cup st(t)$ or $t'' = g(u)$ for some $g \in \mathcal{F}_{key}$ and $u \in st_<(\Phi) \cup st_<(\varepsilon_k\sigma)_{k=1}^n \cup st_<(t)$. Since $a_{\varepsilon\text{TLS}} \notin st(t, \sigma, \Phi)$, $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash_{P'} \varepsilon_j\sigma$ and all $\varepsilon_1, \dots, \varepsilon_n$ are equal after variable renaming, we deduce that in both cases, ir cannot be a composition rule. Since ir is a decomposition rule, we in fact have $P'' = \text{ir}(P', Q)$ where ir is the senc decomposition and $t'' = \langle a_{\varepsilon\text{TLS}}, x_j\sigma \rangle$. Thus we have that $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash_{P'} x_j\sigma$ and so $j \in I$. Therefore, $\Phi \cdot [x_k\sigma]_{k \in I} \vdash \langle a_{\varepsilon\text{TLS}}, x_j\sigma \rangle$.

We have just shown that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$, a proof $Q_j$ and a term $u$ such that $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash_{P|_{p'_j}} u$ and $\Phi \cdot [x_k\sigma]_{k \in I} \vdash_{Q_j} u$. Therefore, by replacing all instances of $P|_{p'_j}$ in $P$ by $Q_j$, we obtain that a proof $P'$ such that $\Phi \cdot [x_k\sigma]_{k \in I} \vdash_{P'} t$. This allows us to conclude.

**Property 2:** Let $u \in st(\varepsilon_i) \setminus X$ and $v \in st(\varepsilon_j) \setminus X$ such that $u$ and $v$ are unifiable and $\text{root}(u) \neq \langle\rangle$. By definition of $\varepsilon_{\text{TLS}}$, $u, v$ unifiable implies that there exists a position $p$ of $\varepsilon_{\text{TLS}}$ such that $u = \varepsilon_i|_p$ and $v = \varepsilon_j|_p$. Since $\varepsilon_i \sim \varepsilon_j$ then the result holds.

**Property 4:** Let $i \in \{1, \dots, n\}$. Consider a minimal proof $P$ for $|P|$ such that $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash_P x_i\sigma$. We do a case analysis on $|P|$. If $|P| = 1$ then either $x_i\sigma \in \mathcal{N}_D \cup \mathcal{F}_{cst}$ or $x_i\sigma \in \Phi$ or $x_i\sigma = \varepsilon_k\sigma$ for some $k \in \{1, \dots, n\}$. But $a_{\varepsilon\text{TLS}} \notin st(x_i\sigma)$. Hence, we deduce that $x_i\sigma \in \mathcal{N}_D \cup \mathcal{F}_{cst}$ or $x_i\sigma \in \Phi$. Therefore, $\Phi \vdash x_i\sigma$ and so $\Phi \cdot [x_k\sigma]_{k \in I-i} \vdash x_i\sigma$.

Otherwise, $|P| > 1$. Following exactly the proof of Property 1 (replacing $t$ by $x_i\sigma$), we deduce that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$, a proof $Q_j$ such that $P|_{p'_j} = \text{ir}(|\Phi| + j, Q_j)$, $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash_{P|_{p'_j}} \langle a_{\varepsilon\text{TLS}}, x_j\sigma \rangle$ and $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash_{Q_j} y_j\sigma$ where ir is the decomposition rule of senc. Let us look at the proof $Q_j$. Since $a_{\varepsilon\text{TLS}} \notin st(y_j\sigma)$, we can deduce by minimality of $|P|$ that $|\Phi| + j \notin Q_j$ (otherwise, using the same reasoning, it would imply that there exists a proof $Q'_j \in st_<(Q_j)$ deducing $y_i\sigma$). Thus, $\Phi \cdot [\varepsilon_k\sigma]_{k \in \{1, \dots, n\}-j} \vdash_{Q_j} y_j\sigma$. Let $I' = \{i \in \{1, \dots, n\} - j \mid \Phi \cdot [\varepsilon_k\sigma]_{k \in \{1, \dots, n\}-j} \vdash x_i\sigma\}$. Note that $I' \subseteq I - j$. By applying Property 1 on $y_j\sigma$ with $[\varepsilon_k\sigma]_{k \in \{1, \dots, n\}-j}$ and $I'$, we deduce that $\Phi \cdot [x_k\sigma]_{k \in I'} \vdash y_j\sigma$.

Therefore, we have proven that if $|\Phi| + i \in st(P)$ then $\Phi \cdot [x_k\sigma]_{k \in I-i} \vdash y_i\sigma$. Otherwise, if for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, $P|_{p_j} = |\Phi| + j$ implies that $i \neq j$ then we also have proven that $\Phi \cdot [x_k\sigma]_{k \in I-i} \vdash x_j\sigma$ using the same replacement of proofs as in the proof of Property 1. Hence, the result holds.

**Property 6:** Let $i \in \{1, \dots, n\}$. Let $\sigma'$ be some ground substitution such that $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash \varepsilon_i\sigma'$. Consider a proof $P$ minimal for $|P|$ such that $\Phi \cdot [\varepsilon_k\sigma]_{k=1}^n \vdash_P \varepsilon_i\sigma'$. If $|P| = 1$ then it implies that $\varepsilon_i\sigma' \in [\varepsilon_k\sigma]_{k=1}$ due to the fact that $a_{\varepsilon\text{TLS}} \notin st(\Phi)$. Therefore, there exists $k \in \{1, \dots, n\}$ such that $\varepsilon_i\sigma' = \varepsilon_k\sigma$. Since we already know that $\varepsilon_i \sim \varepsilon_k$ then the result holds.

Otherwise $|P| > 1$. In such a case $P = \text{ir}(P_1, \dots, P_n)$. We do a case analysis on ir.

■ Case ir is a decomposition rule: by Lemma 19, we deduce that $\varepsilon_i\sigma' \in st(\Phi) \cup st([\varepsilon_k\sigma]_{k=1}^n)$. But since $a_{\varepsilon\text{TLS}} \notin st(\Phi) \cup st(\sigma)$, then we deduce that $\varepsilon_i\sigma' \in [\varepsilon_k\sigma]_{k=1}^n$ which contradicts the minimality of $|P|$.
■ Case ir is a composition rule: Then we directly have that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash x_i\sigma'$. Once again by following the same proof as in Property 1 (replacing $t$ by $x_i\sigma'$), we deduce that $\Phi \cdot [t_{\mathcal{E}_k\sigma}]_{k \in I} \vdash x_i\sigma'$.

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

## B.3 Signcrypt encapsulation

**Lemma 22.** Let $\mathcal{A}_{\mathcal{E}_{\text{signcrypt}} \in \text{Tag}}$, Let $\mathcal{E}_{\text{signcrypt}} = \text{sign}(\langle \mathcal{A}_{\mathcal{E}_{\text{signcrypt}}}, \mathbf{a}_{\text{enc}}(\langle \mathcal{A}_{\mathcal{E}_{\text{signcrypt}}}, x \rangle, \text{pk}(y)) \rangle, z)$ with $t_{\mathcal{E}_{\text{signcrypt}}} = x$ and $X_{\mathcal{E}_{\text{signcrypt}}} = (y, z)$. We have that $(\mathcal{E}_{\text{signcrypt}}, \emptyset)$ is a $\{\mathcal{A}_{\mathcal{E}_{\text{signcrypt}}}\}$-tagged encapsulation and $S = \{(\mathcal{E}_{\text{signcrypt}}, \emptyset)\}$ allows secure channels.

**Proof.** Let $(\mathcal{E}_1, \emptyset), \dots, (\mathcal{E}_n, \emptyset) \in S$ such that the variables of $\mathcal{E}_1, \dots, \mathcal{E}_n$ are disjoints. Since $S = \{(\mathcal{E}_{\text{signcrypt}}, \emptyset)\}$, we have that $\mathcal{E}_i \sim \mathcal{E}_j$ for all $i, j \in \{1, \dots, n\}$. For all $i \in \{1, \dots, n\}$, we will denote $t_{\mathcal{E}_i} = x_i$ and $X_{\mathcal{E}_i} = (y_i, z_i)$. Let $\sigma$ be a ground substitution such that $\text{dom}(\sigma) \subseteq \text{vars}(\mathcal{E}_1, \dots, \mathcal{E}_n)$ and let $\Phi$ be a ground frame such that $\mathcal{A}_{\mathcal{E}_{\text{signcrypt}}} \notin \text{st}(\sigma, \Phi)$. Finally, let $I = \{i \in \{1, \dots, n\} \mid \Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash x_i\sigma\}$. We show that for all $i \in \{1, \dots, n\}$, Properties 1, 2, 4 and 6 of Definition 7 hold.

We first prove that for all term $t$ such that $\mathcal{A}_{\mathcal{E}_{\text{signcrypt}}} \notin \text{st}(t)$, $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_P t$ implies $\Phi \cdot [x_k\sigma]_{k \in I} \vdash t$. Assume that $P$ is minimal for $|P|$. We do a case analysis on $|P|$. If $|P| = 1$ then either $t \in \mathcal{N}_D \cup \mathcal{F}_{\text{est}}$ or $t \in \Phi$ or $t = \mathcal{E}_k\sigma$ for some $k \in \{1, \dots, n\}$. But $\mathcal{A}_{\mathcal{E}_{\text{signcrypt}}} \notin \text{st}(t)$. Hence, we deduce that $t \in \mathcal{N}_D \cup \mathcal{F}_{\text{est}}$ or $t \in \Phi$. Therefore, $\Phi \vdash t$ and so $\Phi \cdot [x_k\sigma]_{k \in I} \vdash t$.

Otherwise, $|P| > 1$. Let us assume that there exist $j \in \{1, \dots, n\}$ and $P' \in \text{st}(P)$ such that $P' = |\Phi| + j$. Since $|P| > 1$, we deduce that there exist ir, $P''$, $P_1, \dots, P_m$, $\ell \in \{1, \dots, m\}$ such that $P'' = \text{ir}(P_1, \dots, P_m) \in \text{st}(P)$ and $P_\ell = P'$. Let us denote $t''$ the term $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P''} t''$. By Lemma 19, we deduce that either $t'' \in \text{st}(\Phi) \cup \text{st}(\mathcal{E}_k\sigma)_{k=1}^n \cup \text{st}(t)$ or $t'' = \text{g}(u)$ for some $g \in \mathcal{F}_{\text{key}}$ and $u \in \text{st}_<(\Phi) \cup \text{st}_<(\mathcal{E}_k\sigma)_{k=1}^n \cup \text{st}_<(t)$. Since $\mathcal{A}_{\mathcal{E}_{\text{signcrypt}}} \notin \text{st}(t, \sigma, \Phi)$, $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P'} \mathcal{E}_j\sigma$ and all $\mathcal{E}_1, \dots, \mathcal{E}_n$ are equal after variable renaming, we deduce that in both cases, ir cannot be a composition rule. Since ir is a decomposition rule, we in fact have $P'' = \text{ir}(P', R)$ where ir the rule sign-decomp and $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_R \text{vk}(z_j\sigma)$. Moreover, we have $t'' = \langle \mathcal{A}_{\mathcal{E}_{\text{signcrypt}}}, \mathbf{a}_{\text{enc}}(\langle \mathcal{A}_{\mathcal{E}_{\text{signcrypt}}}, x_j\sigma \rangle, \text{pk}(y_j\sigma)) \rangle$. Once again since $\mathcal{A}_{\mathcal{E}_{\text{signcrypt}}} \notin \text{st}(t)$, we deduce that $P'' \neq P$. Thus, there exists $Q = \text{ir}'(Q_1, \dots, Q_\ell)$ and $\ell' \in \{1, \dots, \ell\}$ such that $Q \in \text{st}(P)$ and $Q_{\ell'} = P''$.

By the Lemma 19, we can easily show that $\text{ir}'$ cannot be a composition rule for some $g \notin \mathcal{F}_{\text{key}}$ since if would imply that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_Q \mathcal{E}_r\sigma$ for some $r$ which would contradict our hypothesis on the minimality of $|P|$. We also show that $\text{ir}'$ cannot be a composition rule for some $g \in \mathcal{F}_{\text{key}}$. In such a case, it would imply that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_Q \text{g}(t'')$. But since $\mathcal{A}_{\mathcal{E}_{\text{signcrypt}}} \in \text{st}(t'')$, then $Q \neq P$ and so there must be another inference rule $\text{ir}''$ applied on $Q$ in $P$. Once again, by Lemma 19, $\text{ir}''$ cannot be a composition rule for any function symbol since it would imply that $\text{g}(t'') \in \text{st}(\Phi) \cup \text{st}([\mathcal{E}_k\sigma]_{k=1}^n) \cup \text{st}(t)$ but $\mathcal{E}_{\text{signcrypt}}$ only contain the function symbol pk applied on $y$. But since $\mathcal{A}_{\mathcal{E}_{\text{signcrypt}}} \notin \text{st}(\sigma)$, we deduce that $\text{pk}(y_k)\sigma \neq \text{g}(t'')$ for all $k$. Moreover, $\text{ir}''$ cannot be a decomposition rule either since the only rule involving a function symbol $g \in \mathcal{F}_{\text{key}}$ as argument is the signature decomposition which would imply that there exists a term $v$ and a proof $R \in \text{st}(P)$ such that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_R \text{sign}(v, t'')$. Once again, this is prevented by Lemma 19 since $\mathcal{A}_{\mathcal{E}_{\text{signcrypt}}} \notin \text{st}(\sigma)$. Therefore, we can conclude that $\text{ir}'$ cannot be a composition rule for some $g \in \mathcal{F}_{\text{key}}$.

Thus $\text{ir}'$ is a decomposition rule and in fact the second decomposition of the pairing implying that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_Q \mathbf{a}_{\text{enc}}(\langle \mathcal{A}_{\mathcal{E}_{\text{signcrypt}}}, x_j\sigma \rangle, \text{pk}(y_j\sigma))$. Using a similar reasoning as above, we can prove that there exists $R = \text{ir}''(R_1, \dots, R_p)$ and $p' \in \{1, \dots, p\}$ such that $R \in \text{st}(P)$ and $R_{p'} = Q$. Moreover, by Lemma 19, $\text{ir}''$ cannot be a $f$-composition for $f \notin \mathcal{F}_{\text{key}}$ since the only function $f$ possible would be the pair but it would contradict our minimality hypothesis. Similarly as above, we can also prove that $\text{ir}'$ cannot be $f$-composition for $f \in \mathcal{F}_{\text{key}}$. Therefore, it remains that $\text{ir}''$ is a decomposition rule meaning that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_R \langle \mathcal{A}_{\mathcal{E}_{\text{signcrypt}}}, x_j\sigma \rangle$. But it also implies that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash x_j\sigma$ meaning that $j \in I$ and so $\Phi \cdot [x_k\sigma]_{k \in I} \vdash \langle \mathcal{A}_{\mathcal{E}_{\text{signcrypt}}}, x_j\sigma \rangle$.
We have just shown that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$, a proof $Q_j$ and a term $u$ such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{P|_{p'_j}} u$ and $\Phi \cdot [x_k \sigma]_{k \in I} \vdash_{Q_j} u$. Therefore, by replacing all instances of $P|_{p'_j}$ in $P$ by $Q_j$, we obtain that a proof $P'$ such that $\Phi \cdot [x_k \sigma]_{k \in I} \vdash_{P'} t$. This allows us to conclude.

**Property 1:** For all $i \in \{1, \dots, n\}$, for all $t \in \mathcal{T}(\mathcal{F}_{\text{key}}, \{y_i\sigma, z_i\sigma\})$, we have that $a_{\mathcal{E}\text{signcrypt}} \notin \text{st}(t)$. **_Hence we can apply the property we just proved which allows us to conclude._**

**Property 2:** Let $u \in \text{st}(\varepsilon_i) \setminus \mathcal{X}$ and $v \in \text{st}(\varepsilon_j) \setminus \mathcal{X}$ such that $u$ and $v$ are unifiable and $\text{root}(u) \neq \langle \rangle$. By definition of $\mathcal{E}_{\text{signcrypt}}$, $u, v$ unifiable implies that there exists a position $p$ of $\mathcal{E}_{\text{signcrypt}}$ such that $u = \varepsilon_i|_p$ and $v = \varepsilon_j|_p$. Since $\varepsilon_i \sim \varepsilon_j$ then the result holds.

**Property 4:** Let $i \in \{1, \dots, n\}$. Consider a minimal proof $P$ for $|P|$ such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_P x_i \sigma$. We do a case analysis on $|P|$. If $|P| = 1$ then either $x_i \sigma \in \mathcal{N}_D \cup \mathcal{F}_{\text{cst}}$ or $x_i \sigma \in \Phi$ or $x_i \sigma = \varepsilon_k \sigma$ for some $k \in \{1, \dots, n\}$. But $a_{\mathcal{E}\text{signcrypt}} \notin \text{st}(x_i \sigma)$. Hence, we deduce that $x_i \sigma \in \mathcal{N}_D \cup \mathcal{F}_{\text{cst}}$ or $x_i \sigma \in \Phi$. Therefore, $\Phi \vdash x_i \sigma$ and so $\Phi \cdot [x_k \sigma]_{k \in I-i} \vdash x_i \sigma$.

Otherwise, $|P| > 1$. Following exactly the proof of the property we prove at the beginning of this lemma, we deduce that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$, a proof $Q_j$ such that $P|_{p'_j} = \text{ir}_1(\text{ir}_2(\text{ir}_3(|\Phi| + j, Q_j)), R_j)$, $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{P|_{p'_j}} \langle a_{\mathcal{E}\text{signcrypt}}, x_j \sigma \rangle$, $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{Q_j} \text{vk}(z_j \sigma)$ and $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{R_j} y_j \sigma$ where $\text{ir}_1$ is the decomposition rule of $a_{\text{enc}}$, $\text{ir}_2$ is the second decomposition rule of $\langle \rangle$ and $\text{ir}_3$ is the decomposition of sign. Let us look at the proofs $Q_j$ and $R_j$. Since $a_{\mathcal{E}\text{BAC}} \notin \text{st}(y_j \sigma, z_j \sigma)$, we can deduce by minimality of $|P|$ that $|\Phi| + j \notin Q_j$ and $|\Phi| + j \notin R_j$ (otherwise, using the same reasoning, it would imply that there exists a proof $Q'_j \in \text{st}(Q_j)$ (resp. $R'_j$) deducing $\text{vk}(z_j \sigma)$ (resp. $y_j \sigma$)). Thus, $\Phi \cdot [\varepsilon_k \sigma]_{k \in \{1, \dots, n\}-j} \vdash_{Q_j} \text{vk}(z_j \sigma)$ and $\Phi \cdot [\varepsilon_k \sigma]_{k \in \{1, \dots, n\}-j} \vdash_{R_j} y_j \sigma$. Let $I' = \{i \in \{1, \dots, n\} - j \mid \Phi \cdot [\varepsilon_k \sigma]_{k \in \{1, \dots, n\}-j} \vdash x_i \sigma\}$. Note that $I' \subseteq I - j$. By applying Property 1 on $y_j \sigma$ and $\text{vk}(z_j \sigma)$ with $[\varepsilon_k \sigma]_{k \in \{1, \dots, n\}-j}$ and $I'$, we deduce that $\Phi \cdot [x_k \sigma]_{k \in I'} \vdash y_j \sigma$ and $\Phi \cdot [x_k \sigma]_{k \in I'} \vdash \text{vk}(z_j \sigma)$.

Therefore, we have proven that if $|\Phi|+i \in \text{st}(P)$ then $\Phi \cdot [x_k \sigma]_{k \in I-i} \vdash y_i \sigma$ which satisfies Property 4. Otherwise, if for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, $P|_{p_j} = |\Phi| + j$ implies that $i \neq j$ then we also have proven that $\Phi \cdot [x_k \sigma]_{k \in I-i} \vdash x_i \sigma$ by the first property proven in this lemma.

**Property 6:** Let $i \in \{1, \dots, n\}$. Let $\sigma'$ some ground substitution such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash \varepsilon_i \sigma'$. Consider a proof $P$ minimal for $|P|$ such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_P \varepsilon_i \sigma'$. If $|P| = 1$ then it implies that $\varepsilon_i \sigma' \in [\varepsilon_k \sigma]_{k=1}$ due to the fact that $a_{\mathcal{E}\text{signcrypt}} \notin \text{st}(\Phi)$. Therefore, there exists $k \in \{1, \dots, n\}$ such that $\varepsilon_i \sigma' = \varepsilon_k \sigma$. Since we already know that $\varepsilon_i \sim \varepsilon_k$ then the result holds.
Otherwise $|P| > 1$. In such a case $P = \text{ir}(P_1, \dots, P_n)$. We do a case analysis on ir.

- Case ir is a decomposition rule: By Lemma 19, we deduce that $\varepsilon_i \sigma' \in \text{st}(\Phi) \cup \text{st}([\varepsilon_k \sigma]_{k=1}^n)$. But since $a_{\mathcal{E}\text{signcrypt}} \notin \text{st}(\Phi) \cup \text{st}(\sigma)$, then we deduce that $\varepsilon_i \sigma' \in [\varepsilon_k \sigma]_{k=1}^n$ which contradicts the minimality of $|P|$.

- Case ir is a composition rule: In such a case, we have $P = \text{ir}(P_1, P_2)$ and $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{P_1} \langle a_{\mathcal{E}\text{signcrypt}}, a_{\text{enc}}(\langle a_{\mathcal{E}\text{signcrypt}}, x_i \sigma' \rangle, \text{pk}(y_i \sigma')) \rangle$ and $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{P_2} z_i \sigma'$. The latter already gives us part of Property thanks to the first property of the lemma. Let us now focus on $P_1$.

If the last rule of $P_1$ starts by a decomposition rule, then by Lemma 19, we deduce that $\langle a_{\mathcal{E}\text{signcrypt}}, a_{\text{enc}}(\langle a_{\mathcal{E}\text{signcrypt}}, x_i \sigma' \rangle, \text{pk}(y_i \sigma')) \rangle \in \text{st}([\varepsilon_k \sigma]_{k=1}^n)$ which would then imply that there exists $k \in \{1, \dots, n\}$ such that $x_i \sigma' = x_k \sigma$ and $y_i \sigma' = y_k \sigma$. Therefore the result holds. If the last rule of $P_2$ is a composition then we have $P_1 = \text{ir}'(Q_1, Q_2)$ where $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{Q_2} a_{\text{enc}}(\langle a_{\mathcal{E}\text{signcrypt}}, x_i \sigma' \rangle, \text{pk}(y_i \sigma'))$. If the last rule of $Q_2$ is a composition rule then it would imply that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash \langle a_{\mathcal{E}\text{signcrypt}}, x_i \sigma' \rangle$ and so $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash x_i \sigma'$ which would allow us to conclude. If on the other hand the last rule of $Q_2$ is a decomposition rule, then once again we would deduce that $a_{\text{enc}}(\langle a_{\mathcal{E}\text{signcrypt}}, x_i \sigma' \rangle, \text{pk}(y_i \sigma')) \in$
$st([\mathcal{E}_k\sigma]_{k=1}^n)$ and so there would exists $k \in \{1, \dots, n\}$ such that $x_i\sigma' = x_k\sigma$ and $y_i\sigma' = y_k\sigma$. This allows us to conclude.

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

## B.4 Sign encapsulation

**Lemma 23.** Let $\mathcal{A}_{\mathcal{E} \text{sign}} \in \text{Tag}$. Let $\mathcal{E}_{\text{sign}} = \text{sign}(\langle \mathcal{A}_{\mathcal{E} \text{sign}}, x \rangle, y)$ with $t_{\mathcal{E}_{\text{signcrypt}}}, x$ and $\chi_{\mathcal{E}_{\text{sign}}}, y$. We have that $(\mathcal{E}_{\text{sign}}, \text{vk}(y))$ is a $\{\mathcal{A}_{\mathcal{E} \text{sign}}\}$-tagged encapsulation and $S = \{(\mathcal{E}_{\text{sign}}, \text{vk}(y))\}$ allows authentic channels.

**Proof.** Let $(\mathcal{E}_1, \emptyset), \dots, (\mathcal{E}_n, \emptyset) \in S$ such that the variables of $\mathcal{E}_1, \dots, \mathcal{E}_n$ are disjoints. Since $S = \{(\mathcal{E}_{\text{signcrypt}}, \text{vk}(y))\}$, we have that $\mathcal{E}_i \sim \mathcal{E}_j$ for all $i, j \in \{1, \dots, n\}$. For all $i \in \{1, \dots, n\}$, we will denote $t_{\mathcal{E}_i} = x$ and $\chi_{\mathcal{E}_i} = y_i$. Let $\sigma$ be a ground substitution such that $\text{dom}(\sigma) \subseteq \text{vars}(\mathcal{E}_1, \dots, \mathcal{E}_n)$ and let $\Phi$ be a ground frame such that $\mathcal{A}_{\mathcal{E} \text{signcrypt}} \notin \text{st}(\sigma, \Phi)$. Finally, let $I = \{i \in \{1, \dots, n\} \mid \Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash x_i\sigma\}$. We show that for all $i \in \{1, \dots, n\}$, Properties 1, 2, 3 and 6 of Definition 7 hold.

We first prove that for all term $t$ such that $\mathcal{A}_{\mathcal{E} \text{sign}} \notin \text{st}(t)$, $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_P t$ implies $\Phi \cdot [x_k\sigma]_{k \in I} \vdash t$. Assume that $P$ is minimal for $|P|$. We do a case analysis on $|P|$. If $|P| = 1$ then either $t \in \mathcal{N}_D \cup \mathcal{F}_{\text{cst}}$ or $t \in \Phi$ or $t = \mathcal{E}_k\sigma$ for some $k \in \{1, \dots, n\}$. But $\mathcal{A}_{\mathcal{E} \text{sign}} \notin \text{st}(t)$. Hence, we deduce that $t \in \mathcal{N}_D \cup \mathcal{F}_{\text{cst}}$ or $t \in \Phi$. Therefore, $\Phi \vdash t$ and so $\Phi \cdot [x_k\sigma]_{k \in I} \vdash t$.

Otherwise, $|P| > 1$. Let us assume that there exist $j \in \{1, \dots, n\}$ and $P' \in \text{st}(P)$ such that $P' = |\Phi| + j$. Since $|P| > 1$, we deduce that there exist ir, $P'', P_1, \dots, P_m$, $\ell \in \{1, \dots, m\}$ such that $P'' = \text{ir}(P_1, \dots, P_m) \in \text{st}(P)$ and $P_\ell = P'$. Let us denote $t''$ the term $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P''} t''$. By Lemma 19, we deduce that either $t'' \in \text{st}(\Phi) \cup \text{st}(\mathcal{E}_k\sigma)_{k=1}^n \cup \text{st}(t)$ or $t'' = g(u)$ for some $g \in \mathcal{F}_{\text{key}}$ and $u \in \text{st}_<(\Phi) \cup \text{st}_<(\mathcal{E}_k\sigma)_{k=1}^n \cup \text{st}_<(t)$. Since $\mathcal{A}_{\mathcal{E} \text{sign}} \notin \text{st}(t, \sigma, \Phi)$, $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P'} \mathcal{E}_j\sigma$ and all $\mathcal{E}_1, \dots, \mathcal{E}_n$ are equal after variable renaming, we deduce that in both cases, ir cannot be a composition rule. Since ir is a decomposition rule, we in fact have $P'' = \text{ir}(P', R)$ where ir the rule sign-decomp and $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_R \text{vk}(y_j\sigma)$. Moreover, we have $t'' = \langle \mathcal{A}_{\mathcal{E} \text{sign}}, x_j\sigma \rangle$. But it also implies that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash x_j\sigma$ meaning that $j \in I$ and so $\Phi \cdot [x_k\sigma]_{k \in I} \vdash \langle \mathcal{A}_{\mathcal{E} \text{sign}}, x_j\sigma \rangle$.

We have just shown that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$, a proof $Q_j$ and a term $u$ such that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P|_{p'_j}} u$ and $\Phi \cdot [x_k\sigma]_{k \in I} \vdash_{Q_j} u$. Therefore, by replacing all instances of $P|_{p'_j}$ in $P$ by $Q_j$, we obtain that a proof $P'$ such that $\Phi \cdot [x_k\sigma]_{k \in I} \vdash_{P'} t$. This allows us to conclude.

**Property 1:** For all $i \in \{1, \dots, n\}$, for all $t \in \mathcal{T}(\mathcal{F}_{\text{key}}, \{y_i\sigma\})$, we have that $\mathcal{A}_{\mathcal{E} \text{sign}} \notin \text{st}(t)$. Hence we can apply the property we just proved which allows us to conclude.

**Property 2:** Let $u \in \text{st}(\mathcal{E}_i) \setminus \mathcal{X}$ and $v \in \text{st}(\mathcal{E}_j) \setminus \mathcal{X}$ such that $u$ and $v$ are unifiable and $\text{root}(u) \neq \langle \rangle$. By definition of $\mathcal{E}_{\text{signcrypt}}$, $u, v$ unifiable implies that there exists a position $p$ of $\mathcal{E}_{\text{signcrypt}}$ such that $u = \mathcal{E}_i|_p$ and $v = \mathcal{E}_j|_p$. Since $\mathcal{E}_i \sim \mathcal{E}_j$ then the result holds.

**Property 3:** We directly have that $\{\text{sign}(\langle \mathcal{A}_{\mathcal{E} \text{sign}}, x \rangle, y), \text{vk}(y)\} \vdash x$.

**Property 6:** Let $i \in \{1, \dots, n\}$. Let $\sigma'$ some ground substitution such that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash \mathcal{E}_i\sigma'$. Consider a proof $P$ minimal for $|P|$ such that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_P \mathcal{E}_i\sigma'$. If $|P| = 1$ then it implies that $\mathcal{E}_i\sigma' \in [\mathcal{E}_k\sigma]_{k=1}^n$ due to the fact that $\mathcal{A}_{\mathcal{E} \text{sign}} \notin \text{st}(\Phi)$. Therefore, there exists $k \in \{1, \dots, n\}$ such that $\mathcal{E}_i\sigma' = \mathcal{E}_k\sigma$. Since we already know that $\mathcal{E}_i \sim \mathcal{E}_k$ then the result holds.

Otherwise $|P| > 1$. In such a case $P = \text{ir}(P_1, \dots, P_n)$. We do a case analysis on ir.

- Case ir is a decomposition rule: By Lemma 19, we deduce that $\mathcal{E}_i\sigma' \in \text{st}(\Phi) \cup \text{st}([\mathcal{E}_k\sigma]_{k=1}^n)$. But since $\mathcal{A}_{\mathcal{E} \text{sign}} \notin \text{st}(\Phi) \cup \text{st}(\sigma)$, then we deduce that $\mathcal{E}_i\sigma' \in [\mathcal{E}_k\sigma]_{k=1}^n$ which contradicts the minimality of $|P|$.
■ Case ir is a composition rule: In such a case, we have $P = \text{ir}(P_1, P_2)$ and $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_{P_1} \langle a_{\mathcal{E}\text{sign}}, x_i \sigma' \rangle$ and $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_{P_2} z_i \sigma'$. Using the first property of the lemma, the result holds.

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

## B.5 MAC encapsulation

**Lemma 24.** Let $\mathcal{A}_{\mathcal{E}\text{mac}} \in \text{Tag}$. Let $\mathcal{E}_{\text{mac}} = \langle x, h(\langle a_{\mathcal{E}\text{mac}}, x, y \rangle) \rangle$ with $t_{\mathcal{E}_{\text{mac}}} = x$ and $\chi_{\mathcal{E}_{\text{mac}}} = y$. We have that $(\mathcal{E}_{\text{mac}}, \emptyset)$ is a $\{a_{\mathcal{E}\text{mac}}\}$-tagged encapsulation and $S = \{(\mathcal{E}_{\text{mac}}, \emptyset)\}$ allows authentic channels.

**Proof.** Let $(\mathcal{E}_1, \emptyset), \dots, (\mathcal{E}_n, \emptyset) \in S$ such that the variables of $\mathcal{E}_1, \dots, \mathcal{E}_n$ are disjoints. Since $S = \{(\mathcal{E}_{\text{signcrypt}}, \text{vk}(y))\}$, we have that $\mathcal{E}_i \sim \mathcal{E}_j$ for all $i, j \in \{1, \dots, n\}$. For all $i \in \{1, \dots, n\}$, we will denote $t_{\mathcal{E}_i} = x$ and $\chi_{\mathcal{E}_i} = y_i$. Let $\sigma$ be a ground substitution such that $\text{dom}(\sigma) \subseteq \text{vars}(\mathcal{E}_1, \dots, \mathcal{E}_n)$ and let $\Phi$ be a ground frame such that $\mathcal{A}_{\mathcal{E}\text{mac}} \notin \text{st}(\sigma, \Phi)$. Finally, let $I = \{i \in \{1, \dots, n\} \mid \Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash x_i \sigma\}$. In fact we have $I = \{1, \dots, n\}$. We show that for all $i \in \{1, \dots, n\}$, Properties 1, 2, 3 and 6 of Definition 7 hold.

We first prove that for all term $t$ such that $\mathcal{A}_{\mathcal{E}\text{mac}} \notin \text{st}(t)$, $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_P t$ implies $\Phi \cdot [x_k \sigma]_{k \in I} \vdash t$. Assume that $P$ is minimal for $|P|$. We do a case analysis on $|P|$. If $|P| = 1$ then either $t \in \mathcal{N}_D \cup \mathcal{F}_{\text{est}}$ or $t \in \Phi$ or $t = \mathcal{E}_k \sigma$ for some $k \in \{1, \dots, n\}$. But $\mathcal{A}_{\mathcal{E}\text{mac}} \notin \text{st}(t)$. Hence, we deduce that $t \in \mathcal{N}_D \cup \mathcal{F}_{\text{est}}$ or $t \in \Phi$. Therefore, $\Phi \vdash t$ and so $\Phi \cdot [x_k \sigma]_{k \in I} \vdash t$.

Otherwise, $|P| > 1$. Let us assume that there exist $j \in \{1, \dots, n\}$ and $P' \in \text{st}(P)$ such that $P' = |\Phi| + j$. Since $|P| > 1$, we deduce that there exist $ir, P'', P_1, \dots, P_m, \ell \in \{1, \dots, m\}$ such that $P'' = \text{ir}(P_1, \dots, P_m) \in \text{st}(P)$ and $P_\ell = P'$. Let us denote $t''$ the term $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_{P''} t''$. By Lemma 19, we deduce that either $t'' \in \text{st}(\Phi) \cup \text{st}(\mathcal{E}_k \sigma)_{k=1}^n \cup \text{st}(t)$ or $t'' = g(u)$ for some $g \in \mathcal{F}_{\text{key}}$ and $u \in \text{st}_<(\Phi) \cup \text{st}_<(\mathcal{E}_k \sigma)_{k=1}^n \cup \text{st}_<(t)$. Since $\mathcal{A}_{\mathcal{E}\text{mac}} \notin \text{st}(t, \sigma, \Phi)$, $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_{P'} \mathcal{E}_j \sigma$ and all $\mathcal{E}_1, \dots, \mathcal{E}_n$ are equal after variable renaming, we deduce that in both cases, ir cannot be a composition rule. Since ir is a decomposition rule, we in fact have $P'' = \text{ir}(P')$ where ir is one of the decomposition of $\langle \rangle$, and so either $t'' = x_j \sigma$ or $t'' = h(\langle a_{\mathcal{E}\text{mac}}, x_j \sigma, y_j \sigma \rangle)$. If it is the latter then since $\mathcal{A}_{\mathcal{E}\text{mac}} \notin \text{st}(t)$, we deduce that $P \neq P''$ meaning that there exists $Q = \text{ir}'(Q_1, \dots, Q_\ell)$ and $\ell' \in \{1, \dots, \ell\}$ such that $Q \in \text{st}(P)$ and $Q_\ell' = P''$. But there is no decomposition rule for $h$ therefore $ir'$ is necessarily a composition rule.

By the Lemma 19, we can easily show that $ir'$ cannot be a composition rule for some $g \notin \mathcal{F}_{\text{key}}$ since if would imply that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_Q \mathcal{E}_r \sigma$ for some $r$ which would contradict our hypothesis on the minimality of $|P|$. We also show that $ir'$ cannot be a composition rule for some $g \in \mathcal{F}_{\text{key}}$. In such a case, it would imply that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_Q g(t'')$. But since $\mathcal{A}_{\mathcal{E}\text{mac}} \in \text{st}(t'')$, then $Q \neq P$ and so there must be another inference rule $ir''$ applied on $Q$ in $P$. Once again, by Lemma 19, $ir''$ cannot be a composition rule for any function symbol since it would imply that $g(t'') \in \text{st}(\Phi) \cup \text{st}([\mathcal{E}_k \sigma]_{k=1}^n) \cup \text{st}(t)$ but $\mathcal{E}_{\text{mac}}$ does not contain function symbol from $\mathcal{F}_{\text{key}}$ and $\mathcal{A}_{\mathcal{E}\text{mac}} \notin \text{st}(t, \sigma, \Phi)$. Moreover, $ir''$ cannot be a decomposition rule either since the only rule involving a function symbol $g \in \mathcal{F}_{\text{key}}$ as argument is the signature decomposition which would imply that there exists a term $\nu$ and a proof $R \in \text{st}(P)$ such that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_R \text{sign}(\nu, t'')$. Once again, this is prevented by Lemma 19. Therefore, we can conclude that $ir'$ cannot be a composition rule for some $g \in \mathcal{F}_{\text{key}}$.

We just have proven that if $t'' = h(\langle a_{\mathcal{E}\text{mac}}, x_j \sigma, y_j \sigma \rangle)$ then $ir'$ cannot be a composition nor a decomposition rule which is a contradiction. Hence $t'' = x_j \sigma$. Therefore, we have just shown that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$ and a proof $Q_j$ such that $\Phi \cdot [\mathcal{E}_k \sigma]_{k=1}^n \vdash_{P|_{p'_j}} x_j \sigma$ and $\Phi \cdot [x_k \sigma]_{k \in I} \vdash_{Q_j} x_{\sigma}$. Therefore, by replacing all instances of $P|_{p'_j}$ in $P$ by $Q_j$, we obtain that a proof $P'$ such that $\Phi \cdot [x_k \sigma]_{k \in I} \vdash_{P'} t$. This allows us to conclude.
**Property 1:** For all $i \in \{1, \dots, n\}$, for all $t \in \mathcal{T}(\mathcal{F}_{key}, \{y_i\sigma\})$, we have that $a_{\mathcal{E}_{\text{sign}}} \notin \text{st}(t)$. Hence we can apply the property we just proved which allows us to conclude.

**Property 2:** Let $u \in \text{st}(\mathcal{E}_i) \setminus \mathcal{X}$ and $v \in \text{st}(\mathcal{E}_j) \setminus \mathcal{X}$ such that $u$ and $v$ are unifiable and $\text{root}(u) \neq \langle \rangle$. By definition of $\mathcal{E}_{\text{signcrypt}}$, $u, v$ unifiable implies that there exists a position $p$ of $\mathcal{E}_{\text{signcrypt}}$ such that $u = \mathcal{E}_i|_p$ and $v = \mathcal{E}_j|_p$. Since $\mathcal{E}_i \sim \mathcal{E}_j$ then the result holds.

**Property 3:** We directly have that $\{\langle x, h(\langle a_{\mathcal{E}_{\text{mac}}}, x, y \rangle) \rangle\} \vdash x$.

**Property 6:** Let $i \in \{1, \dots, n\}$. Let $\sigma'$ some ground substitution such that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash \mathcal{E}_i\sigma'$. Consider a proof $P$ minimal for $|P|$ such that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_P \mathcal{E}_i\sigma'$. If $|P| = 1$ then it implies that $\mathcal{E}_i\sigma' \in [\mathcal{E}_k\sigma]_{k=1}$ due to the fact that $a_{\mathcal{E}_{\text{mac}}} \notin \text{st}(\Phi)$. Therefore, there exists $k \in \{1, \dots, n\}$ such that $\mathcal{E}_i\sigma' = \mathcal{E}_k\sigma$. Since we already know that $\mathcal{E}_i \sim \mathcal{E}_k$ then the result holds.

Otherwise $|P| > 1$. In such a case $P = \text{ir}(P_1, \dots, P_n)$. We do a case analysis on ir.

- Case ir is a decomposition rule: By Lemma 19, we deduce that $\mathcal{E}_i\sigma' \in \text{st}(\Phi) \cup \text{st}([\mathcal{E}_k\sigma]_{k=1}^n)$. But since $a_{\mathcal{E}_{\text{mac}}} \notin \text{st}(\Phi) \cup \text{st}(\sigma)$, then we deduce that $\mathcal{E}_i\sigma' \in [\mathcal{E}_k\sigma]_{k=1}^n$ which contradicts the minimality of $|P|$.

- Case ir is a composition rule: In such a case, we have $P = \text{ir}(P_1, P_2)$ and $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P_1} x_i\sigma'$ and $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P_2} h(\langle a_{\mathcal{E}_{\text{mac}}}, x_i\sigma', y_i\sigma' \rangle)$. Let us focus on $P_2$. Since $a_{\mathcal{E}_{\text{mac}}} \notin \text{st}(\Phi, \sigma)$, we have that $P_2$ starts by either a decomposition rule or a composition rule. If it is the latter then we have that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash y\sigma'$ and so the result would hold with the first property of the lemma. If it is the former, then by Lemma 19, we would have that $h(\langle a_{\mathcal{E}_{\text{mac}}}, x_i\sigma', y_i\sigma' \rangle) \in \text{st}([\mathcal{E}_k\sigma]_{k=1}^n)$. It would imply that there exists $k \in \{1, \dots, n\}$ such that $x_k\sigma = x_i\sigma'$ and $y_k\sigma = y_i\sigma'$. Hence with the first property of the lemma, the result holds.

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

## B.6 Aenc encapsulation

**Lemma 25.** Let $a_{\mathcal{E}_{\text{aenc}}} \in \text{Tag}$. Let $\mathcal{E}_{\text{TLS}} = \text{aenc}(\langle a_{\mathcal{E}_{\text{aenc}}}, x \rangle, \text{pk}(y))$, $t_{\mathcal{E}_{\text{aenc}}} = x$ and $X_{\mathcal{E}_{\text{aenc}}} = y$. We have that $(\mathcal{E}_{\text{aenc}}, \text{pk}(y))$ is a $\{a_{\mathcal{E}_{\text{aenc}}}\}$-tagged encapsulation and $S = \{(\mathcal{E}_{\text{TLS}}, \text{pk}(y))\}$ allows confidential channels.

**Proof.** Let $(\mathcal{E}_1, \emptyset), \dots, (\mathcal{E}_n, \emptyset) \in S$ such that the variables of $\mathcal{E}_1, \dots, \mathcal{E}_n$ are disjoints. Since $S = \{(\mathcal{E}_{\text{TLS}}, \emptyset)\}$, we have that $\mathcal{E}_i \sim \mathcal{E}_j$ for all $i, j \in \{1, \dots, n\}$. For all $i \in \{1, \dots, n\}$, we will denote $t_{\mathcal{E}_i} = x_i$ and $X_{\mathcal{E}_i} = y_i$. Let $\sigma$ be a ground substitution such that $\text{dom}(\sigma) \subseteq \text{vars}(\mathcal{E}_1, \dots, \mathcal{E}_n)$ and let $\Phi$ be a ground frame such that $a_{\mathcal{E}_{\text{aenc}}} \notin \text{st}(\sigma, \Phi)$. Finally, let $I = \{i \in \{1, \dots, n\} \mid \Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash x_i\sigma\}$. We show that for all $i \in \{1, \dots, n\}$, Properties 1, 2, 4 and 5 of Definition 7 hold.

**Property 1:** Let $i \in \{1, \dots, n\}$. Let $t \in \mathcal{T}(\mathcal{F}_{key}, \{y_i\sigma\})$ such that $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_P t$. Assume that $P$ is minimal for $|P|$. We do a case analysis on $|P|$. If $|P| = 1$ then either $t \in \mathcal{N}_D \cup \mathcal{F}_{cst}$ or $t \in \Phi$ or $t = \mathcal{E}_k\sigma$ for some $k \in \{1, \dots, n\}$. But $a_{\mathcal{E}_{\text{TLS}}} \notin \text{st}(t)$. Hence, we deduce that $t \in \mathcal{N}_D \cup \mathcal{F}_{cst}$ or $t \in \Phi$. Therefore, $\Phi \vdash t$ and so $\Phi \cdot [x_k\sigma]_{k \in I} \vdash t$.

Otherwise, $|P| > 1$. Let us assume that there exists $j \in \{1, \dots, n\}$ and $P' \in \text{st}(P)$ such that $P' = |\Phi| + j$. Since $|P| > 1$, we deduce that there exists ir, $P'', P_1, \dots, P_m$, $\ell \in \{1, \dots, m\}$ such that $P'' = \text{ir}(P_1, \dots, P_m) \in \text{st}(P)$ and $P_\ell = P'$. Let us denote $t''$ the term $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P''} t''$. By Lemma 19, we deduce that either $t'' \in \text{st}(\Phi) \cup \text{st}(\mathcal{E}_k\sigma)_{k=1}^n \cup \text{st}(t)$ or $t'' = g(u)$ for some $g \in \mathcal{F}_{key}$ and $u \in \text{st}_<(\Phi) \cup \text{st}_<(\mathcal{E}_k\sigma)_{k=1}^n \cup \text{st}_<(t)$. Since $a_{\mathcal{E}_{\text{aenc}}} \notin \text{st}(t, \sigma, \Phi)$, $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P'} \mathcal{E}_j\sigma$ and all $\mathcal{E}_1, \dots, \mathcal{E}_n$ are equal after variable renaming, we deduce that in both cases, ir cannot be a composition rule. Therefore ir is the decomposition rule of aenc and we have $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P''} \langle a_{\mathcal{E}_{\text{aenc}}}, x_j\sigma \rangle$. Thus $\Phi \cdot [\mathcal{E}_k\sigma]_{k=1}^n \vdash_{P''} \langle x_j\sigma \text{ and so } j \in I \rangle$. Hence, $\Phi \cdot [x_k\sigma]_{k \in I} \vdash \langle a_{\mathcal{E}_{\text{TLS}}}, x_j\sigma \rangle$.
We have just shown that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$, a proof $Q_j$ and a term $u$ such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{P|_{p'_j}} u$ and $\Phi \cdot [x_k \sigma]_{k \in I} \vdash_{Q_j} u$. Therefore, by replacing all instances of $P|_{p'_j}$ in $P$ by $Q_j$, we obtain that a proof $P'$ such that $\Phi \cdot [x_k \sigma]_{k \in I \vdash P'} t$. This allows us to conclude.

**Property 2:** Let $u \in st(\varepsilon_i) \setminus X$ and $v \in st(\varepsilon_j) \setminus X$ such that $u$ and $v$ are unifiable and root($u$) $\neq \langle\rangle$. By definition of $\varepsilon_{aenc}$, $u, v$ unifiable implies that there exists a position $p$ of $\varepsilon_{TLS}$ such that $u = \varepsilon_i|_p$ and $v = \varepsilon_j|_p$. Since $\varepsilon_i \sim \varepsilon_j$ then the result holds.

**Property 4:** Let $i \in \{1, \dots, n\}$. Consider a minimal proof $P$ for $|P|$ such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_P x_i \sigma$. We do a case analysis on $|P|$. If $|P| = 1$ then either $x_i \sigma \in N_D \cup \mathcal{F}_{cst}$ or $x_i \sigma \in \Phi$ or $x_i \sigma = \varepsilon_k \sigma$ for some $k \in \{1, \dots, n\}$. But $\varepsilon_{aenc} \notin st(x_i \sigma)$. Hence, we deduce that $x_i \sigma \in N_D \cup \mathcal{F}_{cst}$ or $x_i \sigma \in \Phi$. Therefore, $\Phi \vdash x_i \sigma$ and so $\Phi \cdot [x_k \sigma]_{k \in I-i} \vdash x_i \sigma$.

Otherwise, $|P| > 1$. Following exactly the proof of Property 1 (replacing $t$ by $x_i \sigma$), we deduce that for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, if $P|_{p_j} = |\Phi| + j$ then there exists a prefix $p'_j$ of $p_j$, a proof $Q_j$ such that $P|_{p'_j} = \text{ir}_1(|\Phi| + j, Q_j)$, $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{P|_{p'_j}} \langle \varepsilon_{TLS}, x_j \sigma \rangle$ and $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_{Q_j} y_j \sigma$ where $\text{ir}_1$ is the decomposition rule of $aenc$. Let us look at the proof $Q_j$. Since $\varepsilon_{aenc} \notin st(y_j \sigma)$, we can deduce by minimality of $|P|$ that $|\Phi| + j \notin Q_j$ (otherwise, using the same reasoning, it would imply that there exists a proof $Q'_j \in st(Q_j)$ deducing $y_i \sigma$). Thus, $\Phi \cdot [\varepsilon_k \sigma]_{k \in \{1, \dots, n\}-j} \vdash_{Q_j} y_j \sigma$. Let $I' = \{i \in \{1, \dots, n\} - j \mid \Phi \cdot [\varepsilon_k \sigma]_{k \in \{1, \dots, n\}-j} \vdash x_i \sigma\}$. Note that $I' \subseteq I - j$. By applying Property 1 on $y_j \sigma$ with $[\varepsilon_k \sigma]_{k \in \{1, \dots, n\}-j}$ and $I'$, we deduce that $\Phi \cdot [x_k \sigma]_{k \in I'} \vdash y_j \sigma$.

Therefore, we have proven that if $|\Phi| + i \in st(P)$ then $\Phi \cdot [x_k \sigma]_{k \in I-i} \vdash y_i \sigma$. Otherwise, if for all $j \in \{1, \dots, n\}$, for all position $p_j$ of $P$, $P|_{p_j} = |\Phi| + j$ implies that $i \neq j$ then we also have proven that $\Phi \cdot [x_k \sigma]_{k \in I-i} \vdash x_j \sigma$ using the same replacement of proofs as in the proof of Property 1. Hence, the result holds.

**Property 5:** Let $i \in \{1, \dots, n\}$. Let $\sigma'$ be some ground substitution such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash \varepsilon_i \sigma'$ and $\varepsilon_{aenc} \notin st(\sigma')$. We focus first on the left implication of the equivalence. If $\Phi \cdot [x_k \sigma]_{k \in I} \vdash x_i \sigma'$ and $\Phi \cdot [x_k \sigma]_{k \in I} \vdash \text{pk}(y_i) \sigma'$ then we directly have that $\Phi \cdot [x_k \sigma]_{k \in I} \vdash \varepsilon_i \sigma'$. But since for all $k \in I$, $\Phi \cdot [\varepsilon_k \sigma]_{k \in \{1, \dots, n\}} \vdash x_k \sigma$, we deduce that $\Phi \cdot [\varepsilon_k \sigma]_{k \in \{1, \dots, n\}} \vdash \varepsilon_i \sigma'$. Otherwise, there exists $j \in \{1, \dots, n\}$ such that $\varepsilon_i \sigma' = \varepsilon_j \sigma$ and so we directly have that $\Phi \cdot [\varepsilon_k \sigma]_{k \in \{1, \dots, n\}} \vdash \varepsilon_i \sigma'$.

Let us now focus on the right implication of the equivalence. Consider a proof $P$ minimal for $|P|$ such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash_P \varepsilon_i \sigma'$. If $|P| = 1$ then it implies that $\varepsilon_i \sigma' \in [\varepsilon_k \sigma]_{k=1}^n$ due to the fact that $\varepsilon_{aenc} \notin st(\Phi)$. Therefore, there exists $k \in \{1, \dots, n\}$ such that $\varepsilon_i \sigma' = \varepsilon_k \sigma$. Since we already know that $\varepsilon_i \sim \varepsilon_k$ then the result holds.

Otherwise $|P| > 1$. In such a case $P = \text{ir}(P_1, \dots, P_n)$. We do a case analysis on ir.

- Case ir is a decomposition rule: by Lemma 19, we deduce that $\varepsilon_i \sigma' \in st(\Phi) \cup st([\varepsilon_k \sigma]_{k=1}^n)$. But since $\varepsilon_{aenc} \notin st(\Phi) \cup st(\sigma)$, then we deduce that $\varepsilon_i \sigma' \in [\varepsilon_k \sigma]_{k=1}^n$ which contradicts the minimality of $|P|$.

- Case ir is a composition rule: Then we directly have that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash x_i \sigma'$ and $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash \text{pk}(y_i \sigma')$. Once again by following the same proof as in Property 1 (replacing $t$ by $x_i \sigma'$), we deduce that $\Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I} \vdash x_i \sigma'$ and $\Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I} \vdash \text{pk}(y_i \sigma')$ and so the result holds.

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

## B.7 Proof of Theorem 8

**Lemma 26.** Let $S_e$ be a set of Tag-encapsulations allowing authentic, confidential and secure channels. Let $\Phi$ be a ground frame and $\sigma$ be a ground substitution such that Tag $\cap$ st($\sigma$, $\Phi$) = $\emptyset$. Let $(\varepsilon_1, F_1), \dots, (\varepsilon_n, F_n) \in S_e$. Assume that the variables in $\varepsilon_1, \dots, \varepsilon_n$ are disjoint. Let $I$ be the set of
$i \in \{1, \dots, n\}$ such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t_{\varepsilon_i} \sigma$. For all terms $t$, if $\text{Tag} \cap \text{st}(t) = \emptyset$ and $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t$ then $\Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I} \vdash t$.

**Proof.** Consider $(\varepsilon_{n+1}, F_{n+1}) \in S_e$ such that the variables of $\varepsilon_{n+1}$ are disjoint from $\varepsilon_1, \dots, \varepsilon_n$. Take $\sigma'$ the ground substitution such that $t_{\varepsilon_{n+1}} \sigma' = a \in \mathcal{N}_D$ and for all $x \in \chi_{\varepsilon_{n+1}}$, $x\sigma' = t$. Since $\text{Tag} \cap \text{st}(t) = \emptyset$, we deduce that $\text{Tag} \cap \text{st}(\sigma\sigma') = \emptyset$. Moreover, we have $t \in \mathcal{T}(\mathcal{F}_{\mathcal{Key}}, \chi_{\varepsilon_{n+1}}\sigma\sigma')$.

We also that that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t$ implies that $\Phi \cdot [\varepsilon_k \sigma \sigma']_{k=1}^n \vdash t$ which implies $\Phi \cdot [\varepsilon_k \sigma \sigma']_{k=1}^{n+1} \vdash t$. On the other hand, since $a \in \mathcal{N}_D$ and for all $x \in \chi_{\varepsilon_{n+1}}$, $x\sigma' = t$ with $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t$, we deduce that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash \varepsilon_{n+1} \sigma'$. Hence for all $i \in \{1, \dots, n\}$, if $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t_{\varepsilon_i} \sigma$ then $\Phi \cdot [\varepsilon_k \sigma \sigma']_{k=1}^{n+1} \vdash t_{\varepsilon_i} \sigma$.

Thus by applying Property 1 of Definition 7, we deduce that $\Phi \cdot [t_{\varepsilon_k} \sigma \sigma']_{k \in I} \vdash t$ and so $\Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I} \vdash t$. $\quad \blacksquare$

**▶ Lemma 27.** Let $S_e$ be a set of $\text{tag}_A$-encapsulations allowing authentic, confidential and secure channels. Let $S'_e$ be a set of $\text{tag}_B$-encapsulations allowing authentic, confidential and secure channels. If $\text{tag}_A \cap \text{tag}_B = \emptyset$ then $S_e \cup S'_e$ is a set of $\text{tag}_A \cup \text{tag}_B$-encapsulations allowing authentic, confidential and secure channels.

**Proof.** Let $(\varepsilon_1, F_1), \dots, (\varepsilon_n, F_n) \in S_e \cup S'_e$. Assume that the variables in $\varepsilon_1, \dots, \varepsilon_n$ are disjoint. Let $\sigma$ be a ground substitution such that $\text{dom}(\sigma) = \text{vars}(\varepsilon_1, \dots, \varepsilon_n)$ and let $\Phi$ be a ground frame such that $(\text{tag}_A \cup \text{tag}_B) \cap \text{st}(\sigma, \Phi) = \emptyset$. Let $I$ be the set of $i \in \{1, \dots, n\}$ such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t_{\varepsilon_i} \sigma$. Let us denote by $A = \{i \in \{1, \dots, n\} \mid (\varepsilon_i, F_i) \in S_e\}$ and $B = \{i \in \{1, \dots, n\} \mid (\varepsilon_i, F_i) \in S'_e\}$. Moreover, let us denote by $I_A = I \cap A$ and $I_B = I \cap B$. We first start proving the following property:

**Property 0:** For all term $t$, if $(\text{tag}_A \cup \text{tag}_B) \cap \text{st}(t) = \emptyset$ and $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t$ then $\Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I} \vdash t$. Assume w.l.o.g. that $i \in A$. Let us denote $\Phi' = \Phi \cdot [\varepsilon_k \sigma]_{k \in B}$. We have $\Phi' \cdot [\varepsilon_k \sigma]_{k \in A} \vdash t$. But $(\text{tag}_A \cup \text{tag}_B) \cap \text{st}(\sigma, \Phi) = \emptyset$ and so $\text{tag}_A \cap \text{st}(\sigma, \Phi) = \emptyset$. Moreover, $I_A$ is the set of $i \in A$ such that $\Phi' \cdot [\varepsilon_k \sigma]_{k \in A} \vdash t_{\varepsilon_i} \sigma$. Since $S_e$ be a set of $\text{tag}_A$-encapsulations allowing authentic, confidential and secure channels, we deduce by Lemma 26 that $\Phi' \cdot [t_{\varepsilon_k} \sigma]_{k \in I_A} \vdash t$.

If now we denote $\Phi'' = \Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I_A}$, we obtain that $\Phi'' \cdot [\varepsilon_k \sigma]_{k \in B} \vdash t$. Consider the set $I'_B$ of $i \in B$ such that $\Phi'' \cdot [\varepsilon_k \sigma]_{k \in B} \vdash t_{\varepsilon_i} \sigma$. We show that $I'_B = I_B$. If $i \in I_B$ then we know that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t_{\varepsilon_i} \sigma$. By applying once again Lemma 26 on $\Phi'$, $A$ and $I_A$, we deduce that $\Phi' \cdot [t_{\varepsilon_k} \sigma]_{k \in I_A} \vdash t_{\varepsilon_i} \sigma$ and so $\Phi'' \cdot [\varepsilon_k \sigma]_{k \in B} \vdash t_{\varepsilon_i} \sigma$ meaning that $i \in I'_B$. If $i \in I'_B$, we know that $\Phi'' \cdot [\varepsilon_k \sigma]_{k \in B} \vdash t_{\varepsilon_i} \sigma$ and so $\Phi' \cdot [t_{\varepsilon_k} \sigma]_{k \in I_A} \vdash t_{\varepsilon_i} \sigma$. But for all $j \in I_A$, $\Phi' \cdot [\varepsilon_k \sigma]_{k \in A} \vdash t_{\varepsilon_j} \sigma$. Hence we deduce that $\Phi'' \cdot [\varepsilon_k \sigma]_{k \in A} \vdash t_{\varepsilon_i} \sigma$ and so $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t_{\varepsilon_i} \sigma$. This allows us to conclude that $I_B = I'_B$. Thus, we can apply Lemma 26 on $\Phi''$, $I_B$ and $t$ which allows us to deduce that $\Phi'' \cdot [t_{\varepsilon_k} \sigma]_{k \in I_B} \vdash t$ and so we conclude that $\Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I} \vdash t$.

**Property 1:** Direct application of Property 0.

**Property 2:** Let $i, i' \in \{1, \dots, n\}$. Let $u \in \text{st}(\varepsilon_i) \setminus \mathcal{X}$ and let $v \in \text{st}(\varepsilon_{i'}) \setminus \mathcal{X}$ such that $u$ and $v$ are unifiable and $\text{root}(u) \neq \langle \rangle$. Thus $\text{tag}_A \cap \text{tag}_B = \emptyset$, we deduce that either $i, i' \in A$ or $i, i' \in B$. In such a case the result directly holds by applying Property 2 of Definition 7 on either A or B.

**Property 3:** Direct from Definition 7.

**Property 4:** Let $i \in \{1, \dots, n\}$ such that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t_{\varepsilon_i} \sigma$. Assume w.l.o.g. that $i \in A$. Let us denote $\Phi' = \Phi \cdot [\varepsilon_k \sigma]_{k \in B}$. Thus by applying Property 4 of Definition 7 on $\Phi'$, $\sigma$, $I_A$, we deduce that $\Phi' \cdot [t_{\varepsilon_k} \sigma]_{k \in I_A - i} \vdash t_{\varepsilon_i} \sigma$ or there exists $x \in \chi_{\varepsilon_i}$ such that $\Phi' \cdot [t_{\varepsilon_k} \sigma]_{k \in I_A - i} \vdash x\sigma$.

Let us $\Phi'' = \Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I_A - i}$. Consider $I'_B$ the set of $j \in B$ such that $\Phi'' \cdot [\varepsilon_k \sigma]_{k \in B} \vdash t_{\varepsilon_j} \sigma$. We know that for all $k \in I_A - i$, $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t_{\varepsilon_k} \sigma$. Therefore, we deduce that $\Phi \cdot [\varepsilon_k \sigma]_{k=1}^n \vdash t_{\varepsilon_j} \sigma$ and so $I'_B \subseteq I_B$. Hence by applying Lemma 26 on $\Phi''$, $I'_B$ and $x\sigma$ or $t_{\varepsilon_i} \sigma$, we deduce that $\Phi'' \cdot [t_{\varepsilon_k} \sigma]_{k \in I'_B} \vdash x\sigma$ or $\Phi'' \cdot [t_{\varepsilon_k} \sigma]_{k \in I'_B} \vdash t_{\varepsilon_i} \sigma$. But considering that $I'_B \subseteq I_B$, we deduce that $\Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I - i} \vdash x\sigma$ or $\Phi \cdot [t_{\varepsilon_k} \sigma]_{k \in I - i} \vdash t_{\varepsilon_i} \sigma$. Hence the result holds.
Property 5 and 6: Similar proof as Property 4, that is we assume w.l.o.g. that $i \in A$, we apply Property 5 (resp. 6) on the frame $\Phi' = \Phi \cdot [\mathcal{E}_k\sigma]_{k \in B}$ and $I_A$, and when we are in the case of $\Phi' \cdot [t_{\mathcal{E}_k}\sigma]_{k \in I_A}$ deduces a term $u$, we use Lemma 26 on $\Phi'' = \Phi \cdot [t_{\mathcal{E}_k}\sigma]_{k \in I_A}$, $I_B$ and $u$ to obtain that $\Phi \cdot [t_{\mathcal{E}_k}\sigma]_{k \in I}$ deduce $u$. ◀

**▶ Theorem 8.** The following encapsulations are:

**authentic:** $\mathcal{E}_{\text{sign}} = \text{sign}(\langle a_{\mathcal{E}_{\text{sign}}}, x \rangle, x_1)$ and $\mathcal{E}_{\text{mac}} = \langle x, h(\langle a_{\mathcal{E}_{\text{mac}}}, x, x_1 \rangle) \rangle$;

**confidential:** $\mathcal{E}_{\text{aenc}} = \text{aenc}(\langle a_{\mathcal{E}_{\text{aenc}}}, x \rangle, \text{pk}(x_1))$;

**secure:** $\mathcal{E}_{\text{TLS}} = \text{senc}(\langle a_{\mathcal{E}_{\text{TLS}}}, x \rangle, x_1)$, $\mathcal{E}_{\text{BAC}} = \langle t, \text{mac}(\langle a_{\mathcal{E}_{\text{BAC}}}, t \rangle, x_2) \rangle$ with $t = \text{senc}(\langle a_{\mathcal{E}_{\text{BAC}}}, x \rangle, x_1)$, and $\mathcal{E}_{\text{signcrypt}} = \text{sign}(\langle a_{\mathcal{E}_{\text{signcrypt}}}, a_{\text{enc}}(\langle a_{\mathcal{E}_{\text{signcrypt}}}, x \rangle, \text{pk}(x_1)) \rangle, x_2)$.

where $a_{\mathcal{E}_{\text{sign}}}, a_{\mathcal{E}_{\text{mac}}}, a_{\mathcal{E}_{\text{aenc}}}, a_{\mathcal{E}_{\text{TLS}}}, a_{\mathcal{E}_{\text{BAC}}}, a_{\text{signcrypt}}$ are constants.

Moreover, the set $\{(\mathcal{E}_{\text{sign}}, \{vk(x_1)\}), (\mathcal{E}_{\text{mac}}, \emptyset), (\mathcal{E}_{\text{aenc}}, \{\text{pk}(x_1)\}), (\mathcal{E}_{\text{TLS}}, \emptyset), (\mathcal{E}_{\text{BAC}}, \emptyset), (\mathcal{E}_{\text{signcrypt}}, \emptyset)\}$ allows for authentic, confidential and secure channels.

**Proof.** Lemmas 20, 21, 22, 23, 25 and 24 give us that the encapsulations individually allows secure, confidential, authentic channels. Thus the proof is concluded by successive applications of Lemma 27 since all the encapsulations are tagged differently. ◀

# C Proofs of Theorem 17

## C.1 Properties on the composed frame

We say that a term $t$ is a tag$_A$-term if $t = f(\langle a, t_1 \rangle, t_2, \dots, t_n)$ where $a \in \text{tag}_A$ for some $t_1, \dots, t_n$.

**▶ Definition 28.** Let $S$ be a set of tag$_A$-tagged encapsulations. Let $\Phi = [u_1; \dots; u_n]$ be a frame. Let $I \subseteq \{1, \dots, n\}$. We say that $\Phi$ is an executed frame for $S$ and $I$ if:

- for all $i \in I$, $u_i = \mathcal{E}_i \Sigma_i$ for some ground substitutions $\Sigma_i$ and some encapsulation $(\mathcal{E}_i, F_i) \in S$; and

- for all $i \in I$ (resp. $i \notin I$), for all $t \in \text{vars}(\mathcal{E}_i) \Sigma_i$ (resp. $t \in \{u_i\}$), for all positions $p$ of $t$, if $t|_p$ is a tag$_A$-term then:

- either $p = p' \cdot a \cdot p''$ for some position $p'$, $p''$ and there exists $j \in I$ such that $j < i$, $t|_{p' \cdot a}$, $t|_p \in \text{st}(\mathcal{E}_j \Sigma_j) \setminus \text{st}(\Sigma_j)$ and $[u_1; \dots; u_{i-1}] \vdash t|_{p' \cdot a}$;

- or $[u_1; \dots; u_{i-1}] \vdash t|_p$.

**▶ Corollary 29.** Let $S$ be a set of tag$_A$-tagged encapsulations. Let $\Phi = [u_1; \dots; u_n]$ be an executed frame for $S$ and some set $I$. For all $k \in \{1, \dots, n\}$, $[u_1; \dots; u_k]$ is an executed frame for $S$ and $I \setminus \{k+1; \dots; n\}$.

In the rest of the section, if $\Phi = [u_1; \dots; u_n]$ is an executed frame for $S$ and $I$ then for all $i \in I$, we will always denote by $\mathcal{E}_i \Sigma_i$ the term $u_i$ as described in the above definition.

**▶ Lemma 30.** Let $S$ be a set tag$_A$-tagged encapsulations. Let $\Phi$ be a frame and $I \subseteq \{1, \dots, |\Phi|\}$. Assume that $\Phi$ is an executed frame for $S$ and $I$. We have that for all $t \in \mathcal{T}(\mathcal{F}, \mathcal{N})$, if $\Phi \vdash t$ then for all positions $p$ of $t$, if $t|_p$ is a tag$_A$-term then:

- either $p = p' \cdot a \cdot p''$ for some position $p'$, $p''$ and there exists $j \in I$ such that $j \in \text{st}(\mathcal{E}_j \Sigma_j) \setminus \text{st}(\Sigma_j)$ and $\Phi \vdash t|_{p' \cdot a}$;

- or $\Phi \vdash t|_p$.
**Proof.** Let us denote by $P$ the minimal proof such that $\Phi \vdash_P t$. Let us denote $\Phi = [u_1; \dots; u_n]$. We prove this result by induction $|P|$.

*Base case* $|P| = 1$: In such a case, either $t \in \mathcal{N}_D$ or there exists $i \notin I$ such that $t = u_i$ or there exists $i \in I$ such that $t = \mathcal{E}_i \Sigma_i$. However, in the first case, the result trivially holds.

In the second case, by Definition 28, we know that for all positions $p$ of $t$, if $t|_p$ is a tag$_A$-term then:

- either $p = p' \cdot a \cdot p''$ for some position $p'$, $p''$ and there exists $j \in I$ such that $j < i$, $t|_{p'a}$, $t|_p \in st(\mathcal{E}_j \Sigma_j) \setminus st(\Sigma_j)$ and $[u_1; \dots; u_{i-1}] \vdash t|_{p'a}$ which implies that $\Phi \vdash t|_{p'a}$

- or $[u_1; \dots; u_{i-1}] \vdash t|_p$ which implies that $\Phi \vdash t|_p$.

Therefore the result holds.

In the third case, for all positions $p$ of $\mathcal{E}_i \Sigma_i$, we distinguish whether $t|_p \in st(\mathcal{E}_i \Sigma_i) \setminus st(\Sigma_i)$ or not. In the latter, it implies that $t|_p \in st(\Sigma_i)$ and so there exists $t' \in \text{vars}(\mathcal{E}_i) \Sigma_i$ and a position $p'$ such that $t'|_{p'} = t|_p$ and $p'$ is a suffix or $p$. Therefore, by Definition 28 (instantiating $t$ and $p$ of the definition by $t'$ and $p'$ respectively), we obtain that if $t'|_{p'}$ is a tag$_A$-term then:

- either $p' = p'' \cdot a \cdot p'''$ for some position $p''$, $p'''$ and there exists $j \in I$ such that $j < i$, $t'|_{p'' \cdot a}$, $t'|_{p'} \in st(\mathcal{E}_j \Sigma_j) \setminus st(\Sigma_j)$ and $[u_1; \dots; u_{i-1}] \vdash t|_{p'' \cdot a}$. Since $p'$ is a suffix of $p$ then $p = q \cdot p'$ for some $q$. And so we obtain that $p = (q \cdot p'') \cdot a \cdot p'''$, $t|_{(q \cdot p'') \cdot a}$, $t|_p \in st(\mathcal{E}_j \Sigma_j) \setminus st(\Sigma_j)$ and $\Phi \vdash t|_p$. Hence the result holds.

- or $[u_1; \dots; u_{i-1}] \vdash t|_p$ which implies that $\Phi \vdash t|_p$.

In the former case, that is $t|_p \in st(\mathcal{E}_j \Sigma_j) \setminus st(\Sigma_j)$, the result directly holds since $t = \mathcal{E}_i \Sigma_i$ and $\Phi \vdash t$.

*Inductive step* $|P| > 1$ and the last rule of P is a composition: In such a case, $t = f(t_1, \dots, t_m)$ and for all $i \in \{1, \dots, m\}$, $\Phi \vdash t_i$. Therefore, we can apply our inductive hypothesis on all $t_1, \dots, t_n$ which allows us to conclude for all position $p$ of $t$ different from $\varepsilon$. However, in the case where $p = \varepsilon$, we know by hypothesis that $\Phi \vdash t$ and so the result trivially holds.

*Inductive step* $|P| > 1$ and the last rule of P is a decomposition: Since $P$ is minimal, we know that there exists $i \in \{1, \dots, n\}$ such that $t \in st(u_i)$. Thus, we can apply the same reasoning as in the base case $|P| = 1$. This allows us to conclude. $\quad$

**Definition 31.** Let $S$ be a set tag$_A$-tagged encapsulations. Let $\Phi$ be a frame and $I \subseteq \{1, \dots, |\Phi|\}$. Assume that $\Phi$ is an executed frame for $S$ and $I$. Let $\sigma$ be a substitution. We say that $\sigma$ is an executed substitution for $\Phi$ if for all $t \in \text{img}(\sigma)$, for all positions $p$ of $t$, if $t|_p$ is a tag$_A$-term then:

- either $p = p' \cdot a \cdot p''$ for some position $p'$, $p''$ and there exists $j \in I$ such that $t|_{p'a}$, $t|_p \in st(\mathcal{E}_j \Sigma_j) \setminus st(\Sigma_j)$ and $\Phi \vdash t|_{p'a}$;

- or $\Phi \vdash t|_p$.

## C.2 Transformation on composition frame and encapsulations

**Definition 32.** Let $\delta$ be a mapping from terms to nonces. We define the application of $\delta$ on a term $u$, denoted $\mathsf{Ap}_\delta(u)$, as follows:

- if $u \in \text{dom}(\delta)$ then $\mathsf{Ap}_\delta(u) = u^\delta$;

- else if $u \in \mathcal{N} \cup \mathcal{X}$ then $\mathsf{Ap}_\delta(u) = u$;

- else $u = f(u_1, \dots, u_n)$ and $\mathsf{Ap}_\delta(u) = f(\mathsf{Ap}_\delta(u_1), \dots, \mathsf{Ap}_\delta(u_n))$ for some $f$, $u_1, \dots, u_n$.

**Definition 33.** We say that $\delta$ is a tag$_A$-mapping of a frame $\Phi$ when $\text{names}(\Phi) \cap \text{img}(\delta) = \emptyset$, $\text{img}(\delta) \in \mathcal{N}_D$ and $\text{dom}(\delta) \supseteq \{t \in st(\Phi) \mid t$ is a tag$_A$-term$\}$.
**Lemma 34.** Let $\mathcal{S}$ be a set of tag_A-encapsulations allowing authentic, confidential and secure channels. Let $(\mathcal{E}, \ell, \mathcal{S}) \in \mathcal{S}$. For all substitution $\Sigma$, for all tag_A-mapping $\delta$ of $[\mathcal{E}\Sigma]$, for all position $p$ of $\mathcal{E}$, there exists a context $C[\_\cdot]$ built on $\{(\cdot)\} \cup \mathcal{F}_{\text{cst}}$ (possibly just a hole) such that

* $\mathcal{E}\Sigma|_p = C[u_1, \dots, u_n]$;

* for all $i \in \{1, \dots, n\}$, $u_i$ is either a tag_A-term of $\text{dom}(\delta)$ or $u_i \in \text{vars}(\mathcal{E})\Sigma$ or a term of the form $f(v)$ for some $f \in \mathcal{F}_{\text{key}}$ and $v \in \mathcal{X}_{\mathcal{E}\Sigma} \cup \mathcal{F}_{\text{cst}}$.

* $\text{Ap}_\delta(\mathcal{E}\Sigma|_p) = C[\text{Ap}_\delta(u_1), \dots, \text{Ap}_\delta(u_n)]$;

* $\mathcal{E}\text{Ap}_\delta(\Sigma)|_p = C[v_1, \dots, v_n]$;

* for all $i \in \{1, \dots, \ell\}$, $u_i$ is (resp. not) a tag_A-term implies $v_i$ is a tag_A-term (resp. $v_i = \text{Ap}_\delta(u_i)$).

**Proof.** By Definition 5, we know that $\mathcal{E}$ is a fully tag_A-term of $\mathcal{T}(\mathcal{F}, \{x, x_1, \dots, x_n\})$ such that for all $t \in \text{st}(\mathcal{E})$,

* if $\text{root}(t) = f \in \mathcal{F}_{\text{key}}$ then $t = f(y)$ with $y \in \{x_1, \dots, x_n\} \cup \mathcal{F}_{\text{cst}}$

* if $t = f(t', t_1, \dots, t_n)$ and there exists an inference rule $ir(f(y, u_1, \dots, u_n), v_1, \dots, v_m) \to y$ then for all $j \in \{1, \dots, m\}$, for all $i \in \{1, \dots, n\}$, $v_j = g(u_i)$ implies that $t_i \in \{x, x_1, \dots, x_t\}$.

Let $t, s_1, \dots, s_\ell$ be some terms. We prove the different properties by induction on $H - |p|$ where $H$ is the maximal size of all positions in $\mathcal{E}$.

**Base case** $|p| > H$: Such a case is impossible since $H$ is the maximal size of all positions in $\mathcal{E}$.

**Inductive case** $|p| \le H$: By Definition of a fully tag_A-term, we know that either $\text{root}(\mathcal{E}|_p) \in \mathcal{F}_{\text{cst}} \cup \{x, x_1, \dots, x_n, \langle\cdot\rangle\}$ or $\mathcal{E}|_p$ is a tag_A-term. We do a case analysis. If $\text{root}(\mathcal{E}|_p) \in \mathcal{F}_{\text{cst}}$ then the result trivially holds with $C = \mathcal{E}$. If $\text{root}(\mathcal{E}|_p) \in \{x, x_1, \dots, x_n\}$ then the result trivially holds with $C = \_\cdot$. If $\text{root}(\mathcal{E}|_p) = \langle\cdot\rangle$ then $\mathcal{E}|_p = \langle\mathcal{E}|_{p-1}, \mathcal{E}|_{p-2}\rangle$. It implies that $\text{Ap}_\delta(\mathcal{E}|_p\Sigma) = \langle\text{Ap}_\delta(\mathcal{E}|_{p-1}\Sigma), \text{Ap}_\delta(\mathcal{E}|_{p-2}\Sigma)\rangle$ and that $\mathcal{E}\text{Ap}_\delta(\Sigma)|_p = \langle M_1, M_2\rangle$ with $M_1 = \mathcal{E}\text{Ap}_\delta(\Sigma)|_{p-1}$ and $M_2 = \mathcal{E}\text{Ap}_\delta(\Sigma)|_{p-2}$. Therefore, we can apply our inductive hypothesis on $p \cdot 1$ and $p \cdot 2$ which show the existence of a context $C_1$ and $C_2$ satisfying their respective properties. We conclude with $C = \langle C_1, C_2\rangle$. Lastly, if $\mathcal{E}|_p$ is a tag_A-term, then $\mathcal{E}|_p = f(\langle a, \mathcal{E}|_{p-1,2}\rangle, \mathcal{E}|_{p-2}, \dots, \mathcal{E}|_{p,m})$ for some $a \in \text{tag}_A$ and some integer $m$. Therefore, $\mathcal{E}\text{Ap}_\delta(\Sigma)|_p$ is also a tag_A-term. Hence the result holds with $C = \_\cdot$. $\quad$

**Lemma 35.** Let $(\mathcal{E}, \mathcal{F})$ be a tag_A-tagged encapsulation. Let $\Sigma$ be a ground substitution. Let $\delta$ be a tag_A-mapping of $[\mathcal{E}\Sigma]$. For all position $p$ of $\mathcal{E}$, if there exists a term $t$ such that names($t) \cap \text{img}(\delta) = \emptyset$ and $\text{Ap}_\delta(t) = \mathcal{E}\text{Ap}_\delta(\Sigma)|_p$ then $\mathcal{E}|_p$ does not contain tag_A-tagged term and $t = \mathcal{E}\Sigma|_p$.

**Proof.** We prove the result by a downward induction on $|p|$:

**Base case** $\mathcal{E}|_p \in \mathcal{X}$: In such a case, we directly have that $\mathcal{E}\text{Ap}_\delta(\Sigma)|_p = \text{Ap}_\delta(\mathcal{E}|_p\Sigma) = \text{Ap}_\delta(\mathcal{E}\Sigma|_p)$. Thus $t = \mathcal{E}\Sigma|_p$ since names($t) \cap \text{img}(\delta) = \emptyset$. Moreover, $\mathcal{E}|_p \in \mathcal{X}$ implies $\mathcal{E}|_p$ does not contain tag_A-tagged term.

**Inductive case** $\text{root}(\mathcal{E}|_p) = \langle\cdot\rangle$: In such a case, $\mathcal{E}|_p = \langle\mathcal{E}_1, \mathcal{E}_2\rangle$. Thus Definition 32 and $\text{Ap}_\delta(t) = \mathcal{E}\text{Ap}_\delta(\Sigma)|_p$ imply that there exists $t_1, t_2$ such that $t = \langle t_1, t_2\rangle$ and $\text{Ap}_\delta(t_i) = \mathcal{E}\text{Ap}_\delta(\Sigma)|_{p-i}$ for $i = 1, 2$. Therefore, by our inductive hypothesis, we deduce that for $i = 1, 2$, $\mathcal{E}|_{p-i}$ does not contain tag_A-tagged term and $t_i = \mathcal{E}\Sigma|_{p-i}$. Since $\text{root}(\mathcal{E}|_p) = \langle\cdot\rangle$, we can conclude that $\mathcal{E}|_p$ does not contain tag_A-tagged term and $t = \mathcal{E}\Sigma|_p$.

**Inductive case** $\text{root}(\mathcal{E}|_p) \neq \langle\cdot\rangle$: Otherwise, since $\mathcal{E}$ is a fully tag_A-tagged encapsulation, we deduce that $\mathcal{E}|_p = f(\langle a, \mathcal{E}_1\rangle, \mathcal{E}_2, \dots, \mathcal{E}_n)$ for some $a \in \text{tag}_A$ and some $f \in \mathcal{F}$. Thus Definition 32 and $\text{Ap}_\delta(t) = \mathcal{E}\text{Ap}_\delta(\Sigma)|_p$ imply that there exists $t_1, \dots, t_n$ such that $t = f(\langle a, t_1\rangle, t_2, \dots, t_n)$, $\text{Ap}_\delta(t_1) = \mathcal{E}\text{Ap}_\delta(\Sigma)|_{p-1,2}$ and for all $i \in \{2, \dots, n\}$, $\text{Ap}_\delta(t_i) = \mathcal{E}\text{Ap}_\delta(\Sigma)|_{p-i}$. By our inductive hypothesis, we deduce that $t_1 = \mathcal{E}\Sigma|_{p-1,2}$ and for all $i \in \{2, \dots, n\}$, $t_i = \mathcal{E}\Sigma|_{p-i}$. Thus we deduce that $t = \mathcal{E}\Sigma|_p$. But we know
that $\delta$ is a tag$_A$-mapping of $[\mathcal{E}\Sigma]$ and $\mathcal{E}\Sigma|_p$ is tag$_A$-tagged term. Hence by Definition 32, $\mathrm{Ap}_\delta(t) \in \mathcal{N}_D$
which contradicts $t = f(\langle a, t_1 \rangle, t_2, \dots, t_n)$. Hence the case $\mathrm{root}(\mathcal{E}|_p) \neq \langle \rangle$ is impossible.
$\quad \triangleleft$

We can now define how we transform an executed frame $\Phi$ through a tag<sub>A</sub>-mapping of $\Phi$.

**Definition 36.** Let $S$ be a set of tag<sub>A</sub>-encapsulations allowing authentic, confidential and secure channels. Let $\Phi$ be a frame. Let $D, N, H$ be three disjoint sets such that $\Phi$ is an executed frame for $S$ and $D \cup N \cup H$. Let $\delta$ be a tag<sub>A</sub>-mapping of $\Phi$. We define the transformation of $\Phi$ by $\delta$, $D, N$ and $H$, denoted $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi)$, recursively on $|\Phi|$ as follows:

- if $|\Phi| = 0$ then $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi)$ is the empty frame

- if $\Phi = \Phi' \cdot [u]$ with $|\Phi| \notin D \cup N \cup H$ then $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi) = \mathrm{Tr}_{D,N}^{H,\delta}(\Phi') \cdot [\mathrm{Ap}_\delta(u)]$

- if $\Phi = \Phi' \cdot [u]$ with $|\Phi| \in D$ then $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi) = \mathrm{Tr}_{D-|\Phi|,N}^{H,\delta}(\Phi') \cdot [\mathrm{Ap}_\delta(t^i)];$

- if $\Phi = \Phi' \cdot [u]$ with $|\Phi| \in N$ then $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi) = \mathrm{Tr}_{D,N-|\Phi|}^{H,\delta}(\Phi')$.

- if $\Phi = \Phi' \cdot [u]$ with $|\Phi| \in H$ and $(\mathcal{E}_{|\Phi|}, \ell_{|\Phi|}, S_{|\Phi|})$ is an encapsulation allowing authentic channels
  then $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi) = \mathrm{Tr}_{D,N}^{H-|\Phi|,\delta}(\Phi') \cdot [\mathrm{Ap}_\delta(t^i)];$

- else $\Phi = \Phi' \cdot [u]$ and $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi) = \mathrm{Tr}_{D,N}^{H-|\Phi|,\delta}(\Phi')$.

**Lemma 37.** Let $S$ be a set of tag<sub>A</sub>-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 $\delta$ be a tag<sub>A</sub>-mapping of $\Phi$. Assume that $\Phi$ is an executed frame for $S$ and $I$. We have that for all $t \in \mathrm{dom}(\delta)$, if $t\delta \in \mathrm{names}(\mathrm{Tr}_{D,N}^{H,\delta}(\Phi)) \cup \bigcup_{i \in I} \mathrm{names}(\mathrm{Ap}_\delta(\Sigma_i))$ then $\Phi \vdash t$.

**Proof.** Let us denote $\Phi = [u_1; \dots; u_n]$ and $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi) = [v_1; \dots; v_m]$. Let $t \in \mathrm{dom}(\delta)$ such that $t\delta \in \mathrm{names}(\mathrm{Tr}_{D,N}^{H,\delta}(\Phi)) \cup \bigcup_{i \in I} \mathrm{names}(\mathrm{Ap}_\delta(\Sigma_i))$. If $t\delta \in \mathrm{names}(\mathrm{Tr}_{D,N}^{H,\delta}(\Phi))$ then there exists $j \in \{1, \dots, m\}$ such that $t\delta \in \mathrm{names}(v_j)$. Following Definition 36, we deduce that there exists $j \le i$ such that $i \notin N$ and:

- either $i \notin D \cup H$, $v_j = \mathrm{Ap}_\delta(u_i)$ and so $t \in \mathrm{st}(u_i)$

- or $i \in D \cup H$, $v_j = \mathrm{Ap}_\delta(t_{\varepsilon_i} \Sigma_i)$ and so $t \in \mathrm{st}(t_{\varepsilon_i} \Sigma_i) \subseteq \mathrm{st}(\Sigma_i)$.

If $t\delta \in \bigcup_{i \in I} \mathrm{names}(\mathrm{Ap}_\delta(\Sigma_i))$ then $t \in \mathrm{st}(\Sigma_i)$. Thus, we deduce that either $t \in \bigcup_{i \notin I} \mathrm{st}(u_i) \cup \bigcup_{i \in I} \mathrm{st}(\Sigma_i)$.
Consider $i \notin I$ (resp. $i \in I$) such that $t \in \mathrm{st}(u_i)$ (resp. $t \in \mathrm{st}(\Sigma_i)$). By Definition 28, since $t$ is a
tag<sub>A</sub>-term, we deduce that either $[u_1; \dots; u_{i-1}] \vdash t$ or there exist $t' \in \mathrm{st}(u_i)$ (resp. $t' \in \mathrm{st}(\Sigma_i)$) and $k < i$
such that $t \in \mathrm{st}(t')$ and $t', t \in \mathrm{st}(\mathcal{E}_k \Sigma_k) \setminus \mathrm{st}(\mathrm{img}(\Sigma_k))$ and $[u_1; \dots; u_{i-1}] \vdash t'$.

In the former case, the result trivially holds. In the latter case, by Lemma 34, we know that $t' = C[w_1, \dots, w_{n'}]$ where $C$ is a context built on $\{\langle \rangle\} \cup \mathcal{F}_{\mathrm{cst}}$ and for all $w_r \in \{1, \dots, n'\}$, $w_r$ is either a tag<sub>A</sub>-term from $\mathrm{dom}(\delta)$ or $w_r \in \mathcal{T}(\mathcal{F}_{\mathrm{key}} \cup \mathcal{F}_{\mathrm{cst}}, \mathrm{img}(\Sigma))$. But we know that $t\delta \in \mathrm{names}(\mathrm{Ap}_\delta(u_i))$ (resp. $t\delta \in \mathrm{names}(\mathrm{Ap}_\delta(\Sigma_i)))$ and $t' \in \mathrm{st}(u_i)$ (resp. $t' \in \mathrm{st}(\mathrm{img}(\Sigma_i)))$ and $t \in \mathrm{st}(t')$. Thus by Definition 32, we deduce that there exists $r \in \{1, \dots, n'\}$ such that $w_r = t$. Since $[u_1; \dots; u_{i-1}] \vdash t'$ and $C$ is built on $\{\langle \rangle\} \cup \mathcal{F}_{\mathrm{cst}}$, we deduce that $[u_1; \dots; u_{i-1}] \vdash t$ and so the result holds.
$\quad \triangleleft$

Given a set $S \subseteq \mathbb{N}$, given $i \in \mathbb{N}$, we denote by $S|_i$ the set $\{j \in S \mid j < i\}$.

C.3 Deducibility link between composed and abstract frame

**Definition 38.** Let $S$ be a set of tag<sub>A</sub>-encapsulations. Let $\Phi$ be a frame. Let $D, N, H$ be three disjoint sets such that $D \cup N \cup H \subseteq \{1, \dots, |\Phi|\}$. Let $\delta$ be a tag<sub>A</sub>-mapping of $\Phi$. We say that $\Phi$ is a well formed frame for $S$, $D$, $N$ and $H$ if the following properties hold:

- $\Phi$ is an executed frame for $S$ and $D \cup N \cup H$.

- for all $i \in D$, $\Phi \vdash t^i$.
■ for all $i \in \mathbb{N}$, $\Phi \not\to t^i$.

■ for all $i \in \mathbb{H}$, for all $v \in X_{\mathcal{E}_i} \mathbf{A} \mathbf{p}_\delta(\Sigma_i)$, $\mathrm{Tr}_{\mathbb{D},\mathbb{N}}^{\mathbb{H},\delta}(\Phi) \not\to v$

■ for all $i \in \mathbb{H}$, for all $v \in F_i \Sigma_i$, $\mathrm{Tr}_{\mathbb{D}|_{i},\mathbb{N}|_i}^{\mathbb{H},\delta}(\Phi) \vdash v$.

**Lemma 39.** Let $S$ be a set of $\mathbf{tag}_A$-encapsulations. Let $\Phi$ be a frame. Let $\mathbb{D}, \mathbb{N}, \mathbb{H}$ be three disjoint sets such that $\mathbb{I} = \mathbb{D} \cup \mathbb{N} \cup \mathbb{H} \subseteq \{1, \dots, |\Phi|\}$. Let $\delta$ be a $\mathbf{tag}_A$-mapping of $\Phi$. Assume that $\Phi$ is a well formed frame for $S$, $\mathbb{D}$, $\mathbb{N}$ and $\mathbb{H}$. Let $A = \{a \in \mathrm{img}(\delta) \mid u \in \mathrm{dom}(\delta), u\delta = a, \Phi \vdash u\}$. For all $t \in \mathcal{T}(\mathcal{F}, \mathcal{N})$, if $\mathrm{Tr}_{\mathbb{D},\mathbb{N}}^{\mathbb{H},\delta}(\Phi) \cdot [\mathcal{E}_i \mathbf{A} \mathbf{p}_\delta(\Sigma_i)]_{i \in \mathbb{I}} \vdash t$ and names($t) \cap (\mathrm{img}(\delta) \setminus A) = \emptyset$ then:

■ if there exists $t' \in \mathcal{T}(\mathcal{F}, \mathcal{N})$ such that names($t'$) $\cap$ img($\delta$) = $\emptyset$ and $\mathbf{A} \mathbf{p}_\delta(t') = t$ then $\Phi \vdash t'$.

■ if there exists $i \in \mathbb{I}$, a position $p$ of $\mathcal{E}_i$ such that $t = \mathcal{E}_i \mathbf{A} \mathbf{p}_\delta(\Sigma_i)|_p$ then $\Phi \vdash \mathcal{E}_i \Sigma_i|_p$.

**Proof.** Consider a minimal proof $P$ of $\mathrm{Tr}_{\mathbb{D},\mathbb{N}}^{\mathbb{H},\delta}(\Phi) \cdot [\mathcal{E}_i \mathbf{A} \mathbf{p}_\delta(\Sigma_i)]_{i \in \mathbb{I}} \vdash t$. Let us denote $\Phi = [u_1; \dots; u_N]$ and $\mathrm{Tr}_{\mathbb{D},\mathbb{N}}^{\mathbb{H},\delta}(\Phi) = [v_1; \dots; v_M]$. We prove the result by induction on $\mathcal{M}(P)$.

*Base case* $\mathcal{M}(P) = (0,1)$: In such a case, we have that $t \in \mathcal{N}_D \cup \mathcal{F}_{\mathrm{cst}}$. Assume first that $t \notin \mathrm{img}(\delta)$. In such a case, since names($\Phi$) $\cap$ img($\delta$) = $\emptyset$, it implies for all $i \in \mathbb{I}$, for all position $p$ of $\mathcal{E}_i$, $t \neq \mathcal{E}_i \mathbf{A} \mathbf{p}_\delta(\Sigma_i)$. On other hand, $t \in \mathcal{N}_D \cup \mathcal{F}_{\mathrm{cst}}$ and $t \notin \mathrm{img}(\delta)$ also imply that $t = \mathbf{A} \mathbf{p}_\delta(t)$ and names($t) \cap$ img($\delta$) = $\emptyset$. Hence $\Phi \vdash t$.

Assume now that $t \in \mathrm{img}(\delta)$ then there exists $t' \text{ such that } t = \mathbf{A} \mathbf{p}_\delta(t')$. Moreover, we know by hypothesis that names($t) \cap (\mathrm{img}(\delta) \setminus A) = \emptyset$ hence $t \in A$ which allows us to deduce that $\Phi \vdash t'$. Lastly, if there exists $i \in \mathbb{I}$, a position $p$ of $\mathcal{E}_i$ such that $t = \mathcal{E}_i \mathbf{A} \mathbf{p}_\delta(\Sigma_i)$ then by Lemma 35, we deduce that $t' = \mathcal{E}_i \Sigma_i|_p$. Hence the result holds since $\Phi \vdash t'$.

*Base case* $\mathcal{M}(P) = (i, 1)$: In such a case, we deduce that either $t = v_i$ or there exists $k \in \mathbb{I}$ such that $t = \mathcal{E}_k \mathbf{A} \mathbf{p}_\delta(\Sigma_k)$.

Consider first the case $t = \mathcal{E}_k \mathbf{A} \mathbf{p}_\delta(\Sigma_k)$ and there exists $j \in \mathbb{I}$ and a position $p$ of $\mathcal{E}_j$ such that $t = \mathcal{E}_j \mathbf{A} \mathbf{p}_\delta(\Sigma_j)|_p$. Thus we have $\mathcal{E}_k \mathbf{A} \mathbf{p}_\delta(\Sigma_k) = \mathcal{E}_j \mathbf{A} \mathbf{p}_\delta(\Sigma_j)|_p$. By Definition 5, we know that there exists $C[\text{ built on } \{\langle \rangle\} \cup \mathcal{F}_{\mathrm{cst}} \text{ and terms } u_1, \dots, u_n \text{ such that } \mathcal{E}_j|_p = C[u_1, \dots, u_n] \text{ and for all } r \in \{1, \dots, n\},$ either $u_r \in \mathcal{T}(\mathcal{F}_{\mathrm{key}}, \mathcal{X})$ or $u_r$ is a $\mathbf{tag}_A$-tagged term. Moreover, with $\mathcal{E}_k \mathbf{A} \mathbf{p}_\delta(\Sigma_k) = \mathcal{E}_j \mathbf{A} \mathbf{p}_\delta(\Sigma_j)|_p$, we deduce that $\mathcal{E}_k \mathbf{A} \mathbf{p}_\delta(\Sigma_k) = C[u_1 \mathbf{A} \mathbf{p}_\delta(\Sigma_j), \dots, u_n \mathbf{A} \mathbf{p}_\delta(\Sigma_j)]$. For all $r \in \{1, \dots, n\}$, we do a case analysis on $u_r$ and on its position $q$ in $C$.

■ Case $u_r \in \mathcal{T}(\mathcal{F}_{\mathrm{key}}, \mathcal{X})$ and $q$ is a position of $\mathcal{E}_k$ different from variable: In such a case, we deduce that $u_r \mathbf{A} \mathbf{p}_\delta(\Sigma_j) = \mathbf{A} \mathbf{p}_\delta(u_r \Sigma_j)$ and so $\mathbf{A} \mathbf{p}_\delta(u_r \Sigma_j) = \mathcal{E}_k \mathbf{A} \mathbf{p}_\delta(\Sigma_k)|_q$. But $q$ being a position of $\mathcal{E}_k$ implies, by Lemma 35, that $u_r \Sigma_j = \mathcal{E}_k \Sigma_k|_q$. Since $C[\text{ built on } \{\langle \rangle\} \cup \mathcal{F}_{\mathrm{cst}} \mathcal{E}_k \mathbf{A} \mathbf{p}_\delta(\Sigma_k) = C[u_1 \mathbf{A} \mathbf{p}_\delta(\Sigma_j), \dots, u_n \mathbf{A} \mathbf{p}_\delta(\Sigma_j)]$ and $q$ is a position of $\mathcal{E}_k$, we deduce that for all prefix $q'$ of $q$, $\mathrm{root}(\mathcal{E}_k \Sigma_k|_{q'}) = \langle \rangle$ and so $[\mathcal{E}_k \Sigma_k] \vdash \mathcal{E}_k \Sigma_k|_q$. Since $\mathcal{E}_k \Sigma_k \in \Phi$ and $\mathcal{E}_k \Sigma_k|_q = u_r \Sigma_j$, we deduce that $\Phi \vdash u_r \Sigma_j$.

■ Case $u_r \in \mathcal{T}(\mathcal{F}_{\mathrm{key}}, \mathcal{X})$ and $q$ is not a position of $\mathcal{E}_k$ different from variable: Once again, we have $u_r \mathbf{A} \mathbf{p}_\delta(\Sigma_j) = \mathbf{A} \mathbf{p}_\delta(u_r \Sigma_j)$. However, $q$ not being a position of $\mathcal{E}_k$ implies that there exists $y \in \mathrm{dom}(\Sigma_k)$ and a prefix $q'$ of $q$ such that $\mathbf{A} \mathbf{p}_\delta(y \Sigma_k) = \mathcal{E}_j \mathbf{A} \mathbf{p}_\delta(\Sigma_j)|_{p \cdot q'}$ and $p \cdot q'$ is a position of $\mathcal{E}_j$. By Lemma 35, we deduce that $y \Sigma_k = \mathcal{E}_j \Sigma_j|_{p \cdot q'}$. Similarly to the previous case, we deduce that all prefix $q''$ of $q'$, $\mathrm{root}(\mathcal{E}_k \Sigma_k|_{q''}) = \langle \rangle$ and so $[\mathcal{E}_k \Sigma_k] \vdash y \Sigma_k = \mathcal{E}_j \Sigma_j|_{p \cdot q'}$. But $u_r \Sigma_j$ is deducible from $\mathcal{E}_j \Sigma_j|_{p \cdot q'}$ hence we can conclude that $\Phi \vdash u_r \Sigma_j$.

■ Case $u_r$ is a $\mathbf{tag}_A$-tagged term and $q$ is not a position of $\mathcal{E}_k$ different from variable: Since $q$ is not a position of $\mathcal{E}_k$, then there exists $y \in \mathrm{dom}(\Sigma_k)$ and a prefix $q'$ of $q$ such that $\mathbf{A} \mathbf{p}_\delta(y \Sigma_k) = \mathcal{E}_j \mathbf{A} \mathbf{p}_\delta(\Sigma_j)|_{p \cdot q'}$. But by Lemma 35, it would imply that $\mathcal{E}_j|_{p \cdot q'}$ does not contain $\mathbf{tag}_A$-tagged term which is a contradiction with $u_r$ being a $\mathbf{tag}_A$-tagged term. Therefore, this case is impossible.

■ Case $u_r$ is a $\mathbf{tag}_A$-tagged term and $q$ is a position of $\mathcal{E}_k$ different from variable: In such a case, $\mathcal{E}_j \mathbf{A} \mathbf{p}_\delta(\Sigma_j)|_{p \cdot q} = u_r \mathbf{A} \mathbf{p}_\delta(\Sigma_j) = \mathcal{E}_k \mathbf{A} \mathbf{p}_\delta(\Sigma_k)|_q$ implies that $\mathcal{E}_k|_q$ is also a $\mathbf{tag}_A$-tagged term.
By Property 2 of Definition 7, we deduce that $img(mgu(\mathcal{E}_j|_{p,q}, \mathcal{E}_k|_q)) \subseteq \mathcal{X}$. Thus for all position $q'$, if $\mathcal{E}_j|_{p,q'} \in \mathcal{X}$ then $\mathcal{E}_k|_{q'} \in \mathcal{X}$ and $\mathcal{E}_{j|_{p,q'}} \mathcal{A}_{\delta}(\Sigma_j) = \mathcal{E}_k|_{q'} \mathcal{A}_{\delta}(\Sigma_k)$ which implies $\mathcal{E}_{j|_{p,q'}} \Sigma_j = \mathcal{E}_k|_{q'} \Sigma_k$. Therefore, we deduce that $\mathcal{E}_j \Sigma_j|_{p,q} = \mathcal{E}_k \Sigma_k|_q$. But $\mathcal{E}_k \Sigma_k|_q$ is deducible from $\mathcal{E}_k \Sigma_k$ hence so is $u_r \Sigma_j$.

This allows us to conclude that $\Phi \vdash \mathcal{E}_j|_p \Sigma_j$.

Consider now the case $t = \mathcal{E}_k \mathcal{A}_{\delta}(\Sigma_k)$ and there exists $t'$ such that $\text{names}(t') \cap \text{img}(\delta) = \emptyset$ and $\mathcal{A}_{\delta}(t') = t$. By Lemma 35, we deduce that $t' = \mathcal{E}_k \Sigma_k$ and so we directly have that $\Phi \vdash t'$.

Consider now the case $t = v_i$ and there exists $j \in I$, a position $p$ of $\mathcal{E}_j$ such that $t = \mathcal{E}_j \mathcal{A}_p(\Sigma_j)_p$. By Definition 36, we know that there exists $t'$ such that $\text{names}(t') \cap \text{img}(\delta) = \emptyset$ and $\mathcal{A}_{\delta}(t') = v_i$. Hence we have that $\mathcal{E}_j \Sigma_j|_p = t'$. By showing that $\Phi \vdash t'$, the result would thus yield. Therefore, we focus on proving that $\Phi \vdash t'$ which coincides with the last case.

By Definition 36, we know that there exists $j \in \{1, \dots, n\}$ such that $i \le j$ and $j \notin N$ and:

- either $j \notin D \cup H$ and $t = \mathcal{A}_{\delta}(u_j)$. In such a case, since $\text{names}(u_j, t) \cap \text{img}(\delta) = \emptyset$ then $t' = u_j$. Hence we directly have that $\Phi \vdash t'$.

- or $j \in D$ and $v_i = \mathcal{A}_{\delta}(t_{\mathcal{E}_j} \Sigma_j)$. Since $\text{names}(t_{\mathcal{E}_j} \Sigma_j, t') \cap \text{img}(\delta) = \emptyset$, we have that $t_{\mathcal{E}_j} \Sigma_j = t$. But by hypothesis, we already know that $\Phi \vdash t_{\mathcal{E}_j} \Sigma_j$ hence the result holds.

- or $j \in H$, $(\mathcal{E}_j, \ell_j, S_j)$ is an encapsulation allows authentic channels and $v_i = \mathcal{A}_{\delta}(t_{\mathcal{E}_j} \Sigma_j)$. Once again, since $\text{names}(t_{\mathcal{E}_j} \Sigma_j, t') \cap \text{img}(\delta) = \emptyset$, we deduce that $t_{\mathcal{E}_j} \Sigma_j = t'$. Moreover, we know by hypothesis the frame is well formed hence by Definition 38, we have that for all $v \in F_j \mathcal{A}_{\delta}(\Sigma_j)$, $\text{Tr}_{D_j, N_j}^{H,\delta}(\Phi) \vdash v$. Following Definition 36, if we denote by $P'$ the proof of $\text{Tr}_{D_j, N_j}^{H,\delta}(\Phi) \vdash v$, we obtain that $M(P') < (i, 1)$. But by Definition 5, we know that each element of $F_j$ is of the form $f(y)$ where $f \in \mathcal{F}_{key}$ and $y \in \mathcal{X}$. Hence, we deduce that for all $v' \in F_j \Sigma_j$, there exists $v \in F_j \mathcal{A}_{\delta}(\Sigma_j)$ such that $\mathcal{A}_{\delta}(v') = v$. Therefore it implies that for all $v' \in F_j \Sigma_j$, $\text{Tr}_{D_j, N_j}^{H,\delta}(\Phi) \vdash_{P'} \mathcal{A}_{\delta}(v')$ with $M(P') < (i, 1)$. By applying our inductive hypothesis, we deduce that for all $v' \in F_j \Sigma_j$, $\Phi \vdash v'$. Therefore, by Property 3 of Definition 7, we deduce that $\Phi \vdash t_{\mathcal{E}_j} \Sigma_j$ and so $\Phi \vdash t'$.

Inductive case $M(P) > (i, j)$: Assume first that the last rule of $P$ is a composition rule. In such a case, $t = f(t_1, \dots, t_n)$ for some terms $t_1, \dots, t_n$ and for all $k \in \{1, \dots, n\}$, $\text{Tr}_{D,N}^{H,\delta}(\Phi) \cdot [\mathcal{E}_i \mathcal{A}_{\delta}(\Sigma_i)]_{i \in I} \vdash t_k$. If there exists $t'$ such that $\mathcal{A}_{\delta}(t') = t$ then by Definition 32, we deduce that $t = \text{f}(\mathcal{A}_{\delta}(t_1), \dots, \mathcal{A}_{\delta}(t_r))$ for some $t'_1, \dots, t'_r$ such that $t' = \text{f}(t'_1, \dots, t'_r)$ and so for all $k \in \{1, \dots, n\}$, $\mathcal{A}_{\delta}(t'_k) = t_k$. Thus we can apply our inductive hypothesis on all $t'_1, \dots, t'_n$ and deduce that for all $k \in \{1, \dots, n\}$, $\Phi \vdash t'_k$ which allows us to conclude that $\Phi \vdash t'$.

On the other hand, if there exists $\ell \in I$ and a position $p$ of $\mathcal{E}_\ell$ such that $t = \mathcal{E}_\ell \mathcal{A}_{\delta}(\Sigma_\ell)|_p$ then either $\mathcal{E}_\ell|_p \in \mathcal{X}$ or for all $k \in \{1, \dots, n\}$, $t_k = \mathcal{E}_\ell \mathcal{A}_{\delta}(\Sigma_k)|_{p-k}$ with $p \cdot k$ a position of $\mathcal{E}_\ell$. In the former case, we deduce that there exists $x \in \Sigma_\ell$ such that $t = \mathcal{A}_{\delta}(x\Sigma_\ell)$. Therefore, we apply the same reasoning as above. In the latter case, we can apply our inductive hypothesis on all $t_1, \dots, t_k$ and so we deduce that for all $k \in \{1, \dots, n\}$, $\Phi \vdash \mathcal{E}_\ell \Sigma_k|_{p-k}$ which allows us to conclude.

Assume now that the last rule of $P$ is a decomposition rule. Therefore, there exists $x \in \mathcal{X}$, $u'_1, \dots, u'_n, v'_1, \dots, v'_m \in \mathcal{T}(\mathcal{F}_{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'_m) \subseteq \{u'_1, \dots, u'_n\}$; and

- $P = \text{ir}(P', P_1, \dots, P_m)$; and

- $\text{Tr}_{D,N}^{H,\delta}(\Phi) \cdot [\mathcal{E}_i \mathcal{A}_{\delta}(\Sigma_i)]_{i \in I} \vdash_{P'} f(x, u'_1, \dots, u'_n)\sigma$ and for all $k \in \{1, \dots, m\}$, $\text{Tr}_{D,N}^{H,\delta}(\Phi) \cdot [\mathcal{E}_i \mathcal{A}_{\delta}(\Sigma_k)]_{i \in I} \vdash_{P_k} v'_k\sigma$.
Moreover, by minimality of $P$, we deduce that there exists $i' \le i$ such that $f(x, u'_1, \dots, u'_l)\sigma$ is subterm of either $v_{i'}$ or $\mathcal{E}_\ell \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_\ell)$ for some $\ell \in I$. We do case analysis on these two cases.

Case $f(x, u'_1, \dots, u'_l)\sigma \in st(v_{i'})$: By Definition 36, we know that there exists $k \in \{1, \dots, N\}$ such that $i' \le k$ and $k \notin N$ and:

- either $k \notin D \cup H$ and $v_i = \mathbf{A}_{\mathbf{p}_\delta}(u_k)$;

- or $k \in D \cup H$ and $v_i = \mathbf{A}_{\mathbf{p}_\delta}(t_{\mathcal{E}_k} \Sigma_k)$.

By Definition 32, it implies that there exists $t', t''$ subterm of $\Phi$ such that $f(x, u'_1, \dots, u'_n)\sigma = \mathbf{A}_{\mathbf{p}_\delta}(t'')$ with $t'' = f(t', w_1, \dots, w_\ell)$, $\mathbf{A}_{\mathbf{p}_\delta}(t') = t$ and for all $r \in \{1, \dots, n\}$, $\mathbf{A}_{\mathbf{p}_\delta}(w_r) = u'_r\sigma$. However, since for all $r \in \{1, \dots, n\}$, $u'_r \in \mathcal{T}(\mathcal{F}_{\mathit{key}}, \mathcal{X})$ then it implies that for all $y \in \operatorname{dom}(\sigma)$, there exists a term $w$ such that $\mathbf{A}_{\mathbf{p}_\delta}(w) = y\sigma$. Let us define the substitution $\sigma'$ such that for all $y \in \operatorname{dom}(\sigma)$, $y\sigma' = w$ where $\mathbf{A}_{\mathbf{p}_\delta}(w) = y\sigma$. Since we also have that for all $r \in \{1, \dots, m\}$, $v'_1, \dots, v'_r \in \mathcal{T}(\mathcal{F}_{\mathit{key}}, \mathcal{X})$ then we deduce that for all $r \in \{1, \dots, k\}$, $\mathbf{A}_{\mathbf{p}_\delta}(v'_r\sigma') = v'_r\sigma$. By applying our inductive hypothesis on $\mathbf{A}_{\mathbf{p}_\delta}(t'')$ and $\mathbf{A}_{\mathbf{p}_\delta}(v'_1\sigma')$, $\dots$, $\mathbf{A}_{\mathbf{p}_\delta}(v'_k\sigma')$, we deduce that $\Phi \vdash t''$ and for all $r \in \{1, \dots, k\}$, $\Phi \vdash v'_r\sigma'$. Thus it allows us to apply the same decomposition rule and conclude that $\Phi \vdash t'$.

Therefore, we have shown that there exists $t'$ such that $\mathit{names}(t') \cap \mathit{img}(\delta) = \emptyset$, $\mathbf{A}_{\mathbf{p}_\delta}(t') = t$ and $\Phi \vdash t'$. Note that since $\mathit{names}(t') \cap \mathit{img}(\delta) = \emptyset$, if there exists another $t''$ such that $\mathit{names}(t'') \cap \mathit{img}(\delta) = \emptyset$ and $\mathbf{A}_{\mathbf{p}_\delta}(t'') = t$, then $t'' = t'$. Therefore the result holds. Moreover, if there exists $r \in I$ and a position $p$ of $\mathcal{E}_r$ such that $\mathcal{E}_r \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_r)|_p = t$ then by Lemma 35, we deduce that $\mathcal{E}_r \Sigma_r|_p = t'$ and so $\Phi \vdash \mathcal{E}_r \Sigma_r|_p = t'$ which allows us to conclude.

Case $f(x, u'_1, \dots, u'_n)\sigma \in st(\mathcal{E}_\ell \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_\ell))$ for $\ell \in I$: If there is no position $p$ of $\mathcal{E}_\ell$ different from a variable such that $\mathcal{E}_\ell \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_\ell)|_p = f(x, u'_1, \dots, u'_\ell)\sigma$ then it implies that there exists $x \in \Sigma_\ell$ such that $f(x, u'_1, \dots, u'_\ell)\sigma \in \mathbf{A}_{\mathbf{p}_\delta}(x\Sigma_\ell)$. Thus, we can apply the same reasoning as in the case $f(x, u'_1, \dots, u'_\ell)\sigma \in st(v_{i'})$ which allows us to conclude.

Let us consider the case where there exists a position $p$ of $\mathcal{E}_\ell$ different from a variable such that $\mathcal{E}_{c_\ell} \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_\ell)|_p = f(x, u'_1, \dots, u'_\ell)\sigma$. We build a substitution $\sigma'$ as follows:

By Definition 5, we know that for all $r \in \{1, \dots, m\}$, if $v'_r \notin \mathcal{X}$ then for all $r' \in \{1, \dots, n\}$, $\mathit{vars}(u'_{r'}) = \mathit{vars}(v'_{r'}) = \{x\}$ implies $\mathcal{E}_{c_\ell}|_{p|(r'+1)} \in \mathcal{X}$. Thus, we define in such a case $x\sigma'$ such that $u'_{r'}\sigma' = \mathcal{E}_{c_\ell}|_{p|(r'+1)}\Sigma_\ell$. It implies that $u'_{r'}\sigma = \mathbf{A}_{\mathbf{p}_\delta}(u'_{r'}\sigma')$ and $v'_{r'}\sigma = \mathbf{A}_{\mathbf{p}_\delta}(v'_{r'}\sigma')$.

Otherwise, if $v'_r \in \mathcal{X}$ then either there exists $r'$ such that $u'_{r'} = v'_r$ or $u'_{r'} = g(v'_r)$ for some $g \in \mathcal{F}_{\mathit{key}}$. In the former, it implies that $v'_{r'}\sigma = \mathcal{E}_\ell \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_\ell)|_{p|(r'+1)}$ where $p \cdot (r' + 1)$ is a position of $\mathcal{E}_\ell$. Thus we define $u'_{r'}\sigma' = \mathcal{E}_\ell \Sigma_\ell|_{p|(r'+1)}$. In the latter, by Definition 5, we deduce that there exists $t'$ such that $v'_{r'}\sigma = \mathbf{A}_{\mathbf{p}_\delta}(t')$ and so $u'_{r'}\sigma = \mathbf{A}_{\mathbf{p}_\delta}(g(t'))$. By Lemma 35, we deduce thus that $\mathcal{E}_\ell \Sigma_\ell|_{p|(r'+1)} = g(t')$ and we define $v'_{r'}\sigma' = t'$.

We can therefore apply our inductive hypothesis on $\mathcal{E}_{c_\ell} \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_\ell)|_p$, $v'_1\sigma, \dots, v'_m\sigma$ which allows us to deduce that $\Phi \vdash \mathcal{E}_\ell \Sigma_\ell|_p = f(x\sigma', u'_1\sigma', \dots, u'_n\sigma')$ and for all $r \in \{1, \dots, m\}$, $\Phi \vdash v'_{r'}\sigma'$. Thus we can apply the same decomposition rule and obtain that $\Phi \vdash \mathcal{E}_\ell \Sigma_\ell|_{p_1}$.

Let us conclude by verifying the two hypothesis: if there exists $t'$ such that $\mathbf{A}_{\mathbf{p}_\delta}(t') = t$ then by Lemma 35, we deduce that $t' = \mathcal{E}_\ell \Sigma_\ell|_{p_1}$ and so the result holds. If there exists $\ell' \in I$ and a position $p'$ of $\mathcal{E}_{\ell'}$ such that $t = \mathcal{E}_\ell' \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_\ell)|_{p'}$, then we obtain that $\mathcal{E}_{\ell'} \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_\ell') = \mathcal{E}_\ell \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_\ell)|_{p_1}$ with $\Phi \vdash \mathcal{E}_\ell \Sigma_\ell|_{p_1}$. Therefore, we can apply the same reasoning as in the base case $\mathcal{M}(P) = (i, 1)$ and $t = \mathcal{E}_k \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_k) = \mathcal{E}_j \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_j)|_p$ with $\Phi \vdash \mathcal{E}_k \Sigma_k$. This allows us to conclude. $\quad$

**Lemma 40.** 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 $\delta$ be a tag-A-mapping of $\Phi$. Assume that $\Phi$ is a well formed frame for $S$, $D$, $N$ and $H$. Let $I' \subseteq I$ such that for all $i \in I'$, $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi) \cdot [\mathcal{E}_i \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_i)]_{i \in I'} \vdash t_{\mathcal{E}_i} \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_i)$. For all $t \in \mathcal{T}(\mathcal{F}, \mathcal{N})$, $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi) \cdot [t_{\mathcal{E}_i} \mathbf{A}_{\mathbf{p}_\delta}(\Sigma_i)]_{i \in I'} \vdash t$ implies $\mathrm{Tr}_{D,N}^{H,\delta}(\Phi) \vdash t$.