Date Added: May 2011
The authors present a new modal access control logic ACL+ to specify, reason about and enforce access control policies. The logic includes new modalities for permission, control, and ratification to overcome some limits of current access control logics. They present a Hilbert-style proof system for ACL+ and a sound and complete Kripke semantics for it. They exploit Kripke semantics to define Seq-ACL+: a sound, complete, cut-free and terminating calculus for ACL+, proving that ACL+ is decidable. They point at a Prolog implementation of Seq-ACL+ and discuss possible extensions of ACL+ with axioms for subordination between principals.