Pascal Lafourcade (Universite Clermont Auvergne), Dhekra Mahmoud (Universite Clermont Auvergne), Sylvain Ruhault (Agence Nationale de la Sécurité des Systèmes d'Information)

WireGuard is a Virtual Private Network (VPN), presented at NDSS 2017, recently integrated into the Linux Kernel and paid commercial VPNs such as NordVPN, Mullvad and ProtonVPN. It proposes a different approach from other classical VPN such as IPsec or OpenVPN because it does not let configure cryptographic algorithms. The protocol inside WireGuard is a dedicated extension of IKpsk2 protocol from Noise Framework. 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.

View More Papers

DRAINCLoG: Detecting Rogue Accounts with Illegally-obtained NFTs using Classifiers...

Hanna Kim (KAIST), Jian Cui (Indiana University Bloomington), Eugene Jang (S2W Inc.), Chanhee Lee (S2W Inc.), Yongjae Lee (S2W Inc.), Jin-Woo Chung (S2W Inc.), Seungwon Shin (KAIST)

Read More

Analysis of the Effect of the Difference between Japanese...

Rei Yamagishi, Shinya Sasa, and Shota Fujii (Hitachi, Ltd.)

Read More

Predictive Context-sensitive Fuzzing

Pietro Borrello (Sapienza University of Rome), Andrea Fioraldi (EURECOM), Daniele Cono D'Elia (Sapienza University of Rome), Davide Balzarotti (Eurecom), Leonardo Querzoni (Sapienza University of Rome), Cristiano Giuffrida (Vrije Universiteit Amsterdam)

Read More

Detecting Voice Cloning Attacks via Timbre Watermarking

Chang Liu (University of Science and Technology of China), Jie Zhang (Nanyang Technological University), Tianwei Zhang (Nanyang Technological University), Xi Yang (University of Science and Technology of China), Weiming Zhang (University of Science and Technology of China), NengHai Yu (University of Science and Technology of China)

Read More