doc/tripe-protocol.tex: Much protocol documentation.

[tripe] / doc / tripe-protocol.tex

%%% -*- mode: LaTeX; TeX-PDF-mode: t -*-
%%%
%%% The TrIPE protocol specification
%%%
%%% (c) 2017 Straylight/Edgeware
%%%

%%%----- Licensing notice ---------------------------------------------------
%%%
%%% This file is part of Trivial IP Encryption (TrIPE).
%%%
%%% TrIPE is free software: you can redistribute it and/or modify it under
%%% the terms of the GNU General Public License as published by the Free
%%% Software Foundation; either version 3 of the License, or (at your
%%% option) any later version.
%%%
%%% TrIPE is distributed in the hope that it will be useful, but WITHOUT
%%% ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
%%% FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
%%% for more details.
%%%
%%% You should have received a copy of the GNU General Public License
%%% along with TrIPE.  If not, see <https://www.gnu.org/licenses/>.

%%%--------------------------------------------------------------------------
%%% Preamble.

\documentclass[a4paper, article, numbering]{strayman}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[palatino, helvetica, courier, maths=cmr]{mdwfonts}
\usepackage{longtable}
\usepackage{mathenv}
\usepackage{mdwlist}
\usepackage{mdwmath}
\usepackage{mdwref}
\usepackage{mdwtab}
\usepackage{sverb}
\usepackage{crypto}

\bibliographystyle{mdwalpha}
\numberwithin{table}{section}

\title{TrIPE: The Trivial IP Encryption protocol}
\author{Mark Wooding}
%%\date{incomplete}

\let\len\ell
\let\phi\varphi
\let\emptyset\varnothing
\let\emptystring\varepsilon
\let\len\ell
\let\octet\Sigma
\def\syms{\mathbb{Y}}
\def\lift#1{\lfloor#1\rfloor}
\def\padm#1{\hbox{\kern1pt #1}}
\def\upto{\mathbin{.\,.}}
\def\hex#1{\texttt{#1}_x}
\def\PP{\mathbb{P}}
\def\bit{\mathop{\mathrm{bit}}\nolimits}
\def\bitand{\mathord{\&}}
\def\bitor{\mathbin{|}}
\def\t{\cookie{t}}
\def\nil{\cookie{nil}}

\def\fixme#1{\leavevmode\marginpar{FIXME}[FIXME: #1]}

\newenvironment{aside}
  {\begin{list}{}{\rightmargin=0pt}\footnotesize\item\relax}
  {\end{list}}

\errorcontextlines=99

\begin{document}

%%%--------------------------------------------------------------------------

\maketitle
\thispagestyle{empty}

\begin{abstract}
  This document specifies the TrIPE protocol for IP encryption.

  TrIPE is a fairly simple protocol which allows a pair of hosts to exchange
  short messages, typically IP datagrams, over a hostile network while
  maintaining the properties of \emph{secrecy} and \emph{integrity}; i.e.,
  that the content of the messages cannot be determined by eavesdroppers on
  the network, and that either endpoint can determine whether a message
  received is an unaltered copy of one that was sent by the other.

  The protocol is simple enough for a proof of security in the random-oracle
  model.
\end{abstract}

\tableofcontents

%%%--------------------------------------------------------------------------
\section{Introduction} \label{sec:intro}

TrIPE, or `Trivial IP Encryption', is a protocol designed for the secure (but
unreliable) transmission of IP datagrams over a hostile network between a
pair of hosts, named \emph{peers}.  Specifically, it has the following
properties.
\begin{itemize}
\item \emph{Secrecy}: an adversary cannot determine anything about the
  content of transmitted messages, except for their lengths.
\item \emph{Integrity}: a recipient can verify that a message received is an
  unaltered copy of a message sent by its peer, and which has not previously
  been received.
\item \emph{Symmetry}: in the base protocol, the two peers behave
  identically, which simplifies implementation and analysis.  Some ancillary
  portions of the protocol are asymmetric, in order to deal with asymmetry in
  the environment.
\end{itemize}


\subsection{Overview} \label{sec:intro.overview}

The TrIPE protocol is used between a pair of \emph{peers}.  Neither peer is
distinguished in any way: there is no notion of `initiator' or `responder'.

Each peer has an asymmetric key pair, consisting of a \emph{private key}
which should be known only to the peer itself, and a matching \emph{public
key} which must be known by other peers.

The TrIPE protocol contains no messages for negotiating options such as
cryptographic algorithms or network parameters, and there is no exchange of
certificates.  It is assumed that administrators configure their
implementations with the necessary knowledge about the peers with which they
wish to communicate.

The protocol has two main parts.
\begin{itemize}
\item The \emph{key-exchange} subprotocol (\xref{sec:keyexch}) makes use of
  the peers' public and private keys to establish \emph{keyset}, known to the
  peers themselves but not to an adversary in control of the network.
\item The \emph{bulk transfer} (\xref{sec:xfer}) subprotocol uses keysets
  established using the key-exchange protocol to transfer messages between
  the peers.
\end{itemize}
In addition, there are a few minor subprotocols for various special effects.

%%%--------------------------------------------------------------------------
\section{Preliminaries} \label{sec:prelim}

\subsection{Bits} \label{sec:prelim.bit}

A \emph{bit} is an element of the set $\{ 0, 1 \}$.

