Reasoning about security: a logic and a decision methods for role-based access control

Role-based access control (RBAC) is one of the most promising techniques for the design and implementation of security policies and its diffusion may be enhanced by the development of formal and automated method of analysis. This paper presents a logic for practical reasoning about role based access control which simplifies and adapts to RBAC the calculus developed at Digital SRC. Beside a language and a formal semantics, a decision method based on analytic tableaux is also given. Analytic tableaux make it possible to reason about logical consequence, model generation and consistency of a formalised role-based security policy.