CSP

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 $a \rightarrow$ P describes a process which performs an a and then behaves as process P . The choice operator $P ~ \fbox {\phantom{c}} ~Q$ describes a process which offers a choice between process P and process Q , and it has an indexed form $\fbox {\phantom{h}} \,_{a \in A}P_a$, which offers a choice between all of the processes $P_a$. The choice is resolved by the first action to occur. The parallel operator $P \parallel[A] Q$ forces P and Q to synchronise on actions from the set A , but otherwise execute independently. The hiding operator $P ~\backslash~A$ hides the events in set A , which means that no other process can participate in occurrences of these events. The atomic process $\mbox{ \em Stop }$ marks the termination of a process.