Synthesising verified access control systems through model checking

We present a framework for evaluating and generating access control policies. The framework contains a modelling formalism called RW, which is supported by a model checking tool. RW is designed for modelling access control policies, and verifying their properties. The RW language is very expressive, allowing us to model complex access conditions which can depend on data values, other permissions, and agent roles. A property expresses the capability of a coalition of agents to achieve a goal, which may include reading and overwriting certain information. Given a model built based on a policy and a property, the model-checking algorithm decides whether the goal defined by the property is achievable by the coalition within the permissions the policy provides. In the case that the goal is achievable, the algorithm outputs strategies which may be used by the coalition to achieve the goal. The unachievability of legitimate goals may suggest that the policy does not provide the users enough ...

• Type: Journal
• Year: 2008
• Where: JCS
• Authors: Nan Zhang 0003, Mark Ryan, Dimitar P. Guelev
• Keywords: Access Control Policies, JCS 2008, Policy, RW Language