January 2006, 23pp.
For the last three decades, since the seminal paper of Harrison et al, it appeared that formal verification of access control mechanisms might not be feasible. Their work was the first to formalise safety analysis of such systems and showed it is undecidable under a model commonly known as HRU. Research, aiming to find restricted versions of HRU that gain the decidability of this problem, yielded models without satisfactory expressive power for practical systems.
We introduce a new protection model which subsumes HRU, giving it semantics informally and in CSP. In addition, we introduce new safety properties and show that, though in terms of security they are stronger properties than the one defined under HRU, they can be automatically decided under our model and thus under HRU.