On the Decidability of the Safety Problem for Access Control Policies

13 years 4 months ago

Download hal.archives-ouvertes.fr

An access control system regulates the rights of users to gain access to resources in accordance with a speciﬁed policy. The rules in this policy may interact in a way that is not obvious via human inspection; there is, therefore, a need for automated veriﬁcation techniques that can check whether a policy does indeed implement some desired security requirement. Thirty years ago, a formalisation of access control presented a model and a safety speciﬁcation for which satisfaction is undecidable. Subsequent research, aimed at ﬁnding restricted versions that obtain the decidability of this problem, yielded models without satisfactory expressive power for practical systems. Instead of restricting the model, we reexamine the safety speciﬁcation. We develop a new logic that can express a wide variety of safety properties over access control systems, and show that model checking is decidable for a useful fragment of this logic.

E. Kleiner, T. Newcomb

Real-time Traffic