wrestlers.tex: Let `\section' act as a section header in the source.

[doc/wrestlers] / wrestlers.tex

%%% -*-latex-*-
%%%
%%% The Wrestlers Protocol: secure, deniable key-exchange
%%%
%%% (c) 2006 Mark Wooding
%%%

\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[indentpar]{strayman}
  \usepackage[T1]{fontenc}
  \usepackage[palatino, helvetica, courier, maths=cmr]{mdwfonts}
  \usepackage[within = subsection, mdwmargin]{mdwthm}
  \usepackage{mdwlist}
  \usepackage{sverb}
  \ifpdfing\else
    \PassOptionsToPackage{dvips}{xy}
  \fi
\else
  \PassOptionsToClass{runningheads}{llncs}
  \documentclass{llncs}
\fi

\PassOptionsToPackage{show}{slowbox}
%\PassOptionsToPackage{hide}{slowbox}
\usepackage{mdwtab, mdwmath, crypto}
\usepackage{slowbox}
\usepackage{amssymb, amstext}
\usepackage{url, multicol}
\usepackage{tabularx}
\DeclareUrlCommand\email{\urlstyle{tt}}
\ifslowboxshow
  \usepackage[all]{xy}
  \turnradius{4pt}
\fi
\usepackage{mathenv}

\newcommand{\Nupto}[1]{\{0, 1, \ldots, #1 - 1\}}
\iffancystyle
  \let\next\title
\else
  \def\next[#1]{\titlerunning{#1}\title}
\fi
\next
  [The Wrestlers Protocol]
  {The Wrestlers Protocol%
    \ifshort\thanks{This is an extended abstract; the full version
      \cite{wooding-2006:wrestlers} is available from
      \texttt{http://eprint.iacr.org/2006/386/}.}\fi \\
    A simple, practical, secure, deniable protocol for key-exchange}
\iffancystyle
  \author{Mark Wooding \\ \email{mdw@distorted.org.uk}}
\else
  \author{Mark Wooding}
  \institute{\email{mdw@distorted.org.uk}}
\fi

\iffancystyle
  \bibliographystyle{mdwalpha}
  \let\epsilon\varepsilon
  \let\emptyset\varnothing
  \let\le\leqslant\let\leq\le
  \let\ge\geqslant\let\geq\ge
  \numberwithin{table}{section}
  \numberwithin{figure}{section}
  \numberwithin{equation}{subsection}
  \let\random\$
\else
  \bibliographystyle{splncs}
  \expandafter\let\csname claim*\endcsname\claim
  \expandafter\let\csname endclaim*\endcsname\endclaim
\fi

\let\Bin\Sigma
\let\emptystring\lambda
\edef\Pr{\expandafter\noexpand\Pr\nolimits}
\newcommand{\bitsto}{\mathbin{..}}
\newcommand{\E}{{\mathcal{E}}}
\newcommand{\M}{{\mathcal{M}}}
\iffancystyle
  \def\description{%
    \basedescript{%
      \let\makelabel\textit%
      \desclabelstyle\multilinelabel%
      \desclabelwidth{1in}%
    }%
  }
\fi
\def\fixme#1{\marginpar{FIXME}[FIXME: #1]}
\def\hex#1{\texttt{#1}_{x}}

\newenvironment{longproof}[1]{%
  \ifshort#1\expandafter\ignore
  \else\proof\fi
}{%
  \ifshort\else\endproof\fi
}

\def\dbox#1{%
  \vtop{%
    \def\\{\unskip\egroup\hbox\bgroup\strut\ignorespaces}%
    \hbox{\strut#1}%
  }%
}

\def\Wident{\Xid{W}{ident}}
\def\Wkx{\Xid{W}{kx}}
\def\Wdkx{\Xid{W}{dkx}}
\def\Func#1#2{\mathcal{F}[#1\to#2]}
\def\diff#1#2{\Delta_{#1, #2}}
\def\Hid{H_{\textit{ID}}}

%% protocol run diagrams
\def\PRaction#1{#1\ar[r]}
\def\PRcreatex#1{\PRaction{\textsf{Create session\space}#1}}
\def\PRcreate#1#2#3{\PRcreatex{(\text{#1},\text{#2},#3)}}
\def\PRreceivex#1{\PRaction{\textsf{Receive\space}#1}}
\def\PRreceive#1#2{\PRreceivex{\msg{#1}{#2}}}
\def\PRsession#1{\relax\mathstrut#1\ar[r]}
\def\msg#1#2{(\cookie{#1},#2)}
\def\PRresult#1{#1}
\def\PRsendx#1{\PRresult{\textsf{Send\space}#1}}
\def\PRsend#1#2{\PRsendx{\msg{#1}{#2}}}
\def\PRcomplete#1{\textsf{Complete:\space}#1}
\def\PRstate#1{\textsf{State:\space}#1}
\def\PRignore{\textsf{(ignored)}}
\def\PRreveal{\textsf{Session-state reveal}\ar[r]}
\def\protocolrun#1{\[\xymatrix @R=0pt @C=2em {#1}\]}

\def\protocol{%
  \unskip\bigskip
  \begin{tabular*}{\linewidth}%
    {@{\qquad}l@{\extracolsep{0ptplus1fil}}r@{\qquad}}}
\def\endprotocol{\end{tabular*}}
\def\send#1#2{\noalign{%
    \centerline{\xy\ar @{#1}|*+{\mathstrut#2}<.5\linewidth, 0pt>\endxy}}}

%% class-ids for proof of extractor lemma
\let\Cid=\Lambda
\let\Csession=S
\let\Cindex=r
\let\Cquery=Q
\let\Chash=H
\let\Ccheck=c
\let\Ccheckset=V
\let\Ccount=\nu

\def\HG#1{\mathbf{H}_{#1}}

\iffancystyle\else
  \let\xsssec\subsubsection\def\subsubsection#1{\xsssec[#1]{#1.}}
\fi

\begin{document}

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

\maketitle
\iffancystyle \thispagestyle{empty} \fi

\begin{abstract}
  We describe and prove (in the random-oracle model) the security of a simple
  but efficient zero-knowledge identification scheme, whose security is based
  on the computational Diffie--Hellman problem.  Unlike other recent
  proposals for efficient identification protocols, we don't need any
  additional assumptions, such as the Knowledge of Exponent assumption.

  From this beginning, we build a simple key-exchange protocol, and prove
  that it achieves `SK-security' -- and hence security in Canetti's Universal
  Composability framework.

  Finally, we show how to turn the simple key-exchange protocol into a
  slightly more complex one which provides a number of valuable `real-life'
  properties, without damaging its security.
\end{abstract}

\iffancystyle
\newpage
\thispagestyle{empty}
\columnsep=2em \columnseprule=0pt
\tableofcontents[\begin{multicols}{2}\raggedright][\end{multicols}]
%%\listoffigures[\begin{multicols}{2}\raggedright][\end{multicols}]
%% \listoftables[\begin{multicols}{2}\raggedright][\end{multicols}]
\newpage
\fi

%%%--------------------------------------------------------------------------
\section{Introduction}

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{stinson-wu-2006:two-flow-zero-knowledge}; 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{shoup-1999:formal-model-key-exchange} points out, it provides a `secure
ping', by which Bob can know that Alice is `there', but provides no guarantee
that any other communication was sent to or reached her.  However, there are
situations where this an authentic channel between two entities -- e.g., a
device and a smartcard -- where a simple identification protocol can still be
useful.

An authenticated key-exchange protocol lets Alice and Bob agree on a shared
secret, known to them alone, even if there is an enemy who can read and
intercept all of their messages, and substitute messages of her own.  Once
they have agreed on their shared secret, of course, they can use standard
symmetric cryptography techniques to ensure the privacy and authenticity of
their messages.


\subsection{Desirable properties of our protocols}

Our identification protocol has a number of desirable properties.
\begin{itemize}
\item It is \emph{simple} to understand and implement.  In particular, it
  requires only two messages.
\item It is fairly \emph{efficient}, requiring two scalar multiplications by
  each of the prover and verifier.
\item It is provably \emph{secure} (in the random oracle model), assuming the
  intractability of the computational Diffie--Hellman problem.
\end{itemize}

Our key-exchange protocol also has a number of desirable
properties.
\begin{itemize}
\item It is fairly \emph{simple} to understand and implement, though there
  are a few subtleties.  In particular, it is \emph{symmetrical}.  We have
  implemented a virtual private network system based on this protocol.
\item It is \emph{efficient}, requiring four scalar multiplications by each
  participant.  The communication can be reduced to three messages by
  breaking the protocol's symmetry.
\item It is provably \emph{secure} (again, in the random oracle model),
  assuming the intractability of the computational Diffie--Hellman problem,
  and the security of a symmetric encryption scheme.
\item It provides \emph{perfect forward secrecy}.  That is, even if a user's
  long-term secrets are compromised, past sessions remain secure.
\item It is \emph{deniable}.  It is possible to construct simulated
  transcripts of protocol executions between any number of parties without
  knowing any of their private keys.  The simulated transcripts are (almost)
  indistinguishable from real protocol transcripts.  Hence, a transcript
  does not provide useful evidence that a given party was really involved in
  a given protocol execution.
\end{itemize}

\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{koblitz-menezes-2006:another-look-provable-security-ii} (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:security-cbc,bellare-1995:xor-macs,%
bellare-rogaway-1995:oaep,bellare-rogaway-1996:exact-security-sigs,%
bellare-1996:hmac,bellare-1997:concrete-symmetric}; see also
\cite{bellare-1999:practice-oriented-provable-security}.
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:logic-authn}) was given by Bellare and Rogaway
\cite{bellare-rogaway-1994:entity-authn-key-distrib}; the model has since
been enhanced, both by the original authors and others, in
\cite{bellare-rogaway-1995:session-key-distrib,%
  blake-wilson-1997:key-agreement,%
  blake-wilson-menezes-1998:asymm-key-transport}.
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:modular-key-exchange} and
\cite{shoup-1999:formal-model-key-exchange}; 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.  The idea of using formal methods to analyse key-exchange protocols
begins with the logic of Burrows, Abadi and Needham
\cite{burrows-1989:logic-authn}.  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-rogaway-1994:entity-authn-key-distrib}
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-rogaway-1995:session-key-distrib} to study three-party
protocols involving a trusted key-distribution centre.

Blake-Wilson, Johnson and Menezes \cite{blake-wilson-1997:key-agreement}
applied the model of \cite{bellare-rogaway-1994:entity-authn-key-distrib} to
key-exchange protocols using asymmetric cryptography, and Blake-Wilson and
Menezes \cite{blake-wilson-menezes-1998:asymm-key-transport} applied it to
protocols based on the Diffie-Hellman protocol.

The security notion of \cite{bellare-rogaway-1994:entity-authn-key-distrib}
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:modular-key-exchange}
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{shoup-1999:formal-model-key-exchange}, Shoup presents a new model
for key-exchange, also based on the idea of simulation.  He analyses the
previous models, particularly
\cite{bellare-rogaway-1994:entity-authn-key-distrib} and
\cite{bellare-1998:modular-key-exchange}, and highlights some of their inadequacies.

\fi

Canetti and Krawczyk
\cite{canetti-krawczyk-2001:secure-channels-eprint,%
  canetti-krawczyk-2001:secure-channels}
describe a new notion of security in the model of
\cite{bellare-1998:modular-key-exchange}, based on the challenge-session
notion of \cite{bellare-rogaway-1994:entity-authn-key-distrib}.  The security
notion, called `SK-security', seems weaker in various ways than those of
earlier works such as \cite{bellare-rogaway-1994:entity-authn-key-distrib} or
\cite{shoup-1999:formal-model-key-exchange}.  However, the authors show that
their notion suffices for constructing `secure channel' protocols, which they
also define.

\ifshort\else In \cite{canetti-2001:uc-security-eprint,%
  canetti-2001:uc-security},
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:modular-key-exchange} and
\cite{shoup-1999:formal-model-key-exchange}, 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-krawczyk-2002:uc-key-exchange} show that
the SK-security notion of \cite{canetti-krawczyk-2001:secure-channels} is
\emph{equivalent} to a `relaxed' notion of key-exchange security in the UC
framework\ifshort\space of \cite{canetti-2001:uc-security}\fi, and suffices
for the construction of UC secure channels.

The result of \cite{canetti-krawczyk-2002:uc-key-exchange} gives us
confidence that SK-security is the `right' notion of security for
key-exchange protocols.  Accordingly, SK-security is the standard against
which we analyse our key-exchange protocol.


\subsection{Outline of the paper}

The remaining sections of this paper are as follows.
\begin{itemize}
\item Section \ref{sec:prelim} provides the essential groundwork for the rest
  of the paper.  It introduces important notation, and describes security
  notions and intractability assumptions.
\item Section \ref{sec:zk-ident} describes our zero-knowledge identification
  protocol and proves its security.
\item Section \ref{sec:kx} describes the simple version of our key-exchange
  protocol, and proves its security and deniability.  It also describes some
  minor modifications which bring practical benefits without damaging
  security.
\item Finally, section \ref{sec:conc} presents our conclusions.
\end{itemize}

\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-franklin-2003:ibe-weil-pairing}.  It also contains proofs of the
various theorems stated here.
\fi

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

\ifshort
\subsection{Basics}
\let\prelimsec\subsubsection
\else
\let\prelimsec\subsection
\fi

\prelimsec{Miscellaneous notation}

We write $\#S$ for the cardinality of a set $S$.  We write $\Func{D}{R}$ for
the set of all functions with domain $D$ and range $R$.

\prelimsec{Groups}

Let $(G, +)$ be a cyclic group\footnote{
  We find that additive group notation is easier to read.  In particular, in
  multiplicative groups, one ends up with many interesting things tucked away
  in little superscripts.}%
of prime order $q$, and generated by an element $P$.  We shall write the
identity of $G$ as $0_G$, or simply as $0$ when no ambiguity is likely to
arise.  Thus, we have $\langle P \rangle = G$ and $q P = 0$.  Any $X \in G$
can be written as $X = x P$ for some $x \in \{0, 1, \ldots, q - 1\}$.

We consider a cyclic group of order $n$ as a $\Z/n\Z$-module, and in
particular our group $G$ can be seen as a vector space over $\gf{q}$.  This
makes the notation slightly more convenient.

\prelimsec{Bit strings and encodings}
\label{sec:bitenc}

Let $\Bin = \{0, 1\}$ be the set of binary digits.  Then $\Bin^n$ is the set
of $n$-bit strings, and $\Bin^*$ the set of all (finite) bit strings.  If $x
\in \Bin^n$ is a bit string, we write its length as $|x| = n$.  For a bit
string $x \in \Bin^n$, and for $0 \le i < n$, we write $x[i]$ as the $i$th
bit of $x$.  The empty string is denoted $\emptystring$.

Let $x$ and $y$ be two bit strings.  If $|x| = |y| = n$, we write $x \xor y$
to mean the bitwise exclusive-or of $x$ and $y$\ifshort\else: if $z = x \xor
y$ then $|z| = n$, and $z[i] = (x[i] + y[i]) \bmod 2$ for $0 \le i < n$\fi.
We write $x \cat y$ to mean the concatenation of $x$ and $y$\ifshort\else: if
$z = x \cat y$ then $|z| = |x| + |y|$ and $z[i] = x[i]$ if $0 \le i < |x|$
and $z[i] = y[i - |x|]$ if $|x| < i \le |x| + |y|$\fi.

Finally, we let $\bot$ be a value distinct from any bit string.

We shall want to encode group elements $X \in G$ and indices $x \in I =
\gf{q}$ as bit strings.
\ifshort
To this end, we shall assume the existence of efficient, unambiguous
encodings of group elements as $\ell_G$-bit strings, and indices as
$\ell_I$-bit strings.  To reduce clutter, we shall leave encoding and
decoding as implicit operations.
\else
To this end, we shall assume the existence of
integers $\ell_G, \ell_I > 0$ and functions
\[
  e_S\colon S \to \Bin^{\ell_S}
  \quad \textrm{and} \quad
  d_S\colon \Bin^{\ell_S} \to S \cup \{ \bot \}
  \qquad
  \textrm{for } S \in \{ G, \F \}.
\]
with the following properties.
\begin{itemize}
\item The functions are \emph{unique} and \emph{unambiguous}, i.e., for any
  $t \in \Bin^{\ell_S}$, we have
  \[ d_S(t) = \begin{cases}
       s & if there is some $s \in S$ such that $t = e_S(s)$, or \\
       \bot & if no such $s$ exists.
  \end{cases}
  \]
\item The functions should be \emph{efficient} to compute.  Indeed, we shall
  be assuming that the time taken for encoding and decoding is essentially
  trivial.
\end{itemize}
Note that, as we have defined them, all encodings of group elements are the
same length, and similarly for encodings of indices.  This is necessary for
the security of our protocols.

We shall frequently abuse notation by omitting the encoding and decoding
functions where it is obvious that they are required.
\fi

\ifshort\else
\prelimsec{Games, adversaries, and oracles}
\label{sec:games}

Many of the security definitions and results given here make use of
\emph{games}, played with an \emph{adversary}.  An adversary is a
probabilistic algorithm.  In some games, the adversary is additionally
equipped with \emph{oracles}, which perform computations with values chosen
by the adversary and secrets chosen by the game but not revealed to the
adversary.  We impose limits on the adversary's resource usage: in
particular, the total time it takes, and the number of queries it makes to
its various oracles.  Throughout, we include the size of the adversary's
program as part of its `time', in order to model adversaries which contain
large precomputed tables.

The games provide models of someone trying to attack a construction or
protocol.  For security, we will either define a notion of `winning' the
game, and require that all adversaries have only a very small probability of
winning, or we consider two different games and require that no adversary can
distinguish between the two except with very small probability.

Our proofs make frequent use of sequences of games; see
\cite{bellare-rogaway-2006:triple-enc,shoup-2004:sequences-of-games}.
The presentation owes much to Shoup \cite{shoup-2004:sequences-of-games}.  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:oaep-reconsidered} will be
frequently useful.
\begin{lemma}[Difference Lemma]
  \label{lem:shoup}
  Let $S$, $T$, $F$ be events.  Suppose $\Pr[S \mid \bar F] =
  \Pr[T \mid \bar F]$.  Then $|\Pr[S] - \Pr[T]| \le \Pr[F]$.
\end{lemma}
\begin{proof}
  A simple calculation:
  \begin{eqnarray*}[rl]
    |\Pr[S] - \Pr[T]|
    & = |(\Pr[S \mid F]\Pr[F] + \Pr[S \mid \bar F]\Pr[\bar F]) -
         (\Pr[T \mid F]\Pr[F] + \Pr[T \mid \bar F]\Pr[\bar F])| \\
    & = \Pr[F] \cdot |\Pr[S \mid F] - \Pr[T \mid F]| \\
    & \le \Pr[F]
  \end{eqnarray*}
  and we're done!
\end{proof}
\fi


\prelimsec{The random oracle model}
\label{sec:ro}

\ifshort\else
In particular, most of our results will make use of the \emph{random oracle}
model \cite{bellare-rogaway-1993:random-oracles}, in which all the
participants, including the adversary, have access to a number of `random
oracles'.  A random oracle with domain $D$ and range $R$ is an oracle which
computes a function chosen uniformly at random from the set of all such
functions.  (In the original paper
\cite{bellare-rogaway-1993:random-oracles}, random oracles are considered
having domain $\Bin^*$ and range $\Bin^\omega$; we use finite random oracles
here, because they're easier to work with.)

Given a protocol proven secure in the random oracle model, we can instantiate
each random oracle by a supposedly-secure hash function and be fairly
confident that either our protocol will be similarly secure, or one of the
hash functions we chose has some unfortunate property.

Proofs in the random oracle must be interpreted carefully.  For example,
Canetti, Goldreich and Halevi \cite{canetti-2004:rand-oracle-revisit} show
that there are schemes which can be proven secure in the random oracle model
but provably have no secure instantiation in the standard model.
\fi

The random oracle model \ifshort\cite{bellare-rogaway-1993:random-oracles}
\fi is useful for constructing reductions and simulators for two main
reasons.
\begin{enumerate}
\item One can use the transcript of an adversary's queries to random oracles
  in order to extract knowledge from it.
\item One can `program' a random oracle so as to avoid being bound by prior
  `commitments', or to guide an adversary towards solving a selected instance
  of some problem.
\end{enumerate}
Our proofs only make use of the first feature.  This becomes particularly
important when we consider issues of zero-knowledge and deniability in a
concurrent setting, because we want to be able to claim that we retain these
features when the random oracle is instantiated using a cryptographic hash
function, and hash functions definitely aren't `programmable' in this way!
The former property seems rather more defensible -- one would indeed hope
that the only sensible way of working out (anything about) the hash of a
particular string is to actually compute the hash function, and the random
oracle model is, we hope, just giving us a `hook' into this process.

\ifshort\else
(Our protocols can be modified to make use of bilinear pairings so as to
provide identity-based identification and key-exchange, using the techniques
of \cite{boneh-franklin-2003:ibe-weil-pairing}.  Proving the security of the
modifications we discuss would involve `programming' random oracles, but this
doesn't affect the zero-knowledge or deniability of the resulting protocols.)
\fi


\ifshort\else
\prelimsec{Notation for algorithms}

We shall have occasion to describe algorithms by means of a pseudocode.  Our
choice of pseudocode is unlikely to be particularly controversial.  We let $x
\gets y$ denote the action of setting $x$ to the value $y$; similarly, $x
\getsr Y$ denotes the action of sampling $x$ from the set $Y$ uniformly at
random.

