\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{proof}
\usepackage{beamerthemeplainculight}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{mathpartir}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage[absolute,overlay]{textpos}
\usepackage{ifthen}
\usepackage{tikz}
\usepackage{courier}
\usepackage{listings}
\usetikzlibrary{arrows}
\usetikzlibrary{positioning}
\usetikzlibrary{calc}
\usepackage{graphicx} 
\usetikzlibrary{shapes}
\usetikzlibrary{shadows}

\isabellestyle{rm}
\renewcommand{\isastyle}{\rm}%
\renewcommand{\isastyleminor}{\rm}%
\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
\renewcommand{\isatagproof}{}
\renewcommand{\endisatagproof}{}
\renewcommand{\isamarkupcmt}[1]{#1}

% Isabelle characters
\renewcommand{\isacharunderscore}{\_}
\renewcommand{\isacharbar}{\isamath{\mid}}
\renewcommand{\isasymiota}{}
\renewcommand{\isacharbraceleft}{\{}
\renewcommand{\isacharbraceright}{\}}
\renewcommand{\isacharless}{$\langle$}
\renewcommand{\isachargreater}{$\rangle$}
\renewcommand{\isasymsharp}{\isamath{\#}}
\renewcommand{\isasymdots}{\isamath{...}}
\renewcommand{\isasymbullet}{\act}



\definecolor{javared}{rgb}{0.6,0,0} % for strings
\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments
\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords
\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc

\lstset{language=Java,
	basicstyle=\ttfamily,
	keywordstyle=\color{javapurple}\bfseries,
	stringstyle=\color{javagreen},
	commentstyle=\color{javagreen},
	morecomment=[s][\color{javadocblue}]{/**}{*/},
	numbers=left,
	numberstyle=\tiny\color{black},
	stepnumber=1,
	numbersep=10pt,
	tabsize=2,
	showspaces=false,
	showstringspaces=false}

\lstdefinelanguage{scala}{
  morekeywords={abstract,case,catch,class,def,%
    do,else,extends,false,final,finally,%
    for,if,implicit,import,match,mixin,%
    new,null,object,override,package,%
    private,protected,requires,return,sealed,%
    super,this,throw,trait,true,try,%
    type,val,var,while,with,yield},
  otherkeywords={=>,<-,<\%,<:,>:,\#,@},
  sensitive=true,
  morecomment=[l]{//},
  morecomment=[n]{/*}{*/},
  morestring=[b]",
  morestring=[b]',
  morestring=[b]"""
}

\lstset{language=Scala,
	basicstyle=\ttfamily,
	keywordstyle=\color{javapurple}\bfseries,
	stringstyle=\color{javagreen},
	commentstyle=\color{javagreen},
	morecomment=[s][\color{javadocblue}]{/**}{*/},
	numbers=left,
	numberstyle=\tiny\color{black},
	stepnumber=1,
	numbersep=10pt,
	tabsize=2,
	showspaces=false,
	showstringspaces=false}

% beamer stuff 
\renewcommand{\slidecaption}{APP 07, King's College London, 13 November 2012}
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[t]
\frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\
  \LARGE Access Control and \\[-3mm] 
  \LARGE Privacy Policies (7)\\[-6mm] 
  \end{tabular}}\bigskip\bigskip\bigskip

  %\begin{center}
  %\includegraphics[scale=1.3]{pics/barrier.jpg}
  %\end{center}

\normalsize
  \begin{center}
  \begin{tabular}{ll}
  Email:  & christian.urban at kcl.ac.uk\\
  Of$\!$fice: & S1.27 (1st floor Strand Building)\\
  Slides: & KEATS (also homework is there)\\
  \end{tabular}
  \end{center}


\end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Judgements}

\begin{center}
\begin{tikzpicture}[scale=1]
  
  \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};
  \onslide<2->{
  \draw (-1,-0.3) node (X) {};
  \draw (-2.0,-2.0) node (Y) {};
  \draw (0.7,-3) node {\begin{tabular}{l}Gamma\\stands for a collection of formulas\\(``assumptions'')\end{tabular}};
  \draw[red, ->, line width = 2mm] (Y) -- (X);
 
  \draw (1.2,-0.1) node (X1) {};
  \draw (2.8,-0.1) node (Y1) {};
  \draw (4.5,-0.1) node {\begin{tabular}{l}a single formula\end{tabular}};
  \draw[red, ->, line width = 2mm] (Y1) -- (X1);

  \draw (-0.1,0.1) node (X2) {};
  \draw (0.5,1.5) node (Y2) {};
  \draw (1,1.8) node {\begin{tabular}{l}entails sign\end{tabular}};
  \draw[red, ->, line width = 2mm] (Y2) -- (X2);}
  
  \end{tikzpicture}
\end{center}

\pause\pause
\footnotesize Gimel (Phoenician), Gamma (Greek), C and G (Latin), Gim (Arabic),\\[-2mm] ?? (Indian), Ge (Cyrillic) 
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Inference Rules}

\begin{center}
\begin{tikzpicture}[scale=1]
  
  \draw (0.0,0.0) node 
  {\Large\bl{\infer{\Gamma \vdash F_1 \wedge F_2}{\Gamma \vdash F_1 & \Gamma \vdash F_2}}};
 
  \draw (-0.1,-0.7) node (X) {};
  \draw (-0.1,-1.9) node (Y) {};
  \draw (-0.2,-2) node {\begin{tabular}{l}conclusion\end{tabular}};
  \draw[red, ->, line width = 2mm] (Y) -- (X);
 
  \draw (-1,0.6) node (X2) {};
  \draw (0.0,1.6) node (Y2) {};
  \draw (0,1.8) node {\begin{tabular}{l}premisses\end{tabular}};
  \draw[red, ->, line width = 2mm] (Y2) -- (X2);
   \draw (1,0.6) node (X3) {};
  \draw (0.0,1.6) node (Y3) {};
  \draw[red, ->, line width = 2mm] (Y3) -- (X3);
  \end{tikzpicture}
\end{center}

\only<2>{
\begin{textblock}{11}(1,13)
\small
\bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $}
\end{textblock}}
\only<3>{
\begin{textblock}{11}(1,13)
\small
\bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge
        \underbrace{P \,\text{says}\, G}_{F_2} $}
\end{textblock}}

\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]

\begin{center}
\Large
\bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1\Rightarrow F_2 & \Gamma \vdash F_1}}\bigskip\bigskip\bigskip

\bl{\infer{\Gamma\vdash P\,\text{says}\, F}{\Gamma \vdash F}}
\end{center}

\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Digression: Proofs in CS}

Formal proofs in CS sound like science fiction?\pause{} Completely irrelevant!\pause

\begin{itemize}
\item in 2008, verification of a small C-compiler\medskip 
\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
\begin{itemize}
\item 200k loc of proof
\item 25 - 30 person years
\item found 160 bugs in the C code (144 by the proof)
\end{itemize}
\end{itemize}

\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{}

  \begin{tabular}{c@ {\hspace{2mm}}c}
  \\[6mm]
  \begin{tabular}{c}
  \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
  {\footnotesize Bob Harper}\\[-2.5mm]
  {\footnotesize (CMU)}
  \end{tabular}
  \begin{tabular}{c}
  \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
  {\footnotesize Frank Pfenning}\\[-2.5mm]
  {\footnotesize (CMU)}
  \end{tabular} &

  \begin{tabular}{p{6cm}}
  \raggedright
  \color{gray}{published a proof about a specification in a journal (2005),
  $\sim$31pages}
  \end{tabular}\\

  \pause
  \\[0mm]
  
  \begin{tabular}{c}
  \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 
  {\footnotesize Andrew Appel}\\[-2.5mm]
  {\footnotesize (Princeton)}
  \end{tabular} &

  \begin{tabular}{p{6cm}}
  \raggedright
  \color{gray}{relied on their proof in a\\ {\bf security} critical application}
  \end{tabular}
  \end{tabular}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{Proof-Carrying Code}

  \begin{textblock}{10}(2.5,2.2)
  \begin{block}{Idea:}
  \begin{center}
  \begin{tikzpicture}
  \draw[help lines,cream] (0,0.2) grid (8,4);
  
  \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
  \node[anchor=base] at (6.5,2.8) 
     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user: untrusted code\end{tabular}};

  \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);
  \node[anchor=base] at (1.5,2.3) 
     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  developer ---\\ web server\end{tabular}};
  
  \onslide<3->{
  \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
  \node[anchor=base,white] at (6.5,1.1) 
     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}

  \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};
  \onslide<2->{
  \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf certificate};
  \node at (3.8,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof}};
  }

  
  \end{tikzpicture}
  \end{center}
  \end{block}
  \end{textblock}

  %\begin{textblock}{15}(2,12)
  %\small
  %\begin{itemize}
  %\item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 
  %803 loc in C including 2 library functions)\\[-3mm]
  %\item<5-> 167 loc in C implement a type-checker
  %\end{itemize}
  %\end{textblock}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

 \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 
                     draw=black!50, top color=white, bottom color=black!20]
  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
                     draw=red!70, top color=white, bottom color=red!50!black!20]
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<2->[squeeze]
  \frametitle{} 
  
  \begin{columns}
  
  \begin{column}{0.8\textwidth}
  \begin{textblock}{0}(1,2)

  \begin{tikzpicture}
  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
  { \&[-10mm] 
    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
    \node (proof1) [node1] {\large Proof}; \&
    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
    
    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&
    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
     
    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
  };

  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
  
  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
  
  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

  \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 
  \end{tikzpicture}

  \end{textblock}
  \end{column}
  \end{columns}


  \begin{textblock}{3}(12,3.6)
  \onslide<4->{
  \begin{tikzpicture}
  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
  \end{tikzpicture}}
  \end{textblock}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
     
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Mars Pathfinder Mission 1997}

  \begin{center}
  \includegraphics[scale=0.15]{marspath1.png}
  \includegraphics[scale=0.16]{marspath3.png}
  \includegraphics[scale=0.3]{marsrover.png}
  \end{center}
  
  \begin{itemize}
  \item despite NASA's famous testing procedure, the lander crashed frequently on Mars
  \item problem was an algorithm not used in the OS
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Trusted Third Party}

Simple protocol for establishing a secure connection via a mutually
trusted 3rd party (server):

\begin{center}
\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}
Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\
Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\
Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\
Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\
\end{tabular}
\end{center}

\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Encrypted Messages}

  \begin{itemize}
  \item Alice sends a message \bl{$m$}
  \begin{center}
  \bl{Alice says $m$}
  \end{center}\medskip\pause

  \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$})
  \begin{center}
  \bl{Alice says $\{m\}_K$}
  \end{center}\medskip\pause

  \item Decryption of Alice's message\smallskip
  \begin{center}
  \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
              {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
  \end{center}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
  
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Encryption}

  \begin{itemize}
  \item Encryption of a message\smallskip
  \begin{center}
  \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K}
              {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
  \end{center}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
  
    
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Trusted Third Party}

  \begin{itemize}
  \item Alice calls Sam for a key to communicate with Bob
  \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared)
  \item Alice sends the message encrypted with the key and the second key it recieved
  \end{itemize}\bigskip

  \begin{center}
  \bl{\begin{tabular}{lcl}
  $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\
  $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
  $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\
  $A$ sends $B$ &:& $\{m\}_{K_{AB}}$
  \end{tabular}}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
  
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Sending Rule}

  \bl{\begin{center}
  \mbox{\infer{\Gamma \vdash Q \;\textit{says}\; F}
              {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{sends}\; Q : F}}
  \end{center}}\bigskip\pause
  
  \bl{$P \,\text{sends}\, Q : F \dn$}\\
  \hspace{6mm}\bl{$(P \,\text{says}\, F) \Rightarrow (Q \,\text{says}\, F)$}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Trusted Third Party}

  \begin{center}
  \bl{\begin{tabular}{l}
  $A$ sends $S$ : $\textit{Connect}(A,B)$\\  
  \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\ 
  \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge 
  \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
 $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
  $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
  $A$ sends $B$ : $\{m\}_{K_{AB}}$
  \end{tabular}}
  \end{center}\bigskip\pause
  
  
  \bl{$\Gamma \vdash B \,\text{says} \, m$}?
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
  
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Challenge-Response Protocol}

 \begin{itemize}
 \item an engine \bl{$E$} and a transponder \bl{$T$} share a key \bl{$K$}\bigskip
 \item \bl{$E$} sends out a \alert{nonce} \bl{$N$} (random number) to \bl{$T$}\bigskip
 \item \bl{$T$} responds with \bl{$\{N\}_K$}\bigskip
 \item if \bl{$E$} receives  \bl{$\{N\}_K$} from \bl{$T$} then starts engine
 \end{itemize}	
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Challenge-Response Protokol}

  \begin{center}
  \bl{\begin{tabular}{l}
  $E \;\text{says}\; N$\hfill(start)\\
  $E \;\text{sends}\; T : N$\hfill(challenge)\\
  $(T \;\text{says}\; N) \Rightarrow (T \;\text{sends}\; E : \{N\}_K \wedge$\\
  \hspace{3.5cm} $T \;\text{sends}\; E : \text{Id}(T))$\;\;\;\hfill(response)\\
 $T \;\text{says}\; K$\hfill(key)\\
 $T \;\text{says}\; \text{Id}(T)$\hfill(identity)\\
  $(E \;\text{says}\; \{N\}_K \wedge E \;\text{says}\; \text{Id}(T)) \Rightarrow$\\
   \hspace{5cm}$ \text{start\_engine}(T)$\hfill(engine)\\
  \end{tabular}}
  \end{center}\bigskip 
  
  \bl{$\Gamma \vdash \text{start\_engine}(T)$}?
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
     
\end{document}

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