Formal Modeling And Verification Of Ticket-Based Authentication Scheme For IoT Using CSP

Internet of Things(IoT)connects various nodes that include sensor devices,and it provides users with convenient information services.However,the rapid growth of IoT also brings many security challenges,and authentication is one of the key technologies to solve the security problems in IoT.In the reasearch on IoT authentication,authenticaition schemes for different application scenarios have been proposed by researchers.Through the mutual authentication of the sensor device and the mobile device of the foreign network user,the ticket-based IoT authentication scheme solves the problem that the access of foreign network user to the data of sensor device is restricted due to security considerations.This scheme with various new features effectively fills a gap in the research on IoT authentication,but there is still no research on the formal verification and analysis of the scheme.Therefore,it is of great significance to study the security and reliability of the scheme from the perspective of formal methods.This thesis uses the Communicating Sequential Processes(CSP)in the formal methods to model and analyze the scheme.By abstracting the entities in the scheme into processes,describing the behavior,communication and interaction of entity processes in detail,and introducing the intruder into the model to simulate network attacks,we complete the overall modeling of this scheme.Considering the possibility of key leakage caused by many kinds of security threats in the real IoT,we also build formal models for the situation where the key used in this scheme is stolen by the intruder.Then,we use the model checker Process Analysis Toolkit(PAT)to implement the models and verify the four properties that the scheme needs to satisfy,including deadlock freedom,data availability,data security and data authenticity.Through property verification,we find that the scheme cannot satisfy data security and data authenticity in the case of key leakage.We analyze the verification results detailedly,and give the intruder attack methods that lead to the dissatisfaction of these two security properties.Finally,in order to enhance the security of this scheme,we propose two practical improvements to the scheme.The first improvement mainly uses nonce,with the help of public key cryptography.The second improvement is mainly based on previous nonce.The verification results show that the scheme after the first improvement can ensure data security,and the scheme after the second improvement can guarantee data security and data authenticity at the same time.The results show that our improvement methods can effectively improve the security of this scheme and make the scheme can be more reliably applied in practical IoT scenarios.