Abstract:
WireGuard is a new Virtual Private Network (VPN), recently integrated into the Linux Kernel and in OpenBSD.
It proposes a different approach from other classical VPN such as IPsec or OpenVPN because it does not let users configure cryptographic algorithms but instead relies on a close set of preconfigured algorithms.
The protocol inside WireGuard is a dedicated extension of IKpsk2 protocol from Noise Framework.
WireGuard and IKpsk2 protocols have gained a lot of attraction from the academic community and different analyses 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.
Furthermore, when proof assistants are used, protocol models also differ.
In this work, we propose a new, unified formal model of WireGuard protocol in the symbolic model.
Our model is fully based on processes in the applied Pi- alculus, the language used by the automatic cryptographic protocol verifier Sapic+.
It allows us to automatically generate translations into ProVerif and Tamarin proof assistants.
We consider a complete protocol execution, including cookie messages used for resistance against denial of service attacks.
Furthermore, we model an adversary that can read or set static, ephemeral or pre-shared keys, read or set ECDH precomputations, control key distribution.
Eventually, we present our results in a unified and interpretable way, allowing comparisons with previous analyses.
This is joint work with Dhekra Mahmoud and PascalLafourcade.
