On the Decidability of the Safety Problem for Access Control Policies

Abstract : An access control system regulates the rights of users to gain access to resources in accordance with a specified policy. The rules in this policy may interact in a way that is not obvious via human inspection; there is, therefore, a need for automated verification techniques that can check whether a policy does indeed implement some desired security requirement. Thirty years ago, a formalisation of access control presented a model and a safety specification for which satisfaction is undecidable. Subsequent research, aimed at finding restricted versions that obtain the decidability of this problem, yielded models without satisfactory expressive power for practical systems. Instead of restricting the model, we reexamine the safety specification. We develop a new logic that can express a wide variety of safety properties over access control systems, and show that model checking is decidable for a useful fragment of this logic.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.91-103, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00089496
Contributeur : Stephan Merz <>
Soumis le : vendredi 18 août 2006 - 19:48:47
Dernière modification le : vendredi 18 août 2006 - 19:56:36
Document(s) archivé(s) le : lundi 5 avril 2010 - 23:10:27

Fichier

Identifiants

  • HAL Id : inria-00089496, version 1

Collections

Citation

Eldar Kleiner, Tom Newcomb. On the Decidability of the Safety Problem for Access Control Policies. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.91-103, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00089496〉

Partager

Métriques

Consultations de la notice

111

Téléchargements de fichiers

221