格基密码学中数论变换的代数线性分析

摘要

随着NIST后量子密码系统新标准的最终确定以及各国发布在未来十年内转向后量子或至少混合密码的指令，验证后量子密码软件的主题比以往任何时候都更加紧迫。验证格基密码软件的一个关键问题是在高度优化的密码软件中频繁出现的有限域算术汇编代码中的范围检查。这些问题大部分通过可满足性模理论（SMT）处理，但到目前为止，主要局限于Montgomery算术和16位精度。我们通过整数集库（通过python包islpy包装）为CryptoLine工具包添加了半自动范围检查推理能力，这使得验证更多算术密码代码（包括Barrett和Plantard有限域算术）变得更加容易和快速，并通过实验证明这在生产代码中是可行的。

关键词

整数集库, CryptoLine, 形式化验证, 汇编代码

作者

Chun-Ming Chiu - 国立台湾大学，台北，台湾
Jiaxiang Liu - 中国科学院系统软件重点实验室及计算机科学国家重点实验室，软件研究所，北京，中国
Ming-Hsien Tsai - 国立台湾科技大学，台北，台湾
Xiaomu Shi - 中国科学院系统软件重点实验室及计算机科学国家重点实验室，软件研究所，北京，中国
Bow-Yaw Wang - 中央研究院，台北，台湾
Bo-Yin Yang - 中央研究院，台北，台湾

出版信息

DOI: https://doi.org/10.46586/tches.v2025.i3.668-692
出版日期: 2025-06-05
卷期: Vol. 2025 No. 3
章节: 文章

许可

引用方式

Chiu, C.-M., Liu, J., Tsai, M.-H., Shi, X., Wang, B.-Y., & Yang, B.-Y. (2025). Algebraic Linear Analysis for Number Theoretic Transform in Lattice-Based Cryptography. IACR Transactions on Cryptographic Hardware and Embedded Systems, 2025(3), 668-692. https://doi.org/10.46586/tches.v2025.i3.668-692