Analysis of the protocol JFK

[Index]
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.

Software

The automatic verifier ProVerif is available here. The distribution includes the scripts above in subdirectory proverif/examples/jfk. To run ProVerif on these scripts, just run "./gen" in subdirectory proverif/examples/jfk (under Unix or probably also under Cygwin).
Bruno Blanchet