Belief Semantics of Authorization Logic


Andrew K. Hirsch, Michael R. Clarkson


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 proofs are mechanized in Coq.

Publication History

Appeared in CCS 2013.

Official Version


Technical Report

NAL: Logical Results