Research On Formal Automatic Verification Optimization Of Network Security Protocols

The protocols to guarantee the security of network communication are network security protocols.Formal verification can be used to prove whether the network security protocols can guarantee that the security predicted at the beginning of the design will not change during the operation process.Formal verification means using mathematical methods to prove some abstract expression according to its formal attributes.Compared with non-formal verification,the formal verification methods can comprehensively detect unknown vulnerabilities in network security protocols and find new attack methods.The existing formal verification methods can be divided into manual verification,semiautomatic verification and automatic verification.Because the state space of network security protocols are difficult to be exhausted,so compared with manual and semiautomatic verification methods,the automatic verification methods need more complex algorithm design to reduce the search scope of state space as much as possible.However,the automatic verification has the advantage of not requiring the prior knowledge of the formal domain and is contribute to the rapid development and wide application of the network security protocols.Among the existing tools for fully automatic formal verification of network security protocols,SmartVerif can verify the most kinds of network security protocols.However,SmartVerif has some defects,such as long verification time for network security protocol and lack of generality of the neural network used by the framework.The experimental results show that,after the improvement of the work in this dissertation,the verification time of the automatic formal verification framework is shorter than that of the original scheme.At the same time,it makes the network universal and can verify more kinds of network security protocols.The specific work of this dissertation is:1.In this dissertation,a tree form structure transformation technique for constraint solving rules is proposed.Because a lot of highly abstract data are generated during formal verification,a more appropriate data structure is needed to express the formal semantics of the data more explicit.In the tree form data,each node contains two attributes,one is part of the string in the original formal data,the other is the corresponding formal semantics of the string.The formal semantic information of data can be expressed more explicit by the way of tree form data transformation.And when the formalized data is transformed into the input vector of neural network,more formalized features of data can be retained.It is also helpful to judge the formal semantic uniformity of data.2.This dissertation optimizes the cyclic path determination algorithm in proving theorem tree.Cyclic proof is a common problem in automatic formal verification,which is reflected in the formal verification tool used in this dissertation.Cyclic path is generated in the theorem tree.In order to ensure the high efficiency and accuracy of network security protocols verification,it is necessary to detect the loop path as early and accurately as possible.The optimization algorithm can improve the accuracy of non-cyclic path determination,so that the network security protocol used in the current experiment does not occur error verification.3.This dissertation optimizes the deep reinforcement learning algorithm in formal automatic verification.The optimal algorithm makes use of the tree form transformation of constraint solving rules,which can retain more invariant formal features in constraints when embedding into vector space,so that the network can learn the formal features of data.The optimal algorithm also uses the reinforcement learning framework based on Monte Carlo tree search,which makes the neural network universal.Therefore,multiple network security protocols can be used to train a neural network,and the neural network can be used to verify the new network security protocols.The optimal algorithm provides a more effective feedback setting for neural network training,which can accelerate the convergence process of neural network.