A Tale of Two Worlds, a Story of WireGuard Hybridization

PQ-WireGuard, published in 2021 IEEE Symposium on Security and Privacy, is a post-quantum variant of WireGuard VPN, where ECDH-based key exchange is replaced by KEM-based key exchange instantiated with dedicated post-quantum constructions. During our talk, we will present our new work, where we improve PQ-WireGuard by pointing out and fixing vulnerabilities thanks to formal verifications tools. Moreover, we propose a new protocol, named Hybrid-WireGuard, in-line with current best practices for post-quantum transition about hybridization techniques. Using SAPIC+ and the automatic cryptographic protocol verifiers PROVERIF, DEEPSEC and TAMARIN, we prove that our construction is secure in the symbolic model. Furthermore, we show that Hybrid-WireGuard security is a conjunction of WireGuard security and PQ-WireGuard security. We propose an efficient Rust implementation of our new protocol and show that its performance ensures its usability.