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
ac359637
Commit
ac359637
authored
Jan 22, 2021
by
Timmy Weerwag
Browse files
Typos
parent
77c23112
Changes
5
Hide whitespace changes
Inline
Sidebyside
Showing
5 changed files
with
14 additions
and
14 deletions
+14
14
paper/highlevel.tex
paper/highlevel.tex
+4
4
paper/lowlevel.tex
paper/lowlevel.tex
+1
1
paper/preliminaries.tex
paper/preliminaries.tex
+1
1
paper/rfc.tex
paper/rfc.tex
+6
6
paper/tweetverif.tex
paper/tweetverif.tex
+2
2
No files found.
paper/highlevel.tex
View file @
ac359637
...
...
@@ 34,14 +34,14 @@ with it in the proofs (\ref{subsec:curvep2}).
\label
{
subsec:ECC
}
\fref
{
tikz:ProofHighLevel1
}
presents the structure of the proof of the ladder's
correctness. The white tiles are definitions, the orange ones are hypothes
i
s and
correctness. The white tiles are definitions, the orange ones are hypothes
e
s and
the green tiles represent major lemmas and theorems.
% 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 a
n
commutative group.
we prove that
$
M
_{
a,b
}
(
\K
)
$
forms a commutative group.
Under the hypothesis that
$
a
^
2

4
$
is not a square in
$
\K
$
, we prove the correctness of the ladder (
\tref
{
thm:montgomeryladdercorrect
}
).
...
...
@@ 49,7 +49,7 @@ $a^2  4$ is not a square in $\K$, we prove the correctness of the ladder (\tref
\centering
\include
{
tikz/highlevel1
}
% \vspace{0.5cm}
\caption
{
Overview of the proof of Montgomery ladder's correctness
}
\caption
{
Overview of the proof of Montgomery ladder's correctness
.
}
\label
{
tikz:ProofHighLevel1
}
\end{figure}
...
...
@@ 79,7 +79,7 @@ Then, this equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.
The
\textit
{
elliptic curve
}
$
E
_{
a,b
}$
is defined by the equation
$$
y
^
2
=
x
^
3
+
ax
+
b.
$$
$
E
_{
a,b
}
(
\K
)
$
is the set of all points
$
(
x,y
)
\in
\K
^
2
$
satisfying the
$
E
_{
a,b
}$
along with an additional formal point
$
\Oinf
$
, ``at infinity''. Such a curve does not have any singularit
y
.
along with an additional formal point
$
\Oinf
$
, ``at infinity''. Such a curve does not have any singularit
ies
.
\end{dfn}
In this setting, Bartzia and Strub defined the parametric type
\texttt
{
ec
}
which
...
...
paper/lowlevel.tex
View file @
ac359637
...
...
@@ 310,7 +310,7 @@ Lemma M_bound_Zlength :
\begin{sloppypar}
By using each function
\coqe
{
Low.M
}
;
\coqe
{
Low.A
}
;
\coqe
{
Low.Sq
}
;
\coqe
{
Low.Zub
}
;
\coqe
{
Unpack25519
}
;
\coqe
{
clamp
}
;
\coqe
{
Pack25519
}
;
\coqe
{
Inv25519
}
;
\coqe
{
car25519
}
;
\coqe
{
montgomery
_
rec
}
, we defined
in Coq
\coqe
{
Crypto
_
Scalarmult
}
and with VST
\coqe
{
montgomery
_
rec
}
, we defined
\coqe
{
Crypto
_
Scalarmult
}
in Coq
and with VST
proved it matches the exact behavior of X25519 in TweetNaCl.
\end{sloppypar}
...
...
paper/preliminaries.tex
View file @
ac359637
...
...
@@ 281,7 +281,7 @@ Separation logic is an extension of Hoare logic which allows reasoning about
pointers and memory manipulation.
%This logic enforces strict conditions on the memory shared such as being disjoint.
%Separation logic requires memory regions of different function arguments to be disjoint.
Reasoning in separation logic assumes that certain memory regions are nonoverlapping
Reasoning in separation logic assumes that certain memory regions are nonoverlapping
.
We discuss this limitation further in
\sref
{
subsec:withVST
}
.
The Verified Software Toolchain (VST)~
\cite
{
cao2018vstfloyd
}
is a framework
...
...
paper/rfc.tex
View file @
ac359637
...
...
@@ 84,15 +84,15 @@ match m with
end.
\end{lstlisting}
The comments in the ladder represent the text from the RFC which
The comments in the ladder represent the text from the RFC
,
which
our formalization matches perfectly. In order to optimize the
number of calls to
\texttt
{
CSWAP
}
(defined in
\sref
{
cswap
}
)
the RFC uses an additional variable to decide whether a conditional swap
is required or not.
Later in our proof we use a simpler description of the ladder
(
\coqe
{
montgomery
_
rec
}
) which
follows
strictly
\aref
{
alg:montgomeryladder
}
and prove those ladder equivalent.
(
\coqe
{
montgomery
_
rec
}
)
,
which strictly
follows
\aref
{
alg:montgomeryladder
}
,
and prove those ladder
s
equivalent.
RFC 7748 describes the calculations done in X25519 as follows:
\emph
{
``To implement the X25519(k, u) [...] functions (where k is
...
...
@@ 102,7 +102,7 @@ RFC 7748 describes the calculations done in X25519 as follows:
in GF(p), i.e., they are performed modulo p.''
}
~
\cite
{
rfc7748
}
Operations used in the Montgomery ladder of
\coqe
{
RFC
}
are performed on
integers (
S
ee Appendix~
\ref
{
subsubsec:RFCCoq
}
).
integers (
s
ee Appendix~
\ref
{
subsubsec:RFCCoq
}
).
The reduction modulo
$
\p
$
is deferred to the very end as part of the
\coqe
{
ZPack25519
}
operation.
...
...
@@ 110,7 +110,7 @@ We now turn our attention to the decoding and encoding of the byte arrays.
We define the littleendian projection to integers as follows.
\begin{dfn}
Let
\Coqe
{
ZofList
}
:
$
\Z
\rightarrow
\texttt
{
list
}
~
\Z
\rightarrow
\Z
$
,
a function which given
$
n
$
and a list
$
l
$
returns its little
endian decoding with radix
$
2
^
n
$
.
a function which given
$
n
$
and a list
$
l
$
returns its little

endian decoding with radix
$
2
^
n
$
.
\end{dfn}
% \begin{lstlisting}[language=Coq,belowskip=1pt]
% Fixpoint ZofList {n:Z} (a:list Z) : Z :=
...
...
@@ 119,7 +119,7 @@ We define the littleendian projection to integers as follows.
%  h :: q => h + 2^n * ZofList q
% end.
% \end{lstlisting}
Similarly, we define the projection from
an
integers to
a
littleendian list.
Similarly, we define the projection from integers to littleendian list
s
.
\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
$
.
...
...
paper/tweetverif.tex
View file @
ac359637
...
...
@@ 31,8 +31,8 @@
The Netherlands
}
\and
\IEEEauthorblockN
{
Timmy Weerwag
}
\IEEEauthorblockA
{
Radboud University
,
\\
T
he Netherlands
}
\IEEEauthorblockA
{
Radboud University
\&
\\
Open University
\\
of t
he Netherlands
}
\and
\IEEEauthorblockN
{
Freek Wiedijk
}
\IEEEauthorblockA
{
Radboud University,
\\
...
...
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