Paper 2019/779

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

Dennis Jackson, Cas Cremers, Katriel Cohn-Gordon, and 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 distinct public keys. It is left to protocol designers to ensure that the absence of these properties does not lead to attacks. Modern automated protocol analysis tools are able to provably exclude large classes of attacks on complex real-world protocols such as TLS 1.3 and 5G. However, their abstraction of signatures (implicitly) assumes much more than existential unforgeability, thereby missing several classes of practical attacks. We give a hierarchy of new formal 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.

Note: An extended abstract of this paper appears at ACM CCS 2019. This is the long version.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. MINOR revision.ACM CCS 2019
signature schemessymbolic modelsformal methodsTamarin prover
Contact author(s)
cas cremers @ gmail com
2019-07-09: received
Short URL
Creative Commons Attribution


      author = {Dennis Jackson and Cas Cremers and Katriel Cohn-Gordon and Ralf Sasse},
      title = {Seems Legit: Automated Analysis of Subtle Attacks on Protocols that Use Signatures},
      howpublished = {Cryptology ePrint Archive, Paper 2019/779},
      year = {2019},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.