### A tale of two models: formal verification of KEMTLS via Tamarin

##### Abstract

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 equivalent security properties to the main handshake of TLS 1.3 proven 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.

Available format(s)
Category
Public-key cryptography
Publication info
Published elsewhere. ESORICS 2022
Keywords
KEMTLS formal methods TLS Tamarin
Contact author(s)
cherenkov @ riseup net
jhoyland @ cloudflare com
dstebila @ uwaterloo ca
thom @ thomwiggers nl
History
2022-08-29: approved
See all versions
Short URL
https://ia.cr/2022/1111

CC BY

BibTeX

@misc{cryptoeprint:2022/1111,
author = {Sofía Celi and Jonathan Hoyland and Douglas Stebila and Thom Wiggers},
title = {A tale of two models: formal verification of KEMTLS via Tamarin},
howpublished = {Cryptology ePrint Archive, Paper 2022/1111},
year = {2022},
note = {\url{https://eprint.iacr.org/2022/1111}},
url = {https://eprint.iacr.org/2022/1111}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.