CISPA
Browse
cispa_all_3849.pdf (752.32 kB)

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

Download (752.32 kB)
Version 2 2023-12-11, 20:15
Version 1 2023-11-29, 18:26
conference contribution
posted on 2023-12-11, 20:15 authored by Cas CremersCas Cremers, Charlie Jacomme, Philip Lukert
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.

History

Preferred Citation

Cas Cremers, Charlie Jacomme and Philip Lukert. Subterm-based proof techniques for improving the automation and scope of security protocol analysis. In: IEEE Computer Security Foundations Symposium (CSF). 2022.

Primary Research Area

  • Threat Detection and Defenses

Name of Conference

IEEE Computer Security Foundations Symposium (CSF)

Legacy Posted Date

2022-10-14

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3849, title = "Subterm-based proof techniques for improving the automation and scope of security protocol analysis", author = "Cremers, Cas and Jacomme, Charlie and Lukert, Philip", booktitle="{IEEE Computer Security Foundations Symposium (CSF)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC