diff -r f1491e0d7be0 -r 0e78c809b17f slides/slides10.tex
--- a/slides/slides10.tex	Mon Dec 01 06:50:25 2014 +0000
+++ b/slides/slides10.tex	Tue Dec 02 02:29:37 2014 +0000
@@ -1,47 +1,10 @@
 \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}
+\usepackage{../slides}
+\usepackage{../langs}
+\usepackage{../graphics}
 
 % beamer stuff 
-\renewcommand{\slidecaption}{APP 09, King's College London, 10 December 2013}
-\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\renewcommand{\slidecaption}{APP 10, King's College London}
 \newcommand{\bl}[1]{\textcolor{blue}{#1}}
 
 \begin{document}
@@ -302,155 +265,6 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\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}}