Belief Semantics of Authorization Logic
Andrew K. Hirsch, Michael R. Clarkson
TL;DR
This paper introduces a formal belief semantics for authorization logics used in computer security, providing a more direct way to represent principals' beliefs and proving its soundness.
Contribution
It presents a new belief semantics for authorization logic that subsumes Kripke semantics and offers a mechanized proof of soundness in Coq.
Findings
Belief semantics subsumes standard Kripke semantics.
Proof system is sound with respect to both semantics.
Mechanized proof of soundness in Coq.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAccess Control and Trust · Logic, Reasoning, and Knowledge · Security and Verification in Computing