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.