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:
- 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.
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
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.
Verified C Implementation of Curve25519
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.
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.