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