Belief Semantics of Authorization Logic

Andrew K. Hirsch and Michael Clarkson Belief Semantics of Authorization Logic. in Computer and Communication Security, (Berlin, Germany, 2013), ACM.

Abstract: Authorization logics have been used in the theory of computer security to reason about access control decisions. In this work, a formal belief semantics for authorization logics is given. The belief semantics is proved to subsume a standard Kripke semantics. The belief semantics yields a direct representation of principals’ beliefs, without resorting to the technical machinery used in Kripke semantics. A proof system is given for the logic; that system is proved sound with respect to the belief and Kripke semantics. The soundness proof for the belief semantics, and for a variant of the Kripke semantics, is mechanized in Coq.

Releases: - ACM Digital Library - Preprint (PDF) - Coq Tarball