Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coqveriftweetnacl
Commits
2406eb00
Commit
2406eb00
authored
Oct 02, 2020
by
benoit
Browse files
minor
parent
756d8f98
Changes
5
Hide whitespace changes
Inline
Sidebyside
paper/highlevel.tex
View file @
2406eb00
...
...
@@ 37,7 +37,8 @@ with it in the proofs (\ref{subsec:curvep2}).
correctness. The white tiles are definitions, the orange ones are hypothesis and
the green tiles represent major lemmas and theorems.
The plan is as follows.
% The plan is as follows.
% (This is part of the description of the picture).
We consider the field
$
\K
$
and 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 commutative group.
...
...
@@ 51,6 +52,9 @@ $a^2  4$ is not a square in $\K$, we prove the correctness of the ladder (\tref
\label
{
tikz:ProofHighLevel1
}
\end{figure}
% this is for the flow of the text otherwise someone will again complain of a definition poping out of nowhere.
We now turn our attention to the details of the proof of the ladder's correctness.
\begin{dfn}
Given a field
$
\K
$
,
using an appropriate choice of coordinates,
...
...
@@ 79,8 +83,8 @@ Then, this equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.
In this setting, Bartzia and Strub defined the parametric type
\texttt
{
ec
}
which
represents the points on a specific curve. It is parameterized by
a
\texttt
{
K : ecuFieldType
}
,
the type of fields whose characteristic is neither 2 nor 3
,
and
\texttt
{
E : ecuType
}
,
a record that packs the curve parameters
$
a
$
and
$
b
$
a
\texttt
{
K : ecuFieldType
}

the type of fields whose characteristic is neither 2 nor 3

and
\texttt
{
E : ecuType
}

a record that packs the curve parameters
$
a
$
and
$
b
$

along with the proof that
$
\Delta
(
a,b
)
\neq
0
$
.
\begin{lstlisting}
[language=Coq]
Inductive point := EC
_
Inf  EC
_
In of K * K.
...
...
@@ 96,16 +100,12 @@ Definition oncurve (p : point) :=
Inductive ec : Type := EC p of oncurve p.
\end{lstlisting}
Points on an elliptic curve form an
commutative
group when equipped with the following structure.
Points on an elliptic curve form an
abelian
group when equipped with the following structure.
%
\begin{itemize}
\item
The negation of a point
$
P
=
(
x,y
)
$
is defined by reflection over the
$
x
$
axis,
\ie
$

P
=
(
x,

y
)
$
.
\item
The addition of two points
$
P, Q
\in
E
_{
a,b
}
(
\K
)
\setminus
\{\Oinf\}
$
with
$
P
\neq
Q
$
and
$
P
\neq

Q
$
is defined as the negation of the third intersection point of the line through
$
P
$
and
$
Q
$
.
In case
$
P
=
Q
$
, we either use the line tangent to
$
P
$
if
$
P
$
is not an inflection point,
and define
$
P
+
Q
=

P
=

Q
$
otherwise.
In case
$
P
=

Q
$
, we define
$
P
+
Q
=
\Oinf
$
.
\item
The point
$
\Oinf
$
acts as the neutral element. Hence, we define
$

\Oinf
=
\Oinf
$
,
$
P
+
\Oinf
=
P
$
and
$
\Oinf
+
P
=
P
$
.
\item
The addition of two points
$
P
$
and
$
Q
$
is defined as the negation of the third intersection point
of the line passing through
$
P
$
and
$
Q
$
, or tangent to
$
P
$
if
$
P
=
Q
$
.
\item
$
\Oinf
$
is the neutral element under this law: if 3 points are collinear, their sum is equal to
$
\Oinf
$
\end{itemize}
These operations are defined in Coq as follows (where we omit the code for the tangent case):
\begin{lstlisting}
[language=Coq]
...
...
@@ 147,8 +147,8 @@ than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySp
Similar to the definition of
\texttt
{
ec
}
, we define the parametric type
\texttt
{
mc
}
which
represents the points on a specific Montgomery curve.
It is parameterized by
a
\texttt
{
K : ecuFieldType
}
,
the type of fields whose characteristic is neither
2 nor 3
,
and
\texttt
{
M : mcuType
}
,
a record that packs the curve
a
\texttt
{
K : ecuFieldType
}

the type of fields whose characteristic is neither
2 nor 3

and
\texttt
{
M : mcuType
}

a record that packs the curve
parameters
$
a
$
and
$
b
$
along with the proofs that
$
b
\neq
0
$
and
$
a
^
2
\neq
4
$
.
\begin{lstlisting}
[language=Coq,belowskip=0.1
\baselineskip
]
Record mcuType :=
...
...
@@ 177,7 +177,7 @@ Definition add (p1 p2 : point K) :=
( xs,  s * (xs  x1)  y1 )
end.
\end{lstlisting}
And again we prove the result is on the curve:
% (again with coercion):
And again we prove the result is on the curve:
\begin{lstlisting}
[language=Coq]
Lemma addO (p q : mc) : oncurve (add p q).
...
...
@@ 185,21 +185,19 @@ Definition addmc (p1 p2 : mc) : mc :=
MC p1 p2 (addO p1 p2)
\end{lstlisting}
Remarkably, of all the group properties, associativity is the hardest one to prove for elliptic curves.
Instead of reproving this property for Montgomery curves, we transfer it from the Weierstra
{
\ss
}
curves
with a trick.
We define a bijection between a Montgomery curve and its short Weierstra
{
\ss
}
form
(as in
\lref
{
lemma:bijecc
}
)
and prove that it respects the addition as defined on the respective curves.
It is then easy to verify all the group laws for Montgomery curves from the Weierstra
{
\ss
}
ones.
(
\lref
{
lemma:bijecc
}
) and prove that it respects the addition as defined on the
respective curves. In this way we get all the group laws for Montgomery curves from the Weierstra
{
\ss
}
ones.
After
we have
verified the group properties, it follows that the bijection is a group isomorphism.
After
having
verified the group properties, it follows that the bijection is a group isomorphism.
\begin{lemma}
\label
{
lemma:bijecc
}
Let
$
M
_{
a,b
}$
be a Montgomery curve, define
\vspace
{
0.3em
}
$$
a'
=
\frac
{
3

a
^
2
}{
3
b
^
2
}
\text
{
\ \ \ \
and
\ \ \ \
}
b'
=
\frac
{
2
a
^
3

9
a
}{
27
b
^
3
}
.
$$
then
$
E
_{
a',b'
}$
is a Weierstra
{
\ss
}
curve, and the mapping
$
\varphi
: M
_{
a,b
}
\to
E
_{
a',b'
}$
defined as:
then
$
E
_{
a',b'
}$
is a Weierstra
{
\ss
}
curve, and the mapping
$
\varphi
: M
_{
a,b
}
\mapsto
E
_{
a',b'
}$
defined as:
\vspace
{
0.5em
}
\begin{align*}
\varphi
(
\Oinf
_
M)
&
=
\Oinf
_
E
\\
\varphi
( (x , y) )
&
=
\left
(
\frac
{
x
}{
b
}
+
\frac
{
a
}{
3b
}
,
\frac
{
y
}{
b
}
\right
)
...
...
@@ 226,13 +224,13 @@ After we have verified the group properties, it follows that the bijection is a
\label
{
subsec:ECCprojective
}
In a projective plane, points are represented by the triples
$
(
X:Y:Z
)
$
excluding
$
(
0
:
0
:
0
)
$
.
Scalar multiples of triples are identified with eachother,
\ie
Scalar multiples of triples are identified with each
other,
\ie
for all
$
\lambda
\neq
0
$
, the triples
$
(
X:Y:Z
)
$
and
$
(
\lambda
X:
\lambda
Y:
\lambda
Z
)
$
represent
the same point in the projective plane.
For
$
Z
\neq
0
$
, the point
$
(
X:Y:Z
)
$
corresponds to the
point
$
(
X
/
Z,Y
/
Z
)
$
in the affine plane.
Likewise, the point
$
(
X,Y
)
$
in the affine plane corresponds to
$
(
X:Y:
1
)
$
in the projective plane.
The points
$
(
X : Y :
0
)
$
can be considered as points at infinity.
%
The points $(X : Y : 0)$ can be considered as points at infinity.
Using fractions as coordinates, the equation for a Montgomery curve
$
M
_{
a,b
}$
becomes
...
...
@@ 256,11 +254,12 @@ Hypothesis mcu_no_square :
We define
$
\chi
$
and
$
\chi
_
0
$
to return the
\xcoord
of points on a curve.
\begin{dfn}
Let
$
\chi
: M
_{
a,b
}
(
\K
)
\to
\K
\cup
\{\infty\}
$
and
$
\chi
_
0
: M
_{
a,b
}
(
\K
)
\to
\K
$
such that
\begin{align*}
\chi
((x,y))
&
= x,
&
\chi
(
\Oinf
)
&
=
\infty
,
&&
\text
{
and
}
\\
\chi
_
0((x,y))
&
= x,
&
\chi
_
0(
\Oinf
)
&
= 0.
\end{align*}
Let
$
\chi
: M
_{
a,b
}
(
\K
)
\mapsto
\K
\cup
\{\infty\}
$
and
$
\chi
_
0
: M
_{
a,b
}
(
\K
)
\mapsto
\K
$
such that
\vspace
{
0.5em
}
\begin{align*}
\chi
((x,y))
&
= x,
&
\chi
(
\Oinf
)
&
=
\infty
,
&
&
\text
{
and
}
\\
[0.5ex]
\chi
_
0((x,y))
&
= x,
&
\chi
_
0(
\Oinf
)
&
= 0.
\end{align*}
\end{dfn}
Using projective coordinates we prove the formula for differential addition.
% (\lref{lemma:xADD}).
...
...
@@ 270,9 +269,10 @@ Using projective coordinates we prove the formula for differential addition.% (\
let
$
X
_
1
, Z
_
1
, X
_
2
, Z
_
2
, X
_
4
, Z
_
4
\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
\vspace
{
0.5em
}
\begin{align*}
X
_
3
&
= Z
_
4((X
_
1  Z
_
1)(X
_
2+Z
_
2) + (X
_
1+Z
_
1)(X
_
2Z
_
2))
^
2
\\
Z
_
3
&
= X
_
4((X
_
1  Z
_
1)(X
_
2+Z
_
2)  (X
_
1+Z
_
1)(X
_
2Z
_
2))
^
2
,
X
_
3
&
= Z
_
4((X
_
1  Z
_
1)(X
_
2+Z
_
2) + (X
_
1+Z
_
1)(X
_
2Z
_
2))
^
2
\\
[0.5ex]
Z
_
3
&
= X
_
4((X
_
1  Z
_
1)(X
_
2+Z
_
2)  (X
_
1+Z
_
1)(X
_
2Z
_
2))
^
2
\end{align*}
then for any point
$
P
_
1
$
and
$
P
_
2
$
in
$
M
_{
a,b
}
(
\K
)
$
such that
$
X
_
1
/
Z
_
1
=
\chi
(
P
_
1
)
, X
_
2
/
Z
_
2
=
\chi
(
P
_
2
)
$
, and
$
X
_
4
/
Z
_
4
=
\chi
(
P
_
1

P
_
2
)
$
,
...
...
@@ 550,8 +550,7 @@ We now study the case of the scalar multiplication and show similar proofs.
such that
$
\varphi
((
x,y
))
=
((
x,
0
)
,
(
y,
0
))
$
.
\item
[]
$
\varphi
_
t: M
_{
486662
,
2
}
(
\F
{
p
}
)
\mapsto
M
_{
486662
,
1
}
(
\F
{
p
^
2
}
)
$
\\
such that
$
\varphi
((
x,y
))
=
((
x,
0
)
,
(
0
,y
))
$
.
\item
[]
$
\psi
:
\F
{
p
^
2
}
\mapsto
\F
{
p
}$
\\
such that
$
\psi
(
x,y
)
=
x
$
.
\item
[]
$
\psi
:
\F
{
p
^
2
}
\mapsto
\F
{
p
}$
such that
$
\psi
(
x,y
)
=
x
$
.
\end{itemize}
\end{dfn}
...
...
@@ 559,15 +558,17 @@ We now study the case of the scalar multiplication and show similar proofs.
\label
{
lemma:proj
}
For all
$
n
\in
\N
$
, for all point
$
P
\in\F
{
p
}
\times\F
{
p
}$
on the curve
$
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
(respectively on the quadratic twist
$
M
_{
486662
,
2
}
(
\F
{
p
}
)
$
), we have
\vspace
{
0.3em
}
\begin{align*}
P
&
\in
M
_{
486662,1
}
(
\F
{
p
}
)
&
\implies
\varphi
_
c(n
\cdot
P)
&
= n
\cdot
\varphi
_
c(P),
&
&
\text
{
and
}
\\
P
&
\in
M
_{
486662,2
}
(
\F
{
p
}
)
&
\implies
\varphi
_
t(n
\cdot
P)
&
= n
\cdot
\varphi
_
t(P).
P
&
\in
M
_{
486662,1
}
(
\F
{
p
}
)
&
\implies
\varphi
_
c(n
\cdot
P)
&
= n
\cdot
\varphi
_
c(P),
&
&
\text
{
and
}
\\
P
&
\in
M
_{
486662,2
}
(
\F
{
p
}
)
&
\implies
\varphi
_
t(n
\cdot
P)
&
= n
\cdot
\varphi
_
t(P).
\end{align*}
\end{lemma}
Notice that
\vspace
{
0.5em
}
\begin{align*}
\forall
P
\in
M
_{
486662,1
}
(
\F
{
p
}
),
&
&
\psi
(
\chi
_
0(
\varphi
_
c(P)))
&
=
\chi
_
0(P),
&
&
\text
{
and
}
\\
\forall
P
\in
M
_{
486662,2
}
(
\F
{
p
}
),
&
&
\psi
(
\chi
_
0(
\varphi
_
t(P)))
&
=
\chi
_
0(P).
\forall
P
\in
M
_{
486662,1
}
(
\F
{
p
}
),
&
&
\psi
(
\chi
_
0(
\varphi
_
c(P)))
&
=
\chi
_
0(P),
&
&
\text
{
and
}
\\
\forall
P
\in
M
_{
486662,2
}
(
\F
{
p
}
),
&
&
\psi
(
\chi
_
0(
\varphi
_
t(P)))
&
=
\chi
_
0(P).
\end{align*}
In summary, for all
$
n
\in
\N
$
,
$
n <
2
^{
255
}$
, for any point
$
P
\in\F
{
p
}
\times\F
{
p
}$
...
...
paper/lowlevel.tex
View file @
2406eb00
...
...
@@ 244,7 +244,7 @@ the same time.
\label
{
subsec:numreprrfc
}
As described in
\sref
{
subsec:NumberTweetNaCl
}
, numbers in
\TNaCle
{
gf
}
(
typedef of an
array of 16
\TNaCle
{
long long
}
) are represented
(array of 16
\TNaCle
{
long long
}
) are represented
in
$
2
^{
16
}$
and we use a direct mapping to represent that array as a list
integers in Coq. However, in order to show the correctness of the basic operations,
we need to convert this number to an integer.
...
...
@@ 273,8 +273,7 @@ Lemma mult_GF_Zlength :
forall (a:list Z) (b:list Z),
Zlength a = 16 >
Zlength b = 16 >
(Z16.lst (Low.M a b)) :GF =
(Z16.lst a * Z16.lst b) :GF.
(Z16.lst (Low.M a b)):GF = (Z16.lst a * Z16.lst b):GF.
\end{lstlisting}
However for our purpose, simple functional correctness is not enough.
...
...
paper/preliminaries.tex
View file @
2406eb00
...
...
@@ 51,9 +51,9 @@ We define the operation:
&
((X
_{
2
\cdot
P
}
:Z
_{
2
\cdot
P
}
), (X
_{
P + Q
}
:Z
_{
P + Q
}
))
\end{align*}
A pseudocode description of the Montgomery ladder
A pseudocode description of the Montgomery ladder
is given in Algorithm~
\ref
{
alg:montgomeryladder
}
.
The main loop iterates over the bits of the scalar
$
n
$
.
The main loop iterates over the bits of the scalar
$
n
$
.
The
$
k
^{
\text
{
th
}}$
iteration conditionally swaps
the arguments
$
P
$
and
$
Q
$
of
\texttt
{
xDBL
\&
ADD
}
depending on the value of the
$
k
^{
\text
{
th
}}$
bit of
$
n
$
.
...
...
@@ 64,6 +64,8 @@ $(P_b, P_{1b})$.
By using the differential addition and doubling operations we define the Montgomery ladder
computing a
\xcoord
only scalar multiplication (see
\aref
{
alg:montgomeryladder
}
).
% \setlength{\textfloatsep}{1em}
\begin{algorithm}
\caption
{
Montgomery ladder for scalar mult.
}
\label
{
alg:montgomeryladder
}
...
...
@@ 83,7 +85,6 @@ computing a \xcoordonly scalar multiplication (see \aref{alg:montgomeryladder}
\end{algorithmic}
\end{algorithm}
\subsection
{
The X25519 key exchange
}
\label
{
subsec:X25519keyexchange
}
...
...
paper/proofs.tex
View file @
2406eb00
\section
{
Organization of the proof files
}
\label
{
appendix:prooffolders
}
\subheading
{
Requirements
}
\subheading
{
Requirements
.
}
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 compatibility we decided to freeze our dependencies.
\subheading
{
Associated files
}
The
archive
containing the proof is composed of two folders
\textbf
{
\texttt
{
packages
}}
\subheading
{
Associated files
.
}
The
repository
containing the proof is composed of two folders
\textbf
{
\texttt
{
packages
}}
and
\textbf
{
\texttt
{
proofs
}}
.
It aims to be used at the same time as an
\emph
{
opam
}
repository to manage
the dependencies of the proof and to provide the code.
...
...
@@ 26,38 +26,38 @@ and allows us to use the theorem of quadratic reciprocity.
In this folder the reader will find multiple levels of implementation of X25519.
\begin{itemize}
\item
\textbf
{
\texttt
{
Libs/
}}
contains basic libraries and tools to help use
reason with lists and decidable procedures.
reason with lists and decidable procedures.
\item
\textbf
{
\texttt
{
ListsOp/
}}
defines operators on list such as
\Coqe
{
ZofList
}
and related lemmas using
\eg
\VSTe
{
Forall
}
.
\Coqe
{
ZofList
}
and related lemmas using
\eg
\VSTe
{
Forall
}
.
\item
\textbf
{
\texttt
{
Gen/
}}
defines a generic Montgomery ladder which can be
instantiated with different operations. This ladder is the stub for the
following implementations.
instantiated with different operations. This ladder is the stub for the
following implementations.
\item
\textbf
{
\texttt
{
High/
}}
contains the theory of Montgomery curves,
twists, quadratic extensions and ladder.
It also proves the correctness of the ladder over
$
\F
{
\p
}$
.
twists, quadratic extensions and ladder.
It also proves the correctness of the ladder over
$
\F
{
\p
}$
.
\item
\textbf
{
\texttt
{
Mid/
}}
provides a listbased implementation of the
basic operations
\TNaCle
{
A
}
,
\TNaCle
{
Z
}
,
\TNaCle
{
M
}
\ldots
~and the ladder. It
makes the link with the theory of Montgomery curves.
basic operations
\TNaCle
{
A
}
,
\TNaCle
{
Z
}
,
\TNaCle
{
M
}
\ldots
~and the ladder. It
makes the link with the theory of Montgomery curves.
\item
\textbf
{
\texttt
{
Low/
}}
provides a second listbased implementation of
the basic operations
\TNaCle
{
A
}
,
\TNaCle
{
Z
}
,
\TNaCle
{
M
}
\ldots
~and the ladder.
Those functions are proven to provide the same results as the ones in
\texttt
{
Mid/
}
, however their implementation are closer to
\texttt
{
C
}
in order
facilitate the proof of equivalence with TweetNaCl code.
the basic operations
\TNaCle
{
A
}
,
\TNaCle
{
Z
}
,
\TNaCle
{
M
}
\ldots
~and the ladder.
Those functions are proven to provide the same results as the ones in
\texttt
{
Mid/
}
, however their implementation are closer to
\texttt
{
C
}
in order
facilitate the proof of equivalence with TweetNaCl code.
\item
\textbf
{
\texttt
{
rfc/
}}
provides our rfc formalization.
It uses integers for the basic operations
\TNaCle
{
A
}
,
\TNaCle
{
Z
}
,
\TNaCle
{
M
}
\ldots
and the ladder. It specifies the decoding/encoding of/to byte
arrays (seen as list of integers) as in RFC~7748.
It uses integers for the basic operations
\TNaCle
{
A
}
,
\TNaCle
{
Z
}
,
\TNaCle
{
M
}
\ldots
and the ladder. It specifies the decoding/encoding of/to byte
arrays (seen as list of integers) as in RFC~7748.
\end{itemize}
\subheading
{
\texttt
{
proofs/vst/
}}
Here the reader will find four folders.
\begin{itemize}
\item
\textbf
{
\texttt
{
c
}}
contains the C Verifiable implementation of TweetNaCl.
\texttt
{
clightgen
}
will generate the appropriate translation into Clight.
\texttt
{
clightgen
}
will generate the appropriate translation into Clight.
\item
\textbf
{
\texttt
{
init
}}
contains basic lemmas and memory manipulation
shortcuts to handle the aliasing cases.
shortcuts to handle the aliasing cases.
\item
\textbf
{
\texttt
{
spec
}}
defines as Hoare triple the specification of the
functions used in
\TNaCle
{
crypto
_
scalarmult
}
.
functions used in
\TNaCle
{
crypto
_
scalarmult
}
.
\item
\textbf
{
\texttt
{
proofs
}}
contains the proofs of the above Hoare triples
and thus the proof that TweetNaCl code is sound and correct.
and thus the proof that TweetNaCl code is sound and correct.
\end{itemize}
paper/rfc.tex
View file @
2406eb00
...
...
@@ 119,7 +119,7 @@ Fixpoint ZofList {n:Z} (a:list Z) : Z :=
 h :: q => h + 2
^
n * ZofList q
end.
\end{lstlisting}
The encoding from integers to bytes is defined in a similar way
:
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 littleendian encoding as a list with radix
$
2
^
n
$
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment