Security Analysis of JFK Protocol
Zhaoxiong Chen · Mini-micro Systems · 2005
This paper defines a new ideal notion of strand spaces. The corresponding propositions and theorems are also extended so that Strand Spaces can be applied to analyzing some complex security protocols which include plenty cryptographic primitives. Then JFK. a new proposed key exchange protocol for IPsec, is analyzed via this extended Strand Spaces. The paper focuses on the protocol's core security properties: keys' secrecy and authentication's correctness. Through the analysis it is proved that JFK can achieve its security goals. The analysis also gives a steady foundation for more application of the extended Strand Spaces.