(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
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
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.
of Programming Seminars
July 13, 2005
Wean Hall 8220