量智信息中心_量科网

这是后量子密码学掩码NTT硬件形式化验证系列论文的第6篇；论文1[1]建立了QANARY平台的依赖分析，论文2[2]量化了部分NTT掩码下的安全裕度。布尔掩码的复合性质通过NI、SNI和PINI等概念已得到充分理解。而基于素数q的ℤq上的算术掩码——作为基于NTT的后量子密码学的基础——却一直缺乏类似的理论框架。据该团队所知，该团队证明了素数域上算术掩码的首个机器验证复合定理。该工作的核心见解在于更新论证：当在两个流水线阶段之间应用一个全新的随机掩码时，无论阶段1的安全参数如何，中间导线都会变得完全均匀。对于两个参数分别为k1和k2的PF-PINI组件，采用新鲜掩码的两级流水线复合结构满足PF-PINI(k2)性质，阶段1的多重性在复合输出中被完全消除。若没有新鲜掩码，中间导线的多重性最高可达k1，这为差分功耗分析创造了必要条件。该工作在Lean 4中形式化了这两个定理，包含18个机器验证的证明和零个未完成存根。该工作正式桥接了巴雷特归约的代数模型与硬件忠实算术模型，并将定理应用于微软Adams Bridge PQC加速器的形式化诊断：其缺乏级间新鲜掩码导致巴雷特输出导线在一阶探测模型下非均匀，这正是两项独立实证分析[3, 4]及该工作前期结构分析[1]所发现的相同架构缺陷。计算证据进一步表明，1比特屏障在巴雷特归约和蒙哥马利归约中具有普遍性。