X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~mdw/git/tripe/blobdiff_plain/b4e566689f469cc1cffe99e50e16a346d0f9832d..09c873ca00247ea12c1338c25aca3c94aa4638f6:/doc/wrestlers.tex

diff --git a/doc/wrestlers.tex b/doc/wrestlers.tex
index 8d1c2a94..2d321bc4 100644
--- a/doc/wrestlers.tex
+++ b/doc/wrestlers.tex
@@ -1,1147 +1,3698 @@
 %%% -*-latex-*-
 %%%
-%%% $Id: wrestlers.tex,v 1.7 2004/04/08 01:36:17 mdw Exp $
+%%% The Wrestlers Protocol: secure, deniable key-exchange
 %%%
-%%% Description of the Wrestlers Protocol
-%%%
-%%% (c) 2001 Mark Wooding
+%%% (c) 2006 Mark Wooding
 %%%
 
-\newif\iffancystyle\fancystyletrue
+\makeatletter
+\def\@doit#1{#1}
+\ifx\iffancystyle\xxundefined\expandafter\@doit\else\expandafter\@gobble\fi
+{\newif\iffancystyle\fancystyletrue}
+\ifx\ifshort\xxundefined\expandafter\@doit\else\expandafter\@gobble\fi
+{\newif\ifshort\shortfalse}
+\iffancystyle\expandafter\@gobble\else\expandafter\@doit\fi{\newif\ifpdfing}
+\makeatother
+
+\typeout{Options:}
+\typeout{  Fancy style:   \iffancystyle ON\else OFF\fi}
+\typeout{  Short version: \ifshort      ON\else OFF\fi}
+
+\errorcontextlines=\maxdimen
+\showboxdepth=\maxdimen
+\showboxbreadth=\maxdimen
 
 \iffancystyle
-  \documentclass
-    [a4paper, article, 10pt, numbering, noherefloats, notitlepage]
-    {strayman}
+  \documentclass{strayman}
+  \parskip=0pt plus 1pt  \parindent=1.2em
+  \usepackage[T1]{fontenc}
   \usepackage[palatino, helvetica, courier, maths=cmr]{mdwfonts}
-  \usepackage[mdwmargin]{mdwthm}
-  \PassOptionsToPackage{dvips}{xy}
+  \usepackage[within = subsection, mdwmargin]{mdwthm}
+  \usepackage{mdwlist}
+  \usepackage{sverb}
+  \ifpdfing\else
+    \PassOptionsToPackage{dvips}{xy}
+  \fi
 \else
+  \PassOptionsToClass{runningheads}{llncs}
   \documentclass{llncs}
 \fi
 
-\usepackage{mdwtab, mathenv, mdwlist, mdwmath, crypto}
+\PassOptionsToPackage{show}{slowbox}
+%\PassOptionsToPackage{hide}{slowbox}
+\usepackage{mdwtab, mdwmath, crypto}
+\usepackage{slowbox}
 \usepackage{amssymb, amstext}
+\usepackage{url, multicol}
 \usepackage{tabularx}
-\usepackage{url}
-\usepackage[all]{xy}
-
-\errorcontextlines=999
-\showboxbreadth=999
-\showboxdepth=999
-\makeatletter
+\DeclareUrlCommand\email{\urlstyle{tt}}
+\ifslowboxshow
+  \usepackage[all]{xy}
+  \turnradius{4pt}
+\fi
+\usepackage{mathenv}
 
