A Tale of Two Worlds, a Formal Story of WireGuard Hybridization

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. Formal security analysis of PQ-WireGuard. We propose a new and more comprehensive model of PQ-WireGuard than the one presented in [51] and a more powerful attacker. We point out a mistake in the latter symbolic proof which has an impact on Unknown-Key-Share (UKS) attacks' analysis and we identify attack scenarios that are missed. Furthermore, PQ-WireGuard inherits the lack of anonymity from WireGuard. In addition, we point out that PQ-WireGuard uses a non-standard definition of the KEM encapsulation procedure, which impacts the protocol's implementation and analysis. We therefore propose a new version of the protocol, based on the common KEM's definition, which we refer to as PQ-WireGuard ⋆ . We formally prove that this version ensures anonymity, resists Unknown-Key-Share attacks and preserves the remaining properties (agreement and secrecy). Hybrid-WireGuard. We propose a new protocol, called Hybrid-WireGuard, constructed by skillfully combining our improved construction PQ-WireGuard ⋆ , and WireGuard. We model this protocol and formally prove that all the security properties are achieved. Moreover, our analysis shows that if an attack scenario against a security property of Hybrid-WireGuard exists, then it is a combination of an attack on PQ-WireGuard ⋆ and an attack on WireGuard. Adaptive analysis. We base our formal analysis on [59] . We point out, however, that the evaluation strategy used in [59] , is not practical to analyze Hybrid-WireGuard because of a far more larger set of required evaluations. We therefore propose an adaptive evaluation strategy which greatly reduces the number of necessary evaluations needed to assess security properties, while preserving soundness. Instantiation and implementation. We instantiate Hybrid-WireGuard with Classic McEliece [18] and ML-KEM [65] algorithms and propose a generic and efficient implementation in Rust. We provide benchmarks for Hybrid-WireGuard and PQ-WireGuard ⋆ compared to WireGuard and PQ-WireGuard, showing the practical usability of our constructions. Paper organization In Section 2, we present related work, for WireGuard and PQ-WireGuard-based constructions and tools, protocol analysis with Sapic + , and hybridization. Then, in Section 3, we detail WireGuard and PQ-WireGuard handshakes. Next, in Section 4, we describe our methodology for the formal verification of WireGuard, PQ-WireGuard, PQ-WireGuard ⋆ and Hybrid-WireGuard, and present the analyzed security properties. Based on this description, we exhibit the results of our symbolic analysis for WireGuard and PQ-WireGuard in Section 5. Our results on PQ-WireGuard lead us to an improved version of the protocol, which we call PQ-WireGuard ⋆ , described and symbolically assessed in the same section. After, we introduce our protocol Hybrid-WireGuard in Section 6. We also exhibit the results of our symbolic analysis of the protocol, showing that its security is ensured as long as at least the security of the classic primitives or the security of the post-quantum primitives is ensured. Finally, we present our implementation and instantiation of cryptographic primitives in Section 7, and we conclude in Section 8. Related Work Constructions and tools based on WireGuard and PQ-WireGuard. In [10], a tweak is proposed to provide WireGuard with post-quantum security. It consists in transmitting the hash of the identity public key instead of the public key itself, hence protecting it from a quantum computer. The goal is to protect against store-now-decrypt-later attacks. However, this tweak relies on the strong assumption that peers' public keys are unknown to the attacker (a similar assumption is made in WireGuard [36]). NordLynx [67], a variant of WireGuard, proposes a post-quantum solution: after the successful handshake, a KEM key exchange is performed using ML-KEM, within the already mounted WireGuard tunnel. This solution provides post-quantum security for the final session keys, mitigating attacks from