slides07.tex
author Christian Urban <urbanc@in.tum.de>
Tue, 13 Nov 2012 09:29:30 +0000
changeset 67 2522dea979d0
parent 66 2895a7550754
child 68 bc48791bb3a9
permissions -rw-r--r--
updated

\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}[c]
\frametitle{Digression: Proofs in CS}

Formal proofs in CS sound like science fiction?\pause{} Completely irrelevant!\pause

\begin{itemize}
\item in 2008, verification of a small C-compiler\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 an algorithm that is widely used in real-time operating systems
  \item hash been ``proved'' correct by hand in a paper in 1983
  \item but the first algorithm turned out to be incorrect, despite the ``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 (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{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$} then starts engine
 \end{itemize}	
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Challenge-Response Protokol}

  \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}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
     
\end{document}

%%% Local Variables:  
%%% mode: latex
%%% TeX-master: t
%%% End: