# Relating Process Languages for Security and Communication Correctness (Extended Abstract)

Daniele Nantes, Jorge A. Pérez

► To cite this version:

Daniele Nantes, Jorge A. Pérez. Relating Process Languages for Security and Communication Correctness (Extended Abstract). 38th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2018, Madrid, Spain. pp.79-100, 10.1007/978-3-319-92612-4_5. hal-01824820

HAL Id: hal-01824820

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

Submitted on 27 Jun 2018

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
Relating Process Languages for Security and
Communication Correctness (Extended Abstract)*

Daniele Nantes<sup>0000-0002-1959-87301</sup> and Jorge A. Pérez<sup>0000-0002-1452-61802</sup>

¹ Universidade de Brasília, Brazil

² University of Groningen & CWI, Amsterdam, The Netherlands

**Abstract.** Process calculi are expressive specification languages for concurrency. They have been very successful in two research strands: (a) the analysis of *security protocols* and (b) the enforcement of correct *message-passing programs*. Despite their shared foundations, languages and reasoning techniques for (a) and (b) have been separately developed. Here we connect two representative calculi from (a) and (b): we encode a (high-level) π-calculus for multiparty sessions into a (low-level) applied π-calculus for security protocols. We establish the correctness of our encoding, and we show how it enables the integrated analysis of security properties *and* communication correctness by re-using existing tools.

# 1 Introduction

This paper connects two distinct formal models of communicating systems: a process language for the analysis of *security protocols* [12], and a process language for *session-based concurrency* [9,10]. They are representative of two separate research strands:

(a) Process models for security protocols, such as [12] (see also [7]), rely on variants of the applied π-calculus [1] to establish properties related to process execution (e.g., secrecy and confidentiality). These models support cryptography and term passing, but lack support for high-level communication structures.

(b) Process models for session-based communication, such as [10] (see also [11]), use π-calculus variants equipped with type systems to enforce correct message-passing programs. Security extensions of these models target properties such as information flow and access control (cf. [2]), but usually abstract away from cryptography.

We present a *correct encoding* that connects two calculi from these two strands:

- A, a (low-level) applied π-calculus in which processes explicitly describe term communication, cryptographic operations, and state manipulation [12];

- S, a (high-level) π-calculus in which communication actions are organized as multiparty session protocols [10,5].

Our aim is to exploit the complementary strengths of A and S to analyze communicating systems that feature high-level communication structures (as in session-based concurrency [9,10]) *and* use cryptographic operations and global state in protocol exchanges.

Our encoding of S into A describes how the structures typical of session-based, asynchronous concurrency can be compiled down, in a behavior-preserving manner, as

<footnote>* Work partially funded by FAP-DF 0193.001381/2017.</footnote>
process implementations in which communication of terms takes place exploiting rich equational theories and global state. To our knowledge, ours is the first work to relate process calculi for the analysis of communication-centric programs (S) and of security protocols (A), as developed in disjoint research strands.

We believe our results shed light on both (a) and (b). In one direction, they define a new way to reason about multiparty session processes. Process specifications in S can now integrate cryptographic operations and be analyzed by (re)using existing methods. In fact, since A processes can be faithfully translated into multiset rewriting rules using SAPIC [12] (which can in turn be fed into the Tamarin prover [14]), our encoding bridges the gap between S processes and toolsets for the analysis of security properties:

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

Interestingly, this connection can help to enforce communication correctness: we show how SAPIC/Tamarin can check *local formulas* representing local session types [10].

In the other direction, our approach allows us to enrich security protocol specifications with communication structures based on sessions. This is relevant because the analysis of security protocols is typically carried out on models such as, e.g., Horn clauses and rewriting rules, which admit efficient analysis but that lead to too low-level specifications. Our developments fit well in this context, as the structures intrinsic to session-based concurrency can conveniently describe communicating systems in which security protocols appear intertwined with higher-level interaction protocols.

This rest of the paper is organized as follows. § 2 introduces the *Two-Buyer Contract Signing Protocol*, a protocol that is representative of the kind of systems that is hard to specify using S or A alone. § 3 recalls the definitions of S and A, and also introduces $S^*$, which is a variant of S that is useful in our developments. § 4 defines the encoding of S into A, using $S^*$ as stepping stone, and establishes its correctness (Theorems 1, 2, and 3). § 5 shows how our encoding can be used to reduce the enforcement of protocol conformance in S to the model checking of local formulas for A (Theorems 4 and 5). § 6 revisits the Two-Buyer Contract Signing Protocol: we illustrate its process specification using S minimally extended with constructs from A, and show how key correctness properties can be mechanically verified using SAPIC/Tamarin. The paper closes by discussing related works and collecting concluding remarks (§ 7). Additional technical material and further examples are given in an appendix available online [15].

## 2 A Motivating Example: The Trusted Buyers-Seller Protocol

The *Trusted Buyers-Seller Protocol* extends the Two-Buyer Protocol [10], and proceeds in two phases. The first phase follows the global session type in [10], which offers a unified description of the way in which two buyers ($B_1$ and $B_2$) interact to purchase a book from a seller (*S*). In the second phase, once $B_1$ and $B_2$ agree in the terms of the purchase, the role of *S* is delegated to a *trusted third party* (*T*), which creates a contract for the transaction and collects the participants’ signatures. This second phase relies on the *contract signing protocol* [8], which may resolve conflicts (due to unfulfilled promises
<figure><img src="image_3.png" /><figcaption>**Fig. 1.** The Trusted Buyers-Seller Protocol.</figcaption></figure>

from $B_1$ and $B_2$) and abort the conversation altogether. In this protocol, one key security property is *authentication*, which ensures that an attacker cannot impersonate $B_i$, $S$, or $T$. Relevant properties of communication correctness include *fidelity* and *safety*: while the former ensures that processes for $B_i$, $S$, and $T$ follow the protocols specified by global/local types, the latter guarantees that such processes do not get into errors at runtime. The protocol is illustrated in Fig. 1 and described next:

**First Phase** $B_1$, $B_2$, and $S$ start by establishing a session, after executing the Needham-Schroeder-Lowe (NSL) authentication protocol. Subsequently, they interact as follows:

1. $B_1$ sends the book title to $S$. Then, $S$ replies back to both $B_1$ and $B_2$ the quote for the title. Subsequently, $B_1$ tells $B_2$ how much he can contribute.

2. If the amount is within $B_2$'s budget, then he accepts to perform the transaction, informs $B_1$ and $S$, and awaits the contract signing phase. Otherwise, if the amount offered by $B_1$ is not enough, $B_2$ informs $S$ and $B_1$ his intention to abort the protocol.

3. Once $B_1$ and $B_2$ have agreed upon the purchase, $S$ will *delegate* the session to the trusted party $T$, which will lead the contract signing phase. Upon completion of this phase, $S$ (implemented by $T$) sends $B_1$ the delivery date for the book.

**Second Phase** At this point, the trusted authority $T$, $B_1$, and $B_2$ interact as follows:

4. $T$ creates a new contract $ct$ and a new memory cell $s$, useful to record information about the contract. $T$ sends the contract $ct$ to $B_1$ and $B_2$ for them to sign. $T$ can start
relying to the following requests: *success* (in case of successful communication),
*abort* (request to abort the protocol), or *resolve* (request to solve a conflict).

5. Upon reception of contract *ct* from *T*, $B_1$ sends to $B_2$ his promise to sign it. Subsequently, $B_1$ expects to receive $B_2$'s promise:

* If $B_1$ receives a valid response from $B_2$, his promise is converted into a signature $(\langle\text{signature}_1\rangle)$, which is sent back. Now, $B_1$ expects to receive a valid signature from $B_2$: if this occurs, $B_1$ sends to $T$ a *success* message; otherwise, $B_1$ sends $T$ a *resolve* request, which includes the promise by $B_2$ and his own signature.

* If $B_1$ does not receive a valid promise from $B_2$, then $B_1$ asks $T$ to cancel the purchase (an *abort* request), including his own promise $(\langle\text{promise}_1\rangle)$ in the request.

6. Upon reception of contract *ct* from *T*, $B_2$ checks whether he obtained a valid promise from $B_1$; in that case, $B_2$ replies by sending his promise to sign it $(\langle\text{promise}_2\rangle)$. Now, $B_2$ expects to receive $B_1$'s signature on *ct*: if the response is valid, $B_2$ sends its own signature $(\langle\text{signature}_2\rangle)$ to $B_1$; otherwise, $B_2$ asks $T$ to resolve. If $B_2$ does not receive a valid promise, then it aborts the protocol.

Clearly, S and A offer complementary advantages in modeling and analyzing the Trusted Buyers-Seller Protocol. On the one hand, S can represent high-level structures that are typical in the design of multiparty communication protocols. Such structures are essential in, e.g., the exchanges that follow session establishment in the first phase (which involves a step of session delegation to bridge with the second phase) and the handling of requests *success*, *abort* and *resolve* in the second phase. Hence, S and its type-based verification techniques can be used to establish fidelity and safety properties. However, S is not equipped with constructs for directly representing cryptographic operations, as indispensable in, e.g., the NSL protocol for session establishment and in the exchanges of signatures/promises in the contract signing phase. The lack of these constructs prevents the formal analysis of authentication properties. On the other hand, A compensates for the shortcomings of S, for it can directly represent cryptographic operations on exchanged messages, as required to properly model the contract signing phase and, ultimately, to establish authentication. While A can represent the high-level communication structures mentioned above, it offers a too low-level representation of them, which makes reasoning about fidelity and safety more difficult than in S.

