Commit 040187ba authored by benoit's avatar benoit
Browse files

rewrites, add proof description for the figures, smaller code font

parent e39299b4
......@@ -136,6 +136,14 @@ effort required to extend our work to other elliptic-curve software.
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.
C source files are represented by {\color{doc@lstfunctions}.C} while
{\color{doc@lstfunctions}.V} corresponds to Coq files.
\todo{Double Check (new)}
In a nutshell, we formalize X25519 into a Coq function \texttt{RFC},
and we write a specification in Separation logic with VST.
The first step of CompCert compilation (clightgen) is used to translates
the C source code into a DSL (CLight). By using VST,
we step through the translated instructions and verify that the program satisfies the specifications.
Additionally we formally define the scalar multiplication over elliptic curves and show that,
under the same preconditions as used in the specification, \texttt{RFC} computes the desired results
\begin{figure}[h]
\centering
......
......@@ -4,7 +4,7 @@
In this section we present our formalization of RFC~7748~\cite{rfc7748}.
\begin{informaltheorem}
The specification of X25519 in RFC~7748 is formalized by the function \Coqe{RFC} in Coq.
The specification of X25519 in RFC~7748 is formalized by the function \Coqe{RFC} in Coq.
\end{informaltheorem}
More specifically, we formalized X25519 with the following definition:
......@@ -15,13 +15,13 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
let t := montgomery_rec_swap
255 (* iterate 255 times *)
k (* clamped n *)
1 (* x_2 *)
u (* x_3 *)
0 (* z_2 *)
1 (* z_3 *)
1 (* x_2 *)
u (* x_3 *)
0 (* z_2 *)
1 (* z_3 *)
0 (* dummy *)
0 (* dummy *)
u (* x_1 *)
u (* x_1 *)
0 (* previous bit = 0 *) in
let a := get_a t in
let c := get_c t in
......@@ -38,48 +38,48 @@ Fixpoint montgomery_rec_swap (m : nat) (z : T')
(* b: x3 *)
(* c: z2 *)
(* d: z3 *)
(* e: temporary var *)
(* f: temporary var *)
(* e: temporary var *)
(* f: temporary var *)
(* x: x1 *)
(* swap: previous bit value *)
(* swap: previous bit value *)
(T * T * T * T * T * T) :=
match m with
| S n =>
let r := Getbit (Z.of_nat n) z in
(* k_t = (k >> t) & 1 *)
(* k_t = (k >> t) & 1 *)
let swap := Z.lxor swap r in
(* swap ^= k_t *)
(* swap ^= k_t *)
let (a, b) := (Sel25519 swap a b, Sel25519 swap b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 swap c d, Sel25519 swap d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
let e := a + c in (* A = x_2+ z_2 *)
let a := a - c in (* B = x_2- z_2 *)
let c := b + d in (* C = x_3+ z_3 *)
let b := b - d in (* D = x_3- z_3 *)
let d := e^2 in (* AA = A^2 *)
let f := a^2 in (* BB = B^2 *)
let a := c * a in (* CB = C * B *)
let c := b * e in (* DA = D * A *)
let e := a + c in (* x_3= (DA + CB)^2 *)
let a := a - c in (* z_3= x_1* (DA - CB)^2 *)
let b := a^2 in (* z_3= x_1* (DA - CB)^2 *)
let c := d - f in (* E = AA - BB *)
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
let e := a + c in (* A = x_2 + z_2 *)
let a := a - c in (* B = x_2 - z_2 *)
let c := b + d in (* C = x_3 + z_3 *)
let b := b - d in (* D = x_3 - z_3 *)
let d := e^2 in (* AA = A^2 *)
let f := a^2 in (* BB = B^2 *)
let a := c * a in (* CB = C * B *)
let c := b * e in (* DA = D * A *)
let e := a + c in (* x_3= (DA + CB)^2 *)
let a := a - c in (* z_3= x_1* (DA - CB)^2 *)
let b := a^2 in (* z_3= x_1* (DA - CB)^2 *)
let c := d - f in (* E = AA - BB *)
let a := c * C_121665 in
(* z_2 = E * (AA + a24 * E) *)
let a := a + d in (* z_2 = E * (AA + a24 * E) *)
let c := c * a in (* z_2 = E * (AA + a24 * E) *)
let a := d * f in (* x_2 = AA * BB *)
let d := b * x in (* z_3 = x_1* (DA - CB)^2 *)
let b := e^2 in (* x_3 = (DA + CB)^2 *)
(* z_2 = E * (AA + a24 * E) *)
let a := a + d in (* z_2 = E * (AA + a24 * E) *)
let c := c * a in (* z_2 = E * (AA + a24 * E) *)
let a := d * f in (* x_2 = AA * BB *)
let d := b * x in (* z_3 = x_1* (DA - CB)^2 *)
let b := e^2 in (* x_3 = (DA + CB)^2 *)
montgomery_rec_swap n z a b c d e f x r
(* swap = k_t *)
(* swap = k_t *)
| 0%nat =>
let (a, b) := (Sel25519 swap a b, Sel25519 swap b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
(* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 swap c d, Sel25519 swap d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
(* (z_2, z_3) = cswap(swap, z_2, z_3) *)
(a,b,c,d,e,f)
end.
\end{lstlisting}
......@@ -95,10 +95,10 @@ Later in our proof we use a simpler description of the ladder
and prove those ladder equivalent.
\emph{``To implement the X25519(k, u) [...] functions (where k is
the scalar and u is the u-coordinate), first decode k and u and then
perform the following procedure, which is taken from [curve25519] and
based on formulas from [montgomery]. All calculations are performed
in GF(p), i.e., they are performed modulo p.''}~\cite{rfc7748}
the scalar and u is the u-coordinate), first decode k and u and then
perform the following procedure, which is taken from [curve25519] and
based on formulas from [montgomery]. All calculations are performed
in GF(p), i.e., they are performed modulo p.''}~\cite{rfc7748}
Operations used in the Montgomery ladder of \coqe{RFC} are performed on
integers (See Appendix~\ref{subsubsec:RFC-Coq}).
......@@ -108,8 +108,8 @@ The reduction modulo $\p$ is deferred to the very end as part of the
We now turn our attention to the decoding and encoding of the byte arrays.
We define the little-endian projection to integers as follows.
\begin{dfn}
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list}~\Z \rightarrow \Z$,
a function given $n$ and a list $l$ returns its little endian decoding with radix $2^n$.
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list}~\Z \rightarrow \Z$,
a function given $n$ and a list $l$ returns its little endian decoding with radix $2^n$.
\end{dfn}
\begin{lstlisting}[language=Coq,aboveskip=0pt,belowskip=1pt]
Fixpoint ZofList {n:Z} (a:list Z) : Z :=
......@@ -120,10 +120,10 @@ Fixpoint ZofList {n:Z} (a:list Z) : Z :=
\end{lstlisting}
The encoding from integers to bytes is defined in a similar way:
\begin{dfn}
Let \Coqe{ListofZ32} : $\Z \rightarrow \Z \rightarrow \texttt{list}~\Z$, given
$n$ and $a$ returns $a$'s little-endian encoding as a list with radix $2^n$.
%XXX-Peter: Again I'm confused... why are there two \rightarrows?
%XXX-Benoit it is the functional view of arguments and partial functions. It is called Currying.
Let \Coqe{ListofZ32} : $\Z \rightarrow \Z \rightarrow \texttt{list}~\Z$, given
$n$ and $a$ returns $a$'s little-endian encoding as a list with radix $2^n$.
%XXX-Peter: Again I'm confused... why are there two \rightarrows?
%XXX-Benoit it is the functional view of arguments and partial functions. It is called Currying.
\end{dfn}
\begin{lstlisting}[language=Coq,aboveskip=0pt,belowskip=1pt]
Fixpoint ListofZn_fp {n:Z} (a:Z) (f:nat) : list Z :=
......
......@@ -5,8 +5,8 @@ In this section we prove the following theorem:
% In this section we outline the structure of our proofs of the following theorem:
\begin{informaltheorem}
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches
the specifications of RFC~7748~\cite{rfc7748} (\Coqe{RFC}).
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches
the specifications of RFC~7748~\cite{rfc7748} (\Coqe{RFC}).
\end{informaltheorem}
More formally:
......@@ -14,7 +14,7 @@ More formally:
Theorem body_crypto_scalarmult:
(* VST boiler plate. *)
semax_body
(* Clight translation of TweetNaCl. *)
(* Clight translation of TweetNaCl. *)
Vprog
(* Hoare triples for fct calls. *)
Gprog
......
......@@ -2,9 +2,9 @@
\label{subsec:with-VST}
\begin{sloppypar}
We now turn our focus to the formal specification of \TNaCle{crypto_scalarmult}.
We use our definition of X25519 from the RFC in the Hoare triple and prove
its correctness.
We now turn our focus to the formal specification of \TNaCle{crypto_scalarmult}.
We use our definition of X25519 from the RFC in the Hoare triple and prove
its correctness.
\end{sloppypar}
\subheading{Specifications.}
......@@ -53,37 +53,40 @@ SEP (sh [{ v_q }] <<(uch32)-- mVI (RFC n p);
In this specification we state preconditions like:
\begin{itemize}
\item[] \VSTe{PRE}: \VSTe{_p OF (tptr tuchar)}\\
The function \TNaCle{crypto_scalarmult} takes as input three pointers to
arrays of unsigned bytes (\VSTe{tptr tuchar}) \VSTe{_p}, \VSTe{_q} and \VSTe{_n}.
\item[] \VSTe{LOCAL}: \VSTe{temp _p v_p}\\
Each pointer represent an address \VSTe{v_p},
\VSTe{v_q} and \VSTe{v_n}.
\item[] \VSTe{SEP}: \VSTe{sh [{ v_p $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI p}\\
In the memory share \texttt{sh}, the address \VSTe{v_p} points
to a list of integer values \VSTe{mVI p}.
\item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) p}\\
In order to consider all the possible inputs, we assume each
element of the list \texttt{p} to be bounded by $0$ included and $2^8$
excluded.
\item[] \VSTe{PROP}: \VSTe{Zlength p = 32}\\
We also assume that the length of the list \texttt{p} is 32. This defines the
complete representation of \TNaCle{u8[32]}.
\item[] \VSTe{PRE}: \VSTe{_p OF (tptr tuchar)}\\
The function \TNaCle{crypto_scalarmult} takes as input three pointers to
arrays of unsigned bytes (\VSTe{tptr tuchar}) \VSTe{_p}, \VSTe{_q} and \VSTe{_n}.
\item[] \VSTe{LOCAL}: \VSTe{temp _p v_p}\\
Each pointer represent an address \VSTe{v_p},
\VSTe{v_q} and \VSTe{v_n}.
\item[] \VSTe{SEP}: \VSTe{sh [{ v_p $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI p}\\
In the memory share \texttt{sh}, the address \VSTe{v_p} points
to a list of integer values \VSTe{mVI p}.
\item[] \VSTe{Ews [{ c121665 $\!\!\}\!\!]\!$ <<(lg16)-- mVI64 c_121665}\\
In the global memory share \texttt{Ews}, the address \VSTe{c121665} points
to a list of 16 64-bit integer values corresponding to $a/4 = 121665$.
\item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) p}\\
In order to consider all the possible inputs, we assume each
element of the list \texttt{p} to be bounded by $0$ included and $2^8$
excluded.
\item[] \VSTe{PROP}: \VSTe{Zlength p = 32}\\
We also assume that the length of the list \texttt{p} is 32. This defines the
complete representation of \TNaCle{u8[32]}.
\end{itemize}
As postcondition we have conditions like:
\begin{itemize}
\item[] \VSTe{POST}: \VSTe{tint}\\
The function \TNaCle{crypto_scalarmult} returns an integer.
\item[] \VSTe{LOCAL}: \VSTe{temp ret_temp (Vint Int.zero)}\\
The returned integer has value $0$.
\item[] \VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (RFC n p)}\\
In the memory share \texttt{sh}, the address \VSTe{v_q} points
to a list of integer values \VSTe{mVI (RFC n p)} where \VSTe{RFC n p} is the
result of the \TNaCle{crypto_scalarmult} of \VSTe{n} and \VSTe{p}.
\item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (RFC n p)}\\
\VSTe{PROP}: \VSTe{Zlength (RFC n p) = 32}\\
We show that the computation for \VSTe{RFC} fits in \TNaCle{u8[32]}.
\item[] \VSTe{POST}: \VSTe{tint}\\
The function \TNaCle{crypto_scalarmult} returns an integer.
\item[] \VSTe{LOCAL}: \VSTe{temp ret_temp (Vint Int.zero)}\\
The returned integer has value $0$.
\item[] \VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (RFC n p)}\\
In the memory share \texttt{sh}, the address \VSTe{v_q} points
to a list of integer values \VSTe{mVI (RFC n p)} where \VSTe{RFC n p} is the
result of the \TNaCle{crypto_scalarmult} of \VSTe{n} and \VSTe{p}.
\item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (RFC n p)}\\
\VSTe{PROP}: \VSTe{Zlength (RFC n p) = 32}\\
We show that the computation for \VSTe{RFC} fits in \TNaCle{u8[32]}.
\end{itemize}
\TNaCle{crypto_scalarmult} computes the same result as \VSTe{RFC}
......@@ -126,10 +129,10 @@ when \texttt{M(o,a,a)} is called (squaring), the first two memory areas (\texttt
are consumed and VST will expect a third memory section (\texttt{a}) which does not \emph{exist} anymore.
Examples of such cases are illustrated in \fref{tikz:MemSame}.
\begin{figure}[h]%
\centering%
\include{tikz/memory_same_sh}%
\caption{Aliasing and Separation Logic}%
\label{tikz:MemSame}%
\centering%
\include{tikz/memory_same_sh}%
\caption{Aliasing and Separation Logic}%
\label{tikz:MemSame}%
\end{figure}
As a result, a function must either have multiple specifications or specify which
aliasing case is being used.
......@@ -137,16 +140,16 @@ The first option would require us to do very similar proofs multiple times for a
We chose the second approach: for functions with 3 arguments, named hereafter \texttt{o, a, b},
we define an additional parameter $k$ with values in $\{0,1,2,3\}$:
\begin{itemize}
\item if $k=0$ then \texttt{o} and \texttt{a} are aliased.
\item if $k=1$ then \texttt{o} and \texttt{b} are aliased.
\item if $k=2$ then \texttt{a} and \texttt{b} are aliased.
\item else there is no aliasing.
\item if $k=0$ then \texttt{o} and \texttt{a} are aliased.
\item if $k=1$ then \texttt{o} and \texttt{b} are aliased.
\item if $k=2$ then \texttt{a} and \texttt{b} are aliased.
\item else there is no aliasing.
\end{itemize}
In the proof of our specification, we do a case analysis over $k$ when needed.
This solution does not cover all the possible cases of aliasing over 3 pointers
(\eg \texttt{o} = \texttt{a} = \texttt{b}) but it is enough to satisfy our needs.
\subheading{Improving speed.}
\subheading{Improving verification speed.}
To make the verification the smoothest, the Coq formal definition of the function
should be as close as possible to the C implementation.
Optimizations of such definitions are often counter-productive as they increase the
......
......@@ -34,7 +34,16 @@ with it in the proofs (\ref{subsec:curvep2}).
\label{subsec:ECC}
\fref{tikz:ProofHighLevel1} presents the structure of the proof of the ladder's
correctness.
correctness. The white tiles are definitions, the orange one are hypothesis and
the green tiles represent major lemmas and theorems.
We consider elliptic curves over a field $\K$. We assume that the
characteristic of $\K$ is neither 2 or 3.
We formalize the Montgomery curves ($M_{a,b}(\K)$), then by using the equivalent
Weierstra{\ss} form ($E_{a',b'}(\K)$) from the library of Bartzia and Strub, we prove
that $M_{a,b}(\K)$ forms an associative finite group. Under the hypothesis that
$a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref{thm:montgomery-ladder-correct}).
\begin{figure}[h]
\centering
\include{tikz/highlevel1}
......@@ -42,8 +51,6 @@ correctness.
\label{tikz:ProofHighLevel1}
\end{figure}
We consider elliptic curves over a field $\K$. We assume that the
characteristic of $\K$ is neither 2 or 3.
\begin{dfn}
Given a field $\K$,
......@@ -169,14 +176,17 @@ Definition add (p1 p2 : point K) :=
And again we prove the result is on the curve: % (again with coercion):
\begin{lstlisting}[language=Coq]
Lemma addO (p q : mc) : oncurve (add p q).
Definition addmc (p1 p2 : mc) : mc :=
MC p1 p2 (addO p1 p2)
\end{lstlisting}
We then define a bijection between a Montgomery curve and its short Weierstra{\ss} form.
We then define a bijection between a Montgomery curve and its short Weierstra{\ss} form
(\lref{lemma:bij-ecc}).
In this way we get associativity of addition on Montgomery curves from the
corresponding property for Weierstra{\ss} curves.
\begin{lemma}
\label{lemma:bij-ecc}
Let $M_{a,b}$ be a Montgomery curve, define
$$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$
then $E_{a',b'}$ is an elliptic curve, and the mapping
......@@ -187,21 +197,21 @@ corresponding property for Weierstra{\ss} curves.
\end{align*}
is an isomorphism between elliptic curves.
\end{lemma}
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Definition ec_of_mc_point p :=
match p with
| \infty => \infty
| (|x, y|) => (|x/(M#b) + (M#a)/(3%:R * (M#b)), y/(M#b)|)
end.
Lemma ec_of_mc_point_ok p :
oncurve M p ->
ec.oncurve E (ec_of_mc_point p).
Definition ec_of_mc p :=
EC (ec_of_mc_point_ok (oncurve_mc p)).
Lemma ec_of_mc_bij : bijective ec_of_mc.
\end{lstlisting}
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Definition ec_of_mc_point p :=
% match p with
% | \infty => \infty
% | (|x, y|) => (|x/(M#b) + (M#a)/(3%:R * (M#b)), y/(M#b)|)
% end.
% Lemma ec_of_mc_point_ok p :
% oncurve M p ->
% ec.oncurve E (ec_of_mc_point p).
% Definition ec_of_mc p :=
% EC (ec_of_mc_point_ok (oncurve_mc p)).
% Lemma ec_of_mc_bij : bijective ec_of_mc.
% \end{lstlisting}
\subsubsection{Projective coordinates}
\label{subsec:ECC-projective}
......@@ -224,21 +234,26 @@ With this equation we can additionally represent the ``point at infinity''. By
setting $Z=0$, we derive $X=0$, giving us the ``infinite point'' $(0:1:0)$.
By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a
square in \K, we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.
square in \K (Hypothesis \ref{hyp:a_minus_4_not_square}),
we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.
\begin{hypothesis}
\label{hyp:a_minus_4_not_square}
$a^2-4$ is not a square in \K.
\end{hypothesis}
\begin{lstlisting}[language=Coq]
Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.
Hypothesis mcu_no_square :
forall x : K, x^+2 != (M#a)^+2 - 4%:R.
\end{lstlisting}
We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
\begin{dfn}Let $\chi$ and $\chi_0$:\\
-- $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$\\
such that $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$.\\
-- $\chi_0 : M_{a,b}(\K) \to \K$\\
such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.
\vspace{-1em}
\begin{itemize}
\item[--] $\chi : M_{a,b}(\K) \to \K \cup \{\infty\}$\\
such that $\chi(\Oinf) = \infty$ and $\chi((x,y)) = x$.
\item[--] $\chi_0 : M_{a,b}(\K) \to \K$\\
such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.
\end{itemize}
\end{dfn}
Using projective coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).
\begin{lemma}
......@@ -327,6 +342,17 @@ final proof of \coqe{Theorem RFC_Correct}.
\label{subsec:curve_twist_fields}
\fref{tikz:ProofHighLevel2} gives a high-level view of the proofs presented here.
The white tiles are definitions while green tiles are important lemmas and theorems.
A brief overview of the complete proof is described bellow.
We first pose $a = 486662$, $b = 1$, $b' = 2$, $p = 2^{255}-19$, with the equations $C = M_{a,b}$, and $T = M_{a,b'}$.
We prove the primality of $p$ and define the field $\F{p}$.
Subsquently we show that neither $2$ nor $a^2 - 2$ are square in $\F{p}$.
We consider $\F{p^2}$ and define $C(\F{p})$, $T(\F{p})$, and $C(\F{p^2})$.
We prove that for all $x \in \F{p}$ there exist a point of \xcoord $x$ either on $C(\F{p})$ or on the quadratic twist $T(\F{p})$.
We prove that all points in $M(\F{p})$ and $T(\F{p})$ can be projected in $M(\F{p^2})$ and derive that computations done in $M(\F{p})$ and $T(\F{p})$ yield to the same results if projected to $M(\F{p^2})$.
Using \tref{thm:montgomery-ladder-correct} we prove that the ladder is correct for $M(\F{p})$ and $T(\F{p})$; with the previous results, this results in the correctness of the ladder for $M(\F{p^2})$, in other words the correctness of X25519.
\begin{figure}[h]
\centering
......@@ -359,13 +385,6 @@ Definition betweenb x y z := (x <=? z) && (z <? y).
Definition p := locked (2^255 - 19).
Fact Hp_gt0 : p > 0.
Inductive type := Zmodp x of betweenb 0 p x.
Lemma Z_mod_betweenb (x y : Z) :
y > 0 -> betweenb 0 y (x mod y).
Definition pi (x : Z) : type :=
Zmodp (Z_mod_betweenb x Hp_gt0).
Coercion repr (x : type) : Z :=
let: @Zmodp x _ := x in x.
\end{lstlisting}
We define the basic operations ($+, -, \times$) with their respective neutral
......@@ -454,8 +473,6 @@ Inductive type :=
Definition pi (x: Zmodp.type * Zmodp.type) : type :=
Zmodp2 x.1 x.2.
Coercion repr (x: type) : Zmodp.type*Zmodp.type :=
let: Zmodp2 u v := x in (u, v).
Definition mul (x y: type) : type :=
pi ((x.1 * y.1) + (2%:R * (x.2 * y.2)),
(x.1 * y.2) + (x.2 * y.1)).
......@@ -561,15 +578,15 @@ computation in $\F{p^2}$.
for all $x \in \F{p}$ and $P \in M_{486662,1}(\F{p^2})$ such that $\chi_0(P) = x$,
$Curve25519\_Fp(n,x)$ computes $\chi_0(n \cdot P)$.
\end{theorem}
which is formalized in Coq as:
\begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
Theorem curve25519_Fp2_ladder_ok:
forall (n : nat) (x:Zmodp.type),
(n < 2^255)%nat ->
forall (p : mc curve25519_Fp2_mcuType),
p #x0 = Zmodp2.Zmodp2 x 0 ->
curve25519_Fp_ladder n x = (p *+ n)#x0 /p.
\end{lstlisting}
% which is formalized in Coq as:
% \begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
% Theorem curve25519_Fp2_ladder_ok:
% forall (n : nat) (x:Zmodp.type),
% (n < 2^255)%nat ->
% forall (p : mc curve25519_Fp2_mcuType),
% p #x0 = Zmodp2.Zmodp2 x 0 ->
% curve25519_Fp_ladder n x = (p *+ n)#x0 /p.
% \end{lstlisting}
We then prove the equivalence between of operations in $\Ffield$ and $\Zfield$,
in other words between \coqe{Zmodp} and \coqe{:GF}.
......
......@@ -69,6 +69,12 @@ I believe this paper describes a valuable work and contribution, that I apprecia
Such a paper is difficult to write. The authors have visibly devoted great efforts to tackle this difficulty, but it remains a challenging read.
\begin{itemize}
\item The paper takes us from one technical point to another in a manner that seems arbitrary at times, and hinders the overall structure. The problem is quite global, but a typical example is Definition 2.3: as a non-expert, it is hard to understand why this notion is important to introduce here, and it is essentially not used anywhere in the paper.
\end{itemize}
\begin{answer}{EEEEEE}
Computations over Curve25519 are done in $\F{p}$, as a result an easy mistake is to assume the curve defined over $\F{p}$ for all $x \in \F{p}$. However Curve25519 is defined over the quadratic extension which makes the Curve25519 over $\F{p}$ and its quadratic twist isomorphic over $\F{p^2}$ (Definition 2.3).
\end{answer}
\begin{itemize}
\item Figure 1 and Figure 4 are great, and have the potential to help so much the reader against the previous issue. Unfortunately, they are not commenting, and hence fail to do so!
\item The protocol considered is standard, and its implementation made to be of reasonable complexity. The paper should therefore really aim to:
\begin{enumerate}
......@@ -107,15 +113,21 @@ Here are a few linear comments:
\item \textbf{page 2:}\\
Figure 1 is great, but would deserve a lengthy explanation!
\end{itemize}
\begin{answer}{EEEEEE}
We added an additional description of the figure.
\end{answer}
\begin{itemize}
\item \textbf{page 3, column 1:}\\
Definition 2.3: It's been very unclear to me as a non-expert in cryptography and this protocole in particular what was the purpose of this definition.\\
"depending of" $\rightarrow$ "depending on"\\
{\color{gray}"depending of" $\rightarrow$ "depending on"}\\
"depending of the value of the kth bit" $\rightarrow$ unclear what k is at this point
\item \textbf{page 3, column 2:}\\
Algorithm 1: unclear what "m" is\\
"RFC 7748 standardize" $\rightarrow$ "RFC 7748 standardizes"
{\color{gray}"RFC 7748 standardize" $\rightarrow$ "RFC 7748 standardizes"}
\item \textbf{page 4, column 2:}\\
It's minor, but it is more shiny nowadays to cite The Odd Order theorem that the Four Color theorem as a mathematical achievement in Coq\\
......@@ -151,8 +163,8 @@ Here are a few linear comments:
Figure 3: Please comment generously this figure, it looks great but it is frustrating to try to decipher it without help.
\item \textbf{page 9:}\\
"the type of field which characteristic" $\rightarrow$ "whose characteristic"?\\
"The value of add is proven to be on the curve (with coercion)" $\rightarrow$ This parenthesis is too cryptic, it should probably be dropped
{\color{gray}"the type of field which characteristic" $\rightarrow$ "whose characteristic"\\
"The value of add is proven to be on the curve (with coercion)" $\rightarrow$ This parenthesis is too cryptic, it should probably be dropped.}
\item \textbf{page 11:}\\
Figure 4: this one is the apex: it would deserve a full column of explanations
......@@ -162,9 +174,12 @@ Here are a few linear comments:
CompCert: "However, when compiling (...)" $\rightarrow$ I am quite confused about this sentence. Do you mean when compiling the verified C code with gcc? If so, beyond the question whether CompCert matches C17 (which it doesn't, it matches C99), the real problem is to assume that gcc is bug free! I would expect with this whole approach that the expectation is to run a protocole compiled with CompCert.\\
clightGen: "VST does not support (...)" $\rightarrow$ Hard to undertand the relation between this sentence and the previous one.\\
Extending our work: What about proving other NaCl implementations?
\end{itemize}
\begin{answer}{EEEEEE}
\todo{Freek : which version of ISO.}
\end{answer}
\begin{center}
\subheading{===== Requested changes =====}
\end{center}
......
......@@ -298,36 +298,36 @@ literate=
{^n}{{$^n$}}1
{^+n}{{$^n$}}1
{^m}{{$^m$}}1
{^2}{{\makebox[8pt][l]{$^2$}}}1
{^+2}{{\makebox[8pt][l]{$^2$}}}1
{^3}{{\makebox[8pt][l]{$^3$}}}1
{^+3}{{\makebox[8pt][l]{$^3$}}}1
{^2}{{\makebox[4.5pt][l]{$^2$}}}1
{^+2}{{\makebox[4.5pt][l]{$^2$}}}1
{^3}{{\makebox[4.5pt][l]{$^3$}}}1
{^+3}{{\makebox[4.5pt][l]{$^3$}}}1
{^nd}{{$^{nd}$}}1
{^rd}{{$^{rd}$}}1
{^th}{{$^{th}$}}1
{^255}{{$^{255}$}}1
{^-1}{{$^{-1}$}}1
{\%:R}{{}}1
{p1}{{p\makebox[8pt][l]{$_1$}}}1
{p2}{{p\makebox[8pt][l]{$_2$}}}1
{x1}{{x\makebox[8pt][l]{$_1$}}}1
{x2}{{x\makebox[8pt][l]{$_2$}}}1
{x3}{{x\makebox[8pt][l]{$_3$}}}1
{x_1}{{x\makebox[8pt][l]{$_1$}}}1
{x_2}{{x\makebox[8pt][l]{$_2$}}}1
{x_3}{{x\makebox[8pt][l]{$_3$}}}1
{x4}{{x\makebox[8pt][l]{$_4$}}}1
{y1}{{y\makebox[8pt][l]{$_1$}}}1
{y2}{{y\makebox[8pt][l]{$_2$}}}1
{y3}{{y\makebox[8pt][l]{$_3$}}}1
{y4}{{y\makebox[8pt][l]{$_4$}}}1
{z1}{{z\makebox[8pt][l]{$_1$}}}1
{z2}{{z\makebox[8pt][l]{$_2$}}}1
{z3}{{z\makebox[8pt][l]{$_3$}}}1
{z4}{{z\makebox[8pt][l]{$_4$}}}1
{z_2}{{z\makebox[8pt][l]{$_2$}}}1
{z_3}{{z\makebox[8pt][l]{$_3$}}}1
{xs}{{x\makebox[8pt][l]{$_s$}}}1
{p1}{{p\makebox[5pt][l]{$_1$}}}1
{p2}{{p\makebox[5pt][l]{$_2$}}}1
{x1}{{x\makebox[5pt][l]{$_1$}}}1
{x2}{{x\makebox[5pt][l]{$_2$}}}1
{x3}{{x\makebox[5pt][l]{$_3$}}}1
{x_1}{{x\makebox[5pt][l]{$_1$}}}1
{x_2}{{x\makebox[5pt][l]{$_2$}}}1
{x_3}{{x\makebox[5pt][l]{$_3$}}}1
{x4}{{x\makebox[5pt][l]{$_4$}}}1
{y1}{{y\makebox[5pt][l]{$_1$}}}1
{y2}{{y\makebox[5pt][l]{$_2$}}}1
{y3}{{y\makebox[5pt][l]{$_3$}}}1
{y4}{{y\makebox[5pt][l]{$_4$}}}1
{z1}{{z\makebox[5pt][l]{$_1$}}}1
{z2}{{z\makebox[5pt][l]{$_2$}}}1
{z3}{{z\makebox[5pt][l]{$_3$}}}1
{z4}{{z\makebox[5pt][l]{$_4$}}}1
{z_2}{{z\makebox[5pt][l]{$_2$}}}1
{z_3}{{z\makebox[5pt][l]{$_3$}}}1
{xs}{{x\makebox[5pt][l]{$_s$}}}1
{\\-}{{\makebox[9pt][c]{$-$}}}1
{\\+}{{\makebox[9pt][c]{$+$}}}1
{\\*}{{\makebox[9pt][c]{$*$}}}1
......@@ -391,7 +391,7 @@ literate=
% \newcommand{\lstbg}[3][0pt]{{\fboxsep#1\colorbox{#2}{\strut #3}}}
\lstdefinelanguage{diff}{
basicstyle=\ttfamily\small,
basicstyle=\ttfamily\scriptsize,
morecomment=[f][\color{doc@lstidentifiers2}]-,
morecomment=[f][\color{doc@lstfunctions}]+,
morecomment=[f][\color{gray}\textit]{@@},
......@@ -408,9 +408,9 @@ literate=
\lstset{%
lineskip=-0.1em,
%
% basicstyle=\ttfamily\scriptsize, % font that is used for the code
basicstyle=\ttfamily\scriptsize, % font that is used for the code
% basicstyle=\ttfamily\small, % font that is used for the code
basicstyle=\ttfamily\footnotesize, % font that is used for the code
% basicstyle=\ttfamily\footnotesize, % font that is used for the code
identifierstyle=\color{doc@lstidentifier},
commentstyle=\color{doc@lstcomment}\footnotesize,
% \itshape,
......