Belief Semantics of Authorization Logic
This work addresses foundational issues in computer security theory by offering a more intuitive semantics for authorization logics, though it appears incremental as it builds on existing Kripke semantics.
The paper tackles the problem of formalizing authorization logics for computer security by introducing a belief semantics that directly represents principals' beliefs, proving it subsumes standard Kripke semantics and providing a sound proof system mechanized in Coq.
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.