An Integrated Model to Analyze Cryptographic Protocols with Colored Petri Nets
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 Meadowscost-based framework in the formal analysis of security protocol. Based on Meadowsframework, we propose a formal model for JFK protocol with Colored Petri Nets.Moreovevr 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.
Just Fast Keying protocol (JFK) Cost-based Framework Colored Petri nets
Jin Wei Guiping Su Meng Xu
School of Information Science and Engineering, Graduate University of Chinese Academy of Sciences, Beijing
国际会议
11th IEEE High Assurance Systems Engineering Symposium(HASE 2008)(第十一届IEEE高可信系统工程国际研讨会)
南京
英文
457-460
2008-12-03（万方平台首次上网日期，不代表论文的发表时间）