-\title{The Wrestlers Protocol: proof-of-receipt and secure key exchange}
-\author{Mark Wooding \and Clive Jones}
+\newcommand{\Nupto}[1]{\{0, 1, \ldots, #1 - 1\}}
+\iffancystyle
+  \let\next\title
+\else
+  \def\next[#1]{\titlerunning{#1}\title}
+\fi
+\next
+  [The Wrestlers Protocol]
+  {The Wrestlers Protocol%
+    \ifshort\thanks{This is an extended abstract; the full version
+      \cite{Wooding:2006:WP} is available from
+      \texttt{http://eprint.iacr.org/2006/386/}.}\fi \\
+    A simple, practical, secure, deniable protocol for key-exchange}
+\iffancystyle
+  \author{Mark Wooding \\ \email{mdw@distorted.org.uk}}
+\else
+  \author{Mark Wooding}
+  \institute{\email{mdw@distorted.org.uk}}
+\fi
+\date{2 November 2006}
 
-\bibliographystyle{mdwalpha}
+\iffancystyle
+  \bibliographystyle{mdwalpha}
+  \let\epsilon\varepsilon
+  \let\emptyset\varnothing
+  \let\le\leqslant\let\leq\le
+  \let\ge\geqslant\let\geq\ge
+  \numberwithin{table}{section}
+  \numberwithin{figure}{section}
+  \numberwithin{equation}{subsection}
+  \let\random\$
+\else
+  \bibliographystyle{splncs}
+  \expandafter\let\csname claim*\endcsname\claim
+  \expandafter\let\csname endclaim*\endcsname\endclaim
+\fi
 
-\newcolumntype{G}{p{0pt}}
-\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%
+\edef\Pr{\expandafter\noexpand\Pr\nolimits}
+\newcommand{\bitsto}{\mathbin{..}}
+\newcommand{\E}{{\mathcal{E}}}
+\newcommand{\M}{{\mathcal{M}}}
+\iffancystyle
+  \def\description{%
+    \basedescript{%
+      \let\makelabel\textit%
+      \desclabelstyle\multilinelabel%
+      \desclabelwidth{1in}%
+    }%
+  }
+\fi
+\def\fixme#1{\marginpar{FIXME}[FIXME: #1]}
+\def\hex#1{\texttt{#1}_{x}}
+
+\newenvironment{longproof}[1]{%
+  \ifshort#1\expandafter\ignore
+  \else\proof\fi
+}{%
+  \ifshort\else\endproof\fi
+}
+
+\def\dbox#1{%
+  \vtop{%
+    \def\\{\unskip\egroup\hbox\bgroup\strut\ignorespaces}%
+    \hbox{\strut#1}%
   }%
 }
-\let\endmessages\endbasedescript
+
+\def\Wident{\Xid{W}{ident}}
+\def\Wkx{\Xid{W}{kx}}
+\def\Wdkx{\Xid{W}{dkx}}
+\def\Func#1#2{\mathcal{F}[#1\to#2]}
+\def\diff#1#2{\Delta_{#1, #2}}
+\def\Hid{H_{\textit{ID}}}
+
+%% protocol run diagrams
+\def\PRaction#1{#1\ar[r]}
+\def\PRcreatex#1{\PRaction{\textsf{Create session\space}#1}}
+\def\PRcreate#1#2#3{\PRcreatex{(\text{#1},\text{#2},#3)}}
+\def\PRreceivex#1{\PRaction{\textsf{Receive\space}#1}}
+\def\PRreceive#1#2{\PRreceivex{\msg{#1}{#2}}}
+\def\PRsession#1{\relax\mathstrut#1\ar[r]}
+\def\msg#1#2{(\cookie{#1},#2)}
+\def\PRresult#1{#1}
+\def\PRsendx#1{\PRresult{\textsf{Send\space}#1}}
+\def\PRsend#1#2{\PRsendx{\msg{#1}{#2}}}
+\def\PRcomplete#1{\textsf{Complete:\space}#1}
+\def\PRstate#1{\textsf{State:\space}#1}
+\def\PRignore{\textsf{(ignored)}}
+\def\PRreveal{\textsf{Session-state reveal}\ar[r]}
+\def\protocolrun#1{\[\xymatrix @R=0pt @C=2em {#1}\]}
+
+\def\protocol{%
+  \unskip\bigskip
+  \begin{tabular*}{\linewidth}%
+    {@{\qquad}l@{\extracolsep{0ptplus1fil}}r@{\qquad}}}
+\def\endprotocol{\end{tabular*}}
+\def\send#1#2{\noalign{%
+    \centerline{\xy\ar @{#1}|*+{\mathstrut#2}<.5\linewidth, 0pt>\endxy}}}
+
+%% class-ids for proof of extractor lemma
+\let\Cid=\Lambda
+\let\Csession=S
+\let\Cindex=r
+\let\Cquery=Q
+\let\Chash=H
+\let\Ccheck=c
+\let\Ccheckset=V
+\let\Ccount=\nu
+
+\def\HG#1{\mathbf{H}_{#1}}
+
+\iffancystyle\else
+  \let\xsssec\subsubsection\def\subsubsection#1{\xsssec[#1]{#1.}}
+\fi
 
 \begin{document}
 
+%%%--------------------------------------------------------------------------
+
 \maketitle
+\iffancystyle \thispagestyle{empty} \fi
+
 \begin{abstract}
-  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.
+  We describe and prove (in the random-oracle model) the security of a simple
+  but efficient zero-knowledge identification scheme, whose security is based
+  on the computational Diffie-Hellman problem.  Unlike other recent proposals
+  for efficient identification protocols, we don't need any additional
+  assumptions, such as the Knowledge of Exponent assumption.
+
+  From this beginning, we build a simple key-exchange protocol, and prove
+  that it achieves `SK-security' -- and hence security in Canetti's Universal
+  Composability framework.
+
+  Finally, we show how to turn the simple key-exchange protocol into a
+  slightly more complex one which provides a number of valuable `real-life'
+  properties, without damaging its security.
 \end{abstract}
-\tableofcontents
+
+\iffancystyle
 \newpage
+\thispagestyle{empty}
+\columnsep=2em \columnseprule=0pt
+\tableofcontents[\begin{multicols}{2}\raggedright][\end{multicols}]
+%%\listoffigures[\begin{multicols}{2}\raggedright][\end{multicols}]
+%% \listoftables[\begin{multicols}{2}\raggedright][\end{multicols}]
+\newpage
+\fi
 
 %%%--------------------------------------------------------------------------
 
 \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.
 
-%%%--------------------------------------------------------------------------
+This paper proposes protocols for \emph{identification} and
+\emph{authenticated key-exchange}.
+
+An identification protocol allows one party, say Bob, to be sure that he's
+really talking to another party, say Alice.  It assumes that Bob has some way
+of recognising Alice; for instance, he might know her public key.  Our
+protocol requires only two messages -- a challenge and a response -- and has
+a number of useful properties.  It is very similar to, though designed
+independently of, a recent protocol by Stinson and Wu
+\cite{cryptoeprint:2006:337}; we discuss their protocol and compare it to
+ours in \ifshort the full version of this paper. \else
+section~\ref{sec:stinson-ident}.  \fi
+
+Identification protocols are typically less useful than they sound.  As Shoup
+\cite{cryptoeprint:1999:012} points out, it provides a `secure ping', by
+which Bob can know that Alice is `there', but provides no guarantee that any
+other communication was sent to or reached her.  However, there are
+situations where this an authentic channel between two entities -- e.g., a
+device and a smartcard -- where a simple identification protocol can still be
+useful.
+
+An authenticated key-exchange protocol lets Alice and Bob agree on a shared
+secret, known to them alone, even if there is an enemy who can read and
+intercept all of their messages, and substitute messages of her own.  Once
+they have agreed on their shared secret, of course, they can use standard
+symmetric cryptography techniques to ensure the privacy and authenticity of
+their messages.
+
+
+\subsection{Desirable properties of our protocols}
+
+Our identification protocol has a number of desirable properties.
+\begin{itemize}
+\item It is \emph{simple} to understand and implement.  In particular, it
+  requires only two messages.
+\item It is fairly \emph{efficient}, requiring two scalar multiplications by
+  each of the prover and verifier.
+\item It is provably \emph{secure} (in the random oracle model), assuming the
+  intractability of the computational Diffie-Hellman problem.
+\end{itemize}
 
-\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 key-exchange protocol also has a number of desirable
+properties.
+\begin{itemize}
+\item It is fairly \emph{simple} to understand and implement, though there
+  are a few subtleties.  In particular, it is \emph{symmetrical}.  We have
+  implemented a virtual private network system based on this protocol.
+\item It is \emph{efficient}, requiring four scalar multiplications by each
+  participant.  The communication can be reduced to three messages by
+  breaking the protocol's symmetry.
+\item It is provably \emph{secure} (again, in the random oracle model),
+  assuming the intractability of the computational Diffie-Hellman problem,
+  and the security of a symmetric encryption scheme.
+\item It provides \emph{perfect forward secrecy}.  That is, even if a user's
+  long-term secrets are compromised, past sessions remain secure.
+\item It is \emph{deniable}.  It is possible to construct simulated
+  transcripts of protocol executions between any number of parties without
+  knowing any of their private keys.  The simulated transcripts are (almost)
+  indistinguishable from real protocol transcripts.  Hence, a transcript
+  does not provide useful evidence that a given party was really involved in
+  a given protocol execution.
+\end{itemize}
 
-\subsection{Bit strings}
+\ifshort\else
+\subsection{Asymptotic and concrete security results}
+
+Most security definitions for identification (particularly zero-knowledge)
+and key-exchange in the literature are \emph{asymptotic}.  That is, they
+consider a family of related protocols, indexed by a \emph{security
+parameter}~$k$; they that any \emph{polynomially-bounded} adversary has only
+\emph{negligible} advantage.  A polynomially-bounded adversary is one whose
+running time is a bounded by some polynomial~$t(k)$.  The security definition
+requires that, for any such polynomially-bounded adversary, and any
+polynomial $p(k)$, the adversary's advantage is less than $p(k)$ for all
+sufficiently large values of $k$.
+
+Such asymptotic notions are theoretically interesting, and have obvious
+connections to complexity theory.  Unfortunately, such an asymptotic result
+tells us nothing at all about the security of a particular instance of a
+protocol, or what parameter sizes one needs to choose for a given level of
+security against a particular kind of adversary.  Koblitz and Menezes
+\cite{cryptoeprint:2006:229} (among other useful observations) give examples
+of protocols, proven to meet asymptotic notions of security, whose security
+proofs guarantee nothing at all for the kinds of parameters typically used in
+practice.
+
+Since, above all, we're interested in analysing a practical and implemented
+protocol, we follow here the `practice-oriented provable security' approach
+largely inspired by Bellare and Rogaway, and exemplified by
+\cite{Bellare:1994:SCB,Bellare:1995:XMN,Bellare:1995:OAE,Bellare:1996:ESD,%
+Bellare:1996:KHF,Bellare:1997:CST}; see also \cite{Bellare:1999:POP}.
+Rather than attempting to say, formally, whether or not a protocol is
+`secure', we associate with each protocol an `insecurity function' which
+gives an upper bound on the advantage of any adversary attacking the protocol
+within given resource bounds.
+\fi
 
-Most of our notation for bit strings is standard.  The main thing to note is
-that everything is zero-indexed.
+\subsection{Formal models for key-exchange}
 
-\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}
+\ifshort
+
+The first model for studying the \emph{computational} security of
+key-exchange protocols (rather than using protocol-analysis logics like that
+of \cite{Burrows:1989:LAa}) was given by Bellare and Rogaway
+\cite{Bellare:1994:EAK}; the model has since been enhanced, both by the
+original authors and others, in \cite{Bellare:1995:PSS,%
+Blake-Wilson:1997:KAP,Blake-Wilson:1998:EAA}.  The model defines security
+in terms of a game: key-exchange protocols are secure if an adversary can't
+distinguish the key agreed by a chosen `challenge session' from a key chosen
+independently at random.  Other models for key-exchange have been proposed in
+\cite{Bellare:1998:MAD} and \cite{cryptoeprint:1999:012}; these use a
+different notion of security, involving implementation of an ideal
+functionality.
 
-\subsection{Other notation}
+\else
+
+Many proposed key-exchange protocols have turned out to have subtle security
+flaws.  The idea of using formal methods to analyse key-exchange protocols
+begins with the logic of Burrows, Abadi and Needham \cite{Burrows:1989:LAa}.
+Their approach requires a `formalising' step, in which one expresses in the
+logic the contents of the message flows, and the \emph{beliefs} of the
+participants.
+
+Bellare and Rogaway \cite{Bellare:1994:EAK} describe a model for studying the
+computational security of authentication and key-exchange protocols in a
+concurrent setting, i.e., where multiple parties are running several
+instances of a protocol simultaneously.  They define a notion of security in
+this setting, and show that several simple protocols achieve this notion.
+Their original paper dealt with pairs of parties using symmetric
+cryptography; they extended their definitions in \cite{Bellare:1995:PSS} to
+study three-party protocols involving a trusted key-distribution centre.
+
+Blake-Wilson, Johnson and Menezes \cite{Blake-Wilson:1997:KAP} applied the
+model of \cite{Bellare:1994:EAK} to key-exchange protocols using asymmetric
+cryptography, and Blake-Wilson and Menezes \cite{Blake-Wilson:1998:EAA}
+applied it to protocols based on the Diffie-Hellman protocol.
+
+The security notion of \cite{Bellare:1994:EAK} is based on a \emph{game}, in
+which an adversary nominates a \emph{challenge session}, and is given either
+the key agreed by the participants of the challenge session, or a random
+value independently sampled from an appropriate distribution.  The
+adversary's advantage -- and hence the insecurity of the protocol -- is
+measured by its success probability in guessing whether the value it was
+given is really the challenge key.  This challenge-session notion was also
+used by the subsequent papers described above.
+
+Bellare, Canetti and Krawczyk \cite{Bellare:1998:MAD} described a pair of
+models which they called the \textsc{am} (for `authenticated links model')
+and \textsc{um} (`unauthenticated links model').  They propose a modular
+approach to the design of key-exchange protocols, whereby one first designs a
+protocol and proves its security in the \textsc{am}, and then applies a
+authenticating `compiler' to the protocol which they prove yields a protocol
+secure in the realistic \textsc{um}.  Their security notion is new.  They
+define an `ideal model', in which an adversary is limited to assigning
+sessions fresh, random and unknown keys, or matching up one session with
+another, so that both have the same key.  They define a protocol to be secure
+if, for any adversary~$A$ in the \textsc{am} or \textsc{um}, there is an
+ideal adversary~$I$, such that the outputs of $A$ and $I$ are computationally
+indistinguishable.
+
+In \cite{cryptoeprint:1999:012}, Shoup presents a new model for key-exchange,
+also based on the idea of simulation.  He analyses the previous models,
+particularly \cite{Bellare:1994:EAK} and \cite{Bellare:1998:MAD}, and
+highlights some of their inadequacies.
 
+\fi
+
+Canetti and Krawczyk \cite{cryptoeprint:2001:040,Canetti:2001:AKE} describe a
+new notion of security in the model of \cite{Bellare:1998:MAD}, based on the
+challenge-session notion of \cite{Bellare:1994:EAK}.  The security notion,
+called `SK-security', seems weaker in various ways than those of earlier
+works such as \cite{Bellare:1994:EAK} or \cite{cryptoeprint:1999:012}.
+However, the authors show that their notion suffices for constructing `secure
+channel' protocols, which they also define.
+
+\ifshort\else
+In \cite{Canetti:2001:UCS}, Canetti describes the `universal composition'
+framework.  Here, security notions are simulation-based: one defines security
+notions by presenting an `ideal functionality'.  A protocol securely
+implements a particular functionality if, for any adversary interacting with
+parties who use the protocol, there is an adversary which interacts with
+parties using the ideal functionality such that no `environment' can
+distinguish the two.  The environment is allowed to interact freely with the
+adversary throughout, differentiating this approach from that of
+\cite{Bellare:1998:MAD} and \cite{cryptoeprint:1999:012}, where the
+distinguisher was given only transcripts of the adversary's interaction with
+the parties.  With security defined in this way, it's possible to prove a
+`universal composition theorem': one can construct a protocol, based upon
+various ideal functionalities, and then `plug in' secure implementations of
+the ideal functionalities and appeal to the theorem to prove the security of
+the entire protocol.  The UC framework gives rise to very strong notions of
+security, due to the interactive nature of the `environment' distinguisher.
+\fi
+
+Canetti and Krawczyk \cite{Canetti:2002:UCN} show that the SK-security notion
+of \cite{Canetti:2001:AKE} is \emph{equivalent} to a `relaxed' notion of
+key-exchange security in the UC framework\ifshort\space of
+\cite{Canetti:2001:UCS}\fi, and suffices for the construction of UC secure
+channels.
+
+The result of \cite{Canetti:2002:UCN} gives us confidence that SK-security is
+the `right' notion of security for key-exchange protocols.  Accordingly,
+SK-security is the standard against which we analyse our key-exchange
+protocol.
+
+
+\subsection{Outline of the paper}
+
+The remaining sections of this paper are as follows.
 \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$.
+\item Section \ref{sec:prelim} provides the essential groundwork for the rest
+  of the paper.  It introduces important notation, and describes security
+  notions and intractability assumptions.
+\item Section \ref{sec:zk-ident} describes our zero-knowledge identification
+  protocol and proves its security.
+\item Section \ref{sec:kx} describes the simple version of our key-exchange
+  protocol, and proves its security and deniability.  It also describes some
+  minor modifications which bring practical benefits without damaging
+  security.
+\item Finally, section \ref{sec:conc} presents our conclusions.
 \end{itemize}
 
-\subsection{Algorithm descriptions}
+\ifshort
+The full version of this paper describes how to make our protocols
+identity-based by using bilinear pairings using the techniques introduced in
+\cite{Boneh:2003:IBE}.  It also contains proofs of the various theorems
+stated here.
+\fi
+
+%%%--------------------------------------------------------------------------
+
+\section{Preliminaries}
+\label{sec:prelim}
 
-Most of the notation used in the algorithm descriptions should be obvious.
-We briefly note a few features which may be unfamiliar.
+\ifshort
+\subsection{Basics}
+\let\prelimsec\subsubsection
+\else
+\let\prelimsec\subsection
+\fi
+
+\prelimsec{Miscellaneous notation}
+
+We write $\Func{D}{R}$ for the set of all functions with domain $D$ and range
+$R$.
+
+\prelimsec{Groups}
+
+Let $(G, +)$ be a cyclic group\footnote{
+  We find that additive group notation is easier to read.  In particular, in
+  multiplicative groups, one ends up with many interesting things tucked away
+  in little superscripts.}%
+of prime order $q$, and generated by an element $P$.  We shall write the
+identity of $G$ as $0_G$, or simply as $0$ when no ambiguity is likely to
+arise.  Thus, we have $\langle P \rangle = G$ and $q P = 0$.  Any $X \in G$
+can be written as $X = x P$ for some $x \in \{0, 1, \ldots, q - 1\}$.
+
+We consider a cyclic group of order $n$ as a $\Z/n\Z$-module, and in
+particular our group $G$ can be seen as a vector space over $\gf{q}$.  This
+makes the notation slightly more convenient.
+
+\prelimsec{Bit strings and encodings}
+\label{sec:bitenc}
+
+Let $\Bin = \{0, 1\}$ be the set of binary digits.  Then $\Bin^n$ is the set
+of $n$-bit strings, and $\Bin^*$ the set of all (finite) bit strings.  If $x
+\in \Bin^n$ is a bit string, we write its length as $|x| = n$.  For a bit
+string $x \in \Bin^n$, and for $0 \le i < n$, we write $x[i]$ as the $i$th
+bit of $x$.  The empty string is denoted $\emptystring$.
+
+Let $x$ and $y$ be two bit strings.  If $|x| = |y| = n$, we write $x \xor y$
+to mean the bitwise exclusive-or of $x$ and $y$\ifshort\else: if $z = x \xor
+y$ then $|z| = n$, and $z[i] = (x[i] + y[i]) \bmod 2$ for $0 \le i < n$\fi.
+We write $x \cat y$ to mean the concatenation of $x$ and $y$\ifshort\else: if
+$z = x \cat y$ then $|z| = |x| + |y|$ and $z[i] = x[i]$ if $0 \le i < |x|$
+and $z[i] = y[i - |x|]$ if $|x| < i \le |x| + |y|$\fi.
+
+Finally, we let $\bot$ be a value distinct from any bit string.
+
+We shall want to encode group elements $X \in G$ and indices $x \in I =
+\gf{q}$ as bit strings.
+\ifshort
+To this end, we shall assume the existence of efficient, unambiguous
+encodings of group elements as $\ell_G$-bit strings, and indices as
+$\ell_I$-bit strings.  To reduce clutter, we shall leave encoding and
+decoding as implicit operations.
+\else
+To this end, we shall assume the existence of
+integers $\ell_G, \ell_I > 0$ and functions
+\[
+  e_S\colon S \to \Bin^{\ell_S}
+  \quad \textrm{and} \quad
+  d_S\colon \Bin^{\ell_S} \to S \cup \{ \bot \}
+  \qquad
+  \textrm{for } S \in \{ G, \F \}.
+\]
+with the following properties.
 \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$.
+\item The functions are \emph{unique} and \emph{unambiguous}, i.e., for any
+  $t \in \Bin^{\ell_S}$, we have
+  \[ d_S(t) = \begin{cases}
+       s & if there is some $s \in S$ such that $t = e_S(s)$, or \\
+       \bot & if no such $s$ exists.
+  \end{cases}
+  \]
+\item The functions should be \emph{efficient} to compute.  Indeed, we shall
+  be assuming that the time taken for encoding and decoding is essentially
+  trivial.
 \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
+Note that, as we have defined them, all encodings of group elements are the
+same length, and similarly for encodings of indices.  This is necessary for
+the security of our protocols.
+
+We shall frequently abuse notation by omitting the encoding and decoding
+functions where it is obvious that they are required.
+\fi
+
+\ifshort\else
+\prelimsec{Games, adversaries, and oracles}
+\label{sec:games}
+
+Many of the security definitions and results given here make use of
+\emph{games}, played with an \emph{adversary}.  An adversary is a
+probabilistic algorithm.  In some games, the adversary is additionally
+equipped with \emph{oracles}, which perform computations with values chosen
+by the adversary and secrets chosen by the game but not revealed to the
+adversary.  We impose limits on the adversary's resource usage: in
+particular, the total time it takes, and the number of queries it makes to
+its various oracles.  Throughout, we include the size of the adversary's
+program as part of its `time', in order to model adversaries which contain
+large precomputed tables.
+
+The games provide models of someone trying to attack a construction or
+protocol.  For security, we will either define a notion of `winning' the
+game, and require that all adversaries have only a very small probability of
+winning, or we consider two different games and require that no adversary can
+distinguish between the two except with very small probability.
+
+Our proofs make frequent use of sequences of games; see
+\cite{cryptoeprint:2004:332,cryptoeprint:2004:331}.  The presentation owes
+much to Shoup \cite{cryptoeprint:2004:332}.  We begin with a game $\G0$ based
+directly on a relevant security definition, and construct a sequence of games
+$\G1$, $\G2$, \dots, each slightly different from the last.  We define all of
+the games in a sequence over the same underlying probability space -- the
+random coins tossed by the algorithms involved -- though different games may
+have slightly differently-defined events and random variables.  Our goal in
+doing this is to bound the probability of the adversary winning the initial
+game $\G0$ by simultaneously (a) relating the probability of this event to
+that of corresponding events in subsequent games, and (b) simplifying the
+game until the probability of the corresponding event can be computed
+directly.
+
+The following simple lemma from \cite{Shoup:2001:OR} will be frequently
+useful.
+\begin{lemma}[Difference Lemma]
+  \label{lem:shoup}
+  Let $S$, $T$, $F$ be events.  Suppose $\Pr[S \mid \bar F] =
+  \Pr[T \mid \bar F]$.  Then $|\Pr[S] - \Pr[T]| \le \Pr[F]$.
+\end{lemma}
+\begin{proof}
+  A simple calculation:
+  \begin{eqnarray*}[rl]
+    |\Pr[S] - \Pr[T]|
+    & = |(\Pr[S \mid F]\Pr[F] + \Pr[S \mid \bar F]\Pr[\bar F]) -
+         (\Pr[T \mid F]\Pr[F] + \Pr[T \mid \bar F]\Pr[\bar F])| \\
+    & = \Pr[F] \cdot |\Pr[S \mid F] - \Pr[T \mid F]| \\
+    & \le \Pr[F]
+  \end{eqnarray*}
+  and we're done!
+\end{proof}
+\fi
+
+
+\prelimsec{The random oracle model}
+\label{sec:ro}
+
+\ifshort\else
+In particular, most of our results will make use of the \emph{random oracle}
+model \cite{Bellare:1993:ROP}, in which all the participants, including the
+adversary, have access to a number of `random oracles'.  A random oracle with
+domain $D$ and range $R$ is an oracle which computes a function chosen
+uniformly at random from the set of all such functions.  (In the original
+paper \cite{Bellare:1993:ROP}, random oracles are considered having domain
+$\Bin^*$ and range $\Bin^\omega$; we use finite random oracles here, because
+they're easier to work with.)
+
+Given a protocol proven secure in the random oracle model, we can instantiate
+each random oracle by a supposedly-secure hash function and be fairly
+confident that either our protocol will be similarly secure, or one of the
+hash functions we chose has some unfortunate property.
+
+Proofs in the random oracle must be interpreted carefully.  For example,
+Canetti, Goldreich and Halevi \cite{Canetti:2004:ROM} show that there are
+schemes which can be proven secure in the random oracle model but provably
+have no secure instantiation in the standard model.
+\fi
+
+The random oracle model \ifshort\cite{Bellare:1993:ROP} \fi is useful for
+constructing reductions and simulators for two main reasons.
+\begin{enumerate}
+\item One can use the transcript of an adversary's queries to random oracles
+  in order to extract knowledge from it.
+\item One can `program' a random oracle so as to avoid being bound by prior
+  `commitments', or to guide an adversary towards solving a selected instance
+  of some problem.
+\end{enumerate}
+Our proofs only make use of the first feature.  This becomes particularly
+important when we consider issues of zero-knowledge and deniability in a
+concurrent setting, because we want to be able to claim that we retain these
+features when the random oracle is instantiated using a cryptographic hash
+function, and hash functions definitely aren't `programmable' in this way!
+The former property seems rather more defensible -- one would indeed hope
+that the only sensible way of working out (anything about) the hash of a
+particular string is to actually compute the hash function, and the random
+oracle model is, we hope, just giving us a `hook' into this process.
+
+\ifshort\else
+(Our protocols can be modified to make use of bilinear pairings so as to
+provide identity-based identification and key-exchange, using the techniques
+of \cite{Boneh:2003:IBE}.  Proving the security of the modifications we
+discuss would involve `programming' random oracles, but this doesn't affect
+the zero-knowledge or deniability of the resulting protocols.)
+\fi
+
+
+\ifshort\else
+\prelimsec{Notation for algorithms}
+
+We shall have occasion to describe algorithms by means of a pseudocode.  Our
+choice of pseudocode is unlikely to be particularly controversial.  We let $x
+\gets y$ denote the action of setting $x$ to the value $y$; similarly, $x
+\getsr Y$ denotes the action of sampling $x$ from the set $Y$ uniformly at
+random.
+
+The expression $a \gets A^{O(\cdot, x)}(y)$ means `assign to $a$ the value
+output by algorithm $A$ on input $y$, and with oracle access to the algorithm
+which, given input $z$, computes $O(z, x)$'.
+
+We make use of conditional (\IF-\ELSE) and looping (\FOR-\DO and \WHILE-\DO)
+constructions; in order to reduce the amount of space taken up, the bodies of
+such constructions are shown by indentation only.
+
+We don't declare the types of our variables explicitly, assuming that these
+will be obvious by inspection; also, we don't describe our variables' scopes
+explicitly, leaving the reader to determine these from context.
+
+Finally, the notation $\Pr[\textit{algorithm} : \textit{condition}]$ denotes
+the probability that \textit{condition} is true after running the given
+\textit{algorithm}.
+\fi
+
+\prelimsec{Diffie-Hellman problems}
+\label{sec:dhp}
+
+The security of our protocols is related to the hardness of the
+computational, decisional, and gap Diffie-Hellman problems in the group $G$.
+We define these problems and what it means for them to be `hard' here.
+
+The \emph{computational} Diffie-Hellman problem (CDH) is as follows: given
+two group elements $X = x P$ and $Y = y P$, find $Z = x y P$.
+\ifshort\else
+\begin{definition}[The computational Diffie-Hellman problem]
+  Let $(G, +)$ be a cyclic group generated by $P$.  For any adversary $A$, we
+  say that $A$'s \emph{success probability} at solving the computational
+  Diffie-Hellman problem in $G$ is
+  \[ \Succ{cdh}{G}(A) =
+      \Pr[ x \getsr I; y \getsr \Z/\#G\Z : A(x P, y P) = x y P ]
+  \]
+  where the probability is taken over the random choices of $x$ and $y$ and
+  any random decisions made by $A$.  We say that the \emph{CDH insecurity
+  function} of $G$ is
+  \[ \InSec{cdh}(G; t) = \max_A \Succ{cdh}{G}(A) \]
+  where the maximum is taken over adversaries which complete in time $t$.
+\end{definition}
+Certainly, if one can compute discrete logarithms in the group $G$ (i.e.,
+given $x P$, find $x$), then one can solve the computational Diffie-Hellman
+problem.  The converse is not clear, though.  Shoup \cite{Shoup:1997:LBD}
+gives us some confidence in the difficulty of the problem by showing that a
+\emph{generic} adversary -- i.e., one which makes no use of the specific
+structure of a group -- has success probability no greater than $q^2/\#G$.
+
+This isn't quite sufficient for our purposes.  Our proofs will be able to
+come up with (possibly) a large number of guesses for the correct answer, and
+at most one of them will be correct.  Unfortunately, working out which one is
+right seems, in general, to be difficult.  This is the \emph{decision}
+Diffie-Hellman problem (DDH), which \cite{Shoup:1997:LBD} shows, in the
+generic group model, is about as hard as CDH.  (See \cite{Boneh:1998:DDP} for
+a survey of the decision Diffie-Hellman problem.)
+\par\fi
+Our reference problem will be a `multiple-guess computational Diffie-Hellman
+problem' (MCDH), which is captured by a game as follows.  An adversary is
+given a pair of group elements $(x P, y P)$, and an oracle $V(\cdot)$ which
+accepts group elements as input.  The adversary wins the game if it queries
+$V(x y P)$.
+
+\begin{figure}
   \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'$;
+    $\Game{mcdh}{G}(A)$: \+ \\
+      $w \gets 0$; \\
+      $x \getsr \Z/\#G\Z$; $y \getsr \Z/\#G\Z$; \\
+      $A^{V(\cdot)}(x P, y P)$; \\
+      \RETURN $w$;
     \next
-    Function $\id{lr}(b, x_0, x_1)$: \+ \\
-      \RETURN $x_b$;
+    Function $V(Z)$: \+ \\
+      \IF $Z = x y P$ \THEN \\ \ind
+        $w \gets 1$; \\
+        \RETURN $1$; \- \\
+      \RETURN $0$;
   \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.
+
+  \caption{The multiple-guess computational Diffie-Hellman problem:
+    $\Game{mcdh}{G}(A)$}
+  \label{fig:mcdh}
+\end{figure}
+
+\begin{definition}[The multiple-guess computational Diffie-Hellman problem]
+  \label{def:mcdh}
+  Let $(G, +)$ be a cyclic group generated by $P$.  For some adversary $A$,
+  we say that $A$'s \emph{success probability} at solving the multiple-guess
+  computational Diffie-Hellman problem in $G$ is
+  \[ \Succ{mcdh}{G}(A) = \Pr[\Game{mcdh}{G}(A) = 1] \]
+  where $\Game{mcdh}{G}(A)$ is shown in figure~\ref{fig:mcdh}.  We say that
+  the \emph{MCDH insecurity function of $G$} is
+  \[ \InSec{mcdh}(G; t, q_V) = \max_A \Succ{mcdh}{G}(A) \]
+  where the maximum is taken over adversaries which complete in time $t$ and
+  make at most $q_V$-oracle queries.
 \end{definition}
+\ifshort
+We can (loosely) relate the difficulty of MCDH to the difficulty of
+the standard CDH problem, in which the adversary is allowed only a single
+guess.
+\else
+Note that our MCDH problem is not quite the `gap Diffie-Hellman problem'
+(GDH).  The gap problem measures the intractibility of solving CDH even with
+the assistance of an oracle for solving (restricted) decision Diffie-Hellman
+problems in the group.  Specifically, the adversary is given $(X, Y) = (x P,
+y P)$ and tries to find $Z = x y P$, as for CDH, but now it has access to an
+oracle $D(R, S)$ which answers $1$ if $S = x R$ and $0$ otherwise.
+
+Clearly MCDH is at least as hard as GDH, since our simple verification oracle
+$V(Z)$ can be simulated with the gap problem's DDH oracle, as $D(Y, Z)$.
+However, we can (loosely) relate the difficulty of MCDH to the difficulty of
+CDH.
+\fi
+\begin{proposition}[Comparison of MCDH and CDH security]
+  For any cyclic group $(G, +)$,
+  \[ \InSec{mcdh}(G; t, q_V) \le
+       \ifshort q_V\,\InSec{mcdh}(G; t + O(q_V), 1) \else
+                q_V\,\InSec{cdh}(G; t + O(q_V)) \fi.
+  \]
+\end{proposition}
+\begin{longproof}{The proof of this proposition may be found in the full
+    version of this paper.}
+  Let $A$ be an adversary attacking the multiple-guess computational
+  Diffie-Hellman problem in $G$, and suppose that it runs in time $t$ and
+  issues $q_V$ queries to its verification oracle.
+
+  We use a sequence of games.  Game $\G0$ is the original MCDH attack game.
+  In each game $\G{i}$, we let the event $S_i$ be the probability that the
+  adversary wins the game.
+
+  Game $\G1$ is the same as $\G0$, except that we change the behaviour of the
+  verification oracle.  Specifically, we make the oracle always return $0$.
+  We claim that this doesn't affect the adversary's probability of winning,
+  i.e., $\Pr[S_1] = \Pr[S_0]$.  To see this, note that if none of the
+  adversary's $V(\cdot)$ queries was correct, then there is no change in the
+  game; conversely, if any query was correct, then the adversary will have
+  won regardless of its subsequent behaviour (which may differ arbitrarily
+  between the two games).
+
+  We are now ready to construct from $A$ an adversary $B$ attacking the
+  standard computational Diffie-Hellman problem.
+  \begin{program}
+    Adversary $B(X, Y)$: \+ \\
+      $n \gets 0$; \\
+      \FOR $i \in \Nupto{q_V}$ \DO $Q_i \gets 0$; \\
+      $A^{V(\cdot)}$; \\
+      $r \getsr \Nupto{n}$; \\
+      \RETURN $Q_r$;
+    \next
+    Function $D(Z')$: \+ \\
+      $Q_n \gets Z'$; \\
+      $n \gets n + 1$; \\
+      \RETURN $0$;
+  \end{program}
+  Observe that $B$ provides $A$ with an accurate simulation of game $\G1$.
+  Moreover, at the end of the algorithm, we have $0 < n \le q_V$, and the
+  values $Q_0$, $Q_1$, \dots, $Q_{n-1}$ are the values of $A$'s oracle
+  queries.  Hence, with probability $Pr[S_1]$, at least of one of the $Q_i$
+  is the correct answer to the CDH problem.  Let $\epsilon = \Pr[S_1] =
+  \Pr[S_0]$; we claim that $B$'s probability of success is at least
+  $\epsilon/q_V$.  The proposition follows directly from this claim and that,
+  because $A$ was chosen arbitrarily, we can maximize and count resources.
+
+  We now prove the above claim.  For $0 \le i < q_V$, let $W_i$ be the
+  event that $Q_i = x y P$, i.e., that $Q_i$ is the correct response.  A
+  simple union bound shows that
+  \[ \sum_{0\le i<j} \Pr[W_i \mid n = j] \ge \epsilon. \]
+  We now perform a calculation:
+  \begin{eqnarray*}[rl]
+    \Succ{cdh}{G}(B)
+    & =  \sum_{0\le i<q_V} \Pr[W_i \land r = i] \\
+    & =  \sum_{0<j\le q_V} \Pr[n = j]
+         \biggl( \sum_{0\le i<j} \Pr[W_i \land r = i \mid n = j] \biggr) \\
+    & =  \sum_{0<j\le q_V} \Pr[n = j]
+         \biggl( \frac{1}{j} \sum_{0\le i<j} \Pr[W_i \mid n = j] \biggr) \\
+    &\ge \sum_{0<j\le q_V} \Pr[n = j] \frac{\epsilon}{j} \\
+    &\ge \frac{\epsilon}{q_V} \sum_{0<j\le q_V} \Pr[n = j] \\
+    & =  \frac{\epsilon}{q_V}.
+  \end{eqnarray*}
+  which completes the proof.
+\end{longproof}
+
+\ifshort\else
+\prelimsec{Example groups and encodings}
+
+For nonnegative integers $0 \le n < 2^\ell$, there is a natural binary
+encoding $N_\ell\colon \Nupto{2^\ell} \to \Bin^\ell$ which we can define
+recursively as follows.
+\[ N_0(0) = \emptystring \qquad
+   N_\ell(n) = \begin{cases}
+     N_{\ell-1}(n) \cat 0              & if $0 \le n < 2^{\ell-1}$ \\
+     N_{\ell-1}(n - 2^{\ell-1}) \cat 1 & if $2^{\ell-1} \le n < 2^\ell$.
+   \end{cases}
+\]
+Given an encoding $a = N_\ell(n)$ we can recover $n$ as
+\[ n = \sum_{0\le i<\ell} a[i] 2^i. \]
+Hence, given some limit $L \le 2^\ell$, we can encode elements of $\Nupto{L}$
+using the functions $(e, d)$:
+\[ e(L, \ell, n) = N_\ell(n) \qquad
+   d(L, \ell, a) = \begin{cases}
+     N_\ell(a) & if $N_\ell(a) < L$ \\
+     \bot      & otherwise
+   \end{cases}
+\]
+The reader can verify that the functions $e(L, \ell, \cdot)$ and $d(L, \ell,
+\cdot)$ satisfy the requirements of section~\ref{sec:bitenc}.
+
+Given some $q$ with $q < 2^{\ell_I}$, then, we can define an encoding
+$(e_\F, d_\F)$ by $e_\F(n) = e(q, \ell_I, n)$ and $d_\F(a) = d(q, \ell_I,
+a)$.
+
+Let $p$ and $q$ be primes, with $q \mid (p - 1)$.  Then there is an order-$q$
+subgroup of $\F_p^*$.  In practice, an order-$q$ element can be found easily
+by taking elements $h \in \F_p^*$ at random and computing $g = h^{(p-1)/2}$
+until $g \ne 1$; then $G = \langle g \rangle$ is a group of $q$ elements.
+Assuming that $p$ and $q$ are sufficiently large, the Diffie-Hellman problems
+seem to be difficult in $G$.  Some texts recommend additional restrictions on
+$p$, in particular that $(p - 1)/2q$ be either prime or the product of large
+primes.  Primes of this form protect against small-subgroup attacks; but our
+protocols are naturally immune to these attacks, so such precautions are
+unnecessary here.  Elements of $G$ can be encoded readily, since each element
+$n + p\Z$ of $\F_p = \Z/p\Z$ has an obvious `representative' integer $n$ such
+that $0 \le n < p$, and given $2^{\ell_G} > p$, we can encode $n$ as $e(p,
+\ell_G, n)$, as above.
+
+Alternatively, let $\F = \gf{p^f}$ be a finite field, and $E$ be an elliptic
+curve defined over $\F$ such that the group $E(\F)$ of $\F$-rational points
+of $E$ has a prime-order cyclic subgroup $G$.  Elements of $G$ can be
+represented as pairs of elements of $\F$.  If $f = 1$, i.e., $\F = \Z/p\Z$
+then field elements can be encoded as above.  If $p = 2$, we can represent
+the field as $\F_2/(p(x))$ for some irreducible polynomial $p(x) \in \F_2[x]$
+of degree $f$.  An element $r \in \F$ can then be represented by a polynomial
+$r(x)$ with degree less than $f$, and coefficients $c_i \in \{0, 1\}$, i.e.,
+\[ r(x) = \sum_{0\le i<f} c_i x^i \]
+and hence we can uniquely encode $r$ as an $f$-bit string $a$ such that $a[i]
+= c_i$.
+\fi
 
-\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$.
+
+\prelimsec{Symmetric encryption}
+\label{sec:sym-enc}
+
+Our key-exchange protocol requires a symmetric encryption scheme.  Our
+definition is fairly standard, except that, rather than specifying a
+key-generation algorithm, we assume that key generation simply involves
+selecting a string of a given length uniformly at random.
+\begin{definition}[Symmetric encryption schemes]
+  A \emph{symmetric encryption scheme} $\E = (\kappa, E, D)$ consists of:
+  \begin{itemize}
+  \item an integer $\kappa \ge 0$,
+  \item a randomized \emph{encryption algorithm} $E$ which, on input $K \in
+    \Bin^\kappa$ and $p \in \Bin^*$ outputs some $c \in \Bin^*$, written $c
+    \gets E_K(p)$;
+  \item a \emph{decryption algorithm} $D$ which, on input $K \in \Bin^\kappa$
+    and $c \in \Bin^*$ outputs some $p' \in \Bin^* \cup \{\bot\}$, written
+    $p' \gets D_K(c)$.
+  \end{itemize}
+  Furthermore, a symmetric encryption scheme must be \emph{sound}: that is,
+  if $c \gets E_K(p)$ for some $K \in \Bin^\kappa$ and $p \in \Bin^*$, and
+  $p' \gets D_K(c)$ then $p = p'$.
+\end{definition}
+Our security notion for symmetric encryption is the standard notion of
+left-or-right indistinguishability of ciphertexts under chosen-ciphertext
+attack.
+\begin{definition}[IND-CCA]
+  \label{def:ind-cca}
+  Let $\E = (\kappa, E, D)$ be a symmetric encryption scheme, and $A$ be an
+  adversary.  Let $\id{lr}_b(x_0, x_1) = x_b$ for $b \in \{0, 1\}$.  Let
+  \[ P_b =
+     \Pr[K \getsr \Bin^\kappa;
+         b \gets A^{E_K(\id{lr}_b(\cdot, \cdot)), D_K(\cdot)}() :
+	 b = 1]
+  \]
+  An adversary is \emph{valid} if
+  \begin{itemize}
+  \item for any query to its encryption oracle $E_K(\id{lr}_b(x_0, x_1))$ we
+    have $|x_0| = |x_1|$, and
+  \item no query to the decryption oracle $D_K(\cdot)$ is equal to any reply
+    from an encryption query.
+  \end{itemize}
+  If $A$ is valid, then we define its \emph{advantage} in attacking the
+  security of $\E$ as follows
+  \[ \Adv{ind-cca}{\E} = P_1 - P_0. \]
+  Further, we define the \emph{IND-CCA insecurity function of $\E$} to be
+  \[ \InSec{ind-cca}(\E; t, q_E, q_D) = \max_A \Adv{ind-cca}{\E}(A) \]
+  where the maximum is taken over all valid adversaries $A$ which run in time
+  $t$, and issue at most $q_E$ encryption and $q_D$ decryption queries.
 \end{definition}
 
-%%%--------------------------------------------------------------------------
 
-\section{The protocol}
-\label{sec:protocol}
+\subsection{Simulations}
+\label{sec:sim}
 
-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}
+In section~\ref{sec:zk-ident}, we shall prove that our identification
+protocol is zero-knowledge; in section~\ref{sec:denial}, we show that our
+key-exchange protocol is deniable.  In both of these proofs, we shall need to
+demonstrate \emph{simulatability}.
+
+\ifshort
 
-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.
+We consider an adversary~$A$ interacting with a `world'~$W$; we model both as
+probabilistic algorithms.  Both $A$ and~$W$ are given a common input~$c$; the
+world is additionally given a private input~$w$; these are chosen by a
+randomized initialization function $I$.  The adversary is additionally given
+an auxiliary input~$u$ computed from $w$ by a randomized algorithm~$U$.  All
+these algorithms -- the adversary and the world, but also the initialization
+and auxiliary-input algorithms $I$ and~$U$ -- have access to a number of
+random oracles $\mathcal{H} = (H_0, H_1, \ldots, H_{n-1})$.  The adversary
+eventually decides to stop interacting, and produces an output~$a$.
 
-\subsection{Symmetric encryption}
+A \emph{simulator} for $A$'s interaction with $W$ is an algorithm $S^A$ which
+attempts to produce a similar output distribution, but without interacting
+with $W$.  The simulator is given the same inputs $(c, u)$ as we gave
+to~$A$, and $S$ is also allowed to query the random oracles~$\mathcal{H}$.
 
-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.
+To measure the effectiveness of a simulator, we consider a distinguisher~$D$
+which is given $(c, u, a)$, and access to $\mathcal{H}$, and returns a bit
+$b$ representing its verdict as to whether the output $a$ was produced by the
+adversary or the simulator.
 
-A \id{keyset} contains the state required for communication between the two
-players.  In particular it maintains:
+\else
+
+\subsubsection{General framework}
+Consider a game in which an adversary~$A$ interacts with some `world'~$W$,
+which we shall represent as a probabilistic algorithm.  The world may in fact
+represent a number of honest parties communicating in a concurrent fashion,
+but we can consider them as a single algorithm for our present purposes.
+
+Initially the world and the adversary are both given the same \emph{common
+input}~$c$; in addition, the world is given a \emph{private input}~$w$.
+Both $c$ and~$w$ are computed by an \emph{initialization function}~$I$, which
+is considered to be part of the definition of the game.  Finally, the
+adversary decides somehow that it has finished interacting, and outputs a
+value~$a$.  All this we notate as
+\[ (w, c) \gets I(); a \gets A^{W(w, c)}(c). \]
+This game is \emph{simulatable} if there is an algorithm~$S$ -- the
+\emph{simulator} -- which can compute the same things as~$A$, but all by
+itself without interacting with the world.  That is, we run the simulator on
+the common input~$c$, allowing it to interact in some way with the
+adversary~$A$, and finally giving us an output~$s$.
+\[ (w, c) \gets I(); s \gets S^A(c). \]
+We shall say that the simulator is \emph{effective} if it's difficult to tell
+whether a given string was output by the adversary after interacting with the
+world, or by the simulator running by itself.  That is, for any algorithm~$D$
+-- a \emph{distinguisher} -- running in some bounded amount of time, its
+advantage
+\begin{spliteqn*}
+  \Pr[(w, c) \gets I(); a \gets A^{W(w, c)}(c);
+        b \gets D(c, a) : b = 1] - {} \\
+  \Pr[(w, c) \gets I(); s \gets S^A(c); b \gets D(c, s) : b = 1]
+\end{spliteqn*}
+is small.  (Note that we gave the distinguisher the common input as well as
+the output of the adversary or the simulator.)
+
+It's usual to study \emph{transcripts} of interactions in these kinds of
+settings.  We are considering arbitrary adversarial outputs here, so this
+certainly includes adversaries which output a transcript of their
+interactions.  Indeed, for any adversary~$A$, we could construct an
+adversary~$A_T$ which performs the same computation, and outputs the same
+result, but also includes a complete transcript of $A$'s interaction with the
+world.  Therefore we're just providing additional generality.
+
+\subsubsection{Random oracles}
+We shall be considering interactions in which all the parties have access to
+several random oracles.  We could simply say that the random oracles are part
+of the world~$W$.  In the setting described above, only the adversary
+actually interacts with the world (and therefore would be able to query
+random oracles).  The simulator would be forced to `make up' its own random
+oracle, and the distinguisher would have to study the distributions of the
+random-oracle queries and their responses to make up its mind about which it
+was given.
+
+However, this would be a poor model for the real world, since once we
+instantiate the random oracle with a hash function, we know that everyone
+would in actually be able to compute the hash function for themselves.  Thus
+a distinguisher in the real world would be able to tell the difference
+immediately between a real interaction and the simulated transcript, since
+the `random oracle' queries recorded in the latter would be wrong!
+
+Therefore we decide not to include the random oracles as part of the world,
+but instead allow all the participants -- adversary, simulator and
+distinguisher -- access to them.  If we denote by~$\mathcal{H} = (H_0, H_1,
+\ldots, H_{n-1})$ the collection of random oracles under consideration, the
+expression for the distinguisher's advantage becomes
+\begin{spliteqn*}
+  \Pr[(w, c) \gets I(); a \gets A^{W(w, c), \mathcal{H}}(c);
+        b \gets D^{\mathcal{H}}(c, a) : b = 1] - {} \\
+  \Pr[(w, c) \gets I(); s \gets S^{A, \mathcal{H}}(c);
+        b \gets D^{\mathcal{H}}(c, s) : b = 1].
+\end{spliteqn*}
+
+\subsubsection{Auxiliary inputs}
+If an adversary's output can be effectively simulated, then we can
+confidently state that the adversary `learnt' very little of substance from
+its interaction, and certainly very little it can \emph{prove} to anyone
+else.  However, as we have described the setting so far, we fix an adversary
+before we choose inputs to the world, so our model says little about what an
+adversary which has already acquired some knowledge might learn beyond that.
+For example, an adversary might overhear some other conversation between
+honest parties and be able to use this to its advantage.
+
+To this end, we give the adversary an \emph{auxiliary input}~$u$, computed by
+an algorithm~$U$.  We give $U$ both $c$ and $w$, in order to allow the
+adversary to gain some (possibly partial) knowledge of the secrets of the
+other parties.  We also allow $U$ access to the random oracles~$\mathcal{H}$,
+because clearly in the `real world' it would be ridiculous to forbid such an
+algorithm from computing a publicly-known hash function.
+
+The simulator and distinguisher are also given the auxiliary input.  The
+simulator is meant to represent the adversary's ability to compute things on
+its own, without interacting with the world, and since the adversary is given
+the auxiliary input, the simulator must be too.  The distinguisher must be
+given the auxiliary input because otherwise the simulator could just `make
+up' plausible-looking inputs.
+
+\fi
+
+\ifshort
+Because we're interested in a concrete, quantitative analysis, we must
+constrain the resource usage of the various algorithms described above.
+Specifically, we shall be interested in
+\else
+
+\subsubsection{Resource limits}
+We shall not allow our algorithms to perform completely arbitrary
+computations and interactions.  Instead, we impose limits on the amount of
+time they are allowed to take, the number of random-oracle queries they make,
+and so on.  Specifically, we are interested in
+\fi
 \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.
+\item the time $t_A$ taken by the adversary and $t_D$ taken by the
+  distinguisher,
+\item the number of oracle queries $\mathcal{Q}_A = (q_{A,0}, q_{A,1},
+  \ldots, q_{A,n-1})$ made by the adversary, and $\mathcal{Q}_D$ made by the
+  distinguisher,
+\item a number of resource bounds $\mathcal{R}$ on the adversary's
+  interaction with the world (e.g., number of messages of various kinds sent
+  and received), and
+\item a number of bounds $\mathcal{U}$ on the contents of the adversary's
+  auxiliary input~$u$.
 \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$.
+Sometimes we shall not be interested in proving simulatability of adversaries
+with auxiliary inputs.  We write $\mathcal{U} = 0$ to indicate that auxiliary
+input is not allowed.
+
+\ifshort\else
+
+\subsubsection{World syntax}
+It will be worth our while being more precise about what a `world' actually
+is, syntactically.  We define a world to be a single, randomized algorithm
+taking inputs $(\iota, \sigma, \tau, \mu) \in (\Bin^*)^4$; the algorithm's
+output is a pair $(\sigma', \rho) \in (\Bin^*)^2$.  We show how the
+adversary's interaction is mapped on to this world algorithm in
+figure~\ref{fig:sim-world}.
+\begin{itemize}
+\item The `input' $\iota$ is the result of the initialization function~$I$.
+  That is, it is the pair $(w, c)$ of the world's private input and the
+  common input.
+\item The `state' $\sigma$ is empty on the world's first invocation; on each
+  subsequent call, the value of the world's output $\sigma'$ is passed back.
+  In this way, the world can maintain state.
+\item The `type $\tau$ is a token giving the type of invocation this is.
+\item The `message' $\mu$ is any other information passed in; its form will
+  typically depend on the type~$\tau$ of the invocation.
+\item The `new state' $\sigma'$ is the value of $\sigma$ to pass to the next
+  invocation of the world.
+\item The `reply $\rho$ is the actual output of the invocation.
+\end{itemize}
+There are two special invocation types.  The adversary is \emph{forbidden}
+from making special invocations.
+\begin{itemize}
+\item The special invocation type $\cookie{init}$ is used to allow the world to
+  prepare an initial state.  The world is invoked as
+  \[ W^{\mathcal{H}}(\iota, \emptystring, \cookie{init}, \emptystring) \]
+  and should output an initial state $\sigma'$.  The world's reply $\rho$ is
+  ignored.  (Recall that $\emptystring$ represents the empty string.)
+\item The special invocation type $\cookie{random}$ is used to inform the
+  world that the adversary has issued a random oracle query.  The world is
+  invoked as
+  \[ W^{\mathcal{H}}(\iota, \sigma, \cookie{random}, (i, x, h)) \]
+  to indicate that the adversary has queried its random oracle $H_i(\cdot)$
+  on the input $x$, giving output~$h$.  The world may output an updated state
+  $\sigma'$; its reply $\rho$ is ignored.
+\end{itemize}
+The latter special query is a technical device used to allow the `fake-world'
+simulators we define below to be aware of the adversary's random oracle
+queries without being able to `program' the random oracle.  Including it here
+does little harm, and simplifies the overall exposition.
 
 \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$;
+    Interaction $A^{W(w, c), \mathcal{H}}(c, u)$: \+ \\
+      $(\sigma, \rho) \gets
+        W((w, c), \emptystring, \cookie{init}, \emptystring)$; \\
+      $a \gets A^{\id{world}(\cdot, \cdot),
+                  \id{random}(\cdot, \cdot)}(c, u)$; \\
+      \RETURN $a$;
+    \newline
+    Function $\id{world}(\tau, \mu)$: \+ \\
+      \IF $\tau \in \{\cookie{init}, \cookie{random}\}$ \THEN
+        \RETURN $\bot$; \\
+      $(\sigma, \rho) \gets W((w, c), \sigma, \tau, \mu)$; \\
+      \RETURN $\rho$; \-
     \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$;
+    Function $\id{random}(i, x)$: \+ \\
+      $h \gets H_i(x)$; \\
+      $(\sigma, \rho) \gets
+        W((w, c), \sigma, \cookie{random}, (i, x, h))$; \\
+      \RETURN $h$;
   \end{program}
 
-  \caption{Symmetric-key encryption functions}
-  \label{fig:keyset}
+  \caption{Interacting with a world: Interaction $A^{W, \mathcal{H}}$}
+  \label{fig:sim-world}
 \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}.
+\subsubsection{Definitions}
+We are now ready to begin making definitions.
+\fi
 
-\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{definition}[Simulation security]
+  \label{def:sim}
+  Consider the game described above, with the initialization function~$I$,
+  and the world~$W$: let $A$ be an adversary, and let~$U$ be an
+  auxiliary-input function; let $S$ be a simulator, and let $D$ be a
+  distinguisher.  We define $D$'s \emph{advantage against $S$'s simulation of
+    $A$'s interaction with~$W$ with auxiliary inputs provided by~$U$} to be
+  \[ \Adv{sim}{W, I, S}(A, U, D) =
+       \Pr[\Game{real}{W, I, S}(A, U, D) = 1] -
+       \Pr[\Game{sim}{W, I, S}(A, U, D)= 1]
+  \]
+  where the games are as shown in figure~\ref{fig:sim}.
+  Furthermore, we define the \emph{simulator's insecurity function} to be
+  \[ \InSec{sim}(W, I, S;
+      t_D, t_A, \mathcal{Q}_D, \mathcal{Q}_A, \mathcal{R}, \mathcal{U}) =
+      \max_{D, A, U} \Adv{sim}{W, I, S}(A, U, D)
+  \]
+  where the maximum is taken over all distinguishers~$D$ running in
+  time~$t_D$ and making at most $\mathcal{Q}_D$ random-oracle queries, and
+  all adversaries~$A$ running in time~$t_A$, making at most $\mathcal{Q}_A$
+  random-oracle queries, not exceeding the other stated resource
+  bounds~$\mathcal{R}$ on its interaction with~$W$, and auxiliary-input
+  functions producing output not exceeding the stated bounds~$\mathcal{U}$.
+\end{definition}
+\begin{remark}
+  The usual definitions of zero-knowledge, for example, require the simulator
+  to work for all choices of inputs (common, private and auxiliary), rather
+  than for random choices.  Our definition therefore looks weaker.  Our proof
+  of zero-knowledge actually carries through to the traditional
+  stronger-looking definition.  Critically, however, the standard
+  universal quantification over inputs fails to capture deniability in the
+  random oracle model, since the inputs can't therefore depend on the random
+  oracle.  Our formulation therefore actually gives \emph{stronger}
+  deniability than the usual one.
+\end{remark}
 
-\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}
+\begin{figure}
+  \begin{program}
+    $\Game{real}{W, I, S}(A, U, D)$: \+ \\
+      $(w, c) \gets I()$; \\
+      $u \gets U^{\mathcal{H}}(w, c)$; \\
+      $a \gets A^{W(w, c), \mathcal{H}}(c, u)$; \\
+      $b \gets D^{\mathcal{H}}(c, u, a)$; \\
+      \RETURN $b$;
+    \next
+    $\Game{sim}{W, I, S}(A, U, D)$: \+ \\
+      $(w, c) \gets I()$; \\
+      $u \gets U^{\mathcal{H}}(w, c)$; \\
+      $s \gets S^{A, \mathcal{H}}(c, u)$; \\
+      $b \gets D^{\mathcal{H}}(c, u, s)$; \\
+      \RETURN $b$;
+  \end{program}
 
-  \caption{Message contents, as sent by Alice}
-  \label{tab:kx-messages}
-\end{table}
-  
-\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}
+  \caption{Games for simulation: $\Game{real}{W, I}$ and $\Game{sim}{W, I}$}
+  \label{fig:sim}
+\end{figure}
+
+\ifshort\else
+\subsubsection{Fake-world simulators}
+The simulators we shall be considering in the present paper are of a specific
+type which we call `fake-world simulators'.  They work by running the
+adversary in a fake `cardboard cut-out' world, and attempting to extract
+enough information from the adversary's previous interactions and random
+oracle queries to maintain a convincing illusion.
+
+That is, the behaviour of a fake-world simulator~$S$ is simply to allow the
+adversary to interact with a `fake world'~$W'$, which was not given the world
+private input.  That is, there is some world $W'$ such that
+\[ S^{A, \mathcal{H}}(c, u) \equiv A^{W'(u, c), \mathcal{H}}(c, u) \]
+Fake-world simulators are convenient because they allow us to remove from
+consideration the distinguisher~$D$ as the following definition shows.
+\begin{definition}[Fake-world simulation security]
+  \label{def:fakesim}
+  Let $I$, $W$ and $U$ be as in definition~\ref{def:sim}.  Let $A$ be an
+  adversary which outputs a single bit.  Let $S$ be a fake-world simulator.
+  We define $A$'s \emph{advantage against $S$'s fake-world simulation of $W$
+  with auxiliary inputs provided by~$U$} to be
+  \begin{spliteqn*}
+    \Adv{fw}{W, I, S}(A, U) =
+      \Pr[(w, c) \gets I(); u \gets U^{\mathcal{H}}(w, c);
+           b \gets A^{W(w, c), \mathcal{H}}(c, u) : b = 1] - {} \\
+       \Pr[(w, c) \gets I(); u \gets U^{\mathcal{H}}(w, c);
+           b \gets S^{A, \mathcal{H}}(c, u) : b = 1]
+  \end{spliteqn*}
+  Furthermore, we define the \emph{simulator's insecurity function} to be
+  \[ \InSec{fw}(W, I, S;
+      t_D, t, \mathcal{Q}, \mathcal{R}, \mathcal{U}) =
+      \max_{A, U} \Adv{fw}{W, I, S}(A, U)
+  \]
+  where the maximum is taken over all adversaries~$A$ running in time~$t$,
+  making at most $\mathcal{Q}$ random-oracle queries, not exceeding the other
+  stated resource bounds~$\mathcal{R}$ on its interaction with~$W$, and
+  auxiliary-input functions producing output not exceeding the stated
+  bounds~$\mathcal{U}$.
+\end{definition}
+It remains for us to demonstrate that this is a valid way of analysing
+simulators; the following simple proposition shows that this is indeed the
+case.
+\begin{proposition}[Fake-world simulation]
+  \label{prop:fakesim}
+  Let $I$ be an initialization function and let $W$ be a world.  Then, for
+  any fake-world simulator~$S$,
+  \[ \InSec{sim}(W, I, S; t_D, t_A, \mathcal{Q}_D, \mathcal{Q}_A,
+       \mathcal{R}, \mathcal{U}) \le
+     \InSec{fw}(W, I, S; t_A + t_D, \mathcal{Q}_D + \mathcal{Q}_A,
+       \mathcal{R}, \mathcal{U})
+  \]
+  (where addition of query bounds $\mathcal{Q}$ is done elementwise).
+\end{proposition}
+\begin{proof}
+  Let $W$ and $I$ as in the proposition statement be given; also let a
+  distinguisher~$D$ running in time~$t_D$ and making $\mathcal{Q}_D$
+  random-oracle queries, an adversary~$A$ running in time~$t_A$ and making
+  $\mathcal{Q}_A$ random-oracle queries and interacting with its world within
+  the stated bounds~$\mathcal{R}$, an auxiliary-input function~$U$ satisfying
+  the constraints~$\mathcal{U}$ on its output, and a fake-world simulator~$S$
+  all be given.
+
+  We construct an adversary~$B$ outputting a single bit as follows
+  \begin{program}
+    Adversary $B^{W, \mathcal{H}}(c, u)$: \+ \\
+      $a \gets A^{W, \mathcal{H}}(c, u)$; \\
+      $b \gets D^{\mathcal{H}}(c, u, a)$; \\
+      \RETURN $b$;
+  \end{program}
+  A glance at definitions \ref{def:sim} and~\ref{def:fakesim} and the
+  resources used by $B$ shows that
+  \[ \Adv{sim}{W, I, S}(A, U) = \Adv{fw}{W, I, S}(B, U)
+      \le \InSec{fw}(W, I, S;  t_D + t_A, \mathcal{Q}_D + \mathcal{Q}_A,
+       \mathcal{R}, \mathcal{U})
+  \]
+  as required.
+\end{proof}
+\fi
+
+%%%--------------------------------------------------------------------------
+
+\section{A zero-knowledge identification scheme}
+\label{sec:zk-ident}
+
+
+\subsection{Description}
+
+Here we present a simple zero-knowledge identification scheme.  Fix some
+group $G$ with prime order $q = \#G$.  Suppose Alice chooses a private key $x
+\inr \gf{q}$, and publishes the corresponding public key $X = x P$.  Let
+$H_I\colon G^2 \to \Bin^{\ell_I}$ be a secure hash function.  Here's a simple
+protocol which lets her prove her identity to Bob.
+\begin{enumerate}
+\item Bob selects a random $r \inr \gf{q}$, and computes $R = r P$, $Y = r X$,
+  and $c = r \xor H_I(R, Y)$.  He sends the pair $(R, c)$ to Alice as his
+  \emph{challenge}.
+\item Alice receives $(R, c)$.  She computes $Y' = x R$ and $r' = c \xor
+  H_I(R', Y')$, and checks that $R = r' P$.  If so, she sends $Y'$ as her
+  \emph{response}; otherwise she sends $\bot$.
+\item Bob receives $Y'$ from Alice.  He checks that $Y' = Y$.  If so, he
+  accepts that he's talking to Alice; otherwise he becomes suspicious.
+\end{enumerate}
+We name this the Wrestlers Identification Protocol in~$G$, $\Wident^G$ (we
+drop the superscript to refer to the protocol in general, or when no
+ambiguity is likely to result).  A summary is shown in
+figure~\ref{fig:wident}.
 
 \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}
+  \begin{description}
+  \item[Setup] Group $G = \langle P \rangle$; $\#G = q$ is prime.
+    $H_I(\cdot, \cdot)$ is a secure hash.
+  \item[Private key] $x \inr \gf{q}$.
+  \item[Public key] $X = x P$.
+  \item[Challenge] $(R, c)$ where $r \inr \gf{q}$, $R = r P$, $c = r \xor
+    H_I(R, r X)$.
+  \item[Response] $x R = r X$ if $R = (c \xor H_I(R, x R)) P$; otherwise
+    $\bot$.
+  \end{description}
+
+  \caption{Summary of the Wrestlers Identification Protocol, $\Wident$}
+  \label{fig:wident}
 \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}
+\subsection{Security}
 
-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.
+In order to evaluate the security of our protocol, we present a formal
+description of the algorithms involved in figure~\ref{fig:wident}.  Here, the
+hash function $H_I(\cdot, \cdot)$ is modelled as a random oracle.
 
-\subsubsection{The \cookie{kx-pre-challenge} message}
+\begin{figure}
+  \begin{program}
+    Function $\id{setup}()$: \+ \\
+      $x \getsr \gf{q}$; \\
+      $X \gets x P$; \\
+      \RETURN $(x, X)$;
+    \ifshort\newline\else\next\fi
+    Function $\id{challenge}^{H_I(\cdot, \cdot)}(R, c, X)$: \+ \\
+      $r \getsr \gf{q}$; \\
+      $R \gets r P$; $Y \gets r X$; \\
+      $h \gets H_I(R, Y)$; $c \gets r \xor h$; \\
+      \RETURN $(Y, R, c)$; \- \\[\medskipamount]
+    Function $\id{verify}(Y, Y')$: \+ \\
+      \IF $Y' = Y$ \THEN \RETURN $1$; \\
+      \RETURN $0$;
+    \next
+    Function $\id{response}^{H_I(\cdot, \cdot)}(R, c, x)$: \+ \\
+      $Y' \gets x R$; \\
+      $h \gets H_I(R', Y')$; $r' \gets c \xor h$; \\
+      \IF $R \ne r' P$ \THEN \RETURN $\bot$; \\
+      \RETURN $Y'$;
+  \end{program}
 
-If Alice receieves a \cookie{kx-pre-challenge}, she ensures that she's in the
-\cookie{challenge} state: if not, she rejects the message.
+  \caption{Functions implementing $\Wident$ in the random oracle model}
+  \label{fig:wident-ro}
+\end{figure}
 
-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.
+\subsubsection{Completeness}
+Suppose that Bob really is talking to Alice.  Note that $Y' = x R = x (r P) =
+r (x P) = r X = Y$.  Hence $r' = c \xor H_I(R', Y') = c \xor H_I(R, Y) = r$,
+so $r' P = r P = R$, so Alice returns $Y' = Y$ to Bob.  Therefore $\Wident$
+is \emph{complete}: if Bob really is communicating with Alice then he
+accepts.
+
+\subsubsection{Soundness}
+We next show that impersonating Alice is difficult.  The natural way to prove
+this would be to give an adversary a challenge and prove that its probability
+of giving a correct response is very small.  However, we prove a stronger
+result: we show that if the adversary can respond correctly to any of a large
+collection of challenges then it can solve the MCDH problem.
+
+Consider the game $\Game{imp}{\Wident}$ shown in
+figure~\ref{fig:wident-sound}.  An adversary's probability of successfully
+impersonating Alice in our protocol, by correctly responding to any one of
+$n$ challenges, is exactly its probability of winning the game (i.e., causing
+it to return $1$).
 
-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.
-
-\subsubsection{The \cookie{kx-cookie} message}
-
-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.
-
-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.
-
-\subsubsection{The \cookie{kx-challenge} message}
+\begin{figure}
+  \begin{program}
+    $\Game{imp-$n$}{\Wident}(A)$: \+ \\
+      $H_I \getsr \Func{G^2}{\Bin^{\ell_I}}$; \\
+      $(x, X) \gets \id{setup}()$; \\
+      $\id{win} \gets 0$; \\
+      $\Xid{R}{map} \gets \emptyset$; \\
+      $\mathbf{c} \gets \id{challenges}(n)$; \\
+      $(R', Y') \gets A^{H_I(\cdot, \cdot), \id{check}(\cdot, \cdot)}
+        (X, \mathbf{c})$; \\
+      \RETURN $\id{win}$;
+    \newline
+    Function $\id{challenges}(n)$: \+ \\
+      \FOR $i \in \Nupto{n}$ \DO \\ \ind
+        $(Y, R, c) \gets \id{challenge}^{H_I(\cdot, \cdot)}$; \\
+        $\Xid{R}{map} \gets \Xid{R}{map} \cup \{ R \mapsto Y \}$; \\
+        $\mathbf{c}[i] \gets (R, c)$; \- \\
+      \RETURN $\mathbf{c}$; \next
+    Function $\id{check}(R', Y')$: \\
+      \IF $R' \notin \dom \Xid{R}{map}$ \THEN \RETURN $0$; \\
+      $Y \gets \Xid{R}{map}(R')$; \\
+      \IF $\id{verify}(Y, Y')$ \THEN \\ \ind
+        $\id{win} \gets 1$; \\
+        \RETURN $1$; \- \\
+      \RETURN $0$;
+  \end{program}
 
+  \caption{Soundness of $\Wident$: $\Game{imp-$n$}{\Wident}(A)$}
+  \label{fig:wident-sound}
+\end{figure}
 
+\begin{theorem}[Soundness of $\Wident$]
+  \label{thm:wident-sound}
+  Let $A$ be any adversary running in time $t$ and making $q_I$ queries to
+  its random oracle, and $q_V$ queries to its verification oracle.  Let $G$
+  be a cyclic group.  Then
+  \[ \Pr[\Game{imp-$n$}{\Wident^G}(A) = 1] \le
+     \InSec{mcdh}(G; t', q_I + q_V)
+  \]
+  where $t' = t + O(q_I) + O(q_V)$.
+\end{theorem}
+\begin{remark}
+  Note that the security bound here is \emph{independent} of the value of
+  $n$.
+\end{remark}
+\begin{longproof}{The proof of this theorem can be found in the full version
+    of the paper.}
+  We prove this by defining a sequence of games $\G{i}$.  The first will be
+  the same as the attack game $\Game{imp-$n$}{\Wident}(A)$ and the others
+  will differ from it in minor ways.  In each game $\G{i}$, let $S_i$ be the
+  event that $A$ wins the game -- i.e., that it successfully impersonates the
+  holder of the private key~$x$.
+
+  Let game $\G0$ be the attack game $\Game{imp}{\Wident}(A)$, and let $(R',
+  Y')$ be the output of $A$ in the game.
+
+  We define a new game $\G1$ which is the same as $\G0$, except that we query
+  the random oracle $H_I$ at $(R', Y')$ whenever the adversary queries
+  $\id{check}(R', Y')$.  (We don't charge the adversary for this.)  This
+  obviously doesn't affect the adversary's probability of winning, so
+  $\Pr[S_1] = \Pr[S_0]$.
+
+  Game $\G2$ is like $\G1$, except that we change the way we generate
+  challenges and check their responses.  Specifically, we new functions
+  $\id{challenges}_2$ and $\id{check}_2$, as shown in
+  figure~\ref{fig:wident-sound-2}.
+
+  \begin{figure}
+    \begin{program}
+      Function $\id{challenges}_2(n)$: \+ \\
+        $r^* \getsr I$; $R^* \gets r^* P$; $Y^* \gets r^* X$; \\
+        \FOR $i \in \Nupto{n}$ \DO \\ \ind
+          $r \getsr I$; $R \gets r R^*$; $Y \gets r Y^*$; \\
+          $h \gets H_I(R, Y)$; $c \gets r \xor h$; \\
+          $\Xid{R}{map} \gets \Xid{R}{map} \cup \{ R \mapsto r \}$; \\
+          $\mathbf{c}[i] \gets (R, c)$; \- \\
+        \RETURN $\mathbf{c}$;
+      \next
+      Function $\id{check}_2(R', Y')$: \+ \\
+        \IF $R' \notin \dom \Xid{R}{map}$ \THEN \RETURN $0$; \\
+        $r \gets \Xid{R}{map}(R')$; \\
+        \IF $\id{verify}(Y^*, Y'/r)$ \THEN \\ \ind
+          $\id{win} \gets 1$; \\
+          \RETURN $1$; \- \\
+        \RETURN $0$;
+    \end{program}
+
+    \caption{Soundness of $\Wident$: $\id{challenges}_2$ and $\id{check}_2$}
+    \label{fig:wident-sound-2}
+  \end{figure}
+
+  While we're generating and checking challenges in a more complicated way
+  here, we're not actually changing the distribution of the challenges, or
+  changing the winning condition.  Hence $\Pr[S_2] = \Pr[S_1]$.
+
+  Now we change the rules again.  Let $\G3$ be the same as $\G2$ except that
+  we change the winning condition.  Instead, we say that the adversary wins
+  if any of the queries to its random oracle $H_I(R', Y')$ would be a correct
+  response -- i.e., $\id{check}_2(R', Y')$ would return $1$.  Since we query
+  the oracle on $(R', Y')$ on its behalf at the end of the game, no adversary
+  can do worse in this game than it does in $\G2$, so we have $\Pr[S_3] \ge
+  \Pr[S_2]$.  (It's not hard to see that this only helps quite stupid
+  adversaries.  We can transform any adversary into one for which equality
+  holds here.)
+
+  Finally, let $\G4$ be the same as $\G3$ except that we change the way we
+  generate challenges again: rather than computing $h$ and setting $c \gets h
+  \xor r$, we just choose $c$ at random.  Specifically, we use the new
+  function, $\id{challenges}_4$, shown in figure~\ref{fig:wident-sound-4}.
+
+  \begin{figure}
+    \begin{program}
+      Function $\id{challenges}_4(n)$: \+ \\
+        $r^* \getsr I$; $R^* \gets r^* P$; $Y^* \gets r^* X$; \\
+        \FOR $i \in \Nupto{n}$ \DO \\ \ind
+          $r \getsr I$; $R \gets r R^*$; \\
+          $c \getsr \Bin^{\ell_I}$; \\
+          $\Xid{R}{map} \gets \Xid{R}{map} \cup \{ R \mapsto r \}$; \\
+          $\mathbf{c}[i] \gets (R, c)$; \- \\
+        \RETURN $\mathbf{c}$;
+    \end{program}
+
+    \caption{Soundness of $\Wident$: $\id{challenges}_4$}
+    \label{fig:wident-sound-4}
+  \end{figure}
+
+  Since $H_I(\cdot, \cdot)$ is a random function, the adversary can only
+  distinguish $\G4$ from $\G3$ if it queries its random oracle at some $(R, r
+  Y^*)$.  But if it does this, then by the rule introduced in $\G3$ it has
+  already won.  Therefore we must have $\Pr[S_4] = \Pr[S_3]$.
+
+  Our $\id{challenges}_4$ function is interesting, since it doesn't actually
+  make use of $r^*$ or $Y^*$ when generating its challenges.  This gives us
+  the clue we need to bound $\Pr[S_4]$: we can use adversary $A$ to solve the
+  multiple-guess Diffie-Hellman problem in $G$ by simulating the game $\G4$.
+  Specifically, we define the adversary $B$ as shown in
+  figure~\ref{fig:wident-sound-cdh}.  That is, for each query $A$ makes to
+  its random oracle at a new pair $(R', Y')$, we see whether this gives us
+  the answer we're looking for.  We have $\Pr[S_0] \le \Pr[S_4] =
+  \Succ{mcdh}{G}(B) \le \InSec{gdh}(G; t', q_I + q_V)$ as required.
+
+  \begin{figure}
+    \begin{program}
+      Adversary $B^{V(\cdot)}(X, R^*)$: \+ \\
+        $F \gets \emptyset$; $\Xid{R}{map} \gets \emptyset$; \\
+        \FOR $i \in \Nupto{n}$ \DO \\ \ind
+          $r \getsr I$; $R \gets r R^*$; $c \getsr \Bin^{\ell_I}$; \\
+          $\Xid{R}{map} \gets \Xid{R}{map} \cup \{ R \mapsto r \}$; \\
+          $\mathbf{c}[i] \gets (R, c)$; \- \\
+        $(R', Y') \gets A^{H_I(\cdot, \cdot), \id{check}(\cdot, \cdot)}
+          (X, \mathbf{c})$; \\
+        \IF $Y' \neq \bot$ \THEN $H_I(R', Y')$;
+      \next
+      Oracle $H_I(R', Y')$: \+ \\
+        \IF $(R', Y') \in \dom F$ \THEN \\ \quad
+          $h \gets F(x)$; \\
+        \ELSE \\ \ind
+          $\id{check}(R', Y')$; \\
+          $h \getsr \Bin^{\ell_I}$;
+          $F \gets F \cup \{ (R', Y') \mapsto h \}$; \- \\
+        \RETURN $h$;
+      \- \\[\medskipamount]
+      Oracle $\id{check}(R', Y')$: \+ \\
+        \IF $R' \in \dom \Xid{R}{map}$ \THEN
+          $V(Y'/\Xid{R}{map}(R'))$;
+    \end{program}
+
+    \caption{Soundness of $\Wident$: reduction from MCDH}
+    \label{fig:wident-sound-cdh}
+  \end{figure}
+\end{longproof}
+
+\subsubsection{Zero-knowledge}
+Finally we must prove that $\Wident$ is (statistical) zero-knowledge -- i.e.,
+that, except with very small probability, Bob learns nothing of use to him
+except that he's interacting with Alice.  To do this, we show that, for any
+algorithm $B$ which Bob might use to produce his challenge to the real Alice,
+there exists a simulator $S$ which produces transcripts distributed very
+similarly to transcripts of real conversations between $B$ and Alice, the
+difference being that $S$ doesn't know Alice's key.  We shall show that the
+statistical difference between the two distributions is $2^{-\ell_I}$.
+
+The intuition here is that Bob ought to know what answer Alice is going to
+give him when he constructs his challenge.  This is certainly true if he's
+honest: his challenge is $R = r P$ for some $r$ he knows, so he won't learn
+anything useful when Alice responds with $x R = r X$.  However, if Bob sends
+a challenge $R$ when he doesn't know the corresponding $r$, he learns
+something potentially useful.  The accompanying check value $c = r \xor
+H_I(R, r X)$ keeps him honest.
+
+To show this, we present an \emph{extractor} which, given any challenge $(R,
+c)$ Bob can construct, and his history of random-oracle queries, either
+returns a pair $(r, Y)$ such that $R = r P$ and $Y = r X$, or $\bot$;
+moreover, the probability that Alice returns a response $Y' \ne \bot$ given
+the challenge $(R, c)$ is $2^{-\ell}$.  We can, of course, readily convert
+this extractor into a simulator to prove the zero-knowledge property of our
+protocol.
+
+We shall actually consider a slightly more complex setting.  We grant Bob
+access to an oracle which produces random, correctly-formed challenges.  We
+require this to model the legitimate challenges of other parties when we
+analyse the security of our key exchange protocol.
+
+\begin{definition}[Discrete-log extractors]
+  Let $T$, $B$ be randomized algorithms.  Define the game
+  $\Game{dl-ext}{G}(T, B)$ as shown in figure~\ref{fig:dlext}.  The
+  \emph{success probability of $T$ as a discrete-log extractor against $B$}
+  is defined as
+  \[ \Succ{dl-ext}{G}(T, B) = \Pr[\Game{dl-ext}{G}(T, B) = 1]. \]
+\end{definition}
 
 \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)$
+    $\Game{dl-ext}{G}(T, B):$ \+ \\
+      $H_I \getsr \Func{G^2}{\Bin^{\ell_I}}$;
+      $Q_H \gets \emptyset$; $Q_C \gets \emptyset$; \\
+      $(x, X) \gets \id{setup}()$; \\
+      $(R, c) \gets B^{\Xid{H_I}{trap}(\cdot, \cdot), C()}(x, X)$; \\
+      $(r, Y) \gets T(R, c, Q_H)$; \\
+      $Y' \gets x R$; $h' \gets H_I(R, Y')$; $r' \gets c \xor h'$; \\
+      \IF $r \ne \bot$ \THEN \\ \quad
+        \IF $Y = \bot \lor R \ne r P \lor Y \ne Y'$ \THEN \RETURN $0$; \\
+      \IF $R = r' P$ \THEN $(r^*, Y^*) \gets (r', Y')$; \\
+      \ELSE $(r^*, Y^*) \gets (\bot, \bot)$; \\
+      \IF $(R, c) \in Q_C$ \THEN \RETURN $1$; \\
+      \IF $(r, Y) = (r', Y')$ \THEN \RETURN $1$; \\
+      \RETURN $0$;
     \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)$;
+    Oracle $\Xid{H_I}{trap}(R', Y')$: \+ \\
+      $h \gets H_I(R', Y')$; \\
+      $Q_H \gets Q_H \cup \{(R', Y', h)\}$; \\
+      \RETURN $h$; \- \\[\medskipamount]
+    Oracle $C()$: \+ \\
+      $r \getsr \gf{q}$; \\
+      $R \gets r P$; $c \gets r \xor H_I(R, r X)$; \\
+      $Q_C \gets Q_C \cup \{(R, c)\}$; \\
+      \RETURN $(R, c)$
   \end{program}
 
-  \caption{The key-exchange protocol: message handling}
-  \label{fig:kx-messages}
+  \caption{Discrete log extraction game: $\Game{dl-ext}{G}(T, B)$}
+  \label{fig:dlext}
 \end{figure}
 
+Let's unpack this definition slightly.  We make the following demands of our
+extractor.
+\begin{itemize}
+\item It is given a bare `transcript' of $B$'s execution.  In particular, it
+  is given only its output and a list of $B$'s random-oracle queries in no
+  particular order.
+\item While the extractor is not given the private key~$x$, the adversary~$B$
+  is given the private key.
+\item We require that, if the extractor produces values $r, Y \ne \bot$ then
+  $r$ and $Y$ are \emph{correct}; i.e., that $R = r P$ and $Y = x R$.
+\item The extractor is explicitly \emph{not} given the outputs of the
+  challenge-generation oracle $C()$, nor of the random-oracle queries issued
+  by $C()$.  However, we allow the extractor to fail (i.e., return $\bot$) if
+  $B$ simply parrots one of its $C$-outputs.
+\item The extractor is allowed -- indeed \emph{required} -- to fail if the
+  challenge $(R, c)$ is \emph{invalid} (i.e., Alice would return $\bot$ given
+  the challenge).
+\end{itemize}
+The resulting definition bears a striking similarity to the concept of
+\emph{plaintext awareness} in \cite{Bellare:1998:RAN}.
+
+Such an extractor indeed exists, as the following lemma states.
+\begin{lemma}[Effectiveness of extractor $T_\Wident$]
+  \label{lem:dlext}
+  There exists a \emph{universal discrete-log extractor} $T_\Wident$, shown
+  in figure~\ref{fig:twident}, such that, for any algorithm $B$,
+  \[ \Succ{dl-ext}{G}(T_\Wident, B) \ge 1 - \frac{1}{2^{\ell_I}}. \]
+  Moreover, if $B$ issues at most $q_H$ random-oracle queries, then the
+  running time of $T_\Wident$ is $O(q_H)$.
+\end{lemma}
+\ifshort
+The proof of this lemma is given in the full version of this paper.
+\else
+We prove this result at the end of the section.  For now, let us see how to
+prove that $\Wident$ is zero-knowledge.
+\fi
+
 \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$; \- \\
+    Extractor $T_\Wident(R, c, Q_H)$: \+ \\
+      \FOR $(R', Y', h)$ \IN $Q_H$ \DO \\ \ind
+        $r \gets h \xor c$; \\
+        \IF $R = R' = r P \land Y' = r X$ \THEN \RETURN $(r, Y')$; \- \\
+      \RETURN $(\bot, \bot)$;
+  \end{program}
+
+  \caption{The discrete-log extractor $T_\Wident$}
+  \label{fig:twident}
+\end{figure}
+
+We use the set-up described in section~\ref{sec:sim}.  Our initialization
+function~$I_\Wident$ just chooses a random $x \in \gf{q}$ as the world
+private input and sets $X = x P$ as the common input.  In the `real world',
+the adversary is allowed to submit a (single) challenge to the prover; it is
+given the prover's response, and must then compute its output.  This is shown
+on the left hand side of figure~\ref{fig:wident-sim}.
+
+The zero-knowledge property of the scheme is described by the following
+theorem.
+\begin{theorem}[Statistical zero-knowledge of $\Wident$]
+  \label{thm:wident-zk}
+  Let $I_\Wident$, $W_\Wident$ and $S_\Wident$ be the real-prover world and
+  simulator shown in figure~\ref{fig:wident-sim}.  Then, for any~$t$,
+  $q_I$ and $q_C$,
+  \[ \InSec{sim}(W_\Wident, I_\Wident, S_\Wident; t, q_I, q_C, 0) \le
+       \frac{q_C}{2^\ell_I}.
+  \]
+  where $q_C$ is the maximum number of challenges allowed by the adversary.
+\end{theorem}
+\begin{longproof}{}
+  The simulator simply uses the extractor~$T_\Wident$ to extract the answer
+  from the adversary's history of random oracle queries.  Observe that
+  $S_\Wident$ is a fake-world simulator.  By lemma~\ref{lem:dlext}, the
+  extractor fails with probability only $2^{-\ell_I}$.  The theorem follows
+  by a simple union bound and proposition~\ref{prop:fakesim}.
+\end{longproof}
+
+%\ifshort\else
+\begin{figure}
+  \begin{program}
+    Initialization function $I_\Wident()$: \+ \\
+      $x \getsr \gf{q}$; \\
+      $X \gets x P$; \\
+      \RETURN $(x, X)$;
+    \- \\[\medskipamount]
+    Real-prover world $W_\Wident^{H_I(\cdot, \cdot)}
+        ((x, X), \sigma, \tau, \mu)$: \+ \\
+      \IF $\tau = \cookie{challenge}$ \THEN \\ \ind
+        $(R, c) \gets \mu$; \\
+        $Y \gets \id{response}^{H_I(\cdot, \cdot)}(R, c, x)$; \\
+        \RETURN $(1, Y)$; \- \\
       \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$;
+        \RETURN $(\sigma, \bot)$;
+  \next
+  Simulator $S_\Wident$'s fake world \\
+  \hspace{1in} $W_{\text{sim}}^{H_I(\cdot, \cdot)}
+      ((X, u), \sigma, \tau, \mu)$: \+ \\
+      \IF $\tau = \cookie{init}$ \THEN \\ \ind
+        \RETURN $(\emptyset, \emptystring)$; \- \\
+      $Q_H \gets \sigma$; \\
+      \IF $\tau = \cookie{challenge}$ \THEN \\ \ind
+        $(R, c) \gets \mu$; \\
+        $(r, Y) \gets T_\Wident(R, c, Q_H)$; \\
+        \RETURN $(Q_H, Y)$; \- \\
+      \ELSE \IF $\tau = \cookie{random}$ \THEN \\ \ind
+        $(i, (R', Y'), h) \gets \mu$; \\
+        $Q_H \gets Q_H \cup \{(R', Y', h)\}$; \\
+        \RETURN $(Q_H, \emptystring)$; \- \\
+      \ELSE \\ \ind
+        \RETURN $(\sigma, \bot)$;
   \end{program}
 
-  \caption{The key-exchange protocol: support functions}
-  \label{fig:kx-support}
+  \caption{Real-prover and simulator for zero-knowledge of $\Wident$}
+  \label{fig:wident-sim}
 \end{figure}
+%\fi
+
+\ifshort\else
+We now return to proving that the extractor $T_\Wident$ functions as claimed.
+The following two trivial lemmata will be useful, both now and later.
+\begin{lemma}[Uniqueness of discrete-logs]
+  \label{lem:unique-dl}
+  Let $G = \langle P \rangle$ be a cyclic group.  For any $X \in G$ there is
+  a unique $x \in \gf{q}$ where $X = x P$.
+\end{lemma}
+\begin{proof}
+  Certainly such an $x$ exists, since $G$ is cyclic and finite.  Suppose $X =
+  x P = x' P$: then $0 = x P - x' P = (x - x') P$.  Hence $(x - x')$ is a
+  multiple of $q$, i.e., $x = x'$.
+\end{proof}
+\begin{lemma}[Uniqueness of check values]
+  \label{lem:unique-c}
+  Let $G = \langle P \rangle$ be a cyclic group of prime order $q$; let $H_I$
+  be a function $H_I\colon \Bin^{2\ell_G} \to \Bin^{\ell_I}$.  Fix some $x
+  \in \gf{q}$ and define the set
+  \[ V_x = \bigl\{\, (R, c) \in G \times \Bin^{\ell_I} \bigm|
+                R = \bigl( c \xor H_I(R, x R) \bigr) P \,\bigr\}.
+  \]
+  Then, for any $R$, $c$, $c'$, if $(R, c) \in V_x$ and $(R, c') \in V_x$
+  then $c = c'$.
+\end{lemma}
+\begin{proof}
+  From lemma~\ref{lem:unique-dl}, we see that there is a unique $r \in \gf{q}$
+  for which $R = r P$.  Now, if $(R, c) \in V_x$, we must have $r = c \xor
+  H_I(R, x R)$.  It follows that $c = r \xor H_I(R, x R)$.
+\end{proof}
 
-%%%--------------------------------------------------------------------------
+\begin{proof}[Proof of lemma~\ref{lem:dlext}]
+  Let $B$ be any randomized algorithm, and let $(R, c, Q_H)$ be as given to
+  the extractor by $\Game{dl-ext}{G}(T_\Wident, B)$.  Let the quantities
+  $H_I$, $Q_C$, $r$, $r'$, $x$ and $X$ be as in that game.
+
+  Suppose that the extractor returns values $(r, Y) \ne (\bot, \bot)$.  Let
+  $h = r \xor c$; then there must be a query $(R, Y, h) \in Q_H$, and we have
+  $R = r P$ and $Y = r X = r (x P) = x (r P) = x R = Y'$, so the extractor's
+  output must be correct unless it fails.
+
+  Furthermore, in the case where the extractor did not fail, we have $h =
+  H_I(R, Y) = H_I(R, Y')$ and $c = r \xor h$, so the challenge was valid.
+  Therefore, if the challenge was invalid, the extractor will fail.
+
+  We now deal with the challenge-generation oracle.  Suppose that $(R, c')
+  \in Q_C$ for some $c'$.  Now, if $c = c'$ then $(R, c')$ is a repeat of
+  some challenge from the challenge-generation oracle, and the extractor is
+  permitted to fail.  On the other hand, suppose $c \ne c'$; then, the
+  challenge $(R, c)$ must be invalid by lemma~\ref{lem:unique-c}, so the
+  extractor is required to fail, and we have established that indeed it will.
+  From now on, suppose that $R$ is distinct from all the $R$-values returned
+  by $C()$.
+
+  Let $Y = x R$.  Suppose that $B$ queried its random oracle at $(R, Y)$.
+  Let $h = H_I(Y)$, so $r' = c \xor h$.  If the challenge is valid then $R =
+  r' P$; therefore $Y = x R = x r' P = r' X$, so we have $(R, Y, h) \in Q_H$
+  with $R = r P$ and $Y = r X$.  Hence the extractor returns $r = r'$ as
+  required.
+
+  It remains to deal with the case where there is no random-oracle query at
+  $(R, Y)$.  But then $h = H_I(R, Y)$ is uniformly distributed, and
+  independent of the entire game up to this point.  Let $r$ be the correct
+  discrete log of $R$; by lemma~\ref{lem:unique-dl} there is only one
+  possible value.  The extractor always fails under these circumstances, but
+  a correct responder would reply with probability
+  \[ \Pr[h = c \xor r] = \frac{1}{2^{\ell_I}}. \]
+  This concludes the proof.
+\end{proof}
+\begin{remark}
+  Note that the fact that the algorithm~$B$ was given the private key is
+  irrelevant to the above argument.  However, we shall need this property
+  when we come to prove deniability for the key-exchange protocol.
+\end{remark}
+\begin{remark}
+  It's easy to see from the above proof that the extractor works flawlessly
+  on the `honest verifier' algorithm $\id{challenge}$ shown in
+  figure~\ref{fig:wident-ro}.  This shows that $\Wident$ is perfect
+  zero-knowledge against honest verifiers.  We're much more interested in
+  dishonest verifiers, though.
+\end{remark}
+\fi
 
-\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}.
+\ifshort\else
+\subsection{An identity-based identification scheme}
+\label{sec:wident-id}
+
+Boneh and Franklin \cite{Boneh:2003:IBE} showed how to construct an
+identity-based encryption scheme using bilinear pairings.  The resulting
+encryption scheme looks somewhat like a pairing-based version of ElGamal's
+encryption scheme \cite{ElGamal:1985:PKCb}.  We can easily apply their
+techniques to our identification protocol, and thereby obtain an
+identity-based identification scheme.  Providing the necessary formalisms to
+prove theorems analogous to our theorems~\ref{thm:wident-sound}
+and~\ref{thm:wident-zk} would take us too far from our objectives; but given
+appropriate security notions, we can readily adapt our existing proofs to the
+new setting.
+
+\subsubsection{Bilinear pairings}
+Before we describe the necessary modifications to the protocol, we first give
+a (very brief!) summary of cryptographic pairings.  (The Boneh-Franklin paper
+\cite{Boneh:2003:IBE} gives more detail; also \cite{Menezes:2005:IPB}
+provides a useful introduction to the topic.)
+
+Let $(G, +)$, $(G', +)$ and $(G_T, \times)$ be cyclic groups with prime order
+$q$; let $P \in G$ and $P' \in G'$ be elements of order $q$ in $G$ and $G'$
+respectively.  We say that a mapping $\hat{e}\colon G \times G' \to G_T$ is a
+\emph{non-degenerate bilinear pairing} if it satisfies the following
+properties.
+\begin{description}
+\item[Bilinearity] For all $R \in G$ and $S', T' \in G'$, we have $\hat{e}(R,
+  S' + T') = \hat{e}(R, S')\,\hat{e}(R, T')$; and for all $R, S \in G$ and $T'
+  \in G'$ we have $\hat{e}(R + S, T') = \hat{e}(R, T')\,\hat{e}(S, T')$.
+\item[Non-degeneracy] $\hat{e}(P, P') \ne 1$.
+\end{description}
+For practical use, we also want $\hat{e}(\cdot, \cdot)$ to be efficient to
+compute.  The reader can verify that $\hat{e}(a P, b P') = \hat{e}(P,
+P')^{ab}$.  It is permitted for the two groups $G$ and $G'$ to be equal.
+
+We require a different intractability assumption, specifically that the
+\emph{bilinear} Diffie-Hellman problem (BDH) -- given $(a P, b P, a P', c P')
+\in G^2 \times G'^2$, find $\hat{e}(P, P')^{abc} \in G_T$ -- is difficult.
+This implies the difficulty of the computational Diffie-Hellman problem in
+all three of $G$, $G'$ and~$G_T$.
+
+\subsubsection{The identity-based scheme}
+We need a trusted authority; following \cite{Schneier:1996:ACP} we shall call
+him Trent.  Trent's private key is $t \in \gf{q}$; his public key is $T =
+t P$.
+
+Finally, we need cryptographic hash functions $H_I\colon G \times G_T \to
+\Bin^{\ell_I}$ and $\Hid\colon \Bin^* \to G'$; a formal security analysis
+would model these as random oracles.
+
+Alice's public key is $A = \Hid(\texttt{Alice}) \in G'$.  Her private key is
+$K_A = t A \in G'$ -- she needs Trent to give this to her.  Bob can interact
+with Alice in order to verify her identity as follows.
+\begin{enumerate}
+\item Bob computes $\gamma_A = \hat{e}(T, A) \in G_T$.  (He can do this once
+  and store the result if he wants, but it's not that onerous to work it out
+  each time.)
+\item Bob chooses $r \inr \gf{q}$, and sets $R = r P$.  He also computes
+  $\psi = \gamma_A^r$, $h = H_I(R, \psi)$ and $c = r \xor h$.  He sends his
+  challenge $(R, c)$ to Alice.
+\item Alice receives $(R', c')$.  She computes $\psi' = \hat{e}(R, K_A)$, $h'
+  = H_I(R', \psi')$, and $r' = c' \xor h')$.  She checks that $R' = r' P$; if
+  so, she sends $\psi'$ back to Bob; otherwise she refuses to talk to him.
+\item Bob receives $\psi'$.  If $\psi = \psi'$ then he accepts that he's
+  talking to Alice.
+\end{enumerate}
+This works because $\psi = \gamma_A^r = \hat{e}(T, A)^r = \hat{e}(t P, A)^r =
+\hat{e}(r P, A)^t = \hat{e}(R, t A) = \psi'$.
+
+\subsubsection{Informal analysis}
+An analogue to lemma~\ref{lem:dlext} can be proven to show how to extract $r$
+from a verifier's random-oracle queries; statistical zero knowledge would
+then follow easily, as in theorem~\ref{thm:wident-zk}.  Soundness is
+intuitively clear, since an adversary must compute $\psi = \hat{e}(P,
+P')^{art}$ given $A = a P'$, $R = r P$ and $T = t P$, which is an instance of
+the BDH problem.  An analogue of theorem~\ref{thm:wident-sound} would have to
+prove this for an adversary capable of making identity requests as well as
+obtaining challenges.  Finally, our key-exchange protocol can be constructed
+out of this identity-based identification scheme, yielding an identity-based
+authenticated key-exchange protocol.  We leave it to the reader to work
+through the details.
+\fi
 
-\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.
+\ifshort\else
+\subsection{Comparison with the protocol of Stinson and Wu}
+\label{sec:stinson-ident}
+
+Our protocol is similar to a recent proposal by Stinson and Wu
+\cite{cryptoeprint:2006:337}.  They restrict their attention to Schnorr
+groups $G \subset \F_p^*$.  Let $\gamma$ be an element of order $q = \#G$.
+The prover's private key is $a \inr \gf{q}$ and her public key is
+$\alpha = \gamma^a$.  In their protocol, the challenger chooses
+$r \inr \gf{q}$, computes $\rho = \gamma^r$ and $\psi = \alpha^r$, and sends
+a challenge $(\rho, H(\psi))$.  The prover checks that $\rho^q \ne 1$,
+computes $\psi = \rho^a$, checks the hash, and sends $\psi$ back by way of
+response.  They prove their protocol's security in the random-oracle model.
+
+Both the Wrestlers protocol and Stinson-Wu require both prover and verifier
+to compute two exponentiations (or scalar multiplications) each.  The
+sizes of the messages used by the two protocols are also identical.
+
+(An earlier version of the Stinson-Wu protocol used a cofactor
+exponentiation: if we set $f = (p - 1)/q$, then we use $\psi = \alpha^{rf}) =
+\rho^{af} = \gamma^{afr}$.  This is more efficient in typical elliptic curve
+subgroups, since the cofactor of such subgroups is usually small: indeed,
+\cite{SEC1} recommends rejecting groups with cofactor $f > 4$.  However, in
+the Schnorr groups used by Stinson and Wu, the cofactor is much larger than
+$q$, and their new variant is more efficient.)
+
+We note that the zero-knowledge property of the Stinson-Wu protocol requires
+the Diffie-Hellman knowledge of exponent assumption (KEA).  Very briefly:
+suppose $A$ is a randomized algorithm which takes as input $X \in G$ and
+outputs a pair $(r P, r X)$; intuitively, the KEA asserts $A$ must have done
+this by choosing $r$ somehow and then computing its output from it.
+Formally, it asserts the existence of an `extractor' algorithm which takes as
+input the element $X$ and the random coins used by $A$ and outputs $r$ with
+high probability.  This is a very strong assumption, and one which is
+unnecessary for our protocol, since we can present an \emph{explicit}
+extractor.
+
+The KEA assumption as stated in \cite{cryptoeprint:2006:337} allows the
+extractor to fail with some negligible probability, over and above the
+probability that a dishonest verifier managed to guess the correct
+$h = H(\psi)$ without making this random-oracle query.  Not only does our
+protocol achieve zero- knowledge without the KEA, our extractor is, in this
+sense, `perfect'.
+
+Our protocol is just as strong as Stinson-Wu under attack from active
+intruders: see table~\ref{tab:wident-active} for a very brief sketch of the
+case-analysis which would be the basis of a proof of this.
+
+\begin{table}
+  \begin{tabular}[C]{|*{3}{c|}p{8cm}|}
+    \hlx{hv[1]}
+    \multicolumn{2}{|c|}{\textbf{Challenge}} &
+    \textbf{Response} &
+    \textbf{Security}
+    \\ \hlx{v[1]hv}
+    %% unpleasant hacking to make the R and c columns the same width :-(
+    \settowidth{\dimen0}{\textbf{Challenge}}%
+    \dimen0=.5\dimen0
+    \advance\dimen0by-\tabcolsep
+    \advance\dimen0by-.5\arrayrulewidth
+    \hbox to\dimen0{\hfil$R$\hfil}
+         & $c$  & $Y$  & Nothing to prove.			\\ \hlx{v}
+    $R$  & $c'$ & ---  & Prover rejects by lemma~\ref{lem:unique-c};
+                         $Y'$ probably wrong by
+                         theorem~\ref{thm:wident-sound}.         \\ \hlx{v}
+    $R$  & $c$  & $Y'$ & Response is incorrect.			\\ \hlx{v}
+    $R'$ & ---  & $Y$  & Response is incorrect.			\\ \hlx{v}
+    $R'$ & $c$  & $Y'$ & Prover rejects with probability $1 - 2^{-\ell_I}$;
+                         $Y'$ probably wrong by
+                         theorem~\ref{thm:wident-sound}.         \\ \hlx{v}
+    $R'$ & $c'$ & $Y'$ & Simulate prover using extractor
+                         (lemma~\ref{lem:dlext}); $Y'$ probably wrong by
+                         theorem~\ref{thm:wident-sound}.         \\ \hlx{vh}
+  \end{tabular}
+
+  \caption{Security of $\Wident$ against active intruders (summary)}
+  \label{tab:wident-active}
+\end{table}
+
+An identity-based analogue of Stinson-Wu can be defined using a bilinear
+pairing, just as we did in section~\ref{sec:wident-id}.  However, to prove
+the zero-knowledge property, one needs to make a bilinear analogue of the
+knowledge of exponent assumption.
+
+We suspect that a key-exchange protocol like ours can be constructed using
+Stinson-Wu rather than the Wrestlers identification scheme.  We haven't,
+however, gone through all the details, since we believe our protocol is just
+as efficient and is based on much more conservative assumptions.
+\fi
+
+%%%--------------------------------------------------------------------------
+
+\section{A simple key-exchange protocol}
+\label{sec:kx}
+
+In this section, we describe a simple key-exchange protocol built out of the
+identification protocol shown previously.
+
+The key-exchange protocol arises from the following observation.  If Bob
+sends a challenge, presumably to Alice, and gets a correct response, then not
+only did he really send the challenge to Alice but he knows that she received
+it correctly.
+
+So, if Alice and Bob authenticate each other, by the end of it, they should
+each have chosen a random private value, sent the corresponding public value
+to the other, and been convinced that it arrived safely.
+
+Unfortunately, life isn't quite this kind, and we have to do some more work
+to make this scheme secure.
+
+
+Our key exchange protocol essentially consists of two parallel instances of
+the identification protocol.  If Alice receives a correct response to her
+challenge, she will know that Bob received her challenge correctly, and
+\emph{vice versa}.  If we let Alice's challenge be $R_0 = r_0 P$ and Bob's
+challenge be $R_1 = r_1 P$ then each can compute a shared secret $Z = r_0 R_1
+= r_0 r_1 P = r_1 R_0$ unknown to an adversary.  There are, unfortunately, a
+few subtleties involved in turning this intuition into a secure key-exchange
+protocol, which we now describe.
+
+
+\subsection{Overview}
+\label{sec:kx-overview}
+
+We present a quick, informal description of our basic key-exchange protocol.
+In addition to our group $G$, we shall also need a secure symmetric
+encryption scheme $\E = (\kappa, E, D)$, and two secure hash functions
+$H_I\colon \Bin^{2\ell_G} \to \Bin^{\ell_I}$ and $H_K\colon \Bin^{\ell_G+1}
+\to \Bin^\kappa$.
+
+Suppose that Alice's and Bob's private keys are $a$ and $b$ respectively, and
+their public keys are $A = a P$ and $B = b P$.
+\begin{enumerate}
+\item Alice chooses a random index $r \inr \gf{q}$.  She computes $R = r P$ and
+  $c = r \xor H_I(R, r B)$.  She sends the pair $(R, c)$ to Bob.
+\item Similarly, Bob chooses a random $s \inr \gf{q}$.  He computes $S = s P$
+  and $d = s \xor H_I(S, s A)$.  He sends $(S, d)$ to Alice.
+\item Alice receives $(S', d')$ from Bob.  She computes $s' = d' \xor H_I(S',
+  a S')$, and verifies that $S' = s' P$.  If so, she computes $K_A = H_K(0
+  \cat r S')$, and sends $R, E_{K_A}(a S')$ to Bob.
+\item Similarly, Bob receives $(R', c')$ from Alice.  He verifies that $R' =
+  \bigl( c' \xor H_I(R', b R') \bigr) P$.  If so, he computes $K_B = H_K(0
+  \cat s R')$ and sends S, $E_{K_B}(b R')$ to Alice.
+\item Alice receives a ciphertext $(S'', \chi_B)$ from Bob.  She checks that
+  $S'' = S'$, decrypts $\chi_B$, and checks that $D_{K_A}(\chi_B) = r B$.  If
+  so, she uses $H_K(1 \cat r S')$ as her shared secret.
+\item Similarly, Bob receives $(R'', \chi_A)$ from Alice, and checks $R'' =
+  R'$ and $D_{K_B}(\chi_A) = s A$.  If so, he uses $H_K(1 \cat s R')$ as his
+  shared secret.
+\end{enumerate}
+This is the Wrestlers Key Exchange protocol, $\Wkx^{G, \E}$ (again, we omit
+the superscripts when referring to the general protocol, or when confusion is
+unlikely).  A diagrammatic summary of the protocol is shown in
+figure~\ref{fig:wkx}.
 
 \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}
+  \begin{description}
+  \item[Setup] Group $G = \langle P \rangle$; $\#G = q$ is prime.
+    $H_I(\cdot, \cdot)$ and $H_K(\cdot)$ are secure hashes.  $\E = (\kappa,
+    E, D)$ is an IND-CCA2 symmetric encryption scheme.
+  \item[Parties] $U_i$ for $0 \le i < n$.
+  \item[Private keys] $x_i \inr \gf{q}$.
+  \item[Public keys] $X_i = x_i P$.
+  \end{description}
+  \begin{protocol}
+    $r_i \getsr I$; $R_i \gets r_i P$; &
+    $r_j \getsr I$; $R_j \gets r_j P$; \\
+    $c_i \gets r_i \xor H_I(R_i, r_i X_j)$; &
+    $c_j \gets r_j \xor H_I(R_j, r_j X_i)$; \\
+    \send{->}{(R_i, c_i)}
+    \send{<-}{(R_j, c_j)}
+    Check $R_j = \bigl(c_j \xor H_I(x_i R_j)\bigr) P$; &
+    Check $R_i = \bigl(c_i \xor H_I(x_j R_i)\bigr) P$; \\
+    $Z \gets r_i R_j$; $(K_0, K_1) \gets H_K(Z)$; &
+    $Z \gets r_j R_i$; $(K_0, K_1) \gets H_K(Z)$; \\
+    $\chi_i \gets E_{K_0}(x_i R_j)$; &
+    $\chi_j \gets E_{K_0}(x_j R_i)$; \\
+    \send{->}{(R_i, \chi_i)}
+    \send{<-}{(R_j, \chi_j)}
+    Check $D_{K_0}(\chi_j) = r_i X_j$; &
+    Check $D_{K_0}(\chi_i) = r_j X_i$; \\
+    Shared key is $K_1$. & Shared key is $K_1$.
+  \end{protocol}
+
+  \caption{Summary of the Wrestlers Key Exchange protocol, $\Wkx$}
+  \label{fig:wkx}
 \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}
+
+Assume, for the moment, that Alice and Bob's messages are relayed honestly.
+Then:
+\begin{itemize}
+\item $a S' = a S = a (s P) = s (a P) = s A$, so $s' = d' \xor H_I(S' a S') =
+  d \xor H_I(S, s A) = s$, and $S' = S = s P = s' P$, and therefore Alice
+  responds to Bob's message;
+\item similarly $b R' = r B$, so $r' = r$ and $R' = r' P$, and therefore Bob
+  responds to Alice's message;
+\item $b R' = b R = b (r P) = r (b P) = r B$, and $a S' = a S = a (s P) = s
+  (a P) = s A$, and therefore both parties compute their responses correctly;
+  and
+\item $r S' = r S = r (s P) = s (r P) = s R = s R'$, so $K_A = K_B$, and
+  therefore they can decrypt each others' responses, and agree the same
+  shared secret.
+\end{itemize}
+This shows that the protocol is basically valid, but says little about its
+security.  The remainder of this section will describe our protocol in more
+formal detail, and prove its security in a model with multiple parties and an
+adversary who controls the network.
+
+Observe that the protocol as we've presented here is \emph{symmetrical}.
+There's no notion of `initiator' or `responder'.  There are a total of four
+messages which must be sent before both parties accept.  However, this can be
+reduced to three by breaking the symmetry of the protocol and combining one
+or other party's challenge and response messages.  We choose to analyse the
+symmetrical version, since to do so, it suffices to consider only the two
+different kinds of messages.  Since our security model allows the messages to
+be adversarially delayed and reordered, it is easy to show that the security
+of an optimized, asymmetrical protocol is no worse than the symmetrical
+version we present here.
+
+
+\subsection{Security model and security definition}
+\label{sec:um}
+
+Our model is very similar to that of Canetti and Krawczyk
+\cite{Canetti:2001:AKE}, though we have modified it in two ways.
+\begin{enumerate}
+\item We allow all the participants (including the adversary) in the protocol
+  access to the various random oracles required to implement it.
+\item Since we want to analyse a specific, practical scheme, asymptotic
+  results are useless.  We measure the adversary's resource usage carefully,
+  and produce a quantitative bound on the adversary's advantage in the
+  SK-security game.
+\end{enumerate}
+
+\ifshort
+
+Readers interested in the details of the model should see Canetti and
+Krawczyk's paper \cite{Canetti:2001:AKE}, or the full version of this paper.
+
+\else
+
+\subsubsection{Overview}
+We briefly describe our modified model, pointing out the changes we have
+made, and how they apply to our protocol.  Much of Canetti and Krawczyk's
+model (for example, the local and global outputs) is useful for proving more
+general security properties such as demonstrating that SK-security suffices
+for constructing secure channels, and we shall not concern ourselves with
+such details.  Other parts deal with issues such as security parameters and
+ensuring that all the computation is polynomially bounded, which are
+irrelevant since we are dealing with a single concrete protocol rather than a
+family of them.
+
+The entities in the model are the \emph{adversary}~$A$, and a (fixed) number
+of \emph{parties}~$P_i$, for $0 \le i < n$.  If the protocol under
+consideration makes use of random oracles, then all the participants -- the
+adversary and the parties -- are all allowed access to the random oracles.
+
+The parties and the adversary play a `game'.  At the beginning of the game,
+the participants are given some inputs computed by a randomized
+\emph{initialization procedure}~$\id{init}$.  This produces as output a pair
+$(i_U, \mathbf{i})$; the value $i_U$ is the \emph{global input}, and is given
+to all the participants including the adversary.  The vector $\mathbf{i}$ has
+$n$ components, and party $P_i$ is given $(i_U, \mathbf{i}[i])$ as input.
+
+\subsubsection{Sessions}
+Parties don't act directly.  Instead, each party runs a number of
+\emph{sessions}.  A session is represented by a triple $S = (P_i, P_j, s)$,
+where $i, j \in \Nupto{n}$ identify the owning party and a \emph{partner},
+and $s \in \Bin^{\ell_S}$ is a \emph{session-id}.  (The original model
+includes a r\^ole, for distinguishing between initiators and responders.  Our
+protocol is symmetrical, so this distinction isn't useful.)  If $P_i$ runs a
+session $S = (P_i, P_j, s)$ and $P_j$ runs a session $S' = (P_j, P_i, s)$
+then we say that $S$ and $S'$ are \emph{matching}, and that $P_j$ is $P_i$'s
+\emph{partner} for the session.
+
+At most one participant in the game is \emph{active} at any given time.
+Initially the adversary is active.  The adversary may \emph{activate} a
+session in one of two ways.
+\begin{enumerate}
+\item It may \emph{create a session} of a party~$P_i$, by selecting a
+  session-id~$s \in \Bin^{\ell_S}$ and a partner $j$.  There is no
+  requirement that $P_j$ ever have a matching session.  However, all sessions
+  of a party must be distinct, i.e., sessions with the same partner must have
+  different session-ids.
+\item It may \emph{deliver a message}~$\mu \in \Bin^*$, from party~$P_j$, to
+  an existing session~$S = (P_i, P_j, s)$.  There is no requirement that any
+  party previously sent $\mu$: the adversary is free to make up messages as
+  it sees fit.
+\end{enumerate}
+The adversary becomes inactive, and the session becomes active.  The session
+performs some computation, according to its protocol, and may request a
+message~$\mu$ be delivered to the matching session running in its partner
+(which may not exist).  The session may also \emph{terminate}.  In the case
+we are interested in, of key-exchange protocols, a session~$S = (P_i, P_j,
+s)$ may terminate in one of two ways:
+\begin{enumerate}
+\item it may \emph{complete}, outputting $(i, j, s, K)$, for some
+  \emph{session key}~$K$, or
+\item it may \emph{abort}, outputting $(i, j, s, \bot)$.
+\end{enumerate}
+Once it has performed these actions, the session deactivates and the
+adversary becomes active again.  The adversary is given the message~$\mu$, if
+any, and informed of whether the session completed or aborted, but, in the
+case of completion, not of the value of the key~$K$.  A session is
+\emph{running} if it has been created and has not yet terminated.
+
+\subsubsection{Other adversarial actions}
+As well as activating sessions, the adversary has other capabilities, as
+follows.
+\begin{itemize}
+\item It may \emph{expire} any session~$S$, causing the owning party to
+  `forget' the session key output by that session.
+\item It may \emph{corrupt} any party~$P_i$, at will: the adversary learns
+  the entire state of the corrupted party, including its initial
+  input~$\mathbf{i}[i]$, the state of any sessions it was running at the
+  time, and the session keys of any completed but unexpired sessions.  Once
+  corrupted, a party can no longer be activated.  Of course, the adversary
+  can continue to send messages allegedly from the corrupted party.
+\item It may \emph{reveal the state} of a running session~$S$, learning any
+  interesting values specific to that session, but \emph{not} the owning
+  party's long-term secrets.
+\item It may \emph{reveal the session-key} of a completed session~$S$.
+\item It may elect to be \emph{challenged} with a completed session~$S$,
+  provided.  Challenge sessions form part of the security notion for
+  key-exchange protocols.  See below for more details.
+\end{itemize}
+We say that a session $S = (P_i, P_j, s)$ is \emph{locally exposed} if
+\begin{itemize}
+\item it has had its state revealed,
+\item it has had its session-key revealed, or
+\item $P_i$ has been corrupted, and $S$ had not been expired when this
+  happened.
+\end{itemize}
+A session is \emph{exposed} if it is locally exposed, or if its matching
+session exists and has been locally exposed.
+
+At the beginning of the game, a bit $b^*$ is chosen at random.  The adversary
+may choose to be \emph{challenged} with any completed, unexposed
+session;\footnote{%
+  The original Canetti-Krawczyk definition restricts the adversary to a
+  single challenge session, but our proof works independent of the number of
+  challenge sessions, so we get a stronger result by relaxing the requirement
+  here.)}
+the adversary is then given either the session's key -- if $b^* = 1$ -- or a
+string chosen at random and independently of the game so far from a
+protocol-specific distribution -- if $b^* = 0$.  At the end of the game, the
+adversary outputs a single bit~$b$.
+
+\subsubsection{SK-security}
+We've now described the game; it is time to explain the adversary's goal in
+it.  The adversary \emph{wins} the game if either
+\begin{enumerate}
+\item two unexposed, matching sessions complete, but output different
+  keys,\footnote{%
+    The original Canetti-Krawczyk definition differs slightly here.  It
+    requires that `if two \emph{uncorrupted} parties complete matching
+    sessions then they both output the same key' [original emphasis].  This
+    can't be taken at face value, since none of the protocols they claim to
+    be secure actually meet this requirement: they meet only the weaker
+    requirement that parties completing matching sessions output different
+    keys with negligible probability.  We assume here that this is what they
+    meant.}
+  or
+\item the adversary correctly guesses the hidden bit~$b^*$.
+\end{enumerate}
+More formally, we make the following definition.
+\fi
+\begin{definition}[SK-security]
+  \label{def:sk}
+  Let $\Pi^{H_0(\cdot), H_1(\cdot), \ldots}$ be a key-exchange protocol
+  which makes use of random oracles $H_0(\cdot)$, $H_1(\cdot)$, \dots, and
+  let $A$ be an adversary playing the game described \ifshort in
+  \cite{Canetti:2001:AKE}\else previously\fi, where $n$
+  parties run the protocol~$\Pi$.  Let $V$ be the event that any pair of
+  matching, unexposed sessions completed, but output different session keys.
+  Let $W$ be the event that the adversary's output bit matches the game's
+  hidden bit~$b^*$.  We define the adversary's \emph{advantage against the
+    SK-security of the protocol~$\Pi$} to be
+  \[ \Adv{sk}{\Pi}(A, n) = \max(\Pr[V], 2\Pr[W] - 1). \]
+  Furthermore, we define the \emph{SK insecurity function of the
+  protocol~$\Pi$} to be
+  \[ \InSec{sk}(\Pi; t, n, q_S, q_M, q_{H_0}, q_{H_1}, \dots) =
+       \max_A \Adv{sk}{\Pi}(A, n)
+  \]
+  where the maximum is taken over all adversaries~$A$ with total running
+  time~$t$ (not including time taken by the parties), create at most $q_S$
+  sessions, deliver at most $q_M$~messages, and (if applicable) make at most
+  $q_{H_i}$ random-oracle queries to each random oracle $H_i(\cdot)$.
 \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}
+\subsection{Security}
+
+In order to analyse our protocol $\Wkx^{G, \E}$ properly, we must describe
+exactly how it fits into our formal model.
+
+\subsubsection{Sessions and session-ids}
+Our formal model introduced the concept of sessions, which the informal
+description of section~\ref{sec:kx-overview} neglected to do.  (One could
+argue that we described a single session only.)  As we shall show in
+section~\ref{sec:kx-insecure}, our protocol is \emph{insecure} unless we
+carefully modify it to distinguish between multiple sessions.
+
+In the model, distinct key-exchange sessions are given distinct partners and
+session-ids.  In order to prevent sessions interfering with each other, we
+shall make explicit use of the session-ids.
+
+Suppose the session-ids are $\ell_S$-bit strings.  We expand the domain of
+the random oracle $H_I$ so that it's now
+\[ H_I\colon G \times \Bin^{\ell_S} \times G \times G \to \Bin_{\ell_I}. \]
 
-The proof of this theorem is given in section~\ref{sec:cbc-proof}
+\subsubsection{Messages}
+We split the messages our protocols into two parts: a \emph{type}~$\tau$ and
+a \emph{body}~$\mu$.  We assume some convenient, unambiguous encoding of
+pairs $(\tau, \mu)$ as bit-strings.  For readability, we present message
+types as text strings, e.g., `\cookie{challenge}', though in practice one
+could use numerical codes instead.
 
-\subsection{Ciphertext stealing}
+The message body itself may be a tuple of values, which, again, we assume are
+encoded as bit-strings in some convenient and unambiguous fashion.  We shall
+abuse the notation for the sake of readability by dropping a layer of nesting
+in this case: for example, we write $(\cookie{hello}, x, y, z)$ rather than
+$\bigl(\cookie{hello}, (x, y, z)\bigr)$.
 
-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.
+\subsubsection{The protocol}
+Our protocol is represented by three functions, shown in
+figure~\ref{fig:wkx-formal}.
+\begin{itemize}
+\item $\id{init}(n)$ is the initialization function, as described in
+  section~\ref{sec:um}.  It outputs a pair $(\mathbf{p}, \mathbf{i})$, where
+  $\mathbf{i}[i]$ is the private key of party~$P_i$ and $\mathbf{p}[i]$ is
+  the corresponding public key.  Only $P_i$ is given $\mathbf{i}[i]$, whereas
+  all parties and the adversary are given $\mathbf{p}$.
+\item $\id{new-session}^{H_I(\cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
+  (\mathbf{p}, x, i, j, s)$ is the new-session function.  This is executed by
+  party~$P_i$ when the adversary decides to create a new session~$S = (P_i,
+  P_j, s)$.  It is also given the relevant outputs of $\id{init}$, and
+  allowed access to the random oracles $H_I$ and $H_K$.
+\item $\id{message}^{H_I(\cdot, \cdot, \cdot, \cdot), H_K(\cdot)} (\tau,
+  \mu)$ is the incoming-message function.  This is executed by a session when
+  the adversary decides to deliver a message $(\tau, \mu)$ to it.  It makes
+  use of the subsidiary functions $\id{msg-challenge}$ and
+  $\id{msg-response}$ to handle the messages.
+\end{itemize}
+We observe that the protocol never aborts.  We could make it do so if it
+receives an invalid message, but we prefer to ignore invalid messages for the
+sake of robustness.\footnote{%
+  Note that this protocol would therefore require modification before it was
+  acceptable in the simulation-based model of \cite{cryptoeprint:1999:012}.
+  There it is required that a key-exchange protocol terminate after a
+  polynomially-bounded number of messages are delivered to it.}
 
 \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$;
+    Function $\id{init}(n)$: \+ \\
+      \FOR $i \in \Nupto{n}$ \DO \\ \ind
+        $x \getsr \gf{q}$; \\
+        $\mathbf{i}[i] \gets x$; \\
+        $\mathbf{p}[i] \gets x P$; \- \\
+      \RETURN $(\mathbf{p}, \mathbf{i})$;
+    \- \\[\medskipamount]
+    Function $\id{new-session}^{H_I(\cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
+      (\mathbf{p}, x, i, j, s)$: \+ \\
+      $X \gets \mathbf{p}[i]$;
+      $X' \gets \mathbf{p}[j]$;
+      $C \gets \emptyset$; \\
+      $r \getsr \gf{q}$;
+      $R \gets r P$;
+      $Y \gets r X'$; \\
+      $h \gets H_I(X, s, R, Y)$;
+      $c \gets r \xor h$; \\
+      \SEND $(\cookie{challenge}, R, c)$;
+    \- \\[\medskipamount]
+    Function $\id{message}^{H_I(\cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
+      (\tau, \mu)$: \+ \\
+      \IF $\tau = \cookie{challenge}$ \THEN $\id{msg-challenge}(\mu)$; \\
+      \ELSE \IF $\tau = \cookie{response}$ \THEN $\id{msg-response}(\mu)$;
     \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$;
+    Function $\id{msg-challenge}(\mu)$: \+ \\
+      $(R', c') \gets \mu$; \\
+      $Y' \gets x R'$; \\
+      $h' \gets H_I(X', s, R', Y')$; \\
+      $r' \gets c' \xor h'$; \\
+      \IF $R' \ne r' P$ \THEN \RETURN; \\
+      $C \gets C \cup \{R\}$; \\
+      $Z \gets r R'$; \\
+      $(K_0, K_1) \gets H_K(Z)$; \\
+      $\chi \gets E_{K_0}(Y')$; \\
+      \SEND $(\cookie{response}, R, \chi)$;
+    \- \\[\medskipamount]
+    Function $\id{msg-response}(\mu)$: \+ \\
+      $(R', \chi') \gets \mu$; \\
+      \IF $R' \notin C$ \THEN \RETURN; \\
+      $Z \gets r R'$; \\
+      $(K_0, K_1) \gets H_K(Z)$; \\
+      $Y' \gets D_{K_0}(\chi')$; \\
+      \IF $Y' \ne Y$ \THEN \RETURN; \\
+      \OUTPUT $K_1$;
+      \STOP;
   \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.
+  \caption{Formalization of $\Wkx$}
+  \label{fig:wkx-formal}
+\end{figure}
+
+\subsubsection{Session states}
+We must specify what the adversary obtains when it chooses to reveal a
+session's state.  Given the program in figure~\ref{fig:wkx-formal}, we can
+see that the session state consists of the variables $(x, X, X', r, R, Y,
+C)$.
+
+However, $x$ is the owning party's long-term secret, and it seems
+unreasonable to disclose this to an adversary who stops short of total
+corruption.
+
+The public keys $X$ and $X'$ are part of the adversary's input anyway, so
+revealing them doesn't help.  Similarly, the set $C$ of valid challenges
+could have been computed easily by the adversary, since a group element $R'
+\in C$ if and only if the session $S$ responded to some message
+$(\cookie{challenge}, R', c')$.
+
+The value $R = r P$ is easily computed given $r$, and besides is sent in the
+clear in the session's first message.  The expected response $Y = r X'$ is
+also easily computed from $r$.  The converse is also true, since $r$ can be
+recovered from $R$ and $c$ in the session's challenge message and the value
+$Y$.  Besides, $r$ is necessary for computing $Z$ in response to incoming
+challenges.
+
+We conclude that the only `interesting' session state is $r$.
+
+\subsubsection{Security}
+Having formally presented the protocol, we can now state our main theorem
+about its security.  The proof is given in \ifshort the full version of the
+paper\else appendix~\ref{sec:sk-proof}\fi.
+\begin{theorem}[SK-security of $\Wkx$]
+  \label{thm:sk}
+  Let $G$ be a cyclic group.  Let $\E = (\kappa, E, D)$ be a symmetric
+  encryption scheme.  Then
+  \begin{spliteqn*}
+    \InSec{sk}(\Wkx^{G, \E}; t, n, q_S, q_M, q_I, q_K) \le
+      2 q_S \bigl( \InSec{ind-cca}(\E; t', q_M, q_M) + {} \\
+      \InSec{mcdh}(G; t', q_K) +
+      n \,\InSec{mcdh}(G; t', q_M + q_I) \bigr) +
+      \frac{n (n - 1)}{q} +
+      \frac{2 q_M}{2^{\ell_I}}.
+  \end{spliteqn*}
+  where $t' = t + O(n) + O(q_S) + O(q_M q_I) + O(q_K)$.
 \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$:
+
+\ifshort\else
+\subsection{Insecure protocol variants}
+\label{sec:kx-insecure}
+
+It's important to feed the session-id and verifier's public key to the random
+oracle $H_I$ when constructing the check-value~$c$.  Without these, the
+protocol is vulnerable to attack.  In this section, we consider some variants
+of our protocol which hash less information, and show attacks against them.
+
+To simplify the presentation, we shall consider Alice and Bob, and a third
+character Carol.  We shall be attacking a pair of matching sessions $A$
+and~$B$, run by Alice and Bob respectively.  Let Alice and Bob's private keys
+be $x_A$ and~$x_B$, and let their public keys be $X_A = x_A P$ and $X_B = x_B
+P$ respectively.
+
+\subsubsection{Protocol diagram notation}
+In order to keep the presentation as clear as possible, we use a simple
+diagrammatic notation for describing protocol runs.  A line of the form
+\protocolrun{\textit{action} \ar[r] & \PRsession{S} & \textit{result}}
+states that the adversary performs the given \textit{action} on session~$S$,
+with the stated \textit{result}.  The \textit{action} may be
+\begin{itemize}
+\item \textsf{Create session $(P_i, P_j, s)$}: the session is created,
+  running in party~$P_i$, with partner~$P_j$ and session-id~$s$.
+\item \textsf{Receive $\mu$}: the session is activated with an incoming message~$\mu$.
+\item \textsf{Session-state reveal}: The adversary requests the session's
+  internal state.
+\end{itemize}
+The \textit{result} may be
+\begin{itemize}
+\item \textsf{Send $\mu'$}: the session requests the delivery of the
+  message~$\mu'$.
+\item \textsf{Complete: $K$}: the session completes, outputting the key~$K$.
+\item \textsf{State: $\sigma$}: the session's state is revealed to
+  be~$\sigma$.
+\item \textsf{(Ignore)}: the result of the action is unimportant.
+\end{itemize}
+
+\subsubsection{Omitting the session-id}
+Consider a protocol variant where session $S$ sets $h_S = H_I(X_N, R_S,
+Y_S)$, where $N$ is the session's partner.  That is, we've omitted the
+session-id from the hash.  An adversary can cross over two sessions between
+Alice and Bob.  Here's how.
+
+The attack assumes that Alice and Bob set up two pairs of matching sessions
+with each other, thus.
+\protocolrun{
+  \PRcreate{Alice}{Bob}{s} & \PRsession{A} &
+    \PRsend{challenge}{R_A, c_A} \\
+  \PRcreate{Bob}{Alice}{s} & \PRsession{B} &
+    \PRsend{challenge}{R_B, c_B} \\
+  \PRcreate{Alice}{Bob}{s'} & \PRsession{A'} &
+    \PRsend{challenge}{R_{A'}, c_{A'}} \\
+  \PRcreate{Bob}{Alice}{s'} & \PRsession{B'} &
+    \PRsend{challenge}{R_{B'}, c_{B'}}
+}
+Observe that the session pairs use distinct session-ids $s \ne s'$, so this
+is allowed.  Now the adversary crosses over the challenges, using the second
+pair of sessions to provide responses to the challenges issued by the first
+pair.  By revealing the state in the second pair of sessions, the adversary
+can work out the (probably different) session keys accepted by the first
+pair.
+\protocolrun{
+  \PRreceive{challenge}{R_B, c_B} & \PRsession{A'} &
+    \PRsend{response}{R_{A'}, E_{K_{A'B,0}}(x_A R_B)} \\
+  \PRreceive{challenge}{R_A, c_A} & \PRsession{B'} &
+    \PRsend{response}{R_{B'}, E_{K_{B'A,0}}(x_B R_A)} \\
+  \PRreceive{challenge}{R_{A'}, c_{A'}} & \PRsession{A} & \PRignore \\
+  \PRreceive{challenge}{R_{B'}, c_{B'}} & \PRsession{B} & \PRignore \\
+  \PRreveal & \PRsession{A'} & r_{A'} \\
+  \PRreveal & \PRsession{B'} & r_{B'} \\
+  \PRreceive{response}{R_{B'}, E_{K_{B'A,0}}(x_B R_A)} & \PRsession{A} &
+    \PRcomplete{K_{AB',1}} \\
+  \PRreceive{response}{R_{A'}, E_{K_{A'B,0}}(x_A R_B)} & \PRsession{B} &
+    \PRcomplete{K_{BA',1}} \\
+}
+The adversary can now compute $K_{AB'} = H_K(r_{B'} R_A)$ and $K_{B'A} =
+H_K(r_{A'} R_B)$.  Safely in possession of both keys, the adversary can now
+read and impersonate freely.
+
+\subsubsection{Omitting the partner's public key}
+Now consider a protocol variant where session $S$ sets $h_S = H_I(s, R_S,
+Y_S)$, where $s$ is the session-id.  An adversary can use a sessions with
+Carol to attack a session between Alice and Bob.  Here's how the sessions are
+set up.
+\protocolrun{
+  \PRcreate{Alice}{Bob}{s} & \PRsession{A} &
+    \PRsend{challenge}{R_A, c_A} \\
+  \PRcreate{Bob}{Alice}{s} & \PRsession{B} &
+    \PRsend{challenge}{R_B, c_B} \\
+  \PRcreate{Alice}{Carol}{s} & \PRsession{A'} &
+    \PRsend{challenge}{R_{A'}, c_{A'}} \\
+  \PRcreate{Bob}{Carol}{s} & \PRsession{B'} &
+    \PRsend{challenge}{R_{B'}, c_{B'}}
+}
+Although each of Alice and Bob have two sessions with session-id~$s$, this is
+allowed, since they are with different partners.  The rest of the attack in
+fact proceeds identically to the previous case.
+\fi
+
+\subsection{Deniability}
+\label{sec:denial}
+
+We have claimed that the Wrestlers key-exchange protocol is \emph{deniable}.
+In this section, we define what we mean, explain the limits of the
+deniablility of the protocol as currently presented, fix the protocol with an
+additional pass (which can be collapsed to a single message flow by breaking
+the protocol's symmetry), and prove the deniability of the resulting
+protocol.
+
+Our notion of deniability is taken from Di~Raimondo, Gennaro and Krawczyk
+\cite{cryptoeprint:2006:280}, except that, as usual, we opt for a concrete
+security approach.
+
+\subsubsection{Discussion}
+Our definition for deniability is that, for any adversary interacting with
+participants in the protocol, a simulator exists which can compute the same
+things as the adversary.  In particular, since an adversary could output a
+transcript of the interactions between itself and the parties, it would
+follow that a simulator could do this too.  If the simulator is effective,
+its output is indistinguishable from that of the real adversary, and hence no
+`judge' (distinguisher) should be persuaded by evidence presented by someone
+who claims to have witnessed or participated in an interaction.
+
+We work again the model described in~\ref{sec:um}.  That is, our adversary
+has complete control over the ordering and delivery of all messages.  The
+adversary is also able, at any time, to reveal the state of any session.
+However, deniability is obviously impossible against an adversary who can
+\emph{corrupt} other parties, since simulating such an adversary's actions
+would necessarily require the simulator to compute private keys corresponding
+to the known public keys, and this is (we believe) difficult, because an
+efficient algorithm for doing this could easily attack our protocol, which we
+already proved secure.  Therefore, we forbid the adversary from corrupting
+parties.
+
+In order to allow the adversary to participate in the protocol, rather than
+merely observing it, we need to give it one or more private keys.  We could
+modify the initialization function \id{init} from figure~\ref{fig:wkx-formal}
+to give the adversary a private key, but there's an easier way: we can just
+give the adversary a number of private keys in its auxiliary input.
+
+\subsubsection{Definitions}
+Let $\Pi$ be a key-exchange protocol, in the model described in
+section~\ref{sec:um}.  We use the simulation framework of
+section~\ref{sec:sim}.  We define the initialization function $I_\Pi$ to be
+the initialization function of $\Pi$, as before, and the corresponding
+world~$W_\Pi(\iota, \sigma, \tau, \mu)$ is a fairly straightforward mapping
+of the adversary's possible actions to the simulation model:
+\begin{itemize}
+\item The invocation $\cookie{new-session}$ with $\mu = (i, j, s)$ creates a
+  new session on party~$P_i$, with partner~$P_j$ and session-id~$s$.  The
+  reply $\rho = (\delta, m)$ is a \emph{decision} $\delta \in
+  \{\cookie{continue}, \cookie{abort}, \cookie{complete}\}$ and an output
+  message $m \in \Bin^* \cup \{\bot\}$.  If $m \ne \bot$ then $m$ is a
+  message to be sent to the matching session (if any).
+\item The invocation $\cookie{deliver}$ with $\mu = (i, j, s, m)$ delivers
+  message $m$ to the session $S = (P_i, P_j, s)$.  The response $\rho$ is as
+  for $\cookie{new-session}$ invocations.
+\item The invocation $\cookie{reveal-session-state}$ with $\mu = (i, j, s)$
+  reveals to the adversary the state of the running session $S = (P_i, P_j,
+  s)$.  The response $\rho$ is the session's state if $S$ is indeed a running
+  session, or $\bot$ otherwise.
+\item The invocation $\cookie{reveal-session-key}$ with $\mu = (i, j, s)$
+  reveals to the adversary the session-key of the completed session~$S =
+  (P_i, P_j, s)$.  The response $\rho$ is the session key~$K$ if the session
+  is indeed complete, or $\bot$ otherwise.
+\end{itemize}
+There are no invocations corresponding to the adversary actions of corrupting
+parties (since deniability against an corrupting adversary is impossible, as
+discussed earlier), or session expiry or challenging (since they are useless
+in this context).
+
+We measure the deniability of a protocol~$\Pi$, using a given simulator~$S$,
+by the insecurity function $\InSec{sim}(W_\Pi, I_\Pi, S; t_D, t_A,
+\mathcal{Q}_D, \mathcal{Q}_A, \mathcal{R}, \mathcal{U})$ of
+definition~\ref{def:sim}.  The interaction bounds $\mathcal{R} = (q_S, q_M)$
+we place on the adversary are on the number ($q_S$) of \cookie{new-session}
+and ($q_M$) \cookie{deliver} invocations it makes.
+
+We shall (informally) say that a protocol~$\Pi$ is deniable if there is a
+simulator~$S_\Pi$ for which the insecurity function is small for appropriate
+resource bounds on the adversary and distinguisher.
+
+\subsubsection{The current protocol}
+As it stands, $\Wkx$ isn't deniable, according to our definition, for
+arbitrary auxiliary inputs.  Let's see why.
+
+Suppose that Bob is an informant for the secret police, and wants to convince
+a judge that Alice is involved in subversive activities in cyberspace.
+Unfortunately, Bob's job is difficult, because of the strong zero-knowledge
+nature of the Wrestlers identification protocol.  However, Bob can work with
+the judge to bring him the evidence necessary to convict Alice.  Here's how.
+
+Alice's public key is $A$, and Bob's public key is $B$.  The judge chooses
+some session-id $s$, and $r \inr \gf{q}$.  He computes $R = r P$ and $c =
+r \xor H_I(B, s, R, r A)$, and gives Bob the triple $(s, R, c)$, keeping $r$
+secret.  Bob can now persuade Alice to enter into a key-exchange with him,
+with session-id $s$.  He uses $(R, c)$ as his challenge message.  When Alice
+sends back her response $(R', \chi)$ (because Bob's challenge is correctly
+formed), Bob aborts and shows $(R', \chi)$ to the judge.  The judge knows $r$
+and can therefore decrypt $\chi$ and check the response.  If it's wrong, then
+Bob was cheating and gets demoted -- he can't get the right answer by himself
+because that would require him to impersonate Alice.  If it's right, Alice is
+really a subversive element and `disappears' in the night.
+
+We shall show in theorem~\ref{thm:denial} below that this is basically the
+only attack against the deniability of the protocol.  However, we can do
+better.
+
+\subsubsection{Fixing deniability}
+We can fix the protocol to remove even the attack discussed above.  The
+change is simple: we feed \emph{both} parties' challenges to the hash
+function~$H_I$ rather than just the sender's.  We use a five-argument hash
+function (random oracle) $H_I\colon G^2 \times \Bin^{\ell_S} \times G^2 \to
+\Bin^{\ell_I}$.  We introduce a new message pass at the beginning of the
+protocol: each session simply sends its challenge point $R = r P$ in the
+clear as a `pre-challenge'.  The actual challenge is $R$ and $c = r \xor
+H_I(X, R', s, R, c)$, where $R'$ is the challenge of the matching session.
+
+By breaking symmetry, we can reduce the communication complexity of this
+variant to four messages.  As before, we analyse the symmetrical version.
+The extra flow might seem a high price to pay, but we shall see that it has
+additional benefits beyond deniability.
+
+A summary of the new protocol is shown in figure~\ref{fig:wdkx}, and the
+formal description is shown in figure~\ref{fig:wdkx-formal}.
+
+\begin{figure}
+  \begin{description}
+  \item[Setup] Group $G = \langle P \rangle$; $\#G = q$ is prime.
+    $H_I(\cdot, \cdot, \cdot, \cdot, \cdot)$ and $H_K(cdot)$ are secure
+    hashes.  $\E = (\kappa, E, D)$ is an IND-CCA2 symmetric encryption
+    scheme.
+  \item[Parties] $U_i$ for $0 \le i < n$.
+  \item[Private keys] $x_i \inr \gf{q}$.
+  \item[Public keys] $X_i = x_i P$.
+  \end{description}
+
+  \begin{protocol}
+    $r_i \getsr I$; $R_i \gets r_i P$; &
+    $r_j \getsr I$; $R_j \gets r_j P$; \\
+    \send{->}{R_i}
+    \send{<-}{R_j}
+    $c_i \gets r_i \xor H_I(R_j, X_i, s, R_i, r_i X_j)$; &
+    $c_j \gets r_j \xor H_I(R_i, X_j, s, R_j, r_j X_i)$; \\
+    \send{->}{(R_i, c_i)}
+    \send{<-}{(R_j, c_j)}
+    Check $R_j = \bigl(c_j \xor H_I(x_i R_j)\bigr) P$; &
+    Check $R_i = \bigl(c_i \xor H_I(x_j R_i)\bigr) P$; \\
+    $Z \gets r_i R_j$; $(K_0, K_1) \gets H_K(Z)$; &
+    $Z \gets r_j R_i$; $(K_0, K_1) \gets H_K(Z)$; \\
+    $\chi_i \gets E_{K_0}(x_i R_j)$; &
+    $\chi_j \gets E_{K_0}(x_j R_i)$; \\
+    \send{->}{(R_i, \chi_i)}
+    \send{<-}{(R_j, \chi_j)}
+    Check $D_{K_0}(\chi_j) = r_i X_j$; &
+    Check $D_{K_0}(\chi_i) = r_j X_i$; \\
+    Shared key is $K_1$. & Shared key is $K_1$.
+  \end{protocol}
+
+  \caption{Summary of the Deniable Wrestlers Key Exchange protocol, $\Wdkx$}
+  \label{fig:wdkx}
+\end{figure}
+
+\begin{figure}
   \begin{program}
-    Adversary $A'^{E(\cdot)}$: \+ \\
-      $b \gets A^{\Xid{E}{steal}(\cdot)}$; \\
-      \RETURN $b$;
+    Function $\id{init}(n)$: \+ \\
+      \FOR $i \in \Nupto{n}$ \DO \\ \ind
+        $x \getsr \gf{q}$; \\
+        $\mathbf{i}[i] \gets x$; \\
+        $\mathbf{p}[i] \gets x P$; \- \\
+      \RETURN $(\mathbf{p}, \mathbf{i})$;
+    \- \\[\medskipamount]
+    Function $\id{new-session}^{H_I(\cdot, \cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
+      (\mathbf{p}, x, i, j, s)$: \+ \\
+      $X \gets \mathbf{p}[i]$;
+      $X' \gets \mathbf{p}[j]$;
+      $C \gets \emptyset$; \\
+      $r \getsr \gf{q}$;
+      $R \gets r P$;
+      $Y \gets r X'$; \\
+      \SEND $(\cookie{pre-challange}, R)$;
     \- \\[\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)))$;
+    Function $\id{message}^{H_I(\cdot, \cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
+      (\tau, \mu)$: \+ \\
+      \IF $\tau = \cookie{pre-challenge}$ \THEN
+        $\id{msg-pre-challenge}(\mu)$; \\
+      \ELSE \IF $\tau = \cookie{challenge}$ \THEN
+        $\id{msg-challenge}(\mu)$; \\
+      \ELSE \IF $\tau = \cookie{response}$ \THEN $\id{msg-response}(\mu)$;
     \next
-    Function $\id{pad}(x)$: \+ \\
-      $t \gets |x| \bmod \ell$; \\
-      \RETURN $x \cat 0^{\ell-t}$;
+    Function $\id{msg-pre-challenge}(\mu)$: \+ \\
+      $R' \gets \mu$; \\
+      $h \gets H_I(R', X, s, R, c)$; \\
+      $c \gets r \xor h$; \\
+      \SEND $(\id{msg-challenge}, R, c)$;
+    \- \\[\medskipamount]
+    Function $\id{msg-challenge}(\mu)$: \+ \\
+      $(R', c') \gets \mu$; \\
+      $Y' \gets x R'$; \\
+      $h' \gets H_I(R, X', s, R', Y')$; \\
+      $r' \gets c' \xor h'$; \\
+      \IF $R' \ne r' P$ \THEN \RETURN; \\
+      $C \gets C \cup \{R\}$; \\
+      $Z \gets r R'$; \\
+      $(K_0, K_1) \gets H_K(Z)$; \\
+      $\chi \gets E_{K_0}(Y')$; \\
+      \SEND $(\cookie{response}, R, \chi)$;
     \- \\[\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$;
+    Function $\id{msg-response}(\mu)$: \+ \\
+      $(R', \chi') \gets \mu$; \\
+      \IF $R' \notin C$ \THEN \RETURN; \\
+      $Z \gets r R'$; \\
+      $(K_0, K_1) \gets H_K(Z)$; \\
+      $Y' \gets D_{K_0}(\chi')$; \\
+      \IF $Y' \ne Y$ \THEN \RETURN; \\
+      \OUTPUT $K_1$;
+      \STOP;
   \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}
-
-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.
-
-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:
+  \caption{Deniable key-exchange: formalization of $\Wdkx$}
+  \label{fig:wdkx-formal}
+\end{figure}
+
+The security of this variant is given by the following theorem, whose proof
+is \ifshort given in the full version of this paper\else in
+appendix~\ref{sec:sk2-proof}\fi.
+\begin{theorem}[SK-security of $\Wdkx$]
+  \label{thm:sk2}
+  Let $G$ be a cyclic group.  Let $\E = (\kappa, E, D)$ be a symmetric
+  encryption scheme.  Then
+  \[ \InSec{sk}(\Wdkx^{G, \E}; t, n, q_S, q_M, q_I, q_K) =
+       \InSec{sk}(\Wkx^{G, \E}; t, n, q_S, q_M, q_I, q_K)
+  \]
+\end{theorem}
+
+\subsubsection{Deniability of the Wrestlers protocols}
+In order to quantify the level of deniability our protocols provide, we shall
+impose a limit on the auxiliary input to the adversary.  In particular, we
+shall use $\mathcal{U}$ of definition~\ref{def:sim} to count the number of
+\emph{challenges} in the auxiliary input.  That is, $\mathcal{U} = n_C$ is
+the number of tuples $(i, j, s, R', R, c)$ for which there is an $r$ such
+that $R = r P$ and $c = r \xor H_I(R', X_j, s, R, r X_i)$ (or without the
+$R'$ for $\Wkx$).
+
+With this restriction in place, we can state the following theorem about the
+deniability of our protocols.
+\begin{theorem}[Deniability of $\Wkx$ and $\Wdkx$]
+  \label{thm:denial}
+  There exist simulators $S_\Wkx$ and $\Wdkx$ such that
+  \[ \InSec{sim}(W_{\Wkx^{G, \E}}, I_{\Wkx^{G, \E}}, S_{\Wkx^{G, \E}};
+                 t_D, t_A, \mathcal{Q}_D, \mathcal{Q}_A, (q_S, q_M), 0) \le
+       \frac{q_M}{2^{\ell_I}}
+  \]
+  and
+  \iffancystyle\[\else\begin{spliteqn*}\fi
+    \InSec{sim}(W_{\Wdkx^{G, \E}}, I_{\Wdkx^{G, \E}}, S_{\Wdkx^{G, \E}};
+                t_D, t_A, \mathcal{Q}_D, \mathcal{Q}_A, (q_S, q_M), n_C) \le
+    \iffancystyle\else\\\fi
+       \frac{n_C q_S}{\#G} +
+       \frac{q_M}{2^{\ell_I}}.
+  \iffancystyle\]\else\end{spliteqn*}\fi
+  The running time of the simulators is $O(t_A) + O(\mathcal{Q}_A q_M)$.
+\end{theorem}
+\begin{longproof}{The proof of this theorem can be found in the full version
+    of this paper.}
+  The simulators $S_\Wkx$ and $S_\Wdkx$ are very similar.  We describe both
+  here.  Both are fake-world simulators, working as follows.
+  \begin{enumerate}
+  \item Initially, it constructs simulated parties $P_i$, for $0 \le i < n$,
+    giving each the public key $X_i$ from the common input.
+  \item Suppose the adversary requests creation of a new session $S = (P_i,
+    P_j, s)$.  Then the simulator creates a new session, including a random
+    value $r_S \inr \gf{q}$, and computes $R_S = r_S P$, and $Y_S = r_S
+    X_j$.  For $\Wdkx$, it sends the message $(\cookie{pre-challenge}, R_S)$;
+    for $\Wkx$, it additionally computes $h = H_I(X_i, s, R_S, Y_S)$ and
+    sends $(\cookie{challenge}, R_S, r_S \xor h)$.
+  \item Suppose, for $\Wdkx$, the adversary sends a message
+    $(\cookie{pre-challenge}, R')$ to a session~$S = (P_i, P_j, s)$.  The
+    simulator computes $h = H_I(R', X_i, s, R_S, Y_S)$, and sends
+    $(\cookie{challenge}, R_S, r_S \xor h)$.
+  \item Suppose the adversary sends a message $(\cookie{challenge}, R', c')$
+    to session $S = (P_i, P_j, s)$.  The simulator doesn't know $x_i$.
+    \begin{enumerate}
+    \item If $R' = R_T$ for some other simulated session $T$, then the
+      simulator knows $r_T$ such that $R_T = r_T P$.  Let $Y' = r_T X_i$.
+      The simulator computes $h = H_I(X_j, s, R', Y')$ (resp.\ $h = H_I(R_S,
+      X_j, s, R', Y')$) for $\Wkx$ (resp.\ $\Wdkx$) and checks that $r_T = c'
+      \xor h$.  If not, the simulator discards the message.  Otherwise, it
+      computes $(K_0, K_1) = H_K(r_S R')$, and sends the message
+      $(\cookie{response}, R, E_{K_0}(Y'))$.
+    \item \label{en:simextract} Otherwise the simulator runs the extractor
+      $T_\Wident$ on the adversary's history of queries $H_I(X_j, s, R',
+      \cdot)$ (resp.\ $H_I(R_S, X_j, s, R', \cdot)$) for $\Wkx$ (resp.\
+      $\Wdkx$).  The extractor returns $(r', Y')$.  If $Y' = \bot$ then the
+      simulator ignores the message.  Otherwise, the simulator computes
+      $(K_0, K_1) = H_K(r R')$ and sends back $(\cookie{response}, R,
+      E_{K_0}(Y'))$.
+    \end{enumerate}
+  \item Suppose the adversary sends a message $(\cookie{response}, R', \chi)$
+    to session $S = (P_i, P_j, s)$.  The simulator computes $(K_0, K_1) =
+    H_K(r_S R')$, and decrypts $Y' = D_{K_0}(\chi)$.  If $Y' \ne Y_S$ then
+    the simulator discards the message.  Otherwise, it makes the simulated
+    session complete, and outputs key $K_1$.
+  \item Finally, if the adversary reveals a session's state, the simulator
+    reveals $r_S$ as required; if the adversary reveals a session-key, the
+    simulator reveals the $K_1$ it output.
+  \end{enumerate}
+  The only point where the simulation fails to be perfect is in
+  \ref{en:simextract}.  Let $R'$ and $c'$ be the values from an incoming
+  challenge message to session $S = (P_i, P_j, s)$.  Let $r'$ be such that
+  $R' = r' P$ and let $Y' = r' X_i$.  If a random-oracle query $H_I(X_j, s,
+  R', Y')$ (or $H_I(R_S, X_j, s, R', Y')$ for $\Wdkx$) has been issued, then
+  there are a number of possibilities.  Let $h'$ be the result of this query.
+  \begin{itemize}
+  \item The adversary made this query.  Then the extractor will find it and
+    return $Y'$ if $c' = h' \xor r'$, or $\bot$ otherwise.
+  \item Some simulated session $U = (P_{i'}, P_{j'}, s')$ made this query.
+    But simulated sessions only make $H_I$-queries when constructing
+    challenges, so $R' = R_U$ for some session~$U$.  But the simulator does
+    something different in that case.
+  \item In $\Wdkx$, the quadruple $(s, R_S, R', c')$ came from the
+    adversary's auxiliary input.  In this case the simulator must fail.  But
+    $R_S = r_S P$, and $r_S$ was chosen uniformly at random.  If there are at
+    most $n_C$ challenge sets in the auxiliary input then this happens with
+    probability at most $n_C/\#G$ for any given session.
+  \end{itemize}
+  We conclude that the simulator fails with probability
+  \[ \frac{q_M}{2^{\ell_I}} + \frac{q_S n_C}{\#G}. \]
+  (Note that we only consider $n_C = 0$ for $\Wkx$.)  No adversary can
+  distinguish the simulator from a real interaction unless the simulator
+  fails, and the simulator is a fake-world simulator.  We therefore apply
+  proposition~\ref{prop:fakesim}; the theorem follows.
+\end{longproof}
+
+\ifshort\else
+\subsection{Practical issues}
+\label{sec:practice}
+
+\subsubsection{Denial of service from spoofers}
+The adversary we considered in~\ref{sec:um} is very powerful.  Proving
+security against such a powerful adversary is good and useful.  However,
+there are other useful security properties we might like against weaker
+adversaries.
+
+Eavesdropping on the Internet is actually nontrivial.  One needs control of
+one of the intermediate routers between two communicating parties.  (There
+are tricks one can play involving subversion of DNS servers, but this is also
+nontrivial.)  However, injecting packets with bogus source addresses is very
+easy.
+
+Layering the protocol over TCP \cite{rfc793} ameliorates this problem because
+an adversary needs to guess or eavesdrop in order to obtain the correct
+sequence numbers for a spoofed packet; but the Wrestlers protocol is
+sufficiently simple that we'd like to be able to run it over UDP
+\cite{rfc768}, for which spoofing is trivial.
+
+Therefore, it's possible for anyone on the 'net to send Alice a spurious
+challenge message $(R, c)$.  She will then compute $Y = a R$, recover $r' = c
+\xor H_I(\ldots, R, Y)$ check that $R = r' P$ and so on.  That's at least two
+scalar multiplications to respond to a spoofed packet, and even with very
+efficient group operations, coping with this kind of simple denial-of-service
+attack might be difficult.
+
+A straightforward solution is to use the Deniable variant of the protocol,
+and require a challenge to quote its matching session's challenge $R'$ in its
+challenge.  That is, upon receiving a $(\cookie{pre-challenge}, R')$, the
+session sends $(\cookie{challenge}, R', R, c)$.  Alice then rejects any
+\emph{incoming} challenge message which doesn't quote her current challenge
+value.  Now only eavesdroppers can force her to perform expensive
+computations.
+
+Indeed, one need not quote the entire challenge $R'$: it suffices to send
+some short hard-to-guess hash of it, maybe just the bottom 128 bits or so.
+
+This can't reduce security.  Consider any adversary attacking this protocol
+variant.  We can construct an adversary which attacks the original protocol
+just as efficiently.  The new adversary attaches fake $R'$ values to
+challenges output by other parties, and strips them off on delivery,
+discarding messages with incorrect $R'$ values.
+
+\subsubsection{Key confirmation}
+Consider an application which uses the Wrestlers protocol to re-exchange keys
+periodically.  The application can be willing to \emph{receive} incoming
+messages using the new key as soon as the key exchange completes
+successfully; however, it should refrain from \emph{sending} messages under
+the new key until it knows that its partner has also completed.  The partner
+may not have received the final response message, and therefore be unwilling
+to accept a new key; it will therefore (presumably) reject incoming messages
+under this new key.
+
+While key confirmation is unnecessary for \emph{security}, it has
+\emph{practical} value, since it solves the above problem.  If the
+application sends a \cookie{switch} message when it `completes', it can
+signal its partner that it is indeed ready to accept messages under the new
+key.  Our implementation sends $(\cookie{switch-rq}, E_{K_0}(H_S(0, R, R')))$
+as its switch message; the exact contents aren't important.  Our
+retransmission policy (below) makes use of an additional message
+\cookie{switch-ok}, which can be defined similarly.
+
+It's not hard to show that this doesn't adversely affect the security of the
+protocol, since the encrypted message is computed only from public values.
+In the security proof, we modify the generation of \cookie{response}
+messages, so that the plaintexts are a constant string rather than the true
+responses, guaranteeing that the messages give no information about the
+actual response.  To show this is unlikely to matter, we present an adversary
+attacking the encryption scheme by encrypting either genuine responses or
+fake constant strings.  Since the adversary can't distinguish which is being
+encrypted (by the definition of IND-CCA security,
+definition~\ref{def:ind-cca}), the change goes unnoticed.  In order to allow
+incorporate our switch messages, we need only modify this adversary, to
+implement the modified protocol.  This is certainly possible, since the
+messages contain (hashes of) public values.  We omit the details.
+
+However, while the extra message doesn't affect the security of our protocol,
+it would be annoying if an adversary could forge the switch request message,
+since this would be a denial of service.  In the strong adversarial model,
+this doesn't matter, since the adversary can deny service anyway, but it's a
+concern against less powerful adversaries.  Most IND-CCA symmetric encryption
+schemes also provide integrity of plaintexts \cite{Bellare:2000:AER} (e.g.,
+the encrypt-then-MAC generic composition approach \cite{Bellare:2000:AER,%
+Krawczyk:2001:OEA}, and the authenticated-encryption modes of
+\cite{Rogaway:2003:OBC,Bellare:2004:EAX,McGrew:2004:SPG}), so this isn't a
+great imposition.
+
+\subsubsection{Optimization and piggybacking}
+We can optimize the number of messages sent by combining them.  Here's one
+possible collection of combined messages:
+\begin{description}
+\item [\cookie{pre-challenge}] $R$
+\item [\cookie{challenge}] $R'$, $R$, $c = H_I(R', X, s, R, c) \xor r$
+\item [\cookie{response}] $R'$, $R$, $c$, $E_{K_0}(x R')$
+\item [\cookie{switch}] $R'$, $E_{K_0}(x R', H_S(0, R, R'))$
+\item [\cookie{switch-ok}] $R'$, $E_{K_0}(H_S(1, R, R'))$
+\end{description}
+The combination is safe:
 \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}$.
+\item the \cookie{switch} and \cookie{switch-ok} messages are safe by the
+  argument above; and
+\item the other recombinations can be performed and undone in a `black box'
+  way, by an appropriately defined SK-security adversary.
 \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
+
+\subsubsection{Unreliable transports}
+The Internet UDP \cite{rfc768} is a simple, unreliable protocol for
+transmitting datagrams.  However, it's very efficient, and rather attractive
+as a transport for datagram-based applications such as virtual private
+networks (VPNs).  Since UDP is a best-effort rather than a reliable
+transport, it can occasionally drop packets.  Therefore it is necessary for a
+UDP application to be able to retransmit messages which appear to have been
+lost.
+
+We recommend the following simple retransmission policy for running the
+Wrestlers protocol over UDP.
+\begin{itemize}
+\item Initially, send out the \cookie{pre-challenge} message every minute.
+\item On receipt of a \cookie{pre-challenge} message, send the corresponding
+  full \cookie{challenge}, but don't retain any state.
+\item On receipt of a (valid) \cookie{challenge}, record the challenge value
+  $R'$ in a table, together with $K = (K_0, K_1)$ and the response $Y' = x
+  R'$.  If the table is full, overwrite an existing entry at random.  Send
+  the corresponding \cookie{response} message, and retransmit it every ten
+  seconds or so.
+\item On receipt of a (valid) \cookie{response}, discard any other
+  challenges, and stop sending \cookie{pre-challenge} and \cookie{response}
+  retransmits.  At this point, the basic protocol described above would
+  \emph{accept}, so the key $K_1$ is known to be good.  Send the
+  \cookie{switch} message, including its response to the (now known-good)
+  sender's challenge.
+\item On receipt of a (valid) \cookie{switch}, send back a \cookie{switch-ok}
+  message and stop retransmissions.  It is now safe to start sending messages
+  under $K_1$.
+\item On receipt of a (valid) \cookie{switch-ok}, stop retransmissions.  It
+  is now safe to start sending messages under $K_1$.
+\end{itemize}
+
+\subsubsection{Key reuse}
+Suppose our symmetric encryption scheme $\E$ is not only IND-CCA secure
+(definition~\ref{def:ind-cca}) but also provides integrity of plaintexts
+\cite{Bellare:2000:AER} (or, alternatively, is an AEAD scheme
+\cite{Rogaway:2002:AEA}.  Then we can use it to construct a secure channel,
+by including message type and sequence number fields in the plaintexts, along
+with the message body.  If we do this, we can actually get away with just the
+one key $K = H_K(Z)$ rather than both $K_0$ and $K_1$.
+
+To do this, it is essential that the plaintext messages (or additional data)
+clearly distinguish between the messages sent as part of the key-exchange
+protocol and messages sent over the `secure channel'.  Otherwise, there is a
+protocol-interference attack: an adversary can replay key-exchange
+ciphertexts to insert the corresponding plaintexts into the channel.
+
+We offer a sketch proof of this claim in appendix~\ref{sec:sc-proof}.
+\fi
+
+%%%--------------------------------------------------------------------------
+
+\section{Conclusions}
+\label{sec:conc}
+
+We have presented new protocols for identification and authenticated
+key-exchange, and proven their security.  We have shown them to be efficient
+and simple.  We have also shown that our key-exchange protocol is deniable.
+Finally, we have shown how to modify the key-exchange protocol for practical
+use, and proven that this modification is still secure.
+
+%%%--------------------------------------------------------------------------
+
+\section{Acknowledgements}
+
+The Wrestlers Protocol is named after the Wrestlers pub in Cambridge where
+Clive Jones and I worked out the initial design.
+
+%%%--------------------------------------------------------------------------
+
+\iffalse
+\bibliography{%
+  mdw-crypto,%
+  eprint,%
+  focs1990,stoc1990,tissec,jacm,%
+  lncs1997a,lncs1997b,lncs1998a,lncs2001a,%
+  cryptography1990,cryptography2000,cryptography2010,cryptography,%
+  rfc,std}
+\else
+\bibliography{wrestlers}
+\fi
+
+%%%--------------------------------------------------------------------------
+
+\ifshort\def\next{\end{document}}\expandafter\next\fi
+\appendix
+\section{Proofs}
+
+\subsection{Proof of theorem~\ref{thm:sk}}
+\label{sec:sk-proof}
+
+Before we embark on the proof proper, let us settle on some notation.  Let
+$P_i$ be a party.  Then we write $x_i$ for $P_i$'s private key and $X_i = x_i
+P$ is $P_i$'s public key.  Let $S = (P_i, P_j, s)$ be a session.  We write
+$r_S$ for the random value chosen at the start of the session, and $R_S$,
+$c_S$ etc.\ are the corresponding derived values in that session.
+
+The proof uses a sequence of games.  For each game~$\G{i}$, let $V_i$ be the
+event that some pair of unexposed, matching sessions both complete but output
+different keys, and let $W_i$ be the event that the adversary's final output
+equals the game's hidden bit~$b^*$.  To save on repetition, let us write
+\[ \diff{i}{j} = \max(|\Pr[V_i] - \Pr[V_j]|, |\Pr[W_i] - \Pr[W_j]|). \]
+Obviously,
+\[ \diff{i}{j} \le \sum_{i\le k<j} \diff{k}{k + 1}. \]
+
+Here's a quick overview of the games we use.
+\begin{itemize}
+\item $\G0$ is the original SK-security game.
+\item In $\G1$, we abort the game unless all parties' public keys are
+  distinct.  Since keys are generated at random, parties are unlikely to be
+  given the same key by accident.
+\item In $\G2$, we change the way sessions respond to challenge messages, by
+  using the extractor to fake up answers to most challenges.  Since the
+  extractor is good, the adversary is unlikely to notice.
+\item In $\G3$, we abort the game if the adversary ever queries $H_K(\cdot)$
+  on the Diffie-Hellman secret $r_S r_T P$ shared between two unexposed
+  matching sessions.  We show that this is unlikely to happen if the
+  Diffie-Hellman problem is hard.
+\item In $\G4$, we abort the game if any unexposed session \emph{accepts} a
+  response message which wasn't sent by a matching session.
+\end{itemize}
+Finally, we show that the adversary has no advantage in $\G4$.  The theorem
+follows.
+
+For ease of comprehension, we postpone the detailed proofs of some of the
+steps until after we conclude the main proof.
+
+Let $A$ be a given adversary which runs in time~$t$, creates at most~$q_S$
+sessions, delivers at most~$q_M$ messages, and makes at most~$q_I$ queries to
+its $H_I(\cdot, \cdot, \cdot, \cdot)$ oracle and at most~$q_K$ queries to its
+$H_K(\cdot)$ oracle.  Let $\G0$ be the original SK-security game of
+definition~\ref{def:sk}, played with adversary~$A$.
+
+Game~$\G1$ is the same as game~$\G0$ except, if the initialization function
+reports two parties as having the same public key (i.e., we have $X_i \ne
+X_j$ where $0 \le i < j < n$), we stop the game immediately and without
+crediting the adversary with a win.  This only happens when the corresponding
+private keys are equal, i.e., $x_i = x_j$, and since the initialization
+function chooses private keys uniformly at random, this happens with
+probability at most $\binom{n}{2}/\#G$.  Since if this doesn't happen, the
+game is identical to $\G0$, we can apply lemma~\ref{lem:shoup}, and 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})}
+  \label{eq:sk-g0-g1}
+  \diff{0}{1} \le \frac{1}{\#G} \binom{n}{2} = \frac{n (n - 1)}{2 \#G}.
 \end{equation}
-where $t_P$ expresses the overhead of doing the XORs and other care and
-feeding of the CBC adversary; whence
+In game~$\G1$ and onwards, we can assume that public keys for distinct
+parties are themselves distinct.  Note that the game now takes at most
+$O(q_I)$ times longer to process each message delivered by the adversary.
+This is where the $O(q_I q_M)$ term comes from in the theorem statement.
+
+Game~$\G2$ is the same as game~$\G1$, except that we change the way that we
+make parties respond to \cookie{challenge} messages $(\cookie{challenge}, R,
+c)$.  Specifically, suppose that $S = (P_i, P_j, s)$ is a session.
+\begin{itemize}
+\item Suppose $T = (P_j, P_i, s)$ is the matching session of $S$.  The game
+  proceeds as before if $(R, c) = (R_T, c_T)$ is the challenge issued by $T$.
+\item Otherwise, we run the extractor $T_\Wident$ on the adversary's history
+  so far of oracle queries $H_I(X_i, s, R, \cdot)$ to determine a pair $(r,
+  Y)$.  If $r = \bot$ then we discard the message.  Otherwise, we add $R$ to
+  the list~$C$, and return a fake response to the adversary by computing $K =
+  H_K(r R_S)$ and handing the adversary $(\cookie{response}, R_S, E_K(Y))$.
+\end{itemize}
+The following lemma shows how this affects the adversary's probabilities of
+winning.
+\begin{lemma}
+  \label{lem:sk-g1-g2}
+  \begin{equation}
+    \label{eq:sk-g1-g2}
+    \diff{1}{2} \le \frac{q_M}{2^{\ell_I}}.
+  \end{equation}
+\end{lemma}
+
+Let us say that a session $S = (P_i, P_j, s)$ is \emph{ripe} if
+\begin{itemize}
+\item there is a matching session $T = (P_j, P_i, s)$, and
+\item $S$ is unexposed.
+\end{itemize}
+Suppose that $S$ is a ripe session, and that it has a matching session~$T$:
+let $Z_S = Z_T = r_S r_T P$.
+
+Game~$\G3$ is the same as $\G2$, except that the game is immediately aborted
+if ever the adversary queries its random oracle $H_K(\cdot)$ at a value $Z_S$
+for any ripe session~$S$.  The following lemma shows how this affects the
+adversary's probabilities of winning.
+\begin{lemma}
+  \label{lem:sk-g2-g3}
+  For some $t'$ within the bounds given in the theorem statement we have
+  \begin{equation}
+    \label{eq:sk-g2-g3}
+    \diff{2}{3} \le q_S \InSec{mcdh}(G; t', q_K).
+  \end{equation}
+\end{lemma}
+
+Game~$\G4$ is the same as $\G3$ except that the game is immediately aborted
+if ever the adversary sends a response message to a ripe session~$S$ which
+wasn't output by its matching session as a response to $S$'s challenge, with
+the result that $S$ completes.
+
+Let's make this more precise.  Let $U$ and $V$ be a pair of matching
+sessions.  Let $C_U = (\cookie{challenge}, R_U, c_U$ be the challenge message
+sent by $U$.  Let $M_T$ be the set of messages which $T$ has sent upon
+delivery of $C_U$.  Then, in $\G4$, we abort the game if, for any pair $S$
+and~$T$ of matching, unexposed sessions, $S$ has completed as a result of
+being sent a message $\mu \notin M_T$.  We have the following lemma.
+\begin{lemma}
+  \label{lem:sk-g3-g4}
+  For a $t'$ within the stated bounds, we have
+  \begin{equation}
+    \label{eq:sk-g3-g4}
+    \diff{3}{4} \le q_S \bigl( \InSec{ind-cca}(\E; t', q_M, q_M) +
+                         n \cdot \InSec{mcdh}(G; t', q_M + q_I) \bigr)
+  \end{equation}
+\end{lemma}
+
+Finally, let us consider the state we're in with $\G4$.
+\begin{itemize}
+\item No ripe session completes except as a result the adversary faithfully
+  delivering messages between it and its matching session.
+\item The adversary never queries $Z_S$ for any ripe session~$S$.  If we set
+  $K_S = (K_{S, 0}, K_{S, 1}) = H_K(Z_S)$, then $K_{S, 1}$ is the key output
+  by $S$ when it completes.
+\item If $S$ and $T$ are matching ripe sessions, then $K_S = K_T$, since $Z_S
+  = r_S R_T = r_T R_S = Z_T$.
+\item For any ripe session~$S$, $K_{S, 1}$ is uniformly distributed in
+  $\Bin^\kappa$ and independent of the adversary's view.
+\item If $S = (P_i, P_j, s)$ and $T = (P_j, P_i, s)$ are matching ripe
+  sessions, then $Z_S$ depends only $r_S$ and $r_T$.  Hence, once $S$ and~$T$
+  complete, and erase their states, $Z_S$ is independent of everything except
+  the messages sent between the two sessions.  In particular, $Z_S$ is
+  independent of the long-term secrets $x_i$ and~$x_j$, so if either player
+  is later corrupted, the key $K_{S, 1}$ remains independent of the
+  adversary's view.
+\item Hence, the keys output by unexposed sessions are indistinguishable from
+  freshly-generated random strings, and remain so indefinitely.
+\end{itemize}
+We conclude that, for any adversary $A$,
 \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}}
+  \label{eq:sk-g4}
+  \Pr[V_4] = 0 \qquad \text{and} \qquad \Pr[W_4] = \frac{1}{2}.
 \end{equation}
-as required.
-\qed
+Putting equations~\ref{eq:sk-g0-g1}--\ref{eq:sk-g4} together, we find
+\begingroup \splitright=4em minus 4em
+\begin{spliteqn}
+  \Adv{sk}{\Wident^{G, \E}}(A) \le
+     2 q_S \bigl(\InSec{ind-cca}(\E; t', q_M, q_M) + {} \\
+     \InSec{mcdh}(G; t', q_K) +
+     n \,\InSec{mcdh}(G; t', q_M + q_I) \bigr) + {}
+     \frac{n (n - 1)}{\#G} +
+     \frac{2 q_M}{2^{\ell_I}}.
+\end{spliteqn} \endgroup
+The theorem follows, since $A$ was chosen arbitrarily.
+
+
+\begin{proof}[Proof of lemma~\ref{lem:sk-g1-g2}]
+  The two games $\G1$ and~$\G2$ differ only in whether they accept or reject
+  particular challenge messages $(\cookie{challenge}, R, c)$.
+
+  We claim firstly that no message is \emph{accepted} by $\G2$ which would
+  have been rejected by $\G1$.  To prove the claim, it is sufficient to note
+  that the extractor's output, if not $\bot$, is always correct, and hence if
+  $\G2$ accepts a message then $\G1$ would have done so too.
+
+  Since $\G2$ also behaves identically when the adversary submits to~$S$ the
+  challenge from the matching session~$T$, we have nothing to prove in this
+  case.  Let $F$ be the event that the adversary submits a message
+  $(\cookie{challenge}, R, c)$ to a session~$S$ which $S$ would have accepted
+  in $\G1$ but would be rejected by the new rule in~$\G2$.  By
+  lemma~\ref{lem:shoup} we have $\diff{1}{2} \le \Pr[F]$.  To prove the
+  current lemma, therefore, we must show that $\Pr[F] \le q_M/2^{\ell_I}$.
+
+  Rather than consider individual challenge messages, we consider
+  \emph{classes} of messages.  We shall refer to a quadruple~$\Cid = (i, j,
+  s, R)$ as a \emph{class-id}, and define some useful functions:
+  \begin{itemize}
+  \item the class's \emph{session} $\Csession(\Cid) = (P_i, P_j, s)$;
+  \item the class's \emph{index} $\Cindex(\Cid)$ is $r \in I$ where $R = r
+    P$, which is well-defined by lemma~\ref{lem:unique-dl};
+  \item the class's \emph{query} $\Cquery(\Cid) = (X_j, s, R, x_i R)$;
+  \item the class's \emph{hash} $\Chash(\Cid) = H_I(\Cquery(\Cid)) = H_I(X_j,
+    s, R, x_i R)$;
+  \item the class's \emph{check-value} $\Ccheck(\Cid) = \Chash(\Cid) \xor
+    \Cindex(\Cid)$;
+  \item the class's \emph{check-set} $\Ccheckset(\Cid)$ is the set of
+    check-values $c$ such that a message $(\cookie{challenge}, R, c)$ was
+    sent to session $S = (P_i, P_j, s)$; and
+  \item the class's \emph{count} $\Ccount(\Cid) = |\Ccheckset(\Cid)|$.
+  \end{itemize}
+
+  Consider any class-id~$\Cid = (i, j, s, R)$.  A natural question which
+  arises is: which participants have issued $\Cid$'s query, i.e., queried
+  $H_I$ at $\Cquery(\Cid)$?
 
-%%%----- That's all, folks --------------------------------------------------
+  We can characterise the $H_I(\cdot, \cdot, \cdot, \cdot)$ queries of a
+  session $U = (P_{i'}, P_{j'}, s')$ as follows:
+  \begin{itemize}
+  \item computing the check-value for the challenge $R_U$ by querying
+    $H_I(X_{i'}, s', R_U, r_U X_{j'})$, and
+  \item checking an incoming challenge~$R'$ by querying $H_I(X_{j'}, s', R',
+    x_{i'} R')$.
+  \end{itemize}
+  The class~$\Cid$'s query $\Cquery(\Cid)$ is $U$'s check-value query if
+  \[ (j, i, s, R) = (i', j', s', R_U) \]
+  i.e., $U$ is the matching session of $\Csession(\Cid)$, and moreover $R =
+  R_U$ is the challenge value issued by $U$.  For any $c \in
+  \Ccheckset(\Cid)$, if $c = \Ccheck(\Cid)$ then $(\cookie{challenge}, R, c)$
+  is precisely the challenge message issued by~$U$ to $\Csession(\Cid)$; the
+  rules for handling this message didn't change.  However, if $c \ne
+  \Ccheck(\Cid)$ then the message would have been rejected in $\G1$, and we
+  have already shown that $\G2$ continues to reject all messages rejected by
+  $\G1$.
+
+  Let us say that a class-id~$\Cid = (i, j, s, R)$ is \emph{bad} if
+  \begin{enumerate}
+  \item the value $R$ is not the challenge issued by $\Csession(\Cid)$'s
+    matching session, and
+  \item the adversary has not issued $\Cid$'s query $\Cquery(\Cid)$,
+    \emph{but}
+  \item $\Ccheck(\Cid) \in \Ccheckset(\Cid)$, so one of the check-values
+    submitted to $S$ was actually correct.
+  \end{enumerate}
+  We claim that our extractor will work perfectly unless some class-id is
+  bad.  Certainly, if $R$ was issued by the matching session, there is
+  nothing to prove; if the adversary has issued the relevant query then the
+  extractor will recover $\Cindex(\Cid)$ just fine; and if $\Ccheck(\Cid)
+  \notin \Ccheckset(\Cid)$ then all messages in the class would have been
+  rejected by $\G1$ anyway.
+
+  Let $B(\Cid)$ be the event that the class~$\Cid$ is bad.  We claim that
+  \[ \Pr[B(\Cid)] \le \frac{\Ccount(\Cid)}{2^{\ell_I}}. \]
+  The present lemma follows, since
+  \[ \diff{1}{2}
+     \le \Pr[F]
+     \le \sum_\Cid \Pr[B(\Cid)]
+     \le \sum_\Cid \frac{\Ccount(\Cid)}{2^{\ell_I}}
+     =   \frac{1}{2^{\ell_I}} \sum_\Cid \Ccount(\Cid)
+     \le \frac{q_M}{2^{\ell_I}}
+  \]
+  as required.
+
+  Now observe that, in $\G2$, sessions don't actually check incoming
+  challenges in this way any more -- instead we run the extractor.  So, to
+  prove the claim, we consider a class~$\Cid$ where properties~1 and~2 above
+  hold.  The correct hash $\Chash(\Cid)$ is then independent of the rest of
+  the game, so the probability that $\Ccheck(\Cid) \in \Ccheckset(\Cid)$ is
+  precisely $\Ccount(\Cid)/2^{\ell_I}$ as required.
+
+  This completes the proof the lemma.
+\end{proof}
+
+\begin{proof}[Proof of lemma~\ref{lem:sk-g2-g3}]
+  Let $F$ be the event that the adversary makes a query $H_K(Z_S)$ for some
+  ripe session~$S$.  Since $\G3$ proceeds exactly as $\G2$ did unless $F_2$
+  occurs, we apply lemma~\ref{lem:shoup}, which tells us that $\diff{2}{3}
+  \le \Pr[F_2]$.  We must therefore bound this probability.
+
+  To do this, we consider a new game~$\G3'$, which is the same as $\G3$,
+  except that, at the start of the game, we choose a random number $k \inr
+  \Nupto{q_S}$.  For $0 \le i < q_S$, let $S_i$ be the $i$th session created
+  by the adversary.  We define $F'$ to be the event that the adversary
+  queries $H_K(Z_{S_k})$ when $S_k$ is ripe.
+
+  The lemma now follows from these two claims.
+
+  \begin{claim}
+    $\Pr[F] \le q_S \Pr[F']$.
+  \end{claim}
+  To see this, for any session~$S$, let $F_S$ be the event that the adversary
+  queries~$H_K(Z_S)$ when $S$ is ripe.  Then
+  \[ \Pr[F] \le \sum_{0\le i<q_S} \Pr[F_{S_i}]. \]
+  Hence,
+  \[ \Pr[F'] = \Pr[F_{S_k}] = \sum_{0\le i<q_S} \Pr[F_{S_i}] \Pr[k = i]
+             = \frac{1}{q_S} \sum_{0\le i<q_S} \Pr[F_{S_i}]
+             \ge \frac{\Pr[F]}{q_S}
+  \]
+  proving the claim.
+
+  \begin{claim}
+    For some $t' = t + O(n) + O(q_S q_M) + O(q_I) + O(q_K)$, we have
+    $\Pr[F'] \le \InSec{mcdh}(G; t', q_K).$
+  \end{claim}
+  To prove this claim, we construct an adversary~$B$ which solves the MCDH
+  problem in~$G$.  The adversary works as follows.
+  \begin{enumerate}
+  \item It is given a pair $(R^*, S^*) = (r^* P, s^* P)$ of group elements;
+    its objective is to make a verification-oracle query $V(Z^*)$ where $Z^*
+    = r^* s^* P$.
+  \item It sets up a simulation of the game~$\G3'$, by running the
+    $\id{init}$ function, and simulating all of the parties.  In particular,
+    it chooses a random~$k \in \Nupto{q_S}$.
+  \item It sets up accurate simulations of the random oracles $H_K(\cdot)$
+    and $H_I(\cdot, \cdot, \cdot, \cdot)$, which choose random outputs for
+    new, fresh inputs.  However, whenever $A$ queries $H_K(\cdot)$ on a group
+    element $Z$, $B$ also queries $V(Z)$.
+  \item It runs $A$ in its simulated game.  It responds to all of $A$'s
+    instructions faithfully, until the $k$th session-creation.
+  \item When creating the $k$th session $S = S_k = (P_i, P_j, s)$, $B$ has
+    party~$P_i$ choose $R^*$ as its challenge, rather than choosing $r_S$ and
+    setting $R_S = r_S P$.  Because it simulates all the parties, $B$ can
+    compute $Y_S = x_j R$, which is still correct.
+  \item If $A$ requests the creation of a matching session $T = (P_j, P_i,
+    s)$ then $B$ has party~$P_j$ choose $S^*$ as its challenge.  Again, $B$
+    computes $Y_T = x_i S^*$.
+  \item If $A$ ever corrupts the parties $P_i$ or $P_j$, or reveals the
+    session state of $S$ or $T$ then $B$ stops the simulation abruptly and
+    halts.
+  \end{enumerate}
+  Adversary $B$'s running time is within the bounds required of $t'$, and $B$
+  makes at most $q_K$ queries to $V(\cdot)$; we therefore have
+  \[ \Pr[F'] \le \Succ{mcdh}{G}(B) \le \InSec{mcdh}(G; t', q_K) \]
+  as required.
+\end{proof}
+
+\begin{proof}[Proof of lemma~\ref{lem:sk-g3-g4}]
+  Let $F_4$ be the event under which we abort the game~$\G4$.  Clearly, if
+  $F$ doesn't occur, games $\G3$ and $\G4$ proceed identically, so we can
+  apply lemma~\ref{lem:shoup} to see that $\diff{3}{4} \le \Pr[F_4]$.
+  Bounding $\Pr[F_4]$, however, is somewhat complicated.  We use a further
+  sequence of games.
+
+  Firstly, let $\G5$ be like $\G4$ with the exception that we choose, at
+  random, an integer~$k \inr \Nupto{q_S}$.  As we did in the proof for
+  lemma~\ref{lem:sk-g3-g4}, let $S_i$ be the $i$th session created by the
+  adversary.  For each session~$S_i$, let $T_i$ be its matching session, if
+  there is one.  We define $F_5$ to be the event that
+  \begin{itemize}
+  \item $S_k$ completes immediately following delivery of a message $\mu
+    \notin M_{T_k}$, and
+  \item $S_k$ was ripe at this point.
+  \end{itemize}
+  For games~$\G{i}$, for $i > 5$, we define the event $F_i$ to be the event
+  corresponding to $F_5$ in $\G{i}$.  Note that if $S_k$ \emph{is} sent a
+  message in $M_{T_k}$ then $S_k$ immediately completes.
+
+  \begin{claim}
+    $\Pr[F_4] \le \Pr[F_5]/q_S$.
+  \end{claim}
+  This claim is proven exactly as we did for claim~1 of
+  lemma~\ref{lem:sk-g2-g3}.
+
+  Let~$\G6$ be the same as $\G5$ except that we change the encrypted
+  responses of session~$S_k$ and its matching session~$T_k$.  Let $K^* =
+  (K_0^*, K_1^*) = H_K(Z_S)$.  Then, rather than sending $(\cookie{response},
+  R_S, E_{K_0^*}(Y_T))$, session~$S$ sends $(\cookie{response}, R_S,
+  E_{K_0^*}(1^{\ell_G}))$.
+  \begin{claim}
+    $|\Pr[F_6] - \Pr[F_5]| \le \InSec{ind-cca}(\E; t', q_M, q_M).$
+  \end{claim}
+  To prove this claim, we construct an adversary~$B$ which attacks the
+  IND-CCA security of our encryption scheme $\E$.  The adversary~$B$ works as
+  follows.
+  \begin{enumerate}
+  \item It is given no input, but a pair of oracles $E(\cdot, \cdot)$ and
+    $D(\cdot)$; the former encrypts either the left or right input, according
+    to a hidden bit, and the latter decrypts ciphertexts other than those
+    returned by $E(\cdot, \cdot)$.  Its goal is to guess the hidden bit.
+  \item It sets up a simulation of the game~$\G5$, by running the $\id{init}$
+    function, and simulating all of the parties.  In particular, it chooses a
+    random $k \in \Nupto{q_S}$.
+  \item It sets up accurate simulations of the random oracles $H_K(\cdot)$
+    and $H_I(\cdot, \cdot, \cdot, \cdot)$.
+  \item It runs $A$ in its simulated game.  It responds to all of $A$'s
+    instructions faithfully, except for the matching sessions $S_k$ and
+    $T_k$.  Let $S = S_k = (P_i, P_j, s)$, and $T = T_k = (P_j, P_i, s)$.
+  \item Suppose $T$ is sent the message $C_S = (\cookie{challenge}, R_S,
+    c_S)$.  Rather than computing $K^* = H_K(r_T R_S)$ and performing the
+    encryption properly, $B$ queries its left-or-right encryption oracle
+    $E(\cdot, \cdot)$ on $E(1^{\ell_G}, x_j R_S)$, and sends the resulting
+    ciphertext~$\chi$ back to~$S$ as part of a message $(\cookie{response},
+    R_T, \chi)$.  The set $M_T$ is precisely the set of messages constructed
+    in this fashion.  (Recall that challenge messages other than $C_S$ aren't
+    actually delivered to $T$, since we simulate the responses using the
+    extractor, as of $\G2$.)
+  \item Suppose $S$ is sent a message $M = (\cookie{response}, R_T, \chi) \in
+    M_T$.  We immediately stop the simulation, and $B$ returns $0$.
+  \item Suppose, instead, that $S$ is sent some message $M' =
+    (\cookie{response}, R, \chi) \notin M_T$.  There are two cases to
+    consider.  If $R = R_T$ then we must have $\chi$ distinct from the
+    ciphertexts returned by the $E(\cdot, \cdot)$ oracle, so we can invoke
+    the decryption oracle $D(\cdot)$ on $\chi$ to obtain a response $Y$.
+    Alternatively, if $R \ne R_T$, we can compute the key $K = (K_0, K_1) =
+    H_K(r_S R)$, and recover $Y = D_{K_0}(\chi)$.  In either case, if $Y =
+    r_S X_j)$ then $S$ would complete at this point: $B$ stops the simulation
+    and returns $1$.
+  \item If $A$ exposes $S$ (by corrupting $P_i$ or~$P_j$, or revealing $S$ or
+    $T$) then we stop the simulation and $B$ returns $0$.
+  \item Finally, if the game stops, either because $A$ halts, or because of
+    one of the special rules introduced in earlier games, $B$ returns $0$.
+  \end{enumerate}
+  It is clear that $B$'s oracle queries are acceptable, since $|x_j R_S| =
+  \ell_G$ by definition, and $B$ never queries $D(\cdot)$ on a ciphertext
+  returned by its encryption oracle.  By the rules of~$\G3$, we know that the
+  game stops immediately if $A$ ever queries $Z_S$, so the key $K^*$ is
+  independent of everything in $A$'s view except the ciphertexts $\chi$
+  output by $S$ and $T$.  Therefore, if the hidden bit of the IND-CCA game is
+  $1$, $B$ accurately simulates $\G5$, whereas if the bit is $0$ then $B$
+  accurately simulates $\G6$.  We issue no more that $q_M$ encryption or
+  decryption queries.  Finally, $B$'s running time is within the bounds
+  allowed for $t'$.  Therefore,
+  \[ \Adv{ind-cca}{\E}(B) = \Pr[F_5] - \Pr[F_6]
+     \le \InSec{ind-cca}(\E; t', q_M, q_M). \]
+  We construct the adversary~$\bar{B}$ which is the same as $B$ above, except
+  that $\bar{B}$ returns $0$ whenever $B$ returns~$1$, and \emph{vice versa}.
+  Clearly
+  \[ \Adv{ind-cca}{\E}(\bar{B})
+     = (1 - \Pr[F_5]) - (1 - \Pr[F_6])
+     = \Pr[F_6] - \Pr[F_5]
+     \le \InSec{ind-cca}(\E; t', q_M, q_M).
+  \]
+  This proves the claim.
+
+  Let $\G7$ be the same as $\G6$, except that at the start of the game we
+  choose a random $m \in \Nupto{n}$, and when the adversary creates the
+  session $S = S_k = (P_i, P_j, s)$, we abort the game unless $j = m$.
+  Clearly we have $\Pr[F_6] = n \Pr[F_7]$.
+
+  Finally, we can explicitly bound $F_6$.  In $\G6$, the adversary's view is
+  independent of the correct response $Y_S = r_S X_S = x_j R_S$ to $S$'s
+  challenge.  Therefore, if $A$ manages to send any message $\mu \notin M_T$
+  which causes $S$ to complete, then it has impersonated~$P_j$.
+  \begin{claim}
+    $\Pr[F_7] \le \InSec{mcdh}(G; t', q_M + q_I)$.
+  \end{claim}
+  The present lemma follows from this and the previous claims.
+
+  To prove the claim formally, we construct an adversary~$B'$, which behaves
+  as follows.
+  \begin{enumerate}
+  \item It is given as input a public key $X^*$ and a single challenge $(R^*,
+    c^*)$, a random oracle $H^*_I(\cdot, \cdot)$, and an oracle $V(\cdot,
+    \cdot)$, which verifies responses $(R, Y)$.  Its goal is to invoke
+    $V(\cdot, \cdot)$ with a correct response to the challenge.
+  \item It chooses a random $k \in \Nupto{q_S}$ and $m \in \Nupto{n}$. It
+    sets up a simulation of the game~$\G7$, by running the $\id{init}$
+    function, and simulating all of the parties, except that it gives party
+    $P_m$ the public key $X^*$.  This makes no difference, since $P_m$
+    doesn't actually need to give any `honest' responses because of the
+    change we made in $\G6$.
+  \item It sets up accurate simulations of the random oracles $H_K(\cdot)$
+    and $H_I(\cdot, \cdot, \cdot, \cdot)$, with one exception -- see below.
+  \item It runs $A$ in its simulated game.  It responds to all of $A$'s
+    instructions faithfully, except for the session $S_k$.  Let $S = S_k =
+    (P_i, P_j, s)$, and let $T = T_k = (P_j, P_i, s)$ be its matching
+    session.
+  \item When session~$S$ is created, $B'$ checks that $j = m$, and if not
+    stops the simulation and halts.  Otherwise, $B'$ invokes its oracle~$C()$
+    to obtain a pair $(R, c)$.  Session~$S$ sends $C_S = (\cookie{challenge},
+    R, c)$ as its challenge to~$T$.
+  \item When $A$ makes a query $H_I(X^*, s, R, Y)$, $B$ answers it by
+    querying its \emph{own} random oracle $H^*_I(R, Y)$.
+  \item When $S$ receives a message $(\cookie{response}, R, \chi)$, we
+    compute $(K_0, K_1) = r_S R$, and $Y = D_{K_0}(\chi)$.  If $Y \ne \bot$
+    then $B'$ calls $V(R, Y)$.
+  \item If $A$ reveals $S$ or corrupts $P_i$ or $P_j$ then $B'$ stops the
+    simulation immediately and halts.
+  \end{enumerate}
+  The running time of $B'$ is within the bounds required of $t'$; it makes at
+  most $q_I$ random-oracle and at most $q_M$ verification queries.  Clearly
+  $B'$ succeeds whenever $F_7$ occurs.  The claim follows from
+  theorem~\ref{thm:wident-sound}.
+\end{proof}
+
+
+\subsection{Proof of theorem~\ref{thm:sk2}}
+\label{sec:sk2-proof}
+
+The proof is almost identical to the proof of theorem~\ref{thm:sk}, in
+appendix~\ref{sec:sk-proof}.  Unfortunately a black-box reduction doesn't
+seem possible.
+
+We use the games and notation of section~\ref{sec:sk-proof}.
+
+The change to the check-value calculation doesn't affect key-generation at
+all, so the transition to $\G1$ goes through as before.
+
+The transition from $\G1$ to $\G2$ -- answering challenges using the
+extractor -- needs a little care.  Let $S = (P_i, P_j, s)$ be a session, and
+consider an incoming message $(\cookie{challenge}, R, c)$.
+\begin{itemize}
+\item If $T = (P_j, P_i, s)$ is the matching session to $S$, and $R = R_T$ is
+  the public challenge value of $T$, and $c = r_T \xor H_I(R_S, X_j, s, R_T,
+  r_T X_i)$ is the check-value output by $T$ when it received
+  $(\cookie{pre-challenge}, R_S)$ as input, then $S$ replies as it did in
+  $\G1$.
+\item If the challenge message is any other message, then we use the
+  extractor.
+\end{itemize}
+As in lemma~\ref{lem:sk-g1-g2}, we examine which sessions could have queried
+$H_I(R_S, X_j, s, R, x_i R)$, and for the same reasons conclude that only the
+matching session would have done this, and only in response to the
+pre-challenge $R_S$.  It follows that $\diff{1}{2} \le q_M/2^{\ell_I}$ as
+before.
+
+The remaining game steps go through unchanged.  In particular, we conclude
+that a ripe session will only complete if the adversary has transmitted
+messages from its matching session correctly, and the session key is
+independent of the adversary's view.  The theorem follows.
+
+
+\subsection{Sketch proof of single-key protocol for secure channels}
+\label{sec:sc-proof}
+
+We want to show that the Wrestlers Key-Exchange protocol, followed by use of
+the encryption scheme $\E$, with the \emph{same} key $K = K_0$, still
+provides secure channels.
+
+\subsubsection{Secure channels definition}
+We (very briefly!) recall the \cite{Canetti:2001:AKE} definition of a secure
+channels protocol.  We again play a game with the adversary.  At the
+beginning, we choose a bit $b^* \inr \{0, 1\}$ at random.  We allow the
+adversary the ability to establish \emph{secure channels} sessions within the
+parties.  Furthermore, for any running session $S = (P_i, P_j, s)$, we allow
+the adversary to request $S$ to send a message~$\mu$ through its secure
+channel.  Finally, the adversary is allowed to choose one ripe
+\emph{challenge} session, and ask for it to send of one of a \emph{pair} of
+messages $(\mu_0, \mu_1)$, subject to the restriction that $|\mu_0| =
+|\mu_1|$; the session sends message $\mu_{b^*}$.  The adversary may not
+expose the challenge session.
+
+The adversary wins if (a)~it can guess the bit $b^*$, or (b)~it can cause a
+ripe session $S$ (i.e., an unexposed, running session), with a matching
+session~$T$ to output a message other than one that it requested that $T$
+send.
+
+\subsubsection{Protocol definition}
+The protocol begins with Wrestlers key-exchange.  The encryption in the
+key-exchange protocol is performed as $E_K(\cookie{kx}, \cdot)$; encryption
+for secure channels is performed as $E_K(\cookie{sc}, i, o, \cdot)$, where
+$i$ is a sequence number to prevent replays and $o \in \{S, T\}$ identifies
+the sender.
+
+\subsubsection{Proof sketch}
+We use the games and notation of appendix~\ref{sec:sk-proof}.
+
+The proof goes through as far as the step between $\G5$ and $\G6$ in the
+proof of lemma~\ref{lem:sk-g3-g4}.  Here we make the obvious adjustments to
+our adversary against the IND-CCA security of $\E$.  (Our adversary will need
+to use the left-or-right oracle for messages sent using the secure channel
+built on $K^*$.  That's OK.)
+
+In $\G4$, we know that ripe sessions agree the correct key, and the adversary
+never queries the random oracle, so the key is independent of the adversary's
+view.
+
+We define a new game $\G8$, which is like $\G4$, except that we stop the game
+if the adversary ever forges a message sent over the secure channel.  That
+is, if a ripe session $S$ ever announces receipt of a message not sent (at
+the adversary's request) by its matching session $T$.  Let $F_8$ be the event
+that a forgery occurs.  We apply lemma~\ref{lem:shoup}, which tells us that
+$\diff{4}{8} \le \Pr[F_8]$.  To bound $F_8$, we isolate a session at random
+(as in lemmata \ref{lem:sk-g2-g3} and~\ref{lem:sk-g3-g4}), which tells us
+that
+\begin{equation}
+  \label{eq:sc-g4-g8}
+  \diff{4}{8} \le q_S \cdot \InSec{int-ptxt}(\E; t', q_M, q_M)
+\end{equation}
+Finally, we can bound the adversary's advantage at guessing the hidden bit
+$b^*$.  We isolate (we hope) the challenge session $S$ by choosing a target
+session at random, as before.  Let $K^* = H_K(Z_S)$ be the key agreed by the
+session (if it becomes ripe).  We define an adversary $B$ against the IND-CCA
+security of $\E$.  The adversary $B$ simulates the game.  If the adversary
+exposes the target session, or doesn't choose it as the challenge session,
+$B$ fails (and exits 0); otherwise it uses the left-or-right encryption
+oracle to encrypt both of the adversary's message choices, and outputs the
+adversary's choice.  Let $b$ be the adversary's output, and let $\epsilon$ be
+the advantage of our IND-CCA distinguisher.  Then
+\begin{eqnarray*}[rl]
+  \Pr[b = b^*]
+  & = \Pr[b = b^* \wedge b^* = 1] + \Pr[b = b^* \wedge b^* = 0] \\
+  & = \frac{1}{2}\bigl( \Pr[b = b^* \mid b^* = 1] +
+      \Pr[b = b^* \mid b^* = 0] \bigr) \\
+  & = \frac{1}{2}\bigl( \Pr[b = b^* \mid b^* = 1] +
+                        (1 - \Pr[b \ne b^* \mid b^* = 0]) \bigr) \\
+  & = \frac{1}{2}\bigl( \Pr[b = 1 \mid b^* = 1] -
+                        \Pr[b = 1 \mid b^* = 0] + 1 \bigr) \\
+  & = \frac{1}{2}\bigl(1 + q_S\,\Adv{ind-cca}{\E}(B) \bigr) \\
+  & \le \frac{1}{2} \bigl( 1 + q_S\,\InSec{ind-cca}(\E; t', q_M, q_M) \bigr).
+			\eqnumber
+\end{eqnarray*}
 
-\bibliography{mdw-crypto,cryptography,cryptography2000,rfc}
 \end{document}
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
-%%% TeX-master: "wrestlers"
+%%% TeX-master: t
 %%% End:
