An Authorization Logic with Explicit Time

Abstract

We present an authorization logic that permits reasoning with explicit time. Following a proof-theoretic approach, we study the meta-theory of the logic, including cut elimination. We also demonstrate formal connections to proof-carrying authorization's existing approach for handling time and comment on the enforceability of our logic in the same framework. Finally, we illustrate including those with complex interactions between time, authorization, and mutable state.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 02, 2008
Accession Number
ADA476804

Entities

People

  • Deepak Garg
  • Frank Pfenning
  • Henry Deyoung

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Calculus
  • Computer Access Control
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Elimination
  • Hypotheses
  • Identities
  • Intervals
  • Judgment
  • Language
  • Linearity
  • Reasoning
  • Security
  • Students
  • Time Intervals

Fields of Study

  • Computer science

Readers

  • Government and Public Administration Law.
  • Mathematical Modeling and Probability Theory.
  • Theoretical Analysis.