Commit 6571f21c authored by Benoit Viguier's avatar Benoit Viguier
Browse files


parent 6a8234f6
FILES := $(wildcard *.tex) $(wildcard tikz/*.tex) $(wildcard *.sty)
TEX := $(wildcard *.tex)
FILES := $(TEX) $(wildcard tikz/*.tex) $(wildcard *.sty)
tweetverif.pdf: FORCE $(FILES) collection.bib
./ tweetverif.tex
......@@ -24,11 +26,6 @@ clean:
@rm */*.aux 2> /dev/null || true
aspell -t -c tweetverif.tex
aspell -t -c intro.tex
aspell -t -c preliminaries.tex
aspell -t -c lowlevel.tex
aspell -t -c highlevel.tex
aspell -t -c conclusion.tex
aspell -t -c tweetnacl.tex
for f in $(TEX) ; do \
aspell -t -c $$f; \
......@@ -144,15 +144,15 @@ Definition ZInv25519 (x:Z) : Z :=
(* instanciate over Z *)
Instance Z_Ops : (Ops Z Z modP) := {}.
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 *)
apply Mid.A. (* instantiate + *)
apply Mid.M. (* instantiate * *)
apply Mid.Zub. (* instantiate - *)
apply Mid.Sq. (* instantiate x^2 *)
apply Mid.C_0. (* instantiate Const 0 *)
apply Mid.C_1. (* instantiate Const 1 *)
apply Mid.C_121665. (* instantiate (a-2)/4 *)
apply Mid.Sel25519. (* instantiate CSWAP *)
apply Mid.getbit. (* instantiate ith bit *)
(* instanciate montgomery_rec with Z_Ops *)
......@@ -345,7 +345,7 @@ Lemma mult_GF_Zlength :
However for our purpose, simple functional correctness is not enough.
We also need to define the bounds under which the operation is correct,
allowing us to chain them, guaranting us the absence of overflow.
allowing us to chain them, guaranteeing us the absence of overflow.
......@@ -366,7 +366,7 @@ Lemma M_bound_Zlength :
\subsection{Inversions, Reflections and Packing}
We now turn our attention to the inversion in \Zfield and techniques to
increase the verifications speed of complex formulas.
increase the verification speed of complex formulas.
\subheading{Inversions in \Zfield.}
We define a Coq version of the inversion mimicking
......@@ -434,7 +434,7 @@ By using \lref{lemma:mult_correct}, we prove their equivalence in $\Zfield$.
The function \coqe{Inv25519} over list of integers computes the same
result at \coqe{Inv25519_Z} over intergers in \Zfield.
result at \coqe{Inv25519_Z} over integers in \Zfield.
This is formalized in Coq as follows:
......@@ -596,8 +596,8 @@ Theorem Inv25519_Z_correct :
Inv25519_Z x = pow x (2^255-21).
% From \Coqe{Inv25519_Z_GF} (\lref{lemma:Inv_equivalence}) and \Coqe{Inv25519_Z_correct} (Corrolary~\ref{lemma:inv_comput_inv}),
From \lref{lemma:Inv_equivalence} and Corrolary~\ref{lemma:inv_comput_inv},
% From \Coqe{Inv25519_Z_GF} (\lref{lemma:Inv_equivalence}) and \Coqe{Inv25519_Z_correct} (Corollary~\ref{lemma:inv_comput_inv}),
From \lref{lemma:Inv_equivalence} and Corollary~\ref{lemma:inv_comput_inv},
we conclude the functional correctness of the inversion over \Zfield.
......@@ -258,7 +258,7 @@ In order to compute the scalar multiplication,
X25519 uses the Montgomery ladder~\cite{Mon85}.
$x$-coordinates are represented as fractions, the computation of the actual
value is deffered to the end of the ladder with \TNaCle{inv25519}.
value is deferred to the end of the ladder with \TNaCle{inv25519}.
First extract and clamp the value of $n$. Then unpack the value of $p$.
As per RFC~7748~\cite{rfc7748}, set its most significant bit to 0.
......@@ -5,7 +5,7 @@
Our proofs requires the use of \emph{Coq.8.8.2} for the proofs and
\emph{Opam 2.0} to manage the dependencies. We are aware that there exists more
recent versions of Coq; VST; CompCert etc. however to avoid dealing with backward
breaking compatibilities we decided to freeze our dependencies.
breaking compatibility we decided to freeze our dependencies.
\subheading{Associated files}
The archive containing the proof is composed of two folders \textbf{\texttt{packages}}
......@@ -19,7 +19,7 @@ the reader will find the directories \textbf{\texttt{spec}} and \textbf{\texttt{
This folder makes sure that we are using the correct version of
Verifiable Software Toolchain (version 2.0) and CompCert (version 3.2).
Additionaly it pins the version of the elliptic curves library by Bartzia and Strub
Additionally it pins the version of the elliptic curves library by Bartzia and Strub
and allows us to use the theorem of quadratic reciprocity.
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