From dff0fad2fb0c4edacbe668fdd72030e7e8ac5db7 Mon Sep 17 00:00:00 2001
From: Mark Wooding <mdw@distorted.org.uk>
Date: Thu, 2 Nov 2006 13:17:26 +0000
Subject: [PATCH] Add build system.  Write most of the introduction.

---
 .gitignore                     |  10 +
 .links                         |   1 +
 Makefile                       |  10 -
 Makefile.m4                    |  88 ++++++++
 configure.in                   |  30 +++
 background.tex => wr-backg.tex |   8 +-
 wrslide.tex => wr-main.tex     |  71 +++++--
 wrestlers.tex                  | 443 +++++++++++++++++++++++++++++++++--------
 wrshortsl.tex                  |   6 -
 wrslides.cls                   |  13 +-
 wrslides.tex                   |   7 +-
 11 files changed, 559 insertions(+), 128 deletions(-)
 create mode 100644 .links
 delete mode 100644 Makefile
 create mode 100644 Makefile.m4
 create mode 100644 configure.in
 rename background.tex => wr-backg.tex (99%)
 rename wrslide.tex => wr-main.tex (80%)
 delete mode 100644 wrshortsl.tex

diff --git a/.gitignore b/.gitignore
index 79b2cef..87b6f92 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,3 +11,13 @@
 *.blg
 *.tmp
 *.toc
+Makefile
+Makefile.in
+aclocal.m4
+autom4te.cache
+build
+configure
+install-sh
+missing
+COPYING
+Makefile.am
diff --git a/.links b/.links
new file mode 100644
index 0000000..5ecd9c6
--- /dev/null
+++ b/.links
@@ -0,0 +1 @@
+COPYING
diff --git a/Makefile b/Makefile
deleted file mode 100644
index 2c5c168..0000000
--- a/Makefile
+++ /dev/null
@@ -1,10 +0,0 @@
-all: \
-	wrestlers.ps wrestlers.pdf \
-	wrslides.pdf \
-	wrslides-full.pdf
-
-%.ps: %.dvi
-	dvips -o $@ $+
-
-%.dvi: %.tex
-	latex 
\ No newline at end of file
diff --git a/Makefile.m4 b/Makefile.m4
new file mode 100644
index 0000000..4570914
--- /dev/null
+++ b/Makefile.m4
@@ -0,0 +1,88 @@
+## -*-fundamental-*-
+##
+## $Id: Makefile.m4,v 1.1 2002/02/24 15:43:20 mdw Exp $
+##
+## Makefile for IPS
+##
+## (c) 2002 Mark Wooding
+##
+
+##----- Licensing notice ----------------------------------------------------
+##
+## This program is free software; you can redistribute it and/or modify
+## it under the terms of the GNU General Public License as published by
+## the Free Software Foundation; either version 2 of the License, or
+## (at your option) any later version.
+##
+## This program is distributed in the hope that it will be useful,
+## but WITHOUT ANY WARRANTY; without even the implied warranty of
+## MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+## GNU General Public License for more details.
+##
+## You should have received a copy of the GNU General Public License
+## along with this program; if not, write to the Free Software Foundation,
+## Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+
+AUTOMAKE_OPTIONS = foreign
+
+SRC = \
+        wrslides.tex wrslides.cls \
+	wr-backg.tex wr-main.tex ecc.mp \
+	wrestlers.tex
+
+changequote([[, ]])
+
+define([[DOECC]], [[mpost ecc.mp && mptopdf ecc.0 &&]])
+define([[L1]], [[latex $1]])
+define([[LFULL]],
+       [[latex $1 && bibtex $1 && latex $1 && latex $1 && latex $1]])
+define([[OUTPUTS]], [[dnl
+_([[notes]], [[L1]], [[wrslides]],
+  [[\wrslidesfalse]], [[DOECC]])dnl
+_([[slides]], [[L1]], [[wrslides]],
+  [[\wrslidestrue\includeonly{wr-main}]], [[DOECC]])dnl
+_([[longslides]], [[L1]], [[wrslides]],
+  [[\wrslidestrue]], [[DOECC]])dnl
+_([[paper]], [[LFULL]], [[wrestlers]], [[]])dnl
+_([[llncs]], [[LFULL]], [[wrestlers]], [[\fancystylefalse\shorttrue]])dnl
+]])
+define([[adorn]], [[define([[_]], [[$2$]][[1$3 ]])$1]])
+define([[tags]], [[adorn([[$1]])]])
+define([[addsuffix]], [[adorn([[$1]], [[wr-]], [[$2]])]])
+
+DVI = addsuffix([[OUTPUTS]], [[.dvi]])
+DVIGZ = addsuffix([[OUTPUTS]], [[.dvi.gz]])
+PS = addsuffix([[OUTPUTS]], [[.ps]])
+PSGZ = addsuffix([[OUTPUTS]], [[.ps.gz]])
+PDF = addsuffix([[OUTPUTS]], [[.pdf]])
+
+noinst_DATA = $(DVI) $(DVIGZ) $(PS) $(PSGZ) $(PDF)
+
+define([[_]], [[dnl
+wr-$1.dvi: $(SRC)
+	@if [ ! -d $1 ]; then \
+	  mkdir $1; \
+	  for i in $(SRC); do ln -s ../$(srcdir)/$$i $1; done; \
+	  echo '$4' >$1/wr.cfg; \
+	fi
+	cd $1 && $5 $2($3) && cp $3.dvi ../wr-$1.dvi
+wr-$1.pdf: wr-$1.dvi
+	cd $1 && pdflatex $3 && cp $3.pdf ../wr-$1.pdf
+]])
+OUTPUTS
+
+%.gz: %; gzip -9cv $^ >$@.new && mv $@.new $@
+%.ps: %.dvi; dvips -o $@ $^
+
+CLEANFILES = *.dvi *.ps $(DVIGZ) $(PSGZ) $(PDF) *.[0-9] *-[0-9].pdf
+
+Makefile.am: Makefile.m4
+	cd $(srcdir) && m4 Makefile.m4 >Makefile.am
+
+EXTRA_DIST = $(SRC) Makefile.m4
+
+clean:; rm -rf tags([[OUTPUTS]]) && rm -f $(CLEANFILES)
+
+.PHONY: dvi
+
+##----- That's all, folks ---------------------------------------------------
diff --git a/configure.in b/configure.in
new file mode 100644
index 0000000..35b95e9
--- /dev/null
+++ b/configure.in
@@ -0,0 +1,30 @@
+dnl -*-fundamental-*-
+dnl
+dnl $Id: configure.in,v 1.2 2002/07/17 08:52:06 mdw Exp $
+dnl
+dnl Dummy configuration script for Wrestlers Protocol paper
+dnl
+dnl (c) 2002 Mark Wooding
+dnl
+
+dnl ----- Licensing notice --------------------------------------------------
+dnl
+dnl This program is free software; you can redistribute it and/or modify
+dnl it under the terms of the GNU General Public License as published by
+dnl the Free Software Foundation; either version 2 of the License, or
+dnl (at your option) any later version.
+dnl
+dnl This program is distributed in the hope that it will be useful,
+dnl but WITHOUT ANY WARRANTY; without even the implied warranty of
+dnl MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+dnl GNU General Public License for more details.
+dnl
+dnl You should have received a copy of the GNU General Public License
+dnl along with this program; if not, write to the Free Software Foundation,
+dnl Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
+
+AC_INIT(wrestlers.tex)
+AM_INIT_AUTOMAKE(wrestlers, 1.0.0)
+AC_OUTPUT(Makefile)
+
+dnl ----- That's all, folks -------------------------------------------------
diff --git a/background.tex b/wr-backg.tex
similarity index 99%
rename from background.tex
rename to wr-backg.tex
index f2a6554..d08fe6d 100644
--- a/background.tex
+++ b/wr-backg.tex
@@ -321,8 +321,8 @@
   \item Soundness: if $P^*$ convinces $V$ with probability $p > \frac{1}{2}$
     then we can, in theory, run $P^*$ with (say) $c = 0$ and get $\gamma$.
     We then \emph{rewind} $P^*$, give it $c = 1$, and get $\gamma \beta$,
