chiark / gitweb /
doc/tripe-protocol.tex: Much protocol documentation. mdw/docs
authorMark Wooding <mdw@distorted.org.uk>
Fri, 11 May 2018 23:39:55 +0000 (00:39 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Fri, 11 May 2018 23:39:55 +0000 (00:39 +0100)
Unfortunately, it's mostly impenetrable, but maybe it can be improved
later.

doc/tripe-protocol.tex

index 2ab0015..734a559 100644 (file)
 \usepackage[T1]{fontenc}
 \usepackage[utf8]{inputenc}
 \usepackage[palatino, helvetica, courier, maths=cmr]{mdwfonts}
+\usepackage{longtable}
+\usepackage{mathenv}
 \usepackage{mdwlist}
 \usepackage{mdwmath}
-\usepackage{crypto}
 \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}
 
-\def\fixme#1{\marginpar{FIXME}[FIXME: #1]}
+\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}
 
 %%%--------------------------------------------------------------------------
@@ -66,6 +92,8 @@
   model.
 \end{abstract}
 
+\tableofcontents
+
 %%%--------------------------------------------------------------------------
 \section{Introduction} \label{sec:intro}
 
@@ -113,96 +141,162 @@ The protocol has two main parts.
 In addition, there are a few minor subprotocols for various special effects.
 
 %%%--------------------------------------------------------------------------
-\section{Diffie--Hellman groups} \label{sec:dh-group}
+\section{Preliminaries} \label{sec:prelim}
 
-\subsection{Operations} \label{sec:dh-group.ops}
+\subsection{Bits} \label{sec:prelim.bit}
 
-An \emph{encoding} on some set of values $S$ is defined by a pair of
-operations \id{enc} and \id{dec}, as follows.
-\begin{itemize}
-\item Given a value $x \in S$, $\id{enc}(x)$ encodes it as an octet string.
-\item Given an octet string $a$, $\id{dec}(a)$ parses and decodes a value $x$
-  and remainder string $a'$ from it.
-\end{itemize}
-Hence, the possible encodings of values form a prefix-free set of strings.
-Furthermore, if $a'$ is any octet string, and $x \in S$ is any value, then it
-must be the case that $x, a' = \id{dec}(\id{enc}(x) \cat a')$.
-
-A \emph{Diffie--Hellman group} consists of a pair of sets $S$ and $G$, of
-\emph{scalars} and \emph{group elements} respectively, a distinguished
-\emph{generator} element $P \in G$, and a number of operations on these
-groups.  In the following descriptions, $x$ and $y$ are scalars; $X$, $Y$,
-and $Z$ are group elements; and $a$ and $a'$ are octet strings.
-\begin{itemize}
-\item $\id{dh}(x, Y)$ calculates a group element $Z$.  To be a proper
-  Diffie--Hellman group, it must be the case that $\id{dh}(x, \id{dh}(y, P))
-  = \id{dh}(y, \id{dh}(x, P))$ for all scalars $x$ and $y$.  For security, it
-  must be computationally intractable to determine $\id{dh}(x, \id{dh}(y,
-  P))$ given $X = \id{dh}(x, P)$ and $Y = \id{dh}(y, P)$ (i.e., the
-  \emph{computational Diffie--Hellman assumption} must hold).
-\item $\id{enc-ge-public}$ and $\id{dec-ge-public}$ together define an
-  encoding on group elements, for which no special properties are required.
-\item $\id{enc-ge-secret}$ and $\id{dec-ge-secret}$ together define an
-  encoding on group elements where all encodings have the same length, except
-  with negligible probability.
-\item $\id{enc-ge-hash}$ and $\id{dec-ge-hash}$ together define an encoding
-  on group elements where all encodings \emph{should} have the same length,
-  except with negligible probability.\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 $\id{enc-sc}$ and $\id{dec-sc}$ together define an encoding on scalars,
-  where all encodings have the same length.  Let $\id{scsz}$ be the length of
-  an encoded scalar.
-\end{itemize}
-In the following descriptions, decoding functions are not described explicitly
-Decoding operations must validate input sufficiently that the $\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 example, an implementation need not verify that an
-incoming group element is actually within the subgroup generated by $P$; and
-an elliptic-curve group need not verify that an incoming pair of coordinates
-actually correspond to a point on the curve.
+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}
-  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.
+  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. \]
 
