Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆

As engineers continue to develop more sophisticated algorithms to optimize cryptographic algorithms, their often simple mathematical specifications become convoluted in the algorithms, from which a class of correctness bugs arise. Because cryptographic algorithms often secure sensitive information, their correctness, and in turn their security is a top priority. The Number Theoretic Transform (NTT) is an algorithm that enables efficient polynomial multiplication and has recently gained importance in post-quantum cryptography. This thesis presents a proof of correctness of the NTT in F⋆ , a proof-oriented programming language that extracts to OCaml, and shows that we can use the NTT to perform polynomial multiplications. We provide an implementation of the Cooley-Tukey fast NTT algorithm and a proof that it matches the original NTT specification. This thesis also presents a representation of polynomials in the F⋆ subset Low*, which extracts to performant C code.

Name thesis:degree_name

Master

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2024

Author dc:creator

• Ono, Rick R.

Advisors dc:contributor.advisor

• Athalye, Anish
• Zeldovich, Nickolai

Statement dc:rights

• Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)
• Copyright retained by author(s)

Licence dc:rights.uri

• https://creativecommons.org/licenses/by-nc-nd/4.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/157189

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/157189