Principal-Centric Reasoning in Constructive Authorization Logic
Deepak Garg · 2009
We present an authorization logic DTL0 that explicitly relativizes reasoning to beliefs of principals. The logic assumes that principals are conceited in their beliefs. We describe the natural deduction system, sequent calculus, Hilbert-style axiomatization, and Kripke semantics of the logic. We prove several meta-theoretic results including cut-elimination, and soundness and completeness for the Kripke semantics. We also present translations from several other authorization logics into DTL0, and describe formal connections between DTL0 and the modal logic constructive S4.