The expression $a \gets A^{O(\cdot, x)}(y)$ means `assign to $a$ the value
output by algorithm $A$ on input $y$, and with oracle access to the algorithm
which, given input $z$, computes $O(z, x)$'.

We make use of conditional (\IF-\ELSE) and looping (\FOR-\DO and \WHILE-\DO)
constructions; in order to reduce the amount of space taken up, the bodies of
such constructions are shown by indentation only.

We don't declare the types of our variables explicitly, assuming that these
will be obvious by inspection; also, we don't describe our variables' scopes
explicitly, leaving the reader to determine these from context.

Finally, the notation $\Pr[\textit{algorithm} : \textit{condition}]$ denotes
the probability that \textit{condition} is true after running the given
\textit{algorithm}.
\fi

\prelimsec{Diffie-Hellman problems}
\label{sec:dhp}

The security of our protocols is related to the hardness of the
computational, decisional, and gap Diffie-Hellman problems in the group $G$.
We define these problems and what it means for them to be `hard' here.

The \emph{computational} Diffie-Hellman problem (CDH) is as follows: given
two group elements $X = x P$ and $Y = y P$, find $Z = x y P$.
\ifshort\else
\begin{definition}[The computational Diffie-Hellman problem]
  Let $(G, +)$ be a cyclic group generated by $P$.  For any adversary $A$, we
  say that $A$'s \emph{success probability} at solving the computational
  Diffie-Hellman problem in $G$ is
  \[ \Succ{cdh}{G}(A) =
      \Pr[ x \getsr I; y \getsr \Z/\#G\Z : A(x P, y P) = x y P ]
  \]
  where the probability is taken over the random choices of $x$ and $y$ and
  any random decisions made by $A$.  We say that the \emph{CDH insecurity
  function} of $G$ is
  \[ \InSec{cdh}(G; t) = \max_A \Succ{cdh}{G}(A) \]
  where the maximum is taken over adversaries which complete in time $t$.
\end{definition}
Certainly, if one can compute discrete logarithms in the group $G$ (i.e.,
given $x P$, find $x$), then one can solve the computational Diffie-Hellman
problem.  The converse is not clear, though.  Shoup
\cite{shoup-1997:dh-lower-bounds} gives us some confidence in the difficulty
of the problem by showing that a \emph{generic} adversary -- i.e., one which
makes no use of the specific structure of a group -- has success probability
no greater than $q^2/\#G$.

This isn't quite sufficient for our purposes.  Our proofs will be able to
come up with (possibly) a large number of guesses for the correct answer, and
at most one of them will be correct.  Unfortunately, working out which one is
right seems, in general, to be difficult.  This is the \emph{decision}
Diffie-Hellman problem (DDH), which \cite{shoup-1997:dh-lower-bounds} shows,
in the generic group model, is about as hard as CDH.  (See
\cite{boneh-1998:ddh} for a survey of the decision Diffie-Hellman problem.)
\par\fi
Our reference problem will be a `multiple-guess computational Diffie-Hellman
problem' (MCDH), which is captured by a game as follows.  An adversary is
given a pair of group elements $(x P, y P)$, and an oracle $V(\cdot)$ which
accepts group elements as input.  The adversary wins the game if it queries
$V(x y P)$.

\begin{figure}
  \begin{program}
    $\Game{mcdh}{G}(A)$: \+ \\
      $w \gets 0$; \\
      $x \getsr \Z/\#G\Z$; $y \getsr \Z/\#G\Z$; \\
      $A^{V(\cdot)}(x P, y P)$; \\
      \RETURN $w$;
    \next
    Function $V(Z)$: \+ \\
      \IF $Z = x y P$ \THEN \\ \ind
        $w \gets 1$; \\
        \RETURN $1$; \- \\
      \RETURN $0$;
  \end{program}

  \caption{The multiple-guess computational Diffie-Hellman problem:
    $\Game{mcdh}{G}(A)$}
  \label{fig:mcdh}
\end{figure}

\begin{definition}[The multiple-guess computational Diffie-Hellman problem]
  \label{def:mcdh}
  Let $(G, +)$ be a cyclic group generated by $P$.  For some adversary $A$,
  we say that $A$'s \emph{success probability} at solving the multiple-guess
  computational Diffie-Hellman problem in $G$ is
  \[ \Succ{mcdh}{G}(A) = \Pr[\Game{mcdh}{G}(A) = 1] \]
  where $\Game{mcdh}{G}(A)$ is shown in figure~\ref{fig:mcdh}.  We say that
  the \emph{MCDH insecurity function of $G$} is
  \[ \InSec{mcdh}(G; t, q_V) = \max_A \Succ{mcdh}{G}(A) \]
  where the maximum is taken over adversaries which complete in time $t$ and
  make at most $q_V$-oracle queries.
\end{definition}
\ifshort
We can (loosely) relate the difficulty of MCDH to the difficulty of
the standard CDH problem, in which the adversary is allowed only a single
guess.
\else
Note that our MCDH problem is not quite the `gap Diffie-Hellman problem'
(GDH).  The gap problem measures the intractibility of solving CDH even with
the assistance of an oracle for solving (restricted) decision Diffie-Hellman
problems in the group.  Specifically, the adversary is given $(X, Y) = (x P,
y P)$ and tries to find $Z = x y P$, as for CDH, but now it has access to an
oracle $D(R, S)$ which answers $1$ if $S = x R$ and $0$ otherwise.

Clearly MCDH is at least as hard as GDH, since our simple verification oracle
$V(Z)$ can be simulated with the gap problem's DDH oracle, as $D(Y, Z)$.
However, we can (loosely) relate the difficulty of MCDH to the difficulty of
CDH.
\fi
\begin{proposition}[Comparison of MCDH and CDH security]
  For any cyclic group $(G, +)$,
  \[ \InSec{mcdh}(G; t, q_V) \le
       \ifshort q_V\,\InSec{mcdh}(G; t + O(q_V), 1) \else
                q_V\,\InSec{cdh}(G; t + O(q_V)) \fi.
  \]
\end{proposition}
\begin{longproof}{The proof of this proposition may be found in the full
    version of this paper.}
  Let $A$ be an adversary attacking the multiple-guess computational
  Diffie-Hellman problem in $G$, and suppose that it runs in time $t$ and
  issues $q_V$ queries to its verification oracle.

  We use a sequence of games.  Game $\G0$ is the original MCDH attack game.
  In each game $\G{i}$, we let the event $S_i$ be the probability that the
  adversary wins the game.

  Game $\G1$ is the same as $\G0$, except that we change the behaviour of the
  verification oracle.  Specifically, we make the oracle always return $0$.
  We claim that this doesn't affect the adversary's probability of winning,
  i.e., $\Pr[S_1] = \Pr[S_0]$.  To see this, note that if none of the
  adversary's $V(\cdot)$ queries was correct, then there is no change in the
  game; conversely, if any query was correct, then the adversary will have
  won regardless of its subsequent behaviour (which may differ arbitrarily
  between the two games).

  We are now ready to construct from $A$ an adversary $B$ attacking the
  standard computational Diffie-Hellman problem.
  \begin{program}
    Adversary $B(X, Y)$: \+ \\
      $n \gets 0$; \\
      \FOR $i \in \Nupto{q_V}$ \DO $Q_i \gets 0$; \\
      $A^{V(\cdot)}$; \\
      $r \getsr \Nupto{n}$; \\
      \RETURN $Q_r$;
    \next
    Function $D(Z')$: \+ \\
      $Q_n \gets Z'$; \\
      $n \gets n + 1$; \\
      \RETURN $0$;
  \end{program}
  Observe that $B$ provides $A$ with an accurate simulation of game $\G1$.
  Moreover, at the end of the algorithm, we have $0 < n \le q_V$, and the
  values $Q_0$, $Q_1$, \dots, $Q_{n-1}$ are the values of $A$'s oracle
  queries.  Hence, with probability $Pr[S_1]$, at least of one of the $Q_i$
  is the correct answer to the CDH problem.  Let $\epsilon = \Pr[S_1] =
  \Pr[S_0]$; we claim that $B$'s probability of success is at least
  $\epsilon/q_V$.  The proposition follows directly from this claim and that,
  because $A$ was chosen arbitrarily, we can maximize and count resources.

  We now prove the above claim.  For $0 \le i < q_V$, let $W_i$ be the
  event that $Q_i = x y P$, i.e., that $Q_i$ is the correct response.  A
  simple union bound shows that
  \[ \sum_{0\le i<j} \Pr[W_i \mid n = j] \ge \epsilon. \]
  We now perform a calculation:
  \begin{eqnarray*}[rl]
    \Succ{cdh}{G}(B)
    & =  \sum_{0\le i<q_V} \Pr[W_i \land r = i] \\
    & =  \sum_{0<j\le q_V} \Pr[n = j]
         \biggl( \sum_{0\le i<j} \Pr[W_i \land r = i \mid n = j] \biggr) \\
    & =  \sum_{0<j\le q_V} \Pr[n = j]
         \biggl( \frac{1}{j} \sum_{0\le i<j} \Pr[W_i \mid n = j] \biggr) \\
    &\ge \sum_{0<j\le q_V} \Pr[n = j] \frac{\epsilon}{j} \\
    &\ge \frac{\epsilon}{q_V} \sum_{0<j\le q_V} \Pr[n = j] \\
    & =  \frac{\epsilon}{q_V}.
  \end{eqnarray*}
  which completes the proof.
\end{longproof}

\ifshort\else
\prelimsec{Example groups and encodings}

For nonnegative integers $0 \le n < 2^\ell$, there is a natural binary
encoding $N_\ell\colon \Nupto{2^\ell} \to \Bin^\ell$ which we can define
recursively as follows.
\[ N_0(0) = \emptystring \qquad
   N_\ell(n) = \begin{cases}
     N_{\ell-1}(n) \cat 0              & if $0 \le n < 2^{\ell-1}$ \\
     N_{\ell-1}(n - 2^{\ell-1}) \cat 1 & if $2^{\ell-1} \le n < 2^\ell$.
   \end{cases}
\]
Given an encoding $a = N_\ell(n)$ we can recover $n$ as
\[ n = \sum_{0\le i<\ell} a[i] 2^i. \]
Hence, given some limit $L \le 2^\ell$, we can encode elements of $\Nupto{L}$
using the functions $(e, d)$:
\[ e(L, \ell, n) = N_\ell(n) \qquad
   d(L, \ell, a) = \begin{cases}
     N_\ell(a) & if $N_\ell(a) < L$ \\
     \bot      & otherwise
   \end{cases}
\]
The reader can verify that the functions $e(L, \ell, \cdot)$ and $d(L, \ell,
\cdot)$ satisfy the requirements of section~\ref{sec:bitenc}.

Given some $q$ with $q < 2^{\ell_I}$, then, we can define an encoding
$(e_\F, d_\F)$ by $e_\F(n) = e(q, \ell_I, n)$ and $d_\F(a) = d(q, \ell_I,
a)$.

Let $p$ and $q$ be primes, with $q \mid (p - 1)$.  Then there is an order-$q$
subgroup of $\F_p^*$.  In practice, an order-$q$ element can be found easily
by taking elements $h \in \F_p^*$ at random and computing $g = h^{(p-1)/2}$
until $g \ne 1$; then $G = \langle g \rangle$ is a group of $q$ elements.
Assuming that $p$ and $q$ are sufficiently large, the Diffie-Hellman problems
seem to be difficult in $G$.  Some texts recommend additional restrictions on
$p$, in particular that $(p - 1)/2q$ be either prime or the product of large
primes.  Primes of this form protect against small-subgroup attacks; but our
protocols are naturally immune to these attacks, so such precautions are
unnecessary here.  Elements of $G$ can be encoded readily, since each element
$n + p\Z$ of $\F_p = \Z/p\Z$ has an obvious `representative' integer $n$ such
that $0 \le n < p$, and given $2^{\ell_G} > p$, we can encode $n$ as $e(p,
\ell_G, n)$, as above.

Alternatively, let $\F = \gf{p^f}$ be a finite field, and $E$ be an elliptic
curve defined over $\F$ such that the group $E(\F)$ of $\F$-rational points
of $E$ has a prime-order cyclic subgroup $G$.  Elements of $G$ can be
represented as pairs of elements of $\F$.  If $f = 1$, i.e., $\F = \Z/p\Z$
then field elements can be encoded as above.  If $p = 2$, we can represent
the field as $\F_2/(p(x))$ for some irreducible polynomial $p(x) \in \F_2[x]$
of degree $f$.  An element $r \in \F$ can then be represented by a polynomial
$r(x)$ with degree less than $f$, and coefficients $c_i \in \{0, 1\}$, i.e.,
\[ r(x) = \sum_{0\le i<f} c_i x^i \]
and hence we can uniquely encode $r$ as an $f$-bit string $a$ such that $a[i]
= c_i$.
\fi


\prelimsec{Symmetric encryption}
\label{sec:sym-enc}

Our key-exchange protocol requires a symmetric encryption scheme.  Our
definition is fairly standard, except that, rather than specifying a
key-generation algorithm, we assume that key generation simply involves
selecting a string of a given length uniformly at random.
\begin{definition}[Symmetric encryption schemes]
  A \emph{symmetric encryption scheme} $\E = (\kappa, E, D)$ consists of:
  \begin{itemize}
  \item an integer $\kappa \ge 0$,
  \item a randomized \emph{encryption algorithm} $E$ which, on input $K \in
    \Bin^\kappa$ and $p \in \Bin^*$ outputs some $c \in \Bin^*$, written $c
    \gets E_K(p)$;
  \item a \emph{decryption algorithm} $D$ which, on input $K \in \Bin^\kappa$
    and $c \in \Bin^*$ outputs some $p' \in \Bin^* \cup \{\bot\}$, written
    $p' \gets D_K(c)$.
  \end{itemize}
  Furthermore, a symmetric encryption scheme must be \emph{sound}: that is,
  if $c \gets E_K(p)$ for some $K \in \Bin^\kappa$ and $p \in \Bin^*$, and
  $p' \gets D_K(c)$ then $p = p'$.
\end{definition}
Our security notion for symmetric encryption is the standard notion of
left-or-right indistinguishability of ciphertexts under chosen-ciphertext
attack.
\begin{definition}[IND-CCA]
  \label{def:ind-cca}
  Let $\E = (\kappa, E, D)$ be a symmetric encryption scheme, and $A$ be an
  adversary.  Let $\id{lr}_b(x_0, x_1) = x_b$ for $b \in \{0, 1\}$.  Let
  \[ P_b =
     \Pr[K \getsr \Bin^\kappa;
         b \gets A^{E_K(\id{lr}_b(\cdot, \cdot)), D_K(\cdot)}() :
	 b = 1]
  \]
  An adversary is \emph{valid} if
  \begin{itemize}
  \item for any query to its encryption oracle $E_K(\id{lr}_b(x_0, x_1))$ we
    have $|x_0| = |x_1|$, and
  \item no query to the decryption oracle $D_K(\cdot)$ is equal to any reply
    from an encryption query.
  \end{itemize}
  If $A$ is valid, then we define its \emph{advantage} in attacking the
  security of $\E$ as follows
  \[ \Adv{ind-cca}{\E} = P_1 - P_0. \]
  Further, we define the \emph{IND-CCA insecurity function of $\E$} to be
  \[ \InSec{ind-cca}(\E; t, q_E, q_D) = \max_A \Adv{ind-cca}{\E}(A) \]
  where the maximum is taken over all valid adversaries $A$ which run in time
  $t$, and issue at most $q_E$ encryption and $q_D$ decryption queries.
\end{definition}


\subsection{Simulations}
\label{sec:sim}

In section~\ref{sec:zk-ident}, we shall prove that our identification
protocol is zero-knowledge; in section~\ref{sec:denial}, we show that our
key-exchange protocol is deniable.  In both of these proofs, we shall need to
demonstrate \emph{simulatability}.

\ifshort

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$,
which we shall represent as a probabilistic algorithm.  The world may in fact
represent a number of honest parties communicating in a concurrent fashion,
but we can consider them as a single algorithm for our present purposes.

Initially the world and the adversary are both given the same \emph{common
input}~$c$; in addition, the world is given a \emph{private input}~$w$.
Both $c$ and~$w$ are computed by an \emph{initialization function}~$I$, which
is considered to be part of the definition of the game.  Finally, the
adversary decides somehow that it has finished interacting, and outputs a
value~$a$.  All this we notate as
\[ (w, c) \gets I(); a \gets A^{W(w, c)}(c). \]
This game is \emph{simulatable} if there is an algorithm~$S$ -- the
\emph{simulator} -- which can compute the same things as~$A$, but all by
itself without interacting with the world.  That is, we run the simulator on
the common input~$c$, allowing it to interact in some way with the
adversary~$A$, and finally giving us an output~$s$.
\[ (w, c) \gets I(); s \gets S^A(c). \]
We shall say that the simulator is \emph{effective} if it's difficult to tell
whether a given string was output by the adversary after interacting with the
world, or by the simulator running by itself.  That is, for any algorithm~$D$
-- a \emph{distinguisher} -- running in some bounded amount of time, its
advantage
\begin{spliteqn*}
  \Pr[(w, c) \gets I(); a \gets A^{W(w, c)}(c);
        b \gets D(c, a) : b = 1] - {} \\
  \Pr[(w, c) \gets I(); s \gets S^A(c); b \gets D(c, s) : b = 1]
\end{spliteqn*}
is small.  (Note that we gave the distinguisher the common input as well as
the output of the adversary or the simulator.)

It's usual to study \emph{transcripts} of interactions in these kinds of
settings.  We are considering arbitrary adversarial outputs here, so this
certainly includes adversaries which output a transcript of their
interactions.  Indeed, for any adversary~$A$, we could construct an
adversary~$A_T$ which performs the same computation, and outputs the same
result, but also includes a complete transcript of $A$'s interaction with the
world.  Therefore we're just providing additional generality.

\subsubsection{Random oracles}
We shall be considering interactions in which all the parties have access to
several random oracles.  We could simply say that the random oracles are part
of the world~$W$.  In the setting described above, only the adversary
actually interacts with the world (and therefore would be able to query
random oracles).  The simulator would be forced to `make up' its own random
oracle, and the distinguisher would have to study the distributions of the
random-oracle queries and their responses to make up its mind about which it
was given.

However, this would be a poor model for the real world, since once we
instantiate the random oracle with a hash function, we know that everyone
would in actually be able to compute the hash function for themselves.  Thus
a distinguisher in the real world would be able to tell the difference
immediately between a real interaction and the simulated transcript, since
the `random oracle' queries recorded in the latter would be wrong!

Therefore we decide not to include the random oracles as part of the world,
but instead allow all the participants -- adversary, simulator and
distinguisher -- access to them.  If we denote by~$\mathcal{H} = (H_0, H_1,
\ldots, H_{n-1})$ the collection of random oracles under consideration, the
expression for the distinguisher's advantage becomes
\begin{spliteqn*}
  \Pr[(w, c) \gets I(); a \gets A^{W(w, c), \mathcal{H}}(c);
        b \gets D^{\mathcal{H}}(c, a) : b = 1] - {} \\
  \Pr[(w, c) \gets I(); s \gets S^{A, \mathcal{H}}(c);
        b \gets D^{\mathcal{H}}(c, s) : b = 1].
\end{spliteqn*}

\subsubsection{Auxiliary inputs}
If an adversary's output can be effectively simulated, then we can
confidently state that the adversary `learnt' very little of substance from
its interaction, and certainly very little it can \emph{prove} to anyone
else.  However, as we have described the setting so far, we fix an adversary
before we choose inputs to the world, so our model says little about what an
adversary which has already acquired some knowledge might learn beyond that.
For example, an adversary might overhear some other conversation between
honest parties and be able to use this to its advantage.

To this end, we give the adversary an \emph{auxiliary input}~$u$, computed by
an algorithm~$U$.  We give $U$ both $c$ and $w$, in order to allow the
adversary to gain some (possibly partial) knowledge of the secrets of the
other parties.  We also allow $U$ access to the random oracles~$\mathcal{H}$,
because clearly in the `real world' it would be ridiculous to forbid such an
algorithm from computing a publicly-known hash function.

The simulator and distinguisher are also given the auxiliary input.  The
simulator is meant to represent the adversary's ability to compute things on
its own, without interacting with the world, and since the adversary is given
the auxiliary input, the simulator must be too.  The distinguisher must be
given the auxiliary input because otherwise the simulator could just `make
up' plausible-looking inputs.

\fi

\ifshort
Because we're interested in a concrete, quantitative analysis, we must
constrain the resource usage of the various algorithms described above.
Specifically, we shall be interested in
\else

\subsubsection{Resource limits}
We shall not allow our algorithms to perform completely arbitrary
computations and interactions.  Instead, we impose limits on the amount of
time they are allowed to take, the number of random-oracle queries they make,
and so on.  Specifically, we are interested in
\fi
\begin{itemize}
\item the time $t_A$ taken by the adversary and $t_D$ taken by the
  distinguisher,
\item the number of oracle queries $\mathcal{Q}_A = (q_{A,0}, q_{A,1},
  \ldots, q_{A,n-1})$ made by the adversary, and $\mathcal{Q}_D$ made by the
  distinguisher,
\item a number of resource bounds $\mathcal{R}$ on the adversary's
  interaction with the world (e.g., number of messages of various kinds sent
  and received), and
\item a number of bounds $\mathcal{U}$ on the contents of the adversary's
  auxiliary input~$u$.
\end{itemize}
Sometimes we shall not be interested in proving simulatability of adversaries
with auxiliary inputs.  We write $\mathcal{U} = 0$ to indicate that auxiliary
input is not allowed.

\ifshort\else

\subsubsection{World syntax}
It will be worth our while being more precise about what a `world' actually
is, syntactically.  We define a world to be a single, randomized algorithm
taking inputs $(\iota, \sigma, \tau, \mu) \in (\Bin^*)^4$; the algorithm's
output is a pair $(\sigma', \rho) \in (\Bin^*)^2$.  We show how the
adversary's interaction is mapped on to this world algorithm in
figure~\ref{fig:sim-world}.
\begin{itemize}
\item The `input' $\iota$ is the result of the initialization function~$I$.
  That is, it is the pair $(w, c)$ of the world's private input and the
  common input.
\item The `state' $\sigma$ is empty on the world's first invocation; on each
  subsequent call, the value of the world's output $\sigma'$ is passed back.
  In this way, the world can maintain state.
\item The `type $\tau$ is a token giving the type of invocation this is.
\item The `message' $\mu$ is any other information passed in; its form will
  typically depend on the type~$\tau$ of the invocation.
\item The `new state' $\sigma'$ is the value of $\sigma$ to pass to the next
  invocation of the world.
\item The `reply $\rho$ is the actual output of the invocation.
\end{itemize}
There are two special invocation types.  The adversary is \emph{forbidden}
from making special invocations.
\begin{itemize}
\item The special invocation type $\cookie{init}$ is used to allow the world to
  prepare an initial state.  The world is invoked as
  \[ W^{\mathcal{H}}(\iota, \emptystring, \cookie{init}, \emptystring) \]
  and should output an initial state $\sigma'$.  The world's reply $\rho$ is
  ignored.  (Recall that $\emptystring$ represents the empty string.)
\item The special invocation type $\cookie{random}$ is used to inform the
  world that the adversary has issued a random oracle query.  The world is
  invoked as
  \[ W^{\mathcal{H}}(\iota, \sigma, \cookie{random}, (i, x, h)) \]
  to indicate that the adversary has queried its random oracle $H_i(\cdot)$
  on the input $x$, giving output~$h$.  The world may output an updated state
  $\sigma'$; its reply $\rho$ is ignored.
\end{itemize}
The latter special query is a technical device used to allow the `fake-world'
simulators we define below to be aware of the adversary's random oracle
queries without being able to `program' the random oracle.  Including it here
does little harm, and simplifies the overall exposition.

\begin{figure}
  \begin{program}
    Interaction $A^{W(w, c), \mathcal{H}}(c, u)$: \+ \\
      $(\sigma, \rho) \gets
        W((w, c), \emptystring, \cookie{init}, \emptystring)$; \\
      $a \gets A^{\id{world}(\cdot, \cdot),
                  \id{random}(\cdot, \cdot)}(c, u)$; \\
      \RETURN $a$;
    \newline
    Function $\id{world}(\tau, \mu)$: \+ \\
      \IF $\tau \in \{\cookie{init}, \cookie{random}\}$ \THEN
        \RETURN $\bot$; \\
      $(\sigma, \rho) \gets W((w, c), \sigma, \tau, \mu)$; \\
      \RETURN $\rho$; \-
    \next
    Function $\id{random}(i, x)$: \+ \\
      $h \gets H_i(x)$; \\
      $(\sigma, \rho) \gets
        W((w, c), \sigma, \cookie{random}, (i, x, h))$; \\
      \RETURN $h$;
  \end{program}

  \caption{Interacting with a world: Interaction $A^{W, \mathcal{H}}$}
  \label{fig:sim-world}
\end{figure}

\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$,
  and the world~$W$: let $A$ be an adversary, and let~$U$ be an
  auxiliary-input function; let $S$ be a simulator, and let $D$ be a
  distinguisher.  We define $D$'s \emph{advantage against $S$'s simulation of
    $A$'s interaction with~$W$ with auxiliary inputs provided by~$U$} to be
  \[ \Adv{sim}{W, I, S}(A, U, D) =
       \Pr[\Game{real}{W, I, S}(A, U, D) = 1] -
       \Pr[\Game{sim}{W, I, S}(A, U, D)= 1]
  \]
  where the games are as shown in figure~\ref{fig:sim}.
  Furthermore, we define the \emph{simulator's insecurity function} to be
  \[ \InSec{sim}(W, I, S;
      t_D, t_A, \mathcal{Q}_D, \mathcal{Q}_A, \mathcal{R}, \mathcal{U}) =
      \max_{D, A, U} \Adv{sim}{W, I, S}(A, U, D)
  \]
  where the maximum is taken over all distinguishers~$D$ running in
  time~$t_D$ and making at most $\mathcal{Q}_D$ random-oracle queries, and
  all adversaries~$A$ running in time~$t_A$, making at most $\mathcal{Q}_A$
  random-oracle queries, not exceeding the other stated resource
  bounds~$\mathcal{R}$ on its interaction with~$W$, and auxiliary-input
  functions producing output not exceeding the stated bounds~$\mathcal{U}$.
\end{definition}
\begin{remark}
  The usual definitions of zero-knowledge, for example, require the simulator
  to work for all choices of inputs (common, private and auxiliary), rather
  than for random choices.  Our definition therefore looks weaker.  Our proof
  of zero-knowledge actually carries through to the traditional
  stronger-looking definition.  Critically, however, the standard
  universal quantification over inputs fails to capture deniability in the
  random oracle model, since the inputs can't therefore depend on the random
  oracle.  Our formulation therefore actually gives \emph{stronger}
  deniability than the usual one.
\end{remark}

\begin{figure}
  \begin{program}
    $\Game{real}{W, I, S}(A, U, D)$: \+ \\
      $(w, c) \gets I()$; \\
      $u \gets U^{\mathcal{H}}(w, c)$; \\
      $a \gets A^{W(w, c), \mathcal{H}}(c, u)$; \\
      $b \gets D^{\mathcal{H}}(c, u, a)$; \\
      \RETURN $b$;
    \next
    $\Game{sim}{W, I, S}(A, U, D)$: \+ \\
      $(w, c) \gets I()$; \\
      $u \gets U^{\mathcal{H}}(w, c)$; \\
      $s \gets S^{A, \mathcal{H}}(c, u)$; \\
      $b \gets D^{\mathcal{H}}(c, u, s)$; \\
      \RETURN $b$;
  \end{program}

  \caption{Games for simulation: $\Game{real}{W, I}$ and $\Game{sim}{W, I}$}
  \label{fig:sim}
\end{figure}

\ifshort\else
\subsubsection{Fake-world simulators}
The simulators we shall be considering in the present paper are of a specific
type which we call `fake-world simulators'.  They work by running the
adversary in a fake `cardboard cut-out' world, and attempting to extract
enough information from the adversary's previous interactions and random
oracle queries to maintain a convincing illusion.

That is, the behaviour of a fake-world simulator~$S$ is simply to allow the
adversary to interact with a `fake world'~$W'$, which was not given the world
private input.  That is, there is some world $W'$ such that
\[ S^{A, \mathcal{H}}(c, u) \equiv A^{W'(u, c), \mathcal{H}}(c, u) \]
Fake-world simulators are convenient because they allow us to remove from
consideration the distinguisher~$D$ as the following definition shows.
\begin{definition}[Fake-world simulation security]
  \label{def:fakesim}
  Let $I$, $W$ and $U$ be as in definition~\ref{def:sim}.  Let $A$ be an
  adversary which outputs a single bit.  Let $S$ be a fake-world simulator.
  We define $A$'s \emph{advantage against $S$'s fake-world simulation of $W$
  with auxiliary inputs provided by~$U$} to be
  \begin{spliteqn*}
    \Adv{fw}{W, I, S}(A, U) =
      \Pr[(w, c) \gets I(); u \gets U^{\mathcal{H}}(w, c);
           b \gets A^{W(w, c), \mathcal{H}}(c, u) : b = 1] - {} \\
       \Pr[(w, c) \gets I(); u \gets U^{\mathcal{H}}(w, c);
           b \gets S^{A, \mathcal{H}}(c, u) : b = 1]
  \end{spliteqn*}
  Furthermore, we define the \emph{simulator's insecurity function} to be
  \[ \InSec{fw}(W, I, S;
      t_D, t, \mathcal{Q}, \mathcal{R}, \mathcal{U}) =
      \max_{A, U} \Adv{fw}{W, I, S}(A, U)
  \]
  where the maximum is taken over all adversaries~$A$ running in time~$t$,
  making at most $\mathcal{Q}$ random-oracle queries, not exceeding the other
  stated resource bounds~$\mathcal{R}$ on its interaction with~$W$, and
  auxiliary-input functions producing output not exceeding the stated
  bounds~$\mathcal{U}$.
\end{definition}
It remains for us to demonstrate that this is a valid way of analysing
simulators; the following simple proposition shows that this is indeed the
case.
\begin{proposition}[Fake-world simulation]
  \label{prop:fakesim}
  Let $I$ be an initialization function and let $W$ be a world.  Then, for
  any fake-world simulator~$S$,
  \[ \InSec{sim}(W, I, S; t_D, t_A, \mathcal{Q}_D, \mathcal{Q}_A,
       \mathcal{R}, \mathcal{U}) \le
     \InSec{fw}(W, I, S; t_A + t_D, \mathcal{Q}_D + \mathcal{Q}_A,
       \mathcal{R}, \mathcal{U})
  \]
  (where addition of query bounds $\mathcal{Q}$ is done elementwise).
\end{proposition}
\begin{proof}
  Let $W$ and $I$ as in the proposition statement be given; also let a
  distinguisher~$D$ running in time~$t_D$ and making $\mathcal{Q}_D$
  random-oracle queries, an adversary~$A$ running in time~$t_A$ and making
  $\mathcal{Q}_A$ random-oracle queries and interacting with its world within
  the stated bounds~$\mathcal{R}$, an auxiliary-input function~$U$ satisfying
  the constraints~$\mathcal{U}$ on its output, and a fake-world simulator~$S$
  all be given.

  We construct an adversary~$B$ outputting a single bit as follows
  \begin{program}
    Adversary $B^{W, \mathcal{H}}(c, u)$: \+ \\
      $a \gets A^{W, \mathcal{H}}(c, u)$; \\
      $b \gets D^{\mathcal{H}}(c, u, a)$; \\
      \RETURN $b$;
  \end{program}
  A glance at definitions \ref{def:sim} and~\ref{def:fakesim} and the
  resources used by $B$ shows that
  \[ \Adv{sim}{W, I, S}(A, U) = \Adv{fw}{W, I, S}(B, U)
      \le \InSec{fw}(W, I, S;  t_D + t_A, \mathcal{Q}_D + \mathcal{Q}_A,
       \mathcal{R}, \mathcal{U})
  \]
  as required.
\end{proof}
\fi

%%%--------------------------------------------------------------------------
\section{A zero-knowledge identification scheme}
\label{sec:zk-ident}


\subsection{Description}

Here we present a simple zero-knowledge identification scheme.  Fix some
group $G$ with prime order $q = \#G$.  Suppose Alice chooses a private key $x
\inr \gf{q}$, and publishes the corresponding public key $X = x P$.  Let
$H_I\colon G^2 \to \Bin^{\ell_I}$ be a secure hash function.  Here's a simple
protocol which lets her prove her identity to Bob.
\begin{enumerate}
\item Bob selects a random $r \inr \gf{q}$, and computes $R = r P$, $Y = r X$,
  and $c = r \xor H_I(R, Y)$.  He sends the pair $(R, c)$ to Alice as his
  \emph{challenge}.
\item Alice receives $(R, c)$.  She computes $Y' = x R$ and $r' = c \xor
  H_I(R', Y')$, and checks that $R = r' P$.  If so, she sends $Y'$ as her
  \emph{response}; otherwise she sends $\bot$.
\item Bob receives $Y'$ from Alice.  He checks that $Y' = Y$.  If so, he
  accepts that he's talking to Alice; otherwise he becomes suspicious.
\end{enumerate}
We name this the Wrestlers Identification Protocol in~$G$, $\Wident^G$ (we
drop the superscript to refer to the protocol in general, or when no
ambiguity is likely to result).  A summary is shown in
figure~\ref{fig:wident}.

\begin{figure}
  \begin{description}
  \item[Setup] Group $G = \langle P \rangle$; $\#G = q$ is prime.
    $H_I(\cdot, \cdot)$ is a secure hash.
  \item[Private key] $x \inr \gf{q}$.
  \item[Public key] $X = x P$.
  \item[Challenge] $(R, c)$ where $r \inr \gf{q}$, $R = r P$, $c = r \xor
    H_I(R, r X)$.
  \item[Response] $x R = r X$ if $R = (c \xor H_I(R, x R)) P$; otherwise
    $\bot$.
  \end{description}

  \caption{Summary of the Wrestlers Identification Protocol, $\Wident$}
  \label{fig:wident}
\end{figure}


\subsection{Security}

In order to evaluate the security of our protocol, we present a formal
description of the algorithms involved in figure~\ref{fig:wident}.  Here, the
hash function $H_I(\cdot, \cdot)$ is modelled as a random oracle.

\begin{figure}
  \begin{program}
    Function $\id{setup}()$: \+ \\
      $x \getsr \gf{q}$; \\
      $X \gets x P$; \\
      \RETURN $(x, X)$;
    \ifshort\newline\else\next\fi
    Function $\id{challenge}^{H_I(\cdot, \cdot)}(R, c, X)$: \+ \\
      $r \getsr \gf{q}$; \\
      $R \gets r P$; $Y \gets r X$; \\
      $h \gets H_I(R, Y)$; $c \gets r \xor h$; \\
      \RETURN $(Y, R, c)$; \- \\[\medskipamount]
    Function $\id{verify}(Y, Y')$: \+ \\
      \IF $Y' = Y$ \THEN \RETURN $1$; \\
      \RETURN $0$;
    \next
    Function $\id{response}^{H_I(\cdot, \cdot)}(R, c, x)$: \+ \\
      $Y' \gets x R$; \\
      $h \gets H_I(R', Y')$; $r' \gets c \xor h$; \\
      \IF $R \ne r' P$ \THEN \RETURN $\bot$; \\
      \RETURN $Y'$;
  \end{program}

  \caption{Functions implementing $\Wident$ in the random oracle model}
  \label{fig:wident-ro}
\end{figure}

\subsubsection{Completeness}
Suppose that Bob really is talking to Alice.  Note that $Y' = x R = x (r P) =
r (x P) = r X = Y$.  Hence $r' = c \xor H_I(R', Y') = c \xor H_I(R, Y) = r$,
so $r' P = r P = R$, so Alice returns $Y' = Y$ to Bob.  Therefore $\Wident$
is \emph{complete}: if Bob really is communicating with Alice then he
accepts.

\subsubsection{Soundness}
We next show that impersonating Alice is difficult.  The natural way to prove
this would be to give an adversary a challenge and prove that its probability
of giving a correct response is very small.  However, we prove a stronger
result: we show that if the adversary can respond correctly to any of a large
collection of challenges then it can solve the MCDH problem.

Consider the game $\Game{imp}{\Wident}$ shown in
figure~\ref{fig:wident-sound}.  An adversary's probability of successfully
impersonating Alice in our protocol, by correctly responding to any one of
$n$ challenges, is exactly its probability of winning the game (i.e., causing
it to return $1$).

\begin{figure}
  \begin{program}
    $\Game{imp-$n$}{\Wident}(A)$: \+ \\
      $H_I \getsr \Func{G^2}{\Bin^{\ell_I}}$; \\
      $(x, X) \gets \id{setup}()$; \\
      $\id{win} \gets 0$; \\
      $\Xid{R}{map} \gets \emptyset$; \\
      $\mathbf{c} \gets \id{challenges}(n)$; \\
      $(R', Y') \gets A^{H_I(\cdot, \cdot), \id{check}(\cdot, \cdot)}
        (X, \mathbf{c})$; \\
      \RETURN $\id{win}$;
    \newline
    Function $\id{challenges}(n)$: \+ \\
      \FOR $i \in \Nupto{n}$ \DO \\ \ind
        $(Y, R, c) \gets \id{challenge}^{H_I(\cdot, \cdot)}$; \\
        $\Xid{R}{map} \gets \Xid{R}{map} \cup \{ R \mapsto Y \}$; \\
        $\mathbf{c}[i] \gets (R, c)$; \- \\
      \RETURN $\mathbf{c}$; \next
    Function $\id{check}(R', Y')$: \\
      \IF $R' \notin \dom \Xid{R}{map}$ \THEN \RETURN $0$; \\
      $Y \gets \Xid{R}{map}(R')$; \\
      \IF $\id{verify}(Y, Y')$ \THEN \\ \ind
        $\id{win} \gets 1$; \\
        \RETURN $1$; \- \\
      \RETURN $0$;
  \end{program}

  \caption{Soundness of $\Wident$: $\Game{imp-$n$}{\Wident}(A)$}
  \label{fig:wident-sound}
\end{figure}

\begin{theorem}[Soundness of $\Wident$]
  \label{thm:wident-sound}
  Let $A$ be any adversary running in time $t$ and making $q_I$ queries to
  its random oracle, and $q_V$ queries to its verification oracle.  Let $G$
  be a cyclic group.  Then
  \[ \Pr[\Game{imp-$n$}{\Wident^G}(A) = 1] \le
     \InSec{mcdh}(G; t', q_I + q_V)
  \]
  where $t' = t + O(q_I) + O(q_V)$.
\end{theorem}
\begin{remark}
  Note that the security bound here is \emph{independent} of the value of
  $n$.
\end{remark}
\begin{longproof}{The proof of this theorem can be found in the full version
    of the paper.}
  We prove this by defining a sequence of games $\G{i}$.  The first will be
  the same as the attack game $\Game{imp-$n$}{\Wident}(A)$ and the others
  will differ from it in minor ways.  In each game $\G{i}$, let $S_i$ be the
  event that $A$ wins the game -- i.e., that it successfully impersonates the
  holder of the private key~$x$.

  Let game $\G0$ be the attack game $\Game{imp}{\Wident}(A)$, and let $(R',
  Y')$ be the output of $A$ in the game.

  We define a new game $\G1$ which is the same as $\G0$, except that we query
  the random oracle $H_I$ at $(R', Y')$ whenever the adversary queries
  $\id{check}(R', Y')$.  (We don't charge the adversary for this.)  This
  obviously doesn't affect the adversary's probability of winning, so
  $\Pr[S_1] = \Pr[S_0]$.

  Game $\G2$ is like $\G1$, except that we change the way we generate
  challenges and check their responses.  Specifically, we new functions
  $\id{challenges}_2$ and $\id{check}_2$, as shown in
  figure~\ref{fig:wident-sound-2}.

  \begin{figure}
    \begin{program}
      Function $\id{challenges}_2(n)$: \+ \\
        $r^* \getsr I$; $R^* \gets r^* P$; $Y^* \gets r^* X$; \\
        \FOR $i \in \Nupto{n}$ \DO \\ \ind
          $r \getsr I$; $R \gets r R^*$; $Y \gets r Y^*$; \\
          $h \gets H_I(R, Y)$; $c \gets r \xor h$; \\
          $\Xid{R}{map} \gets \Xid{R}{map} \cup \{ R \mapsto r \}$; \\
          $\mathbf{c}[i] \gets (R, c)$; \- \\
        \RETURN $\mathbf{c}$;
      \next
      Function $\id{check}_2(R', Y')$: \+ \\
        \IF $R' \notin \dom \Xid{R}{map}$ \THEN \RETURN $0$; \\
        $r \gets \Xid{R}{map}(R')$; \\
        \IF $\id{verify}(Y^*, Y'/r)$ \THEN \\ \ind
          $\id{win} \gets 1$; \\
          \RETURN $1$; \- \\
        \RETURN $0$;
    \end{program}

    \caption{Soundness of $\Wident$: $\id{challenges}_2$ and $\id{check}_2$}
    \label{fig:wident-sound-2}
  \end{figure}

  While we're generating and checking challenges in a more complicated way
  here, we're not actually changing the distribution of the challenges, or
  changing the winning condition.  Hence $\Pr[S_2] = \Pr[S_1]$.

  Now we change the rules again.  Let $\G3$ be the same as $\G2$ except that
  we change the winning condition.  Instead, we say that the adversary wins
  if any of the queries to its random oracle $H_I(R', Y')$ would be a correct
  response -- i.e., $\id{check}_2(R', Y')$ would return $1$.  Since we query
  the oracle on $(R', Y')$ on its behalf at the end of the game, no adversary
  can do worse in this game than it does in $\G2$, so we have $\Pr[S_3] \ge
  \Pr[S_2]$.  (It's not hard to see that this only helps quite stupid
  adversaries.  We can transform any adversary into one for which equality
  holds here.)

  Finally, let $\G4$ be the same as $\G3$ except that we change the way we
  generate challenges again: rather than computing $h$ and setting $c \gets h
  \xor r$, we just choose $c$ at random.  Specifically, we use the new
  function, $\id{challenges}_4$, shown in figure~\ref{fig:wident-sound-4}.

  \begin{figure}
    \begin{program}
      Function $\id{challenges}_4(n)$: \+ \\
        $r^* \getsr I$; $R^* \gets r^* P$; $Y^* \gets r^* X$; \\
        \FOR $i \in \Nupto{n}$ \DO \\ \ind
          $r \getsr I$; $R \gets r R^*$; \\
          $c \getsr \Bin^{\ell_I}$; \\
          $\Xid{R}{map} \gets \Xid{R}{map} \cup \{ R \mapsto r \}$; \\
          $\mathbf{c}[i] \gets (R, c)$; \- \\
        \RETURN $\mathbf{c}$;
    \end{program}

    \caption{Soundness of $\Wident$: $\id{challenges}_4$}
    \label{fig:wident-sound-4}
  \end{figure}

  Since $H_I(\cdot, \cdot)$ is a random function, the adversary can only
  distinguish $\G4$ from $\G3$ if it queries its random oracle at some $(R, r
  Y^*)$.  But if it does this, then by the rule introduced in $\G3$ it has
  already won.  Therefore we must have $\Pr[S_4] = \Pr[S_3]$.

  Our $\id{challenges}_4$ function is interesting, since it doesn't actually
  make use of $r^*$ or $Y^*$ when generating its challenges.  This gives us
  the clue we need to bound $\Pr[S_4]$: we can use adversary $A$ to solve the
  multiple-guess Diffie-Hellman problem in $G$ by simulating the game $\G4$.
  Specifically, we define the adversary $B$ as shown in
  figure~\ref{fig:wident-sound-cdh}.  That is, for each query $A$ makes to
  its random oracle at a new pair $(R', Y')$, we see whether this gives us
  the answer we're looking for.  We have $\Pr[S_0] \le \Pr[S_4] =
  \Succ{mcdh}{G}(B) \le \InSec{gdh}(G; t', q_I + q_V)$ as required.

  \begin{figure}
    \begin{program}
      Adversary $B^{V(\cdot)}(X, R^*)$: \+ \\
        $F \gets \emptyset$; $\Xid{R}{map} \gets \emptyset$; \\
        \FOR $i \in \Nupto{n}$ \DO \\ \ind
          $r \getsr I$; $R \gets r R^*$; $c \getsr \Bin^{\ell_I}$; \\
          $\Xid{R}{map} \gets \Xid{R}{map} \cup \{ R \mapsto r \}$; \\
          $\mathbf{c}[i] \gets (R, c)$; \- \\
        $(R', Y') \gets A^{H_I(\cdot, \cdot), \id{check}(\cdot, \cdot)}
          (X, \mathbf{c})$; \\
        \IF $Y' \neq \bot$ \THEN $H_I(R', Y')$;
      \next
      Oracle $H_I(R', Y')$: \+ \\
        \IF $(R', Y') \in \dom F$ \THEN \\ \quad
          $h \gets F(x)$; \\
        \ELSE \\ \ind
          $\id{check}(R', Y')$; \\
          $h \getsr \Bin^{\ell_I}$;
          $F \gets F \cup \{ (R', Y') \mapsto h \}$; \- \\
        \RETURN $h$;
      \- \\[\medskipamount]
      Oracle $\id{check}(R', Y')$: \+ \\
        \IF $R' \in \dom \Xid{R}{map}$ \THEN
          $V(Y'/\Xid{R}{map}(R'))$;
    \end{program}

    \caption{Soundness of $\Wident$: reduction from MCDH}
    \label{fig:wident-sound-cdh}
  \end{figure}
\end{longproof}

\subsubsection{Zero-knowledge}
Finally we must prove that $\Wident$ is (statistical) zero-knowledge -- i.e.,
that, except with very small probability, Bob learns nothing of use to him
except that he's interacting with Alice.  To do this, we show that, for any
algorithm $B$ which Bob might use to produce his challenge to the real Alice,
there exists a simulator $S$ which produces transcripts distributed very
similarly to transcripts of real conversations between $B$ and Alice, the
difference being that $S$ doesn't know Alice's key.  We shall show that the
statistical difference between the two distributions is $2^{-\ell_I}$.

The intuition here is that Bob ought to know what answer Alice is going to
give him when he constructs his challenge.  This is certainly true if he's
honest: his challenge is $R = r P$ for some $r$ he knows, so he won't learn
anything useful when Alice responds with $x R = r X$.  However, if Bob sends
a challenge $R$ when he doesn't know the corresponding $r$, he learns
something potentially useful.  The accompanying check value $c = r \xor
H_I(R, r X)$ keeps him honest.

To show this, we present an \emph{extractor} which, given any challenge $(R,
c)$ Bob can construct, and his history of random-oracle queries, either
returns a pair $(r, Y)$ such that $R = r P$ and $Y = r X$, or $\bot$;
moreover, the probability that Alice returns a response $Y' \ne \bot$ given
the challenge $(R, c)$ is $2^{-\ell}$.  We can, of course, readily convert
this extractor into a simulator to prove the zero-knowledge property of our
protocol.

We shall actually consider a slightly more complex setting.  We grant Bob
access to an oracle which produces random, correctly-formed challenges.  We
require this to model the legitimate challenges of other parties when we
analyse the security of our key exchange protocol.

\begin{definition}[Discrete-log extractors]
  Let $T$, $B$ be randomized algorithms.  Define the game
  $\Game{dl-ext}{G}(T, B)$ as shown in figure~\ref{fig:dlext}.  The
  \emph{success probability of $T$ as a discrete-log extractor against $B$}
  is defined as
  \[ \Succ{dl-ext}{G}(T, B) = \Pr[\Game{dl-ext}{G}(T, B) = 1]. \]
\end{definition}

\begin{figure}
  \begin{program}
    $\Game{dl-ext}{G}(T, B):$ \+ \\
      $H_I \getsr \Func{G^2}{\Bin^{\ell_I}}$;
      $Q_H \gets \emptyset$; $Q_C \gets \emptyset$; \\
      $(x, X) \gets \id{setup}()$; \\
      $(R, c) \gets B^{\Xid{H_I}{trap}(\cdot, \cdot), C()}(x, X)$; \\
      $(r, Y) \gets T(R, c, Q_H)$; \\
      $Y' \gets x R$; $h' \gets H_I(R, Y')$; $r' \gets c \xor h'$; \\
      \IF $r \ne \bot$ \THEN \\ \quad
        \IF $Y = \bot \lor R \ne r P \lor Y \ne Y'$ \THEN \RETURN $0$; \\
      \IF $R = r' P$ \THEN $(r^*, Y^*) \gets (r', Y')$; \\
      \ELSE $(r^*, Y^*) \gets (\bot, \bot)$; \\
      \IF $(R, c) \in Q_C$ \THEN \RETURN $1$; \\
      \IF $(r, Y) = (r', Y')$ \THEN \RETURN $1$; \\
      \RETURN $0$;
    \next
    Oracle $\Xid{H_I}{trap}(R', Y')$: \+ \\
      $h \gets H_I(R', Y')$; \\
      $Q_H \gets Q_H \cup \{(R', Y', h)\}$; \\
      \RETURN $h$; \- \\[\medskipamount]
    Oracle $C()$: \+ \\
      $r \getsr \gf{q}$; \\
      $R \gets r P$; $c \gets r \xor H_I(R, r X)$; \\
      $Q_C \gets Q_C \cup \{(R, c)\}$; \\
      \RETURN $(R, c)$
  \end{program}

  \caption{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:pub-enc-notions}.

Such an extractor indeed exists, as the following lemma states.
\begin{lemma}[Effectiveness of extractor $T_\Wident$]
  \label{lem:dlext}
  There exists a \emph{universal discrete-log extractor} $T_\Wident$, shown
  in figure~\ref{fig:twident}, such that, for any algorithm $B$,
  \[ \Succ{dl-ext}{G}(T_\Wident, B) \ge 1 - \frac{1}{2^{\ell_I}}. \]
  Moreover, if $B$ issues at most $q_H$ random-oracle queries, then the
  running time of $T_\Wident$ is $O(q_H)$.
\end{lemma}
\ifshort
The proof of this lemma is given in the full version of this paper.
\else
We prove this result at the end of the section.  For now, let us see how to
prove that $\Wident$ is zero-knowledge.
\fi

\begin{figure}
  \begin{program}
    Extractor $T_\Wident(R, c, Q_H)$: \+ \\
      \FOR $(R', Y', h)$ \IN $Q_H$ \DO \\ \ind
        $r \gets h \xor c$; \\
        \IF $R = R' = r P \land Y' = r X$ \THEN \RETURN $(r, Y')$; \- \\
      \RETURN $(\bot, \bot)$;
  \end{program}

  \caption{The discrete-log extractor $T_\Wident$}
  \label{fig:twident}
\end{figure}

We use the set-up described in section~\ref{sec:sim}.  Our initialization
function~$I_\Wident$ just chooses a random $x \in \gf{q}$ as the world
private input and sets $X = x P$ as the common input.  In the `real world',
the adversary is allowed to submit a (single) challenge to the prover; it is
given the prover's response, and must then compute its output.  This is shown
on the left hand side of figure~\ref{fig:wident-sim}.

The zero-knowledge property of the scheme is described by the following
theorem.
\begin{theorem}[Statistical zero-knowledge of $\Wident$]
  \label{thm:wident-zk}
  Let $I_\Wident$, $W_\Wident$ and $S_\Wident$ be the real-prover world and
  simulator shown in figure~\ref{fig:wident-sim}.  Then, for any~$t$,
  $q_I$ and $q_C$,
  \[ \InSec{sim}(W_\Wident, I_\Wident, S_\Wident; t, q_I, q_C, 0) \le
       \frac{q_C}{2^\ell_I}.
  \]
  where $q_C$ is the maximum number of challenges allowed by the adversary.
\end{theorem}
\begin{longproof}{}
  The simulator simply uses the extractor~$T_\Wident$ to extract the answer
  from the adversary's history of random oracle queries.  Observe that
  $S_\Wident$ is a fake-world simulator.  By lemma~\ref{lem:dlext}, the
  extractor fails with probability only $2^{-\ell_I}$.  The theorem follows
  by a simple union bound and proposition~\ref{prop:fakesim}.
\end{longproof}

%\ifshort\else
\begin{figure}
  \begin{program}
    Initialization function $I_\Wident()$: \+ \\
      $x \getsr \gf{q}$; \\
      $X \gets x P$; \\
      \RETURN $(x, X)$;
    \- \\[\medskipamount]
    Real-prover world $W_\Wident^{H_I(\cdot, \cdot)}
        ((x, X), \sigma, \tau, \mu)$: \+ \\
      \IF $\tau = \cookie{challenge}$ \THEN \\ \ind
        $(R, c) \gets \mu$; \\
        $Y \gets \id{response}^{H_I(\cdot, \cdot)}(R, c, x)$; \\
        \RETURN $(1, Y)$; \- \\
      \ELSE \\ \ind
        \RETURN $(\sigma, \bot)$;
  \next
  Simulator $S_\Wident$'s fake world \\
  \hspace{1in} $W_{\text{sim}}^{H_I(\cdot, \cdot)}
      ((X, u), \sigma, \tau, \mu)$: \+ \\
      \IF $\tau = \cookie{init}$ \THEN \\ \ind
        \RETURN $(\emptyset, \emptystring)$; \- \\
      $Q_H \gets \sigma$; \\
      \IF $\tau = \cookie{challenge}$ \THEN \\ \ind
        $(R, c) \gets \mu$; \\
        $(r, Y) \gets T_\Wident(R, c, Q_H)$; \\
        \RETURN $(Q_H, Y)$; \- \\
      \ELSE \IF $\tau = \cookie{random}$ \THEN \\ \ind
        $(i, (R', Y'), h) \gets \mu$; \\
        $Q_H \gets Q_H \cup \{(R', Y', h)\}$; \\
        \RETURN $(Q_H, \emptystring)$; \- \\
      \ELSE \\ \ind
        \RETURN $(\sigma, \bot)$;
  \end{program}

  \caption{Real-prover and simulator for zero-knowledge of $\Wident$}
  \label{fig:wident-sim}
\end{figure}
%\fi

\ifshort\else
We now return to proving that the extractor $T_\Wident$ functions as claimed.
The following two trivial lemmata will be useful, both now and later.
\begin{lemma}[Uniqueness of discrete-logs]
  \label{lem:unique-dl}
  Let $G = \langle P \rangle$ be a cyclic group.  For any $X \in G$ there is
  a unique $x \in \gf{q}$ where $X = x P$.
\end{lemma}
\begin{proof}
  Certainly such an $x$ exists, since $G$ is cyclic and finite.  Suppose $X =
  x P = x' P$: then $0 = x P - x' P = (x - x') P$.  Hence $(x - x')$ is a
  multiple of $q$, i.e., $x = x'$.
\end{proof}
\begin{lemma}[Uniqueness of check values]
  \label{lem:unique-c}
  Let $G = \langle P \rangle$ be a cyclic group of prime order $q$; let $H_I$
  be a function $H_I\colon \Bin^{2\ell_G} \to \Bin^{\ell_I}$.  Fix some $x
  \in \gf{q}$ and define the set
  \[ V_x = \bigl\{\, (R, c) \in G \times \Bin^{\ell_I} \bigm|
                R = \bigl( c \xor H_I(R, x R) \bigr) P \,\bigr\}.
  \]
  Then, for any $R$, $c$, $c'$, if $(R, c) \in V_x$ and $(R, c') \in V_x$
  then $c = c'$.
\end{lemma}
\begin{proof}
  From lemma~\ref{lem:unique-dl}, we see that there is a unique $r \in \gf{q}$
  for which $R = r P$.  Now, if $(R, c) \in V_x$, we must have $r = c \xor
  H_I(R, x R)$.  It follows that $c = r \xor H_I(R, x R)$.
\end{proof}

\begin{proof}[Proof of lemma~\ref{lem:dlext}]
  Let $B$ be any randomized algorithm, and let $(R, c, Q_H)$ be as given to
  the extractor by $\Game{dl-ext}{G}(T_\Wident, B)$.  Let the quantities
  $H_I$, $Q_C$, $r$, $r'$, $x$ and $X$ be as in that game.

  Suppose that the extractor returns values $(r, Y) \ne (\bot, \bot)$.  Let
  $h = r \xor c$; then there must be a query $(R, Y, h) \in Q_H$, and we have
  $R = r P$ and $Y = r X = r (x P) = x (r P) = x R = Y'$, so the extractor's
  output must be correct unless it fails.

  Furthermore, in the case where the extractor did not fail, we have $h =
  H_I(R, Y) = H_I(R, Y')$ and $c = r \xor h$, so the challenge was valid.
  Therefore, if the challenge was invalid, the extractor will fail.

  We now deal with the challenge-generation oracle.  Suppose that $(R, c')
  \in Q_C$ for some $c'$.  Now, if $c = c'$ then $(R, c')$ is a repeat of
  some challenge from the challenge-generation oracle, and the extractor is
  permitted to fail.  On the other hand, suppose $c \ne c'$; then, the
  challenge $(R, c)$ must be invalid by lemma~\ref{lem:unique-c}, so the
  extractor is required to fail, and we have established that indeed it will.
  From now on, suppose that $R$ is distinct from all the $R$-values returned
  by $C()$.

  Let $Y = x R$.  Suppose that $B$ queried its random oracle at $(R, Y)$.
  Let $h = H_I(Y)$, so $r' = c \xor h$.  If the challenge is valid then $R =
  r' P$; therefore $Y = x R = x r' P = r' X$, so we have $(R, Y, h) \in Q_H$
  with $R = r P$ and $Y = r X$.  Hence the extractor returns $r = r'$ as
  required.

  It remains to deal with the case where there is no random-oracle query at
  $(R, Y)$.  But then $h = H_I(R, Y)$ is uniformly distributed, and
  independent of the entire game up to this point.  Let $r$ be the correct
  discrete log of $R$; by lemma~\ref{lem:unique-dl} there is only one
  possible value.  The extractor always fails under these circumstances, but
  a correct responder would reply with probability
  \[ \Pr[h = c \xor r] = \frac{1}{2^{\ell_I}}. \]
  This concludes the proof.
\end{proof}
\begin{remark}
  Note that the fact that the algorithm~$B$ was given the private key is
  irrelevant to the above argument.  However, we shall need this property
  when we come to prove deniability for the key-exchange protocol.
\end{remark}
\begin{remark}
  It's easy to see from the above proof that the extractor works flawlessly
  on the `honest verifier' algorithm $\id{challenge}$ shown in
  figure~\ref{fig:wident-ro}.  This shows that $\Wident$ is perfect
  zero-knowledge against honest verifiers.  We're much more interested in
  dishonest verifiers, though.
\end{remark}
\fi


\ifshort\else
\subsection{An identity-based identification scheme}
\label{sec:wident-id}

Boneh and Franklin \cite{boneh-franklin-2003:ibe-weil-pairing} showed how to
construct an identity-based encryption scheme using bilinear pairings.  The
resulting encryption scheme looks somewhat like a pairing-based version of
ElGamal's encryption scheme \cite{elgamal-1985:dlog-enc-sign}.  We can
easily apply their techniques to our identification protocol, and thereby
obtain an identity-based identification scheme.  Providing the necessary
formalisms to prove theorems analogous to our theorems~\ref{thm:wident-sound}
and~\ref{thm:wident-zk} would take us too far from our objectives; but given
appropriate security notions, we can readily adapt our existing proofs to the
new setting.

\subsubsection{Bilinear pairings}
Before we describe the necessary modifications to the protocol, we first give
a (very brief!) summary of cryptographic pairings.  (The Boneh--Franklin
paper \cite{boneh-franklin-2003:ibe-weil-pairing} gives more detail; also
\cite{menezes-2005:intro-pairing-crypto} provides a useful introduction to
the topic.)

Let $(G, +)$, $(G', +)$ and $(G_T, \times)$ be cyclic groups with prime order
$q$; let $P \in G$ and $P' \in G'$ be elements of order $q$ in $G$ and $G'$
respectively.  We say that a mapping $\hat{e}\colon G \times G' \to G_T$ is a
\emph{non-degenerate bilinear pairing} if it satisfies the following
properties.
\begin{description}
\item[Bilinearity] For all $R \in G$ and $S', T' \in G'$, we have $\hat{e}(R,
  S' + T') = \hat{e}(R, S')\,\hat{e}(R, T')$; and for all $R, S \in G$ and $T'
  \in G'$ we have $\hat{e}(R + S, T') = \hat{e}(R, T')\,\hat{e}(S, T')$.
\item[Non-degeneracy] $\hat{e}(P, P') \ne 1$.
\end{description}
For practical use, we also want $\hat{e}(\cdot, \cdot)$ to be efficient to
compute.  The reader can verify that $\hat{e}(a P, b P') = \hat{e}(P,
P')^{ab}$.  It is permitted for the two groups $G$ and $G'$ to be equal.

We require a different intractability assumption, specifically that the
\emph{bilinear} Diffie-Hellman problem (BDH) -- given $(a P, b P, a P', c P')
\in G^2 \times G'^2$, find $\hat{e}(P, P')^{abc} \in G_T$ -- is difficult.
This implies the difficulty of the computational Diffie-Hellman problem in
all three of $G$, $G'$ and~$G_T$.

\subsubsection{The identity-based scheme}
We need a trusted authority; following \cite{schneier-1996:applied-crypto} we
shall call him Trent.  Trent's private key is $t \in \gf{q}$; his public key
is $T = t P$.

Finally, we need cryptographic hash functions $H_I\colon G \times G_T \to
\Bin^{\ell_I}$ and $\Hid\colon \Bin^* \to G'$; a formal security analysis
would model these as random oracles.

Alice's public key is $A = \Hid(\texttt{Alice}) \in G'$.  Her private key is
$K_A = t A \in G'$ -- she needs Trent to give this to her.  Bob can interact
with Alice in order to verify her identity as follows.
\begin{enumerate}
\item Bob computes $\gamma_A = \hat{e}(T, A) \in G_T$.  (He can do this once
  and store the result if he wants, but it's not that onerous to work it out
  each time.)
\item Bob chooses $r \inr \gf{q}$, and sets $R = r P$.  He also computes
  $\psi = \gamma_A^r$, $h = H_I(R, \psi)$ and $c = r \xor h$.  He sends his
  challenge $(R, c)$ to Alice.
\item Alice receives $(R', c')$.  She computes $\psi' = \hat{e}(R, K_A)$, $h'
  = H_I(R', \psi')$, and $r' = c' \xor h')$.  She checks that $R' = r' P$; if
  so, she sends $\psi'$ back to Bob; otherwise she refuses to talk to him.
\item Bob receives $\psi'$.  If $\psi = \psi'$ then he accepts that he's
  talking to Alice.
\end{enumerate}
This works because $\psi = \gamma_A^r = \hat{e}(T, A)^r = \hat{e}(t P, A)^r =
\hat{e}(r P, A)^t = \hat{e}(R, t A) = \psi'$.

\subsubsection{Informal analysis}
An analogue to lemma~\ref{lem:dlext} can be proven to show how to extract $r$
from a verifier's random-oracle queries; statistical zero knowledge would
then follow easily, as in theorem~\ref{thm:wident-zk}.  Soundness is
intuitively clear, since an adversary must compute $\psi = \hat{e}(P,
P')^{art}$ given $A = a P'$, $R = r P$ and $T = t P$, which is an instance of
the BDH problem.  An analogue of theorem~\ref{thm:wident-sound} would have to
prove this for an adversary capable of making identity requests as well as
obtaining challenges.  Finally, our key-exchange protocol can be constructed
out of this identity-based identification scheme, yielding an identity-based
authenticated key-exchange protocol.  We leave it to the reader to work
through the details.
\fi


\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-wu-2006:two-flow-zero-knowledge}.  They restrict their
attention to Schnorr groups $G \subset \F_p^*$.  Let $\gamma$ be an element
of order $q = \#G$.  The prover's private key is $a \inr \gf{q}$ and her
public key is $\alpha = \gamma^a$.  In their protocol, the challenger chooses
$r \inr \gf{q}$, computes $\rho = \gamma^r$ and $\psi = \alpha^r$, and sends
a challenge $(\rho, H(\psi))$.  The prover checks that $\rho^q \ne 1$,
computes $\psi = \rho^a$, checks the hash, and sends $\psi$ back by way of
response.  They prove their protocol's security in the random-oracle model.

Both the Wrestlers protocol and Stinson--Wu require both prover and verifier
to compute two exponentiations (or scalar multiplications) each.  The
sizes of the messages used by the two protocols are also identical.

(An earlier version of the Stinson--Wu protocol used a cofactor
exponentiation: if we set $f = (p - 1)/q$, then we use $\psi = \alpha^{rf}) =
\rho^{af} = \gamma^{afr}$.  This is more efficient in typical elliptic curve
subgroups, since the cofactor of such subgroups is usually small: indeed,
\cite{certicom-2000:sec1} recommends rejecting groups with cofactor $f > 4$.
However, in the Schnorr groups used by Stinson and Wu, the cofactor is much
larger than $q$, and their new variant is more efficient.)

We note that the zero-knowledge property of the Stinson--Wu protocol requires
the Diffie-Hellman knowledge of exponent assumption (KEA).  Very briefly:
suppose $A$ is a randomized algorithm which takes as input $X \in G$ and
outputs a pair $(r P, r X)$; intuitively, the KEA asserts $A$ must have done
this by choosing $r$ somehow and then computing its output from it.
Formally, it asserts the existence of an `extractor' algorithm which takes as
input the element $X$ and the random coins used by $A$ and outputs $r$ with
high probability.  This is a very strong assumption, and one which is
unnecessary for our protocol, since we can present an \emph{explicit}
extractor.

The KEA assumption as stated in
\cite{stinson-wu-2006:two-flow-zero-knowledge} allows the extractor to fail
with some negligible probability, over and above the probability that a
dishonest verifier managed to guess the correct $h = H(\psi)$ without making
this random-oracle query.  Not only does our protocol achieve zero- knowledge
without the KEA, our extractor is, in this sense, `perfect'.

Our protocol is just as strong as Stinson--Wu under attack from active
intruders: see table~\ref{tab:wident-active} for a very brief sketch of the
case-analysis which would be the basis of a proof of this.

\begin{table}
  \begin{tabular}[C]{|*{3}{c|}p{8cm}|}
    \hlx{hv[1]}
    \multicolumn{2}{|c|}{\textbf{Challenge}} &
    \textbf{Response} &
    \textbf{Security}
    \\ \hlx{v[1]hv}
    %% unpleasant hacking to make the R and c columns the same width :-(
    \settowidth{\dimen0}{\textbf{Challenge}}%
    \dimen0=.5\dimen0
    \advance\dimen0by-\tabcolsep
    \advance\dimen0by-.5\arrayrulewidth
    \hbox to\dimen0{\hfil$R$\hfil}
         & $c$  & $Y$  & Nothing to prove.			\\ \hlx{v}
    $R$  & $c'$ & ---  & Prover rejects by lemma~\ref{lem:unique-c};
                         $Y'$ probably wrong by
                         theorem~\ref{thm:wident-sound}.         \\ \hlx{v}
    $R$  & $c$  & $Y'$ & Response is incorrect.			\\ \hlx{v}
    $R'$ & ---  & $Y$  & Response is incorrect.			\\ \hlx{v}
    $R'$ & $c$  & $Y'$ & Prover rejects with probability $1 - 2^{-\ell_I}$;
                         $Y'$ probably wrong by
                         theorem~\ref{thm:wident-sound}.         \\ \hlx{v}
    $R'$ & $c'$ & $Y'$ & Simulate prover using extractor
                         (lemma~\ref{lem:dlext}); $Y'$ probably wrong by
                         theorem~\ref{thm:wident-sound}.         \\ \hlx{vh}
  \end{tabular}

  \caption{Security of $\Wident$ against active intruders (summary)}
  \label{tab:wident-active}
\end{table}

An identity-based analogue of Stinson--Wu can be defined using a bilinear
pairing, just as we did in section~\ref{sec:wident-id}.  However, to prove
the zero-knowledge property, one needs to make a bilinear analogue of the
knowledge of exponent assumption.

We suspect that a key-exchange protocol like ours can be constructed using
Stinson--Wu rather than the Wrestlers identification scheme.  We haven't,
however, gone through all the details, since we believe our protocol is just
as efficient and is based on much more conservative assumptions.
\fi

%%%--------------------------------------------------------------------------
\section{A simple key-exchange protocol}
\label{sec:kx}

In this section, we describe a simple key-exchange protocol built out of the
identification protocol shown previously.

The key-exchange protocol arises from the following observation.  If Bob
sends a challenge, presumably to Alice, and gets a correct response, then not
only did he really send the challenge to Alice but he knows that she received
it correctly.

So, if Alice and Bob authenticate each other, by the end of it, they should
each have chosen a random private value, sent the corresponding public value
to the other, and been convinced that it arrived safely.

Unfortunately, life isn't quite this kind, and we have to do some more work
to make this scheme secure.


Our key exchange protocol essentially consists of two parallel instances of
the identification protocol.  If Alice receives a correct response to her
challenge, she will know that Bob received her challenge correctly, and
\emph{vice versa}.  If we let Alice's challenge be $R_0 = r_0 P$ and Bob's
challenge be $R_1 = r_1 P$ then each can compute a shared secret $Z = r_0 R_1
= r_0 r_1 P = r_1 R_0$ unknown to an adversary.  There are, unfortunately, a
few subtleties involved in turning this intuition into a secure key-exchange
protocol, which we now describe.


\subsection{Overview}
\label{sec:kx-overview}

We present a quick, informal description of our basic key-exchange protocol.
In addition to our group $G$, we shall also need a secure symmetric
encryption scheme $\E = (\kappa, E, D)$, and two secure hash functions
$H_I\colon \Bin^{2\ell_G} \to \Bin^{\ell_I}$ and $H_K\colon \Bin^{\ell_G+1}
\to \Bin^\kappa$.

Suppose that Alice's and Bob's private keys are $a$ and $b$ respectively, and
their public keys are $A = a P$ and $B = b P$.
\begin{enumerate}
\item Alice chooses a random index $r \inr \gf{q}$.  She computes $R = r P$ and
  $c = r \xor H_I(R, r B)$.  She sends the pair $(R, c)$ to Bob.
\item Similarly, Bob chooses a random $s \inr \gf{q}$.  He computes $S = s P$
  and $d = s \xor H_I(S, s A)$.  He sends $(S, d)$ to Alice.
\item Alice receives $(S', d')$ from Bob.  She computes $s' = d' \xor H_I(S',
  a S')$, and verifies that $S' = s' P$.  If so, she computes $K_A = H_K(0
  \cat r S')$, and sends $R, E_{K_A}(a S')$ to Bob.
\item Similarly, Bob receives $(R', c')$ from Alice.  He verifies that $R' =
  \bigl( c' \xor H_I(R', b R') \bigr) P$.  If so, he computes $K_B = H_K(0
  \cat s R')$ and sends S, $E_{K_B}(b R')$ to Alice.
\item Alice receives a ciphertext $(S'', \chi_B)$ from Bob.  She checks that
  $S'' = S'$, decrypts $\chi_B$, and checks that $D_{K_A}(\chi_B) = r B$.  If
  so, she uses $H_K(1 \cat r S')$ as her shared secret.
\item Similarly, Bob receives $(R'', \chi_A)$ from Alice, and checks $R'' =
  R'$ and $D_{K_B}(\chi_A) = s A$.  If so, he uses $H_K(1 \cat s R')$ as his
  shared secret.
\end{enumerate}
This is the Wrestlers Key Exchange protocol, $\Wkx^{G, \E}$ (again, we omit
the superscripts when referring to the general protocol, or when confusion is
unlikely).  A diagrammatic summary of the protocol is shown in
figure~\ref{fig:wkx}.

\begin{figure}
  \begin{description}
  \item[Setup] Group $G = \langle P \rangle$; $\#G = q$ is prime.
    $H_I(\cdot, \cdot)$ and $H_K(\cdot)$ are secure hashes.  $\E = (\kappa,
    E, D)$ is an IND-CCA2 symmetric encryption scheme.
  \item[Parties] $U_i$ for $0 \le i < n$.
  \item[Private keys] $x_i \inr \gf{q}$.
  \item[Public keys] $X_i = x_i P$.
  \end{description}
  \begin{protocol}
    $r_i \getsr I$; $R_i \gets r_i P$; &
    $r_j \getsr I$; $R_j \gets r_j P$; \\
    $c_i \gets r_i \xor H_I(R_i, r_i X_j)$; &
    $c_j \gets r_j \xor H_I(R_j, r_j X_i)$; \\
    \send{->}{(R_i, c_i)}
    \send{<-}{(R_j, c_j)}
    Check $R_j = \bigl(c_j \xor H_I(x_i R_j)\bigr) P$; &
    Check $R_i = \bigl(c_i \xor H_I(x_j R_i)\bigr) P$; \\
    $Z \gets r_i R_j$; $(K_0, K_1) \gets H_K(Z)$; &
    $Z \gets r_j R_i$; $(K_0, K_1) \gets H_K(Z)$; \\
    $\chi_i \gets E_{K_0}(x_i R_j)$; &
    $\chi_j \gets E_{K_0}(x_j R_i)$; \\
    \send{->}{(R_i, \chi_i)}
    \send{<-}{(R_j, \chi_j)}
    Check $D_{K_0}(\chi_j) = r_i X_j$; &
    Check $D_{K_0}(\chi_i) = r_j X_i$; \\
    Shared key is $K_1$. & Shared key is $K_1$.
  \end{protocol}

  \caption{Summary of the Wrestlers Key Exchange protocol, $\Wkx$}
  \label{fig:wkx}
\end{figure}

Assume, for the moment, that Alice and Bob's messages are relayed honestly.
Then:
\begin{itemize}
\item $a S' = a S = a (s P) = s (a P) = s A$, so $s' = d' \xor H_I(S' a S') =
  d \xor H_I(S, s A) = s$, and $S' = S = s P = s' P$, and therefore Alice
  responds to Bob's message;
\item similarly $b R' = r B$, so $r' = r$ and $R' = r' P$, and therefore Bob
  responds to Alice's message;
\item $b R' = b R = b (r P) = r (b P) = r B$, and $a S' = a S = a (s P) = s
  (a P) = s A$, and therefore both parties compute their responses correctly;
  and
\item $r S' = r S = r (s P) = s (r P) = s R = s R'$, so $K_A = K_B$, and
  therefore they can decrypt each others' responses, and agree the same
  shared secret.
\end{itemize}
This shows that the protocol is basically valid, but says little about its
security.  The remainder of this section will describe our protocol in more
formal detail, and prove its security in a model with multiple parties and an
adversary who controls the network.

Observe that the protocol as we've presented here is \emph{symmetrical}.
There's no notion of `initiator' or `responder'.  There are a total of four
messages which must be sent before both parties accept.  However, this can be
reduced to three by breaking the symmetry of the protocol and combining one
or other party's challenge and response messages.  We choose to analyse the
symmetrical version, since to do so, it suffices to consider only the two
different kinds of messages.  Since our security model allows the messages to
be adversarially delayed and reordered, it is easy to show that the security
of an optimized, asymmetrical protocol is no worse than the symmetrical
version we present here.


\subsection{Security model and security definition}
\label{sec:um}

Our model is very similar to that of Canetti and Krawczyk
\cite{canetti-krawczyk-2001:secure-channels}, though we have modified it in
two ways.
\begin{enumerate}
\item We allow all the participants (including the adversary) in the protocol
  access to the various random oracles required to implement it.
\item Since we want to analyse a specific, practical scheme, asymptotic
  results are useless.  We measure the adversary's resource usage carefully,
  and produce a quantitative bound on the adversary's advantage in the
  SK-security game.
\end{enumerate}

\ifshort

Readers interested in the details of the model should see Canetti and
Krawczyk's paper \cite{canetti-krawczyk-2001:secure-channels}, or the full
version of this paper.

\else

\subsubsection{Overview}
We briefly describe our modified model, pointing out the changes we have
made, and how they apply to our protocol.  Much of Canetti and Krawczyk's
model (for example, the local and global outputs) is useful for proving more
general security properties such as demonstrating that SK-security suffices
for constructing secure channels, and we shall not concern ourselves with
such details.  Other parts deal with issues such as security parameters and
ensuring that all the computation is polynomially bounded, which are
irrelevant since we are dealing with a single concrete protocol rather than a
family of them.

The entities in the model are the \emph{adversary}~$A$, and a (fixed) number
of \emph{parties}~$P_i$, for $0 \le i < n$.  If the protocol under
consideration makes use of random oracles, then all the participants -- the
adversary and the parties -- are all allowed access to the random oracles.

The parties and the adversary play a `game'.  At the beginning of the game,
the participants are given some inputs computed by a randomized
\emph{initialization procedure}~$\id{init}$.  This produces as output a pair
$(i_U, \mathbf{i})$; the value $i_U$ is the \emph{global input}, and is given
to all the participants including the adversary.  The vector $\mathbf{i}$ has
$n$ components, and party $P_i$ is given $(i_U, \mathbf{i}[i])$ as input.

\subsubsection{Sessions}
Parties don't act directly.  Instead, each party runs a number of
\emph{sessions}.  A session is represented by a triple $S = (P_i, P_j, s)$,
where $i, j \in \Nupto{n}$ identify the owning party and a \emph{partner},
and $s \in \Bin^{\ell_S}$ is a \emph{session-id}.  (The original model
includes a r\^ole, for distinguishing between initiators and responders.  Our
protocol is symmetrical, so this distinction isn't useful.)  If $P_i$ runs a
session $S = (P_i, P_j, s)$ and $P_j$ runs a session $S' = (P_j, P_i, s)$
then we say that $S$ and $S'$ are \emph{matching}, and that $P_j$ is $P_i$'s
\emph{partner} for the session.

At most one participant in the game is \emph{active} at any given time.
Initially the adversary is active.  The adversary may \emph{activate} a
session in one of two ways.
\begin{enumerate}
\item It may \emph{create a session} of a party~$P_i$, by selecting a
  session-id~$s \in \Bin^{\ell_S}$ and a partner $j$.  There is no
  requirement that $P_j$ ever have a matching session.  However, all sessions
  of a party must be distinct, i.e., sessions with the same partner must have
  different session-ids.
\item It may \emph{deliver a message}~$\mu \in \Bin^*$, from party~$P_j$, to
  an existing session~$S = (P_i, P_j, s)$.  There is no requirement that any
  party previously sent $\mu$: the adversary is free to make up messages as
  it sees fit.
\end{enumerate}
The adversary becomes inactive, and the session becomes active.  The session
performs some computation, according to its protocol, and may request a
message~$\mu$ be delivered to the matching session running in its partner
(which may not exist).  The session may also \emph{terminate}.  In the case
we are interested in, of key-exchange protocols, a session~$S = (P_i, P_j,
s)$ may terminate in one of two ways:
\begin{enumerate}
\item it may \emph{complete}, outputting $(i, j, s, K)$, for some
  \emph{session key}~$K$, or
\item it may \emph{abort}, outputting $(i, j, s, \bot)$.
\end{enumerate}
Once it has performed these actions, the session deactivates and the
adversary becomes active again.  The adversary is given the message~$\mu$, if
any, and informed of whether the session completed or aborted, but, in the
case of completion, not of the value of the key~$K$.  A session is
\emph{running} if it has been created and has not yet terminated.

\subsubsection{Other adversarial actions}
As well as activating sessions, the adversary has other capabilities, as
follows.
\begin{itemize}
\item It may \emph{expire} any session~$S$, causing the owning party to
  `forget' the session key output by that session.
\item It may \emph{corrupt} any party~$P_i$, at will: the adversary learns
  the entire state of the corrupted party, including its initial
  input~$\mathbf{i}[i]$, the state of any sessions it was running at the
  time, and the session keys of any completed but unexpired sessions.  Once
  corrupted, a party can no longer be activated.  Of course, the adversary
  can continue to send messages allegedly from the corrupted party.
\item It may \emph{reveal the state} of a running session~$S$, learning any
  interesting values specific to that session, but \emph{not} the owning
  party's long-term secrets.
\item It may \emph{reveal the session-key} of a completed session~$S$.
\item It may elect to be \emph{challenged} with a completed session~$S$,
  provided.  Challenge sessions form part of the security notion for
  key-exchange protocols.  See below for more details.
\end{itemize}
We say that a session $S = (P_i, P_j, s)$ is \emph{locally exposed} if
\begin{itemize}
\item it has had its state revealed,
\item it has had its session-key revealed, or
\item $P_i$ has been corrupted, and $S$ had not been expired when this
  happened.
\end{itemize}
A session is \emph{exposed} if it is locally exposed, or if its matching
session exists and has been locally exposed.

At the beginning of the game, a bit $b^*$ is chosen at random.  The adversary
may choose to be \emph{challenged} with any completed, unexposed
session;\footnote{%
  The original Canetti-Krawczyk definition restricts the adversary to a
  single challenge session, but our proof works independent of the number of
  challenge sessions, so we get a stronger result by relaxing the requirement
  here.)}
the adversary is then given either the session's key -- if $b^* = 1$ -- or a
string chosen at random and independently of the game so far from a
protocol-specific distribution -- if $b^* = 0$.  At the end of the game, the
adversary outputs a single bit~$b$.

\subsubsection{SK-security}
We've now described the game; it is time to explain the adversary's goal in
it.  The adversary \emph{wins} the game if either
\begin{enumerate}
\item two unexposed, matching sessions complete, but output different
  keys,\footnote{%
    The original Canetti-Krawczyk definition differs slightly here.  It
    requires that `if two \emph{uncorrupted} parties complete matching
    sessions then they both output the same key' [original emphasis].  This
    can't be taken at face value, since none of the protocols they claim to
    be secure actually meet this requirement: they meet only the weaker
    requirement that parties completing matching sessions output different
    keys with negligible probability.  We assume here that this is what they
    meant.}
  or
\item the adversary correctly guesses the hidden bit~$b^*$.
\end{enumerate}
More formally, we make the following definition.
\fi
\begin{definition}[SK-security]
  \label{def:sk}
  Let $\Pi^{H_0(\cdot), H_1(\cdot), \ldots}$ be a key-exchange protocol
  which makes use of random oracles $H_0(\cdot)$, $H_1(\cdot)$, \dots, and
  let $A$ be an adversary playing the game described \ifshort in
  \cite{canetti-krawczyk-2001:secure-channels}\else previously\fi, where $n$
  parties run the protocol~$\Pi$.  Let $V$ be the event that any pair of
  matching, unexposed sessions completed, but output different session keys.
  Let $W$ be the event that the adversary's output bit matches the game's
  hidden bit~$b^*$.  We define the adversary's \emph{advantage against the
    SK-security of the protocol~$\Pi$} to be
  \[ \Adv{sk}{\Pi}(A, n) = \max(\Pr[V], 2\Pr[W] - 1). \]
  Furthermore, we define the \emph{SK insecurity function of the
  protocol~$\Pi$} to be
  \[ \InSec{sk}(\Pi; t, n, q_S, q_M, q_{H_0}, q_{H_1}, \dots) =
       \max_A \Adv{sk}{\Pi}(A, n)
  \]
  where the maximum is taken over all adversaries~$A$ with total running
  time~$t$ (not including time taken by the parties), create at most $q_S$
  sessions, deliver at most $q_M$~messages, and (if applicable) make at most
  $q_{H_i}$ random-oracle queries to each random oracle $H_i(\cdot)$.
\end{definition}


\subsection{Security}

In order to analyse our protocol $\Wkx^{G, \E}$ properly, we must describe
exactly how it fits into our formal model.

\subsubsection{Sessions and session-ids}
Our formal model introduced the concept of sessions, which the informal
description of section~\ref{sec:kx-overview} neglected to do.  (One could
argue that we described a single session only.)  As we shall show in
section~\ref{sec:kx-insecure}, our protocol is \emph{insecure} unless we
carefully modify it to distinguish between multiple sessions.

In the model, distinct key-exchange sessions are given distinct partners and
session-ids.  In order to prevent sessions interfering with each other, we
shall make explicit use of the session-ids.

Suppose the session-ids are $\ell_S$-bit strings.  We expand the domain of
the random oracle $H_I$ so that it's now
\[ H_I\colon G \times \Bin^{\ell_S} \times G \times G \to \Bin_{\ell_I}. \]

\subsubsection{Messages}
We split the messages our protocols into two parts: a \emph{type}~$\tau$ and
a \emph{body}~$\mu$.  We assume some convenient, unambiguous encoding of
pairs $(\tau, \mu)$ as bit-strings.  For readability, we present message
types as text strings, e.g., `\cookie{challenge}', though in practice one
could use numerical codes instead.

The message body itself may be a tuple of values, which, again, we assume are
encoded as bit-strings in some convenient and unambiguous fashion.  We shall
abuse the notation for the sake of readability by dropping a layer of nesting
in this case: for example, we write $(\cookie{hello}, x, y, z)$ rather than
$\bigl(\cookie{hello}, (x, y, z)\bigr)$.

\subsubsection{The protocol}
Our protocol is represented by three functions, shown in
figure~\ref{fig:wkx-formal}.
\begin{itemize}
\item $\id{init}(n)$ is the initialization function, as described in
  section~\ref{sec:um}.  It outputs a pair $(\mathbf{p}, \mathbf{i})$, where
  $\mathbf{i}[i]$ is the private key of party~$P_i$ and $\mathbf{p}[i]$ is
  the corresponding public key.  Only $P_i$ is given $\mathbf{i}[i]$, whereas
  all parties and the adversary are given $\mathbf{p}$.
\item $\id{new-session}^{H_I(\cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
  (\mathbf{p}, x, i, j, s)$ is the new-session function.  This is executed by
  party~$P_i$ when the adversary decides to create a new session~$S = (P_i,
  P_j, s)$.  It is also given the relevant outputs of $\id{init}$, and
  allowed access to the random oracles $H_I$ and $H_K$.
\item $\id{message}^{H_I(\cdot, \cdot, \cdot, \cdot), H_K(\cdot)} (\tau,
  \mu)$ is the incoming-message function.  This is executed by a session when
  the adversary decides to deliver a message $(\tau, \mu)$ to it.  It makes
  use of the subsidiary functions $\id{msg-challenge}$ and
  $\id{msg-response}$ to handle the messages.
\end{itemize}
We observe that the protocol never aborts.  We could make it do so if it
receives an invalid message, but we prefer to ignore invalid messages for the
sake of robustness.\footnote{%
  Note that this protocol would therefore require modification before it was
  acceptable in the simulation-based model of
  \cite{shoup-1999:formal-model-key-exchange}.  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 \gf{q}$; \\
        $\mathbf{i}[i] \gets x$; \\
        $\mathbf{p}[i] \gets x P$; \- \\
      \RETURN $(\mathbf{p}, \mathbf{i})$;
    \- \\[\medskipamount]
    Function $\id{new-session}^{H_I(\cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
      (\mathbf{p}, x, i, j, s)$: \+ \\
      $X \gets \mathbf{p}[i]$;
      $X' \gets \mathbf{p}[j]$;
      $C \gets \emptyset$; \\
      $r \getsr \gf{q}$;
      $R \gets r P$;
      $Y \gets r X'$; \\
      $h \gets H_I(X, s, R, Y)$;
      $c \gets r \xor h$; \\
      \SEND $(\cookie{challenge}, R, c)$;
    \- \\[\medskipamount]
    Function $\id{message}^{H_I(\cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
      (\tau, \mu)$: \+ \\
      \IF $\tau = \cookie{challenge}$ \THEN $\id{msg-challenge}(\mu)$; \\
      \ELSE \IF $\tau = \cookie{response}$ \THEN $\id{msg-response}(\mu)$;
    \next
    Function $\id{msg-challenge}(\mu)$: \+ \\
      $(R', c') \gets \mu$; \\
      $Y' \gets x R'$; \\
      $h' \gets H_I(X', s, R', Y')$; \\
      $r' \gets c' \xor h'$; \\
      \IF $R' \ne r' P$ \THEN \RETURN; \\
      $C \gets C \cup \{R\}$; \\
      $Z \gets r R'$; \\
      $(K_0, K_1) \gets H_K(Z)$; \\
      $\chi \gets E_{K_0}(Y')$; \\
      \SEND $(\cookie{response}, R, \chi)$;
    \- \\[\medskipamount]
    Function $\id{msg-response}(\mu)$: \+ \\
      $(R', \chi') \gets \mu$; \\
      \IF $R' \notin C$ \THEN \RETURN; \\
      $Z \gets r R'$; \\
      $(K_0, K_1) \gets H_K(Z)$; \\
      $Y' \gets D_{K_0}(\chi')$; \\
      \IF $Y' \ne Y$ \THEN \RETURN; \\
      \OUTPUT $K_1$;
      \STOP;
  \end{program}

  \caption{Formalization of $\Wkx$}
  \label{fig:wkx-formal}
\end{figure}

\subsubsection{Session states}
We must specify what the adversary obtains when it chooses to reveal a
session's state.  Given the program in figure~\ref{fig:wkx-formal}, we can
see that the session state consists of the variables $(x, X, X', r, R, Y,
C)$.

However, $x$ is the owning party's long-term secret, and it seems
unreasonable to disclose this to an adversary who stops short of total
corruption.

The public keys $X$ and $X'$ are part of the adversary's input anyway, so
revealing them doesn't help.  Similarly, the set $C$ of valid challenges
could have been computed easily by the adversary, since a group element $R'
\in C$ if and only if the session $S$ responded to some message
$(\cookie{challenge}, R', c')$.

The value $R = r P$ is easily computed given $r$, and besides is sent in the
clear in the session's first message.  The expected response $Y = r X'$ is
also easily computed from $r$.  The converse is also true, since $r$ can be
recovered from $R$ and $c$ in the session's challenge message and the value
$Y$.  Besides, $r$ is necessary for computing $Z$ in response to incoming
challenges.

We conclude that the only `interesting' session state is $r$.

\subsubsection{Security}
Having formally presented the protocol, we can now state our main theorem
about its security.  The proof is given in \ifshort the full version of the
paper\else appendix~\ref{sec:sk-proof}\fi.
\begin{theorem}[SK-security of $\Wkx$]
  \label{thm:sk}
  Let $G$ be a cyclic group.  Let $\E = (\kappa, E, D)$ be a symmetric
  encryption scheme.  Then
  \begin{spliteqn*}
    \InSec{sk}(\Wkx^{G, \E}; t, n, q_S, q_M, q_I, q_K) \le
      2 q_S \bigl( \InSec{ind-cca}(\E; t', q_M, q_M) + {} \\
      \InSec{mcdh}(G; t', q_K) +
      n \,\InSec{mcdh}(G; t', q_M + q_I) \bigr) +
      \frac{n (n - 1)}{q} +
      \frac{2 q_M}{2^{\ell_I}}.
  \end{spliteqn*}
  where $t' = t + O(n) + O(q_S) + O(q_M q_I) + O(q_K)$.
\end{theorem}


\ifshort\else
\subsection{Insecure protocol variants}
\label{sec:kx-insecure}

It's important to feed the session-id and verifier's public key to the random
oracle $H_I$ when constructing the check-value~$c$.  Without these, the
protocol is vulnerable to attack.  In this section, we consider some variants
of our protocol which hash less information, and show attacks against them.

To simplify the presentation, we shall consider Alice and Bob, and a third
character Carol.  We shall be attacking a pair of matching sessions $A$
and~$B$, run by Alice and Bob respectively.  Let Alice and Bob's private keys
be $x_A$ and~$x_B$, and let their public keys be $X_A = x_A P$ and $X_B = x_B
P$ respectively.

\subsubsection{Protocol diagram notation}
In order to keep the presentation as clear as possible, we use a simple
diagrammatic notation for describing protocol runs.  A line of the form
\protocolrun{\textit{action} \ar[r] & \PRsession{S} & \textit{result}}
states that the adversary performs the given \textit{action} on session~$S$,
with the stated \textit{result}.  The \textit{action} may be
\begin{itemize}
\item \textsf{Create session $(P_i, P_j, s)$}: the session is created,
  running in party~$P_i$, with partner~$P_j$ and session-id~$s$.
\item \textsf{Receive $\mu$}: the session is activated with an incoming message~$\mu$.
\item \textsf{Session-state reveal}: The adversary requests the session's
  internal state.
\end{itemize}
The \textit{result} may be
\begin{itemize}
\item \textsf{Send $\mu'$}: the session requests the delivery of the
  message~$\mu'$.
\item \textsf{Complete: $K$}: the session completes, outputting the key~$K$.
\item \textsf{State: $\sigma$}: the session's state is revealed to
  be~$\sigma$.
\item \textsf{(Ignore)}: the result of the action is unimportant.
\end{itemize}

\subsubsection{Omitting the session-id}
Consider a protocol variant where session $S$ sets $h_S = H_I(X_N, R_S,
Y_S)$, where $N$ is the session's partner.  That is, we've omitted the
session-id from the hash.  An adversary can cross over two sessions between
Alice and Bob.  Here's how.

The attack assumes that Alice and Bob set up two pairs of matching sessions
with each other, thus.
\protocolrun{
  \PRcreate{Alice}{Bob}{s} & \PRsession{A} &
    \PRsend{challenge}{R_A, c_A} \\
  \PRcreate{Bob}{Alice}{s} & \PRsession{B} &
    \PRsend{challenge}{R_B, c_B} \\
  \PRcreate{Alice}{Bob}{s'} & \PRsession{A'} &
    \PRsend{challenge}{R_{A'}, c_{A'}} \\
  \PRcreate{Bob}{Alice}{s'} & \PRsession{B'} &
    \PRsend{challenge}{R_{B'}, c_{B'}}
}
Observe that the session pairs use distinct session-ids $s \ne s'$, so this
is allowed.  Now the adversary crosses over the challenges, using the second
pair of sessions to provide responses to the challenges issued by the first
pair.  By revealing the state in the second pair of sessions, the adversary
can work out the (probably different) session keys accepted by the first
pair.
\protocolrun{
  \PRreceive{challenge}{R_B, c_B} & \PRsession{A'} &
    \PRsend{response}{R_{A'}, E_{K_{A'B,0}}(x_A R_B)} \\
  \PRreceive{challenge}{R_A, c_A} & \PRsession{B'} &
    \PRsend{response}{R_{B'}, E_{K_{B'A,0}}(x_B R_A)} \\
  \PRreceive{challenge}{R_{A'}, c_{A'}} & \PRsession{A} & \PRignore \\
  \PRreceive{challenge}{R_{B'}, c_{B'}} & \PRsession{B} & \PRignore \\
  \PRreveal & \PRsession{A'} & r_{A'} \\
  \PRreveal & \PRsession{B'} & r_{B'} \\
  \PRreceive{response}{R_{B'}, E_{K_{B'A,0}}(x_B R_A)} & \PRsession{A} &
    \PRcomplete{K_{AB',1}} \\
  \PRreceive{response}{R_{A'}, E_{K_{A'B,0}}(x_A R_B)} & \PRsession{B} &
    \PRcomplete{K_{BA',1}} \\
}
The adversary can now compute $K_{AB'} = H_K(r_{B'} R_A)$ and $K_{B'A} =
H_K(r_{A'} R_B)$.  Safely in possession of both keys, the adversary can now
read and impersonate freely.

\subsubsection{Omitting the partner's public key}
Now consider a protocol variant where session $S$ sets $h_S = H_I(s, R_S,
Y_S)$, where $s$ is the session-id.  An adversary can use a sessions with
Carol to attack a session between Alice and Bob.  Here's how the sessions are
set up.
\protocolrun{
  \PRcreate{Alice}{Bob}{s} & \PRsession{A} &
    \PRsend{challenge}{R_A, c_A} \\
  \PRcreate{Bob}{Alice}{s} & \PRsession{B} &
    \PRsend{challenge}{R_B, c_B} \\
  \PRcreate{Alice}{Carol}{s} & \PRsession{A'} &
    \PRsend{challenge}{R_{A'}, c_{A'}} \\
  \PRcreate{Bob}{Carol}{s} & \PRsession{B'} &
    \PRsend{challenge}{R_{B'}, c_{B'}}
}
Although each of Alice and Bob have two sessions with session-id~$s$, this is
allowed, since they are with different partners.  The rest of the attack in
fact proceeds identically to the previous case.
\fi

\subsection{Deniability}
\label{sec:denial}

We have claimed that the Wrestlers key-exchange protocol is \emph{deniable}.
In this section, we define what we mean, explain the limits of the
deniablility of the protocol as currently presented, fix the protocol with an
additional pass (which can be collapsed to a single message flow by breaking
the protocol's symmetry), and prove the deniability of the resulting
protocol.

Our notion of deniability is taken from Di~Raimondo, Gennaro and Krawczyk
\cite{raimondo-2006:deniable-authn-key-exchange}, except that, as usual, we
opt for a concrete security approach.

\subsubsection{Discussion}
Our definition for deniability is that, for any adversary interacting with
participants in the protocol, a simulator exists which can compute the same
things as the adversary.  In particular, since an adversary could output a
transcript of the interactions between itself and the parties, it would
follow that a simulator could do this too.  If the simulator is effective,
its output is indistinguishable from that of the real adversary, and hence no
`judge' (distinguisher) should be persuaded by evidence presented by someone
who claims to have witnessed or participated in an interaction.

We work again the model described in~\ref{sec:um}.  That is, our adversary
has complete control over the ordering and delivery of all messages.  The
adversary is also able, at any time, to reveal the state of any session.
However, deniability is obviously impossible against an adversary who can
\emph{corrupt} other parties, since simulating such an adversary's actions
would necessarily require the simulator to compute private keys corresponding
to the known public keys, and this is (we believe) difficult, because an
efficient algorithm for doing this could easily attack our protocol, which we
already proved secure.  Therefore, we forbid the adversary from corrupting
parties.

In order to allow the adversary to participate in the protocol, rather than
merely observing it, we need to give it one or more private keys.  We could
modify the initialization function \id{init} from figure~\ref{fig:wkx-formal}
to give the adversary a private key, but there's an easier way: we can just
give the adversary a number of private keys in its auxiliary input.

\subsubsection{Definitions}
Let $\Pi$ be a key-exchange protocol, in the model described in
section~\ref{sec:um}.  We use the simulation framework of
section~\ref{sec:sim}.  We define the initialization function $I_\Pi$ to be
the initialization function of $\Pi$, as before, and the corresponding
world~$W_\Pi(\iota, \sigma, \tau, \mu)$ is a fairly straightforward mapping
of the adversary's possible actions to the simulation model:
\begin{itemize}
\item The invocation $\cookie{new-session}$ with $\mu = (i, j, s)$ creates a
  new session on party~$P_i$, with partner~$P_j$ and session-id~$s$.  The
  reply $\rho = (\delta, m)$ is a \emph{decision} $\delta \in
  \{\cookie{continue}, \cookie{abort}, \cookie{complete}\}$ and an output
  message $m \in \Bin^* \cup \{\bot\}$.  If $m \ne \bot$ then $m$ is a
  message to be sent to the matching session (if any).
\item The invocation $\cookie{deliver}$ with $\mu = (i, j, s, m)$ delivers
  message $m$ to the session $S = (P_i, P_j, s)$.  The response $\rho$ is as
  for $\cookie{new-session}$ invocations.
\item The invocation $\cookie{reveal-session-state}$ with $\mu = (i, j, s)$
  reveals to the adversary the state of the running session $S = (P_i, P_j,
  s)$.  The response $\rho$ is the session's state if $S$ is indeed a running
  session, or $\bot$ otherwise.
\item The invocation $\cookie{reveal-session-key}$ with $\mu = (i, j, s)$
  reveals to the adversary the session-key of the completed session~$S =
  (P_i, P_j, s)$.  The response $\rho$ is the session key~$K$ if the session
  is indeed complete, or $\bot$ otherwise.
\end{itemize}
There are no invocations corresponding to the adversary actions of corrupting
parties (since deniability against an corrupting adversary is impossible, as
discussed earlier), or session expiry or challenging (since they are useless
in this context).

We measure the deniability of a protocol~$\Pi$, using a given simulator~$S$,
by the insecurity function $\InSec{sim}(W_\Pi, I_\Pi, S; t_D, t_A,
\mathcal{Q}_D, \mathcal{Q}_A, \mathcal{R}, \mathcal{U})$ of
definition~\ref{def:sim}.  The interaction bounds $\mathcal{R} = (q_S, q_M)$
we place on the adversary are on the number ($q_S$) of \cookie{new-session}
and ($q_M$) \cookie{deliver} invocations it makes.

We shall (informally) say that a protocol~$\Pi$ is deniable if there is a
simulator~$S_\Pi$ for which the insecurity function is small for appropriate
resource bounds on the adversary and distinguisher.

\subsubsection{The current protocol}
As it stands, $\Wkx$ isn't deniable, according to our definition, for
arbitrary auxiliary inputs.  Let's see why.

Suppose that Bob is an informant for the secret police, and wants to convince
a judge that Alice is involved in subversive activities in cyberspace.
Unfortunately, Bob's job is difficult, because of the strong zero-knowledge
nature of the Wrestlers identification protocol.  However, Bob can work with
the judge to bring him the evidence necessary to convict Alice.  Here's how.

Alice's public key is $A$, and Bob's public key is $B$.  The judge chooses
some session-id $s$, and $r \inr \gf{q}$.  He computes $R = r P$ and $c =
r \xor H_I(B, s, R, r A)$, and gives Bob the triple $(s, R, c)$, keeping $r$
secret.  Bob can now persuade Alice to enter into a key-exchange with him,
with session-id $s$.  He uses $(R, c)$ as his challenge message.  When Alice
sends back her response $(R', \chi)$ (because Bob's challenge is correctly
formed), Bob aborts and shows $(R', \chi)$ to the judge.  The judge knows $r$
and can therefore decrypt $\chi$ and check the response.  If it's wrong, then
Bob was cheating and gets demoted -- he can't get the right answer by himself
because that would require him to impersonate Alice.  If it's right, Alice is
really a subversive element and `disappears' in the night.

We shall show in theorem~\ref{thm:denial} below that this is basically the
only attack against the deniability of the protocol.  However, we can do
better.

\subsubsection{Fixing deniability}
We can fix the protocol to remove even the attack discussed above.  The
change is simple: we feed \emph{both} parties' challenges to the hash
function~$H_I$ rather than just the sender's.  We use a five-argument hash
function (random oracle) $H_I\colon G^2 \times \Bin^{\ell_S} \times G^2 \to
\Bin^{\ell_I}$.  We introduce a new message pass at the beginning of the
protocol: each session simply sends its challenge point $R = r P$ in the
clear as a `pre-challenge'.  The actual challenge is $R$ and $c = r \xor
H_I(X, R', s, R, c)$, where $R'$ is the challenge of the matching session.

By breaking symmetry, we can reduce the communication complexity of this
variant to four messages.  As before, we analyse the symmetrical version.
The extra flow might seem a high price to pay, but we shall see that it has
additional benefits beyond deniability.

A summary of the new protocol is shown in figure~\ref{fig:wdkx}, and the
formal description is shown in figure~\ref{fig:wdkx-formal}.

\begin{figure}
  \begin{description}
  \item[Setup] Group $G = \langle P \rangle$; $\#G = q$ is prime.
    $H_I(\cdot, \cdot, \cdot, \cdot, \cdot)$ and $H_K(cdot)$ are secure
    hashes.  $\E = (\kappa, E, D)$ is an IND-CCA2 symmetric encryption
    scheme.
  \item[Parties] $U_i$ for $0 \le i < n$.
  \item[Private keys] $x_i \inr \gf{q}$.
  \item[Public keys] $X_i = x_i P$.
  \end{description}

  \begin{protocol}
    $r_i \getsr I$; $R_i \gets r_i P$; &
    $r_j \getsr I$; $R_j \gets r_j P$; \\
    \send{->}{R_i}
    \send{<-}{R_j}
    $c_i \gets r_i \xor H_I(R_j, X_i, s, R_i, r_i X_j)$; &
    $c_j \gets r_j \xor H_I(R_i, X_j, s, R_j, r_j X_i)$; \\
    \send{->}{(R_i, c_i)}
    \send{<-}{(R_j, c_j)}
    Check $R_j = \bigl(c_j \xor H_I(x_i R_j)\bigr) P$; &
    Check $R_i = \bigl(c_i \xor H_I(x_j R_i)\bigr) P$; \\
    $Z \gets r_i R_j$; $(K_0, K_1) \gets H_K(Z)$; &
    $Z \gets r_j R_i$; $(K_0, K_1) \gets H_K(Z)$; \\
    $\chi_i \gets E_{K_0}(x_i R_j)$; &
    $\chi_j \gets E_{K_0}(x_j R_i)$; \\
    \send{->}{(R_i, \chi_i)}
    \send{<-}{(R_j, \chi_j)}
    Check $D_{K_0}(\chi_j) = r_i X_j$; &
    Check $D_{K_0}(\chi_i) = r_j X_i$; \\
    Shared key is $K_1$. & Shared key is $K_1$.
  \end{protocol}

  \caption{Summary of the Deniable Wrestlers Key Exchange protocol, $\Wdkx$}
  \label{fig:wdkx}
\end{figure}

\begin{figure}
  \begin{program}
    Function $\id{init}(n)$: \+ \\
      \FOR $i \in \Nupto{n}$ \DO \\ \ind
        $x \getsr \gf{q}$; \\
        $\mathbf{i}[i] \gets x$; \\
        $\mathbf{p}[i] \gets x P$; \- \\
      \RETURN $(\mathbf{p}, \mathbf{i})$;
    \- \\[\medskipamount]
    Function $\id{new-session}^{H_I(\cdot, \cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
      (\mathbf{p}, x, i, j, s)$: \+ \\
      $X \gets \mathbf{p}[i]$;
      $X' \gets \mathbf{p}[j]$;
      $C \gets \emptyset$; \\
      $r \getsr \gf{q}$;
      $R \gets r P$;
      $Y \gets r X'$; \\
      \SEND $(\cookie{pre-challange}, R)$;
    \- \\[\medskipamount]
    Function $\id{message}^{H_I(\cdot, \cdot, \cdot, \cdot, \cdot), H_K(\cdot)}
      (\tau, \mu)$: \+ \\
      \IF $\tau = \cookie{pre-challenge}$ \THEN
        $\id{msg-pre-challenge}(\mu)$; \\
      \ELSE \IF $\tau = \cookie{challenge}$ \THEN
        $\id{msg-challenge}(\mu)$; \\
      \ELSE \IF $\tau = \cookie{response}$ \THEN $\id{msg-response}(\mu)$;
    \next
    Function $\id{msg-pre-challenge}(\mu)$: \+ \\
      $R' \gets \mu$; \\
      $h \gets H_I(R', X, s, R, c)$; \\
      $c \gets r \xor h$; \\
      \SEND $(\id{msg-challenge}, R, c)$;
    \- \\[\medskipamount]
    Function $\id{msg-challenge}(\mu)$: \+ \\
      $(R', c') \gets \mu$; \\
      $Y' \gets x R'$; \\
      $h' \gets H_I(R, X', s, R', Y')$; \\
      $r' \gets c' \xor h'$; \\
      \IF $R' \ne r' P$ \THEN \RETURN; \\
      $C \gets C \cup \{R\}$; \\
      $Z \gets r R'$; \\
      $(K_0, K_1) \gets H_K(Z)$; \\
      $\chi \gets E_{K_0}(Y')$; \\
      \SEND $(\cookie{response}, R, \chi)$;
    \- \\[\medskipamount]
    Function $\id{msg-response}(\mu)$: \+ \\
      $(R', \chi') \gets \mu$; \\
      \IF $R' \notin C$ \THEN \RETURN; \\
      $Z \gets r R'$; \\
      $(K_0, K_1) \gets H_K(Z)$; \\
      $Y' \gets D_{K_0}(\chi')$; \\
      \IF $Y' \ne Y$ \THEN \RETURN; \\
      \OUTPUT $K_1$;
      \STOP;
  \end{program}

  \caption{Deniable key-exchange: formalization of $\Wdkx$}
  \label{fig:wdkx-formal}
\end{figure}

The security of this variant is given by the following theorem, whose proof
is \ifshort given in the full version of this paper\else in
appendix~\ref{sec:sk2-proof}\fi.
\begin{theorem}[SK-security of $\Wdkx$]
  \label{thm:sk2}
  Let $G$ be a cyclic group.  Let $\E = (\kappa, E, D)$ be a symmetric
  encryption scheme.  Then
  \[ \InSec{sk}(\Wdkx^{G, \E}; t, n, q_S, q_M, q_I, q_K) =
       \InSec{sk}(\Wkx^{G, \E}; t, n, q_S, q_M, q_I, q_K)
  \]
\end{theorem}

\subsubsection{Deniability of the Wrestlers protocols}
In order to quantify the level of deniability our protocols provide, we shall
impose a limit on the auxiliary input to the adversary.  In particular, we
shall use $\mathcal{U}$ of definition~\ref{def:sim} to count the number of
\emph{challenges} in the auxiliary input.  That is, $\mathcal{U} = n_C$ is
the number of tuples $(i, j, s, R', R, c)$ for which there is an $r$ such
that $R = r P$ and $c = r \xor H_I(R', X_j, s, R, r X_i)$ (or without the
$R'$ for $\Wkx$).

With this restriction in place, we can state the following theorem about the
deniability of our protocols.
\begin{theorem}[Deniability of $\Wkx$ and $\Wdkx$]
  \label{thm:denial}
  There exist simulators $S_\Wkx$ and $\Wdkx$ such that
  \[ \InSec{sim}(W_{\Wkx^{G, \E}}, I_{\Wkx^{G, \E}}, S_{\Wkx^{G, \E}};
                 t_D, t_A, \mathcal{Q}_D, \mathcal{Q}_A, (q_S, q_M), 0) \le
       \frac{q_M}{2^{\ell_I}}
  \]
  and
  \iffancystyle\[\else\begin{spliteqn*}\fi
    \InSec{sim}(W_{\Wdkx^{G, \E}}, I_{\Wdkx^{G, \E}}, S_{\Wdkx^{G, \E}};
                t_D, t_A, \mathcal{Q}_D, \mathcal{Q}_A, (q_S, q_M), n_C) \le
    \iffancystyle\else\\\fi
       \frac{n_C q_S}{\#G} +
       \frac{q_M}{2^{\ell_I}}.
  \iffancystyle\]\else\end{spliteqn*}\fi
  The running time of the simulators is $O(t_A) + O(\mathcal{Q}_A q_M)$.
\end{theorem}
\begin{longproof}{The proof of this theorem can be found in the full version
    of this paper.}
  The simulators $S_\Wkx$ and $S_\Wdkx$ are very similar.  We describe both
  here.  Both are fake-world simulators, working as follows.
  \begin{enumerate}
  \item Initially, it constructs simulated parties $P_i$, for $0 \le i < n$,
    giving each the public key $X_i$ from the common input.
  \item Suppose the adversary requests creation of a new session $S = (P_i,
    P_j, s)$.  Then the simulator creates a new session, including a random
    value $r_S \inr \gf{q}$, and computes $R_S = r_S P$, and $Y_S = r_S
    X_j$.  For $\Wdkx$, it sends the message $(\cookie{pre-challenge}, R_S)$;
    for $\Wkx$, it additionally computes $h = H_I(X_i, s, R_S, Y_S)$ and
    sends $(\cookie{challenge}, R_S, r_S \xor h)$.
  \item Suppose, for $\Wdkx$, the adversary sends a message
    $(\cookie{pre-challenge}, R')$ to a session~$S = (P_i, P_j, s)$.  The
    simulator computes $h = H_I(R', X_i, s, R_S, Y_S)$, and sends
    $(\cookie{challenge}, R_S, r_S \xor h)$.
  \item Suppose the adversary sends a message $(\cookie{challenge}, R', c')$
    to session $S = (P_i, P_j, s)$.  The simulator doesn't know $x_i$.
    \begin{enumerate}
    \item If $R' = R_T$ for some other simulated session $T$, then the
      simulator knows $r_T$ such that $R_T = r_T P$.  Let $Y' = r_T X_i$.
      The simulator computes $h = H_I(X_j, s, R', Y')$ (resp.\ $h = H_I(R_S,
      X_j, s, R', Y')$) for $\Wkx$ (resp.\ $\Wdkx$) and checks that $r_T = c'
      \xor h$.  If not, the simulator discards the message.  Otherwise, it
      computes $(K_0, K_1) = H_K(r_S R')$, and sends the message
      $(\cookie{response}, R, E_{K_0}(Y'))$.
    \item \label{en:simextract} Otherwise the simulator runs the extractor
      $T_\Wident$ on the adversary's history of queries $H_I(X_j, s, R',
      \cdot)$ (resp.\ $H_I(R_S, X_j, s, R', \cdot)$) for $\Wkx$ (resp.\
      $\Wdkx$).  The extractor returns $(r', Y')$.  If $Y' = \bot$ then the
      simulator ignores the message.  Otherwise, the simulator computes
      $(K_0, K_1) = H_K(r R')$ and sends back $(\cookie{response}, R,
      E_{K_0}(Y'))$.
    \end{enumerate}
  \item Suppose the adversary sends a message $(\cookie{response}, R', \chi)$
    to session $S = (P_i, P_j, s)$.  The simulator computes $(K_0, K_1) =
    H_K(r_S R')$, and decrypts $Y' = D_{K_0}(\chi)$.  If $Y' \ne Y_S$ then
    the simulator discards the message.  Otherwise, it makes the simulated
    session complete, and outputs key $K_1$.
  \item Finally, if the adversary reveals a session's state, the simulator
    reveals $r_S$ as required; if the adversary reveals a session-key, the
    simulator reveals the $K_1$ it output.
  \end{enumerate}
  The only point where the simulation fails to be perfect is in
  \ref{en:simextract}.  Let $R'$ and $c'$ be the values from an incoming
  challenge message to session $S = (P_i, P_j, s)$.  Let $r'$ be such that
  $R' = r' P$ and let $Y' = r' X_i$.  If a random-oracle query $H_I(X_j, s,
  R', Y')$ (or $H_I(R_S, X_j, s, R', Y')$ for $\Wdkx$) has been issued, then
  there are a number of possibilities.  Let $h'$ be the result of this query.
  \begin{itemize}
  \item The adversary made this query.  Then the extractor will find it and
    return $Y'$ if $c' = h' \xor r'$, or $\bot$ otherwise.
  \item Some simulated session $U = (P_{i'}, P_{j'}, s')$ made this query.
    But simulated sessions only make $H_I$-queries when constructing
    challenges, so $R' = R_U$ for some session~$U$.  But the simulator does
    something different in that case.
  \item In $\Wdkx$, the quadruple $(s, R_S, R', c')$ came from the
    adversary's auxiliary input.  In this case the simulator must fail.  But
    $R_S = r_S P$, and $r_S$ was chosen uniformly at random.  If there are at
    most $n_C$ challenge sets in the auxiliary input then this happens with
    probability at most $n_C/\#G$ for any given session.
  \end{itemize}
  We conclude that the simulator fails with probability
  \[ \frac{q_M}{2^{\ell_I}} + \frac{q_S n_C}{\#G}. \]
  (Note that we only consider $n_C = 0$ for $\Wkx$.)  No adversary can
  distinguish the simulator from a real interaction unless the simulator
  fails, and the simulator is a fake-world simulator.  We therefore apply
  proposition~\ref{prop:fakesim}; the theorem follows.
\end{longproof}

\ifshort\else
\subsection{Practical issues}
\label{sec:practice}

\subsubsection{Denial of service from spoofers}
The adversary we considered in~\ref{sec:um} is very powerful.  Proving
security against such a powerful adversary is good and useful.  However,
there are other useful security properties we might like against weaker
adversaries.

Eavesdropping on the Internet is actually nontrivial.  One needs control of
one of the intermediate routers between two communicating parties.  (There
are tricks one can play involving subversion of DNS servers, but this is also
nontrivial.)  However, injecting packets with bogus source addresses is very
easy.

Layering the protocol over TCP \cite{rfc793} ameliorates this problem because
an adversary needs to guess or eavesdrop in order to obtain the correct
sequence numbers for a spoofed packet; but the Wrestlers protocol is
sufficiently simple that we'd like to be able to run it over UDP
\cite{rfc768}, for which spoofing is trivial.

Therefore, it's possible for anyone on the 'net to send Alice a spurious
challenge message $(R, c)$.  She will then compute $Y = a R$, recover $r' = c
\xor H_I(\ldots, R, Y)$ check that $R = r' P$ and so on.  That's at least two
scalar multiplications to respond to a spoofed packet, and even with very
efficient group operations, coping with this kind of simple denial-of-service
attack might be difficult.

A straightforward solution is to use the Deniable variant of the protocol,
and require a challenge to quote its matching session's challenge $R'$ in its
challenge.  That is, upon receiving a $(\cookie{pre-challenge}, R')$, the
session sends $(\cookie{challenge}, R', R, c)$.  Alice then rejects any
\emph{incoming} challenge message which doesn't quote her current challenge
value.  Now only eavesdroppers can force her to perform expensive
computations.

Indeed, one need not quote the entire challenge $R'$: it suffices to send
some short hard-to-guess hash of it, maybe just the bottom 128 bits or so.

This can't reduce security.  Consider any adversary attacking this protocol
variant.  We can construct an adversary which attacks the original protocol
just as efficiently.  The new adversary attaches fake $R'$ values to
challenges output by other parties, and strips them off on delivery,
discarding messages with incorrect $R'$ values.

\subsubsection{Key confirmation}
Consider an application which uses the Wrestlers protocol to re-exchange keys
periodically.  The application can be willing to \emph{receive} incoming
messages using the new key as soon as the key exchange completes
successfully; however, it should refrain from \emph{sending} messages under
the new key until it knows that its partner has also completed.  The partner
may not have received the final response message, and therefore be unwilling
to accept a new key; it will therefore (presumably) reject incoming messages
under this new key.

While key confirmation is unnecessary for \emph{security}, it has
\emph{practical} value, since it solves the above problem.  If the
application sends a \cookie{switch} message when it `completes', it can
signal its partner that it is indeed ready to accept messages under the new
key.  Our implementation sends $(\cookie{switch-rq}, E_{K_0}(H_S(0, R, R')))$
as its switch message; the exact contents aren't important.  Our
retransmission policy (below) makes use of an additional message
\cookie{switch-ok}, which can be defined similarly.

It's not hard to show that this doesn't adversely affect the security of the
protocol, since the encrypted message is computed only from public values.
In the security proof, we modify the generation of \cookie{response}
messages, so that the plaintexts are a constant string rather than the true
responses, guaranteeing that the messages give no information about the
actual response.  To show this is unlikely to matter, we present an adversary
attacking the encryption scheme by encrypting either genuine responses or
fake constant strings.  Since the adversary can't distinguish which is being
encrypted (by the definition of IND-CCA security,
definition~\ref{def:ind-cca}), the change goes unnoticed.  In order to allow
incorporate our switch messages, we need only modify this adversary, to
implement the modified protocol.  This is certainly possible, since the
messages contain (hashes of) public values.  We omit the details.

However, while the extra message doesn't affect the security of our protocol,
it would be annoying if an adversary could forge the switch request message,
since this would be a denial of service.  In the strong adversarial model,
this doesn't matter, since the adversary can deny service anyway, but it's a
concern against less powerful adversaries.  Most IND-CCA symmetric encryption
schemes also provide integrity of plaintexts
\cite{bellare-namprempre-2000:authn-enc-notions} (e.g., the
encrypt-then-MAC generic composition approach
\cite{bellare-namprempre-2000:authn-enc-notions,%
  krawczyk-2001:order-enc-authn},
and the authenticated-encryption modes of
\cite{rogaway-2001:ocb,bellare-2004:eax,%
  mcgrew-viega-2004:gcm-security-performance}),
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
transmitting datagrams.  However, it's very efficient, and rather attractive
as a transport for datagram-based applications such as virtual private
networks (VPNs).  Since UDP is a best-effort rather than a reliable
transport, it can occasionally drop packets.  Therefore it is necessary for a
UDP application to be able to retransmit messages which appear to have been
lost.

We recommend the following simple retransmission policy for running the
Wrestlers protocol over UDP.
\begin{itemize}
\item Initially, send out the \cookie{pre-challenge} message every minute.
\item On receipt of a \cookie{pre-challenge} message, send the corresponding
  full \cookie{challenge}, but don't retain any state.
\item On receipt of a (valid) \cookie{challenge}, record the challenge value
  $R'$ in a table, together with $K = (K_0, K_1)$ and the response $Y' = x
  R'$.  If the table is full, overwrite an existing entry at random.  Send
  the corresponding \cookie{response} message, and retransmit it every ten
  seconds or so.
\item On receipt of a (valid) \cookie{response}, discard any other
  challenges, and stop sending \cookie{pre-challenge} and \cookie{response}
  retransmits.  At this point, the basic protocol described above would
  \emph{accept}, so the key $K_1$ is known to be good.  Send the
  \cookie{switch} message, including its response to the (now known-good)
  sender's challenge.
\item On receipt of a (valid) \cookie{switch}, send back a \cookie{switch-ok}
  message and stop retransmissions.  It is now safe to start sending messages
  under $K_1$.
\item On receipt of a (valid) \cookie{switch-ok}, stop retransmissions.  It
  is now safe to start sending messages under $K_1$.
\end{itemize}

\subsubsection{Key reuse}
Suppose our symmetric encryption scheme $\E$ is not only IND-CCA secure
(definition~\ref{def:ind-cca}) but also provides integrity of plaintexts
\cite{bellare-namprempre-2000:authn-enc-notions} (or, alternatively,
is an AEAD scheme \cite{rogaway-2002:aead}.  Then we can use it to construct
a secure channel, by including message type and sequence number fields in the
plaintexts, along with the message body.  If we do this, we can actually get
away with just the one key $K = H_K(Z)$ rather than both $K_0$ and $K_1$.

To do this, it is essential that the plaintext messages (or additional data)
clearly distinguish between the messages sent as part of the key-exchange
protocol and messages sent over the `secure channel'.  Otherwise, there is a
protocol-interference attack: an adversary can replay key-exchange
ciphertexts to insert the corresponding plaintexts into the channel.

We offer a sketch proof of this claim in appendix~\ref{sec:sc-proof}.
\fi

%%%--------------------------------------------------------------------------
\section{Conclusions}
\label{sec:conc}

We have presented new protocols for identification and authenticated
key-exchange, and proven their security.  We have shown them to be efficient
and simple.  We have also shown that our key-exchange protocol is deniable.
Finally, we have shown how to modify the key-exchange protocol for practical
use, and proven that this modification is still secure.

%%%--------------------------------------------------------------------------
\section{Acknowledgements}

The Wrestlers Protocol is named after the Wrestlers pub in Cambridge where
Clive Jones and I worked out the initial design.

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

\bibliography{mdw-crypto}

%%%--------------------------------------------------------------------------
\ifshort\def\next{\end{document}}\expandafter\next\fi
\appendix
\section{Proofs}

\subsection{Proof of theorem~\ref{thm:sk}}
\label{sec:sk-proof}

Before we embark on the proof proper, let us settle on some notation.  Let
$P_i$ be a party.  Then we write $x_i$ for $P_i$'s private key and $X_i = x_i
P$ is $P_i$'s public key.  Let $S = (P_i, P_j, s)$ be a session.  We write
$r_S$ for the random value chosen at the start of the session, and $R_S$,
$c_S$ etc.\ are the corresponding derived values in that session.

The proof uses a sequence of games.  For each game~$\G{i}$, let $V_i$ be the
event that some pair of unexposed, matching sessions both complete but output
different keys, and let $W_i$ be the event that the adversary's final output
equals the game's hidden bit~$b^*$.  To save on repetition, let us write
\[ \diff{i}{j} = \max(|\Pr[V_i] - \Pr[V_j]|, |\Pr[W_i] - \Pr[W_j]|). \]
Obviously,
\[ \diff{i}{j} \le \sum_{i\le k<j} \diff{k}{k + 1}. \]

Here's a quick overview of the games we use.
\begin{itemize}
\item $\G0$ is the original SK-security game.
\item In $\G1$, we abort the game unless all parties' public keys are
  distinct.  Since keys are generated at random, parties are unlikely to be
  given the same key by accident.
\item In $\G2$, we change the way sessions respond to challenge messages, by
  using the extractor to fake up answers to most challenges.  Since the
  extractor is good, the adversary is unlikely to notice.
\item In $\G3$, we abort the game if the adversary ever queries $H_K(\cdot)$
  on the Diffie-Hellman secret $r_S r_T P$ shared between two unexposed
  matching sessions.  We show that this is unlikely to happen if the
  Diffie-Hellman problem is hard.
\item In $\G4$, we abort the game if any unexposed session \emph{accepts} a
  response message which wasn't sent by a matching session.
\end{itemize}
Finally, we show that the adversary has no advantage in $\G4$.  The theorem
follows.

For ease of comprehension, we postpone the detailed proofs of some of the
steps until after we conclude the main proof.

Let $A$ be a given adversary which runs in time~$t$, creates at most~$q_S$
sessions, delivers at most~$q_M$ messages, and makes at most~$q_I$ queries to
its $H_I(\cdot, \cdot, \cdot, \cdot)$ oracle and at most~$q_K$ queries to its
$H_K(\cdot)$ oracle.  Let $\G0$ be the original SK-security game of
definition~\ref{def:sk}, played with adversary~$A$.

Game~$\G1$ is the same as game~$\G0$ except, if the initialization function
reports two parties as having the same public key (i.e., we have $X_i \ne
X_j$ where $0 \le i < j < n$), we stop the game immediately and without
crediting the adversary with a win.  This only happens when the corresponding
private keys are equal, i.e., $x_i = x_j$, and since the initialization
function chooses private keys uniformly at random, this happens with
probability at most $\binom{n}{2}/\#G$.  Since if this doesn't happen, the
game is identical to $\G0$, we can apply lemma~\ref{lem:shoup}, and see that
\begin{equation}
  \label{eq:sk-g0-g1}
  \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.  Note that the game now takes at most
$O(q_I)$ times longer to process each message delivered by the adversary.
This is where the $O(q_I q_M)$ term comes from in the theorem statement.

Game~$\G2$ is the same as game~$\G1$, except that we change the way that we
make parties respond to \cookie{challenge} messages $(\cookie{challenge}, R,
c)$.  Specifically, suppose that $S = (P_i, P_j, s)$ is a session.
\begin{itemize}
\item Suppose $T = (P_j, P_i, s)$ is the matching session of $S$.  The game
  proceeds as before if $(R, c) = (R_T, c_T)$ is the challenge issued by $T$.
\item Otherwise, we run the extractor $T_\Wident$ on the adversary's history
  so far of oracle queries $H_I(X_i, s, R, \cdot)$ to determine a pair $(r,
  Y)$.  If $r = \bot$ then we discard the message.  Otherwise, we add $R$ to
  the list~$C$, and return a fake response to the adversary by computing $K =
  H_K(r R_S)$ and handing the adversary $(\cookie{response}, R_S, E_K(Y))$.
\end{itemize}
The following lemma shows how this affects the adversary's probabilities of
winning.
\begin{lemma}
  \label{lem:sk-g1-g2}
  \begin{equation}
    \label{eq:sk-g1-g2}
    \diff{1}{2} \le \frac{q_M}{2^{\ell_I}}.
  \end{equation}
\end{lemma}

Let us say that a session $S = (P_i, P_j, s)$ is \emph{ripe} if
\begin{itemize}
\item there is a matching session $T = (P_j, P_i, s)$, and
\item $S$ is unexposed.
\end{itemize}
Suppose that $S$ is a ripe session, and that it has a matching session~$T$:
let $Z_S = Z_T = r_S r_T P$.

Game~$\G3$ is the same as $\G2$, except that the game is immediately aborted
if ever the adversary queries its random oracle $H_K(\cdot)$ at a value $Z_S$
for any ripe session~$S$.  The following lemma shows how this affects the
adversary's probabilities of winning.
\begin{lemma}
  \label{lem:sk-g2-g3}
  For some $t'$ within the bounds given in the theorem statement we have
  \begin{equation}
    \label{eq:sk-g2-g3}
    \diff{2}{3} \le q_S \InSec{mcdh}(G; t', q_K).
  \end{equation}
\end{lemma}

Game~$\G4$ is the same as $\G3$ except that the game is immediately aborted
if ever the adversary sends a response message to a ripe session~$S$ which
wasn't output by its matching session as a response to $S$'s challenge, with
the result that $S$ completes.

Let's make this more precise.  Let $U$ and $V$ be a pair of matching
sessions.  Let $C_U = (\cookie{challenge}, R_U, c_U$ be the challenge message
sent by $U$.  Let $M_T$ be the set of messages which $T$ has sent upon
delivery of $C_U$.  Then, in $\G4$, we abort the game if, for any pair $S$
and~$T$ of matching, unexposed sessions, $S$ has completed as a result of
being sent a message $\mu \notin M_T$.  We have the following lemma.
\begin{lemma}
  \label{lem:sk-g3-g4}
  For a $t'$ within the stated bounds, we have
  \begin{equation}
    \label{eq:sk-g3-g4}
    \diff{3}{4} \le q_S \bigl( \InSec{ind-cca}(\E; t', q_M, q_M) +
                         n \cdot \InSec{mcdh}(G; t', q_M + q_I) \bigr)
  \end{equation}
\end{lemma}

Finally, let us consider the state we're in with $\G4$.
\begin{itemize}
\item No ripe session completes except as a result the adversary faithfully
  delivering messages between it and its matching session.
\item The adversary never queries $Z_S$ for any ripe session~$S$.  If we set
  $K_S = (K_{S, 0}, K_{S, 1}) = H_K(Z_S)$, then $K_{S, 1}$ is the key output
  by $S$ when it completes.
\item If $S$ and $T$ are matching ripe sessions, then $K_S = K_T$, since $Z_S
  = r_S R_T = r_T R_S = Z_T$.
\item For any ripe session~$S$, $K_{S, 1}$ is uniformly distributed in
  $\Bin^\kappa$ and independent of the adversary's view.
\item If $S = (P_i, P_j, s)$ and $T = (P_j, P_i, s)$ are matching ripe
  sessions, then $Z_S$ depends only $r_S$ and $r_T$.  Hence, once $S$ and~$T$
  complete, and erase their states, $Z_S$ is independent of everything except
  the messages sent between the two sessions.  In particular, $Z_S$ is
  independent of the long-term secrets $x_i$ and~$x_j$, so if either player
  is later corrupted, the key $K_{S, 1}$ remains independent of the
  adversary's view.
\item Hence, the keys output by unexposed sessions are indistinguishable from
  freshly-generated random strings, and remain so indefinitely.
\end{itemize}
We conclude that, for any adversary $A$,
\begin{equation}
  \label{eq:sk-g4}
  \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
\begingroup \splitright=4em minus 4em
\begin{spliteqn}
  \Adv{sk}{\Wident^{G, \E}}(A) \le
     2 q_S \bigl(\InSec{ind-cca}(\E; t', q_M, q_M) + {} \\
     \InSec{mcdh}(G; t', q_K) +
     n \,\InSec{mcdh}(G; t', q_M + q_I) \bigr) + {}
     \frac{n (n - 1)}{\#G} +
     \frac{2 q_M}{2^{\ell_I}}.
\end{spliteqn} \endgroup
The theorem follows, since $A$ was chosen arbitrarily.


\begin{proof}[Proof of lemma~\ref{lem:sk-g1-g2}]
  The two games $\G1$ and~$\G2$ differ only in whether they accept or reject
  particular challenge messages $(\cookie{challenge}, R, c)$.

  We claim firstly that no message is \emph{accepted} by $\G2$ which would
  have been rejected by $\G1$.  To prove the claim, it is sufficient to note
  that the extractor's output, if not $\bot$, is always correct, and hence if
  $\G2$ accepts a message then $\G1$ would have done so too.

  Since $\G2$ also behaves identically when the adversary submits to~$S$ the
  challenge from the matching session~$T$, we have nothing to prove in this
  case.  Let $F$ be the event that the adversary submits a message
  $(\cookie{challenge}, R, c)$ to a session~$S$ which $S$ would have accepted
  in $\G1$ but would be rejected by the new rule in~$\G2$.  By
  lemma~\ref{lem:shoup} we have $\diff{1}{2} \le \Pr[F]$.  To prove the
  current lemma, therefore, we must show that $\Pr[F] \le q_M/2^{\ell_I}$.

  Rather than consider individual challenge messages, we consider
  \emph{classes} of messages.  We shall refer to a quadruple~$\Cid = (i, j,
  s, R)$ as a \emph{class-id}, and define some useful functions:
  \begin{itemize}
  \item the class's \emph{session} $\Csession(\Cid) = (P_i, P_j, s)$;
  \item the class's \emph{index} $\Cindex(\Cid)$ is $r \in I$ where $R = r
    P$, which is well-defined by lemma~\ref{lem:unique-dl};
  \item the class's \emph{query} $\Cquery(\Cid) = (X_j, s, R, x_i R)$;
  \item the class's \emph{hash} $\Chash(\Cid) = H_I(\Cquery(\Cid)) = H_I(X_j,
    s, R, x_i R)$;
  \item the class's \emph{check-value} $\Ccheck(\Cid) = \Chash(\Cid) \xor
    \Cindex(\Cid)$;
  \item the class's \emph{check-set} $\Ccheckset(\Cid)$ is the set of
    check-values $c$ such that a message $(\cookie{challenge}, R, c)$ was
    sent to session $S = (P_i, P_j, s)$; and
  \item the class's \emph{count} $\Ccount(\Cid) = |\Ccheckset(\Cid)|$.
  \end{itemize}

  Consider any class-id~$\Cid = (i, j, s, R)$.  A natural question which
  arises is: which participants have issued $\Cid$'s query, i.e., queried
  $H_I$ at $\Cquery(\Cid)$?

  We can characterise the $H_I(\cdot, \cdot, \cdot, \cdot)$ queries of a
  session $U = (P_{i'}, P_{j'}, s')$ as follows:
  \begin{itemize}
  \item computing the check-value for the challenge $R_U$ by querying
    $H_I(X_{i'}, s', R_U, r_U X_{j'})$, and
  \item checking an incoming challenge~$R'$ by querying $H_I(X_{j'}, s', R',
    x_{i'} R')$.
  \end{itemize}
  The class~$\Cid$'s query $\Cquery(\Cid)$ is $U$'s check-value query if
  \[ (j, i, s, R) = (i', j', s', R_U) \]
  i.e., $U$ is the matching session of $\Csession(\Cid)$, and moreover $R =
  R_U$ is the challenge value issued by $U$.  For any $c \in
  \Ccheckset(\Cid)$, if $c = \Ccheck(\Cid)$ then $(\cookie{challenge}, R, c)$
  is precisely the challenge message issued by~$U$ to $\Csession(\Cid)$; the
  rules for handling this message didn't change.  However, if $c \ne
  \Ccheck(\Cid)$ then the message would have been rejected in $\G1$, and we
  have already shown that $\G2$ continues to reject all messages rejected by
  $\G1$.

  Let us say that a class-id~$\Cid = (i, j, s, R)$ is \emph{bad} if
  \begin{enumerate}
  \item the value $R$ is not the challenge issued by $\Csession(\Cid)$'s
    matching session, and
  \item the adversary has not issued $\Cid$'s query $\Cquery(\Cid)$,
    \emph{but}
  \item $\Ccheck(\Cid) \in \Ccheckset(\Cid)$, so one of the check-values
    submitted to $S$ was actually correct.
  \end{enumerate}
  We claim that our extractor will work perfectly unless some class-id is
  bad.  Certainly, if $R$ was issued by the matching session, there is
  nothing to prove; if the adversary has issued the relevant query then the
  extractor will recover $\Cindex(\Cid)$ just fine; and if $\Ccheck(\Cid)
  \notin \Ccheckset(\Cid)$ then all messages in the class would have been
  rejected by $\G1$ anyway.

  Let $B(\Cid)$ be the event that the class~$\Cid$ is bad.  We claim that
  \[ \Pr[B(\Cid)] \le \frac{\Ccount(\Cid)}{2^{\ell_I}}. \]
  The present lemma follows, since
  \[ \diff{1}{2}
     \le \Pr[F]
     \le \sum_\Cid \Pr[B(\Cid)]
     \le \sum_\Cid \frac{\Ccount(\Cid)}{2^{\ell_I}}
     =   \frac{1}{2^{\ell_I}} \sum_\Cid \Ccount(\Cid)
     \le \frac{q_M}{2^{\ell_I}}
  \]
  as required.

  Now observe that, in $\G2$, sessions don't actually check incoming
  challenges in this way any more -- instead we run the extractor.  So, to
  prove the claim, we consider a class~$\Cid$ where properties~1 and~2 above
  hold.  The correct hash $\Chash(\Cid)$ is then independent of the rest of
  the game, so the probability that $\Ccheck(\Cid) \in \Ccheckset(\Cid)$ is
  precisely $\Ccount(\Cid)/2^{\ell_I}$ as required.

  This completes the proof the lemma.
\end{proof}

\begin{proof}[Proof of lemma~\ref{lem:sk-g2-g3}]
  Let $F$ be the event that the adversary makes a query $H_K(Z_S)$ for some
  ripe session~$S$.  Since $\G3$ proceeds exactly as $\G2$ did unless $F_2$
  occurs, we apply lemma~\ref{lem:shoup}, which tells us that $\diff{2}{3}
  \le \Pr[F_2]$.  We must therefore bound this probability.

  To do this, we consider a new game~$\G3'$, which is the same as $\G3$,
  except that, at the start of the game, we choose a random number $k \inr
  \Nupto{q_S}$.  For $0 \le i < q_S$, let $S_i$ be the $i$th session created
  by the adversary.  We define $F'$ to be the event that the adversary
  queries $H_K(Z_{S_k})$ when $S_k$ is ripe.

  The lemma now follows from these two claims.

  \begin{claim}
    $\Pr[F] \le q_S \Pr[F']$.
  \end{claim}
  To see this, for any session~$S$, let $F_S$ be the event that the adversary
  queries~$H_K(Z_S)$ when $S$ is ripe.  Then
  \[ \Pr[F] \le \sum_{0\le i<q_S} \Pr[F_{S_i}]. \]
  Hence,
  \[ \Pr[F'] = \Pr[F_{S_k}] = \sum_{0\le i<q_S} \Pr[F_{S_i}] \Pr[k = i]
             = \frac{1}{q_S} \sum_{0\le i<q_S} \Pr[F_{S_i}]
             \ge \frac{\Pr[F]}{q_S}
  \]
  proving the claim.

  \begin{claim}
    For some $t' = t + O(n) + O(q_S q_M) + O(q_I) + O(q_K)$, we have
    $\Pr[F'] \le \InSec{mcdh}(G; t', q_K).$
  \end{claim}
  To prove this claim, we construct an adversary~$B$ which solves the MCDH
  problem in~$G$.  The adversary works as follows.
  \begin{enumerate}
  \item It is given a pair $(R^*, S^*) = (r^* P, s^* P)$ of group elements;
    its objective is to make a verification-oracle query $V(Z^*)$ where $Z^*
    = r^* s^* P$.
  \item It sets up a simulation of the game~$\G3'$, by running the
    $\id{init}$ function, and simulating all of the parties.  In particular,
    it chooses a random~$k \in \Nupto{q_S}$.
  \item It sets up accurate simulations of the random oracles $H_K(\cdot)$
    and $H_I(\cdot, \cdot, \cdot, \cdot)$, which choose random outputs for
    new, fresh inputs.  However, whenever $A$ queries $H_K(\cdot)$ on a group
    element $Z$, $B$ also queries $V(Z)$.
  \item It runs $A$ in its simulated game.  It responds to all of $A$'s
    instructions faithfully, until the $k$th session-creation.
  \item When creating the $k$th session $S = S_k = (P_i, P_j, s)$, $B$ has
    party~$P_i$ choose $R^*$ as its challenge, rather than choosing $r_S$ and
    setting $R_S = r_S P$.  Because it simulates all the parties, $B$ can
    compute $Y_S = x_j R$, which is still correct.
  \item If $A$ requests the creation of a matching session $T = (P_j, P_i,
    s)$ then $B$ has party~$P_j$ choose $S^*$ as its challenge.  Again, $B$
    computes $Y_T = x_i S^*$.
  \item If $A$ ever corrupts the parties $P_i$ or $P_j$, or reveals the
    session state of $S$ or $T$ then $B$ stops the simulation abruptly and
    halts.
  \end{enumerate}
  Adversary $B$'s running time is within the bounds required of $t'$, and $B$
  makes at most $q_K$ queries to $V(\cdot)$; we therefore have
  \[ \Pr[F'] \le \Succ{mcdh}{G}(B) \le \InSec{mcdh}(G; t', q_K) \]
  as required.
\end{proof}

\begin{proof}[Proof of lemma~\ref{lem:sk-g3-g4}]
  Let $F_4$ be the event under which we abort the game~$\G4$.  Clearly, if
  $F$ doesn't occur, games $\G3$ and $\G4$ proceed identically, so we can
  apply lemma~\ref{lem:shoup} to see that $\diff{3}{4} \le \Pr[F_4]$.
  Bounding $\Pr[F_4]$, however, is somewhat complicated.  We use a further
  sequence of games.

  Firstly, let $\G5$ be like $\G4$ with the exception that we choose, at
  random, an integer~$k \inr \Nupto{q_S}$.  As we did in the proof for
  lemma~\ref{lem:sk-g3-g4}, let $S_i$ be the $i$th session created by the
  adversary.  For each session~$S_i$, let $T_i$ be its matching session, if
  there is one.  We define $F_5$ to be the event that
  \begin{itemize}
  \item $S_k$ completes immediately following delivery of a message $\mu
    \notin M_{T_k}$, and
  \item $S_k$ was ripe at this point.
  \end{itemize}
  For games~$\G{i}$, for $i > 5$, we define the event $F_i$ to be the event
  corresponding to $F_5$ in $\G{i}$.  Note that if $S_k$ \emph{is} sent a
  message in $M_{T_k}$ then $S_k$ immediately completes.

  \begin{claim}
    $\Pr[F_4] \le \Pr[F_5]/q_S$.
  \end{claim}
  This claim is proven exactly as we did for claim~1 of
  lemma~\ref{lem:sk-g2-g3}.

  Let~$\G6$ be the same as $\G5$ except that we change the encrypted
  responses of session~$S_k$ and its matching session~$T_k$.  Let $K^* =
  (K_0^*, K_1^*) = H_K(Z_S)$.  Then, rather than sending $(\cookie{response},
  R_S, E_{K_0^*}(Y_T))$, session~$S$ sends $(\cookie{response}, R_S,
  E_{K_0^*}(1^{\ell_G}))$.
  \begin{claim}
    $|\Pr[F_6] - \Pr[F_5]| \le \InSec{ind-cca}(\E; t', q_M, q_M).$
  \end{claim}
  To prove this claim, we construct an adversary~$B$ which attacks the
  IND-CCA security of our encryption scheme $\E$.  The adversary~$B$ works as
  follows.
  \begin{enumerate}
  \item It is given no input, but a pair of oracles $E(\cdot, \cdot)$ and
    $D(\cdot)$; the former encrypts either the left or right input, according
    to a hidden bit, and the latter decrypts ciphertexts other than those
    returned by $E(\cdot, \cdot)$.  Its goal is to guess the hidden bit.
  \item It sets up a simulation of the game~$\G5$, by running the $\id{init}$
    function, and simulating all of the parties.  In particular, it chooses a
    random $k \in \Nupto{q_S}$.
  \item It sets up accurate simulations of the random oracles $H_K(\cdot)$
    and $H_I(\cdot, \cdot, \cdot, \cdot)$.
  \item It runs $A$ in its simulated game.  It responds to all of $A$'s
    instructions faithfully, except for the matching sessions $S_k$ and
    $T_k$.  Let $S = S_k = (P_i, P_j, s)$, and $T = T_k = (P_j, P_i, s)$.
  \item Suppose $T$ is sent the message $C_S = (\cookie{challenge}, R_S,
    c_S)$.  Rather than computing $K^* = H_K(r_T R_S)$ and performing the
    encryption properly, $B$ queries its left-or-right encryption oracle
    $E(\cdot, \cdot)$ on $E(1^{\ell_G}, x_j R_S)$, and sends the resulting
    ciphertext~$\chi$ back to~$S$ as part of a message $(\cookie{response},
    R_T, \chi)$.  The set $M_T$ is precisely the set of messages constructed
    in this fashion.  (Recall that challenge messages other than $C_S$ aren't
    actually delivered to $T$, since we simulate the responses using the
    extractor, as of $\G2$.)
  \item Suppose $S$ is sent a message $M = (\cookie{response}, R_T, \chi) \in
    M_T$.  We immediately stop the simulation, and $B$ returns $0$.
  \item Suppose, instead, that $S$ is sent some message $M' =
    (\cookie{response}, R, \chi) \notin M_T$.  There are two cases to
    consider.  If $R = R_T$ then we must have $\chi$ distinct from the
    ciphertexts returned by the $E(\cdot, \cdot)$ oracle, so we can invoke
    the decryption oracle $D(\cdot)$ on $\chi$ to obtain a response $Y$.
    Alternatively, if $R \ne R_T$, we can compute the key $K = (K_0, K_1) =
    H_K(r_S R)$, and recover $Y = D_{K_0}(\chi)$.  In either case, if $Y =
    r_S X_j)$ then $S$ would complete at this point: $B$ stops the simulation
    and returns $1$.
  \item If $A$ exposes $S$ (by corrupting $P_i$ or~$P_j$, or revealing $S$ or
    $T$) then we stop the simulation and $B$ returns $0$.
  \item Finally, if the game stops, either because $A$ halts, or because of
    one of the special rules introduced in earlier games, $B$ returns $0$.
  \end{enumerate}
  It is clear that $B$'s oracle queries are acceptable, since $|x_j R_S| =
  \ell_G$ by definition, and $B$ never queries $D(\cdot)$ on a ciphertext
  returned by its encryption oracle.  By the rules of~$\G3$, we know that the
  game stops immediately if $A$ ever queries $Z_S$, so the key $K^*$ is
  independent of everything in $A$'s view except the ciphertexts $\chi$
  output by $S$ and $T$.  Therefore, if the hidden bit of the IND-CCA game is
  $1$, $B$ accurately simulates $\G5$, whereas if the bit is $0$ then $B$
  accurately simulates $\G6$.  We issue no more that $q_M$ encryption or
  decryption queries.  Finally, $B$'s running time is within the bounds
  allowed for $t'$.  Therefore,
  \[ \Adv{ind-cca}{\E}(B) = \Pr[F_5] - \Pr[F_6]
     \le \InSec{ind-cca}(\E; t', q_M, q_M). \]
  We construct the adversary~$\bar{B}$ which is the same as $B$ above, except
  that $\bar{B}$ returns $0$ whenever $B$ returns~$1$, and \emph{vice versa}.
  Clearly
  \[ \Adv{ind-cca}{\E}(\bar{B})
     = (1 - \Pr[F_5]) - (1 - \Pr[F_6])
     = \Pr[F_6] - \Pr[F_5]
     \le \InSec{ind-cca}(\E; t', q_M, q_M).
  \]
  This proves the claim.

  Let $\G7$ be the same as $\G6$, except that at the start of the game we
  choose a random $m \in \Nupto{n}$, and when the adversary creates the
  session $S = S_k = (P_i, P_j, s)$, we abort the game unless $j = m$.
  Clearly we have $\Pr[F_6] = n \Pr[F_7]$.

  Finally, we can explicitly bound $F_6$.  In $\G6$, the adversary's view is
  independent of the correct response $Y_S = r_S X_S = x_j R_S$ to $S$'s
  challenge.  Therefore, if $A$ manages to send any message $\mu \notin M_T$
  which causes $S$ to complete, then it has impersonated~$P_j$.
  \begin{claim}
    $\Pr[F_7] \le \InSec{mcdh}(G; t', q_M + q_I)$.
  \end{claim}
  The present lemma follows from this and the previous claims.

  To prove the claim formally, we construct an adversary~$B'$, which behaves
  as follows.
  \begin{enumerate}
  \item It is given as input a public key $X^*$ and a single challenge $(R^*,
    c^*)$, a random oracle $H^*_I(\cdot, \cdot)$, and an oracle $V(\cdot,
    \cdot)$, which verifies responses $(R, Y)$.  Its goal is to invoke
    $V(\cdot, \cdot)$ with a correct response to the challenge.
  \item It chooses a random $k \in \Nupto{q_S}$ and $m \in \Nupto{n}$. It
    sets up a simulation of the game~$\G7$, by running the $\id{init}$
    function, and simulating all of the parties, except that it gives party
    $P_m$ the public key $X^*$.  This makes no difference, since $P_m$
    doesn't actually need to give any `honest' responses because of the
    change we made in $\G6$.
  \item It sets up accurate simulations of the random oracles $H_K(\cdot)$
    and $H_I(\cdot, \cdot, \cdot, \cdot)$, with one exception -- see below.
  \item It runs $A$ in its simulated game.  It responds to all of $A$'s
    instructions faithfully, except for the session $S_k$.  Let $S = S_k =
    (P_i, P_j, s)$, and let $T = T_k = (P_j, P_i, s)$ be its matching
    session.
  \item When session~$S$ is created, $B'$ checks that $j = m$, and if not
    stops the simulation and halts.  Otherwise, $B'$ invokes its oracle~$C()$
    to obtain a pair $(R, c)$.  Session~$S$ sends $C_S = (\cookie{challenge},
    R, c)$ as its challenge to~$T$.
  \item When $A$ makes a query $H_I(X^*, s, R, Y)$, $B$ answers it by
    querying its \emph{own} random oracle $H^*_I(R, Y)$.
  \item When $S$ receives a message $(\cookie{response}, R, \chi)$, we
    compute $(K_0, K_1) = r_S R$, and $Y = D_{K_0}(\chi)$.  If $Y \ne \bot$
    then $B'$ calls $V(R, Y)$.
  \item If $A$ reveals $S$ or corrupts $P_i$ or $P_j$ then $B'$ stops the
    simulation immediately and halts.
  \end{enumerate}
  The running time of $B'$ is within the bounds required of $t'$; it makes at
  most $q_I$ random-oracle and at most $q_M$ verification queries.  Clearly
  $B'$ succeeds whenever $F_7$ occurs.  The claim follows from
  theorem~\ref{thm:wident-sound}.
\end{proof}


\subsection{Proof of theorem~\ref{thm:sk2}}
\label{sec:sk2-proof}

The proof is almost identical to the proof of theorem~\ref{thm:sk}, in
appendix~\ref{sec:sk-proof}.  Unfortunately a black-box reduction doesn't
seem possible.

We use the games and notation of section~\ref{sec:sk-proof}.

The change to the check-value calculation doesn't affect key-generation at
all, so the transition to $\G1$ goes through as before.

The transition from $\G1$ to $\G2$ -- answering challenges using the
extractor -- needs a little care.  Let $S = (P_i, P_j, s)$ be a session, and
consider an incoming message $(\cookie{challenge}, R, c)$.
\begin{itemize}
\item If $T = (P_j, P_i, s)$ is the matching session to $S$, and $R = R_T$ is
  the public challenge value of $T$, and $c = r_T \xor H_I(R_S, X_j, s, R_T,
  r_T X_i)$ is the check-value output by $T$ when it received
  $(\cookie{pre-challenge}, R_S)$ as input, then $S$ replies as it did in
  $\G1$.
\item If the challenge message is any other message, then we use the
  extractor.
\end{itemize}
As in lemma~\ref{lem:sk-g1-g2}, we examine which sessions could have queried
$H_I(R_S, X_j, s, R, x_i R)$, and for the same reasons conclude that only the
matching session would have done this, and only in response to the
pre-challenge $R_S$.  It follows that $\diff{1}{2} \le q_M/2^{\ell_I}$ as
before.

The remaining game steps go through unchanged.  In particular, we conclude
that a ripe session will only complete if the adversary has transmitted
messages from its matching session correctly, and the session key is
independent of the adversary's view.  The theorem follows.


\subsection{Sketch proof of single-key protocol for secure channels}
\label{sec:sc-proof}

We want to show that the Wrestlers Key-Exchange protocol, followed by use of
the encryption scheme $\E$, with the \emph{same} key $K = K_0$, still
provides secure channels.

\subsubsection{Secure channels definition}
We (very briefly!) recall the \cite{canetti-krawczyk-2001:secure-channels}
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:
%%% mode: latex
%%% TeX-master: t
%%% End: