Title :
The Modeling Analysis of Cryptographic Protocols using Promela
Author :
Xiao, Meihua ; Li, Jing
Author_Institution :
Sch. of Inf. Eng., Nanchang Univ.
Abstract :
The analysis and verification of security protocols is an important field in the security of computer nowadays. Model checking technique to the analysis of security protocols has proved remarkably successful, which involves three parts: modeling of system behaviors, description of system properties and system verification. Modeling of system behaviors is a highly challenging task because of its complexity, especially modeling of intruder capability. A general method is proposed to construct a Promela model of the cryptographic protocol, and make use of this way to model the Helsinki protocol. The Promela model of Helsinki protocol is automatically verified by model checker Spin and an attack to Helsinki protocol has successfully been found. Experimental result shows the verification validity via message sequence chart. The general method may become a good guideline for verifying similar cryptographic protocols
Keywords :
cryptography; formal verification; protocols; Helsinki protocol; Promela; cryptographic protocol; formal method; model checker Spin; model checking technique; security protocol; system behavior modeling; system property description; system verification; Computer science; Computer security; Cryptographic protocols; Cryptography; Electronic mail; Guidelines; IP networks; Information analysis; Information security; Laboratories; Cryptographic protocol; formal method; model checking;
Conference_Titel :
Intelligent Control and Automation, 2006. WCICA 2006. The Sixth World Congress on
Conference_Location :
Dalian
Print_ISBN :
1-4244-0332-4
DOI :
10.1109/WCICA.2006.1713191