A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol presented at IEEEEuroS&P 2019

by Karthikeyan Bhargavan, Bruno Blanchet, Benjamin Lipp,

Summary : WireGuard is a free and open source Virtual Private Network (VPN) that aims to replace IPsec and OpenVPN. It is based on a new cryptographic protocol derived from the Noise Protocol Framework. This paper presents the first mechanised cryptographic proof of the protocol underlying WireGuard, using the CryptoVerif proof assistant. We analyse the entire WireGuard protocol as it is, including transport data messages, in an ACCE-style model. We contribute proofs for correctness, message secrecy, forward secrecy, mutual authentication, session uniqueness, and resistance against key compromise impersonation, identity mis-binding, and replay attacks. We also discuss the strength of the identity hiding provided by WireGuard. Our work provides novel contributions that are reusable beyond WireGuard. First, we extend CryptoVerif to account for the absence of public key validation in Diffie-Hellman groups such as Curve25519, which WireGuard's authenticated key exchange is based upon. To our knowledge, this is the first mechanised proof employing such a precise model. Second, we prove, partly using CryptoVerif, several indifferentiability lemmas, useful to simplify random oracle calls.