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