SPA and Semantic Equivalences

 In the following, protocols will be specified using the Security Process Algebra, an extension of Milner's CCS [Mil89]. SPA has one additional operator, namely the hiding operator E / L of CSP [Hoa85], which is useful in characterizing some security properties in an algebraic style. Moreover the set of visible actions is partitioned into high and low level actions in order to specify multilevel systems.

SPA syntax is based on the following elements: a set $I = \{a,b, \ldots \}$ of input actions, a set $O = \{\bar{a},\bar{b}, \ldots \}$ of output actions, a set ${\cal L} = I \cup O$ of visible actions, ranged over by $\alpha$, and the usual function $\bar\cdot : {\cal L} \rightarrow {\cal L}$ such that $a \in I \Longrightarrow \bar{a} \in O$ and $\bar{a} \in O \Longrightarrow \bar{\bar{a}} = a \in I$;two sets $Act_H$ and $Act_L$ of high and low level actions such that $\overline{Act_H} = Act_H$, $\overline{Act_L} = Act_L$, $Act_H \cup Act_L = {\cal L}$ and $Act_H \cap Act_L = \emptyset$where $\bar{L} \stackrel{\rm def}{=}\{ \bar{a} : a \in L \}$; a set $Act = {\cal L} \cup \{\tau\}$ of actions ($\tau$ is the internal, invisible action), ranged over by $\mu$; a set K of constants, ranged over by Z . The syntax of SPA agents is defined as follows: $$\begin{eqnarray*} E & ::= & \underline{0}\mid \mu . E \mid E+E \mid E\vert E \mid E \setminus L \mid E / L \mid E[f] \mid Z\end{eqnarray*}$$ where $L \subseteq {\cal L}$ and $f: Act \rightarrow Act$ is such that $f(\bar\alpha) = \overline{f(\alpha)},\ f(\tau) = \tau$.Moreover, for every constant Z there must be the corresponding definition: $Z \stackrel{\rm def}{=}E$. The meaning of $\underline{0}$, $\mu . E$, E+E , E|E , $E \setminus L$, E[f] and $Z \stackrel{\rm def}{=}E$ is as for CCS [Mil89]. Intuitively, $\underline{0}$ is the empty process, which cannot do any action; $\mu . E$ can do an action $\mu$ and then behaves like E ; $E_1 + E_2$ can alternatively choose  to behave like $E_1$ or $E_2$; $E_1 \vert E_2$ is the parallel composition of $E_1$ and $E_2$,where the executions of the two systems are interleaved, possibly synchronized on complementary input/output actions, producing an internal $\tau$.$E \setminus L$ can execute all the actions E is able to do, provided that they do not belong to $L \cup \bar{L}$; E / L turns all the actions in L into internal $\tau$'s; if E can execute action $\mu$, then E[f] performs $f(\mu)$; finally, Z does what E does, when $Z \stackrel{\rm def}{=}E$.

Let ${\cal E}$ be the set of SPA agents, ranged over by E , F . Let ${\cal L}(E)$ denote the sort of E , i.e., the set of the (possibly executable) actions occurring syntactically in E . The sets of high level agents and low level ones are defined as ${\cal E}_{H}\stackrel{\rm def}{=}\{ E \in {\cal E} \mid {\cal L}({E}) \subseteq Act_H \cup \{ \tau \} \}$and ${\cal E}_{L}\stackrel{\rm def}{=}\{ E \in {\cal E} \mid {\cal L}({E}) \subseteq Act_L \cup \{ \tau \} \}$, respectively. The operational semantics of SPA is given (as usual) associating to each agent a particular state of the labelled transition system $({\cal E},Act,\rightarrow)$ where $\rightarrow \subseteq {\cal E}\times Act \times {\cal E}$ and, intuitively, $E \stackrel{{\mu}}{\rightarrow} E'$ means that agent E can execute $\mu$ moving to E' (see [FG95,FG] for more details).

In the following the expression $E \stackrel{{\mu}}{\Longrightarrow} E'$ is a shorthand for $E(\stackrel{{\tau}}{\rightarrow})^* E_1 \stackrel{{\mu}}{\rightarrow} E_2 (\stackrel{{\tau}}{\rightarrow})^* E'$,where $(\stackrel{{\tau}}{\rightarrow})^*$ denotes a (possibly empty) sequence of $\tau$labelled transitions. We also extend the `$\Longrightarrow$' notation to sequences of actions; $E \stackrel{{\gamma}}{\Longrightarrow} E'$ with $\gamma \in {\cal L}^+, \gamma = \gamma_1 \gamma_2 \ldots \gamma_n$ means that $\exists E_1,E_2, \ldots, E_{n-1}$ such that $E \stackrel{{\gamma_1}}{\Longrightarrow} E_1 \stackrel{{\gamma_2}}{\Longrightar... ...amma_{n-1}}}{\Longrightarrow} E_{n-1} \stackrel{{\gamma_n}}{\Longrightarrow} E'$. For the empty sequence $\epsilon$we have that $E \stackrel{{\epsilon}}{\Longrightarrow} E'$ stands for $E (\stackrel{{\tau}}{\rightarrow})^* E'$.

We recall here the definition of trace equivalence

Definition 2.1

A trace of a process E is a sequence of actions that E can execute. The set of traces is defined as follows: $T(E) \stackrel{\rm def}{=}\{ \gamma \in {\cal L}^* \mid \exists E': E \stackrel{{\gamma}}{\Longrightarrow} E' \}$. E and F are trace equivalent (notation $E \approx_T F$) if and only if T(E) = T(F) . $\rule{2mm}{2mm}$