Computer Science Department
School of Computer Science, Carnegie Mellon University
Principal Centric Reasoning in
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. Translations from several other authorization logics into DTL0 , as well as formal connections between DTL0 and the modal logic constructive S4 are also presented. Finally, a related logic BL0 is considered and its properties are studied.