Name
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/HASE.2008.23 | HASE |
Keywords | Field | DocType |
colored petri nets,just fast keying protocol,security protocol,cost-based model,intruder process,petri nets,jfk protocol,dos-resistant property,just fast keying protocol (jfk),cost-based framework,cryptographic protocol,integrated model,formal analysis,cryptographic protocols,devel-yao model,new integrated model,analyze cryptographic protocols,cpn tools,formal model,security,computational modeling,protocols,modeling | CPN Tools,Authentication,Petri net,Cryptographic protocol,Computer science,Colored petri,Security properties,Merge (version control),Distributed computing | Conference |
ISSN | ISBN | Citations |
1530-2059 | 978-0-7695-3482-4 | 1 |
PageRank | References | Authors |
0.38 | 4 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Wei Jin | 1 | 83 | 25.25 |
| Guiping Su | 2 | 13 | 2.36 |
| Meng Xu | 3 | 2 | 0.73 |