Abstract Security Properties in Process Algebra

A theory of abstract security properties is presented in process algebra with abstract security properties defined as special kinds of equivalent classes of processes, that is, the sets of processes that are equally secure. In the context of process algebra, investigation of abstract security properties can be cast into the investigation of the properties of process algebra operators. It proves that partial orders can be defined on the sets of abstract security properties to generate CPOs. Thus the theory of CPOs and fixed-points can be used. An investigation is made into the actions of algebra operators on the sets of abstract security properties. A theorem is given to show that process algebra operators are monotony functions. From the above theorem, (1) compositional invariant security properties and constructive security properties are proved to exist, and (2) security properties are degraded under operators of process algebra, which is known as “bucket principle”, i.e, a composed system cannot be securer than the weakest link of the system. Finally, a formal definition of absolute security property is given, and is associated with trivial properties of processes. A theorem shows that absolute security property is itself trivial property.