Skip to Main content Skip to Navigation
Reports

A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol

Résumé : WireGuard est un logiciel de réseau privé virtuel (VPN) gratuit et open source qui cherche à remplacer IPsec et OpenVPN. Il est fondé sur un nouveau protocole cryptographique dérivé de la famille de protocoles Noise. Ce document présente la première preuve cryptographique mécanisée du protocole de WireGuard, obtenue avec l’assistant de preuve CryptoVerif. Nous analysons le protocole WireGuard en entier, tel qu’il est, y compris les messages de transport de données, dans un modèle du style ACCE. Nous obtenons des preuves de correction, secret des messages, forward secrecy, authentification mutuelle, unicité des sessions, et résistance contre des attaques d’imposture par compromis de clés, de mauvaise liaison d’identités, et de rejeu. Nous discutons également la robustesse de la protection des identités fournie par WireGuard. Notre travail fournit aussi de nouvelles contributions théoriques, réutilisables au-delà de WireGuard. Premièrement, nous étendons CryptoVerif pour tenir compte de l’absence de validation des clés publiques dans des groupes Diffie-Hellman populaires comme Curve25519, qui est utilisé dans beaucoup de protocoles modernes dont WireGuard. À notre connaissance, c’est la première preuve cryptographique mécanisée qui utilise un modèle aussi précis. Deuxièmement, nous prouvons plusieurs lemmes d’indifférentiabilité qui sont utiles pour simplifier les preuves de suites de dérivations de clés.
Document type :
Reports
Complete list of metadatas

Cited literature [48 references]  Display  Hide  Download

https://hal.inria.fr/hal-02100345
Contributor : Bruno Blanchet <>
Submitted on : Wednesday, June 12, 2019 - 9:20:09 PM
Last modification on : Monday, March 16, 2020 - 3:54:05 PM

File

RR-9269v2.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02100345, version 2

Collections

Citation

Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan. A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. [Research Report] RR-9269, Inria Paris. 2019, pp.49. ⟨hal-02100345v2⟩

Share

Metrics

Record views

5452

Files downloads

3271