Post-Quantum

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.

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