Douglas Stebila

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

Comparison of features in our two Tamarin models of KEMTLS.

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.

Keywords: post-quantum cryptography, TLS, key exchange, KEMTLS

Reference

Sofía Celi, Jonathan Hoyland, Douglas Stebila, Thom Wiggers. A tale of two models: formal verification of KEMTLS via Tamarin. In Vijay Atluri, Roberto di Pietro, editors, Proc. 27th European Symposium on Research in Computer Security (ESORICS) 2022, LNCS, vol. 13556, pp. 63–83. Springer, September 2022. © Springer.

Download

Code

• KEMTLS main website
• Tamarin model #1
• Tamarin model #2

BibTeX

@inproceedings{ESORICS:CHST22,
 	Author = {Sof{\' i}a Celi and Jonathan Hoyland and Douglas Stebila and Thom Wiggers},
 	Booktitle = {Proc. 27th European Symposium on Research in Computer Security (ESORICS) 2022},
 	Doi = {10.1007/978-3-031-17143-7_4},
 	Editor = {Vijay Atluri and Roberto di Pietro},
 	Month = {September},
 	Pages = {63--83},
 	Publisher = {Springer},
 	Series = {LNCS},
 	Title = {A tale of two models: formal verification of {KEMTLS} via {T}amarin},
 	Volume = {13556},
 	Year = {2022}
 }

Funding

• Natural Sciences and Engineering Research Council of Canada (NSERC) Discovery grant RGPIN-2016-05146
• Natural Sciences and Engineering Research Council of Canada (NSERC) Discovery grant RGPIN-2022-03187
• NLnet Assure grant for the project "Standardizing KEMTLS"
• European Research Council through Starting Grant No. 805031 (EPOQUE)