Explicitly Timed Authorization Logic

December 1, 2008

Carnegie Mellon University

A document describes explicitly timed authorization logic (nicknamed "η-logic"). In prior authorization logics, it is, variously, impossible or difficult to handle time explicitly; express security policies that involve complex, time-dependent relationships; or reason accurately about time. By enabling explicit mention of time, η-logic makes it easier to reason about time-dependent consequences of policies.

This logic combines ideas from a prior authorization logic and prior hybrid and constraint-based logics. This logic has been made constructive to keep evidence as direct as possible and to include linearity to model consumable authorizations. This logic is designed to be deployed with proof-carrying authorization (PCA), according to which security policies are formalized in a logic and each access request is accompanied by a proof establishing that authorization follows logically from the policies, except that unlike in prior logics, the proof can be refined to mention that access is allowed at the time of the request.

The document follows a proof-theoretic approach leading to a meta-theory of η-logic. It shows that a reasonably expressive fragment of η-logic can be enforced straightforwardly in a PCA architecture. The expressiveness of η-logic is illustrated through examples.

This work was done by Henry DeYoung, Deepak Garg, and Frank Pfenning of Carnegie Mellon University.

CMU-0001