A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols.

该论文提出了首个面向协议计算后量子安全性的机械化证明体系。核心贡献是设计了一个新的计算一阶逻辑 PQ-BC，该逻辑相对量子攻击者是可靠的，并基于此实现了机械化证明工具 PQ-SQUIRREL（通过修改经典的 SQUIRREL 证明器并加入新

历史摘要 · 未重新核验 · IEEE S&P