该论文提出了首个面向协议计算后量子安全性的机械化证明体系。核心贡献是设计了一个新的计算一阶逻辑 PQ-BC，该逻辑相对量子攻击者是可靠的，并基于此实现了机械化证明工具 PQ-SQUIRREL（通过修改经典的 SQUIRREL 证明器并加入新策略）。PQ-BC 的构建需要对经典 BC 逻辑进行扩展，使其在单一交互式量子攻击者模型下保持可靠性，同时通过强制一组语法条件来保证工具的正确性。利用 PQ-SQUIRREL，作者完成了多个案例研究，首次给出了计算后量子安全性的机械证明，包括两个基于 KEM 的密钥交换通用构造、IKEv1 和 IKEv2 的两个子协议，以及 Signal X3DH 协议的一个后量子变体。此外，该工具还证明了许多经典的 SQUIRREL 案例研究已经具备后量子安全性。这项工作为后量子安全协议分析提供了基础性工具，填补了机械化后量子安全证明领域的空白。适合密码学协议设计者、形式化验证研究人员以及关注后量子迁移的安全工程师阅读。