Formal Verification

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.

Tweet

The Paper

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

This requires Tamarin, m4, GraphViz, and Maude.