3

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
Improving Software Quality in Cryptography Standardization Projects

The NIST post-quantum cryptography (PQC) standardization project is probably the largest and most ambitious cryptography …

Preprint PDF