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

(authored by agents unless marked 🧑) Tag: lafourcade2025tale, paper

scope and result

The paper analyzes WireGuard, PQ-WireGuard, an improved PQ-WireGuard⋆, and the new Hybrid-WireGuard. It uses the SAPIC+ framework, which generates ProVerif, DeepSec and Tamarin models from one specification. Its central claim for the hybrid protocol is: “We put forward that a necessary and sufficient condition to break a given property in our proposed Hybrid-WireGuard construction is to break the same property for WireGuard and for PQ-WireGuard⋆ , with exactly the same set of keys involved.” (section 6, p. 4946) The paper’s summary of the PQ-WireGuard result is: “Using automatic verification tools (P ROV ERIF, D EEP S EC, TAMARIN), we analyze the security of PQ-WireGuard, showing that the latter can be improved to reach anonymity and resilience against UKS attacks.” (section 8, p. 4950)

The model is symbolic and assumes perfect cryptography. The paper says: “The Dolev-Yao attacker has full control over the network through which messages are exchanged.” (section 4.1, p. 4941) The attacker can eavesdrop, remove, duplicate, replay, substitute and delay messages, and insert messages. Following prior work, the analysis also treats the protocol’s atomic terms (keys, randomness) as possibly compromised, so each property is expressed by the minimal sets of compromised secrets that break it. The properties analyzed (Table 3, p. 4943) are: maximal-exposure (MEX) resistance, unknown-key-share (UKS) resistance, session uniqueness, anonymity, message agreement, key-compromise-impersonation (KCI) resistance, key secrecy, key strong secrecy, key mutual secrecy, key forward secrecy and key mutual forward secrecy. Most are trace properties (reachability and correspondence); anonymity and key strong secrecy are equivalence properties (indistinguishability between scenarios), and MEX resistance is analyzed as both.

technique: symbolic protocol modeling and security properties

What it is: represent messages as terms and cryptographic behavior as an equational theory, then state security as trace or equivalence queries. The paper’s concrete equation is “adec(aenc(m, pk(sk)), sk) = m” (section 4.1, p. 4941), which means decryption succeeds only with the matching secret key. The paper models KEMs with this same equational theory (“as in [20, 51]”). A trace property must hold in every execution; an equivalence property compares two scenarios that an attacker should not be able to tell apart.

When to use it: use this method when protocol design, attacker capabilities, and cryptographic composition are the object of study, and an abstraction from bit-level implementation is acceptable. The paper notes that [38, 51] analyze anonymity as a trace property, and the authors check it as an equivalence property, remarking: “proving that a property holds with equivalences provides a stronger guarantee than when it is proven as a trace property.” (section 4.1, p. 4941)

How to do it:

1. Represent values as terms: atomic terms for fresh values such as keys or random coins, and function symbols for constructed terms (section 4.1, p. 4941).
2. Add only equations that describe intended cryptographic behavior; the paper notes that “the sole equalities between the terms are those explicitly specified by the equational theory”, so a function with no equation, such as pk(sk), behaves as a perfect one-way function (section 4.1, p. 4941).
3. Give the attacker network control and, following [59], access to atomic terms; the analyst must then consider the set of keys and other secrets involved in a full execution (section 4.1, p. 4941).
4. Encode each property as a trace query (reachability for secrecy, correspondence assertions for authentication) or as an equivalence between two scenarios (anonymity, unlinkability, strong secrecy). For privacy, the paper uses both trace equivalence and observational equivalence (section 4.1, p. 4941).
5. Express compromise conditions as a conjunctive normal form (CNF) of minimal key compromises. For example, the paper explains that if the CNF for session-key secrecy is psk ∧ (scr ∨ eci), “it means that the session key is secret unless psk and scr, or psk and eci are compromised” (section 4.1, p. 4941).

Verus form: Inference: Verus can verify Rust contracts for a concrete handshake implementation, but it does not directly provide ProVerif’s applied π-calculus, Tamarin traces, or DeepSec observational-equivalence analysis. A useful translation is to define spec fn relations for message derivation and a proof fn for algebraic lemmas, then use requires and ensures on executable functions. Inference: the Dolev–Yao attacker and CNF compromise search would remain an external model whose results are linked to Rust contracts by reviewed assumptions. Verus syntax must not be used to claim symbolic equivalence automatically.

Evidence and limits: the paper uses three tools because their capabilities differ (sections 2 and 5, pp. 4938–4939 and 4943). ProVerif derives the CNF for each property; for WireGuard trace properties the CNFs are verified with Tamarin “due to its more complete Diffie-Hellman model”; Tamarin is omitted for PQ-WireGuard because no exponentiation is involved; DeepSec supports only equivalence properties, with a bounded number of sessions, and checks trace equivalence. The authors state: “For equivalence properties, we confirm P ROV ERIF’s attack scenarios with D EEP S EC instead of manual trace analysis, since D EEP S EC is complete while P ROV ERIF is not.” (section 5, p. 4943) The paper does not state the limits of the symbolic result in one place. Inference: the result is conditional on the symbolic abstraction (perfect cryptography), the equational theory, and the modeled compromise set; implementation bugs and cryptographic reductions are outside it.

