Verification of Secure Inter-operation Properties in Multi-domain RBAC Systems

The increased complexity of modern access control (AC) systems stems partly from the need to support diverse and multiple administrative domains. Systems engineering is a key technology to manage this complexity since it is capable of assuring that an operational system will adhere to the initial conceptual design and defined requirements. Specifically, the verification stage of an AC system should be based on techniques that have a sound and mathematical underpinning. Working on this assumption, model checking techniques are applied for the verification of predefined system properties, and thus, conducting a security analysis of a system. In this paper, we propose the utilization of automated and error-free model checking techniques for the verification of security properties in multi-domain AC systems. Therefore, we propose a formal definition in temporal logic of four AC system properties regarding secure inter-operation with Role-Based Access Control (RBAC) policies in order to be verified by using model checking. For this purpose, we demonstrate the implementation of a tool chain for expressing RBAC security policies, reasoning on role hierarchies and properly feeding the model checking process. The proposed approach can be applied in any RBAC model to efficiently detect non-conformance between an AC system and its security specifications. As a proof of concept, we provide examples illustrating the verification of the defined secure inter-operation properties in multi-domain RBAC policies.