Commit 5ad9b788 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more stuff in paper

parent 2b776174
......@@ -91,8 +91,9 @@ Appendix~\ref{appendix:proof-folders}.
\subheading{Organization of this paper.}
\sref{sec:preliminaries} give the necessary background on Curve25519 and X25519
implementations and a brief explanation of how formal verification works.
\sref{sec:C-Coq-RFC} provides the specification of X25519 and in addition the proofs
techniques used to show the correctness with respect to RFC~7748~\cite{rfc7748}.
\sref{sec:Coq-RFC} provides our formalization of RFC~7748~\cite{rfc7748}'s X25519.
\sref{sec:C-Coq} provides the specification of TweetNaCl's X25519 and some of the
proofs techniques used to show the correctness with respect to RFC~7748~\cite{rfc7748}.
\sref{sec:maths} describes our extension of the formal library by Bartzia
and Strub and the correctness of X25519 implementation with respect to Bernstein's
specifications~\cite{Ber14}.
......
\section{Formalizing X25519 from RFC~7748}
\label{sec:Coq-RFC}
In this section we present our formalization of RFC~7748~\cite{rfc7748}.
\begin{informaltheorem}
The specification of X25519 in RFC~7748 is formalized by \Coqe{ZCrypto_Scalarmult}.
\end{informaltheorem}
More precisely, we formalized X25519 with the following definition.
\begin{coq}
Definition ZCrypto_Scalarmult n p :=
let t := montgomery_rec
255 (* iterate 255 times *)
(Zclamp n) (* clamped n *)
1 (* x_2 *)
(ZUnpack25519 p) (* x_3 *)
0 (* z_2 *)
1 (* z_3 *)
0 (* dummy *)
0 (* dummy *)
(ZUnpack25519 p) (* x_1 *) in
let a := get_a t in
let c := get_c t in
ZPack25519 (Z.mul a (ZInv25519 c)).
\end{coq}
We first present a generic description of the Montgomery ladder (\ref{subsec:spec-ladder}).
Then we turn our attention to the different steps of the computation (\ref{subsec:spec-unpack-clamp-inv-pack}).
\subsection{A generic ladder}
\label{subsec:spec-ladder}
% \emph{``All calculations are performed in GF(p), i.e., they are performed modulo p.''}
TweetNaCl implements X25519 with numbers represented as arrays.
RFC~7748 defines X25519 over field elements. As we show the equivalence between
the different representation, to simplify our proof, we define operations used
in the ladder over generic types \coqe{T} and \coqe{T'}.
Those types are later instantiated as natural numbers, integers, field elements,
list of integers.
The generic definition of the ladder (\coqe{montgomery_rec}) and its parallel with
the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}.
Our formalization differs slightly from the RFC. Indeed in order to optimize the
number of \texttt{CSWAP} calls the RFC uses an additional variable to decide
whether a conditionnal swap is required or not. Our description of the ladder
follows strictly the shape of the exponent as described in \aref{alg:montgomery-ladder}.
This divergence is allowed by the RFC:
\emph{``Note that these formulas are slightly different from Montgomery's
original paper. Implementations are free to use any correct formulas.''}~\cite{rfc7748}.
We later prove our ladder correct in that respect (\sref{sec:maths}).
% In appendix~\ref{subsubsec:CryptoScalarmult}, we show the the formalization of
% \TNaCle{crypto_scalarmult} over lists of integers. We define it as
% \Coqe{Crypto_Scalarmult} or \Coqe{CSM}. For the sake of space and simplicity we
% do not display the definitions of each underlying function.
\subsection{Unpacking, clamping, Inversion and Packing}
\label{subsec:spec-unpack-clamp-inv-pack}
Inputs of X25519
% \emph{``To implement the X25519(k, u) and X448(k, u) functions (where k is
% the scalar and u is the u-coordinate), first decode k and u and then
% perform the following procedure, which is taken from [curve25519] and
% based on formulas from [montgomery]. All calculations are performed
% in GF(p), i.e., they are performed modulo p.''}~\cite{rfc7748}
\coqe{montgomery_rec} only computes the ladder steps.
While the inversion, the packing, the unpacking (setting bit 255 to \texttt{0})
and the clamping are not defined in a generic manner, we show their equivalence
between the different representations.
Appendix~\ref{subsubsec:ZCryptoScalarmult} shows the instantiation of our ladder
over Integers (type \coqe{Z}). We call it \coqe{ZCrypto_Scalarmult}.
The modulo reduction is applied in \coqe{ZPack25519} translating every
underlying operations as over \Zfield. As a result this specification can be
interpreted as the formalization of X25519 in RFC~7748.
\section{Proving equivalence of X25519 in C and Coq}
\label{sec:C-Coq-RFC}
\label{sec:C-Coq}
In this section we prove the following theorem:
% In this section we outline the structure of our proofs of the following theorem:
\begin{theorem}
\begin{informaltheorem}
\label{thm:VST-RFC}
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches
the specifications of RFC~7748~\cite{rfc7748}
\end{theorem}
the specifications of RFC~7748~\cite{rfc7748} (\Coqe{ZCrypto_Scalarmult})
\end{informaltheorem}
More formally.
\todo{INSERT COQ DEFINITION HERE}
We first describe the global structure of our proof (\ref{subsec:proof-structure}).
We introduce our translation of RFC~7748 (\ref{subsec:spec-rfc}) and specify
......@@ -86,37 +89,7 @@ This guarantees us the correctness of the implementation.
\subsection{A Correct Specification}
\label{subsec:spec-rfc}
TweetNaCl implements X25519 with numbers represented as arrays.
RFC~7748 defines X25519 over field elements. In order to simplify our proofs,
we define operations used in the ladder over generic types
\coqe{T} and \coqe{T'}. Those types are later instantiated as natural numbers,
integers, field elements, list of integers.
The generic definition of the ladder (\coqe{montgomery_rec}) and its parallel with
the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}.
It has to be noted that the RFC uses an additional variable to optimize the number
of \texttt{CSWAP} calls:
\emph{``Note that these formulas are slightly different from Montgomery's
original paper. Implementations are free to use any correct formulas.''}~\cite{rfc7748}.
We later prove our ladder correct in that respect (\sref{sec:maths}).
\coqe{montgomery_rec} only computes the ladder steps.
While the inversion, the packing, the unpacking (setting bit 255 to \texttt{0})
and the clamping are not defined in a generic manner, we show their equivalence
between the different representations.
Appendix~\ref{subsubsec:ZCryptoScalarmult} shows the instantiation of our ladder
over Integers (type \coqe{Z}). We call it \coqe{ZCrypto_Scalarmult}.
The modulo reduction is applied in \coqe{ZPack25519} translating every
underlying operations as over \Zfield. As a result this specification can be
interpreted as the formalization of X25519 in RFC~7748.
In appendix~\ref{subsubsec:CryptoScalarmult}, we show the the formalization of
\TNaCle{crypto_scalarmult} over lists of integers. We define it as
\Coqe{Crypto_Scalarmult} or \Coqe{CSM}. For the sake of space and simplicity we
do not display the definitions of each underlying function.
% The location of the definitions are listed in Appendix~\ref{appendix:proof-files}.
......
TEX := $(filter-out tweetverif.tex,$(wildcard *.tex))
FILES := $(TEX) $(wildcard tikz/*.tex) $(wildcard *.sty)
NO_COLOR="\033[0m"
RED = "\033[31m"
BRIGHTRED = "\033[91m"
YELLOW = "\033[93m"
ORANGE = "\033[33m"
GRAY = "\033[37m"
GREEN = "\033[32m"
BOLD = "\033[1m"
tweetverif.pdf: FORCE tweetverif.tex
@echo $(BOLD)$(GREEN)"Building tweetverif.pdf"$(NO_COLOR)
python3 latexrun.py tweetverif.tex
tweetverif.tex: FORCE $(FILES) collection.bib
@echo $(BOLD)$(YELLOW)"Generating tweetverif.tex"$(NO_COLOR)
python3 gen.py tweetverif.tex
......@@ -14,7 +26,7 @@ depend:
.PHONY: clean FORCE
clean:
@echo cleaning...
@echo $(BOLD)$(RED)"cleaning..."$(NO_COLOR)
@rm -fr latex.out 2> /dev/null || true
@rm *.pdf 2> /dev/null || true
@rm *.aux 2> /dev/null || true
......@@ -26,7 +38,9 @@ clean:
@rm *.fls 2> /dev/null || true
@rm *.log 2> /dev/null || true
@rm *.out 2> /dev/null || true
@rm *.bck 2> /dev/null || true
@rm */*.aux 2> /dev/null || true
@rm tweetverif.tex 2> /dev/null || true
spell:
for f in $(TEX) ; do \
......
......@@ -59,8 +59,8 @@ def main():
files = [x for x in glob.glob("**/*.tex", recursive=True) if not is_ignored(x) and is_tex(x) and not (x == fn) and is_not_tikz(x)]
for f in files:
print(f)
# for f in files:
# print(f)
main = [x for x in files if not is_appendix(x)]
appendices = [x for x in files if is_appendix(x)]
......@@ -76,12 +76,12 @@ def main():
for f in appendices:
appendix_output += " \\input{{{}}}\n".format(f)
output = read('_head.tex')
output = read('_' + fn)
output = output.replace('\\intput{main}\n', '$main_output')
output = output.replace('\\intput{appendix}\n', '$appendix_output')
output = Template(output)
output = output.safe_substitute(main_output = main_output, appendix_output = appendix_output)
print(output)
# print(output)
save(fn, output)
......
......@@ -38,6 +38,8 @@
{\color{red} \bf TODO: #1}
}
\newenvironment{informaltheorem}{\bigskip\itshape\noindent}{\bigskip}
\floatstyle{ruled}
\newfloat{Listing}{htb}{lst}
\floatstyle{plain}
......
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