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:

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:

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.

Read the Noise Explorer paper

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.

Read the HACL* paper

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.

Read the Fiat-Crypto paper