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.