Information Security Seminar 

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.