Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
8b9f4c04
Commit
8b9f4c04
authored
Feb 13, 2020
by
Benoit Viguier
Browse files
more space, less details
parent
02d38ac7
Changes
2
Hide whitespace changes
Inline
Side-by-side
paper/3-RFC.tex
View file @
8b9f4c04
...
@@ -83,25 +83,15 @@ match m with
...
@@ -83,25 +83,15 @@ match m with
(a,b,c,d,e,f)
(a,b,c,d,e,f)
end.
end.
\end{lstlisting}
\end{lstlisting}
% The definitions of the encoding and decoding functions are detailed later
% in this section.
Our formalization
differs slightly from
the RFC. In
deed in
order to optimize the
Our formalization
matches perfectly
the RFC. In order to optimize the
number of calls to
\texttt
{
CSWAP
}
(defined in
\sref
{
cswap
}
)
number of calls to
\texttt
{
CSWAP
}
(defined in
\sref
{
cswap
}
)
the RFC uses an additional variable to decide
the RFC uses an additional variable to decide whether a conditional swap
whether a conditional swap is required or not. Our description of the ladder
is required or not, this differ from
\aref
{
alg:montgomery-ladder
}
.
follows strictly the shape of the exponent as described in
\aref
{
alg:montgomery-ladder
}
.
This divergence is allowed by the RFC:
\emph
{
``Note that these formulas are slightly different from Montgomery's
original paper. Implementations are free to use any correct formulas.''
}
~
\cite
{
rfc7748
}
.
We later prove our ladder correct in that respect (
\sref
{
sec:maths
}
).
% TweetNaCl implements X25519 with numbers represented as arrays.
Later in our proof we use a simpler description of the ladder
% RFC~7748 defines X25519 over field elements. We show the equivalence between
(
\coqe
{
montgomery
_
rec
}
) which follows strictly the shape of
% the different number representations. To simplify our proof, we define operations
the exponent and prove those ladder equivalent.
% used in the ladder over generic types \coqe{T} and \coqe{T'}.
% Those types are later instantiated as list of integers, integers, natural
% numbers, or field elements.
\emph
{
``To implement the X25519(k, u) [...] functions (where k is
\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
the scalar and u is the u-coordinate), first decode k and u and then
...
@@ -109,11 +99,6 @@ perform the following procedure, which is taken from [curve25519] and
...
@@ -109,11 +99,6 @@ perform the following procedure, which is taken from [curve25519] and
based on formulas from [montgomery]. All calculations are performed
based on formulas from [montgomery]. All calculations are performed
in GF(p), i.e., they are performed modulo p.''
}
~
\cite
{
rfc7748
}
in GF(p), i.e., they are performed modulo p.''
}
~
\cite
{
rfc7748
}
% In TweetNaCl, as described in \sref{subsec:Number-TweetNaCl},
% elements of $\F{p}$ are represented as big integers using radix $2^{16}$.
% We use a direct mapping to represent such an array of limbs
% as a list of integers in Coq.
% RFC~7748 states that \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 performed on
Operations used in the Montgomery ladder of
\coqe
{
RFC
}
are performed on
integers (See Appendix~
\ref
{
subsubsec:RFC-Coq
}
).
integers (See Appendix~
\ref
{
subsubsec:RFC-Coq
}
).
The reduction modulo
$
\p
$
is deferred to the very end as part of the
The reduction modulo
$
\p
$
is deferred to the very end as part of the
...
@@ -122,7 +107,6 @@ We define the little-endian projection to integers as follows.
...
@@ -122,7 +107,6 @@ We define the little-endian projection to integers as follows.
\begin{dfn}
\begin{dfn}
Let
\Coqe
{
ZofList
}
:
$
\Z
\rightarrow
\texttt
{
list
}
~
\Z
\rightarrow
\Z
$
,
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
$
.
a function given
$
n
$
and a list
$
l
$
returns its little endian decoding with radix
$
2
^
n
$
.
% We define it in Coq as:
\end{dfn}
\end{dfn}
\begin{lstlisting}
[language=Coq,aboveskip=0pt,belowskip=1pt]
\begin{lstlisting}
[language=Coq,aboveskip=0pt,belowskip=1pt]
Fixpoint ZofList
{
n:Z
}
(a:list Z) : Z :=
Fixpoint ZofList
{
n:Z
}
(a:list Z) : Z :=
...
...
paper/5-highlevel.tex
View file @
8b9f4c04
...
@@ -280,43 +280,48 @@ differential additions and point doublings using projective coordinates.
...
@@ -280,43 +280,48 @@ differential additions and point doublings using projective coordinates.
By taking
\aref
{
alg:montgomery-ladder
}
and replacing
\texttt
{
xDBL
\&
ADD
}
by a
By taking
\aref
{
alg:montgomery-ladder
}
and replacing
\texttt
{
xDBL
\&
ADD
}
by a
combination of the formulae from
\lref
{
lemma:xADD
}
and
\lref
{
lemma:xDBL
}
,
combination of the formulae from
\lref
{
lemma:xADD
}
and
\lref
{
lemma:xDBL
}
,
we define a ladder
\coqe
{
opt
_
montgomery
}
(in which
$
\K
$
has not been fixed yet),
we define a ladder
\coqe
{
opt
_
montgomery
}
(in which
$
\K
$
has not been fixed yet).
similar to the one used in TweetNaCl.
% similar to the one used in TweetNaCl (with \coqe{montgomery_rec}).
This definition is closely related to
\coqe
{
montgomery
_
rec
_
swap
}
that was used
% shown above.
in the definition of
\coqe
{
RFC
}
, and is easily proved to correspond to it.
In Coq this correspondence proof is hidden in the proof of
\coqe
{
RFC
_
Correct
}
shown above.
% We prove its correctness for any point whose \xcoord is not 0.
%
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Lemma opt_montgomery_x :
% forall (n m : nat) (x : K),
% n < 2^m -> x != 0 ->
% forall (p : mc M), p#x0 = x ->
% opt_montgomery n m x = (p *+ n)#x0.
% \end{lstlisting}
% We can remark that for an input $x = 0$, the ladder returns $0$.
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Lemma opt_montgomery_0:
% forall (n m : nat), opt_montgomery n m 0 = 0.
% \end{lstlisting}
% Also \Oinf\ is the neutral element of $M_{a,b}(\K)$.
% \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
% Lemma p_x0_0_eq_0 : forall (n : nat) (p : mc M),
% p #x0 = 0%:R -> (p *+ n) #x0 = 0%R.
% \end{lstlisting}
% This gives us the theorem of the correctness of the Montgomery ladder.
We prove its correctness for any point whose
\xcoord
is not 0.
\begin{lstlisting}
[language=Coq,belowskip=-0.25
\baselineskip
]
Lemma opt
_
montgomery
_
x :
forall (n m : nat) (x : K),
n < 2
^
m -> x != 0 ->
forall (p : mc M), p#x0 = x ->
opt
_
montgomery n m x = (p *+ n)#x0.
\end{lstlisting}
We can remark that for an input
$
x
=
0
$
, the ladder returns
$
0
$
.
\begin{lstlisting}
[language=Coq,belowskip=-0.25
\baselineskip
]
Lemma opt
_
montgomery
_
0:
forall (n m : nat), opt
_
montgomery n m 0 = 0.
\end{lstlisting}
Also
\Oinf\
is the neutral element of
$
M
_{
a,b
}
(
\K
)
$
.
\begin{lstlisting}
[language=Coq,belowskip=-0.25
\baselineskip
]
Lemma p
_
x0
_
0
_
eq
_
0 : forall (n : nat) (p : mc M),
p #x0 = 0
%:R -> (p *+ n) #x0 = 0%R.
\end{lstlisting}
This gives us the theorem of the correctness of the Montgomery ladder.
This gives us the theorem of the correctness of the Montgomery ladder.
\begin{theorem}
\begin{theorem}
\label
{
thm:montgomery-ladder-correct
}
\label
{
thm:montgomery-ladder-correct
}
For all
$
n, m
\in
\N
$
,
$
x
\in
\K
$
,
$
P
\in
M
_{
a,b
}
(
\K
)
$
,
For all
$
n, m
\in
\N
$
,
$
x
\in
\K
$
,
$
P
\in
M
_{
a,b
}
(
\K
)
$
,
if
$
\chi
_
0
(
P
)
=
x
$
then
\coqe
{
opt
_
montgomery
}
returns
$
\chi
_
0
(
n
\cdot
P
)
$
if
$
\chi
_
0
(
P
)
=
x
$
then
\coqe
{
opt
_
montgomery
}
returns
$
\chi
_
0
(
n
\cdot
P
)
$
\end{theorem}
\end{theorem}
\begin{lstlisting}
[language=Coq
,belowskip=-0.5
\baselineskip
]
\begin{lstlisting}
[language=Coq]
Theorem opt
_
montgomery
_
ok (n m: nat) (x : K) :
Theorem opt
_
montgomery
_
ok (n m: nat) (x : K) :
n < 2
^
m ->
n < 2
^
m ->
forall (p : mc M), p#x0 = x ->
forall (p : mc M), p#x0 = x ->
opt
_
montgomery n m x = (p *+ n)#x0.
opt
_
montgomery n m x = (p *+ n)#x0.
\end{lstlisting}
\end{lstlisting}
The definition of
\coqe
{
opt
_
montgomery
}
is closely related to
\coqe
{
montgomery
_
rec
_
swap
}
that was used in
\coqe
{
RFC
}
.
We proved their equivalence, and used it in our
final proof of
\coqe
{
Theorem RFC
_
Correct
}
.
\subsection
{
Curves, twists and extension fields
}
\subsection
{
Curves, twists and extension fields
}
\label
{
subsec:curve
_
twist
_
fields
}
\label
{
subsec:curve
_
twist
_
fields
}
...
...
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