-\subsection{Primitive encoding functions} \label{sec:dh-group.encode}
+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)$.
 
-\subsubsection{I2OSP}
-If $\ell$ and $n$ are integers with $0 \le n < 2^{8\ell}$, then $[n]_\ell$
-denotes the $\ell$-digit big-endian base-256 encoding of $n$.  Specifically,
-let $a_0$, $a_1$, \ldots, $a_{\ell-1}$ be the unique integers such that $0
-\le a_i < 256$ for $0 \le i < \ell$, and
-\[ n = \sum_{0\le i<\ell} 2^{8i} a_i \]
-Then $[n]_\ell$ is the $\ell$-octet string $a_{\ell-1} \cat \cdots \cat a_1
-\cat a_0$.
+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}
-Given an integer $0 \le n < 2^{524288}$, the function $\id{i2vosp}(n)$
-determines a variable-length big-endian base-256 encoding of $n$.  If $n = 0$
-then let $\ell = 1$; otherwise, let $\ell$ be the unique integer such that
-$2^{8(\ell-1)} \le n < 2^{8\ell}$; since $n$ is bounded, it must be that
-$\ell < 65536$.  Then $\id{i2vosp}(n) = [\ell]_2 \cat [n]_\ell$.
+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(n)$ be the unique ring
+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
-smallest nonnegative integer $n$ such that $x = \phi_q(n)$; it is necessarily
-the case that $0 \le \id{fe2ip}(x) < q$.
+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
@@ -219,66 +313,1297 @@ space over $\gf{r}$.
   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 \]
-where $x_i \in \gf{r}$ for $0 \le i < m$.  Then inductively define
-\[ \id{fe2ip}(x) = \sum_{0\le i<m} r^i \id{fe2ip}(x_i) \]
+\[ 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}
-Given a field element $x \in \gf{q}$, the function $\id{fe2osp}(x)$
-determines a fixed-length encoding of $x$.  Let $\ell$ be the unique integer
-such that $2^{8(\ell-1)} < q \le 2^{8\ell}$.  Then $\id{fe2osp}(x) =
-[\id{fe2ip}(x)]_\ell$.
+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}
-Given a field element $x \in \gf{q}$ for some $q \le 2^{524288}$, the
-function $\id{fe2vosp}(x)$ determines a variable-length encoding of $x$;
-specifically, $\id{fe2vosp}(x) = \id{i2vosp}(\id{fe2ip}(x))$.
+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}
-Given a projective point $Q = (X : Y : Z)$ on an elliptic curve $E(k)$ over
-some finite field $k$, the function $\id{ec2osp}$ determines an encoding of
-$Q$.  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
-$[0]_1$, i.e., a single zero octet.  Otherwise, let $x = X/Z$ and $y = Y/Z$;
-the encoding of $Q$ is then $[4]_1 \cat \id{fe2osp}(x) \cat \id{fe2osp}(y)$.
+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}
-Given a projective point $Q = (X : Y : Z)$ on an elliptic curve $E(k)$ over
-some finite field $k$, the function $\id{ec2vosp}$ determines a
-variable-length encoding of $Q$.  If $Z = 0$, the encoding is simply $[0]_2$,
-i.e., two zero octets.  Otherwise, let $x = X/Z$ and $y = Y/Z$; the encoding
-of $Q$ is then $\id{fe2vosp}(x) \cat \id{fe2vosp}(y)$.  This is unambiguous
-since the first two octets of an encoding constructed by $\id{i2vosp}$ are
-not both zero.
+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}
 
-Let $p$ be an odd prime, let $q$ be an odd prime factor of $p - 1$, and let
-$g \ne 1$ be an element of $\gf{p}^*$ such that $g^q = 1$.  The cyclic
-subgroup $G \subseteq \gf{p}^*$ generated by $g$ is a \emph{Schnorr group};
-the scalars are the finite field $S = \gf{q}$; and the generator is $P = g$.
+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 $\id{dh}(x, Y) = Y^x$.
-\item 
+  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
+%  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}