A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol
| Title | A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol |
| Publication Type | Conference Paper |
| Year of Publication | 2019 |
| Authors | Lipp, Benjamin, Blanchet, Bruno, Bhargavan, Karthikeyan |
| Conference Name | 2019 IEEE European Symposium on Security and Privacy (EuroS P) |
| Date Published | jun |
| Publisher | IEEE |
| ISBN Number | 978-1-7281-1148-3 |
| Keywords | authorisation, Collaboration, composability, compositionality, computational model, computer network security, cryptographic proof, cryptographic protocol, cryptographic protocols, CryptoVerif proof assistant, Elliptic curve cryptography, IP networks, Noise Protocol Framework, open source Virtual Private Network, Policy Based Governance, policy-based governance, privacy, protocol verification, Protocols, pubcrawl, security protocols, Standards, transport data messages, verification, Virtual private networks, vpn, WireGuard virtual private network protocol |
| Abstract | 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 protocol underlying 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. |
| URL | https://ieeexplore.ieee.org/document/8806752 |
| DOI | 10.1109/EuroSP.2019.00026 |
| Citation Key | lipp_mechanised_2019 |
- open source Virtual Private Network
- WireGuard virtual private network protocol
- vpn
- Virtual private networks
- verification
- transport data messages
- standards
- security protocols
- pubcrawl
- Protocols
- protocol verification
- privacy
- policy-based governance
- Policy Based Governance
- authorisation
- Noise Protocol Framework
- IP networks
- Elliptic curve cryptography
- CryptoVerif proof assistant
- Cryptographic Protocols
- cryptographic protocol
- cryptographic proof
- computer network security
- computational model
- Compositionality
- composability
- collaboration