Modal Access Control Logic - Axiomatization, Semantics and FOL Theorem Proving (bibtex)
by Valerio Genovese, Daniele Rispoli, Dov M. Gabbay, Leendert W. N. van der Torre
Abstract:
We present and study a Modal Access Control Logic (M-ACL) to specify and reason about access control policies. We identify canonical properties of well-known access control axioms. We provide a Hilbert-style proof-system and we prove soundness, completeness and decidability of the logic. We present a sound and complete embedding of Modal Access Control Logic into First-Order Logic. We show how to use SPASS theorem prover to reason about access control policies expressed as formulas of Modal Access Control Logic, and we compare our logic with existing ones.
Reference:
Modal Access Control Logic - Axiomatization, Semantics and FOL Theorem Proving (Valerio Genovese, Daniele Rispoli, Dov M. Gabbay, Leendert W. N. van der Torre), In STAIRS, 2010.
Bibtex Entry:
@InProceedings{Genovese2010,
  Title                    = {Modal Access Control Logic - Axiomatization, Semantics and FOL Theorem Proving},
  Author                   = {Valerio Genovese and Daniele Rispoli and Dov M. Gabbay and Leendert W. N. van der Torre},
  Booktitle                = {STAIRS},
  Year                     = {2010},
  Pages                    = {114-126},

  Abstract                 = {We present and study a Modal Access Control Logic (M-ACL) to specify and reason about access control policies. We identify canonical properties of well-known access control axioms. We provide a Hilbert-style proof-system and we prove soundness, completeness and decidability of the logic. We present a sound and complete embedding of Modal Access Control Logic into First-Order Logic. We show how to use SPASS theorem prover to reason about access control policies expressed as formulas of Modal Access Control Logic, and we compare our logic with existing ones.},
  Bdsk-url-1               = {http://icr.uni.lu/leonvandertorre/papers/genovese_STAIRS.pdf},
  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Crossref                 = {DBLP:conf/stairs/2010},
  Ee                       = {http://dx.doi.org/10.3233/978-1-60750-675-1-114},
  Timestamp                = {2013.07.26},
  Url                      = {http://icr.uni.lu/leonvandertorre/papers/genovese_STAIRS.pdf}
}
Powered by bibtexbrowser