Research On Planning-based Automatic Verification Technology For Cryptographic Protocols

In recent years, automatic verification technology obtains more and more attentions, and comes to be a hotspot in the research area of cryptographic protocols. By taking sufficient account of the running characteristics and laws of cryptographic protocols, the dissertation does profound research on the formal model of cryptographic protocols and its verification mechanisms and algorithms based on planning theory. The main contributions of the dissertation are summarized as follows:1. Review of relative research status quo.The existing research results of Formal analytical methods and automatic verification tools of cryptographic protocols and intelligence planning theory are reviewed, among which research hotspot and shortage of these areas are analyzed.2. Research on the formal model of cryptographic protocols.Planning theory is brought into the area of formal analysis for cryptographic protocols. Based on the running characteristics and laws of cryptographic protocols, attack planning theory for cryptographic protocols is presented, and a formal model for verifying security of cryptographic protocols is established, including its basic assumptions, first-order syntax, formal definition and operational semantics. Then the concrete procedure for establishing the model is expatiated based on NS public-key protocol.3. Research on the improving strategy of Dolev-Yao Model.The shortages of classical Dolev-Yao Model are analyzed, and then Dolev-Yao model is improved based on basic message element strategy. The feasibility is guaranteed by extending the semantic of application, which avoids the occurrences of "state space explosion" problem, and enhances the completeness of attack planning problem model of cryptographic protocols.4. Research on security verification mechanism of cryptographic protocols.Based on profound analysis of characteristics of attack planning problem model of cryptographic protocols, a SAT based automatic verification mechanism of the model is presented and proved to be sound and complete formally.5. Research on security verification algorithms of cryptographic protocols.Based the aforementioned mechanisms, automatic verification algorithms of attack planning problem model of cryptographic protocols are studied and designed, including the respective sub-algorithms of planning graph extending phase, SAT encoding phase and SAT solving phase, and correctness of SAT encoding algorithm is proved. During SAT solving phase, WalkSAT algorithm is improved by clause weight and learning mechanism, and then the improved algorithm is applied to solve SAT problem. 6. Design and implementation of automatic verification prototype system of cryptographic protocols.Based on attack planning problem model of cryptographic protocols and its automatic verification mechanism and algorithms, an automatic verification prototype system of cryptographic protocols, namely ACPV, is designed and implemented, and its efficiency is tested.