On Formal Analysis of Cryptographic Protocols and Supporting Tool

Cryptographic protocols are crucial for secure communications and networks, distribution systems and electronic commerce. Model checking technique and supporting tool for analyzing cryptographic protocols are discussed. A model checking technique based on logic of algorithm knowledge for cryptographic protocols is proposed, which can specify explicitly the intruder model capabilities. The knowledge completeness of intruder abilities is proved. An efficient verification model generating system is developed based on PDL (Protocols description language) and SPIN/Promela for cryptographic protocols. Some optimization strategies are implemented in the system to reduce the state explosion complexity, such as partial order reduction, syntactic reorder and static analysis. More than ten cryptographic protocols are analyzed and published flaws are rediscovered successfully with the system. The verification system can be used as an efficient and reliable tool for evaluation of the network security.