% File              : ccittx509_1.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
{CCITT X.509 (1)}%
% authors
{CCITT}%
% date of the first publication
{1987}%
% editor name
{}%
% date of submission
{}%
% date of last change, empty or = date of submission
{22/11/2002}

\begin{abstract}
One message protocol from the recommendations of the CCITT for the CCITT.X.509 standard.
\end{abstract}

\begin{remark}
This protocol presented here is actually a simplified version from
\cite{BurrowsAbadiNeedham89} and \cite{abadi96prudent}.
\end{remark}

\begin{core}
\begin{declarations}
\dcl{A, B}{principal}
\dcl{Na, Nb}{nonce}
\dcl{Ta, Tb}{timestamp}
\dcl{Ya, Yb}{userdata}
\dcl{Xa, Xb}{userdata}
\dcl{PK, SK}{principal -> key (keypair)}
\end{declarations}

\begin{messages}
\msg{1}{A}{B}{A, \crypt{Ta, Na, B, Xa, \crypt{Ya}{PK(B)}}{SK(A)}}
%\msg{2}{B}{A}{B, \crypt{Tb, Nb, A, Na, Xb, \crypt{Yb}{PK(A)}}{SK(B)}}
%\msg{3}{A}{B}{A, \crypt{Nb}{SK(A)}}
\end{messages}
\end{core}

\begin{explanation}
The timestamp \code{Ta} and nonce \code{Na} are not used here.

\code{Xa} and \code{Ya} are the data transmitted,
the privacy of \code{Ya} is ensured by its encryption with 
the public key of \code{B} and the authenticity of \code{Xa} and \code{Ya}
is ensured by the encryption with the private key of \code{A}.
\end{explanation}

\begin{remark}
%As said above, this is a simplified version of the protocol of \cite{CCITT_X.509}.
As explained in \cite{BurrowsAbadiNeedham89}, 
in the original protocol specification \cite{CCITT_X.509},
only a hash of the data is signed, for efficiency reasons.
This means that the message should be specified by:
\begin{messages}
\msg{1}{A}{B}{A, Ta, Na, B, Xa, \crypt{Ya}{PK(B)}, 
   \crypt{h(Ta, Na, B, Xa, \crypt{Ya}{PK(B)})}{SK(A)}}
\end{messages}
where \code{h} is a one-way function.
\end{remark}

\begin{property}
The protocol must ensure the confidentiality of \code{Ya}: 
if \code{A} and \code{B} follow the protocol,  then an attacker should not be able to obtain \code{Ya}.

The protocol must ensure the recipient \code{B} of the message
that the data \code{Xa} and \code{Ya} originate from \code{A}.
\end{property}

\begin{references}
\cite{CCITT_X.509}, \cite{BurrowsAbadiNeedham89}.
\end{references}

\begin{attacks}
\cite{abadi96prudent}.
%with a signature.
%(the two occurences of $A$ in the message link $A$ identity to his signature).
Failure of the authenticity of \code{Xa} and \code{Ya}.
\begin{messages}
\msg{i.1}{A}{I(B)}{A, \crypt{Ta, Na, B, Xa, \crypt{Ya}{PK(B)}}{SK(A)}}
\msg{ii.1}{I}{B}{I, \crypt{Ta, Na, B, Xa, \crypt{Ya}{PK(B)}}{SK(I)}}
\end{messages}
\end{attacks}

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

\begin{addcomment}{Michael Roe}{20/11/2002}
The requirements section should include a confidentiality
property:  if \code{A} and \code{B} follow the protocol,  then an
attacker should not be able to obtain \code{Ya}.

\textit{Note of the moderator: this property has been added above,
  following the comment.}
\end{addcomment}

\begin{addcomment}{Michael Roe}{20/11/2002}
In this protocol, private keys are used for different two
  operations: digital signature and message decryption. 
  The processing done with the key is not the same in the two cases,
  and the difference can matter in protocol verification. 
  The notation ought to distinguish the two operations
\end{addcomment}

\end{protocol}
\end{document}

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