Next: Value-Passing SPA Up: The model Previous: The model

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 of input actions, a set of output actions, a set of visible actions, ranged over by , and the usual function such that and ;two sets and of high and low level actions such that , , and where ; a set of actions ( is the internal, invisible action), ranged over by ; a set K of constants, ranged over by Z . The syntax of SPA agents is defined as follows: where and is such that .Moreover, for every constant Z there must be the corresponding definition: . The meaning of , , E+E , E|E , , E[f] and is as for CCS [Mil89]. Intuitively, is the empty process, which cannot do any action; can do an action and then behaves like E ; can alternatively choose  to behave like or ; is the parallel composition of and ,where the executions of the two systems are interleaved, possibly synchronized on complementary input/output actions, producing an internal . can execute all the actions E is able to do, provided that they do not belong to ; E / L turns all the actions in L into internal 's; if E can execute action , then E[f] performs ; finally, Z does what E does, when .

Let be the set of SPA agents, ranged over by E , F . Let 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 and , respectively. The operational semantics of SPA is given (as usual) associating to each agent a particular state of the labelled transition system where and, intuitively, means that agent E can execute moving to E' (see [FG95,FG] for more details).

In the following the expression is a shorthand for ,where denotes a (possibly empty) sequence of labelled transitions. We also extend the `' notation to sequences of actions; with means that such that . For the empty sequence we have that stands for .

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: . E and F are trace equivalent (notation ) if and only if T(E) = T(F) .

Next: Value-Passing SPA Up: The model Previous: The model