% File              : yahalomBAN.tex
% Version           : $Revision: 1.1 $
% Last-modified     : $Date: 2005/01/04 11:45:32 $
% Last-modifier     : FJ

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

\begin{document}
\begin{protocol}{Lowe's modified version of Yahalom}%
{Paulson}{0/0/2001}{}{}{04/10/2002}

\begin{abstract}
Lowe'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}{\crypt{A, Na, Nb}{Kbs}}
\msg{3}{S}{A}{\crypt{B, Kab, Na, Nb}{Kas}}
\msg{4}{S}{B}{\crypt{A, Kab}{Kbs}}
\msg{5}{A}{B}{\crypt{A, B, S, Nb}{Kab}}
\end{messages}
\end{core}

\begin{remark}
This version of the Yahalom protocol is presented
in \cite{Lowe98} to illustrate 
a verification technique by model checking.
\end{remark}

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

\begin{references}
\cite{Lowe98}
\end{references}

\begin{proofs}
\cite{Lowe98}
\end{proofs}

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

\end{protocol}
\end{document}

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