量子科技中心_量科网

Barrett约简是所有基于NTT的后量子密码学实际实现中的非线性核心。现有组合框架（ISW、t-SNI、PINI、DOM）仅处理GF(2)上的布尔掩码；在素数域上的一阶算术掩码和一阶探测模型下，尚无任何框架能提供关于Barrett泄漏的形式化机器验证表征。基于该团队先前系列工作——QANARY[15]、部分NTT掩码边界[14]、代数基础[16]以及蝶形组合[18]——该工作填补了这一空白。该工作证明了一个三分法：对于任意q>0和移位s，Barrett内部线映射fx(m)=((x+2s−m)mod2s)modq的原像基数属于{0,1,2}，且绝不超过2。该工作将此称为"1比特屏障"：最大重数2意味着每条内部线的最小熵损失至多为1比特，这一结论对所有模数具有普适性。计数为零的情况（即不可达输出值）表明实际泄漏通常严格小于1比特，因此该边界是保守的。该工作引入PF-PINI（素数域PINI）：Barrett满足PF-PINI(2)；Cooley-Tukey蝶形满足PF-PINI(1)。该工作观察到（尚未证明）若引入级间新鲜掩码，组合流水线的最大重数为max(k1,k2)，因此1比特屏障得以传播。该三分法、PF-PINI实例化以及基数结果已在Lean 4与Mathlib中完成机器验证：12个已证明结论，零个未完成项，对所有q>0普适（最小熵边界由标准定义推导）。Adams Bridge缺乏级间新鲜掩码，违反了PF-PINI组合规则，这解释了为何论文1[15]和论文2[14]发现了漏洞。NIST IR 8547建议对PQC实现验证采用形式化方法。1比特屏障为ML-KEM（FIPS 203）和ML-DSA（FIPS 204）中掩码Barrett约简提供了首个普适的机器验证基数边界，并对应1比特泄漏解释。