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 DTL₀ , as well as formal connections between DTL₀ and the modal logic constructive S4 are also presented. Finally, a related logic BL₀ is considered and its properties are studied.

125 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu