A Model Checking Based Approach for Verification of Attribute-Based Access Control Policies in Cloud Infrastructures

  • Igor KotenkoEmail author
  • Igor Saenko
  • Dmitry Levshun
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 1156)


Attribute-Based Access Control (ABAC) model is a perspective access control model for cloud infrastructures used for automation of industrial, transport and energy systems as they include large number of users, resources and dynamical changed permissions. The paper considers the features of ABAC model and the theoretical background for verification of the ABAC policies based on the model checking. The possibility of applying the model checking is justified on the example of the ABAC policy. Implementation of the proposed approach was made using the UPPAAL verification tool. Experimental assessment shows high acceptability of the model checking not only for finding anomalies in ABAC policies but for finding decisions to eliminate them.


Access control Model checking Temporal logics ABAC Cloud infrastructure 



This work was partially supported by grants of RFBR (projects No. 16-29-09482, 18-07-01369, 18-07-01488, 18-37-20047, 18-29-22034, 18-37-20047, 19-07-00953, 19-07-01246), by the budget (the project No. 0073-2019-0002), and by Government of Russian Federation (Grant 08-08).


  1. 1.
    Braghin, C., Sharygina, N., Barone-Adesi, K.: A model checking-based approach for security policy verification of mobile systems. Formal Aspects Comput. 23(5), 627–648 (2011)CrossRefGoogle Scholar
  2. 2.
    Clarke, E.M., Grumberg, O., Peled, D.: Model checking (2000)Google Scholar
  3. 3.
    Deng, Y., Wang, J., Tsai, J.J., Beznosov, K.: An approach for modeling and analysis of security system architectures. IEEE Trans. Knowl. Data Eng. 15(5), 1099–1119 (2003)CrossRefGoogle Scholar
  4. 4.
    Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and change-impact analysis of access-control policies. In: Proceedings of the 27th International Conference on Software Engineering, pp. 196–205. ACM (2005)Google Scholar
  5. 5.
    Holzmann, G.J.: The model checker spin. IEEE Trans. Software Eng. 23(5), 279–295 (1997)CrossRefGoogle Scholar
  6. 6.
    Hu, V.: Attribute based access control (ABAC) definition and considerations. Tech. rep, National Institute of Standards and Technology (2014)Google Scholar
  7. 7.
    Hu, V.C., Kuhn, D.R., Ferraiolo, D.F., Voas, J.: Attribute-based access control. Computer 48(2), 85–88 (2015)CrossRefGoogle Scholar
  8. 8.
    Jaeger, T., Tidswell, J.E.: Practical safety in flexible access control models. ACM Trans. Inf. Syst. Secur. (TISSEC) 4(2), 158–190 (2001)CrossRefGoogle Scholar
  9. 9.
    Karataş, G., Akbulut, A.: Survey on access control mechanisms in cloud computing. J. Cyber Secur. Mobility 7(3), 1–36 (2018)CrossRefGoogle Scholar
  10. 10.
    Kolomeets, M., Chechulin, A., Kotenko, I., Saenko, I.: Access control visualization using triangular matrices. In: 2019 27th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), pp. 348–355. IEEE (2019)Google Scholar
  11. 11.
    Kolovski, V., Hendler, J., Parsia, B.: Analyzing web access control policies. In: Proceedings of the 16th International Conference on World Wide Web, pp. 677–686. ACM (2007)Google Scholar
  12. 12.
    Kotenko, I., Polubelova, O.: Verification of security policy filtering rules by model checking. In: Proceedings of the 6th IEEE International Conference on Intelligent Data Acquisition and Advanced Computing Systems, vol. 2, pp. 706–710. IEEE (2011)Google Scholar
  13. 13.
    Kuhn, D.R., Coyne, E.J., Weil, T.R.: Adding attributes to role-based access control. Computer 43(6), 79–81 (2010)CrossRefGoogle Scholar
  14. 14.
    Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transfer (STTT) 1(1), 134–152 (1997)CrossRefGoogle Scholar
  15. 15.
    Lee, A.J.: Credential-based access control. In: Encyclopedia of Cryptography and Security, pp. 271–272 (2011)Google Scholar
  16. 16.
    Lin, D., Rao, P., Bertino, E., Li, N., Lobo, J.: EXAM: a comprehensive environment for the analysis of access control policies. Int. J. Inf. Secur. 9(4), 253–273 (2010)CrossRefGoogle Scholar
  17. 17.
    Lopez, J., Rubio, J.E.: Access control for cyber-physical systems interconnected to the cloud. Comput. Netw. 134, 46–54 (2018)CrossRefGoogle Scholar
  18. 18.
    Mocanu, D., Turkmen, F., Liotta, A., et al.: Towards ABAC policy mining from logs with deep learning. In: Proceedings of the 18th International Multiconference, IS2015, pp. 124–128 (2015)Google Scholar
  19. 19.
    Rothmaier, G., Kneiphoff, T., Krumm, H.: Using spin and eclipse for optimized high-level modeling and analysis of computer network attack models. In: International SPIN Workshop on Model Checking of Software, pp. 236–250. Springer (2005)Google Scholar
  20. 20.
    Servos, D., Osborn, S.L.: Current research and open problems in attribute-based access control. ACM Comput. Surv. (CSUR) 49(4), 65 (2017)CrossRefGoogle Scholar
  21. 21.
    Subashini, S., Kavitha, V.: A survey on security issues in service delivery models of cloud computing. J. Netw. Comput. Appl. 34(1), 1–11 (2011)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.St. Petersburg Institute for Informatics and Automation of the Russian Academy of Sciences (SPIIRAS)Saint-PetersburgRussia
  2. 2.St. Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University)Saint-PetersburgRussia

Personalised recommendations