Paper 2025/1179
A Tale of Two Worlds, a Formal Story of WireGuard Hybridization
, Université Clermont Auvergne, CNRS, Clermont Auvergne INP, Mines Saint-Etienne, LIMOS, 63000 Clermont-Ferrand, France, Université Clermont Auvergne, CNRS, Clermont Auvergne INP, Mines Saint-Etienne, LIMOS, 63000 Clermont-Ferrand, France, Agence Nationale de la Sécurité des Systèmes d’Information (ANSSI), France, Agence Nationale de la Sécurité des Systèmes d’Information (ANSSI), FranceAbstract
PQ-WireGuard is a post-quantum variant of WireGuard Virtual Private Network (VPN), where Diffie-Hellman-based key exchange is replaced by post-quantum Key Encapsulation Mechanisms-based key exchange. In this paper, we first conduct a thorough formal analysis of PQ-WireGuard's original design, in which we point out and fix a number of weaknesses. This leads us to an improved construction PQ-WireGuard*. Secondly, we propose and formally analyze a new protocol, based on both WireGuard and PQ-WireGuard*, named Hybrid-WireGuard, compliant with current best practices for post-quantum transition about hybridization techniques. For our analysis, we use the SAPIC+ framework that enables the generation of three state-of-the-art protocol models for the verification tools ProVerif, DeepSec and Tamarin from a single specification, leveraging the strengths of each tool. We formally prove that Hybrid-WireGuard is secure. Eventually, we propose a generic, efficient and usable Rust implementation of our new protocol.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Minor revision. 34th USENIX Security Symposium (2025)
- Contact author(s)
-
pascal lafourcade @ uca fr
dhekra mahmoud @ uca fr
sylvain ruhault @ gmail com
abdulrahman taleb @ ssi gouv fr - History
- 2025-08-04: last of 2 revisions
- 2025-06-23: received
- See all versions
- Short URL
- https://ia.cr/2025/1179
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2025/1179,
author = {Pascal Lafourcade and Dhekra Mahmoud and Sylvain Ruhault and Abdul Rahman Taleb},
title = {A Tale of Two Worlds, a Formal Story of {WireGuard} Hybridization},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/1179},
year = {2025},
url = {https://eprint.iacr.org/2025/1179}
}
