Subterm-based proof techniques for improving the automation and scope of security protocol analysis

Cas Cremers; Charlie Jacomme; Philip Lukert

Paper 2022/1130

Subterm-based proof techniques for improving the automation and scope of security protocol analysis

Cas Cremers

, Helmholtz Center for Information Security

Charlie Jacomme

, Helmholtz Center for Information Security

Philip Lukert

, Helmholtz Center for Information Security

Abstract

During the last decades, many advances in the field of automated security protocol analysis have seen the field mature and grow from being applicable to toy examples, to modeling intricate protocol standards and finding real-world vulnerabilities that extensive manual analysis had missed. However, modern security protocols often contain elements for which such tools were not originally designed, such as protocols that construct, by design, terms of unbounded size, such as counters, trees, and blockchains. Protocol analysis tools such as Tamarin and ProVerif have some very restricted support, but typically lack the ability to effectively reason about dynamically growing unbounded-depth terms. In this work, we introduce subterm-based proof techniques that are tailored for automated protocol analysis in the Tamarin prover. In several case studies, we show that these techniques improve automation (allow for analyzing more protocols, or remove the need for manually specified invariants), efficiency (reduce proof size for existing analyses), and expressive power (enable new kinds of properties). In particular, we provide the first automated proofs for TreeKEM, S/Key, and Tesla Scheme~2; and we show substantial benefits, most notably in WPA2 and 5G-AKA, two of the largest automated protocol proofs.

Note: An extended abstract of this paper appears at CSF 2023. This is the long version.

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Published elsewhere. CSF 2023
Keywords: subterms symbolic models formal methods Tamarin prover
Contact author(s): cremers @ cispa de
charlie jacomme @ cispa de
philip lukert @ cispa de
History: 2022-08-31: approved; 2022-08-30: received; See all versions
Short URL: https://ia.cr/2022/1130
License: CC BY

BibTeX

@misc{cryptoeprint:2022/1130,
      author = {Cas Cremers and Charlie Jacomme and Philip Lukert},
      title = {Subterm-based proof techniques for improving the automation and scope of security protocol analysis},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1130},
      year = {2022},
      note = {\url{https://eprint.iacr.org/2022/1130}},
      url = {https://eprint.iacr.org/2022/1130}
}