Efficient symbolic automated analysis of administrative attribute-based rbac-policies

Automated techniques for the security analysis of Role-Based Access Control (RBAC) access control policies are crucial for their design and maintenance. The definition of administrative domains by means of attributes attached to users makes the RBAC model easier to use in real scenarios but complicates the development of security analysis tech-niques, that should be able to modularly reason about a wide range of attribute domains. In this paper, we describe an automated symbolic security analysis technique for adminis-trative attribute-based RBAC policies. A class of formulae of first-order logic is used as an adequate symbolic repre-sentation for the policies and their administrative actions. State-of-the-art automated theorem proving techniques are used (off-the-shelf) to mechanize the security analysis pro-cedure. Besides discussing the assumptions for the effective-ness and termination of the procedure, we demonstrate its efficiency through an extensive empirical evaluation