A tale of two models: formal analysis of KEMTLS in Tamarin
Conference presentation of our KEMTLS formal analysis paper at ESORICS 2022
Thom Wiggers
Senior Cryptography Researcher
Thom Wiggers is a cryptography researcher at PQShield.
His PhD thesis was on the interactions of post-quantum cryptography with protocols, under the supervision of Peter Schwabe, at the Institute of Computing and Information Sciences, Radboud University in The Netherlands.
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 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 …
Sofía Celi
KEMTLS with Delayed Forward Identity Protection in (Almost) a Single Round
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 …
felix-gunther
Invited Lecture: TLS and Post-Quantum (Applied Cryptography, Radboud University)
Invited lecture about TLS, its history and making TLS post quantum. I also discuss KEMTLS.
LaTeX Tips and Tricks
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.
Improving Software Quality in Cryptography Standardization Projects
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 …
Matthias J. Kannwischer
Cloudflare Internship
If you’re curious about some of the things I’ve worked on while at Cloudflare, see this post on Cloudflare’s internal blog.
Building confidence in cryptographic protocols
An introduction to formal analysis and our proof of the security of KEMTLS.
Making protocols post-quantum
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 …