<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">% File              : andrewBAN.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
{Andrew Secure RPC}%
% authors
{M. Satyanarayanan}%
% date of the first publication
{1987}%
% editor name
{}%
% date of submission
{}%
% date of last change, empty or = date of submission
{14/11/2011}


\begin{abstract}
Exchanged of a fresh shared key.
Symmetric key cryptography.
\end{abstract}

\begin{core}
\begin{declarations}
\dcl{A, B}{principal}
\dcl{Kab, K'ab}{symkey}
\dcl{Na, Nb, N'b}{nonce}
\dcl{succ}{nonce -&gt; nonce}
\end{declarations}

\begin{messages}
\msg{1}{A}{B}{A, \crypt{Na}{Kab}}
\msg{2}{B}{A}{\crypt{succ{Na}, Nb}{Kab}}
\msg{3}{A}{B}{\crypt{succ{Nb}}{Kab}}
\msg{4}{B}{A}{\crypt{K'ab, N'b}{Kab}}
\end{messages}
\end{core}

\begin{explanation}
This protocol establishes the fresh
shared symmetric key \code{K'ab}.
The nonce \code{N'b} is sent in message \code{4}
to be used in a future session.

We assume that initially, the symmetric keys \code{Kab}
is known only to \code{A} and \code{B}.
\end{explanation}

\begin{property}
The protocol must guaranty the secrecy of the new shared key
\code{K'ab}:
in every session, the value of \code{K'ab} must be known only by
the participants playing the roles of \code{A} and \code{B}.

The protocol must guaranty the authenticity of \code{K'ab}:
in every session, on reception of message \code{4},
\code{A} must be ensured that the key \code{K'ab} in the message
has been created by \code{A} in the same session.
\end{property}

\begin{references}
\cite{Andrew}
\end{references}

\begin{attacks}
\cite{BurrowsAbadiNeedham89}.
The message \code{4} contains nothing that 
\code{A} knows to be fresh. Hence, an intruder \code{I}
can replay this message in another session of the protocol
to convinced \code{B} to accept an old compromised key.
\begin{messages}
\msg{i.1}{A}{B}{A, \crypt{Na}{Kab}}
\msg{i.2}{B}{A}{\crypt{succ{Na}, Nb}{Kab}}
\msg{i.3}{A}{B}{\crypt{succ{Nb}}{Kab}}
\msg{i.4}{B}{A}{\crypt{K'ab, N'b}{Kab}}
\msg{ii.1}{A}{B}{A, \crypt{Ma}{Kab}}
\msg{ii.2}{B}{A}{\crypt{succ{Ma}, Mb}{Kab}}
\msg{ii.3}{A}{B}{\crypt{succ{Mb}}{Kab}}
\msg{ii.4}{B}{I(A)}{\crypt{K''ab, M'b}{Kab}}
\msg{ii.4}{I(B)}{A}{\crypt{K'ab, N'b}{Kab}}
\end{messages}
\end{attacks}

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

\end{protocol}
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
</pre></body></html>