A tale of two models: formal verification of KEMTLS in Tamarin

KEMTLS is a proposal for changing the TLS handshake to authenticate the handshake using long-term key encapsulation mechanism keys instead of signatures, motivated by trade-offs in the characteristics of post-quantum algorithms. Proofs of the security of KEMTLS and its variant KEMTLS-PDK have previously been done manually in the reductionist model under computational assumptions. In this paper, we present analyses of KEMTLS and KEMTLS-PDK using two distinct Tamarin models. In the first analysis, we adapt the extensive Tamarin model of TLS 1.3 of Cremers et al. (ACM CCS 2017) to KEMTLS(-PDK); this model closely follows the wire-format of the protocol specification. We show that KEMTLS(-PDK) has the same security properties as TLS 1.3 in this model. We were able to fully automate this Tamarin proof, compared with the previous TLS 1.3 Tamarin model, which requires a big manual proving effort; we also uncovered some inconsistencies in the previous model. In the second analysis, we present a novel Tamarin model of KEMTLS(-PDK), which closely follows the “multi-stage key exchange” security model in the pen-and-paper proof of KEMTLS(-PDK). The second approach is further away from the wire-format of the protocol specification but captures more subtleties in security definitions, like deniability and different levels of forward secrecy; it also identifies some flaws in the security claims from the pen-and-paper proofs. Our positive security results increase the confidence in the design of KEMTLS(-PDK). Moreover, viewing these models side-by-side allows us to comment on the trade-off in symbolic analysis between detail in protocol specification and granularity of security properties.

ESORICS 2022