A Tale of Two Worlds — Hybrid-WireGuard

The Lafourcade–Mahmoud–Ruhault–Taleb paper from USENIX Security 2025 is one of two concurrent independent works that revisit the original PQ-WireGuard. The other is pq-wireguard-revisited (Hashimoto et al., IACR 2025/1758). Lafourcade et al. focus on formal verification and hybridization, with a Rust implementation; Hashimoto et al. focus on a leaner cryptographic redesign with the new RKEM primitive.

Three contributions

Formal analysis of PQ-WireGuard. They model PQ-WireGuard in SAPIC+, a framework that compiles a single specification to ProVerif, Tamarin, and DeepSec — letting them exploit each tool's strengths (Tamarin: associative-commutative DH; ProVerif: efficient unbounded-session analysis; DeepSec: trace-equivalence properties). They identify gaps in the prior symbolic proof (Donenfeld and Milner, Hülsing et al.), notably a missed UKS attack scenario, and show PQ-WireGuard inherits WireGuard's lack-of-anonymity issue. They also flag a non-standard KEM encapsulation definition in the original PQ-WireGuard that affects implementation. The fixed version is named PQ-WireGuard⋆, formally proven to provide anonymity, UKS resistance, agreement, and secrecy.

Hybrid-WireGuard. A new protocol combining PQ-WireGuard⋆ with classical WireGuard, designed to provide hybrid security: secure as long as either the classical or the post-quantum scheme remains unbroken. This is the recommended migration shape during the transitional period — the European Telecommunications Standards Institute's stance, OpenSSH 9.9's X25519+ML-KEM hybrid, Apple's PQ3, etc. The headline formal result: any attack on Hybrid-WireGuard decomposes into an attack on PQ-WireGuard⋆ and an attack on WireGuard.

Adaptive evaluation strategy. SAPIC+'s naive evaluation of all relevant security properties for a hybrid protocol explodes combinatorially. They propose an adaptive strategy that prunes the state space while preserving soundness — necessary in practice because the unfiltered analysis is intractable.

Rust implementation. A "generic, efficient and usable" Rust implementation of Hybrid-WireGuard, instantiated with Classic McEliece and ML-KEM, with benchmarks comparing against WireGuard, PQ-WireGuard, and PQ-WireGuard⋆.

How it diverges from Hashimoto et al.

The two papers reached overlapping conclusions independently:

Both found the UKS attack from KEM-binding issues
Both noted PQ-WireGuard's reliance on additional KEM assumptions

The fixes are different:

Aspect	Lafourcade et al.	Hashimoto et al.
Structural change	Concatenate static PKs to PSK in `H4`	Redesign around RKEM, eliminate duplicated PSK absorption
PSK in key schedule	Two inclusions (preserved)	One inclusion (streamlined)
Identity hiding assumption	Drop "PKs hidden from adversary"; insert PSK into anti-DoS MACs	Preserve original assumption; prove identity hiding and unlinkability
Anti-DoS cost	Recipient performs PK ops to look up PSK (against the original DoS model)	DoS-protection model preserved
Server PK memory	Classic McEliece (large) preserved	RKEM/Rebar reduces 190–390×
Implementation	Rust with bench	Implementation referenced, online

Practically: Hashimoto et al. is the better engineering result for kernel-level deployment (memory budget); Lafourcade et al. is the better formal-methods result and provides a working hybrid Rust implementation that conservative deployers could adopt today.

Both are needed inputs for a real PQ-WireGuard standardization process.

Why it matters

The paper is also a worked example of using SAPIC+ on a real industrial protocol — a useful reference for anyone building post-quantum hybrid handshakes (TLS, IKEv2, Signal, IMessage PQ3 are all in this category).

Cross-references: pq-wireguard, pq-wireguard-revisited, reinforcing-kem, ml-kem, post-quantum-cryptography, crqc-timeline.