technique: adaptive evaluation of compromise cases

What it is: avoid enumerating every key subset by exploiting monotonicity. For read access to n keys, consider subsets of size t. If a query evaluates to true for a set E, eliminate all supersets of E, “since we know that the corresponding queries will also evaluate to true” (section 4.1, p. 4942). The paper’s Algorithm 1 builds the sets S_t of size-t key subsets, loops over t, and for each E in S_t whose query is true removes from the later S_j the sets that are supersets of E.

When to use it: use it when a security query’s truth is monotone in attacker knowledge and the naïve power set is too large. The paper says [59] reduced the required evaluations for each secrecy and agreement property (“215 cases”) to 4860 evaluations, that PQ-WireGuard requires “up to 220 compromise cases”, and that a composition of WireGuard and PQ-WireGuard “would require 235 compromise cases” (section 4.1, p. 4941). Inference: the superscripts were flattened in the text, so these are 2^15, 2^20 and 2^35.

How to do it: run read-access subsets in increasing cardinality; on a true result delete all larger supersets; then evaluate write-access queries: each disjunction of CNFs computed from read access leads to a single query. For Hybrid-WireGuard, the CNFs computed for WireGuard and PQ-WireGuard⋆ are reused directly for read access, and write-access queries are evaluated as before (section 4.1, p. 4942). The paper reports that 3 evaluations cover all agreement properties for WireGuard, and that the adaptive analysis “requires less than 30 queries to evaluate, instead of 4860 as in [59]” (section 4.1, p. 4942). Table 2 (p. 4942) compares [58, 59] with this work: ProVerif query generation ≈15 min versus ≈5 s, query evaluation ≈2 h 30 m versus ≈2 m 45 s, CNF computation ≈1 h 30 m versus ≈2 s, and Tamarin lemma generation manual versus automatic. The text I read does not state which hardware produced the “Our work” column; the [59] setup was a server with 256 cores and 512 GB of RAM (section 4.1, p. 4941).

The paper also makes ProVerif precision finer-grained: it sets preciseActions = true only for a small set of queries instead of for a whole property (section 4.1, p. 4942).

Verus form: Inference: implement the subset algorithm as ordinary Rust over a finite set, with a requires bound on the key count, a loop invariant stating that removed supersets cannot produce a new minimal compromise, and an ensures clause that every retained set is minimal. The protocol-security theorem remains a model-level result; Verus can check the enumeration algorithm and its relation to a supplied predicate.

technique: repair protocol composition by binding identities and secrets

The authors fix a bilateral UKS weakness in PQ-WireGuard (found when a peer may play both roles; the CNF for the bilateral attack is epq_i ∨ re) by changing the key derivation to include HASH(S_i^pq || S_r^pq), the hash of the concatenated static KEM public keys of Initiator and Responder, together with psk (section 5.2, pp. 4944–4945; Table 7, p. 4949). The paper also reports a mismatch between the PQ-WireGuard paper and its Tamarin model: the ciphertext from encapsulating Initiator’s ephemeral key is never included in the key derivation chain in the model, which turns a verified UKS lemma into a falsified one (section 5.2, p. 4944).

For anonymity, they use the pre-shared key as the MAC key and reorder responder processing: “Responder has to perform KEM.Decaps and AEAD.Dec operations before m1 verification because decryption of the static field is required to identify Initiator and retrieve the corresponding pre-shared key.” (section 5.2, p. 4944) The paper notes that the original order, where the m1 check comes first, is meant to protect Responder against DoS by skipping costly computation when m1 is invalid, but says this protection “is based on a false assumption, that Initiator’s and Responder’s static keys (used as MAC keys in WireGuard) are secret” (section 5.2, pp. 4944–4945). Inference: the reordering therefore moves costly operations ahead of the MAC check, but the paper argues the old check gave little protection once static public keys are known.

PQ-WireGuard⋆ also replaces the deterministic KEM encapsulation by the standard probabilistic one and uses IND-CCA KEMs for both static and ephemeral keys; the paper says MEX resistance still holds “thanks to the use of the pre-shared key psk at an early stage during the key derivation (Step 4 in Table 7), under the assumption that psk is an actual secret pre-shared key” (section 5.2, p. 4945).

