Research On Formal Security Verification Methods For The Design Of AKE Protocols In Industrial Internet Of Things

With the rapid development of Industrial Internet of Things technology,network information security issues have become increasingly prominent.The openness of industrial networks increases the attack surface,and the capability of attackers is also enhanced with the improvement of technology,making network security protection for the Industrial Internet of Things more challenging.Therefore,addressing security issues is crucial for the Industrial Internet of Things.Security protocols serve as basic and effective means to ensure system security,but various security threats exist in open networks.Attackers can target security protocols from multiple angles,exploiting design defects to render them ineffective.Considering that design defects in security protocols are difficult to identify manually,formal analysis methods and automated verification tools have become indispensable and effective means.Security protocols are designed for different scenarios and have distinct security requirements.Formal analysis must be goal-oriented,verifying various security attributes and expanding the description of attackers according to requirements.Among formal security protocol analysis methods,model checking-based approaches are the easiest to automate,leading to the emergence of numerous automatic protocol verification tools.However,the attacker models and algorithms adopted by these automated analysis tools lack scalability,unable to cope with new attack methods,and the protocol vulnerabilities discovered are not comprehensive enough.Consequently,Colored Petri Nets(CPN)and their development software,CPN Tools,have become one of the best solutions for studying formal security protocol analysis,offering outstanding modeling and detection capabilities,and ease of understanding.In this context,this thesis focuses on the formal analysis method of Colored Petri Nets(CPN)security protocol based on model checking,proposing a formal verification method of CPN based on Fail-stop security protocol.Using this as a guide,the authentication and key exchange(AKE)protocol scheme in the relevant literature of the Industrial Internet of Things M2M scenario is examined.After identifying problems such as insufficient security and heavy load,a lightweight anonymous AKE protocol for CoAP and general M2M scenarios is proposed to address these issues.The research results of this thesis provide a new theoretical basis for the design and formalization analysis and verification of Industrial Internet of Things security protocols.The main research contents are as follows:Firstly,this study investigates the modeling method of security protocol and attacker model,using the traditional TMN protocol as an example for CPN modeling and security analysis.The attacker model of Dolev-Yao is adopted,reflecting the attacker’s abilities in splitting,assembling,forwarding,and replaying protocol messages.Upon verifying the security design defects of the protocol,all corresponding attack paths are identified.Although this verification method meets the basic requirements of formal verification for security protocols,it presents problems such as high complexity and poor reusability,necessitating further improvement.Consequently,the study explores the method of extending the Dolev-Yao attacker model and improves the formal description method of attacker CPN.By setting the initial attacker knowledge base and updating it in real time,the second run effect of the protocol is realized in a single simulation.Building on the simplified CPN model,the verification range of protocol security is increased.This method verifies the security attributes and protocol resistance of the system in cases of partial "breach".Additionally,the improved method enhances the reusability of the method,enabling its application in the analysis and design of various security protocols.Secondly,a major obstacle for formalized methods based on model checking is the problem of state space explosion.To avoid model state space explosion,various solutions are investigated.In the modeling process of the TMN protocol,a“Line-up”control mode for secondary running is proposed.By controlling the synchronous progress of tokens,a large amount of useless state space caused by random ignition transitions of two processes is eliminated.However,in the proposed formal verification method of CPN based on the Failstop feature,the verification process is carried out incrementally based on protocol steps.The message of each step of the protocol is taken as the verification module,limiting the state space to a relatively confined range.Additionally,when discovering protocol vulnerabilities,the method of setting a Log fusion place enables efficient search and extraction of attack paths onthe-fly.Finally,using the CPN formal verification method for design guidance,two anonymous AKE protocols are proposed.The first protocol employs a lightweight elliptic curve algorithm to complete the AKE process in the form of pre-shared information.The second protocol,in combination with physically unclonable functions(PUFs),implements a more lightweight anonymous AKE scheme.Verified using the proposed CPN formalism method,both protocols are secure under the extended Dolev-Yao attacker model and possess the Fail-stop feature,allowing them to terminate the agreement in time and initiate corresponding processing when anomalies are detected.Simultaneously,the effectiveness of the improved CPN verification method is tested.Through continuous improvement,the method greatly enhances the efficiency of modeling and verification without weakening the attacker’s ability.