wrestlers.tex: Fix citations to catch up with Bibtex database changes.
[doc/wrestlers] / wrestlers.tex
index 633a93d..8a05c61 100644 (file)
@@ -5,31 +5,42 @@
 %%% (c) 2006 Mark Wooding
 %%%
 
-\newif\iffancystyle\fancystylefalse
-\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,
-    runinsubsubsec]
-    {strayman}
+  \documentclass{strayman}
+  \parskip=0pt plus 1pt  \parindent=1.2em
   \usepackage[T1]{fontenc}
   \usepackage[palatino, helvetica, courier, maths=cmr]{mdwfonts}
   \usepackage[within = subsection, mdwmargin]{mdwthm}
   \usepackage{mdwlist}
   \usepackage{sverb}
-  \PassOptionsToPackage{dvips}{xy}
+  \ifpdfing\else
+    \PassOptionsToPackage{dvips}{xy}
+  \fi
 \else
-  \documentclass[a4paper]{llncs}
-  \usepackage{a4wide}
+  \PassOptionsToClass{runningheads}{llncs}
+  \documentclass{llncs}
 \fi
 
 \PassOptionsToPackage{show}{slowbox}
 %\PassOptionsToPackage{hide}{slowbox}
-\usepackage{mdwtab, mathenv, mdwmath, crypto}
+\usepackage{mdwtab, mdwmath, crypto}
 \usepackage{slowbox}
 \usepackage{amssymb, amstext}
 \usepackage{url, multicol}
   \usepackage[all]{xy}
   \turnradius{4pt}
 \fi
+\usepackage{mathenv}
 
