A Mechanised Cryptographic Proof of the WireGuard VPN Protocol

This page presents the CryptoVerif scripts for our analysis of WireGuard:

Benjamin Lipp, Bruno Blanchet, and Karthikeyan Bhargavan. A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. In: 4th IEEE European Symposium on Security and Privacy (EuroS&P'19), Stockholm, Sweden, June 2019.

A longer version of our paper contains more details on:

slides of the talk

Our models run with CryptoVerif version 2.01pl1.

Archive containing all files mentioned below.

Library file

wireguard.cvl: the library of primitives as we use it for verifying WireGuard.

Models

Models of WireGuard

The models

We provide 5 main files, from which more models are generated using the m4 preprocessor (see next subsection):
  1. WG.25519.m4.cv: this file serves to generate the files for variants 1, 2, and 3 of our model described in Section V.A. The beginning of this file contains comments on the m4 macros we use and how they influence which queries we prove in different models.
  2. WG.25519.correctness.m4.cv: the separate model for correctness we describe in Section VI,
  3. WG.25519.dos.cv: the separate model for DOS we describe in Section VI,
  4. WG.25519.identityhiding.m4.cv: the separate model for identity hiding we describe in Section VI,
  5. WG.25519.keysecrecy.m4.cv: this file serves to generate the model files for variants 1, 2, and 3 of our model, to prove key secrecy, described in Section VI.
We include the main generated models in this distribution: The file results summarizes the results obtained by running these models in CryptoVerif.

Running the proofs

The Bash script ./run can be used to generate all model files and run our entire analysis. It accepts two optional parameters. If none of them are given, the script generates the files for the AB-BA scenario (see below) and runs all the proofs in CryptoVerif.

The first parameter is AB or AB-BA and indicates whether the script models only sessions in which A is the initiator and B is the responder, or also sessions in which B is the initiator and A is the responder (accounting for the fact that WireGuard endpoints change roles during a long-term session). The script defaults to AB-BA.

The second parameter is true by default. If called with false, the script will only generate the models using the preprocessor m4, but not start their analysis using CryptoVerif.

Models on Indifferentiability

Run them with
./cryptoverif indiff_HKDF_1.ocv
./cryptoverif indiff_HKDF_2.ocv

The expected results are
RESULT Proved indistinguishability between game 28 and game 1 up to probability (2. * qH2 * qH1 + qH1 * qH1 + qH3 * qH3 + qH2 * qH3) / |output1|
All queries proved.

and
RESULT Proved indistinguishability between game 27 and game 1 up to probability (qH2 + 2. * qH2 * qH1 + qH2 * qH3) / |output1|
All queries proved.

Benjamin Lipp and Bruno Blanchet,