A Process Calculus for Universal Concurrent Constraint Programming: Semantics, Logic and Application Carlos Olarte LIX, Ecole Polytechnique Paris France Editor: Frank Valencia Download: PDF Abstract: We introduce the Universal Timed Concurrent Constraint Programming (utcc) process calculus; a generalisation of Timed Concurrent Constraint Programming. The utcc calculus allows for the specification of mobile behaviours in the sense of Milner's $\pi$-calculus: Generation and communication of private links. We first endow utcc with an operational semantics and then with a symbolic semantics to deal with problematic operational aspects involving infinitely many substitutions and divergent internal computations. The novelty of the symbolic semantics is to use temporal constraints to represent finitely infinitely-many substitutions. We also show that utcc has a strong connection with Pnueli's Temporal Logic. This connection can be used to prove reachability properties of processes. As a compelling example, we use utcc to exhibit the secrecy flaw of the Needham-Schroeder security protocol. Introduction Process calculi treat concurrent processes much like the $\lambda$-calculus treat computable functions. They provide a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. Concurrent Constraint Programming (CCP) [17] is a process calculus which combines the traditional operational view of process calculi with a declarative one based upon logic. This combination allows CCP to benefit from the large body of techniques of both process calculi and logic. In fact, CCP has successfully been used in the modelling of several concurrent scenarios: E.g., Biological, Timed, Reactive and Stochastic systems [19]. Nevertheless, the basic CCP lacks a mechanism to specify generation and communication of private links; i.e. mobility as usually understood in concurrency theory. Such mechanism is fundamental for the specification of systems where agents change their communication structure (mobile systems) as well as protocols where nonces (i.e, randomly-generated unguessable items) are transmitted. In fact, generation and communication of private links are the central operations of one of the main representative formalisms for mobility in concurrency theory, namely the $\pi$-calculus [11]. We aim at extending CCP to specify mobility. The extension ought to comply with two criteria that distinguish basic CCP from other formalisms: (1) Logic correspondence which provides CCP with a unique declarative view of processes and (2) determinism which is the source of CCP's elegant and simple characterisations (e.g., the clousure operator semantics [17]). Another general criterion for our extension is (3) to be applicable to meaningful concurrent scenarios, in particular those not yet explored using CCP calculi. Agents in CCP interact with each other by telling and asking information represented as constraints in a global store. The process tell(c) adds the constraint $c$ to the store and the ask process when c do P executes $P$ if c is entailed by the store. The process $\localp{x;c}{P}$ declares a private variable $x$ for $P$ constrained by $c$ and $P\parallel Q$ stands for the parallel execution of P and Q. The computations of processes are deterministic in that the final store is always the same regardless of the execution order of parallel components. Mobility can be modelled by adding linear parametric ask processes to CCP as done in Linear CCP [6]. A parametric ask A(x) can be viewed as a process when c do P with a variable x declared as a formal parameter. Intuitively, A(x) may evolve into P[y/x], i.e. $P$ with x replaced by y, if c[y/x] is entailed by the store. Mobility is exhibited when y is a private variable (link) from some other process. This extension, however, does not adhere to Criterion (2), i.e. it is non-deterministic: If both c[y/x] and c[z/x] are entailed by the store, A(x) may evolve to either P[y/x] or P[z/x]. The above kind of non-determinism can be avoided by extending CCP only with persistent parametric asks following the semantics of the persistent $\pi$-calculus in [14]. The idea is that if both $c[y/x]$ and $c[z/x]$ are entailed by the store, a persistent $A(x)$ evolves into $A(x) \parallel P[y/x] \parallel P[z/x]$. Forcing every ask to be persistent, however, makes the extension not suitable for modelling typical scenarios where a process stops after performing its query (e.g., web-services requests). Our strategy is therefore to extend CCP with temporary parametric ask operations. Intuitively, these operations behave as persistent parametric asks during a time-interval but may disappear afterwards. We do this by generalising the timed CCP model in [16]. We call this extension Universal Timed CCP (utcc). As explained below, we shall show that complies with previously-mentioned criteria (1-3). Contributions. We first give utcc an operational semantics. However, parametric ask operations pose technical problems: They may generate infinitely many substitutions thus causing divergent (i.e., infinite) internal computations. We resolve this problem by endowing utcc with a novel symbolic semantics that uses temporal constraints to represent finitely a possible infinite number substitutions. We then show that allows for mobility and it is deterministic (Criterion 2). We shall show a strong correspondence with Linear-Time Temporal Logic (LTL) by providing a compositional encoding of utcc processes into LTL formulae (Criterion 1). This correspondence with the standard logic for the verification of concurrent systems allows for reachability analysis central to security protocols: If there is a way to reach a state where an intruder knows a secret, then there is a secrecy breach. To illustrate the applicability of (Criterion 3), we use it to model and predict the secrecy flaw in the well-known Needham-Schroeder Protocol [9]. To the our knowledge this is the first symbolic semantics for a CCP calculus as well as the first one in concurrency theory using temporal constraints as finite representations of substitutions. Furthermore, we are not aware of any other work applying a CCP calculus to model security protocols. Preliminaries In this section we describe the temporal concurrent constraint () model [16] following the presentation in [19]. CCP calculi are parametric in a constraint system (). A cs can be represented as a pair where is a signature of function and predicate symbols, and is a first-order theory over $\Sigma$. Given a , let be its underlying first-order language with variables x,y,..., and logic symbols . Constraints c,d,... are formulae over $\cL.$ We say that c entails d in , written , iff (i.e., iff $c {\imply} d$ is true in all models of ). We shall omit "$\Delta$" in $\entails_{\Delta}$ when no confusion arises. For operational reasons $\entails$ is often required to be decidable. We use $\vec{t}$ for a sequence of terms $t_1,\ldots,t_n$ with length $\vert \vec{t} \vert=n.$ If $\vert\vec{t} \vert= 0$ then $\vec{t}$ is written as $\epsilon$. We use $c[\vec{t}/\vec{x}]$, where $\vert\vec{t}\vert=\vert\vec{x}\vert$ and $x_i$'s are pairwise distinct, to denote c with the free occurrences of xi replaced with ti. The substitution [t/x] will be similarly applied to other syntactic entities. The calculus extends for timed systems [16]. Time is conceptually divided into time intervals (or time units). In a particular time interval, a process P gets an input c from the environment, it executes with this input as the initial store, and when it reaches its resting point, it outputs the resulting store d to the environment. The resting point determines a residual process Q which is then executed in the next time interval. The resulting store d is not automatically transferred to the next time interval.  Definition 1: Processes P, Q, ... in tcc are built from constraints in the underlying cs by the following syntax: P,Q :== skip | tell(c) | when c do P | P||Q  | (local x; c)P | next P | unless c next P | !P with the variables in x being pairwise distinct.   The process skip does nothing and tell(c) adds c to the store in the current time interval. If in the current time interval c can eventually be derived from the store, when c do P evolves into P within the same time interval. Otherwise when c do P evolves into skip. P||Q denotes P and Q running in parallel during the current time interval and (local x; c)P binds x in P by declaring it private to P under a constraint c. The bound variables bv(Q) (free variables fv(Q)) are those with a bound (a not bound) occurrence in Q. We write (local x)P as short for  (local x; true)P The unit-delay executes $P$ in the next time interval. The time-out is also an unit-delay, but is executed in the next time unit iff is not entailed by the final store at the current time interval. We use as short for , with repeated $n$ times. Finally, the replication means , i.e., unboundly many copies of but one at a time. Universal Timed cc In [16] it is shown that processes are finite-state. This means it cannot be used to describe infinite-state behaviours like those arising from mobility which is one of the main concerns in this paper. Mobility is understood in the sense of the $\pi$-calculus, i.e, communication of private variables (or links). In this section we introduce an extension to which by following a logic approach it provides for mobile behaviour. We call this extension Universal tcc (utcc). Abstractions To model mobile behaviour, replaces the tcc ask operation when c do P with a more general parametric ask construction, namely $\absp{\vec{x}}{c}{P}$. This process can be viewed as a $\lambda$-abstraction of the process $P$ on the variables $\vec{x}$ under the constraint (or with the guard) $c$. From a programming language perspective, $\vec{x}$ in $\localp{\vec{x};c}{P}$ can be viewed as the local variables of $P$ while $\vec{x}$ in $\absp{\vec{x}}{c}{P}$ can be viewed as the formal parameters of $P.$ From a logic perspective we shall show that the new binder has a pleasant duality with the local operator: The processes $\localp{\vec{x};c}{P}$ and $\absp{\vec{x}}{c}{P}$ correspond, resp., to the existential and universal formulae $\exists \vec{x} (c \wedge F_P)$ and $\forall \vec{x} (c \imply F_P)$ where $F_P$ corresponds to $P$. Definition 2 (utcc Processes). The utcc processes result from replacing in the syntax in Definition 1 the expression when c do P with (abs x; c)P with the variables in x being pairwise distinct.   Intuitively, $Q=\absp{\vec{x}}{c}{P}$ performs $P[\vec{t}/\vec{x}]$ in the current time interval for all the terms $\vec{t}$ $c[\vec{t}/\vec{x}]$ is entailed by the store. $Q$ binds the variables $\vec{x}$ in $P$ and $c$. Sets (.) and (.), are extended accordingly. Furthermore $Q$ evolves into $\skipp$ at the end of the time unit. We shall use $\whenp{c}{P}$ for the "empty" abstraction $\absp{\epsilon}{c}{P}.$ Mobile links. We conclude this section with a little example illustrating how mobility is obtained from the interplay between abstractions and local processes.    Operational Semantics (SOS) The structural operational semantics (SOS) of considers transitions between process-store configurations with stores represented as constraints and processes quotiented by $\equiv$. We use $\gamma,\gamma',\ldots$ to range over configurations. The SOS transitions are given by the relations $\redi$ and $\Longrightarrow$ in Table 1. The internal transition should be read as `` with store reduces, in one internal step, to with store ''. The observable transition should be read as `` on input , reduces in one time unit to and outputs ''. The observable transitions are obtained from finite sequences of internal transitions. Table 1: Internal and observable reductions. $\equiv$ and $F$ are given in Definitions 3 and 4. In $\rAbs$, $\vec{x} \neq \vec{t}$ denotes $\bigvee_{1\leq i \leq \vert\vec{x}\vert}x_i\neq t_i$. If $\vert\vec{x}\vert=0$, $\vec{x} \neq \vec{t}$ is defined as $\false$. $\begin{array}{l} \rightinfer[\rTell]{\left\langle \tellp{c},d\right\rangle \:... ...} \left\langle Q,d\right\rangle \: \notredi_{{}} {} } \\ \\ \end{array}$ We only describe some of the rules in Table 1. The other rules are standard, easily seen to realise the operational intuitions given above (see [19] for further details). As clarified below, the seemingly missing rules for ``next'' and ``unless'' processes are given by $\rObserv$. We dwell a little upon the description of Rule $\rLocal$ as it may seem somewhat complex. Consider $Q = \localp{x;c}{P}$ in Rule $\rLocal$. The global store is $d$ and the local store is $c$. We distinguish between the external (corresponding to $Q$) and the internal point of view (corresponding to $P$). From the internal point of view, the information about , possibly appearing in the ``global'' store , cannot be observed. Thus, before reducing $P$ we first hide the information about that may have in $d$ by existentially quantifying in . Similarly, from the external point of view, the observable information about $x$ that the reduction of internal agent $P$ may produce (i.e., ) cannot be observed. Thus we hide it by existentially quantifying $x$ in $c'$ before adding it to the global store. Additionally, we make $c'$ the new private store of the evolution of the internal process. Rule ${\rAbs}$ describes the behaviour of $\absp{\vec{x}}{c}{P}$. If the store entails $c[\vec{t}/\vec{x}]$ then $P[\vec{t}/\vec{x}]$ is executed. Additionally, the abstraction persists in the current time interval to allow other potential replacements of $\vec{x}$ in $P$ but $c$ is augmented with $x_i \neq t_i$ to avoid executing $P[\vec{t}/\vec{x}]$ again. Rule $\rObserv$ says that an observable transition from labelled with $(c,d)$ is obtained from a terminating sequence of internal transitions from $\left\langle P, c\right\rangle$ to a . The process $R$ to be executed in the next time interval is equivalent to (the ``future'' of $Q$). $F(Q)$ is obtained by removing from abstractions and any local information which has been stored in $Q$, and by ``unfolding'' the sub-terms within ``next'' and ``unless'' expressions. We can now illustrate the observable transition showing the expected behaviour in our mobility example. Infinite behaviour within time-units Due to abstractions the SOS may induce an infinite sequence of internal transitions within a time interval thus never producing an observable transition. Abstraction Loops. One source of infinite internal behaviour involves looping (recursion) in abstractions. E.g. let $R=\absp{x}{\outp_1(x)}{ \localp{z}{\tellp{\outp_1(z)}})}$. Each time $R$ gets a link on $\outp_1$, it generates a new link $z$ on $\outp_1$ thus causing infinite internal behaviour. (A similar problem involves several abstractions producing mutual recursive behaviour.) This kind of looping problems can be avoided by requiring for each $\absp{x}{c}{P}$ that $P$ must be a ``next'' expression. This restriction, however, may also disallow behaviour which will not cause infinite internal computations. Infinitely Many Substitutions. Another source of infinite internal behaviour involves the cs under consideration. Let $R=\absp{x}{c}{P}.$ If the current store $d$ entails $c[t/x]$ for infinitely many $t$'s, then $R$ will have to produce $P[t/x]$ for each such $t$. This kind of infinite internal behaviour can be avoided by allowing only guards $c$ so that for any $d$ the set $\{ t \vert d \entails c[t/x] \}$ modulo logic equivalence is finite. This seems inconvenient for the modelling of cryptographic knowledge as typically is done in process calculi: The presence of some messages entails the presence of arbitrary compositions among them. We discuss this at length in our security application in Section 6. Symbolic Semantics In this section we define a symbolic semantics for utcc whose basic idea is to use temporal constraints to represent in a finite way a possibly infinite number of substitutions as well as the information that an infinite loop may provide. It turns out that without appealing to the syntactic restrictions mentioned above, this semantics guarantees that every sequence of internal transitions is finite. Symbolic Intuitions Before defining the symbolic semantics let us give some intuitions of its basic principles. A. Substitutions as Constraints. Take $R=\absp{x}{c}{P}.$ The operational semantics performs $P[t/x]$ for every $t$ $c[t/x]$ is entailed by the store $d.$ Instead, the symbolic semantics dictates that $R$ should produce $e= d \wedge \forall x (c \imply d')$ where, similarly, $d'$ should be produced according to the symbolic semantics by $P$. Let $t$ be an arbitrary term $d \entails c[t/x].$ The idea is that if $e'$ is operationally produced by $P[t/x]$ then $e'$ should be entailed by $d'[t/x]$. Since $d\entails c[t/x]$ then $e \entails d'[t/x] \entails e'.$ Therefore $e$ entails the constraint that any arbitrary $P[t/x]$ produces. B. Timed Dependencies in Substitutions. The symbolic semantics represents as temporal constraints dependencies between substitutions from one time interval to another. E.g., suppose that for $R$ above, $P=\nextp{\tellp{e}}$. Operationally, once we move to the next time unit, the constraints produced are of the form $e[t/x]$ for those $t$'s the final store $d$ in the previous time unit entails $c[t/x]$. The symbolic semantics captures this as $e'=(\past d) \wedge \forall x ((\past c) \imply e)$ where $\past$ is the "previous" modality in temporal logic. Intuitively, $\past c'$ means that $c'$ holds in the previous time interval. Temporal Formulae and Constraints We shall use (a fragment of) the standard Linear-Time Temporal Logic (LTL) in [10] for our symbolic semantics. The modalities $\past F,\nextt F$ and $\always F$ state, resp., that $F$ holds previously, next and always. We use $\forall x F$ for $\neg \exists x \neg F$, and the eventual modality $\sometime F$ as an abbreviation of $\neg \always \neg F$. We presuppose the reader is familiar with the basic concepts of Model Theory. The non-logical symbols of $\cL$ are given meaning in an underlying $\cL$-structure, or $\cL$-model, $\cM(\cL)=(\cI,\cD).$ (They are interpreted via $\cI$ as relations over a domain $\cD$ of the corresponding arity.) A state $s$ is a mapping assigning to each variable $x$ in $\cL$ a value $s[x]$ in $\cD$. This interpretation is extended to $\cL$-expressions in the usual way ( $s[f(x)]=\cI(f)(s[x])$). We write $s \models_{\cM(\cL)} c$ iff $c$ is true $s$ in $\cM(\cL)$. The state $s$ is an $x$-variant of $s'$ iff $s'[y]=s[y]$ for each $y\neq x.$ We use $\sigma$ to range over infinite sequences of states. Furthermore, $\sigma$ is an $x$-variant of $\sigma'$ iff $\sigma(i)$ is an $x$-variant of $\sigma'(i)$ for each $i\geq0$. LTL Theories. Given a cs $(\Delta, \Sigma)$ with first-order language $\cL$, the LTL theory induced by $\Delta$, $T(\Delta)$ is the set of LTL sentences that are LTL valid in all the $\cL$-structures (or $\cL$-models) of $\Delta.$ We write $F \entails_{T(\Delta)} G$ iff $(F \imply G) \in T(\Delta)$. We omit "" in $\entails_{T(\Delta)}$ when no confusion arises. Future-free constraints. For the symbolic semantics we take the liberty of assuming that the constraints in processes and configurations are replaced with certain LTL formulae. Namely, future-free formulae: Those which do not contain occurrences of $\always$ and $\nextt.$ So, for example a process-store configuration of the form $\tuple{\absp{y}{\past c}{P}}{\past d}$ may appear in the transitions of the symbolic semantics. We shall abuse the notation by assuming that, in the context of the symbolic semantics, $c,d,c',d',\ldots$ range over future-free formulae. In the context of the SOS, however, $c,d,c',d',\ldots$ range over state formulae only. Future-free formulae preserve the decidability of their underlying . Symbolic Reductions. The internal and observable symbolic transitions $\redi_s, \Longrightarrow_s$ are defined as in Table 1 with $\entails$ replaced by $\entails_T$ and with $\rAbs$ and $\rObserv$ replaced, resp., by $\rAbsSym$ and $\rObservSym$ in Table 2 (with $c,c'$ and $d'$ representing future-free formulae rather than just state-formulae). The rule $\rAbsSym$ represents with the temporal constraint $\forall \vec{x} (c \imply d')$ the substitutions that its operational counterpart $\rAbs$ would induce as intuitively explained in Section 4.1(A). Notice that in the reduction of $P$ the variables $\vec{x}$ in $d$ are hidden, via existential quantification, to avoid clashes with those in $P$. The function $F_s$ in $\rObservSym$ is similar to its operational counterpart $F$. However, $F_s$ records the final global and local stores as well as abstraction guards as past information. As explained in Section 4.1(B) this past information is needed in next time unit. Table 2: Symbolic Rules for Internal and Observable Transitions. The function $F_s$ is given in Definition 7. $\begin{array}{l} \rightinfer[\rAbsSym]{ \begin{array}{l} \tuple{ \absp{\vec{x}... ...e Q,d\right\rangle \: \not \hspace{-.1cm}\redisym {} } \\ \\ \end{array}$ Finally, it is easy to verify that no infinite sequence $\gamma_1 \redisym \gamma_2 \redisym \ldots$ can be generated by the symbolic semantics. Thus we avoid the problems discussed in Section 3.2. Semantic Results We now look at the semantics results for . First of all, as the basic CCP, utcc is deterministic. Operational Correspondence. The correspondence between the two semantics is given below. It states that the (untimed) constraints entailed by the outputs of any arbitrary long sequence of observable reductions coincide with those of the corresponding one in the symbolic semantics. We say that $P$ is abstracted-unless free iff it has no occurrences of processes of the form $\unlessp{c}{Q}$ under the scope of an abstraction. We confined ourselves to abstracted-unless free processes due to the problem of representing the negation of entailment as logic formulae. Take $P=\absp{x}{\true}{Q}$ where $Q=\unlessp{e}{\tellp{e'}}.$ Let $d$ be the final store in the first time unit when running $P$. Operationally, $\tellp{e'}[t/x]$ is executed in the second time unit for those $t$'s $d \not\entails e[t/x].$ Following Section 4.1 one may try to capture this in the symbolic semantics with $\past d \wedge \forall x (\past (\neg e) \imply e')$ as if we had $Q=\whenp{\neg e}{\nextp{\tellp{e'}}}.$ This wrongly assumes, however, that in general $d \not \entails e[t/x]$ is equivalent to $d \entails \neg e[t/x].$ Abstract-unless free processes represent a meaningful and practical fragment of utcc They are sufficient to express all the examples and intended applications of this paper. Furthermore, we have proven they are able to model Turing Machines which bears witness to their universal expressiveness. LTL Correspondence. The compositional encoding in Definition 8 gives a pleasant correspondence between $\utcc$ processes and LTL formulae. It shows the duality between local and abstraction operators, represented resp. as existential and universal quantified formulae. A key aspect of Theorem 3 is that it allows using well-established techniques from LTL for reachability analysis of utcc processes: E.g., to verify if a given security protocol modelled in utcc can reach a state where secrecy is violated. Applications This section illustrates the use of in the analysis of security protocols. In particular, we shall exhibit the secrecy flaw of the Needham-Schroeder protocol (NS) [9]. Figure 1: Needham-Schroeder Protocol NS aims at distributing two nonces (unguessable secrets) in a secure way. Figure 1(a) shows the steps of NS where $m$ and $n$ represent the nonces generated, resp., by the principals $A$ and $B$. The notation $\{m,A\}_B$ represents the message obtained by encrypting with $B$'s public key the composition $m$ with $A$'s identifier. In [9] it is shown how an attacker ($C$ in Figure 1(b)) can reveal $n$ thus violating the secrecy property. Modelling NS in utcc. As typically done we follow the Dolev and Yao thread model [7] which presupposes an attacker that can eavesdrop, disassemble, compose, encrypt and decrypt messages with available keys. It also presupposes that cryptography is unbreakable. We begin by defining a cs based on [7] which follows the Dolev and Yao model. Intuitively, $\cP$ and $\cK$ represent the principal identifiers $A,B,\ldots$ and keys $k,k',\ldots$. We use $\{m\}_k$, $\{m_1,m_2\}$, $k^{-1}$, resp., for $\encp(m,k)$ (encryption), $\pairp(m_1,m_2)$(composition) and $\invp(k)$ (inverse key). Furthermore, $\keypp(x)$ represents the public key of $x$. From [7] one can show that $\entailsec$ is decidable. The rule $\rEnc$ says that if one can infer that the message $m$ as well as a key $k$ are output on the global channel $\outp$, then one may as well infer that $\{m\}_k$ is also output on $\outp$. The other rules can be explained similarly. Table: Security entailment relation. $\begin{array}{cc} \rightinfer[\rPrj]{F \entailsec \outp(m_{i}) }{F \entailsec ... ...(m)}{F \entailsec \outp(k^{-1}) F\entailsec \outp(\{m\}_k)} \end{array}$ We now specify the principals. The NS model uses $\mathbf{Init}$ and $\mathbf{Resp}$ describing the role of the initiator and the responder $A$ and $B$ in Figure 1(a). Posting messages, nonce generation, message reception are modelled, resp., using tell, local and wait processes. $$\begin{array}{ll} \mathbf{Init}(i,r) \defsymbol &\localp{m}... ...              \parallel\bangp{\tellp{\secretp(n)}} \end{array}$$ Notice that since Responder's nonce cannot be known by an attacker, $\mathbf{Resp}(t)$ states that $n$ is secret. We also define an observer $\cO$ telling $\failp$ whenever a secret appears unprotected on the global channel $\outp.$ Additionally the observer remembers every message that was ever on $\outp$ by transferring them across the time intervals. $$%\scriptsize \begin{array}{lll} \cO &\defsymbol & !\absp{n}{\... ...\ & & !\absp{m}{\outp(m)}\nextp{\tellp{\outp(m)}} \end{array}$$ The situation in Figure 1(b) can be modelled as: $$%\scriptsize \begin{array}{c} \mathcal{NS} = \mathbf{Init}(A,... ...sp}(B) \parallel \cO \parallel \tellp{c_{\it init}} \end{array}$$ with ${c_{\it init}=\outp(\keypp(C)^{-1})\wedge\forall _{{\it id}\in\cP} (\outp(id) \wedge \outp(\keypp(id)))}$ representing the initial knowledge available for an attacker. Namely, all the principal ids, their public keys and the compromised private key of $C$. We can use the symbolic semantics to show that $\mathcal{NS}$ eventually outputs $\failp:$ Alternatively, the above proposition can be proved using Theorem 3 and LTL deduction. Notice that we cannot use the SOS to exhibit an output of $\failp$ since the secure will generate infinite substitutions within a time interval (see Section 3.2). E.g., If $F\entails \outp(m)$ then $F\entails \outp(\{ m,m \})$ and $F\entails \outp(\{m,m,m\})$ and so on. This illustrates the relevance of the symbolic semantics and the correspondence in Theorem 3. Related and Concluding Remarks In [4] a symbolic semantics is introduced to deal with the infinite-branching of a $\pi$-calculus reduction relation caused by infinitely many substitutions. Roughly, boolean constraints over names represent conditions the transition must hold to take place. Similar approaches [7,3] are followed for other $\pi$-calculus variants. These calculi, however, are conceptually different from CCP. Furthermore, here not only did the symbolic semantics deal with the infinite-branching problem but also with temporal issues and divergent internal computation introduced by the operational semantics. Mobility has been introduced in other CCP-related formalisms. In particular LMNtal [18] and Atomic CCP [8] where logical variables also represent links. LMNtal has emerged as an unifying model of concurrency, as such it is not restricted to be deterministic. Similarly, Atomic CCP is non-deterministic. To our knowledge no correspondence between these languages and logic has been given. Several process calculi have been specifically designed for the analysis of security protocols, e.g., [7,3,5]. Although can be used to reason about certain aspects of security protocols (e.g., secrecy), it was not designed exclusively for this domain of application. Nevertheless, its LTL characterisation offers a reasoning technique for reachability, to our knowledge not provided by the above calculi. The rather successful logic programming approach to security protocols in [2] is closely related to ours in . The basic difference is that the underlying logic in [2] is Horn clauses while ours is LTL. Also our approach benefits from the operational view of process calculi. Finally, in [1] soft constraints are used to give an interesting quantitative approach to analysing integrity, confidentiality and authentication in security protocols. This approach is, however, more related to constraint satisfaction than to CCP. Since preserves the basic properties of , we believe it allows for a smooth extension of the elegant clousure operator semantics in [16]. From a practical point of view, we have implemented in Oz [15] an interpreter executing programs written in . Following the SOS, the interpreter computes the final stores given the input sequences and the process to be executed. To avoid problems with infinitely many substitutions, we restricted $m$, $m_1$ and $m_2$ in Rules $\rEnc$ and $\rPair$ to have less than a fix number of applications of $\encp$ and $\pairp$. In this way we have automatically verified Proposition 2. Bibliography 1 G. Bella and S. Bistarelli. Soft constraints for security protocol analysis: Confidentiality. In Proc. of PADL'01. LNCS, 2001. 2 B. Blanchet. Security Protocols: From Linear to Classical Logic by Abstract Interpretation. Information Processing Letters, 95(5), 2005. 3 M. Boreale. Symbolic trace analysis of cryptographic protocols. In Proc. of ICALP'01. LNCS, 2001. 4 M. Boreale and R. D. Nicola. A symbolic semantics for the pi-calculus. Information and Computation, 126, 1996. 5 F. Crazzolara and G. Winskel. Events in security protocols. In Proc. of CCS '01. ACM Press, 2001. 6 F. Fages, P. Ruet, and S. Soliman. Linear concurrent constraint programming: Operational and phase semantics. Information and Computation, 165, 2001. 7 M. Fiore and M. Abadi. Computing symbolic models for verifying cryptographic protocols. In Proc. of the 14th IEEE Workshop on Computer Security Foundations. IEEE Computer Society, 2001. 8 C. Laneve and U. Montanari. Mobility in the CC-paradigm. In Mathematical Foundations of Computer Science, 1992. 9 G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proc. of TACAS'96. LNCS, 1996. 10 Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1991. 11 R. Milner. Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, 1999. 12 M. L. Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1967. 13 M. Nielsen, C. Palamidessi, and F. Valencia. Temporal concurrent constraint programming: Denotation, logic and applications. Nordic Journal of Computing, 9(1), 2002. 14 C. Palamidessi, V. Saraswat, F. Valencia, and B. Victor. On the expressiveness of linearity vs persistence in the asychronous pi-calculus. In Proc. of LICS'06. IEEE Computer Society, 2006. 15 P. V. Roy and S. Haridi. Concepts, Techniques, and Models of Computer Programming. MIT Press, 2004. 16 V. Saraswat, R. Jagadeesan, and V. Gupta. Foundations of timed concurrent constraint programming. In Proc. of LICS'94. IEEE Computer Society, 1994. 17 V. A. Saraswat. Concurrent Constraint Programming. MIT Press, 1993. 18 K. Ueda, N. Kato, K. Hara, and K. Mizuno. LMNtal as a unifying declarative language: Live demonstration. In Proc. of ICLP'06. LNCS, 2006. 19 F. Valencia. Temporal concurrent constraint programming. PhD thesis, BRICS, 2003.