Home > Research > Publications & Outputs > Verification of secure inter-operation properti...
View graph of relations

Verification of secure inter-operation properties in multi-domain RBAC systems

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Close
Publication date06/2013
Host publicationSoftware Security and Reliability-Companion (SERE-C), 2013 IEEE 7th International Conference on
PublisherIEEE
Pages35-44
Number of pages10
ISBN (print)9781479929245
<mark>Original language</mark>English
Event2013 IEEE 7th International Conference on Software Security and Reliability-Companion (SERE-C) - Gaithersburg, MD, USA, United Kingdom
Duration: 18/06/201320/06/2013

Conference

Conference2013 IEEE 7th International Conference on Software Security and Reliability-Companion (SERE-C)
Country/TerritoryUnited Kingdom
Period18/06/1320/06/13

Conference

Conference2013 IEEE 7th International Conference on Software Security and Reliability-Companion (SERE-C)
Country/TerritoryUnited Kingdom
Period18/06/1320/06/13

Abstract

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.