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 techniques, that should be able to modularly reason about a wide range of attribute domains. In this paper, 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. Copyright 2011 ACM.

Efficient symbolic automated analysis of administrative attribute-based RBAC-policies / Alberti, F.; Armando, A.; Ranise, S.. - (2011), pp. 165-175. (Intervento presentato al convegno 6th International Symposium on Information, Computer and Communications Security, ASIACCS 2011 tenutosi a Hong Kong, chn nel 2011) [10.1145/1966913.1966935].

Efficient symbolic automated analysis of administrative attribute-based RBAC-policies

Ranise S.
2011-01-01

Abstract

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 techniques, that should be able to modularly reason about a wide range of attribute domains. In this paper, 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. Copyright 2011 ACM.
2011
Proceedings of the 6th International Symposium on Information, Computer and Communications Security, ASIACCS 2011
United States
ACM
9781450305648
Alberti, F.; Armando, A.; Ranise, S.
Efficient symbolic automated analysis of administrative attribute-based RBAC-policies / Alberti, F.; Armando, A.; Ranise, S.. - (2011), pp. 165-175. (Intervento presentato al convegno 6th International Symposium on Information, Computer and Communications Security, ASIACCS 2011 tenutosi a Hong Kong, chn nel 2011) [10.1145/1966913.1966935].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333156
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 32
  • ???jsp.display-item.citation.isi??? ND
social impact