\documentclass{splib}

\begin{document}
% main environment
\begin{protocol}%
  {Needham-Schroeder Public Key}%
  {Roger Needham and Michael Schroeder}%
  {12/1978}%
  {Ralf Treinen}%
  {04/11/2002}%
  {09/12/2002}

\begin{abstract}
  Mutual authentication, using a trusted key server 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}{KPa}}
\msg{7}{A}{B}{\crypt{Nb}{KPb}}
\end{messages}
\end{core}

\begin{explanation}
  This protocol has been proposed by \cite{NeedhamSchroeder78cacm}. In this
  protocol description, \code{KSa} (resp. \code{KSb}, \code{KSs}) is the secret key corresponding
  to the public key \code{KPa} (resp. \code{KPb}, \code{KPs}).
\end{explanation}

\begin{property}
  After completion of the protocol, the two principals \code{A} and \code{B} should be
  convinced about the identity of their respective correspondent.
\end{property}

\begin{references}
\cite{NeedhamSchroeder78cacm}.
\end{references}

\begin{proofs}
  Burrows, Abadi and Needham \cite{BAN} prove the correctness of the protocol
  in the sense of their logical framework. However, they point out a possible
  replay attack which, according to them, could be avoided by using
  timestamps.
\end{proofs}

\begin{attacks}
  An intruder \code{I} may impersonate \code{A}, by inciting \code{A} to initiate a second
  session\cite{Lowe74ipl}. In the following, we ignore the message exchanges
  with the public key server and only consider messages between the
  principals \code{A} and \code{B}, and the intruder \code{I}. 
  We assume that the intruder \code{I} possesses a key pair
  \code{(KPi, KSi)}, and we may also assume that every principal
  knows the public keys \code{KPa}, \code{KPb} and \code{KPi}.

\begin{messages}
\msg{i.3}{A}{I}{\crypt{Na,A}{KPi}}
\msg{ii.3}{I(A)}{B}{\crypt{Na,A}{KPb}}
\msg{ii.6}{B}{I(A)}{\crypt{Na,Nb}{KPa}}
\msg{i.6}{I}{A}{\crypt{Na,Nb}{KPa}}
\msg{i.7}{A}{I}{\crypt{Nb}{KPi}}
\msg{ii.7}{I(A)}{B}{\crypt{Nb}{KPb}}
\end{messages}
\end{attacks}

\begin{remark}
  It has been proposed to fix the protocol by including the respondent's
  identity in the response \cite{Lowe74ipl}.
\end{remark}

\begin{see}
  \crossref{nspkLowe}
\end{see}

\end{protocol}
\end{document}


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