+\newcommand{\Nupto}[1]{\{0, 1, \ldots, #1 - 1\}}
 \iffancystyle
-  \def\next{\title[The Wrestlers Protocol]}
+  \let\next\title
 \else
-  \def\next{\title}
+  \def\next[#1]{\titlerunning{#1}\title}
 \fi
 \next
-  {The Wrestlers Protocol \\
+  [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}}
   \numberwithin{equation}{subsection}
   \let\random\$
 \else
-  \bibliographystyle{plain}
+  \bibliographystyle{splncs}
   \expandafter\let\csname claim*\endcsname\claim
   \expandafter\let\csname endclaim*\endcsname\endclaim
 \fi
 
-\iffancystyle
-  \newcommand{\Nupto}[1]{\N_{<{#1}}}
-\else
-  \newcommand{\Nupto}[1]{\{0, 1, \ldots, #1 - 1\}}
-\fi
 \let\Bin\Sigma
 \let\emptystring\lambda
 \edef\Pr{\expandafter\noexpand\Pr\nolimits}
 \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}%
 \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\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}
   We describe and prove (in the random-oracle model) the security of a simple
 
 \iffancystyle
 \newpage
+\thispagestyle{empty}
 \columnsep=2em \columnseprule=0pt
 \tableofcontents[\begin{multicols}{2}\raggedright][\end{multicols}]
 %%\listoffigures[\begin{multicols}{2}\raggedright][\end{multicols}]
 
 \section{Introduction}
 
-%% Blah...
-%% Very brief discussion of key-exchange
-%% models of secure key exchange
-%% mutter about protocol actually being implemented
-
-
-
-In this paper, we concern ourselves mainly with \emph{authenticated key
-  exchange}.  That is, we present a system whereby two parties, say Alice and
-Bob, can communicate over an insecure channel, and end up knowing a shared
-random key unknown to anyone else.  \fixme{write the rest of this}
-
-
-\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)$, there is a bound~$n$ such that the adversary's advantage
-is less than $p(k)$ for all choices of $k > n$.
-
-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{Koblitz:2006:ALP} (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.
+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.
 
-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:2000: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.
+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}
@@ -228,7 +246,8 @@ Our identification protocol has a number of desirable properties.
   intractability of the computational Diffie-Hellman problem.
 \end{itemize}
 
-Our key-exchange protocol also has a number of desirable properties.
+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
@@ -249,18 +268,147 @@ Our key-exchange protocol also has a number of desirable properties.
   a given protocol execution.
 \end{itemize}
 
+\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
 
 \subsection{Formal models for key-exchange}
 
+\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.
+
+\else
+
 Many proposed key-exchange protocols have turned out to have subtle security
-flaws.  Burrows, Abadi and Needham \cite{Burrows:1989:LA} presented a formal
-logic for the analysis of authentication and key-exchange protocols.  Formal
-models for analysing the \emph{computational} security of key-exchange
-protocols began with Bellare and Rogaway \cite{Bellare:1994:EAK}, extended in
-\cite{Bellare:1995:PSS, Blake-Wilson:1997:KAP, Blake-Wilson:1998:EAA,
-  Bellare:1998:MAD}.
+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}
@@ -275,26 +423,35 @@ The remaining sections of this paper are as follows.
 \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:...} presents our conclusions.
+  security.
+\item Finally, section \ref{sec:conc} presents our conclusions.
 \end{itemize}
 
+\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}
 
-\subsection{Miscellaneous notation}
+\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$.
-\iffancystyle
-We write $\Nupto{n} = \{\, i \in \Z \mid 0 \le i < n \,\} = \{0, 1, \ldots, n
-- 1\}$ for the set of nonnegative integers less than $n$.
-\fi
-
 
-\subsection{Groups}
+\prelimsec{Groups}
 
 Let $(G, +)$ be a cyclic group\footnote{
   We find that additive group notation is easier to read.  In particular, in
@@ -303,10 +460,13 @@ Let $(G, +)$ be a cyclic group\footnote{
 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 \Nupto{q}$.
+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.
 
-\subsection{Bit strings and encodings}
+\prelimsec{Bit strings and encodings}
 \label{sec:bitenc}
 
 Let $\Bin = \{0, 1\}$ be the set of binary digits.  Then $\Bin^n$ is the set
@@ -316,23 +476,30 @@ 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$: if $z = x \xor y$ then $|z|
-= n$, and $z[i] = (x[i] + y[i]) \bmod 2$ for $0 \le i < n$.  We write $x \cat
-y$ to mean the concatenation of $x$ and $y$: 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|$.
+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 =
-\Nupto{|G|}$ as bit strings.  To this end, we shall assume the existence of
+\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, I \}.
+  \textrm{for } S \in \{ G, \F \}.
 \]
 with the following properties.
 \begin{itemize}
@@ -353,9 +520,10 @@ 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
 
-
-\subsection{Games, adversaries, and oracles}
+\ifshort\else
+\prelimsec{Games, adversaries, and oracles}
 \label{sec:games}
 
 Many of the security definitions and results given here make use of
@@ -373,44 +541,47 @@ 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.  
+distinguish between the two except with very small probability.
 
 Our proofs make frequent use of sequences of games; see
-\cite{Shoup:2004:SGT,Bellare:2004:CBG}.  The presentation owes much to Shoup
-\cite{Shoup:2004:SGT}.  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.
+\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|\bar F] = \Pr[T|\bar F]$.
-  Then $|\Pr[S] - \Pr[T]| \le \Pr[F]$.
+  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|F]\Pr[F] + \Pr[S|\bar F]\Pr[\bar F]) -
-         (\Pr[T|F]\Pr[F] + \Pr[T|\bar F]\Pr[\bar F])| \\
-    & = \Pr[F] \cdot |\Pr[S|F] - \Pr[T|F]| \\
+    & = |(\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
 
 
-\subsection{The random oracle model}
+\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
@@ -429,9 +600,10 @@ 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 is useful for constructing reductions and simulators
-for two main reasons.
+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.
@@ -449,14 +621,17 @@ 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:2001:IBE}.  Proving the security of the modifications we
+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
 
 
-\subsection{Notation for algorithms}
+\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
@@ -479,9 +654,9 @@ 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
 
-
-\subsection{Diffie-Hellman problems}
+\prelimsec{Diffie-Hellman problems}
 \label{sec:dhp}
 
 The security of our protocols is related to the hardness of the
@@ -490,12 +665,13 @@ 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 \Nupto{|G|} : A(x P, y P) = x y P ]
+      \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
@@ -508,7 +684,7 @@ 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|$.
+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
@@ -517,30 +693,18 @@ 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{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}
 
 \begin{figure}
   \begin{program}
     $\Game{mcdh}{G}(A)$: \+ \\
       $w \gets 0$; \\
-      $x \getsr \Nupto{|G|}$; $y \getsr \Nupto{|G|}$; \\
+      $x \getsr \Z/\#G\Z$; $y \getsr \Z/\#G\Z$; \\
       $A^{V(\cdot)}(x P, y P)$; \\
       \RETURN $w$;
     \next
@@ -556,6 +720,23 @@ $V(x y P)$.
   \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
