We present a model of access control which provides fine-grained data-dependent control, can express permissions about permissions, can express delegation, and can describe systems which avoid the root-bottleneck problem. We describe a language for describing goals of agents; these goals are typically to read or write the values of some resources. We provide a decision procedure which determines whether a given coalition of agents has the means (possibly indirectly) to achieve its goal. This question is decidable in the situation of the potential intruders acting in parallel with legitimate users and taking whatever temporary opportunities the actions of the legitimate users present. Our technique can also be used to synthesise finite access control systems, from an appropriately formulated logical theory describing a high-level policy. As well as the verification tool, we have developed a tool which can translate the access control policy in to XACML, a language for specifying access control systems which can be used to generate Java code.

Joint work with Dimitar Guleuv and Nan Zhang.