本文介绍了首个基于机械化证明的后量子安全协议验证方法。作者提出了PQ-BC，一种针对量子攻击者计算安全性的计算一阶逻辑，并实现了对应的机械化支持工具PQ-SQUIRREL。该工作基于经典的BC逻辑及其在SQUIRREL证明器中的机械化实现。PQ-BC的发展需要使BC逻辑对单一交互式量子攻击者保持完备性。作者通过修改SQUIRREL，依赖PQ-BC的完备性结果并强制执行一组语法条件，实现了PQ-SQUIRREL证明器；此外，还提供了新的策略来扩展工具范围。利用PQ-SQUIRREL，作者进行了多个案例研究，提供了首个机械化的后量子安全性证明，包括两个通用的基于KEM的密钥交换构造、IKEv1和IKEv2的两个子协议，以及Signal的X3DH协议的一个后量子变体。此外，他们用PQ-SQUIRREL证明了几个经典的SQUIRREL案例已经具有后量子安全性。这项工作的贡献在于将形式化验证扩展到后量子设置，为安全协议的后量子安全性提供了自动化的推理工具。