-    from which we compute $\beta$.  This works with probability at least $p -
-    \frac{1}{2}$.
+    from which we compute $\beta$.  This works with probability at least $2
+    (p - \frac{1}{2})$.
   \end{itemize}
 \end{slide}
 
@@ -339,7 +339,7 @@ guaranteed to lose.
 
 On the other hand, if $n > r$, there must be a winning row, because there are
 too many ones to fit otherwise.  In fact, there must be at least $n - r$
-winning rows.  So our probability of winning must be at least $(n - r)/2r$.
+winning rows.  So our probability of winning must be at least $(n - r)/r$.
 
 Apply this to the problem of our dishonest prover.  The `table''s rows are
 indexed by all the possible inputs to the prover -- the value $\alpha$ and
@@ -347,7 +347,7 @@ its own internal coin tosses.  (We only consider provers running in bounded
 time, so these are finite.)  The columns are indexed by our coin $c$.  We
 know that $2 r p$ of the entries contain $1$.  Hence, the probability that we
 win is at least
-\[ \frac{2 r p - r}{2 r} = p - \frac{1}{2}. \]
+\[ \frac{2 r p - r}{r} = 2 \biggl( p - \frac{1}{2} \biggr). \]
 
 \begin{slide}
   \head{Zero-knowledge \seq: an example (cont.)}
diff --git a/wrslide.tex b/wr-main.tex
similarity index 80%
rename from wrslide.tex
rename to wr-main.tex
index 96bbe36..185bc37 100644
--- a/wrslide.tex
+++ b/wr-main.tex
@@ -4,7 +4,7 @@
 
 \begin{slide}
   \resetseq
-  \head{Identification using Diffie-Hellman \seq: Properties}
+  \head{Identification using Diffie-Hellman \seq: properties}
   \topic{properties}
 
   \begin{itemize}
@@ -17,7 +17,7 @@
 \end{slide}
 
 \begin{slide}
-  \head{Identification using Diffie-Hellman \seq: Basic setting}
+  \head{Identification using Diffie-Hellman \seq: basic setting}
   \topic{setting}
 
   \begin{itemize}
@@ -31,7 +31,7 @@
 \end{slide}
 
 \begin{slide}
-  \head{Identification using Diffie-Hellman \seq: Na\"\i ve attempt}
+  \head{Identification using Diffie-Hellman \seq: na\"\i ve attempt}
   \topic{protocol design}
 
   \begin{protocol}
@@ -54,7 +54,7 @@
 \end{slide}
 
 \begin{slide}
-  \head{Identification using Diffie-Hellman \seq: Fix it with a hash}
+  \head{Identification using Diffie-Hellman \seq: fix it with a hash}
   \protocolskip0pt
 
   \begin{protocol}
@@ -102,7 +102,7 @@
 \end{slide}
 
 \begin{slide}
-  \head{Identification using Diffie-Hellman \seq: The Wrestlers Protocol
+  \head{Identification using Diffie-Hellman \seq: the Wrestlers Protocol
   $\Wident$}
 
   \begin{protocol}
@@ -125,7 +125,7 @@
 \end{slide}
 
 \begin{slide}
-  \head{Identification using Diffie-Hellman \seq: Identification-based
+  \head{Identification using Diffie-Hellman \seq: identification-based
   $\Wident$}
 
   \begin{protocol}
@@ -190,7 +190,7 @@
 \end{slide}
     
 \begin{slide}
-  \head{Mutual identification \seq: Key exchange?}
+  \head{Mutual identification \seq: key exchange?}
 
   \begin{protocol}
     Alice & Bob \\
@@ -213,7 +213,7 @@
 
 \begin{slide}
   \resetseq
-  \head{Key exchange \seq: Properties}
+  \head{Key exchange \seq: properties}
   \topic{properties}
 
   \begin{itemize}
@@ -227,7 +227,7 @@
 \end{slide}
 
 \begin{slide}
-  \head{Key exchange \seq: Setting}
+  \head{Key exchange \seq: setting}
   \topic{setting}
 
   \begin{itemize}
@@ -244,7 +244,7 @@
 \end{slide}
 
 \begin{slide}
-  \head{Key exchange \seq: Broken first attempt}
+  \head{Key exchange \seq: broken first attempt}
   \topic{protocol design}
 
   \begin{protocol}
@@ -267,7 +267,7 @@
 \end{slide}
 
 \begin{slide}
-  \head{Key exchange \seq: Solution -- encrypt responses}
+  \head{Key exchange \seq: solution -- encrypt responses}
 
   \begin{protocol}
     Alice & Bob \\
@@ -290,7 +290,7 @@
 \end{slide}
 
 \begin{slide}
-  \head{Key exchange \seq: Multiple sessions}
+  \head{Key exchange \seq: multiple sessions}
 
   \begin{protocol}
     Alice & Bob \\
@@ -316,7 +316,52 @@
 \end{slide}
 
 \begin{slide}
-  \head{Key exchange \seq: Fully deniable variant}
+  \head{Key exchange \seq: proof sketch}
+
+  \begin{itemize}
+  \item $\G0$ is SK-security game.
+  \item In $\G1$, stop game unless all parties have distinct public keys
+    (collision bound).
+  \item In $\G2$, use extractor to answer challenges other than from matching
+    session.
+  \item In $\G3$, stop game if adversary queries $H(\cookie{key}, r_A r_b P)$
+    (CDH in $G$).
+  \item In $\G4$, stop game if session accepts response except from matching
+    session.
+    \begin{itemize}
+    \item In $\G5$, focus on a single session (factor of $q_S$).
+    \item In $\G6$, encrypt $1^{|Y|}$ instead of $Y = x R$ (IND-CCA of $\E$).
+    \item In $\G7$, focus on a single party (factor of $n$).
+    \item Now if party accepts, reduce from impersonating in $\Wident$.
+    \end{itemize}
+  \end{itemize}
+\end{slide}
+
+\begin{slide}
+  \head{Key exchange \seq: security result}
+  \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)}{|G|} +
+      \frac{2 q_M}{2^{\ell_I}}.
+  \end{spliteqn*}
+  \begin{multicols}{2}
+    \begin{itemize}
+    \item $t$ is running time of adversary
+    \item $n$ is number of parties
+    \item $q_S$ is number of new sessions
+    \item $q_M$ is number of messages sent
+    \item $q_I$ is number of $H(\cookie{check}, \cdot)$ queries
+    \item $q_K$ is number of $H(\cookie{key}, \cdot)$ queries
+    \item $t' = t + O(q_S) + O(q_M q_I) + O(q_K)$
+    \end{itemize}
+  \end{multicols}
+\end{slide}
+
+\begin{slide}
+  \head{Key exchange \seq: fully deniable variant}
 
   \begin{protocol}
     Alice & Bob \\
diff --git a/wrestlers.tex b/wrestlers.tex
index 633a93d..24f1876 100644
--- a/wrestlers.tex
+++ b/wrestlers.tex
@@ -6,7 +6,9 @@
 %%%
 
 \newif\iffancystyle\fancystylefalse
+\newif\ifshort\shortfalse
 \fancystyletrue
+\InputIfFileExists{wr.cfg}\relax\relax
 \errorcontextlines=\maxdimen
 \showboxdepth=\maxdimen
 \showboxbreadth=\maxdimen
@@ -135,6 +137,8 @@
 \let\Ccheckset=V
 \let\Ccount=\nu
 
+\def\HG#1{\mathbf{H}_{#1}}
+
 \begin{document}
 
 %%%--------------------------------------------------------------------------
@@ -170,50 +174,31 @@
 
 \section{Introduction}
 
-%% Blah...
-%% Very brief discussion of key-exchange
-%% models of secure key exchange
-%% mutter about protocol actually being implemented
-
-
 
-In this paper, we concern ourselves mainly with \emph{authenticated key
-  exchange}.  That is, we present a system whereby two parties, say Alice and
-Bob, can communicate over an insecure channel, and end up knowing a shared
-random key unknown to anyone else.  \fixme{write the rest of this}
+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; we discuss their
+protocol in section~\ref{sec:stinson-ident}.
 
-\subsection{Asymptotic and concrete security results}
-
-Most security definitions for identification (particularly zero-knowledge)
-and key-exchange in the literature are \emph{asymptotic}.  That is, they
-consider a family of related protocols, indexed by a \emph{security
-parameter}~$k$; they that any \emph{polynomially-bounded} adversary has only
-\emph{negligible} advantage.  A polynomially-bounded adversary is one whose
-running time is a bounded by some polynomial~$t(k)$.  The security definition
-requires that, for any such polynomially-bounded adversary, and any
-polynomial $p(k)$, there is a bound~$n$ such that the adversary's advantage
-is less than $p(k)$ for all choices of $k > n$.
-
-Such asymptotic notions are theoretically interesting, and have obvious
-connections to complexity theory.  Unfortunately, such an asymptotic result
-tells us nothing at all about the security of a particular instance of a
-protocol, or what parameter sizes one needs to choose for a given level of
-security against a particular kind of adversary.  Koblitz and Menezes
-\cite{Koblitz:2006:ALP} (among other useful observations) give examples of
-protocols, proven to meet asymptotic notions of security, whose security
-proofs guarantee nothing at all for the kinds of parameters typically used in
-practice.
+Identification protocols are typically less useful than they sound.  As Shoup
+\cite{Shoup:1999:OFM} points out, it provides a `secure ping', by which Bob
+can know that Alice is `there', but provides no guarantee that any other
+communication was sent to or reached her.  However, there are situations
+where this an authentic channel between two entities -- e.g., a device and a
+smartcard -- where a simple identification protocol can still be useful.
 
-Since, above all, we're interested in analysing a practical and implemented
-protocol, we follow here the `practice-oriented provable security' approach
-largely inspired by Bellare and Rogaway, and exemplified by
-\cite{Bellare:1994:SCB, Bellare:1995:XMN, Bellare:1995:OAE, Bellare:1996:ESD,
-  Bellare:1996:KHF, Bellare:2000:CST}; see also \cite{Bellare:1999:POP}.
-Rather than attempting to say, formally, whether or not a protocol is
-`secure', we associate with each protocol an `insecurity function' which
-gives an upper bound on the advantage of any adversary attacking the protocol
-within given resource bounds.
+An authenticated key-exchange protocol lets Alice and Bob agree on a shared
+secret, known to them alone, even if there is an enemy who can read and
+intercept all of their messages, and substitute messages of her own.  Once
+they have agreed on their shared secret, of course, they can use standard
+symmetric cryptography techniques to ensure the privacy and authenticity of
+their messages.
 
 
 \subsection{Desirable properties of our protocols}
@@ -228,7 +213,18 @@ Our identification protocol has a number of desirable properties.
   intractability of the computational Diffie-Hellman problem.
 \end{itemize}
 
-Our key-exchange protocol also has a number of desirable properties.
+Our key-exchange protocol also has a number of desirable
+properties.\footnote{%
+  We don't claim resistance to `key-compromise impersonation' (KCI) attacks.
+  To perform a KCI attack, an adversary learns a party's -- say Alice's --
+  secret and somehow uses this to impersonate Bob to Alice.  Our model
+  doesn't consider this to be a legitimate attack.  The purpose of a
+  key-exchange protocol is to provide a shared secret for some other,
+  high-level protocol between the participants.  If one of the parties is
+  already corrupted -- i.e., the adversary could be impersonating her -- then
+  it is impossible for us to make any meaningful security statement about the
+  high-level protocol anyway, so it seems unreasonable to expect the
+  key-exchange protocol to cope.}
 \begin{itemize}
 \item It is fairly \emph{simple} to understand and implement, though there
   are a few subtleties.  In particular, it is \emph{symmetrical}.  We have
@@ -249,18 +245,124 @@ Our key-exchange protocol also has a number of desirable properties.
   a given protocol execution.
 \end{itemize}
 
+\subsection{Asymptotic and concrete security results}
 
