Belief Semantics of Authorization Logic

A formal belief semantics is given for a constructive, first-order authorization logic. 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 Kripke semantics is mechanized in Coq.