From: Mark Wooding Date: Thu, 2 Nov 2006 13:17:26 +0000 (+0000) Subject: Add build system. Write most of the introduction. X-Git-Tag: eprint-1~1 X-Git-Url: https://git.distorted.org.uk/~mdw/doc/wrestlers/commitdiff_plain/dff0fad2fb0c4edacbe668fdd72030e7e8ac5db7 Add build system. Write most of the introduction. --- 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}