Paper Info
Title
Modeling and Verifying Ticket-Based Authentication Scheme for IoT Using CSP
Abstract
Internet 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.
Year
DOI
Venue
2021
10.1109/ISPA-BDCloud-SocialCom-SustainCom52081.2021.00120
19TH IEEE INTERNATIONAL SYMPOSIUM ON PARALLEL AND DISTRIBUTED PROCESSING WITH APPLICATIONS (ISPA/BDCLOUD/SOCIALCOM/SUSTAINCOM 2021)
Keywords
DocType
ISSN
IoT, Authentication, Security, Modeling, Verification, CSP
Conference
2158-9178
Citations 
PageRank 
References 
0
0.34
0
Authors
4
Name
Order
Citations
PageRank
Chen Zhao100.34
Jiaqi Yin226.80
Huibiao Zhu328.48
Ran Li401.01