Research On Modeling And Verification Of Smart Home Access Control For Intra-domain And Inter-domain Security

With the rapid development of Internet of Things(IoT)technology,smart homes have been widely used.Smart homes not only significantly enhance comfort and convenience but also provide high-quality and diverse services through collaboration with other IoT systems,such as cross-domain access through joint smart healthcare systems for in-home care and medical services.However,as smart home applications bring convenience to daily life,they also pose security and privacy challenges.Within homes,traditional access control models cannot adequately balance rational authorization for multiple users with personal device privacy protection.In collaborative environments,a domain-interaction model is also required to assign access control policies for mobile subjects and access objects across multiple domains in response to complex cross-domain access requests.This article addresses the problems arising from traditional access control in smart homes,including the tedious assignment of multiple user device permissions,insufficient protection of personal device privacy,and the access control requirements of multi-domain cooperation spaces interacting with other IoT environments.Access control models and verification were developed and conducted for IoT domains and collaboration spaces in smart homes.The main research content of this article is as follows:(1)This article addresses issues in home IoT environments,such as limited computing and storage resources,cumbersome distribution of multiple user permissions,and insufficient device privacy protection,by analyzing and extending roles in the traditional RBAC model.The proposed domaininteraction RBAC-LE model introduces environment and device functional roles,integrates device permissions into functional roles,and combines them with contextual environments to enhance access control flexibility and reduce the complexity of permission distribution.By dividing devices into different regions and utilizing location attributes and device privacy roles to restrict user access,RBAC-LE effectively manages access permissions within homes from both functional and privacy perspectives.(2)To meet the access control requirements in multi-domain collaboration spaces formed by interactions between smart homes and other IoT environments,this article proposes the domaininteraction access control IDAC-TC model.The model establishes the mapping relationship between roles in different domain spaces to support cross-domain access requests.Meanwhile,the model uses a topological structure to represent the environmental characteristics of domain spaces,extracting topological attributes as contextual information for access control to constrain permission distribution and access behavior.Additionally,the model can achieve adaptive permission distribution based on topological structure changes to respond to changes in cross-domain behavior by access subjects.(3)This article verified the access control model using the USE tool,demonstrating the correctness and reliability of the proposed model.Additionally,a prototype system was developed,including modules for user management,device management,and intra-and inter-domain access control,with each module’s functionality validated.The results showed that the system is efficient and reliable,serving to enhance user security and privacy.