ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2018, Vol. 55 ›› Issue (8): 1809-1825.doi: 10.7544/issn1000-1239.2018.20170250

Previous Articles    

Location-Constrained Access Control Model and Verification Methods

Cao Yan1, Huang Zhiqiu1,2,3, Kan Shuanglong1, Peng Huanfeng1,Ke Changbo1,4   

  1. 1(School of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106);2(Key Laboratory of Safety-Critical Software(Nanjing University of Aeronautics and Astronautics), Ministry of Industry and Information Technology, Nanjing 211106);3(Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing 210093);4(School of Computer Science, Nanjing University of Posts and Telecommunications, Nanjing 210023)
  • Online:2018-08-01

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

CLC Number: