% File              : shoupRubin.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
{SK3}%
% authors
{Victor Shoup and Avi D. Rubin}%
% date of the first publication
{1996}%
% editor name
{}%
% date of submission
{}%
% date of last change, empty or = date of submission
{11/02/2003}

\begin{abstract}
Symmetric key distribution using Smart Cards, by Shoup and Rubin.
\end{abstract}

\begin{core}
\begin{declarations}
\dcl{A, B, S, Ca, Cb}{principal}
\dcl{Ka, Kb}{symkey}
\dcl{Kac, Kbc}{symkey}
\dcl{Na, Nb}{nonce}
\dcl{0,1,2}{number}
\freedcl{alias Kab = \crypt{A, 0}{Kb}}
\freedcl{alias Pab = Kab + \crypt{B, 1}{Ka}}
\end{declarations}

\begin{messages}
\msg{1}{A}{S}{A, B}
\msg{2}{S}{A}{Pab, \crypt{Pab, B, 2}{Ka}}
\msg{3}{A}{Ca}{A}
\msg{4}{Ca}{A}{Na, \crypt{Na, 1, 1}{Kac}}
\msg{5}{A}{B}{A, Na}
\msg{6}{B}{Cb}{A, Na}
\msg{7}{Cb}{B}{Nb, \crypt{Nb, 0, 0}{Kab}, \crypt{Na, Nb, 1}{Kab},
  \crypt{Nb, 0, 1}{Kab}}
\msg{8}{B}{A}{Nb, \crypt{Na, Nb, 1}{Kab}}
\msg{9}{A}{Ca}{B, Na, Nb, Pab, \crypt{Pab, B, 2}{Ka},
  \crypt{Na, Nb, 1}{Kab}, \crypt{Nb, 0, 1}{Kab}}
\msg{10}{Ca}{A}{\crypt{Nb, 0, 0}{Kab}, \crypt{Nb, 0, 1}{Kab}}
\msg{11}{A}{B}{\crypt{Nb, 0, 1}{Kab}}
\end{messages}
\end{core}

\begin{explanation}
\begin{itemize}
\item the operator \code{\crypt{M}{K}} denotes DES encryption.
\item the operator \code{+} is xor.
\item the principal \code{Ca} (resp. \code{Cb} is a smart card
  connected to \code{A} (resp. \code{B}) and used to store its 
  long term keys.
\item \textbf{NB:} the connection between \code{A} and \code{Ca}
  (resp. \code{B} and \code{Cb}) is assumed to be secure
  (i.e. no intruder has the capability to listen to this connection).
\item \code{Ka} (resp. \code{Kb}) is a long term (symmetric) keys
  associated to the principal \code{A} (resp. \code{B}).
  It is assumed to be known initially only by \code{Ca}
  (resp. \code{Cb}) and the server \code{S}.
\item \code{Kac} (resp. \code{Kbc}) is a secret symmetric key
  share (and initially only known by) \code{A} and \code{Ca}
  (resp. \code{B} and \code{Cb}).
\item \code{0}, \code{1}, \code{2} are arbitrary padding constants, known to
  every principal.
\end{itemize}

\begin{itemize}
\item[\code{1,2}] \code{A} requires and obtains from the server
  \code{S} the pair key \code{Pab} associed to \code{A} and \code{B}.
  \code{\crypt{Pab, B, 2}{Ka}} is a verifier for this value.
\item[\code{3,4}] \code{A} requires and abtains a nonce \code{Na} from
  her smart card \code{Ca}. \code{\crypt{Na, 1, 1}{Kac}} is a
  verifier. In \cite{ShoupRubin96}, it is suggested to use a 8 bytes
  counter on \code{Ca} to generate \code{Na}.
\item[\code{5}] \code{A} sends the nonce, meaning she request the
  establishment of a session symmetric key.
\item[\code{6,7}] \code{B} obtains the nonce \code{Nb} from \code{Cb}
  (same remark as in \code{3,4} for the counters).
  \code{\crypt{Nb, 0, 0}{Kb}} is a session key and
  \code{\crypt{Na, Nb, 1}{Kab}}, and \code{\crypt{Nb, 0, 1}{Kab}}
  are verifiers respectively for \code{A} and \code{B}.
\item[\code{8}] \code{B} transmits the nonce \code{Nb} and \code{A}'s
  verifier to \code{A}.
\item[\code{9}] the nonce \code{Nb} and \code{A}'s verifier
  are transmitted to \code{A}.
\item[\code{10}] \code{A}'s smart card \code{Ca} makes the
  verifications, computes the session key \code{\crypt{Nb, 0, 0}{Kb}}
  and transmits it to \code{A}.
\item[\code{11}] \code{A} aknowledge to \code{B}, who can compare
  this message to his verifier remaining from message \code{7}.
\end{itemize}
\end{explanation}

\begin{property}
The session key \code{\crypt{Nb, 0, 0}{Kb}} must remain secret.
\end{property}

\begin{references}
\cite{ShoupRubin96}. Some variants and implementation issues
are discussed in the update~\cite{Shoup96update}.
See also the implementor's paper \cite{Jerdonek98}.
\end{references}

\begin{proofs}
The proof of \cite{ShoupRubin96} is
based on the probabilistic definition of secure key distribution
from Bellare and Rogaway \cite{BellareRogaway95}.

\cite{Bella00} uses a theorem proving approach, following Paulson's
inductive method.
\end{proofs}

\begin{remark}
See \cite{Shoup96update}. The nonce \code{Na} that \code{A} obtains
from his smart card \code{Ca} must actually be truly random and not
implemented by counters as first suggested in~\cite{ShoupRubin96}.

Indeed, if the next value of \code{Na} (sent in message \code{5} of
session \code{i}) is predictable 
(let us call it \code{Na'}), then then the intruder \code{I} can query \code{B} for 
the verifiers including \code{Na'} (session \code{ii}) 
and use them to answer the next challenge of \code{A} 
(hence, authentication error in session \code{iii}).
\begin{messages}
\msg{i.5}{A}{B}{A, Na}
\msg{ii.5}{I(A)}{B}{A, Na'}
\msg{ii.6}{B}{Cb}{A, Na'}
\msg{ii.7}{Cb}{B}{Nb', \crypt{Nb', 0, 0}{Kab}, \crypt{Na', Nb', 1}{Kab},
  \crypt{Nb', 0, 1}{Kab}}
\msg{ii.8}{B}{A}{Nb', \crypt{Na', Nb', 1}{Kab}}
\msg{iii.5}{A}{I(B)}{A, Na'}
\msg{iii.8}{I(B)}{A}{Nb', \crypt{Na', Nb', 1}{Kab}}
\end{messages}
According to~\cite{Shoup96update}, the nonce \code{Nb} may though be a
counter.
\end{remark}

%\begin{see} %\crossref{}, see all.aux for labels names
%\end{see}

\end{protocol}
\end{document}

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