Abstract: With the advent of Internet of things and cyber-physical systems, location-constrained access control systems need to consider security requirements of cyber spaces and physical spaces simultaneously, because the boundary between the physical and the cyber world becomes unclear in these new paradigms. However, the most existing access control models consider physical and cyber security separately, and they are oblivious to cyber-physical interactions. Authorization models are needed to help the security policy design and express higher-level organizational security rules. Firstly, the environment model (EM) and location-constrained role-based access control (LCRBAC) model are proposed. The environment model is presented for describing the static topology configuration of cyber space and physical space. The LCRBAC model is used to describe dynamic behaviors of cyber entities and physical entities. Secondly, given the bigraphs and bigraphs reactive systems that describe the environment configuration and entities behaviors respectively, a labeled transition system is obtained by applying reaction rules to the environment configuration. Thirdly, policy modification proposals are proposed for deadlock states, violation states, and unreachable states based on the verification results on the labeled transition system. Finally, a case study concerned with a bank building automation access control system is conducted to evaluate the effectiveness of the proposed approach.

Key words: location-constrained access control system, model checking, bigraphs, reaction rules, verification