DOC PREVIEW
Principal-Centric Reasoning in Constructive Authorization Logic

This preview shows page 1-2-3-4-5-6-7-8-58-59-60-61-62-63-64-65-66-118-119-120-121-122-123-124-125 out of 125 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 125 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

IntroductionThe logic DTL0Structural Proof TheoryNatural DeductionMeta-Theory of the Natural Deduction SystemProof TermsSequent CalculusMeta-Theory of the Sequent CalculusEquivalenceKripke Semantics for DTL0Canonical Kripke Model and CompletenessConnections to Other LogicsConnection to CS4Translation from an Authorization Logic with Lax ModalitiesTranslation from an Authorization Logic with Weak Normal ModalitiesTranslation from Soutei``Binder'' Logic and its TranslationRelated WorkConclusionReferences-reduction and -expansionProperties of the Sequent Calculus (Section 3.5)Proof of Equivalence from Section 3.6The Axiomatic System for DTL0Proof of EquivalenceProofs from Section 4SoundnessCanonical Kripke Model and CompletenessProofs from Section 5.1The Axiomatic System for CS4mProof of SoundnessProof of CompletenessProofs from Section 5.2Proof of SoundnessProof of CompletenessProofs from Section 5.3The Axiomatic System for IIKProof of SoundnessProof of CompletenessProofs from Section 5.4Proof of SoundnessProof of CompletenessProofs from Section 5.5The Axiomatic System for BL0Proofs of Theorems 5.6 and 5.7Proof of Theorem 5.9Principal-Centric Reasoning inConstructive Authorization LogicDeepak GargApril 14, 2009CMU-CS-09-120School of Computer ScienceCarnegie Mellon UniversityPittsburgh, PA 15213e-mail: [email protected] present an authorization logic DTL0that explicitly relativizes reasoning to beliefsof principals. The logic assumes that principals are conceited in their beliefs. Wedescribe the natural deduction system, sequent calculus, Hilbert-style axiomatization,and Kripke semantics of the logic. We prove several meta-theoretic results includingcut-elimination, and soundness and completeness for the Kripke semantics. Translationsfrom several other authorization logics into DTL0, as well as formal connections betweenDTL0and the modal logic constructive S4 are also presented. Finally, a related logicBL0is 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 Translation1 IntroductionAuthorization refers to the act of deciding whether or not an agent making a requestto perform an operation on a resource should be allowed to do so. For example, theagent may be a browser trying to read pages from a website. In that case, the site’s webserver may consult the browser’s credentials and a .htaccess file to determine whetherto send the pages or not. Such access control is pervasive in computer systems. Assystems and their user environments evolve, policies used for access control may becomecomplex 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 ina textual description of policies. Second, policies may be enforced end-to-end usinggeneric logic-based mechanisms like proof-carrying authorization [8–10, 40]. Third, bywriting policies in a logic, there is hope that the policies themselves can be checked forcorrectness against some given criteria (see e.g., [3, 33, 42, 44]).Whereas first-order logic and sometimes propositional logic suffice to express manyauthorization policies, decentralized systems pose a peculiar challenge: how do we ex-press and combine policies of different agents and systems? This is often necessarysince policies and the authorizations derived from them may vary from system to sys-tem. Policies of different users, programs, and systems may also interact to allow ordeny access. To model such decentralized policies, Abadi and others proposed logicswith formulas of the form K says A, where K is an agent or a system (abstractly calleda principal) and A is a formula representing a policy [6, 39]. The intended meaning ofthe formula is that principal K states, or believes that policy A holds. From a logicalperspective K says · is a modality and the logic is an indexed modal logic with onemodality for each principal. We call such a modal logic an authorization logic. In thepast fifteen years there have been numerous proposals describing authorization logicsthat differ widely in the specific axioms (or inference rules) used for K says · [2, 3, 8–10, 21, 23, 25, 31–33, 40, 41]. One emerging trend is the increased use of intuitionisticlogics for authorization (e.g., [3, 25, 29, 31–33, 40, 50]) as opposed to classical logics.This paper presents a new intuitionistic authorization logic called DTL0. This logicis peculiar in a certain respect: it abandons the usual objectivity in reasoning fromhypothesis, relativizing hypothetical reasoning to principals. The hypothetical judgmentof the logic has the form ΓK−→ A, which means, up to a first approximation, that principalK may reason from hypothesis Γ that A is true. While principal K reasons, K says Aimplies A for each A, thus making all policies local to K available. This may not betrue when another principal K0reasons. Reasoning of different principals may interactthrough the says connective. Although this choice of binding hypothetical reasoning toprincipals may be unintuitive from a philosophical point of view, it seems quite apt forreasoning about authorization policies.Our primary interest in developing DTL0is deployment in proof-carrying authoriza-tion [8–10, 40]. Hence our main focus is DTL0’s proof-theory, especially a natural deduc-tion system (with proof-terms) and a sequent calculus, which we describe in detail. Weprove several meta-theoretic properties of both formulations, including cut-eliminationfor the sequent calculus. We also present a Hilbert-style proof system for DTL0, and1sound and complete Kripke semantics. The principal-centric reasoning of DTL0reflectsin the Kripke semantics: worlds are explicitly associated with principals who may viewthem. This suggests that principals in DTL0may be related to nominals from hybridlogic [15, 20, 22]. We also show that DTL0is a generalization of constructive modalS4 [7, 46], and describe a sound and complete translation from DTL0to multi-modalconstructive S4.Besides investigating the theory of DTL0, a second goal of this paper is to understandhow the logic relates to existing authorization logics, and to the


Principal-Centric Reasoning in Constructive Authorization Logic

Download Principal-Centric Reasoning in Constructive Authorization Logic
Our administrator received your request to download this document. We will send you the file to your email shortly.
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 2 2 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?