# 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]].