--- /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:
+