% File              : wideMouthedFrog.tex
% Version           : $Revision: 1.2 $
% Last-modified     : $Date: 2005/01/04 10:35:35 $
% Last-modifier     : FJ

\documentclass{splib}

\begin{document}
% main environment
\begin{protocol}%
% name
{Wide Mouthed Frog}%
% authors
{Michael Burrows}%
% date of the first publication
{1989}%
% editor name
{}%
% date of submission
{}%
% date of last change, empty or = date of submission
{20/11/2002}

\begin{abstract}
Distribution of a fresh shared key.
Symmetric key cryptography with server and timestamps.
\end{abstract}

\begin{core}
\begin{declarations}
\dcl{A, S}{principal}
\dcl{Kas, Kbs, Kab}{symkey}
\dcl{Ta, Ts}{timestamp}
\end{declarations}

\begin{messages}
\msg{1}{A}{S}{A, \crypt{Ta, B, Kab}{Kas}}
\msg{2}{S}{B}{\crypt{Ts, A, Kab}{Kbs}}
\end{messages}
\end{core}

\begin{explanation}
Some explanations quoted from \cite{BurrowsAbadiNeedham89}:
\begin{quote}
"It is assumed that the encryption is done in such a way that we know
the whole message was sent at once.  If two separate encrypted
sections are included in one message, we treat them as though they
arrived in separate messages.  A message cannot be understood by a
principal who does not know the key (or, in the case of public-key
cryptography, by a principal who does not know the inverse of the
key); the key cannot be deduced from the encrypted message.  Each
encrypted message contains sufficient redundancy to allow a principal
who decrypts it to verify that he has used the right key.  In
addition, messages contain sufficient information for a principal to
detect (and ignore) his own messages."
\end{quote}

\begin{quote}
"\code{A} sends a session key to \code{S}, including a timestamp \code{Ta}.
\code{S} checks that the first message is timely, and if it is, it forwards
the message to \code{B}, together with its own timestamp \code{Ts}.   
\code{B} then checks that the timestamp 
from \code{S} is later than any other it has received from \code{S}." 
\end{quote}
\end{explanation}

\begin{property}
The protocol must guaranty the secrecy of the new shared key
\code{Kab}:
in every session, the value of \code{Kab} must be known only by
the participants playing the roles of \code{A} and \code{B} and \code{S}.

The protocol must guaranty the authenticity of \code{Kab}:
in every session, on reception of message \code{2}, 
\code{B} must be ensured that the key \code{Kab} in the message
has been created by \code{S} in the same session on behalf of \code{A}.
\end{property}

\begin{references}
\cite{BurrowsAbadiNeedham89}
\end{references}

\begin{proofs}
\cite{BurrowsAbadiNeedham89}
\end{proofs}

\begin{attacks}
\paragraph{1.}
\cite{AndersonNeedham95}.
By replaying the second message within an appropriate time window, 
the intruder \code{I} can make the server \code{S} update the timestamp
of an non-fresh key \code{Kab}.
This way, he can extend the life time
of a (possibly compromised) key \code{Kab} as wanted, 
whereas \code{A} and \code{B}
think that it has expired and has been destroyed.
\begin{messages}
\msg{i.1}{A}{S}{A, \crypt{Ta, B, Kab}{Kas}}
\msg{i.2}{S}{B}{\crypt{Ts, A, Kab}{Kbs}}
\msg{ii.1}{I(B)}{S}{B, \crypt{Ts, A, Kab}{Kbs}}
\msg{ii.2}{S}{A}{\crypt{T's, B, Kab}{Kas}}
\msg{iii.1}{I(A)}{S}{A, \crypt{T's, B, Kab}{Kas}}
\msg{iii.2}{S}{B}{\crypt{T''s, A, Kab}{Kbs}}
\msg{...}{}{}{}
\end{messages}

\paragraph{2.}
\cite{Lowe97}.
In this attack, \code{B} thinks that \code{A} has
established two sessions with him, when \code{A}
thinks he has established only one session.
\begin{messages}
\msg{i.1}{A}{S}{A, \crypt{Ta, B, Kab}{Kas}}
\msg{i.2}{S}{B}{\crypt{Ts, A, Kab}{Kbs}}
\msg{ii.2}{S}{B}{\crypt{Ts, A, Kab}{Kbs}}
\end{messages}
\cite{Lowe97} proposes a correction of the protocol
which is described in \crossref{wideMouthedFrogLowe}.
\end{attacks}

\begin{addcomment}{Martin Abadi}{November 18, 2002}
The \cite{AndersonNeedham95} and \cite{Lowe97} "attacks" fail, because of the
protocol features described in the quotations above. The "attacks"
may work only against (deliberately or unintentionally) weakened
variants of the protocol.
\end{addcomment}


\begin{see}
\crossref{wideMouthedFrogLowe}
\end{see}

\end{protocol}
\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
