本文针对认证数据结构（Authenticated Data Structures）的开发与实现正确性难题，提出了一种基于新关系分离逻辑的形式化证明方法。认证数据结构允许不可信的第三方执行操作并生成可验证的输出证明，但此类系统容易因实现错误导致安全漏洞。作者首先设计了一种关系分离逻辑，用于推理使用抗碰撞哈希函数的程序，该逻辑为类型系统构建了两个语义模型，从而阐释了如何通过类型抽象来强制实现安全性与正确性。基于这些模型，论文进一步证明了库中多项优化的正确性，并展示了如何将优化的、手工编写的认证数据结构实现与自动生成的代码安全链接。所有结果均在 Coq 证明助手中使用 Iris 框架完成机械化验证。该工作为认证数据结构库的可靠实现提供了坚实的理论基础，有助于减少此类系统中的安全缺陷。适合形式化验证、编程语言理论与安全协议交叉领域的研究者阅读。