一条胜利于众：对使用聚合签名的协议进行形式化验证（扩展版）
密码学与安全
2025-05-16 v1
摘要
聚合签名是将来自不同方家的多个签名压缩为单个签名的数字签名，从而减少存储和带宽需求。BLS 聚合签名是一种流行的聚合签名类型，已被以太坊、Dfinity 和 Cloudflare 等部署，正在进行 IETF 标准化。然而，BLS 聚合签名使用起来困难，需要协议开发者小心处理细致要求。本文设计了首批能够使形式化验证工具（如 Tamarin 和 ProVerif）应用于使用这些签名的协议的模型。我们引入基于通用聚合签名加密安全定义的通用模型，允许攻击者利用安全要求未满足的协议。我们还引入了第二类模型，具体针对 BLS 聚合签名进行形式化建模。我们通过对一个名为 SANA 的设备认证协议进行建模和分析来展示我们方法的实际相关性。尽管 SANA 声称已提供正确性证明，但使用 Tamarin 我们发现了未记录的假设，当这些假设被省略时会导致攻击。
引用
@article{arxiv.2505.10316,
title = {One For All: Formally Verifying Protocols which use Aggregate Signatures (extended version)},
author = {Xenia Hofmeier and Andrea Raguso and Ralf Sasse and Dennis Jackson and David Basin},
journal= {arXiv preprint arXiv:2505.10316},
year = {2025}
}