软件学报

作者：田新蕾，董奕逸，张济显，王伟嘉

单位：田新蕾，山东大学 网络空间安全学院, 山东 青岛 26623711,董奕逸，山东大学 网络空间安全学院, 山东 青岛 26623702,张济显，山东大学 网络空间安全学院, 山东 青岛 26623703,王伟嘉，山东大学 网络空间安全学院, 山东 青岛 266237;泉城实验室, 山东 济南 25010304

关键词：后量子密码;Falcon;形式化验证;Jasmin;EasyCrypt

基金：国家重点研发计划 (2023YFA1009500, 2021YFA1000600); 国家自然科学基金 (62372273); 泉城实验室重点项目 (QCLZD202306)

Falcon作为一种后量子数字签名算法, 被选为美国国家标准与技术研究院(National Institute of Standards and Technology, NIST)首批标准化方案之一. Falcon的核心算法在实际实现中很容易出错，引发可能的密码学误用问题. 对 Falcon 核心函数进行形式化验证, 以确保其正确性是非常重要的. 在过去 10 年中,计算机辅助密码学领域将形式化方法引入了密码学工程. 这使得高性能密码实现具有了强有力的函数正确性和特定实现安全性属性的形式化保证. 贡献包括: (1) 构建了完整的证明框架, 通过形式化验证方法, 成功弥合了 Falcon 的实际代码实现与数学描述之间的差距; (2) 在 EasyCrypt 证明体系中验证了 Falcon 中的 Montgomery 模乘、NTT 算法、FFT 算法的正确性, 并对整数高斯采样算法的正确性证明方法进行了探索; (3) 给出及优化了基于 Jasmin 混合编程的 Falcon 签名与验证实现.

来源：2025年第11期

《软件学报》期刊编辑部

查看软件学报杂志2025年第11期