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
f9914841
Commit
f9914841
authored
Sep 21, 2019
by
Benoit Viguier
Browse files
small fixes
parent
1b4c230d
Changes
3
Hide whitespace changes
Inline
Side-by-side
paper/6_conclusion.tex
View file @
f9914841
...
...
@@ -83,4 +83,4 @@ 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
the mathematical definitions as given in~
\cite
[Sec.~2]
{
Ber06
}
(
\tref
{
thm:Elliptic-CSM
}
)
.
the mathematical definitions as given in~
\cite
[Sec.~2]
{
Ber06
}
.
paper/A4_files.tex
View file @
f9914841
% \todo{I don't think this belongs to the paper but more to the associated materials}
\subsection
{
Content of the proof files
}
\label
{
appendix:proof-files
}
We provide below the location of the most important definitions and lemmas of our proofs.
%
\subsection{Content of the proof files}
%
\label{appendix:proof-files}
%
%
We provide below the location of the most important definitions and lemmas of our proofs.
% \subsubsection{Definitions}
% ~
...
...
paper/Makefile
View file @
f9914841
...
...
@@ -39,6 +39,7 @@ clean:
@
rm
*
.log 2> /dev/null
||
true
@
rm
*
.out 2> /dev/null
||
true
@
rm
*
.bck 2> /dev/null
||
true
@
rm
*
.bak 2> /dev/null
||
true
@
rm
*
/
*
.aux 2> /dev/null
||
true
@
rm
tweetverif.tex 2> /dev/null
||
true
...
...
Write
Preview
Supports
Markdown
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