该论文研究了认证数据结构（Authenticated Data Structures）的形式化验证问题。认证数据结构允许不可信的第三方执行操作并生成可验证操作输出的证明，但这类数据结构的正确实现具有挑战性。本文提出了一种基于关系分离逻辑（relational separation logic）的新方法，用于对使用抗碰撞哈希函数的程序进行推理。作者利用该逻辑构建了类型系统的两个语义模型，从而证明了自动生成认证数据结构的库在安全性和正确性方面的性质。此外，论文还验证了该库的若干优化，并展示了如何将优化的手写认证数据结构实现与自动生成的代码安全地链接。所有结果均在Coq证明助手中使用Iris框架进行了机械化。该工作为认证数据结构的可靠实现提供了理论基础，适合对形式化验证、程序逻辑和密码学协议感兴趣的研究人员阅读。