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

SLMIA-SR: Speaker-Level Membership Inference Attacks against Speaker Recognition Systems

Guangke Chen (ShanghaiTech University), Yedi Zhang (National University of Singapore), Fu Song (Institute of Software, Chinese Academy of Sciences; University of Chinese Academy of Sciences)

Read More

Understanding and Analyzing Appraisal Systems in the Underground Marketplaces

Zhengyi Li (Indiana University Bloomington), Xiaojing Liao (Indiana University Bloomington)

Read More

Sharing cyber threat intelligence: Does it really help?

Beomjin Jin (Sungkyunkwan University), Eunsoo Kim (Sungkyunkwan University), Hyunwoo Lee (KENTECH), Elisa Bertino (Purdue University), Doowon Kim (University of Tennessee, Knoxville), Hyoungshick Kim (Sungkyunkwan University)

Read More