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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com