@@ -567,11 +748,16 @@ 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 q_V\cdot\InSec{cdh}(G; t + O(q_V)). \]
+  \[ \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{proof}
+\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.
@@ -605,14 +791,13 @@ CDH.
       \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$, the
-  output of $A$ is stored in $Q_{n-1}$ 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.
+  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
@@ -631,10 +816,10 @@ CDH.
     & =  \frac{\epsilon}{q_V}.
   \end{eqnarray*}
   which completes the proof.
-\end{proof}
+\end{longproof}
 
-
-\subsection{Example groups and encodings}
+\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
@@ -658,23 +843,23 @@ using the functions $(e, d)$:
 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 < 2^{\ell_I}$ and $I = \Nupto{q}$, then, we can define an
-encoding $(e_I, d_I)$ by $e_I(n) = e(q, \ell_I, n)$ and $d_I(a) = d(q,
-\ell_I, a)$.
-
-Let $p$ and $q$ be primes, with $q|(p - 1)$.  Then there is an order-$q$
-subgroup of $(\Z/p\Z)^*$.  In practice, an order-$q$ element can be found
-easily by taking elements $h \in (\Z/p\Z)^*$ 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 $\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.
+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
@@ -687,9 +872,10 @@ $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{Symmetric encryption}
+\prelimsec{Symmetric encryption}
 \label{sec:sym-enc}
 
 Our key-exchange protocol requires a symmetric encryption scheme.  Our
@@ -714,14 +900,14 @@ selecting a string of a given length uniformly at random.
 Our security notion for symmetric encryption is the standard notion of
 left-or-right indistinguishability of ciphertexts under chosen-ciphertext
 attack.
-\begin{definition}
-  [Indistinguishability under chosen-ciphertext attack (IND-CCA)]
+\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]
+     \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}
@@ -746,7 +932,31 @@ attack.
 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}.  
+demonstrate \emph{simulatability}.
+
+\ifshort
+
+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$.
+
+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}$.
+
+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.
+
+\else
 
 \subsubsection{General framework}
 Consider a game in which an adversary~$A$ interacts with some `world'~$W$,
@@ -838,14 +1048,23 @@ 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
-the auxiliary input because otherwise the simulator could just `make up'
-plausible-looking inputs.
+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 the time $t_A$ taken by the adversary and $t_D$ taken by the
   distinguisher,
@@ -860,7 +1079,9 @@ and so on.  Specifically, we are interested in
 \end{itemize}
 Sometimes we shall not be interested in proving simulatability of adversaries
 with auxiliary inputs.  We write $\mathcal{U} = 0$ to indicate that auxiliary
-output is not allowed.
+input is not allowed.
+
+\ifshort\else
 
 \subsubsection{World syntax}
 It will be worth our while being more precise about what a `world' actually
@@ -876,7 +1097,7 @@ figure~\ref{fig:sim-world}.
 \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 `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
@@ -932,6 +1153,8 @@ does little harm, and simplifies the overall exposition.
 
 \subsubsection{Definitions}
 We are now ready to begin making definitions.
+\fi
+
 \begin{definition}[Simulation security]
   \label{def:sim}
   Consider the game described above, with the initialization function~$I$,
@@ -965,7 +1188,7 @@ We are now ready to begin making definitions.
   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 that the usual one.
+  deniability than the usual one.
 \end{remark}
 
 \begin{figure}
@@ -989,6 +1212,7 @@ We are now ready to begin making definitions.
   \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
@@ -1064,6 +1288,7 @@ case.
   \]
   as required.
 \end{proof}
+\fi
 
 %%%--------------------------------------------------------------------------
 
@@ -1074,14 +1299,14 @@ case.
 \subsection{Description}
 
 Here we present a simple zero-knowledge identification scheme.  Fix some
-group $G$.  Suppose Alice chooses a private key $x \inr \Nupto{|G|}$, 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.
+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 \Nupto{|G|}$, 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 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$.
@@ -1095,11 +1320,11 @@ figure~\ref{fig:wident}.
 
 \begin{figure}
   \begin{description}
-  \item[Setup] Group $G = \langle P \rangle$; $|G| = q$ is prime.
+  \item[Setup] Group $G = \langle P \rangle$; $\#G = q$ is prime.
     $H_I(\cdot, \cdot)$ is a secure hash.
-  \item[Private key] $x \inr \Nupto{q}$.
+  \item[Private key] $x \inr \gf{q}$.
   \item[Public key] $X = x P$.
