% File              : smartright_viewonly.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
{SmartRight view-only}%
% authors
{Jean-Pierre Andreaux, Sylvain Chevreau, Eric Diehl}%
% date of the first publication
{2001}%
% editor name
{Thomas Genet}%
% date of submission
{06/03/2003}%
% date of last change, empty or = date of submission
{06/03/2003}

\begin{abstract}
This \emph{view-only} protocol is part of the \ahref{http://www.smartright.org}{SmartRight}
system designed by Thomson for copy protection 
for the Digital Video Broadcasting technology.
Its purpose is to ensure that the digital content
broadcasted can be view only once.
It uses symmetric key cryptography with nonces and xor.
\end{abstract}

\begin{core}
\begin{declarations}
\dcl{CC, TC}{principal}
\dcl{VoKey, VoR, VoRi, CW}{number}
\dcl{Kc}{key}
\dcl{h}{number -> number}
\end{declarations}

\begin{messages}
\msg{1}{CC}{TC}{\crypt{VoKey, CW+VoR}{Kc}}
\msg{2}{TC}{CC}{VoRi}
\msg{3}{CC}{TC}{VoR, \crypt{h(VoRi)}{VoKey}}
\end{messages}
\end{core}

\begin{explanation}
The above presentation and these explanations
are extracted from \cite{GenetTalpinTong03}:

The protocol is deployed between two smartcards:
\code{CC} (Converter Card) and \code{TC} (Terminal Card),
respectively in an access device (i.e. a digital receiver)
receiving a scrambled digital content 
and a presentation device (i.e. a television) which is 
supposed to descramble the content before rendering it.
The keys used to scramble the content are called \emph{control words}
\code{CW}.

The cards \code{CC} and \code{TC} share a secret symmetric encryption
key \code{Kc}.

\code{CC} generates first the random values \code{VoKey} and \code{VoR},
and sends them encrypted to \code{TC} (in message \code{1}), 
together with a \code{CW} which has been received
(by the access divice) with the scrambled content.
The operator \code{+} is xor.

\code{TC} then sends in return a random challenge \code{VoRi} (message \code{2}).
The message \code{3} is the answer of \code{CC} to the challenge.
After receiving the message \code{3}, \code{TC} checks if the answer
is correct, by comparing the hashed value \code{h(VoRi)}
with its own value, and if so, it extracts \code{CW}
and uses it to descramble the content.

\paragraph{Note on memory management:}
\begin{itemize}
\item After sending the message \code{3}, 
  \code{CC} deletes \code{VoR} and \code{VoKey} from its memory.
\item After receiving and accepting the message \code{3},
  \code{TC} deletes \code{VoRi} from its memory.
\end{itemize}
This is very important (with respect to the property below)
because of the control aspects given below.

\paragraph{Note on control:} 
The principal \code{CC} and \code{TC} switch to the next state
only once they have received the next message expected
(and not once they have send a message as usual).
More precisely:
\begin{itemize}
\item After sending message \code{2}, \code{TC} will continue
  to accept a (new) message \code{1} and reply by a (new) \code{VoRi}
  (message \code{2}) until it receives the message \code{3} and
  accepts it.
\item After sending message \code{2}, \code{TC} will 
  process all the messages \code{3} it shall receive until
  it receives a new message \code{1}.
\end{itemize}
\end{explanation}

\begin{property}
cited from \cite{GenetTalpinTong03}:
The control word \code{CW} may be extracted by \code{TC} only once
at the time where the protocol is played.
\end{property}

\begin{references}
\cite{SmartRight01}, \cite{GenetTalpinTong03}.
\end{references}

\begin{proofs}
The above property is proved in \cite{GenetTalpinTong03}
in an automated way on a term rewriting model
using \ahref{http://www.irisa.fr/lande/genet/timbuk/index.html}{Timbuk}, 
a verification tool using abstract interpretation over tree automata domains.
\end{proofs}

\end{protocol}
\end{document}

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




