A Formal Model for Cryptographic Protocols Based on Planning Theory

Planning theory is brought into the area of formal analysis for cryptographic protocols. Based on the running characteristics and laws of cryptographic protocols in the real networks, an attack planning theory for cryptographic protocols is presented, and a formal model, namely attack planning problem model of cryptographic protocols, is established for verifying the security properties of cryptographic protocols, including its first-order syntax, formal definitions and operational semantics. Meanwhile, the shortages of classical Dolev-Yao model are analyzed, and then the Dolev-Yao model is improved based on the basic message element strategy, which avoids the occurrences of “state space explosion” problem and enhances the completeness of attack planning problem model of cryptographic protocols. The feasibility of the improved Dolev-Yao model is guaranteed by extending the semantic of application. Finally, an instance for analyzing the NS public-key protocol based on the attack planning problem model is shown to illustrate the model utility. The formal model for cryptographic protocols presented, whose purpose is to verify cryptographic protocols and find the faults existing in them, is to prove faultiness, and can be conveniently used for both manual deductions and automatic implementations.