Modeling and Verifying Ticket-Based Authentication Scheme for IoT Using CSP

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.