这篇 SoK（系统化知识）论文对计算机辅助密码学（Computer-Aided Cryptography）领域进行了跨领域的系统化梳理。计算机辅助密码学是一个活跃的研究方向，致力于开发和应用形式化、机器可检查的方法来设计、分析和实现密码学协议。论文聚焦于三个主要领域：（1）设计级安全性，涵盖符号安全性和计算安全性；（2）功能正确性与效率；（3）实现级安全性，重点关注数字侧信道抗性。在每个领域中，作者首先阐明了计算机辅助密码学在应对当前挑战中的作用——它能提供何种帮助以及存在的注意事项；随后提出了对现有工具的 taxonomy（分类法），比较了它们的准确性、覆盖范围、可信度和易用性；接着 highlights（重点介绍）了主要成就、权衡取舍和研究挑战。在覆盖这三个主要领域之后，论文呈现了两个案例研究：第一个研究尝试整合不同领域的工具，以巩固它们能提供的保证；第二个研究总结了计算机辅助密码学社区参与 TLS 1.3 标准化工作的经验教训。最后，论文对论文作者、工具开发者和标准化组织提出了未来发展的建议。该论文是该领域的权威性综述，适合密码学研究者、安全形式化方法开发者、协议设计者以及标准化参与者阅读。