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

\documentclass{splib}
\usepackage[latin1]{inputenc} 
\usepackage[T1]{fontenc} 

\begin{document}
\begin{protocol}{Yahalom}%
{Yahalom}{0/0/1988}{}{}{04/10/2002}

\begin{abstract}
Distribution of a fresh symmetric shared key by
a trusted server and mutual authentication.
Symmetric keys and trusted server.
\end{abstract}

\begin{core}
\begin{declarations}
\dcl{A, B, S}{principal}
\dcl{Na, Nb}{number fresh}
\dcl{Kas, Kbs, Kab}{key}
\end{declarations}

\begin{declarations}
\dcl{A knows}{A, B, S, Kas}
\dcl{B knows}{B, S, Kbs}
\dcl{S knows}{S, A, B, Kas, Kbs}
\end{declarations}

\begin{messages}
\msg{1}{A}{B}{ A, Na }
\msg{2}{B}{S}{ B, \crypt{A, Na, Nb}{Kbs} }
\msg{3}{S}{A}{ \crypt{B, Kab, Na, Nb}{Kas}, \crypt{A, Kab}{Kbs} }
\msg{4}{A}{B}{ \crypt{A, Kab}{Kbs}, \crypt{Nb}{Kab} }
\end{messages}
\end{core}

\begin{explanation}
The fresh symmetric shared key \code{Kab} is created by the server
\code{S} and sent encrypted, in message \code{3} both to \code{A}
(directly) and to \code{B} (indirectly).
\end{explanation}

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

\code{A} must be also properly authentified to \code{B}.
\end{property}

\begin{references}
This version of the Yahalom protocol 
is the one found in~\cite{BurrowsAbadiNeedham89}
(cited as personal communication in this paper).

It is also presented in~\cite{ClarkJacob97}.
\end{references}

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

\begin{see}
\crossref{yahalomBAN},\\
\crossref{yahalomPaulson}.
\end{see}

\end{protocol}
\end{document}

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