The elementary operators $\bitand$ (`and'), $\bitor$ (`or'), and $\xor$
(`exclusive-or', or just `xor') are defined on bits as shown in
\xref{tab:prelim.bit.ops}.
\begin{table}
  \begin{tabular}[C]{|cc|ccc|}                                     \hlx{hv}
    $a$ & $b$ & $a \bitand b$ & $a \bitor b$ & $a \xor b$       \\ \hlx{vhv}
     0  &  0  &      0     &     0     &     0                  \\ \hlx{v}
     0  &  1  &      0     &     1     &     1                  \\ \hlx{v}
     1  &  0  &      0     &     1     &     1                  \\ \hlx{v}
     1  &  1  &      1     &     1     &     0                  \\ \hlx{vh}
  \end{tabular}
  \caption{Elementary bit operators} \label{tab:prelim.bit.ops}
\end{table}

Let $n$ be an integer.  For $i \ge 0$, define $\bit_i n \in \{ 0, 1 \}$ such
that, for any $N \ge 0$,
\[ n \equiv \sum_{0\le i<N} 2^i \bit_i n \pmod{2^N} \padm. \]
Let $(b_i)_{i\ge0}$ be an infinite sequence of bits.  If this sequence
\emph{converges} -- i.e., there exists some $N \ge 0$ such that $b_i = b_N$
for all $i \ge N$ -- then there exists a unique integer $n$ -- specifically,
$n = \sum_{0\le i<N} 2^i b_i - 2^N b_N$ -- such that $\bit_i n = b_i$ for all
$i \ge 0$.  The sequence of bits corresponding to an integer is called its
\emph{two's complement representation}.

Let $m$ and $n$ be integers.  For each elementary bit operator~$\circ$,
define $m \circ n$ to be the unique integer~$r$ such that $\bit_i r = \bit_i
m \circ \bit_i n$.


\subsection{Octet strings} \label{sec:prelim.string}

An \emph{octet} is an integer between~0 and~255 inclusive; formally, define
$\octet = \{ 0, 1, \ldots, 255 \}$.

An \emph{octet string} is a finite sequence of octets.  Define $\octet^n$ to
be the set of $n$-octet strings, Formally, define $\octet^0 = \emptystring$,
where $\emptystring$ denotes the empty string, and $\octet^n = \octet \times
\octet^{n-1}$ for $n > 0$.  The set of all octet strings is $\octet^* =
\bigcup_{i\ge0} \octet^i$.

Let $x, y \in \octet^*$ be octet strings.  The \emph{length} of $x$, denoted
$\len(x)$, is the unique $n$ such that $x \in \octet^n$.

For any $0 \le i < \len(x)$, define the \emph{$i$th octet} of $x$ as follows.
If $x = \emptystring$ then this is not well-defined.  Otherwise, we have $x =
(a, y)$ with $a \in \octet$ and $y \in \octet^{\len(x)-1}$.  Inductively
define $x[0] = a$, and $x[i] = y[i - 1]$ for $1 \le i < \len(x)$.

When $x_i \in \octet$ for $0 \le i < n$, then $[x_0, x_1, \ldots, x_{n-1}]$
denotes the octet string $x \in \octet^n$ such that $\len(a) = n$ and $x[i] =
x_i$ for $0 \le i < n$.  A text string in monospace type surrounded by
double-quote marks \texttt{"}\dots\texttt{"} denotes the octet string
containing the corresponding ASCII code points; e.g., \texttt{"example"}
denotes the octet string $[101, 120, 97, 109, 112, 108, 101]$.
\begin{aside}
  Double quotes themselves do not occur within such strings in this
  specification, so the issue of escaping does not arise.
\end{aside}

If $\ell$ and $n$ are integers with $0 \le n < 256^\ell$, then $[n]_\ell$
denotes the $\ell$-digit big-endian base-256 encoding of $n$.  Specifically,
$a = [n]_\ell$ is the unique octet string such that $\len(a) = \ell$ and
\[ n = \sum_{0\le i<\ell} 2^{8i} a[\ell - i - 1] \padm. \]
Similarly, $[n]'_\ell$ denotes the $\ell$-digit little-endian base-256
encoding of $n$; specifically, $a = [n]'_\ell$ is the unique octet string
such that $\len(a) = \ell$ and
\[ n = \sum_{0\le i<\ell} 2^{8i} a[i] \padm. \]

The \emph{concatenation} of $x$ and $y$, denoted $x \cat y$, is the octet
string $z$ such that $\len(z) = \len(x) + \len(y)$, and $z[i] = x[i]$ if $0
\le i < \len(x)$, or $z[i] = y[i - \len(x)]$ if $\len(x) \le i < \len(z)$.

If $n \ge 0$, the \emph{$n$-fold repetition of $x$}, denoted $x^n$, consists
of $n$ copies of $x$ concatenated together.  Formally, $x^0 = \emptystring$,
and $x^n = x^{n-1} \cat x$ if $n \ge 1$.

If $0 \le i \le j \le \len(x)$, then the \emph{substring} of $x$
\emph{between $i$ and $j$}, denoted $x[i \upto j]$, is the octet string $z$
of length $j - i$ such that $z[k] = x[k - i]$ for $0 \le k < j - i$.  It is
always the case that $x = x[0 \upto i] \cat x[i \upto j] \cat x[j \upto
\len(x)]$.

For each elementary bit operator $\circ$ defined in
\xref{tab:prelim.bit.ops}, and each pair of octet strings $x$ and $y$ of
equal length, define $x \circ y$ to be the octet string $z$ such that
$\len(z) = \len(x) = \len(y)$ and $z[i] = x[i] \circ y[i]$ for $0 \le i <
\len(z)$.


\subsection{Integers} \label{sec:prelim.integer}

Define the \emph{length} $\len(n)$ of a nonnegative integer $n \in \N$ as
follows: if $n = 0$ then $\len(n) = 1$; otherwise, $\len(n)$ is the unique
integer $\ell$ such that $256^{\ell-1} \le n < 256^\ell$.

Numbers written in monospace type with a subscript~$x$ are in hexadecimal;
the digits \texttt{0}--\texttt{9} have their usual values, and letters
\texttt{a}--\texttt{f} have values 10--15.  For example, $\hex{9c} = 156$.


\subsection{Symbols} \label{sec:prelim.symbol}

A \emph{symbol} is an object with no properties other than its distinctive
identity, and no operations other than comparison for equality.  Symbols are
written as a name in monospace type, e.g., \cookie{example}.  A symbol's name
exists only to allow a human reader to distinguish it from other symbols.

The set of symbols is denoted $\syms$.  If $A$ is a set disjoint from
$\syms$, then $\lift{A} = A \cup \syms$.


\subsection{Encodings} \label{sec:prelim.encode}

An \emph{encoding}~$C$ on some set of values $S$ is defined by a pair of
operations, as follows.
\begin{itemize}
\item An \emph{encoding operation}~$C.\id{enc}$.  Given a value $x \in S$,
  $C.\id{enc}$ encodes it as an octet string $a = C.\id{enc}(x) \in
  \octet^*$.
\item A \emph{decoding operation}~$C.\id{dec}$.  Given a string $a \in
  \octet^*$, $C.\id{dec}$ returns a pair $(x, a') = C.\id{dec}(a)$: if the
  operation succeeded, then $x \in S$ is the decoded value, and $a' \in
  \octet^*$ is the remaining suffix of~$a$; otherwise $x =
  \cookie{err-malformed}$ and $a' = \emptystring$.
\end{itemize}
Hence, the possible encodings of values form a prefix-free set of strings.
Furthermore, for any $a' \in \octet^*$ and $x \in S$, it must be the case
that $x, a' = \id{dec}(\id{enc}(x) \cat a')$.

This specification does not define decoding operations explicitly; their
behaviour is unambiguously determined by the corresponding encoding
operations.

\subsubsection{I2VOSP}
The encoding $\id{i2vosp}$ represents an integer ~$n$ in the range $0 \le n <
2^{524288}$ as a variable-length sequence of octets in big-endian order.
Specifically, $\id{i2vosp}.\id{enc}(n) = [\len(n)]_2 \cat [n]_{\len(n)}$,
which is well-defined because $0 < \len(n) < 65536$.

\subsubsection{FE2IP}
Given an element $x$ of a finite field $\gf{q}$, the function $\id{fe2ip}$
determines a unique integer such that $0 \le \id{fe2ip}(x) < q$.
\begin{aside}
  Note that, unlike the other definitions in this section, $\id{fe2ip}$ is a
  plain function, and not an encoding.
\end{aside}

If $q$ is prime, then $\gf{q} = \Z/q\Z$: let $\phi_q$ be the unique ring
homomorphism from $\Z$ to $\gf{q}$, and define $\id{fe2ip}(x)$ to be the
unique integer $n$ such that $0 \le n < q$ and $x = \phi_q(n)$.

Otherwise, $q = r^m$ for some prime power $r$ and an integer $m > 1$.  Fix an
ordered basis $\{ u_0, u_1, \ldots, u_{m-1} \}$ for $\gf{q}$ as a vector
space over $\gf{r}$.
\begin{aside}
  This is often a polynomial basis: if $u(t) = u_0 + u_1 t + \cdots + u_{m-1}
  t^{m-1} + t^m$ is a monic irreducible polynomial of degree~$m$ over
  $\gf{r}$, then $\{ u_0, u_1, \cdots, u_{m-1} \}$ is a suitable basis,
  representing $\gf{q}$ as the quotient ring $\gf{r}[t]/(u(t))$.  Other
  representations are also possible.

  In practice, this case occurs when dealing with elliptic curves, and the
  specification for a curve over a non-prime field will include a description
  of the field representation sufficient to apply this definition.
\end{aside}
Then any element $x \in \gf{q}$ can be written uniquely as a sum
\[ x = \sum_{0\le i<m} u_i x_i \padm, \]
where $x_i \in \gf{r}$ for $0 \le i < m$.  Inductively define
\[ \id{fe2ip}(x) = \sum_{0\le i<m} r^i \id{fe2ip}(x_i) \padm. \]
\begin{aside}
  On the left, \id{fe2ip} is working in the extension field $\gf{q}$; on the
  right, \id{fe2ip} is working in the subfield $\gf{r}$.
\end{aside}
Inductively, we will have $0 \le \id{fe2ip}(x_i) < r$, and hence $0 \le x <
r^m = q$.

\subsubsection{FE2OSP}
The encoding $\id{fe2osp}$ represents a field element~$x \in \gf{q}$ as a
fixed-length sequence of octets.  Specifically, $\id{fe2osp}.\id{enc}(x) =
[\id{fe2ip}(x)]_{\len(q-1)}$.

\subsubsection{FE2VOSP}
The encoding $\id{fe2vosp}$ represents a field element~$x \in \gf{q}$ as a
variable-length sequence of octets; its use is deprecated.  Specifically,
$\id{fe2vosp}.\id{enc}(x) = \id{i2vosp}.\id{enc}(\id{fe2ip}(x))$.

\subsubsection{EC2OSP}
The encoding $\id{ec2osp}$ represents a (homogeneous) projective point $Q =
(X : Y : Z)$ on an elliptic curve $E(k)$ over some finite field $k$ as a
sequence of octets.  For finite points, i.e., where $Z \ne 0$, this encoding
is fixed-length, which is good enough.  If $Z = 0$, the encoding is simply
$\id{ec2osp}.\id{enc}(Q) = [0]$, i.e., a single zero octet.  Otherwise, let
$x = X/Z$ and $y = Y/Z$; then $\id{ec2osp}.\id{enc}(Q) = [4] \cat
\id{fe2osp}.\id{enc}(x) \cat \id{fe2osp}.\id{enc}(y)$.

\subsubsection{EC2VOSP}
The encoding $\id{ec2osp}$ represents a (homogeneous) projective point $Q =
(X : Y : Z)$ on an elliptic curve $E(k)$ over some finite field $k$ as a
variable-length sequence of octets; its use is deprecated.  If $Z = 0$, the
encoding is simply $\id{ec2vosp}.\id{enc}(Q) = [0, 0]$, i.e., two zero
octets.  Otherwise, let $x = X/Z$ and $y = Y/Z$; then
$\id{ec2vosp}.\id{enc}(Q) = \id{fe2vosp}(x) \cat \id{fe2vosp}(y)$.
\begin{aside}
  This is unambiguous since the first two octets of an encoding constructed
  by $\id{i2vosp}$ are not both zero.
\end{aside}


\subsection{Hash functions} \label{sec:prelim.hash}

A cryptographic \emph{hash function} maps input octet strings, to
fixed-length outputs, called \emph{hashes} or, sometimes, \emph{digests}.
\begin{aside}
  Hash functions used in practice often have large but finite limits on the
  lengths of input they can process; e.g., SHA256 can process inputs of up to
  $2^{61}$ octets.  TrIPE does not need to hash messages anywhere near this
  large, so this specification ignores this detail.
\end{aside}

Hash functions are not keyed, which makes expressing the desired security
properties difficult.  The formal analysis of TrIPE models hash functions as
a (non-programmable) \emph{random oracle} -- a magic box to which all
parties, including the adversary, have access, which returns for each
possible input an independent, uniformly distributed, random result, subject
only to the requirement that it return the same result if queried again at
the same input string.  Clearly, no fixed function with a simple description
can possibly instantiate a random oracle.

Certainly, the traditional requirements of preimage resistance,
second-preimage resistance, and collision resistance are necessary, but far
from sufficient.

A hash function~$H$ consists of the following operations and parameters.
\begin{itemize}
\item A \emph{hash length} $H.\id{hsz} > 0$.
\item A \emph{block size}~$H.\id{bsz}$.  If the hash function processes
  inputs in fixed-length `blocks', then $H.\id{bsz}$ is the length of these
  blocks (e.g., SHA512 acts on 128-octet blocks).  If the hash function does
  not process input in fixed-length blocks, then $H.\id{bsz} = 0$.
\item A \emph{hash operation}~$H.\id{hash}$.  For any \emph{message} $x \in
  \octet^*$, $H.\id{hash}$ calculates and returns a \emph{hash} $h =
  H.\id{hash}(x) \in \octet^{H.\id{hsz}}$.
\end{itemize}

\subsubsection{RIPEMD-160}
The RIPEMD-160 function is defined in \cite{Bosselaers:1997:RCH}.  The
function $\id{ripemd-160}.\id{hash}$ is the function defined there;
$\id{ripemd-160}.\id{hsz} = 20$ and $\id{ripemd-160}.\id{bsz} = 64$.

\subsubsection{SHA256 and SHA512}
The SHA256 and SHA512 functions are defined in FIPS~180--4
\cite{Anonymous:2012:SHS}.  The function $\id{sha256}.\id{hash}$ is the
function defined there as SHA256; $\id{sha256}.\id{hsz} = 32$ and
$\id{sha256.bsz} = 64$.  Similarly, the function $\id{sha512}.\id{hash}$ is
the function defined there as SHA512; $\id{sha512}.\id{hsz} = 64$ and
$\id{sha512.bsz} = 128$.

\subsubsection{SHA3}
The SHA3 family of functions is defined in FIPS~202 \cite{NIST:2015:SSP}.
For each $w \in \{ 224, 256, 384, 512 \}$, $H = \id{sha3}(w)$ is a hash
function as follows: $H.\id{hash}$ is the function SHA3-$w$ defined in
\cite{NIST:2015:SSP}, $H.\id{hsz} = w/8$, and $H.\id{bsz} = 200 - w/8$.


\subsection{Mask-generation function} \label{sec:prelim.mgf}

Let $H$ be a hash function, let $x \in \octet^*$, and let $0 \le n < 2^{32}
H.\id{hsz}$.  Define $\id{mgf}(H, x, n)$ by
\begin{itemize}
\item $\id{mgf}(H, x, 0) = \emptystring$;
\item $\id{mgf}(H, x, i \cdot H.\id{hsz}) = \id{mgf}(H, x, (i - 1)
  H.\id{hsz}) \cat H(x \cat [i - 1]_4)$ for $0 < i < 2^{32}$; and
\item $\id{mgf}(H, x, i \cdot H.\id{hsz} + j) = \id{mgf}(H, x, i \cdot
  H.\id{hsz}) \cat H(x \cat [i]_4)[0 \upto j]$ for $0 < i < 2^{32}$ and $0 <
  j < H.\id{hsz}$.
\end{itemize}


\subsection{Blockciphers} \label{sec:prelim.prp}

A \emph{blockcipher}, also known as a \emph{pseudorandom permutation}
(PRP), is a family of permutations, indexed by a \emph{key}, all acting on
the set of octet strings of some fixed length.

A blockcipher~$B$ consists of the following operations and parameters.
\begin{itemize}
\item A \emph{key size} $B.\id{ksz} \ge 0$.
\item A \emph{block size} $B.\id{bsz} > 0$.
\item An \emph{encryption operation}~$B.E$.  Given a \emph{key} $K \in
  \octet^{B.\id{ksz}}$ and an input string $x \in \octet^{B.\id{bsz}}$, $B.E$
  calculates and returns a result $y \in \octet^{B.\id{bsz}}$.
\item An \emph{decryption operation}~$B.D$.  Given a \emph{key} $K \in
  \octet^{B.\id{ksz}}$ and an input string $y \in \octet^{B.\id{bsz}}$, $B.D$
  calculates and returns a result $x \in \octet^{B.\id{bsz}}$.  For any $K$,
  $B.D(K, \cdot)$ must be the inverse of $B.E(K, \cdot)$, i.e., for all $K
  \in \octet^{B.\id{ksz}}$ and all $x \in \octet^{B.\id{bsz}}$, it holds that
  $B.D(K, B.E(K, x)) = x$.
\end{itemize}
\begin{aside}
  Blockcipher designs frequently offer a range of key sizes rather than just
  a single fixed size; e.g., AES offers 16-, 24-, and 32-octet keys.  This
  specification treats such designs as a family of blockciphers, one for each
  distinct key size.
\end{aside}

The security requirement on blockciphers is that no efficient adversary can
distinguish an oracle which implements $B.E$ using a randomly-chosen key from
one which implements a randomly chosen permutation on the same set of
strings, except with negligible probability.

\subsubsection{Twofish}
The Twofish blockcipher is defined in \cite{Schneier:1999:TEAb}.  If $k \in
\{ 0, 8, \ldots, 256 \}$ then $B = \id{twofish}(k)$ is a blockcipher defined
as follows: the key length is $B.\id{ksz} = k/8$; the block size is
$B.\id{bsz} = 16$; the encryption and decryption operations $B.E$ and $B.D$
are the Twofish encryption and decryption algorithms defined in
\cite{Schneier:1999:TEAb}.

\subsubsection{AES (Rijndael)}
The AES blockcipher is defined in \cite{FIPS:2001:AES}, and its design
explained in \cite{Daemen:2002:DRA}.  If $k \in \{ 128, 192, 256 \}$ then $B
= \id{aes}(k)$ is a blockcipher defined as follows: the key length is
$B.\id{ksz} = k/8$; the block size is $B.\id{bsz} = 16$; the encryption and
decryption operations $B.E$ and $B.D$ are the AES encryption and decryption
algorithms defined in \cite{FIPS:2001:AES}.


\subsection{Salsa20 and ChaCha} \label{sec:prelim.latin}

Salsa20 and ChaCha are stream ciphers designed by Bernstein, defined in
\cite{Bernstein:2005:SS} and \cite{Bernstein:2008:CVS} (rather tersely)
respectively; \cite{Bernstein:2007:SFS} is a later description of Salsa20,
including a thorough design rationale, but lacks a formal notation for the
core function.

If $k \in \octet^{16} \cup \octet^{32}$, and $n \in \octet^{16}$, then
\cite{Bernstein:2005:SS} defines $\mathrm{Salsa20}_k(n) \in \octet^{64}$.
This is generalized in \cite{Bernstein:2007:SFS} to Salsa20/$r$, for any
(even) number of rounds~$r$.  The definition of ChaCha in
\cite{Bernstein:2008:CVS} doesn't provide a handy notation for the resulting
function, but it seems reasonable to define $\mathrm{ChaCha}r_k(n)$ by
analogy.

For $K \in \octet^{16} \cup \octet^{32}$, $r \in \{ 0, 2, \ldots \}$, $v \in
\octet^8$, and $0 \le i < 2^{64}$, define $\id{salsa20-core}(K, r, v, i) =
\mathrm{Salsa20/}r_K(v \cat [i]'_8)$, and $\id{chacha-core}(K, r, v, i) =
\mathrm{ChaCha}r_K(v \cat [i]'_8)$.

Let $f$ be $\id{salsa20-core}$ or $\id{chacha-core}$, let $K \in \octet^{16}
\cup \octet^{32}$, let $r$ be a nonnegative even integer, and let $0 \le n <
2^{70}$.  Define $g(f, K, r, v, n)$ by
\begin{itemize}
\item $g(f, K, r, v, 0) = \emptystring$;
\item $g(f, K, r, v, 64 i) = g(f, K, r, v, 64 (i - 1)) \cat f(K, r, v, i -
  1)$ for $0 < i < 2^{64}$; and
\item $g(f, K, r, v, 64 i + j) = g(f, K, r, v, 64 i) \cat f(K, r, v, i)[0
  \upto j]$ for $0 < i < 2^{64}$ and $0 < j < 64$.
\end{itemize}
Finally, define
\begin{itemize}
\item $\id{salsa20}(K, r, v, n) = g(\id{salsa20-core}, K, r, v, n)$ and
\item $\id{chacha}(K, r, v, n) = g(\id{chacha-core}, K, r, v, n)$.
\end{itemize}


\subsection{Symmetric encryption} \label{sec:prelim.symmenc}

A \emph{symmetric encryption scheme}~$E$ consists of the following operations
and parameters.
\begin{itemize}
\item A \emph{key length}~$E.\id{ksz} \ge 0$.
\item An \emph{initialization vector size}~$E.\id{ivsz} > 0$.
\item A safe \emph{data limit} $E.\id{n-limit} > 0$; see \xref{sec:bulk.ops}.
\item An \emph{encryption operation}~$E.E$.  Given a \emph{key} $K \in
  \octet^{E.\id{ksz}}$, an \emph{initialization vector} $v \in
  \octet^{E.\id{ivsz}}$, and a \emph{message} $m \in \octet^*$, $E.E$
  calculates and returns a \emph{ciphertext} $y = E.E(K, v, m) \in \octet^*$.
\item A \emph{decryption operation}~$E.D$.  Given a \emph{key} $K \in
  \octet^{E.\id{ksz}}$, an \emph{initialization vector} $v \in
  \octet^{E.\id{ivsz}}$, and a \emph{ciphertext} $y \in \octet^*$, $E.D$
  calculates and returns a \emph{message} $m = E.D(K, v, y) \in \octet^*$.
  To be a proper symmetric encryption scheme, it must hold that $E.D(K, v,
  E.E(K, v, m)) = m$ for all $K \in \octet^{E.\id{ksz}}$, all $v in
  \octet^{E.\id{ivsz}}$, and all $m \in \octet^*$.
\end{itemize}
\begin{aside}
  The function $E.E(K, v, \cdot)$ need not be surjective; i.e., there may be
  many $y' \in \octet^*$ for which $y' \ne E.E(K, v, m)$ for any $K$, $v$,
  $m$.  There is no requirement on the result of $E.D(K, v, y')$.
\end{aside}
Security is defined as \emph{left-or-right indistinguishability under
chosen-plaintext attack} (IND-CPA).  An adversary is given an oracle which
accepts pairs of messages $(m_0, m_1)$ with $\len(m_0) = \len(m_1)$.  At the
start of the game, the oracle selects $K$ uniformly at random from
$\octet^{E.\id{ksz}}$ and chooses $b \in \{ 0, 1 \}$, also uniformly at
random.  On each query $(m_0, m_1)$, the oracle selects $v$ uniformly at
random from $\octet^{E.\id{ivsz}}$, and returns $E.E(K, v, m_b)$ to the
adversary.  The security requirement is that no efficient adversary should be
able to correctly guess~$b$ with probability significantly different from
$\frac{1}{2}$.

\subsubsection{Ciphertext Block Chaining}
TrIPE's version of CBC is rather unusual.  It uses ciphertext stealing rather
than padding to deal with messages which aren't an exact multiple of the
block size; specifically, it uses the `CBC-CS2' variant described in
\cite{Dworkin:2010:RBC} and analysed by \cite{Rogaway:2012:SCS}.  Ciphertext
stealing doesn't work properly if the message is shorter than the block size;
in this case, TrIPE's variant of CBC switches to Ciphertext Feedback (CFB)
mode.

Given a blockcipher $B$, the symmetric encryption scheme $E = \id{cbc}(B)$ is
defined as follows.
\begin{itemize}
\item $E.\id{ksz} = B.\id{ksz}$.
\item $E.\id{ivsz} = B.\id{bsz}$.
\item $E.\id{n-limit} = 2^{4\cdot B.\id{bsz}-41/2} B.\id{bsz}$.
\item Given $K$, $v$, and $m$, $E.E$ works as follows.
  \begin{enumerate}
  \item Write $\len(m) = n \cdot B.\id{bsz} + t$, where $0 \le t <
    B.\id{bsz}$.
  \item If $n = 0$, then set $y_0 = m \xor B.E(K, v)[0 \upto t]$, and go to
    step~\ref{en:cbc.enc.done}.
    \begin{aside}
      This step is CFB encryption rather than CBC-CS2.  I'm not aware of any
      literature showing that this combination is secure, though in fact it
      is.  The proof of CBC-CS in \cite{Rogaway:2012:SCS} shows that CBC-CS2
      ciphertexts are indistinguishable from uniformly distributed strings;
      and this step is equivalent to setting $y_0 = m \xor E.E(K, v,
      [0]_{B.\id{bsz}})[0 \upto t]$.  Since $E.E(k, v, [0]_{B.\id{bsz}})$ is
      indeed a CBC-CS2 ciphertext (indeed, it is a vanilla CBC ciphertext,
      since the message is exactly one block long), it is indistinguishable
      from uniform, and so $y_0 = m \xor E.E(k, v, [0]_{B.\id{bsz}})[0 \upto
      t]$ is also indistinguishable form uniform.
    \end{aside}
  \item For $0 \le i < n$, set $m_i = m[i \cdot B.\id{bsz} \upto (i + 1)
    \cdot B.\id{bsz}]$, and set $m_n = m[n \cdot B.\id{bsz} \upto \len(m)]$.
  \item Set $y_{-1} = v$, and, for $0 \le i < n - 1$, set $y_i = B.E(K, m_i
    \xor y_{i-1})$.
  \item If $t = 0$, then set $y_{n-1} = B.E(K, m_{n-1} \xor y_{m-2})$ and
    $y_n = \emptystring$, and go to step~\ref{en:cbc.enc.done}.
  \item Set $r = B.E(K, m_{n-1} \xor y_{n-2})$.
  \item Set $y_n = r[0 \upto t]$.
  \item Set $y_{n-1} = B.E(K, (m_n \xor y_n) \cat r[t \upto B.\id{bsz}])$.
  \item \label{en:cbc.enc.done} Finally, $E.E(K, v, m) = y_0 \cat y_1 \cat
    \cdots \cat y_{n-1} \cat y_n$.
  \end{enumerate}
\item Given $K$, $v$, and $Y$, $E.D$ works as follows.
  \begin{enumerate}
  \item Write $\len(y) = n \cdot B.\id{bsz} + t$, where $0 \le t <
    B.\id{bsz}$.
  \item If $n = 0$, then set $m_0 = y \xor B.E(K, v)[0 \upto t]$ and go to
    step~\ref{en:cbc.dec.done}.
  \item For $0 \le i < n$, set $y_i = y[i \cdot B.\id{bsz} \upto (i + 1)
    \cdot B.\id{bsz}]$, and set $y_n = y[n \cdot B.\id{bsz} \upto \len(y)]$.
  \item Set $y_{-1} = v$, and, for $0 \le i < n - 1$, set $m_i = B.D(K, y_i) \xor
    y_{i-1}$.
  \item If $t = 0$, then set $m_{n-1} = B.D(K, y_{n-1}) \xor y_{n-2}$
    and $m_n = \emptystring$, and go to step~\ref{en:cbc.dec.done}.
  \item Set $s = B.D(K, y_{n-1})$.
  \item Set $m_{n-1} = B.D(K, y_n \cat s[t \upto B.\id{bsz}]) \xor y_{n-2}$.
  \item Set $m_n = s[0 \upto t] \xor y_n$.
  \item \label{en:cbc.dec.done} Finally, $E.D(K, v, y) = m_0 \cat m_1 \cat
    \cdots \cat m_{n-1} \cat m_n$.
  \end{enumerate}
\end{itemize}
\begin{aside}
  Decryption is correct.  First, encryption preserves length: if $n = 0$ then
  $y = B.E(K, v)[0 \upto t]$, so $\len(y) = t = \len(m)$; otherwise
  $\len(y_i) = B.\id{bsz}$, and $\len(y_n) = t$, and $\len(y) = n \cdot
  B.\id{bsz} + t = \len(x)$.  Then, examining the decryption algorithm, we
  see the following.
  \begin{itemize}
  \item If $n = 0$ then $B.E(K, v)[0 \upto t] \xor y = B.E(K, v)[0 \upto t]
    \xor B.E(K, v)[0 \upto t] \xor m = m$.
  \item Both the encryption and decryption algorithms compute the same $y_i$,
    for $-1 \le i \le n$.  Specifically, $y_{-1} = v$ and $y = y_0 \cat y_1
    \cat \cdots \cat y_{n-1} \cat y_n$ in each case, and $\len(y_i) =
    B.\id{bsz}$ for $0 \le i < n$, and $\len(y_n) = t$.
  \item For $0 \le i < n - 1$, $B.D(K, y_i) \xor y_{i-1} = B.D(K, B.E(K, m_i
    \xor y_{i-1})) \xor y_{i-1} = m_i$.
  \item When $n > 0$ and $t = 0$, $B.D(K, y_{n-1}) \xor y_{n-2} = B.D(K, B.E(K, m_{n-1}
    \xor y_{n-2})) \xor y_{n-2} = m_{n-2}$.
  \item When $n > 0$ and $t > 0$, we have $s = B.D(K, y_{n-1}) = (m_n \xor
    y_n) \cat r[t \upto B.\id{bsz}]$, so $s[0 \upto t] = m_n \xor y_n$, and
    $s[t \upto B.\id{bsz}] = r[t \upto B.\id{bsz}]$.  Hence $B.D(K, y_n \cat
    s[t \upto B.\id{bsz}]) \xor y_{n-2} = B.D(K, r[0 \upto t] \cat r[t \upto
    B.\id{bsz}]) \xor y_{n-2} = B.D(K, r) \xor y_{n-2} = m_{n-1}$; and $s[0
    \upto t] \xor y_n = m_n$.
  \end{itemize}
\end{aside}


\subsection{Message authentication} \label{sec:prelim.mac}

A \emph{message authentication code} (MAC) calculates a fixed-length
\emph{tag} given a secret \emph{key} and a \emph{message}.  The recipient of
a message can recalculate the expected tag and compare it to the one
provided: if the two match, the recipient can be confident that the message
was not altered since it was transmitted.

A message authentication code~$M$ consists of the following operations and
parameters.
\begin{itemize}
\item A \emph{key size}~$M.\id{ksz} \ge 0$.
\item A \emph{tag size}~$M.\id{tsz} > 0$.
\item A \emph{tagging operation}~$M.\id{tag}$.  Given a key~$K \in
  \octet^{M.\id{ksz}}$, and a message $m \in \octet^*$, $M.\id{tag}$
  calculates and returns a tag $t = M.\id{tag}(K, m) \in
  \octet^{M.\id{t.tsz}}$.
\end{itemize}
\begin{aside}
  Some message authentication codes in the literature require an additional
  \emph{nonce} input.  This specification currently does not admit such MACs.
\end{aside}

The security requirement property on message authentication codes is that an
efficient adversary who does not know the key should be unable to determine a
tag for any new message, even if it is allowed to query the correct tags for
messages of its choice.
\begin{aside}
  It is important that tags are verified in constant time, so that an
  adversary does not learn (for example) which octet of an attempted forgery
  is the first one which doesn't match the expected tag.  In the presence of
  such a leak, it is easy to forge a correct tag, figuring out the right
  octets one by one.
\end{aside}

\subsubsection{HMAC}
The HMAC construction builds a MAC from a hash function.  Originally
described in \cite{Bellare:1996:HC}, HMAC is standardized in \cite{rfc2104}
and \cite{FIPS:2002:KHM}.

If $H$ is a hash function with $H.\id{bsz} > 0$, and $0 \le k \le
H.\id{bsz}$, then the MAC $M = \id{hmac}(H)$ is defined as follows.
\begin{itemize}
\item $M.\id{ksz} = k$.
\item $M.\id{tsz} = H.\id{hsz}$.
\item $M.\id{tag}(K, m) = H.\id{hash}(\id{pad}(K, 92) \cat
  H.\id{hash}(\id{pad}(K, 54) \cat m))$, where $\id{pad}(K, a) =
  [a]^{H.\id{bsz}} \xor (K \cat [0]^{H.\id{bsz}-k})$.
\end{itemize}


\subsection{Poly1305} \label{sec:prelim.poly1305}

Poly1305 is a nonce-based MAC designed and specified by Bernstein
\cite{Bernstein:2005:PAM}.

For $r, s \in \octet^{16}$, and $m \in \octet^*$, define $\id{poly1305}(r, s,
m)$ as follows.  Write $m = m_0 \cat m_1 \cat \cdots \cat m_{n-1}$, where
$\len(m_i) = 16$ for $0 \le i < n - 1$, and $1 \le \len(m_{n-1}) \le 16$.
(If $m = \emptystring$ then $n = 0$ and no $m_i$ are defined.)

\def\b{\penalty0\relax}
Let $r' \in \gf{2^{130}-5}$ be such that $[\id{fe2ip}(r')]'_{16} = (r \bitand
[\hex{ff},\b \hex{ff},\b \hex{ff},\b \hex{0f},\b \hex{fc},\b \hex{ff},\b
\hex{ff},\b \hex{0f},\b \hex{fc},\b \hex{ff},\b \hex{ff},\b \hex{0f},\b
\hex{fc},\b \hex{ff},\b \hex{ff},\b \hex{0f}]$.  For $0 \le i < n$, let $m'_i
\in \gf{2^{130}-5}$ be such that $[\id{fe2ip}(m'_i - 2^{8\len(m_i)})]'_{16} =
m_i$.  Let $u' = \sum_{0\le i<n} r'^{n-i} m'_i$.

Let $\hat{s} \in \Z$ be such that $[\hat{s}]'_{16} = s$.  Then
$[\hat{t}]'_{16} = \id{poly1305}(r, s, m) \in \octet^{16}$ is the unique
16-octet string such that $\hat{t} \equiv \hat{s} + \id{fe2ip}(u')
\pmod{2^{128}}$.

Our $\id{poly1305}(r, m, s)$ is the same as $\mathrm{Poly1305}_r(m, s)$ in
\cite{Bernstein:2005:PAM}.


%%%--------------------------------------------------------------------------
\section{Diffie--Hellman groups} \label{sec:dh-group}

\subsection{Operations} \label{sec:dh-group.ops}

A \emph{Diffie--Hellman group}~$D$ consists of a pair of sets $D.S$ and
$D.G$, of \emph{scalars} and \emph{group elements} respectively, a
distinguished \emph{generator} element $D.P \in D.G$, and a number of
operations on these groups.
\begin{itemize}
\item A \emph{group operation}~$D.\id{dh}$.  Given a scalar $x \in D.S$ and a
  group element $Y \in D.G$, $D.\id{dh}$ calculates and returns a group
  element $Z = D.\id{dh}(x, Y) \in D.G (x, Y)$.  To be a proper
  Diffie--Hellman group, it must be the case that $D.\id{dh}(x, D.\id{dh}(y,
  P)) = D.\id{dh}(y, D.\id{dh}(x, D.P))$ for all scalars $x$ and $y$.
\item A \emph{validity checking operation}~$D.\id{validp}$.  Given a group
  element $X \in D.G$, $D.\id{validp}$ verifies that that $Z = D.\id{dh}(y,
  X)$ can be calculated and published without leaking information about~$y$.
  If this is safe, then $D.\id{validp}(X) = \t$; otherwise, $D.\id{validp}(X)
  = \nil$.
  \begin{aside}
    Typically, this means that $X$ lies within the subgroup generated by
    $D.P$, i.e., that there exists some $x$ such that $X = D.\id{dh}(x,
    D.P)$.  Some groups may have special structure that allows safety to be
    determined more cheaply.
  \end{aside}
\item An encoding $D.\id{ge-public}$ on \emph{public group elements}, for
  which no special properties are required.
\item An encoding $D.\id{ge-secret}$ on \emph{secret group elements}, where
  all encodings have the same length, except for a negligible fraction of
  group elements.
\item An encoding $D.\id{ge-hash}$ on \emph{hashed group elements}, where all
  encodings \emph{should} have the same length, except for a negligible
  fraction of scalars.\footnote{%
    The existence of groups without (mostly) fixed-length hashing encodings
    is a historical mistake.  If a variable-length encoding is used here,
    information about group element(s) being hashed may leak to an adversary
    through timing channels.} %
  The decoding operation is never invoked, so it need not be possible to
  implement it efficiently, though it must be theoretically possible to
  decode encodings unambiguously.
\item An encoding $D.\id{sc}$ on \emph{scalars}, where all encodings have the
  same length, denoted $D.\id{scsz}$; i.e., $D.\id{scsz} =
  \ell(D.\id{sc}.\id{enc}(x))$ for all $x \in S$.
\end{itemize}
Decoding operations must validate input sufficiently that the $D.\id{dh}$
operation can be performed successfully and without leaking secret inputs
during the computation; but it is \emph{not} necessary to perform further
precise verification.  For the most part, an implementation need not verify
that an incoming group element is actually within the subgroup generated by
$D.P$; and an elliptic-curve group need not verify that an incoming pair of
coordinates actually correspond to a point on the curve; the necessary
checking is shown explicitly using the Diffie--Hellman group's
$D.\id{validp}$ function where appropriate.
\begin{aside}
  In an ideal world, we would only have one group-element encoding rather
  than three.  The present situation is caused by unfortunate historical
  mistakes.  Of course, nothing prevents newer Diffie--Hellman group
  specifications from using the same (constant-length) encoding for all three
  group-element encodings described above, and, indeed, the X25519 and X448
  groups defined below do this.
\end{aside}

For security, it must be computationally intractable to determine
$D.\id{dh}(x, D.\id{dh}(y, D.P))$ given only $X = D.\id{dh}(x, D.P)$ and $Y =
D.\id{dh}(y, D.P)$ (i.e., the \emph{computational Diffie--Hellman assumption}
must hold).


\subsection{Schnorr groups} \label{sec:dh-group.schnorr}

For historical reasons, there are two variants of Schnorr groups, named
\cookie{v0} and \cookie{constlen}.  The \cookie{v0} variant is deprecated;
new deployments should use \cookie{constlen} if possible.

Let $p < 2^{524288}$ be an odd prime, let $q$ be a prime factor of $p - 1$,
let $g \ne 1$ be an element of $\gf{p}^*$ such that $g^q = 1$, and let $v$ be
one of the symbols \cookie{v0} or \cookie{constlen}.  Then $D =
\id{schnorr}(p, q, g, v)$ is a Diffie--Hellman group, as follows.

The group itself is the cyclic subgroup $D.G = \langle g \rangle \subseteq
\gf{p}^*$ generated by $g$; the scalars are the finite field $D.S = \gf{q}$;
and the generator is $D.P = g$.

For security, $p$ must be large enough to thwart index-calculus style
discrete-logarithm algorithms in $\gf{p}^*$, and $q$ must be large enough to
thwart generic discrete-logarithm algorithms within the subgroup $G$.  For
new deployments, it is recommended that $p \ge 2^{3071}$ and $q \ge 2^{255}$.

\begin{itemize}
\item The Diffie--Hellman operation is simply exponentiation in $\gf{p}$,
  given by $D.\id{dh}(x, Y) = Y^x$.  (Technically this is an abuse of
  notation: exponentiation is defined for integer exponents, and $x$ is an
  element of a finite field.  For every $Y \in G$, define $\theta_Y\colon \Z
  \to G$ by $\theta_Y(n) = Y^n$; then $q\Z \subseteq \ker \theta_Y$, and
  $\theta_Y$ factors through $\Z/q\Z = \gf{q}$ as $\theta_Y = \theta'_Y \circ
  \phi_q$, where $\phi_q$ is the unique ring homomorphism from $\Z$ to
  $\gf{q}$.  Then $\id{dh}(x, Y) = \theta'_Y(x)$.)
\item Since $\gf{p}$ contains at most one subgroup with any given order,
  $D.\id{validp}(X) = \t$ if and only if $X^q = 1$.
\item The public group-element encoding is FE2VOSP in the field $\gf{p}$;
  i.e., $D.\id{ge-public} = \id{fe2vosp}$.
\item The secret group-element encoding is FE2OSP in the field $\gf{p}$;
  i.e., $D.\id{ge-secret} = \id{fe2osp}$.
\item If $v = \cookie{v0}$, the hash group-element encoding is FE2VOSP, so
  $D.\id{ge-hash} = D.\id{ge-public}$.  If $v = \cookie{constlen}$, the hash
  group-element encoding is FE2OSP, so $D.\id{ge-hash} =
  D.\id{ge-secret}(X)$.
\item The scalar encoding is FE2OSP in the field $\gf{q}$, i.e., $D.\id{sc} =
  D.\id{fe2osp}$; hence $D.\id{scsz} = \len(q - 1)$.
\end{itemize}


\subsection{Short-Weierstraß elliptic curve groups}
\label{sec:dh-group.trad-ec}

For historical reasons, there are two variants of short-Weierstraß groups,
named \cookie{v0} and \cookie{constlen}.  The \cookie{v0} variant is
deprecated; new deployments should use \cookie{constlen} if possible.

Let $p$ be a prime; let $q = p^m$ be some prime power, and let $k = \gf{q}$
be the finite field with $q$ elements.

Projective 2-space over $k$, written $\PP^2(k)$, consists of equivalence
classes of triples $(X, Y, Z) \in k^3 \setminus \{ (0, 0, 0) \}$ under the
equivalence relation $(X, Y, Z) \sim (t X, t Y, t Z)$ for any $t \in k
\setminus \{ 0 \}$.  The equivalence class containing $(X, Y, Z)$ is denoted
$(X : Y : Z)$.

The $k$-rational points on elliptic curve $E$, denoted $E(k)$, consist of
those (homogeneous) projective points $(X : Y : Z) \in \PP^2(k)$ satisfying
an equation.  There are a number of cases to consider:
\begin{itemize}
\item if $p > 3$, then the equation is $Y^2 Z = X^3 + a X Z^2 + b Z^3$, where
  $a, b \in k$ with $4 a^3 + 27 b^2 \ne 0$;
\item if $p = 3$, then the equation is $Y^2 Z = X^3 + c X^2 Z + a X Z^2 + b
  Z^3$, for $a \ne 0$, where $a, b, c \in k$ with $a^3 \ne c^2 (a^2 - b c)$;
  and
\item if $p = 2$, then there are two subcases:
  \begin{itemize}
  \item for \emph{ordinary} curves, the equation is $Y^2 Z + X Y Z = X^3 + a
    X^2 Z + b Z^3$, where $a, b \in k$ with $b \ne 0$; and
  \item for \emph{supersingular} curves, the equation is $Y^2 Z + c Y Z^2 =
    X^3 + a X Z^2 + b Z^3$, where $a, b, c \in k$ with $c \ne 0$.
  \end{itemize}
\end{itemize}
\begin{aside}
  Implementations frequently use other coordinate systems; Jacobian
  projective coordinates are especially popular.  The use of homogeneous
  coordinates in this specification is for convenience of presentation, and
  is not intended to prohibit implementations from using other coordinate
  systems internally.

  Most elliptic curve cryptography implementations handle only `prime fields'
  for which $p > 3$ and $m = 1$, and ordinary curves over `binary fields'
  where $p = 2$.
\end{aside}

The points of $E(k)$ form an abelian group, written additively, with identity
$O = (0 : 1 : 0)$.  Choose $P \in E(k) \setminus \{ O \}$ to generate a
subgroup $\langle P \rangle \in E(k)$ with prime order~$r$.

For security, $r$ must be large enough to thwart generic discrete-logarithm
algorithms within the subgroup $\langle P \rangle$.  For new deployments, it
is recommended that $r \ge 2^{255}$.  A number of other conditions should
also hold.
\begin{itemize}
\item $r \ne q$;
\item $m = 1$ or $m$ is prime;
\item $r^2 > \#E(k)$; and
\item $p^d \not\equiv 1 \pmod{r}$ for any $d < (r - 1)/100$.
\end{itemize}
There are well-known difficulties in implementing short-Weierstraß elliptic
curve arithmetic free of microarchitectural side-channels.

Finally, let $v$ be one of the symbols \cookie{v0} or \cookie{constlen}.
Then $D = \id{ec}(k, E, P, r, v)$ is a Diffie--Hellman group as follows.  The
group itself is the subgroup $D.G = \langle P \rangle$ generated by $P$; the
scalars are the finite field $S = \gf{r}$; and the generator is the point
$D.P = P$.

The Diffie--Hellman group operations are as follows.
\begin{itemize}
\item The Diffie--Hellman operation is elliptic curve scalar multiplication,
  given by $D.\id{dh}(x, Y) = x Y$.
\item Since $r^2 > \#E(k)$, there can be at most one subgroup of $E(k)$ with
  order $r$; therefore $D.\id{validp}(X) = \t$ if and only if $r X = O$.
\item The public group-element encoding is EC2VOSP; i.e.,
  $D.\id{ge-public} = \id{ec2vosp}$.
\item The secret group-element encoding is EC2OSP; i.e.,
  $D.\id{ge-secret} = \id{ec2osp}$.
\item If $v = \cookie{v0}$, the hash group-element encoding is EC2VOSP, so
  $D.\id{ge-hash} = D.\id{ge-public}$.  If $v = \cookie{constlen}$, the hash
  group-element encoding is EC2OSP, so $D.\id{ge-hash} = D.\id{ge-secret}$.
\item The scalar encoding is FE2OSP in the field $\gf{r}$, i.e.,
  $D.\id{enc-sc} = \id{fe2osp}$; hence $D.\id{scsz} = \len(q - 1)$.
\end{itemize}


\subsection{The X25519 group} \label{sec:dh-group.x25519}

The X25519 function was introduced by Bernstein in \cite{Bernstein:2006:CDH},
where it was originally named `Curve25519'.  It uses a carefully chosen
elliptic curve over the finite field $k = \gf{p^2}$, where $p = 2^{255} -
19$; specifically
\[ E(k) = \{\, (X : Y : Z) \mid Y^2 Z = X^3 + 486662 X^2 Z + X Z^2 \,\}
  \padm.
\]
\cite{Bernstein:2006:CDH} completely defines X25519 as a function on 32-octet
strings.
\begin{aside}
  Note that this is \emph{not} quite the same function as specified in
  RFC7748 \cite{rfc7748}.  That specification requires that implementations
  ignore the most significant bit of public key; the original definition
  considers that bit significant (and has place-value $-19$).  Correct and
  honest senders will not set this bit.
\end{aside}

Thus, $D = \id{x25519}$ is a Diffie--Hellman group as follows.  Both the
scalars and group are simply the set of all octet strings of length~32; i.e.,
$D.S = D.G = \octet^{32}$.  The generator is the point $D.P = [9, 0, \ldots,
0]$.

\begin{itemize}
\item The Diffie--Hellman operation is the X25519 operation: $D.\id{dh}(x, Y)
  = \id{X25519}(x, Y)$.
\item By design, X25519 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} = 32$.
\end{itemize}


\subsection{The X448 group} \label{sec:dh-group.x448}

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}

%%%----- That's all, folks --------------------------------------------------

%  LocalWords:  TrIPE LaTeX encodings endian monic osp vosp TrIPE's schnorr
%  LocalWords:  constlen Weierstraß abelian additively keyexch xfer dec dh
%  LocalWords:  validp ge sc scsz fe decrypts sha th hsz hbsz ok hv iiv
%  LocalWords:  naclbox crypto eprint rfc PRP FIPS ripemd eblk bcksz aes
%  LocalWords:  rijndael chacha surjective indistinguishability bsz MACs ccc
%  LocalWords:  hmac IANA vh ripemd mgf ksz aes cbc ivsz tsz fc tx blkc kx
%  LocalWords:  prechal chal switchok bh nop eping epong exch kx upd activep
%  LocalWords:  retransmit lev

\end{document}