-  \item[Challenge] $(R, c)$ where $r \inr \Nupto{q}$, $R = r P$, $c = r \xor
+  \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$.
@@ -1119,12 +1344,12 @@ hash function $H_I(\cdot, \cdot)$ is modelled as a random oracle.
 \begin{figure}
   \begin{program}
     Function $\id{setup}()$: \+ \\
-      $x \getsr \Nupto{q}$; \\
+      $x \getsr \gf{q}$; \\
       $X \gets x P$; \\
       \RETURN $(x, X)$;
-    \next
+    \ifshort\newline\else\next\fi
     Function $\id{challenge}^{H_I(\cdot, \cdot)}(R, c, X)$: \+ \\
-      $r \getsr \Nupto{q}$; \\
+      $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]
@@ -1208,13 +1433,14 @@ it to return $1$).
   Note that the security bound here is \emph{independent} of the value of
   $n$.
 \end{remark}
-\begin{proof}
+\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.
 
@@ -1332,8 +1558,7 @@ it to return $1$).
     \caption{Soundness of $\Wident$: reduction from MCDH}
     \label{fig:wident-sound-cdh}
   \end{figure}
-
-\end{proof}
+\end{longproof}
 
 \subsubsection{Zero-knowledge}
 Finally we must prove that $\Wident$ is (statistical) zero-knowledge -- i.e.,
@@ -1364,8 +1589,7 @@ 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.  The extractor is
-permitted to fail given 
+analyse the security of our key exchange protocol.
 
 \begin{definition}[Discrete-log extractors]
   Let $T$, $B$ be randomized algorithms.  Define the game
@@ -1374,26 +1598,6 @@ permitted to fail given
   is defined as
   \[ \Succ{dl-ext}{G}(T, B) = \Pr[\Game{dl-ext}{G}(T, B) = 1]. \]
 \end{definition}
-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}.  
 
 \begin{figure}
   \begin{program}
@@ -1406,7 +1610,7 @@ The resulting definition bears a striking similarity to the concept of
       $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^*) = (r', Y')$; \\
+      \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$; \\
@@ -1417,30 +1621,68 @@ The resulting definition bears a striking similarity to the concept of
       $Q_H \gets Q_H \cup \{(R', Y', h)\}$; \\
       \RETURN $h$; \- \\[\medskipamount]
     Oracle $C()$: \+ \\
-      $r \getsr \Nupto{q}$; \\
+      $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)$    
+      \RETURN $(R, c)$
   \end{program}
 
   \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$ which,
-  for any algorithm $B$,
+  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}
+    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 \Nupto{q}$ as the world
+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
@@ -1458,18 +1700,19 @@ theorem.
   \]
   where $q_C$ is the maximum number of challenges allowed by the adversary.
 \end{theorem}
-\begin{proof}
+\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{proof}
+\end{longproof}
 
+%\ifshort\else
 \begin{figure}
   \begin{program}
     Initialization function $I_\Wident()$: \+ \\
-      $x \getsr \Nupto{|G|}$; \\
+      $x \getsr \gf{q}$; \\
       $X \gets x P$; \\
       \RETURN $(x, X)$;
     \- \\[\medskipamount]
@@ -1503,52 +1746,39 @@ theorem.
   \caption{Real-prover and simulator for zero-knowledge of $\Wident$}
   \label{fig:wident-sim}
 \end{figure}
+%\fi
 
-We now return to proving that our extractor exists and functions as claimed.
-The following two trivial lemmas will be useful, both now and later.
+\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 integer $x$ where $0 \le x < |G|$ and $X = x P$.
+  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 $|G|$.
+  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; let $H_I$ be a function
-  $H_I\colon \Bin^{2\ell_G} \to \Bin^{\ell_I}$.  Fix some $x \in
-  \Nupto{|G|}$ and define the set
+  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'$. 
+  then $c = c'$.
 \end{lemma}
 \begin{proof}
-  From lemma~\ref{lem:unique-dl}, we see that there is a unique $r \in
-  \Nupto{|G|}$ 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)$.
+  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}]
-  Our extractor $T_\Wident$ is shown in figure~\ref{fig:twident}.
-
-  \begin{figure}
-    \begin{program}
-      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}
-
   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.
@@ -1598,15 +1828,17 @@ The following two trivial lemmas will be useful, both now and later.
   zero-knowledge against honest verifiers.  We're much more interested in
   dishonest verifiers, though.
 \end{remark}
