Commit 1d4849db authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more test

parent 14d2db75
......@@ -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 \Coqe{RFC}.
The specification of X25519 in RFC~7748 is formalized by \Coqe{RFC} in Coq.
\end{informaltheorem}
More precisely, we formalized X25519 with the following definition.
......@@ -29,7 +29,11 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
\end{lstlisting}
We first present a generic description of the Montgomery ladder (\ref{subsec:spec-ladder}).
Then we turn our attention to the different steps of the computation (\ref{subsec:spec-unpack-clamp-inv-pack}).
Then we describe our mapping between little-endian representations and integers
(\ref{subsec:integer-bytes}) which we use to formalize the encoding and decoding.
We then turn our attention to the last steps of the computation
(\ref{subsec:spec-unpack-clamp-inv-pack}).
......@@ -39,9 +43,9 @@ Then we turn our attention to the different steps of the computation (\ref{subse
% \emph{``All calculations are performed in GF(p), i.e., they are performed modulo p.''}
TweetNaCl implements X25519 with numbers represented as arrays.
RFC~7748 defines X25519 over field elements. As we show the equivalence between
the different representation, to simplify our proof, we define operations used
in the ladder over generic types \coqe{T} and \coqe{T'}.
RFC~7748 defines X25519 over field elements. We show the equivalence between
the different number representations. To simplify our proof, we define operations
used in the ladder over generic types \coqe{T} and \coqe{T'}.
Those types are later instantiated as natural numbers, integers, field elements,
list of integers.
......@@ -57,43 +61,92 @@ This divergence is allowed by the RFC:
original paper. Implementations are free to use any correct formulas.''}~\cite{rfc7748}.
We later prove our ladder correct in that respect (\sref{sec:maths}).
% In appendix~\ref{subsubsec:CryptoScalarmult}, we show the the formalization of
% \TNaCle{crypto_scalarmult} over lists of integers. We define it as
% \Coqe{Crypto_Scalarmult} or \Coqe{CSM}. For the sake of space and simplicity we
% do not display the definitions of each underlying function.
\subsection{Unpacking, clamping, Inversion and Packing}
\label{subsec:spec-unpack-clamp-inv-pack}
\subsection{Integers and Bytes}
\label{subsec:integer-bytes}
\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}
Operations used in the montgomery ladder of \coqe{RFC} are intentiated over
integers (See Appendix~\ref{subsubsec:RFC-Coq}). The modulo reduction by $\p$
is done at the end with the \coqe{ZPack25519} operation.
In TweetNaCl, as described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are
represented in base $2^{16}$ and we use a direct mapping to represent that array as a list
integers in Coq.
We define the little-endian projection to integers as follows.
\begin{dfn}
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list}~\Z \rightarrow \Z$,
a parameterized map by $n$ between a list $l$ and its little endian representation
with a radix $2^n$.
\end{dfn}
We define it in Coq as:
\begin{lstlisting}[language=Coq]
Fixpoint ZofList {n:Z} (a:list Z) : Z :=
match a with
| [] => 0
| h :: q => h + 2^n * ZofList q
end.
\end{lstlisting}
\Coqe{ZofList} is used in the decoding of the bytes array and also as a
base to verify operations over lists in TweetNaCl (See~\ref{subsec:num-repr-rfc}).
Similarly the encoding from integers to bytes is defined:
\begin{dfn}
Let \Coqe{ListofZ32} : $\Z \rightarrow \Z \rightarrow \texttt{list}~\Z$, given
$n$ and $a$ returns $a$'s little-endian representation
as a list with radix $2^n$.
\end{dfn}
We define it in Coq as:
\begin{lstlisting}[language=Coq]
Fixpoint ListofZn_fp {n:Z} (a:Z) (f:nat) : list Z :=
match f with
| 0%nat => []
| S fuel => (a mod 2^n) :: ListofZn_fp (a/2^n) fuel
end.
Definition ListofZ32 {n:Z} (a:Z) : list Z :=
ListofZn_fp n a 32.
\end{lstlisting}
In order to increase the trust in our formalization, we prove that
\Coqe{ListofZ32} and \Coqe{ZofList} are inverse to each other.
\begin{lstlisting}[language=Coq]
Lemma ListofZ32_ZofList_Zlength: forall (l:list Z),
Forall (fun x => 0 <= x < 2^n) l ->
Zlength l = 32 ->
ListofZ32 n (ZofList n l) = l.
\end{lstlisting}
With those tools at hand, we formally define the decoding and encoding as specified in the RFC.
\begin{lstlisting}[language=Coq]
Definition decodeScalar25519 (l: list Z) : Z :=
ZofList 8 (clamp l).
Definition decodeUCoordinate (l: list Z) : Z :=
ZofList 16 (Unpack25519 l).
ZofList 8 (upd_nth 31 l
(Z.land (nth 31 l 0) 127)).
Definition encodeUCoordinate (x: Z) : list Z :=
ListofZ32 8 x.
\end{lstlisting}
Inputs of X25519
% \emph{``To implement the X25519(k, u) and X448(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}
\subsection{Clamping, Inversion and Packing}
\label{subsec:spec-unpack-clamp-inv-pack}
\coqe{montgomery_rec} only computes the ladder steps.
While the inversion, the packing, the unpacking (setting bit 255 to \texttt{0})
and the clamping are not defined in a generic manner, we show their equivalence
between the different representations.
We have seen that \coqe{montgomery_rec} only computes the ladder steps.
While the inversion, the packing
Appendix~\ref{subsubsec:ZCryptoScalarmult} shows the instantiation of our ladder
over Integers (type \coqe{Z}). We call it \coqe{ZCrypto_Scalarmult}.
The modulo reduction is applied in \coqe{ZPack25519} translating every
underlying operations as over \Zfield. As a result this specification can be
interpreted as the formalization of X25519 in RFC~7748.
% Appendix~\ref{subsubsec:ZCryptoScalarmult} shows the instantiation of our ladder
% over Integers (type \coqe{Z}). We call it \coqe{ZCrypto_Scalarmult}.
% The modulo reduction is applied in \coqe{ZPack25519} translating every
% underlying operations as over \Zfield. As a result this specification can be
% interpreted as the formalization of X25519 in RFC~7748.
......@@ -14,8 +14,8 @@ More formally.
\todo{INSERT COQ DEFINITION HERE}
We first describe the global structure of our proof (\ref{subsec:proof-structure}).
We introduce our translation of RFC~7748 (\ref{subsec:spec-rfc}) and specify
the Hoare triple before proving its correctness with VST (\ref{subsec:with-VST}).
Using our formalization of RFC~7748 (\sref{sec:Coq-RFC}) we specify the Hoare
triple before proving its correctness with VST (\ref{subsec:with-VST}).
We provide an example of equivalence of operations over different number
representations (\ref{subsec:num-repr-rfc}). Then, we describe efficient techniques
used to in some of our more complex proofs (\ref{subsec:inversions-reflections}).
......
......@@ -3,14 +3,14 @@
In this section we prove the following theorem:
% \label{thm:Elliptic-RFC}
\begin{informaltheorem}
\label{thm:Elliptic-RFC}
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) computes the
The implementation of X25519 in TweetNaCl computes the
$\F{p}$-restricted $x$-coordinate scalar multiplication on $E(\F{p^2})$ where $p$ is $\p$
and $E$ is the elliptic curve $y^2 = x^3 + 486662 x^2 + x$.
\end{informaltheorem}
More formally:
More formally, we prove that our formalization of the RFC matches the definitions of Curve25519 by Bernstein:
\begin{lstlisting}[language=Coq]
Theorem RFC_Correct: forall (n p : list Z)
(P:mc curve25519_Fp2_mcuType),
......@@ -20,7 +20,8 @@ Theorem RFC_Correct: forall (n p : list Z)
Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
Fp2_x (decodeUCoordinate p) = P#x0 ->
RFC n p =
encodeUCoordinate ((P *+ (Z.to_nat (decodeScalar25519 n))) _x0).
encodeUCoordinate
((P *+ (Z.to_nat (decodeScalar25519 n))) _x0).
\end{lstlisting}
We first review the work of Bartzia and Strub \cite{BartziaS14} (\ref{subsec:ECC-Weierstrass}).
......
......@@ -10,10 +10,10 @@ Generic definition of the ladder:
(* Typeclass to encapsulate the operations *)
Class Ops (T T': Type) (Mod: T -> T):=
{
+ : T -> T -> T; (* Add *)
* : T -> T -> T; (* Mult *)
- : T -> T -> T; (* Sub *)
x^2 : T -> T; (* Square *)
A : T -> T -> T; (* Add *)
M : T -> T -> T; (* Mult *)
Zub : T -> T -> T; (* Sub *)
Sq : T -> T; (* Square *)
C_0 : T; (* Constant 0 *)
C_1 : T; (* Constant 1 *)
C_121665: T; (* const (a-2)/4 *)
......@@ -21,6 +21,12 @@ Class Ops (T T': Type) (Mod: T -> T):=
Getbit: Z -> T' -> Z; (* ith bit *)
}.
Local Notation "X + Y" := (A X Y) (only parsing).
Local Notation "X - Y" := (Zub X Y) (only parsing).
Local Notation "X * Y" := (M X Y) (only parsing).
Local Notation "X ^2" := (Sq X) (at level 40,
only parsing, left associativity).
Fixpoint montgomery_rec (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
(* a: x2 *)
......@@ -122,17 +128,17 @@ Module Mid.
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))).
(* Clamping *)
Definition clamp (n : list Z) : list Z :=
(* set last 3 bits to 0 *)
let x := nth 0 n 0 in
let x' := Z.land x 248 in
(* set bit 255 to 0 and bit 254 to 1 *)
let t := nth 31 n 0 in
let t' := Z.lor (Z.land t 127) 64 in
(* update the list *)
let n' := upd_nth 31 n t' in
upd_nth 0 n' x'.
(* x^{p - 2} *)
Definition ZInv25519 (x:Z) : Z :=
......@@ -156,7 +162,7 @@ Definition decodeScalar25519 (l: list Z) : Z :=
ZofList 8 (clamp l).
Definition decodeUCoordinate (l: list Z) : Z :=
ZofList 16 (Unpack25519 l).
ZofList 8 (upd_nth 31 l (Z.land (nth 31 l 0) 127)).
Definition encodeUCoordinate (x: Z) : list Z :=
ListofZ32 8 x.
......@@ -181,27 +187,25 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
in encodeUCoordinate o.
\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{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)).
% \end{lstlisting}
\subsubsection{Equivalence between For Loops}
\label{subsubsec:for}
......
......@@ -169,7 +169,7 @@ morekeywords=[5]{by, done, exact, reflexivity, tauto, romega, omega,
morekeywords=[6]{do, last, first, try, idtac, repeat},
%
% Control
morekeywords=[7]{Forall, ZofList, Zlength, length},
% morekeywords=[7]{Forall, ZofList, Zlength, length, ListofZ32},
%
% Comments delimiters, we do turn this off for the manual
morecomment=[s]{(*}{*)},
......@@ -246,11 +246,14 @@ literate=
% {\@\@}{{$@$}}1
{:GF}{{\color{doc@lstfunctions}{:$GF$}}}1
% {0}{{\color{doc@lstnumbers}{$0$}}}1
{32}{{\color{doc@lstnumbers}{$32$}}}1
% {32}{{\color{doc@lstnumbers}{$32$}}}1
{2^8}{{\color{doc@lstnumbers}{$2^8$}}}1
{2^16}{{\color{doc@lstnumbers}{$2^{16}$}}}1
{2^26}{{\color{doc@lstnumbers}{$2^{26}$}}}1
{2^62}{{\color{doc@lstnumbers}{$2^{62}$}}}1
% {2^16}{{\color{doc@lstnumbers}{$2^{16}$}}}1
{2^16}{{$2^{16}$}}1
% {2^26}{{\color{doc@lstnumbers}{$2^{26}$}}}1
{2^26}{{$2^{26}$}}1
% {2^62}{{\color{doc@lstnumbers}{$2^{62}$}}}1
{2^62}{{$2^{62}$}}1
{2^256}{{\color{doc@lstnumbers}{$2^{256}$}}}1
{2^255-19}{{\color{doc@lstnumbers}{$2^{255}-19$}}}1
{2^255-21}{{\color{doc@lstnumbers}{$2^{255}-21$}}}1
......
......@@ -81,7 +81,7 @@
% SECTION V
% Spec of Curve nP
\begin{scope}[yshift=-7.25 cm,xshift=0 cm]
\begin{scope}[yshift=-7.5 cm,xshift=0 cm]
\draw (0,0) -- (0.4, 0.4) -- (1.75,0.4) -- (1.75,0) -- cycle;
\draw (0,0) -- (1.75,0) -- (1.75,-1) -- (0, -1) -- cycle;
\draw (0.3,-0.05) node[textstyle] {Definition};
......@@ -89,7 +89,7 @@
\end{scope}
% Correctness Theorem
\begin{scope}[yshift=-6.75 cm,xshift=6 cm]
\begin{scope}[yshift=-7 cm,xshift=6 cm]
\draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle;
\draw (0,0) -- (2.5,0) -- (2.5,-1.5) -- (0, -1.5) -- cycle;
\draw (0.3,-0.05) node[textstyle] {Proof};
......@@ -99,10 +99,10 @@
\path [thick, double, ->] (1.75,-3.5) edge [out=0, in=-180] (3, -3.5);
\path [thick, double] (1.75,-3.5) edge [out=0, in=90] (2.25, -4);
\path [thick, double] (2.25, -4) edge [out=-90, in=90] (2.25, -6.75);
\path [thick, double] (2.25, -6.75) edge [out=-90, in=-180] (3, -7.5);
\path [thick, double, ->] (3, -7.5) edge [out=0, in=-180] (6, -7.5);
\path [thick, double, ->] (1.75,-7.75) edge [out=0, in=-180] (6, -7.75);
\path [thick, double] (2.25, -4) edge [out=-90, in=90] (2.25, -7);
\path [thick, double] (2.25, -7) edge [out=-90, in=-180] (3, -7.75);
\path [thick, double, ->] (3, -7.75) edge [out=0, in=-180] (6, -7.75);
\path [thick, double, ->] (1.75,-8) edge [out=0, in=-180] (6, -8);
\end{tikzpicture}
Markdown is supported
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