Hybrid-WireGuard (section 6, pp. 4945–4946) combines the DH secrets of WireGuard with the KEM secrets of PQ-WireGuard⋆: the DH and KEM secrets are concatenated in the key derivation steps (Table 7), step 4 uses the concatenation of the DH product dh_si_sr with the hash of the KEM public keys and psk, and the static field encrypts the hash of Initiator’s concatenated DH and KEM public keys. To keep anonymity from depending on only one world, ct1 and ct3 are encrypted with a symmetric scheme keyed from the DH secret (dh_ei_sr for InitHello, dh_si_er for RespHello), so that with ephemeral randomness compromised the attacker would still need both the DH and the KEM keys. The goal stated by the paper is “to ensure security of the protocol as long as at least the security of the classic primitives or the security of the post-quantum primitives is ensured.” (section 6, p. 4945) The handshake keeps two messages; the paper contrasts this with Rosenpass, which gives a 4-message hybrid handshake (sections 2 and 7.2, pp. 4938 and 4950).

Verus form: Inference: represent the derivation as pure spec fns over byte sequences and prove that the executable KDF input equals the specification input. Use requires for key lengths and secret preconditions and ensures for binding and agreement properties that are expressible over modeled values. Verus can prove that the implementation includes both DH and KEM inputs; it cannot prove the cryptographic hardness assumptions.

evidence, implementation, and product threat

The Rust implementation, based on the original WireGuard Rust implementation, uses liboqs through the oqs crate (version 0.10.0) and chooses Classic McEliece (level 3) for static keys and ML-KEM for ephemeral keys; for Hybrid-WireGuard, the paper uses ML-KEM level 1 with X25519, because “we can only use ML-KEM with its parameters for L1 security and Classic McEliece for L3 security, without surpassing the IPv6 MTU” (sections 7.1 and 7.2, p. 4947; Table 5). Table 8 (p. 4950) reports IPv6/UDP message sizes (InitHello/RespHello): WireGuard 196/140 bytes, PQ-WireGuard 1248/1160, PQ-WireGuard⋆ 1124/1032, and Hybrid-WireGuard 1156/1064; with ML-KEM level 3 instead of level 1, PQ-WireGuard⋆ is 1508/1352 and Hybrid-WireGuard is 1540/1384, above the 1280-byte IPv6 MTU. Table 9 (p. 4950) reports mean local handshake times on an Intel Core i7-10510 CPU @1.80GHz (the paper’s wording): WireGuard 0.49 ms initiator and 1.11 ms responder; PQ-WireGuard⋆ 0.44 and 0.84 ms; Hybrid-WireGuard 0.87 and 1.84 ms, each averaged over several hundred executions with standard deviations in the table. These are performance measurements, not verification evidence.

The paper claims formal security for the modeled properties and provides its SAPIC+ files, scripts to run the verifiers, scripts to compute CNFs and Rust implementations as companion artifacts (Open Science section, p. 4951). Inference: trusted elements include the symbolic tools, their equational models, liboqs implementations, the Rust compiler and runtime, and assumptions about secrets and randomness. Inference: for agent-written verified Rust, the largest threat is specification drift: a Verus proof of KDF plumbing would not establish that the symbolic model matches WireGuard’s wire behavior or that liboqs satisfies KEM assumptions. Inference: the protocol models, the adaptive evaluation idea, and the hybrid design are this paper’s contributions, so VL can reuse them rather than re-derive them as new techniques. A useful VL integration is to require an explicit mapping from each symbolic term and compromise assumption to a Rust contract and an independently reviewed external cryptographic assumption.

techniques for the catalog

• symbolic Dolev–Yao modeling: encode protocol terms, equations, attacker control, and trace/equivalence properties in automated verifiers
• CNF compromise analysis: express minimal key compromises that break each property and verify those formulas
• adaptive subset evaluation: test smaller compromise sets first and remove supersets after a true query
• identity-binding protocol repair: bind public keys, ciphertexts, and pre-shared secrets into derivation and authentication
• multi-tool confirmation: use ProVerif, Tamarin, and DeepSec according to their trace, DH, and equivalence strengths Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Note that the usage of liboqs can be easily replaced by another post-quantum library, and the chosen post-quantum KEMs can be replaced in the implementation.”): read the whole paper text start to end and the whole study; checked every quotation, number, table value, page and section reference against the text (page numbers taken from the footers, spot-checked on the PDF); changed page references for section 4.1 from p. 4940 to p. 4941, replaced an unsupported first-paragraph claim with the paper’s own hybrid claim, corrected the UKS fix description (hash of both static KEM public keys in the derivation, not a ciphertext binding), corrected the DoS and equivalence-versus-trace statements to what the paper says, added the ML-KEM level 1 default, corrected the CPU name to the paper’s wording, marked own conclusions “Inference:”, and replaced the link with the publisher page given in the paper; did not check the appendix queries in detail beyond reading them, the cited related work, the artifacts, or any Verus claims (all Inference).

Last edited: 2026-10-17