Model checking based on compositional reasoning for cryptographic protocols
Dengguo Feng · Journal of China Institute of Communications · 2003
A cryptographic protocol together with its cryptographic algorithm was regarded as one system, and based on compositional reasoning techniques, a formal model for the system was built. Using assume-guarantee based compositional reasoning techniques, a new assume-guarantee based reasoning rule and algorithm were proposed, and the soundness of the rule was proved. In realizing model checking to the cryptographic protocol system, several difficulties were solved such as decomposition of the system and generation of assumed function. Using this formal model and assume- guarantee based reasoning techniques, the kerberos v5 cryptographic protocol system was verified.