+ \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}