\subsection{The X25519 key exchange}
\label{subsec:X25519-key-exchange}

From now on let $\F{p}$ be the field with $p=2^{255}-19$ elements.
We consider the elliptic curve $E$ over $\F{p}$ defined by the
equation $y^2 = x^3 + 486662 x^2 + x$.
For every $x \in \F{p}$ there exists a point $P$ in $E(\F{p^2})$
such that $x$ is the \xcoord of $P$.

The core of the X25519 key-exchange protocol is a scalar\hyp{}multiplication
function, which we will also refer to as X25519.
This function receives as input two arrays of $32$ bytes each.
One of them is interpreted as the little-endian encoding of a
non-negative 256-bit integer $n$ (see \ref{sec:Coq-RFC}).
The other is interpreted as the little-endian encoding of
the \xcoord $x_P \in \F{p}$ of a point in $E(\F{p^2})$,
using the standard mapping of integers modulo $p$ to elements in $\F{p}$.

The X25519 function first computes a scalar $n'$ from $n$ by setting
bits at position 0, 1, 2 and 255 to \texttt{0}; and at position 254
to \texttt{1}.
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.
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$).
The parties exchange $X_{P_a}$ and $X_{P_b}$ and compute their shared secret
$s_a \cdot  s_b \cdot B$ with
X25519 on $s_a$ and $X_{P_b}$ (respectively $s_b$ and $X_{P_a}$).