A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol
| Autor: | Karthikeyan Bhargavan, Benjamin Lipp, Bruno Blanchet |
|---|---|
| Přispěvatelé: | Programming securely with cryptography (PROSECCO ), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), ANR-17-CE39-0004,TECAP,Analyse de protocoles - unir les outils existants(2017), ANR-14-CE28-0014,AnaStaSec,Analyse Statique pour la Sécurité(2014), European Project: 688722,H2020 Pilier Industrial Leadership,H2020-ICT-2015,NEXTLEAP(2016), European Project: 683032,H2020 ERC,ERC-2015-CoG,CIRCUS(2016), Programming securely with cryptography (PROSECCO), Inria Paris, Blanchet, Bruno, Analyse de protocoles - unir les outils existants - - TECAP2017 - ANR-17-CE39-0004 - AAPG2017 - VALID, Appel à projets générique - Analyse Statique pour la Sécurité - - AnaStaSec2014 - ANR-14-CE28-0014 - Appel à projets générique - VALID, NEXTLEAP - NEXTLEAP - - H2020 Pilier Industrial Leadership2016-01-01 - 2018-12-31 - 688722 - VALID, An end-to-end verification architecture for building Certified Implementations of Robust, Cryptographically Secure web applications - CIRCUS - - H2020 ERC2016-04-01 - 2021-03-31 - 683032 - VALID |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Correctness
Computer science computer.internet_protocol Vérification Cryptography 02 engineering and technology Computer security computer.software_genre VPN Public-key cryptography [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Forward secrecy Modèle calculatoire 0202 electrical engineering electronic engineering information engineering Protocoles cryptographiques [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR] business.industry Computational model Proof assistant Verification 020206 networking & telecommunications Cryptographic protocol Security protocols IPsec Key (cryptography) 020201 artificial intelligence & image processing business computer |
| Zdroj: | 4th IEEE European Symposium on Security and Privacy 4th IEEE European Symposium on Security and Privacy, Jun 2019, Stockholm, Sweden. pp.231-246 [Research Report] RR-9269, Inria Paris. 2019, pp.49 2019 IEEE European Symposium on Security and Privacy (EuroS&P) EuroS&P [Research Report] RR-9269, Inria Paris. 2019, pp.50 |
| Popis: | WireGuard is a free and open source Virtual Private Network (VPN) that aims to replace IPsec and OpenVPN. It is based on a new cryptographic protocol derived from the Noise Protocol Framework. This paper presents the first mechanised cryptographic proof of the protocolunderlying WireGuard, using the CryptoVerif proof assistant. We analyse the entire WireGuard protocol as it is, including transport data messages, in an ACCE-style model. We contribute proofs for correctness, message secrecy, forward secrecy, mutual authentication, session uniqueness, and resistance against key compromise impersonation, identity mis-binding, and replay attacks. We also discuss the strength of the identity hiding provided by WireGuard. Our work also provides novel theoretical contributions that are reusable beyond WireGuard. First, we extend CryptoVerif to account for the absence of public key validation in popular Diffie-Hellman groups like Curve25519, which is used in many modern protocols including WireGuard. To our knowledge, this is the first mechanised cryptographic proof for any protocol employing such a precise model. Second, we prove several indifferentiability lemmas that are useful to simplify the proofs for sequences of key derivations.; 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 devalidation 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|