Automatic Conformance Checking of Role-Based Access Control Policies via Alloy

  • David Power
  • Mark Slaymaker
  • Andrew Simpson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6542)


Access control policies are a crucial aspect of many security-critical software systems. It is generally accepted that the construction of access control policies is not a straightforward task. Further, any mistakes in the process have the potential to give rise both to security risks, due to the provision of inappropriate access, and to frustration on behalf of legitimate end-users when they are prevented from performing essential tasks. In this paper we describe a tool for constructing role-based access control (RBAC) policies, which are automatically checked for conformance with constraints described using predicate logic. These constraints may represent general healthiness conditions that should hold of all policies conforming to a general model, or capture requirements pertaining to a particular deployment.


Access Control Policy Language Alloy Model Predicate Logic Access Control Policy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Zhang, N., Ryan, M., Guelev, D.: Evaluating access control policies through model checking. In: Zhou, J., López, J., Deng, R.H., Bao, F. (eds.) ISC 2005. LNCS, vol. 3650, pp. 446–460. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Crampton, J., Huth, M.: Towards an access-control framework for countering insider threats. In: Bishop, M., Gollman, D., Hunker, J., Probst, C. (eds.) Insider Threats in Cyber Security and Beyond. Springer, Heidelberg (2010)Google Scholar
  3. 3.
    Bertino, E., Crampton, J.: Security for distributed systems: Foundations of access control. In: Qian, Y., Tipper, D., Krishnamurthy, P., Joshi, J. (eds.) Information Assurance: Survivability and Security in Networked Systems, pp. 39–80. Morgan Kaufmann, San Francisco (2007)Google Scholar
  4. 4.
    Gouglidis, A., Mavridis, I.: On the definition of access control requirements for grid and cloud computing systems. In: Networks for Grid Applications. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol. 25, part 2, pp. 19–26 (2010)Google Scholar
  5. 5.
    Harrison, M.A., Ruzzo, W.L., Ullman, J.D.: Protection in operating systems. Communications of the ACM 19(8), 461–471 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    De Capitani di Vimercati, S., Foresti, S., Samarati, P.: Authorization and access control. In: Petkovíc, M., Jonker, W. (eds.) Security, Privacy, and Trust in Modern Data Management, pp. 39–53. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Ferraiolo, D.F., Kuhn, D.R., Chandramouli, R.: Role-based access control. Artech House Publishers, Boston (2003)zbMATHGoogle Scholar
  8. 8.
    Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering Methodologies 11(2), 256–290 (2002)CrossRefGoogle Scholar
  9. 9.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)Google Scholar
  10. 10.
    Simpson, A.C., Power, D.J., Russell, D., Slaymaker, M.A., Kouadri-Mostefaoui, G., Ma, X., Wilson, G.: A healthcare-driven framework for facilitating the secure sharing of data across organisational boundaries. Studies in Health Technology and Informatics 138, 3–12 (2008)Google Scholar
  11. 11.
    Slaymaker, M.A., Power, D.J., Russell, D., Wilson, G., Simpson, A.C.: Accessing and aggregating legacy data sources for healthcare research, delivery and training. In: Proceedings of the 2008 ACM Symposium on Applied Computing (SAC 2008), pp. 1317–1324 (2008)Google Scholar
  12. 12.
    Slaymaker, M.A., Power, D.J., Russell, D., Simpson, A.C.: On the facilitation of fine-grained access to distributed healthcare data. In: Jonker, W., Petković, M. (eds.) SDM 2008. LNCS, vol. 5159, pp. 169–184. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  13. 13.
    Simpson, A.C., Power, D.J., Russell, D., Slaymaker, M.A., Bailey, V., Tromans, C.E., Brady, J.M., Tarassenko, L.: GIMI: the past, the present, and the future. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 368, 3891–3905 (2010)CrossRefGoogle Scholar
  14. 14.
    Ferraiolo, D.F., Sandhu, R.S., Gavrilla, S., Kuhn, D.R., Chandramouli, R.: Proposed NIST standard for role-based access control. ACM Transactions on Information and Systems Security 4(3), 224–274 (2001)CrossRefGoogle Scholar
  15. 15.
    El Kalam, A.A., Baida, R.E., Balbiani, P., Benferhat, S., Cuppens, F., Deswarte, Y., Miège, A., Saurel, C., Trouessin, G.: Organization Based Access Control. In: Proceedings of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks (Policy 2003), Como, Italie (2003)Google Scholar
  16. 16.
    Power, D.J., Slaymaker, M.A., Simpson, A.C.: On formalising and normalising role-based access control systems. The Computer Journal 52(3), 303–325 (2009)CrossRefGoogle Scholar
  17. 17.
    Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Woodcock, J.C.P., Davies, J.W.M.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)zbMATHGoogle Scholar
  19. 19.
    Power, D.J., Slaymaker, M.A., Simpson, A.C.: On the modelling and analysis of amazon web services access policies. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, p. 394. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  20. 20.
    Slaymaker, M.A., Power, D.J., Simpson, A.C.: Formalising and validating RBAC-to-XACML translation using lightweight formal methods. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 349–362. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  21. 21.
    Crampton, J.: Specifying and enforcing constraints in role-based access control. In: Proceedings of the 8th ACM Symposium on Access Control Models and Technologies (SACMAT 2003), pp. 43–50 (2003)Google Scholar
  22. 22.
    Hu, H., Ahn, G.: Enabling verification and conformance testing for access control model. In: Proceedings of the 13th ACM Symposium on Access Control Models and Technologies (SACMAT 2008), pp. 195–204 (2008)Google Scholar
  23. 23.
    Hughes, G., Bultan, T.: Automated verification of access control policies using a SAT solver. International Journal on Software Tools for Technology Transfer 10(6), 503–520 (2007)CrossRefGoogle Scholar
  24. 24.
    Zhang, N., Guelev, D.P., Ryan, M.: Synthesising verified access control systems through model checking. Journal of Computer Security 16(1), 1–61 (2007)CrossRefGoogle Scholar
  25. 25.
    Becker, M.Y.: Specification and analysis of dynamic authorisation policies. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF 2009), pp. 203–217 (2009)Google Scholar
  26. 26.
    Behnke, R., Berghammer, R., Meyer, E., Schneider, P.: RELVIEW - A system for calculating with relations and relational programming. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 318–321. Springer, Heidelberg (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • David Power
    • 1
  • Mark Slaymaker
    • 1
  • Andrew Simpson
    • 1
  1. 1.Computing LaboratoryOxford UniversityOxfordUnited Kingdom

Personalised recommendations