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/examples/jfk. To run ProVerif on these
scripts, just run "./gen" in subdirectory proverif/examples/jfk
(under Unix or probably also under Cygwin).