Formal Security Analysis and Improvement Based on LonTalk Authentication Protocol

Security analysis of security protocol can be used to ensure communication security in the network. The process of security protocol analysis using the formal analysis method is simple and standardized, which is a research hotspot in the field of information security. In this study, a formal analysis method based on colored Petri net theory and Dolev-Yao attacker model is adopted to analyze LonTalk authentication protocol, and three types of attackable vulnerabilities including replay, tamper, and spoofing are found in LonTalk authentication protocol; thus, a secure LonTalk-SA authentication protocol is proposed. The LonTalk-SA authentication protocol was added with a trusted third-party server, which authenticates the identity of the sender and receiver and generates session keys through XOR operations on random numbers. The formal analysis of the new scheme shows that the new scheme can effectively resist three types of attacks, provide bidirectional authentication of communication nodes, and ensure the confidentiality, integrity, and authentication of messages during transmission, thus improving the security of protocols.