\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
\usepackage{amsfonts, amsmath, amssymb}
\usepackage[T1]{fontenc}

% this should be the last package used
\usepackage{pdfsetup}
\usepackage[shortcuts]{extdash}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{rm}


\begin{document}

\title{$(1-\delta)$-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform}
\author{Katharina Kreuzer}
\maketitle

\begin{abstract}
This article formalizes the specification and the algorithm of the cryptographic scheme CRYSTALS-KYBER with multiplication using the Number Theoretic Transform and verifies its $(1-\delta)$-correctness proof. 
CRYSTALS-KYBER is a key encapsulation mechanism in lattice-based post-quantum cryptography. 

This entry formalizes the key generation, encryption and decryption algorithms and shows that the algorithm decodes correctly under a highly probable assumption ($(1-\delta)$-correctness). Moreover, the Number Theoretic Transform (NTT) in the case of Kyber and the convolution theorem thereon is formalized.
\end{abstract}


\newpage
\tableofcontents

\newpage
\parindent 0pt\parskip 0.5ex

\section{Introduction}
CRYSTALS-KYBER is a cryptographic key encapsulation mechanism and one of the finalists of the third round in the NIST standardization project for post-quantum cryptography \cite{report3rdroundNIST}. That is, even with feasible quantum computers, Kyber is thought to be hard to crack. It was introduced in \cite{kyber} and its documentation can be found in \cite{KyberAS}.

Kyber is based on algebraic lattices and the module-LWE (Learning with Errors) Problem. 
Working over the quotient ring $R_q := \mathbb{Z}_q[x]/(x^{2^{n'}}+1)$ and vectors thereof, Kyber takes advantage of:
\begin{itemize}
\item properties both from polynomials and vectors
\item cyclic properties of $\mathbb{Z}_q$ (where $q$ is a prime) 
\item cyclic properties of the quotient ring
\item the splitting of $x^{2^{n'}}+1$ as a reducible, cyclotomic polynomial over $\mathbb{Z}_q$
\end{itemize}

The algorithm in Kyber is quite simple:
\begin{enumerate}
\item Let Alice have a public key $A \in R_q^{k\times k}$ and a secret $s\in R_q^k$. Then she generates a second public key $t = Av + e$ using an error vector $e\in R_q^k$.
\item Bob (who wants to send a message to Alice) takes Alice's public keys $A$ and $t$ as well as his secret key $r\in R_q^k$, the message $m\in\{0,1\}^{256}$ and two random errors $e_1\in R_q^k$ and $e_2\in R_q$. He then computes the values 
$u = A^Tr + e_1$ and $v = t^r + e_2 + \lceil q/2\rfloor m$ and sends them to Alice.
\item Knowing her secret $s$, Alice can recover the message $m$ from $u$ and $v$ By calculating $v-s^Tu$. Any eavesdropper however cannot distinguish the encoded message from random samples.
\end{enumerate}

The Number Theoretic Transform (NTT) is an analogue to the Discrete Fourier Transform in the setting of finite fields. 
As an extension to the AFP-entry "Number\_Theoretic\_Transform" \cite{NTT}, a special version of the NTT on $R_q$ is formalized. 
The main difference is that the NTT used in Kyber has a "twiddle" factor, allowing for an easier implementation but requirng a $2n$-th root of unity instead of a $n$-th root of unity. 
Moreover, the structure of $R_q$ is negacyclic, since $x^n\equiv -1\mod x^n+1$, instead of a cyclic convolution of the normal NTT. 
Additionally, the convolution theorem for the NTT in Kyber was formalized. It states $NTT (f\cdot g)  = NTT(f) \cdot NTT(g)$. 

In this work, we formalize the algorithms and verify the $(1-\delta)$-correctness of Kyber and refine the algorithms to compute fast multiplication using the NTT.

\vspace{1cm}
\input{session}

%\nocite{kyber}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

