该论文对IETF RFC 8555标准化的ACME证书颁发与管理协议进行了深入的符号化安全分析。ACME协议是Web公钥基础设施（PKI）的核心组成部分，被Let's Encrypt等证书颁发机构用于颁发超过10亿张证书，目前绝大多数HTTPS连接都依赖通过ACME颁发的证书。然而，尽管ACME至关重要，其安全性此前并未像TLS 1.3或OAuth等其他协议标准那样得到深入分析。以往的形式化分析仅考虑了早期草案版本的加密核心，忽略了许多安全关键的低级细节，这些细节在长达100页的RFC中占据重要地位，例如递归数据结构、带有异步子协议的长时间运行会话、以及针对多域名证书的颁发。本研究通过建立全面的符号模型，涵盖了ACME协议的所有主要功能和安全目标，包括客户端与服务器之间的交互、域名验证、证书请求与颁发、以及撤销等流程。分析发现了一些先前未知的安全缺陷，例如在某些配置下，攻击者可能通过操纵域名验证过程或利用状态混淆来获得未经授权的证书。该研究还提出了协议改进建议，并验证了修复措施的有效性。这项工作对于理解ACME协议的实际安全性、指导部署配置以及未来协议演进具有重要意义。适合协议设计者、安全研究员以及PKI实施者阅读。