-\subsection{Formal models for key-exchange}
+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:2006:ALP} (among other useful observations) give examples of
+protocols, proven to meet asymptotic notions of security, whose security
+proofs guarantee nothing at all for the kinds of parameters typically used in
+practice.
+
+Since, above all, we're interested in analysing a practical and implemented
+protocol, we follow here the `practice-oriented provable security' approach
+largely inspired by Bellare and Rogaway, and exemplified by
+\cite{Bellare:1994:SCB,Bellare:1995:XMN,Bellare:1995:OAE,Bellare:1996:ESD,%
+Bellare:1996:KHF,Bellare:2000:CST}; see also \cite{Bellare:1999:POP}.
+Rather than attempting to say, formally, whether or not a protocol is
+`secure', we associate with each protocol an `insecurity function' which
+gives an upper bound on the advantage of any adversary attacking the protocol
+within given resource bounds.
 
-Many proposed key-exchange protocols have turned out to have subtle security
-flaws.  Burrows, Abadi and Needham \cite{Burrows:1989:LA} presented a formal
-logic for the analysis of authentication and key-exchange protocols.  Formal
-models for analysing the \emph{computational} security of key-exchange
-protocols began with Bellare and Rogaway \cite{Bellare:1994:EAK}, extended in
-\cite{Bellare:1995:PSS, Blake-Wilson:1997:KAP, Blake-Wilson:1998:EAA,
-  Bellare:1998:MAD}.
 
+\subsection{Formal models for key-exchange}
 
