Commit 3b681936 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

typos

parent d14762d4
......@@ -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 cruves \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}).
......@@ -345,7 +345,7 @@ Coq~\cite{coq-faq} is an interactive theorem prover. It provides an expressive
formal language to write mathematical definitions, algorithms and theorems together
with their proofs. It has been used in the proof of the four-color theorem~\cite{gonthier2008formal}.
The CompCert C compiler~\cite{Leroy-backend} was implemented with it.
The Compcert C sematinc is very close to C17~\cite{ISO:C17}, giving us the guarantee
The Compcert C semantic is very close to C17~\cite{ISO:C17}, giving us the guarantee
that the intended behavior is preserved through the compilation to the machine code.
As opposed to other systems such as F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17},
......
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