Frank Pfenning
Carnegie Mellon University
(joint work with Deepak Garg and Kevin Watkins)


Authorization logics are traditionally used to specify access control policies.  More recently, in the proof-carrying authorization architecture, they have also been employed directly to enforce policies via explicit checking of proofs expressed in the logic.  Authorization logics provide a great deal of flexibility, but this may make it difficult for principals to understand the consequences of their policy decisions and for users to obtain the necessary proof objects.

In ongoing work we investigate a new constructive foundation for authorization logics which makes it easier to construct them modularly and to reason about them mechanically.  At the core is the separation of judgments from propositions and a lax modality indexed by principals.  We have formally verified some properties of the core logic itself, such as cut-elimination, and we are now interested in methods for establishing properties of policies expressed in the logic, such as independence and non-interference.
In this talk we explain the underlying design philosophy and the indexed lax logic at the heart of our approach.  We also give a brief survey of the technical results obtained so far.

Principles of Programming Seminars

July 13, 2005
3:30 p.m.
Wean Hall 8220