Accession Number : ADA476804


Title :   An Authorization Logic with Explicit Time


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE


Personal Author(s) : DeYoung, Henry ; Garg, Deepak ; Pfenning, Frank


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a476804.pdf


Report Date : 02 Feb 2008


Pagination or Media Count : 96


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.


Descriptors :   *REASONING , *TIME , *LOGIC , CONTROL , THEORY , ELIMINATION , COMPUTER ACCESS CONTROL , HYBRID SYSTEMS , LINEARITY , SECURITY , INTERACTIONS


Subject Categories : Computer Systems Management and Standards


Distribution Statement : APPROVED FOR PUBLIC RELEASE