# Belief Semantics of Authorization Logic

arXiv: https://arxiv.org/abs/1302.2123 · HTML: https://mlsanity.com/paper/1302.2123/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Feb 2013.

## Built on by (most cited first, 1 of 1)

- [Security Properties as Nested Causal Statements](https://mlsanity.com/paper/2104.00872/) (2021)

## Abstract (arXiv)

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.