Visible to the public Modeling and Verifying Ticket-Based Authentication Scheme for IoT Using CSP

TitleModeling and Verifying Ticket-Based Authentication Scheme for IoT Using CSP
Publication TypeConference Paper
Year of Publication2021
AuthorsZhao, Chen, Yin, Jiaqi, Zhu, Huibiao, Li, Ran
Conference Name2021 IEEE Intl Conf on Parallel & Distributed Processing with Applications, Big Data & Cloud Computing, Sustainable Computing & Communications, Social Computing & Networking (ISPA/BDCloud/SocialCom/SustainCom)
Date Publishedsep
KeywordsAnalytical models, authentication, CSP, Data models, Data security, Internet of Things, IoT, Mobile handsets, Modeling, pubcrawl, resilience, Resiliency, security, System recovery, Trustworthy Systems, verification
AbstractInternet of Things (IoT) connects various nodes such as sensor devices. For users from foreign networks, their direct access to the data of sensor devices is restricted because of security threats. Therefore, a ticket-based authentication scheme was proposed, which can mutually authenticate a mobile device and a sensor device. This scheme with new features fills a gap in IoT authentication, but the scheme has not been verified formally. Hence, it is important to study the security and reliability of the scheme from the perspective of formal methods.In this paper, we model this scheme using Communicating Sequential Processes (CSP). Considering the possibility of key leakage caused by security threats in IoT networks, we also build models where one of the keys used in the scheme is leaked. With the model checker Process Analysis Toolkit (PAT), we verify four properties (deadlock freedom, data availability, data security, and data authenticity) and find that the scheme cannot satisfy the last two properties with key leakage. Thus, we propose two improved models. The verification results show that the first improved model can guarantee data security, and the second one can ensure both data security and data authenticity.
Citation Keyzhao_modeling_2021