A Unified Symbolic Analysis of WireGuard

A Unified Symbolic Analysis of WireGuard

Speakers: Pascal Lafourcade

Conference: NDSS Symposium

YouTube: https://www.youtube.com/watch?v=hK2W4PdEfjo

Overview

This talk presents a groundbreaking, unified symbolic analysis of the WireGuard protocol, a modern VPN solution rapidly gaining adoption due to its simplicity and robustness. Given by Pascal Lafourcade, this research addresses the critical need for rigorous, automated security assessment of complex cryptographic protocols, a challenge highlighted by historical vulnerabilities in systems like TLS 1.3 and IKE despite extensive prior analysis. WireGuard, initially introduced at NDSS 2017 and now a staple in the Linux Kernel and commercial VPNs, intentionally restricts user configuration of cryptographic algorithms to enhance security, making a comprehensive formal analysis all the more vital.

The core motivation behind this work is to overcome the fragmentation of previous WireGuard security analyses. Prior studies often operated under differing adversarial models, analyzed incomplete protocol versions, or relied on various proof assistants, making a holistic understanding of WireGuard's security posture difficult. This research proposes a novel, unified formal model of WireGuard within the symbolic model, enriching existing models by incorporating a more complete protocol execution—including cookie messages for DoS resistance—and a more precise adversary model. This allows for a unified, interpretable assessment, direct comparison with prior works, and the discovery of new insights and vulnerabilities.

Key contributions include a comprehensive review and proposal of this new symbolic model, development of a dedicated methodology and tools to automatically assess all key compromise combinations, and the confirmation of a known anonymity flaw (now proven in the symbolic model). Crucially, the talk also reveals a critical vulnerability related to ECDH pre-computations, demonstrating that access to these pre-computed values can be as potent as access to static private keys. The research further derives necessary and sufficient conditions for security property compromises and proposes formally proven remediations for the identified anonymity and pre-computation issues.

Background

▶ Watch: Introduction: Challenges in cryptographic protocol analysis. (0:00)

The foundation of this analysis rests on the symbolic model of cryptography, where cryptographic primitives are treated as perfect, represented by abstract function symbols. The adversary in this model, typically a Dolev-Yao attacker, possesses complete control over the network, capable of eavesdropping, modifying, injecting, or delaying messages. This model is particularly effective for reasoning about protocol logic and identifying high-level flaws. Tools like PROVERIF and TAMARIN are central to symbolic analysis, translating protocol descriptions—often in the applied Pi-Calculus or as multiset rewrite rules, respectively—into verifiable security properties. This work leverages SAPIC+, a tool that unifies and supports the combined theories of both PROVERIF and TAMARIN.

Previous security analyses of WireGuard and its underlying Noise protocol, IKpsk2, have been conducted using both symbolic and computational models. Symbolic analyses of WireGuard, particularly those based on TAMARIN (e.g., references 24, 33 in the paper), focused on properties such as correctness, key agreement, secrecy, and identity hiding, often against specific key compromise scenarios. Computational analyses, such as those employing CRYPTOVERIF (reference 43), also contributed to understanding WireGuard's security in a more concrete, computational setting. For IKpsk2, PROVERIF (reference 35) and TAMARIN (references 31, 53) have confirmed claimed security properties, with reference 31 notably assessing a wider range of key compromise scenarios and modeling anonymity through observational equivalence.

Despite these efforts, a critical assessment reveals significant disparities and incompleteness in prior works. Many analyses modeled incomplete versions of WireGuard, for example, omitting message authentication codes (MACs) in initial handshake messages or simplifying transport messages. Figure 6 in the paper vividly illustrates these differences, underscoring how this new model unifies and enriches these prior representations, with the computational model in reference 43 being the closest, yet still incomplete, for symbolic analysis. Adversary models also varied, with some (e.g., 24, 35, 25) primarily capturing key leakage but not modification, while others (e.g., 31, 43) included both. Crucially, while some (reference 35) captured static and pre-shared key compromise, others (24, 25, 31, 43) also included ephemeral key compromise. The symbolic model from reference 31 for IKpsk2 was the most precise in capturing key corruption via leakage and modification. This current work builds upon this by introducing novel adversarial capabilities specifically related to ECDH pre-computations, thus addressing a significant gap in previous analyses.

Key Findings

▶ Watch: Overview of key contributions and identified vulnerabilities. (1:15)

The comprehensive unified symbolic analysis of WireGuard yielded several critical findings, confirming known issues, uncovering new vulnerabilities, and providing precise conditions for security compromises.

