Thom Wiggers
Thom Wiggers
Home
Posts
Talks
Publications
Teaching
Docs
Contact
Light
Dark
Automatic
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
Cite
×