Formalization of RBAC policy with object class hierarchy

Formal methods and reasoning techniques can be useful tools for the representation and analysis of security policies and access control procedures. This paper presents a logical approach to representing and evaluating role-based access control (RBAC) policies, using description logics and a proof method, called tableaux. We propose a new variation of the RBAC model with a classification mechanism for objects. The key feature supported is the ability to model object classes, and class hierarchies used to restrict the validity and to control the propagation of authorization rules. We also demonstrate how access control decisions are made by tableaux, considering role and class hierarchies.