Tom Arnold

Verified Post-Quantum Cryptography

Last updated: 2022/04/26

Abstract

Cryptosystems are being developed to resist attacks by quantum computers, and efforts are being made to formally verify software to guard against implementation flaws. In this project we will study post-quantum cryptography and formal verification by implementing the McEliece cryptosystem using refinement types.

Overview

The goal of this project is to learn more about cryptography and formal verification by studying, implementing, and analyzing variants of the McEliece cryptosystem in a language designed for formal verification. This project has two aspects. The first is post-quantum cryptography (PQC). PQC is the study of cryptosystems which are resistant to attacks by quantum computers; in other words, systems for which there are no known quantum algorithms that can effectively break them. An example of a cryptosystem which is not post-quantum is the widely used RSA system which is vulnerable to Shor's algorithm due to being based on integer factorization. The second aspect is formal verification, or using automation to verify program correctness. We use refinement types to eliminate entire classes of errors, and proofs written in code combined with the type system and an automated theorem prover to automatically verify programs after changes are made.

The McEliece cryptosystem dates back to the 70s when it was proposed by Robert McEliece. The McEliece system is based on coding theory and is not vulnerable to any known quantum attacks, and recently a variant of this system known as Classic McEliece has made it to round 3 of the NIST Post Quantum Cryptography standardization effort. Classic McEliece is a KEM (Key Encapsulation Method) based on the Niederreiter PKE (Public Key Encryption) which is a high-performance variant of the original McEliece cryptosystem. For the scope of this project we will focus on implementing and comparing the two PKE variants (McEliece and Niederreiter).

To verify our implementation we use the Haskell programming language with LiquidHaskell which is a functional language with refinement types. LiquidHaskell is an extension that focuses on code verification while the program writen are otherwise regular Haskell.

Plan of Work

Due-dates are based on the in-class presentation schedule. See weekly status for progress.

Milestone 1 - 2022/02/03

2 weekends

Milestone 2 - 2022/03/01

4 weekends

Milestone 3 - 2022/03/29

4 weekends

Deliverables

Presentations

Source Code

Resources

McEliece

Coding Theory

Cryptography

Formal Verification

Up