A topology-aware access control model for collaborative cyber-physical spaces: Specification and verification

In collaborative environment, distributed multiple cyber-physical spaces interoperate with each other aiming to provide an intelligent spatial environment for their users to conduct their collaborative activities. Subjects and objects roam in the physical and cyber spaces among domains to support the completion of the activities. These dynamic behaviors bring great challenges to security issue. The actions of roaming subjects and roaming objects need to be specified and checked against security requirements of constituent domains. However, the existing inter-domain access control models was proposed for the traditional information system and focus on the cyber security. They cannot deal with the intricacies of cross-domain access requests in cyber-physical spaces. In this paper, we propose a formal inter-domain model to specify cyber-physical access control policies and a model checking approach to ensure security requirements hold in these policies. We first present a formal definition of the topology configuration to capture the environment characteristics of the cyber-physical spaces. It provides important contextual information for the access control system. Then, based on topology attributes defined in the topology configuration, a topology-aware inter-domain access control model TA-CPAC is proposed. It can adjust the permission assignment adaptively to react to the behaviors changes of subjects and objects. Next, the topology configuration and TA-CPAC model are formalized by the use of bigraphs and bigraphs reactive systems respectively, which allows us to utilize the model checking technology to reason about that whether the behaviors of roaming subjects and objects satisfy security requirements of all constituent domains. Finally, the effectiveness of our approach is evaluated by a collaborative scenario in a smart city. (C) 2019 Elsevier Ltd. All rights reserved.