# Confidentiality Analysis of Mobile Systems

Jérôme Feret

► To cite this version:

Jérôme Feret. Confidentiality Analysis of Mobile Systems. he 7th International Symposium on Static Analysis (SAS’00), J. Palsberg, Jun 2000, Santa Barbara, United States. pp.135–154, 10.1007/978-3-540-45099-3_8 . inria-00527941

HAL Id: inria-00527941

https://inria.hal.science/inria-00527941v1

Submitted on 15 Feb 2025

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

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

<figure><img src="image_1.png" /></figure>
# Confidentiality Analysis of Mobile Systems

Jérôme Feret

jerome.feret@ens.fr

Laboratoire d'Informatique de l'École Normale Supérieure
ENS-LIENS, 45, rue d'Ulm, 75230 PARIS cédex 5, FRANCE

http://www.di.ens.fr/~feret

**Abstract.** We propose an abstract interpretation-based analysis for automatically detecting all potential interactions between the agents of a part of a mobile system, without much knowledge about the rest of it. We restrict our study to mobile systems written in the π-calculus, and introduce a non-standard semantics which restores the link between channels and the processes that have created them. This semantics also allows to describe the interaction between a system and an unknown context. It is, to the best of our knowledge, the first analysis for this problem. We then abstract this non-standard semantics into an approximated one so as to automatically obtain a non-uniform description of the communication topology of mobile systems which compute in hostile contexts.

## 1 Introduction

Growing requirements of society impose the use of widely spread mobile systems of processes. In such systems the communication topology dynamically changes during processes computations, so that their analysis is a very difficult task. Furthermore, the size of systems, such as the Internet for instance, is large enough to prevent a single person from knowing the whole system. That is why we are interested in validating properties on a mobile system, which is a part of bigger one, called its context, without having precise knowledge of this context.

We address the problem of proving the confidentiality of such a mobile system: we propose to automatically infer a sound and accurate description of the topology of the interactions between the agents of this mobile system, in order to prove that private information can only be communicated to authorized agents. This description should be non-uniform, in order to distinguish between recursive instances of processes. This allows for instance to prove that in an *ftp* protocol the response to a query is returned to the correct customer.

We propose an automatic abstract interpretation-based analysis for the full π-calculus [18,19] which is a suitable formalism to describe mobile systems of processes. We present a new non-standard semantics, in the style of Venet's work [22], which mainly consists of labeling each recursive instance of processes with markers, in a deterministic way inferred during process creation. This labeling allows to trace precisely the origin of channels and to distinguish between recursive instances of processes, which cannot be done with the standard semantics. Besides, we require no further restrictions on the π-calculus. Moreover, our
semantics is general enough to approximate the potential behaviour of a small
known system in any unknown context.

Several abstractions of our non-standard semantics can be deduced, using Abstract Interpretation, we propose a generic abstract semantics to describe the interactions between processes and between the system’s context, in order to automatically prove confidentiality properties. The implementation of the product between this semantics and another one focusing on counting occurrences of processes during computations [13] has lead to original results.

The standard semantics is given in Sect. 3. We define the non-standard semantics in Sect. 4. We design a generic abstract analysis to validate confidentiality of systems in Sect. 5 and instantiate it in Sect. 6.

**Acknowledgments.** We deeply thank anonymous referees for their signif-
icant comments on an early version. We wish also to thank Patrick and Rad-
hia Cousot, Arnaud Venet, Ian Mackie, François Maurel, David Monniaux and
François Pottier, for their comments and discussions.

## 2 Related Work

The problem of proving the confidentiality of a mobile system has been studied extensively. Several type-based methods have been proposed to capture non-interference properties between processes in [1,16] or to study information flow properties in [15]. All these works rely on the use of a partial order of security levels, and consist in statically checking that, owing analyzed properties, low security level agents cannot violate higher security level information.

Control flow analysis only focus on the flow information. Several uniform (or
monovariant) analyses have been proposed [3,4]. Non-uniform (or polyvariant)
analysis allows to describe the interaction between iterations of the same re-
cursive process. This is not achievable by type-based methods, since the same
security level is inferred for all recursive instances of the same process. For in-
stance, in [20] to prove the confidentiality of a customer-server protocol, the
set of customers has to be known before the beginning of the analysis. Only
very few non-uniform analyses are available. Some alias analyses to infer pointer
equality relationships are non-uniform, e.g. [12] which refines a uniform analysis
(trivially based on type declaration). This has been applied by Colby to design
a non-uniform control flow analysis for CML in [6]. This requires a good uniform
approximation of the control flow of a system before starting the non-uniform
analysis.

Our study follows Venet's work on the π-calculus [22], which allows to infer
a sound non-uniform description of the topology of communication between the
agents of *friendly systems* [18], in where resources cannot be nested. We consider
the full π-calculus with nested replications. Moreover, we consider any open sys-
tem and approximate the interaction between this system and its context which,
to the best of our knowledge has never been achieved in a control flow analysis
of the π-calculus. In particular, contrary to [1] we can propagate interactions
without immediately reporting an error. Our framework can be easily adapted
to other formalisms such as *the mobile ambients* [5], for instance.

3 π-calculus

π-calculus [18,19] is a formalism used to describe mobile systems, which is based
on the use of processes and channels. We consider a lazy synchronous version
of the polyadic π-calculus, inspired by the asynchronous version introduced by
Turner [21] and the chemical abstract machine [2] in which communication prim-
itives are very simple while ensuring the same expressive power. Let Channel
be a countable set of channel names. The standard semantics of the π-calculus,
given in Fig. 1, relies on the use of both a reduction relation to define results of
processes computations, and a congruence relation to reveal redexes by making
the processes meet.

*Example 1.* We model a system *S* which describes an *ftp* protocol. A resource creates repeatedly a new customer which sends a query to the server, composed with data and his email address. Data processing is abstracted away to make everything simpler. The server receives the query and returns the data back to the customer’s email.

Syntax of S is given as follows:

$$
S := (\nu \text{ port})(\nu \text{ gen}) (\mathbf{Server} \mid \mathbf{Customer} \mid \text{gen}![])
$$

where

$$
\mathbf{Server} := *\mathit{port?}[\mathit{info},\mathit{add}] (\mathit{add}![\mathit{info}])
$$

$$
\mathbf{Customer} := *\mathit{gen?}[] ((\nu \mathit{data}) (\nu \mathit{email}) \mathit{port}![\mathit{data},\mathit{email}] | \mathit{gen}![])
$$

For example, a short computation of S is given as follows:

$$
\begin{align*}
S & \rightarrow (\nu \text{ port})(\nu \text{ gen})(\nu \text{ data}_1)(\nu \text{ email}_1) \\
  & \qquad (\text{Server} \mid \text{Customer} \mid \text{port!}[\text{data}_1, \text{email}_1] \mid \text{gen!}] ) \\
  & \rightarrow (\nu \text{ port})(\nu \text{ gen})(\nu \text{ data}_1)(\nu \text{ email}_1) \\
  & \qquad (\text{Server} \mid \text{Customer} \mid \text{email}_1![\text{data}_1] \mid \text{gen!}] ) \\
  & \rightarrow (\nu \text{ port})(\nu \text{ gen})(\nu \text{ data}_1)(\nu \text{ email}_1) (\nu \text{ data}_2)(\nu \text{ email}_2) \\
  & \qquad (\text{Server} \mid \text{Customer} \mid \text{gen!}] \mid \text{email}_1![\text{data}_1] \mid \text{port!}[\text{data}_2, \text{email}_2]) \\
  & \rightarrow (\nu \text{ port})(\nu \text{ gen})(\nu \text{ data}_1)(\nu \text{ email}_1) (\nu \text{ data}_2)(\nu \text{ email}_2) \\
  & \qquad (\text{Server} \mid \text{Customer} \mid \text{gen!}] \mid \text{email}_1![\text{data}_1] \mid \text{email}_2![\text{data}_2]) \quad \square
\end{align*}
$$

As illustrated in the above example, the configuration of a mobile system *S*
at any stage is always congruent to one of the particular form, (ν c)(P₁ | ... | Pₙ)
where c is a sequence of names, and P₁, ..., Pₙ are sub-processes beginning
with a matching, a message, an input guard or a replication guard. Those are
syntactic copies of sub-processes of *S*, which have been substituted during the
communications. Standard semantics does not allow to trace neither the origin
of those processes, nor the origin of the channels they have declared, because
of the use of α-conversion: in example 1, it is impossible to express that in the
sub-process emailᵢ![:dataᵢ], channels emailᵢ and dataᵢ have been created by the
same recursive instance of the resource Customer.
$$ P ::= \begin{array}{lcl} P & ::= & \text{action.}P \qquad (\text{Action}) \\ & | & (P | P) \qquad (\text{Parallel composition}) \\ & | & \emptyset \qquad (\text{End of a process}) \end{array} $$

