Sciweavers

JCS
2008

Synthesising verified access control systems through model checking

13 years 3 months ago
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 ...
Nan Zhang 0003, Mark Ryan, Dimitar P. Guelev
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JCS
Authors Nan Zhang 0003, Mark Ryan, Dimitar P. Guelev
Comments (0)