Commit 6fb70d4c authored by Benoit Viguier's avatar Benoit Viguier
Browse files

low level finished (hopefully)

parent 5270d4e3
~\\
~\\
~\\
\subsection{Coq definitions}
\label{appendix:coq}
\subsubsection{Montgomery Ladder}
\label{subsubsec:coq-ladder}
~
Generic definition of the ladder:
\begin{lstlisting}[language=Coq]
......@@ -77,9 +80,123 @@ match t with
end.
\end{lstlisting}
\subsubsection{ZCrypto\_Scalarmult}
\label{subsubsec:ZCryptoScalarmult}
~
Instanciation of the Class \Coqe{Ops} with operations over \Z and modulo \p.
\begin{lstlisting}[language=Coq]
Definition modP (x:Z) : Z :=
Z.modulo x (Z.pow 2 255 - 19).
(* Encapsulate in a module. *)
Module Mid.
(* shift to the right by n bits *)
Definition getCarry (n:Z) (m:Z) : Z :=
Z.shiftr m n.
(* logical and with n ones *)
Definition getResidue (n:Z) (m:Z) : Z :=
Z.land n (Z.ones n).
Definition car25519 (n:Z) : Z :=
38 * getCarry 256 n + getResidue 256 n.
(* The carry operation is invariant under modulo *)
Lemma Zcar25519_correct:
forall (n:Z), n:GF = (Mid.car25519 n) :GF.
(* Define Mid.A, Mid.M ... *)
Definition A a b := Z.add a b.
Definition M a b :=
car25519 (car25519 (Z.mul a b)).
Definition Zub a b := Z.sub a b.
Definition Sq a := M a a.
Definition C_0 := 0.
Definition C_1 := 1.
Definition C_121665 := 121665.
Definition Sel25519 (b p q:Z) :=
if (Z.eqb b 0) then p else q.
Definition getbit (i:Z) (a: Z) :=
if (Z.ltb a 0) then
0
else if (Z.ltb i 0) then
Z.land a 1
else
Z.land (Z.shiftr a i) 1.
End Mid.
(* Packing is applying a modulo p *)
Definition ZPack25519 n :=
Z.modulo n (Z.pow 2 255 - 19).
(* And with 255 ones *)
(* unset last 3 bits *)
(* set bit 254 *)
Definition Zclamp (n : Z) : Z :=
(Z.lor
(Z.land n (Z.land (Z.ones 255) (-8)))
(Z.shiftl 64 (31 * 8))).
(* x^{p - 2} *)
Definition ZInv25519 (x:Z) : Z :=
Z.pow x (Z.pow 2 255 - 21).
(* instanciate over Z *)
Instance Z_Ops : (Ops Z Z modP) := {}.
Proof.
apply Mid.A. (* instanciate + *)
apply Mid.M. (* instanciate * *)
apply Mid.Zub. (* instanciate - *)
apply Mid.Sq. (* instanciate x^2 *)
apply Mid.C_0. (* instanciate Const 0 *)
apply Mid.C_1. (* instanciate Const 1 *)
apply Mid.C_121665. (* instanciate (a-2)/4 *)
apply Mid.Sel25519. (* instanciate CSWAP *)
apply Mid.getbit. (* instanciate ith bit *)
Defined.
(* instanciate montgomery_rec with Z_Ops *)
Definition ZCrypto_Scalarmult n p :=
let t := montgomery_rec
255 (* iterate 255 times *)
(Zclamp n) (* clamped n *)
1 (* x_2 *)
(ZUnpack25519 p) (* x_3 *)
0 (* z_2 *)
1 (* z_3 *)
0 (* dummy *)
0 (* dummy *)
(ZUnpack25519 p) (* x_1 *) in
let a := get_a t in
let c := get_c t in
ZPack25519 (Z.mul a (ZInv25519 c)).
\end{lstlisting}
\subsubsection{CSM}
\label{subsubsec:CryptoScalarmult}
~
\begin{lstlisting}[language=Coq]
Definition Crypto_Scalarmult n p :=
let t := montgomery_rec
255 (* iterate 255 times *)
(clamp n) (* clamped n *)
Low.C_1 (* x_2 *)
(Unpack25519 p) (* x_3 *)
Low.C_0 (* z_2 *)
Low.C_1 (* z_3 *)
Low.C_0 (* dummy *)
Low.C_0 (* dummy *)
(Unpack25519 p) (* x_1 *) in
let a := get_a t in
let c := get_c t in
Pack25519 (Low.M a (Inv25519 c)).
Definition CSM := Crypto_Scalarmult.
\end{lstlisting}
\subsubsection{Equivalence between For Loops}
\label{subsubsec:for}
~
\begin{lstlisting}[language=Coq]
Variable T: Type.
Variable g: nat -> T -> T.
......
\subsection{Content of the proof files}
\label{appendix:proof-files}
We provide below the location of the most important definitions and lemmas of our proofs.
\subsubsection{Definitions}
~
\begin{table}[h]
\begin{tabular}{ l | l | l }
Definition & File & Description \\
\hline
% \coqe{} & \texttt{} & \\
\end{tabular}
\end{table}
\subsubsection{Lemmas and Theorems}
~
\begin{table}[h]
\begin{tabular}{ l | l | l }
Definition & File & Description \\
\hline
\end{tabular}
\end{table}
% \subsection{Files}
%
% \begin{table}
% \begin{tabular}{ l | l }
% File & Content \\
% \hline
% \texttt{Gen/ABCDEF\_eq.v} & ... \\
% \texttt{Gen/ABCDEF.v} & ... \\
% \texttt{Gen/abstract\_fn\_rev\_abcdef.v} & ... \\
% \texttt{Gen/abstract\_fn\_rev\_eq.v} & ... \\
% \texttt{Gen/abstract\_fn\_rev.v} & ... \\
% \texttt{Gen/abstract\_rec\_rev\_abcdef.v} & ... \\
% \texttt{Gen/abstract\_rec\_rev\_eq.v} & ... \\
% \texttt{Gen/abstract\_rec\_rev.v} & ... \\
% \texttt{Gen/abstract\_rec.v} & ... \\
% \texttt{Gen/AMZubSqSel\_List.v} & ... \\
% \texttt{Gen/AMZubSqSel\_Prop.v} & ... \\
% \texttt{Gen/AMZubSqSel.v} & ... \\
% \texttt{Gen/Get\_abcdef.v} & ... \\
% \texttt{Gen/montgomery\_rec\_eq.v} & ... \\
% \texttt{Gen/montgomery\_rec.v} & ... \\
% \texttt{Gen/montgomery\_step\_gen.v} & ... \\
% \texttt{Gen/rec\_f\_extr.v} & ... \\
% \texttt{Gen/step\_gen.v} & ... \\
% \texttt{High/curve25519\_Fp2.v} & ... \\
% \texttt{High/curve25519\_Fp\_incl\_Fp2.v} & ... \\
% \texttt{High/curve25519\_Fp\_twist25519\_Fp\_eq.v} & ... \\
% \texttt{High/curve25519\_Fp.v} & ... \\
% \texttt{High/curve25519\_twist25519\_Fp\_incl\_Fp2.v} & ... \\
% \texttt{High/fermat.v} & ... \\
% \texttt{High/GRing\_tools.v} & ... \\
% \texttt{High/ladder.v} & ... \\
% \texttt{High/mcgroup.v} & ... \\
% \texttt{High/mc.v} & ... \\
% \texttt{High/montgomery.v} & ... \\
% \texttt{High/opt\_ladder\_extr.v} & ... \\
% \texttt{High/opt\_ladder.v} & ... \\
% \texttt{High/prime\_and\_legendre.v} & ... \\
% \texttt{High/prime\_cert.v} & ... \\
% \texttt{High/prime\_ssrprime.v} & ... \\
% \texttt{High/twist25519\_Fp\_incl\_Fp2.v} & ... \\
% \texttt{High/twist25519\_Fp.v} & ... \\
% \texttt{High/Zmodp2\_rules.v} & ... \\
% \texttt{High/Zmodp2.v} & ... \\
% \texttt{High/Zmodp\_Ring.v} & ... \\
% \texttt{High/Zmodp.v} & ... \\
% \texttt{Libs/Bound\_Decidable.v} & ... \\
% \texttt{Libs/Decidable.v} & ... \\
% \texttt{Libs/Export.v} & ... \\
% \texttt{Libs/Expr\_Decidable.v} & ... \\
% \texttt{Libs/Forall\_extended.v} & ... \\
% \texttt{Libs/Formula\_Decidable.v} & ... \\
% \texttt{Libs/Fun\_Decidable.v} & ... \\
% \texttt{Libs/HeadTailRec.v} & ... \\
% \texttt{Libs/LibTactics\_Rennes.v} & ... \\
% \texttt{Libs/LibTactics\_SF.v} & ... \\
% \texttt{Libs/LibTactics.v} & ... \\
% \texttt{Libs/List\_Decidable.v} & ... \\
% \texttt{Libs/List\_ext\_Decidable.v} & ... \\
% \texttt{Libs/List\_Ltac.v} & ... \\
% \texttt{Libs/Lists\_extended.v} & ... \\
% \texttt{Libs/Logic\_extended.v} & ... \\
% \texttt{Libs/Relations.v} & ... \\
% \texttt{Libs/Term\_Decidable.v} & ... \\
% \texttt{Libs/ZArith\_extended.v} & ... \\
% \texttt{ListsOp/Export.v} & ... \\
% \texttt{ListsOp/Forall\_ZofList.v} & ... \\
% \texttt{ListsOp/Forall\_ZopList.v} & ... \\
% \texttt{ListsOp/LogicalList.v} & ... \\
% \texttt{ListsOp/Zipp.v} & ... \\
% \texttt{ListsOp/ZofList.v} & ... \\
% \texttt{ListsOp/ZunopList.v} & ... \\
% \texttt{Low/AMZubSqSel\_Correct.v} & ... \\
% \texttt{Low/A.v} & ... \\
% \texttt{Low/BackCarry.v} & ... \\
% \texttt{Low/Binary\_select.v} & ... \\
% \texttt{Low/Car25519\_bounds.v} & ... \\
% \texttt{Low/Car25519.v} & ... \\
% \texttt{Low/Carry\_n.v} & ... \\
% \texttt{Low/Carry.v} & ... \\
% \texttt{Low/Constant.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult\_lemmas\_List\_List16.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult\_lemmas.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult\_lemmas\_Z\_List16.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult.v} & ... \\
% \texttt{Low/Crypto\_Scalarmult\_.v} & ... \\
% \texttt{Low/Export.v} & ... \\
% \texttt{Low/Get\_abcdef.v} & ... \\
% \texttt{Low/GetBit\_pack25519.v} & ... \\
% \texttt{Low/GetBit.v} & ... \\
% \texttt{Low/Inner\_M1.v} & ... \\
% \texttt{Low/Inv25519\_gen.v} & ... \\
% \texttt{Low/Inv25519.v} & ... \\
% \texttt{Low/List16.v} & ... \\
% \texttt{Low/M\_low\_level\_compute.v} & ... \\
% \texttt{Low/M.v} & ... \\
% \texttt{Low/Outer\_M1.v} & ... \\
% \texttt{Low/Pack25519.v} & ... \\
% \texttt{Low/Pack.v} & ... \\
% \texttt{Low/Prep\_n.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_aux.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_1b.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_1.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_2b.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_2.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose\_step.v} & ... \\
% \texttt{Low/Reduce\_by\_P\_compose.v} & ... \\
% \texttt{Low/Reduce\_by\_P.v} & ... \\
% \texttt{Low/ScalarMult\_gen\_small.v} & ... \\
% \texttt{Low/ScalarMult\_rev\_fn\_gen.v} & ... \\
% \texttt{Low/ScalarMult\_rev.v} & ... \\
% \texttt{Low/Sel25519.v} & ... \\
% \texttt{Low/S.v} & ... \\
% \texttt{Low/Unpack25519.v} & ... \\
% \texttt{Low/Z.v} & ... \\
% \texttt{Mid/AMZubSqSel.v} & ... \\
% \texttt{Mid/Car25519.v} & ... \\
% \texttt{Mid/Crypto\_Scalarmult\_Fp.v} & ... \\
% \texttt{Mid/Crypto\_Scalarmult\_Mod.v} & ... \\
% \texttt{Mid/Crypto\_Scalarmult.v} & ... \\
% \texttt{Mid/Export.v} & ... \\
% \texttt{Mid/GetBit\_bitn.v} & ... \\
% \texttt{Mid/GetBit.v} & ... \\
% \texttt{Mid/Instances.v} & ... \\
% \texttt{Mid/Inv25519.v} & ... \\
% \texttt{Mid/MinusList.v} & ... \\
% \texttt{Mid/M\_low\_level.v} & ... \\
% \texttt{Mid/Mod.v} & ... \\
% \texttt{Mid/M.v} & ... \\
% \texttt{Mid/Pack25519.v} & ... \\
% \texttt{Mid/Prep\_n.v} & ... \\
% \texttt{Mid/Reduce.v} & ... \\
% \texttt{Mid/ScalMult.v} & ... \\
% \texttt{Mid/SubList.v} & ... \\
% \texttt{Mid/SumList.v} & ... \\
% \texttt{Mid/Unpack25519.v} & ... \\
% \texttt{Mid/ZCarry.v} & ... \\
% \end{tabular}
% \end{table}
%
% \begin{table}
% \begin{tabular}{ l | l }
% File & Content \\
% \hline
% \texttt{c/tweetnaclVerifiableC.v} & \\
% \texttt{init/init\_tweetnacl.v} & \\
% \texttt{init/missing\_lemmae.v} & \\
% \texttt{proofs/split\_array\_lemmas.v} & \\
% \texttt{proofs/verif\_A.v} & \\
% \texttt{proofs/verif\_car25519\_compute.v} & \\
% \texttt{proofs/verif\_car25519.v} & \\
% \texttt{proofs/verif\_crypto\_scalarmult\_lemmas.v} & \\
% \texttt{proofs/verif\_crypto\_scalarmult.v} & \\
% \texttt{proofs/verif\_inv25519.v} & \\
% \texttt{proofs/verif\_M\_compute\_pre.v} & \\
% \texttt{proofs/verif\_M\_compute.v} & \\
% \texttt{proofs/verif\_M\_lemmas.v} & \\
% \texttt{proofs/verif\_M.v} & \\
% \texttt{proofs/verif\_pack25519\_lemmas.v} & \\
% \texttt{proofs/verif\_pack25519.v} & \\
% \texttt{proofs/verif\_sel25519.v} & \\
% \texttt{proofs/verif\_set25519.v} & \\
% \texttt{proofs/verif\_S.v} & \\
% \texttt{proofs/verif\_unpack25519.v} & \\
% \texttt{proofs/verif\_Z.v} & \\
% \texttt{spec/spec\_A.v} & \\
% \texttt{spec/spec\_car25519.v} & \\
% \texttt{spec/spec\_crypto\_scalarmult.v} & \\
% \texttt{spec/spec\_inv25519.v} & \\
% \texttt{spec/spec\_M.v} & \\
% \texttt{spec/spec\_pack25519.v} & \\
% \texttt{spec/spec\_sel25519.v} & \\
% \texttt{spec/spec\_set25519.v} & \\
% \texttt{spec/spec\_S.v} & \\
% \texttt{spec/spec\_unpack25519.v} & \\
% \texttt{spec/spec\_Z.v} & \\
% \end{tabular}
% \end{table}
......@@ -205,7 +205,7 @@ With those coordinates we prove the following lemmas for the addition of two poi
such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.
\end{dfn}
\begin{lemma}
\label{lemma-add}
\label{lemma:add}
Let $M_{a,b}(\K)$ be a Montgomery curve such that $a^2-4$ is not a square, and
let $X_1, Z_1, X_2, Z_2, X_3, Z_3 \in \K$, such that $(X_1,Z_1) \neq (0,0)$, $(X_2,Z_2) \neq (0,0)$, $X_4 \neq 0$ and $Z_4 \neq 0$.
Define
......@@ -250,7 +250,7 @@ then for any point $P_1$ and $P_2$ on $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_
With those coordinates we also prove a similar lemma for point doubling.
\begin{lemma}
\label{lemma-double}
\label{lemma:double}
Let $M_{a,b}(\K)$ be a Montgomery curve such that $a^2-4$ is not a square, and
let $X_1, Z_1, X_2, Z_2, X_3, Z_3 \in \K$, such that $(X_1,Z_1) \neq (0,0)$. Define
\begin{align*}
......@@ -274,7 +274,7 @@ we have $X_3/Z_3 = \chi(2P_1)$.
% (p \+ p)#x = inf_div x3 z3.
% \end{lstlisting}
With these two lemmas (\ref{lemma-add} and \ref{lemma-double}), we have the basic
With these two lemmas (\ref{lemma:add} and \ref{lemma:double}), we have the basic
tools to compute efficiently additions and point doubling on projective coordinates.
\subsubsection{Scalar Multiplication Algorithms}
......@@ -292,12 +292,12 @@ it provides slightly more computations and an extra variable, we can prevent suc
See \aref{alg:montgomery-ladder}.
\begin{lemma}
\label{lemma-montgomery-ladder}
\label{lemma:montgomery-ladder}
\aref{alg:montgomery-ladder} is correct, \ie it respects its output conditions given the input conditions.
\end{lemma}
In Curve25519 we are only interested in the $x$ coordinate of points, using
Lemmas \ref{lemma-add} and \ref{lemma-double}, and replacing the if statements
Lemmas \ref{lemma:add} and \ref{lemma:double}, and replacing the if statements
with conditional swapping we can define a ladder similar to the one used in TweetNaCl.
See \aref{alg:montgomery-double-add}
......@@ -340,14 +340,14 @@ See \aref{alg:montgomery-double-add}
\end{algorithm}
\begin{lemma}
\label{lemma-montgomery-double-add}
\label{lemma:montgomery-double-add}
\aref{alg:montgomery-double-add} is correct, \ie it respects its output
conditions given the input conditions.
\end{lemma}
%% here we have \chi and \chi_0 ...
We formalized this lemma (\ref{lemma-montgomery-double-add}):
We formalized this lemma (\ref{lemma:montgomery-double-add}):
\begin{lstlisting}[language=Coq]
Lemma opt_montgomery_x :
forall (n m : nat) (x : K),
......@@ -365,7 +365,7 @@ Also \Oinf\ is the neutral element over $M_{a,b}(\K)$, we have:
$$\forall P, P + \Oinf\ = P$$
thus we derive the following lemma.
% \begin{lemma}
% \label{lemma-montgomery-double-add}
% \label{lemma:montgomery-double-add}
% Algorithm \ref{montgomery-double-add} is correct even if $x=0$, \ie it respects its output conditions given the input conditions or $x=0$.
% \end{lemma}
\begin{lstlisting}[language=Coq]
......
This diff is collapsed.
......@@ -309,8 +309,8 @@ literate=
\def\coqe{\lstinline[language=Coq, basicstyle=\ttfamily\normalsize]}
\def\Coqe{\lstinline[language=Coq, basicstyle=\ttfamily\normalsize]}
% inline in table / displaymath...
\def\coqes{\lstinline[language=Coq, basicstyle=\scriptsize]}
\def\Coqes{\lstinline[language=Coq, basicstyle=\scriptsize]}
\def\coqes{\lstinline[language=Coq, basicstyle=\normalsize]}
\def\Coqes{\lstinline[language=Coq, basicstyle=\normalsize]}
......
......@@ -70,9 +70,10 @@ The Netherlands}
\bibliography{collection}}
\begin{appendix}
\input{tweetnacl.tex}
\input{code-tweetnacl.tex}
\input{coq.tex}
\input{proofs.tex}
\input{files.tex}
\end{appendix}
\end{document}
......@@ -134,9 +134,6 @@ Local Ltac solve_equiv_fabcdef i :=
[| assumption];
replace (254 - (254 - i)) with i ; [|omega];
subst; simpl;
(* rewrite /fa /fb /fc /fd /fe /ff; *)
(* rewrite /ScalarMult_gen_small.fa /ScalarMult_gen_small.fb /ScalarMult_gen_small.fc; *)
(* rewrite /ScalarMult_gen_small.fd /ScalarMult_gen_small.fe /ScalarMult_gen_small.ff; *)
reflexivity.
Lemma body_crypto_scalarmult: semax_body Vprog Gprog f_crypto_scalarmult_curve25519_tweet crypto_scalarmult_spec.
......@@ -441,7 +438,6 @@ replace (force_val
reflexivity.
omega.
}
(* apply Z.land_nonneg ; right ; omega. *)
freeze [0;1;4;5;6;7;8;9] L.
assert(Hgb:= getbit_0_or_1 i z).
......@@ -590,7 +586,6 @@ replace (force_val
unfold_nm_overlap_array_sep ; simpl.
thaw L.
(* clear Heqf0 H55 f0. *)
clears f0.
freeze [0;2;3;4;6;7;8;9] L.
......@@ -790,8 +785,7 @@ replace (force_val
remember (Low.A a1 c1) as e'.
remember (Low.Sel25519 (Low.getbit i z) a4 b2) as a'.
remember (Low.Sel25519 (Low.getbit i z) b2 a4) as b'.
(* Opaque c_121665. *)
(* this is sper slow with cancel and entailer, better do it manually *)
(* this is super slow with cancel and entailer, better do it manually *)
focus_SEP 8 9 2 3 0 1 4 6 5.
solve_bounds_by_values. (* this does nothing but if forces the 2^16 to be in Z and not in Z.pos ! *)
go_lowerx.
......@@ -828,7 +822,7 @@ replace (force_val
apply Z.eqb_neq; omega.
}
rewrite H254false.
(* this is sper slow with cancel and entailer, better do it manually *)
(* this is super slow with cancel and entailer, better do it manually *)
solve_bounds_by_values. (* this does nothing but if forces the 2^16 to be in Z and not in Z.pos ! *)
go_lowerx.
rewrite <- andp_assoc.
......@@ -855,7 +849,7 @@ replace (force_val
}
rewrite H254false.
(* this is sper slow with cancel and entailer, better do it manually *)
(* this is super slow with cancel and entailer, better do it manually *)
remember (montgomery_fn List_Z_Ops 255 254 z a b c d nil16 nil16 x) as m. (* prevent some computing... *)
go_lowerx.
rewrite <- andp_assoc.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment