chiark / gitweb /
Much documentation progress.
authormdw <mdw>
Sun, 13 Jul 2003 11:16:27 +0000 (11:16 +0000)
committermdw <mdw>
Sun, 13 Jul 2003 11:16:27 +0000 (11:16 +0000)
doc/wrestlers.tex

index c175b1a9a971d4c4b7a0740293d3f5e9fc29e0db..0f8cc00016040898384c1e9e5f96307a591c0312 100644 (file)
@@ -1,6 +1,6 @@
 %%% -*-latex-*-
 %%%
-%%% $Id: wrestlers.tex,v 1.5 2002/01/13 14:55:31 mdw Exp $
+%%% $Id: wrestlers.tex,v 1.6 2003/07/13 11:16:27 mdw Exp $
 %%%
 %%% Description of the Wrestlers Protocol
 %%%
@@ -10,6 +10,9 @@
 %%%----- Revision history ---------------------------------------------------
 %%%
 %%% $Log: wrestlers.tex,v $
+%%% Revision 1.6  2003/07/13 11:16:27  mdw
+%%% Much documentation progress.
+%%%
 %%% Revision 1.5  2002/01/13 14:55:31  mdw
 %%% More incomplete stuff.
 %%%
 %%% Initial versions of documentation.
 %%%
 
-\newif\iffancystyle\fancystylefalse
+\newif\iffancystyle\fancystyletrue
 
 \iffancystyle
   \documentclass
     [a4paper, article, 10pt, numbering, noherefloats, notitlepage]
     {strayman}
   \usepackage[palatino, helvetica, courier, maths=cmr]{mdwfonts}
-  \usepackage[margin]{amsthm}
+  \usepackage[mdwmargin]{mdwthm}
+  \PassOptionsToPackage{dvips}{xy}
 \else
-  \documentclass[a4paper]{article}
-  \usepackage{a4wide}
-  \usepackage{amsthm}
+  \documentclass{llncs}
 \fi
 
+\usepackage{mdwtab, mathenv, mdwlist, mdwmath, crypto}
 \usepackage{amssymb, amstext}
-\usepackage{mdwtab, mathenv}
+\usepackage{tabularx}
+\usepackage{url}
+\usepackage[all]{xy}
 
 \errorcontextlines=999
 \showboxbreadth=999
 \title{The Wrestlers Protocol: proof-of-receipt and secure key exchange}
 \author{Mark Wooding \and Clive Jones}
 
-\bibliographystyle{alpha}
-
-\newtheorem{theorem}{Theorem}
-\renewcommand{\qedsymbol}{$\square$}
-
-\newcommand{\getsr}{\stackrel{\scriptscriptstyle R}{\gets}}
-\newcommand{\inr}{\in_{\scriptscriptstyle R}}
-\newcommand{\oracle}[1]{\mathcal{#1}}
-
-\newcommand{\expt}[2]{\mathbf{Exp}^{\text{\normalfont#1}}_{#2}}
-\newcommand{\adv}[2]{\mathbf{Adv}^{\text{\normalfont#1}}_{#2}}
-\newcommand{\ord}{\mathop{\operator@font ord}}
-\newcommand{\poly}[1]{\mathop{\operator@font poly}({#1})}
-\newcommand{\negl}[1]{\mathop{\operator@font negl}({#1})}
-\newcommand{\compind}{\stackrel{c}{\approx}}
+\bibliographystyle{mdwalpha}
 
 \newcolumntype{G}{p{0pt}}
-
-\newcommand{\xor}{\oplus}
-\renewcommand{\epsilon}{\varepsilon}
-
-\newenvironment{program}
-  {\begin{tabular}[C]{|G|}\hlx{hv[][\tabcolsep]}\begin{tabbing}}
-  {\end{tabbing}\\\hlx{v[][\tabcolsep]h}\end{tabular}}
+\def\Nupto#1{\N_{<{#1}}}
+\let\Bin\Sigma
+\let\epsilon\varepsilon
+\let\emptystring\lambda
+\def\bitsto{\mathbin{..}}
+\turnradius{4pt}
+\def\fixme{\marginpar{FIXME}}
+\def\messages{%
+  \basedescript{%
+    \desclabelwidth{2.5cm}%
+    \desclabelstyle\pushlabel%
+    \let\makelabel\cookie%
+  }%
+}
+\let\endmessages\endbasedescript
 
 \begin{document}
 
 \maketitle
 \begin{abstract}
-  Fill this in later.
+  The Wrestlers Protocol\footnote{%
+    `The Wrestlers' is a pub in Cambridge which serves good beer and
+    excellent Thai food.  It's where the authors made their first attempts at
+    a secure key-exchange protocol which doesn't use signatures.} %
+  is a key-exchange protocol with the interesting property that it leaves no
+  evidence which could be used to convince a third party that any of the
+  participants are involved.  We describe the protocol and prove its security
+  in the random oracle model.
+
+  Almost incidentally, we provide a new security proof for the CBC encryption
+  mode.  Our proof is much simpler than that of \cite{Bellare:2000:CST}, and
+  gives a slightly better security bound.
+
+  % I've not yet decided whose key-exchange model to use, but this ought to
+  % be mentioned.
 \end{abstract}
 \tableofcontents
 \newpage
 %%%--------------------------------------------------------------------------
 
 \section{Introduction}
+\label{sec:intro}
 % Some waffle here about the desirability of a key-exchange protocol that
 % doesn't leave signatures lying around, followed by an extended report of
 % the various results.
 
 %%%--------------------------------------------------------------------------
 
-\section{A simple authentication protocol}
-% Present the basic Diffie-Hellman-based authenticator, and prove that an
-% authentication oracle is useless if the hash function has appropriate
-% properties.
-
-We begin by introducing a simple proof-of-identity protocol, based on the
-Diffie-Hellman key-exchange protocol \cite{Diffie:1976:NDC} and prove some of
-its useful properties.
-
-\subsection{Introduction}
-
-We start by selecting a security parameter $k$.  We choose a cyclic group $G
-= \langle g \rangle$ with $q = |G|$ prime, in which the decision
-Diffie-Hellman problem is assumed to be hard \cite{Boneh:1998:DDP}; we
-require that $q$ is a $k$-bit number.  Suitable groups include elliptic
-curves over finite fields and prime-order subgroups of prime fields.
-Throughout, we shall write the group operation as multiplication, and we
-shall assume that group elements are interchangeable with their binary
-representations.
-
-Alice can choose a private key $\alpha$ from the set $\{ 1, 2, \ldots, q - 1
-\}$ and publish her corresponding public key $a = g^\alpha$.
-
-A simplistic proof-of-identity protocol might then proceed as follows:
-\begin{enumerate}
-\item Bob chooses a random exponent $\beta$, also from $\{ 1, 2, \ldots, q -
-  1 \}$, and sends a \emph{challenge} $b = g^\beta$ to Alice.
-\item Alice computes her \emph{response} $b^\alpha$ and returns it to Bob.
-\item If Alice's response is equal to $a^\beta$ then Bob is satisfied.
-\end{enumerate}
-If Bob always plays by the rules then this protocol is evidently secure,
-since computing $g^{\alpha\beta}$ given $g^\alpha$ and $g^\beta$ is precisely
-the Diffie-Hellman problem.
-
-This protocol has a flaw, though: by using Alice as an oracle for the
-function $x \mapsto x^\alpha$, he could conceivably acquire information about
-Alice's private key which he could later use to impersonate her.  As an
-example, Bob can submit $-g^\beta$ as a challenge: if the reply
-$(-g^\beta)^\alpha = g^{\alpha\beta}$, Bob can conclude that $\alpha$ is
-even.
-
-We fix the protocol by requiring that Bob prove that he already knows the
-answer to his challenge.  We introduce a hash function $h$ whose properties
-we shall investigate later.  The \emph{Wrestlers Authentication Protocol} is
-then:
-\begin{enumerate}
-\item Bob chooses a secret $\beta \getsr \{ 1, 2, \ldots, q - 1 \}$.  He
-  computes his \emph{challenge} $b \gets g^\beta$ and also a \emph{check
-    value} $c \gets \beta \xor h(a^\beta)$.  He sends the pair $(b, c)$.
-\item Alice receives $(b', c')$.  She computes $r \gets b'^\alpha$ and
-  $\gamma \gets c' \xor h(R)$.  If $b' = g^\gamma$, she sends $r$ back as her
-  \emph{response}; otherwise she sends the distinguished value $\bot$.
-\item Bob receives $r'$.  If $r' = a^\beta$ then he accepts that he's talking
-  to Alice.
-\end{enumerate}
-We show that the introduction of the check value has indeed patched up the
-weakness described above, and that the check value itself hasn't made an
-impersonator's job much easier.
-
-\subsection{Analysis in the random oracle model}
-
-Here, we prove that the Wrestlers Authentication Protocol is secure if $h$ is
-implemented by a public \emph{random oracle} \cite{Bellare:1993:ROP}.
-
-Fix a private key $\alpha \inr \{ 1, 2, \ldots, q - 1\}$ and the corresponding public
-key $a = g^\alpha$, and consider a probabilistic polynomial-time adversary
-$A$, equipped with two oracles.  One is a random oracle $\oracle{H}\colon
-\{0, 1\}^* \to \{0, 1\}^k$, which implements a function $h$ randomly selected
-from the set of all functions with that signature; the other is an
-authentication oracle $\oracle{O}\colon G \times \{0, 1\}^k \to G \cup \{
-\bot \}$ defined by:
-\[
-\oracle{O}^(b, c) = \begin{cases}
-  b^\alpha & if $b = g^{c \xor h(b^\alpha)}$ \\
-  \bot     & otherwise
-\end{cases}
-\]
-The authentication oracle will play the part of Alice in the following.  We
-first show that access to this authentication oracle can't help an adversary
-learn how to impersonate Alice.
-
-\begin{theorem}
-  The Wrestlers Authentication Protocol with random oracle is computational
-  zero knowledge \cite{Brassard:1989:SZK}.
-  \label{thm:wap-czk}
-\end{theorem}
-\begin{proof}
-  \newcommand{\Hlist}{\textit{$\oracle{H}$-list}}
-  \newcommand{\Hsim}{\textit{$\oracle{H}$-sim}}
-  \newcommand{\Osim}{\textit{$\oracle{O}$-sim}}
-  \renewcommand{\H}{\oracle{H}}
-  \renewcommand{\O}{\oracle{O}}
-  %
-  Let $A$ be any probabilistic polynomial-time adversary with access to a
-  random.  We shall construct a probabilistic polynomial-time adversary $A'$
-  without either oracle such that the probability distributions on the output
-  of $A$ and $A'$ are equal.  Specifically, $A'$ runs $A$ with simulated
-  random and authentication oracles whose behaviour is computationally
-  indistinguishable from the originals.  The algorithm for $A'$ and the
-  simulated oracles is shown in figure~\ref{fig:wap-czk-sim}.
-
-  \begin{figure}
-    \begin{program}
-      \quad \= \kill
-      Adversary $A'^{\H(\cdot)}$: \+ \\
-        $\Hlist \gets \emptyset$; \\
-        $r \gets A^{\Hsim(\cdot), \Osim(\cdot, \cdot)}$; \\
-        \textbf{return} $r$; \- \\[\medskipamount]
-      %
-      Simulated random oracle $\Hsim(q)$: \+ \\
-        \textbf{if} $\exists r : (q, r) \in \Hlist$ \textbf{then}
-          \textbf{return} $r$; \\
-        $r \getsr \H(q)$; \\
-        $\Hlist \gets \Hlist \cup \{ (q, r) \}$; \\
-        \textbf{return} $r$; \- \\[\medskipamount]
-      %
-      Simulated authentication oracle $\Osim(b, c)$: \+ \\
-        \textbf{if} $\exists q, r : (q, r) \in \Hlist \wedge
-                                    b = g^{c \xor r} \wedge
-                                    q = a^{c \xor r}$ \textbf{then}
-          \textbf{return} $a^{c \xor r}$; \\
-        \textbf{else} \textbf{return} $\bot$;
-    \end{program}
-    %
-    \caption{The algorithm and simulated oracles for the proof of
-        theorem~\ref{thm:wap-czk}.}
-    \label{fig:wap-czk-sim}
-  \end{figure}
-  
-  Firstly we show that $A'$ runs in polynomial time.  The only modifications
-  to $\Hlist$ are in $\Hsim$, which adds at most one element for each oracle
-  query.  Since $\Hlist$ is initially empty and $A$ can only make $\poly{k}$
-  queries to $\Hsim$, this implies that $|\Hlist|$ is always
-  polynomially-bounded.  Each query can be answered in polynomial time:
-  indeed, the search implied by the test $\exists r : (q, r) \in \Hlist$ can
-  be performed in $O(\log q)$ time by indexing $\Hlist$ on $q$ using a radix
-  tree.  Now, since $|\Hlist|$ is polynomially bounded, the test $\exists q,
-  r : (q, r) \in \Hlist \wedge b = g^{c \xor r} \wedge q = a^{c \xor r}$ at
-  the start of $\Osim$ runs in polynomial time even though it requires an
-  exhaustive search of the history of $A$'s queries to its simulated random
-  oracle.
-  
-  Next, we examine the behaviour of the simulated oracles.  Since $\Hsim$ is
-  implemented in terms of the public random oracle $\H$, and returns the same
-  answers to queries, its probability distribution must be identical.
-  
-  We turn our attention to the simulation of the authentication oracle.
-  Consider a query $(b, c)$ made by $A$ to its authentication oracle.
-  
-  Firstly, suppose that there is a $\beta$ such that $b = g^\beta$ and $c =
-  \beta \xor r$ where $r$ is the response to a previous query made by $A$ to
-  its random oracle on $a^\beta$.  Then the true authentication oracle $\O$
-  is satisfied because $b = g^\beta = g^{c \xor r} = g^{c \xor h(a^\beta)} =
-  g^{c \xor h(b^\alpha)}$, and returns $b^\alpha$.  Similarly, the simulated
-  authentication oracle $\Osim$ will find the pair $(a^\beta, r) \in \Hlist$,
-  recover $\beta = c \xor r$, confirm that $b = g^\beta$, and return
-  $a^\beta$ as required.  These events all occur with probability 1.
-
-  Conversely, suppose that there is no such $\beta$.  Then the simulated
-  oracle $\Osim$ will reject the query, returning $\bot$, again with
-  probability 1.  However, a genuine authentication oracle $\O$ will succeed
-  and return $b^\alpha$ with probability $2^{-k}$.  To see this, note that $b
-  = g^\gamma$ for some $\gamma \in \{ 0, 1, \ldots, q - 1 \}$, and the
-  probability that $h(b^\alpha) = c \xor \gamma$ is precisely $2^{-k}$, since
-  $c$ and $\gamma$ are $k$-bit strings.  Since this probability is
-  negligible, we have shown that the distributions of the simulated oracles
-  $\Hsim$ and $\Osim$ are computationally indistinguishable from the genuine
-  oracles $\H$ and $\O$.  The theorem follows.
-\end{proof}
+\section{Preliminaries}
+\label{sec:prelim}
+% Here we provide definitions of the various kinds of things we use and make,
+% and describe some of the notation we use.
 
-Our next objective is to show that pretending to be Alice is hard without
-knowledge of her secret $\alpha$.  We say that an adversary $A$
-\emph{impersonates} in the Wrestlers Authentication Protocol with probability
-$\epsilon$ if
-\[ \Pr[A^{\oracle{H}(\cdot)}(g^\alpha, g^\beta,
-                             \beta \xor h(g^{\alpha\beta}))
-         = g^{\alpha\beta}]
-     = \epsilon
-\]
-where the probability is taken over all choices of $\alpha, \beta \in \{ 1,
-2, \ldots, q - 1 \}$ and random oracles $\oracle{H}$.
-
-\begin{theorem}
-  Assuming that the Diffie-Hellman problem is hard in $G$, no probabilistic
-  polynomial-time adversary can impersonate in the Wrestlers Authentication
-  Protocol with random oracle with better than negligible probability.
-  \label{thm:wap-dhp}
-\end{theorem}
-\begin{proof}
-  \newcommand{\Hlist}{\textit{$\oracle{H}$-list}}
-  \newcommand{\Hqueries}{\textit{$\oracle{H}$-queries}}
-  \newcommand{\Hsim}{\textit{$\oracle{H}$-sim}}
-  \renewcommand{\H}{\oracle{H}}
-  %
-  We prove the theorem by contradiction.  Given a polynomial-time adversary
-  $A$ which impersonates Alice with non-negligible probability $\epsilon$, we
-  construct an adversary which solves the Diffie-Hellman problem with
-  probability no less than $\epsilon \poly{k}$, i.e.,
-  \[ \Pr[A'(g^\alpha, g^\beta) = g^{\alpha\beta}] \ge \epsilon \poly{k}. \]
-  Thus, if there is any polynomial-time $A$ which impersonates with better
-  than negligible probability, then there is a polynomial-time $A'$ which
-  solves Diffie-Hellman with essentially the same probability, which would
-  violate our assumption of the hardness of Diffie-Hellman.
-
-  The idea behind the proof is that the check value is only useful to $A$
-  once it has discovered the correct response to the challenge, which it must
-  have done by solving the Diffie-Hellman problem.  Hence, our Diffie-Hellman
-
-  \begin{figure}
-    \begin{program}
-      \quad \= \kill
-      Adversary $A'(a, b)$: \+ \\
-        $\Hlist \gets \emptyset$; \\
-        $\Hqueries \gets \emptyset$; \\
-        $r \getsr \{ 0, 1 \}^k$; \\
-        $x \gets A^{\Hsim(\cdot)}(a, b, r)$; \\
-        $c \getsr (\Hlist \cup \{ x \}) \cap G$; \\
-        \textbf{return} $c$; \- \\[\medskipamount]
-      %
-      Simulated random oracle $\Hsim(q)$: \+ \\
-        \textbf{if} $\exists r : (q, r) \in \Hlist$
-          \textbf{then} \textbf{return} $r$; \\
-        $r \gets \{ 0, 1 \}^k$; \\
-        $\Hlist \gets \Hlist \cup \{ (q, r) \}$; \\
-        $\Hqueries \gets \Hqueries \cup \{ q \}$; \\
-        \textbf{return} $r$;
-    \end{program}
-    %
-    \caption{The algorithm for the proof of theorem~\ref{thm:wap-dhp}}
-    \label{fig:wap-dhp-rdc}
-  \end{figure}
-
-  The adversary $A'$ is shown in figure~\ref{fig:wap-dhp-rdc}.  It generates
-  a random check-value and runs the impersonator $A$.
-  
-  The simulated random oracle $\Hsim$ gathers together the results of all of
-  the random oracle queries made by $A$.  The final result returned by $A'$
-  is randomly chosen from among all of the `plausible' random oracle queries
-  and $A$'s output, i.e., those queries which are actually members of the
-  group.  The check value given to $A$ is most likely incorrect (with
-  probability $1 - 2^{-k}$): the intuition is that $A$ can only notice if it
-  actually computes the right answer and then checks explicitly.
-
-  If $A$ does compute the correct answer $g^{\alpha\beta}$ and either returns
-  it or queries $\Hsim$ on it, then $A'$ succeeds with probability $\epsilon
-  / |(\Hlist \cup \{ x \}) \cap G| = \epsilon \poly{k}$, since $|\Hlist|$ is
-  no greater than the number of random oracle queries made by $A$ (which must
-  be polynomially bounded).\footnote{%
-    This polynomial factor introduces a loss in the perceived security of the
-    authentication protocol.  It appears that this loss is only caused by the
-    possibility of the adversary $A$ being deliberately awkward and checking
-    the value of $c$ after having computed the answer.  However, we can't see
-    a way to improve the security bound on the scheme without imposing
-    artificial requirements on $A$.} %
+\subsection{Bit strings}
+
+Most of our notation for bit strings is standard.  The main thing to note is
+that everything is zero-indexed.
+
+\begin{itemize}
+\item We write $\Bin = \{0, 1\}$ for the set of binary digits.  Then $\Bin^n$
+  is the set of $n$-bit strings, and $\Bin^*$ is the set of all bit strings.
+\item If $x$ is a bit string then $|x|$ is the length of $x$.  If $x \in
+  \Bin^n$ then $|x| = n$.
+\item If $x, y \in \Bin^n$ are strings of bits of the same length then $x
+  \xor y \in \Bin^n$ is their bitwise XOR.
+\item If $x$ and $y$ are bit strings then $x \cat y$ is the result of
+  concatenating $y$ to $x$.  If $z = x \cat y$ then we have $|z| = |x| +
+  |y|$.
+\item The empty string is denoted $\emptystring$.  We have $|\emptystring| =
+  0$, and $x = x \cat \emptystring = \emptystring \cat x$ for all strings $x
+  \in \Bin^*$.
+\item If $x$ is a bit string and $i$ is an integer satisfying $0 \le i < |x|$
+  then $x[i]$ is the $i$th bit of $x$.  If $a$ and $b$ are integers
+  satisfying $0 \le a \le b \le |x|$ then $x[a \bitsto b]$ is the substring
+  of $x$ beginning with bit $a$ and ending just \emph{before} bit $b$.  We
+  have $|x[i]| = 1$ and $|x[a \bitsto b]| = b - a$; if $y = x[a \bitsto b]$
+  then $y[i] = x[a + i]$.
+\item If $x$ is a bit string and $n$ is a natural number then $x^n$ is the
+  result of concatenating $x$ to itself $n$ times.  We have $x^0 =
+  \emptystring$ and if $n > 0$ then $x^n = x^{n-1} \cat x = x \cat x^{n-1}$.
+\end{itemize}
+
+\subsection{Other notation}
+
+\begin{itemize}
+\item If $n$ is any natural number, then $\Nupto{n}$ is the set $\{\, i \in
+  \Z \mid 0 \le i < n \,\} = \{ 0, 1, \ldots, n \}$.
+\item The symbol $\bot$ (`bottom') is different from every bit string and
+  group element.
+\item We write $\Func{l}{L}$ as the set of all functions from $\Bin^l$ to
+  $\Bin^L$, and $\Perm{l}$ as the set of all permutations on $\Bin^l$.
+\end{itemize}
+
+\subsection{Algorithm descriptions}
+
+Most of the notation used in the algorithm descriptions should be obvious.
+We briefly note a few features which may be unfamiliar.
+\begin{itemize}
+\item The notation $a \gets x$ denotes the action of assigning the value $x$
+  to the variable $a$.
+\item The notation $a \getsr X$, where $X$ is a finite set, denotes the
+  action of assigning to $a$ a random value $x \in X$ according to the
+  uniform probability distribution on $X$; i.e., following $a \getsr X$,
+  $\Pr[a = x] = 1/|X|$ for any $x \in X$.
+\end{itemize}
+The notation is generally quite sloppy about types and scopes.  In
+particular, there are implicit coercions between bit strings, integers and
+group elements.  Any simple injective mapping will do for handling the
+conversions.  We don't think these informalities cause much confusion, and
+they greatly simplify the presentation of the algorithms.
+
+\subsection{Random oracles}
+
+We shall analyse the Wrestlers Protocol in the random oracle model
+\cite{Bellare:1993:ROP}.  That is, each participant including the adversary
+is given oracle access (only) to a uniformly-distributed random function
+$H\colon \Bin^* \to \Bin^\infty$ chosen at the beginning of the game: for any
+input string $x$, the oracle can produce, on demand, any prefix of an
+infinitely long random answer $y = H(x)$.  Repeating a query yields a prefix
+of the same random result string; asking a new query yields a prefix of a new
+randomly-chosen string.
+
+We shan't need either to query the oracle on very long input strings nor
+shall we need outputs much longer than a representation of a group index.
+Indeed, since all the programs we shall be dealing with run in finite time,
+and can therefore make only a finite number of oracle queries, each with a
+finitely long result, we can safely think about the random oracle as a finite
+object.
+
+Finally, we shall treat the oracle as a function of multiple inputs and
+expect it to operate on some unambiguous encoding of all of the arguments in
+order.
+
+\subsection{Symmetric encryption}
+
+\begin{definition}[Symmetric encryption]
+  \label{def:sym-enc}
+  A \emph{symmetric encryption scheme} $\mathcal{E} = (E, D)$ is a pair of
+  algorithms:
+  \begin{itemize}
+  \item a randomized \emph{encryption algorithm} $E\colon \keys \mathcal{E}
+    \times \Bin^* \to \Bin^*$; and
+  \item a deterministic \emph{decryption algorithm} $E\colon \keys
+    \mathcal{E} \times \Bin^* \to \Bin^* \cup \{ \bot \}$
+  \end{itemize}
+  with the property that, for any $K \in \keys \mathcal{E}$, any plaintext
+  message $x$, and any ciphertext $y$ returned as a result of $E_K(x)$, we
+  have $D_K(y) = x$.
+\end{definition}  
+
+\begin{definition}[Chosen plaintext security for symmetric encryption]
+  \label{def:sym-cpa}
+  Let $\mathcal{E} = (E, D)$ be a symmetric encryption scheme.  Let $A$ be
+  any algorithm.  Define
+  \begin{program}
+    Experiment $\Expt{lor-cpa-$b$}{\mathcal{E}}(A)$: \+ \\
+      $K \getsr \keys \mathcal{E}$; \\
+      $b' \getsr A^{E_K(\id{lr}(b, \cdot, \cdot))}$; \\
+      \RETURN $b'$;
+    \next
+    Function $\id{lr}(b, x_0, x_1)$: \+ \\
+      \RETURN $x_b$;
+  \end{program}
+  An adversary $A$ is forbidden from querying its encryption oracle
+  $E_K(\id{lr}(b, \cdot, \cdot))$ on a pair of strings with differing
+  lengths.  We define the adversary's \emph{advantage} in this game by
+  \begin{equation}
+    \Adv{lor-cpa}{\mathcal{E}}(A) =
+      \Pr[\Expt{lor-cpa-$1$}{\mathcal{E}}(A) = 1] -
+      \Pr[\Expt{lor-cpa-$0$}{\mathcal{E}}(A) = 1]
+  \end{equation}
+  and the \emph{left-or-right insecurity of $\mathcal{E}$ under
+  chosen-plaintext attack} is given by
+  \begin{equation}
+    \InSec{lor-cpa}(\mathcal{E}; t, q_E, \mu_E) =
+      \max_A \Adv{lor-cpa}{\mathcal{E}}(A)
+  \end{equation}
+  where the maximum is taken over all adversaries $A$ running in time $t$ and
+  making at most $q_E$ encryption queries, totalling most $\mu_E$ bits of
+  plaintext.
+\end{definition}
+
+\subsection{The decision Diffie-Hellman problem}
+
+Let $G$ be some cyclic group.  The standard \emph{Diffie-Hellman problem}
+\cite{Diffie:1976:NDC} is to compute $g^{\alpha\beta}$ given $g^\alpha$ and
+$g^\beta$.  We need a slightly stronger assumption: that, given $g^\alpha$
+and $g^\beta$, it's hard to tell the difference between the correct
+Diffie-Hellman value $g^{\alpha\beta}$ and a randomly-chosen group element
+$g^\gamma$.  This is the \emph{decision Diffie-Hellman problem}
+\cite{Boneh:1998:DDP}.
+
+\begin{definition}
+  \label{def:ddh}
+  Let $G$ be a cyclic group of order $q$, and let $g$ be a generator of $G$.
+  Let $A$ be any algorithm.  Then $A$'s \emph{advantage in solving the
+  decision Diffie-Hellman problem in $G$} is
+  \begin{equation}
+    \begin{eqnalign}[rl]
+      \Adv{ddh}{G}(A) =
+      & \Pr[\alpha \getsr \Nupto{q}; \beta \getsr \Nupto{q} :
+            A(g^\alpha, g^\beta, g^{\alpha\beta}) = 1] - {} \\
+      & \Pr[\alpha \getsr \Nupto{q}; \beta \getsr \Nupto{q};
+            \gamma \getsr \Nupto{q} :
+            A(g^\alpha, g^\beta, g^\gamma) = 1].
+    \end{eqnalign}
+  \end{equation}
+  The \emph{insecurity function of the decision Diffie-Hellman problem in
+  $G$} is
+  \begin{equation}
+    \InSec{ddh}(G; t) = \max_A \Adv{ddh}{G}(A)
+  \end{equation}
+  where the maximum is taken over all algorithms $A$ which run in time $t$.
+\end{definition}
+
+%%%--------------------------------------------------------------------------
+
+\section{The protocol}
+\label{sec:protocol}
+
+The Wrestlers Protocol is parameterized.  We need the following things:
+\begin{itemize}
+\item A cyclic group $G$ whose order~$q$ is prime.  Let $g$ be a generator
+  of~$G$.  We require that the (decision?\fixme) Diffie-Hellman problem be
+  hard in~$G$.  The group operation is written multiplicatively.
+\item A symmetric encryption scheme $\mathcal{E} = (E, D)$.  We require that
+  $\mathcal{E}$ be secure against adaptive chosen-plaintext attacks.  Our
+  implementation uses Blowfish \cite{Schneier:1994:BEA} in CBC mode with
+  ciphertext stealing.  See section~\ref{sec:cbc} for a description of
+  ciphertext stealing and an analysis of its security.
+\item A message authentication scheme $\mathcal{M} = (T, V)$.  We require
+  that $\mathcal{M}$ be (strongly) existentially unforgeable under
+  chosen-message attacks.  Our implementation uses RIPEMD-160
+  \cite{Dobbertin:1996:RSV} in the HMAC \cite{Bellare:1996:HC} construction.
+\item An instantiation for the random oracle.  We use RIPEMD-160 again,
+  either on its own, if the output is long enough, or in the MGF-1
+  \cite{RFC2437} construction, if we need a larger output.\footnote{%
+    The use of the same hash function in the MAC as for instantiating the
+    random oracle is deliberate, with the aim of reducing the number of
+    primitives whose security we must assume.  In an application of HMAC, the
+    message to be hashed is prefixed by a secret key padded out to the hash
+    function's block size.  In a `random oracle' query, the message is
+    prefixed by a fixed identification string and not padded.  Interference
+    between the two is then limited to the case where one of the HMAC keys
+    matches a random oracle prefix, which happens only with very tiny
+    probability.}%
+\end{itemize}
+
+An authenticated encryption scheme with associated data (AEAD)
+\cite{Rogaway:2002:AEAD, Rogaway:2001:OCB, Kohno:2003:CWC} could be used
+instead of a separate symmetric encryption scheme and MAC.
+
+\subsection{Symmetric encryption}
+
+The same symmetric encryption subprotocol is used both within the key
+exchange, to ensure secrecy and binding, and afterwards for message
+transfer.  It provides a secure channel between two players, assuming that
+the key was chosen properly.
+
+A \id{keyset} contains the state required for communication between the two
+players.  In particular it maintains:
+\begin{itemize}
+\item separate encryption and MAC keys in each direction (four keys in
+  total), chosen using the random oracle based on an input key assumed to be
+  unpredictable by the adversary and a pair of nonces chosen by the two
+  players; and
+\item incoming and outgoing sequence numbers, to detect and prevent replay
+  attacks.
+\end{itemize}
+
+The operations involved in the symmetric encryption protocol are shown in
+figure~\ref{fig:keyset}.
+
+The \id{keygen} procedure initializes a \id{keyset}, resetting the sequence
+numbers, and selecting keys for the encryption scheme and MAC using the
+random oracle.  It uses the nonces $r_A$ and $r_B$ to ensure that with high
+probability the keys are different for the two directions: assuming that
+Alice chose her nonce $r_A$ at random, and that the keys and nonce are
+$\kappa$~bits long, the probability that the keys in the two directions are
+the same is at most $2^{\kappa - 2}$.
+
+The \id{encrypt} procedure constructs a ciphertext from a message $m$ and a
+\emph{message type} $\id{ty}$.  It encrypts the message giving a ciphertext
+$y$, and computes a MAC tag $\tau$ for the triple $(\id{ty}, i, y)$, where
+$i$ is the next available outgoing sequence number.  The ciphertext message
+to send is then $(i, y, \tau)$.  The message type codes are used to
+separate ciphertexts used by the key-exchange protocol itself from those sent
+by the players later.
+
+The \id{decrypt} procedure recovers the plaintext from a ciphertext triple
+$(i, y, \tau)$, given its expected type code $\id{ty}$.  It verifies that the
+tag $\tau$ is valid for the message $(\id{ty}, i, y)$, checks that the
+sequence number $i$ hasn't been seen before,\footnote{%
+  The sequence number checking shown in the figure is simple but obviously
+  secure.  The actual implementation maintains a window of 32 previous
+  sequence numbers, to allow out-of-order reception of messages while still
+  preventing replay attacks.  This doesn't affect our analysis.}%
+and then decrypts the ciphertext $y$.
+
+\begin{figure}
+  \begin{program}
+    Structure $\id{keyset}$: \+ \\
+      $\Xid{K}{enc-in}$; $\Xid{K}{enc-out}$; \\
+      $\Xid{K}{mac-in}$; $\Xid{K}{mac-out}$; \\
+      $\id{seq-in}$; $\id{seq-out}$; \- \\[\medskipamount]
+    Function $\id{gen-keys}(r_A, r_B, K)$: \+ \\
+      $k \gets \NEW \id{keyset}$; \\
+      $k.\Xid{K}{enc-in} \gets H(\cookie{encryption}, r_A, r_B, K)$; \\
+      $k.\Xid{K}{enc-out} \gets H(\cookie{encryption}, r_B, r_A, K)$; \\
+      $k.\Xid{K}{mac-in} \gets H(\cookie{integrity}, r_A, r_B, K)$; \\
+      $k.\Xid{K}{mac-out} \gets H(\cookie{integrity}, r_B, r_A, K)$; \\
+      $k.\id{seq-in} \gets 0$; \\
+      $k.\id{seq-out} \gets 0$; \\
+      \RETURN $k$;
+    \next
+    Function $\id{encrypt}(k, \id{ty}, m)$: \+ \\
+      $y \gets (E_{k.\Xid{K}{enc-out}}(m))$; \\
+      $i \gets k.\id{seq-out}$; \\
+      $\tau \gets T_{k.\Xid{K}{mac-out}}(\id{ty}, i, y)$; \\
+      $k.\id{seq-out} \gets i + 1$; \\
+      \RETURN $(i, y, \tau)$; \- \\[\medskipamount]
+    Function $\id{decrypt}(k, \id{ty}, c)$: \+ \\
+      $(i, y, \tau) \gets c$; \\
+      \IF $V_{k.\Xid{K}{mac-in}}((\id{ty}, i, y), \tau) = 0$ \THEN \\ \ind
+        \RETURN $\bot$; \- \\
+      \IF $i < k.\id{seq-in}$ \THEN \RETURN $\bot$; \\
+      $m \gets D_{k.\Xid{K}{enc-in}}(y)$; \\
+      $k.\id{seq-in} \gets i + 1$; \\
+      \RETURN $m$;
+  \end{program}
+
+  \caption{Symmetric-key encryption functions}
+  \label{fig:keyset}
+\end{figure}
+
+\subsection{The key-exchange}
+
+The key-exchange protocol is completely symmetrical.  Either party may
+initiate, or both may attempt to converse at the same time.  We shall
+describe the protocol from the point of view of Alice attempting to exchange
+a key with Bob.
+
+Alice's private key is a random index $\alpha \inr \Nupto{q}$.  Her public
+key is $a = g^\alpha$.  Bob's public key is $b \in G$.  We'll subscript the
+variables Alice computes with an~$A$, and the values Bob has sent with a~$B$.
+Of course, if Bob is following the protocol correctly, he will have computed
+his $B$ values in a completely symmetrical way.
+
+There are six messages in the protocol, and we shall briefly discuss the
+purpose of each before embarking on the detailed descriptions.  At the
+beginning of the protocol, Alice chooses a new random index $\rho_A$ and
+computes her \emph{challenge} $r_A = g^{\rho_A}$.  Eventually, the shared
+secret key will be computed as $K = r_B^{\rho_A} = r_A^{\rho_B} =
+g^{\rho_A\rho_B}$, as for standard Diffie-Hellman key agreement.
+
+Throughout, we shall assume that messages are implicitly labelled with the
+sender's identity.  If Alice is actually trying to talk to several other
+people she'll need to run multiple instances of the protocol, each with its
+own state, and she can use the sender label to decide which instance a
+message should be processed by.  There's no need for the implicit labels to
+be attached securely.
+
+We'll summarize the messages and their part in the scheme of things before we
+start on the serious detail.  For a summary of the names and symbols used in
+these descriptions, see table~\ref{tab:kx-names}.  The actual message
+contents are summarized in table~\ref{tab:kx-messages}.  A state-transition
+diagram of the protocol is shown in figure~\ref{fig:kx-states}.  If reading
+pesudocode algorithms is your thing then you'll find message-processing
+procedures in figure~\ref{fig:kx-messages} with the necessary support procedures
+in figure~\ref{fig:kx-support}.
+
+\begin{table}
+  \begin{tabularx}{\textwidth}{Mr X}
+    G                     & A cyclic group known by all participants \\
+    q = |G|               & The prime order of $G$ \\
+    g                     & A generator of $G$ \\
+    E_K(\cdot)            & Encryption under key $K$, here used to denote
+                            application of the $\id{encrypt}(K, \cdot)$
+                            operation \\ 
+    \alpha \inr \Nupto{q} & Alice's private key \\
+    a = g^{\alpha}        & Alice's public key \\
+    \rho_A \inr \Nupto{q} & Alice's secret Diffie-Hellman value \\
+    r_A = g^{\rho_A}      & Alice's public \emph{challenge} \\
+    c_A = H(\cookie{cookie}, r_A)
+                          & Alice's \emph{cookie} \\
+    v_A = \rho_A \xor H(\cookie{expected-reply}, r_A, r_B, b^{\rho_A})
+                          & Alice's challenge \emph{check value} \\
+    r_B^\alpha = a^{\rho_B}
+                          & Alice's reply \\
+    K = r_B^{\rho_A} = r_B^{\rho_A} = g^{\rho_A\rho_B}
+                          & Alice and Bob's shared secret key \\
+    w_A = H(\cookie{switch-request}, c_A, c_B)
+                          & Alice's \emph{switch request} value \\
+    u_A = H(\cookie{switch-confirm}, c_A, c_B)
+                          & Alice's \emph{switch confirm} value \\
+  \end{tabularx}
+
+  \caption{Names used during key-exchange}
+  \label{tab:kx-names}
+\end{table}
+
+\begin{table}
+  \begin{tabular}[C]{Ml}
+    \cookie{kx-pre-challenge}, r_A \\
+    \cookie{kx-cookie}, r_A, c_B \\
+    \cookie{kx-challenge}, r_A, c_B, v_A \\
+    \cookie{kx-reply}, c_A, c_B, v_A, E_K(r_B^\alpha)) \\
+    \cookie{kx-switch}, c_A, c_B, E_K(r_B^\alpha, w_A)) \\
+    \cookie{kx-switch-ok}, E_K(u_A))
+  \end{tabular}
+
+  \caption{Message contents, as sent by Alice}
+  \label{tab:kx-messages}
+\end{table}
   
-  It remains to show that if $A$ never queries its random oracle on
-  $g^{\alpha\beta}$ then it cannot distinguish the random check value $r$
-  from the correct one $\beta \xor \H(g^{\alpha\beta})$, and hence won't
-  notice that $A'$ is lying to it.  But this is obvious: $A$'s probability of
-  guessing the random value that would have been returned had it actually
-  queried $\Hsim$ on the input $g^{\alpha\beta}$ is equal to the probability
-  of it guessing $\beta \xor r$ instead, since $\Hsim$ chooses its responses
-  uniformly at random.  This completes the proof.
-\end{proof}
+\begin{messages}
+\item[kx-pre-challenge] Contains a plain statement of Alice's challenge.
+  This is Alice's first message of a session.
+\item[kx-cookie] A bare acknowledgement of a received challenge: it restates
+  Alice's challenge, and contains a hash of Bob's challenge.  This is an
+  engineering measure (rather than a cryptographic one) which prevents
+  trivial denial-of-service attacks from working.
+\item[kx-challenge] A full challenge, with a `check value' which proves the
+  challenge's honesty.  Bob's correct reply to this challenge informs Alice
+  that she's received his challenge correctly.
+\item[kx-reply] A reply.  This contains a `check value', like the
+  \cookie{kx-challenge} message above, and an encrypted reply which confirms
+  to Bob Alice's successful receipt of his challenge and lets Bob know he
+  received Alice's challenge correctly.
+\item[kx-switch] Acknowledges Alice's receipt of Bob's \cookie{kx-reply}
+  message, including Alice's own reply to Bob's challenge.  Tells Bob that
+  she can start using the key they've agreed.
+\item[kx-switch-ok] Acknowlegement to Bob's \cookie{kx-switch} message.
+\end{messages}
+
+\begin{figure}
+  \small
+  \let\ns\normalsize
+  \let\c\cookie
+  \[ \begin{graph}
+     []!{0; <4.5cm, 0cm>: <0cm, 1.5cm>::}
+     *++[F:<4pt>]\txt{\ns Start \\ Choose $\rho_A$} ="start"
+     :[dd]
+     *++[F:<4pt>]\txt{
+       \ns State \c{challenge} \\
+       Send $(\c{pre-challenge}, r_A)$}
+     ="chal"
+     [] "chal" !{!L(0.5)} ="chal-cookie"
+     :@(d, d)[l]
+     *+\txt{Send $(\c{cookie}, r_A, c_B)$}
+     ="cookie"
+     |*+\txt{Receive \\ $(\c{pre-challenge}, r_B)$ \\ (no spare slot)}
+     :@(u, u)"chal-cookie"
+     "chal" :@/_0.8cm/ [ddddl]
+     *+\txt{Send \\ $(\c{challenge}, $\\$ r_A, c_B, v_A)$}
+     ="send-chal"
+     |<>(0.67) *+\txt\small{
+       Receive \\ $(\c{pre-challenge}, r_B)$ \\ (spare slot)}
+     "chal" :@/^0.8cm/ "send-chal" |<>(0.33)
+     *+\txt{Receive \\ $(\c{cookie}, r_B, c_A)$}
+     :[rr]
+     *+\txt{Send \\ $(\c{reply}, c_A, c_B, $\\$ v_A, E_K(r_B^\alpha))$}
+     ="send-reply"
+     |*+\txt{Receive \\ $(\c{challenge}, $\\$ r_B, c_A, v_B)$}
+     "chal" :"send-reply"
+     |*+\txt{Receive \\ $(\c{challenge}, $\\$ r_B, c_A, v_B)$}
+     "send-chal" :[ddd]
+     *++[F:<4pt>]\txt{
+       \ns State \c{commit} \\
+       Send \\ $(\c{switch}, c_A, c_B, $\\$ E_K(r_B^\alpha, w_A))$}
+     ="commit"
+     |*+\txt{Receive \\ $(\c{reply}, c_B, c_A, $\\$ v_B, E_K(b^{\rho_A}))$}
+     :[rr]
+     *+\txt{Send \\ $(\c{switch-ok}, E_K(u_A))$}
+     ="send-switch-ok"
+     |*+\txt{Receive \\ $(\c{switch}, c_B, c_A, $\\$ E_K(b^{\rho_A}, w_B))$}
+     "send-reply" :"commit"
+     |*+\txt{Receive \\ $(\c{reply}, c_B, c_A, $\\$ v_B, E_K(b^{\rho_A}))$}
+     "send-reply" :"send-switch-ok"
+     |*+\txt{Receive \\ $(\c{switch}, c_B, c_A, $\\$ E_K(b^{\rho_A}, w_B))$}
+     :[dddl]
+     *++[F:<4pt>]\txt{\ns Done}
+     ="done"
+     "commit" :"done"
+     |*+\txt{Receive \\ $(\c{switch-ok}, E_K(u_B))$}
+     "send-chal" [r] !{+<0cm, 0.75cm>}
+     *\txt\itshape{For each outstanding challenge}
+     ="for-each"
+     !{"send-chal"+DL-<8pt, 8pt> ="p0",
+       "for-each"+U+<8pt> ="p1",
+       "send-reply"+UR+<8pt, 8pt> ="p2",
+       "send-reply"+DR+<8pt, 8pt> ="p3",
+       "p0" !{"p1"-"p0"} !{"p2"-"p1"} !{"p3"-"p2"}
+      *\frm<8pt>{--}}
+  \end{graph} \]
+
+  \caption{State-transition diagram for key-exchange protocol}
+  \label{fig:kx-states}
+\end{figure}
+
+We now describe the protocol message by message, and Alice's actions when she
+receives each.  Since the protocol is completely symmetrical, Bob should do
+the same, only swapping round $A$ and $B$ subscripts, the public keys $a$ and
+$b$, and using his private key $\beta$ instead of $\alpha$.
+
+\subsubsection{Starting the protocol}
+
+As described above, at the beginning of the protocol Alice chooses a random
+$\rho_A \inr \Nupto q$, and computes her \emph{challenge} $r_A = g^{\rho_A}$
+and her \emph{cookie} $c_A = H(\cookie{cookie}, r_A)$.  She sends her
+announcement of her challenge as
+\begin{equation}
+  \label{eq:kx-pre-challenge}
+  \cookie{kx-pre-challenge}, r_A
+\end{equation}
+and enters the \cookie{challenge} state.
+
+\subsubsection{The \cookie{kx-pre-challenge} message}
+
+If Alice receieves a \cookie{kx-pre-challenge}, she ensures that she's in the
+\cookie{challenge} state: if not, she rejects the message.
+
+She must first calculate Bob's cookie $c_B = H(\cookie{cookie}, r_B)$.  Then
+she has a choice: either she can send a full challenge, or she can send the
+cookie back.
+
+Suppose she decides to send a full challenge.  She must compute a \emph{check
+value}
+\begin{equation}
+  \label{eq:v_A}
+  v_A = \rho_A \xor H(\cookie{expected-reply}, r_A, r_B, b^{\rho_A})
+\end{equation}
+and sends
+\begin{equation}
+  \label{eq:kx-challenge}
+  \cookie{kx-challenge}, r_A, c_B, v_A
+\end{equation}
+to Bob.  Then she remembers Bob's challenge for later use, and awaits his
+reply.
+
+If she decides to send only a cookie, she just transmits
+\begin{equation}
+  \label{eq:kx-cookie}
+  \cookie{kx-cookie}, r_A, c_B
+\end{equation}
+to Bob and forgets all about it.
+
+Why's this useful?  Well, if Alice sends off a full \cookie{kx-challenge}
+message, she must remember Bob's $r_B$ so she can check his reply and that
+involves using up a table slot.  That means that someone can send Alice
+messages purporting to come from Bob which will chew up Alice's memory, and
+they don't even need to be able to read Alice's messages to Bob to do that.
+If this protocol were used over the open Internet, script kiddies from all
+over the world might be flooding Alice with bogus \cookie{kx-pre-challenge}
+messages and she'd never get around to talking to Bob.
+
+By sending a cookie intead, she avoids committing a table slot until Bob (or
+someone) sends either a cookie or a full challenge, thus proving, at least,
+that he can read her messages.  This is the best we can do at this stage in
+the protocol.  Against an adversary as powerful as the one we present in
+section~\fixme\ref{sec:formal} this measure provides no benefit (but we have
+to analyse it anyway); but it raises the bar too sufficiently high to
+eliminate a large class of `nuisance' attacks in the real world.
+
+Our definition of the Wrestlers Protocol doesn't stipulate when Alice should
+send a full challenge or just a cookie: we leave this up to individual
+implementations, because it makes no difference to the security of the
+protocol against powerful adversaries.  But we recommend that Alice proceed
+`optimistically' at first, sending full challenges until her challenge table
+looks like it's running out, and then generating cookies only if it actually
+looks like she's under attack.  This is what our pseudocode in
+figure~\ref{fig:kx-messages} does.
 
-We conclude here that the Wrestlers Authentication Protocol is a secure
-authentication protocol in the random oracle model: impersonation is hard if
-the Diffie-Hellman problem is hard, and proving one's identity doesn't leak
-secret key information.
+\subsubsection{The \cookie{kx-cookie} message}
 
-\subsection{Requirements on hash functions}
+When Alice receives a \cookie{kx-cookie} message, she must ensure that she's
+in the \cookie{challenge} state: if not, she rejects the message.  She checks
+the cookie in the message against the value of $c_A$ she computed earlier.
+If all is well, Alice sends a \cookie{kx-challenge} message, as in
+equation~\ref{eq:kx-challenge} above.
 
-Having seen that the Wrestlers Authentication Protocol is secure in the
-random oracle model, we now ask which properties we require from the hash
-function.  This at least demonstrates that the protocol isn't deeply flawed,
-and suggests an efficient implementation in terms of conventional hash
-functions.
+This time, she doesn't have a choice about using up a table slot to remember
+Bob's $r_B$.  If her table size is fixed, she must choose a slot to recycle.
+We suggest simply recycling slots at random: this means there's no clever
+pattern of \cookie{kx-cookie} messages an attacker might be able to send to
+clog up all of Alice's slots.
 
-Here we investigate more carefully the properties required of the hash
-function, and provide a more quantitative analysis of the protocol.
+\subsubsection{The \cookie{kx-challenge} message}
 
-Looking at the proofs of the previous two sections, we see that the random
-oracles are mainly a device which allow our constructions to `grab hold' of
-the hashing operations performed by the adversary.
+
+
+\begin{figure}
+  \begin{program}
+    Procedure $\id{kx-initialize}$: \+ \\
+      $\rho_A \getsr [q]$; \\
+      $r_a \gets g^{\rho_A}$; \\
+      $\id{state} \gets \cookie{challenge}$; \\
+      $\Xid{n}{chal} \gets 0$; \\
+      $k \gets \bot$; \\
+      $\id{chal-commit} \gets \bot$; \\
+      $\id{send}(\cookie{kx-pre-challenge}, r_A)$; \- \\[\medskipamount]
+    Procedure $\id{kx-receive}(\id{type}, \id{data})$: \\ \ind
+      \IF $\id{type} = \cookie{kx-pre-challenge}$ \THEN \\ \ind
+        \id{msg-pre-challenge}(\id{data}); \- \\
+      \ELSE \IF $\id{type} = \cookie{kx-cookie}$ \THEN \\ \ind
+        \id{msg-cookie}(\id{data}); \- \\
+      \ELSE \IF $\id{type} = \cookie{kx-challenge}$ \THEN \\ \ind
+        \id{msg-challenge}(\id{data}); \- \\
+      \ELSE \IF $\id{type} = \cookie{kx-reply}$ \THEN \\ \ind
+        \id{msg-reply}(\id{data}); \- \\
+      \ELSE \IF $\id{type} = \cookie{kx-switch}$ \THEN \\ \ind
+        \id{msg-switch}(\id{data}); \- \\
+      \ELSE \IF $\id{type} = \cookie{kx-switch-ok}$ \THEN \\ \ind
+        \id{msg-switch-ok}(\id{data}); \-\- \\[\medskipamount]
+    Procedure $\id{msg-pre-challenge}(\id{data})$: \+ \\
+      \IF $\id{state} \ne \cookie{challenge}$ \THEN \RETURN; \\
+      $r \gets \id{data}$; \\
+      \IF $\Xid{n}{chal} \ge \Xid{n}{chal-thresh}$ \THEN \\ \ind
+        $\id{send}(\cookie{kx-cookie}, r_A, \id{cookie}(r_A)))$; \- \\
+      \ELSE \+ \\
+        $\id{new-chal}(r)$; \\
+        $\id{send}(\cookie{kx-challenge}, r_A,
+                   \id{cookie}(r), \id{checkval}(r))$; \-\-\\[\medskipamount]
+    Procedure $\id{msg-cookie}(\id{data})$: \+ \\
+      \IF $\id{state} \ne \cookie{challenge}$ \THEN \RETURN; \\
+      $(r, c_A) \gets \id{data}$; \\
+      \IF $c_A \ne \id{cookie}(r_A)$ \THEN \RETURN; \\
+      $\id{new-chal}(r)$; \\
+      $\id{send}(\cookie{kx-challenge}, r_A,
+                 \id{cookie}(r), \id{checkval}(r))$; \- \\[\medskipamount]
+    Procedure $\id{msg-challenge}(\id{data})$: \+ \\
+      \IF $\id{state} \ne \cookie{challenge}$ \THEN \RETURN; \\
+      $(r, c_A, v) \gets \id{data}$; \\
+      \IF $c_A \ne \id{cookie}(r_A)$ \THEN \RETURN; \\
+      $i \gets \id{check-reply}(\bot, r, v)$; \\
+      \IF $i = \bot$ \THEN \RETURN; \\
+      $k \gets \id{chal-tab}[i].k$; \\
+      $y \gets \id{encrypt}(k, \cookie{kx-reply}, r^\alpha)$; \\
+      $\id{send}(\cookie{kx-reply}, c_A, \id{cookie}(r),
+                 \id{checkval}(r), y)$
+    \next
+    Procedure $\id{msg-reply}(\id{data})$: \+ \\
+      $(c, c_A, v, y) \gets \id{data}$; \\
+      \IF $c_A \ne \id{cookie}(r_A)$ \THEN \RETURN; \\
+      $i \gets \id{find-chal}(c)$; \\
+      \IF $i = \bot$ \THEN \RETURN; \\
+      \IF $\id{check-reply}(i, \id{chal-tab}[i].r, v) = \bot$ \THEN \\ \ind
+        \RETURN; \- \\
+      $k \gets \id{chal-tab}[i].k$; \\
+      $x \gets \id{decrypt}(k, \cookie{kx-reply}, y)$; \\
+      \IF $x = \bot$ \THEN \RETURN; \\
+      \IF $x \ne b^{\rho_A}$ \THEN \RETURN; \\
+      $\id{state} \gets \cookie{commit}$; \\
+      $\id{chal-commit} \gets \id{chal-tab}[i]$; \\
+      $w \gets H(\cookie{switch-request}, c_A, c)$; \\
+      $x \gets \id{chal-tab}[i].r^\alpha$; \\
+      $y \gets \id{encrypt}(k, (x, \cookie{kx-switch}, w))$; \\
+      $\id{send}(\cookie{kx-switch}, c_A, c, y)$; \-\\[\medskipamount]
+    Procedure $\id{msg-switch}(\id{data})$: \+ \\
+      $(c, c_A, y) \gets \id{data}$; \\
+      \IF $c_A \ne \cookie(r_A)$ \THEN \RETURN; \\
+      $i \gets \id{find-chal}(c)$; \\
+      \IF $i = \bot$ \THEN \RETURN; \\
+      $k \gets \id{chal-tab}[i].k$; \\
+      $x \gets \id{decrypt}(k, \cookie{kx-switch}, y)$; \\
+      \IF $x = \bot$ \THEN \RETURN; \\
+      $(x, w) \gets x$; \\
+      \IF $\id{state} = \cookie{challenge}$ \THEN \\ \ind
+        \IF $x \ne b^{\rho_A}$ \THEN \RETURN; \\
+        $\id{chal-commit} \gets \id{chal-tab}[i]$; \- \\
+      \ELSE \IF $c \ne \id{chal-commit}.c$ \THEN \RETURN; \\
+      \IF $w \ne H(\cookie{switch-request}, c, c_A)$ \THEN \RETURN; \\
+      $w \gets H(\cookie{switch-confirm}, c_A, c)$; \\
+      $y \gets \id{encrypt}(y, \cookie{kx-switch-ok}, w)$; \\
+      $\id{send}(\cookie{switch-ok}, y)$; \\
+      $\id{done}(k)$; \- \\[\medskipamount]
+    Procedure $\id{msg-switch-ok}(\id{data})$ \+ \\
+      \IF $\id{state} \ne \cookie{commit}$ \THEN \RETURN; \\
+      $y \gets \id{data}$; \\
+      $k \gets \id{chal-commit}.k$; \\
+      $w \gets \id{decrypt}(k, \cookie{kx-switch-ok}, y)$; \\
+      \IF $w = \bot$ \THEN \RETURN; \\
+      $c \gets \id{chal-commit}.c$; \\
+      $c_A \gets \id{cookie}(r_A)$; \\
+      \IF $w \ne H(\cookie{switch-confirm}, c, c_A)$ \THEN \RETURN; \\
+      $\id{done}(k)$;
+  \end{program}
+
+  \caption{The key-exchange protocol: message handling}
+  \label{fig:kx-messages}
+\end{figure}
+
+\begin{figure}
+  \begin{program}
+    Structure $\id{chal-slot}$: \+ \\
+      $r$; $c$; $\id{replied}$; $k$; \- \\[\medskipamount]
+    Function $\id{find-chal}(c)$: \+ \\
+      \FOR $i = 0$ \TO $\Xid{n}{chal}$ \DO \\ \ind
+        \IF $\id{chal-tab}[i].c = c$ \THEN \RETURN $i$; \- \\
+      \RETURN $\bot$; \- \\[\medskipamount]
+    Function $\id{cookie}(r)$: \+ \\
+      \RETURN $H(\cookie{cookie}, r)$; \- \\[\medskipamount]
+    Function $\id{check-reply}(i, r, v)$: \+ \\
+      \IF $i \ne \bot \land \id{chal-tab}[i].\id{replied} = 1$ \THEN \\ \ind
+        \RETURN $i$; \- \\
+      $\rho \gets v \xor H(\cookie{expected-reply}, r, r_A, r^\alpha)$; \\
+      \IF $g^\rho \ne r$ \THEN \RETURN $\bot$; \\
+      \IF $i = \bot$ \THEN $i \gets \id{new-chal}(r)$; \\
+      $\id{chal-tab}[i].k \gets \id{gen-keys}(r_A, r, r^{\rho_A})$; \\
+      $\id{chal-tab}[i].\id{replied} \gets 1$; \\
+      \RETURN $i$;
+    \next
+    Function $\id{checkval}(r)$: \\ \ind
+      \RETURN $\rho_A \xor H(\cookie{expected-reply},
+                             r_A,r, b^{\rho_A})$; \- \\[\medskipamount]
+    Function $\id{new-chal}(r)$: \+ \\
+      $c \gets \id{cookie}(r)$; \\
+      $i \gets \id{find-chal}(c)$; \\
+      \IF $i \ne \bot$ \THEN \RETURN $i$; \\
+      \IF $\Xid{n}{chal} < \Xid{n}{chal-max}$ \THEN \\ \ind
+        $i \gets \Xid{n}{chal}$; \\
+        $\id{chal-tab}[i] \gets \NEW \id{chal-slot}$; \\
+        $\Xid{n}{chal} \gets \Xid{n}{chal} + 1$; \- \\
+      \ELSE \\ \ind
+        $i \getsr [\Xid{n}{chal-max}]$; \- \\
+      $\id{chal-tab}[i].r \gets r$; \\
+      $\id{chal-tab}[i].c \gets c$; \\
+      $\id{chal-tab}[i].\id{replied} \gets 0$; \\
+      $\id{chal-tab}[i].k \gets \bot$; \\
+      \RETURN $i$;
+  \end{program}
+
+  \caption{The key-exchange protocol: support functions}
+  \label{fig:kx-support}
+\end{figure}
 
 %%%--------------------------------------------------------------------------
 
-\section{A key-exchange protocol}
-% Present the Wrestlers protocol in all its glory.  Show, by means of the
-% previous proofs, that the Wrestlers protocol is simulatable in the
-% authenticated model using a much simpler protocol.  Show that the simpler
-% protocol is SK-secure.
+\section{CBC mode encryption}
+\label{sec:cbc}
+
+Our implementation of the Wrestlers Protocol uses Blowfish
+\cite{Schneier:1994:BEA} in CBC mode.  However, rather than pad plaintext
+messages to a block boundary, with the ciphertext expansion that entails, we
+use a technique called \emph{ciphertext stealing}
+\cite[section 9.3]{Schneier:1996:ACP}.
+
+\subsection{Standard CBC mode}
+
+Suppose $E$ is an $\ell$-bit pseudorandom permutation.  Normal CBC mode works
+as follows.  Given a message $X$, we divide it into blocks $x_0, x_1, \ldots,
+x_{n-1}$.  Choose a random \emph{initialization vector} $I \inr \Bin^\ell$.
+Before passing each $x_i$ through $E$, we XOR it with the previous
+ciphertext, with $I$ standing in for the first block:
+\begin{equation}
+  y_0 = E_K(x_0 \xor I) \qquad
+  y_i = E_K(x_i \xor y_{i-1} \ \text{(for $1 \le i < n$)}.
+\end{equation}
+The ciphertext is then the concatenation of $I$ and the $y_i$.  Decryption is
+simple:
+\begin{equation}
+  x_0 = E^{-1}_K(y_0) \xor I \qquad
+  x_i = E^{-1}_K(y_i) \xor y_{i-1} \ \text{(for $1 \le i < n$)}
+\end{equation}
+See figure~\ref{fig:cbc} for a diagram of CBC encryption.
+
+\begin{figure}
+  \[ \begin{graph}
+    []!{0; <0.85cm, 0cm>: <0cm, 0.5cm>::}
+    *+=(1, 0)+[F]{\mathstrut x_0}="x"
+      :[dd] *{\xor}="xor"
+      [ll] *+=(1, 0)+[F]{I} :"xor"
+      :[dd] *+[F]{E}="e" :[ddd] *+=(1, 0)+[F]{\mathstrut y_0}="i"
+      "e" [l] {K} :"e"
+    [rrruuuu] *+=(1, 0)+[F]{\mathstrut x_1}="x"
+      :[dd] *{\xor}="xor"
+      "e" [d] :`r [ru] `u "xor" "xor"
+      :[dd] *+[F]{E}="e" :[ddd]
+      *+=(1, 0)+[F]{\mathstrut y_1}="i"
+      "e" [l] {K} :"e"
+    [rrruuuu] *+=(1, 0)+[F--]{\mathstrut x_i}="x"
+      :@{-->}[dd] *{\xor}="xor"
+      "e" [d] :@{-->}`r [ru] `u "xor" "xor"
+      :@{-->}[dd] *+[F]{E}="e" :@{-->}[ddd]
+      *+=(1, 0)+[F--]{\mathstrut y_i}="i"
+      "e" [l] {K} :@{-->}"e"
+    [rrruuuu] *+=(1, 0)+[F]{\mathstrut x_{n-1}}="x"
+      :[dd] *{\xor}="xor"
+      "e" [d] :@{-->}`r [ru] `u "xor" "xor"
+      :[dd] *+[F]{E}="e" :[ddd]
+      *+=(1, 0)+[F]{\mathstrut y_{n-1}}="i"
+      "e" [l] {K} :"e"
+  \end{graph} \]
+
+  \caption{Encryption using CBC mode}
+  \label{fig:cbc}
+\end{figure}
+    
+\begin{definition}[CBC mode]
+  \label{def:cbc}
+  Let $P\colon \keys P \times \Bin^\ell to \Bin^\ell$ be a pseudorandom
+  permutation.  We define the symmetric encryption scheme
+  $\Xid{\mathcal{E}}{CBC}^P = (\Xid{E}{CBC}^P, \Xid{D}{CBC}^P)$ for messages
+  in $\Bin^{\ell\Z}$ by setting $\keys \Xid{\mathcal{E}}{CBC} = \keys P$ and
+  defining the encryption and decryption algorithms as follows:
+  \begin{program}
+    Algorithm $\Xid{E}{CBC}^P_K(x)$: \+ \\
+      $I \getsr \Bin^\ell$; \\
+      $y \gets I$; \\
+      \FOR $i = 0$ \TO $|x|/\ell$ \DO \\ \ind
+        $x_i \gets x[\ell i \bitsto \ell (i + 1)]$; \\
+        $y_i \gets P_K(x_i \xor I)$; \\
+        $I \gets y_i$; \\
+        $y \gets y \cat y_i$; \- \\
+      \RETURN $y$;
+    \next
+    Algorithm $\Xid{D}{CBC}^P_K(y)$: \+ \\
+      $I \gets y[0 \bitsto \ell]$; \\
+      $x \gets \emptystring$; \\
+      \FOR $1 = 0$ \TO $|y|/\ell$ \DO \\ \ind
+        $y_i \gets y[\ell i  \bitsto  \ell (i + 1)]$; \\
+        $x_i \gets P^{-1}_K(y_i) \xor I$; \\
+        $I \gets y_i$; \\
+        $x \gets x \cat x_i$; \- \\
+      \RETURN $x$;
+  \end{program}
+\end{definition}
+
+\begin{theorem}[Security of standard CBC mode]
+  \label{thm:cbc}
+  Let $P\colon \keys P \times \Bin^\ell \to \Bin^\ell$ be a pseudorandom
+  permutation.  Then,
+  \begin{equation}
+    \InSec{lor-cpa}(\Xid{\mathcal{E}}{CBC}; t, q_E + \mu_E) \le
+      2 \cdot \InSec{prp}(P; t + q t_P, q) +
+      \frac{q (q - 1)}{2^\ell - 2^{\ell/2}}
+  \end{equation}
+  where $q = \mu_E/\ell$ and $t_P$ is some small constant.
+\end{theorem}
+
+\begin{note}
+  Our security bound is slightly better than that of \cite[theorem
+  17]{Bellare:2000:CST}.  Their theorem statement contains a term $3 \cdot q
+  (q - 1) 2^{-\ell-1}$.  Our result lowers the factor from 3 to just over 2.
+  Our proof is also much shorter and considerably more comprehensible.
+\end{note}
+
+The proof of this theorem is given in section~\ref{sec:cbc-proof}
+
+\subsection{Ciphertext stealing}
+
+Ciphertext stealing allows us to encrypt any message in $\Bin^*$ and make the
+ciphertext exactly $\ell$ bits longer than the plaintext.  See
+figure~\ref{fig:cbc-steal} for a diagram.
+
+\begin{figure}
+  \[ \begin{graph}
+    []!{0; <0.85cm, 0cm>: <0cm, 0.5cm>::}
+    *+=(1, 0)+[F]{\mathstrut x_0}="x"
+      :[dd] *{\xor}="xor"
+      [ll] *+=(1, 0)+[F]{I} :"xor"
+      :[dd] *+[F]{E}="e" :[ddddd] *+=(1, 0)+[F]{\mathstrut y_0}="i"
+      "e" [l] {K} :"e"
+    [rrruuuu] *+=(1, 0)+[F]{\mathstrut x_1}="x"
+      :[dd] *{\xor}="xor"
+      "e" [d] :`r [ru] `u "xor" "xor"
+      :[dd] *+[F]{E}="e" :[ddddd]
+      *+=(1, 0)+[F]{\mathstrut y_1}="i"
+      "e" [l] {K} :"e"
+    [rrruuuu] *+=(1, 0)+[F--]{\mathstrut x_i}="x"
+      :@{-->}[dd] *{\xor}="xor"
+      "e" [d] :@{-->}`r [ru] `u "xor" "xor"
+      :@{-->}[dd] *+[F]{E}="e" :@{-->}[ddddd]
+      *+=(1, 0)+[F--]{\mathstrut y_i}="i"
+      "e" [l] {K} :@{-->}"e"
+    [rrruuuu] *+=(1, 0)+[F]{\mathstrut x_{n-2}}="x"
+      :[dd] *{\xor}="xor"
+      "e" [d] :@{-->}`r [ru] `u "xor" "xor"
+      :[dd] *+[F]{E}="e"
+      "e" [l] {K} :"e"
+    [rrruuuu] *+=(1, 0)+[F]{\mathstrut x_{n-1} \cat 0^{\ell-t}}="x"
+      :[dd] *{\xor}="xor"
+      "e" [d] :`r [ru] `u "xor" "xor"
+      "e" [dddddrrr] *+=(1, 0)+[F]{\mathstrut y_{n-1}[0 \bitsto t]}="i"
+      "e" [dd] ="x"
+      "i" [uu] ="y"
+      []!{"x"; "e" **{}, "x"+/4pt/ ="p",
+          "x"; "y" **{}, "x"+/4pt/ ="q",
+          "y"; "x" **{}, "y"+/4pt/ ="r",
+          "y"; "i" **{}, "y"+/4pt/ ="s",
+          "e";
+          "p" **\dir{-};
+          "q" **\crv{"x"};
+          "r" **\dir{-};
+          "s" **\crv{"y"};
+          "i" **\dir{-}?>*\dir{>}}
+      "xor" :[dd] *+[F]{E}="e"
+      "e" [l] {K} :"e"
+      "e" [dddddlll] *+=(1, 0)+[F]{\mathstrut y_{n-2}}="i"
+      "e" [dd] ="x"
+      "i" [uu] ="y"
+      []!{"x"; "e" **{}, "x"+/4pt/ ="p",
+          "x"; "y" **{}, "x"+/4pt/ ="q",
+          "y"; "x" **{}, "y"+/4pt/ ="r",
+          "y"; "i" **{}, "y"+/4pt/ ="s",
+          "x"; "y" **{} ?="c" ?(0.5)/-4pt/ ="cx" ?(0.5)/4pt/ ="cy",
+          "e";
+          "p" **\dir{-};
+          "q" **\crv{"x"};
+          "cx" **\dir{-};
+          "c" *[@]\cir<4pt>{d^u};
+          "cy";
+          "r" **\dir{-};
+          "s" **\crv{"y"};
+          "i" **\dir{-}?>*\dir{>}}
+  \end{graph} \]
+
+  \caption{Encryption using CBC mode with ciphertext stealing}
+  \label{fig:cbc-steal}
+\end{figure}  
+
+\begin{definition}[CBC stealing]
+  \label{def:cbc-steal}
+  Let $P\colon \keys P \times \Bin^\ell \to \Bin^\ell$ be a pseudorandom
+  permutation.  We define the symmetric encryption scheme
+  $\Xid{\mathcal{E}}{CBC-steal}^P = (\Xid{G}{CBC}^P, \Xid{E}{CBC-steal}^P,
+  \Xid{D}{CBC-steal}^P)$ for messages in $\Bin^{\ell\Z}$ by setting $\keys
+  \Xid{\mathcal{E}}{CBC-steal} = \keys P$ and defining the encryption and
+  decryption algorithms as follows:
+  \begin{program}
+    Algorithm $\Xid{E}{CBC-steal}^P_K(x)$: \+ \\
+      $I \getsr \Bin^\ell$; \\
+      $y \gets I$; \\
+      $t = |x| \bmod \ell$; \\
+      \IF $t \ne 0$ \THEN $x \gets x \cat 0^{\ell-t}$; \\
+      \FOR $i = 0$ \TO $|x|/\ell$ \DO \\ \ind
+        $x_i \gets x[\ell i \bitsto \ell (i + 1)]$; \\
+        $y_i \gets P_K(x_i \xor I)$; \\
+        $I \gets y_i$; \\
+        $y \gets y \cat y_i$; \- \\
+      \IF $t \ne 0$ \THEN \\ \ind
+        $b \gets |y| - 2\ell$; \\
+        $y \gets $\=$y[0 \bitsto b] \cat
+                     y[b + \ell \bitsto |y|] \cat {}$ \\
+                  \>$y[b \bitsto b + t]$; \- \\
+      \RETURN $y$;
+    \next
+    Algorithm $\Xid{D}{CBC-steal}^P_K(y)$: \+ \\
+      $I \gets y[0 \bitsto \ell]$; \\
+      $t = |y| \bmod \ell$; \\
+      \IF $t \ne 0$ \THEN \\ \ind
+        $b \gets |y| - t - \ell$; \\
+        $z \gets P^{-1}_K(y[b \bitsto b + \ell])$; \\
+        $y \gets $\=$y[0 \bitsto b] \cat
+                     y[b + \ell \bitsto |y|] \cat {}$ \\
+                  \>$z[t \bitsto \ell]$; \- \\
+      $x \gets \emptystring$; \\
+      \FOR $1 = 0$ \TO $|y|/\ell$ \DO \\ \ind
+        $y_i \gets y[\ell i \bitsto \ell (i + 1)]$; \\
+        $x_i \gets P^{-1}_K(y_i) \xor I$; \\
+        $I \gets y_i$; \\
+        $x \gets x \cat x_i$; \- \\
+      \IF $t \ne 0$ \THEN \\ \ind
+        $x \gets x \cat z[0 \bitsto t] \xor y[b \bitsto b + t]$; \- \\
+      \RETURN $x$;
+  \end{program}
+\end{definition}
+
+\begin{theorem}[Security of CBC with ciphertext stealing]
+  \label{thm:cbc-steal}
+  Let $P\colon \keys P \times \Bin^\ell \to \Bin^\ell$ be a pseudorandom
+  permutation.  Then
+  \begin{equation}
+    \InSec{lor-cpa}(\Xid{\mathcal{E}}{CBC-steal}; t, q_E, \mu_E) \le
+      2 \cdot \InSec{prp}(P; t + q t_P, q) +
+      \frac{q (q - 1)}{2^\ell - 2^{\ell/2}}
+  \end{equation}
+  where $q = \mu_E/\ell$ and $t_P$ is some small constant.
+\end{theorem}
+
+\begin{proof}
+  This is an easy reducibility argument.  Let $A$ be an adversary attacking
+  $\Xid{\mathcal{E}}{CBC-steal}^P$.  We construct an adversary which attacks
+  $\Xid{\mathcal{E}}{CBC}^P$:
+  \begin{program}
+    Adversary $A'^{E(\cdot)}$: \+ \\
+      $b \gets A^{\Xid{E}{steal}(\cdot)}$; \\
+      \RETURN $b$;
+    \- \\[\medskipamount]
+    Oracle $\Xid{E}{steal}(x_0, x_1)$: \+ \\
+      \IF $|x_0| \ne |x_1|$ \THEN \ABORT; \\
+      \RETURN $\id{steal}(|x_0|, E(\id{pad}(x_0), \id{pad}(x_1)))$;
+    \next
+    Function $\id{pad}(x)$: \+ \\
+      $t \gets |x| \bmod \ell$; \\
+      \RETURN $x \cat 0^{\ell-t}$;
+    \- \\[\medskipamount]
+    Function $\id{steal}(l, y)$: \+ \\
+      $t \gets l \bmod \ell$; \\
+      \IF $t \ne 0$ \THEN \\ \ind
+        $b \gets |y| - 2\ell$; \\
+        $y \gets $\=$y[0 \bitsto b] \cat
+                     y[b + \ell \bitsto |y|] \cat y[b \bitsto b + t]$; \- \\
+      \RETURN $y$;
+  \end{program}
+  Comparing this to definition~\ref{def:cbc-steal} shows that $A'$ simlates
+  the LOR-CPA game for $\Xid{\mathcal{E}}{CBC-steal}$ perfectly.  The theorem
+  follows.
+\end{proof}
 
+\subsection{Proof of theorem~\ref{thm:cbc}}
+\label{sec:cbc-proof}
 
-% messages
-%
-% pre-challenge: g^b
-% cookie: g^b, h(cookie, g^b')
-% challenge: g^b, h(g^b'), b + h(reply-check, g^b, g^b', g^ab')
-% reply: g^b, h(g^b'), b + h(reply-check, g^b, g^b', g^ab'), E_k(g^a'b)
-% switch: h(g^b), h(g^b'), E_k(g^a'b, h(switch-request, g^a, g^a'))
-% switch-ok: E_k(g^ab, h(switch-confirm, g^a, g^a'))begin{
+Consider an adversary $A$ attacking CBC encryption using an ideal random
+permutation $P(\cdot)$.  Pick some point in the attack game when we're just
+about to encrypt the $n$th plaintext block.  For each $i \in \Nupto{n}$,
+let $x_i$ be the $i$th block of plaintext we've processed; let $y_i$ be the
+corresponding ciphertext; and let $z_i = P^{-1}(y_i)$, i.e., $z_i = x_i \xor
+I$ for the first block of a message, and $z_i = x_i \xor y_{i-1}$ for the
+subsequent blocks.
 
+Say that `something went wrong' if any $z_i = z_j$ for $i \ne j$.  This is
+indeed a disaster, because it means that $y_i = y_j$ , so he can detect it,
+and $x_i \xor y_{i-1} = x_j \xor y_{j-1}$, so he can compute an XOR
+difference between two plaintext blocks from the ciphertext and thus
+(possibly) reveal whether he's getting his left or right plaintexts
+encrypted.  The alternative, `everything is fine', is much better.  If all
+the $z_i$ are distinct, then because $y_i = P(z_i)$, the $y_i$ are all
+generated by $P(\cdot)$ on inputs it's never seen before, so they're all
+random subject to the requirement that they be distinct.  If everything is
+fine, then, the adversary has no better way of deciding whether he has a left
+oracle or a right oracle than tossing a coin, and his advantage is therefore
+zero.  Thus, we must bound the probability that something went wrong.
 
-We now describe the full Wrestlers Protocol, in a multi-party setting.  Fix a
-cyclic group $G = \langle g \rangle$ of order $q = |G|$.  Each player $P_i$
-chooses a private key $\alpha_i \in \{ 1, 2, \ldots, q - 1 \}$ and publishes
-the corresponding public key $a_i = g^{\alpha_i}$ to the other players.
+Assume that, at our point in the game so far, everything is fine.  But we're
+just about to encrypt $x^* = x_n$.  There are two cases:
+\begin{itemize}
+\item If $x_n$ is the first block in a new message, we've just invented a new
+  random IV $I \in \Bin^\ell$ which is unknown to $A$, and $z_n = x_n \xor
+  I$.  Let $y^* = I$.
+\item If $x_n$ is \emph{not} the first block, then $z_n = x_n \xor y_{n-1}$,
+  but the adversary doesn't yet know $y_{n-1}$, except that because $P$ is a
+  permutation and all the $z_i$ are distinct, $y_{n-1} \ne y_i$ for any $0
+  \le i < n - 1$.  Let $y^* = y_{n-1}$.
+\end{itemize}
+Either way, the adversary's choice of $x^*$ is independent of $y^*$.  Let
+$z^* = x^* \xor y^*$.  We want to know the probability that something goes
+wrong at this point, i.e., that $z^* = z_i$ for some $0 \le i < n$.  Let's
+call this event $C_n$.  Note first that, in the first case, there are
+$2^\ell$ possible values for $y^*$ and in the second there are $2^\ell - n +
+1$ possibilities for $y^*$.  Then
+\begin{eqnarray}[rl]
+  \Pr[C_n]
+  & = \sum_{x \in \Bin^\ell} \Pr[C_n \mid x^* = x] \Pr[x^* = x] \\
+  & = \sum_{x \in \Bin^\ell}
+          \Pr[x^* = x] \sum_{0\le i<n} \Pr[y^* = z_i \xor x] \\
+  & \le \sum_{0\le i<n} \frac{1}{2^\ell - n}
+        \sum_{x \in \Bin^\ell} \Pr[x^* = x] \\
+  & = \frac{n}{2^\ell - n}
+\end{eqnarray}
 
+Having bounded the probability that something went wrong for any particular
+block, we can proceed to bound the probability of something going wrong in
+the course of the entire game.  Let's suppose that $q = \mu_E/\ell \le
+2^{\ell/2}$; for if not, $q (q - 1) > 2^\ell$ and the theorem is trivially
+true, since no adversary can achieve advantage greater than one.
 
+Let's give the name $W_i$ to the probability that something went wrong after
+encrypting $i$ blocks.  We therefore want to bound $W_q$ from above.
+Armed with the knowledge that $q \le 2^{\ell/2}$, we have
+\begin{eqnarray}[rl]
+  W_q &\le \sum_{0\le i<q} \Pr[C_i]
+       \le \sum_{0\le i<q} \frac{i}{2^\ell - i} \\
+      &\le \frac{1}{2^\ell - 2^{\ell/2}} \sum_{0\le i<q} i \\
+      &= \frac{q (q - 1)}{2 \cdot (2^\ell - 2^{\ell/2})}
+\end{eqnarray}
+Working through the definition of LOR-CPA security, we can see that $A$'s
+(and hence any adversary's) advantage against the ideal system is at most $2
+W_q$.
 
+By using an adversary attacking CBC encryption as a statistical test in an
+attempt to distinguish $P_K(\cdot)$ from a pseudorandom permutation, we see
+that
+\begin{equation}
+  \InSec{prp}(P; t + q t_P, q) \ge
+    \frac{1}{2} \cdot
+      \InSec{lor-cpa}(\Xid{\mathcal{E}}{CBC}; t, q_E, \mu_E) -
+    \frac{q (q - 1)}{2 \cdot (2^\ell - 2^{\ell/2})}
+\end{equation}
+where $t_P$ expresses the overhead of doing the XORs and other care and
+feeding of the CBC adversary; whence
+\begin{equation}
+  \InSec{lor-cpa}(\Xid{\mathcal{E}}{CBC}; t, q_E, \mu_E) \le
+  2 \cdot \InSec{prp}(P; t, q) + \frac{q (q - 1)}{2^\ell - 2^{\ell/2}}
+\end{equation}
+as required.
+\qed
 
 %%%----- That's all, folks --------------------------------------------------
 
-\bibliography{cryptography,mdw-crypto}
+\bibliography{mdw-crypto,cryptography,cryptography2000,rfc}
 \end{document}
 
 %%% Local Variables: