Belief Semantics of Authorization Logic

Authorization logics deserve semantics that represent their usage. We introduce a semantics appropriate for proof-carrying authorization.


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.

%d bloggers like this: