CMU-CS-07-166
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-07-166

Henry DeYoung, Deepak Garg, Frank Pfenning

February 2008

CMU-CS-07-166.pdf

Keywords: Access control logic, hybrid logic, temporal logic, proof-carrying authorization

We present an authorization logic that permits reasoning with explicit time. Following a prooftheoretic 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 the expressiveness of the logic through examples, including those with complex interactions between time, authorization, and mutable state.

95 pages


Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu