Abstract
Nowadays, DoS-resistant property has become more and more valuable for designing a cryptographic protocol. In this paper, we concentrate on the suitability of applying CPN Tools to merging Devel-Yao model into Meadows' cost-based framework in the formal analysis of security protocol. Based on Meadows' framework, we propose a formal model for JFK protocol with Colored Petri Nets. Moreover, we add the powerful intruder process followed with Devel-Yao model into the cost-based model developed earlier, and get a new integrated model, which could be formally analyzed with the simulation approach provided by CPN Tools, successfully verifying not only the DoS-resistant property by comparing the computational costs of initiator and responder in JFK, but also some security properties of JFK such as privacy, authentication.