Formal Verification
WireGuard has undergone all sorts of formal verification, covering aspects of the cryptography, protocol, and implementation. Below details the various efforts.
Symbolic Verification of Protocol using Tamarin
The WireGuard protocol, described in the technical paper, and based on Noise, has been formally verified in the symbolic model using Tamarin. This means that there is a security proof of the WireGuard protocol. The protocol has been verified to possess the following security properties:
- Correctness
- Strong key agreement & authenticity
- Key-compromise impersonation resistance
- Unknown key-share attack resistance
- Key secrecy
- Forward secrecy
- Session uniqueness
- Identity hiding
This is joint work of Jason Donenfeld and Kevin Milner.
These results are extensively discussed in the WireGuard formal verification paper. This paper is a draft work in progress, but the main results are there.
Read the WireGuard Tamarin verification paper
The Tamarin Model
The Tamarin model is open source and can be re-run for independent verification:
$ git clone https://git.zx2c4.com/wireguard-tamarin/
$ cd wireguard-tamarin
$ make
This requires Tamarin, m4, GraphViz, and Maude.
Computational Proof of Protocol in eCK Model
In attempting construct a computational proof of WireGuard in the eCK model, it turns out that the WireGuard protocol does not fit cleanly into the traditional eCK model, because the key confirmation message is part of the transport layer. So, this paper instead proves a variant of the WireGuard protocol, which is morally equivalant to the actual protocol, producing a very strong result.
This is joint work of Benjamin Dowling and Kenneth G. Paterson.
Read the WireGuard Computational eCK Model Proof paper
Computational Proof of Protocol in ACCE Model
This thesis constructs a mechanised cryptographic proof of the entire WireGuard protocol, including transport data messages, in an ACCE-like computational model using CryptoVerif. The properties proved are:
- Correctness
- Message secrecy
- Forward secrecy
- Mutual authentication
- Key-compromise impersonation resistance
- Unknown key-share attack resistance
- Replay resistance of the first protocol message
The model is available for download and may be used in CryptoVerif 2.00.
This is the work of Benjamin Lipp.
Read the WireGuard Computational ACCE Proof paper
Symbolic Verification of Protocol using ProVerif
The Noise Explorer project seeks to formally verify all Noise protocol patterns by generating ProVerif models. The model relevant to WireGuard is Noise Explorer's model of IK, which may be plugged into ProVerif to generate proofs for various properties.
This is the work of Nadim Kobeissi and Karthikeyan Bhargavan.
Verified C Implementation of Curve25519
HACL*
WireGuard makes use of HACL*'s 64-bit Curve25519 scalar multiplication implementation. The curve is specified in F*, which is then able to prove things about implementation strategies. KreMLin lowers it down to verified C.
HACL* is joint work of Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche.
Fiat-Crypto
WireGuard also makes use of Fiat-Crypto's 32-bit Curve25519 scalar multiplication implementation. The curve is specified in Coq, which is then able to prove things about implementation strategies and emit verified C.
Fiat-Crypto is joint work of Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala.