+\end{frame}
+
+\begin{frame}{Key exchange: protocols}
+ %% overlays
+ %% 1 - original broken protocol
+ %% 2 - encrypt responses
+ %% 3 - session-ids
+ %% 4 - pre-challenges
+ \begin{protocol}{3.9}{17}
+ \node [alice, thoughts] at (0, 1.5)
+ {\footnotesize Private $a$; public $A = a P$};
+
+ \node [bob, thoughts] at (0, 3)
+ {{ $u \getsr \Nupto{q}$; \\
+ $U \gets u P$;
+ $Y_B \gets u A$; }};
+ \only<4->
+ {\path [message, ->] (0, 6) -- node [above] {$\alert<4>{U}$} +(1, 0);}
+ \path [message, ->] (0, 9) -- node [above]
+ {$U, u \xor H(\cookie{check},
+ \only<3->{\alert<3>{B}, \alert<3>{s},}
+ \only<4->{\alert<4>{V},}
+ U, Y_B$)}
+ +(1, 0);
+
+ \node [alice, thoughts] at (0, 11)
+ {{\strut
+ \only<1>{$Z \gets v U$; \\}%
+ \action<only@2-| alert@2>
+ {$(K, \hat{K}) \gets H(\cookie{key}, v U)$; \\}%
+ $Y'_B \gets a U$; }};
+ \path [message, <-] (0, 13.5) -- node [above]
+ {$\action<only@2-| alert@2>{E_{\hat{K}}(}
+ Y'_B
+ \action<only@2-| alert@2>{)}$}
+ +(1, 0);
+
+ \node [bob, other, thoughts] at (0, 1.5)
+ {\footnotesize Private $b$; public $B = b P$};
+
+ \node [alice, other, thoughts] at (0, 3)
+ {{ $v \getsr \Nupto{q}$; \\
+ $V \gets v P$;
+ $Y_A \gets v B$; }};
+ \only<4->
+ {\path [message, other, <-] (0, 7.5) --
+ node [above] {$\alert<4>{V}$} +(1, 0);}
+ \path [message, other, <-] (0, 10.5) -- node [above]
+ {$V, v \xor H(\cookie{check},
+ \only<3->{\alert<3>{A}, \alert<3>{s},}
+ \only<4->{\alert<4>{U},}
+ V, Y_A$)}
+ +(1, 0);
+
+ \node [bob, other, thoughts] at (0, 11)
+ {{\strut
+ \only<1>{$Z \gets u V$; \\}%
+ \action<only@2-| alert@2>
+ {$(K, \hat{K}) \gets H(\cookie{key}, u V)$; \\}%
+ $Y'_A \gets b V$; }};
+ \path [message, other, ->] (0, 15) -- node [above]
+ {${\action<only@2-| alert@2>{E_{\hat{K}}(}}
+ Y'_A
+ {\action<only@2-| alert@2>{)}}$}
+ +(1, 0);
+ \node [bob, thoughts] at (0, 15.5) {Use key $K$;};
+ \node [alice, thoughts] at (0, 15.5) {Use key $K$;};
+ \end{protocol}
+\end{frame}