%%%
\newif\iffancystyle\fancystylefalse
+\newif\ifshort\shortfalse
\fancystyletrue
+\InputIfFileExists{wr.cfg}\relax\relax
\errorcontextlines=\maxdimen
\showboxdepth=\maxdimen
\showboxbreadth=\maxdimen
\let\Ccheckset=V
\let\Ccount=\nu
+\def\HG#1{\mathbf{H}_{#1}}
+
\begin{document}
%%%--------------------------------------------------------------------------
\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}
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
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}
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}
%%%--------------------------------------------------------------------------
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
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}
\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
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
\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.
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}
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
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
\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.
%%%--------------------------------------------------------------------------
$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
\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,
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).
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) +
\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}
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}
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
\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}
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:
~mdw / doc / wrestlers / commitdiff