Access control is ubiquitous to the extent that we hardly perceive its presence in our activities--from who we give our house keys to, to who can authorize the publication of article reviews on a Web site. In light of this, the relative paucity of logical frameworks for reasoning about access controls is perhaps quite surprising.

Collinson and Pym propose one such logical framework for modeling and reasoning about access control. Compared to earlier efforts, which focused on just a logic, the focus of this work is on the joint development of an operational model and a logic for access control. The operational model is based on the SCRP calculus that delineates the passive notion of a resource from that of an active process. The logic is based on a variant of the logic of bunched implications. The surprising fact is that this entire framework is highly coherent, as demonstrated by a Hennessy-Milner-style equivalence between the logic and the calculus.

The paper builds on the authors’ earlier work on the calculus (SCRP) and the logic (MBI) of resources and processes. The important notion of a role is modeled by introducing a process connective into the calculus, and the “says” modality in the modal logic. This notion of a role is inspired from an earlier similar notion [1]. There seem to be some differences between the two notions, but the authors do not dwell on these differences.

The bulk of the paper is given over to examples of how the theoretical framework can be used to reason about access control decisions. A number of scenarios are studied and modeled, starting with very simple resource models and culminating in a sophisticated example where the resource component models the beliefs of the various entities in the scenario considered. These examples clearly bring out the significance of the work, providing both an assembly language for performing access control and an associated logic for reasoning about the access control actions.