Post-Quantum

Revisiting PQ WireGuard: A Comprehensive Security Analysis With a New Design Using Reinforced KEMs
WireGuard is a VPN protocol with an efficient, DH-based handshake. Prior attempts at making it PQ heavily relied on Classic McEliece, which has deployment complications. We revisit PQ WireGuard and manage to get rid of one of the uses of Classic McEliece by providing optimized KEMs. We also fix a flaw in the security of post-quantum WireGuard, which assumed KEM binding properties not necessarily provided by Classic McEliece.
Keitaro Hashimoto, Shuichi Katsumata, Guilhem Niot, Thom Wiggers
Preprint Cite
A tale of two models: formal verification of KEMTLS in Tamarin
We prove the security of KEMTLS in two Tamarin models. One mode is based on the Cremers et al. model of TLS 1.3; the other closely resembles our pen-and-paper proofs. These models allow us to analyse KEMTLS, and its extension KEMTLS-PDK from different angles.
Sofía Celi , Jonathan Hoyland, Douglas Stebila , Thom Wiggers
Preprint PDF Cite Project DOI
Verifying Post Quantum Signatures in 8kB of RAM
In this paper, we study implementations of post-quantum signature schemes on resource-constrained devices. We focus on verification of …
Ruben Gonzalez, Andreas Hülsing, Matthias J. Kannwischer , Juliane Krämer, Tanja Lange, Marc Stöttinger, Elisabeth Waitz, Thom Wiggers, Bo-Yin Yang
Preprint PDF Cite DOI