New Modalities for Access Control Logics: Permission, Control and Ratification

We 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. We present a Hilbert-style proof system for ACL +  and a sound and complete Kripke semantics for it. We exploit the Kripke semantics to define Seq-ACL + : a sound, complete and cut-free sequent calculus for ACL + , implying that ACL +  is at least semi-decidable. We point at a Prolog implementation of Seq-ACL +  and discuss possible extensions of ACL +  with axioms for subordination between principals.