4-lowlevel.tex 1.21 KB
 Peter Schwabe committed Jun 20, 2019 1 \section{Proving equivalence of X25519 in C and Coq}  Benoit Viguier committed Sep 18, 2019 2 \label{sec:C-Coq}  Benoit Viguier committed Aug 01, 2019 3   Benoit Viguier committed Sep 02, 2019 4 5 In this section we prove the following theorem: % In this section we outline the structure of our proofs of the following theorem:  Benoit Viguier committed Sep 18, 2019 6   Benoit Viguier committed Sep 18, 2019 7 \begin{informaltheorem}  benoit committed Sep 28, 2020 8 9  The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches the specifications of RFC~7748~\cite{rfc7748} (\Coqe{RFC}).  Benoit Viguier committed Sep 18, 2019 10 11 \end{informaltheorem}  Benoit Viguier committed Sep 20, 2019 12 13 14 15 16 More formally: \begin{lstlisting}[language=Coq] Theorem body_crypto_scalarmult: (* VST boiler plate. *) semax_body  benoit committed Sep 28, 2020 17  (* Clight translation of TweetNaCl. *)  Benoit Viguier committed Sep 20, 2019 18  Vprog  Benoit Viguier committed Sep 21, 2019 19  (* Hoare triples for fct calls. *)  Benoit Viguier committed Sep 20, 2019 20 21 22  Gprog (* fct we verify. *) f_crypto_scalarmult_curve25519_tweet  Benoit Viguier committed Sep 21, 2019 23  (* Our Hoare triple, see below. *)  Benoit Viguier committed Sep 20, 2019 24 25  crypto_scalarmult_spec. \end{lstlisting}  Benoit Viguier committed Jun 21, 2019 26   Benoit Viguier committed Sep 30, 2019 27 % We first describe the global structure of our proof (\ref{subsec:proof-structure}).  Benoit Viguier committed Sep 19, 2019 28 Using our formalization of RFC~7748 (\sref{sec:Coq-RFC}) we specify the Hoare  Benoit Viguier committed Feb 15, 2020 29 triple before proving its correctness with VST (\ref{subsec:with-VST}).  Benoit Viguier committed Sep 02, 2019 30 We provide an example of equivalence of operations over different number  Benoit Viguier committed Jan 14, 2020 31 representations (\ref{subsec:num-repr-rfc}).  Benoit Viguier committed Jan 16, 2020 32 % Then, we describe efficient techniques used in some of our more complex proofs (\ref{subsec:inversions-reflections}).