Automated and Efficient Analysis of Role-Based Access Control with Attributes

We consider an extension of the Role-Based Access Control model in which rules assign users to roles based on attributes. We consider an open (allow-by-default) policy approach in which rules can assign users negated roles thus preventing access to the permissions associated to the role. The problems of detecting redundancies and inconsistencies are formally stated. By expressing the conditions on the attributes in the rules with formulae of theories that can be efficiently decided by Satisfiability Modulo Theories (SMT) solvers, we characterize the decidability and complexity of the problems of detecting redundancies and inconsistencies. The proof of the result is constructive and based on an algorithm that repeatedly solves SMT problems. An experimental evaluation with synthetic benchmark problems shows the practical viability of our technique.