+\fi
 
 
+\ifshort\else
 \subsection{An identity-based identification scheme}
 \label{sec:wident-id}
 
-Boneh and Franklin \cite{Boneh:2001:IBE} showed how to construct an
+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:1984:PKC}.  We can easily apply their
+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}
@@ -1617,7 +1849,7 @@ 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:2001:IBE} gives more detail; also \cite{Menezes:2006:IPB}
+\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
@@ -1627,8 +1859,8 @@ respectively.  We say that a mapping $\hat{e}\colon G \times G' \to G_T$ is a
 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')$.
+  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
@@ -1643,7 +1875,7 @@ 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 \Nupto{q}$; his public key is $T =
+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
@@ -1657,7 +1889,7 @@ with Alice in order to verify her identity as follows.
 \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 \Nupto{q}$, and sets $R = r P$.  He also computes
+\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'
@@ -1681,24 +1913,26 @@ 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
 
 
+\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{Stinson:2006:EST}.  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 \Nupto{q}$ and her public key is $\alpha =
-\gamma^a$.  In their protocol, the challenger chooses $r \inr \Nupto{q}$,
-computes $\rho = \gamma^r$ and $\psi = \alpha^r$, and sends a challenge
-$(\rho, H(\rho, \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.
+\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.  
+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}) =
@@ -1719,11 +1953,12 @@ 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{Stinson:2006:EST} 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(\rho, \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'.
+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
@@ -1738,7 +1973,7 @@ case-analysis which would be the basis of a proof of this.
     \\ \hlx{v[1]hv}
     %% unpleasant hacking to make the R and c columns the same width :-(
     \settowidth{\dimen0}{\textbf{Challenge}}%
-    \dimen0=.5\dimen0    
+    \dimen0=.5\dimen0
     \advance\dimen0by-\tabcolsep
     \advance\dimen0by-.5\arrayrulewidth
     \hbox to\dimen0{\hfil$R$\hfil}
@@ -1755,7 +1990,7 @@ case-analysis which would be the basis of a proof of this.
                          (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}
@@ -1769,6 +2004,7 @@ 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
 
 %%%--------------------------------------------------------------------------
 
@@ -1813,10 +2049,10 @@ $H_I\colon \Bin^{2\ell_G} \to \Bin^{\ell_I}$ and $H_K\colon \Bin^{\ell_G+1}
 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 \Nupto{|G|}$.  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 \Nupto{|G|}$.  He computes $S
-  = s P$ and $d = s \xor H_I(S, s A)$.  He sends $(S, d)$ to Alice.
+\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.
@@ -1837,40 +2073,32 @@ figure~\ref{fig:wkx}.
 
 \begin{figure}
   \begin{description}
-  \item[Setup] Group $G = \langle P \rangle$; $|G| = q$ is prime.
+  \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 \Nupto{q}$.
+  \item[Private keys] $x_i \inr \gf{q}$.
   \item[Public keys] $X_i = x_i P$.
   \end{description}
-  \[ \begin{graph}
-    !{0; <8cm, 0cm>: <0cm, 3cm>::}
-    *+[F]\dbox{$r_i \getsr I$; $R_i \gets r_i P$ \\
-               $c_i \gets r_i \xor H_I(R_i, r_i X_j)$} ="i0"
-    [d]
-    *+[F]\dbox{Check $R_j = \bigl(c_j \xor H_I(x_i R_j)\bigr) P$ \\
-               $Z \gets r_i R_j$; $K \gets H_K(0, Z)$ \\
-               $\chi_i \gets E_K(x_i R_j)$} ="i1"
-    [d]
-    *+[F]\dbox{Check $D_K(\chi_j) = r_i X_j$ \\
-               Shared key is $H_K(1, Z)$} ="i2"
-    "i0" [r]
-    *+[F]\dbox{$r_j \getsr I$; $R_j \gets r_j P$ \\
-               $c_j \gets r_j \xor H_I(R_j, r_j X_i)$} ="j0"
-    [d]
-    *+[F]\dbox{Check $R_i = \bigl(c_i \xor H_I(x_j R_i)\bigr) P$ \\
-               $Z \gets r_j R_i$; $K \gets H_K(0, Z)$ \\
-               $\chi_j \gets E_K(x_j R_i)$} ="j1"
-    [d]
-    *+[F]\dbox{Check $D_K(\chi_i) = r_j X_i$ \\
-               Shared key is $H_K(1, Z)$} ="j2"
-    %
-    "i0" : |(0)/3.25cm/*+{(R_i, c_i)} "j1"
-    "i1" : |(0)/3.25cm/*+{(R_i, \chi_i)} "j2"
-    "j0" : |(0)/3.25cm/*+{(R_j, c_j)} "i1"
-    "j1" : |(0)/3.25cm/*+{(R_j, \chi_j)} "i2"
-  \end{graph} \]
+  \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}
@@ -1886,7 +2114,7 @@ Then:
   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 
+  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.
@@ -1912,7 +2140,7 @@ version we present here.
 \label{sec:um}
 
 Our model is very similar to that of Canetti and Krawczyk
-\cite{Canetti:2002:???}, though we have modified it in two ways.
+\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.
@@ -1922,6 +2150,13 @@ Our model is very similar to that of Canetti and Krawczyk
   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
@@ -1947,13 +2182,13 @@ $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 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{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.
@@ -2047,11 +2282,13 @@ it.  The adversary \emph{wins} the game if either
 \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 previously, where $n$
+  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
@@ -2073,7 +2310,7 @@ More formally, we make the following definition.
 \subsection{Security}
 
 In order to analyse our protocol $\Wkx^{G, \E}$ properly, we must describe
-exactly how it fits into the formal model described in our formal model.
+exactly how it fits into our formal model.
 
 \subsubsection{Sessions and session-ids}
 Our formal model introduced the concept of sessions, which the informal
@@ -2127,15 +2364,15 @@ 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{Shoup:1999:OFM}.  There
-  it is required that a key-exchange protocol terminate after a
+  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{program}
     Function $\id{init}(n)$: \+ \\
       \FOR $i \in \Nupto{n}$ \DO \\ \ind
-        $x \getsr \Nupto{|G|}$; \\
+        $x \getsr \gf{q}$; \\
         $\mathbf{i}[i] \gets x$; \\
         $\mathbf{p}[i] \gets x P$; \- \\
       \RETURN $(\mathbf{p}, \mathbf{i})$;
@@ -2145,7 +2382,7 @@ sake of robustness.\footnote{%
       $X \gets \mathbf{p}[i]$;
       $X' \gets \mathbf{p}[j]$;
       $C \gets \emptyset$; \\
-      $r \getsr \Nupto{|G|}$;
+      $r \getsr \gf{q}$;
       $R \gets r P$;
       $Y \gets r X'$; \\
       $h \gets H_I(X, s, R, Y)$;
@@ -2179,7 +2416,7 @@ sake of robustness.\footnote{%
       \OUTPUT $K_1$;
       \STOP;
   \end{program}
-  
+
   \caption{Formalization of $\Wkx$}
   \label{fig:wkx-formal}
 \end{figure}
@@ -2211,23 +2448,25 @@ 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 appendix~\ref{sec:sk-proof}.
+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
-      \frac{n (n - 1)}{|G|} +
-      \frac{2 q_M}{2^{\ell_I}} + {}\\
-      2 q_S \bigl( \InSec{mcdh}(G; t', q_K) +
-                   n \cdot \InSec{mcdh}(G; t', q_M + q_I) +
-                   \InSec{ind-cca}(\E; t', q_M, q_M) \bigr)
+      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}
 
 
+\ifshort\else
 \subsection{Insecure protocol variants}
 \label{sec:kx-insecure}
 
@@ -2325,7 +2564,7 @@ set up.
 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}
@@ -2338,7 +2577,7 @@ 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{DiRaimondo:2006:DAK}, except that, as usual, we opt for a concrete
+\cite{cryptoeprint:2006:280}, except that, as usual, we opt for a concrete
 security approach.
 
 \subsubsection{Discussion}
@@ -2421,7 +2660,7 @@ 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 \Nupto{q}$.  He computes $R = r P$ and $c =
+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
@@ -2456,45 +2695,36 @@ 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.
+  \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 \Nupto{q}$.
+  \item[Private keys] $x_i \inr \gf{q}$.
   \item[Public keys] $X_i = x_i P$.
   \end{description}
-  \[ \begin{graph}
-    !{0; <8cm, 0cm>: <0cm, 3cm>::}
-    *+[F]\dbox{$r_i \getsr I$; $R_i \gets r_i P$} ="i-1"
-    [d]
-    *+[F]\dbox{$c_i \gets r_i \xor H_I(R_j, X_i, s, R_i, r_i X_j)$} ="i0"
-    [d]
-    *+[F]\dbox{Check $R_j = \bigl(c_j \xor H_I(x_i R_j)\bigr) P$ \\
-               $Z \gets r_i R_j$; $K \gets H_K(0, Z)$ \\
-               $\chi_i \gets E_K(x_i R_j)$} ="i1"
-    [d]
-    *+[F]\dbox{Check $D_K(\chi_j) = r_i X_j$ \\
-               Shared key is $H_K(1, Z)$} ="i2"
-    "i-1" [r]
-    *+[F]\dbox{$r_j \getsr I$; $R_j \gets r_j P$} ="j-1"
-    [d]
-    *+[F]\dbox{$c_j \gets r_j \xor H_I(R_i, X_j, s, R_j, r_j X_i)$} ="j0"
-    [d]
-    *+[F]\dbox{Check $R_i = \bigl(c_i \xor H_I(x_j R_i)\bigr) P$ \\
-               $Z \gets r_j R_i$; $K \gets H_K(0, Z)$ \\
-               $\chi_j \gets E_K(x_j R_i)$} ="j1"
-    [d]
-    *+[F]\dbox{Check $D_K(\chi_i) = r_j X_i$ \\
-               Shared key is $H_K(1, Z)$} ="j2"
-    %
-    "i-1" : |(0)/3.25cm/*+{R_i} "j0"
-    "i0" : |(0)/3.25cm/*+{(R_i, c_i)} "j1"
-    "i1" : |(0)/3.25cm/*+{(R_i, \chi_i)} "j2"
-    "j-1" : |(0)/3.25cm/*+{R_j} "i0"
-    "j0" : |(0)/3.25cm/*+{(R_j, c_j)} "i1"
-    "j1" : |(0)/3.25cm/*+{(R_j, \chi_j)} "i2"
-  \end{graph} \]
+
+  \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}
@@ -2504,7 +2734,7 @@ formal description is shown in figure~\ref{fig:wdkx-formal}.
   \begin{program}
     Function $\id{init}(n)$: \+ \\
       \FOR $i \in \Nupto{n}$ \DO \\ \ind
-        $x \getsr \Nupto{|G|}$; \\
+        $x \getsr \gf{q}$; \\
         $\mathbf{i}[i] \gets x$; \\
         $\mathbf{p}[i] \gets x P$; \- \\
       \RETURN $(\mathbf{p}, \mathbf{i})$;
@@ -2514,7 +2744,7 @@ formal description is shown in figure~\ref{fig:wdkx-formal}.
       $X \gets \mathbf{p}[i]$;
       $X' \gets \mathbf{p}[j]$;
       $C \gets \emptyset$; \\
-      $r \getsr \Nupto{|G|}$;
+      $r \getsr \gf{q}$;
       $R \gets r P$;
       $Y \gets r X'$; \\
       \SEND $(\cookie{pre-challange}, R)$;
@@ -2555,13 +2785,14 @@ formal description is shown in figure~\ref{fig:wdkx-formal}.
       \OUTPUT $K_1$;
       \STOP;
   \end{program}
-  
+
   \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 in appendix~\ref{sec:sk2-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
@@ -2590,14 +2821,17 @@ deniability of our protocols.
        \frac{q_M}{2^{\ell_I}}
   \]
   and
-  \[ \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
-       \frac{n_C q_S}{|G|} +
+  \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{proof}
+\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}
@@ -2605,7 +2839,7 @@ deniability of our protocols.
     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 \Nupto{|G|}$, and computes $R_S = r_S P$, and $Y_S = r_S
+    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)$.
@@ -2657,17 +2891,17 @@ deniability of our protocols.
     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.
+    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|}. \]
+  \[ \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{proof}
-
+\end{longproof}
 
+\ifshort\else
 \subsection{Practical issues}
 \label{sec:practice}
 
@@ -2683,11 +2917,11 @@ 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
+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.
+\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
@@ -2713,8 +2947,6 @@ 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.
 
-There's another denial-of-service attack against the Wrestlers protocol.  
-
 \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
@@ -2729,19 +2961,115 @@ 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.  The \cookie{switch} message can be as simple as $(\cookie{switch},
-E_{K_0}(\cookie{switch}))$.
+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 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}
 
 \subsubsection{Unreliable transports}
-The Internet UDP \cite{RFC768} is a simple, unreliable protocol for
+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).
-
+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.
 
 %%%--------------------------------------------------------------------------
 
@@ -2752,10 +3080,17 @@ Clive Jones and I worked out the initial design.
 
 %%%--------------------------------------------------------------------------
 
-\bibliography{mdw-crypto,cryptography2000,cryptography,rfc}
+\bibliography{%
+  mdw-crypto,%
+  eprint,%
+  focs1990,stoc1990,tissec,jacm,%
+  lncs1997a,lncs1997b,lncs1998a,lncs2001a,%
+  cryptography1990,cryptography2000,cryptography2010,cryptography,%
+  rfc,std}
 
 %%%--------------------------------------------------------------------------
 
+\ifshort\def\next{\end{document}}\expandafter\next\fi
 \appendix
 \section{Proofs}
 
@@ -2768,7 +3103,6 @@ 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
@@ -2811,14 +3145,16 @@ 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
+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}
   \label{eq:sk-g0-g1}
-  \diff{0}{1} \le \frac{1}{|G|} \binom{n}{2} = \frac{n (n - 1)}{2 |G|}.
+  \diff{0}{1} \le \frac{1}{\#G} \binom{n}{2} = \frac{n (n - 1)}{2 \#G}.
 \end{equation}
 In game~$\G1$ and onwards, we can assume that public keys for distinct
-parties are themselves 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,
@@ -2856,8 +3192,7 @@ 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' = t + O(n) + O(q_S) + O(q_M q_I) + O(q_K)$ not much
-  larger than $t$ we have
+  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).
@@ -2877,6 +3212,7 @@ 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) +
@@ -2911,15 +3247,15 @@ We conclude that, for any adversary $A$,
   \Pr[V_4] = 0 \qquad \text{and} \qquad \Pr[W_4] = \frac{1}{2}.
 \end{equation}
 Putting equations~\ref{eq:sk-g0-g1}--\ref{eq:sk-g4} together, we find
-\fixme{format prettily}
+\begingroup \splitright=4em minus 4em
 \begin{spliteqn}
-  \Adv{sk}{\Wident^{G, \E}}(A) \le \\
-     q_S \bigl( \InSec{mcdh}(G; t', q_K) +
-                n \cdot \InSec{mcdh}(G; t', q_M + q_I) +
-                \InSec{ind-cca}(\E; t', q_M, q_M) \bigr) + {}\\
-     \frac{n (n - 1)}{|G|} +
+  \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}
+\end{spliteqn} \endgroup
 The theorem follows, since $A$ was chosen arbitrarily.
 
 
@@ -3007,7 +3343,7 @@ The theorem follows, since $A$ was chosen arbitrarily.
      =   \frac{1}{2^{\ell_I}} \sum_\Cid \Ccount(\Cid)
      \le \frac{q_M}{2^{\ell_I}}
   \]
-  as required.  
+  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
@@ -3076,9 +3412,8 @@ The theorem follows, since $A$ was chosen arbitrarily.
     session state of $S$ or $T$ then $B$ stops the simulation abruptly and
     halts.
   \end{enumerate}
-  Adversary $B$'s running time is $t' = t + O(n) + O(q_S q_M) + O(q_I) +
-  O(q_K)$, and $B$ makes at most $q_K$ queries to $V(\cdot)$; we therefore
-  have
+  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}
@@ -3166,8 +3501,9 @@ The theorem follows, since $A$ was chosen arbitrarily.
   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$.  Finally, we issue no more that $q_M$
-  encryption or decryption queries.  Therefore,
+  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
@@ -3184,7 +3520,7 @@ The theorem follows, since $A$ was chosen arbitrarily.
   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$
@@ -3225,8 +3561,10 @@ The theorem follows, since $A$ was chosen arbitrarily.
   \item If $A$ reveals $S$ or corrupts $P_i$ or $P_j$ then $B'$ stops the
     simulation immediately and halts.
   \end{enumerate}
-  Clearly $B'$ succeeds whenever $F_7$ occurs; hence we can apply
-  theorem~\ref{thm:wident-sound}.  The claim follows.
+  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}
 
 
@@ -3235,7 +3573,7 @@ The theorem follows, since $A$ was chosen arbitrarily.
 
 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.  
+seem possible.
 
 We use the games and notation of section~\ref{sec:sk-proof}.
 
@@ -3265,9 +3603,91 @@ 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*}
+
 \end{document}
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
-%%% End: 
+%%% End: