Abstract
Attribute-based Access Control (ABAC) extends traditional Access Control by considering an access request as a set of pairs attribute name-value, making it particularly useful in the context of open and distributed systems, where security relevant information can be collected from different sources. However, ABAC enables attribute hiding attacks, allowing an attacker to gain some access by withholding information.
In this paper, we first introduce the notion of policy resistance to attribute hiding attacks. We then propose the tool ATRAP (Automatic Term Rewriting for Authorisation Policies), based on the recent formal ABAC language PTaCL, which first automatically searches for resistance counter-examples using Maude, and then automatically searches for an Isabelle proof of resistance. We illustrate our approach with two simple examples of policies and propose an evaluation of ATRAP performances.
Work partially supported by the International Exchange Scheme of the Royal Society and conducted in part at Imperial College London where A. Griesmayer was supported by the Marie Curie Fellowship “DiVerMAS” (FP7-PEOPLE-252184).
Chapter PDF
Similar content being viewed by others
References
Alberti, F., Armando, A., Ranise, S.: Efficient symbolic automated analysis of administrative attribute-based rbac-policies. In: Proceedings of the 6th ACM ASIACCS 2011, pp. 165–175. ACM, New York (2011)
Armando, A., Ranise, S.: Scalable automated symbolic analysis of administrative role-based access control policies by smt solving. Journal of Computer Security 20(4), 309–352 (2012)
Barker, S., Fernández, M.: Term rewriting for access control. In: Damiani, E., Liu, P. (eds.) Data and Applications Security 2006. LNCS, vol. 4127, pp. 179–193. Springer, Heidelberg (2006)
Bertolissi, C., Uttha, W.: Automated analysis of rule-based access control policies. In: Proceedings of the 7th Workshop on Programming Languages Meets Program Verification, PLPV 2013, pp. 47–56. ACM, New York (2013)
Bonatti, P., De Capitani Di Vimercati, S., Samarati, P.: An algebra for composing access control policies 5(1), 1–35 (2002)
Brucker, A.D., Brügger, L., Kearney, P., Wolff, B.: An approach to modular and testable security models of real-world health-care applications. In: Proceedings of ACM SACMAT 2011, pp. 133–142. ACM, New York (2011)
Bruns, G., Huth, M.: Access control via Belnap logic: Intuitive, expressive, and analyzable policy composition. ACM Transactions on Information and System Security 14(1), 9 (2011)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)
Crampton, J., Huth, M.: An authorization framework resilient to policy evaluation failures. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 472–487. Springer, Heidelberg (2010)
Crampton, J., Morisset, C.: PTaCL: A language for attribute-based access control in open systems. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 390–409. Springer, Heidelberg (2012)
Dougherty, D.J., Kirchner, C., Kirchner, H., Santana de Oliveira, A.: Modular access control via strategic rewriting. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 578–593. Springer, Heidelberg (2007)
Eker, S.: Associative-commutative rewriting on large terms. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 14–29. Springer, Heidelberg (2003)
Griesmayer, A., Liu, Z., Morisset, C., Wang, S.: A framework for automated and certified refinement steps. Innov. Syst. Softw. Eng. 9(1), 3–16 (2013)
Griesmayer, A., Morisset, C.: Automated certification of authorisation policy resistance. CoRR, abs/1306.4624 (2013), http://arxiv.org/abs/1306.4624
Guelev, D.P., Ryan, M., Schobbens, P.-Y.: Model-checking access control policies. In: Zhang, K., Zheng, Y. (eds.) ISC 2004. LNCS, vol. 3225, pp. 219–230. Springer, Heidelberg (2004)
Hughes, G., Bultan, T.: Automated verification of access control policies using a sat solver. Int. J. Softw. Tools Technol. Transf. 10(6), 503–520 (2008)
Jobe, W.: Functional completeness and canonical forms in many-valued logics. Journal of Symbolic Logic 27(4), 409–422 (1962)
Kirchner, C., Kirchner, H., Santana de Oliveira, A.: Analysis of rewrite-based access control policies. Electron. Notes Theor. Comput. Sci. 234, 55–75 (2009)
Kleene, S.: Introduction to Metamathematics. D. Van Nostrand, Princeton (1950)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
OASIS. eXtensible Access Control Markup Language (XACML) Version 2.0. Committee Specification (2005)
OASIS. eXtensible Access Control Markup Language (XACML) Version 3.0. Committee Specification 01 (2010)
Rao, P., Lin, D., Bertino, E., Li, N., Lobo, J.: An algebra for fine-grained integration of XACML policies. In: Proceedings of the 14th ACM Symposium on Access Control Models and Technologies, pp. 63–72. ACM, New York (2009)
Tschantz, M., Krishnamurthi, S.: Towards reasonability properties for access-control policy languages. In: Ferraiolo, D., Ray, I. (eds.) 11th ACM Symposium on Access Control Models and Technologies, Proceedings, SACMAT 2006, pp. 160–169. ACM (2006)
Wenzel, M.: The isabelle/isar reference manual (2007)
Wijesekera, D., Jajodia, S.: A propositional policy algebra for access control 6(2), 286–235 (2003)
Zhang, N., Ryan, M., Guelev, D.P.: Synthesising verified access control systems through model checking. J. Comput. Secur. 16(1), 1–61 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Griesmayer, A., Morisset, C. (2013). Automated Certification of Authorisation Policy Resistance. In: Crampton, J., Jajodia, S., Mayes, K. (eds) Computer Security – ESORICS 2013. ESORICS 2013. Lecture Notes in Computer Science, vol 8134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40203-6_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-40203-6_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40202-9
Online ISBN: 978-3-642-40203-6
eBook Packages: Computer ScienceComputer Science (R0)