Commit b6ba7ef3 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

removing stuff + feedback from Freek

parent f9914841
......@@ -16,13 +16,13 @@ One core component of TweetNaCl (and NaCl) is the key-exchange protocol X25519~\
This protocol is being used by a wide variety of applications~\cite{things-that-use-curve25519}
such as SSH, Signal Protocol, Tor, Zcash, and TLS to establish a shared secret over
an insecure channel.
The X25519 key exchange protocol is a an $x$-coordinate only
The X25519 key exchange protocol is a an \xcoord only
elliptic-curve Diffie-Hellman key-exchange using the Montgomery
curve $E: y^2 = x^3 + 486662 x^2 + x$ over the field $\F{\p}$.
Note that originally, the name ``Curve25519'' referred to the key exchange protocol,
but Bernstein suggested to rename the scheme to X25519 and to use the name
X25519 for the protocol and Curve25519 for the underlying elliptic curve~\cite{Ber14}.
We make use of this updated terminology in this paper.
We use this updated terminology in this paper.
\subheading{Contribution of this paper}
We provide a mechanized formal proof of the correctness of the X25519
......@@ -50,8 +50,8 @@ This extension may be of independent interest.
\subheading{Related work.}
Two methodologies exist to get formal guarantees that software meets its specification.
This can be done either by synthesizing a formal specification and then generating
machine code by refinement, or by writing a specification and verifying that the
This can be done either by writing a formal specification and then synthesis
machine code by refinement, or by formalizing a specification and verifying that the
implementation satisfies it.
% One of the earliest example of this first approach is the
......@@ -74,9 +74,9 @@ that work our approach makes a complete link between the C implementation and
the formal mathematical definition of the group theory behind elliptic curves.
Synthesis approaches force the user to depend on generated code which may not
be optimal (speed, compactness...) and they require compiler tweaks in order
be optimal (speed, compactness) and they require compiler tweaks in order
to achieve the desired properties. On the other hand, carefully handcrafted
optimized code will force the verifier to consider all the possible special cases
optimized code forces the verifier to consider all the possible special cases
and write a low level specification of the details of the code in order to prove
the correctness of the algorithm.
......
......@@ -14,7 +14,7 @@ Finally, we provide a brief description of the formal tools we use in our proofs
\begin{dfn}
Given a field \K, let $a,b \in \K$ such that $a^2 \neq 4$ and $b \neq 0$,
$M_{a,b}$ is a Montgomery curve defined over $\K$ with equation:
$M_{a,b}$ is the Montgomery curve defined over $\K$ with equation:
$$M_{a,b}: by^2 = x^3 + ax^2 + x$$
\end{dfn}
......@@ -22,12 +22,14 @@ Finally, we provide a brief description of the formal tools we use in our proofs
For any algebraic extension $\L$ of $\K$, $\K \subseteq \L$,
$M_{a,b}(\L)$ is the set of $\L$-rational points which satisfy the equation with
addition to the point at infinity $\Oinf$.
% "with addition of" is a mistake in English
$$M_{a,b}(\L) = \{\Oinf\} \cup \{(x,y) \in \L \times \L~|~by^2 = x^3 + ax^2 + x\}$$
\end{dfn}
Details of the formalization can be found in \sref{subsec:ECC-Montgomery}.
For $M_{a,b}$ over $\F{p}$, the parameter $b$ is known as the ``twisting factor'',
for $b'\in \F{p}\backslash\{0\}$ and $b' \neq b$, the curves $M_{a,b}$ and $M_{a,b'}$
For $M_{a,b}$ over $\F{p}$, the parameter $b$ is known as the ``twisting factor''.
For $b'\in \F{p}\backslash\{0\}$ and $b' \neq b$, the curves $M_{a,b}$ and $M_{a,b'}$
are isomorphic via $(x,y) \mapsto (x, \sqrt{b'/b} \cdot y)$.
\begin{dfn}
......@@ -36,19 +38,22 @@ are isomorphic via $(x,y) \mapsto (x, \sqrt{b'/b} \cdot y)$.
\end{dfn}
Points over $M_{a,b}(\K)$ can be equipped with a structure of an abelian group
with the addition operation $\boxplus$ and with neutral element the point at infinity $\Oinf$.
with the addition operation $+$ and with neutral element the point at infinity $\Oinf$.
Using this law, we have the scalar multiplication over $M_{a,b}(\K)$ defined by:
$$n\cdot P = \underbrace{P \boxplus \cdots \boxplus P}_{n\text{ times}}$$
$$n\cdot P = \underbrace{P + \cdots + P}_{n\text{ times}}$$
In order to efficiently computes the scalar multiplication we use an algorithm
In order to efficiently compute the scalar multiplication we use an algorithm
similar to square-and-multiply: the Montgomery ladder where the basic operations
are addition and doubling.
We consider x-coordinate-only operations. In order to simplify computations,
such coordinates are represented as $X/Z$ fractions. We define two operations:
We consider \xcoord-only operations. In order to simplify computations,
such coordinates are represented as $X/Z$ fractions and use the $(X : Z)$ notation.
$(X : 1)$ is abbreviated as $X$. See \sref{subsec:ECC-projective} for more details.
We define two operations:
\begin{align*}
\texttt{xADD} &: (X_P, Z_P, X_Q , Z_Q, X_{P \boxminus Q}, Z_{P \boxminus Q}) \mapsto (X_{P \boxplus Q}, Z_{P \boxplus Q})\\
\texttt{xDBL} &: (X_P, Z_P) \mapsto (X_{2 \cdot P}, Z_{2 \cdot P})
\texttt{xADD} &: ((X_P:Z_P), (X_Q:Z_Q), (X_{P - Q}:Z_{P - Q})) \mapsto \\
&(X_{P + Q}:Z_{P + Q})\\
\texttt{xDBL} &: (X_P:Z_P) \mapsto (X_{2 \cdot P}:Z_{2 \cdot P})
\end{align*}
In the Montgomery ladder, % notice that
the arguments of \texttt{xADD} and \texttt{xDBL}
......@@ -59,26 +64,26 @@ Given a pair $(X_0, X_1)$ and a Boolean $b$, \texttt{CSWAP} returns the pair
$(X_b, X_{1-b})$.
By using the differential addition and doubling operations we define the Montgomery ladder
computing a $x$-coordinate-only scalar multiplication (see \aref{alg:montgomery-ladder}).
computing a \xcoord-only scalar multiplication (see \aref{alg:montgomery-ladder}).
\begin{algorithm}
\caption{Montgomery ladder for scalar mult.}
\label{alg:montgomery-ladder}
\begin{algorithmic}
\REQUIRE{x-coordinate of $P$ : $P.x$, scalars $n$ and $m$, $n < 2^m$}
\ENSURE{$Q = n \cdot P$}
\REQUIRE{\xcoord of $P$ : $(X_P:Z_P)$, scalars $n$ and $m$, $n < 2^m$}
\ENSURE{\xcoord of $Q$ : $(X_Q:Z_Q)$ where $Q = n \cdot P$}
\STATE $Q \leftarrow \Oinf$
\STATE $R \leftarrow (X_P,Z_P)$
\STATE $R \leftarrow (X_P:Z_P)$
\FOR{$k$ := $m$ down to $1$}
\STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$
\STATE $Q \leftarrow \texttt{xDBL}(Q)$
\STATE $R \leftarrow \texttt{xADD}(Q,R,X_P,Z_P)$
\STATE $R \leftarrow \texttt{xADD}(Q,R,(X_P:Z_P))$
\STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$
\ENDFOR
\RETURN $Q$
\end{algorithmic}
\end{algorithm}
Finally given $(X_Q : Z_Q)$, we compute the fraction representing the \xcoord of $n \cdot P$.
......@@ -87,28 +92,30 @@ computing a $x$-coordinate-only scalar multiplication (see \aref{alg:montgomery-
For any value $x \in \F{p}$, for the elliptic curve $E$ over $\F{p^2}$
defined by $y^2 = x^3 + 486662 x^2 + x$, there exist a point $P$ over $E(\F{p^2})$
such that $x$ is the $x$-coordinate of $P$.
such that $x$ is the \xcoord of $P$.
Given $n \in \N$ and $x \in \Ffield$, such that $x$ is the $x$-coordinate of
a point $P$ of $E(\F{p^2})$, X25519 returns the $x$-coordinate of the
scalar multiplication of $P$ by $n$, thus $n \cdot P$.
Given $n \in \N$ and $x \in \Ffield$, such that $x$ is the \xcoord of
a point $P$ of $E(\F{p^2})$, X25519 returns the \xcoord of $n \cdot P$, the
scalar multiplication of $P$ by $n$.
% Note that the result is the same with $n \cdot (-P) = -(n \cdot P)$.
X25519 makes use of the little endian bijection for its arguments of 32-bytes:
X25519 makes use of the little endian encoding (see \ref{subsec:integer-bytes})
for its arguments of 32-bytes:
\texttt{n} the secret key and \texttt{p} the public key.
% Curve25519 has a cofactor of 8.
In order to avoid attacks where an attacker
could discover some bits of the private key, values of $n$ are forced into the
shape of $2^{254} + 8\{0,1,\ldots,2^{251}-1\}$. This is done by setting bit 255
In order to avoid attacks where an attacker could discover some bits of the
private key, values of $n$ are forced into the shape of
$2^{254} + 8\{0,1,\ldots,2^{251}-1\}$. This is done by setting bit 255
to \texttt{0}; bit 254 to \texttt{1} and the lower 3 bits to \texttt{0},
making $n$ effectively a multiple of 8. This operation is known as the clamping.
RFC~7748~\cite{rfc7748} formalized the X25519 Diffie–Hellman key-exchange algorithm.
Given the base point $B$ where $B.x=9$, each party generate a secret random number
$s_a$ (respectively $s_b$), and computes $P_a$ (respectively $P_b$), the result
of the scalar multiplication between $B$ and $s_a$ (respectively $s_b$).
The party exchanges $P_a$ and $P_b$ and computes their shared secret with X25519
over $s_a$ and $P_b$ (respectively $s_b$ and $P_a$).
RFC~7748~\cite{rfc7748} standardized the X25519 Diffie–Hellman key-exchange algorithm.
Given the base point $B$ where $X_B=9$, each party generate a secret random number
$s_a$ (respectively $s_b$), and computes $X_{P_a}$ (respectively $X_{P_b}$), the
\xcoord of $P_A = s_a \cdot B$ (respectively $P_B = s_b \cdot B$).
% , the scalar multiplication of $B$ by $s_a$ (respectively $s_b$).
The party exchanges $X_{P_a}$ and $X_{P_b}$ and computes their shared secret with X25519
over $s_a$ and $X_{P_b}$ (respectively $s_b$ and $X_{P_a}$).
......@@ -117,8 +124,8 @@ over $s_a$ and $P_b$ (respectively $s_b$ and $P_a$).
\subsection{TweetNaCl specifics}
\label{subsec:Number-TweetNaCl}
As its name suggests, TweetNaCl aims for code compactness (in tweets).
As a result it uses a few defines and typedef to gain precious bytes while
As its name suggests, TweetNaCl aims for code compactness (in 100 tweets).
As a result it uses a few defines and typedefs to gain precious bytes while
still remaining readable.
\begin{lstlisting}[language=Ctweetnacl]
#define FOR(i,n) for (i = 0;i < n;++i)
......@@ -157,8 +164,8 @@ The individual ``limbs'' $a_i$ are represented as
typedef i64 gf[16];
\end{lstlisting}
Conversion from the input byte array to this representation is done
as follows:
Conversion from the input byte array to this representation in radix $2^{16}$ is
done as follows:
\begin{lstlisting}[language=Ctweetnacl]
sv unpack25519(gf o, const u8 *n)
{
......@@ -216,10 +223,23 @@ sv car25519(gf o)
In order to simplify the verification of this function,
we treat the last iteration of the loop $i = 15$ as a separate step.
Inverses in $\Ffield$ are computed with \TNaCle{inv25519}.
It takes the exponentiation by $2^{255}-21$ with the square-and-multiply algorithm.
Fermat's little theorem gives the correctness.
Inverses in $\Zfield$ are computed with \TNaCle{inv25519}.
It uses exponentiation by $2^{255}-21$, computed with the square-and-multiply
algorithm. Fermat's little theorem gives the correctness.
Notice that in this case the inverse of $0$ is defined as $0$.
\begin{lstlisting}[language=Ctweetnacl]
sv inv25519(gf o,const gf i)
{
gf c;
int a;
set25519(c,i);
for(a=253;a>=0;a--) {
S(c,c);
if(a!=2&&a!=4) M(c,c,i);
}
FOR(a,16) o[a]=c[a];
}
\end{lstlisting}
\TNaCle{sel25519} implements a constant-time conditional swap (\texttt{CSWAP}) by
applying a mask between two fields elements.
......@@ -236,9 +256,9 @@ sv sel25519(gf p,gf q,i64 b)
}
\end{lstlisting}
Finally, we require the \TNaCle{pack25519} function,
Finally, we need the \TNaCle{pack25519} function,
which converts from the internal redundant radix-$2^{16}$
representation to a unique byte array:
representation to a unique byte array.
\begin{lstlisting}[language=Ctweetnacl]
sv pack25519(u8 *o,const gf n)
{
......@@ -273,12 +293,13 @@ byte array.
\subheading{The Montgomery ladder.}
With these low-level arithmetic and helper functions at hand, we can now
% at hand is valid English: readily accessible when needed.
turn our attention to the core of the X25519 computation:
the \TNaCle{crypto_scalarmult} API function of TweetNaCl.
In order to compute the scalar multiplication,
X25519 uses the Montgomery ladder~\cite{Mon85}.
$x$-coordinates are represented as not-evaluated fractions, the computation of
\xcoords are represented as not-evaluated fractions, the computation of
the quotient 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$.
......@@ -342,12 +363,14 @@ int crypto_scalarmult(u8 *q,
\subsection{Coq and VST}
\label{subsec:Coq-VST}
Coq~\cite{coq-faq} is an interactive theorem prover. It provides an expressive
formal language to write mathematical definitions, algorithms and theorems together
with their proofs. It has been used in the proof of the four-color theorem~\cite{gonthier2008formal}.
Coq~\cite{coq-faq} is an interactive theorem prover based on type theory. It
provides an expressive formal language to write mathematical definitions,
algorithms and theorems together with their proofs. It has been used in the proof
of the four-color theorem~\cite{gonthier2008formal}.
The CompCert C compiler~\cite{Leroy-backend} was implemented with it.
The Compcert C semantic is very close to C17~\cite{ISO:C17}, giving us the guarantee
that the intended behavior is preserved through the compilation to the machine code.
The Compcert C semantics is almost identical to C17~\cite{ISO:C17}, giving us the
guarantee that the intended behavior is preserved through compilation to the
machine code.
As opposed to other systems such as F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17},
Coq does not rely on an SMT solver in its trusted code base.
......@@ -375,11 +398,12 @@ pointers and memory manipulation. This logic enforces strict conditions on the
memory shared such as being disjoint.
We discuss this limitation further in \sref{subsec:with-VST}.
The Verified Software Toolchain (VST)~\cite{cao2018vst-floyd} is a framework
which uses Separation logic to prove the functional correctness of C programs.
which uses Separation logic proven correct with respect to CompCert semantics
to prove the functional correctness of C programs.
The first step consists of translating the source code into Clight,
an intermediate representation used by CompCert.
For such purpose we use the parser of CompCert: \texttt{clightgen}.
In a second step we define the Hoare triple encapsulating the specification of the
piece of software we want to prove. Then using VST, we use a strongest
For such purpose one uses the parser of CompCert: \texttt{clightgen}.
In a second step one defines the Hoare triple representing the specification of
the piece of software one wants to prove. Then using VST, one uses a strongest
postcondition approach to prove the correctness of the triple.
This approach can be seen as a forward symbolic execution of the program.
......@@ -28,7 +28,7 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
in encodeUCoordinate o.
\end{lstlisting}
Where \coqe{montgomery_rec} is defined as follows:
In this definition \coqe{montgomery_rec} is defined as follows:
\begin{lstlisting}[language=Coq]
Fixpoint montgomery_rec (m : nat) (z : T')
......@@ -78,16 +78,19 @@ match m with
end.
\end{lstlisting}
The functions encoding and decoding of the byte array are detailed in
\ref{subsec:integer-bytes}.
RFC~7748 states \emph{``All calculations are performed in GF(p), i.e., they are performed modulo p.''}
Operations used in the Montgomery ladder of \coqe{RFC} are intentiated over
integers $Z$ (See Appendix~\ref{subsubsec:RFC-Coq}). The modulo reduction by $\p$
is deferred at the end with the \coqe{ZPack25519} operation.
We define $\Zfield$ as the field of integers where the modulo reduction by $\p$ is
deferred at the end of the computations.
We define $\Zfield$ as integers in which the modulo reduction by $\p$ is
deferred at the end to the computations.
We use this notation to emphasis its difference with $\Ffield$ where the
modulo by $\p$ is applied in each operations.
We first present a generic description of the Montgomery ladder (\ref{subsec:spec-ladder}).
We briefly introduce our generic description of the Montgomery ladder (\ref{subsec:spec-ladder}).
Then we describe our mapping between little-endian representations and integers
(\ref{subsec:integer-bytes}) which we use to formalize the encoding and decoding.
......@@ -103,11 +106,11 @@ TweetNaCl implements X25519 with numbers represented as arrays.
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.
Those types are later instantiated as list of integers, integers, natural
numbers, field elements.
The generic definition of the ladder (\coqe{montgomery_rec}) and its parallel with
the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}.
% The generic definition of the ladder (\coqe{montgomery_rec}) and its parallel with
% the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}.
Our formalization differs slightly from the RFC. Indeed in order to optimize the
number of calls to \texttt{CSWAP} the RFC uses an additional variable to decide
......@@ -132,7 +135,7 @@ in GF(p), i.e., they are performed modulo p.''}~\cite{rfc7748}
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.
represent that array as a list of integers in Coq.
We define the little-endian projection to integers as follows.
\begin{dfn}
......@@ -193,5 +196,5 @@ Definition encodeUCoordinate (x: Z) : list Z :=
ListofZ32 8 x.
\end{lstlisting}
Where \coqe{clamp} is taking care of setting and unsetting the selected bits
as per stated in the RFC.
In this definition, \coqe{clamp} is taking care of setting and unsetting the
selected bits as per stated in the RFC.
......@@ -451,14 +451,14 @@ To prove the correctness of the result we can use multiple strategies such as:
the resulting exponent is $2^{255}-21$.
\end{itemize}
We use the second method for the benefits of simplicity. However it requires to
apply the unrolling and exponentiation formulas 255 times. This can be automated
apply the unrolling and exponentiation formulas 255 times. This could be automated
in Coq with tacticals such as \Coqe{repeat}, but it generates a proof object which
will take a long time to verify.
\subheading{Speeding up with Reflections.} This technique provides us with
flexibility, \eg we don't need to know the number of times nor the order
in which the lemmas needs to be applied (chapter 15 in \cite{CpdtJFR}).
\subheading{Reflections.} In order to speed up the verification we use a
technique called ``Reflection''. It provides us with flexibility, \eg we don't
need to know the number of times nor the order in which the lemmas needs to be
applied (chapter 15 in \cite{CpdtJFR}).
The idea is to \emph{reflect} the goal into a decidable environment.
We show that for a property $P$, we can define a decidable Boolean property
......@@ -468,139 +468,11 @@ By applying $reify\_P$ on $P$ our goal become $P_{bool} = true$.
We then compute the result of $P_{bool}$. If the decision goes well we are
left with the tautology $true = true$.
To prove that the \Coqe{Inv25519_Z} is computing $x^{2^{255}-21}$,
we define a Domain Specific Language (DSL).
\begin{dfn}
Let \Coqe{expr_inv} denote an expression which is either a term;
a multiplication of expressions; a squaring of an expression or a power of an expression.
And Let \Coqe{formula_inv} denote an equality between two expressions.
\end{dfn}
\begin{lstlisting}[language=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.
Inductive formula_inv :=
| Eq_inv : expr_inv -> expr_inv -> formula_inv.
\end{lstlisting}
The denote functions are defined as follows:
\begin{lstlisting}[language=Coq]
Fixpoint e_inv_denote (m:expr_inv) : Z :=
match m with
| R_inv =>
term_denote
| M_inv x y =>
(e_inv_denote x) * (e_inv_denote y)
| S_inv x =>
(e_inv_denote x) * (e_inv_denote x)
| P_inv x p =>
pow (e_inv_denote x) (Z.pos p)
end.
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{lstlisting}
All denote functions also take as an argument the environment containing the variables.
We do not show it here for the sake of readability,
given that an environment, \Coqe{term_denote} returns the appropriate variable.
With this Domain Specific Language we have the following equality:
\begin{lstlisting}[backgroundcolor=\color{white}]
f_inv_denote
(Eq_inv (M_inv R_inv (S_inv R_inv))
(P_inv R_inv 3))
= (x * x^2 = x^3)
\end{lstlisting}
On the right side, \Coqe{(x * x^2 = x^3)} depends on $x$. On the left side,
\texttt{(Eq\_inv (M\_inv R\_inv (S\_inv R\_inv)) (P\_inv R\_inv 3))} does not depend on $x$.
This allows us to use computations in our decision procedure.
We define \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 DSL and
we prove their equality.
\begin{lstlisting}[language=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).
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{lstlisting}
We then derive the following lemma.
With this technique we prove the functional correctness of the inversion over \Zfield.
\begin{lemma}
\label{lemma:reify}
With an appropriate choice of variables, \Coqe{pow_inv} denotes \Coqe{Inv25519_Z}.
\end{lemma}
In order to prove formulas in \Coqe{formula_inv},
we have the following a decidable procedure.
We define \Coqe{pow_expr_inv}, a function which returns the power of an expression.
We then compare the two values and decide over their equality.
\begin{lstlisting}[language=Coq]
Fixpoint pow_expr_inv (t:expr_inv) : Z :=
match t with
(* power of a term is 1. *)
| R_inv => 1
(* x^a * x^b = x^{a+b}. *)
| M_inv x y =>
(pow_expr_inv x) + (pow_expr_inv y)
(* (x^a)^2 = x^{2a}. *)
| S_inv x =>
2 * (pow_expr_inv x)
(* (x^b)^a = x^{a*b}. *)
| P_inv x p =>
(Z.pos p) * (pow_expr_inv x)
end.
Definition decide_e_inv (l1 l2:expr_inv) : bool :=
(pow_expr_inv l1) ==? (pow_expr_inv l2).
Definition decide_f_inv (f:formula_inv) : bool :=
match f with
| Eq_inv x y => decide_e_inv x y
end.
\end{lstlisting}
We prove our decision procedure correct.
\begin{lemma}
\label{lemma:decide}
For all formulas $f$, if the decision over $f$ returns \Coqe{true},
then the denoted equality by $f$ is true.
\end{lemma}
Which is formalized as:
\begin{lstlisting}[language=Coq]
Lemma decide_formula_inv_impl :
forall (f:formula_inv),
decide_f_inv f = true ->
f_inv_denote f.
\end{lstlisting}
By reification to over DSL (\lref{lemma:reify}) and by applying our decision
(\lref{lemma:decide}), we prove the following corollary.
\begin{lemma}
\label{lemma:inv_comput_inv}
\Coqe{Inv25519_Z} computes an inverse in \Zfield.
\end{lemma}
Which is formalized as:
\begin{lstlisting}[language=Coq]
Theorem Inv25519_Z_correct :
forall (x:Z),
Inv25519_Z x = pow x (2^255-21).
\end{lstlisting}
% 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.
\begin{corollary}
\label{cor:inv_comput_field}
\Coqe{Inv25519} computes an inverse in \Zfield.
\end{corollary}
\end{lemma}
Which is formalized as:
\begin{lstlisting}[language=Coq]
Corollary Inv25519_Zpow_GF :
......@@ -610,10 +482,11 @@ Corollary Inv25519_Zpow_GF :
(pow (Z16.lst g) (2^255-21)) :GF.
\end{lstlisting}
\subheading{Another applications of reflections: packing}
This reflection technique can also be used where proofs requires some computing
over a small and finite domain of variables to test e.g. for all $i$ such that $0 \le i < 16$.
Using reflection we prove that we can split the for loop in \TNaCle{pack25519} into two parts.
This reflection technique is also used where proofs requires some computing
over a small and finite domain of variables to test e.g. for all $i$ such that
$0 \le i < 16$.
Using reflection we prove that we can split the for loop in \TNaCle{pack25519}
into two parts.
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
......@@ -632,9 +505,11 @@ for(i=1;i<15;i++) {
}
\end{lstlisting}
This loop separation allows simpler proofs. The first loop is seen as the subtraction of a number in \Zfield.
We then prove that with the iteration of the second loop, the number represented in $\Zfield$ stays the same.
This leads to the proof that \TNaCle{pack25519} is effectively reducing modulo $\p$ and returning a number in base $2^8$.
This loop separation allows simpler proofs. The first loop is seen as the
subtraction of a number in \Zfield. We then prove that with the iteration of the
second loop, the number represented in $\Zfield$ stays the same. This leads to
the proof that \TNaCle{pack25519} is effectively reducing modulo $\p$ and
returning a number in base $2^8$.
\begin{lstlisting}[language=Coq]
Lemma Pack25519_mod_25519 :
forall (l:list Z),
......
......@@ -5,7 +5,7 @@ In this section we prove the following informal theorem:
\begin{informaltheorem}
The implementation of X25519 in TweetNaCl computes the
$\F{p}$-restricted $x$-coordinate scalar multiplication on $E(\F{p^2})$ where $p$ is $\p$
$\F{p}$-restricted \xcoord 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}
......@@ -217,7 +217,7 @@ $a^2-4$ is not a square in \K.
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 $x$-coordinate of points on a curve.
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$.\\
......@@ -270,7 +270,8 @@ we can define a ladder similar to the one used in TweetNaCl (See \aref{alg:montg
\begin{algorithmic}
\REQUIRE{$x \in \K\backslash \{0\}$, scalars $n$ and $m$, $n < 2^m$}
\ENSURE{$a/c = \chi_0(n \cdot P)$ for any $P$ such that $\chi_0(P) = x$}
\STATE $(a,b,c,d) \leftarrow (1,x,0,1)$
\STATE $(a,c) \leftarrow (1,0)$ ~~~~~~~~~~~~~~~{\color{gray}\textit{$\chi_0(\Oinf) = (1:0)$}}
\STATE $(b,d) \leftarrow (x,1)$ ~~~~~~~~~~~~~~~{\color{gray}\textit{$\chi_0(P) = (x:1)$}}
\FOR{$k$ := $m$ downto $1$}
\IF{$k^{\text{th}}$ bit of $n$ is $1$}
\STATE $(a,b) \leftarrow (b,a)$
......@@ -426,7 +427,7 @@ we can find a $y$ such that $(x,y)$ is either on the curve or on the quadratic t
\begin{lemma}
\label{lemma:curve-or-twist}
For all $x \in \F{p}$, there exists a point $P$ over $M_{486662,1}(\F{p})$ or
over $M_{486662,2}(\F{p})$ such that the $x$-coordinate of $P$ is $x$.
over $M_{486662,2}(\F{p})$ such that the \xcoord of $P$ is $x$.
\end{lemma}
\begin{lstlisting}[language=Coq]
Theorem x_is_on_curve_or_twist:
......@@ -478,6 +479,9 @@ Similarly as in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_rin
\label{lemma:Zmodp2_ring}
$\F{p^2}$ is a commutative ring.
\end{lemma}
%% TOO LONG
%% If need remove this paragraph
We can then specialize the basic operations in order to speed up the verification
of formulas by using rewrite rules:
\begin{align*}
......@@ -489,6 +493,10 @@ of formulas by using rewrite rules:
(0, a)\cdot (0,b) &= (2\cdot a\cdot b, 0)\\
(0,a)^{-1} &= ((2\cdot a)^{-1},0)
\end{align*}
The injection $a \mapsto (a,0)$ from $\F{p}$ to $\F{p^2}$ preserves
$0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusions.
......@@ -561,6 +569,6 @@ Theorem curve25519_Fp2_ladder_ok:
We then prove the equivalence between of operations in $\Ffield$ and $\Zfield$,
in other words between \coqe{Zmodp} and \coqe{:GF}.
This allows us to show that given a clamped value $n$ and normalized $x$-coordinate of $P$,
This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$,
\coqe{RFC} gives the same results as $Curve25519\_Fp$.
This proves the correctness of TweetNaCl's X25519 and RFC~7748.
......@@ -11,7 +11,7 @@ proving an inconsistency.
In our case we rely on:
\begin{itemize}
\item \textbf{Calculus of Inductive Construction}. The intuitionistic logic
\item \textbf{Calculus of Inductive Constructions}. The intuitionistic logic
used by Coq must be consistent in order to trust the proofs. As an axiom,
we assumed that the functional extensionality, which is also consistent with that logic.
$$\forall x, f(x) = g(x) \implies f = g$$
......@@ -82,5 +82,5 @@ We first formalized X25519 from RFC~7748~\cite{rfc7748} in Coq. Then we proved
that TweetNaCl's implementation of X25519 matches our formalization.
In a second step we extended the Coq library for elliptic curves \cite{BartziaS14}
by Bartzia and Strub to support Montgomery curves. Using this extension we
proved that the X25519 from the RFC and its implementation in TweetNaCl matches
proved that the X25519 from the RFC and therefore its implementation in TweetNaCl matches
the mathematical definitions as given in~\cite[Sec.~2]{Ber06}.
......@@ -203,3 +203,6 @@
\newcommand{\p}{\ensuremath{2^{255}-19}}
\newcommand{\Zfield}{\ensuremath{\mathbb{Z}_{\p}}}