Vincent Hwang
Academia Sinica and National Taiwan University

Jiaxiang Liu
Shenzhen University

Gregor Seiler
IBM Research Zurich

Xiaomu Shi
Shenzhen University

Ming-Hsien Tsai
National Applied Research Labs

Bow-Yaw Wang
Academia Sinica

Bo-Yin Yang
Academia Sinica

Keywords: NIST PQC, NTT, Verification, NTRU, Kyber, Saber

Abstract

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.