Automatic Security Protocol Verification Technique Based On Reinforcement Learning

Recent years,the issue of network security has become more and more serious,and the need of securing network is urgent.In order to solve this problem,researchers have designed various security protocols to enhance the security of network.However,many security protocols that have been put into practical applications cannot provide their de-clared security services at runtime.Therefore,security testing for security protocols has become an important part in testing.After researchers design or optimize a security pro-tocol,they need to further prove the security of the protocol.Compared with informal security protocol verification technique,formal methods can detect unknown vulnera-bilities in security protocols and software more comprehensively and in-depth.It can not only prove the security of security protocols,but also help to discover new meth-ods of attacking the protocols.However,due to the complexity of security protocols,existing formal method technique cannot fully automatically verify all security proto-cols.During verification,experts are required to assist the verification tool to complete the verification.Excessive labor cost and learning cost hinder the further development and application of formal method technique.To solve the above-mentioned problem and challenge,this dissertation focuses on the automatic security protocol verification technique,and carries on the following threefold research work:1.We propose a technique to fully automatically verify security protocols using dy-namic strategy,and then design and implement the corresponding prototype sys-tem.This technique solves the state space explosion problem in existing formal automatic verification.Compared with existing formal verification tools,the sys-tem can automatically search for the correct proof path without any human guid-ance.This work can discover all security vulnerabilities in the security protocol,given a security property,and ensure that the security protocol will not be com-promised by attackers.To the best of our knowledge,this system is the first to use dynamic strategy to fully automatically verifying security protocols.Exper-imental results show that the system achieves the generality and full automation in protocol verification,which greatly outperforms state-of-the-art tools.2.We propose a technique to formally modeling and verifying accountability proto-cols,and then design and implement the corresponding prototype system.To re-duce the complexity of modeling accountability protocols,this technique extends the applied pi calculus and automatically translates the calculus into ProVerif Ian-guage,where the abnormal operations and supplementary codes for modeling completeness are automatically generated.In particular,our definition of com-pleteness is general that it can cover all the disputing processes in existing ac-countability protocols.Experimental results show that the technique can be used to analyzing two typical accountability protocols and we further find weaknesses in the non-repudiation protocol.3.We propose a technique to formally verifying the 5G-AKA protocol.This tech-nique uses multiset rewrite rules to model the 5G-AKA protocol.The proto-col model is based on the four-party message interaction process in the protocol specification.The capabilities of attackers are more comprehensive than those defined by existing work.Security properties include secrecy,authentication-related properties,and privacy.Then,we verified the protocol model using a general and fully automatically verification tool,SmartVerif.The experimental results show that all the security properties in the 5G-AKA protocol model hold.In addition,we conducted a formal analysis of the 5G-AKA protocol using the previously defined accountability property,and we found that the protocol de-signers did not design a process for achieve accountability,and there were design flaws.To solve the problem,we modified the 5G-AKA protocol,and the modi-fied protocol was verified using SmartVerif.The verification results showed that the modified protocol guarantees the fairness and completeness of accountability.