Analysis of the protocol JFK
In collaboration with Martín Abadi and Cédric Fournet, we
have analyzed the protocol JFK (Just Fast Keying), a proposed
replacement of IKE for IPsec.
A long version and a short version
of the paper are available.
Here are the ProVerif scripts for analyzing both variants JFKr and JFKi
The automatic verifier ProVerif is available
The distribution includes the scripts above in subdirectory proverif[version]/examples/pi/jfk and versions adapted for the typed front-end in proverif[version]/examples/pitype/jfk. To run ProVerif on these scripts, just run "./prepare" in the desired subdirectory and run ProVerif on the generated files (the files *.pi or *.pv, excluding the files *.m4.*).