Application And Research Of Security Protocol Formal Analysis Technology

Security protocols use cryptographic algorithms to achieve security goals such as authentication and key distribution.However,the security protocols themself still have security risks.All kinds of attacks on the security protocol have led to the disclosure of personal,enterprise,or national confidential infor-mation and have resulted in property losses.With the help of computers and mathematics,the formal method can automatically,quickly,and comprehen-sively analyze the security protocols,find the vulnerabilities in security pro-tocols and prove the security properties of the protocols.The formal method has been applied to the analysis of a large number of protocols since it was proposed,which has promoted the research and development of security proto-cols.However,the current development of the formal method is still not mature enough.In this paper,we focus on the research of the formal method of security protocols.We deeply discuss the principles of the ProVerif formal tool and propose an analysis method for security protocols by using the ProVerif tools.We verify the FIDO UAF protocol with this method and present the evaluation.Besides,we present the defects of the ProVerif tools and the formal analysis methods and put forward the improvement recommendation.The main work and innovation of this paper include:(1)We propose a method of analyzing security protocol based on the ProVerif tool.This method proposes the modeling method of the malicious entities under the inter-process communication model,the verification method of unlinkability,and the analysis method of minimal assumptions.(2)We formally verify the UAF protocol with our method.First,we formally translate the protocol flow,security assumptions,security proper-ties from the UAF documents to formal expressions.Second,we propose the ProVerif model of the UAF protocol.Then,the UAFVerif tool is devel-oped to analyze all possible UAF protocol scenarios and automatically find the minimal security assumptions of the protocol.According to the conclu-sion of minimal assumptions,several types of attacks towards the UAF pro-tocol are proposed.We successfully implemented one type of attack on two types of android APPs and obtained one CNNVD vulnerability ID.Finally,we put forward suggestions to the UAF protocol for improvement.(3)We summarize the defects of the ProVerif tool and formal analysis method and present the improvement plans.The defects include that the ProVerif is difficult to support protocol analysis under the non-Dolev-Yao model,does not support complex mathematical operation and counter model,does not sup-port authentication analysis under variable entity operation and is difficult to support analysis under corrupt entity attack scenarios,and so on.