In [Sch96] a general framework for analysing security
properties within the process algebra CSP is presented. Only a
limited number of CSP operators are necessary. If a is a CSP
event, A a set of events and P and Q CSP processes,
then the prefix operator P describes a
process which performs an a and then behaves as process P . The
choice operator
describes a process which
offers a choice between process P and process Q , and it has an
indexed form
, which offers a choice between
all of the processes
. The choice is resolved by the first action
to occur. The parallel operator
forces
P and Q to synchronise on actions from the set A , but otherwise
execute independently. The hiding operator
hides
the events in set A , which means that no other process can
participate in occurrences of these events. The atomic process
marks the termination of a
process.