Frank Pfenning
Carnegie
Mellon University

(joint work with Deepak Garg and Kevin Watkins)

Abstract:

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