By Jonas Nick
We are excited to share the current progress on our research into the aggregation of signatures based on curve secp256k1: There is now an early draft Bitcoin Improvement Proposal (BIP) for non-interactive half-aggregation of BIP 340 Schnorr signatures. This proposal has a variety of potential applications in the Bitcoin ecosystem. Moreover, to the best of our knowledge, this would be the first BIP with a formal specification, which is a mathematically precise description of the scheme. The formal specification can be used to prevent multiple classes of security issues and potentially help future formal software verification efforts.
Half-Aggregation
About five years ago, signature half-aggregation was first mentioned on the Bitcoin mailing list. It allows aggregating multiple Schnorr signatures into a single signature that is about half as long as the sum of the individual signatures. Importantly, this scheme is non-interactive, which means that a set of signatures can be half-aggregated by a third party without any involvement from the signers. This scheme has been discussed on and off over the years in the Bitcoin space but only recently received attention from the academic community. Chalkias, Garillot, Kondi and Nikolaenko as well as Chen and Zhao prove security under sensible assumptions, which inspired us to start writing a specification. If you want to learn more about half-aggregation, have a look at the "cross-input signature aggregation" repository or this presentation and pair-programming session.
Bitcoiners have already come up with various potential applications for half-aggregation. For example, half-aggregation can reduce the bandwidth requirement of off-chain networks that gossip BIP-340 signatures. On the other hand, half-aggregation applied to the Bitcoin consensus protocol could cut down on the size of transactions in multiple ways:
- Bitcoin script opcodes requiring multiple signatures could take a single half-aggregate signature instead.
- Transactions could have a single half-aggregate signature instead of one signature per input.
- Since half-aggregation is non-interactive, block producers could aggregate transaction signatures into a single half-aggregate signature per block.
Note that some of these ideas have complex trade-offs (which are collected here). Our draft specification only covers the cryptographic scheme and does not prescribe a particular application. While it may be useful to some off-chain protocols immediately, we intend the half-aggregation specification to aid future discussions around consensus changes.
To avoid confusion, we would also like to mention a different signature aggregation approach that provides much larger space savings. We call it full aggregation because the size of the aggregate signature is equal to a regular Schnorr signature. However, due to its complexity, full aggregation is not always preferable to half aggregation. In particular, similar to the MuSig2 multi-signature scheme, full aggregation is an interactive protocol with at least two rounds and requires securely keeping signing state. Also, it (probably) does not permit deterministic signing without adding relatively massive complications to the scheme (similar to MuSig-DN for example). Therefore, we believe that even for protocols that already require interaction, the simplicity of half-aggregation may beat the efficiency of full aggregation.
Our specification of half aggregation differs from the scheme initially discussed on the mailing list by the added capability for incremental aggregation, which we found in Chen and Zhao's work. Incremental aggregation allows us to aggregate additional signatures into an existing half-aggregate signature. Surprisingly, this is a straightforward generalization of regular half-aggregation and does not add significant complexity to the specification.
Formal Specification
The half-aggregation BIP draft is similar in scope to BIP 340 ("BIP Schnorr") since both specify a cryptographic scheme without particular applications. BIP 340's specification consists of two parts, the actual specification in pseudocode and a reference implementation in python. This situation is not ideal. This situation is not ideal, primarily because the meaning of the pseudocode is not specified. The readers rely on their intuition to determine what the pseudocode is doing; this judgment may differ from reader to reader. The python reference implementation can help in case the pseudocode is unclear. Many programmers are familiar with python, and it comes with an extensive language reference. However, the reference manual describes the meaning of individual operations in natural language, which again leaves room for interpretation.
In contrast, the half-aggregation BIP draft has a formal specification. Each operation of the specification has a precisely defined meaning (semantics), which implies that the overall behavior of the scheme is unambiguous. Such precision is a nice feature, but on its own may not be worth the effort. Most importantly for us, the rigorous definition of the scheme paves the way for computer-aided formal proofs.
With software tools known as proof assistants, it is possible to prove that the formal specification has certain properties, like the absence of out-of-bound array access or integer overflow. Moreover, one can formally prove completeness of the specification, i.e., applying the aggregation algorithm to valid BIP 340 signatures always yields a valid half-aggregate signature. In principle, it is also possible to prove the security of the specified scheme using proof assistants. In the case of half-aggregation, this would be a relevant and ambitious research project.
Proving theorems about specifications is especially valuable because the behavior of specifications is often not identical to the abstract mathematical scheme they are based on. In fact, the security properties of the abstract scheme may not survive translation to a specification, leading to critical vulnerabilities. This problem can be circumvented if the proofs apply directly to the specification.
A formal specification is also a necessary prerequisite to do formal verification, which is the process of proving that the behavior of an implementation matches that of the specification. This allows for writing a highly optimized implementation and then formally verifying it against a specification. If the specification is correct, then the implementation is also correct, and proofs about the specification carry over.
Implementations that are supposed to undergo formal verification are generally not written in common programming languages. Instead, implementers use languages like Verifiable C or F* and its ecosystem.
The formal specification language we use for half-aggregation is hacspec. One of its most compelling features is that it is embedded in rust: hacspec specifications are also valid rust code. So one can build, run, manage dependencies and test the specification like any other rust project. Thus, the specification can also serve as a reference implementation and remove the need to add extra python code as in BIP 340. A downside is that readers of the BIP may not be as familiar with rust as with python. Additionally, hacspec code does not necessarily look like idiomatic rust and misses some primitives and rust standard library components. To help readers of the half-aggregation BIP draft, we also included informal pseudocode, which is similar in syntax and semantics to BIP 340's pseudocode. For the kind of theorem proving and software verification mentioned above, the hacspec typechecker program can translate hacspec code into specialized languages like Coq, F*, and EasyCrypt, which are starting points for proof engineering.
Conclusion
Half-aggregation of BIP 340 signatures has potential applications in various scenarios. We hope our half-aggregation BIP draft can serve as a valuable foundation for further exploration. We invite you to review the draft and provide feedback. What do you think about the absence of a python reference implementation and adding a formal specification written in hacspec? Besides being a fun experiment, we believe this is a promising direction that has the potential to advance the robustness of the Bitcoin ecosystem significantly.
Note: This blog was originally posted at https://medium.com/blockstream/half-aggregation-of-bip-340-signatures-163b4d7da1de