- Posted on
Comprehensive WireGuard Analysis: The research performed a unified symbolic analysis of the WireGuard protocol (including WireGuard with cookies) using three tools (ProVerif, Tamarin, and Seic+), going beyond previous analyses in scope and depth of the threat model.
Threat Model Enhancements: The analysis incorporated a more comprehensive threat model than previous work, including:
- Read and write access to all keys.
- Pre-computation vulnerability: Modeling the impact of pre-computed values stored in memory, showing that its compromise can be as detrimental as private key compromise.
Security Property Verification: The analysis verified three key security properties:
- Message agreement.
- Key secrecy (including perfect forward secrecy).
- Anonymity.
Key Findings Regarding Security Properties:
- Compromise of initial static key distribution severely impacts all security properties.
- Compromise of the pre-shared key (PSK) jeopardizes all security properties; the PSK should be mandatory, not optional.
- The pre-computation significantly weakens security in some cases, mirroring the impact of private key compromise; its removal is recommended.
- WireGuard does not provide anonymity as claimed. Attacks were identified leveraging MAC values in the first two messages, revealing initiator and responder identities.
Proposed Anonymity Fixes: Three fixes for the anonymity flaws are proposed: removing MACs entirely or modifying the MAC computation to incorporate a secret key known only to the initiator and responder. These fixes have been formally verified.
Recommendations:
- Users should always use a pre-shared key.
- Secure initial static key distribution is crucial.
- Users should not rely on WireGuard for anonymity.
- Stakeholders should remove the pre-computation step to enhance security and address the anonymity vulnerabilities.
Methodology: The use of multiple tools (ProVerif and Tamarin, with Seic+ as a bridge) provided faster results from ProVerif and a more in-depth threat model analysis from Tamarin. The models and results are publicly available.