diff -r be35ff24cccc -r d1d07f05325a slides07.tex --- a/slides07.tex Sun Dec 09 13:00:33 2012 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,976 +0,0 @@ -\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: -