Principal-Centric Reasoning in Constructive Authorization Logic

Abstract

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

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 14, 2009
Accession Number
ADA506999

Entities

People

  • Deepak Garg

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Calculus
  • Computer Access Control
  • Computer Science
  • Computers
  • Construction
  • Cybersecurity
  • Elimination
  • Identities
  • Judgment
  • Language
  • Notation
  • Reasoning
  • Semantics
  • Simulations
  • Standards
  • Test And Evaluation
  • Translations

Readers

  • Artificial Intelligence
  • Computer Engineering
  • Mathematical Modeling and Probability Theory.