A process algebraic approach to security policies

We discuss the nature of security policies, particularly those that arise in the context of healthcare informatics, and the kind of mathematical framework needed to describe and reason about them. Various special purpose frameworks for this purpose have been presented over the years, many using bespoke logics and models of computation. We argue that the properties of interest can be expressed cleanly in a mainstream formal method, in particular in the process algebra CSP. This has a number of advantages: we have a well-established, uniform framework with well-defined semantics to work with and access to a number of well established tools to verify and validate our models and implementations. By way of illustration we describe a CSP formulation of a policy for a clinical trials application drawn for the Framework 5 HARP Project.