
diff -r be35ff24cccc -r d1d07f05325a slides/slides07.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/slides07.tex	Sun Sep 22 15:22:11 2013 +0100
@@ -0,0 +1,976 @@
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{proof}
+\usepackage{beamerthemeplainculight}
+\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}
+
+% 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, 13 November 2012}
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+
+
+% The data files, written on the first run.
+\begin{filecontents}{re-python.data}
+1 0.029
+5 0.029
+10 0.029
+15 0.032
+16 0.042
+17 0.042
+18 0.055
+19 0.084
+20 0.136
+21 0.248
+22 0.464
+23 0.899
+24 1.773
+25 3.505
+26 6.993
+27 14.503
+28 29.307
+#29 58.886
+\end{filecontents}
+
+\begin{filecontents}{re1.data}
+1 0.00179
+2 0.00011
+3 0.00014
+4 0.00026
+5 0.00050
+6 0.00095
+7 0.00190
+8 0.00287
+9 0.00779
+10 0.01399
+11 0.01894
+12 0.03666
+13 0.07994
+14 0.08944
+15 0.02377
+16 0.07392
+17 0.22798
+18 0.65310
+19 2.11360
+20 6.31606
+21 21.46013
+\end{filecontents}
+
+\begin{filecontents}{re2.data}
+1  0.00240
+2  0.00013
+3  0.00020
+4  0.00030
+5  0.00049
+6  0.00083
+7  0.00146
+8  0.00228
+9  0.00351
+10  0.00640
+11  0.01217
+12  0.02565
+13  0.01382
+14  0.02423
+15  0.05065 
+16  0.06522
+17  0.02140
+18  0.05176
+19  0.18254
+20  0.51898
+21  1.39631
+22  2.69501
+23  8.07952
+\end{filecontents}
+
+\begin{filecontents}{re-internal.data}
+1 0.00069
+301 0.00700
+601 0.00297
+901 0.00470
+1201 0.01301
+1501 0.01175
+1801 0.01761
+2101 0.01787
+2401 0.02717
+2701 0.03932
+3001 0.03470
+3301 0.04349
+3601 0.05411
+3901 0.06181
+4201 0.07119
+4501 0.08578
+\end{filecontents}
+
+\begin{filecontents}{re3.data}
+1 0.001605
+501 0.131066
+1001 0.057885
+1501 0.136875
+2001 0.176238
+2501 0.254363
+3001 0.37262
+3501 0.500946
+4001 0.638384
+4501 0.816605
+5001 1.00491
+5501 1.232505
+6001 1.525672
+6501 1.757502
+7001 2.092784
+7501 2.429224
+8001 2.803037
+8501 3.463045
+9001 3.609
+9501 4.081504
+10001 4.54569
+\end{filecontents}
+
+
+\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\\
+  Of$\!$fice: & S1.27 (1st floor Strand Building)\\
+  Slides: & KEATS (also homework is there)\\
+  \end{tabular}
+  \end{center}
+
+
+\end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Judgements}
+
+\begin{center}
+\begin{tikzpicture}[scale=1]
+  
+  \draw (0.0,0.0) node {\LARGE \bl{$\Gamma \vdash F$}};
+  \onslide<2->{
+  \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}
+
+\pause\pause
+\footnotesize Gimel (Phoenician), Gamma (Greek), C and G (Latin), Gim (Arabic),\\[-2mm] ?? (Indian), Ge (Cyrillic) 
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Inference Rules}
+
+\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}
+
+\only<2>{
+\begin{textblock}{11}(1,13)
+\small
+\bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $}
+\end{textblock}}
+\only<3>{
+\begin{textblock}{11}(1,13)
+\small
+\bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge
+        \underbrace{P \,\text{says}\, G}_{F_2} $}
+\end{textblock}}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1\Rightarrow F_2 & \Gamma \vdash F_1}}\bigskip\bigskip\bigskip
+
+\bl{\infer{\Gamma\vdash P\,\text{says}\, F}{\Gamma \vdash F}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[t]
+
+We want to prove
+
+\begin{center}
+\bl{$\Gamma \vdash \text{del\_file}$}
+\end{center}\pause
+
+There is an inference rule
+
+\begin{center}
+\bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}}
+\end{center}\pause
+
+So we can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause
+
+\bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\
+So we can use the rule
+
+\begin{center}
+\bl{\infer{\Gamma, F \vdash F}{}}
+\end{center}
+
+\onslide<5>{\bf\alert{What is wrong with this?}}
+\hfill{\bf Done. Qed.}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Digression: Proofs in CS}
+
+Formal proofs in CS sound like science fiction? Completely irrelevant!
+Lecturers gone mad!\pause
+
+\begin{itemize}
+\item in 2008, verification of a small C-compiler
+\begin{itemize}
+\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
+\item is as good as \texttt{gcc -O1}, but less buggy 
+\end{itemize}
+\medskip 
+\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
+\begin{itemize}
+\item 200k loc of proof
+\item 25 - 30 person years
+\item found 160 bugs in the C code (144 by the proof)
+\end{itemize}
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{}
+
+  \begin{tabular}{c@ {\hspace{2mm}}c}
+  \\[6mm]
+  \begin{tabular}{c}
+  \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
+  {\footnotesize Bob Harper}\\[-2.5mm]
+  {\footnotesize (CMU)}
+  \end{tabular}
+  \begin{tabular}{c}
+  \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
+  {\footnotesize Frank Pfenning}\\[-2.5mm]
+  {\footnotesize (CMU)}
+  \end{tabular} &
+
+  \begin{tabular}{p{6cm}}
+  \raggedright
+  \color{gray}{published a proof about a specification in a journal (2005),
+  $\sim$31pages}
+  \end{tabular}\\
+
+  \pause
+  \\[0mm]
+  
+  \begin{tabular}{c}
+  \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 
+  {\footnotesize Andrew Appel}\\[-2.5mm]
+  {\footnotesize (Princeton)}
+  \end{tabular} &
+
+  \begin{tabular}{p{6cm}}
+  \raggedright
+  \color{gray}{relied on their proof in a\\ {\bf security} critical application}
+  \end{tabular}
+  \end{tabular}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{Proof-Carrying Code}
+
+  \begin{textblock}{10}(2.5,2.2)
+  \begin{block}{Idea:}
+  \begin{center}
+  \begin{tikzpicture}
+  \draw[help lines,cream] (0,0.2) grid (8,4);
+  
+  \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
+  \node[anchor=base] at (6.5,2.8) 
+     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user: untrusted code\end{tabular}};
+
+  \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);
+  \node[anchor=base] at (1.5,2.3) 
+     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  developer ---\\ web server\end{tabular}};
+  
+  \onslide<3->{
+  \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
+  \node[anchor=base,white] at (6.5,1.1) 
+     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}
+
+  \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};
+  \onslide<2->{
+  \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf certificate};
+  \node at (3.8,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof}};
+  }
+
+  
+  \end{tikzpicture}
+  \end{center}
+  \end{block}
+  \end{textblock}
+
+  %\begin{textblock}{15}(2,12)
+  %\small
+  %\begin{itemize}
+  %\item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 
+  %803 loc in C including 2 library functions)\\[-3mm]
+  %\item<5-> 167 loc in C implement a type-checker
+  %\end{itemize}
+  %\end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+ \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 
+                     draw=black!50, top color=white, bottom color=black!20]
+  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
+                     draw=red!70, top color=white, bottom color=red!50!black!20]
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<2->[squeeze]
+  \frametitle{} 
+  
+  \begin{columns}
+  
+  \begin{column}{0.8\textwidth}
+  \begin{textblock}{0}(1,2)
+
+  \begin{tikzpicture}
+  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+  { \&[-10mm] 
+    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+    \node (proof1) [node1] {\large Proof}; \&
+    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+    
+    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&
+    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
+    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+     
+    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
+    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\
+
+    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
+    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+  };
+
+  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+  
+  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
+  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
+
+  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
+  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
+  
+  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
+  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
+
+  \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 
+  \end{tikzpicture}
+
+  \end{textblock}
+  \end{column}
+  \end{columns}
+
+
+  \begin{textblock}{3}(12,3.6)
+  \onslide<4->{
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+     
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Mars Pathfinder Mission 1997}
+
+  \begin{center}
+  \includegraphics[scale=0.15]{marspath1.png}
+  \includegraphics[scale=0.16]{marspath3.png}
+  \includegraphics[scale=0.3]{marsrover.png}
+  \end{center}
+  
+  \begin{itemize}
+  \item despite NASA's famous testing procedure, the lander crashed frequently on Mars
+  \item problem was an algorithm not used in the OS
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Priority Inheritance Protocol}
+
+  \begin{itemize}
+  \item \ldots a scheduling algorithm that is widely used in real-time operating systems
+  \item has been ``proved'' correct by hand in a paper in 1983
+  \item \ldots but the first algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause
+  
+  \item we specified the algorithm and then proved that the specification makes
+  ``sense''	
+ \item we implemented our specification in C on top of PINTOS (used for teaching at Stanford)
+ \item our implementation was much more efficient than their reference implementation
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+  
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Regular Expression Matching}
+\tiny
+
+\begin{tabular}{@ {\hspace{-6mm}}cc}
+\begin{tikzpicture}[y=.1cm, x=.15cm]
+ 	%axis
+	\draw (0,0) -- coordinate (x axis mid) (30,0);
+    	\draw (0,0) -- coordinate (y axis mid) (0,30);
+    	%ticks
+    	\foreach \x in {0,5,...,30}
+     		\draw (\x,1pt) -- (\x,-3pt)
+			node[anchor=north] {\x};
+    	\foreach \y in {0,5,...,30}
+     		\draw (1pt,\y) -- (-3pt,\y) 
+     			node[anchor=east] {\y}; 
+	%labels      
+	\node[below=0.3cm] at (x axis mid) {\bl{a}s};
+	\node[rotate=90, left=0.6cm] at (y axis mid) {secs};
+
+	%plots
+	\draw[color=blue] plot[mark=*, mark options={fill=white}] 
+		file {re-python.data};
+	\only<1->{
+	\draw[color=red] plot[mark=triangle*, mark options={fill=white} ] 
+		file {re1.data};}
+	\only<1->{	 
+         \draw[color=green] plot[mark=square*, mark options={fill=white} ] 
+		file {re2.data};}
+    
+	%legend
+	\begin{scope}[shift={(4,20)}] 
+	\draw[color=blue] (0,0) -- 
+		plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) 
+		node[right]{\footnotesize Python};
+	\only<1->{\draw[yshift=6mm, color=red] (0,0) -- 
+		plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0)
+		node[right]{\footnotesize Scala V1};}
+	\only<1->{	
+	 \draw[yshift=12mm, color=green] (0,0) -- 
+		plot[mark=square*, mark options={fill=white}] (0.25,0) -- (0.5,0)
+		node[right]{\footnotesize Scala V2 with simplifications};}
+	\end{scope}
+\end{tikzpicture} &
+
+\begin{tikzpicture}[y=.35cm, x=.00045cm]
+ 	%axis
+	\draw (0,0) -- coordinate (x axis mid) (10000,0);
+    	\draw (0,0) -- coordinate (y axis mid) (0,6);
+    	%ticks
+    	\foreach \x in {0,2000,...,10000}
+     		\draw (\x,1pt) -- (\x,-3pt)
+			node[anchor=north] {\x};
+    	\foreach \y in {0,1,...,6}
+     		\draw (1pt,\y) -- (-3pt,\y) 
+     			node[anchor=east] {\y}; 
+	%labels      
+	\node[below=0.3cm] at (x axis mid) {\bl{a}s};
+	\node[rotate=90, left=0.6cm] at (y axis mid) {secs};
+
+	%plots
+	\draw[color=blue] plot[mark=*, mark options={fill=white}] 
+		file {re-internal.data};
+	\only<1->{	 
+         \draw[color=red] plot[mark=triangle*, mark options={fill=white} ] 
+		file {re3.data};}
+    
+	%legend
+	\begin{scope}[shift={(2000,4)}] 
+	\draw[color=blue] (0,0) -- 
+		plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) 
+		node[right]{\footnotesize Scala Internal};
+        \only<1->{
+	\draw[yshift=6mm, color=red] (0,0) -- 
+		plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0)
+		node[right]{\footnotesize Scala V3};}
+	\end{scope}
+\end{tikzpicture}
+\end{tabular}\bigskip\pause
+\normalsize
+\begin{itemize}
+\item I needed a proof in order to make sure my program is correct
+\end{itemize}\pause
+
+\begin{center}
+\bl{End Digression.\\ (Our small proof is 0.0005\% of the OS-proof.)}
+\end{center}
+
+\end{frame}}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{One More Thing}
+
+\begin{itemize}
+\item I arrived at King's last year
+\item Maxime Crochemore told me about a string algorithm (suffix sorting) that appeared at a
+conference in 2007 (ICALP)
+\item ``horribly incomprehensible'', no implementation, but claims to be the best \bl{$O(n + k)$} algorithm\bigskip\pause
+
+\item Jian Jiang found 1 error and 1 superfluous step in this algorithm
+\item he received 88\% for the project and won the prize for the best 7CCSMPRJ project  in the department
+\item no proof \ldots{} yet
+\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{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}
+
+  \begin{itemize}
+  \item Alice calls Sam for a key to communicate with Bob
+  \item Sam responds with a key that Alice can read and a key Bob can read (pre-shared)
+  \item Alice sends the message encrypted with the key and the second key it recieved
+  \end{itemize}\bigskip
+
+  \begin{center}
+  \bl{\begin{tabular}{lcl}
+  $A$ sends $S$ &:& $\textit{Connect}(A,B)$\\
+  $S$ sends $A$ &:& $\{K_{AB}\}_{K_{AS}}$ \textcolor{black}{and} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
+  $A$ sends $B$ &:& $\{K_{AB}\}_{K_{BS}}$\\
+  $A$ sends $B$ &:& $\{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 \;\textit{says}\; F}
+              {\Gamma \vdash P \;\textit{says}\; F & \Gamma \vdash P \;\textit{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$ : $\textit{Connect}(A,B)$\\  
+  \bl{$S \,\text{says}\, (\textit{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{Challenge-Response Protocol}
+
+ \begin{itemize}
+ \item an engine \bl{$E$} and a transponder \bl{$T$} share a key \bl{$K$}\bigskip
+ \item \bl{$E$} sends out a \alert{nonce} \bl{$N$} (random number) to \bl{$T$}\bigskip
+ \item \bl{$T$} responds with \bl{$\{N\}_K$}\bigskip
+ \item if \bl{$E$} receives  \bl{$\{N\}_K$} from \bl{$T$}, it starts engine
+ \end{itemize}	
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  
+    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Challenge-Response Protocol}
+
+  \begin{center}
+  \bl{\begin{tabular}{l}
+  $E \;\text{says}\; N$\hfill(start)\\
+  $E \;\text{sends}\; T : N$\hfill(challenge)\\
+  $(T \;\text{says}\; N) \Rightarrow (T \;\text{sends}\; E : \{N\}_K \wedge$\\
+  \hspace{3.5cm} $T \;\text{sends}\; E : \text{Id}(T))$\;\;\;\hfill(response)\\
+ $T \;\text{says}\; K$\hfill(key)\\
+ $T \;\text{says}\; \text{Id}(T)$\hfill(identity)\\
+  $(E \;\text{says}\; \{N\}_K \wedge E \;\text{says}\; \text{Id}(T)) \Rightarrow$\\
+   \hspace{5cm}$ \text{start\_engine}(T)$\hfill(engine)\\
+  \end{tabular}}
+  \end{center}\bigskip 
+  
+  \bl{$\Gamma \vdash \text{start\_engine}(T)$}?
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+     
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Exchange of a Fresh Key}
+
+\bl{$A$} and \bl{$B$} share a (``super-secret'') key \bl{$K_{AB}$} and want to share another key
+
+ \begin{itemize}
+ \item assumption \bl{$K_{AB}$} is only known to \bl{$A$} and \bl{$B$}\bigskip 
+ \item \bl{$A \,\text{sends}\, B :  A, \{N_A\}_{K_{AB}}$} 
+ \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$}
+ \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$}
+  \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}
+  \item<2> \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}
+ \end{itemize}\bigskip
+  
+  Assume \bl{$K^{new}_{AB}$} is compromised by \bl{$I$}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
+     
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{The Attack}
+
+An intruder \bl{$I$} convinces \bl{$A$} to accept the compromised key \bl{$K^{new}_{AB}$}\medskip 
+
+\begin{minipage}{1.1\textwidth}
+\begin{itemize}
+ \item \bl{$A \,\text{sends}\, B :  A, \{N_A\}_{K_{AB}}$} 
+ \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$}
+ \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$}
+  \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\;\;recorded by \bl{$I$}\pause
+  \item \bl{$A \,\text{sends}\, B :  A, \{M_A\}_{K_{AB}}$} 
+ \item \bl{$B\,\text{sends}\, A : \{M_A + 1, M_B\}_{K_{AB}}$}
+ \item \bl{$A \,\text{sends}\, B : \{M_B + 1\}_{K_{AB}}$}
+  \item \bl{$B \,\text{sends}\, I : \{K^{newer}_{AB}, N^{newer}_B\}_{K_{AB}}$}\;intercepted by \bl{$I$}
+  \item \bl{$I \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\pause
+   \item \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}\;\;\;\;\bl{$I$} can read it also
+ \end{itemize}	
+ \end{minipage}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+     
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Another Challenge-Response}
+
+\bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify
+each other\bigskip
+
+ \begin{itemize}
+ \item \bl{$A \,\text{sends}\, B :  A, N_A$} 
+ \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$}
+ \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$}
+ \end{itemize}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
+     
+   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Another Challenge-Response}
+
+\bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify
+each other\bigskip
+
+ \begin{itemize}
+ \item \bl{$A \,\text{sends}\, B :  A, N_A$} 
+ \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$}
+ \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$}
+ \end{itemize}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
+     
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Another Challenge-Response}
+
+Unfortunately, an intruder \bl{$I$} can impersonate \bl{$B$}.
+
+\begin{center}
+\begin{tabular}{@{\hspace{-7mm}}c@{\hspace{1mm}}c@{}}
+\begin{tabular}{@{}l@{}}
+\onslide<1->{\bl{$A \,\text{sends}\, I :  A, N_A$}}\\ 
+\onslide<4->{\bl{$I \,\text{sends}\, A :  \{N_A,\!K'_{\!AB}\}_{K_{\!AB}}$}}\\ 
+\onslide<5->{\bl{$A \,\text{sends}\, I : \{N_A\}_{K'_{AB}}$}}\\
+\end{tabular}
+&
+\begin{tabular}{@{}l@{}}
+\onslide<2->{\bl{$I \,\text{sends}\, A :  B, N_A$}}\\ 
+\onslide<3->{\bl{$A \,\text{sends}\, I :  \{N_A,\!K'_{\!AB}\}_{K_{\!AB}}$}}\\ 
+\onslide<6->{\bl{$I \,\text{sends}\, A : \{N_A\}_{K'_{AB}}$}}\\
+\end{tabular}
+\end{tabular}
+\end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%          
+     
+     
+\end{document}
+
+%%% Local Variables:  
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
+




