Computer Science Department
School of Computer Science, Carnegie Mellon University


Principal Centric Reasoning in
Constructive Authorization Logic

Deepak Garg

April 2009


Keywords: Authorization logic, intuitionistic modal logic, logical translation

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.

125 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by