A tale of two models: Formal analysis of KEMTLS in Tamarin
A tale of two models: Formal analysis of KEMTLS in Tamarin Sofia Celi, Jonathan Hoyland, Douglas Stebila and me. Once upon a time... Observation: PQ signatures are quite big and/or …

A tale of two models: Formal analysis of KEMTLS in Tamarin Sofia Celi, Jonathan Hoyland, Douglas Stebila and me. Once upon a time... Observation: PQ signatures are quite big and/or …
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 …
The recent KEMTLS protocol (Schwabe, Stebila and Wiggers,CCS’20) is a promising design for a quantum-safe TLS handshake protocol. Focused on the web setting, wherein clients learn …
Invited lecture about TLS, its history and making TLS post quantum. I also discuss KEMTLS.
After a discussion on twitter I decided I should write down a few of the tips and tricks I’ve learnt over the years of writing papers and many other things in LaTeX.
The NIST post-quantum cryptography (PQC) standardization project is probably the largest and most ambitious cryptography standardization effort to date, and as such it makes an …
If you’re curious about some of the things I’ve worked on while at Cloudflare, see this post on Cloudflare’s internal blog.
An introduction to formal analysis and our proof of the security of KEMTLS.
Post-quantum key exchange and signature algorithms come with different trade-offs that we’re not used to. How do we handle that when updating protocols, and is this an opportunity …
A brief overview of three to-do/project management apps.