25/02/2010, 18:00 — 19:00 — Room P4.35, Mathematics Building
Frank Pfenning, Carnegie Mellon University
Reasoning about the Consequences of Authorization PoliciesinaLinear
Epistemic Logic
Authorization policies are not stand-alone objects: they are used
to selectively permit actions that change the state of a system.
Thus, it is desirable to have a framework for reasoning about the
semantic consequences of policies. To this end, we extend a
rewriting interpretation of linear logic with connectives for
modeling affirmation, knowledge, and possession. To cleanly confine
semantic effects to the rewrite sequence, we introduce a monad. The
result is a richly expressive logic that elegantly integrates
policies and their effects. After presenting this logic and its
metatheory, we demonstrate its utility by proving properties that
relate a simple file system's policies to their semantic
consequences. This talk represents joint work with Henry DeYoung.
Note exceptional week day, time and location. Joint session with the Logic and Computation Seminar.
