cryptography

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.

Invited lecture about TLS, its history and making TLS post quantum. I also discuss KEMTLS.

An introduction to formal analysis and our proof of the security of KEMTLS.

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.

We analyse the difficulty of the LPN problem in restricted memory.

In this paper, we study implementations of post-quantum signature schemes on resource-constrained devices. We focus on verification of …

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.

We investigate getting rid of signatures in TLS

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.