\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} 

\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}

\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: