Transactions on Cryptographic Hardware and Embedded Systems, Volume 2022
Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, Saber, and NTRU
Academia Sinica and National Taiwan University
IBM Research Zurich
National Applied Research Labs
Keywords: 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.
Transactions of Cryptographic Hardware and Embedded Systems, Volume 2022, Issue 4Paper
October 31, 2022
BibTeX 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. https://doi.org/10.46586/tches.v2022.i4.718-750. Artifact available at https://artifacts.iacr.org/tches/2022/a20