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

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) $\pi$-calculus for multiparty sessions into a (low-level) applied $\pi$-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.

Work partially funded by FAP-DF 0193.001381/2017.

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 $\pi$-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 $\pi$-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:

• $\mathsf {A}$, a (low-level) applied $\pi$-calculus in which processes explicitly describe term communication, cryptographic operations, and state manipulation [12];

• $\mathsf {S}$, a (high-level) $\pi$-calculus in which communication actions are organized as multiparty session protocols [5, 10].

Our aim is to exploit the complementary strenghts of $\mathsf {A}$ and $\mathsf {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 $\mathsf {S}$ into $\mathsf {A}$ describes how the structures typical of session-based, asynchronous concurrency can be compiled down, in a behavior-preserving manner, as 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 ($\mathsf {S}$) and of security protocols ($\mathsf {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 $\mathsf {S}$ can now integrate cryptographic operations and be analyzed by (re)using existing methods. In fact, since $\mathsf {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 $\mathsf {S}$ processes and toolsets for the analysis of security properties:

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. Section 2 introduces the Two-Buyer Contract Signing Protocol, a protocol that is representative of the kind of systems that is hard to specify using $\mathsf {S}$ or $\mathsf {A}$ alone. Section 3 recalls the definitions of $\mathsf {S}$ and $\mathsf {A}$, and also introduces $\mathsf {S}^\star$, which is a variant of $\mathsf {S}$ that is useful in our developments. Section 4 defines the encoding of $\mathsf {S}$ into $\mathsf {A}$, using $\mathsf {S}^\star$ as stepping stone, and establishes its correctness (Theorems 1, 2, and 3). Section 5 shows how our encoding can be used to reduce the enforcement of protocol conformance in $\mathsf {S}$ to the model checking of local formulas for $\mathsf {A}$ (Theorems 4 and 5). Section 6 revisits the Two-Buyer Contract Signing Protocol: we illustrate its process specification using $\mathsf {S}$ minimally extended with constructs from $\mathsf {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 (Sect. 7). Additional technical material and further examples are given in an appendix available online [15].

Fig. 1.

The trusted Buyers-Seller protocol.

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 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 replying to the following requests: $\texttt {success}$ (in case of successful communication), $\texttt {abort}$ (request to abort the protocol), or $\texttt {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 $\texttt {success}$ message; otherwise, $B_1$ sends T a $\texttt {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 $\texttt {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, $\mathsf {S}$ and $\mathsf {A}$ offer complementary advantages in modeling and analyzing the Trusted Buyers-Seller Protocol. On the one hand, $\mathsf {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 $\texttt {success}$, $\texttt {abort}$ and $\texttt {resolve}$ in the second phase. Hence, $\mathsf {S}$ and its type-based verification techniques can be used to establish fidelity and safety properties. However, $\mathsf {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 sigining phase. The lack of these constructs prevents the formal analysis of authentication properties. On the other hand, $\mathsf {A}$ compensates for the shortcomings of $\mathsf {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 $\mathsf {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 $\mathsf {S}$.

Our encoding from $\mathsf {S}$ into $\mathsf {A}$, given in Sect. 4, will serve to combine the individual strengths of both languages. In Sect. 6, we will revisit this example: we will give a process specification using an extension of $\mathsf {S}$ with some constructs from $\mathsf {A}$. This is consistent, because $\mathsf {A}$ is a low-level process language, and our encoding will define how to correctly compile $\mathsf {S}$ down to $\mathsf {A}$ (constructs from $\mathsf {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: $\mathsf {A}$ and $\mathsf {S}$

3.1 The Applied $\pi$- Calculus ($\mathsf {A}$)

Preliminaries. As usual in symbolic protocol analysis, messages are modelled by abstract terms ($t, t', \ldots$). We assume a countably infinite set of variables $\mathcal {V}$, a countably infinite set of names $\mathcal{N}=\text{ PN } \cup \text{ FN }$ ($\text{ FN }$ for fresh names, $\text{ PN }$ for public names), and a signature $\varSigma$ (a set of function symbols, each with its arity).

We denote by $\mathcal {T}_\varSigma$ the set of well-sorted terms built over $\varSigma$, $\mathcal{N}$, and $\mathcal {V}$. The set of ground terms (i.e., terms without variables) is denoted $\mathcal {M}_\varSigma$. A substitution is a partial function from variables to terms. We denote by $\sigma =\{t_1/x_1, \ldots , t_n/x_n\}$ the substitution whose domain is $Dom(\sigma )=\{x_1, \ldots , 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}_\varSigma$, 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\ne b \Rightarrow a\ne _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,\ldots , t_k)| \ t_i \in \mathcal {T}_\varSigma , F\in \varSigma _{fact} \ \text{ of } \text{ arity } \ k \}$, where $\varSigma _{fact}$ is an unsorted signature, disjoint from $\varSigma$. 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.

Table 1. Syntax of $\mathsf {A}$: terms and processes.

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 $\mathsf {A}$ inherits from the applied $\pi$-calculus [1] input and output constructs in which terms appear both as communication subjects and objects. Also, $\mathsf {A}$ includes a conditional construct based on term equality, as well as constructs for reading from and updating an explicit global state:

• first binds the value N to a key M and then proceeds as P. Successive inserts may modify this binding; simply “undefines” the mapping for the key M and proceeds as P.

• 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.

• and 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 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 $\mathsf {A}$, which is defined 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 \text {FN}$ is the set of fresh names generated by the processes; $\mathcal {S}: \mathcal {M}_{\varSigma }\rightarrow \mathcal {M}_\varSigma$ 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}_{\varSigma }$ is the set of currently acquired locks. We write $\mathcal {S}(M)=\bot$ 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}.\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}.\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.

Table 2. Deduction rules for $\mathsf {A}$. In rule [Appl]: $\widetilde{t}=(t_1, \ldots , t_n)$.

Table 3. Operational semantics for $\mathsf {A}$.

Transitions are of the form , where $\mathcal {F}$ is a set of ground facts (see Table 3). We write for and for . As usual, denotes the reflexive, transitive closure of . Transitions denote either standard process operations or operations on the global state; they are sometimes denoted and , respectively.

3.2 Multiparty Session Processes ($\mathsf {S}$)

Syntax. The syntax of processes, ranged over by $P, Q, \ldots$ and that of expressions, ranged over by $e,e', \ldots$, 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, \ldots$ and another ranges over session names $s, s', \ldots$. Variables range over $x,y, \ldots$; participants (or roles) range over the naturals and are denoted as $\mathtt {p},\mathtt {q}, \mathtt {p}', \ldots$; labels range over $l,l',\ldots$ and constants range over $\texttt {true}, \texttt {false}, \ldots$. We write $\widetilde{\mathtt {p}}$ to denote a finite sequence of participants $\mathtt {p}_1, \ldots , \mathtt {p}_n$ (and similarly for other elements). Given a session name s and a participant $\mathtt {p}$, we write $s [{\mathtt {p}}]$ to denote a (session) endpoint.

Table 4. Process syntax and naming conventions for $\mathsf {S}$.

The intuitive meaning of processes is as in [5, 10]. The processes $\overline{u}[{\mathtt {p}}](y).{P}$ and $u[{\mathtt {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 replaced by an endpoint of the form $s [{\mathtt {p}_i}]$ (i.e., the runtime channel of $\mathtt {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 \mathtt {p}, l\rangle .P$ and $c\, \& (\mathtt {p},\{ l_i : P_{i}\}_{i\in I})$). The input/output operations (including delegation) specify the channel and the sender or the receiver, respectively.

Message queues model asynchronous communication. A message $(\mathtt {p} \triangleright \mathtt {q}\!:\! v)$ indicates that $\mathtt {p}$ has sent a value v to $\mathtt {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 [{\widetilde{\mathtt {p}}}]:h$ we denote the queue h of the session s initiated between participants $\widetilde{\mathtt {p}} = \mathtt {p}_1, \ldots , \mathtt {p}_n$; when the participants are clear from the context we shall write s : h instead of $s [{\widetilde{\mathtt {p}}}]:h$.

Request/accept actions bind channel variables, value receptions bind value variables, channel receptions bind channel variables, hidings bind shared and session names. In $(\nu s) P$ all occurrences of $s [{\mathtt {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.

Table 5. Structural congruence for $\mathsf {S}$ processes.

Table 6. Reduction rules for $\mathsf {S}$ (Rule [If-F] omitted).

Semantics. $\mathsf {S}$ processes are governed by a reduction semantics, which relies on a structural congruence relation, denoted $\equiv$ and defined by adding $\alpha$-conversion to the rules of Table 5. Reduction rules are given in Table 6; we write $P \longrightarrow _{\mathsf {S}}P'$ for a reduction step. We rely on the following syntax for contexts: .

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[\widetilde{\mathtt {p}}]:\emptyset$ in the rule). Rules [Send], [Deleg] and [Sel] add values, channels and labels, respectively, into the message queue; in Rule [Send], $e\downarrow 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 $\mathsf {S}^\star$

We now introduce $\mathsf {S}^\star$, a variant of $\mathsf {S}$ which will simplify the definition of our encoding into $\mathsf {A}$. The syntax of $\mathsf {S}^\star$ processes is as follows:

where $c_{\mathtt {p}\mathtt {q}}$ denotes a channel annotated with participant identities, $h \,{::=}\, h\!\cdot \! m \mathord {\;\mathbf {|}\;}\emptyset$ and $m \,{::=}\, \langle {\mathtt {msg}}, v\rangle \mathord {\;\mathbf {|}\;}\langle {\mathtt {chan}},s_{{\mathtt {p}}{\mathtt {q}}}\rangle \mathord {\;\mathbf {|}\;}\langle {\mathtt {lbl}}, l\rangle$. The main differences between $\mathsf {S}$ and $\mathsf {S}^\star$ are:

• Intra-session communication relies on annotated channels, and output prefixes include a sort for the communicated messages (${\mathtt {msg}}$ for values, ${\mathtt {chan}}$ for delegated sessions, ${\mathtt {lbl}}$ for labels).

• While $\mathsf {S}$ uses a single queue per session, in $\mathsf {S}^\star$ for each pair of participants there will be two queues, one in each direction. This simplifies the definition of structural congruence $\equiv$ for $\mathsf {S}^\star$, which results from that for $\mathsf {S}$ as expected and is omitted.

• Constructs for session request and acceptance in $\mathsf {S}^\star$ depend on a sequence of variables, rather than on a single variable. In these constructs, denoted $\overline{u}[{\mathtt {p}}](\widetilde{y}).{P}$ and $u[{\mathtt {p}}](\widetilde{y}).{P}$, respectively, $\widetilde{y}$ is a sequence of variables of the form $y_{\mathtt {p}\mathtt {q}}$, for some $\mathtt {p}$, $\mathtt {q}$.

With these differences in mind, the reduction semantics for $\mathsf {S}^\star$, denoted $\longrightarrow _{\mathsf {S}^\star }$, follows that for $\mathsf {S}$ (Table 6). Reduction rules for $\mathsf {S}^\star$ include the following:

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

It is straightforward to define an auxiliary encoding . For instance:

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

Theorem 1

Let $P \in \mathsf {S}$. Then: (a) If $P \longrightarrow _{\mathsf {S}}P'$, then .

(b) If , then there exists $P' \in \mathsf {S}$ such that $P \longrightarrow _{\mathsf {S}}P'$ and .

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

4 Encoding $\mathsf {S}^\star$ into $\mathsf {A}$

We now present our encoding and establish its correctness. The encoding is defined in Table 7; it uses the set of facts 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 , $\mathtt{fst}$ and $\mathtt{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 $\mathcal {S}$. In SAPIC, we implement queues $y_{{\mathtt {p}}{\mathtt {q}}}$ and as $q(y, \mathtt{p}, \mathtt{q})$ and $q(y, \mathtt{q}, \mathtt{p})$, respectively, where q is a function symbol for queues. Also, $s_{{\mathtt {p}}{\mathtt {q}}}:\emptyset$ is implemented as .

Table 7. Encoding from $\mathsf {S}^\star$ to $\mathsf {A}$.

Session Initiation. The (high-level) mechanism of session initiation of Rule [Init] in $\mathsf {S}^\star$ (Table 6) is implemented in $\mathsf {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 . 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 first acquires a lock in the queue $c_{{\mathtt {p}}{\mathtt {q}}}$ to avoid interference. Then, a process checks the state of $c_{{\mathtt {p}}{\mathtt {q}}}$ and enqueues message at its end. Finally, the encoding signals this operation by executing before unlocking $c_{{\mathtt {p}}{\mathtt {q}}}$ and proceeding as as $\llbracket P \rrbracket$. The encoding of session delegation is very similar: the only differences are the sort of the communicated object and the event signaled at the end ().

As above, process first acquires a lock and checks the queue . If it is of the form then it stores it in a variable $z_v$: it consumes the first part ($\textit{fst}(z_v)$) and updates $c_{{\mathtt {q}}{\mathtt {p}}}$ with the second part. The implementation then signals an event before unlocking and proceeding as $\llbracket P \rrbracket$. Process (reception of a delegated session) is similar; in this case, the queue should contain a value of sort ${\mathtt {chan}}$ and the associated event is .

Process simply executes an event $\mathsf {close}$. In the prototype SAPIC implementation of our encoding, this event mentions the name of the corresponding session .

Finally, process is $\mathbf {0}$ because we implement queues using the global state in $\mathsf {A}$. The implementation of the remaining constructs in $\mathsf {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., ), use the input of a dummy value that allows processes to reduce.

Correctness of $\llbracket \cdot \rrbracket$ . We first associate to each ground process $P\in \mathsf {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 process , with . A process configuration for R, denoted , is defined as:

$$\begin{aligned} (\mathcal {E}\!\cup \!\{s\}, \mathcal {S}\cup \{s_{{\mathtt {p}_j}{\mathtt {q}_k}}:h_{j,k}\,|\, j,k \in I'\}, \Big \{\prod _{i\in I}\llbracket P_i \rrbracket \Big \}, \sigma , \mathcal {L}), \end{aligned}$$

where and $\sigma$ is grounding for $x_i$, $i=1,\ldots ,n$.

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

Theorem 2

(Completeness). Let $P \in \mathsf {S}^\star$. If $P\longrightarrow _{\mathsf {S}^\star }P'$ then for all process configuration C, there exists a process configuration $C'$ such that .

Proof

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

   $\square$

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

Theorem 3

(Soundness). Let $P\in \mathsf {S}^\star$ and C be such that . Then there exist $P'\in \mathsf {S}^\star$, a $C'$, and $\lambda$ such that and .

5 Multiparty Session Types and Their Local Formulas

Using and $\llbracket \cdot \rrbracket$, in this section we connect well-typedness of processes in $\mathsf {S}$ [10] with the satisfiability of local formulas, which model the execution of $\mathsf {A}$ processes.

5.1 Global and Local Types

Rather than defining multiparty session types for $\mathsf {A}$ processes, we would like to model checking local types by re-using existing tools for $\mathsf {A}$: SAPIC [12] and Tamarin [14]. Concretely, next we shall connect typability for $\mathsf {S}$ processes with satifiability for $\mathsf {A}$ processes. To formalize these results, we first recall some essential notions for multiparty session types; the reader is referred to [5, 10] 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 found in [15].

Example 1

Figure 2 gives three global types for the protocol in Sect. 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.

Table 8. Global and local types [10].

Fig. 2.

Global Types for the Trusted Buyer-Seller Protocol (Sect. 2).

Typing judgements for expressions and processes are of the form $\varGamma {} \vdash {e:S}$ or $\varGamma {} \vdash {P\triangleright \!\!\varDelta }$, where $\varGamma \,{::=}\, \emptyset \mathord {\;\mathbf {|}\;}\varGamma , x:S$ and $\varDelta \,{::=}\, \emptyset \mathord {\;\mathbf {|}\;}\varDelta , c:T$. The standard environment $\varGamma$ assigns variables to sorts and service names to closed global types; the session environment $\varDelta$ associates channels to local types. We write $\varGamma , x:S$ only if $x\notin dom(\varGamma )$, where $dom(\varGamma )$ denotes the domain of $\varGamma$. We adopt the same convention for a : G and c : T, and write $\varDelta ,\varDelta '$ only if $dom(\varDelta )\cap dom(\varDelta ') =\emptyset$. Typing rules are as in [5, 10]; as discussed in those works, typability for $\mathsf {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 $\mathsf {A}$

Following the approach in [12], properties of processes in $\mathsf {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 $\mathsf {S}$ processes, using encoding $\llbracket \cdot \rrbracket$.

Definition 1

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

We will denote by $\mathsf{tr}_P$, a trace from a set $\mathtt{traces}({P})$, for some process P. We will write $\mathsf{tr}$ when P is clear from the context. Notice that, $\mathsf{tr}_P=\mathsf{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: ${\mathtt {temp}}$ and ${\mathtt {msg}}$. Each variable of sort $\mathtt {s}$ will be interpreted in the domain $D(\mathtt {s})$; in particular, we will denote by $\mathcal{V}_{{\mathtt {temp}}}$ the set of temporal variables, which is interpreted in the domain $D({\mathtt {temp}})=\mathcal{Q}$; also, $\mathcal{V}_{{\mathtt {msg}}}$ is the set of message variables, which is interpreted in the domain $D({\mathtt {msg}})= \mathcal{M}$. Below, we will adopt a function $\theta : \mathcal{V} \rightarrow \mathcal{M} \cup \mathcal{Q}$ that maps variables to terms respecting the variable’s sorts, that is $\theta (x:\mathtt {s}) \in D(\mathtt {s})$.

Definition 2

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

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:

Given a process P, in the definition below, $\mathsf{tr}$ denotes a trace in $\mathtt{traces}({P})$, $idx(\mathsf{tr})$ denotes the positions in $\mathsf{tr}$, and $\mathsf{tr}_i$ denotes the i-th position in $\mathsf{tr}$.

Definition 3

(Satisfaction relation [12]). The satisfaction relation $(\mathsf{tr}, \theta ) \vDash \varphi$ between a trace $\mathsf{tr}$, a valuation $\theta$, and a trace formula $\varphi$ is defined as follows

Satisfaction of $(\forall x:\mathtt {s})\varphi$, $\varphi \vee \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 $\mathtt {p}$ and $\mathtt {q}$. Given $k:{\mathtt {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 ${\mathtt {msg}}$.

Definition 4

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

where the quantified variables have sorts $i, j, k:{\mathtt {temp}}$ and z : S, and variables i and z are fresh. The extension of $\varPhi _{}( \_)$ to session environments, denoted $\widehat{\varPhi }(\_)$, is as expected: .

Remark 2

Since each local type is associated to a unique local formula, the mapping $\varPhi _{\_}( \_)$ is invertible. That said, from a local formula $\varphi$ we can obtain the corresponding type $\varPhi ^{-1}_{}(\varphi )$. For instance, for the local formula one has $\varPhi ^{-1}_{}(\varphi _\mathtt{out})= s [{\mathtt {p}}]: !\langle \mathtt {q},S\rangle .\varPhi ^{-1}_{s [{\mathtt {p}}]}(\varphi ')$. The other cases are similar.

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

Theorem 4

Let $\varGamma \vdash P\triangleright \varDelta$ be a well-typed $\mathsf {S}$ process. Also, let . Then there exists a $\theta$ such that $(\mathsf{tr}, \theta )\vDash \widehat{\varPhi }(\varDelta )$.

Theorem 5

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

Example 2

The projection of $G_{\text {init}}$ onto participant 3 (Buyer1), under session s is: $s [{3}]: !\langle \mathtt {1},string\rangle .?(\mathtt {1},int). !\langle \mathtt {2},int\rangle . \& (2, \{\mathtt{ok}:(G_{\text{ contract }}|_{3}), \lnot \mathtt{ok}:\mathtt{end}\})$.

The local formula associated is:

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

6 Revisiting the Two-Buyer Contract Signing Protocol

We recall the motivating example introduced in Sect. 2. Using a combination of constructs from $\mathsf {S}$ and $\mathsf {A}$, we first develop a protocol specification which is compiled down to $\mathsf {A}$ using our encoding; the resulting $\mathsf {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 $\mathsf {S}$ only, abstracting away from cryptography, and using existing type systems for $\mathsf {S}$ to enforce protocol correctness. Then, compile this resulting $\mathsf {S}$ specification down to $\mathsf {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:

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:

where processes , , and are given in Tables 11 and 12. Process T illustrates how we may combine constructs from $\mathsf {S}$ (important to represent, e.g., session establishment on b and delegation from S) and features from $\mathsf {A}$ (essential to, e.g., manipulate the memory cell s, which records contract information). Indeed, T uses the $\mathsf {A}$ construct to initialize the cell s and to update it. Therefore, the sound and complete encoding proposed in Sect. 4 allows us to specify processes in $\mathsf {A}$, while retaining the high-level constructs from $\mathsf {S}$.

Table 9. : $B_1$’s contract signing processes.$[m]_X$ denotes

Table 10. : $B_2$’s contract signing processes.

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

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

Table 11. : abort process executed by T

Table 12. e : resolve processes executed by T

Table 13 shows the translation of $B_1$ in $\mathsf {A}$, using our encoding. For simplicity, we omit the details related to the session establishment (using NSL), which follow Table 7. Process specifications for $B_2, S$, and T in $\mathsf {A}$ can be obtained similarly. As mentioned in Sect. 4, the communication is done via updating session queues $s_{ij}$, for $i,j=1,2,3$.

Table 13. Translation of $B_1$ into $\mathsf {A}$.

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 $\mathsf {honest}(\_)$, $\mathsf {sndnonce}(\_ ,\_ , \_)$, $\mathsf {rcvnonce}(\_,\_, \_)$, and $\mathsf {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$:

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.

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_\mathtt{init}$, presented in Fig. 2. The corresponding local formula can be obtained following Definition 4:

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 Fig. 2.

7 Related Works and Concluding Remarks

We have connected two distinct process models: the calculus $\mathsf {S}$ for multiparty session-based communication [10] and the calculus $\mathsf {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 (Definition 4). Results so far are very promising, as discussed in Sect. 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].