\usepackage{beamerthemeplaincu}

%\usepackage[T1]{fontenc}

%\usepackage[latin1]{inputenc}

\newcommand{\isaliteral}[1]{}

\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}

\renewcommand{\slidecaption}{APP 07, King's College London, 19 November 2013}

  Office: & S1.27 (1st floor Strand Building)\\

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

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

  \frametitle{Security Levels}

  \small

  \begin{itemize}

  \item Top secret (\bl{$T\!S$})

  \item Secret (\bl{$S$})

  \item Public (\bl{$P$})

  \end{itemize}

  \bl{$slev(P) < slev(S) < slev(T\!S)$}\pause

  \item Bob has a clearance for ``secret''

  \item Bob can read documents that are public or sectret, but not top secret

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

%

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

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

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

%

  \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

  \item \bl{$slev($Bob$)$ $=$ $S$}

  \item \bl{$slev($File$)$ $=$ $P$}

  \item \bl{$slev(P) < slev(S)$}

%

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

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

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

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

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