\documentclass{splib}

\begin{document}
% main environment
\begin{protocol}%
  {Lowe's fixed version of Needham-Schroder Public Key}%
  {Gavin Lowe}%
  {1995}%
  {}%
  {}%
  {06/11/2002}

\begin{abstract}
  This protocol is an amended version of the \crossref{nspk}.
  Its purpose id mutual authentication, using a trusted keyserver and public keys.
  
\end{abstract}

\begin{core}
\begin{declarations}
\dcl{A,B,S}{Principal}
\dcl{Na,Nb}{Nonce}
\dcl{KPa,KPb,KPs,KSa,KSb,KSs}{Key}
\dcl{KPa,KSa}{is a key pair}
\dcl{KPb,KSb}{is a key pair}
\dcl{KPs,KSs}{is a key pair}
\end{declarations}

\begin{messages}
\msg{1}{A}{S}{A,B}
\msg{2}{S}{A}{\crypt{KPb, B}{KSs}}
\msg{3}{A}{B}{\crypt{Na, A}{KPb}}
\msg{4}{B}{S}{B,A}
\msg{5}{S}{B}{\crypt{KPa, A}{KSs}}
\msg{6}{B}{A}{\crypt{Na, Nb, B}{KPa}}
\msg{7}{A}{B}{\crypt{Nb}{KPb}}
\end{messages}
\end{core}

\begin{explanation}
  Compared to the original version of the \crossref{nspk} protocol,
  the identity of the responder \code{B} has been added in
  the message \code{6} to prevent the attack discovered in~\cite{Lowe74ipl}.
\end{explanation}

\begin{property}
See \crossref{nspk}.
\end{property}

\begin{references}
\cite{Lowe74ipl}
\end{references}

\begin{proofs}
  It is reported in \cite{Lowe74ipl} 
  that the technique that permitted to find the 
  Lowe attack on the \crossref{nspk} protocol
  (running FDR on a CSP presentation of the protocol)
  found no attack on this protocol.
\end{proofs}

\begin{see}
  \crossref{nspk}
\end{see}

\end{protocol}
\end{document}


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