We present a formal, logical framework for the representation and analysis
of an expressive class of authorization and obligation policies. Basic concepts of
the language and operational model are given, and details of the representation
are defined, with an attention to how different classes of policies can be written
in our framework. We show how complex dependencies amonst policy rules can
be represented, and illustrate how the formalization of policies is joined to a
dynamic depiction of system behaviour. Algorithmically, we use a species of
abductive, constraint logic programming to analyse for the holding of a number
of interesting properties of policies (coverage, modality conflict, equivalence of
policies, etc.). We describe one implementation of our ideas, and conclude with
remarks on related work and future research.