View Full Document

Principal-Centric Reasoning in Constructive Authorization Logic



View the full content.
View Full Document
View Full Document

6 views

Unformatted text preview:

Principal Centric Reasoning in Constructive Authorization Logic Deepak Garg April 14 2009 CMU CS 09 120 School of Computer Science Carnegie Mellon University Pittsburgh PA 15213 e mail dg cs cmu edu Abstract 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 This work was partly supported by the Air Force Research Laboratory under grant no FA87500720028 Keywords Authorization Logic Intuitionistic Modal Logic Logical Translation 1 Introduction Authorization refers to the act of deciding whether or not an agent making a request to perform an operation on a resource should be allowed to do so For example the agent may be a browser trying to read pages from a website In that case the site s web server may consult the browser s credentials and a htaccess file to determine whether to send the pages or not Such access control is pervasive in computer systems As systems and their user environments evolve policies used for access control may become complex and error prone This suggests the need for formal mechanisms to represent enforce and analyze policies Logic appears to be a useful mechanism for these purposes Policies may be expressed as formulas in a suitably chosen logic This has several merits First the logic s rigorous inference eliminates any ambiguity that may be inherent in a textual description of policies Second policies may be enforced end to end using generic logic based



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Principal-Centric Reasoning in Constructive Authorization Logic and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Principal-Centric Reasoning in Constructive Authorization Logic and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?