CISPA
Browse
cispa_all_2941.pdf (778.81 kB)

Seems Legit: Automated Analysis of Subtle Attacks on Protocols that use Signatures

Download (778.81 kB)
conference contribution
posted on 2023-11-29, 18:11 authored by Daniel Jackson, Cas CremersCas Cremers, Katriel Cohn-Gordon, Ralf Sasse
The standard definition of security for digital signatures—existential unforgeability—does not ensure certain properties that protocol designers might expect. For example, in many modern signature schemes, one signature may verify against multiple different public keys. It is left to protocol designers to ensure that these properties do not break protocol security goals, often without success. Modern automated protocol analysis tools are able to prove the absence of large classes of attacks on complex real-world protocols such as TLS 1.3 and 5G. However, their abstraction of signatures assumes much more than existential unforgeability, thereby missing several classes of practical attacks. We give a hierarchy of new symbolic models for signature schemes that captures these subtleties, and thereby allows us to analyse (often unexpected) behaviours of real-world protocols that were previously out of reach of symbolic analysis. We implement our models in the Tamarin Prover, yielding the first way to perform these analyses automatically, and validate them on several case studies. In the process, we find new attacks on DRKey and SOAP’s WS-Security, both protocols which were previously proven secure in traditional symbolic models.

History

Preferred Citation

Daniel Jackson, Cas Cremers, Katriel Cohn-Gordon and Ralf Sasse. Seems Legit: Automated Analysis of Subtle Attacks on Protocols that use Signatures. In: ACM Conference on Computer and Communications Security (CCS). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

ACM Conference on Computer and Communications Security (CCS)

Legacy Posted Date

2019-07-03

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_2941, title = "Seems Legit: Automated Analysis of Subtle Attacks on Protocols that use Signatures", author = "Jackson, Daniel and Cremers, Cas and Cohn-Gordon, Katriel and Sasse, Ralf", booktitle="{ACM Conference on Computer and Communications Security (CCS)}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC