Analysis of the protocol JFK
![[Index]](../flech_g.gif)
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