% File              : gong.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
{Gong}%
% authors
{Li Gong}%
% date of the first publication
{1989}%
% editor name
{}%
% date of submission
{}%
% date of last change, empty or = date of submission
{6/02/2003}

\begin{abstract}
Mutual authentication protocol of two principals with a trusted
server, and exchange of a new symmetric key.
Uses one-way functions and no encryption.
\end{abstract}

\begin{core}
\begin{declarations}
\dcl{A, B, S}{principal}
\dcl{Na, Nb, Ns}{number}
\dcl{Pa, Pb}{number}
\dcl{K, Ha, Hb}{number}
\dcl{f1}{number, number, number, number -> number}
\dcl{f2}{number, number, number, number -> number}
\dcl{f3}{number, number, number, number -> number}
\dcl{g}{number, number, number, number -> number}
\dcl{xor}{number,number -> number}
\freedcl{}
\freedcl{alias \code{K} =  \code{f1(Ns,Na,B,Pa)}}
\freedcl{alias \code{Ha} = \code{f2(Ns,Na,B,Pa)}}
\freedcl{alias \code{Hb} = \code{f3(Ns,Na,B,Pa)}}
\end{declarations}

\begin{messages}
\msg{1}{A}{B}{A, B, Na}
\msg{2}{B}{S}{A, B, Na, Nb}
\msg{3}{S}{B}{Ns, xor(f1(Ns, Nb, A, Pb), K),}
\msg{}{}{}{xor(f2(Ns, Nb, A, Pb), Ha),}
\msg{}{}{}{xor(f3(Ns, Nb, A, Pb), Hb),}
\msg{}{}{}{g(K, Ha, Hb, Pb)}
\msg{4}{B}{A}{Ns, Hb}
\msg{5}{A}{B}{Ha}
\end{messages}
\end{core}

\begin{explanation}
\code{f1}, \code{f2}, \code{f3}, and \code{g}
are one-way functions. 

Initially, the principal \code{A} 
(resp. \code{B}) shares the long-term secret \code{Pa}
(resp. \code{Pb}) with the server \code{S}.

\code{Na}, \code{Nb} and \code{Ns} are nonces and
\code{Ha}, \code{Hb} and \code{K} are just aliases for
resp. \code{f2(Ns,Na,B,Pa)}, 
\code{f3(Ns,Na,B,Pa)}, and \code{f1(Ns,Na,B,Pa)}.

We assume commutativity and associativity for the \code{xor}
operator, 
\begin{quote}
\code{xor(x, y)} = \code{xor(y, x)}\\
\code{xor(x, xor(y, z))} = \code{xor(xor(x, y), z)}
\end{quote}
as well as the xor axioms:
\begin{quote}
\code{xor(x, 0)} = \code{x}\\
\code{xor(x, x)} = \code{0}
\end{quote}
Hence, the principal \code{B} can extract 
\code{Ha}, \code{Hb} and \code{K} from the message \code{3},
and check them using the checksum \code{g(K, Ha, Hb, Pb)}.

Knowing \code{Pa}, the principal \code{A} can construct
\code{Ha}, \code{Hb} and \code{K} once he has received \code{Ns}
in message \code{4}, he can check the check value for \code{Hb}
he has just computed against the one sent by \code{B} in message
\code{4} and send the last message.
\end{explanation}

\begin{property}
The protocol must guaranty the secrecy of \code{K}:
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.

The protocol must also ensure mutual authentication of 
\code{A} and \code{B}.
\end{property}

\begin{references}
\cite{Gong89}
\end{references}

\end{protocol}
\end{document}

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