Research On Planning Theory And Algorithm For Cryptographic Protocol Attacks

Based on the running characteristics of cryptographic protocols, the dissertation does profound research on the formal model of cryptographic protocols, mechanism for cryptographic protocol attacks and corresponding planning algorithms using planning theory. The main contributions of the dissertation are summarized as follows:1. Review of relative research status quo.The existing research results of cryptographic protocol formal analytical methods, intelligent planning theory and its applications in the cryptographic protocol formal analysis are reviewed, among which research hotspot and shortage of these areas are analyzed.2. Research on attack planning theory for cryptographic protocols.Using intelligent planning theory, combined with the running characteristics of cryptographic protocols, attack planning theory for cryptographic protocols is presented, an attack planning problem model for cryptographic protocols is established, its basic assumptions, first-order syntax, and operational semantics are given. Based on Dolev-Yao attacker model, improving strategies for attacker action application are proposed, and an attack planning system for cryptographic protocols is established.3. Research on algebra semantics of cryptographic protocols.The algebra properties of cryptographic protocol message term structure are studied, algebra freeness hypotheses for primitive operation are proposed, attacker's computation ability and behavior are discussed from the point of algebra, the principals'behavior and operations are represented by transference functions, moreover, the formal semantics of the cryptographic protocol running process is given by function sequence, the soundness of attack planning system for cryptographic protocols is formally proved by equivalent transformation in algebra.4. Research on planning algorithms for cryptographic protocol attacks.Based on characteristics analysis of the attack planning problem model for cryptographic protocols, a SAT based planning mechanism for cryptographic protocol attacks is proposed, a set of planning algorithms for cryptographic protocol attacks are designed. The research emphases are put on planning graph construction algorithm which is based on mutex exclusion and node validity analysis policies, SAT encoding algorithm which is based on overloaded splitting action representation and extended coding axioms, SAT solving algorithm which is based on learching mechanism and space complexity optimization measurement.5. Design and implementation of cryptographic protocol attack planning system. Based on cryptographic protocol attack planning theory and algorithms, a planning prototype system for cryptographic protocol attacks is designed and implemented, and its efficiency is proved.