You are here


ASASP is a tool for the automated safety analysis of administrative access control policies in (extensions of) the Role-Based Access Control (RBAC) model.  The goal of the tool is to establish if untrusted users can get permissions to access sensitive resources.  ASASP is capable of performing an analysis that is parametric in the number of users, i.e. it certifies safety with respect to a finite but unknown number of users.  ASASP is also capable of taking into account attribute-based assignments of roles to users and temporal constraints on the RBAC policies.

Official web-site:

Role-Based Access Control (RBAC) policies have been widely adopted by enterprise and complex organizations around the world.  Because of their size and complexity, automated techniques for their security analysis are crucial for design and maintenance. In particular, the definition of administrative domains by means of attributes restrieved from user profiles makes the RBAC model easier to use in real scenarios but complicates the development of security analysis techniques, that should be able to modularly reason about a wide range of attribute domains. Another complication is the use of contextual information, such as time and location, in the expression of the authorization conditions of RBAC policies.

The prototype tool ASASP (short for Automated Symbolic Analysis of Security Policies) implements a symbolic backward reachability analysis to solve user-role reachability problems, i.e. it is capable of establishing if there exists a coalition of administrators capable of giving a certain set of priviliges to a certain (untrusted) user. ASASP uses the model checker MCMT to mechanize the backward reachability procedure and integrates several herustic to alleviate the state-space explosion problem while providing a flexibile framework to express various extensions of RBAC policies encompassing attributes and contextual information.  Despite is flexibility, ASASP is competitive with other tools for the analysis of administrative RBAC policies such as Mohawk and VAC or the tool by Uzun et al. for the analysis of temporal RBAC policies.  To the best of our knowledge, ASASP is the only tool capable of handling user-role assignments based on attributes.

The tool is available on request.  Please, send an email to Silvio Ranise.

Relevant papers

  1. S. Ranise and A. Truong, "Incremental Analysis of Evolving Administrative Role Based Access Control Policies", In 28th Annual IFIP WG 11.3 Working Conference on Data and Applications Security and Privacy (DBSeC), Springer LNCS, 2014. To appear.
  2. S. Ranise, A. Truong, A. Armando, "Scalable and Precise Automated Analysis of Administrative Temporal Role-Based Access Control", In ACM Symposium on Access Control Models and Technologies (SACMAT), ACM Press, 2014. To appear.
  3. S. Ranise, A. Truong, A. Armando, "Boosting Model Checking to Analyse Large ARBAC Policies", Chapter in Security and Trust Management (Audun Jøsang, Pierangela Samarati, Marinella Petrocchi, eds.), Springer Berlin Heidelberg, LNCS vol. 7783, pp. 273-288, 2013.
  4. Alessandro Armando, Silvio Ranise, "Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving", In Journal of Computer Security, vol. 20, no. 4, pp. 309-352, 2012.
  5. F. Alberti, A. Armando, S. Ranise, "ASASP: automated symbolic analysis of security policies", In CADE'11: Proceedings of the 23rd international conference on Automated deduction, Springer-Verlag, LNCS vol. 6803, Berlin, Heidelberg, pp. 26-33, 2011.
  6. F. Alberti, A. Armando, S. Ranise, "Efficient symbolic automated analysis of administrative attribute-based RBAC-policies", In ASIACCS '11: Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, ACM, New York, NY, USA, pp. 165-175, 2011.
  7. A. Armando and S. Ranise, "Automated symbolic analysis of ARBAC-policies", In STM'10: Proceedings of the 6th international conference on Security and trust management, Springer-Verlag, Berlin, Heidelberg, pp. 17-34, 2011.