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

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.