本文提出了一种针对基于2-power cyclotomic环的模块格密码系统的概率多项式时间量子攻击。攻击的核心创新在于利用扩域链Q⊂Q(ζ_8)⊂⋯⊂Q(ζ_{2^k})对主理想问题（PIP）进行塔式分解，将高维格上的困难问题转化为低维子域上的可解问题。对于ML-KEM-1024，作者验证了逼近因子γ≤21<q/2=1665，成功概率≥0.99。该量子算法需要O(n^3 log^2 n)个量子门、O(n^2 log n)个量子比特和多项式时间的经典计算。攻击同样适用于Falcon、Hawk、NTRU-HPS和NTRU-HRSS的所有标准化参数集。这一结果意味着，如果攻击被证实正确，那么当前NIST选定的后量子密码标准中基于2-power cyclotomic环的多个方案将不再安全。论文是作者系列工作的第四部分，提供了完整的理论分析和算法复杂度证明。

论文提出了一种混合形式化验证方法，结合高层演绎推理和电路级推理，用于高度优化的加密汇编代码。该方法在 EasyCrypt 证明助手中扩展实现，通过使用等价性检查将安全保障传播到同一计算的不同优化或不同架构的实现中，从而降低低级别函数的证明工作量，并分摊证明开销。论文以 ML-KEM（一种后量子密码算法）在 Jasmin 中的形式化验证实现为例，首次获得了在 x86-64 架构上性能与最快非验证实现相当的形式化验证实现。这证明了混合方法在兼顾性能与安全性方面的有效性。研究背景在于现有形式化验证方法在处理深度优化汇编代码时面临可扩展性挑战，而本文结合两种推理范式，利用电路级推理处理底层优化细节，利用演绎推理处理高层语义，显著提升了验证效率。实验结果表明，该方法能够在保持高性能的同时实现形式化安全保障，适合对密码学实现安全性和正确性有高要求的场景。