Commit d33cbd71 authored by benoit's avatar benoit
Browse files

start to integrates comments

parent 9420810b
......@@ -38,7 +38,7 @@ to our RFC formalization.
This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-Appel}
to establish a link between C and Coq.
VST uses separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
to show that the semantics of the program satisfy a functional specification in Coq.
to show that the semantics of the program satisfies a functional specification in Coq.
To the best of our knowledge, this is the first time that VST
is used in the formal proof of correctness of an implementation
of an asymmetric cryptographic primitive.
......@@ -28,7 +28,7 @@ are isomorphic via $(x,y) \mapsto (x, \sqrt{b/b'} \cdot y)$.
Points in $M_{a,b}(\K)$ can be equipped with a structure of an abelian group
with the addition operation $+$ and with neutral element the point at infinity $\Oinf$.
For a point $P \in M_{a,b}(\K)$ and a positive integer $n$ we obtain the scalar product
$$n\cdot P = \underbrace{P + \cdots + P}_{n\text{ times}}.$$
$$n\cdot P = \underbrace{P + \cdots + P}_{n\text{ times}}.$$
In order to efficiently compute the scalar multiplication we use an algorithm
similar to square-and-multiply: the Montgomery ladder where the basic operations
......@@ -40,13 +40,13 @@ $(X : Z)$, with $x = X/Z$; the point at infinity is represented as $(1:0)$.
See \sref{subsec:ECC-projective} for more details.
We define the operation:
\texttt{xDBL\&ADD} &: (x_{Q-P}, (X_P:Z_P), (X_Q:Z_Q)) \mapsto \\
&((X_{2 \cdot P}:Z_{2 \cdot P}), (X_{P + Q}:Z_{P + Q}))
\texttt{xDBL\&ADD} & : (x_{Q-P}, (X_P:Z_P), (X_Q:Z_Q)) \mapsto \\
& ((X_{2 \cdot P}:Z_{2 \cdot P}), (X_{P + Q}:Z_{P + Q}))
In the Montgomery ladder, % notice that
% the arguments of \texttt{xADD} and \texttt{xDBL}
the arguments $P$ and $Q$ of \texttt{xDBL\&ADD}
are swapped depending of the value of the $k^{\text{th}}$ bit.
are swapped depending on the value of the $k^{\text{th}}$ bit.
We use a conditional swap \texttt{CSWAP} to change the arguments of the above
function while keeping the same body of the loop. \label{cswap}
Given a pair $(P_0, P_1)$ and a bit $b$, \texttt{CSWAP} returns the pair
......@@ -55,20 +55,20 @@ $(P_b, P_{1-b})$.
By using the differential addition and doubling operations we define the Montgomery ladder
computing a \xcoord-only scalar multiplication (see \aref{alg:montgomery-ladder}).
\caption{Montgomery ladder for scalar mult.}
\REQUIRE{\xcoord $x_P$ of a point $P$, scalar $n$ with $n < 2^m$}
\ENSURE{\xcoord $x_Q$ of $Q = n \cdot P$}
\STATE $Q = (X_Q:Z_Q) \leftarrow (1:0)$
\STATE $R = (X_R:Z_R) \leftarrow (x_P:1)$
\FOR{$k$ := $m$ down to $1$}
\caption{Montgomery ladder for scalar mult.}
\REQUIRE{\xcoord $x_P$ of a point $P$, scalar $n$ with $n < 2^m$}
\ENSURE{\xcoord $x_Q$ of $Q = n \cdot P$}
\STATE $Q = (X_Q:Z_Q) \leftarrow (1:0)$
\STATE $R = (X_R:Z_R) \leftarrow (x_P:1)$
\FOR{$k$ := $m$ down to $1$}
\STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$
% \STATE $Q \leftarrow \texttt{xDBL}(Q)$
% \STATE $R \leftarrow \texttt{xADD}(x_P,Q,R)$
\STATE $(Q,R) \leftarrow \texttt{xDBL\&ADD}(x_P,Q,R)$
\STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$
......@@ -23,7 +23,7 @@ This operation is often called ``clamping'' of the scalar $n$.
Note that $n' \in 2^{254} + 8\{0,1,\ldots,2^{251}-1\}$.
X25519 then computes the \xcoord of $n'\cdot P$.
RFC~7748~\cite{rfc7748} standardize the X25519 Diffie–Hellman key-exchange algorithm.
RFC~7748~\cite{rfc7748} standardizes the X25519 Diffie–Hellman key-exchange algorithm.
Given the base point $B$ where $X_B=9$, each party generates a secret random number
$s_a$ (respectively $s_b$), and computes $X_{P_a}$ (respectively $X_{P_b}$), the
\xcoord of $P_A = s_a \cdot B$ (respectively $P_B = s_b \cdot B$).
......@@ -128,7 +128,13 @@ Here are a few linear comments:
\item \textbf{page 6, column 1:}\\
In ListofZn\_fp $\rightarrow$ The use of fuel might deserve a comment. Don't you end up having to prove at some point that you can always compute ahead of time an overapproximation of the fuel needed? Wouldn't it have been simple to use the strong recursion principle of naturals to define the function?
In our case the fuel is used to garantee to have as an output a list of 32 elements. This allows to prove that for all List of 32 bytes, ListofZn\_fp (ZofList L) = L. With this lemma at hand we can later simplify some of the expressions.
\item \textbf{page 6, column 2:}\\
"and the same code as a pure Coq function" $\rightarrow$ I would rephrase, the term "same code" is misleading.
Specification: I think explaining the structure of a VST statement would be necessary to help an unfamiliar reader understand this specification.
Markdown is supported
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