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 of JFK.


The automatic verifier ProVerif is available here. 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.*).
Bruno Blanchet