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

\begin{itemize}

\item hashes and salts to guaranty data integrity\bigskip

\item storing passwords (brute force attacks and dictionary attacks)

\end{itemize}

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

\begin{itemize}

\item differential privacy for annonymizing research data

\begin{center}

User\;\;\;\;    

\begin{tabular}{c}

tell me \bl{$f(x)$} $\Rightarrow$\\

$\Leftarrow$ \bl{$f(x) + \text{noise}$}

\end{tabular}

\;\;\;\;\begin{tabular}{@{}c}

Database\\

\bl{$x_1, \ldots, x_n$}

\end{tabular}

\end{center}

\item \bl{$f(x)$} can be released, if \bl{$f$} is insensitive to

individual entries  \bl{$x_1, \ldots, x_n$}\\

\item The intuition: whatever is learned from the dataset would be learned regardless of whether

\bl{$x_i$} participates\bigskip\pause

\item Tor webservice

\end{itemize}

\end{frame}}

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

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

\mode<presentation>{

\begin{frame}[c]

\frametitle{\begin{tabular}{c}9th Lecture:\\ Privacy\end{tabular}}

\begin{itemize}

\item zero-knowledge proofs

\item requires NP problems, for example graph isomorphisms\bigskip\pause

\item random number generators

\end{itemize}

\end{frame}}

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