Action Refinement in Process Algebra and Security Issues

In the design process of distributed systems we may have to replace abstract specifications of components by more concrete specifications, thus providing more detailed design information. In the context of process algebra, this well-known approach is often referred to as action refinement. We study the relationships between action refinement and security properties within the Security Process Algebra (SPA). First we formalize the concept of action refinement as a structural inductive transformation. Then we prove several compositional results which can be exploited in the stepwise development of processes. Finally, we consider information flow security properties for SPA processes and define a decidable class of secure processes which is closed under refinement.