A Unified Symbolic Analysis of WireGuard
Sylvain Ruhault, Pascal Lafourcade, Dhekra Mahmoud · 2024
WireGuard [22], [21] is a Virtual Private Network (VPN), presented at NDSS 2017, recently integrated into the Linux Kernel [57] and paid commercial VPNs such as NordVPN, Mullvad and ProtonVPN [56].It proposes a different approach from other classical VPN such as IPsec [29] or OpenVPN [48] because it does not let users configure cryptographic algorithms.The protocol inside WireGuard is a dedicated extension of IKpsk2 protocol from Noise Framework [49].Different analyses of WireGuard and IKpsk2 protocols have been proposed, in both the symbolic and the computational model, with or without computer-aided proof assistants.These analyses however consider different adversarial models or refer to incomplete versions of the protocols.In this work, we propose a unified formal model of WireGuard protocol in the symbolic model.Our model uses the automatic cryptographic protocol verifiers SAPIC + , PROVERIF and TAMARIN.We consider a complete protocol execution, including cookie messages used for resistance against denial of service attacks.We model a precise adversary that can read or set static, ephemeral or pre-shared keys, read or set ecdh pre-computations, control key distribution.Eventually, we present our results in a unified and interpretable way, allowing comparisons with previous analyses.Finally thanks to our models, we give necessary and sufficient conditions for security properties to be compromised, we confirm a flaw on the anonymity of the communications and point an implementation choice which considerably weakens its security.We propose a remediation that we prove secure using our models.