% 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}{BAN simplified version of Yahalom}%
{Burrows Abadi Needham}{0/0/1989}{}{}{09/10/2002}

\begin{abstract}
An amended version of the \crossref{yahalom} protocol,
presented in the BAN logic paper.
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, Kab, Nb}{Kbs} }
\msg{4}{A}{B}{ \crypt{A, Kab, Nb}{Kbs}, \crypt{Nb}{Kab} }
\end{messages}
\end{core}

\begin{explanation}
Compared to the original version of the \crossref{yahalom} protocol,
the nonce \code{Nb} is added to the second cipher of message \code{3},
to prevent a malicious \code{A} to reuse an old value of \code{Kab}.

Also, \code{Nb} is sent in cleartext in message \code{2}, which makes
possible the attacks below.
\end{explanation}

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

\begin{references}
This simplified version of the Yahalom protocol 
was proposed in~\cite{BurrowsAbadiNeedham89}.
\end{references}

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

\begin{attacks}
Replay attack with interleaving and type error in~\cite{Syverson_replay}.
\begin{messages}
\msg{i.1}{A}{I(B)}{A, Na}
\msg{i.2}{B}{I(S)}{B, Nb, \crypt{A, Na}{Kbs}}
\msg{ii.1}{I(A)}{B}{A, Na, Nb}
\msg{ii.2}{B}{I(S)}{B, Nb, \crypt{A, Na, Nb}{Kbs}}
\msg{i.3}{}{}{Omitted}
\msg{i.4}{I(A)}{B}{\crypt{A, Na, Nb}{Kbs}, \crypt{Nb}{Na}}
\end{messages}
In the message \code{1} of session \code{ii}, the pair \code{Na, Nb} is
used as a nonce \code{N'a},
and in the last message of session \code{i},  \code{Na} is used as the key \code{Kab}.

A second replay attack is described in the same paper~\cite{Syverson_replay}.
\begin{messages}
\msg{i.1}{A}{I(B)}{A, Na}
\msg{ii.1}{I(B)}{A}{B, Na}
\msg{ii.2}{A}{I(S)}{A, N'a, \crypt{B, Na}{Kas}}
\msg{iii.1}{}{}{Omitted}
\msg{iii.2}{I(A)}{S}{A, Na, \crypt{B, Na}{Kas}}
\msg{iii.3}{S}{I(B)}{Na, \crypt{A, Kab, Na}{Kbs}, \crypt{B, Kab, Na}{Kas}}
\msg{i.2}{}{}{Omitted}
\msg{i.3}{I(S)}{A}{Ni, \crypt{B, Kab, Na}{Kas}, \crypt{A, Kab, Na}{Kbs}}
\msg{i.4}{A}{I(B)}{\crypt{A, Kab, Na}{Kbs}, \crypt{Ni}{Kab}}
\end{messages}
\end{attacks}

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

\end{protocol}
\end{document}

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