$$ \begin{array}{lcl} \text{action} & ::= & c![x_1, \dots, x_n] \qquad (\text{Message}) \\ & | & c?[x_1, \dots, x_n] \qquad (\text{Input guard}) \\ & | & *c?[x_1, \dots, x_n] \qquad (\text{Replication guard}) \\ & | & (\nu x) \qquad (\text{Channel creation}) \end{array} $$

where $c, x_1, \dots, x_n, x, y \in \text{Channel}, n \ge 0$. Input guard, replication guard and channel creation are the only name binders, i.e in $c?[x_1, \dots, x_n]P$ (resp. $(\nu x)P$), occurrences of $x_1, x_2, \dots, x_n$ (resp. $x$) in $P$ are considered bound. Usual rules about scopes, substitution and $\alpha$-conversion apply. We denote by $\mathcal{FN}(P)$ the set of free names of $P$, i.e names which are not under a scope binder and by $\mathcal{BN}(P)$ the set of bound names of $P$.

(a) Syntax

$$ \begin{array}{l@{\qquad}l} (\nu x)P \equiv (\nu y)P[x \leftarrow y] & \text{if } y \notin \mathcal{FN}(P) \qquad (\alpha\text{-conversion}) \\ P | Q \equiv Q | P & \text{(Commutativity)} \\ P | (Q | R) \equiv (P | Q) | R & \text{(Associativity)} \\ (\nu x)(\nu y)P \equiv (\nu y)(\nu x)P & \text{(Swapping)} \\ ((\nu x)P) | Q \equiv (\nu x)(P | Q) & \text{if } x \notin \mathcal{FN}(Q) \qquad (\text{Extrusion}) \end{array} $$

where $c, x, y \in \text{Channel}$

(b) Congruence relation

$$ c![x_1, \dots, x_n]P \mid c?[y_1, \dots, y_n]Q \rightarrow P \mid Q[y_1 \leftarrow x_1, \dots, y_n \leftarrow x_n] \\ c![x_1, \dots, x_n]P \mid *c?[y_1, \dots, y_n]Q \rightarrow P \mid Q[y_1 \leftarrow x_1, \dots, y_n \leftarrow x_n] \mid *c?[y_1, \dots, y_n]Q $$

$$ \frac{P \to Q}{(\nu x)P \to (\nu x)Q} \qquad \frac{P' \equiv P \quad P \to Q \quad Q \equiv Q'}{P' \to Q'} \qquad \frac{P \to P'}{P \mid Q \to P' \mid Q} $$

where $c, x_1, \dots, x_n, y_1, \dots, y_n \in \text{Channel}$

(c) Reduction relation

<caption>**Fig. 1.** The chemical semantics</caption>
# 4 Non-standard Semantics

The non-standard semantics is a refined semantics, which aims at explicitly specifying the links between channels and the instances of processes which have declared them. Any instance of a process is identified unambiguously by a marker in order to distinguish that instance from all others. Tracing the origin of channel names is then easily done by identifying each new channel name with the marker of the process which has created it. Venet, in [22], has designed such a non-standard semantics, but its applies only to a small part of the π-calculus, called the friendly systems [18]. It especially requires resources not to be nested, and the system to be closed. We propose a new non-standard semantics in order to remove those restrictions.

## 4.1 Closed Systems

Let Lbl be an infinite set of labels. We denote by Id the set of all binary trees the leaves of which are all labeled with ε and the nodes of which are labeled with a pair (i, j) where both i and j are in Lbl. The tree having a node labeled a, a left sibling t₁ and a right one t₂ is denoted by N(a, t₁, t₂).

Let us first consider the case of a closed mobile system S in the π-calculus (the general case will be considered in Sect 4.2) and assume without any loss of generality that two channel binders of S are never used on the same channel name. We locate syntactic components of S by marking each sign ? and ! occurring in S with distinct labels in Lbl, the subset of Lbl used in labeling S is denoted by Lbl<sub>used</sub>. A non-standard configuration is a set of thread instances, where a thread instance is a triplet composed with a syntactic component, a marker and an environment. The syntactic component is a copy of a sub-process of S, the marker is calculated at the creation of the thread and the environment specifies the semantic value of each free name of the syntactic component. Thread instances are created at the beginning of the system computation and while processes are running. In both cases, several threads are spawned, corresponding to a set of syntactic components, calculated by applying the function Agent, defined as follows, either on S for initial threads, or on the continuation of running processes.

$$ 
\begin{align*}
Agent(\emptyset) &= \{\} \\
Agent(x^i[x_1, \dots, x_n]P) &= \{x^i[x_1, \dots, x_n]P\} \\
Agent(y^i[y_1, \dots, y_n]P) &= \{y^i[y_1, \dots, y_n]P\} \\
Agent(*y^i[y_1, \dots, y_n]P) &= \{*y^i[y_1, \dots, y_n]P\} \\
Agent(P | Q) &= Agent(P) \cup Agent(Q) \\
Agent((\nu x)P) &= Agent(P)
\end{align*}
$$

Markers are binary trees in Id. Initial thread markers are ε, while new threads markers are calculated recursively from the marker of the threads whose computation has lead to their creation:

- when an execution does not involve fetching a resource, the marker of the computed thread is just passed to the threads in its continuation;
- when a resource is fetched, markers of new threads in its continuation are $N((i, j), id_*, id_!)$, where $(*y?^i[\bar{y}]P,id_*,E_*)$ is the resource thread and $(x!^j[\bar{x}]Q,id_!,E_!)$ the message thread.

Environments map each free name of syntactic components to a pair $(a, b)$ where $a$ is a bound name of $S$ and $b$ is a marker. Intuitively, $a$ refers to the binder $(\nu a)$ which has been used in declaring the channel, and $b$ is the marker of the thread which has declared it. While threads are running, environments are calculated in order to mimic the standard semantics.

The translation of a labeled system $S$ into a set of initial threads and non-standard computation rules are given in Fig. 2. Standard and non-standard semantics are in bisimulation. The proof relies on that non-standard computations cannot yield conflicts between threads markers.

*Example 2.* We give the non-standard configuration describing the ftp server, just after that two connections with customers have been completed.

Labelling of $S$ is given as follows:

$$S := (\nu \text{ port})(\nu \text{ gen}) (\mathbf{Server} | \mathbf{Customer} | \text{gen!}^6])$$

where

$$\mathbf{Server} := *\text{port?}^1[\text{info,add}] (\text{add?}^2[\text{info}])$$

$$\mathbf{Customer} := *\text{gen?}^3[] ((\nu \text{ data}) (\nu \text{ email}) \text{ port?}^4[\text{data, email}] | \text{gen?}^5[]))$$

The non-standard configuration is given as follows, each sub-process is denoted by the first label occurring in its syntax.

$$\left\{ \begin{array}{l} \left( \begin{array}{l} 1, \varepsilon, \left\{ \begin{array}{l} \text{port} \mapsto (\text{port}, \varepsilon) \end{array} \right. \right\} \\ \left( \begin{array}{l} 3, \varepsilon, \left\{ \begin{array}{l} \text{gen} \mapsto (\text{gen}, \varepsilon) \\ \text{port} \mapsto (\text{port}, \varepsilon) \end{array} \right. \right\} \\ \left( \begin{array}{l} 2, id'_1, \left\{ \begin{array}{l} \text{add} \mapsto (\text{email}, id_1) \\ \text{info} \mapsto (\text{data}, id_1) \end{array} \right. \right\} \\ \left( \begin{array}{l} 2, id'_2, \left\{ \begin{array}{l} \text{add} \mapsto (\text{email}, id_2) \\ \text{info} \mapsto (\text{data}, id_2) \end{array} \right. \right\} \\ \left( \begin{array}{l} 5, id_2, \left\{ \begin{array}{l} \text{gen} \mapsto (\text{gen}, \varepsilon) \end{array} \right. \right\} \end{array} \right) \end{array} \right\} \quad \text{where} \quad \left\{ \begin{array}{l} id_1 = N((3, 6), \varepsilon, \varepsilon) \\ id'_1 = N((1, 4), \varepsilon, id_1) \\ id_2 = N((3, 5), \varepsilon, id_1) \\ id'_2 = N((1, 4), \varepsilon, id_2) \end{array} \right.$$

We shall remark that, since $S$ has no embedded resources, markers are all sequences, instead of trees. It explicitly appears that each time a copy of sub-process 2 is created, both channels add and info are bound to two channel names created by the same replication of the resource 3. $\square$

## 4.2 Interactions with a Context

We now extend our non-standard semantics to open systems. An open system $S$ is a part of a bigger closed system, the rest of which is called its context. The context is a set of processes, concurrently running with the processes of $S$. We
$$
C_0(S) = \{(p, \varepsilon, E_p) \mid p \in \text{Agent}(S)\}, \text{ where } E_p = \begin{cases} \mathcal{F}\mathcal{N}(p) & \to \mathcal{BN}(S) \times \text{Id} \\ x & \mapsto (x, \varepsilon) \end{cases}.
$$

(a) $C_0$ calculates the set of initial threads

Let $C$ be a non-standard configuration,
if there are $\lambda, \mu \in C$,
with $\lambda=(y_1^{?i}[y_1, \dots, y_n]P, id_?, E_?)$ and $\mu=(x!^j[x_1, \dots, x_n]Q, id_!, E_!)$,
such that $E_?(y) = E_!(x)$,
then $C \to_2 C'$,
where $C' = (C \setminus \{\lambda, \mu\}) \cup (f_?(Agent(P))) \cup (f_!(Agent(Q)))$,

$$
f_? : Ag \mapsto \left( Ag, id_?, \begin{cases} z \mapsto E_?(z) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{FN}(y_1^{?i}[y_1, \dots, y_n]P) \\ y_k \mapsto E_!(x_k) & \text{if } y_k \in \mathcal{FN}(Ag) \\ z \mapsto (z, id_?) & \text{if } \begin{cases} z \in \mathcal{FN}(Ag) \cap \mathcal{BN}(y_1^{?i}[y_1, \dots, y_n]P) \\ z \notin \{y_k \mid k \in [|1; n|]\} \end{cases} \end{cases} \right)
$$

$$
\text{and } f_! : \text{Ag} \mapsto \left( \text{Ag}, id_!, \begin{cases} z \mapsto E_!(z) & \text{if } z \in \mathcal{FN}(\text{Ag}) \cap \mathcal{FN}(x!^j[x_1, \dots, x_n]Q) \\ z \mapsto (z, id_!) & \text{if } z \in \mathcal{FN}(\text{Ag}) \cap \mathcal{BN}(x!^j[x_1, \dots, x_n]Q) \end{cases} \right).
$$

(b) Non-standard communication

Let $C$ be a non-standard configuration,
if there are $\lambda, \mu \in C$,
with $\lambda=(*y_1^{?i}[y_1, \dots, y_n]P, id_?, E_?)$ and $\mu = (x!^j[x_1, \dots, x_n]Q, id_!, E_!)$,
such that $E_?(y) = E_!(x)$,
then $C \to_2 C'$,
where $C' = (C \setminus \{\mu\}) \cup (f_?(Agent(P))) \cup (f_!(Agent(Q)))$,
$id_* = N((i, j), id_?, id_!)$

$$
f_? : Ag \mapsto \left( Ag, id_*, \begin{cases} z \mapsto E_?(z) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{FN}(y_1^{?i}[y_1, \dots, y_n]P) \\ y_k \mapsto E_!(x_k) & \text{if } y_k \in \mathcal{FN}(Ag) \\ z \mapsto (z, id_*) & \text{if } \begin{cases} z \in \mathcal{FN}(Ag) \cap \mathcal{BN}(y_1^{?i}[y_1, \dots, y_n]P) \\ z \notin \{y_k \mid k \in [|1; n|]\} \end{cases} \end{cases} \right)
$$

$$
\text{and } f_! : \text{Ag} \mapsto \left( \text{Ag}, id_!, \begin{cases} z \mapsto E_!(z) & \text{if } z \in \mathcal{FN}(\text{Ag}) \cap \mathcal{FN}(x!^j[x_1, \dots, x_n]Q) \\ z \mapsto (z, id_!) & \text{if } z \in \mathcal{FN}(\text{Ag}) \cap \mathcal{BN}(x!^j[x_1, \dots, x_n]Q) \end{cases} \right).
$$

(c) Non-standard resource fetching

<caption>**Fig. 2.** Non-standard semantics for close systems</caption>
represent this context by the set of names it shares with $S$, called unsafe names, and approximate it as an intruder which is able to form any possible process working on these channel names. An interaction between $S$ and its context, may only consist in a communication between a process $p_S$ of the first one and a process $p_{cont}$ of the second one, via an unsafe name. This communication is called spying when $p_{cont}$ is the receiver, and spoiling when $p_{cont}$ is the message sender. While spying, the context listens to new channel names which get unsafe. While spoiling, the context may pass any name to $S$, either an unsafe name created by a binder of $S$ or a name created by the context itself, thus we have to introduce an infinite set of unsafe names that the context may have created. At last, spoiling may lead to a resource fetching, which would require to create an unambiguous marker, otherwise the consistency of the semantics would not be preserved.

Since $\alpha$-conversion allows us to choose the names of new channels created by the context, we may assume those channels have been declared by recursive instances of a single process. Choosing $cont_?$, $cont_! \in Lbl \setminus Lbl_{used}$ and $ext \in Channel \setminus BN(S)$, such channels will be seen as if they were created by the binder $(\nu ext)$ of a recursive instance of a process whose marker is $t_n$, where $t_n$ is recursively defined as follows:

$$ \left\{ \begin{array}{l} t_0 = N((cont_?, cont_!), \varepsilon, \varepsilon) \\ t_{n+1} = N((cont_?, cont_!), \varepsilon, t_n) \end{array} \right. $$

We then denote by $\mathcal{EN}$ the set $\{(ext, t_n) | n \in \mathbb{N}\}$ and assume that every spoiling message are syntactic copies of a single process, whose first sign is labeled with $cont_?$. The coherence of our semantics mainly relies on the fact that during a computation, there cannot have been two different instances of a single process with the same marker. We guarantee this property by associating to each spoiling message an hypothetical fresh marker $t_n$.

A non-standard configuration is now a triplet $(C, \text{Unsafe}, \text{Unused})$, where $C$ is a set of threads, $\text{Unsafe}$ is a set of pairs $(a,id)$, such that channel names created by the binder $(\nu a)$ of the recursive instance of a process whose marker was $id$ is unsafe, and $\text{Unused}$ is a set of fresh markers which have not been used as markers for spoiling message. $S$ may start with several initial configurations, since free names have to be chosen among the set of initial unsafe names. The transition relation $\mapsto$ holds both with computations inside the mobile system $S$ and computations involving the system $S$ and its context. Initial non-standard configurations and computation rules are given in Figs. 3 and 4.

$$ \left( \left\{ (p, \varepsilon, E_p) \mid p \in \text{Agent}(S) \right\}, \mathcal{EN}, \{t_n \mid n \in \mathbb{N}\} \right) \in C_0(S) \\ \iff \left\{ \begin{array}{l} \forall p \in \text{Agent}(S), \forall x \in \mathcal{FN}(p), \\ E_p(x) = (x, \varepsilon) \text{ if } x \in BN(S), \\ \exists n \text{ such that } E_p(x) = (ext, t_n) \text{ otherwise} \end{array} \right. $$

<caption>Fig. 3. Non-standard initial configurations for open systems</caption>
$$ \frac{C \to_2 C'}{(C, \text{Unsafe, Unused}) \mapsto (C', \text{Unsafe, Unused})} $$

(a) Non-standard safe transitions

Let (C, Unsafe, Unused) be a non-standard configuration,
if there is $\lambda \in C$, with $\lambda=(x!^j[x_1, ..., x_n]P, id_!, E_!)$,
such that $E_!(x) \in \text{Unsafe}$,
then (C, Unsafe, Unused) $\mapsto$ (C', Unsafe', Unused),
where $C' = (C \setminus \{\lambda\}) \cup (f_!(\text{Agent}(P)))$,

$$ f_! : Ag \mapsto \left( Ag, id_! \begin{cases} z \mapsto E(z) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{FN}(x!^j[x_1, ..., x_n]P) \\ z \mapsto (z, id_!) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{BN}(x!^j[x_1, ..., x_n]P) \end{cases} \right) $$
and $\text{Unsafe}' = \text{Unsafe} \cup \{E(x_k) | k \in [[1; n]]\}$.

(b) Non-standard spied communication

Let (C, Unsafe, Unused) be a non-standard configuration,
if there are $\lambda \in C$, with $\lambda=(y?^i[y_1, ..., y_n]P, id?, E?)$ and $u_1, ..., u_n \in \text{Unsafe}$,
such that $E_?(y) \in \text{Unsafe}$,
then (C, Unsafe, Unused) $\mapsto$ (C', Unsafe, Unused),
where $C' = (C \setminus \{\lambda\}) \cup (f_?(\text{Agent}(P)))$,

$$ f_? : Ag \mapsto \left( Ag, id_? \begin{cases} z \mapsto E_?(z) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{FN}(y?^i[y_1, ..., y_n]P) \\ y_k \mapsto u_k & \text{if } y_k \in \mathcal{FN}(Ag) \\ z \mapsto (z, id_?) & \text{if } \begin{cases} z \in \mathcal{FN}(Ag) \cap \mathcal{BN}(y?^i[y_1, ..., y_n]P) \\ z \notin \{y_k | k \in [[1; n]]\} \end{cases} \end{cases} \right) $$

(c) Non-standard spoilt communication

Let (C, Unsafe, Unused) be a non-standard configuration,
if there are $\lambda \in C$, with $\lambda=(*y?^i[y_1, ..., y_n]P, id?, E_?), u_1, ..., u_n \in \text{Unsafe}, id \in \text{Unused}$,
such that $E_?(y) \in \text{Unsafe}$,
then (C, Unsafe, Unused) $\mapsto$ (C', Unsafe, Unused')
where $C' = C \cup (f_?(\text{Agent}(P)))$,
$\text{id}_* = N((i, \text{conb}_!), id?, id)$,

$$ f_? : Ag \mapsto \left( Ag, id_*, \begin{cases} z \mapsto E_?(z) & \text{if } z \in \mathcal{FN}(Ag) \cap \mathcal{FN}(y?^i[y_1, ..., y_n]P) \\ y_k \mapsto u_k & \text{if } y_k \in \mathcal{FN}(Ag) \\ z \mapsto (z, id_*) & \text{if } \begin{cases} z \in \mathcal{FN}(Ag) \cap \mathcal{BN}(y?^i[y_1, ..., y_n]P) \\ z \notin \{y_k | k \in [[1; n]]\} \end{cases} \end{cases} \right) $$

and $\text{Unused}' = \text{Unused} \setminus \{id\}$.

(d) Non-standard spoilt resource fetching

<caption>Fig. 4. Non-standard transitions for open systems</caption>
# 5 Abstract Semantics

We denote by $\mathcal{C}$ the set of all possible non-standard configurations. The set of all possible non-standard configurations a system may take during a finite computation is given by its collecting semantics [7], and can be expressed as the least fix point of the $\cup$-complete endomorphism $\mathbb{F}$ on the complete lattice $(\wp(\mathcal{C}), \subseteq, \cup, \emptyset, \cap, \mathcal{C})$ defined as follows:

$$ \mathbb{F}(X) = C_0(\mathcal{S}) \cup \{C \mid \exists C' \in X : C' \to C\}. $$

Usually, this semantics is not decidable, we use abstract interpretation [8] to design an abstract domain in which a description of the collecting semantics will be finitely designed. We introduce two lattices, left as parameter of our abstraction, $(Id_I^\sharp, \sqsubseteq_1, \cup_1, \perp_1, \cap_1, \top_1)$ and $(Id_2^\sharp, \sqsubseteq_2, \cup_2, \perp_2, \cap_2, \top_2)$, to respectively represent sets of markers and sets of pairs of markers, related to their concrete domains via two monotone maps, $\gamma_1$ and $\gamma_2$:

$$ \begin{aligned} \gamma_1 &: (Id_I^\sharp, \sqsubseteq_1) \to (\wp(Id), \sqsubseteq), \text{ with } \gamma_1(\perp_1) = \emptyset, \\ \gamma_2 &: (Id_2^\sharp, \sqsubseteq_2) \to (\wp(Id \times Id), \sqsubseteq) \text{ with } \gamma_2(\perp_2) = \emptyset. \end{aligned} $$

Let $\mathcal{P}$ be the set of all sub-processes of $\mathcal{S}$, and $\mathcal{C}$ be the set $\{(p, x, y) \mid p \in \mathcal{P}, x \in \mathcal{F}\mathcal{N}(p), y \in \{\mathit{ext}\} \cup \mathcal{B}\mathcal{N}(\mathcal{S})\}$. $\mathcal{C}$ is the set of all possible interactions between agents of $\mathcal{S}$. The interaction $(p, x, y)$ denotes the fact that the channel name $x \in \mathcal{F}\mathcal{N}(p)$ has been declared by the $(\nu y)$ binder, if $y \neq \mathit{ext}$, or has been declared by the context otherwise. Our abstract domain is then the product of three functional domains:

$$ C^{\sharp} = (C_{\mathcal{P}ro}^{\sharp} \times C_{\mathcal{C}om}^{\sharp} \times C_{\mathcal{E}sc}^{\sharp}) \text{ where } \left\{ \begin{array}{ll} C_{\mathcal{P}ro}^{\sharp} : & \mathcal{P}ro \to Id_I^{\sharp} \\ C_{\mathcal{C}om}^{\sharp} : & \mathcal{C}an \to Id_2^{\sharp} \\ C_{\mathcal{E}sc}^{\sharp} : & \mathcal{B}\mathcal{N}(\mathcal{S}) \cup \{\mathit{ext}\} \to Id_I^{\sharp} \end{array} \right. $$

$C_{\mathcal{P}ro}^{\sharp}$ maps each sub-process to the set of markers it may be marked with. $C_{\mathcal{C}om}^{\sharp}$ maps each interaction $(P, x, y)$ to the set of pairs of markers $(id_1, id_2)$, such that $x$ is the free name of a thread whose marker was $id_1$; this thread may have been declared by the $(\nu y)$ binder of a thread whose marker was $id_2$. Finally $C_{\mathcal{E}sc}^{\sharp}$ maps each names $x$ to the set of markers $id$ such that a channel name declared by the binder $(\nu x)$ of a thread whose marker was $id$ may be unsafe.

An abstract configuration $C^{\sharp} = (f_{\mathcal{P}ro}^{\sharp}, f_{\mathcal{C}an}^{\sharp}, f_{\mathcal{E}sc}^{\sharp})$ is then related to a set of concrete configurations by the monotone map $\gamma$, where $\gamma(C^{\sharp})$ is:

$$ \left\{ A \in \wp(\mathcal{C}) \left| \begin{array}{l} \forall (C, \mathit{esc}, \mathit{unused}) \in A, \\ \left\{ \begin{array}{l} \exists (x, id) \in \mathit{esc} \\ \exists (P, id, E) \in C, \\ \left( \exists (P, id, E) \in C, \\ \exists x \in \mathcal{F}\mathcal{N}(P) \end{array} \right) \end{array} \Rightarrow \begin{array}{l} id \in \gamma_1(f_{\mathit{esc}}^{\sharp}(x)) \\ id \in \gamma_1(f_{\mathcal{P}ro}^{\sharp}(P)) \\ (id, id') \in \gamma_2(f_{\mathcal{C}an}^{\sharp}(P, x, y)) \\ \text{where } E(x) = (y, id') \end{array} \end{array} \right\}. $$
The abstract semantics is given by an initial abstract configuration $C_0^\sharp$ and a transition relation $\to$, in Figs. 5 to 10. In the relation $C_1^\sharp \to C_2^\sharp$, $C_2^\sharp$ represents new interactions between agents induced by an abstract computation. The transition relation $\to$ uses several abstract primitives, which must satisfy some soundness conditions:

- two abstract projections: $\Pi_1 : \mathrm{Id}_2^\sharp \to \mathrm{Id}_1^\sharp$ and $\Pi_2 : \mathrm{Id}_2^\sharp \to \mathrm{Id}_1^\sharp$, such that $\{u \in \mathrm{Id} \mid \exists v \in \mathrm{Id} \text{ such that } (u, v) \in \gamma_2(c)\} \subseteq \gamma_1(\Pi_1(c))$ and $\{v \in \mathrm{Id} \mid \exists u \in \mathrm{Id} \text{ such that } (u, v) \in \gamma_2(c)\} \subseteq \gamma_1(\Pi_2(c));$

- two abstract injections: $\mathrm{Inj}_1 : \mathrm{Id}_1^\sharp \to \mathrm{Id}_2^\sharp$ and $\mathrm{Inj}_2 : \mathrm{Id}_1^\sharp \to \mathrm{Id}_2^\sharp$, such that $\{(u, v) \in \mathrm{Id} \times \mathrm{Id} \mid u \in \gamma_1(c)\} \subseteq \gamma_2(\mathrm{Inj}_1(c))$ and $\{(u, v) \in \mathrm{Id} \times \mathrm{Id} \mid v \in \gamma_1(c)\} \subseteq \gamma_2(\mathrm{Inj}_2(c));$

- two abstract joins: $\bowtie : \mathrm{Id}_2^\sharp \times \mathrm{Id}_2^\sharp \to \mathrm{Id}_2^\sharp$ and $\bowtie : \mathrm{Id}_2^\sharp \times \mathrm{Id}_2^\sharp \to \mathrm{Id}_2^\sharp$, such that $\{(u, v) \in \mathrm{Id} \times \mathrm{Id} \mid \exists w \in \Sigma^* \begin{pmatrix} (w, u) & \in \gamma_2(c) \\ (w, v) & \in \gamma_2(c') \end{pmatrix} \} \subseteq \gamma_2(\bowtie (c, c'))$ and $\{(u, v) \in \mathrm{Id} \times \mathrm{Id} \mid \exists w \in \mathrm{Id} \begin{pmatrix} (v, w) & \in \gamma_2(c) \\ (u, w) & \in \gamma_2(c') \end{pmatrix} \} \subseteq \gamma_2(\bowtie (c, c));$

- two abstract marker creators: $\mathrm{push}_1^{(i,j)} : \mathrm{Id}_1^\sharp \times \mathrm{Id}_1^\sharp \to \mathrm{Id}_1^\sharp$ and $\mathrm{push}_2^{(i,j)} : \mathrm{Id}_1^\sharp \times \mathrm{Id}_2^\sharp \to \mathrm{Id}_2^\sharp$, such that $\begin{cases} N((i, j), u, v) & | \quad u \in \gamma_1(c_g) \\ v \in \gamma_1(c_d) \end{cases} \subseteq \gamma_1(\mathrm{push}_1^{(i,j)}(c_g, c_d))$ and $\begin{cases} (N((i, j), u, v), w) & | \quad u \in \gamma_1(c_g) \\ (v, w) & \in \gamma_2(c_d) \end{cases} \subseteq \gamma_2(\mathrm{push}_2^{(i,j)}(c_g, c_d));$

- an abstract marker duplicator: $\mathrm{dpush} : \mathrm{Id}_1^\sharp \to \mathrm{Id}_2^\sharp$, such that $\{(u, u) \mid u \in \gamma_1(c)\} \subseteq \gamma_2(\mathrm{dpush}(c));$

- initial abstract markers: $\varepsilon_1^\sharp \in \mathrm{Id}_1^\sharp$, $\varepsilon_2^\sharp \in \mathrm{Id}_2^\sharp$, $t^\sharp \in \mathrm{Id}_1^\sharp$ such that $\{\varepsilon\} \subseteq \gamma_1(\varepsilon_1^\sharp)$, $\{(\varepsilon, \varepsilon)\} \subseteq \gamma_2(\varepsilon_2^\sharp)$ and $\{t_n \mid n \in \mathbb{N}\} \subseteq \gamma_1(t^\sharp)$.

Roughly speaking, $\Pi_1$ (resp. $\Pi_2$) projects every pair of markers onto its first (resp. second) component. $\mathrm{Inj}_1$ (resp. $\mathrm{Inj}_2$) constructs for every marker the set of pair whose first (resp. second) component is that marker. $\bowtie$ and $\bowtie$ allow to calculate and propagate relational information between the components of a pair of markers throughout communication and resource fetching computations. $\mathrm{push}_1^{(i,j)}$ constructs every marker of the processes created during a replication, using the set of markers of the resource given in its first argument and the set of markers of the message sender given in its second argument. $\mathrm{push}_2^{(i,j)}$ acts similarly to $\mathrm{push}_1^{(i,j)}$, but it takes into account relational information about markers of the free channels names of the message sender. $\mathrm{dpush}$ duplicates every marker into a pair of markers, this is used while creating new channel names. All these conditions imply the following proposition:

**Proposition 1.** If $C \in \gamma(C^\sharp)$ and $C \rightsquigarrow D$, then there exists $D^\sharp$ such that $C^\sharp \to D^\sharp$ and $D \in \gamma(C^\sharp \sqcup D^\sharp)$.
$$
C_0^\sharp = (i_{pro}^\sharp, i_{can}^\sharp, i_{esc}^\sharp)
$$
$$
\text{where}
$$
$$
\left\{
\begin{array}{l}
i_{pro}^\sharp = \begin{cases}
\text{Pro} \to \text{Id}_1^\sharp & \\
P \mapsto \varepsilon_1^\sharp \text{ if } P \in (\text{Agent}(S)) & \\
P \mapsto \bot_1^\sharp \text{ otherwise} &
\end{cases} \\
\\
i_{can}^\sharp = \begin{cases}
\text{Can} \to \text{Id}_2^\sharp & \\
(P, x, x) \mapsto \varepsilon_2^\sharp & \text{if } \begin{cases}
P \in (\text{Agent}(S)) \\
x \in \mathcal{BN}(S) \cap \mathcal{FN}(P)
\end{cases} \\
\\
(P, x, \text{ext}) \mapsto (\text{Inj}_1(\varepsilon_1^\sharp)) \cap_2 (\text{Inj}_2(t^\sharp)) & \text{if } \begin{cases}
P \in (\text{Agent}(S)) \\
x \in \mathcal{FN}(S) \cap \mathcal{FN}(P)
\end{cases} \\
\\
(P, x, y) \mapsto \bot_2^\sharp & \text{otherwise} \\
\\
i_{esc}^\sharp = \begin{cases}
\mathcal{BN}(S) \cup \{\text{ext}\} \to \text{Id}_1^\sharp & \\
\text{ext} \mapsto t^\sharp & \\
x \mapsto \bot_1^\sharp \text{ if } x \in \mathcal{BN}(S) &
\end{cases}
\end{array}
\right.
$$

<caption>Fig. 5. Initial abstract configuration</caption>

As a consequence, the abstract counterpart $\mathbb{F}^\sharp$ of $\mathbb{F}$, defined by

$$
\mathbb{F}^{\sharp}(C^{\sharp}) = C_{0}^{\sharp} \sqcup C^{\sharp} \sqcup \{\overline{C}^{\sharp} | C^{\sharp} \to \overline{C}^{\sharp}\},
$$

satisfies the soundness condition $\mathbb{F} \circ \gamma \subseteq \gamma \circ \mathbb{F}^\sharp$. Using Kleene's theorem, we prove
the soundness of our analysis:

$$
\textbf{Theorem 1.} \quad lfp_{\emptyset} \mathbb{F} \subseteq \bigcup_{n \in \mathbb{N}} \gamma(\mathbb{F}^{\sharp n}(\bot_{\sharp}))
$$

We compute a sound approximation of our abstract semantics by using a
widening operator [7,9] $\nabla : C^{\sharp} \times C^{\sharp} \rightarrow C^{\sharp}$ satisfying the following properties:

$$
- \forall C_1^\sharp, C_2^\sharp \in C^\sharp, C_1^\sharp \sqcup C_2^\sharp \subseteq C_1^\sharp \nabla C_2^\sharp
$$

- for all increasing sequence $(C_n^\sharp) \in (C^\sharp)^N$, the sequence $(C_n^\nabla)$ defined as

$$
\begin{cases}
C_0^\nabla = C_0^\sharp \\
C_{n+1}^\nabla = C_n^\nabla \nabla C_n^\sharp
\end{cases}
$$

is ultimately stationary.

We can easily construct a widening operator $\nabla$ on our abstract domain from
existing widening operators $\nabla_1$ on $Id_1$ and $\nabla_2$ on $Id_2$.

**Theorem 2.** *Abstract iteration[9,10]* *The abstract iteration $(C_n^\nabla)$ of $\mathbb{F}^\sharp$ defined as follows*

$$
\left\{
\begin{array}{l@{\quad}l}
C_0^\nabla = \bot & \\
C_{n+1}^\nabla = \left\{ \begin{array}{ll} C_n^\nabla & \text{if } \mathbb{F}^\sharp(C_n^\nabla) \subseteq C_n^\nabla \\ C_n^\nabla \nabla \mathbb{F}^\sharp(C_n^\nabla) & \text{otherwise} \end{array} \right. &
\end{array}
\right.
$$

is ultimately stationary and its limit $C^\nabla$ satisfies $lfp_0\mathbb{F} \subseteq \gamma(C^\nabla)$.
Let $(f_{pro}^{\sharp}, f_{can}^{\sharp}, f_{esc}^{\sharp})$ be an abstract configuration,
we consider $u \in \mathcal{C}hannel$ and $y?^i[y_1, \dots, y_n]P, x!^j[x_1, \dots, x_n]Q$ two sub-processes,
such that

$$
f_{can}^{\sharp}(y?^{i}[y_1, \dots, y_n]P, y, u) = id_{\sharp}^{i},
$$

$$
f_{can}^{\sharp}(x!^{j}[x_1, \dots, x_n]Q, x, u) = id_{\sharp}^{j},
$$

$$
\perp_1 \neq (\Pi_2(id_{\sharp}^j)) \cap_1 (\Pi_2(id_{\sharp}^l)),
$$

and we introduce

$$
id_{can} \triangleq (\Pi_2(id_{\sharp}^j)) \cap_1 (\Pi_2(id_{\sharp}^l)),
$$

$$
id_{pro}^{\gamma} \triangleq \Pi_1(id_{\sharp}^{\gamma} \cap_2 \mathrm{Inj}_2(id_{\mathrm{can}})),
$$

$$
id_{pro}^{l} \triangleq \Pi_{1}(id_{\sharp}^{l} \cap_{2} \mathrm{Inj}_{2}(id_{\mathrm{can}})),
$$

$$
id_k^t \triangleq \mathrel{\substack{\bowtie \\ \to}} ( \bowtie (id_{\sharp}^j, id_{\sharp}^l), f_{can}^{\sharp}(x!^j[x_1, \dots, x_n]Q, x_k, t) ) \cap_2 \mathrm{Inj}_1(id_{pro}^\gamma).
$$

Then we have

$$
(f_{pro}^{\sharp}, f_{can}^{\sharp}, f_{esc}^{\sharp}) \to (g_{pro}^{\sharp}, g_{can}^{\sharp}, \emptyset)
$$

$$
\text{where } g_{pro}^{\sharp} = \begin{cases} p \mapsto \mathrm{id}_{pro}^{\gamma} & \text{if } p \in (\mathrm{Agent}(P)) \\ q \mapsto \mathrm{id}_{pro}^{l} & \text{if } q \in (\mathrm{Agent}(Q)) \end{cases}
$$

and $g_{can}^{\sharp} =$

$$
\left\{
\begin{array}{ll}
(p, z, z) \mapsto \mathrm{dpush}(\mathrm{id}_{pro}^{\gamma}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ z \in \mathcal{BN}(P) \cap \mathcal{FN}(p) \\ z \notin \{y_i \mid i \in [|1; n|]\} \end{cases} \\[2ex]
(p, y_k, t) \mapsto id_k^t & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ y_k \in \mathcal{BN}(P) \cap \mathcal{FN}(p) \\ p \in (\mathrm{Agent}(P)) \end{cases} \\[2ex]
(p, z, t) \mapsto f_{can}^{\sharp}(y?^i[y_1, \dots, y_n]P, z, t) \cap_2 \mathrm{Inj}_1(\mathrm{id}_{pro}^{\gamma}) & \text{if } \begin{cases} z \in \mathcal{FN}(P) \cap \mathcal{FN}(p) \\ z \neq y \end{cases} \\[2ex]
(p, y, u) \mapsto f_{can}^{\sharp}(y?^i[y_1, \dots, y_n]P, y, u) \cap_2 \mathrm{Inj}_2(id_{can}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ y \in \mathcal{FN}(P) \cap \mathcal{FN}(p) \\ p \in (\mathrm{Agent}(Q)) \end{cases} \\[2ex]
(q, z, z) \mapsto \mathrm{dpush}(\mathrm{id}_{pro}^{l}) & \text{if } \begin{cases} z \in \mathcal{BN}(Q) \cap \mathcal{FN}(q) \\ q \in (\mathrm{Agent}(Q)) \end{cases} \\[2ex]
(q, z, t) \mapsto f_{can}^{\sharp}(x!^j[x_1, \dots, x_n]Q, z, t) \cap_2 \mathrm{Inj}_1(\mathrm{id}_{pro}^{l}) & \text{if } \begin{cases} z \in \mathcal{FN}(Q) \cap \mathcal{FN}(q) \\ z \neq x \end{cases} \\[2ex]
(q, x, u) \mapsto f_{can}^{\sharp}(x!^j[x_1, \dots, x_n]Q, x, u) \cap_2 \mathrm{Inj}_2(id_{can}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(Q)) \\ x \in \mathcal{FN}(Q) \cap \mathcal{FN}(q) \end{cases}
\end{array}
\right.
$$

<caption>Fig. 6. Abstract communication</caption>
Let $(f_{pro}^{\sharp}, f_{can}^{\sharp}, f_{esc}^{\sharp})$ be an abstract configuration,
we consider $u \in \mathcal{C}hannel$ and $*y?^i[y_1, ..., y_n]P, x!^j[x_1, ..., x_n]Q$ two sub-processes,
such that

$$
\begin{align*}
f_{can}^{\sharp}(*y?^i[y_1, \dots, y_n]P, y, u) &= id_{\sharp}^?, \\
f_{can}^{\sharp}(x!^j[x_1, \dots, x_n]Q, x, u) &= id_{\sharp}^t, \\
\bot_1 \neq (\Pi_2(id_{\sharp}^?)) \cap \Pi_1(\Pi_2(id_{\sharp}^t)),
\end{align*}
$$

and we introduce

$$
\begin{align*}
id_{can} &\triangleq (\Pi_2(id_{\sharp}^?)) \cap_1 (\Pi_2(id_{\sharp}^t)), \\
id_{pro}^{?} &\triangleq \Pi_1(id_{\sharp}^? \cap_2 \mathrm{Inj}_2(id_{can})), \\
id_{pro}^{t} &\triangleq \Pi_1(id_{\sharp}^{t} \cap_2 \mathrm{Inj}_2(id_{can})), \\
id_{s,t} &\triangleq \mathrm{Inj}_1(id_{pro}^{t}) \cap_2 \mathrel{\substack{\bowtie \\ \to}} (\bowtie (id_{\sharp}^{t}, id_{\sharp}^{?}), f_{can}^{\sharp}(y?^i[y_1, \dots, y_n]P, s, t)), \\
id_{k}^{t} &\triangleq f_{can}^{\sharp}(x!^j[x_1, \dots, x_n]Q, x_k, t).
\end{align*}
$$

Then we have

$$
(f_{pro}^{\sharp}, f_{can}^{\sharp}, f_{esc}^{\sharp}) \to (g_{pro}^{\sharp}, g_{can}^{\sharp}, \emptyset)
$$

$$
\text{where } g_{pro}^{\sharp} = \begin{cases} p \mapsto \text{idpro}^{?} & | \ p \in (\text{Agent}(P)) \\ q \mapsto \text{idpro}^{t} & | \ q \in (\text{Agent}(Q)) \end{cases}
$$

and $g_{can}^{\sharp} =$

$$
\[
\left\{
\begin{array}{ll}
(p, z, z) \mapsto \mathrm{dpush}(\mathrm{push}_1^{(i,j)}(\mathrm{idpro}^?, \mathrm{idpro}^!)) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ z \in \mathcal{BN}(P) \cap \mathcal{FN}(p) \\ z \notin \{y_i \mid i \in [|1; n|]\} \end{cases} \\[2ex]
(p, y_k, t) \mapsto \mathrm{push}_2^{(i,j)}(\mathrm{idpro}^?, \mathrm{id}_k^t) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ y_k \in \mathcal{BN}(P) \cap \mathcal{FN}(p) \\ p \in (\mathrm{Agent}(P)) \end{cases} \\[2ex]
(p, z, t) \mapsto \mathrm{push}_2^{(i,j)}(\mathrm{idpro}^?, \mathrm{id}_{z,t}) & \text{if } \begin{cases} z \in \mathcal{FN}(P) \cap \mathcal{FN}(p) \\ z \neq y \end{cases} \\[2ex]
(p, y, u) \mapsto \mathrm{push}_2^{(i,j)}(\mathrm{idpro}^?, \mathrm{id}_{y,u}) \cap_2 \mathrm{Inj}_2(\mathrm{id}_{can}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ y \in \mathcal{FN}(P) \cap \mathcal{FN}(p) \\ q \in (\mathrm{Agent}(Q)) \end{cases} \\[2ex]
(q, z, z) \mapsto \mathrm{dpush}(\mathrm{idpro}^!) & \text{if } \begin{cases} q \in (\mathrm{Agent}(Q)) \\ z \in \mathcal{BN}(Q) \cap \mathcal{FN}(q) \\ q \in (\mathrm{Agent}(Q)) \end{cases} \\[2ex]
(q, z, t) \mapsto f_{can}^{\sharp}(x!^j[x_1, \dots, x_n]Q, z, t) \cap_2 \mathrm{Inj}_1(\mathrm{idpro}^!) & \text{if } \begin{cases} z \in \mathcal{FN}(Q) \cap \mathcal{FN}(q) \\ z \neq x \end{cases} \\[2ex]
(q, x, u) \mapsto f_{can}^{\sharp}(x!^j[x_1, \dots, x_n]Q, x, u) \cap_2 \mathrm{Inj}_2(\mathrm{id}_{can}) & \text{if } \begin{cases} q \in (\mathrm{Agent}(Q)) \\ x \in \mathcal{FN}(Q) \cap \mathcal{FN}(q) \end{cases}
\end{array}
\right.
\]
$$

<caption>**Fig. 7.** Abstract resource fetching</caption>
Let $(f_{pro}^{\sharp}, f_{can}^{\sharp}, f_{esc}^{\sharp})$ be an abstract configuration,

we consider $u \in \mathcal{C}hannel$ and $x!^j[x_1, \dots, x_n]Q$ a sub-process, such that

$$f_{can}^{\sharp}(x!^j[x_1, \dots, x_n]Q, x, u) = id_{\sharp}^1, \\ \perp_1 \neq (f_{esc}^{\sharp}(u)) \cap_1 (\Pi_2(id_{\sharp}^2)),$$

and we introduce

$$id_{can} \triangleq (f_{esc}^{\sharp}(u)) \cap_1 (\Pi_2(id_{\sharp}^1)),$$

$$id_{pro}^{\prime} \triangleq \Pi_1(id_{\sharp}^{1} \cap_2 \mathrm{Inj}_2(id_{can})) .$$

Then we have $(f_{pro}^{\sharp}, f_{can}^{\sharp}, f_{esc}^{\sharp}) \to (g_{pro}^{\sharp}, g_{can}^{\sharp}, g_{esc}^{\sharp})$

where

$$g_{pro}^{\sharp} = \{q \mapsto id_{pro}^{\prime} \text{ if } q \in (\mathrm{Agent}(Q))\},$$

$$g_{can}^{\sharp} =$$

$$\left\{
\begin{array}{ll}
(q, z, z) \mapsto \mathrm{dpush}(id_{pro}^{\prime}) & \text{if } \begin{cases} q \in (\mathrm{Agent}(Q)) \\ z \in \mathcal{BN}(Q) \cap \mathcal{FN}(q) \end{cases} \\[2ex]
(q, z, t) \mapsto f_{can}^{\sharp}(x!^i[x_1, \dots, x_n]Q, z, t) \cap_2 \mathrm{Inj}_1(id_{pro}^{\prime}) & \text{if } \begin{cases} q \in (\mathrm{Agent}(Q)) \\ z \in \mathcal{FN}(Q) \cap \mathcal{FN}(q) \\ z \neq x \end{cases} \\[2ex]
(q, x, u) \mapsto f_{can}^{\sharp}(x!^i[x_1, \dots, x_n]Q, x, u) \cap_2 \mathrm{Inj}_2(id_{can}) & \text{if } \begin{cases} q \in (\mathrm{Agent}(Q)) \\ x \in \mathcal{FN}(Q) \cap \mathcal{FN}(q), \end{cases}
\end{array}
\right.
$$
$$g_{esc}^{\sharp} = \{t \mapsto \Pi_2(f_{can}^{\sharp}(Q, x_k, t) \cap_2 \mathrm{Inj}_1(id_{pro}^{\prime})), \forall k \in [|1; n|].$$

<caption>**Fig. 8.** Abstract spied communication</caption>

Let $(f_{pro}^{\sharp}, f_{can}^{\sharp}, f_{esc}^{\sharp})$ be an abstract configuration,

we consider $u \in \mathcal{C}hannel$ and $y?^i[y_1, \dots, y_n]P$ a sub-process, such that

$$f_{can}^{\sharp}(y?^i[y_1, \dots, y_n]P, y, u) = id_{\sharp}^2, \\ \perp_1 \neq (f_{esc}^{\sharp}(u)) \cap_1 (\Pi_2(id_{\sharp}^3)),$$

and we introduce

$$id_{can} \triangleq (f_{esc}^{\sharp}(u)) \cap_1 (\Pi_2(id_{\sharp}^2)),$$

$$id_{pro}^{\prime} \triangleq \Pi_1(id_{\sharp}^{2} \cap_2 \mathrm{Inj}_2(id_{can})) .$$

Then we have $(f_{pro}^{\sharp}, f_{can}^{\sharp}, f_{esc}^{\sharp}) \to (g_{pro}^{\sharp}, g_{can}^{\sharp}, \emptyset)$

where

$$g_{pro}^{\sharp} = \{p \mapsto id_{pro}^{\prime} \text{ if } p \in (\mathrm{Agent}(P))\},$$

$$g_{can}^{\sharp} =$$

$$\left\{
\begin{array}{ll}
(p, z, z) \mapsto \mathrm{dpush}(id_{pro}^{\prime}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ z \in \mathcal{BN}(P) \cap \mathcal{FN}(p) \\ z \notin \{y_i \mid i \in [|1; n|]\} \end{cases} \\[2ex]
(p, z, t) \mapsto f_{can}^{\sharp}(y?^i[y_1, \dots, y_n]Q, z, t) \cap_2 \mathrm{Inj}_1(id_{pro}^{\prime}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ z \in \mathcal{FN}(P) \cap \mathcal{FN}(p) \\ z \neq y \end{cases} \\[2ex]
(p, y, u) \mapsto f_{can}^{\sharp}(y?^i[y_1, \dots, y_n]P, y, u) \cap_2 \mathrm{Inj}_2(id_{can}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ y \in \mathcal{FN}(P) \cap \mathcal{FN}(p) \end{cases} \\[2ex]
(p, y_k, t) \mapsto (\mathrm{Inj}_1(id_{pro}^{\prime}) \cap_2 \mathrm{Inj}_2(f_{esc}^{\sharp}(t))) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ y_k \in \mathcal{BN}(P) \cap \mathcal{FN}(p). \end{cases}
\end{array}
\right.
$$

<caption>**Fig. 9.** Abstract spoilt communication</caption>
Let $(f_{pro}^\sharp, f_{can}^\sharp, f_{esc}^\sharp)$ be an abstract configuration,
we consider $u \in \text{Channel}$ and $*y?^i[y_1, \dots, y_n]P$ a sub-process, such that
$f_{can}^\sharp(*y?^i[y_1, \dots, y_n]P, y, u) = id_\sharp$
$\perp_1 \neq (\Pi_2(id_\sharp^?)) \cap_1 (f_{esc}^\sharp(u)),$

and we introduce

$$
id_{can} \triangleq (\Pi_2(id_{\sharp}^?)) \cap_1 (f_{esc}^{\sharp}(u)),
$$

$$
id_{pro}^{?} \triangleq \Pi_1(id_{\sharp}^{?} \cap_2 \mathrm{Inj}_2(id_{\mathrm{can}})),
$$

$$
id_{pro}^{*} \triangleq \mathrm{push}_{1}^{(i, \mathrm{cont}_{1})}(id_{pro}^{?}, t^{?}),
$$

$$
id_{s,t} \triangleq \mathrm{Inj}_1(t^?) \cap_2 \mathrm{Inj}_2(\Pi_2(f_{can}^\sharp(y?^i[y_1, \dots, y_n]P, s, t) \cap_2 \mathrm{Inj}_1(id_{pro}^?))).
$$

Then we have $(f_{pro}^{\sharp}, f_{can}^{\sharp}, f_{esc}^{\sharp}) \to (g_{pro}^{\sharp}, g_{can}^{\sharp}, \emptyset)$

$$
\text{where } g_{pro}^{\sharp} = \{ p \mapsto id_{pro}^{*} \mid p \in (\text{Agent}(P)) \}
$$

and

$g_{can}^{\sharp} =$

$$
\[
g_{can}^{\sharp} =
\begin{cases}
(p, z, z) \mapsto \mathrm{dpush}(id_{pro}^{*}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ z \in \mathcal{BN}(P) \cap \mathcal{FN}(p) \\ z \notin \{y_i \mid i \in [|1; n|]\} \end{cases} \\[2ex]
(p, y_k, t) \mapsto \mathrm{Inj}_1(id_{pro}^{*}) \cap_2 \mathrm{Inj}_2(f_{esc}^{\sharp}(t)) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ y_k \in \mathcal{BN}(P) \cap \mathcal{FN}(p) \end{cases} \\[2ex]
(p, z, t) \mapsto \mathrm{push}_2^{(i, \mathrm{cont}_1)}(id_{pro}^{?}, id_{z,t}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ z \in \mathcal{FN}(P) \cap \mathcal{FN}(p) \\ z \neq y \end{cases} \\[2ex]
(p, y, u) \mapsto \mathrm{push}_2^{(i, \mathrm{cont}_1)}(id_{pro}^{?}, id_{y,u}) \cap_2 \mathrm{Inj}_2(id_{can}) & \text{if } \begin{cases} p \in (\mathrm{Agent}(P)) \\ y \in \mathcal{FN}(P) \cap \mathcal{FN}(p). \end{cases}
\end{cases}
\]
$$

<caption>Fig. 10. Abstract spoilt resource fetching</caption>

6 Abstract Domains

Many domains can be used to instantiate the parametric domains $Id_1^\sharp$ and $Id_2^\sharp$
and their associated primitives, depending on which complexity and which level
of accuracy we expect. We have explained in [13, Sect. 6.1] that an unexpensive
uniform analysis can be obtained by instantiating both $Id_1^\sharp$ and $Id_2^\sharp$ with the
lattice $\{\bot, \top\}$ with the following concretization functions:

$$
\gamma_1 : \begin{cases} \bot \mapsto \emptyset \\ \top \mapsto \mathrm{Id} \end{cases} \quad \text{and} \quad \gamma_2 : \begin{cases} \bot \mapsto \emptyset \\ \top \mapsto \mathrm{Id} \times \mathrm{Id} \end{cases} .
$$

For the sake of comparison, this analysis is at least as accurate as the one of
Nielson et al. [3] and takes into account unreachable code.

Non-uniform analyses [6,22] are much more expensive. We obtain an accu-
rate analysis by using the reduced product of both a non relational domain
$Id_1^{un}$ (resp. $Id_2^{un}$) and a relational domain $Id_1^{rel}$ (resp. $Id_2^{rel}$) to represent sets of
*Example 3.* Our analysis may be used in proving the confidentiality of our ftp server. We denote by $C^{\#} = (f_{pro}^{\#}, f_{can}^{\#}, f_{esc}^{\#})$ the result of our analysis. $f_{can}^{\#}$ is given in Fig. 11 while $f_{esc}^{\#}$ maps each channel to $\perp_1$. These results are precise enough to prove that channels *data* (resp. *email*) can be passed only to channels *info* (resp. *add*), and cannot be listened to by any processes of an unknown context. Furthermore, using theorem 3, we can conclude that anytime a process 4 is spawned, its free channels are bound to channels created by the same recursive instance of resource 3. □

# 7 Conclusion

We have designed a powerful non-standard semantics, which is able to describe the behaviour of any mobile system expressed in the $\pi$-calculus, while tracing precisely the origin of channels. Moreover, our abstraction allows to analyze the behaviour of a part of a system whatever its context may be, which has many applications, such as analyzing a system part by part or analyzing the security of a known system inside a hostile context.

We have approximated this non-standard semantics into an abstract one, which focuses on confidentiality properties. We have obtained results which have at least the same level of accuracy than those obtained on the *friendly systems* [22], while our semantics works on the full $\pi$-calculus and can be applied to open mobile system. Analyzing a system part by part may lead to more accurate results than analyzing a complete system, especially while detecting mutual exclusion [13].

# References

1. Martin Abadi. Secrecy by typing in security protocol. In Proc. 5th FPCA, volume 523 of Lecture Notes in Computer Science, pages 427–447. Springer-Verlag, 1991.

2. G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96:217–248, 1992.

3. C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Control flow analysis for the $\pi$-calculus. In Proc. CONCUR '98, number 1466 in Lecture Notes in Computer Science, pages 84–98. Springer-Verlag, 1998.

4. C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Static analysis of processes for no read-up and no write-down. In Proc. FOSSACS '99, number 1578 in Lecture Notes in Computer Science, pages 120–134. Springer-Verlag, 1999.

5. L. Cardelli and A. D. Gordon. Mobile ambients. In Foundations of Software Science and Computational Structures, volume 1378 of Lecture Notes in Computer Science, pages 140–155. Springer, 1998.

6. C. Colby. Analyzing the communication topology of concurrent programs. In Symposium on Partial Evaluation and Program Manipulation, 1995.

7. P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303–342. Prentice-Hall, Inc., Englewood Cliffs, 1981.
$$
\left\{
\begin{array}{ll}
(1, \text{port, port}) & \mapsto ((\varepsilon, \varepsilon), \{x_{\lambda} = y_{\lambda} = 0, \forall \lambda \in \Sigma\}) \\
(2, \text{add, email}) & \mapsto \left\{
\begin{array}{l}
((1, 4)(3, 5) * (3, 6), (3, 5) * (3, 6)), \\
y_{\lambda} = x_{\lambda}, \forall \lambda \in \Sigma \setminus \{(1, 4)\} \\
x_{\lambda} = 0, \forall \lambda \in \Sigma \setminus \{(1, 4); (3, 5); (3, 6)\} \\
x_{(3,6)} = x_{(1,4)} = 1 \\
y_{(1,4)} = 0
\end{array}
\right\} \\
(2, \text{info, data}) & \mapsto \left\{
\begin{array}{l}
((1, 4)(3, 5) * (3, 6), (3, 5) * (3, 6)), \\
y_{\lambda} = x_{\lambda}, \forall \lambda \in \Sigma \setminus \{(1, 4)\} \\
x_{\lambda} = 0, \forall \lambda \in \Sigma \setminus \{(1, 4); (3, 5); (3, 6)\} \\
x_{(3,6)} = x_{(1,4)} = 1 \\
y_{(1,4)} = 0
\end{array}
\right\} \\
(3, \text{port, port}) & \mapsto ((\varepsilon, \varepsilon), \{x_{\lambda} = y_{\lambda} = 0, \forall \lambda \in \Sigma\}) \\
(3, \text{gen, gen}) & \mapsto ((\varepsilon, \varepsilon), \{x_{\lambda} = y_{\lambda} = 0, \forall \lambda \in \Sigma\}) \\
(4, \text{port, port}) & \mapsto \left\{
\begin{array}{l}
((3, 5) * (3, 6), \varepsilon), \\
y_{\lambda} = 0, \forall \lambda \in \Sigma \\
x_{\lambda} = 0, \forall \lambda \in \Sigma \setminus \{(3, 5); (3, 6)\} \\
x_{(3,6)} = 1
\end{array}
\right\} \\
(4, \text{email, email}) & \mapsto \left\{
\begin{array}{l}
((3, 5) * (3, 6), (3, 5) * (3, 6)), \\
y_{\lambda} = x_{\lambda}, \forall \lambda \in \Sigma \\
x_{\lambda} = 0, \forall \lambda \in \Sigma \setminus \{(3, 5); (3, 6)\} \\
x_{(3,6)} = 1
\end{array}
\right\} \\
(4, \text{data, data}) & \mapsto \left\{
\begin{array}{l}
((3, 5) * (3, 6), (3, 5) * (3, 6)), \\
y_{\lambda} = x_{\lambda}, \forall \lambda \in \Sigma \\
x_{\lambda} = 0, \forall \lambda \in \Sigma \setminus \{(3, 5); (3, 6)\} \\
x_{(3,6)} = 1
\end{array}
\right\} \\
(5, \text{gen, gen}) & \mapsto \left\{
\begin{array}{l}
(3, 5) * (3, 6), \varepsilon, \\
y_{\lambda} = 0, \forall \lambda \in \Sigma \\
x_{\lambda} = 0, \forall \lambda \in \Sigma \setminus \{(3, 5); (3, 6)\} \\
x_{(3,6)} = 1
\end{array}
\right\} \\
(6, \text{gen, gen}) & \mapsto ((\varepsilon, \varepsilon), \{x_{\lambda} = y_{\lambda} = 0, \forall \lambda \in \Sigma\})
\end{array}
\right.
$$

<caption>Fig. 11. $f_{can}^{\#}$: the ftp server analysis</caption>
8. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *Conference Record of the Fourth ACM Symposium on Principles of Programming Languages*, pages 238–252, Los Angeles, California, U.S.A., 1977.

9. P. Cousot and R. Cousot. Abstract interpretation frameworks. *Journal of logic and computation*, 2(4):511–547, August 1992.

10. P. Cousot and R. Cousot. Comparing the Galois connection and widening--narrowing approaches to abstract interpretation. In *Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, PLILP'92*, volume 631 of *Lecture Notes in Computer Science*, pages 269–295. Springer-Verlag, 1992.

11. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In *Proceedings of the Fifth Conference on Principles of Programming Languages*. ACM Press, 1978.

12. A. Deutsch. A storeless model of aliasing and its abstraction using finite representations of right-regular equivalence relations. In *Proceedings of the 1992 International Conference on Computer Languages*, pages 2–13. IEEE Computer Society Press, Los Alamitos, California, U.S.A., 1992.

13. J. Feret. Conception de π-sa : un analyseur statique générique pour le π-calcul. Mémoire de dea, SPP, september 1999. Electronically available at http://www.di.ens.fr/feret/dea.html.

14. P. Granger. Static analysis of linear congruence equalities among variables of a program. In *TAPSOFT'91*, volume 493. Lecture Notes in Computer Science, 1991.

15. Matthew Hennessy and James Riely. Resource access control in systems of mobile agents. In U. Nestmann and B. Pierce, editors, *3rd International Workshop on High-Level Concurrent Languages (HLCL'98)*, volume 16(3) of *Electronic Notes in Theoretical Computer Science*, Nice, September 1998. Elsevier. Available from http://www.elsevier.nl/locate/entcs. Full version available as Sussex CSTR 98/02, 1998. Available from http://www.cogs.susx.ac.uk/.

16. K. Honda, V. Vasconcelos, and N. Yoshida. Secure information flow as types process behaviour. In *Proc. ESOP'00*, number 1782 in Lecture Notes in Computer Science. Springer-Verlag, 2000.

17. M. Karr. Affine relationships among variables of a program. *Acta Informatica*, pages 133–151, 1976.

18. R. Milner. The polyadic π-calculus: a tutorial. In *Proceedings of the International Summer School on Logic and Algebra of Specification*. Springer Verlag, 1991.

19. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. *Information and Computation*, 100:1–77, 1992.

20. James Riely and Matthew Hennessy. Secure resource access for mobile agents. Draft. Available from http://www.depaul.edu/~jriely, June 1999.

21. D. N. Turner. *The Polymorphic Pi-Calculus: Theory and Implementation*. PhD thesis, Edinburgh University, 1995.

22. A. Venet. Automatic determination of communication topologies in mobile systems. In *Proceedings of the Fifth International Static Analysis Symposium SAS'98*, volume 1503 of *Lecture Notes in Computer Science*, pages 152–167. Springer-Verlag, 1998.