\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{proof}
\usepackage{beamerthemeplaincu}
%\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}
\usetikzlibrary{plotmarks}
\isabellestyle{rm}
\renewcommand{\isastyle}{\rm}%
\renewcommand{\isastyleminor}{\rm}%
\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
\renewcommand{\isatagproof}{}
\renewcommand{\endisatagproof}{}
\renewcommand{\isamarkupcmt}[1]{#1}
\newcommand{\isaliteral}[1]{}
\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#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, 19 November 2013}
\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\\
Office: & S1.27 (1st floor Strand Building)\\
Slides: & KEATS (also homework is there)\\
\end{tabular}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
Recall the following scenario:
\begin{itemize}
\item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file}}
should be deleted, then this file must be deleted.
\item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether
\textcolor{blue}{\isa{file}} should be deleted (delegation).
\item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file}}.
\end{itemize}\bigskip
\small
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
\isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\
\isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
\isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\
\end{tabular}}\medskip
\textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\begin{tabular}{@ {\hspace{-2mm}}c@ {}}The Access Control Problem\end{tabular}}
\begin{center}
\begin{tikzpicture}[scale=1]
\draw[line width=1mm] (-.3, -0.5) rectangle (1.5,2);
\draw (-2.7,1) node {\begin{tabular}{l}access\\request\\ (\bl{$F$})\end{tabular}};
\draw (4.2,1) node {\begin{tabular}{l}provable/\\not provable\end{tabular}};
\draw (0.6,0.8) node {\footnotesize \begin{tabular}{l}AC-\\ Checker:\\ applies\\ inference\\ rules\end{tabular}};
\draw[red, ->, line width = 2mm] (1.7,1) -- (2.7,1);
\draw[red,<-, line width = 2mm] (-0.6,1) -- (-1.6,1);
\draw[red, <-, line width = 3mm] (0.6,2.2) -- (0.6,3.2);
\draw (0.6,4) node {\begin{tabular}{l}\large Access Policy (\boldmath\bl{$\Gamma$})\end{tabular}};
\end{tikzpicture}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\begin{itemize}
\item \bl{$P \,\text{says}\, F$} means \bl{$P$} can send a ``signal'' \bl{$F$} through a wire, or
can make a ``statement'' \bl{$F$}\bigskip\pause
\item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\
\bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip
\begin{center}
\bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Security Levels}
\small
\begin{itemize}
\item Top secret (\bl{$T\!S$})
\item Secret (\bl{$S$})
\item Public (\bl{$P$})
\end{itemize}
\begin{center}
\bl{$slev(P) < slev(S) < slev(T\!S)$}\pause
\end{center}
\begin{itemize}
\item Bob has a clearance for ``secret''
\item Bob can read documents that are public or sectret, but not top secret
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Reading a File}
\bl{\begin{center}
\begin{tabular}{c}
\begin{tabular}{@ {}l@ {}}
\only<2->{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$}}\\
\only<2->{\hspace{3cm}}Bob controls Permitted $($File, read$)$\\
Bob says Permitted $($File, read$)$\only<2->{\\}
\only<2>{\textcolor{red}{$slev($File$)$ $<$ $slev($Bob$)$}}%
\only<3>{\textcolor{red}{$slev($File$)$ $=$ $P$}\\}%
\only<3>{\textcolor{red}{$slev($Bob$)$ $=$ $S$}\\}%
\only<3>{\textcolor{red}{$slev(P)$ $<$ $slev(S)$}\\}%
\end{tabular}\\
\hline
Permitted $($File, read$)$
\end{tabular}
\end{center}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Substitution Rule}
\small
\bl{\begin{center}
\begin{tabular}{c}
$\Gamma \vdash slev(P) = l_1$ \hspace{4mm} $\Gamma \vdash slev(Q) = l_2$
\hspace{4mm} $\Gamma \vdash l_1 < l_2$\\\hline
$\Gamma \vdash slev(P) < slev(Q)$
\end{tabular}
\end{center}}\bigskip\pause
\begin{itemize}
\item \bl{$slev($Bob$)$ $=$ $S$}
\item \bl{$slev($File$)$ $=$ $P$}
\item \bl{$slev(P) < slev(S)$}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Reading a File}
\bl{\begin{center}
\begin{tabular}{c}
\begin{tabular}{@ {}l@ {}}
$slev($File$)$ $<$ $slev($Bob$)$ $\Rightarrow$\\
\hspace{3cm}Bob controls Permitted $($File, read$)$\\
Bob says Permitted $($File, read$)$\\
$slev($File$)$ $=$ $P$\\
$slev($Bob$)$ $=$ $T\!S$\\
\only<1>{\textcolor{red}{$?$}}%
\only<2>{\textcolor{red}{$slev(P) < slev(S)$}\\}%
\only<2>{\textcolor{red}{$slev(S) < slev(T\!S)$}}%
\end{tabular}\\
\hline
Permitted $($File, read$)$
\end{tabular}
\end{center}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Transitivity Rule}
\small
\bl{\begin{center}
\begin{tabular}{c}
$\Gamma \vdash l_1 < l_2$
\hspace{4mm} $\Gamma \vdash l_2 < l_3$\\\hline
$\Gamma \vdash l_1 < l_3$
\end{tabular}
\end{center}}\bigskip
\begin{itemize}
\item \bl{$slev(P) < slev (S)$}
\item \bl{$slev(S) < slev (T\!S)$}
\item[] \bl{$slev(P) < slev (T\!S)$}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Reading Files}
\begin{itemize}
\item Access policy for Bob for reading
\end{itemize}
\bl{\begin{center}
\begin{tabular}{c}
\begin{tabular}{@ {}l@ {}}
$\forall f.\;slev(f)$ \only<1>{$<$}\only<2>{\textcolor{red}{$\le$}} $slev($Bob$)$ $\Rightarrow$\\
\hspace{3cm}Bob controls Permitted $(f$, read$)$\\
Bob says Permitted $($File, read$)$\\
$slev($File$)$ $=$ \only<1>{$P$}\only<2>{\textcolor{red}{$T\!S$}}\\
$slev($Bob$)$ $=$ $T\!S$\\
$slev(P) < slev(S)$\\
$slev(S) < slev(T\!S)$
\end{tabular}\\
\hline
Permitted $($File, read$)$
\end{tabular}
\end{center}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Writing Files}
\begin{itemize}
\item Access policy for Bob for {\bf writing}
\end{itemize}
\bl{\begin{center}
\begin{tabular}{c}
\begin{tabular}{@ {}l@ {}}
$\forall f.\;slev($Bob$)$ $\le$ $slev(f)$ $\Rightarrow$\\
\hspace{3cm}Bob controls Permitted $(f$, write$)$\\
Bob says Permitted $($File, write$)$\\
$slev($File$)$ $=$ $T\!S$\\
$slev($Bob$)$ $=$ $S$\\
$slev(P) < slev(S)$\\
$slev(S) < slev(T\!S)$
\end{tabular}\\
\hline
Permitted $($File, write$)$
\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}
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{Sending Rule}
\bl{\begin{center}
\mbox{$\infer{\Gamma \vdash Q \;\text{says}\; F}
{\Gamma \vdash P \;\text{says}\; F & \Gamma \vdash P \;\text{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$ : $\text{Connect}(A,B)$\\
\bl{$S \,\text{says}\, (\text{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{Public/Private Keys}
\begin{itemize}
\item Bob has a private and public key: \bl{$K_{Bob}^{pub}$}, \bl{$K_{Bob}^{priv}$}\bigskip
\begin{center}
\bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_{K_{Bob}^{pub}} &
\Gamma \vdash K_{Bob}^{priv}}}}
\end{center}\bigskip\pause
\item this is {\bf not} a derived rule!
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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$}, it starts engine
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Challenge-Response Protocol}
\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}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Exchange of a Fresh Key}
\bl{$A$} and \bl{$B$} share a (``super-secret'') key \bl{$K_{AB}$} and want to share another key
\begin{itemize}
\item assumption \bl{$K_{AB}$} is only known to \bl{$A$} and \bl{$B$}\bigskip
\item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$}
\item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$}
\item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$}
\item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}
\item<2> \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}
\end{itemize}\bigskip
Assume \bl{$K^{new}_{AB}$} is compromised by \bl{$I$}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{The Attack}
An intruder \bl{$I$} convinces \bl{$A$} to accept the compromised key \bl{$K^{new}_{AB}$}\medskip
\begin{minipage}{1.1\textwidth}
\begin{itemize}
\item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$}
\item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$}
\item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$}
\item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\;\;recorded by \bl{$I$}\pause
\item \bl{$A \,\text{sends}\, B : A, \{M_A\}_{K_{AB}}$}
\item \bl{$B\,\text{sends}\, A : \{M_A + 1, M_B\}_{K_{AB}}$}
\item \bl{$A \,\text{sends}\, B : \{M_B + 1\}_{K_{AB}}$}
\item \bl{$B \,\text{sends}\, I : \{K^{newer}_{AB}, N^{newer}_B\}_{K_{AB}}$}\;intercepted by \bl{$I$}
\item \bl{$I \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\pause
\item \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}\;\;\;\;\bl{$I$} can read it also
\end{itemize}
\end{minipage}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
A Man-in-the-middle attack in real life:
\begin{itemize}
\item the card only says yes or no to the terminal if the PIN is correct
\item trick the card in thinking transaction is verified by signature
\item trick the terminal in thinking the transaction was verified by PIN
\end{itemize}
\begin{minipage}{1.1\textwidth}
\begin{center}
\mbox{}\hspace{-6mm}\includegraphics[scale=0.5]{pics/chip-attack.png}
\includegraphics[scale=0.3]{pics/chipnpinflaw.png}
\end{center}
\end{minipage}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Problems with EMV}
\begin{itemize}
\item it is a wrapper for many protocols
\item specification by consensus (resulted unmanageable complexity)
\item its specification is 700 pages in English plus 2000+ pages for testing, additionally some
further parts are secret
\item other attacks have been found
\item one solution might be to require always online verification of the PIN with the bank
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\begin{tabular}{c}Problems with WEP (Wifi)\end{tabular}}
\begin{itemize}
\item a standard ratified in 1999
\item the protocol was designed by a committee not including cryptographers
\item it used the RC4 encryption algorithm which is a stream cipher requiring a unique nonce
\item WEP did not allocate enough bits for the nonce
\item for authenticating packets it used CRC checksum which can be easily broken
\item the network password was used to directly encrypt packages (instead of a key negotiation protocol)\bigskip
\item encryption was turned off by default
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Protocols are Difficult}
\begin{itemize}
\item even the systems designed by experts regularly fail\medskip
\item try to make everything explicit (you need to authenticate all data you might rely on)\medskip
\item the one who can fix a system should also be liable for the losses\medskip
\item cryptography is often not {\bf the} answer\bigskip\bigskip
\end{itemize}
logic is one way protocols are studied in academia
(you can use computers to search for attacks)
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Public-Key Infrastructure}
\begin{itemize}
\item the idea is to have a certificate authority (CA)
\item you go to the CA to identify yourself
\item CA: ``I, the CA, have verified that public key \bl{$P^{pub}_{Bob}$} belongs to Bob''\bigskip
\item CA must be trusted by everybody
\item What happens if CA issues a false certificate? Who pays in case of loss? (VeriSign
explicitly limits liability to \$100.)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: