Formalizing Aggregate Signatures in the Symbolic Model

Abstract

Security protocols are a crucial part of most applications. In recent years, automated formal verification tools, such as Tamarin and ProVerif, were effectively used to prove security properties and find attacks on complex protocols, such as 5G and TLS. To widen the range of protocols that can be modeled, we need new symbolic models of the underlying cryptographic primitives. An exciting family of signatures that have not been deeply studied in the symbolic model are multi-party signatures. This class of signatures includes blind signatures, which gained importance through e-voting, proxy signatures, which are crucial for some distributed systems, and aggregate signatures, which are applied in blockchains. We present the first symbolic models for aggregate signatures, namely BonehLynn-Shacham (BLS) signatures, in the Tamarin Prover. Signature aggregation enables combining multiple signatures into one short signature, which reduces storage and bandwidth requirements. This is especially beneficial in applications with a large number of signatures and signing parties, such as certificate chains or blockchains. In contrast to other multi-party signature models that only consider a fixed number of parties, our model allows an arbitrary number of signers, which poses interesting challenges to correctly represent the individual elements and to achieve termination. We explore attacks on aggregate signatures and apply methods of recent works that improved symbolic models of signatures. We extend our models to cover attacks with two effective approaches: firstly, we explicitly enable certain attacks, and secondly, we create models that implicitly allow subtle behaviors that are not forbidden by the computational definition. Those methods allow us to prove properties under fewer assumptions and to find more attacks than with a standard model. The evaluation of our models using a synthetic protocol shows that our models are effective and the analysis of isolated examples provides confidence in the correctness of our models. With our models, it is possible to develop models for real-world protocols that rely on aggregate signatures. We developed different techniques to model the aggregation of arbitrarily many signatures. Those techniques are highly promising for future models of further multi-party signatures, which would further enlarge the number of protocols that can be modeled by automated formal verification tools.