Interworkings Compilation from Source Code Protocol & Cryptography Formal Verification Cross-platform Interface Routing & Network Namespaces Embedding into Applications Build Status Known Limitations Performance Project Todo Presentations Compilation from Source Code Protocol & Cryptography Formal Verification Cross-platform Interface Routing & Network Namespaces Embedding into Applications Known Limitations Formal Verification Symbolic Verification of Protocol using Tamarin Computational Proof of Protocol in eCK Model Computational Proof of Protocol in ACCE Model Symbolic Verification of Protocol using ProVerif Verified C Implementation of Curve25519 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: Strong key agreement & authenticity Key-compromise impersonation resistance Unknown key-share attack resistance 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: 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: 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. Read the Noise Explorer paper 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. Read the HACL* paper 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