Commit 4759a1ab authored by Benoit Viguier's avatar Benoit Viguier
Browse files

work on text

parent 4f5eb8bc
......@@ -11,12 +11,13 @@ application and has been optimized for source code compactness.
It maintains some degree of readability in order to be
easily auditable.
This library makes use of Curve25519\cite{Ber06}, an elliptic
curve defined over the field \Zfield.
It defines the function \texttt{crypto\_scalarmult} which
takes as input a scalar $n$ and the $x$ coordinate of a
point $P$ and returns the $x$ coordinate of the
point $[n]P$.
This library makes use of Curve25519\cite{Ber06}, a function over a \F{p}-restricted
x-coordinate scalar multiplication on $E(\F{p^2})$, where $p$ is the prime number \p
and E is the elliptic curve $y^2 = x^3 + 486662 x^2 + x$.
% It defines the function \texttt{crypto\_scalarmult} which
% takes as input a scalar $n$ and the $x$ coordinate of a
% point $P$ and returns the $x$ coordinate of the
% point $[n]P$.
Coq is a formal system that allows us to machine-check our proofs. The Compcert\cite{Leroy-backend}
compiler and the Verifiable Software Toolchain (VST)\cite{2012-Appel} are build
......
......@@ -273,7 +273,7 @@ As Post-condition we have:
\todo[inline]{theorem between CSM and Timmy representation here. Eg.}
\begin{lstlisting}[language=CoqD]
\begin{lstlisting}[language=Coq]
Theorem CSM_eq :
forall (n:list Z) (p:list Z),
Zlength n = 16 ->
......
\section{Mathematical Model}
\todo[inline]{Timmy needs to write here}
We extend the work of Evmorfia-Iro Bartzia and Pierre-Yves Strub \cite{DBLP:conf/itp/BartziaS14} to support Montgomery curves.
\subsection{Formalization of Elliptic Curves}
In this section, we consider elliptic curves over a field \K. We assume that the characteristic of \K is neither 2 or 3.
Definition 1. let \K\ be a field. Using an appropriate choice of coordinates, an elliptic curve \E\ is a plane cubic albreaic curve $\E(x,y)$ defined by an equation of the form:
$$\E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$$
where the $a_i$'s are in \K\ and the curve has no singular point (\ie no cusps or self-intersections). The set of points, written $\E(\K)$, is formed by the solutions $(x,y)$ of \E\ augmented by a distinguished point \Oinf\ (called point at infinity):
$$\E(\K) = \{(x,y) \in \K \times \K | \E(x,y)\} \cup \{\Oinf\}$$
In our case, this equation $\E(x,y)$ can be reduced into its Weierstrass form:
$$y^2 = x^3 + ax + b$$
Moreover, such curve does not present any singularity if $\Delta(a,b) = 4a^3 + 27b^2$ is not equal to $0$.
In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which represent the points on a specific curve. It is parametrized by a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 -- and \texttt{E : ecuType} -- a record that packs the curve parameters $a$ and $b$ along with the prof that $\Delta(a,b) \neq 0$.
\begin{lstlisting}[language=Coq]
Record ecuType :=
{ A : K; B : K; _ : 4 * A^3 + 27 * B^2 != 0}.
Inductive point := EC_Inf | EC_In of K * K.
Notation "(| x , y |)" := (EC_In x y).
Definition oncurve (p: point) :=
if p is (| x, y |)
then y^2 == x^3 + A * x + B
else true.
Inductive ec : Type := EC p of oncurve p.
\end{lstlisting}
......@@ -9,54 +9,54 @@ As described in Section \ref{sec:impl}, numbers in \TNaCle{gf} are represented
in base $2^{16}$ and we can use a direct mapping to represent that array as a list
integers in Coq. However in order to show the correctness of the basic operations,
we need to convert this number as a full integer. For this reason we define
\coqDe{ZofList : Z -> list Z -> Z}:
\begin{coqD}
\Coqe{ZofList : Z -> list Z -> Z}:
\begin{Coq}
Fixpoint ZofList {n:Z} (a:list Z) : Z :=
match a with
| [] => 0
| h :: q => h + (pow 2 n) * ZofList q
end.
Notation "Z16.lst A" := (ZofList 16 A).
\end{coqD}
\end{Coq}
It converts any list of integer from a base $2^n$ to an single integer. In our
case we define a notation where $n$ is $16$.
The following Coq notation is defined to convert any integer to its representant
in \Zfield.
\begin{coqD}
\begin{Coq}
Notation "A :GF" := (A mod (2^255-19)).
\end{coqD}
\end{Coq}
Using these two definitions, we proved lemmas such as the correctness of the
multiplication \coqDe{M}:
\begin{coqD}
multiplication \Coqe{M}:
\begin{Coq}
Lemma mult_GF_Zlength :
forall (a:list Z) (b:list Z),
Zlength a = 16 ->
Zlength b = 16 ->
(Z16.lst (M a b)) :GF =
(Z16.lst a * Z16.lst b) :GF.
\end{coqD}
\end{Coq}
For all list of integers \texttt{a} and \texttt{b} of length 16 representing
$A$ and $B$ in \Zfield, the number represented in \Zfield by the list \coqDe{(M a b)}
$A$ and $B$ in \Zfield, the number represented in \Zfield by the list \Coqe{(M a b)}
is equal to $A \times B \bmod 2^{255}-19$.
In a similar fashion we can define a Coq version of the inversion mimicking
the behavior of \TNaCle{inv25519} over \coqDe{list Z}. \coqDe{step_pow} contains
the behavior of \TNaCle{inv25519} over \Coqe{list Z}. \Coqe{step_pow} contains
the body of the for loop.
\begin{coqD}
\begin{Coq}
Definition step_pow (a:Z) (c g:list Z) : list Z :=
let c := Sq c in
if a <>? 1 && a <>? 3
then M c g
else c.
\end{coqD}
\end{Coq}
\coqDe{pow_fn_rev} is responsible of the iteration of the loop by making
\Coqe{pow_fn_rev} is responsible of the iteration of the loop by making
recursive calls.
\begin{coqD}
\begin{Coq}
Function pow_fn_rev (a:Z) (b:Z) (c g: list Z)
{measure Z.to_nat a} : (list Z) :=
if a <=? 0
......@@ -64,17 +64,17 @@ Function pow_fn_rev (a:Z) (b:Z) (c g: list Z)
else
let prev := pow_fn_rev (a - 1) b c g in
step_pow (b - 1 - a) prev g.
\end{coqD}
\end{Coq}
% This \coqDe{Function} requires a proof of termination. It is done by proving the
% Well-foundness of the decreasing argument: \coqDe{measure Z.to_nat a}.
% This \Coqe{Function} requires a proof of termination. It is done by proving the
% Well-foundness of the decreasing argument: \Coqe{measure Z.to_nat a}.
Calling \coqDe{pow_fn_rev} 254 times allows us to reproduce the same behavior as
Calling \Coqe{pow_fn_rev} 254 times allows us to reproduce the same behavior as
the Clight definition.
\begin{coqD}
\begin{Coq}
Definition Inv25519 (x:list Z) : list Z :=
pow_fn_rev 254 254 x x.
\end{coqD}
\end{Coq}
\subsection{Inversions and Reflections}
......@@ -91,7 +91,7 @@ correctness of the result we can use multiple strategy such as:
We choose the second method. The only drawback is that it requires to apply the
unrolling and exponentiation lemmas 255 times. This can be automated in Coq with
tacticals such as \coqDe{repeat}, but it generates a big proof object which
tacticals such as \Coqe{repeat}, but it generates a big proof object which
will take a long time to verify.
\subsubsection{Speeding up with Reflections}
......@@ -102,48 +102,48 @@ times the lemmas needs to be applied.
The idea is to \textit{reflect} the goal into a decidable environment.
In our case, we show that for a property $P$, we can define a decidable
boolean property $P_{bool}$ such that if $P_{bool}$ is \coqDe{true} then $P$ holds.
boolean property $P_{bool}$ such that if $P_{bool}$ is \Coqe{true} then $P$ holds.
$$P_{bool} = true \implies P$$
With VST we proved that \TNaCle{inv25519} in \texttt{Clight} is equivalent to its Coq
functional definition \coqDe{Inv25519}. We also proved that \coqDe{Inv25519}
over \coqDe{list Z} is equivalent to applying
\coqDe{Inv25519_Z} over \coqDe{Z}
functional definition \Coqe{Inv25519}. We also proved that \Coqe{Inv25519}
over \Coqe{list Z} is equivalent to applying
\Coqe{Inv25519_Z} over \Coqe{Z}
% With VST we proved that \TNaCle{inv25519} in \texttt{Clight} is equivalent to its Coq
% functional definition \coqDe{Inv25519}. We also proved that \coqDe{pow_fn_rev}
% over \coqDe{list Z} is equivalent to applying
% \coqDe{pow_fn_rev_Z} over \coqDe{Z}
% functional definition \Coqe{Inv25519}. We also proved that \Coqe{pow_fn_rev}
% over \Coqe{list Z} is equivalent to applying
% \Coqe{pow_fn_rev_Z} over \Coqe{Z}
\begin{coqD}
\begin{Coq}
Lemma Inv25519_Z_GF :
forall (g:list Z),
length g = 16 ->
(Z16.lst (Inv25519 g)) :GF =
(Inv25519_Z (Z16.lst g)) :GF.
\end{coqD}
\end{Coq}
% \begin{coqD}
% \begin{Coq}
% Lemma pow_fn_rev_Z_GF :
% forall (a:Z) (b:Z) (c:list Z) (g:list Z),
% Zlength c = 16 ->
% Zlength g = 16 ->
% (Z16.lst (pow_fn_rev a b c g)) :GF =
% (pow_fn_rev_Z a b (Z16.lst c) (Z16.lst g)) :GF .
% \end{coqD}
% \end{Coq}
where \coqDe{Inv25519_Z} reproduces the same pattern as \coqDe{Inv25519}.
where \Coqe{Inv25519_Z} reproduces the same pattern as \Coqe{Inv25519}.
\begin{coqD}
\begin{Coq}
Definition Inv25519_Z (x:Z) : Z :=
pow_fn_rev_Z 254 254 x x.
\end{coqD}
\end{Coq}
\coqDe{pow_fn_rev_Z} mimicks \coqDe{pow_fn_rev} over \coqDe{Z} instead of
\coqDe{list Z}. The structure is the same:
the application \coqDe{step_pow_Z} and the loop itself \coqDe{pow_fn_rev_Z}
\Coqe{pow_fn_rev_Z} mimicks \Coqe{pow_fn_rev} over \Coqe{Z} instead of
\Coqe{list Z}. The structure is the same:
the application \Coqe{step_pow_Z} and the loop itself \Coqe{pow_fn_rev_Z}
\begin{coqD}
\begin{Coq}
Definition step_pow_Z (a:Z) (c:Z) (g:Z) : Z :=
let c := c * c in
if a <>? 1 && a <>? 3
......@@ -157,25 +157,25 @@ Function pow_fn_rev_Z (a:Z) (b:Z) (c:Z) (g: Z)
else
let prev := pow_fn_rev_Z (a - 1) b c g in
step_pow_Z (b - 1 - a) prev g.
\end{coqD}
\end{Coq}
%
% In line with the definition of \coqDe{Inv25519}, we define the inversion modulo
% $2^{255}-19$ as an instance of \coqDe{pow_fn_rev_Z} where \coqDe{a} and \coqDe{b} are 254.
% In line with the definition of \Coqe{Inv25519}, we define the inversion modulo
% $2^{255}-19$ as an instance of \Coqe{pow_fn_rev_Z} where \Coqe{a} and \Coqe{b} are 254.
\subsubsection{A Simple Domain Specific Language}
To prove that the \coqDe{Inv25519_Z} is computing $x^{2^{255}-21}$,
To prove that the \Coqe{Inv25519_Z} is computing $x^{2^{255}-21}$,
we define a Domain Specific Language:
\begin{coqD}
\begin{Coq}
Inductive expr_inv :=
| R_inv : expr_inv
| M_inv : expr_inv -> expr_inv -> expr_inv
| S_inv : expr_inv -> expr_inv
| P_inv : expr_inv -> positive -> expr_inv.
\end{coqD}
\end{Coq}
An expression can be either a term, a multiplication, a squaring or a power.
This is denoted as follow:
\begin{coqD}
\begin{Coq}
Fixpoint e_inv_denote (m:expr_inv) : Z :=
match m with
| R_inv =>
......@@ -187,36 +187,36 @@ Fixpoint e_inv_denote (m:expr_inv) : Z :=
| P_inv x p =>
pow (e_inv_denote x) (Z.pos p)
end.
\end{coqD}
\end{Coq}
We defined \coqDe{step_inv} and \coqDe{pow_inv} to mirror the behavior of
\coqDe{step_pow_Z} and respectively \coqDe{pow_fn_rev_Z} over our new domain.
We defined \Coqe{step_inv} and \Coqe{pow_inv} to mirror the behavior of
\Coqe{step_pow_Z} and respectively \Coqe{pow_fn_rev_Z} over our new domain.
\begin{coqD}
\begin{Coq}
Lemma step_inv_step_pow_eq :
forall (a:Z) (c:expr_inv) (g:expr_inv),
e_inv_denote (step_inv a c g) =
step_pow_Z a (e_inv_denote c) (e_inv_denote g).
\end{coqD}
\begin{coqD}
\end{Coq}
\begin{Coq}
Lemma pow_inv_pow_fn_rev_eq :
forall (a:Z) (b:Z) (c:expr_inv) (g:expr_inv),
e_inv_denote (pow_inv a b c g) =
pow_fn_rev_Z a b (e_inv_denote c) (e_inv_denote g).
\end{coqD}
\end{Coq}
We also define what is a formula in our language: a simple equality.
\begin{coqD}
\begin{Coq}
Inductive formula_inv :=
| Eq_inv : expr_inv -> expr_inv -> formula_inv.
\end{coqD}
\end{Coq}
This is denoted as follow:
\begin{coqD}
\begin{Coq}
Definition f_inv_denote (t : formula_inv) : Prop :=
match t with
| Eq_inv x y => e_inv_denote x = e_inv_denote y
end.
\end{coqD}
\end{Coq}
With such Domain Specific Language we have the equivalence between:
\begin{lstlisting}[backgroundcolor=\color{white}]
f_inv_denote
......@@ -227,11 +227,11 @@ f_inv_denote
\subsubsection{Deciding formulas}
In order to prove formulas in \coqDe{formula_inv},
In order to prove formulas in \Coqe{formula_inv},
we define a decidable procedure.
We first compute the power of each side of the formula and then check their
equality.
\begin{coqD}
\begin{Coq}
Fixpoint pow_expr_inv (t:expr_inv) : Z :=
match t with
| R_inv => 1
......@@ -250,37 +250,37 @@ Definition decide_f_inv (f:formula_inv) : bool :=
match f with
| Eq_inv x y => decide_e_inv x y
end.
\end{coqD}
We proved that our procedure is correct: for all formulas in \coqDe{formula_inv}, if
\coqDe{decide_f_inv} returns \coqDe{true}, then the denoted equality is correct.
\begin{coqD}
\end{Coq}
We proved that our procedure is correct: for all formulas in \Coqe{formula_inv}, if
\Coqe{decide_f_inv} returns \Coqe{true}, then the denoted equality is correct.
\begin{Coq}
Lemma decide_formula_inv_impl :
forall (f:formula_inv),
decide_f_inv f = true ->
f_inv_denote f.
\end{coqD}
\end{Coq}
By reification to our Domain Specific Language and then by applying
\texttt{decide\_formula\_inv\_impl} and computing \texttt{decide\_f\_inv},
we proved that \coqDe{Inv25519} is indeed computing an inverse in
we proved that \Coqe{Inv25519} is indeed computing an inverse in
modulo $2^{255}-19$.
\begin{coqD}
\begin{Coq}
Theorem Inv25519_Z_correct :
forall (x:Z),
Inv25519_Z x = pow x (2^255-21).
\end{coqD}
\end{Coq}
From \coqDe{Inv25519_Z_correct} and \coqDe{Inv25519_Z_GF}, we conclude the
From \Coqe{Inv25519_Z_correct} and \Coqe{Inv25519_Z_GF}, we conclude the
functionnal correctness of the inversion over \Zfield.
\begin{coqD}
\begin{Coq}
Corollary Inv25519_Zpow_GF :
forall (g:list Z),
length g = 16 ->
Z16.lst (Inv25519 g) :GF =
(pow (Z16.lst g) (2^255-21)) :GF.
\end{coqD}
\end{Coq}
\subsubsection{Packing and other applications}
......@@ -307,10 +307,10 @@ This loop separation allows simpler proofs. The first loop is seen as the substr
We then proved than with the iteration of the second loop, the number represented in \Zfield stays the same.
This lead to the proof that \TNaCle{pack25519} is effectively reducing mod $2^{255}-19$ and returning a number in base $2^8$.
\begin{coqD}
\begin{Coq}
Lemma Pack25519_mod_25519 :
forall (l:list Z),
Zlength l = 16 ->
Forall (fun x => -2^62 < x < 2^62) l ->
ZofList 8 (Pack25519 l) = (Z16.lst l) mod (2^255-19).
\end{coqD}
\end{Coq}
......@@ -113,7 +113,7 @@ It is to be noted that the \texttt{clightgen} tool has not been formally verifie
While the final state of a For loops can be computed by a simple recursive function,
we must define invariants that are true for each step of the iteration.
\begin{coqD}
\begin{Coq}
Variable T : Type.
Variable g : nat -> T -> T.
......@@ -135,7 +135,7 @@ Definition rec_fn_rev (n:nat) (s:T) :=
Lemma Tail_Head_equiv :
forall (n:nat) (s:T),
rec_fn n s = rec_fn_rev n s.
\end{coqD}
\end{Coq}
In order to prove the for loops, we must define invariants.
......
......@@ -143,7 +143,8 @@ VeriSmall: Verified Smallfoot Shape Analysis, by Andrew W. Appel. In CPP 2011: F
@misc{coq-faq,
title = {{The Coq Proof Assistant} -- {Frequently Asked Questions}},
note = {\url{https://coq.inria.fr/faq}}
author = {},
note = {\url{https://coq.inria.fr/faq}},
}
......@@ -1103,3 +1104,16 @@ VeriSmall: Verified Smallfoot Shape Analysis, by Andrew W. Appel. In CPP 2011: F
year = {2016},
note = {\url{http://csrc.nist.gov/publications/drafts/nistir-8105/nistir_8105_draft.pdf}}
}
@inproceedings{DBLP:conf/itp/BartziaS14,
author = {Evmorfia-Iro Bartzia and Pierre-Yves Strub},
title = {A Formal Library for Elliptic Curves in the Coq Proof Assistant},
booktitle = {Interactive Theorem Proving},
editor = {Gerwin Klein and Ruben Gamboa},
publisher = SV,
series = LNCS,
volume = {8558},
year = {2014},
pages = {77-92},
note = {\url{https://hal.inria.fr/hal-01102288}}
}
......@@ -40,7 +40,7 @@
%make title bold and 14 pt font (Latex default is non-bold, 16 pt)
\title{\Large \bf A Coq proof of Tweetnacl's Curve25519 correctness.%
\thanks{
Date: somewhen in 2018.}
Date: somewhen in 2019.}
}
%for single author (just remove % characters)
......
......@@ -22,140 +22,144 @@
\vrule height0.75em width0.5em depth0.25em\fi}
\DeclareMathOperator*{\argmin}{arg\,min}
\DeclareMathOperator*{\Vol}{Vol}
\DeclareMathOperator*{\Supp}{Supp}
\newcommand{\cR}{\ensuremath{\mathcal R}}
\newcommand{\cS}{\ensuremath{\mathcal S}}
\newcommand{\CVPDf}{\ensuremath{\algo{CVP}_{\tilde{D}_4}}}
\newcommand{\CVPDfZf}{\ensuremath{\algo{CVP}_{D_4/\ZZ^4}}}
\newcommand{\LDEncode}{\algo{Encode}}
\newcommand{\LDDecode}{\algo{Decode}}
% \DeclareMathOperator*{\argmin}{arg\,min}
% \DeclareMathOperator*{\Vol}{Vol}
% \DeclareMathOperator*{\Supp}{Supp}
% \newcommand{\cR}{\ensuremath{\mathcal R}}
% \newcommand{\cS}{\ensuremath{\mathcal S}}
%
% \newcommand{\CVPDf}{\ensuremath{\algo{CVP}_{\tilde{D}_4}}}
% \newcommand{\CVPDfZf}{\ensuremath{\algo{CVP}_{D_4/\ZZ^4}}}
% \newcommand{\LDEncode}{\algo{Encode}}
% \newcommand{\LDDecode}{\algo{Decode}}
\usepackage{soul}\let\strikethrough\st\let\st\undefined
\newcommand{\T}{L}
% \newcommand{\T}{L}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\Z}{\ensuremath{\mathbb{Z}}}
\newcommand{\K}{\ensuremath{\mathbb{K}}}
\newcommand{\ZZ}{\ensuremath{\mathbb{Z}}}
\newcommand{\corr}{\,\hat{=}\,}
\newcommand{\E}{\ensuremath{\mathcal{E}}}
\newcommand{\Oinf}{\ensuremath{\mathcal{O}}}
\newcommand{\F}[1]{\ensuremath{\mathbb{F}_{#1}}}
\newcommand{\RR}{\ensuremath{\mathbb{R}}}
% \newcommand{\RR}{\ensuremath{\mathbb{R}}}
\newcommand{\N}{\ensuremath{\mathbb{N}}}
\newcommand{\mbf}{\ensuremath{\mathbf}}
\newcommand{\rando}{\ensuremath{\xleftarrow{\$}}}
\newcommand{\la}{\ensuremath{\leftarrow}}
\newcommand{\MD}{\ensuremath{\mathcal{D}}\xspace}
\newcommand{\MS}{\ensuremath{\mathcal{D}}\xspace}
\newcommand{\MA}{\ensuremath{\mathcal{A}}\xspace}
\newcommand{\MB}{\ensuremath{\mathcal{B}}\xspace}
\newcommand{\MP}{\ensuremath{\mathcal{P}}\xspace}
\newcommand{\tA}{\ensuremath{t_{\mathcal{A}}}}
\newcommand{\eA}{\ensuremath{\varepsilon_{\mathcal{A}}}}
\newcommand{\tS}{\ensuremath{t_{\mathcal{D}}}}
\newcommand{\eS}{\ensuremath{\varepsilon_{\mathcal{D}}}}
\newcommand{\vX}{\mathcal X}
\newcommand{\vY}{\mathcal Y}
\newcommand{\MR}{\ensuremath{\mathcal{R}}\xspace}
\newcommand{\tR}{\ensuremath{t_{\mathcal{R}}}}
\newcommand{\eR}{\ensuremath{\varepsilon_{\mathcal{R}}}}
\newcommand{\tD}{\ensuremath{t_{\mathcal{D}}}}
\newcommand{\eD}{\ensuremath{\varepsilon_{\mathcal{D}}}}
\newcommand{\sis}{\textsf{SIS}\xspace}
\newcommand{\isis}{\textsf{ISIS}\xspace}
\newcommand{\lwe}{\textsf{LWE}\xspace}
\newcommand{\dlwe}{\textsf{LWE}\xspace}
\newcommand{\rdlwe}{\textsf{R-LWE}\xspace}
\newcommand{\ee}{\ensuremath{\varepsilon}}
\newcommand{\sS}{\ensuremath{\sigma}}
\newcommand{\sE}{\ensuremath{\sigma}}
\newcommand{\DS}{\ensuremath{D_{\sS}}}
\newcommand{\DE}{\ensuremath{D_{\sE}}}
%\newcommand{\Dy}{\ensuremath{D_y}}
\newcommand{\Dy}{\ensuremath{[-B, B]}}
\newcommand{\Dysc}{\ensuremath{D_{y,\mat{Sc}}}}
\newcommand{\Dz}{\ensuremath{D_z}}
\newcommand{\bit}{\ensuremath{\{0,1\}}}
\newcommand{\eqdef}{\stackrel{\mathrm{def}}=}
\newcommand{\rand}{\getsr}
\newcommand{\rounddq}[1]{\ensuremath{\lfloor #1 \rceil_{d,q}}}
\newcommand{\roundd}[1]{\ensuremath{\lfloor #1 \rceil_d}}
\newcommand{\norm}[1]{\ensuremath{||#1||}}
\newcommand{\KeyGen}{\keygen}
\newcommand{\Sign}{\sign}
\newcommand{\Verify}{\verify}
\newcommand{\keygen}{\ensuremath{\mathsf{KeyGen}}}
\newcommand{\sign}{\ensuremath{\mathsf{Sign}}}
\newcommand{\verify}{\ensuremath{\mathsf{Verify}}}
\newcommand{\start}{\underline{\ensuremath{\mathsf{Start}}}\xspace}
\newcommand{\randO}{\ensuremath{\underline{\mathsf{Rand}}^{O_c}}\xspace}
\newcommand{\signO}{\ensuremath{\underline{\mathsf{Sign}}^{O_c}}\xspace}
\newcommand{\finishO}{\ensuremath{\underline{\mathsf{Finish}}^{O_c}}}
\newcommand{\instance}{\underline{\ensuremath{\mathsf{Instance}}}}
\newcommand{\Sample}{\ensuremath{\mathsf{Sample}}}
\newcommand{\keygenQ}{\ensuremath{\mathsf{KeyGen}}}
\newcommand{\signQ}{\ensuremath{\mathsf{Sign}}}
\newcommand{\verifyQ}{\ensuremath{\mathsf{Verify}}}
\newcommand{\CHgen}{\ensuremath{\mathsf{ChGen}}}
\newcommand{\inputtext}{\textsf{INPUT:}\;}
\newcommand{\outputtext}{\textsf{OUTPUT:}\;}
\newcommand{\iftext}{\mathbf{if\;}}
\newcommand{\elsetext}{\mathbf{else\;}}
\newcommand{\then}{\mathbf{then\;}}
\newcommand{\return}{\mathbf{return\;}}
\newcommand{\mat}[1]{\mathbf{#1}}
\renewcommand{\vec}[1]{\mathbf{#1}}
\newcommand{\modq}{\ensuremath{\; (\bmod \; q)}}
% \newcommand{\rando}{\ensuremath{\xleftarrow{\$}}}
% \newcommand{\la}{\ensuremath{\leftarrow}}
% \newcommand{\MD}{\ensuremath{\mathcal{D}}\xspace}
% \newcommand{\MS}{\ensuremath{\mathcal{D}}\xspace}
% \newcommand{\MA}{\ensuremath{\mathcal{A}}\xspace}
% \newcommand{\MB}{\ensuremath{\mathcal{B}}\xspace}
% \newcommand{\MP}{\ensuremath{\mathcal{P}}\xspace}
% \newcommand{\tA}{\ensuremath{t_{\mathcal{A}}}}
% \newcommand{\eA}{\ensuremath{\varepsilon_{\mathcal{A}}}}
% \newcommand{\tS}{\ensuremath{t_{\mathcal{D}}}}
% \newcommand{\eS}{\ensuremath{\varepsilon_{\mathcal{D}}}}
% \newcommand{\vX}{\mathcal X}
% \newcommand{\vY}{\mathcal Y}
% \newcommand{\MR}{\ensuremath{\mathcal{R}}\xspace}
% \newcommand{\tR}{\ensuremath{t_{\mathcal{R}}}}
% \newcommand{\eR}{\ensuremath{\varepsilon_{\mathcal{R}}}}
%
% \newcommand{\tD}{\ensuremath{t_{\mathcal{D}}}}
% \newcommand{\eD}{\ensuremath{\varepsilon_{\mathcal{D}}}}
% \newcommand{\sis}{\textsf{SIS}\xspace}
% \newcommand{\isis}{\textsf{ISIS}\xspace}
% \newcommand{\lwe}{\textsf{LWE}\xspace}
% \newcommand{\dlwe}{\textsf{LWE}\xspace}
% \newcommand{\rdlwe}{\textsf{R-LWE}\xspace}
%
% \newcommand{\ee}{\ensuremath{\varepsilon}}
%
% \newcommand{\sS}{\ensuremath{\sigma}}
% \newcommand{\sE}{\ensuremath{\sigma}}
% \newcommand{\DS}{\ensuremath{D_{\sS}}}
% \newcommand{\DE}{\ensuremath{D_{\sE}}}
% %\newcommand{\Dy}{\ensuremath{D_y}}
% \newcommand{\Dy}{\ensuremath{[-B, B]}}
% \newcommand{\Dysc}{\ensuremath{D_{y,\mat{Sc}}}}
% \newcommand{\Dz}{\ensuremath{D_z}}
% \newcommand{\bit}{\ensuremath{\{0,1\}}}
% \newcommand{\eqdef}{\stackrel{\mathrm{def}}=}
% \newcommand{\rand}{\getsr}
% \newcommand{\rounddq}[1]{\ensuremath{\lfloor #1 \rceil_{d,q}}}
% \newcommand{\roundd}[1]{\ensuremath{\lfloor #1 \rceil_d}}
% \newcommand{\norm}[1]{\ensuremath{||#1||}}
% \newcommand{\KeyGen}{\keygen}
% \newcommand{\Sign}{\sign}
% \newcommand{\Verify}{\verify}
% \newcommand{\keygen}{\ensuremath{\mathsf{KeyGen}}}
% \newcommand{\sign}{\ensuremath{\mathsf{Sign}}}
% \newcommand{\verify}{\ensuremath{\mathsf{Verify}}}
% \newcommand{\start}{\underline{\ensuremath{\mathsf{Start}}}\xspace}