Research And Implementation Of Key Technologies For Formal Analysis Of Protocol Security

Various types of protocols are necessary for the normal operation of the network,and the security of these protocols is crucial for the overall security of the network environment.Formal analysis techniques can effectively discover vulnerabilities and weaknesses in protocols by formally describing,modeling,and verifying them.Therefore,formal analysis has been widely researched and applied.Although formal analysis methods perform well in detecting specification problems in the protocol itself,it is challenging to discover issues related to the security of the protocol’s surroundings.To address this problem,this paper studies the formal analysis process,proposes process standardization,and presents a specific point model for security assumptions.Based on this,the paper provides modeling schemes for various contents based on the ProVerif tool and comprehensively analyzes and evaluates the OIDC protocol to validate the feasibility of the proposed approach.The main contributions of this paper are as follows:1)In response to the lack of clear specifications in the formal analysis process,this paper proposes specifications and specific steps for the formal description and formal modeling in the process.Specific modeling schemes based on the Pro Verif tool are provided for various protocol contents.2)In response to the limitation of formal analysis methods in analyzing the security of the protocol’s surrounding,this paper proposes the concept of specific point in conjunction with security assumptions,and provides definitions and modeling schemes for the three types of special points identified.To maintain the simplicity and efficiency of the formal analysis process when introducing the specific point model,a modular modeling method based on orchestration mechanism is proposed.3)Based on the proposed methods,this paper conducts a comprehensive analysis of the OIDC protocol to verify the feasibility and significance of the methods.By reviewing the official standard and related materials of the OIDC protocol,the complete process of discovery,dynamic registration and the main part of the protocol under the three authentication authorization modes of the OIDC protocol are summarized and transformed into formal descriptions.Finally,based on the ProVerif,the security of the OIDC protocol was verified and analyzed under both the basic model and the specific point model,revealing multiple issues related to the security of the protocol’s surroundings.