Preserving Information Flow Properties of CSP Specifications under Refinement


Large systems are often designed using a top-down-approach, and iterative 
refinement of abstract specifications is an essential part of this development 
technique. Unfortunately, it is well-known that information flow properties 
such as the Perfect Security Property are in general not closed under 
refinement of the system. As a solution to this problem, security-preserving 
refinement operators were presented by Mantel in 2001 which are capable of 
correcting a possibly insecure refinement request on a labelled transition 
system and providing an optimal approximation. In this thesis we present a 
novel technique to translate processes specified in the language of 
Communicating Sequential Processes to labelled transition systems, apply the 
refinement operators, and translate the refined, secure system back into a 
secure CSP process. The technique is proven sound w.r.t. the traces of the 
process, effectively providing a way to perform secure, iterative refinement 
on CSP. This work bases strongly on H. Mantel’s work in 2001 and his PhD thesis, 
the refinement operators are presented in a similar, compatible form and theory.