量智信息中心_量科网

这是后量子密码学掩码NTT硬件形式化验证系列论文的第7篇；第1篇论文[1]建立了QANARY平台的结构依赖性分析，第2篇论文[2]量化了部分NTT掩码下的安全裕度。对于任意深度的k级掩码NTT流水线（采用级间新鲜掩码和每级PF-PINI(≤2)组件），该工作证明任意输出值的原像满足每次观测的基数界限为2·q²ᵏ⁻²，该结果在Lean 4中经过机器验证，且不含任何\texttt{sorry}。根据标准的（非正式）语义转换（将该基数除以总掩码元组空间大小q²ᵏ⁻¹），每次观测的条件概率界限为2/q，与流水线深度k无关。QANARY程序此前已为掩码NTT硬件的每次观测泄露建立了机器验证的基数界限：Barrett约简的PF-PINI(2)（第5篇论文[3]）、带级间新鲜掩码的2级组合（第6篇论文[4]）、底层通用性定理（第3篇论文[5]）以及蝶形线路的PF-PINI(1)（第4篇论文[6]）。本文通过四项贡献为该程序画上句号。第一，将第6篇论文的两级结果推广至任意k≥1的k级组合定理，给出末级决定的界限Gₖ₋₁.𝚖𝚊𝚡𝙼𝚞𝚕𝚝·q²ᵏ⁻²：仅末级的PF-PINI参数保留，中间参数被级间新鲜掩码消除。第二，Montgomery约简满足PF-PINI(2)且紧致最大重数为2。第三，研究人员将这些结果整合为任意深度k的PF-PINI(≤2)流水线在级间新鲜掩码下的端到端界限2·q²ᵏ⁻²。第四，一个经Lean验证的假设违反条件锚定了先前的经验性和结构性Adams Bridge分析（[1, 2, 7, 8]）。