One For All: Formally Verifying Protocols which use Aggregate Signatures (extended version)

TL;DR

This paper develops formal models for aggregate signatures, especially BLS signatures, enabling verification of protocols using these signatures and uncovering security flaws in a device attestation protocol.

Contribution

It introduces the first formal models for aggregate signatures suitable for verification tools, facilitating analysis of protocols like SANA for security flaws.

Findings

Uncovered undocumented assumptions in SANA protocol.

Demonstrated the applicability of models to real-world protocols.

Enabled formal verification of aggregate signature-based protocols.

Abstract

Aggregate signatures are digital signatures that compress multiple signatures from different parties into a single signature, thereby reducing storage and bandwidth requirements. BLS aggregate signatures are a popular kind of aggregate signature, deployed by Ethereum, Dfinity, and Cloudflare amongst others, currently undergoing standardization at the IETF. However, BLS aggregate signatures are difficult to use correctly, with nuanced requirements that must be carefully handled by protocol developers. In this work, we design the first models of aggregate signatures that enable formal verification tools, such as Tamarin and ProVerif, to be applied to protocols using these signatures. We introduce general models that are based on the cryptographic security definition of generic aggregate signatures, allowing the attacker to exploit protocols where the security requirements are not satisfied. We also introduce a second family of models formalizing BLS aggregate signatures in particular. We demonstrate our approach's practical relevance by modelling and analyzing in Tamarin a device attestation protocol called SANA. Despite SANA's claimed correctness proof, with Tamarin we uncover undocumented assumptions that, when omitted, lead to attacks.