| 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 talk, we describe an automated symbolic security analysis technique
for administrative attribute-based RBAC policies. A class of formulae of first-order
logic is used as an adequate symbolic representation 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 procedure. Besides discussing the
assumptions for the effectiveness and termination of the procedure, we demonstrate its
efficiency through an extensive empirical evaluation. |
