A Unified Symbolic Analysis of WireGuard
Pascal Lafourcade
Network and Distributed System Security (NDSS) Symposium 2024 · Day 1 · Applied Cryptography
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.