Conformance checking of RBAC policy and its implementation

The purpose a security policy is to specify rules to govern access to system resources preferably without considering implementation details. Both policy and its implementation might be altered, and after introducing changes, it is not obvious that, they are consistent. Therefore, we need to validate conformance between policy and its implementation. In this paper we describe an approach based on finite-model checking to verify that a RBAC implementation conforms to a security policy. We make use of the model-checking system SPIN, and show how to express RBAC policy constraints by means of LTL and how to model an RBAC implementation in SPIN's internal modeling language PROMELA.