A Mechanised Cryptographic Proof of the WireGuard VPN Protocol

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:

• the cryptographic primitives and constants used in WireGuard (Section 2),
• the model of Curve25519 we created (Section 3.3; it fixes a problem in that model in the conference version),
• 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).

Our models run with CryptoVerif version 2.01pl1.

Archive containing all files mentioned below.

Library file

Models

Models of WireGuard

The models

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.

• Models generated from 1)
  • Variant 1) of Section V.A, with the 4 compromise scenarios:
    • WG.25519.AB-BA.S_i_compr.S_r_compr.replay_prot.cv static keys dynamically compromised
    • WG.25519.AB-BA.S_i_compr.E_r_compr.replay_prot.cv A's private static key dynamically compromised and B's ephemeral compromised
    • WG.25519.AB-BA.E_i_compr.S_r_compr.replay_prot.cv B's private static key dynamically compromised and A's ephemeral compromised
    • WG.25519.AB-BA.E_i_compr.E_r_compr.replay_prot.cv ephemerals compromised
    • WG.25519.AB-BA.1st_msg.replay_prot.cv Model for the replay protection for the 1st message, with ephemerals compromised
  • Variant 2) of Section V.A (PSK secure, all other keys compromised) WG.25519.AB-BA.only_psk.replay_prot.cv
  • Variant 3) of Section V.A (all keys compromised) WG.25519.AB-BA.uniquesession_chbinding_weakUKS.replay_prot.cv
• WG.25519.AB-BA.correctness.replay_prot.cv generated from 2),
• WG.25519.AB.identityhiding.replay_prot.cv generated from 4).
• Models generated from 5), similar to those generated from 1):
  • WG.25519.keysecrecy.AB-BA.S_i_compr.S_r_compr.replay_prot.cv
  • WG.25519.keysecrecy.AB-BA.S_i_compr.E_r_compr.replay_prot.cv
  • WG.25519.keysecrecy.AB-BA.E_i_compr.E_r_compr.replay_prot.cv
  • WG.25519.keysecrecy.AB-BA.E_i_compr.S_r_compr.replay_prot.cv
  • WG.25519.keysecrecy.AB-BA.1st_msg.replay_prot.cv
  • WG.25519.keysecrecy.AB-BA.only_psk.replay_prot.cv
  • WG.25519.keysecrecy.AB-BA.uniquesession_chbinding_weakUKS.replay_prot.cv

Running the proofs

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

• The file indiff_HKDF_1.ocv proves Lemma 4 of our paper.
• The file indiff_HKDF_2.ocv proves Lemma 5 of our paper.