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:
Our models run with CryptoVerif version 2.01.
- the cryptographic primitives and constants used in WireGuard (Section 2),
- the model of Curve25519 we created (Section 3.3),
- our indifferentiablity results, especially:
- exact probabilities instead of asymptotic versions (Section 4),
- proofs for all results (Appendix)
- a more explicit explanation how these results are
applied to WireGuard (Section 4).
- the guidance we use for one of our proofs (Section 6).
Archive containing all files mentioned below.
wireguard.cvl: the library of primitives as we use it for verifying
Models of WireGuard
We provide 5 main files, from which more models are generated using the
m4 preprocessor (see next subsection):
We include the main generated models in this distribution:
The file results summarizes the results obtained by running these
models in CryptoVerif.
- 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.
- WG.25519.correctness.m4.cv: the separate model for correctness we
describe in Section VI,
- WG.25519.dos.cv: the separate model for DOS we describe in Section
- WG.25519.identityhiding.m4.cv: the separate model for identity
hiding we describe in Section VI,
- 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.
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
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.
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,