The Cpi-calculus: a Model for Confidential Name Passing

TL;DR

The paper introduces the Cpi-calculus, a formal model extending pi-calculus to enforce confidentiality by preventing channels from being forwarded, thus controlling information dissemination in distributed systems.

Contribution

It presents a subcalculus of pi-calculus where channels are confidential and cannot be forwarded, enabling formal reasoning about privacy without extra language constructs.

Findings

Channels cannot be forwarded once received

Encoding of pi-calculus into Cpi-calculus demonstrated

Representation of privacy notions like group creation and name hiding

Abstract

Sharing confidential information in distributed systems is a necessity in many applications, however, it opens the problem of controlling information sharing even among trusted parties. In this paper, we present a formal model in which dissemination of information is disabled at the level of the syntax in a direct way. We introduce a subcalculus of the pi-calculus in which channels are considered as confidential information. The only difference with respect to the pi-calculus is that channels once received cannot be forwarded later on. By means of examples, we give an initial idea of how some privacy notions already studied in the past, such as group creation and name hiding, can be represented without any additional language constructs. We also present an encoding of the (sum-free) pi-calculus in our calculus.

Tables

Table 1. Table 1: Syntax of prefixes and processes.

Table 2. Table 2: LTS rules.

$ (out)          ⁢!kl.⁢!kl→PP (in)               ⁢k?x.⁢k?l→P⁢P{/lx} (match)        π.α→PP′             ⁢[=aa]π.α→PP′ (res)              α→PP′∉k⁢n(α)            α→⁢(⁢νk)P⁢(⁢νk)P′ (open)             ⁢!kl→PQ≠kl            ⁢(⁢νl)!kl→⁢(⁢νl)PQ (par-l)                   α→PQ=∩⁢bn(α)⁢fn(R)∅             α→|PR|QR (comm-l)              ⁢!kl→PP′⁢k?l→QQ′             τ→|PQ|P′Q′ (close-l)                        ⁢(⁢νl)!kl→PP′⁢k?l→QQ′∉l⁢fn(Q)                τ→|PQ⁢(⁢νl)(|P′Q′) (rep-act)       α→PP′           !Pα→P′|!P (rep-comm)               ⁢!kl→PP′⁢k?l→PP′′               !Pτ→(|P′P′′)|!P (rep-close)                        ⁢(⁢νl)!kl→PP′⁢k?l→PP′′∉l⁢fn(P)                 !Pτ→(⁢νl)(|P′P′′)|!P (out)          ⁢!kl.⁢!kl→PP (in)               ⁢k?x.⁢k?l→P⁢P{/lx} (match)        π.α→PP′             ⁢[=aa]π.α→PP′ (res)              α→PP′∉k⁢n(α)            α→⁢(⁢νk)P⁢(⁢νk)P′ (open)             ⁢!kl→PQ≠kl            ⁢(⁢νl)!kl→⁢(⁢νl)PQ (par-l)                   α→PQ=∩⁢bn(α)⁢fn(R)∅             α→|PR|QR (comm-l)              ⁢!kl→PP′⁢k?l→QQ′             τ→|PQ|P′Q′ (close-l)                        ⁢(⁢νl)!kl→PP′⁢k?l→QQ′∉l⁢fn(Q)                τ→|PQ⁢(⁢νl)(|P′Q′) (rep-act)       α→PP′           !Pα→P′|!P (rep-comm)               ⁢!kl→PP′⁢k?l→PP′′               !Pτ→(|P′P′′)|!P (rep-close)                        ⁢(⁢νl)!kl→PP′⁢k?l→PP′′∉l⁢fn(P)                 !Pτ→(⁢νl)(|P′P′′)|!P \begin{array}[t]{@{}c@{}}{\vbox{\hbox{\hbox{\small\small{(out)}}}\hbox{$\displaystyle\vbox{\hbox{\hskip 24.01045pt\vbox{\vbox{}\hbox{\hskip-24.01045pt\hbox{\hbox{$\displaystyle\displaystyle k!l.P\xrightarrow{k!l}P$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{(in)}}}\hbox{$\displaystyle\vbox{\hbox{\hskip 41.39236pt\vbox{\vbox{}\hbox{\hskip-41.39235pt\hbox{\hbox{$\displaystyle\displaystyle k?x.P\xrightarrow{k?l}P\{l/x\}$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{(match)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 19.3499pt\vbox{\hbox{\hskip-19.34988pt\hbox{\hbox{$\displaystyle\displaystyle\pi.P\xrightarrow{\alpha}P^{\prime}$}}}\vbox{}}}\over\hbox{\hskip 34.08018pt\vbox{\vbox{}\hbox{\hskip-34.08017pt\hbox{\hbox{$\displaystyle\displaystyle[a=a]\pi.P\xrightarrow{\alpha}P^{\prime}$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{(res)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 37.04204pt\vbox{\hbox{\hskip-37.04202pt\hbox{\hbox{$\displaystyle\displaystyle P\xrightarrow{\alpha}P^{\prime}\quad k\notin\mathsf{n}(\alpha)$}}}\vbox{}}}\over\hbox{\hskip 32.51602pt\vbox{\vbox{}\hbox{\hskip-32.516pt\hbox{\hbox{$\displaystyle\displaystyle(\nu k)P\xrightarrow{\alpha}(\nu k)P^{\prime}$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{(open)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 35.86423pt\vbox{\hbox{\hskip-35.86423pt\hbox{\hbox{$\displaystyle\displaystyle P\xrightarrow{k!l}Q\quad k\not=l$}}}\vbox{}}}\over\hbox{\hskip 31.9951pt\vbox{\vbox{}\hbox{\hskip-31.99509pt\hbox{\hbox{$\displaystyle\displaystyle(\nu l)P\xrightarrow{(\nu l)k!l}Q$}}}}}}$}}\vspace{2ex}}\\ {\vbox{\hbox{\hbox{\small\small{(par-l)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 56.8394pt\vbox{\hbox{\hskip-56.83939pt\hbox{\hbox{$\displaystyle\displaystyle P\xrightarrow{\alpha}Q\quad\mathsf{bn}(\alpha)\cap\mathsf{fn}(R)=\emptyset$}}}\vbox{}}}\over\hbox{\hskip 34.00351pt\vbox{\vbox{}\hbox{\hskip-34.0035pt\hbox{\hbox{$\displaystyle\displaystyle P\;|\;R\xrightarrow{\alpha}Q\;|\;R$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{(comm-l)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 39.70602pt\vbox{\hbox{\hskip-39.70602pt\hbox{\hbox{$\displaystyle\displaystyle P\xrightarrow{k!l}P^{\prime}\quad Q\xrightarrow{k?l}Q^{\prime}$}}}\vbox{}}}\over\hbox{\hskip 34.7179pt\vbox{\vbox{}\hbox{\hskip-34.7179pt\hbox{\hbox{$\displaystyle\displaystyle P\;|\;Q\xrightarrow{\tau}P^{\prime}\;|\;Q^{\prime}$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{(close-l)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 71.53152pt\vbox{\hbox{\hskip-71.53151pt\hbox{\hbox{$\displaystyle\displaystyle P\xrightarrow{(\nu l)k!l}P^{\prime}\quad Q\xrightarrow{k?l}Q^{\prime}\quad l\notin\mathsf{fn}(Q)$}}}\vbox{}}}\over\hbox{\hskip 46.5559pt\vbox{\vbox{}\hbox{\hskip-46.5559pt\hbox{\hbox{$\displaystyle\displaystyle P\;|\;Q\xrightarrow{\tau}(\nu l)(P^{\prime}\;|\;Q^{\prime})$}}}}}}$}}\vspace{2ex}}\\ {\vbox{\hbox{\hbox{\small\small{(rep-act)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 14.27756pt\vbox{\hbox{\hskip-14.27754pt\hbox{\hbox{$\displaystyle\displaystyle P\xrightarrow{\alpha}P^{\prime}$}}}\vbox{}}}\over\hbox{\hskip 27.34863pt\vbox{\vbox{}\hbox{\hskip-27.34862pt\hbox{\hbox{$\displaystyle\displaystyle!P\xrightarrow{\alpha}P^{\prime}\;|\;!P$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{(rep-comm)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 40.37952pt\vbox{\hbox{\hskip-40.3795pt\hbox{\hbox{$\displaystyle\displaystyle P\xrightarrow{k!l}P^{\prime}\quad P\xrightarrow{k?l}P^{\prime\prime}$}}}\vbox{}}}\over\hbox{\hskip 42.05807pt\vbox{\vbox{}\hbox{\hskip-42.05806pt\hbox{\hbox{$\displaystyle\displaystyle!P\xrightarrow{\tau}(P^{\prime}\;|\;P^{\prime\prime})\;|\;!P$}}}}}}$}}}\qquad{\vbox{\hbox{\hbox{\small\small{(rep-close)}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 72.15675pt\vbox{\hbox{\hskip-72.15674pt\hbox{\hbox{$\displaystyle\displaystyle P\xrightarrow{(\nu l)k!l}P^{\prime}\quad P\xrightarrow{k?l}P^{\prime\prime}\quad l\notin\mathsf{fn}(P)$}}}\vbox{}}}\over\hbox{\hskip 50.00717pt\vbox{\vbox{}\hbox{\hskip-50.00716pt\hbox{\hbox{$\displaystyle\displaystyle!P\xrightarrow{\tau}(\nu l)(P^{\prime}\;|\;P^{\prime\prime})\;|\;!P$}}}}}}$}}}\end{array}$

Table 3. Table 3: Encoding of π 𝜋 \pi -calculus processes into C _ ​ π subscript 𝐶 _ 𝜋 C_{\_}\pi processes.

Equations

$$(\nu session)channel!session.Alice|channel?x.Bob$$

$$\alpha ::=k!l|k?l|(\nu l)k!l|\tau$$

$$P_{\_}1\stackrel{{\alpha }_{\_}1}{\to }{P}_{\_}2\stackrel{{\alpha }_{\_}2}{\to }\dots \stackrel{{\alpha }_{\_}m}{\to }{P}_{\_}m+1.$$

$$\text{mbox}ifP\sim Q\text{mbox}andP\stackrel{\alpha }{\to }{P}^{\prime },\text{mbox}where\mathsf{bn}(\alpha )\cap \mathsf{fn}(Q)=\varnothing ,\text{mbox}thenQ\stackrel{\alpha }{\to }{Q}^{\prime }\text{mbox}and{P}^{\prime }\sim Q^{\prime },$$

$$(\nu k)(((\nu l)k!l.m?y.[y=l]\pi .0)|k?x.P)\sim (\nu k)(((\nu l)k!l.m?y.0)|k?x.P)$$

$$k?x.(\nu l)(l!x.0|l?y.0)$$

$$(\nu session)channel!session.Alice|channel?x.Bob|Carol$$

$$Q=(\nu n)l!n.n?x.[x=l].Q^{\prime },$$

$$k!l.k?y.[y=l]\pi .P_{\_}1|k?x.[x=l]k!l.P_{\_}2$$

$$(\nu k)((\nu l)k!l.0|k?x.P)$$

$$(\nu g_{\_}l)((\nu l)P|Q)$$

$$(\nu n)k!n.n?x.[x=g_{\_}l]n!l$$

$$k?(x_{\_}1,x_{\_}2).x_{\_}2!g.P|k!(l,m_{\_}l).Q|m_{\_}l?y.y!(l,m_{\_}l).0$$

$$k?(x_{\_}1,x_{\_}2).(\nu e)n_{\_}g!e.x_{\_}2!e.P|k!(l,m_{\_}l).Q|m_{\_}l?y.y?z.z!(l,m_{\_}l).0|n_{\_}g?y.y!g.0$$

$$(\nu e)n_{\_}g!e.m_{\_}l!e.P|Q|m_{\_}l?y.y?z.z!(l,m_{\_}l).0|n_{\_}g?y.y!g.0$$

$$(\nu e)(P|Q|e?z.z!(l,m_{\_}l).0|e!g.0)$$

$$\begin{array}[t]{@{}c@{}}\llbracket P_{\_}1\;|\;P_{\_}2\rrbracket=\llbracket P_{\_}1\rrbracket\;|\;\llbracket P_{\_}2\rrbracket\qquad\llbracket!P\rrbracket=!\llbracket P\rrbracket\qquad\llbracket 0\rrbracket=0\end{array}$$

$$H=\prod _{\_}i\in \{1,\dots ,n\}{H}_{\_}{k}_{\_}i,$$

$$(\nu k)(((\nu l)k!l.m?y.[y=l]\pi .0)|k?x.P)\sim (\nu k)(((\nu l)k!l.m?y.0)|k?x.P).$$

$$\begin{array}[t]{@{}rcl@{\;\;}l@{}}{\cal R}&=&\{\big{(}(\nu k)((\nu l)k!l.m?y.[y=l]\pi.0\;|\;k?x.P),(\nu k)((\nu l)k!l.m?y.0\;|\;k?x.P)\big{)},\\ &&\;\;\big{(}(\nu k)(\nu l)(m?y.[y=l]\pi.0\;|\;Q),(\nu k)(\nu l)(m?y.0\;|\;Q)\big{)},\\ &&\;\;\big{(}(\nu l)(m?y.[y=l]\pi.0\;|\;Q),(\nu l)(m?y.0\;|\;Q)\big{)},\\ &&\;\;\big{(}(\nu k)(\nu l)([n=l]\pi.0\;|\;Q),(\nu k)(\nu l)(0\;|\;Q)\big{)},\\ &&\;\;\big{(}(\nu l)([n=l]\pi.0\;|\;Q),(\nu l)(0\;|\;Q)\big{)}\\ &&\;\;\big{(}(\nu k)(\nu l)(\nu n)([n=l]\pi.0\;|\;Q),(\nu k)(\nu l)(\nu n)(0\;|\;Q)\big{)},\\ &&\;\;\big{(}(\nu l)(\nu n)([n=l]\pi.0\;|\;Q),(\nu l)(\nu n)(0\;|\;Q)\big{)}\\ &&\;\;\;|\;\mbox{for all}\;n,m\in{\cal C},\;\mbox{such that}\;n\not=l,\;\hbox{ and all processes}\;P\;\mbox{and}\;Q,\;\hbox{such that}\;l\notin\mathsf{fo}(Q)\,\}\end{array}$$

$$(\nu k)((\nu l)k!l.m?y.[y=l]\pi .0|k?x.P)\stackrel{\alpha }{\to }{P}^{\prime }.$$

$$(\nu k)((\nu l)k!l.m?y.0|k?x.P)\stackrel{\tau }{\to }(\nu k)(\nu l)(m?y.0|P\{l/x\}),$$

$$(\nu k)(\nu l)(m?y.[y=l]\pi .0|Q)\stackrel{\alpha }{\to }{P}^{\prime },$$

$$(\nu k)(\nu l)(m?y.[y=l]\pi .0|Q)\stackrel{m?n}{\to }(\nu k)(\nu l)([n=l]\pi .0|Q),$$

$$(\nu k)(\nu l)(m?y.0|Q)\stackrel{m?n}{\to }(\nu k)(\nu l)(0|Q),$$

$$(\nu k)(\nu l)(m?y.[y=l]\pi .0|Q)\stackrel{\alpha }{\to }(\nu k)(\nu l)(m?y.[y=l]\pi .0|Q^{\prime }),$$

$$(\nu k)(\nu l)(m?y.0|Q)\stackrel{\alpha }{\to }(\nu k)(\nu l)(m?y.0|Q^{\prime }),$$

$$(\nu k)(\nu l)(m?y.[y=l]\pi .0|Q)\stackrel{(\nu k)\alpha }{\to }(\nu l)(m?y.[y=l]\pi .0|Q^{\prime }),$$

$$(\nu k)(\nu l)(m?y.0|Q)\stackrel{(\nu k)\alpha }{\to }(\nu l)(m?y.0|Q^{\prime }),$$

Full text

1 Introduction

Sharing sensitive information over the internet has become an everyday routine: sending personal data and/or credit card number for online shopping is just one of the examples where the sensitive information can be disposed to other parties. Such cases open the problem of controlling information sharing even among trusted parties. The problem of privacy can (and must) be perceived both from a legal and technological point of view. One of the first who explored privacy in the information age, a legal scholar, Alan Westin had recognized that “Building privacy controls into emerging technologies will require strong effort…” [21]. On the other hand, new technologies can also provide new ways to deal with privacy problems [18]. According to Solove [17], there are four types of privacy violation: invasions, information collection, information processing, and information dissemination (see also [11]). The focus of this paper will be on presenting the techniques for controlling information dissemination in distributed systems.

Although there is a further taxonomy for information dissemination violation by Solove, all these sub-types roughly speak about harms of revealing the personal data or threats of spreading information. In distributed systems where communication of entities is central, controlling the flow of confidential information poses some obstacles. The capability of forwarding, that makes it possible to disseminate received information, may be recognized as one problem in controlling such systems.

Even in the examples of well-structured communications between two parties, such as the ones respecting the protocols specified by session types [10], it can be permissible for any party to forward (i.e., delegate) its session end-point. The session delegation is crucial for establishing sessions between the two parties [5, 19], such as in

[TABLE]

where $\mathit{Alice}$ creates a fresh channel $\mathit{session}$ and sends one end-point along $\mathit{channel}$ to $\mathit{Bob}$. However, it is also possible that the receiving party forwards the channel (cf. session delegation), as we may specify $\mathit{Bob}=\mathit{forward}!x.\mathit{Bob}^{\prime}$. Such forwarding capability may be appealing to have in some cases (e.g., forwarding tasks from a master to a slave process), but considering $\mathit{session}$ is a channel created by $\mathit{Alice}$, pointing to some private data and shared exclusively with $\mathit{Bob}$, one might argue that $\mathit{Bob}$ should not gain the capability of session delegation just by receiving $\mathit{session}$. Hence, if we consider the name of channel $\mathit{session}$ to be confidential, $\mathit{Alice}$ should be the one who decides whether to let a third party knows about the channel. In addition, we may argue that in some cases there is no predefined set of parties that may receive $\mathit{session}$ in any future. Indeed, $\mathit{Alice}$ should be able to send $\mathit{session}$ end-point to any other party she decides. Therefore, we may conclude that confidential information can also be shared in open-ended systems, where the set of users of the information cannot be statically predefined.

In this paper, we present a formal model in which dissemination of information is disabled at the level of the syntax in a direct way. We build on the $\pi$-calculus [16], a process model tailored for communication-centric systems, by introducing a subcalculus which we call Confidential $\pi$-calculus, abbreviated $C_{\_}\pi$. The only information shared in our calculus are names of channels, so channels are the confidential information. This is the only difference of our model with respect to the $\pi$-calculus, names of channels are confidential and hence once received cannot be forwarded later on. By means of examples, the paper gives an initial idea of how some privacy notions already studied in the past, such as group creation and name hiding, can be represented without any additional language constructs. We also define the non-forwarding property and show that, naturally, all $C_{\_}\pi$ processes satisfy this property. This result is then reused to differentiate the $\pi$-calculus processes that never forward received channels: if a $\pi$ process is bisimilar to a $C_{\_}\pi$ process then the $\pi$ process satisfies the non-forwarding property. We also propose an encoding from $\pi$-calculus into $C_{\_}\pi$-calculus and show its completeness. The paper presents initial results of the investigation of the model, formalization of some of the results are left for an extended version of the paper.

The paper is organized as follows. In Section 2, we start by presenting the syntax and semantics of $C_{\_}\pi$-calculus, and we state some properties of the labeled transition system. In Section 3 we define a behavioral equivalence relation, called strong bisimilarity. Using the definition of strong bisimilarity we state and prove that the closed domains for channels are directly representable in $C_{\_}\pi$. Another consequence of this result is the possibility of creating channels with similar behavior to $CCS$ channels [13]. Using the strong bisimilarity relation and non-forwarding of $C_{\_}\pi$ processes, we also propose a method for differentiating $\pi$-calculus processes that never forward received channels. In addition Section 4 presents some further informal insights on $C_{\_}\pi$ and several interesting scenarios which are naturally represented in our model. Even though non-forwarding property restricts the syntax of the $\pi$-calculus, in Section 5 we show the $C_{\_}\pi$ is expressive enough to model the $\pi$-calculus. The base idea of the encoding is to create dedicated processes for each channel that handle sending the respective channels. In Section 6 we conclude and point to the related work.

2 Process Model

In this section, we present the syntax and semantics of $C_{\_}\pi$. The main difference with respect to the $\pi$-calculus processes is that in $C_{\_}\pi$ names received in an input cannot be later used as an object of an output, hence disallowing forwarding. Apart from this difference, the remainder of this section should come as no surprise to a reader familiar with the $\pi$-calculus. To make a clear distinction between names of variables bound in input and names of channels, we introduce two disjoint countable sets ${\cal V}$ and ${\cal C}$, where ${\cal V}$ is the set of variables, ranged over by $x,y,z,\ldots$, and ${\cal C}$ is the set of channel names, ranged over by $k,l,m,\ldots$. We denote with ${\cal N}$ the union of sets ${\cal V}$ and ${\cal C}$, and we let $a,b,c,\ldots$ range over ${\cal N}$.

Syntax.

Table 1 presents the syntax of the language. An inactive process is represented with [math]. The prefixed process $\pi.P$ comprehends process $a!k.P$, which on name $a$ sends channel $k$ and then proceeds as $P$, process $a?x.P$ which on name $a$ receives a channel and substitutes the received channel for $x$ in $P$, and the last prefix $[a=b]\pi.P$ which exhibits $\pi.P$ only if $a$ and $b$ are the same name. Notice that in our language, differently from the $\pi$-calculus, there is a syntactic restriction of the objects in prefixes: only a channel ($k$) can be sent and only a variable ($x$) can be used as a placeholder for a channel to be received. For example, $\pi$-calculus process $a?x.b!x.0$ is not part of the $C_{\_}\pi$ syntax. There is no restriction on subjects of prefixes and names to be matched, these can be either variables or channels ($a$). Parallel composition $P\;|\;P$ stands for two processes simultaneously active, that may interact. Channel restriction $(\nu k)P$ expresses that a new channel $k$, known only to process $P$, is created. Replicated process $!P$ introduces an infinite behavior. Intuitively, consider $!P$ stands for an infinite parallel composition of copies of process $P$ (i.e., $P\;|\;P\;|\;\cdots$). Here, we do not consider the choice operator (i.e., the sum) since we believe it is not fundamental to our approach, but we remark choice can be added in expected lines.

In $(\nu k)P$ and $a?x.P$, the channel $k$ and the variable $x$ are binding with scope $P$. The set of bound names $\mathsf{bn}(P)$, for any process $P$, is defined as the union of bound channels and bound variables in $P$. The set of free names $\mathsf{fn}(P)$ and the set of names $\mathsf{n}(P)$, for any $P$, are defined analogously. In addition, we use $\mathsf{fo}(P)$ to denote the set of all free channels appearing as objects of output prefixes in process $P$.

Semantics.

We present an operational semantics for our model in terms of the labeled transition system, which build on observable labeled actions $\alpha$, defined as

[TABLE]

Action $k!l$ sends the channel $l$ on the channel $k$, while $k?l$ receives the channel $l$ on channel $k$. In action $(\nu l)k!l$ the sent channel $l$ is bound, and $\tau$ stands for internal action. Notice that, as in the $\pi$-calculus, names bound in the input (variables) cannot appear in labels of observable actions. To retain the same notation as for processes, we denote by $\mathsf{fn}(\alpha)$, $\mathsf{bn}(\alpha)$ and $\mathsf{n}(\alpha)$, the sets of free, bound and all names of observable $\alpha$, respectively. As we noted above, these sets contain only channels, and not variables.

The transition relation is defined inductively by the rules given in Table 2. Notice that the action labels and transition rules are defined exactly as in the $\pi$-calculus [16]. The symmetric rules for (par-l), (comm-l) and (close-l) are elided from the table. Rules (out), (in) and (match) are consistent with the explanations of the corresponding syntactic constructs. Rule (res) ensures that the action of the process is the action of the process scoped over by channel restriction if the channel specified in restriction is not mentioned in the action. Rule (open) opens the scope of the restricted channel, enabling the extrusion of its scope while ensuring that subject and the object of the action are different channels. Rule (par-l) lifts the action of one of the branches, and the side condition ensures that the channel bound in the action is not specified as free in the other branch. In rule (comm-l) two processes performing dual actions, one sending and other receiving $l$ along $k$, synchronize their actions in the respective parallel composition. In rule (close-l) the channel sent ($l$) by the left process is bound and after the synchronization with the right process (performing the dual action), the scope of $l$ is closed while avoiding unintended name capture. Rules (rep-act), (rep-comm) and (rep-close) describe the actions of a replicated process. The first rule lifts the action of a single copy of the replicated process and activates $!P$ in parallel. The second and the third rules show cases when two copies of replicated process synchronize their actions, either through communicating a free or bound channel, where, again, in both cases a copy of $!P$ is activated in parallel. As usual, we identify $\alpha$-convertible processes, and thus, we use our transition rules up to $\alpha$-conversion when needed.

We now present some specific results of the transition relation in the $C_{\_}\pi$-calculus. Our first result shows the relation between the set of free channels appearing as objects of output prefixes in the process and the process redexes: this set can be (possibly) enlarged only by opening the scope of a bound channel. Even more, the input actions do not affect the set of free channels appearing as objects of output prefixes in the process.

Lemma 1

Let $P\xrightarrow{\alpha}P^{\prime}$.

If $\alpha=k?l$ then $\mathsf{fo}(P^{\prime})=\mathsf{fo}(P)$. 2. 2.

If $\alpha=k!l$ then $l\in\mathsf{fo}(P)$ and $\mathsf{fo}(P^{\prime})\subseteq\mathsf{fo}(P)$. 3. 3.

If $\alpha=(\nu l)k!l$ then $l\in\mathsf{bn}(P)$ and $\mathsf{fo}(P^{\prime})\subseteq\mathsf{fo}(P)\cup\{l\}$. 4. 4.

If $\alpha=\tau$ then $\mathsf{fo}(P^{\prime})\subseteq\mathsf{fo}(P)$.

Proof 2.1**.**

The proof is by induction on the derivation $P\xrightarrow{\alpha}P^{\prime}$. We only discuss the base case of $3.$, when rule (open) is applied. Then, $P=(\nu l)P_{\_}1$ and $(\nu l)P_{\_}1\xrightarrow{(\nu l)k!l}P^{\prime}$ is derived from $P_{\_}1\xrightarrow{k!l}P^{\prime}$. By $2.$ of this Lemma, we get $l\in\mathsf{fo}(P_{\_}1)$ and $\mathsf{fo}(P^{\prime})\subseteq\mathsf{fo}(P_{\_}1)$. Since $l\in\mathsf{bn}((\nu l)P_{\_}1)$, we conclude $\mathsf{fo}(P^{\prime})\subseteq\mathsf{fo}((\nu l)P_{\_}1)\cup\{l\}$.

As a direct consequence of Lemma 1 we get the next corollary.

Corollary 2.2**.**

If $P\xrightarrow{k?l}P^{\prime}$ and $l\notin\mathsf{fo}(P)$ then $l\notin\mathsf{fo}(P^{\prime})$. 2. 2.

If $l\notin\mathsf{fo}(P)$ then there is no process $P^{\prime}$ and channel $k$ such that $P\xrightarrow{k!l}P^{\prime}$.

What we can conclude from Corollary 2.2 combining its two statements is that a $C_{\_}\pi$ process cannot send a channel that it previously has received if the channel was not specified as an object of an output prefix in the first place. To show that this property is preserved also by all possible redexes of the process let us first relate the set of free channels appearing in output prefixes of the set and any its execution trace. The result is a direct consequence of Lemma 1.

Corollary 2.3**.**

If $P\xrightarrow{\alpha_{\_}1}P_{\_}1\xrightarrow{\alpha_{\_}2}\ldots\xrightarrow{\alpha_{\_}m}P_{\_}m$ then $\mathsf{fo}(P_{\_}m)\subseteq\mathsf{fo}(P)\cup\mathsf{bn}(\alpha_{\_}1)\cup\ldots\cup\mathsf{bn}(\alpha_{\_}m)$.

The next theorem states that if the channel received by a process was not previously specified as an object of an output prefix, it will not be sent in any of the process possible evolutions. Hence, for the $C_{\_}\pi$ processes forwarding a channel, in a sense that a process can send a channel he learns through receiving, is not possible. Before the theorem, we present the precise definition of non-forwarding.

Definition 2.4** (Non-forwarding Property).**

A process $P_{\_}1$ satisfies the non-forwarding property if whenever

[TABLE]

then if $l\notin\mathsf{fn}(P_{\_}i)$ and $\alpha_{\_}i=k?l$, for some $i=1,\ldots,m-1$, then $\alpha_{\_}j\not=k^{\prime}!l$, for all $j=i+1,\ldots,m$.

Notice that in the last definition we could also add the condition $\alpha_{\_}i\not=(\nu l)k^{\prime}!l$, for all $j=i+1,\ldots,m$. But, since without loss of generality we can assume all bound outputs are fresh, we can omit such condition. The next theorem attests that all $C_{\_}\pi$ processes respect the non-forwarding property, but in a more rigorous way, where the only restriction for the channel is not to be specified as the free object of any output prefix.

Theorem 2.5** (The $C_{\_}\pi$ Processes Respect the Non-Forwarding Property).**

Let

[TABLE]

Then, if $l\notin\mathsf{fo}(P_{\_}i)$ and $\alpha_{\_}i=k?l$, for some $i=1,\ldots,m-1$, then $\alpha_{\_}j\not=k^{\prime}!l$, for all $j=i+1,\ldots,m$.

Proof 2.6**.**

*Since without loss of generality we can assume all bound outputs are fresh and $l\notin\mathsf{fo}(P_{\_}i)$, using Corollary 2.3 we get $l\notin\mathsf{fo}(P_{\_}j)$, for $j=i+1,\ldots,m+1$. Hence, by Corollary 2.2 $2.$ we get $\alpha_{\_}j\not=k^{\prime}!l$, for $j=i+1,\ldots,m$. *

The result of Theorem 2.5 should come as no surprise, $C_{\_}\pi$ processes are designed to respect the non-forwarding property. However, considering the $\pi$-calculus, it appears to be nontrivial to differentiate processes that respect the non-forwarding property. To attack this goal, we will see in the next section that Theorem 2.5 can be reused in Proposition 3.10.

3 Behavioral equivalence

Based on the notion of observable actions, introduced in Section 2, we investigate some specific behavioral identities of our model. To this end, we introduce a behavioral equivalence, called strong bisimulation, which, colloquially speaking, relates two processes if one can play a symmetric game over them: each action of one process can be mimicked by the other (and with the order reversed), leading to two processes that are again related. The relation that we are interested in is the largest such relation, called strong bisimilarity.

Definition 3.7** (Strong bisimilarity).**

The largest symmetric binary relation over processes $\sim$, satisfying

[TABLE]

for some process $Q^{\prime}$, is called strong bisimilarity.

Notice that, since our transition rules match those of the $\pi$-calculus, our strong bisimilarity relation is precisely one of the $\pi$-calculus [16], restricted to the $C_{\_}\pi$ processes. One consequence of the non-forwarding property of our calculus is the possibility of the creation of closed domains for channels. A property, resembling the creation of a secure channel, which scope is statically determined, can be formally stated using the definition of strong bisimilarity.

Proposition 3.8** (Closed Domains for Channels).**

For any process $P$, channel $m$ and prefix $\pi$, the following equality holds

[TABLE]

Proof 3.9**.**

The proof follows by coinduction on the definition of the strong bisimulation (see Appendix A).

In both processes in Proposition 3.8 the left thread creates a new channel $l$ and sends it over a (private) channel $k$ to the right thread. The equality states that then the channel $l$ cannot be received afterward in the left thread. This is due to the fact that the right thread cannot forward received channels. We may notice that both processes in the proposition define the final scope for channel $l$, hence, determining a closed domain for the channel. The interpretation of this proposition can be twofold. On one hand, the right thread after receiving a fresh channel ($l$) cannot send the received channel, since it respects the non-forwarding property. On the other hand, the left thread sends the channel $l$ (to the right thread) only once and the channel afterward behaves “statically”, since then it cannot be exchanged even between any two sub-processes of process $P\{l/x\}$. Further explanations are given in the next section.

The $\pi$-calculus processes that do not forward names.

The $C_{\_}\pi$ processes satisfy our non-forwarding property (Definition 2.4): if the received channel is new to the process it will not be sent later on. Generally, the $\pi$-calculus processes do not meet the non-forwarding property. However, we may notice that there are some $\pi$-calculus processes which are not part of the $C_{\_}\pi$ syntax but still respect this property. For example, consider the $\pi$-calculus process

[TABLE]

where any received channel along $k$ is then sent on $l$, but since $l$ is restricted, the process will not output the received channel. But the condition that the channel along which the forwarding is performed (here $l$) is restricted is not enough. For example, the $\pi$-calculus process $k?x.(\nu l)(k!l.l!x.0\;|\;l?y.0)$ does not satisfy the non-forwarding property.

This hints that differentiating $\pi$-calculus processes that do not forward received channels, in any of their possible evolutions, may not be a simple task. As one solution to the problem we propose the next result which states that a $\pi$-calculus process $P$, and any of its possible evolutions, do not forward received channels if one can find a $C_{\_}\pi$ process $Q$, such that $P$ and $Q$ are bisimilar. In the theorem, we refer to the non-forwarding property of Definition 2.4, extended to consider all $\pi$-calculus processes. Naturally, the result of the next theorem refers to sum-free $\pi$-calculus processes, since in this paper we are not considering the sum operator in the $C_{\_}\pi$.

Proposition 3.10** (The $\pi$-calculus Processes That do not Forward Names).**

Let $P$ be a $\pi$-calculus process. If there is a $C_{\_}\pi$ process $Q$, such that $P\sim Q$, then $P$ satisfies the non-forwarding property.

Proof 3.11**.**

The proof is derived to Appendix A.

Although the result of Proposition 3.10 is only of the existential nature, we believe it is a step towards more practical results. One such result might be proving that for a given $\pi$-calculus process $P$ one can derive a $C_{\_}\pi$ process $Q$ such that if $P\sim Q$ then $P$ respect the non-forwarding property. There we can also use a relaxed definition of the non-forwarding property, in which processes do not forward names received along some predefined set of channels. We leave such investigations for future work.

4 Examples

In this section, we further investigate some interesting scenarios representable in $C_{\_}\pi$. Since a process in our calculus can learn new names but cannot gain the capability to send such names, we may distinguish two levels of channel ownership of a process that are invariant to the process evolution:

administrator: the process that creates the channel, it has all capabilities over the channel;

• -

user: the process that learns the channel name through communication (scope extrusion) and can communicate along the channel but cannot send it.

Hence, all administrators are also users but the conversely is not true. Also, notice that any process that receives a channel can become a user for that channel (but not administrator), and, hence, all processes may be considered as potential users for any channel. If we consider modelling our opening example in $C_{\_}\pi$ calculus

[TABLE]

$\mathit{Alice}$ is the administrator for $\mathit{session}$ and $\mathit{Bob}$ becomes a user after the reception. In $C_{\_}\pi$ it is not possible for $\mathit{Bob}$ afterward to send $\mathit{session}$ to a third party (e.g., to $\mathit{Carol}$). If $\mathit{Bob}$ wants $\mathit{Carol}$ to get the access to channel $\mathit{session}$ he can only tell $\mathit{Alice}$ and let her decide whether she wants to send $\mathit{session}$ to $\mathit{Carol}$ or not. Therefore, we can have

• •

$\mathit{Bob}=\mathit{channel}!\mathit{carol}.0$, where $\mathit{Bob}$ sends to $\mathit{Alice}$ channel $\mathit{carol}$, and then terminates;

• •

$\mathit{Alice}=\mathit{channel}?y.y!\mathit{session}.\mathit{Alice^{\prime}}$, where $\mathit{Alice}$ receives the channel from $\mathit{Bob}$ and decides to send $\mathit{session}$ along the received channel, and

• •

$\mathit{Carol}=\mathit{carol}?x.\mathit{Carol^{\prime}}$, where $\mathit{Carol}$ can finally receive $\mathit{session}$ along channel $\mathit{carol}$.

We remark this simple example relies on the purely concurrent setting, here $\mathit{session}$ can be held by three or more parties at the same time. The correlation of the $C_{\_}\pi$ and the linearity of session types would need further investigation.

4.1 Authentication

In the $C_{\_}\pi$-calculus specifying $(\nu l)P$ means $P$ is the administrator for channel $l$. Process $P$ can extrude the scope of $l$ by sending, but none of the receiving processes will ever become administrators for the received channel $l$, since they will never gain the capability for sending $l$. Since sending capability cannot be transferred to other processes, we may conclude the administrator property over some channel can be used as an authentication over processes. For example, a process $Q$ that previously has received $l$ may check at any point if the other party with whom he is communicating at the moment over $l$ is actually an administrator or only a user for channel $l$. This can be done by specifying

[TABLE]

where first the private session with other party listening on $l$ is established by sending a fresh channel $n$, and then along $n$ a channel is expected to be received. If the channel received is $l$, then the other party has proved to be an administrator for $l$. Notice that $Q$ itself does not have to be an administrator for $l$ in this example.

As another example, consider that the above process $P$ has two threads running in parallel

[TABLE]

where, before activating $\pi.P_{\_}1$ and $P_{\_}2$ and their possible interactions, both threads test whether the other one is an administrator for channel $l$. Namely, after the first synchronization, the left thread matches the received channel with $l$, i.e., we obtain configuration $k?y.[y=l]\pi.P_{\_}1\;|\;[l=l]k!l.P_{\_}2\{l/x\}$. If the channel received is $l$, then the right thread concludes that the left thread is an administrator for $l$ and sends the same channel back. Then, the left thread also matches the received channel with $l$ and continues only if the two names match, leading to $[l=l]\pi.P_{\_}1\{l/y\}\;|\;P_{\_}2\{l/x\}$. After that, both threads have proved to be administrators for $l$, meaning that both have proved that they originate from process $P$.

4.2 Modelling groups and name hiding

Controlling name sharing in the $\pi$-calculus has been investigated in past and several process models are proposed to this end. In [2], on the $\pi$-calculus syntax, an additional construct is introduced, called group creation, and a typing discipline is developed. The intention of the group construct is to restrict communications: channels specified to be in a group cannot be communicated outside the scope of the corresponding group construct. Hence, the group creation closes the domain for channels specified in the construct. In [6], on the $\pi$-calculus syntax, an additional construct hide is introduced. Construct hide has similar properties to channel restriction, but it is more static since it forbids the channel extrusion for the channel specified to be hidden. Again, roughly speaking, hide construct closes the domain for a channel specified in the construct. In what follows, we try to represent similar behaviors without any additional language constructs, but directly in the $C_{\_}\pi$ calculus (and hence, directly in the $\pi$-calculus). Formalization of the relationship between the mentioned models and the $C_{\_}\pi$ is left for future work.

As one way to represent closed domain for a channel $l$ in the $C_{\_}\pi$ we may consider process

[TABLE]

resembling the one from Proposition 3.8, where the left thread creates the channel $l$, sends it to the right thread and then terminates. The right thread receives the channel, after which the two actions synchronize and the starting process silently evolves to $(\nu k)(\nu l)(0\;|\;P\{l/x\})$. As we have shown in Proposition 3.8, process (and any its subprocess) $P\{l/x\}$ cannot perform output with object $l$ since channel $l$ was not originally created by process $P$. For this property we can state that name $l$ will never leak out of the scope of $P$, hence that all communications along channel $l$ are private to process $P$. Also, we may observe that channel $l$ in process $(\nu k)(\nu l)(0\;|\;P\{l/x\})$ has a static behavior, similar to $CCS$ channels [13].

This constellation indeed resembles the group creation of the $\pi$-calculus with groups and name hiding. The similarity is that in the $\pi$-calculus with groups, a channel declared as a member of a group cannot be acquired as a result of communication by the process outside the scope of the group. The major difference is that in our example the channel behaves as a $CCS$-like channel, i.e., the channel cannot be acquired as a result of communication by any process. This brings us to our next example, that combines channel declaration and authentication, presented in Section 4.1. Consider that for a given channel, we want to statically determine a boundary for the possible channel extrusion, the part of the process we shall call a group. In that case, we may conclude that only members of the group should be able to receive the given channel. As a concrete example consider process

[TABLE]

where by $g_{\_}l$ we denote that the scope of channel $g_{\_}l$ determines the group for channel $l$. Now, to make sure that channel $l$, whose administrator is process $P$, is sent only to processes scoped over with $g_{\_}l$, before each sending of channel $l$, we must make sure that the receiver is an administrator for channel $g_{\_}l$. Hence, instead of construct $k!l$ in $P$, we would use

[TABLE]

where first a private session with the process willing to receive $l$ is established through channel $n$, and then the channel received on $n$ is matched with $g_{\_}l$. Only if the name received on $n$ is $g_{\_}l$, i.e., after the other process has proved that he is a member of the group, channel $l$ is sent. Notice that if the other process can send $g_{\_}l$ this means the process originates either from $P$ or from $Q$.

4.3 Open-ended groups

Groups described in the previous example provide an interesting framework to investigate sharing protected resources in distributed environments but has the limitation that a group, once created, always has a fixed scope, which sometimes might be considered too restrictive. In $C_{\_}\pi$ open-ended groups are directly modeled, since sending a resource in $C_{\_}\pi$ does not transmit the capability for its further dissemination. For example, in $(\nu\mathit{group})k!\mathit{group}.P$ the administrator of $\mathit{group}$, that is the process that creates the group, can send the name of the group to other processes, while the receiving process only becomes a user of the group and does not gain the capability to invite new members to the group.

5 Encoding Uncontrolled Name Passing

In this section, we show how to model forwarding in $C_{\_}\pi$, as in the standard $\pi$-calculus. We start by presenting the basic idea, which we later formalize by means of an encoding.

Throughout this section, we use the polyadic version of our calculus. This enables us to formalize our ideas in a more crisp way, but, as in the $\pi$-calculus, each polyadic communication can be represented by a sequence of monadic ones. Furthermore, we will use poliadicity in a controlled way, so that we do not introduce a non-well sorted communications [14].

In the $\pi$-calculus, there is no syntactic restriction on names that can appear as objects of output prefixes, hence a process like $k?x.g!x.P\;|\;k!l.Q$ may be specified. One way to represent this process in $C_{\_}\pi$ is to:

• •

create a special process dedicated for (repeatedly) sending channel $l$, called handler of the channel,

• •

while sending channel $l$ also send a channel dedicated for communicating with the handler, and

• •

bypass sending of the received channel to the handler process.

Hence, we may try to represent the $\pi$-calculus process introduced above as

[TABLE]

where the process in the middle now sends $l$ together with channel $m_{\_}l$ dedicated for communicating with the handler process (the rightmost one), and the leftmost process receives both channels and instead of sending $l$ along $g$ it sends $g$ to the handler along $m_{\_}l$. The handler process receives $g$ and sends $l$ (again, together with $m_{\_}l$) along the received channel, in such way mimicking forwarding. Such representation does not work in the case when the leftmost process is not an administrator for channel $g$ (e.g., assume process $k?x.g!x.P$ is derived from $k?y.k?x.y!x.P$), since then the process cannot send $g$ to the handler process. To this end, we must refine our representation of forwarding to support situations when processes are potentially not administrators for any given channel. Thus, we introduce another type of handler processes which are in charge of forwarding channels that are subjects of output actions. For example, the starting $\pi$-calculus process would be represented as

[TABLE]

where we added the rightmost thread, which is the handler process of channel $g$, used to bypass sending of channel $g$ in the leftmost thread. Now the communication in this process goes as follows: first, the two leftmost threads synchronize on channel $k$ (as in previous examples), leading to

[TABLE]

where the name $x_{\_}2$ is instantiated with handler name $m_{\_}{l}$ (eliding from the substitution in process $P$). Then, instead of sending $l$ on $g$, the new channel $e$ is created and sent to the handlers of $l$ and $g$

[TABLE]

enabling handler of channel $g$ to send $g$ to the handler of channel $l$, leading to $(\nu e)(P\;|\;Q\;|\;g!(l,m_{\_}{l}).0\;|\;0)$ where sending $l$ (together with the handling name $m_{\_}{l}$) along channel $g$ is finally activated.

Notice that we need a few generalizations of this approach:

• •

each name can be sent infinitely many times, hence, each handling process must be repeatedly available for communication;

• •

each channel can be used either as a subject or as an object of output action, and, hence, for each channel we need both types of handler processes (one as for $l$ and the other as for $g$ in the last example). For the rest of this section we will call the handler of a channel a process that comprehends both types of handlers mentioned above for that channel;

• •

in the source language, processes synchronize their dual (i.e., input/output) actions directly, while in the target language output process first synchronize with the handler process, and only after that handler process synchronize with the input process. In the example above, process $P$ may proceed even though the channel $l$ has not been received by any process. Hence, we need a mechanism to allow processes in the target language to synchronize their actions directly.

We formalize these ideas by introducing an encoding as a pair $(\llbracket\cdot\rrbracket,\varphi_{\_}{\llbracket\;\rrbracket})$, where $\llbracket\cdot\rrbracket$ is a translation function and $\varphi_{\_}{\llbracket\;\rrbracket}$ is a renaming policy [7]. The translation maps each $\pi$-calculus (source) term $P$ into the $C_{\_}\pi$ (target) term $\llbracket P\rrbracket$, and while doing so it uses the renaming policy, that maps each name of the source term $a$ into a tuple of names $(a,n_{\_}a,m_{\_}a)$, where $n_{\_}a$ and $m_{\_}a$ are not names of any source term, and for each name $a$ different names $n_{\_}a$ and $m_{\_}a$ are used. Also, the translation uses some additional names, which we assume to be from a reserved set of names, disjoint from all names of the source language and all names introduced by the renaming policy. All these definitions follow the idea of [7].

The translation function is defined in Table 3. The first rule in the table translates a process scoped with the channel restriction. The source process is encoded as scoped with the original channel name $k$ and the two names associated to $k$ by the renaming policy, i.e. $n_{\_}k$ and $m_{\_}k$, and it introduces the handler process for the channel in parallel with $\llbracket P\rrbracket$. We use $(\nu k,n,m)$ to abbreviate $(\nu k)(\nu n)(\nu m)$. The handler process has two threads in parallel. The left thread is repeatedly available to be invoked on $n_{\_}k$ (see the rule of output) and it sends channel $k$ along the received channel. The use of this process will be only to send $k$ to the right thread of any other handler process (as $n_{\_}g$ in the example above). The right thread of the handler is repeatedly available to be invoked on $m_{\_}k$ and it receives a pair of names (see the rule for output). Along the left received name ($x_{\_}1$) it receives a channel (from the left thread of some handler process) and outputs the channel $k$ together with “addresses” of the handler, $n_{\_}k$ and $m_{\_}k$, and, in addition, a new channel $t$. By sending $n_{\_}k$ and $m_{\_}k$, we make possible for the process that receives (see the rule for input) to be able afterward to directly invoke the handler for $k$. By sending a new channel $t$ to the receiving process and also (in the continuation of the right thread of the handler) to the sending process we establish a private connection between the two processes, which then can directly synchronize and activate their continuations at the same time.

The encoding of the output process creates two fresh channels $e_{\_}1$ and $e_{\_}2$, and sends one end of $e_{\_}1$ to the left thread handler process of name $a$ (the subject of the output) and the other end of $e_{\_}1$, together with and $e_{\_}2$, to the right thread of the handler process for name $b$ (the object of the output). In the continuation, before activating the image of $P$, along $e_{\_}2$ a channel is received and used for the output (to synchronize directly with the input process). We remark that in this rule names $e_{\_}1,e_{\_}2$ and $y$ are taken to be from the reserved set of names, and hence cannot appear as free in $\llbracket P\rrbracket$. The same assumption is made for names $x^{\prime}$ and $y$ in the rule for input, hence there also $x^{\prime}$ and $y$ are not free in $\llbracket P\rrbracket$. In the rule for input four channels are received, the channel together with addresses of his handler and a fresh channel (see the right thread of a handler process). The received fresh channel is only used, as we noted, to synchronize with the sending process (same as the channel received in this synchronization). The rest of the rules shows that the encoding is homomorphism elsewhere.

Notice the encoding does not interfere with our notion of ownership described in Section 4. The role of channel administrator is still present, i.e., handlers are included in that domain. Hence, controlling such domain can still be done, in contrast to the regular $\pi$-calculus processes where one cannot statically identify a domain where the sending the channel capability is confined to.

We may also notice that in the rule for output (Table 3) the two channels (the addresses) of the two handler processes are used, one for the object and the other for the subject of the prefix. This reflects the fact that in order to be capable to mimic all the actions of the source term, we need to introduce handler processes for all free names of the input and output prefixes of the source term. Since the handler processes are introduced directly in the rule for restricted channels (Table 3), we give our main result for the correctness of the encoding only for the $\pi$-calculus processes that contain only bound names. A $\pi$-calculus process that has no free names is called closed.

As closed $\pi$-calculus processes can only exhibit $\tau$ transitions, and those match the reduction semantic [16], for the simplicity we chose to deal with the reduction semantics of the $\pi$-calculus. Therefore, our operational correspondence result relates the set of closed $\pi$-calculus processes, with the reduction semantics (using the reduction relation $\rightarrow$, as defined in [16]), and $C_{\_}\pi$-processes with the labeled transition system. Notice that the reduction relation of the $\pi$-calculus relies on the structural congruence relation [16], which, by rule $[a=a]\pi.P\equiv\pi.P$, may introduce free names. These newly introduced names are not of our interest, as they do not require handlers. To this end, for a $\pi$-calculus process $P$ we define $\mathsf{fnn}(P)$, a subset of $\mathsf{fn}(P)$ that is invariant with respect to the structural congruence relation. Hence, we define $\mathsf{fnn}([a=a]\pi.P)=\mathsf{fnn}(\pi.P)$, and otherwise $\mathsf{fnn}(P)$ coincides with $\mathsf{fn}(P)$. Notice that this means $\mathsf{fnn}([a=b]\pi.P)=\{a,b\}\cup\mathsf{fnn}(\pi.P)$, if $a\not=b$.

We use $\xrightarrow{\tau}\negthickspace{}^{*}$ to denote the transitive closure of $\xrightarrow{\tau}$. We are now ready to present our result, showing that if the source term $P$ reduces to $Q$ then the encoding of $P$ reduces in a number of $\tau$ steps to the process bisimilar to the encoding of the process $Q$. Again, we assume that the $\pi$-calculus processes are sum-free. First, we present an auxiliary result.

Lemma 5.12**.**

If $P\rightarrow Q$ then $\llbracket P\rrbracket\;|\;\mathit{H}\xrightarrow{\tau}\negthickspace{}^{*}\sim\llbracket Q\rrbracket\;|\;\mathit{H},$ where

• •

if $\mathsf{fnn}(P)=\{k_{\_}1,\ldots,k_{\_}n\}$ then

[TABLE]

• •

if $\mathsf{fnn}(P)=\emptyset$ then $\mathit{H}=0$.

Proof 5.13**.**

The proof is derived to Appendix B.

The above result can already be seen as a form of non-standard completeness as it uses the top-level handlers. This hints that the completeness result can also be stated for $\pi$-calculus processes that are not closed, with the encoding that is not compositional, but weakly compositional, such as the encoding from the join-calculus into the $\pi$-calculus [4]. We leave such investigations for future work.

Our main result, given in the next theorem, is a direct consequence of Lemma 5.12.

Theorem 5.14** (Operational Correspondence: Completeness).**

Let $P$ be a closed (sum-free) $\pi$-calculus process. If $P\rightarrow Q$ then $\llbracket P\rrbracket\xrightarrow{\tau}\negthickspace{}^{*}\sim\llbracket Q\rrbracket$.

We also believe that our encoding satisfies the soundness property [7]. This claim relies on the fact that the encoding manipulates the source names in a controlled way. Each name of a source term is translated into a triple of names, and a renaming policy ensures that for different source names different triples of names are used. Other names introduced by the encoding are bound. Using this fact and the fact that each source prefix is translated into a sequence of prefixes of always the same length, we may notice that different post-processing steps might get interleaved, but post-processing steps of different reduction steps in a source term cannot interfere with each other. We also leave formalization of this claim for future work.

6 Conclusions and related work

The notion of secrecy has been studied intensively in process calculi in the past and the variety of techniques have been proposed. The most related to our work are process models building on the $\pi$-calculus, such as [2, 6, 3, 11, 8, 20].

Cardelli et al. [2] introduce a language construct for group creation and a typing discipline, where a group is a type for a channel. The group creation construct blocks communications of channels that are declared as members of the group outside the initial scope of the group, hence preventing the leakage of protected channels. Kouzapas and Philippou [11] extend the model of $\pi$-calculus with groups by constructs that allow reasoning about the private data in information systems. The work of Giunti et. al. [6] introduces an operator called hide which binds a name and has a similar behavior as a name restriction, but in contrast to name restriction it blocks a name extrusion, for which the scope of the hide operator forms a kind of a group that the “hidden” name cannot exit. The paper by Vivas and Yoshida [20] introduces an operator called filter that is statically associated to a process and blocks all actions of the process along names that are not contained in the (polarized) filter. We also mention [8, 3] where the types associate the security levels to channels, where, in the latter work downgrading the security level of a channel is admissible and it is achieved by introducing special, so-called, declassified input and output prefix constructs. All the above approaches share the property that, when building on the $\pi$-calculus model, additional language construct and/or a typing discipline is introduced in order to represent some specific aspect of secrecy in a dedicated way. We believe that $C_{\_}\pi$-calculus appears to be more suitable as an underlying model when studying secrecy, and as such that many aspects of secrecy can be represented in a more canonical way. As a first step, we plan to make a precise representation of group creation [2] in the $C_{\_}\pi$-calculus, following the intuition provided in Section 4.2.

Several fragments of the $\pi$-calculus have been used in different ways and for different purposes. The asynchronous $\pi$-calculus [9], proposed by Honda and Takoro, constrains the syntax by allowing only an inactive process to be the continuation of the output prefix, in this way modelling asynchronous communications. The Localised $\pi$-calculus [12], proposed by Merro and Sangiorgi, disallows the input capability for the received names and does not consider the matching operator. There, the syntactic restriction is that input placeholder cannot appear as a subject of an input, but, in contrast to our work, the forwarding of names is allowed. The Private $\pi$-calculus [15], proposed by Sangiorgi, makes the restriction that objects of output prefixes are always considered as bound, making the symmetry with the input prefixes. Although in Private $\pi$-calculus the forwarding of names is not possible, it differs significantly from our work in the restriction that one name can be sent only once. All these calculi share our goal to investigate specific notions in a dedicated way, without requiring the introduction of specialized primitives, instead by considering a suitable fragment of the $\pi$-calculus.

In this paper, we have presented Confidential $\pi$-calculus, a fragment of the $\pi$-calculus [16] in which the forwarding of received names is disabled at the syntax level. To the best of our knowledge, this is the first process model based on the $\pi$-calculus that represents the controlled name passing by constraining and not extending the original syntax. Some specific properties of our labeled transition system are given and the non-forwarding property is defined. All $C_{\_}\pi$ processes satisfy this property and the method to differentiate the $\pi$-calculus process that never forward received names is proposed, relying on the strong bisimilarity relation of $C_{\_}\pi$ processes and $\pi$ processes. The strong bisimilarity relation is also used to show that the creation of closed domains for channels is directly representable in the $C_{\_}\pi$. Examples presented in the paper already give some intuition on scenarios directly representable in $C_{\_}\pi$, such as authentication and group modelling, and a complete formalization of these ideas is left for future work. The encoding presented here shows that our model is as expressive as the $\pi$-calculus, and the formal verification of the correctness of the encoding is given in the form of the completeness of operational correspondence. The soundness of the encoding is left for future work.

Acknowledgments. The author would like to thank Hugo Torres Vieira and Jovanka Pantović for supervising the work presented here and a great help, to Daniel Hirschkoff for valuable email discussions, and to anonymous reviewers for useful remarks and suggestions. This work has been partially supported by the Ministry of Education and Science of the Republic of Serbia, project ON174026.

Appendix A Proofs from Section 3

Proposition 1**.**

3.8* For any process $P$, channel $m$ and prefix $\pi$, next equality holds*

[TABLE]

Proof A.15**.**

The proof follows by coinduction, by showing that the relation

[TABLE]

where $n\not=l$, is contained in the strong bisimilarity, i.e., ${\cal R}\subseteq\sim$.

We show that each action of one process can be mimicked by the other process in the pair in $\cal R$, leading to processes that are again in relation $\cal R$. Let the process in the first pair

[TABLE]

Then, since actions of the starting process can only be actions of its two branches, we conclude that either $\alpha=(\nu l)k!l$ or $\alpha=k?n$ or it is the synchronization of these two actions, in which case $\alpha=\tau$. We reject the first two options, since the subject of the action is bound in the starting process and by rule (res) it cannot be observed outside of the process. Hence, we conclude $\alpha=\tau$ and $P^{\prime}=(\nu k)(\nu l)(m?y.[y=l]\pi.0\;|\;P\{l/x\})$. Then, by applying (out), (open), (in), (close-l) and (res), respectively, we get

[TABLE]

and since $l\notin\mathsf{fn}(P)$ and $x$ cannot appear as an object in the prefixes in $P$ we conclude $l\notin\mathsf{fo}(P\{l/x\})$. Hence, we have \big{(}(\nu k)(\nu l)(m?y.[y=l]\pi.0\;|\;P\{l/x\}),(\nu k)(\nu l)(m?y.0\;|\;P\{l/x\})\big{)}\in{\cal R}. The symmetric case is analogous.

Now let us consider processes in the second pair of $\cal R$. If

[TABLE]

then observable $\alpha$ can originate from both of the branches or from their synchronization.

—Left branch:*  If the observable originate from the left branch, then $\alpha=m?n$, and by (in), (par-l) and (res) we get*

[TABLE]

where, by the side condition of (res) we conclude $n\notin\{k,l\}$. In the same way we get

[TABLE]

and \big{(}(\nu k)(\nu l)([n=l]\pi.0\;|\;Q),(\nu k)(\nu l)(0\;|\;Q)\big{)}\in{\cal R} holds.

—Right branch:*  If the action originates from the right branch, i.e., from $Q\xrightarrow{\alpha}Q^{\prime}$, we distinguish two cases:*

• (i)

if by rules (par-r) and (res) is derived

[TABLE]

where we conclude that $k,l\notin\mathsf{n}(\alpha)$, hence $l\notin\mathsf{fo}(Q^{\prime})$. Then by the same rules we get

[TABLE]

and \big{(}(\nu k)(\nu l)(m?y.[n=l]\pi.0\;|\;Q^{\prime}),(\nu k)(\nu l)(m?y.0\;|\;Q^{\prime})\big{)}\in{\cal R} holds.

• (ii)

if by rules (par-r), (res) and (open) is derived

[TABLE]

then $l\notin\mathsf{n}(\alpha)$. Notice that the scope of channel $l$ cannot be extruded this way since $l\notin\mathsf{fo}(Q)$. Hence, process $Q$ cannot perform output action with object $l$. Then by the same rules we get

[TABLE]

and, again, \big{(}(\nu l)(m?y.[n=l]\pi.0\;|\;Q^{\prime}),(\nu l)(m?y.0\;|\;Q^{\prime})\big{)}\in{\cal R} holds.

—Synchronization of branches:*  We again distinguish two cases:*

• (i)

if from

[TABLE]

where we can make the same observation on $Q$ as before to conclude that $l\not=n$, by rules (comm-r) and (res) is derived

[TABLE]

Then, using $m?y.0\xrightarrow{m?n}0$, and the same rules as above we get

[TABLE]

and we get \big{(}(\nu k)(\nu l)([n=l]\pi.0\;|\;Q^{\prime}),(\nu k)(\nu l)(0\;|\;Q^{\prime})\big{)}\in{\cal R}.

• (ii)

if from

[TABLE]

where as before we can assume $l\not=n$, by rules (close-r) and (res) is derived

[TABLE]

then using $m?y.0\xrightarrow{m?n}0$, we may observe

[TABLE]

and \big{(}(\nu k)(\nu l)(\nu n)([n=l]\pi.0\;|\;Q^{\prime}),(\nu k)(\nu l)(\nu n)(0\;|\;Q^{\prime})\big{)}\in{\cal R}.

The symmetric cases and the rest of the pairs from $\cal R$ are analogous. For the rest of the pairs note that in all left branch of the first components we have $[n=l]\pi.0$, where $n\not=l$, and hence, its observational power is equivalent to the observational power of inactive process [math] appearing as the left branch in the right components.

Proposition 2**.**

3.10* Let $P$ be a (sum-free) $\pi$-calculus process. If there is a $C_{\_}\pi$ process $Q$, such that $P\sim Q$, then $P$ satisfies the non-forwarding property.*

Proof A.16**.**

Let $P_{\_}1=P$ be a be a (sum-free) $\pi$-calculus process and let $P_{\_}1\xrightarrow{\alpha_{\_}1}P_{\_}2\xrightarrow{\alpha_{\_}2}\ldots\xrightarrow{\alpha_{\_}{m}}P_{\_}{m+1}.$ Let us fix $i\in\{1,\ldots,m-1\}$, and assume $l\notin\mathsf{fn}(P_{\_}i)$ and $\alpha_{\_}i=k?l$. Since without loss of generality we can assume all bound outputs are fresh, we get $\alpha_{\_}j\not=(\nu l)k^{\prime}!l$, for all $j=i+1,\ldots,m$, directly. In addition to the first assumption, let us assume there is $j\in\{i+1,\ldots,m\}$ such that $\alpha_{\_}j=k^{\prime}!l$. Since $P_{\_}1\sim Q_{\_}1$ (where $Q_{\_}1=Q$), we conclude there are $C_{\_}\pi$ processes $Q_{\_}2,\ldots,Q_{\_}{m+1}$ such that

[TABLE]

and $P_{\_}n\sim Q_{\_}n$, for all $n=1,\ldots,m+1$, where $Q_{\_}i\xrightarrow{k?l}Q_{\_}{i+1}$ and $Q_{\_}j\xrightarrow{k^{\prime}!l}Q_{\_}{j+1}$. We now distinguish two cases.

If $l\notin\mathsf{fn}(Q_{\_}i)$ then we get a direct contradiction with Theorem 2.5. 2. 2.

If $l\in\mathsf{fn}(Q_{\_}i)$, we choose a fresh channel $l^{\prime}$ and a substitution $\sigma$ that is defined only on channel $l$ and maps it to $l^{\prime}$. Then, from $P_{\_}j\xrightarrow{\alpha_{\_}j}P_{\_}{j+1}$, by consequitive application of Lemma $1.4.8$ of **[16]**, we conclude $(P_{\_}j)\sigma\xrightarrow{(\alpha_{\_}j)\sigma}(P_{\_}{j+1})\sigma$, for all $j=i+1,\ldots,m$. Since $l\notin\mathsf{fn}(P_{\_}i)$ we get $(P_{\_}i)\sigma=P_{\_}i$. Now from

[TABLE]

and $P_{\_}1\sim Q_{\_}1$, we again conclude there are $C_{\_}\pi$ processes $Q_{\_}2,\ldots,Q_{\_}{m+1}$ such that

[TABLE]

where $P_{\_}j\sim Q_{\_}j$, for all $j=1,\ldots,i$ and $(P_{\_}j)\sigma\sim Q_{\_}j$, for all $j=i+1,\ldots,m+1$. Since $l^{\prime}$ has been chosen to be a fresh channel, we get $l^{\prime}\notin\mathsf{fn}(Q_{\_}i)$, and since $Q_{\_}i\xrightarrow{(k)\sigma?l^{\prime}}Q_{\_}{i+1}$ and $Q_{\_}j\xrightarrow{(k^{\prime})\sigma!l^{\prime}}Q_{\_}{j+1}$, we fall into the first case, and hence, we again get contradiction with Theorem 2.5.

Appendix B Proofs from Section 5

Abbreviations.

For the sake of readability, use the abbreviation

[TABLE]

assuming that $\varphi_{\_}{\llbracket\;\rrbracket}(k)=(k,n_{\_}k,m_{\_}k)$, and we omit writing trailing [math]’s whenever possible.

We may notice that the encoding defined in Table 3 does not introduce any free names by itself, except in the rule for output (and matching prefixed output), where names $n_{\_}a$ and $m_{\_}b$ are introduced. We may also notice also that these introduced names are the ones specified in the renaming policy of names $a$ and $b$, respectively. Hence, the following result is straightforward.

Lemma B.17** (Name invariance).**

Let $P$ be a $\pi$-calculus process and let substitutions $\sigma$ and $\sigma^{\prime}$ be such that $\varphi_{\_}{\llbracket\;\rrbracket}((a)\sigma)=(\varphi_{\_}{\llbracket\;\rrbracket}(a))\sigma^{\prime}$, for all $a\in{\cal N}$. Then $\llbracket(P)\sigma\rrbracket=(\llbracket P\rrbracket)\sigma^{\prime}$.

For the operational correspondence, we will need only one case of the name invariance result, and we state it in the next corollary.

Corollary B.18**.**

If $\varphi_{\_}{\llbracket\;\rrbracket}(k)=(k,n_{\_}k,m_{\_}k)$ and $\varphi_{\_}{\llbracket\;\rrbracket}(x)=(x,n_{\_}x,m_{\_}x)$ then

[TABLE]

For the operational correspondence we will need definition of strong bisimilarity of polyadic $C_{\_}\pi$-calculus. Such definition is exactly the same as Definition 3.7, except that labels of the LTS (where rules in Table 2 are adapted for polyadic calculus following expected lines) are carrying a tuple of channels, i.e.,

[TABLE]

For such strong bisimilarity relation $\sim$ we may show to obey some standard properties stated in the next proposition.

Proposition B.19**.**

$\sim$* is an equivalence relation and a non-input congruence;* 2. 2.

$[a=a]\pi.P\sim\pi.P$; 3. 3.

$P_{\_}1\;|\;(P_{\_}2\;|\;P_{\_}3)\sim(P_{\_}1\;|\;P_{\_}2)\;|\;P_{\_}3$; 4. 4.

$P_{\_}1\;|\;P_{\_}2\sim P_{\_}2\;|\;P_{\_}1$; 5. 5.

$P\;|\;0\sim P$; 6. 6.

$(\nu k)(\nu l)P\sim(\nu l)(\nu k)P$; 7. 7.

$(\nu k)0\sim 0$; 8. 8.

$P_{\_}1\;|\;(\nu k)P_{\_}2\sim(\nu k)(P_{\_}1\;|\;P_{\_}2)$, if $k\notin\mathsf{fn}(P_{\_}1)$; 9. 9.

$!P\sim P\;|\;!P$; 10. 10.

$(\nu k)!k?(x_{\_}1,\ldots,x_{\_}n).P\sim 0$; 11. 11.

$(\nu k,n_{\_}k,m_{\_}k)\mathit{H}_{\_}k\sim 0$.

We take the structural congruence relation $\equiv$ as it is defined for the $\pi$-calculus processes in [16].

Lemma B.20**.**

If $P\equiv Q$ then $\llbracket P\rrbracket\sim\llbracket Q\rrbracket$.

Proof B.21**.**

The proof is by case analysis on the structural congruence rule applied.

$[a=a]\pi.P\equiv\pi.P$.

We distinguish two cases for prefix $\pi$.

1. (a)

If $\pi=[b_{\_}1=c_{\_}1]\ldots[b_{\_}n=c_{\_}n]d?x$, then by definition of the encoding and Proposition B.19 we get

[TABLE] 2. (b)

If $\pi=[b_{\_}1=c_{\_}1]\ldots[b_{\_}n=c_{\_}n]d!g$, then, again, by definition of the encoding and Proposition B.19 we get

[TABLE] 2. 2.

$(\nu k)(\nu l)P\equiv(\nu l)(\nu k)P$. By the definition of the encoding and Proposition B.19 we get

[TABLE] 3. 3.

$(\nu k)0\equiv 0$. By the definition of the encoding and Proposition B.19 we get

[TABLE] 4. 4.

$P\;|\;(\nu a)Q\equiv(\nu a)(P\;|\;Q)$, if $a\notin\mathsf{fn}(P)$. By the definition of the encoding and Proposition B.19 we get

[TABLE] 5. 5.

The rest of the cases are analogous.

Lemma B.22**.**

Let $P$ and $Q$ be $\pi$-calculus processes.

If $P\equiv Q$ then $\mathsf{fnn}(P)=\mathsf{fnn}(Q)$. 2. 2.

If $a\notin\mathsf{fnn}(P)$ then there exist a $\pi$-calculus process $P^{\prime}$ such that $P\equiv P^{\prime}$ and $a\notin\mathsf{fn}(P^{\prime})$. 3. 3.

if $a\notin\mathsf{fnn}(P)$ and $P\rightarrow Q$ then $a\notin\mathsf{fnn}(Q)$.

Proof B.23**.**

The only structural congruence rule affecting free names is $[a=a]\pi.P\equiv\pi.P$, and by the definition $\mathsf{fnn}([a=a]\pi.P)=\mathsf{fnn}(\pi.P)$. 2. 2.

Assume $a\notin\mathsf{fnn}(P)$. If $a\notin\mathsf{fn}(P)$ then the proof is finished. Now assume $a\in\mathsf{fn}(P)$. Then $a$ can appear only in $P$ in a sub-process of the form $[a=a]\pi.Q$. In this case we may show, by induction on the structure of $P$, that using the structural congruence rule $[a=a]\pi.Q\equiv\pi.Q$, we can get rid of all such matchings that mention name $a$. 3. 3.

Follows by an easy induction on $\rightarrow$ derivation.

• Lemma 5.12

If $P\rightarrow Q$ then $\llbracket P\rrbracket\;|\;\mathit{H}\xrightarrow{\tau}\negthickspace{}^{*}\sim\llbracket Q\rrbracket\;|\;\mathit{H},$ where

• –

if $\mathsf{fnn}(P)=\{k_{\_}1,\ldots,k_{\_}n\}$, then

[TABLE]

• –

if $\mathsf{fnn}(P)=\emptyset$ then $\mathit{H}=0$.

Proof B.24**.**

The proof is by induction on $\rightarrow$ derivation.

Base case*: $k!l.P\;|\;k?x.Q\rightarrow P\;|\;Q\{l/x\}$. Since $k$ and $l$ are free in the starting process, we can encode it as*

[TABLE]

where if $\mathsf{fnn}(k!l.P\;|\;k?x.Q)=\{k,l,k_{\_}1,\ldots,k_{\_}n\}$ then $\mathit{H}=\prod\limits_{\_}{i\in\{1,\ldots,n\}}\mathit{H}_{\_}{k_{\_}i}.$ If $\mathsf{fnn}(k!l.P\;|\;k?x.Q)=\{k,l\}$ then $\mathit{H}=0$. Then,

[TABLE]

where the output process synchronize with the left thread of the handler of name $k$ and with the right thread of the handler of name $l$. At this point, the two handlers can synchronize and the last process evolves to

[TABLE]

where, after the synchronization of the two handlers, name $l$ (together with $n_{\_}l$, $m_{\_}l$ and $t^{\prime}$) is finally received in the input process, after which channel $t^{\prime}$ is also received in the left-hand side process, making the encoding of processes $P$ an $Q$ only unlocked in the synchronization:

[TABLE]

By Corollary B.18 we get

[TABLE]

Hence, we conclude the last derived process in equation (1) is equal to

[TABLE]

Since $e_{\_}2,e_{\_}1,t^{\prime}\notin\mathsf{fn}(\llbracket P\rrbracket\;|\;\llbracket Q\{l/x\}\rrbracket\;|\;0\;|\;\mathit{H}_{\_}k\;|\;!n_{\_}l?y.y!l\;|\;0)$, by Proposition B.19 we have that the last derived process is strongly bisimilar to

[TABLE] 2. 2.

$P\;|\;R\rightarrow Q\;|\;R$* is derived from $P\rightarrow Q$. By induction hypothesis*

[TABLE]

where $S\sim\llbracket Q\rrbracket\;|\;\mathit{H}_{\_}1$ and if $\mathsf{fnn}(P)=\{k_{\_}1,\ldots,k_{\_}n\}$ then

[TABLE]

*and if $\mathsf{fnn}(P)=\emptyset$ then $\mathit{H}_{\_}1=0$. Now, if $\mathsf{fnn}(R)\setminus\mathsf{fnn}(P)=\{l_{\_}1,\ldots,l_{\_}m\}$, let us take *

[TABLE]

If $\mathsf{fnn}(R)\setminus\mathsf{fnn}(P)=\emptyset$ let us take $\mathit{H}_{\_}2=0$. Then, by (par-l) we can derive

[TABLE]

By Lemma B.19 we get $\llbracket P\rrbracket\;|\;\mathit{H}_{\_}1\;|\;\llbracket R\rrbracket\;|\;\mathit{H}_{\_}2\sim\llbracket P\rrbracket\;|\;\llbracket R\rrbracket\;|\;\mathit{H}_{\_}1\;|\;\mathit{H}_{\_}2$ then

[TABLE]

where $S^{\prime}\sim S\;|\;\llbracket R\rrbracket\;|\;\mathit{H}_{\_}2$, by the definition of strong bisimilarity. We can now conclude

[TABLE] 3. 3.

$(\nu k)P\rightarrow(\nu k)Q$* is derived from $P\rightarrow Q$. Again, by induction hypothesis*

[TABLE]

where $S\sim\llbracket Q\rrbracket\;|\;\mathit{H}_{\_}1$ and if $\mathsf{fnn}(P)=\{k_{\_}1,\ldots,k_{\_}n\}$ then

[TABLE]

while if $\mathsf{fnn}(P)=\emptyset$ then $\mathit{H}_{\_}1=0$. Since,

[TABLE]

we distinguish two cases:

1. (a)

if $k\in\mathsf{fnn}(P)$ then $\mathit{H}_{\_}k\;|\;\mathit{H}=\mathit{H}_{\_}1$. Since $k,n_{\_}k,m_{\_}k\notin\mathsf{fn}(\mathit{H})$, by Proposition B.19 we get

[TABLE]

where $\xrightarrow{\tau}\negthickspace{}^{*}$ transition(s) follows by the induction hypothesis and rule (res). By Proposition B.19

[TABLE]

and by definition and transitivity of strong bisimilarity we get

[TABLE] 2. (b)

if $k\notin\mathsf{fnn}(P)$, then $\mathit{H}=\mathit{H}_{\_}1$. By Lemma B.22 there exist $P^{\prime}$ such that $P\equiv P^{\prime}$ and $k\notin\mathsf{fn}(P^{\prime})$. Since $\equiv$ is a congruence and by Lemma B.20 we get $\llbracket P\rrbracket\sim\llbracket P^{\prime}\rrbracket$ and $\llbracket(\nu k)P\rrbracket\sim\llbracket(\nu k)P^{\prime}\rrbracket$. Then, by definition of the encoding and Proposition B.19 we have

[TABLE]

Since $P\rightarrow Q$ and $k\notin\mathsf{fnn}(P)$, by Lemma B.22 we get $k\notin\mathsf{fnn}(Q)$. By the same lemma we conclude there exist $Q^{\prime}$ such that $Q\equiv Q^{\prime}$ and $k\notin\mathsf{fn}(Q^{\prime})$. Hence, again

[TABLE]

*By definition and transitivity of strong bisimilarity we get *

[TABLE] 4. 4.

$P^{\prime}\rightarrow Q^{\prime}$* is derived from $P\rightarrow Q$, where $P\equiv P^{\prime}$ and $Q\equiv Q^{\prime}$. By induction hypothesis*

[TABLE]

where $S\sim\llbracket Q\rrbracket\;|\;\mathit{H}_{\_}1$, and if $\mathsf{fnn}(P)=\{k_{\_}1,\ldots,k_{\_}n\}$ then

[TABLE]

while if $\mathsf{fnn}(P)=\emptyset$ then $\mathit{H}_{\_}1=0$. By Lemma B.20 and Lemma B.22, $P\equiv P^{\prime}$ implies $\llbracket P\rrbracket\sim\llbracket P^{\prime}\rrbracket$ and $\mathsf{fnn}(P)=\mathsf{fnn}(P^{\prime}$), and $Q\equiv Q^{\prime}$ implies $\llbracket Q\rrbracket\sim\llbracket Q^{\prime}\rrbracket$. Then, by Proposition B.19 we get $\llbracket P\rrbracket\;|\;\mathit{H}_{\_}1\sim\llbracket P^{\prime}\rrbracket\;|\;\mathit{H}_{\_}1$, hence, by definition of strong bisimilarity

[TABLE]

where $S^{\prime}\sim S\sim\llbracket Q\rrbracket\;|\;\mathit{H}_{\_}1\sim\llbracket Q^{\prime}\rrbracket\;|\;\mathit{H}_{\_}1$, which completes the proof.

As a direct consequence of Lemma 5.12, we get the operational correspondence result for the encoding of closed $\pi$-calculus processes.

• Theorem 5.14

Let $P$ be a closed (sum-free) $\pi$-calculus process. If $P\rightarrow Q$ then $\llbracket P\rrbracket\xrightarrow{\tau}\negthickspace{}^{*}\sim\llbracket Q\rrbracket$.