1. Confirmation of Anonymity Flaw: Contrary to initial claims in the WireGuard specification and some symbolic analyses, this research formally confirms that WireGuard's anonymity property is not satisfied. This vulnerability, previously identified in computational analyses, is now rigorously proven in the symbolic model using observational equivalence. The root cause lies in the RecHello message, where an adversary can compute and compare MAC fields based on known public keys, thereby distinguishing between potential initiators. This attack does not rely on network mechanisms but is inherent to the protocol's design.

1. Critical ECDH Pre-computation Vulnerability: A significant discovery is that compromising ECDH pre-computations (e.g., gaining access to pre-computed shared secrets between static keys from process memory) grants an adversary the same power as compromising the static private key itself. This challenges the intuitive belief that pre-computation compromise is a weaker form of attack. The derived DNF formulas explicitly demonstrate that pre-computation compromise (e.g., Rc in DNF1*) contributes to breaking security properties in a manner analogous to static key compromise (e.g., Ru or Rv).

1. Derivation of Necessary and Sufficient Conditions: The methodology allowed for the derivation and formal proof of necessary and sufficient conditions for the compromise of 34 security properties, including agreement, secrecy, and Perfect Forward Secrecy (PFS). These conditions are expressed as compact Disjunctive Normal Form (DNF) formulas (e.g., DNF1* for RecHello agreement, DNF3* for k6 secrecy with PFS), offering unprecedented precision and comprehensiveness compared to previous analyses. These formulas precisely delineate which combinations of key compromises lead to specific security property violations.

1. Crucial Role of Pre-shared Keys (psk): The analysis consistently highlighted that pre-shared key (psk) compromise (e.g., Rs or Ms in DNF formulas) is a significant factor in breaking various security properties, especially in the presence of an active adversary. This underscores the importance of systematically employing an optional pre-shared key within WireGuard deployments, as it offers a robust layer of defense.

1. Criticality of Initial Key Distribution: The research emphasizes that the security of WireGuard fundamentally relies on the secure and honest out-of-band distribution of static public keys. The DNF formulas include terms like D_u and D_v, indicating that dishonest distribution of static keys directly compromises core security properties. This highlights a critical attack surface that must be meticulously protected.

1. Unified and Comprehensive Symbolic Model: The development of the most comprehensive symbolic model of WireGuard to date is a key contribution itself. This model integrates full protocol execution, including CookieRep messages, and a precise adversary model that captures key leakage, modification, and dishonest distribution for static, ephemeral, pre-shared, and pre-computed keys, providing a robust framework for analysis.

Technical Deep Dive

▶ Watch: Background on symbolic analysis and related work. (2:00)

The technical core of this research revolves around a meticulous and exhaustive symbolic analysis of the WireGuard protocol.

WireGuard Protocol Description

WireGuard operates in two distinct phases: a key exchange phase and a transport phase. The key exchange is a 1.5-RTT process involving two primary messages: InitHello (sent by the Initiator) and RecHello (sent by the Responder). Following these, TransData messages are used for encrypted payload transmission. A fourth message, CookieRep, provides crucial denial-of-service (DoS) protection. Peers can interchangeably act as either Initiator or Responder.

The protocol relies on a specific, non-configurable suite of cryptographic primitives:

• A cyclic group G, instantiated with Curve25519 for elliptic curve Diffie-Hellman (ECDH) key agreement.
• A hash function h (Blake2s) for 32-byte fingerprints.
• Message authentication codes (MACs): hmac (Blake2s 32) for 32-byte MACs and mac (Blake2s 52) for 16-byte MACs.
• Key derivation functions (KDFs): kdf1, kdf2, kdf3 for deriving 32-byte key tuples.
• Authenticated encryption algorithms (AEADs): aead (ChaCha20-Poly1305) and xaead (XChaCha20-Poly1305).
• A padding scheme pad.

Protocol messages are structured with specific identifiers and fields:

• InitHello: 103siXUtsmac1mac – contains a session identifier si, Initiator's ephemeral key X, encrypted static public key U, encrypted timestamp ts, and two MACs.
• RecHello: 203srsiYmac1mac – includes Responder's ephemeral key Y, and an encrypted empty string.
• TransData: 303srikpad(Pik) or 303sirkpad(Prk) – carries encrypted payloads.
• CookieRep: 403sipT – for DoS protection, comprising a random nonce p and an encrypted cookie T.

The message computation involves a complex sequence of KDFs and AEAD operations to derive session keys and chaining values. For instance, an InitHello message involves computing ck, h0, h1, C0, h2, C1, k1, U, h3, C2, k2, ts, h4, and finally the mac using a key derived from public values. While WireGuard is an extension of the Noise framework's IKpsk2 protocol, key distinctions exist, such as WireGuard's 1.5-RTT exchange, clear counter transmission in transport messages, and specific headers/session identifiers not present in generic IKpsk2. These differences necessitate a precise, dedicated analysis.

