\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: & N7.07 (North Wing, Bush House)\\

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

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%