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.
Appeared in CCS 2013.