Skip to content

GitLab

Commit cc7d9014 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

typos

parent 3b681936
Hide whitespace changes
Inline Side-by-side
paper/conclusion.tex
View file @ cc7d9014
......@@ -77,7 +77,7 @@ does not impact the trust of our proof.
\subheading{A complete proof.}
We provide a mechanized formal proof of the correctness of the X25519 implementation in TweetNaCl.
We first proved that TweetNaCl's implementation of X25519 matches RFC~7748 (\tref{thm:VST-RFC}).
In a second step we extended the COq library for elliptic curves \cite{BartziaS14}
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 implementation in TweetNaCl matches the mathematical
definitions as given in~\cite[Sec.~2]{Ber06} (\tref{thm:Elliptic-CSM}).
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