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.

JFKr
JFKi
Script for the proof of Lemma 3
Script for the proof of Lemma 9

Software

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