Post-Quantum

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
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