+The X448 function is fully specified in RFC7748 \cite{rfc7748}. It uses a
+carefully chosen elliptic curve named `Ed448-Goldilocks', introduced by
+Hamburg in \cite{cryptoeprint:2015:625}, over the finite field $k =
+\gf{p^2}$, where $p = 2^{448} - 2^{224} - 1$, specifically,
+\[ E(k) = \{\, (X : Y : Z) \mid Y^2 Z = X^3 + 156326 X^2 Z + X Z^2 \,\}
+ \padm.
+\]
+\cite{rfc7748} completely defines X448 as a function on 56-octet strings.
+
+Thus, $D = \id{x448}$ is a Diffie--Hellman group as follows. Both the
+scalars and group are simply the set of all octet strings of length~56; i.e.,
+$D.S = D.G = \octet^{56}$. The generator is the point $D.P = [5, 0, \ldots,
+0]$.
+
+\begin{itemize}
+\item The Diffie--Hellman operation is the X448 operation: $D.\id{dh}(x, Y) =
+ \id{X448}(x, Y)$.
+\item By design, X448 is specified and secure for all possible public-key
+ values; hence $D.\id{validp}(X) = \t$ for all $X \in D.G$.
+\item Group elements are already fixed-length octet strings. All three
+ group-element encodings are therefore the identity function; i.e.,
+ $D.\id{ge-public} = D.\id{ge-secret} = D.\id{ge-hash} = X$.
+\item Scalars are already fixed-length octet strings. The scalar encoding is
+ therefore the identity function, i.e., $D.\id{sc}.\id{enc}(x) = x$; and
+ $D.\id{scsz} = 56$.
+\end{itemize}
+
+%%%--------------------------------------------------------------------------
+\section{Bulk transforms} \label{sec:bulk}
+
+\subsection{Operations} \label{sec:bulk.ops}
+
+A \emph{bulk transform}~$T$ consists of a number of parameters and
+operations, as follows.
+\begin{itemize}
+\item A safe \emph{data limit} $E.\id{n-limit} > 0$; see \xref{sec:bulk.ops}.
+\item A \emph{key-generation operation} $T.\id{gen}$. Given an octet string
+ $z \in \octet^*$, $T.\id{gen}$ derives and returns the cryptographic key~$K
+ = T.\id{gen}(z)$ required by $T.E$ and $T.D$, which are described below.
+ \begin{aside}
+ Throughout the protocol, $x$ will be a public contribution from the
+ sender, $y$ a public contribution from the recipient (or empty), and $z$
+ a shared secret known only to both.
+ \end{aside}
+\item An \emph{encryption operation} $T.E$. Given a key~$K$ returned by
+ $T.\id{gen}$, a message type code $0 \le c < 2^{32}$, a sequence number $0
+ \le i < 2^{32}$, and a message~$m \in \octet^*$, $T.E$ computes and returns
+ a ciphertext $y = T.E(K, c, i, m) \in \octet^*$
+\item A \emph{decryption operation} $T.D$. Given a key~$K$ returned by
+ $T.\id{gen}$, a message type code $0 \le c < 2^{32}$, and a ciphertext $y
+ \in \octet^*$, $T.D$ attempts to decrypt the ciphertext, returning a pair
+ $(i, m) = T.D(K, c, y)$. If the operation succeeds, $0 \le i < 2^{32}$ is
+ a sequence number, and $m \in \octet^*$ is the decrypted message;
+ otherwise, $i = 0$ and $m \in \syms$. For correctness, for any key~$K$
+ returned by $T.\id{gen}$, any $0 \le c < 2^{32}$, any $0 \le i < 2^{32}$,
+ and any $m \in \octet^*$, it must hold that $T.D(K, c, T.E(K, c, i, m)) =
+ (i, m)$.
+\end{itemize}
+\begin{aside}
+ The security of an encryption scheme tends to degrade as more data is
+ encrypted with a single key. The data limit is chosen to keep the
+ probability of a `bad event' which compromises data security below
+ $2^{-40}.$
+\end{aside}
+
+
+\subsection{The \cookie{v0} transform} \label{sec:bulk.v0}
+
+Let $E$ be a symmetric encryption scheme, let $M$ be a message authentication
+code, and let $H$ be a hash function, such that
+\begin{itemize}
+\item $H.\id{hsz} \ge E.\id{ksz}$, and
+\item $H.\id{hsz} \ge M.\id{ksz}$.
+\end{itemize}
+The \cookie{v0} transform $T = \id{tx-v0}(E, M, H)$ is defined as follows.
+\begin{itemize}
+\item $T.\id{n-limit} = E.\id{n-limit}$.
+\item If $z$ is an octet string, then $K = T.\id{gen}(z)$ is determined as
+ follows.
+ \begin{enumerate}
+ \item Let $K_E = H.\id{hash}(\texttt{"tripe-encryption"} \cat [0] \cat z)[0
+ \upto E.\id{ksz}]$.
+ \item Let $K_M = H.\id{hash}(\texttt{"tripe-integrity"} \cat [0] \cat z)[0
+ \upto M.\id{ksz}]$.
+ \item Then $K = (K_E, K_M)$.
+ \end{enumerate}
+\item If $K = (K_E, K_M) \in \octet^{E.\id{ksz}} \times
+ \octet^{M.\id{ksz}}$, $0 \le c < 2^{32}$, $0 \le i < 2^{32}$, and $m \in
+ \octet^*$, then $y = T.E(K, c, i, m)$ is determined as follows.
+ \begin{enumerate}
+ \item \label{en:bulk.v0.encrypt-iv} Choose $v$ uniformly at random from
+ $\octet^{E.\id{ivsz}}$.
+ \item Let $y_0 = E.E(K_E, v, m)$.
+ \item Let $t = M.\id{tag}(K_M, [c]_4 \cat [i]_4 \cat v \cat y_0)$.
+ \item Finally, $y = t \cat [i]_4 \cat v \cat y_0$.
+ \end{enumerate}
+\item If $K = (K_E, K_M) \in \octet^{E.\id{ksz}} \times \octet^{M.\id{ksz}}$,
+ $0 \le c < 2^{32}$, and $y \in \octet^*$, then $(i, m) = T.D(K, c, y)$ are
+ determined as follows.
+ \begin{enumerate}
+ \item If $\len(y) < M.\id{tsz} + 4 + E.\id{ivsz}$ then set $i = 0$ and $m =
+ \cookie{err-malformed}$, and go to step~\ref{en:bulk.v0.decrypt-done}.
+ \item Let $t = y[0 \upto M.\id{tsz}]$; let $i_0 = y[M.\id{tsz} \upto
+ M.\id{tsz} + 4]$; let $v = y[M.\id{tsz} + 4 \upto M.\id{tsz} +
+ E.\id{ivsz} + 4]$; let $y_0 = y[M.\id{tsz} + E.\id{ivsz} + 4 \upto
+ \len(y)]$.
+ \item If $t \ne M.\id{tag}(K_M, [c]_4 \cat i_0 \cat v \cat y_0)$ then set
+ $i = 0$ and $m = \cookie{err-tag}$, and go to
+ step~\ref{en:bulk.v0.decrypt-done}.
+ \item Let $0 \le i < 2^{32}$ be the unique integer such that $[i]_4 = i_0$.
+ \item Let $m = E.D(K_E, v, y_0)$.
+ \item \label{en:bulk.v0.decrypt-done} Return $i$ and $m$.
+ \end{enumerate}
+\end{itemize}
+The random selection of~$v$ in step~\ref{en:bulk.v0.encrypt-iv} of $T.E$
+above admits the possibility of kleptographic leakage of secrets by a
+malicious implementation. This transform is therefore deprecated.
+
+
+\subsection{The \cookie{iiv} transform} \label{sec:bulk.iiv}
+
+Let $E$ be a symmetric encryption scheme, let $M$ be a message authentication
+code, let $B$ be a blockcipher, and let $H$ be a hash function, such that
+\begin{itemize}
+\item $H.\id{hsz} \ge E.\id{ksz}$,
+\item $H.\id{hsz} \ge M.\id{ksz}$,
+\item $H.\id{hsz} \ge B.\id{ksz}$,
+\item $B.\id{bsz} \ge 4$, and
+\item $B.\id{bsz} \ge E.\id{ivsz}$.
+\end{itemize}
+The \cookie{iiv} (`implicit IV') transform $T = \id{tx-iiv}(E, M, B, H)$ is
+defined as follows.
+\begin{itemize}
+\item $T.\id{n-limit} = E.\id{n-limit}$.
+\item If $z$ is an octet string, then $K = T.\id{gen}(z)$ is determined as
+ follows.
+ \begin{enumerate}
+ \item Let $K_B = H.\id{hash}(\texttt{"tripe-blkc"} \cat [0] \cat z)[0 \upto
+ B.\id{ksz}]$.
+ \item Let $K_E = H.\id{hash}(\texttt{"tripe-encryption"} \cat [0] \cat z)[0
+ \upto E.\id{ksz}]$.
+ \item Let $K_M = H.\id{hash}(\texttt{"tripe-integrity"} \cat [0] \cat z)[0
+ \upto M.\id{ksz}]$.
+ \item Then $K = (K_B, K_E, K_M)$.
+ \end{enumerate}
+\item If $K = (K_B, K_E, K_M) \in \octet^{B.\id{ksz}} \times
+ \octet^{E.\id{ksz}} \times \octet^{M.\id{ksz}}$, $0 \le c < 2^{32}$, $0 \le
+ i < 2^{32}$, and $m \in \octet^*$, then $y = T.E(K, c, i, m)$ is determined
+ as follows.
+ \begin{enumerate}
+ \item Set $v = B.E([i]_{B.\id{bsz}})[0 \upto E.\id{ivsz}]$.
+ \item Let $y_0 = E.E(K_E, v, m)$.
+ \item Let $t = M.\id{tag}(K_M, [c]_4 \cat [i]_4 \cat y_0)$.
+ \item Finally, $y = t \cat [i]_4 \cat y_0$.
+ \end{enumerate}
+\item If $K = (K_B, K_E, K_M) \in \octet^{B.\id{bsz}} \times
+ \octet^{E.\id{ksz}} \times \octet^{M.\id{ksz}}$, $0 \le c < 2^{32}$, and $y
+ \in \octet^*$, then $(i, m) = T.D(K, c, y)$ are determined as follows.
+ \begin{enumerate}
+ \item If $\len(y) < M.\id{tsz} + 4$ then set $i = 0$ and $m =
+ \cookie{err-malformed}$, and go to step~\ref{en:bulk.iiv.decrypt-done}.
+ \item Let $t = y[0 \upto M.\id{tsz}]$; let $i_0 = y[M.\id{tsz} \upto
+ M.\id{tsz} + 4]$; let $y_0 = y[M.\id{tsz} + 4 \upto \len(y)]$.
+ \item If $t \ne M.\id{tag}(K_M, [c]_4 \cat i_0 \cat y_0)$ then set $i = 0$
+ and $m = \cookie{err-tag}$, and go to
+ step~\ref{en:bulk.iiv.decrypt-done}.
+ \item Let $0 \le i < 2^{32}$ be the unique integer such that $[i]_4 = i_0$.
+ \item Set $v = B.E([i]_{B.\id{bsz}})[0 \upto E.\id{ivsz}]$.
+ \item Let $m = E.D(K_E, v, y_0)$.
+ \item \label{en:bulk.iiv.decrypt-done} Return $i$ and $m$.
+ \end{enumerate}
+\end{itemize}
+
+
+\subsection{The \cookie{naclbox} transform} \label{sec:bulk.naclbox}
+
+Let $f$ be $\id{salsa20}$ or $\id{chacha}$, and $r$ be a nonnegative even
+integer, let $k$ be 16 or 32, and let $H$ be a hash function, such that
+$H.\id{hsz} \ge k$. The \cookie{naclbox} transform $T = \id{tx-naclbox}(f,
+r, k, H)$ is defined as follows.
+\begin{itemize}
+\item $T.\id{n-limit} = 2^{134}$.
+ \begin{aside}
+ I'm not aware of any especially useful data limit for Salsa20 or ChaCha,
+ so this is just an upper bound on the amount of data which can be
+ encrypted with a single key.
+ \end{aside}
+\item If $z$ is an octet string, then $T.\id{gen}(z) =
+ H.\id{hash}(\texttt{"tripe-encryption"} \cat [0] \cat z)[0 \upto k]$.
+\item If $K \in \octet^k$, $0 \le c < 2^{32}$, $0 \le i < 2^{32}$, and $m
+ \in \octet^*$, then $y = T.E(K, c, i, m)$ is determined as follows.
+ \begin{enumerate}
+ \item Set $v = [i]_4 \cat [c]_4$.
+ \item Let $u = f(K, r, v, \len(m) + 32)$.
+ \item Let $y_0 = m \xor u[32 \upto \len(u)]$.
+ \item Let $r = u[0 \upto 16]$, and $s = u[16 \upto 32]$.
+ \item Let $t = \id{poly1305}(r, s, y_0)$.
+ \item Finally, $y = t \cat [i]_4 \cat y_0$.
+ \end{enumerate}
+\item If $K \in \octet^k$, $0 \le c < 2^{32}$, and $y \in \octet^*$, then
+ $(i, m) = T.D(K, c, y)$ are determined as follows.
+ \begin{enumerate}
+ \item If $\len(y) < 20$ then set $i = 0$ and $m = \cookie{err-malformed}$
+ and go to step~\ref{en:bulk.naclbox.decrypt-done}.
+ \item Let $t = y[0 \upto 16]$; let $i_0 = y[16 \upto 20]$; let $y_0 = y[20
+ \upto \len(y)]$.
+ \item Set $v = i_0 \cat [c]_4$.
+ \item Let $u = f(K, r, v, \len(m) + 32)$.
+ \item Let $r = u[0 \upto 16]$, and $s = u[16 \upto 32]$.
+ \item If $t \ne \id{poly1305}(r, s, y_0)$ then set $i = 0$ and $m =
+ \cookie{err-tag}$, and go to step~\ref{en:bulk.naclbox.decrypt-done}.
+ \item Let $0 \le i < 2^{32}$ be the unique integer such that $[i]_4 = i_0$.
+ \item Let $m = y_0 \xor u[32 \upto \len(u)]$.
+ \item \label{en:bulk.naclbox.decrypt-done} Return $i$ and $m$.
+ \end{enumerate}
+\end{itemize}
+
+%%%--------------------------------------------------------------------------
+\section{High-level protocol structure} \label{sec:highlev}
+
+\subsection{Message structure} \label{sec:highlev.msg}
+
+TrIPE messages are transmitted over UDP \cite{rfc768}. Where a fixed port
+number is wanted, implementations should use port~4070, which has been
+allocated by IANA.
+
+The first octet of a packet holds a type code. The interpretation of the
+remaining octets depends on the type code. The defined type codes are
+summarized in \xref{tab:highlev.msgtype}. Message codes in the range
+240--255 are reserved for implementation-specific features and experiments.
+\begin{table}
+ \begin{tabular}[C]{|l|c|c|} \hlx{hv}
+ \textbf{Name} & \textbf{Code} & \textbf{Section} \\ \hlx{vhv}
+ MSG\_PACKET & $\hex{00}$ & \ref{sec:xfer.packet} \\ \hlx{vhv}
+ KX\_PRECHAL & $\hex{10}$ & \ref{sec:keyexch.prechal} \\ \hlx{v}
+ KX\_CHAL & $\hex{11}$ & \ref{sec:keyexch.chal} \\ \hlx{v}
+ KX\_REPLY & $\hex{12}$ & \ref{sec:keyexch.reply} \\ \hlx{v}
+ KX\_SWITCH & $\hex{13}$ & \ref{sec:keyexch.switch} \\ \hlx{v}
+ KX\_SWITCHOK & $\hex{14}$ & \ref{sec:keyexch.switchok} \\ \hlx{vhv}
+ MISC\_NOP & $\hex{20}$ & \ref{sec:misc.nop} \\ \hlx{v}
+ MISC\_PING & $\hex{21}$ & \ref{sec:misc.ping} \\ \hlx{v}
+ MISC\_PONG & $\hex{22}$ & \ref{sec:misc.pong} \\ \hlx{v}
+ MISC\_EPING & $\hex{23}$ & \ref{sec:misc.eping} \\ \hlx{v}
+ MISC\_EPONG & $\hex{24}$ & \ref{sec:misc.epong} \\ \hlx{v}
+ MISC\_GREET & $\hex{25}$ & \ref{sec:misc.greet} \\ \hlx{vh}
+ \end{tabular}
+ \caption{Defined message types} \label{tab:highlev.msgtype}
+\end{table}
+
+In general, messages do not identify the sending or receiving peers
+explicitly; instead, these are implied by the IP addresses and port numbers
+in the encapsulating datagram.
+
+
+\subsection{Keysets} \label{sec:highlev.keyset}
+
+A \emph{keyset}~$S$ is an object with components
+\begin{itemize}
+\item a bulk transform $S.T$;
+\item bulk-transform keys $S.K_T$ and $S.K_R$;
+\item a next outgoing sequence number $0 \le S.i_T \le 2^{32}$;
+\item a set $S.I_R \subseteq 2^{\{i\in\Z\mid0\le i<2^{32}\}}$, which is a
+ conservative approximation of the set of seen incoming sequence numbers;
+\item an integer~$n \ge 0$;
+\item a pair of times $\id{t-limit}$ and $\id{t-exch}$;
+\item a pair of integers $\id{n-limit}$ and $\id{n-exch}$; and
+\item a flag $\id{kx-queued-p} \in \{ \nil, \t \}$.
+\end{itemize}
+
+\subsubsection{Initialization}
+The operation $\id{init-keyset}$ constructs a new keyset~$S$ given a bulk
+transform~$T$ and three octet strings~$x$, $y$, and $z$. The operation
+$\id{init-keyset}$ proceeds as follows.
+\begin{enumerate}
+\item $S.T = T$.
+\item $S.K_T = T.\id{gen}(x \cat y \cat z)$; $S.K_R = T.\id{gen}(y \cat x
+ \cat z)$.
+\item $S.i_T = 0$.
+\item $S.I_R = \emptyset$.
+\item $S.n = 0$.
+\item $S.\id{t-limit}$ is the time one hour into the future; $S.\id{t-exch}$
+ is a random time between thirty and fifty minutes hour into the future.
+ \begin{aside}
+ The randomization breaks symmetry. If both peers re-initiate key
+ exchange simultaneously, then the key-exchange protocol may take twice as
+ many round trips as would normally be necessary.
+ \end{aside}
+\item $S.\id{n-limit} = T.\id{n-limit}$; $S.\id{n-exch} = \lfloor
+ T.\id{n-limit}/2 \rfloor$.
+\item $S.\id{kx-queued-p} = \nil$.
+\end{enumerate}
+
+\subsubsection{Encryption and decryption}
+The operation $\id{encrypt}$ encrypts a message~$m \in \octet^*$, given a
+keyset~$S$ and a message type code $0 \le c < 2^{32}$, returning a ciphertext
+or failure indicator $y \in \lift{\octet^*}$. The operation $\id{encrypt}(S,
+c, m)$ proceeds as follows.
+\begin{enumerate}
+\item If $S.\id{t-exch}$ is in the past, or $S.n \le S.\id{n-exch} < S.n +
+ \len(m)$, or $S.i_T = 2^{31}$, and $S.\id{kx-queued-p} = \nil$, then
+ \begin{enumerate}
+ \item initiate a fresh key-exchange with the peer
+ (\xref{sec:keyexch.init}); and
+ \item update $S.\id{kx-queued-p} \gets \t$.
+ \end{enumerate}
+\item If $S.\id{t-limit}$ is in the past, or $S.\id{n-limit} < S.n +
+ \len(m)$, or $S.i_T = 2^{32}$, then return $\cookie{err-expired}$.
+\item Let $y = S.T.E(S.K_T, c, S.i_T, m)$.
+\item Update $S.i_T \gets S.i_T + 1$.
+\item Update $S.n \gets S.n + \len(m)$.
+\item Return $y$.
+\end{enumerate}
+
+The operation $\id{decrypt}$ decrypts a ciphertext~$y \in \octet^*$, given a
+keyset~$S$ and a message type code $0 \le c < 2^{32}$, returning a message or
+failure indicator $m \in \lift{\octet^*}$. The operation $\id{decrypt}(S, c,
+y)$ proceeds as follows.
+\begin{enumerate}
+\item Let $(i, m) = S.T.D(S.K_R, c, y)$.
+\item If $m \in \syms$ then return $m$.
+ \begin{aside}
+ There are many reasons this might fail, not necessarily as a result of
+ enemy action. \fixme{discussion}
+ \end{aside}
+\item If $i \in S.I_R$ then return $\cookie{err-replay}$.
+ \begin{aside}
+ The message is a replay. This may indicate an attack; conscientious
+ implementations will report this in a log.
+ \end{aside}
+\item Update $S.I_R \gets \id{upd-seq}(S.I_R, i)$. The detailed choice of
+ the function $\id{upd-seq}$ is implementation specific, but the following
+ properties must hold, so as to cope reliably with a limited amount of
+ packet reordering by the network while strictly forbidding message replay.
+ In the following, let $I' = I \cup \{ i \}$, and let $\hat{\imath} = \max
+ I'$.
+ \begin{itemize}
+ \item It must be a conservative approximation to the union operation:
+ $I' \subseteq \id{upd-seq}(I, i)$.
+ \item It must not include sequence numbers beyond the largest seen so far:
+ $\max \id{upd-seq}(I, i) = \hat{\imath}$.
+ \item It must accurately reflect the state of the 31 sequence numbers
+ preceding the largest seen so far: $j \in \id{upd-seq}(I, i) \iff j \in
+ I'$ for $\hat{\imath} - 32 < j < \hat{\imath}$.
+ \end{itemize}
+\item Return $m$.
+\end{enumerate}
+
+%%%--------------------------------------------------------------------------
+\section{Key exchange} \label{sec:keyexch}
+
+This is the most complicated part of the TrIPE protocol.
+
+Key exchange occurs between a pair of peers. Key exchange is symmetrical, so
+it is described from the point of view of one peer.
+
+
+\subsection{Key exchange state} \label{sec:keyexch.state}
+
+An implementation maintains its \emph{key-exchange state} in an object~$X$,
+with components
+\begin{itemize}
+\item a Diffie--Hellman group $X.D$;
+\item a hash function $X.H$;
+\item the implementation's own private key $X.a \in X.D.S$;
+\item the implementation's own public key $X.A \in X.D.G$;
+\item its peer's public key $X.B \in X.D.G$;
+\item a pending keyset $X.S$;
+\item an ephemeral secret $X.r \in X.D.S$;
+\item a corresponding ephemeral group element $X.R \in X.D.G$; and
+\item a flag $X.\id{activep} \in \{ \nil, \t \}$.
+\end{itemize}
+A pair of peers must be configured with the same Diffie--Hellman group and
+hash. If an implementation's private key is $X.a$, then its public key $X.A
+= X.D.\id{dh}(X.a, X.D.P)$.
+
+The initial pending keyset~$X.S$ and ephemeral values~$X.r$ and $X.R$ may be
+arbitrary; initially, $X.\id{activep} = \nil$.
+
+
+\subsection{Initiating key exchange} \label{sec:keyexch.init}
+
+Key exchange can be initiated in several ways:
+\begin{itemize}
+\item when a peer starts up, because it has no established keyset;
+\item when the $\id{encrypt}$ operation (\xref{sec:highlev.keyset})
+ determines that a keyset needs replacing;
+\item when a peer receives KX\_PRECHAL (\xref{sec:keyexch.prechal}) and no
+ key exchange is currently in progress.
+\end{itemize}
+The procedure to initiate key-exchange is as follows.
+\begin{enumerate}
+\item If $X.\id{activep} = \t$, then there is nothing to do: return
+ immediately.
+\item Select a new ephemeral secret $r \in X.S$ uniformly at random; update
+ $X.r \gets r$ and $X.R \gets X.D.\id{dh}(X.r, X.D.P)$.
+\item Update $X.\id{activep} \gets \t$.
+\item If key-exchange was not initiated as a result of an incoming
+ KX\_PRECHAL message, then send KX\_PRECHAL \xref{sec:keyexch.prechal}.
+\end{enumerate}
+
+
+\subsection{Utility functions} \label{sec:keyexch.util}
+
+The following definitions will be used throughout the key-exchange
+subprotocol.
+
+\subsubsection{Challenge cookie construction}
+Let $R' \in X.D.G$ be a group element; then define $\id{challenge-cookie}(R')
+= X.H.\id{hash}(\texttt{"tripe-cookie"} \cat [0] \cat
+X.D.\id{ge-hash}.\id{enc}(R'))$.
+
+\subsubsection{Expected-reply hash}
+Let $A, R', R, U \in X.D.G$ be group elements; then
+\[ \id{expected-reply-hash}(A, R', R, U) =
+ X.H.\id{hash}(\begin{eqnalign}[l<{{}}][t]
+ \texttt{"tripe-expected-reply"} \cat [0] \cat \\
+ X.D.\id{ge-hash}.\id{enc}(A) \cat \\
+ X.D.\id{ge-hash}.\id{enc}(R') \cat \\
+ X.D.\id{ge-hash}.\id{enc}(R) \cat \\
+ X.D.\id{ge-hash}.\id{enc}(U)) \padm.
+ \end{eqnalign}
+\]
+
+\subsubsection{Check-value construction}
+Let $R' \in X.D.G$ be a group element; then $\id{make-check-value}(R')$ is
+defined as follows.
+\begin{enumerate}
+\item Let $U = X.D.\id{dh}(X.r, X.B)$.
+\item Let $h = \id{expected-reply-mask}(X.A, R', X.R, U)$.
+\item Then $\id{make-check-value}(R') = X.D.\id{sc}.\id{enc}(X.r)
+ \xor \id{mgf}(X.H, h, X.D.\id{scsz})$.
+\end{enumerate}
+
+\subsubsection{Check-value verification}
+Let $R' \in X.D.G$ be a group element and $c \in \octet^{X.D.\id{scsz}}$ an
+octet string; then $\id{check-value-ok-p}(R', c)$ is defined as follows.
+\begin{enumerate}
+\item Let $U = X.D.\id{dh}(X.a, R')$.
+\item Let $h = \id{expected-reply-mask}(X.B, X.R, R', U)$.
+\item Let $(r', c') = X.D.\id{sc}.\id{dec}(c \xor \id{mgf}(X.H, h,
+ X.D.\id{scsz}))$.
+\item If $r' \in X.D.S$ and $c' = \emptystring$ and $X.D.\id{dh}(r', X.D.P) =
+ R'$ then $\id{check-value-ok-p}(R', c) = \t$; otherwise
+ $\id{check-value-ok-p}(R', c) = \nil$.
+\end{enumerate}
+
+
+\subsection{The prechallenge message KX\_PRECHAL} \label{sec:keyexch.prechal}
+
+\subsubsection{Transmission}
+Sending KX\_PRECHAL proceeds as follows.
+\begin{enumerate}
+\item Let $m' = [\hex{10}] \cat X.D.\id{ge-public}.\id{enc}(X.R)$.
+\item Transmit $m'$ to the peer.
+\end{enumerate}
+
+\subsubsection{Retransmission}
+An implementation should retransmit KX\_PRECHAL message periodically while
+key-exchange is active. The following strategy is recommended. Add a new
+component $X.t$ to the state. When key exchange is initiated, initialize
+$X.t = 2$. Perform the following procedure at key-exchange initiation, and
+at every retransmission.
+\begin{enumerate}
+\item If $X.\id{activep} = \nil$, then do nothing and return.
+\item Select $t$ at random between $5/6\,X.t$ and $7/6\,X.t$.
+\item Schedule retransmission $t$ seconds into the future.
+\item Update $X.t \gets \min(5/4\,X.t, 300)$.
+\end{enumerate}
+
+\subsubsection{Reception}
+On receipt of a KX\_PRECHAL message $m'$, perform the following procedure.
+\begin{enumerate}
+\item Set $m_0 = m'[1 \upto \len(m')]$. (We know $m' = [\hex{10}] \cat
+ m_0$.)
+\item Set $(R', m_1) = X.D.\id{ge-public}.\id{dec}(m_0)$. If $R' \in \syms$
+ then the message is malformed: discard it.
+\item If $m_1 \ne \emptystring$ then the message is malformed: discard it.
+\item Set $m = [\hex{11}] \cat X.D.\id{ge-public}.\id{enc}(X.R) \cat
+ \id{challenge-cookie}(R') \cat \id{make-check-value}(R')$.
+\item Transmit $m$ to the peer.
+\end{enumerate}
+
+
+\subsection{The challenge message KX\_CHAL} \label{sec:keyexch.chal}
+
+\subsubsection{Reception}
+On receipt of a KX\_CHAL message $m'$, perform the following procedure.
+\begin{enumerate}
+\item Set $m_0 = m'[1 \upto \len(m')]$. (We know $m' = [\hex{11}] \cat
+ m_0$.)
+\item Set $(R', m_1) = X.D.\id{ge-public}.\id{dec}(m_0)$. If $R' \in \syms$
+ then the message is malformed; discard it.
+\item If $\len(m_1) \ne X.H.\id{hsz} + X.D.\id{scsz}$ then the message is
+ malformed; discard it.
+\item Set $h' = m_1[0 \upto X.H.\id{hsz}]$ and $c' = m_1[X.D.\id{scsz} \upto
+ \len(m_1)]$.
+\item If $h' \ne \id{challenge-cookie}(X.R)$ then the message is malformed;
+ discard it.
+\item If $\id{check-value-ok-p}(R', c') \ne \t$ then the message is
+ malformed; discard it.
+\item Set $Z = X.D.\id{dh}(X.r, R')$.
+ \fixme{Need per-challenge state.}
+\end{enumerate}
+
+%%%--------------------------------------------------------------------------
+\section{Message transfer} \label{sec:xfer}
+
+\fixme{describe}
+
+%%%--------------------------------------------------------------------------
+\section{Miscellaneous protocol aspects} \label{sec:misc}
+
+\subsection{No-operation (keepalive)} \label{sec:misc.nop}
+\fixme{describe}
+
+\subsection{Transport and encrypted ping} \label{sec:misc.ping}
+\fixme{describe}
+
+\subsection{Greetings} \label{sec:misc.greet}
+\fixme{describe}
+
+\subsection{Tokens and knocking} \label{sec:misc.knock}
+\fixme{describe}
+
+%%%----- Back matter --------------------------------------------------------
+
+\bibliography{mdw-crypto,eprint,rfc,%
+ cryptography1990,cryptography2000,cryptography2010,hash}
+
+\appendix
+
+%%%--------------------------------------------------------------------------
+\section{Summary of notation} \label{sec:notation}
+
+\begin{longtable}[c]{|l|p{10cm}|} \hlx{hv}
+ \textbf{Notation} & \textbf{Meaning} \\ \hlx{vh}
+ \endhead \hlx{bh}
+ \endfoot \hlx{v}
+
+ $\cookie{example}$ & A symbol. \\ \hlx{v}
+ $\syms$ & The set of symbols. \\ \hlx{v}
+ $\lift{A}$ & The set $A$ lifted to include
+ symbols. \\ \hlx{vh/v}
+
+ $\octet = \{ 0, 1, \dots, 255 \}$ &
+ The set of octets. \\ \hlx{v}
+ $\octet^*$ & The set of all octet strings. \\ \hlx{v}
+ $\octet^\ell$ & The set of octet strings of
+ length~$\ell$. \\ \hlx{v}
+ $\emptystring$ & The empty octet string. \\ \hlx{v}
+ $\ell = \len(x)$ & The length of an octet
+ string. \\ \hlx{v}
+ $x[i]$ & The $i$th octet of string~$x$ \\ \hlx{v}
+ $x[i \upto j]$ & The $(j - i)$-octet substring
+ of~$x$, starting at
+ position~$i$. \\ \hlx{v}
+ $x \cat y$ & The concatenation of $x$
+ and~$y$. \\ \hlx{v}
+ $x^n$ & The $n$-fold repetition of
+ $x$. \\ \hlx{v}
+ $x \bitand y$ & The bitwise and of $x$
+ and~$y$. \\ \hlx{v}
+ $x \bitor y$ & The bitwise (inclusive) or of
+ $x$ and~$y$. \\ \hlx{v}
+ $x \xor y$ & The bitwise exclusive-or of
+ $x$ and~$y$. \\ \hlx{v}
+ $[a_0, a_1, \ldots, a_{n-1}]$ & The $n$-octet string consisting
+ of octets $a_0$, $a_1$, \ldots,
+ $a_{n-1}$. \\ \hlx{v}
+ \texttt{"example"} & The octet string holding the
+ ASCII encoding of a text
+ string. \\ \hlx{v}
+ $[n]_\ell$ & The $\ell$-octet big-endian
+ encoding of $n$. \\ \hlx{v}
+ $[n]'_\ell$ & The $\ell$-octet little-endian
+ encoding of $n$. \\ \hlx{vh/v}
+
+ $\ell = \len(n)$ & The `length' of an integer. \\ \hlx{v}
+ $\hex{9c}$ & An integer in hexadecimal. \\ \hlx{vh/v}
+
+ $C$ & An encoding. \\ \hlx{v}
+ $C.\id{enc}$ & The encoding operation. \\ \hlx{v}
+ $C.\id{dec}$ & The decoding operation. \\ \hlx{vh/v}
+
+ $H$ & A hash function. \\ \hlx{v}
+ $H.\id{hsz}$ & The hash output size. \\ \hlx{v}
+ $H.\id{bsz}$ & The hash block size. \\ \hlx{v}
+ $h = H.\id{hash}(m)$ & The hashing operation. \\ \hlx{vh/v}
+
+ $B$ & A blockcipher (PRP). \\ \hlx{v}
+ $B.\id{ksz}$ & The blockcipher key size. \\ \hlx{v}
+ $B.\id{bsz}$ & The blockcipher block size. \\ \hlx{v}
+ $y = B.E(K, x)$ & The blockcipher encryption
+ operation. \\ \hlx{v}
+ $x = B.D(K, y)$ & The blockcipher decryption
+ operation. \\ \hlx{vh/v}
+
+ $E$ & A symmetric encryption
+ scheme. \\ \hlx{v}
+ $E.\id{ksz}$ & The symmetric encryption
+ key size. \\ \hlx{v}
+ $E.\id{ivsz}$ & The symmetric encryption
+ initialization vector size. \\ \hlx{v}
+ $y = E.E(K, v, m)$ & The symmetric encryption
+ operation. \\ \hlx{v}
+ $m = E.D(K, v, y)$ & The symmetric decryption
+ operation. \\ \hlx{vh/v}
+
+ $M$ & A message authentication
+ code (MAC). \\ \hlx{v}
+ $M.\id{ksz}$ & The MAC key size. \\ \hlx{v}
+ $M.\id{tsz}$ & The MAC tag size. \\ \hlx{v}
+ $t = M.\id{tag}(K, m)$ & The MAC tagging operation. \\ \hlx{vh/v}
+
+ $D$ & A Diffie--Hellman group. \\ \hlx{v}
+ $D.S$ & The set of scalars. \\ \hlx{v}
+ $D.G$ & The set of group elements. \\ \hlx{v}
+ $D.P$ & The well-known generator. \\ \hlx{v}
+ $D.\id{scsz}$ & The length of an encoded
+ scalar. \\ \hlx{v}
+ $Z = D.\id{dh}(x, Y)$ & The group operation. \\ \hlx{v}
+ $D.\id{ge-public}$ & The public group-element
+ encoding. \\ \hlx{v}
+ $D.\id{ge-secret}$ & The secret group-element
+ encoding. \\ \hlx{v}
+ $D.\id{ge-hash}$ & The group-element encoding
+ for hashing. \\ \hlx{v}
+ $D.\id{sc}$ & The scalar encoding. \\ \hlx{vh/v}
+
+ $T$ & A bulk transform. \\ \hlx{v}
+ $K = T.\id{gen}(x, y, z)$ & The bulk transform
+ key-generation operation. \\ \hlx{v}
+ $y = T.E(K, i, c, m)$ & The bulk transform encryption
+ operation. \\ \hlx{v}
+ $(i, m) = T.D(K, c, y)$ & The bulk transform decryption
+ operation. \\ \hlx{v}
+
+\end{longtable}