cryptography

A tale of two models: formalizing 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
Project
Building confidence in cryptographic protocols
An introduction to formal analysis and our proof of the security of KEMTLS.
Thom Wiggers
Last updated on 2022-02-27 1 min read research
Project
More efficient post-quantum KEMTLS with pre-distributed public keys
We make KEMTLS more efficient in scenarios where the client already has the server’s long-term public key, for example through caching or because it’s pre-installed.
Preprint PDF Cite Project DOI
Practically Solving LPN
We analyse the difficulty of the LPN problem in restricted memory.
Thom Wiggers, Simona Samardjiska
Preprint PDF Cite Code Dataset
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
Post-Quantum TLS without handshake signatures
We present an alternative to TLS 1.3, by authenticating using only Key-Encapsulation Mechanisms. This allows us to get rid of handshake signatures, as post-quantum signature schemes are expensive, both in bytes and computation times.
Preprint PDF Cite Code Dataset Project DOI
Post-Quantum TLS with KEMs
We investigate getting rid of signatures in TLS
Thom Wiggers
Solving LPN Using Large Covering Codes

Since quantum computers are expected to break most of the cryptographic schemes we rely on today, we need to look at alternatives. …

2019-04-08 10:45 Utrecht, The Netherlands
Thom Wiggers
Slides
Rephrasing TLS key exchange in terms of KEMs
In the RFC for TLS 1.3 (RFC8446) especially, the key exchange is defined in terms of (EC)DH key shares being exchanged. This limits us to algorithms which support non-interactive key exchanges, while this is not necessary for the security of TLS 1.
Thom Wiggers
Last updated on 2020-10-07 3 min read research
Time-invariant equality in assembly

For crypto code it's important that it's time-invariant, otherwise it is vulnerable to timing attacks. I've had to build this time-invariant equality test from scratch, because I couldn't find something on Google. I hope it's useful to someone else.

Thom Wiggers
Last updated on 2019-07-23 2 min read security