An authorization policy states the conditions under which an action is permitted or forbidden. In this dissertation, we use formal methods to ensure that policies written in certain languages are unambiguous and to provide provably correct algorithms for reasoning about policies. For example, we describe how questions about entailment, such as ``may Alice edit the database?'', can be answered efficiently.

We begin by showing that a fragment of first-order logic can be used to represent and reason about policies. Because we use first-order logic, policies have a clear syntax and semantics. We show that further restricting the fragment results in a language that is still quite expressive yet is also tractable. More precisely, questions about entailment can be answered in time that is a low-order polynomial (indeed, almost linear in some cases), as can questions about the consistency of policy sets.

In addition to developing our own language, we have examined two policy languages, XrML and ODRL. We focused on these languages because, when we began our work, they seemed to have the strongest support from industry. We found that the specifications for both languages have significant problems, which is not surprising since neither includes formal semantics. We discussed the problems that we found with the language developers and then proposed formal semantics for each language. We present our semantics here. In addition, we consider the complexity of determining if a permission is implied by a set of statements in each language. We prove that the general problem for XrML is undecidable and the general problem for ODRL is decidable and NP-hard. Finally, we define fragments of both languages that are fairly expressive and for which the problem is polynomial-time computable.