Belief Semantics of Authorization Logic
Logic in Computer Science
2013-08-06 v3 Cryptography and Security
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.
Keywords
Cite
@article{arxiv.1302.2123,
title = {Belief Semantics of Authorization Logic},
author = {Andrew K. Hirsch and Michael R. Clarkson},
journal= {arXiv preprint arXiv:1302.2123},
year = {2013}
}