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

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.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. CSF 2023
subterms symbolic models formal methods Tamarin prover
Contact author(s)
cremers @ cispa de
charlie jacomme @ cispa de
philip lukert @ cispa de
2022-08-31: approved
2022-08-30: received
See all versions
Short URL
Creative Commons Attribution


      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{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.