Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU


  • Vincent Hwang Academia Sinica, Taipei, Taiwan; National Taiwan University, Taipei, Taiwan
  • Jiaxiang Liu Shenzhen University, Shenzhen, China
  • Gregor Seiler IBM Research Zurich, Zurich, Switzerland
  • Xiaomu Shi Shenzhen University, Shenzhen, China
  • Ming-Hsien Tsai National Applied Research Labs, Taipei, Taiwan
  • Bow-Yaw Wang Academia Sinica, Taipei, Taiwan
  • Bo-Yin Yang Academia Sinica, Taipei, Taiwan



NIST PQC, NTT, verification, NTRU, Kyber, Saber


Postquantum cryptography requires a different set of arithmetic routines from traditional public-key cryptography such as elliptic curves. In particular, in each of the lattice-based NISTPQC Key Establishment finalists, every state-ofthe-art optimized implementation for lattice-based schemes still in the NISTPQC round 3 currently uses a different complex multiplication based on the Number Theoretic Transform. We verify the NTT-based multiplications used in NTRU, Kyber, and SABER for both the AVX2 implementation for Intel CPUs and for the pqm4 implementation for the ARM Cortex M4 using the tool CryptoLine. e extended CryptoLine and as a result are able to verify that in six instances multiplications are correct including range properties.
We demonstrate the feasibility for a programmer to verify his or her high-speed assembly code for PQC, as well as to verify someone else’s high-speed PQC software in assembly code, with some cooperation from the programmer.




How to Cite

Hwang, V., Liu, J., Seiler, G., Shi, X., Tsai, M.-H., Wang, B.-Y., & Yang, B.-Y. (2022). Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU. IACR Transactions on Cryptographic Hardware and Embedded Systems, 2022(4), 718–750.