A tale of two models: Formal verification of KEMTLS via Tamarin
Sofía Celi, Jonathan Hoyland, Douglas Stebila, Thom WiggersAbstract
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. Prior proofs of security of KEMTLS and its variant KEMTLS-PDK have been hand-written proofs in the reductionist model under computational assumptions. In this paper, we present computer-verified symbolic analyses of KEMTLS and KEMTLS-PDK using two distinct Tamarin models. In the first analysis, we adapt the detailed Tamarin model of TLS 1.3 by Cremers et al. (ACM CCS 2017), which closely follows the wire-format of the protocol specification, to KEMTLS(-PDK). 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 required 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 from prior pen-and-paper proofs 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.