Our encoding from S into A, given in § 4, will serve to combine the individual
strengths of both languages. In § 6, we will revisit this example: we will give a process
specification using an extension of S with some constructs from A. This is consistent,
because A is a low-level process language, and our encoding will define how to correctly
compile S down to A (constructs from A will be treated homomorphically). Moreover,
we will show how to use SAPIC/Tamarin to verify that implementations for $B_1$, $B_2$, S,
and T respect their intended local types.

3 Two Process Models: A and S

**3.1 The Applied π- calculus (A)**

**Preliminaries** As usual in symbolic protocol analysis, messages are modelled by ab-
stract terms $(t, t', \ldots)$. We assume a countably infinite set of variables $V$, a countably
$$M, N ::= x, y | p | n | f(M_1, \dots, M_n) \quad (f \in \Sigma)$$

$$P, Q ::= \mathbf{0} \mid \mathit{out}(M, N); P \mid \mathit{in}(M, N); P \mid P \mid Q \mid !P \mid \nu n; P \mid \mathit{insert}((M, N)); P \mid \mathit{delete} M; P \mid \mathit{lookup} M \text{ as } x \text{ in } P \text{ else } Q \mid \mathit{lock} M; P \mid \mathit{ unlock } M; P \mid \mathit{ event } F; P \mid \text{ if } M = N \text{ then } P \text{ else } Q$$

<caption>**Table 1.** Syntax of A: Terms and Processes.</caption>

infinite set of names $\mathcal{N} = \text{PN} \cup \text{FN}$ (FN for fresh names, PN for public names), and a signature $\Sigma$ (a set of function symbols, each with its arity).

We denote by $\mathcal{T}_\Sigma$ the set of well-sorted terms built over $\Sigma$, $\mathcal{N}$, and $\mathcal{V}$. The set of ground terms (i.e., terms without variables) is denoted $M_\Sigma$. A substitution is a partial function from variables to terms. We denote by $\sigma = \{t_1/x_1, \dots, t_n/x_n\}$ the substitution whose domain is $\text{Dom}(\sigma) = \{x_1, \dots, x_n\}$. We say $\sigma$ is *grounding* for $t$ if $t\sigma$ is ground. We equip the term algebra with an equational theory $=_{E}$, which is the smallest equivalence relation containing identities in $E$, a finite set of pairs the form $M = N$ where $M, N \in \mathcal{T}_\Sigma$, that is closed under application of function symbols, renaming of names, and substitution of variables by terms of the same sort. Furthermore, we require $E$ to distinguish different fresh names, i.e., $\forall a, b \in \text{FN} : a \neq b \Rightarrow a \neq_E b$.

Given a set $S$, we write $S^*$ and $S^\#$ to denote the sets of finite sequences of elements and of finite multisets of elements from $S$. We use the superscript $\#$ to annotate the usual multiset operations, e.g., $S_1 \cup^\# S_2$ denotes the union of multisets $S_1, S_2$. Application of substitutions is extended to sets, multisets, and sequences as expected.

The set of *facts* is $\mathcal{F} := \{F(t_1, \dots, t_k) | t_i \in \mathcal{T}_\Sigma, F \in \Sigma_{\text{fact}} \text{ of arity } k\}$, where $\Sigma_{\text{fact}}$ is an unsorted signature, disjoint from $\Sigma$. Facts will be used to annotate protocols (via events) and to define multiset rewrite rules. A fixed set of fact symbols will be used to encode the adversary's knowledge, freshness information, and the messages on the network. The remaining fact symbols are used to represent the protocol state. For instance, fact $K(m)$ denotes that $m$ is known by the adversary.

**Syntax and Semantics** The grammar for terms $(M, N)$ and processes $(P, Q)$, given in Table 1, follows [12]. In addition to usual operators for concurrency, replication, and name creation, the calculus A inherits from the applied $\pi$-calculus [1] input and output constructs in which terms appear both as communication subjects and objects. Also, A includes a conditional construct based on term equality, as well as constructs for reading from and updating an explicit global state:

- `insert((M, N)); P` first binds the value $N$ to a key $M$ and then proceeds as $P$. Successive inserts may modify this binding; `delete M; P` simply “undefines” the mapping for the key $M$ and proceeds as $P$.

- `lookup M as x in P else Q` retrieves the value associated to $M$, binding it to variable $x$ in $P$. If the mapping is undefined for $M$ then the process behaves as $Q$.

- `lock M; P` and ` unlock M; P` allow to gain and release exclusive access to a resource/key $M$, respectively, and to proceed as $P$ afterwards. These operations are essential to specify parallel processes that may read/update a common memory.

Moreover, the construct `event F; P` adds $F \in \mathcal{F}$ to a multiset of ground facts before proceeding as $P$. These facts will be used in the transition semantics for A, which is de-
$$ \frac{a \in (\mathrm{FN} \cup \mathrm{PN}) \setminus \tilde{n}}{\nu\tilde{n} \cdot \sigma \vdash a} \quad [\mathrm{Name}] \quad \frac{\nu\tilde{n} \cdot \sigma \vdash t \quad t =_E t'}{\nu\tilde{n} \cdot \sigma \vdash t'} \quad [\mathrm{Eq}] \quad \frac{x \in \mathrm{Dom}(\sigma)}{\nu\tilde{n} \cdot \sigma \vdash x\sigma} \quad [\mathrm{Frame}] \quad \frac{\nu\tilde{n} \cdot \sigma \vdash t_i}{\nu\tilde{n} \cdot \sigma \vdash \tilde{f}t} \quad [\mathrm{App}] $$

<caption>**Table 2.** Deduction rules for A. In Rule [Appl]: $\tilde{t} = (t_1, \dots, t_n)$.</caption>

fined by a labelled relation between *process configurations* of the form $(\mathcal{E}, \mathcal{S}, \mathcal{P}, \sigma, \mathcal{L})$, where: $\mathcal{P}$ is a multiset of ground processes representing the processes executed in parallel; $\mathcal{E} \subseteq \mathrm{FN}$ is the set of fresh names generated by the processes; $\mathcal{S}: \mathcal{M}_{\Sigma} \to \mathcal{M}_{\Sigma}$ is a partial function modeling stored information (state); $\sigma$ is a ground substitution modeling the messages sent to the environment; and $\mathcal{L} \subseteq \mathcal{M}_{\Sigma}$ is the set of currently acquired locks. We write $\mathcal{S}(M) = \perp$ to denote that there is no information stored for $M$ in $\mathcal{S}$. Also, notation $\mathcal{L}\backslash M$ stands for the set $\mathcal{L}\backslash\{M'|M' =_E M\}$.

We also require the notions of *frame* and a *deduction relation*. A frame $\nu\tilde{n} \cdot \sigma$ consists of a set of fresh names $\tilde{n}$ and a substitution $\sigma$: it represents the sequence of messages that have been observed by an adversary during a protocol execution and secrets $\tilde{n}$ generated by the protocol, a priori unknown to the adversary. The deduction relation $\nu\tilde{n} \cdot \sigma \vdash t$ models the adversary's ability to compute new messages from observed ones: it is the smallest relation between frames and terms defined by the rules in Table 2.

Transitions are of the form $(\mathcal{E}, \mathcal{S}, \mathcal{P}, \sigma, \mathcal{L}) \xrightarrow{\mathcal{F}}_A (\mathcal{E}', \mathcal{S}', \mathcal{P}', \sigma', \mathcal{L}')$, where $\mathcal{F}$ is a set of ground facts (see Table 3). We write $\rightarrow_A$ for $\emptyset \rightarrow_A$ and $\xrightarrow{f}$ for $\{f\} \rightarrow_A$. As usual, $\rightarrow_A^*$ denotes the reflexive, transitive closure of $\rightarrow_A$. Transitions denote either standard process operations or operations on the global state; they are sometimes denoted $\rightarrow_{A_P}$ and $\rightarrow_{A_S}$, respectively.

## 3.2 Multiparty Session Processes (S)

**Syntax** The syntax of processes, ranged over by $P, Q, \dots$ and that of expressions, ranged over by $e, e', \dots$, is given by the grammar of Table 4, which also shows name conventions. We assume two disjoint countable set of names: one ranges over *shared names* $a, b, \dots$ and another ranges over *session names* $s, s', \dots$. Variables range over $x, y, \dots$; *participants* (or *roles*) range over the naturals and are denoted as $p, q, p', \dots$; *labels* range over $l, l', \dots$ and *constants* range over $\mathrm{true}, \mathrm{false}, \dots$. We write $\tilde{p}$ to denote a finite sequence of participants $p_1, \dots, p_n$ (and similarly for other elements). Given a session name $s$ and a participant $p$, we write $s[p]$ to denote a (*session*) *endpoint*.

The intuitive meaning of processes is as in [10,5]. The processes $\bar{u}[p](y).P$ and $u[p](y).Q$ can respectively request and accept to initiate a session through a shared name $u$. In both processes, the bound variable $y$ is the placeholder for the channel that will be used in communications. After initiating a session, each channel placeholder will be replaced by an endpoint of the form $s[p_i]$ (i.e., the runtime channel of $p_i$ in session $s$). Within an established session, process may send and receive basic values or session names (*session delegation*) and select and offer labeled, deterministic choices (cf. constructs $c \oplus \langle p, l \rangle.P$ and $c \& (p, \{l_i : P_i\}_{i \in I})$). The input/output operations (including delegation) specify the channel and the sender or the receiver, respectively.
**Standard Operations**

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

**Operations on Global State**

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

where:

C0: if $a'$ fresh

C5: if $M =_E N$

C1: if $\nu\mathcal{E}.\sigma \vdash M$

C6: if $M \neq_E N$

C2: if $x$ is fresh, $\nu\mathcal{E}.\sigma \vdash M$

C7: if $\exists N.N =_E M$ and $S(N) =_E V$

C3: if $\exists \tau.\nu\mathcal{E}.\sigma \vdash M$ and $\nu\mathcal{E}.\sigma \vdash N\tau$ and $\tau$ grounding for $N$

C8: if $\forall N.N =_E M \Rightarrow S(N) = \perp$

C4: if $M =_E M'$ and $\exists \tau.N =_E N'\tau$ and $\tau$ grounding for $N'$

C9: if $M \notin \mathcal{L}$

<figure><img src="image_6.png" /><figcaption>**Table 4.** Process syntax and naming conventions for S.</figcaption></figure>

Message queues model asynchronous communication. A message $(p \triangleright q : v)$ indicates that $p$ has sent a value $v$ to $q$. The empty queue is denoted by $\emptyset$. By $h \cdot m$ we denote the queue obtained by concatenating message $m$ to the queue $h$. By $s[\tilde{p}] : h$ we
$$
\begin{array}{l}
P | \mathbf{0} \equiv P \qquad P | Q \equiv Q | P \qquad (P | Q) | R \equiv P | (Q | R) \qquad (\nu a)\mathbf{0} \equiv \mathbf{0} \qquad (\nu s)(s : \emptyset) \equiv \mathbf{0} \\
(\nu r)P | Q \equiv (\nu r)(P | Q), \text{ if } r \notin fn(Q) \qquad (\nu r)(\nu r')P \equiv (\nu r')(\nu r)P, \text{ where } r ::= a | s \\
s[\tilde{p}] : h \cdot (q \triangleright p : \zeta) \cdot (q' \triangleright p' : \zeta') \cdot h' \equiv s[\tilde{p}] : h \cdot (q' \triangleright p' : \zeta') \cdot (q \triangleright p : \zeta) \cdot h', \text{ if } p \neq p' \text{ or } q \neq q'
\end{array}
$$

<caption>**Table 5.** Structural Congruence for S Processes.</caption>

denote the queue *h* of the session *s* initiated between participants $\tilde{p} = p_1, \dots, p_n$; when the participants are clear from the context we shall write $s : h$ instead of $s[\tilde{p}] : h$.

Request/accept actions bind channel variables, value receptions bind value vari-
ables, channel receptions bind channel variables, hidings bind shared and session names.
In (νs)P all occurrences of s[p] and queue s inside P are bound. We denote by fn(Q)
the set of free names in Q. A process is closed if it does not contain free variables or
free session names. Unless stated otherwise, we only consider closed processes.

**Semantics** S processes are governed by a reduction semantics, which relies on a *struc-*
*tural congruence* relation, denoted ≡ and defined by adding α-conversion to the rules of
Table 5. Reduction rules are given in Table 6; we write *P* —→*S* *P'* for a reduction step.
We rely on the following syntax for contexts: *E* ::= [] | *P* | (να)*E* | (νs)*E* | *E* | *E*.

We briefly discuss the reduction rules. Rule [Init] describes the initiation of a new
session among *n* participants that synchronize over the shared name *a*. After session
initiation, the participants will share a private session name (*s* in the rule), and an empty
queue associated to it (*s*[*p*] : ∅ in the rule). Rules [Send], [Deleg] and [Sel] add values,
channels and labels, respectively, into the message queue; in Rule [Send], *e* ↓ *v* denotes
the evaluation of the expression *e* into a value *v*. Rules [Recv], [SRecv] and [Branch]
perform complementary de-queuing operations. Other rules are self-explanatory.

**3.3 The Calculus S\***

We now introduce S\*, a variant of S which will simplify the definition of our encoding
into A. The syntax of S\* processes is as follows:

$$
\begin{array}{l}
P, Q ::= \mathbf{0} \mid \bar{u}[p](\tilde{y}).P \mid u[p](\tilde{y}).P \mid P \mid Q \mid (\nu n)P \mid \text{if } e \text{ then } P \text{ else } Q \\
\qquad \mid c_{pq}!(e : \mathbf{msg}).P \mid c_{pq}?(y).P \mid c_{pq}?(x).P \mid c_{pq}!\langle c'_{p'q'} : \mathbf{chan} \rangle.P \mid \\
\qquad \mid c_{pq} \oplus \langle l : \mathbf{lbl} \rangle.P \mid c_{pq} \& (\{l_i : P_i\}_{i \in I}) \mid s_{pq} : h
\end{array}
$$

where $c_{pq}$ denotes a channel annotated with participant identities, $h ::= h \cdot m | \emptyset$ and $m ::= \langle msg, v \rangle | \langle chan, s_{pq} \rangle | \langle tbl, l \rangle$. The main differences between S and S\* are:

- Intra-session communication relies on annotated channels, and output prefixes in-
clude a *sort* for the communicated messages (*msg* for values, *chan* for delegated
sessions, *lbl* for labels).

- While S uses a single queue per session, in S\* for each pair of participants there will be two queues, one in each direction. This simplifies the definition of structural congruence ≡ for S\*, which results from that for S as expected and is omitted.

- Constructs for session request and acceptance in S\* depend on a sequence of vari-
ables, rather than on a single variable. In these constructs, denoted $\bar{u}[p](\tilde{y})$.P and
$u[p](\tilde{y})$.P, respectively, $\tilde{y}$ is a sequence of variables of the form $y_{pq}$, for some p, q.
<table><caption>**Table 6.** Reduction rules for S (Rule [If-F] omitted).</caption>
  <tbody>
    <tr>
      <td>a[p<sub>1</sub>](y)P<sub>1</sub> | ... | a[p<sub>n-1</sub>](y)P<sub>n-1</sub> | a&#773;p<sub>n</sub>(y).P<sub>n</sub> &rarr; S<br/>(&nu;s)(P<sub>1</sub>{s[p<sub>1</sub>]/y} | ... | P<sub>n-1</sub>{s[p<sub>n-1</sub>]/y} | P<sub>n</sub>{s[p<sub>n</sub>]/y} | s&#773;p : &emptyset;)<br/>s[p]!(&q;e).P | s : h &rarr; S P | s:h.(p&rarr; q:v) (e &down; v) [Send]<br/>s[p]!(&q; s'[p']).P | s : h &rarr; S P | s:h.(p&rarr; q:s'[p']) [Deleg]<br/>s[p] &oplus; (&q;l).P | s : h &rarr; S P | s:h.(p&rarr; q:l) [Sel]<br/>s[p]?(q, x).P | s:(p&rarr;p:v).h &rarr; S P{v/x} | s&#773;p : h [Recv]<br/>s[p]?((&q; y)).P | s:(q&rarr;p:s'[p']) . h &rarr; S P{s'[p']/y} | s&#773;p : h [SRecv]<br/>s[p] &amp; (q, {l<sub>i</sub> : P<sub>i</sub>}<sub>i&isin;I</sub>) | s:(q&rarr;p:l<sub>j</sub>).h &rarr; S P<sub>j</sub> | s : h (j &isin; I) [Branch]<br/>if e then P else Q &rarr; S P (e &down; true) [If-T]<br/>P &equiv; P' and P' &rarr; S Q' and Q &equiv; Q' &rarr; P &rarr; S Q [Str]<br/>P &rarr; S P' &rarr; E[P] &rarr; S E[P'] [Ctx]</td>
    </tr>
  </tbody>
</table>

With these differences in mind, the reduction semantics for $S^*$, denoted $\rightarrow_S S^*$, follows
that for S (Table 6). Reduction rules for $S^*$ include the following:

<table>
  <tbody>
    <tr>
      <td>a[1](<span style="text-decoration: overline;">y</span><sub>1</sub>).P<sub>1</sub> | ... | a[n-1](<span style="text-decoration: overline;">y</span><sub>n-1</sub>).P<sub>n-1</sub> | <span style="text-decoration: overline;">a</span>[n](<span style="text-decoration: overline;">y</span><sub>n</sub>).P<sub>n</sub> &rarr; S<sup>*</sup></td>
      <td>[Init<sup>*</sup>]</td>
    </tr>
    <tr>
      <td>(&nu;s)(P<sub>1</sub>{s/y} | ... | P<sub>n-1</sub>{s/y} | P<sub>n</sub>{s/y} | <span style="text-decoration: overline;">y</span><sub>i</sub>{s/y} : &emptyset; | ... | <span style="text-decoration: overline;">y</span><sub>n</sub>{s/y} : &emptyset;)</td>
      <td></td>
    </tr>
    <tr>
      <td>y<sub>pq</sub>!(e : msg).P | y<sub>pq</sub> : h &rarr; S<sup>*</sup> P | y<sub>pq</sub> : h &middot; &lang;msg, v&rang; (e &down; v)</td>
      <td>[Send<sup>*</sup>]</td>
    </tr>
    <tr>
      <td>y<sub>pq</sub>?(x).P | y<sub>qp</sub> : &lang;msg, v&rang; . h &rarr; S<sup>*</sup> P{v/x} | y<sub>qp</sub> : h</td>
      <td>[Recv<sup>*</sup>]</td>
    </tr>
  </tbody>
</table>

Notice that in Rule [Init*], we only need to write $P_i\{s/y\}$: after reduction, these variables will be of the form $s_{pq}$. In that rule, each $\tilde{y}_i\{s/y\} : \emptyset$ denotes several queues (one for each name $y_{pq} \in \tilde{y}_i$), rather than a single queue.

It is straightforward to define an auxiliary encoding $([\cdot]) : S \mapsto S^*$. For instance:

$$
\begin{align*}
([s[p]!\langle q, e \rangle.P]) &= s_{pq}!\langle e : \text{msg} \rangle.([P]) & ([s[p]?(q, x).P]) &= s_{qp}?(x).([P]) \\
([s[p]!\langle q, z_p' \rangle.P]) &= s_{pq}!\langle z_{p'} : \text{chan} \rangle.([P]) & ([s[p]?(\langle q, x \rangle.P]) &= s_{qp}?(\langle x \rangle).([P])
\end{align*}
$$

The full encoding, given in [15], enjoys the following property:

**Theorem 1.** Let $P \in S$. Then: (a) If $P \to_S P'$, then $([P] \to_S [P'])$.

(b) If $([P] \to_S R)$, then there exists $P' \in S$ such that $P \to_S P'$ and $([P'] = R)$.

Given the encoding $([\cdot]) : S \to S^*$ and Theorem 1 above, we now move on to define an encoding $[\cdot] : S^* \to A$. By composing these encodings (and their correctness results— Theorems 2 and 3), we will obtain a behavioral-preserving compiler of S into A.

4 Encoding S* Into A

We now present our encoding $[\cdot] : S^* \to A$ and establish its correctness. The encoding is defined in Table 7; it uses the set of facts $F_S = \{\text{honest}, \text{sndnonce}, \text{rcvnonce}, \text{sndchann}, \text{rcvchann}, \text{out}, \text{inp}, \text{dels}, \text{recs}, \text{sel}, \text{bra}, \text{close}\}$. Facts will be used as event annotations in process executions, and also for model checking communication correctness via trace formulas in the following section. Our encoding will rely on the equational theory for *pairing*, which is embedded in Tamarin prover [14], and includes function symbols $\langle-, -\rangle$, *fst* and *snd*, for pairing and projection of first and second parameters of a pair. Communication within a secure established session is expressed by the manipulation of queues, which will be stored in the set of states *S*. In SAPIC, we implement queues $y_{pq}$ and $y_{qp}$ as $q(y, p, q)$ and $q(y, q, p)$, respectively, where *q* is a function symbol for queues. Also, $s_{pq} : \emptyset$ is implemented as *insert*($s_{pq}$, *init*)).
Implementing Session Establishment

$$ \llbracket \bar{a}[3](\tilde{y}_3).P \rrbracket = \nu s; P_{31}; P_{32}; \text{insert}(\langle \tilde{s}_{ij}, \emptyset \rangle); \text{event init}(\tilde{s}_{ij}); $$
event sndchann(pk(ska$_{31}$), pk(y$_{1}$), s); out(u$_{1}$, s);
event sndchann(pk(ska$_{32}$), pk(y$_{2}$), s); out(u$_{2}$, s); $\llbracket P \rrbracket$

$P_{3i} = \nu \text{ ska}_{3i}; \text{out}(c, pk(ska_{3i})); \text{event honest}(pk(ska_{3i})); \text{in}(c, pk(y_i));$
$\nu n_{31}; \text{event} \text{ndnonce}(pk(ska_{3i}), pk(y_i), aenc(\langle n_{3i}, pk(ska_{3i}), pk(y_i) \rangle))$
out(c, aenc(\langle n_{3i}, pk(ska_{3i}), pk(y_i) \rangle)); in(c, aenc(\langle n_{3i}, u_i, pk(y_i) \rangle, pk(ska_{3i}))); \\
\text{event rcvnonce(pk(y_i), pk(ska_{3i}), aenc(\langle n_{3i}, u_i, pk(y_i) \rangle, pk(ska_{3i})))}

$$ \llbracket a[i](\tilde{y}_i).P \rrbracket = \nu \text{ ska}_i; \text{in}(c, pk(x_i)); \text{event honest}(pk(ska_i)); \text{in}(c, aenc(\langle y, pk(x_i) \rangle, pk(ska_i))); $$
event rcvnonce(pk(x$_{i}$), pk(ska$_{i}$), aenc(\langle y, pk(x$_{i}$) \rangle, pk(ska$_{i}$)))
$\nu n_i$; event \text{ndnonce}(pk(ska$_{i}$), pk(x$_{i}$), aenc(\langle y, n_i, pk(ska$_{i}$) \rangle, pk(x$_{i}$)))
out(c, aenc(\langle y, n_i, pk(ska$_{i}$) \rangle, pk(x$_{i}$))); in(n$_{i}$, z);
event rcvchann(pk(x$_{i}$), pk(ska$_{i}$), z); $\llbracket P \rrbracket $ \\

Implementing Intra-Session Communication

$$ \llbracket c_{pq}!\langle e : \text{msg} \rangle.P \rrbracket = \text{lock } c_{pq}; \text{lookup } c_{pq} \text{ as } x \text{ in } (\text{insert}(\langle c_{pq}, x \cdot \langle \text{msg}, v \rangle \rangle)); $$
event out(c$_{pq}$, v); unlock c$_{pq}$; $\llbracket P \rrbracket$ $e \downarrow v$

$$ \llbracket c_{pq}?(x).P \rrbracket = \text{lock } c_{qp}; \text{lookup } c_{qp} \text{ as } z_v \text{ in } (\text{iffst}(z_v) = \langle \text{msg}, z \rangle \text{ then } (\text{insert}(\langle c_{qp}, \text{snd}(z_v) \rangle)); \text{event inp}(c_{qp}, \text{fst}(z_v)); \text{unlock } c_{qp}; \llbracket P\{z/x\} \rrbracket) $$

$$ \llbracket c_{pq}!\langle c' : \text{chan} \rangle.P \rrbracket = \text{lock } c_{pq}; \text{lookup } c_{pq} \text{ as } x \text{ in } (\text{insert}(\langle c_{pq}, x \cdot \langle \text{chan}, c' \rangle \rangle)); $$
event dels(c$_{pq}$, c'); unlock c$_{pq}$; $\llbracket P \rrbracket$

$$ \llbracket c_{pq}?((x).P \rrbracket = \text{lock } c_{qp}; \text{lookup } c_{qp} \text{ as } z_v \text{ in } (\text{iffst}(z_v) = \langle \text{chan}, z \rangle \text{ then } (\text{insert}(\langle c_{qp}, \text{snd}(z_v) \rangle)); \text{event recs}(c_{qp}, \text{fst}(z_v)); \text{unlock } c_{qp}; \llbracket P\{z/x\} \rrbracket) $$

$$ \llbracket c_{pq} \oplus \langle l : \text{lbl} \rangle.P \rrbracket = \text{lock } c_{pq}; \text{lookup } c_{pq} \text{ as } x \text{ in } (\text{insert}(\langle c_{pq}, x \cdot \langle \text{lbl}, l \rangle \rangle)); $$
event sel(c$_{pq}$, l); unlock c$_{pq}$; $\llbracket P \rrbracket$

$$ \llbracket c_{pq} \& \langle \{l_i : P_i\} \rangle \rrbracket = \text{lock } c_{qp}; \text{lookup } c_{qp} \text{ as } z_l \text{ in } (\text{iffst}(z_l) = \langle \text{lbl}, l_1 \rangle \text{ then } \text{insert}(\langle c_{qp}, \text{snd}(z_l) \rangle)); \text{event bra}(c_{qp}, l_1); \text{unlock } c_{qp}; \llbracket P_1 \rrbracket $$
else iffst(z_l) = \langle \text{lbl}, l_2 \rangle \text{ then } \text{insert}(\langle c_{qp}, \text{snd}(z_l) \rangle); \text{event bra}(c_{qp}, l_2); \text{unlock } c_{qp}; \llbracket P_2 \rrbracket) $$

$$ \llbracket \mathbf{0} \rrbracket = \text{event close} \quad \llbracket s[\bar{p}] : h \rrbracket = \mathbf{0} $$
$$ \llbracket (\nu s)P \rrbracket = \nu s; \llbracket P \rrbracket \quad \llbracket P \mid Q \rrbracket = \llbracket P \rrbracket \mid \llbracket Q \rrbracket \quad \llbracket \text{if } e \text{ then } P \text{ else } Q \rrbracket = \text{if } e \text{ then } \llbracket P \rrbracket \text{ else } \llbracket Q \rrbracket $$

<caption>**Table 7.** Encoding from $S^*$ to A.</caption>

**Session Initiation.** The (high-level) mechanism of session initiation of Rule [Init] in $S^*$ (Table 6) is implemented in A by following the Needham-Schroeder-Lowe (NSL) authentication protocol [13]; see Table 7 (top). We use NSL because it is simple, and it has already been formalized in SAPIC. For simplicity, we present the implementation for three participants; the extension to n participants is as expected. The encoding creates queues for intra-session communication using processes `insert((\tilde{s}_{ij}, \emptyset))`. The security verification uses the built-in library `asymmetric-encryption` available in Tamarin [14], and assumes the usual signature and equational theory for public keys pk, secret keys sk, asymmetric encryption aenc and decryption dec.

**Intra-session Communication.** Process $\llbracket c_{pq}!\langle e : \text{msg} \rangle.P \rrbracket$ first acquires a lock in the queue $c_{pq}$ to avoid interference. Then, a `lookup - as -` process checks the state of $c_{pq}$
and enqueues message $\langle msg, v \rangle$ at its end. Finally, the encoding signals this operation by executing event out($c_{pq}, v$) before unlocking $c_{pq}$ and proceeding as as $[[P]]$. The encoding of session delegation $[[c_{pq},!\langle c : chan \rangle, P]]$ is very similar: the only differences are the sort of the communicated object and the event signaled at the end ($dels(c_{pq}, c'$)).

As above, process $[[c_{pq}?(x).P]]$ first acquires a lock and checks the queue $c_{qp}$. If it is of the form $\langle msg, -$\rangle$ then it stores it in a variable $z_v$: it consumes the first part $(fst(z_v))$ and updates $c_{qp}$ with the second part. The implementation then signals an event event inp($c_{pq}, z_v$) before unlocking $c_{qp}$ and proceeding as $[[P]]$. Process $[[c_{pq}?((x)).P]]$ (reception of a delegated session) is similar; in this case, the queue should contain a value of sort chan and the associated event is recs($c_{pq}, fst(z_v)$).

Process $[[0]]$ simply executes an event close. In the prototype SAPIC implementation of our encoding, this event mentions the name of the corresponding session $c_{qp}$.

Finally, process $[[c_{pq} : h]]$ is 0 because we implement queues using the global state in A. The implementation of the remaining constructs in A is self-explanatory.

**Remark 1.** Since our encoding operates on *untyped* processes, we could have sort mismatches in queues (cf. Rule [If-F]). To avoid this, encodings of input-like processes (e.g., $s_{pq}?(x).P$), use the input of a *dummy* value that allows processes to reduce.

**Correctness of** $[[\cdot]]$. We first associate to each ground process $P \in S^*$ a process configuration via the encoding in Table 7. Below we assume that $\tilde{s}, I$, and $I'$ may be empty, allowing the encoding of communicating processes (obtained after session initiation); we also assume that the set of (free) variables in $P$ (denoted $var(P)$) can be instantiated with ground terms that can be deduced from the current frame.

**Definition 1** Suppose an $S^*$ process $R \equiv (\nu s)(\prod_{i \in I} P_i | \prod_{j,k \in I'} s_{p_j q_k} : h_{j,k})$, with $var(R) = \{x_1, \dots, x_n\}$. A process configuration for $R$, denoted $C[[R]]$, is defined as:

$$ (\mathcal{E} \cup \{s\}, S \cup \{s_{p_j q_k} : h_{j,k} | j, k \in I'\}, \{\prod_{i \in I} [[P_i]]\}, \sigma, \mathcal{L}), $$

where $var(R) \subseteq \text{dom}(\sigma)$ and $\sigma$ is grounding for $x_i$, $i = 1, \dots, n$.

With some abuse of notation we say that $C$ is a process configuration for $R$. Observe that different process configurations $C, C', \dots$ can be associated to a same process $R \in S$ once one considers variations of $\mathcal{E}, S, \sigma, \mathcal{L}$.

**Theorem 2 (Completeness).** Let $P \in S^*$. If $P \to_{S^*} P'$ then for all process configuration $C$, there exists a process configuration $C'$ such that $C[[P]] \to_{A^*} C'[[[P']]]$.

*Proof.* The proof is by structural induction, analyzing the rule applied in $P \to_{S^*} P'$. □ via encoding in Table 7 and the rules in Table 3. See [15] for details.

To prove soundness, we rely on a Labeled Transition System for $S^*$, denoted $P \xrightarrow{\lambda} P'$. Such an LTS, and the proof of the theorem below, can be found in [15].

**Theorem 3 (Soundness).** Let $P \in S^*$ and $C$ be such that $C[[P]] \to_{A_P} R$. Then there exist $P' \in S^*$, $C'$, and $\lambda$ such that $R \to_{A^*} C'[[[P']]]$ and $P \xrightarrow{\lambda} P'$.
$S ::= \mathbf{bool} \mid \mathbf{nonce} \mid \mathbf{msg} \mid \mathbf{temp} \mid \dots \mid G \quad \text{Sorts} \quad U ::= S \mid T \quad \text{Exchange Types}$

(Global Types) $G ::= \mathbf{p} \to \mathbf{q} : \langle U \rangle . G \mid \mathbf{p} \to \mathbf{q} : \{ l_i : G_i \}_{i \in I} \mid \text{end}$

(Local Types) $T ::=! \langle \mathbf{p}, U \rangle . T \mid ?(\mathbf{p}, U) . T \mid \oplus \langle \mathbf{p}, \{ l_i : T_i \} \rangle \mid \&(\mathbf{p}, \{ l_i : T_i \}) \mid \text{end}$

<caption>**Table 8.** Global and Local Types [10].</caption>

# 5 Multiparty Session Types and Their Local Formulas

Using $([\cdot,])$ and $[[\cdot,]]$, in this section we connect well-typedness of processes in $S$ [10] with the satisfiability of *local formulas*, which model the execution of A processes.

## 5.1 Global and Local Types

Rather than defining multiparty session types for A processes, we would like to model checking local types by re-using existing tools for A: SAPIC [12] and Tamarin [14]. Concretely, next we shall connect typability for S processes with satisfiability for A processes. To formalize these results, we first recall some essential notions for multiparty session types; the reader is referred to [10,5] for an in-depth presentation.

*Global types* $G, G'$ describe multiparty session protocols from a vantage point; they offer a complete perspective on how two or more participants should interact. On the other hand, *local (session) types* $T, T'$ describe how each participant contributes to the multiparty protocol. A *projection function* relates global and local types: the projection of $G$ onto participant $n$ is denoted $G|_n$. The syntax for global and local types, given in Table 8 is standard [10]. A complete description of session types can be found in [15].

*Example 1.* Fig. 2 gives three global types for the protocol in § 2: while $G_{\text{init}}$ represents the first phase, both $G_{\text{contract}}$ and $G_{\text{sign}}$ are used to represent the second. In $G_{\text{sign}}$, we use $G_{\text{resolve}_i}$ to denote a global protocol for resolving conflicts; see [15] for details.

Typing judgements for expressions and processes are of the form $\Gamma \vdash e : S$ or $\Gamma \vdash P \triangleright \Delta$, where $\Gamma ::= \emptyset \mid \Gamma, x : S$ and $\Delta ::= \emptyset \mid \Delta, c : T$. The *standard environment* $\Gamma$ assigns variables to sorts and service names to closed global types; the *session environment* $\Delta$ associates channels to local types. We write $\Gamma, x : S$ only if $x \notin \text{dom}(\Gamma)$, where $\text{dom}(\Gamma)$ denotes the domain of $\Gamma$. We adopt the same convention for $a : G$ and $c : T$, and write $\Delta, \Delta'$ only if $\text{dom}(\Delta) \cap \text{dom}(\Delta') = \emptyset$. Typing rules are as in [10,5]; as discussed in those works, typability for S processes ensure communication correctness in terms of *session fidelity* (well-typed processes respect prescribed local protocols) and *communication safety* (well-typed processes do not feature communication errors), among other properties.

## 5.2 Satisfiability of Local Formulas from A

Following the approach in [12], properties of processes in A will be established via analysis of *traces*, which describe the possible executions of a process. This will allow us to prove communication correctness of S processes, using encoding $[[\cdot,]]$.
<figure><img src="image_7.png" /><figcaption>Fig. 2. Global Types for the Trusted Buyer-Seller Protocol (§ 2).</figcaption></figure>

**Definition 1 (Traces of P [12]).** Given a ground process $P \in \mathbf{A}$, we define the set of traces of $P$, denoted by traces($P$), as

$$ \text{traces}(P) = \{[F_1, \dots, F_n] \mid (\emptyset, \{P\}, \emptyset, \emptyset) \overset{F_1}{\rightleftharpoons} \dots \overset{F_n}{\rightleftharpoons} (\mathcal{E}_n, S_n, P_n, \sigma_n, \mathcal{L}_n) \} $$

We will denote by $\text{tr}_P$, a trace from a set traces($P$), for some process $P$. We will write $\text{tr}$ when $P$ is clear from the context. Notice that, $\text{tr}_P = \text{tr}_Q$ does not necessarily imply that $P = Q$: each process may implement more than one session in different ways.

SAPIC and Tamarin [14] consider two sorts: temp and msg. Each variable of sort s will be interpreted in the domain $D(s)$; in particular, we will denote by $\mathcal{V}_{\text{temp}}$ the set of temporal variables, which is interpreted in the domain $D(\text{temp}) = Q$; also, $\mathcal{V}_{\text{msg}}$ is the set of message variables, which is interpreted in the domain $D(\text{msg}) = M$. Below, we will adopt a function $\theta: \mathcal{V} \to M \cup Q$ that maps variables to terms respecting the variable's sorts, that is $\theta(x: s) \in D(s)$.

**Definition 2 (Trace atoms [12]).** A trace atom has of one of the forms:

$$ A ::= \perp \mid t_1 \approx t_2 \mid i < j \mid i \doteq k \mid F@i $$

denoting, respectively, false, term equality, timepoint ordering, timepoint equality, or an action for a fact $F$ and a timepoint $i$. The construction of trace formula $\varphi$ respects the usual first-order convention:

$$ \varphi, \psi ::= A \mid \neg \varphi \mid \varphi \wedge \psi \mid \varphi \vee \psi \mid \varphi \to \psi \mid \varphi \leftrightarrow \psi \mid (\exists x: s).\varphi \mid (\forall x: s).\varphi $$

Given a process $P$, in the definition below, $\text{tr}$ denotes a trace in traces($P$), $\text{idx}(\text{tr})$ denotes the positions in $\text{tr}$, and $\text{tr}_i$ denotes the $i$-th position in $\text{tr}$.
**Definition 3 (Satisfaction relation [12]).** The satisfaction relation $(\text{tr}, \theta) \models \varphi$ between a trace $\text{tr}$, a valuation $\theta$, and a trace formula $\varphi$ is defined as follows

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
(\text{tr}, \theta) \models \bot & \text{never} & (\text{tr}, \theta) \models t_1 \approx t_2 & \text{iff } t_1\theta =_E t_2\theta \\
(\text{tr}, \theta) \models i \prec j & \text{iff } \theta(i) < \theta(j) & (\text{tr}, \theta) \models \neg\varphi & \text{iff not } (\text{tr}, \theta) \models \varphi \\
(\text{tr}, \theta) \models i \doteq j & \text{iff } \theta(i) = \theta(j) & (\text{tr}, \theta) \models \varphi_1 \wedge \varphi_2 & \text{iff } (\text{tr}, \theta) \models \varphi_1 \text{ and } (\text{tr}, \theta) \models \varphi_2 \\
(\text{tr}, \theta) \models F@i & \text{iff } \theta(i) \in \text{idx}(\text{tr}) \text{ and } F\theta =_E \text{tr}_{\theta(i)} & & \\
(\text{tr}, \theta) \models (\exists x : s).\varphi & \text{iff there exists } u \in D(s) \text{ such that } (\text{tr}, \theta[x \mapsto u]) \models \varphi & &
\end{array}
$$

Satisfaction of $(\forall x : s)\varphi$, $\varphi \lor \psi$ and $\varphi \Rightarrow \psi$ can be obtained from the cases above.

## 5.3 From Local Types to Local Formulas

Below we assume $s$ is an established session between participants $p$ and $q$. Given $k$: $\text{temp}$ and a trace formula $\varphi$, we write $\varphi(k)$ to say that there is a fact $F$ such that $F@k$ is an atom in $\varphi$. Below we assume that $S$ is a subsort of $\text{msg}$.

**Definition 4 (Local Formula).** Given a local type $T$ and an endpoint $s[p]$, its local formula $\Phi_{s[p]}(T)$ is defined inductively as follows:

$$ 
\begin{align*}
\Phi_{s[p]} (!\langle q, S \rangle.T) &= \exists i, z. (\text{out}(s_{pq}, z)@i \land \psi(\Phi_{s[p]}(T))) \\
\Phi_{s[p]} (?(q, U).T) &= \exists i, z. (\text{inp}(s_{pq}, z)@i \land \psi(\Phi_{s[p]}(T))) \\
\Phi_{s[p]} (\oplus\langle q, \{l_i : T_i\}_{i \in I}\rangle) &= \exists i. \bigvee_{j \in I} (\text{sel}(s_{pq}, l_j)@i \land \psi(\Phi_{s[p]}(T_j))) \\
\Phi_{s[p]} (&(q, \{l_i : T_i\}_{i \in I})) = \exists i. \bigvee_{j \in I} (\text{bra}(s_{pq}, l_j)@i \land \psi(\Phi_{s[p]}(T_j))) \\
\Phi_{s[p]} (\text{end}) &= \exists i. \text{close}@i.
\end{align*}
$$

where $\psi(\Phi_{s[p]}(T)) := \forall k.(\Phi_{s[p]}(T)(k) \Rightarrow i \prec k))$ the quantified variables have sorts $i, j, k$: $\text{temp}$ and $z: S$, and variables $i$ and $z$ are fresh. The extension of $\Phi(-)$ to session environments, denoted $\hat{\Phi}(-)$, is as expected: $\hat{\Phi}(\Delta, s[p] : T) = \hat{\Phi}(\Delta) \land \Phi_{s[p]}(T)$.

**Remark 2.** Since each local type is associated to a unique local formula, the mapping $\Phi_{-}(-)$ is invertible. That said, from a local formula $\varphi$ we can obtain the corresponding type $\Phi^{-1}(\varphi)$. For instance, for the local formula $\varphi_{\text{out}} := \exists i. (\text{out}(s_{pq}, z)@i \land \psi(\Phi_{s[p]}(T)))$, one has $\Phi^{-1}(\varphi_{\text{out}}) = s[p] : !\langle q, S \rangle. \Phi^{-1}_{s[p]}(\varphi')$. The other cases are similar.

The following theorems give a bi-directional connection between (a) well-typedness and (b) satisfiability of the corresponding local formulas (see [15]):

**Theorem 4.** Let $\Gamma \vdash P \triangleright \Delta$ be a well-typed $S$ process. Also, let $\text{tr} \in \text{traces}(\llbracket \llbracket P \rrbracket \rrbracket)$. Then there exists a $\theta$ such that $(\text{tr}, \theta) \models \hat{\Phi}(\Delta)$.

**Theorem 5.** Let $\text{tr}$ and $\varphi$ be a trace and a local formula, respectively. Suppose $\theta$ is an instantiation such that $(\text{tr}, \theta) \models \varphi$. Then there is a $P \in S$ such that

$$ \Gamma_{\varphi} \vdash P \triangleright \Phi^{-1}(\varphi) \quad \text{where } \Gamma_{\varphi} = \{\theta(x) : \text{sort}(x) \mid x \in \text{dom}(\theta)\} $$
*Example 2.* The projection of $G_{init}$ onto participant 3 (Buyer1), under session s is: $s[3]: !\langle 1, string \rangle .? (1, int) .!\langle 2, int \rangle .&(2, \{ok : (G_{contract}|_3), \neg ok : end\})$.

The local formula associated is:

$$ \Phi_{s[3]}(T) = \exists i_1, z_1. \mathit{out}(s_{31}, z_1) @ i_1 \wedge (\exists i_2 z_2. \mathit{inp}(s_{31}, z_2) @ i_2 \wedge (\exists i_3 z_3. \mathit{out}(s_{32}, z_3)) @ i_3 \\ \wedge (\exists i_4 i_5 z_4. ((\mathit{bra}(s_{32}, \mathit{ok}) @ i_4 \wedge \Phi_{s[3]}(T')) \vee \mathit{bra}(s_{32}, \neg \mathit{ok}) @ i_4 \wedge \mathit{close}(i_5))) \\ \wedge ((i_1 < i_2 < i_3 < i_4 \wedge \psi(\Phi_{s[3]}(T')))) \vee (i_1 < i_2 < i_4 < i_5 \wedge \psi(\Phi_{s[3]}(T')))) $$

where $T'$ is the projection of $G_{contract}$ onto participant 3.

# 6 Revisiting the Two-Buyer Contract Signing Protocol

We recall the motivating example introduced in § 2. Using a combination of constructs from S and A, we first develop a protocol specification which is compiled down to A using our encoding; the resulting A process can be then used to verify authentication and protocol correctness properties in SAPIC/Tamarin. Figure 2 shows the corresponding global types, and their associated local types (obtained via projection following [10]).

An alternative approach to specification/verification would be as follows. First, specify the protocol using S only, abstracting away from cryptography, and using existing type systems for S to enforce protocol correctness. Then, compile this resulting S specification down to A, where the resulting specification can be enhanced with cryptographic exchanges and authentication properties can be enforced with SAPIC/Tamarin.

## 6.1 Process Specification

Process specifications for $B_i$ and $S$ are as follows:

$$ B_1 = \bar{a}[3](y).y[3]!\langle 1, \text{"Title"} \rangle.y[3]?(1, x_1).y[3]!(2, x_1 \text{ div } 2).y[3]&(2, \{\text{ok} : B_1^{\text{sct}}, \neg \text{ok} : \mathbf{0}\}) $$

$$ B_2 = a[2](y).y[2]?(1, x_2).y[2]?(3, x_3).\mathit{if} x_2 - x_3 \le 99 \mathit{then} y[2] \oplus (\{1, 3\}, \mathit{ok}).B_2^{\text{sct}} \\ \mathit{else} y[2] \oplus (\{1, 3\}, \neg \mathit{ok}).\mathbf{0} $$

$$ S = a[1](y).y[1]?(3, x_1).y[1]!(\{2, 3\}, \text{quote}).y[1]&(2, \{\text{ok} : \bar{b}[2](z).y[2]!\langle 1, y \rangle.z[2]?(1, x_4). \\ y[1]!\langle 2, \text{date} \rangle.\mathbf{0}, \neg \text{ok} : \mathbf{0}\}) $$

where processes $B_1^{sct}$ and $B_2^{sct}$, which implement the contract signing phase, are as in Tables 9 and 10, respectively. The specification for the trusted authority $T$ is as follows:

$$ \begin{array}{l} b[1](z).z[1]?(2, t).\nu sk(T); t[3]!(\{1, 2\}, pk(sk(T))).y[1]?(3, z_2).y[1]?(2, z_3).(\nu s)\mathit{insert}((s, init)). \\ (\nu ct)t[3]!(\{1, 2\}, ct).t[3]&(\{1, 2\}, \{\mathit{abort} : P_{Ab}^T, \mathit{res}_1 : P_{R_1}^T, \mathit{res}_2 : P_{R_2}^T, \mathit{success} : z[1]!\langle 2, \mathit{ok} \rangle.\mathbf{0}\}) \end{array} $$

where processes $P_{Ab}^T$, $P_{R_1}^T$, and $P_{R_2}^T$ are given in Tables 11 and 12. Process T illustrates how we may combine constructs from S (important to represent, e.g., session establishment on b and delegation from S) and features from A (essential to, e.g., manipulate the memory cell s, which records contract information). Indeed, T uses the A construct `insert` to initialize the cell s and `lookup` _ as _ to update it. Therefore, the sound and complete encoding proposed in § 4 allows us to specify processes in A, while retaining the high-level constructs from S.
$$
\begin{align*}
B_1^{\text{sct}} &= y[3]?(1, z_1).\nu\text{sk}(B_1).y[3]!(\{1, 2\}, pk(sk(B_1))).y[3]?(2, z_3).y[3]?(1, z_4). \\
&\qquad y[3]!(2, m_1).y[3]\&(2, \{\ok : P_{\text{conv}}^1, \not\ok : \mathbf{0}\}))
\end{align*}
$$

$$
\begin{align*}
P_{\text{conv}}^{1} &= y[3]?(2, z_5). (\text{if } \text{pcsver}(z_3, pk(sk(B_1)), z_1, z_4, z_5) = \text{true then } (y[3] \oplus (2, \text{ok})). \\
&\qquad y[3]!(2, S_1). y[3]\&(2, \{\text{ok} : P_{\text{sign}}^{1}, \neg\text{ok} : P_{\text{res}}^{1}\}) \text{ else } y[3] \oplus (1, \text{abort}). P_{\text{abort}}^{1})
\end{align*}
$$

$$
P_{\text{sign}}^{1} = y[3]?(2, z_6). (\text{if } \text{sver}(z_3, z_4, z_6) = \text{true then } (y[3] \oplus (1, \text{success}).\mathbf{0} \text{ else } P_{\text{res}}^{1})
$$

$$
P_{\text{res}}^{1} = y[3] \oplus (1, \text{res}_1).y[3]!(1, (S_1, x_1)).y[3]?(1, z_7).\mathbf{0}
$$

$$
P_{\text{abort}}^{1} = y[3] \oplus (1, \text{abort}).y[3]!(1, [ct, B_1, B_2, \text{abort}]_{B_1}).y[3]?(1, z_8).\mathbf{0}
$$

<caption>**Table 9.** $B_1^{sct}$: $B_1$'s contract signing processes. $[m]_X$ denotes $\langle m, \text{sign}(sk(x), m) \rangle$</caption>

$$
\begin{align*}
B_2^{\text{sct}} &= y[2]?(1, z_1).y[2]?(1, z_2).\nu\text{sk}(B_2).y[2]!(\{1, 3\}, pk(sk(B_2))).y[2]?(3, z_9).y[2]?(3, z_{10}). \\
&\quad (\text{if } \text{pcsver}(z_2, pk(sk(B_2)), z_1, z_4, z_{10}) = \text{true then } (y[2] \oplus (3, \text{ok}).y[2]!(3, m_2)). \\
&\qquad y[2]\&(3, \{\text{ok} : P_{\text{sign}}^2, \neg\text{ok} : \mathbf{0}\}) \text{ else } y[2] \oplus (3, \neg\text{ok}).\mathbf{0})
\end{align*}
$$

$$
\begin{align*}
P_{\text{Sign}}^{2} &= y[2]?(3, z_{11}).\text{if } \text{sver}(z_2, z_4, z_{11}) = \text{true then } y[2] \oplus (3, \text{ok}).y[2]!(3, S_2). \\
&\qquad y[2] \oplus (1, \text{success}).\mathbf{0} \text{ else } y[2] \oplus (3, \neg\text{ok}).P_{\text{resolve}}^{2}
\end{align*}
$$

$$
P_{\text{resolve}}^{2} = y[2] \oplus (1, \text{res}_2).y[2]!(1, S_2).y[2]?(1, z_{12}).\mathbf{0}
$$

<caption>**Table 10.** $B_2^{sct}$: $B_2$'s contract signing processes.</caption>

$$
\begin{align*}
P_{Ab}^{T} &= \mathit{lock} s; y[1]?(3, y_1). \mathit{if} \ \mathit{sver}(\mathit{fst}(y_1), \mathit{snd}(y_1)) = \mathit{true} \ \mathit{then} \ (\mathit{lookup} s \ \mathit{as} \ y_2 \ \mathit{in} \\
& \qquad (\mathit{if} \ \mathit{fst}(y_2) = \mathit{init} \ \mathit{then} \ (\mathit{insert}((s, [y_1]_T)); y[1]!(3, [y_1]_T); \mathit{ unlock} \ s_{pq})) \\
& \qquad \mathit{else} \ (\mathit{if} \ \mathit{fst}(y_2) = \mathit{abort} \ \mathit{then} \ y[1]!(3, y_2); \mathit{ unlock} \ s_{pq}))) \\
& \qquad \mathit{else} \ \mathit{if} \ \mathit{fst}(y_2) = \mathit{res}_i \ \mathit{then} \ y[1]!(3, y_2); \mathit{ unlock} \ s_{pq}))
\end{align*}
$$

<caption>**Table 11.** $P_{Ab}^T$: abort process executed by T</caption>

To model the second phase of the protocol, we consider a Private Contract Signature

$$
\Sigma_{\text{pcs}} = \{aenc(-, -), senc(-, -), pk(-), sk(-), pcs, sign, tsign, sdec(, ), adec(, ), sconvert, tconvert, pcsver, sverif\}
$$

with function symbols for promises and signatures, and for verifying the validity of
exchanged messages. As for constructors: pcs(x, y, w, z) is the promise of x to y to
sign contract z given by w; sign(x, y) is the signature of x in z; pk(x) is the public key
of x; sk(x) is the secret key of x; aenc(x, y) is the asymmetric encryption of y using
key x; and senc(x, y) is the symmetric encryption of y using key x. Destructor sdec(, )
 resp. adec(, ) enforces symmetric (resp. asymmetric) decryption; the other destructors
( sconvert, tconvert, pcsver, sverif ) are defined from the rules in Epcs:

$$
sdec(x, senc(x, y)) \to y \qquad tconvert(w, pcs(x, y, pk(w), z)) \to sign(x, z)
$$

$$
\mathrm{adec}(\mathrm{sk}(x), \mathrm{aenc}(\mathrm{pk}(x), y)) \to y \qquad \mathrm{pcsver}(\mathrm{pk}(x), y, w, z, \mathrm{pcs}(x, y, w, z)) \to \mathrm{true}
$$

$$
\mathrm{sver}(\mathrm{pk}(x), z, \mathrm{sign}(x, z)) \to \mathrm{true} \qquad \mathrm{sconvert}(x, \mathrm{pcs}(x, y, w, z)) \to \mathrm{sign}(x, z)
$$

Table 13 shows the translation of $B_1$ in A, using our encoding. For simplicity, we
omit the details related to the session establishment (using NSL), which follow Table 7.
$P_{res_1}^T = \text{lock } s; y[1]?(3, y_3). \text{ if } m'_{11} =_{E_{pcs}} \text{ true then } (\text{if } m'_{12} =_{E_{pcs}} \text{ true then } (\text{lookup } s \text{ as } y_3 \text{ in } (\text{if } \text{fst}(y_3) = \text{abort then } y[1]!(3, \text{snd}(y_3)). \text{ unlock } s)) \\
\text{else } (\text{if } \text{fst}(y_3) = \text{res}_2 \text{ then } y[1]!(3, \text{snd}(y_3)). z[1]!(2, \text{ok}). \text{ unlock } s)) \\
\text{else } y[1]!(3, \text{tconvert}(\text{sk}(T), \text{snd}(m'_1))). z[1]!(2, \text{ok}). \text{ unlock } s))$

$P_{res_2}^T = \text{lock } s; y[1]?(2, w_3); \text{ if } m'_{21} =_{E_{pcs}} \text{ true then } (\text{if } m'_{22} =_{E_{pcs}} \text{ true then } (\text{lookup } s \text{ as } w_3 \text{ in } (\text{if } \text{fst}(w_3) = \text{abort then } y[1]!(2, \text{snd}(w_3)); \text{ unlock } s)) \\
\text{else } (\text{if } \text{fst}(w_3) = \text{res}_1 \text{ then } (y[1]!(2, \text{snd}(w_3)); z[1]!(2, \text{ok}); \text{ unlock } s)) \\
\text{else } y[1]!(3, \text{tconvert}(\text{sk}(T), \text{fst}(m'_2))); \text{ insert}((s, \langle \text{res}_2, \text{snd}(w_3) \rangle)); \\
z[1]!(2, \text{ok}); \text{ unlock } s))$

<caption>**Table 12.** $P_{res_1}^T$ e $P_{res_2}^T$: resolve processes executed by T</caption>

```
\nu s; P_{31}; P_{32}; \text{insert}((\tilde{s}_{ij}, \emptyset)); \text{event init}(\tilde{s}_{ij}); \text{event sndchann}(pk(ska_{31}), pk(y_1), s);
out(u_1, s); \text{event} \text{sndchann}(pk(ska_{32}), pk(y_2), s); out(u_2, s);
lock s_{31}; \text{lookup } s_{31} \text{ as } x_{31} \text{ in}
\quad \text{insert}((s_{31}, x_{31} \cdot \langle \text{msg}, \text{"Title"} \rangle)); \text{event out}(s_{31}, \text{"Title"}); \text{unlock } s_{31};
lock s_{13}; \text{lookup } s_{13} \text{ as } x \text{ in}
\quad \text{if } \text{fst}(x) = \langle \text{msg}, z \rangle \text{ then } \text{insert}((s_{31}, \text{snd}(x))); \text{event inp}(s_{31}, z); \text{ unlock } s_{13}
lock s_{32}; \text{lookup } s_{32} \text{ as } x_{32}; \text{ in}
\quad \text{insert}((s_{32}, \langle \text{msg}, \text{"quote"} \rangle)); \text{event out}(s_{32}, \text{"quote"}); \text{ unlock } s_{32};
lock s_{23}; \text{lookup } s_{23} \text{ as } x_{23} \text{ in } (\text{if } \text{fst}(x_{23}) = \langle \text{lbl}, \text{ok} \rangle \text{ then}
\quad \text{insert}((s_{23}, \text{snd}(x_{23}))); \text{event bra}(s_{23}, \text{accept}); \text{ unlock } s_{23}; \llbracket B_1^{\text{sct}} \rrbracket
\quad \text{else } \text{event bra}(s_{23}, \neg \text{ok}); \text{ unlock } s_{23}; 0)
```

<caption>**Table 13.** Translation of $B_1$ into A.</caption>

Process specifications for $B_2$, $S$, and $T$ in A can be obtained similarly. As mentioned in § 4, the communication is done via updating session queues $s_{ij}$, for $i, j = 1, 2, 3$.

## 6.2 Using SAPIC/Tamarin to Verify Authentication and Local Session Types

We conclude this section by briefly discussing how to use our developments to verify properties associated to authentication and protocol correctness.

Concerning authentication, we can use SAPIC/Tamarin to check the correctness of the authentication phase implemented by NSL. The proof checks that events honest(-), sndnonce(-, -, -), rcvnonce(-, -, -), and rcvchann(-, -, -) occur in the order specified by the encoding in Table 7. This way, e.g., the following lemma verifies the correctness of the specification of the fragment of NSL authentication with respect to participant $B_2$:

```
lemma B2_NSL correctness :
exists - trace
(All pk_{12} pk_{1s} pk_2 pk_s #i #j #k #l.
    honest(pk_{12})@i & honest(pk_{1s})@j & honest(pk_2)@k & honest(pk_s)@l
    =\> (Ex x y z s #j_1 #k_1 #l_1.rcvnonce(pk_{12}, pk_2, x, y)@j_1 & sndnonce(pk_2, pk_{12}, z)@k_1
        & rcvchann(pk_{12}, pk_2, s)@l_1 & j_1 < k_1 & k_1 < l_1))
```
The lemma below says that the session channel exchanged using NSL is secret. The proof relies on asymmetric-encryption, which is built in the Tamarin library.

lemma Chann_is_secret :
(All pk12 pk2 pk1s pk8 s z n x y w z n2 #i #j #l #i1 #i2 #j1 #j2 #k1 #l1 #l2.
(honest(pk12)@i& honest(pk2)@j & honest(pk1s)@k & honest(pk8)@l
& sndnonce(pk2, pk12, z)@i1 & rcvnonce(pk2, pk12, n, z)@j1 & sndnonce(pk12, pk2, w)@i2
& rcvnonce(pk12, pk2, n2, w)@j2 & sndnonce(pk8, pk1s, x)@i3 & rcvnonce(pk8, pk1s, y, x)@j2
& sndchann(pk12, k2, s)@k1 & rcvchann(pk12, pk2, s)@k2 & sndchann(pk1s, pk8, s)@l1
& rcvchann(pk12, pk2, s)@l2) = not(Ex #j. KU(s)@j))

We now consider properties associated to fidelity/safety of processes with respect to their local types. The lemma below ensures protocol fidelity of $B_1$ and $B_2$ with respect to the corresponding projections of the global type $G_{init}$, presented in Figure 2. The corresponding local formula can be obtained following Definition 4:

lemma B1_B2_protocol_fidelity :
exists - trace
(Ex x y z s #j #j1 #k #k1 #l.out(s31, x)@j & inp(s31, z)@k & out(s32, s)@l & j < k & k < l
& ((bra(s32, ok))@j1 & l < j1) | (bra(s32, not ok)@k1 & l < k1 & Φ(G_contract|3))) &
(Ex x y z s #j #j1 #k #k1 #l. inp(s21, z)@k & inp(s23, s)@l & j < k & k < l
&((sel(s23, ok)@j1 & l < j1 & Φ(G_contract|2)) | (sel(s23, not ok)@k1 & l < k1)))

Using similar lemmas, we can also prove protocol fidelity for processes *S* and *T* with respect to the projections of the global types presented in Figure 2.

# 7 Related Works and Concluding Remarks

We have connected two distinct process models: the calculus S for multiparty session-based communication [10] and the calculus A for the analysis of security protocols [12]. To our knowledge, this is the first integration of sessions (in the sense of [11]) within process languages for security protocol analysis. Indeed, research on security extensions to behavioral types (cf. the survey [2]) seems to have proceeded independently from approaches such as those overviewed in [7]. The work in [6] is similar in spirit to ours, but is different in conception and details, as it uses a session graph specification to generate a cryptographic functional implementation that enjoys session integrity. Extensions of session types (e.g., [4,16]) address security issues in various ways, but do not directly support cryptographic operations, global state, nor connections with “applied” languages for (automated) verification, which are all enabled by our approach.

Our work should be mutually beneficial for research on (a) behavioral types and contracts and on (b) automated analysis of security protocols: for the former, our work enables the analysis of security properties within multiparty session protocols; for the latter, our approach enables protocol specifications enriched with high-level communication structures based on sessions. In ongoing work, we have used SAPIC/Tamarin to implement our encodings and the verification technique for communication correctness, based on local formulas (Def. 4). Results so far are very promising, as discussed in § 6.

In future work, we intend to explore our approach to process specification and verification in the setting of ProVerif [3], whose input language is a typed applied $\pi$-calculus. We also plan to connect our approach with existing type systems for secure information flow and access control in multiparty sessions [4].
*Acknowledgements* We are grateful to the anonymous reviewers for their useful remarks and suggestions. Pérez is also affiliated to the NOVA Laboratory for Computer Science and Informatics (supported by FCT grant NOVA LINCS PEst/UID/CEC/04516/2013), Universidade Nova de Lisboa, Portugal.

References

1. M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Proc. of POPL'01, pages 104–115, 2001.

2. M. Bartoletti, I. Castellani, P. Deniélou, M. Dezani-Ciancaglini, S. Ghilezan, J. Pantovic, J. A. Pérez, P. Thiemann, B. Toninho, and H. T. Vieira. Combining behavioural types with security analysis. *J. Log. Algebr. Meth. Program.*, 84(6):763–780, 2015.

3. B. Blanchet. Modeling and verifying security protocols with the applied pi calculus and proverif. *Foundations and Trends in Privacy and Security*, 1(1-2):1–135, 2016.

4. S. Capecchi, I. Castellani, and M. Dezani-Ciancaglini. Typing access control and secure information flow in sessions. *Inf. Comput.*, 238:68–105, 2014.

5. M. Coppo, M. Dezani-Ciancaglini, L. Padovani, and N. Yoshida. A gentle introduction to multiparty asynchronous session types. In *Formal Methods for Multicore Programming*, volume 9104 of LNCS, pages 146–178. Springer, 2015.

6. R. Corin, P. Deniélou, C. Fournet, K. Bhargavan, and J. J. Leifer. Secure implementations for typed session abstractions. In Proc. of CSF 2007, pages 170–186. IEEE, 2007.

7. V. Cortier and S. Kremer. Formal models and techniques for analyzing security protocols: A tutorial. *Foundations and Trends in Programming Languages*, 1(3):151–267, 2014.

8. J. A. Garay, M. Jakobsson, and P. D. MacKenzie. Abuse-free optimistic contract signing. In Proc. of CRYPTO'99, volume 1666 of LNCS, pages 449–466. Springer, 1999.

9. K. Honda, V. T. Vasconcelos, and M. Kubo. Language Primitives and Type Discipline for Structured Communication-Based Programming. In *ESOP'98*, number 1381 in LNCS, 1998.

10. K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In *POPL*, pages 273–284, 2008.

11. H. Hüttel, I. Lanese, V. T. Vasconcelos, L. Caires, M. Carbone, P. Deniélou, D. Mostrous, L. Padovani, A. Ravara, E. Tuosto, H. T. Vieira, and G. Zavattaro. Foundations of session types and behavioural contracts. *ACM Comput. Surv.*, 49(1):3, 2016.

12. S. Kremer and R. Künnemann. Automated analysis of security protocols with global state. In Proc. of SP 2014, pages 163–178. IEEE, 2014.

13. G. Lowe. Breaking and fixing the needham-schroeder public-key protocol using FDR. Software - Concepts and Tools, 17(3):93–102, 1996.

14. S. Meier, B. Schmidt, C. Cremers, and D. A. Basin. The TAMARIN prover for the symbolic analysis of security protocols. In Proc. of CAV 2013, volume 8044 of LNCS, pages 696–701. Springer, 2013.

15. D. Nantes and J. A. Pérez. Relating Process Languages for Security and Communication Correctness (Full Version). Technical report, 2018. http://www.jperez.nl.

16. F. Pfenning, L. Caires, and B. Toninho. Proof-carrying code in a session-typed process calculus. In Proc. of CPP 2011, volume 7086 of LNCS, pages 21–36. Springer, 2011.