| 摘要: |
| Falcon作为一种后量子数字签名算法, 被选为美国国家标准与技术研究院(National Institute of Standards and Technology, NIST)首批标准化方案之一. Falcon的核心算法在实际实现中很容易出错，引发可能的密码学误用问题. 对 Falcon 核心函数进行形式化验证, 以确保其正确性是非常重要的. 在过去 10 年中,计算机辅助密码学领域将形式化方法引入了密码学工程. 这使得高性能密码实现具有了强有力的函数正确性和特定实现安全性属性的形式化保证. 贡献包括: (1) 构建了完整的证明框架, 通过形式化验证方法, 成功弥合了 Falcon 的实际代码实现与数学描述之间的差距; (2) 在 EasyCrypt 证明体系中验证了 Falcon 中的 Montgomery 模乘、NTT 算法、FFT 算法的正确性, 并对整数高斯采样算法的正确性证明方法进行了探索; (3) 给出及优化了基于 Jasmin 混合编程的 Falcon 签名与验证实现. |
| 关键词: 后量子密码 Falcon 形式化验证 Jasmin EasyCrypt |
| DOI：10.13328/j.cnki.jos.007368 |
| 分类号:TP311 |
| 基金项目:国家重点研发计划 (2023YFA1009500, 2021YFA1000600); 国家自然科学基金 (62372273); 泉城实验室重点项目 (QCLZD202306) |
|
| Formal Verification Techniques for Implementing Post-quantum Cryptography Falcon |
|
TIAN Xin-Lei1, DONG Yi-Yi1, ZHANG Ji-Xian1, WANG Wei-Jia1,2
|
|
1.School of Cyber Science and Technology, Shandong University, Qingdao 266237, China;2.Quan Cheng Laboratory, Jinan 250103, China
|
| Abstract: |
| Falcon, a post-quantum digital signature algorithm, has been selected as one of the first schemes standardized by the National Institute of Standards and Technology (NIST). Its core algorithms, however, are highly error-prone in practical implementations, raising risks of cryptographic misuse. Ensuring the correctness of Falcon through formal verification is therefore essential. In this work, this study introduces a comprehensive proof framework that bridges the gap between Falcon’s mathematical specification and its real-world implementation. Within the EasyCrypt proof system, this study formally verifies the correctness of Falcon’s Montgomery modular multiplication, NTT, and FFT algorithms, and further explores proof techniques for integer Gaussian sampling. Moreover, this study presents and optimizes Falcon’s signing and verification implementations using Jasmin hybrid programming, thereby providing both formal correctness guarantees and practical efficiency. |
| Key words: post-quantum cryptography Falcon formal verification Jasmin EasyCrypt |
