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
e15af18b
Commit
e15af18b
authored
Sep 20, 2019
by
Benoit Viguier
Browse files
more text
parent
9201b098
Changes
14
Hide whitespace changes
Inline
Sidebyside
paper/1_intro.tex
View file @
e15af18b
...
...
@@ 27,9 +27,12 @@ We make use of this updated terminology in this paper.
\subheading
{
Contribution of this paper
}
We provide a mechanized formal proof of the correctness of the X25519
implementation in TweetNaCl.
This proof is done in two steps:
We first prove equivalence of the C implementation of X25519
to an implementation in Coq~
\cite
{
coqfaq
}
.
This proof is done in three steps:
we first formalize RFC~7748~
\cite
{
rfc7748
}
in Coq~
\cite
{
coqfaq
}
.
% This part uses generic techniques to facilitate later proofs.
In a second step we prove equivalence of the C implementation of X25519
to our RFC formalization.
This part of the proof uses the Verifiable Software Toolchain (VST)~
\cite
{
2012Appel
}
to establish a link between C and Coq.
VST uses Separation logic~
\cite
{
1969Hoare,Reynolds02separationlogic
}
...
...
@@ 38,7 +41,7 @@ To the best of our knowledge, this is the first time that
VST is used in the formal proof of correctness of an implementation
of an asymmetric cryptographic primitive.
In a
second
step we prove that the Coq implementation matches
In a
last
step we prove that the Coq implementation matches
the mathematical definition of X25519 as given in~
\cite
[Sec.~2]
{
Ber06
}
.
We accomplish this step of the proof by extending the Coq library
for elliptic curves~
\cite
{
BartziaS14
}
by Bartzia and Strub to
...
...
@@ 83,8 +86,14 @@ the theory of elliptic curves.
\subheading
{
Reproducing the proofs.
}
To maximize reusability of our results we placed the code of our formal proof
presented in this paper into the public domain. They are available at XXXXXXX
presented in this paper into the public domain.
\ifpublic
They are available at XXXXXXX
with instructions of how to compile and verify our proof.
\else
They are available in the associated materials with instructions of how
to compile and verify our proof.
\fi
A description of the content of the archive is provided in
Appendix~
\ref
{
appendix:prooffolders
}
.
...
...
@@ 92,12 +101,20 @@ Appendix~\ref{appendix:prooffolders}.
\sref
{
sec:preliminaries
}
give the necessary background on Curve25519 and X25519
implementations and a brief explanation of how formal verification works.
\sref
{
sec:CoqRFC
}
provides our formalization of RFC~7748~
\cite
{
rfc7748
}
's X25519.
\sref
{
sec:CCoq
}
provides the specification of TweetNaCl's X25519 and some of the
\sref
{
sec:CCoq
}
provides the specification
s
of TweetNaCl's X25519 and some of the
proofs techniques used to show the correctness with respect to RFC~7748~
\cite
{
rfc7748
}
.
\sref
{
sec:maths
}
describes our extension of the formal library by Bartzia
and Strub and the correctness of X25519 implementation with respect to Bernstein's
specifications~
\cite
{
Ber14
}
.
And lastly in
\sref
{
sec:Conclusion
}
we discuss the trusted code base of this proof.
\fref
{
tikz:ProofOverview
}
shows a graph of dependencies of the proofs.
\begin{figure}
[h]
\centering
\include
{
tikz/proof
}
\caption
{
Structure of the proof
}
\label
{
tikz:ProofOverview
}
\end{figure}
% Five years ago:
...
...
paper/2_preliminaries.tex
View file @
e15af18b
...
...
@@ 89,14 +89,15 @@ 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
$
.
Given
$
n
\in
\N
$
and
$
x
\in
\F
{
\p
}
$
, such that
$
x
$
is the
$
x
$
coordinate of
a point
$
P
$
of
$
E
(
\F
{
\
p
}
)
$
, X25519 returns the
$
x
$
coordinate of the
Given
$
n
\in
\N
$
and
$
x
\in
\F
field
$
, 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
$
.
% 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 32bytes:
\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
% 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
to
\texttt
{
0
}
; bit 254 to
\texttt
{
1
}
and the lower 3 bits to
\texttt
{
0
}
,
...
...
@@ 168,10 +169,10 @@ sv unpack25519(gf o, const u8 *n)
\end{lstlisting}
The radix
$
2
^{
16
}$
representation in limbs of
$
64
$
bits is
highly redundant; for any element
$
A
\in
\F
{
\p
}
$
there are
highly redundant; for any element
$
A
\in
\F
field
$
there are
multiple ways to represent
$
A
$
as
$
(
a
_
0
,
\dots
,a
_{
15
}
)
$
.
This is used to avoid carry handling in the implementations of addition
(
\TNaCle
{
A
}
) and subtraction (
\TNaCle
{
Z
}
) in
$
\F
{
\p
}
$
:
(
\TNaCle
{
A
}
) and subtraction (
\TNaCle
{
Z
}
) in
$
\F
field
$
:
\begin{lstlisting}
[language=Ctweetnacl]
sv A(gf o,const gf a,const gf b)
{
int i;
...
...
@@ 215,7 +216,7 @@ 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
$
\
Z
field
$
are computed with
\TNaCle
{
inv25519
}
.
Inverses in
$
\
F
field
$
are computed with
\TNaCle
{
inv25519
}
.
It takes the exponentiation by
$
2
^{
255
}

21
$
with the squareandmultiply algorithm.
Fermat's little theorem gives the correctness.
Notice that in this case the inverse of
$
0
$
is defined as
$
0
$
.
...
...
@@ 277,7 +278,7 @@ 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
$
x
$
coordinates 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
$
.
...
...
paper/3_RFC.tex
View file @
e15af18b
...
...
@@ 28,19 +28,76 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
in encodeUCoordinate o.
\end{lstlisting}
Where
\coqe
{
montgomery
_
rec
}
is defined as follows:
\begin{lstlisting}
[language=Coq]
Fixpoint montgomery
_
rec (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
(* a: x2 *)
(* b: x3 *)
(* c: z2 *)
(* d: z3 *)
(* e: temporary var *)
(* f: temporary var *)
(* x: x1 *)
(T * T * T * T * T * T) :=
match m with
 0
%nat => (a,b,c,d,e,f)
 S n =>
let r := Getbit (Z.of
_
nat n) z in
(* k
_
t = (k >> t)
&
1 *)
(* swap < k
_
t *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x
_
2, x
_
3) = cswap(swap, x
_
2, x
_
3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r 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 *)
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 *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x
_
2, x
_
3) = cswap(swap, x
_
2, x
_
3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z
_
2, z
_
3) = cswap(swap, z
_
2, z
_
3) *)
montgomery
_
rec n z a b c d e f x
end.
\end{lstlisting}
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:RFCCoq
}
). 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.
This aims to formalize 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:specladder
}
).
Then we describe our mapping between littleendian representations and integers
(
\ref
{
subsec:integerbytes
}
) which we use to formalize the encoding and decoding.
We then turn our attention to the last steps of the computation
(
\ref
{
subsec:specunpackclampinvpack
}
).
% subsection or subheading ?
\subsection
{
A generic ladder
}
\label
{
subsec:specladder
}
% \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. We show the equivalence between
...
...
@@ 53,7 +110,7 @@ The generic definition of the ladder (\coqe{montgomery_rec}) and its parallel wi
the definition of RFC~7748 are provided in Appendix~
\ref
{
subsubsec:coqladder
}
.
Our formalization differs slightly from the RFC. Indeed in order to optimize the
number of
\texttt
{
CSWAP
}
calls
the RFC uses an additional variable to decide
number of
calls to
\texttt
{
CSWAP
}
the RFC uses an additional variable to decide
whether a conditionnal swap is required or not. Our description of the ladder
follows strictly the shape of the exponent as described in
\aref
{
alg:montgomeryladder
}
.
This divergence is allowed by the RFC:
...
...
@@ 73,13 +130,9 @@ 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:RFCCoq
}
). The modulo reduction by
$
\p
$
is done at the end with the
\coqe
{
ZPack25519
}
operation.
In TweetNaCl, as described in
\sref
{
subsec:NumberTweetNaCl
}
, 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.
In TweetNaCl, as described in
\sref
{
subsec:NumberTweetNaCl
}
, 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 littleendian projection to integers as follows.
\begin{dfn}
...
...
@@ 125,7 +178,8 @@ Lemma ListofZ32_ZofList_Zlength: forall (l:list Z),
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.
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 :=
...
...
@@ 139,14 +193,5 @@ Definition encodeUCoordinate (x: Z) : list Z :=
ListofZ32 8 x.
\end{lstlisting}
\subsection
{
Clamping, Inversion and Packing
}
\label
{
subsec:specunpackclampinvpack
}
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.
Where
\coqe
{
clamp
}
is taking care of setting and unsetting the selected bits
as per stated in the RFC.
paper/4_lowlevel.tex
View file @
e15af18b
...
...
@@ 5,13 +5,24 @@ In this section we prove the following theorem:
% In this section we outline the structure of our proofs of the following theorem:
\begin{informaltheorem}
\label
{
thm:VSTRFC
}
The implementation of X25519 in TweetNaCl (
\TNaCle
{
crypto
_
scalarmult
}
) matches
the specifications of RFC~7748~
\cite
{
rfc7748
}
(
\Coqe
{
RFC
}
)
the specifications of RFC~7748~
\cite
{
rfc7748
}
(
\Coqe
{
RFC
}
)
.
\end{informaltheorem}
More formally.
\todo
{
INSERT COQ DEFINITION HERE
}
More formally:
\begin{lstlisting}
[language=Coq]
Theorem body
_
crypto
_
scalarmult:
(* VST boiler plate. *)
semax
_
body
(* Clight translation of TweetNaCl. *)
Vprog
(* Hoare tripples for fct calls. *)
Gprog
(* fct we verify. *)
f
_
crypto
_
scalarmult
_
curve25519
_
tweet
(* Our Hoare tripple, see below. *)
crypto
_
scalarmult
_
spec.
\end{lstlisting}
We first describe the global structure of our proof (
\ref
{
subsec:proofstructure
}
).
Using our formalization of RFC~7748 (
\sref
{
sec:CoqRFC
}
) we specify the Hoare
...
...
@@ 30,15 +41,7 @@ used to in some of our more complex proofs (\ref{subsec:inversionsreflections})
In order to prove the correctness of X25519 in TweetNaCl code
\TNaCle
{
crypto
_
scalarmult
}
,
we use VST to prove that the code matches our functional Coq specification of
\Coqe
{
RFC
}
.
Then, we prove that our specification of the scalar multiplication matches the mathematical definition
of elliptic curves and Theorem 2.1 by Bernstein~
\cite
{
Ber06
}
(
\tref
{
thm:EllipticRFC
}
).
\fref
{
tikz:ProofOverview
}
shows a graph of dependencies of the proofs.
The mathematical proof of X25519 is presented in
\sref
{
sec:maths
}
.
\begin{figure}
[h]
\centering
\include
{
tikz/proof
}
\caption
{
Structure of the proof
}
\label
{
tikz:ProofOverview
}
\end{figure}
of elliptic curves and Theorem 2.1 by Bernstein~
\cite
{
Ber06
}
(
\sref
{
sec:maths
}
).
Verifying
\TNaCle
{
crypto
_
scalarmult
}
also implies verifying all the functions
subsequently called:
\TNaCle
{
unpack25519
}
;
\TNaCle
{
A
}
;
\TNaCle
{
Z
}
;
\TNaCle
{
M
}
;
...
...
@@ 54,26 +57,34 @@ We also prove that TweetNaCl's code is \textbf{correct}:
\begin{itemize}
\item
X25519 is correctly implemented (we get what we expect) .
\item
Operations on
\TNaCle
{
gf
}
(
\TNaCle
{
A
}
,
\TNaCle
{
Z
}
,
\TNaCle
{
M
}
,
\TNaCle
{
S
}
)
are equivalent to operations (
$
+
,

,
\times
,x
^
2
$
) in
\Zfield
.
are equivalent to operations (
$
+
,

,
\times
,x
^
2
$
) in
$
\Zfield
$
.
\item
The Montgomery ladder computes the multiple of a point.
% \item The Montgomery ladder computes a scalar multiplication between a natural
% number and a point.
\end{itemize}
In order to prove the soundness and correctness of
\TNaCle
{
crypto
_
scalarmult
}
,
we first create a skeleton of the Montgomery ladder with abstract operations which
can be instantiated over
\eg
lists, integers, field elements.
A high level specification (over a generic field
$
\K
$
) allows us to prove the
correctness of the ladder with respect to the theory of elliptic curves.
we reuse the generic Montgomery ladder defined in
\sref
{
sec:CoqRFC
}
.
We define a Highlevel specification by instantiating the ladder with a generic
field
$
\K
$
, this allows us to prove the correctness of the ladder with respect
to the theory of elliptic curves.
This highlevel specification does not rely on the parameters of Curve25519.
By instantiating
$
\K
$
with
$
\Zfield
$
, and the parameters of Curve25519 (
$
a
=
486662
, b
=
1
$
),
we define a midlevel specification.
We later specialize
$
\K
$
with
$
\Ffield
$
, and the parameters of Curve25519 (
$
a
=
486662
, b
=
1
$
),
to derive the correctness of
\coqe
{
RFC
}
(
\sref
{
sec:maths
}
).
We define a midlevel specification by instantiating the ladder over
$
\Zfield
$
.
Additionally we also provide a lowlevel specification close to the
\texttt
{
C
}
code
(over lists of
$
\Z
$
). We show this specification to be equivalent to the
\emph
{
semantic version
}
of C (Clight) using the VST.
This low level specification gives us the soundness assurance.
By showing that operations over instances (
$
\K
=
\Zfield
$
,
$
\Z
$
, list of
$
\Z
$
) are
equivalent, we bridge the gap between the low level and the high level specification
RFC~7748's X25519 formalization (
\sref
{
sec:CoqRFC
}
) takes as input list of
$
\Z
$
.
However the inner Montgomery ladder operates on
$
\Zfield
$
. We show its equivalence
with our midlevel and lowlevel specifications.
By showing that operations over instances (
$
\K
=
\Ffield
$
,
$
\Zfield
$
, list of
$
\Z
$
) are
equivalent, we bridge the gap between the different level of specification
with Curve25519 parameters.
As such, we prove all specifications to equivalent (
\fref
{
tikz:ProofStructure
}
).
This guarantees us the correctness of the implementation.
...
...
@@ 100,8 +111,8 @@ This guarantees us the correctness of the implementation.
\subsection
{
Applying the Verifiable Software Toolchain
}
\label
{
subsec:withVST
}
We now turn our focus to the specification of
the Hoare triple with our
specifica
tion
s
of
\TNaCle
{
crypto
_
scalarmult
}
over lists of integers
and prov
ing
We now turn our focus to the
formal
specification of
\TNaCle
{
crypto
_
scalarmult
}
.
We use our defini
tion of
X25519 from the RFC in the Hoare triple
and prov
e
its correctness.
\subheading
{
Specifications.
}
...
...
@@ 181,14 +192,14 @@ As Postcondition we have:
We show that the computation for
\VSTe
{
RFC
}
fits in
\TNaCle
{
u8[32]
}
.
\end{itemize}
This specification shows that
\TNaCle
{
crypto
_
scalarmult
}
in C
computes the same
result as
\VSTe
{
RFC
}
in Coq provided that inputs are within
their respective
bounds: arrays of 32 bytes.
This specification
(proven with VST)
shows that
\TNaCle
{
crypto
_
scalarmult
}
in C
computes the same
result as
\VSTe
{
RFC
}
in Coq provided that inputs are within
their respective
bounds: arrays of 32 bytes.
\begin{theorem}
\label
{
thm:cryptovst
}
\TNaCle
{
crypto
_
scalarmult
}
in TweetNaCl has the same behavior as
\coqe
{
RFC
}
in Coq.
\end{theorem}
%
\begin{theorem}
%
\label{thm:cryptovst}
%
\TNaCle{crypto_scalarmult} in TweetNaCl has the same behavior as \coqe{RFC} in Coq.
%
\end{theorem}
...
...
@@ 291,35 +302,24 @@ As described in \sref{subsec:NumberTweetNaCl}, numbers in \TNaCle{gf} are repre
in base
$
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 a full integer.
\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 + (pow 2 n) * ZofList q
end.
\end{lstlisting}
We define a notation where
$
n
$
is
$
16
$
.
We reuse the mapping
$
\text
{
\coqe
{
ZofList
}}
:
\Z
\rightarrow
\texttt
{
list
}
~
\Z
\rightarrow
\Z
$
from
\sref
{
subsec:integerbytes
}
and define a notation where
$
n
$
is
$
16
$
, placing us with a radix of
$
2
^{
16
}$
.
\begin{lstlisting}
[language=Coq]
Notation "Z16.lst A" := (ZofList 16 A).
\end{lstlisting}
To facilitate working in
\Zfield
, we define the
\coqe
{
:GF
}
notation.
To facilitate working in
$
\Zfield
$
, we define the
\coqe
{
:GF
}
notation.
\begin{lstlisting}
[language=Coq]
Notation "A :GF" := (A mod (2
^
25519)).
\end{lstlisting}
Later in
\sref
{
sec:maths
}
, we formally define
\F
{
\p
}
.
Equivalence between operations under
\coqe
{
:GF
}
and in
\F
{
\p
}
are easily proven.
Later in
\sref
{
sec:maths
}
, we formally define
$
\F
field
$
.
Equivalence between operations under
\coqe
{
:GF
}
and in
$
\F
field
$
are easily proven.
Using these two definitions, we prove intermediate lemmas such as the correctness of the
multiplication
\Coqe
{
Low.M
}
where
\Coqe
{
Low.M
}
replicate the computations and steps done in C.
\begin{lemma}
\label
{
lemma:mult
_
correct
}
\Coqe
{
Low.M
}
implements correctly the multiplication over
\Zfield
.
\Coqe
{
Low.M
}
implements correctly the multiplication over
$
\Zfield
$
.
\end{lemma}
And specified in Coq as follows:
\begin{lstlisting}
[language=Coq]
...
...
@@ 358,7 +358,7 @@ Lemma M_bound_Zlength :
\subsection
{
Inversions, Reflections and Packing
}
\label
{
subsec:inversionsreflections
}
We now turn our attention to the multiplicative inverse in
\Zfield
and techniques
We now turn our attention to the multiplicative inverse in
$
\Zfield
$
and techniques
to improve the verification speed of complex formulas.
\subheading
{
Inversion in
\Zfield
.
}
...
...
@@ 641,9 +641,12 @@ Lemma Pack25519_mod_25519 :
(Z16.lst l) mod (2
^
25519).
\end{lstlisting}
\todo
{
FINALIZE CONCLUSION HERE
}
By proving that each functions
\coqe
{
Low.M
}
;
\coqe
{
Low.A
}
;
\coqe
{
Low.Sq
}
;
\coqe
{
Low.Zub
}
;
\coqe
{
Unpack25519
}
;
\coqe
{
clamp
}
;
\coqe
{
Pack25519
}
;
\coqe
{
car25519
}
are behaving over
\coqe
{
list Z
}
as their equivalent over
\coqe
{
Z
}
in
\coqe
{
:GF
}
(in
\Zfield
), we prove the correctness of
as their equivalent over
\coqe
{
Z
}
in
\coqe
{
:GF
}
(in
\Zfield
), we prove the
correctness of
% \begin{theorem}
% \label{thm:cryptorfc}
...
...
paper/5_highlevel.tex
View file @
e15af18b
\section
{
Proving that X25519 in Coq matches the mathematical model
}
\label
{
sec:maths
}
In this section we prove the following theorem:
In this section we prove the following
informal
theorem:
% \label{thm:EllipticRFC}
\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
$
and
$
E
$
is the elliptic curve
$
y
^
2
=
x
^
3
+
486662
x
^
2
+
x
$
.
\end{informaltheorem}
More
formal
ly, we prove that our formalization of the RFC matches the definitions of Curve25519 by Bernstein:
More
precise
ly, 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),
...
...
@@ 559,17 +558,11 @@ Theorem curve25519_Fp2_ladder_ok:
curve25519
_
Fp
_
ladder n x = (p *+ n)#x0 /p.
\end{lstlisting}
\todo
{
FINALIZE / CONCLUDE HERE
}
We then prove the equivalence between of operations over
\coqe
{
Zmodp
}
and
\coqe
{
:GF
}
(seen as
\Zfield
).
This allows us to show that given a clamped value
$
n
$
and normalized
$
x
$
coordinate of
$
P
$
,
$
Curve
25519
\_
Fp
$
is equivalent to RFC~7748~
\cite
{
rfc7748
}
. This is formalized as follows:
\begin{lstlisting}
[language=Coq]
Lemma ZCrypto
_
Scalarmult
_
curve25519
_
ladder:
forall (n:nat) (x:Z),
ZCrypto
_
Scalarmult n x = val
(curve25519
_
Fp
_
ladder
(Z.to
_
nat (Zclamp n))
(Zmodp.pi (modP (ZUnpack25519 x)))).
\end{lstlisting}
$
Curve
25519
\_
Fp
$
is equivalent to RFC~7748~
\cite
{
rfc7748
}
.
From
\tref
{
thm:RFC
}
and
\tref
{
thm:generalscalarmult
}
, we prove the correctness
of
\TNaCle
{
crypto
_
scalarmult
}
(
\tref
{
thm:EllipticRFC
}
).
paper/6_conclusion.tex
View file @
e15af18b
...
...
@@ 75,6 +75,9 @@ We believe that the type change of the loop index (\TNaCle{int} instead of \TNaC
does not impact the trust of our proof.
\subheading
{
A complete proof.
}
\todo
{
REWRITE
}
We provide a mechanized formal proof of the correctness of the X25519 implementation in TweetNaCl.
We first proved that TweetNaCl's implementation of X25519 matches RFC~7748 (
\tref
{
thm:VSTRFC
}
).
In a second step we extended the Coq library for elliptic curves
\cite
{
BartziaS14
}
...
...
paper/A2_coq.tex
View file @
e15af18b
...
...
@@ 27,7 +27,7 @@ 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')
Fixpoint montgomery
_
rec (m: nat) (z: T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
(* a: x2 *)
(* b: x3 *)
...
...
@@ 94,18 +94,18 @@ Definition modP (x:Z) : Z :=
(* Encapsulate in a module. *)
Module Mid.
(* shift to the right by n bits *)
Definition getCarry (n:Z) (m:Z) : Z :=
Definition getCarry (n:
Z) (m:
Z) : Z :=
Z.shiftr m n.
(* logical and with n ones *)
Definition getResidue (n:Z) (m:Z) : Z :=
Definition getResidue (n:
Z) (m:
Z) : Z :=
Z.land n (Z.ones n).
Definition car25519 (n:Z) : Z :=
Definition car25519 (n:
Z) : Z :=
38 * getCarry 256 n + getResidue 256 n.
(* The carry operation is invariant under modulo *)
Lemma Zcar25519
_
correct:
forall (n:Z), n:GF = (Mid.car25519 n) :GF.
forall (n:
Z), n:GF = (Mid.car25519 n) :GF.
(* Define Mid.A, Mid.M ... *)
Definition A a b := Z.add a b.
...
...
@@ 116,20 +116,20 @@ Module Mid.
Definition C
_
0 := 0.
Definition C
_
1 := 1.
Definition C
_
121665 := 121665.
Definition Sel25519 (b p q:Z) :=
Definition Sel25519 (b p q:
Z) :=
if (Z.eqb b 0) then p else q.
Definition getbit (i:Z) (a: Z) :=
if (Z.ltb a 0) then
if (Z.ltb a 0) then
(* a < 0*)
0
else if (Z.ltb i 0) then
else if (Z.ltb i 0) then
(* i < 0 *)
Z.land a 1
else
else
(* 0 <= a
&
0 <= i *)
Z.land (Z.shiftr a i) 1.
End Mid.
(* Clamping *)
Definition clamp (n
: list Z) : list Z :=
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
...
...
@@ 141,9 +141,14 @@ Definition clamp (n : list Z) : list Z :=
upd
_
nth 0 n' x'.
(* x
^{
p  2
}
*)
Definition ZInv25519 (x:Z) : Z :=
Definition ZInv25519 (x:
Z) : Z :=
Z.pow x (Z.pow 2 255  21).
(* reduction modulo P *)
Definition ZPack25519 (n: Z) : Z :=
Z.modulo n (Z.pow 2 255  19).
(* instantiate over Z *)
Instance Z
_
Ops : (Ops Z Z modP) :=
{}
.
Proof.
...
...
paper/A3_proofs.tex
View file @
e15af18b
...
...
@@ 36,13 +36,17 @@ In this folder the reader will find multiple levels of implementation of X25519.
instantiated with different operations. This ladder is the stub for the
following implementations.
\item
\textbf
{
\texttt
{
Mid/
}}
provides a listbased implementation of the
basic operations
\TNaCle
{
A
}
,
\TNaCle
{
Z
}
,
\TNaCle
{
M
}
\ldots
and the ladder. It
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.
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.
\end{itemize}
\subheading
{
\texttt
{
proofs/vst/
}}
...
...
paper/A4_files.tex
View file @
e15af18b
\todo
{
I don't think this belongs to the paper but more to the associated materials
}
%
\todo{I don't think this belongs to the paper but more to the associated materials}
\subsection
{
Content of the proof files
}
\label
{
appendix:prooffiles
}
We provide below the location of the most important definitions and lemmas of our proofs.
\subsubsection
{
Definitions
}
~
\begin{table}
[h]
%
\subsubsection{Definitions}
%
~
\begin{table
*
}
[h]
% \caption{Definitions}
% \label{table:specs}
\begin{tabular}
{
l  l  l
}
Definition
&
File
&
Description
\\
\hline
\texttt
{
ZofList
}
&
\texttt
{
ListsOp/ZofList.v
}
&
List
$
\leftrightarrow
$
\Z\\
\texttt
{
ZofList
}
&
\texttt
{
ListsOp/ZofList.v
}
&
\Z
$
\rightarrow
$
List
\Z
$
\rightarrow
$
\Z\\
\texttt
{
ListofZ32
}
&
\texttt
{
ListsOp/ListofZ.v
}
&
\Z
$
\rightarrow
$
\Z
$
\rightarrow
$
list
\Z\\
\hline
\multicolumn
{
3
}{
c
}{
Elliptic Curve
\&
Fields
}
\\
\hline
...
...
@@ 98,15 +99,21 @@ We provide below the location of the most important definitions and lemmas of ou
\hline
\multicolumn
{
3
}{
c
}{
X25519 over
\Z
and list of
\Z
}
\\
\hline
\texttt
{
ZCrypto
\_
Scalarmult
}
&
\texttt
{
Mid/Crypto
\_
Scalarmult.v
}
&
RFC
specification of X25519
\\
\texttt
{
ZCrypto
\_
Scalarmult
}
&
\texttt
{
Mid/Crypto
\_
Scalarmult.v
}
&
integers
specification of X25519
\\
\texttt
{
Crypto
\_
Scalarmult
}
&
\texttt
{
Low/Crypto
\_
Scalarmult.v
}
&
list specification of X25519
\\
\texttt
{
CSM
}
&
\texttt
{
Low/Crypto
\_
Scalarmult
\_
.v
}
&
aliasing of
\texttt
{
Crypto
\_
Scalarmult
}
\\
\hline
\multicolumn
{
3
}{
c
}{
RFC~7748
}
\\
\hline
\texttt
{
decodeScalar25519
}
&
\texttt
{
rfc/rfc.v
}
&
Decode the scalar
\\
\texttt
{
decodeUCoordinate
}
&
\texttt
{
rfc/rfc.v
}
&
Decode the xcoordinate
\\
\texttt
{
encodeUCoordinate
}
&
\texttt
{
rfc/rfc.v
}
&
Encode the resulting xcoordinate
\\
\texttt
{
RFC
}
&
\texttt
{
rfc/rfc.v
}
&
specification of X25519 as in RFC~7748
\\
\hline
\end{tabular}
\end{table}
\end{table
*
}
\subsubsection
{
Lemmas and Theorems
}
~
%
\subsubsection{Lemmas and Theorems}
%
~
% \begin{table}[h]
% \begin{tabular}{ l  l  l }
% Definition & File & Description \\
...
...
paper/_macros.tex
View file @
e15af18b
\newtheorem
{
theorem
}{
Theorem
}
[section]
\newtheorem
{
lemma
}
[theorem]
{
Lemma
}
\newtheorem
{
proposition
}
[theorem]
{
Proposition
}
\newtheorem
{
corollary
}
[theorem]
{
Corollary
}
\newtheorem
{
dfn
}
[theorem]
{
Definition
}
\newtheorem
{
hypothesis
}
[theorem]
{
Hypothesis
}
...
...
@@ 164,40 +163,40 @@
% \def\gets{{\leftarrow}}