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