% File              : yahalomBAN.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}{Paulson's strengthened version of Yahalom}%
{Paulson}{0/0/2001}{}{}{04/10/2002}


\begin{abstract}
Paulson's modified version of the \crossref{yahalom} protocol.
%following the suggestion of~\cite{BurrowsAbadiNeedham89}.
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, Nb, \crypt{A, Na}{Kbs} }
\msg{3}{S}{A}{ Nb, \crypt{B, Kab, Na}{Kas}, \crypt{A, B, Kab, Nb}{Kbs} }
\msg{4}{A}{B}{ \crypt{A, B, Kab, Nb}{Kbs}, \crypt{Nb}{Kab} }
\end{messages}
\end{core}

\begin{explanation}
To prevent the attacks~\cite{Syverson_replay} of to
\crossref{yahalomBAN} protocol,
the name of \code{B} has been added to the cipher sent by \code{S} in
message \code{3} and transmitted by \code{A} in message \code{4}.
\end{explanation}

\begin{property}
See~\crossref{yahalom}.
\end{property}

\begin{references}
\cite{Paulson_yahalom}
\end{references}

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

\begin{see}
\crossref{yahalom},\\
\crossref{yahalomBAN}
\end{see}

\end{protocol}
\end{document}

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