+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:LA}.
+Their approach requires a `formalising' step, in which one expresses in the
+logic the contents of the message flows, and the \emph{beliefs} of the
+participants.
+
+Bellare and Rogaway \cite{Bellare:1994:EAK} describe a model for studying the
+computational security of authentication and key-exchange protocols in a
+concurrent setting, i.e., where multiple parties are running several
+instances of a protocol simultaneously.  They define a notion of security in
+this setting, and show that several simple protocols achieve this notion.
+Their original paper dealt with pairs of parties using symmetric
+cryptography; they extended their definitions in \cite{Bellare:1995:PSS} to
+study three-party protocols involving a trusted key-distribution centre.
+
+Blake-Wilson, Johnson and Menezes \cite{Blake-Wilson:1997:KAP} applied the
+model of \cite{Bellare:1994:EAK} to key-exchange protocols using asymmetric
+cryptography, and Blake-Wilson and Menezes \cite{Blake-Wilson:1998:EAA}
+applied it to protocols based on the Diffie-Hellman protocol.
+
+The security notion of \cite{Bellare:1994:EAK} is based on a \emph{game}, in
+which an adversary nominates a \emph{challenge session}, and is given either
+the key agreed by the participants of the challenge session, or a random
+value independently sampled from an appropriate distribution.  The
+adversary's advantage -- and hence the insecurity of the protocol -- is
+measured by its success probability in guessing whether the value it was
+given is really the challenge key.  This challenge-session notion was also
+used by the subsequent papers described above.
+
+Bellare, Canetti and Krawczyk \cite{Bellare:1998:MAD} described a pair of
+models which they called the \textsc{am} (for `authenticated links model')
+and \textsc{um} (`unauthenticated links model').  They propose a modular
+approach to the design of key-exchange protocols, whereby one first designs a
+protocol and proves its security in the \textsc{am}, and then applies a
+authenticating `compiler' to the protocol which they prove yields a protocol
+secure in the realistic \textsc{um}.  Their security notion is new.  They
+define an `ideal model', in which an adversary is limited to assigning
+sessions fresh, random and unknown keys, or matching up one session with
+another, so that both have the same key.  They define a protocol to be secure
+if, for any adversary~$A$ in the \textsc{am} or \textsc{um}, there is an
+ideal adversary~$I$, such that the outputs of $A$ and $I$ are computationally
+indistinguishable.
+
+In \cite{Shoup:1999:OFM}, Shoup presents a new model for key-exchange, also
+based on the idea of simulation.  He analyses the previous models,
+particularly \cite{Bellare:1994:EAK} and \cite{Bellare:1998:MAD}, and
+highlights some of their inadequacies.
+
+Canetti and Krawczyk \cite{Canetti:2001:AKE} describe a new notion of
+security in the basic model of \cite{Bellare:1998:MAD}, based on the
+challenge-session notion of \cite{Bellare:1994:EAK}.  The security notion,
+called `SK-security', seems weaker in various ways than those of earlier
+works such as \cite{Bellare:1994:EAK} or \cite{Shoup:1999:OFM}.  However, the
+authors show that their notion suffices for constructing `secure channel'
+protocols, which they also define.
+
+In \cite{Canetti:2001:UCP}, Canetti describes the `universal composition'
+framework.  Here, security notions are simulation-based: one defines security
+notions by presenting an `ideal functionality'.  A protocol securely
+implements a particular functionality if, for any adversary interacting with
+parties who use the protocol, there is an adversary which interacts with
+parties using the ideal functionality such that no `environment' can
+distinguish the two.  The environment is allowed to interact freely with the
+adversary throughout, differentiating this approach from that of
+\cite{Bellare:1998:MAD} and \cite{Shoup:1999:OFM}, 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.
+
+Canetti and Krawczyk \cite{Canetti:2002:UCN} show that the SK-security notion
+of \cite{Canetti:2001:AKE} is \emph{equivalent} to a `relaxed' notion of
+key-exchange security in the UC framework, and suffices for the construction
+of UC secure channels.
+
+The result of \cite{Canetti:2002:UCN} gives us confidence that SK-security is
+the `right' notion of security for key-exchange protocols.  Accordingly,
+SK-security is the standard against which we analyse our key-exchange
+protocol.
 
 
 \subsection{Outline of the paper}
@@ -276,7 +378,7 @@ The remaining sections of this paper are as follows.
   protocol, and proves its security and deniability.  It also describes some
   minor modifications which bring practical benefits without damaging
   security. 
-\item Finally, section \ref{sec:...} presents our conclusions.
+\item Finally, section \ref{sec:conc} presents our conclusions.
 \end{itemize}
 
 %%%--------------------------------------------------------------------------
@@ -569,7 +671,7 @@ However, we can (loosely) relate the difficulty of MCDH to the difficulty of
 CDH.
 \begin{proposition}[Comparison of MCDH and CDH security]
   For any cyclic group $(G, +)$,
-  \[ \InSec{mcdh}(G; t, q_V) \le q_V\cdot\InSec{cdh}(G; t + O(q_V)). \]
+  \[ \InSec{mcdh}(G; t, q_V) \le q_V\,\InSec{cdh}(G; t + O(q_V)). \]
 \end{proposition}
 \begin{proof}
   Let $A$ be an adversary attacking the multiple-guess computational
@@ -716,12 +818,13 @@ left-or-right indistinguishability of ciphertexts under chosen-ciphertext
 attack.
 \begin{definition}
   [Indistinguishability under chosen-ciphertext attack (IND-CCA)]
+  \label{def:ind-cca}
   Let $\E = (\kappa, E, D)$ be a symmetric encryption scheme, and $A$ be an
   adversary.  Let $\id{lr}_b(x_0, x_1) = x_b$ for $b \in \{0, 1\}$.  Let
   \[ P_b =
-    \Pr[K \getsr \Bin^\kappa;
-    b \gets A^{E_K(\id{lr}_b(\cdot, \cdot)), D_K(\cdot)}() :
-    b = 1]
+     \Pr[K \getsr \Bin^\kappa;
+         b \gets A^{E_K(\id{lr}_b(\cdot, \cdot)), D_K(\cdot)}() :
+	 b = 1]
   \]
   An adversary is \emph{valid} if
   \begin{itemize}
@@ -1505,7 +1608,7 @@ theorem.
 \end{figure}
 
 We now return to proving that our extractor exists and functions as claimed.
-The following two trivial lemmas will be useful, both now and later.
+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
@@ -1627,8 +1730,8 @@ respectively.  We say that a mapping $\hat{e}\colon G \times G' \to G_T$ is a
 properties.
 \begin{description}
 \item[Bilinearity] For all $R \in G$ and $S', T' \in G'$, we have $\hat{e}(R,
-  S' + T') = \hat{e}(R, S') \hat{e}(R, T')$; and for all $R, S \in G$ and $T'
-  \in G'$ we have $\hat{e}(R + S, T') = \hat{e}(R, T') \hat{e}(S, T')$.
+  S' + T') = \hat{e}(R, S')\,\hat{e}(R, T')$; and for all $R, S \in G$ and $T'
+  \in G'$ we have $\hat{e}(R + S, T') = \hat{e}(R, T')\,\hat{e}(S, T')$.
 \item[Non-degeneracy] $\hat{e}(P, P') \ne 1$.
 \end{description}
 For practical use, we also want $\hat{e}(\cdot, \cdot)$ to be efficient to
@@ -1912,7 +2015,7 @@ version we present here.
 \label{sec:um}
 
 Our model is very similar to that of Canetti and Krawczyk
-\cite{Canetti:2002:???}, though we have modified it in two ways.
+\cite{Canetti:2001:AKE}, though we have modified it in two ways.
 \begin{enumerate}
 \item We allow all the participants (including the adversary) in the protocol
   access to the various random oracles required to implement it.
@@ -2218,11 +2321,11 @@ about its security.  The proof is given in appendix~\ref{sec:sk-proof}.
   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)}{|G|} +
