Name
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/SERE-C.2013.25 | Software Security and Reliability-Companion |
Keywords | Field | DocType |
multi-domain rbac systems,predefined system property,model checking technique,operational system,multi-domain ac system,model checking,ac system property,model checking process,rbac model,error-free model checking technique,ac system,secure inter-operation properties,security analysis,authorisation,systems engineering,formal specification,collaboration,verification,formal verification,computational modeling,access control,rbac,temporal logic | Model checking,Computer science,Role-based access control,Theoretical computer science,Formal specification,Runtime verification,Access control,Security policy,Temporal logic,Formal verification,Distributed computing | Conference |
ISBN | Citations | PageRank |
978-1-4799-2924-5 | 1 | 0.35 |
References | Authors | |
16 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Antonios Gouglidis | 1 | 58 | 9.82 |
| Ioannis Mavridis | 2 | 240 | 27.01 |
| Vincent C. Hu | 3 | 143 | 12.86 |