Commit 1dcdac35 authored by Freek Wiedijk's avatar Freek Wiedijk
Browse files

fiddling with the abstract

parent 29ec42c5
% \subsection*{Abstract} % \subsection*{Abstract}
\begin{abstract} \begin{abstract}
Based on a formal definition of the X25519 key exchange protocol We formally prove that the C implementation of
from Bernstein's 2006 paper, as standardized in RFC 7748, the X25519 key exchange protocol
we formally prove that the C implementation of in the TweetNaCl library is correct.
this protocol in the TweetNaCl library is We prove both that it correctly implements the protocol from
correct and free from all undefined behaviors, like arithmetic overflows Bernstein's 2006 paper, as standardized in RFC 7748,
as well that there are no undefined behaviors
like arithmetic overflows
and array out of bound errors. and array out of bound 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 that X25519 is mathematically correct
......
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