Mechanised cryptographic proof of the WireGuard protocol

[blipp at mailbox.org]

Dear all,

With Bruno Blanchet and Karthik Bhargavan from the Prosecco research group at Inria Paris, we continued working on our mechanised cryptographic proof of the WireGuard protocol since my master's thesis was finished last year.

I am happy to say that a paper we wrote about our work was accepted at this year's EuroS&P conference [1]. A long version of the paper is as of now available at https://hal.inria.fr/hal-02100345, and the code and the models at https://cryptoverif.inria.fr/WireGuard.

Differences to my master's thesis that is linked at the moment on WireGuard's formal verification page https://www.wireguard.com/formal-verification/ under the headline “Computational Proof of Protocol in ACCE Model” include:

- We now use a precise model of the elliptic curve group Curve25519. This removes the gap between our previous proof and what WireGuard actually does, and thus increases confidence in the proof. This is, to the best of our knowledge, the first work that analyses WireGuard with such a precise model.
- We analyse the identity hiding property of WireGuard.
- We analyse the DoS protection provided by the MACs and the cookie message.
- We provide a comparison with 5 other works that analysed WireGuard or the underlying Noise IKpsk2 protocol. This includes symbolic analyses using ProVerif and Tamarin, and a manual cryptographic proof.

If you have questions regarding our work, please reach out, I am happy to explain more details.

Best regards,
Benjamin

[1] https://www.ieee-security.org/TC/EuroSP2019/

-- 
Research group: https://prosecco.gforge.inria.fr/
Personal website: https://benjaminlipp.de/