% File              : Bull.tex
% Version           : 
% Last-modified     : 19/10/2005
% Last-modifier     : Delaune

\documentclass{splib}

\begin{document}
% main environment
\begin{protocol}%
% name
{Bull's Authentication Protocol}%
% authors
{J.~Bull}%
% date of the first publication
{1997}%
% editor name
{}%
% date of submission
{}%
% date of last change, empty or = date of submission
{}

\newcommand{\xor}{\oplus}

\begin{abstract}
This protocol, described in~\cite{bull97}, aims at establishing fresh
session keys between a fixed number of participants (for instance 3) and a server: one
key for each pair of agents adjacent in the chain. 
\end{abstract}


\begin{core}
\begin{declarations}
\dcl{A, B, C, S}{principal}
\dcl{Kab, Kbc}{fresh symkey}
\dcl{Na, Nb, Nc}{fresh number}
\dcl{Kas, Kbs, Kcs}{symkey}
\dcl{h}{message, symkey -> message }
\end{declarations}

\code{A computes Xa = h(\tuple{A,B,Na},Kas), \tuple{A,B,Na}}
\begin{messages}
\msg{1} {A}{B}{Xa}
\end{messages}

\code{B computes Xb = h(\tuple{B,C,Nb,Xa},Kbs), \tuple{B,C,Nb,Xa}}

\begin{messages}
\msg{2} {B}{C}{Xb}
\end{messages}

\code{C computes Xc = h(\tuple{C,S,Nc,Xb},Kcs), \tuple{C,S,Nc,Xb}}

\begin{messages}
\msg{3} {C}{S}{Xc}
\end{messages}

\begin{messages}
\msg{4} {S}{C}{A, B, Kab xor h(Na,Kas), \crypt{A,B,Na}{Kab},} 
\msg{}  {} {} {B, A, Kab xor h(Nb,Kbs), \crypt{B,A,Nb}{Kab},}
\msg{}  {} {} {B, C, Kbc xor h(Nb,Kbs), \crypt{B,C,Nb}{Kbc},}
\msg{}  {} {} {C, B, Kbc xor h(Nc,Kcs), \crypt{C,B,Nc}{Kbc}}
\msg{5} {C}{B}{A, B, Kab xor h(Na,Kas), \crypt{A,B,Na}{Kab},}
\msg{}  {} {} {B, A, Kab xor h(Nb,Kbs), \crypt{B,A,Nb}{Kab},}
\msg{}  {} {} {B, C, Kbc xor h(Nb,Kbs), \crypt{B,C,Nb}{Kbc}}
\msg{6} {B}{A}{A, B, Kab xor h(Na,Kas), \crypt{A,B,Na}{Kab}}
\end{messages}
\end{core}

\begin{explanation}
The protocol is initiated by \code{A} and then goes through
\code{B} and \code{C} before reaching \code{S}.  At the end, new session
keys \code{Kab} and \code{Kbc} are established. 
The properties of exclusive or are:

\begin{eqnarray*}
\code{x xor (y xor z)} &=& \code{(x xor y) xor z} ~~\mbox{(E1)}\\
\code{x xor y} &=& \code{y xor x}  ~~\mbox{(E2)}\\
\code{x xor 0} &=& \code{x}  ~~\mbox{(E3)}\\
\code{x xor x} &=& \code{0}  ~~\mbox{(E4)}
\end{eqnarray*}

\end{explanation}

\begin{property}
The protocol must guaranty the secrecy of \code{Kxy}.
 Each key \code{Kxy}
should be known to exactly \code{x} and \code{y} (and also \code{S}),
even if some nodes other than \code{x} and \code{y} %(for example\code{C}
 are malicious.

\end{property}

\begin{references}
\cite{bull97}
\end{references}

%\begin{proofs}
%\end{proofs}

\begin{attacks}
This protocol is subject to an attack~\cite{RS98} that can be mounted by a
dishonest participant. 
For example, assume that \code{C} is a malicious agent. He can
intercept \code{Kab xor h(Nb,Kbs)} and \code{Kbc xor h(Nb,Kbs)} sent by
\code{S} at step~4, and since \code{C} knows the session key \code{Kbc}, he
can compute \code{Kbc xor Kab xor h(Nb,Kbs) xor Kbc xor h(Nb,Kbs)}.
Since this term is actually equal to \code{Kab}, the agent \code{C} learns 
a session key that should be shared only by
\code{A} and~\code{B}.
\end{attacks}

%\begin{remark}
%\end{remark}

%\begin{see} %\crossref{}, see all.aux for labels names
%\end{see}

\end{protocol}
\end{document}