Key Technical Approach & Methodology

The methodology is grounded in the symbolic model, extending the applied Pi-Calculus, and leveraging the SAPIC+ protocol verifier, which integrates PROVERIF and TAMARIN.

Comprehensive Adversary Model: The adversary model, drawing from reference 5, considers four dimensions of compromise:

1. Kind of data: Long-term keys (ltkX), ephemeral keys (ekX), pre-shared keys (psk), and ECDH pre-computations (pre).
2. Whose data: Initiator's or Responder's.
3. When compromise occurs: Before protocol execution, after protocol execution (for PFS), or during initial key distribution.
4. Type of compromise:

• R (Reveal): Data is generated honestly but revealed to the adversary (e.g., RltkX for revealing agent X's long-term private key).
• M (Modify): Data is generated dishonestly or modified by the attacker.
• D (Dishonest Distribution): Specific to long-term public keys.

The research considers all relevant combinations of these capabilities, in conjunction with the standard Dolev-Yao adversary. Notably, Rc and Mi are introduced for reveal and modify of pre-computations, respectively.

Methodology for Evaluating Security Properties:

1. Initial Search: Identify all compromise scenarios where a property is violated (e.g., att(s) is true for secrecy properties).
2. Formula Derivation: SAPIC+ generates PROVERIF files for all possible key compromise combinations. Satisfied queries are combined into compact formulas, first as Conjunctive Normal Form (CNF) and then as Disjunctive Normal Form (DNF). This process, illustrated in Figure 7, reduces over 2 million (2^21) potential compromise cases to a manageable set of DNF formulas.
3. PFS Assessment: Perfect Forward Secrecy is assessed by introducing "phases" in PROVERIF, distinguishing between key compromise before and after protocol execution.
4. TAMARIN Integration: The derived DNF formulas are translated into TAMARIN lemmas for formal validation of their necessary and sufficient conditions. For anonymity, which uses observational equivalence, PROVERIF is primarily used, as SAPIC+ does not yet directly translate this to TAMARIN.

The analysis covered 34 security properties: 4 agreement properties (for RecHello and TransData messages), 12 secrecy properties (for session key k6 and derived keys C_i, Cr from both Initiator's and Responder's views, including PFS), and anonymity (for WireGuard with and without cookies).

System Design & Implementation Details

The system design centers on SAPIC+, which enables defining protocol models and security properties in a unified framework, then exporting them to PROVERIF or TAMARIN for verification.

1. Protocol Modeling: A detailed formal model of WireGuard was developed in the applied Pi-Calculus, encompassing all messages, cryptographic primitives, and the complete protocol execution, including the CookieRep message. This model is unprecedented in its comprehensiveness for symbolic analysis. Figure 8 provides an extract of the SAPIC+ reference process, detailing Initiator and Responder processes and key compromise processes like Revealpsk, RevealLtki, RevealPre, RevealEki, and RevealEkr.
2. Adversary Model Implementation: The rich adversary model is implemented by dynamically modifying protocol processes. For instance, key modification is modeled by replacing a new psk with in(psk), allowing the adversary to inject arbitrary values. Reveal events are inserted to model key leakage. Security property queries are constructed with disjunctions of various key compromise scenarios for thorough assessment.
3. Automated Assessment Pipeline: A suite of Python scripts, leveraging the SymPy package (reference 54), automates the entire analysis workflow:

• PROVERIF File Generation: Scripts generate up to 4860 PROVERIF files per property, covering all key compromise combinations.
• Parallel PROVERIF Evaluation: GNU parallel (reference 55) is used to run PROVERIF queries concurrently, drastically accelerating verification.
• DNF Computation: Post-PROVERIF results, scripts compute DNF formulas for each property by combining individual compromise scenarios.
• TAMARIN Lemma Generation and Verification: Simplified DNF formulas are translated into TAMARIN lemmas, then verified by the TAMARIN prover.

The models and tools are publicly available on a Gitlab repository (reference 38), with a Docker image for easy reproduction. Full experiments require substantial computational resources (e.g., 256 CPU cores, 512 GB RAM), while simpler experiments can run on standard laptops.

Demo / Proof of Concept

▶ Watch: Detailed description of the WireGuard protocol. (4:00)

While the talk does not feature a live "demo" in the traditional sense of a software demonstration, the entire research constitutes a robust proof of concept for a novel, automated formal verification methodology. The "demonstration" lies in the successful execution of the comprehensive analytical pipeline and the verifiable results derived.

The research's proof of concept is embodied by:

• The SAPIC+ framework's capability to model complex protocols like WireGuard and its adversary model, then automatically generate inputs for PROVERIF and TAMARIN.
• The automated Python scripts that orchestrated the generation of thousands of PROVERIF files (up to 4860 per property), parallel execution using GNU parallel, computation of compact DNF formulas using SymPy, and subsequent translation into TAMARIN lemmas for formal verification.
• The successful derivation of precise necessary and sufficient conditions for the compromise of 34 security properties, expressed as DNF formulas.
• The formal symbolic proof of the anonymity flaw in WireGuard using observational equivalence in PROVERIF.
• The formal proof of the ECDH pre-computation vulnerability, demonstrating its equivalence to static private key compromise.
• The formal proof of proposed remediations for both the anonymity and pre-computation issues.

All models, tools, and scripts are publicly available on a Gitlab repository and via a Docker image and Zenodo, along with detailed instructions in Appendix A for independent reproduction. For instance, Experiment E1 (PFS of session key) takes about 15 minutes on a standard laptop, while more extensive experiments like E2 (agreement and secrecy) complete in approximately 9 hours on a dedicated server. This artifact availability allows for direct verification and further research, serving as a concrete "proof of concept" for the methodology's efficacy and reproducibility.

Defensive Implications

▶ Watch: Our comprehensive adversary model and methodology. (6:00)

The findings of this unified symbolic analysis provide concrete, actionable defensive implications for WireGuard users, developers, and implementers.

1. Anonymity Fixes: The confirmed anonymity flaw necessitates a protocol modification. The proposed remediation involves changing the message authentication code (MAC) computation in the RecHello message. Instead of using h(M, U*), the MAC key should incorporate values known only to the Initiator and Responder, such as h(Uguv) or h(Upsk). These proposed fixes have been formally proven to restore anonymity. This also requires adapting the order of operations during InitHello reception: first decrypt U, then check U, and only then check the authentication code. Implementing these changes is crucial for WireGuard deployments where anonymity is a desired property.

1. ECDH Pre-computation Security: The critical finding that compromising ECDH pre-computations is equivalent to compromising the static private key itself has significant implications for implementation security. The strong recommendation is to remove the implementation optimization of pre-computing ECDH products between static keys at interface setting. Instead, all ECDH computations should occur dynamically upon InitHello reception. This prevents an adversary from gaining powerful access to pre-computed values through memory corruption or other side-channel attacks, effectively mitigating a potent attack vector.

1. Systematic Use of Pre-shared Keys (psk): The analysis consistently demonstrates the significant role of pre-shared keys (psk) in maintaining security, particularly against active adversaries. Even though psk is optional in WireGuard, the research strongly recommends that WireGuard users systematically employ a pre-shared key in their configurations. This adds a crucial layer of defense against various compromise scenarios and enhances the overall security posture.

1. Secure Initial Key Distribution: The fundamental security of WireGuard heavily relies on the correct and honest out-of-band distribution of static public keys. The research underscores that if static keys are dishonestly distributed, core security properties can be compromised. Defenders must ensure that the processes for initial key exchange and public key distribution are robustly secured, employing trusted channels and verification mechanisms to prevent tampering or impersonation during this critical phase. This assumption must be strictly maintained, as any compromise here directly impacts the integrity and confidentiality of subsequent communications.

Key Takeaways

• WireGuard's anonymity property is formally proven to be broken in the symbolic model, confirming prior computational findings, and specific protocol modifications are proposed and proven to restore it.
• Access to ECDH pre-computations between static keys is equivalent to compromising the static private key itself, necessitating a change in implementation practices to avoid pre-computation optimization.
• A novel, comprehensive symbolic model of WireGuard, incorporating full protocol execution and a precise adversary model, provides the most detailed security assessment to date.
• The research derived necessary and sufficient conditions for the compromise of 34 security properties, expressed as compact DNF formulas, offering unprecedented clarity on WireGuard's security posture.
• The pre-shared key (psk), though optional, is crucial for maintaining security against active adversaries and should be systematically employed in WireGuard deployments.
• The security of WireGuard is fundamentally dependent on the secure and honest out-of-band distribution of static public keys, which must be rigorously protected.

About the Speaker(s)

Pascal Lafourcade is a distinguished researcher in the field of cryptography and information security. While specific titles and affiliations beyond his name and the conference are not detailed in the provided transcript, his work, as demonstrated by this presentation at the NDSS Symposium, showcases deep expertise in formal methods for protocol analysis, symbolic modeling, and the identification of subtle vulnerabilities in widely deployed cryptographic systems. His contributions are instrumental in enhancing the security and understanding of complex protocols like WireGuard.