Title: Security Preserving Refinement of CSP Specifications

Abstract:
Stepwise refinement of a system specification is the essential part of the iterative design
principle. Taking security into account, it is desirable to specify security properties on a
high level and to preserve their validity when refining the specification.
Considering information flow properties, refinement does not preserve security proper-
ties in general. In "Preserving Information Flow Properties under Refinement", Mantel 
introduced refinement operators that preserve possibilistic information flow properties.  
The system model is based on sets of possible system executions, the so-called trace-
semantics. Once a security property has been proven for such a set of system executions 
using well-known unwinding techniques, information from the proof is passed as a 
parameter to the refinement operator. As a result, the refined specification provably 
satisfies the security property, too. The proof information needs to be extracted only 
once, whereas security preserving refinement can then be carried out multiple times.
However, the definition of the refinement operators is a purely semantic definition.
Thus, stepwise refinement is still tedious when one is confronted with a syntactic spec-
ification. In this thesis, security preserving refinement of syntactic specifications is pre-
sented, using Hoare's Communicating Sequential Processes for modelling systems
with cooperating processes.