Cryptology ePrint Archive: Report 2019/779

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

Dennis Jackson and Cas Cremers and Katriel Cohn-Gordon and Ralf Sasse

Abstract: 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.

Category / Keywords: cryptographic protocols / signature schemes, symbolic models, formal methods, Tamarin prover

Original Publication (with minor differences): ACM CCS 2019

Date: received 3 Jul 2019

Contact author: cas cremers at gmail com

Available format(s): PDF | BibTeX Citation

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

Version: 20190709:182139 (All versions of this report)

Short URL: ia.cr/2019/779