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

\documentclass{splib}

\begin{document}
% main environment
\begin{protocol}%
% name
{Kerberos V5}%
% authors
{B. Clifford Neuman and Theodore Ts'o}%
% date of the first publication
{1994}%
% editor name
{}%
% date of submission
{}%
% date of last change, empty or = date of submission
{07/11/2002}

\begin{abstract}
Distribution of a symmetric key (in a \emph{ticket}),
for communication between a client and a server,
with authentication.
\end{abstract}

\begin{remark}
This protocol is based on based on the \crossref{nssk} protocol
and uses timestamps and nonces to correct the flaw of Denning Sacco.
\end{remark}

\begin{core}
\begin{declarations}
\dcl{A, G, C, S, U }{principal}
\dcl{N1, N2 }{nonce}
\dcl{L1, L2 }{nonce}
\dcl{T1start, T1expire }{timestamp}
\dcl{T2start, T2expire }{timestamp}
\dcl{Kcg, Kcs, Kag, Ku, Kgs }{key}
\end{declarations}

\begin{messages}
\msg{1}{C}{A}{U, G, L1, N1}
\msg{2}{A}{C}{U, \crypt{U, C, G, Kcg, T1start, T1expire}{Kag},}
\msg{}{}{}{\crypt{G, Kcg, T1start, T1expire}{Ku}}
\msg{3}{C}{G}{S, L2, N2, \crypt{U, C, G, Kcg, T1start, T1expire}{Kag},}
\msg{}{}{}{\crypt{C, T1}{Kcg}}
\msg{4}{G}{C}{U, \crypt{U, C, S, Kcs, T2start, T2expire}{Kgs},}
\msg{}{}{}{\crypt{S, Kcs, T2start, T2expire, N2}{Kcg}}
\msg{5}{C}{S}{\crypt{U, C, S, Kcs, T2start, T2expire}{Kgs},}
\msg{}{}{}{\crypt{C, T2}{Kcs}}
\msg{6}{S}{C}{\crypt{T2}{Kcs}}
\end{messages}
\end{core}

\begin{explanation}
\begin{description}
\item \code{C} is a client, 
\item \code{S} is a a server (\code{C} wants to communicate with \code{S}),
\item \code{U} is a user on behalf of which \code{A} and \code{S} communicate,
\item \code{G} is a ticket granting server, 
\item \code{A} is a key distribution center (trusted server).
\end{description}
The keys \code{Kag} and \code{Kgs} are long term symmetric key
whose values are supposed to be known initially
only by, \code{A} and \code{G}, respectively \code{G} and \code{S}.

\code{L1} and \code{L2} are lifetimes, \code{N1} and \code{N2} are
nonces.
\code{T1start}, \code{T1expire}, \code{T2start}, \code{T2expire} are
time stamps which define the interval of validity of the ticket in
which they are contained.

\code{U} is a user on behalf of whom the client \code{C} communicates.
In particular, \code{C} initially knows the value of the key \code{Ku}.

The key \code{Kcg} is freshly generated by \code{A} for communication
between \code{C} and \code{G}, and in transmitted 
to \code{C} in message \code{2}, encrypted by \code{Ku},
and indirectly to \code{G}, in the \emph{ticket}
\code{\crypt{U, C, G, Kcg, T1start, T1expire}{Kag}}
which \code{C} transmits blindly to \code{G} in message \code{3}.

The authentificator \code{\crypt{C, T1}{Kcg}} is used by \code{G}
to check timeliness of the ticket.

The key \code{Kcs} is freshly generated by \code{G} for communication
between \code{C} and \code{G}, and in transmitted 
to \code{C} in message \code{4}, encrypted by \code{Kcg},
and indirectly to \code{S}, in the \emph{ticket}
\code{\crypt{U, C, S, Kcs, T2start, T2expire}{Kgs}}
which \code{C} transmits blindly to \code{S} in message \code{5}.
\end{explanation}

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

\code{A} and \code{C} must agree on the values of
\code{T1start} and \code{T1expire}.

\code{G} and \code{C} must agree on the values of
\code{T2start} and \code{T2expire} and \code{T1}.

\code{C} and \code{S} must agree on the value of \code{T2}.
\end{property}

\begin{references}
\cite{kerberos}
\end{references}

\begin{proofs}
\begin{itemize}
\item \cite{kerberos}
\item \cite{BurrowsAbadiNeedham89}
\item \cite{BellovinMerritt-kerberos} modelization with Abstract State Machines
(stepwise refinements), and (manual) proof of correctness.
\end{itemize}
\end{proofs}

\begin{see} 
\crossref{nssk}
\end{see}

\end{protocol}
\end{document}

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