% File              : wooLamPif.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
{Woo and Lam Pi f}%
% authors
{Woo, Lam}%
% date of the first publication
{1994}%
% editor name
{}%
% date of submission
{}%
% date of last change, empty or = date of submission
{27/10/2001}

\begin{abstract}
One way authentification protocol with
public keys and trusted server.
\end{abstract}

\begin{core}
\begin{declarations}
\dcl{A, B, S}{principal}
\dcl{shared}{(principal, principal):key}
\dcl{Nb}{nonce}
\end{declarations}

%\begin{declarations}
%\dcl{A knows}{A, B, Kas}
%\dcl{B knows}{B, S, Kbs}
%\dcl{S knows}{S, Kas, Kbs}
%\end{declarations}

\begin{messages}
\msg{1.}{A}{B}{A}
\msg{2.}{B}{A}{Nb}
\msg{3.}{A}{B}{\crypt{A,B,Nb}{\apply{shared}{A, S}}}
\msg{4.}{B}{S}{\crypt{A, B, Nb, \crypt{A, B, Nb}{\apply{shared}{A, S}}}{\apply{shared}{B, S}}}
\msg{5.}{S}{B}{\crypt{A, B, Nb}{\apply{shared}{B, S}}}
\end{messages}
\end{core}

\begin{explanation}
\code{shared(A, S)} is a long term symmetric key shared
by \code{A} and \code{S}. Initially, \code{A} only knowns
\code{shared(A, S)} and the name of \code{B},
\code{B} only knowns \code{shared(B, S)}
and \code{S} knowns all shared keys, 
i.e. \code{S} given any principal's name \code{X}, 
\code{S} knowns \code{shared(X, S)},
or in other terms, \code{S} knows the ``function'' \code{shared}.
\end{explanation}

\begin{property}
Woo and Lam give in~\cite{WooLam94} the following definition of 
correctness for this protocol:

whenever the principal \code{B} finishes the execution of the protocol,
the initiator of the protocol execution is in fact the 
principal \code{A} claimed in message \code{1}.
\end{property}

\begin{references}
\cite{WooLam94}, \cite{ClarkJacob97}.
\end{references}

\begin{proofs}
\cite{WooLam94}
\end{proofs}

\begin{attacks}
No known attacks.
\end{attacks}

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

\begin{see} %\crossref{}, see all.aux for labels names
\crossref{wooLamPi1},
\crossref{wooLamPi2},
\crossref{wooLamPi3},
\crossref{wooLamPi}.
\end{see}

\end{protocol}
\end{document}

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