Model Based Analysis and Validation of Access Control Policies

We present a model based approach to describing, analysing and validating access control policies. Access control policies are de- scribed using VDM { a model oriented formal method. Policy descrip- tions are concise and may be easily manipulated. The structure of the VDM description is derived from the OASIS standard access control policy language XACML. It is therefore straightforward to translate be- tween XACML policies and their corresponding VDM models. We show how the existing tool support for VDM enables a number of ways of validating these policies, each of which are valuable at dieren t stages of the development and maintenance life cycle.