-      \frac{2 q_M}{2^{\ell_I}} + {}\\
-      2 q_S \bigl( \InSec{mcdh}(G; t', q_K) +
-                   n \cdot \InSec{mcdh}(G; t', q_M + q_I) +
-                   \InSec{ind-cca}(\E; t', q_M, q_M) \bigr)
+      \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}
@@ -2683,11 +2786,11 @@ are tricks one can play involving subversion of DNS servers, but this is also
 nontrivial.)  However, injecting packets with bogus source addresses is very
 easy.
 
-Layering the protocol over TCP \cite{RFC793} ameliorates this problem because
+Layering the protocol over TCP \cite{RFC0793} ameliorates this problem because
 an adversary needs to guess or eavesdrop in order to obtain the correct
 sequence numbers for a spoofed packet; but the Wrestlers protocol is
 sufficiently simple that we'd like to be able to run it over UDP
-\cite{RFC768}, for which spoofing is trivial.
+\cite{RFC0768}, for which spoofing is trivial.
 
 Therefore, it's possible for anyone on the 'net to send Alice a spurious
 challenge message $(R, c)$.  She will then compute $Y = a R$, recover $r' = c
@@ -2713,8 +2816,6 @@ just as efficiently.  The new adversary attaches fake $R'$ values to
 challenges output by other parties, and strips them off on delivery,
 discarding messages with incorrect $R'$ values.
 
-There's another denial-of-service attack against the Wrestlers protocol.  
-
 \subsubsection{Key confirmation}
 Consider an application which uses the Wrestlers protocol to re-exchange keys
 periodically.  The application can be willing to \emph{receive} incoming
@@ -2729,19 +2830,103 @@ While key confirmation is unnecessary for \emph{security}, it has
 \emph{practical} value, since it solves the above problem.  If the
 application sends a \cookie{switch} message when it `completes', it can
 signal its partner that it is indeed ready to accept messages under the new
-key.  The \cookie{switch} message can be as simple as $(\cookie{switch},
-E_{K_0}(\cookie{switch}))$.
+key.  Our implementation sends $(\cookie{switch-rq}, E_{K_0}(H_S(0, R, R')))$
+as its switch message; the exact contents aren't important.  Our
+retransmission policy (below) makes use of an additional message
+\cookie{switch-ok}, which can be defined similarly.
+
+It's not hard to show that this doesn't adversely affect the security of the
+protocol, since the encrypted message is computed only from public values.
+In the security proof, we modify the generation of \cookie{response}
+messages, so that the plaintexts are a constant string rather than the true
+responses, guaranteeing that the messages give no information about the
+actual response.  To show this is unlikely to matter, we present an adversary
+attacking the encryption scheme by encrypting either genuine responses or
+fake constant strings.  Since the adversary can't distinguish which is being
+encrypted (by the definition of IND-CCA security,
+definition~\ref{def:ind-cca}), the change goes unnoticed.  In order to allow
+incorporate our switch messages, we need only modify this adversary, to
+implement the modified protocol.  This is certainly possible, since the
+messages contain (hashes of) public values.  We omit the details.
+
+\subsubsection{Optimization and piggybacking}
+We can optimize the number of messages sent by combining them.  Here's one
+possible collection of combined messages:
+\begin{description}
+\item [\cookie{pre-challenge}] $R$
+\item [\cookie{challenge}] $R'$, $R$, $c = H_I(R', X, s, R, c) \xor r$
+\item [\cookie{response}] $R'$, $R$, $c$, $E_{K_0}(x R')$
+\item [\cookie{switch}] $R'$, $E_{K_0}(x R', H_S(0, R, R'))$
+\item [\cookie{switch-ok}] $R'$, $E_{K_0}(H_S(1, R, R'))$
+\end{description}
+The combination is safe:
+\begin{itemize}
+\item the \cookie{switch} and \cookie{switch-ok} messages are safe by the
+  argument above; and
+\item the other recombinations can be performed and undone in a `black box'
+  way, by an appropriately defined SK-security adversary.
+\end{itemize}
 
 \subsubsection{Unreliable transports}
-The Internet UDP \cite{RFC768} is a simple, unreliable protocol for
+The Internet UDP \cite{RFC0768} is a simple, unreliable protocol for
 transmitting datagrams.  However, it's very efficient, and rather attractive
 as a transport for datagram-based applications such as virtual private
-networks (VPNs).
-
+networks (VPNs).  Since UDP is a best-effort rather than a reliable
+transport, it can occasionally drop packets.  Therefore it is necessary for a
+UDP application to be able to retransmit messages which appear to have been
+lost.
 
+We recommend the following simple retransmission policy for running the
+Wrestlers protocol over UDP.
+\begin{itemize}
+\item Initially, send out the \cookie{pre-challenge} message every minute.
+\item On receipt of a \cookie{pre-challenge} message, send the corresponding
+  full \cookie{challenge}, but don't retain any state.
+\item On receipt of a (valid) \cookie{challenge}, record the challenge value
+  $R'$ in a table, together with $K = (K_0, K_1)$ and the response $Y' = x
+  R'$.  If the table is full, overwrite an existing entry at random.  Send
+  the corresponding \cookie{response} message, and retransmit it every ten
+  seconds or so.
+\item On receipt of a (valid) \cookie{response}, discard any other
+  challenges, and stop sending \cookie{pre-challenge} and \cookie{response}
+  retransmits.  At this point, the basic protocol described above would
+  \emph{accept}, so the key $K_1$ is known to be good.  Send the
+  \cookie{switch} message, including its response to the (now known-good)
+  sender's challenge.
+\item On receipt of a (valid) \cookie{switch}, send back a \cookie{switch-ok}
+  message and stop retransmissions.  It is now safe to start sending messages
+  under $K_1$.
+\item On receipt of a (valid) \cookie{switch-ok}, stop retransmissions.  It
+  is now safe to start sending messages under $K_1$.
+\end{itemize}
 
 \subsubsection{Key reuse}
+Suppose our symmetric encryption scheme $\E$ is not only IND-CCA secure
+(definition~\ref{def:ind-cca}) but also provides integrity of plaintexts
+\cite{Bellare:2000:AER} (or, alternatively, is an AEAD scheme \fixme{AEAD
+cite}) 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}.
+
+%%%--------------------------------------------------------------------------
 
+\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.
 
 %%%--------------------------------------------------------------------------
 
@@ -2768,7 +2953,6 @@ P$ is $P_i$'s public key.  Let $S = (P_i, P_j, s)$ be a session.  We write
 $r_S$ for the random value chosen at the start of the session, and $R_S$,
 $c_S$ etc.\ are the corresponding derived values in that session.
 
-
 The proof uses a sequence of games.  For each game~$\G{i}$, let $V_i$ be the
 event that some pair of unexposed, matching sessions both complete but output
 different keys, and let $W_i$ be the event that the adversary's final output
@@ -2818,7 +3002,9 @@ game is identical to $\G0$, we can apply lemma~\ref{lem:shoup}, and see that
   \diff{0}{1} \le \frac{1}{|G|} \binom{n}{2} = \frac{n (n - 1)}{2 |G|}.
 \end{equation}
 In game~$\G1$ and onwards, we can assume that public keys for distinct
-parties are themselves distinct.
+parties are themselves distinct.  Note that the game now takes at most
+$O(q_I)$ times longer to process each message delivered by the adversary.
+This is where the $O(q_I q_M)$ term comes from in the theorem statement.
 
 Game~$\G2$ is the same as game~$\G1$, except that we change the way that we
 make parties respond to \cookie{challenge} messages $(\cookie{challenge}, R,
@@ -2856,8 +3042,7 @@ for any ripe session~$S$.  The following lemma shows how this affects the
 adversary's probabilities of winning.
 \begin{lemma}
   \label{lem:sk-g2-g3}
-  For some $t' = t + O(n) + O(q_S) + O(q_M q_I) + O(q_K)$ not much
-  larger than $t$ we have
+  For some $t'$ within the bounds given in the theorem statement we have
   \begin{equation}
     \label{eq:sk-g2-g3}
     \diff{2}{3} \le q_S \InSec{mcdh}(G; t', q_K).
@@ -2877,6 +3062,7 @@ and~$T$ of matching, unexposed sessions, $S$ has completed as a result of
 being sent a message $\mu \notin M_T$.  We have the following lemma.
 \begin{lemma}
   \label{lem:sk-g3-g4}
+  For a $t'$ within the stated bounds, we have
   \begin{equation}
     \label{eq:sk-g3-g4}
     \diff{3}{4} \le q_S \bigl( \InSec{ind-cca}(\E; t', q_M, q_M) +
@@ -2911,12 +3097,11 @@ We conclude that, for any adversary $A$,
   \Pr[V_4] = 0 \qquad \text{and} \qquad \Pr[W_4] = \frac{1}{2}.
 \end{equation}
 Putting equations~\ref{eq:sk-g0-g1}--\ref{eq:sk-g4} together, we find
-\fixme{format prettily}
 \begin{spliteqn}
-  \Adv{sk}{\Wident^{G, \E}}(A) \le \\
-     q_S \bigl( \InSec{mcdh}(G; t', q_K) +
-                n \cdot \InSec{mcdh}(G; t', q_M + q_I) +
-                \InSec{ind-cca}(\E; t', q_M, q_M) \bigr) + {}\\
+  \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}
@@ -3076,9 +3261,8 @@ The theorem follows, since $A$ was chosen arbitrarily.
     session state of $S$ or $T$ then $B$ stops the simulation abruptly and
     halts.
   \end{enumerate}
-  Adversary $B$'s running time is $t' = t + O(n) + O(q_S q_M) + O(q_I) +
-  O(q_K)$, and $B$ makes at most $q_K$ queries to $V(\cdot)$; we therefore
-  have
+  Adversary $B$'s running time is within the bounds required of $t'$, and $B$
+  makes at most $q_K$ queries to $V(\cdot)$; we therefore have
   \[ \Pr[F'] \le \Succ{mcdh}{G}(B) \le \InSec{mcdh}(G; t', q_K) \]
   as required.
 \end{proof}
@@ -3166,8 +3350,9 @@ The theorem follows, since $A$ was chosen arbitrarily.
   independent of everything in $A$'s view except the ciphertexts $\chi$
   output by $S$ and $T$.  Therefore, if the hidden bit of the IND-CCA game is
   $1$, $B$ accurately simulates $\G5$, whereas if the bit is $0$ then $B$
-  accurately simulates $\G6$.  Finally, we issue no more that $q_M$
-  encryption or decryption queries.  Therefore,
+  accurately simulates $\G6$.  We issue no more that $q_M$ encryption or
+  decryption queries.  Finally, $B$'s running time is within the bounds
+  allowed for $t'$.  Therefore,
   \[ \Adv{ind-cca}{\E}(B) = \Pr[F_5] - \Pr[F_6]
      \le \InSec{ind-cca}(\E; t', q_M, q_M). \]
   We construct the adversary~$\bar{B}$ which is the same as $B$ above, except
@@ -3225,8 +3410,10 @@ The theorem follows, since $A$ was chosen arbitrarily.
   \item If $A$ reveals $S$ or corrupts $P_i$ or $P_j$ then $B'$ stops the
     simulation immediately and halts.
   \end{enumerate}
-  Clearly $B'$ succeeds whenever $F_7$ occurs; hence we can apply
-  theorem~\ref{thm:wident-sound}.  The claim follows.
+  The running time of $B'$ is within the bounds required of $t'$; it makes at
+  most $q_I$ random-oracle and at most $q_M$ verification queries.  Clearly
+  $B'$ succeeds whenever $F_7$ occurs.  The claim follows from
+  theorem~\ref{thm:wident-sound}.
 \end{proof}
 
 
@@ -3265,6 +3452,88 @@ that a ripe session will only complete if the adversary has transmitted
 messages from its matching session correctly, and the session key is
 independent of the adversary's view.  The theorem follows.
 
+
+\subsection{Sketch proof of single-key protocol for secure channels}
+\label{sec:sc-proof}
+
+We want to show that the Wrestlers Key-Exchange protocol, followed by use of
+the encryption scheme $\E$, with the \emph{same} key $K = K_0$, still
+provides secure channels.
+
+\subsubsection{Secure channels definition}
+We (very briefly!) recall the \cite{Canetti:2001:AKE} definition of a secure
+channels protocol.  We again play a game with the adversary.  At the
+beginning, we choose a bit $b^* \inr \{0, 1\}$ at random.  We allow the
+adversary the ability to establish \emph{secure channels} sessions within the
+parties.  Furthermore, for any running session $S = (P_i, P_j, s)$, we allow
+the adversary to request $S$ to send a message~$\mu$ through its secure
+channel.  Finally, the adversary is allowed to choose one ripe
+\emph{challenge} session, and ask for it to send of one of a \emph{pair} of
+messages $(\mu_0, \mu_1)$, subject to the restriction that $|\mu_0| =
+|\mu_1|$; the session sends message $\mu_{b^*}$.  The adversary may not
+expose the challenge session.
+
+The adversary wins if (a)~it can guess the bit $b^*$, or (b)~it can cause a
+ripe session $S$ (i.e., an unexposed, running session), with a matching
+session~$T$ to output a message other than one that it requested that $T$
+send.
+
+\subsubsection{Protocol definition}
+The protocol begins with Wrestlers key-exchange.  The encryption in the
+key-exchange protocol is performed as $E_K(\cookie{kx}, \cdot)$; encryption
+for secure channels is performed as $E_K(\cookie{sc}, i, o, \cdot)$, where
+$i$ is a sequence number to prevent replays and $o \in \{S, T\}$ identifies
+the sender.
+
+\subsubsection{Proof sketch}
+We use the games and notation of appendix~\ref{sec:sk-proof}.
+
+The proof goes through as far as the step between $\G5$ and $\G6$ in the
+proof of lemma~\ref{lem:sk-g3-g4}.  Here we make the obvious adjustments to
+our adversary against the IND-CCA security of $\E$.  (Our adversary will need
+to use the left-or-right oracle for messages sent using the secure channel
+built on $K^*$.  That's OK.)
+
+In $\G4$, we know that ripe sessions agree the correct key, and the adversary
+never queries the random oracle, so the key is independent of the adversary's
+view.
+
+We define a new game $\G8$, which is like $\G4$, except that we stop the game
+if the adversary ever forges a message sent over the secure channel.  That
+is, if a ripe session $S$ ever announces receipt of a message not sent (at
+the adversary's request) by its matching session $T$.  Let $F_8$ be the event
+that a forgery occurs.  We apply lemma~\ref{lem:shoup}, which tells us that
+$\diff{4}{8} \le \Pr[F_8]$.  To bound $F_8$, we isolate a session at random
+(as in lemmata \ref{lem:sk-g2-g3} and~\ref{lem:sk-g3-g4}), which tells us
+that
+\begin{equation}
+  \label{eq:sc-g4-g8}
+  \diff{4}{8} \le q_S \cdot \InSec{int-ptxt}(\E; t', q_M, q_M)
+\end{equation}
+Finally, we can bound the adversary's advantage at guessing the hidden bit
+$b^*$.  We isolate (we hope) the challenge session $S$ by choosing a target
+session at random, as before.  Let $K_* = H_K(Z_S)$ be the key agreed by the
+session (if it becomes ripe).  We define an adversary $B$ against the IND-CCA
+security of $\E$.  The adversary $B$ simulates the game.  If the adversary
+exposes the target session, or doesn't choose it as the challenge session,
+$B$ fails (and exits 0); otherwise it uses the left-or-right encryption
+oracle to encrypt both of the adversary's message choices, and outputs the
+adversary's choice.  Let $b$ be the adversary's output, and let $\epsilon$ be
+the advantage of our IND-CCA distinguisher.  Then
+\begin{eqnarray*}[rl]
+  \Pr[b = b^*]
+  & = \Pr[b = b^* \wedge b^* = 1] + \Pr[b = b^* \wedge b^* = 0] \\
+  & = \frac{1}{2}\bigl( \Pr[b = b^* \mid b^* = 1] +
+      \Pr[b = b^* \mid b^* = 0] \bigr) \\
+  & = \frac{1}{2}\bigl( \Pr[b = b^* \mid b^* = 1] +
+                        (1 - \Pr[b \ne b^* \mid b^* = 0]) \bigr) \\
+  & = \frac{1}{2}\bigl( \Pr[b = 1 \mid b^* = 1] -
+                        \Pr[b = 1 \mid b^* = 0] + 1 \bigr) \\
+  & = \frac{1}{2}\bigl(1 + q_S\,\Adv{ind-cca}{\E}(B) \bigr) \\
+  & \le \frac{1}{2} \bigl( 1 + q_S\,\InSec{ind-cca}(\E; t', q_M, q_M) \bigr).
+			\eqnumber
+\end{eqnarray*}
+
 \end{document}
 
 %%% Local Variables: 
diff --git a/wrshortsl.tex b/wrshortsl.tex
deleted file mode 100644
index ad79cb3..0000000
--- a/wrshortsl.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-\let\short\relax
-\input wrslides
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "wrslides"
-%%% End: 
diff --git a/wrslides.cls b/wrslides.cls
index 1d7913e..aa82096 100644
--- a/wrslides.cls
+++ b/wrslides.cls
@@ -1,4 +1,11 @@
-\PassOptionsToClass{a4, article}{mdwslides}
+\newif\ifwrslides \wrslidestrue
+\InputIfFileExists{wr.cfg}\relax\relax
+
+\ifwrslides
+  \PassOptionsToClass{a4, slidesonly}{mdwslides}
+\else
+  \PassOptionsToClass{a4, article, twoside}{mdwslides}
+\fi
 \LoadClass{mdwslides}
 
 \newif\ifpdf
@@ -17,7 +24,6 @@
   \pdftrue
 \fi
 
-
 \RequirePackage{mdwlist}
 \RequirePackage[T1]{fontenc}
 \RequirePackage{colour}
@@ -29,6 +35,7 @@
 \RequirePackage{graphicx}
 \RequirePackage[palatino, helvetica, courier, maths = cmr]{mdwfonts}
 \RequirePackage{mdwthm}
+\RequirePackage{multicol}
 
 \def\Nupto#1{\{0, 1, \ldots, #1 - 1\}}
 \def\Bin{\{0, 1\}}
@@ -65,7 +72,7 @@
 \newcommand{\E}{{\mathcal{E}}}
 
 \def\Wident{\Xid{W}{ident}}
-\def\Wkw{\Xid{W}{kx}}
+\def\Wkx{\Xid{W}{kx}}
 
 \def\other{\colour{blue}}
 \def\diff{\colour{red}}
diff --git a/wrslides.tex b/wrslides.tex
index a444f79..ae50308 100644
--- a/wrslides.tex
+++ b/wrslides.tex
@@ -1,7 +1,4 @@
 \documentclass{wrslides}
-\ifx\short\xxundefined\else
-  \includeonly{wrslide}
-\fi
 
 \begin{document}
 
@@ -21,8 +18,8 @@
   \bigskip
 \end{slide}
 
-\include{background}
-\include{wrslide}
+\include{wr-backg}
+\include{wr-main}
 
 \end{document}
 
-- 
2.11.0

