Commit 01f7a34d authored by Freek Wiedijk's avatar Freek Wiedijk
Browse files

- removed hyphen in RFC-7748 in abstract

- added why Timmy's work also is interesting if you are not
interested in math but only in crypto (it's a sanity check
on our formalization of the RFC)
parent cbec0bd8
......@@ -2,7 +2,7 @@
Based on a formal definition of the X25519 key exchange protocol
from Bernstein's 2006 paper, as standardized in RFC-7748,
from Bernstein's 2006 paper, as standardized in RFC 7748,
we formally prove that the C implementation of
this protocol in the TweetNaCl library is
correct and free from all undefined behaviors, like arithmetic overflows
......@@ -45,6 +45,8 @@ of an asymmetric cryptographic primitive.
In the last step we prove that the Coq implementation matches
the mathematical definition of X25519 as given in~\cite[Sec.~2]{Ber06}.
This is important as a check that there are no transcription errors
in our formal version of the X25519 definition.
We do this by extending the Coq library
for elliptic curves~\cite{BartziaS14} by Bartzia and Strub to
support Montgomery curves, and in particular Curve25519.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment