Agda：扩展版中已认证、仅认证的跳表的形式化验证
Formal Verification of Authenticated, Append-Only Skip Lists in Agda: Extended Version
摘要：
经过身份验证的仅限登录的Skiplists（AAOSL）可以维护和查询经过身份验证的日志（例如区块链），而无需任何一方存储或验证整个日志，或者信任另一方关于其内容。AAOSL可以帮助实现有效的动态参与（例如，一致）并减少存储开销。在本文中，我们形式化的AAOSL最初描述的Maniatis和Baker，并证明其关键的正确性。我们的模型和证据是机器检查在阿格达。我们的证明适用于原来的建设推广，并提供信心，这种推广的实例可以在实践中使用。我们的形式化工作也产生了一些简化和优化。
英文摘要：
Authenticated Append-Only Skiplists (AAOSLs) enable maintenance and querying of an authenticated log (such as a blockchain) without requiring any single party to store or verify the entire log, or to trust another party regarding its contents. AAOSLs can help to enable efficient dynamic participation (e.g., in consensus) and reduce storage overhead. In this paper, we formalize an AAOSL originally described by Maniatis and Baker, and prove its key correctness properties. Our model and proofs are machine checked in Agda. Our proofs apply to a generalization of the original construction and provide confidence that instances of this generalization can be used in practice. Our formalization effort has also yielded some simplifications and optimizations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
