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
7827a51b
Commit
7827a51b
authored
Oct 01, 2019
by
Freek Wiedijk
Browse files
wording of the abstract
parent
e4acd36b
Changes
1
Hide whitespace changes
Inline
Side-by-side
paper/0_abstract.tex
View file @
7827a51b
...
@@ -5,9 +5,9 @@
...
@@ -5,9 +5,9 @@
in the TweetNaCl library is correct.
in the TweetNaCl library is correct.
We prove both that it correctly implements the protocol from
We prove both that it correctly implements the protocol from
Bernstein's 2006 paper, as standardized in RFC~7748,
Bernstein's 2006 paper, as standardized in RFC~7748,
well as the absence of undefined behavior
as
well as the absence of undefined behavior
like arithmetic overflows
like arithmetic overflows
and array out of bound errors.
and array out of bound
s
errors.
We also formally prove, based on the work of Bartzia and Strub,
We also formally prove, based on the work of Bartzia and Strub,
that X25519 is mathematically correct, i.e.,
that X25519 is mathematically correct, i.e.,
that it correctly computes scalar multiplication on
that it correctly computes scalar multiplication on
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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