\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{proof}
\usepackage{beamerthemeplaincu}
\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}
\setmonofont[Scale=MatchLowercase]{Consolas}
\newfontfamily{\consolas}{Consolas}

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

% beamer stuff 
\renewcommand{\slidecaption}{APP 09, King's College London, 10 December 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 (10)\\[-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{\mbox{}\\[20mm]\huge Revision}

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

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




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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,t]
\frametitle{\begin{tabular}{c}2nd Lecture:\\ E-Voting\end{tabular}}

\begin{itemize}
\item Integrity 
\item Ballot Secrecy
\item Voter Authentication
\item Enfranchisement
\item Availability
\end{itemize}



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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,t]
\frametitle{\begin{tabular}{c}2nd Lecture:\\ E-Voting\end{tabular}}

Online Banking vs.~E-Voting

\begin{itemize}
\item online banking: if fraud occurred you try to identify who did what (somebody's account got zero)\bigskip
\item e-voting: some parts can be done electronically, but not the actual voting (final year project: online voting)
\end{itemize}



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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\tikzset{alt/.code args={<#1>#2#3#4}{%
  \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}} % \pgfkeysalso doesn't change the path
}}

\mode<presentation>{
\begin{frame}[t]
\frametitle{\begin{tabular}{c}3rd Lecture:\\ Buffer Overflow Attacks\end{tabular}}

\begin{itemize}
\item the problem arises from the way C/C++ organises its function calls\\[-8mm]\mbox{}
\end{itemize}

\begin{center}
\begin{tikzpicture}[scale=1]
%\draw[black!10,step=2mm] (0,0) grid (9,4);
%\draw[black!10,thick,step=10mm] (0,0) grid (9,4);

\node at (0.5,4.5) {\small\begin{tabular}{l}main\\[-2mm] prog.\end{tabular}};
\draw[line width=0mm, white, alt=<2->{fill=red}{fill=blue}] (0,2.5) rectangle (1,3.8);
\draw[line width=0mm, white, alt=<9->{fill=red}{fill=blue}] (0,0.2) rectangle (1,0.5);
\draw[line width=1mm, alt=<3->{fill=yellow}{fill=blue}] (0,2.0) rectangle (1,2.5);
\draw[line width=1mm, alt=<6->{fill=red}{fill=blue}] (0,1.0) rectangle (1,2.0);
\draw[line width=1mm, alt=<7->{fill=yellow}{fill=blue}] (0,0.5) rectangle (1,1.0);
\draw[line width=1mm] (0,0) -- (0,4);
\draw[line width=1mm] (1,0) -- (1,4);

\node at (3.5,3.5) {\small\begin{tabular}{l}fact(n)\end{tabular}};
\draw[line width=1mm, alt=<{4-5,8}>{fill=red}{fill=blue}] (3,1.0) rectangle (4,3.0);

\onslide<3-4>{\draw[->, line width=1mm,red] (1,2.3) to node [above,sloped,midway] {n=4} (3,3);}
\onslide<5>{\draw[<-, line width=1mm,red] (1,2.3) to node [above,sloped,midway] {res=24} (3,1);}

\onslide<7-8>{\draw[->, line width=1mm,red] (1,0.8) to node [above,sloped,midway] {n=3} (3,3);}
\onslide<9>{\draw[<-, line width=1mm,red] (1,0.8) to node [above,sloped,midway] {res=6} (3,1);}


\node at (7.75,3.9) {\small\begin{tabular}{l}stack\end{tabular}};
\draw[line width=1mm] (7,3.5) -- (7,0.5) -- (8.5,0.5) -- (8.5,3.5);

\onslide<3,4,7,8>{
\node at (7.75, 0.8) {ret};
\draw[line width=1mm] (7,1.1) -- (8.5,1.1);
}
\onslide<3>{
\node at (7.75, 1.4) {4};
\draw[line width=1mm] (7,1.7) -- (8.5,1.7);
}
\onslide<7>{
\node at (7.75, 1.4) {3};
\draw[line width=1mm] (7,1.7) -- (8.5,1.7);
}




\end{tikzpicture}
\end{center}

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

\begin{center}
\begin{tikzpicture}[scale=1]
%\draw[black!10,step=2mm] (0,0) grid (9,4);
%\draw[black!10,thick,step=10mm] (0,0) grid (9,4);

\node at (0.5,4.5) {\small\begin{tabular}{l}main\\[-2mm] prog.\end{tabular}};
\draw[line width=0mm, white, alt=<2->{fill=red}{fill=blue}] (0,2.5) rectangle (1,3.8);
\draw[line width=1mm, white, fill=blue] (0,1.0) rectangle (1,2.0);
\draw[line width=1mm, alt=<3->{fill=yellow}{fill=blue}] (0,2.0) rectangle (1,2.5);
\draw[line width=1mm] (0,0) -- (0,4);
\draw[line width=1mm] (1,0) -- (1,4);

\node at (3.5,3.5) {\small\begin{tabular}{l}fact(n)\end{tabular}};
\draw[line width=0mm, alt=<{4-}>{red, fill=red}{blue, fill=blue}] (3,2.8) rectangle (4,3.0);
\draw[line width=0mm, alt=<{5-}>{red, fill=red}{blue, fill=blue}] (3,2.8) rectangle (4,2.0);
\draw[line width=0mm, alt=<{7-}>{red, fill=red}{blue, fill=blue}] (3,2.0) rectangle (4,1.0);
\draw[line width=1mm] (3,1.0) rectangle (4,3.0);

\onslide<3->{\draw[->, line width=1mm,red] (1,2.3) to node [above,sloped,midway] {n=4} (3,3);}
\onslide<5->{\draw[<-, line width=2mm,red] (4,2) to node [above,sloped,midway] 
{\begin{tabular}{l}user\\[-1mm] input\end{tabular}} (6,2);}
\onslide<8->{\draw[<-, line width=1mm,red] (1,-2) to (3,1);}

\node at (7.75,3.9) {\small\begin{tabular}{l}stack\end{tabular}};
\draw[line width=1mm] (7,3.5) -- (7,0.5) -- (8.5,0.5) -- (8.5,3.5);

\onslide<3->{
\draw[line width=1mm,alt=<6->{fill=red}{fill=white}] (7,0.5) rectangle (8.5,1.1);
\node at (7.75, 0.8) {\alt<6->{@a\#}{ret}};
\draw[line width=1mm,alt=<6->{fill=red}{fill=white}] (7,1.1) rectangle (8.5,1.7);
\node at (7.75, 1.4) {\alt<6->{!?w;}4};
}

\onslide<4->{
\draw[line width=1mm,fill=red] (7,1.7) rectangle (8.5,3.0);
\node[white] at (7.75, 2.4) {buffer};
}

\end{tikzpicture}
\end{center}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\begin{tabular}{c}3rd Lecture:\\ Unix Access Control\end{tabular}}

\begin{itemize}
\item privileges are specified by file access permissions (``everything is a file'') 
\end{itemize}\medskip

\begin{center}
  \begin{tikzpicture}[scale=1]
  
  \draw[line width=1mm] (-.3, 0) rectangle (1.5,2);
  \draw (4.7,1) node {Internet};
  \draw (-2.7,1.7) node {\footnotesize Application};
  \draw (0.6,1.7) node {\footnotesize Interface};
  \draw (0.6,-0.4) node {\footnotesize \begin{tabular}{c}unprivileged\\[-1mm] process\end{tabular}};
  \draw (-2.7,-0.4) node {\footnotesize \begin{tabular}{c}privileged\\[-1mm] process\end{tabular}};
  
  \draw[line width=1mm] (-1.8, 0) rectangle (-3.6,2);

  \draw[white] (1.7,1) node (X) {};
  \draw[white] (3.7,1) node (Y) {};
  \draw[red, <->, line width = 2mm] (X) -- (Y);
 
  \draw[red, <->, line width = 1mm] (-0.6,1) -- (-1.6,1);
  \end{tikzpicture}
\end{center}

\begin{itemize}
\item the idea is make the attack surface smaller and 
mitigate the consequences of an attack
\end{itemize}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,t]
\frametitle{\begin{tabular}{c}3rd Lecture:\\ Unix Access Control\end{tabular}}

\begin{itemize}
\item when a file with setuid is executed, the resulting process will assume the 
UID given to the owner of the file
\end{itemize}

\small\tt
\begin{center}
\begin{verbatim}
$ ls -ld . * */*
drwxr-xr-x 1 ping staff  32768 Apr  2 2010 .
-rw----r-- 1 ping students  31359 Jul 24 2011 manual.txt
-r--rw--w- 1 bob students   4359 Jul 24 2011 report.txt
-rwsr--r-x 1 bob students 141359 Jun  1 2013 microedit
dr--r-xr-x 1 bob staff  32768 Jul 23 2011 src
-rw-r--r-- 1 bob staff  81359 Feb 28 2012 src/code.c
-r--rw---- 1 emma students    959 Jan 23 2012 src/code.h
\end{verbatim}
\end{center}


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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,t]
\frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}}

Bell-LaPadula access model:

 \begin{itemize}
  \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if
  \bl{$P$}'s security level is at least as high as \bl{$O$}'s.
  \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if
  \bl{$O$}'s security level is at least as high as \bl{$P$}'s.\medskip

  \item Meta-Rule: All principals in a system should have a sufficiently high security level
  in order to access an object.
  \end{itemize}\bigskip

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,t]
\frametitle{\begin{tabular}{c}4th Lecture:\\ Security Levels\end{tabular}}

Biba (data integrity)

  \begin{itemize}
  \item Biba: {\bf `no read down'} - {\bf `no write up'}
  \item \alert{Read Rule}: A principal \bl{$P$} can read an object \bl{$O$} if and only if
  \bl{$P$}'s security level is lower or equal than \bl{$O$}'s.
  \item \alert{Write Rule}: A principal \bl{$P$} can write an object \bl{$O$} if and only if
  \bl{$O$}'s security level is lower or equal than \bl{$P$}'s.
  \end{itemize}

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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,t]
\frametitle{\begin{tabular}{c}4th Lecture:\\ Protocols\end{tabular}}

A mutual authentication protocol

\begin{center}
\begin{tabular}{ll}
\bl{$A \rightarrow B$:} & \bl{$N_a$}\\  
\bl{$B \rightarrow A$:} & \bl{$\{N_a, N_b\}_{K_{ab}}$}\\
\bl{$A \rightarrow B$:} & \bl{$N_b$}\\
\end{tabular}
\end{center}


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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,t]
\frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}}


\begin{itemize}
\item formulas
\item judgements
\end{itemize}\pause

\begin{center}
  \begin{tikzpicture}[scale=1]
  
  \draw[line width=1mm] (-.3, 0) 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}granted/\\not granted\end{tabular}};
  \draw (0.6,1.2) node {\footnotesize \begin{tabular}{l}Access\\Control\\Checker\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 (\bl{$\Gamma$})\end{tabular}};

  \end{tikzpicture}
\end{center}


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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,t]
\frametitle{\begin{tabular}{c}5th Lecture:\\ Access Control Logic\end{tabular}}

\begin{center}
\begin{tikzpicture}[scale=1]
  
  \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};
  \onslide<1->{
  \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}


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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\begin{tabular}{c}5th Lecture:\\ Inference Rules\end{tabular}}


\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{\begin{tabular}{c}6th Lecture:\\ Privacy\end{tabular}}




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



\end{document}

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

