KEMTLS

I gave an overview of the challenges for transitioning TLS to PQC, and highlighted a number of proposals to mitigate the impact of large post-quantum signatures.

Ph.D. thesis on post-quantum cryptography in TLS. I investigate current proposals for post-quantum TLS, but more importantly we propose …

The ubiquitous use of smartphones has contributed to more and more users conducting their online browsing activities through apps, …

Conference talk about our publication KEMTLS vs. Post-Quantum TLS: Performance on Embedded Systems at SPACE 2022

We investigate the performance of KEMTLS and PQ instantiations of TLS 1.3 on embedded devices.

We investigate the performance of post-quantum TLS and KEMTLS clients in WolfSSL on embedded systems

Conference presentation of our KEMTLS formal analysis paper at ESORICS 2022

A tale of two models: Formal analysis of KEMTLS in Tamarin Sofía Celi, Jonathan Hoyland, Douglas Stebila and Thom Wiggers. Once upon a time... Observation: PQ signatures are quite big and/or slow Idea: Use KEMs for authentication Proposal: KEMTLS KEMTLS sequenceDiagram Client->>+Server: ClientHello: ephemeral kex Server->>-Client: ServerHello: ephemeral kex Server->>+Client: Certificate: static KEM pk Client->>-Server: Ciphertext Client->>Server: ClientFinished rect rgba(0, 0, 0, 0) Client-->>Server: Application Data end Server->>Client: ServerFinished Server-->>Client: Application Data sequenceDiagram Client->>+Server: ClientHello: ephemeral kex Server->>-Client: ServerHello: ephemeral kex Server->>+Client: Certificate: static KEM pk Client->>-Server: Ciphertext Client->>Server: ClientFinished rect pink Client-->>Server: Application Data end Server->>Client: ServerFinished Server-->>Client: Application Data Ephemeral KEM key exchange KEM public key in certificate Avoid extra round-trip by letting client send data immediately KEMTLS variants Mutual authentication What if the client already knows the server's public key?

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.