329 \end{center} |
329 \end{center} |
330 |
330 |
331 \end{frame}} |
331 \end{frame}} |
332 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
332 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
333 |
333 |
|
334 |
|
335 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
336 \mode<presentation>{ |
|
337 \begin{frame}[t] |
|
338 |
|
339 We want to prove |
|
340 |
|
341 \begin{center} |
|
342 \bl{$\Gamma \vdash \text{del\_file}$} |
|
343 \end{center}\pause |
|
344 |
|
345 There is an inference rule |
|
346 |
|
347 \begin{center} |
|
348 \bl{\infer{\Gamma \vdash P \,\text{says}\, F}{\Gamma \vdash F}} |
|
349 \end{center}\pause |
|
350 |
|
351 So we can derive \bl{$\Gamma \vdash \text{Alice} \,\text{says}\,\text{del\_file}$}.\bigskip\pause |
|
352 |
|
353 \bl{$\Gamma$} contains already \bl{$\text{Alice} \,\text{says}\,\text{del\_file}$}. \\ |
|
354 So we can use the rule |
|
355 |
|
356 \begin{center} |
|
357 \bl{\infer{\Gamma, F \vdash F}{}} |
|
358 \end{center} |
|
359 |
|
360 \onslide<5>{\bf\alert{What is wrong with this?}} |
|
361 \hfill{\bf Done. Qed.} |
|
362 |
|
363 \end{frame}} |
|
364 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
365 |
|
366 |
334 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
367 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
335 \mode<presentation>{ |
368 \mode<presentation>{ |
336 \begin{frame}[c] |
369 \begin{frame}[c] |
337 \frametitle{Digression: Proofs in CS} |
370 \frametitle{Digression: Proofs in CS} |
338 |
371 |
339 Formal proofs in CS sound like science fiction?\pause{} Completely irrelevant!\pause |
372 Formal proofs in CS sound like science fiction? Completely irrelevant! |
|
373 Lecturers gone mad!\pause |
340 |
374 |
341 \begin{itemize} |
375 \begin{itemize} |
342 \item in 2008, verification of a small C-compiler\medskip |
376 \item in 2008, verification of a small C-compiler |
|
377 \begin{itemize} |
|
378 \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' |
|
379 \item is as good as \texttt{gcc -O1}, but less buggy |
|
380 \end{itemize} |
|
381 \medskip |
343 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) |
382 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) |
344 \begin{itemize} |
383 \begin{itemize} |
345 \item 200k loc of proof |
384 \item 200k loc of proof |
346 \item 25 - 30 person years |
385 \item 25 - 30 person years |
347 \item found 160 bugs in the C code (144 by the proof) |
386 \item found 160 bugs in the C code (144 by the proof) |
532 \mode<presentation>{ |
571 \mode<presentation>{ |
533 \begin{frame}[c] |
572 \begin{frame}[c] |
534 \frametitle{Priority Inheritance Protocol} |
573 \frametitle{Priority Inheritance Protocol} |
535 |
574 |
536 \begin{itemize} |
575 \begin{itemize} |
537 \item an algorithm that is widely used in real-time operating systems |
576 \item \ldots a scheduling algorithm that is widely used in real-time operating systems |
538 \item hash been ``proved'' correct by hand in a paper in 1983 |
577 \item has been ``proved'' correct by hand in a paper in 1983 |
539 \item but the first algorithm turned out to be incorrect, despite the ``proof''\bigskip\pause |
578 \item \ldots but the first algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause |
540 |
579 |
541 \item we specified the algorithm and then proved that the specification makes |
580 \item we specified the algorithm and then proved that the specification makes |
542 ``sense'' |
581 ``sense'' |
543 \item we implemented our specification in C on top of PINTOS (Stanford) |
582 \item we implemented our specification in C on top of PINTOS (used for teaching at Stanford) |
544 \item our implementation was much more efficient than their reference implementation |
583 \item our implementation was much more efficient than their reference implementation |
545 \end{itemize} |
584 \end{itemize} |
546 |
585 |
547 \end{frame}} |
586 \end{frame}} |
548 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
587 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
651 \item I arrived at King's last year |
690 \item I arrived at King's last year |
652 \item Maxime Crochemore told me about a string algorithm (suffix sorting) that appeared at a |
691 \item Maxime Crochemore told me about a string algorithm (suffix sorting) that appeared at a |
653 conference in 2007 (ICALP) |
692 conference in 2007 (ICALP) |
654 \item ``horribly incomprehensible'', no implementation, but claims to be the best \bl{$O(n + k)$} algorithm\bigskip\pause |
693 \item ``horribly incomprehensible'', no implementation, but claims to be the best \bl{$O(n + k)$} algorithm\bigskip\pause |
655 |
694 |
656 \item Jian Jiang found 1 error and 1 superfluous step |
695 \item Jian Jiang found 1 error and 1 superfluous step in this algorithm |
657 \item he received 88\% for the project and won the prize for the best 7CCSMPRJ project |
696 \item he received 88\% for the project and won the prize for the best 7CCSMPRJ project in the department |
658 \item no proof \ldots{} yet |
697 \item no proof \ldots{} yet |
659 \end{itemize} |
698 \end{itemize} |
660 |
699 |
661 \end{frame}} |
700 \end{frame}} |
662 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
701 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
826 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
866 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
827 \mode<presentation>{ |
867 \mode<presentation>{ |
828 \begin{frame}[c] |
868 \begin{frame}[c] |
829 \frametitle{Exchange of a Fresh Key} |
869 \frametitle{Exchange of a Fresh Key} |
830 |
870 |
831 \bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to share another key |
871 \bl{$A$} and \bl{$B$} share a (``super-secret'') key \bl{$K_{AB}$} and want to share another key |
832 |
872 |
833 \begin{itemize} |
873 \begin{itemize} |
834 \item assumption \bl{$K_{AB}$} is only known to \bl{$A$} and \bl{$B$}\bigskip |
874 \item assumption \bl{$K_{AB}$} is only known to \bl{$A$} and \bl{$B$}\bigskip |
835 \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$} |
875 \item \bl{$A \,\text{sends}\, B : A, \{N_A\}_{K_{AB}}$} |
836 \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$} |
876 \item \bl{$B\,\text{sends}\, A : \{N_A + 1, N_B\}_{K_{AB}}$} |
837 \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$} |
877 \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$} |
838 \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$} |
878 \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$} |
839 \item<2> \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$} |
879 \item<2> \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$} |
840 \end{itemize}\bigskip |
880 \end{itemize}\bigskip |
841 |
881 |
842 \bl{$N^{new}_B$} is to be used in future messages\\ |
|
843 Assume \bl{$K^{new}_{AB}$} is compromised by \bl{$I$} |
882 Assume \bl{$K^{new}_{AB}$} is compromised by \bl{$I$} |
844 \end{frame}} |
883 \end{frame}} |
845 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
884 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
846 |
885 |
847 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
886 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
858 \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$} |
897 \item \bl{$A \,\text{sends}\, B : \{N_B + 1\}_{K_{AB}}$} |
859 \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\;\;recorded by \bl{$I$}\pause |
898 \item \bl{$B \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\;\;recorded by \bl{$I$}\pause |
860 \item \bl{$A \,\text{sends}\, B : A, \{M_A\}_{K_{AB}}$} |
899 \item \bl{$A \,\text{sends}\, B : A, \{M_A\}_{K_{AB}}$} |
861 \item \bl{$B\,\text{sends}\, A : \{M_A + 1, M_B\}_{K_{AB}}$} |
900 \item \bl{$B\,\text{sends}\, A : \{M_A + 1, M_B\}_{K_{AB}}$} |
862 \item \bl{$A \,\text{sends}\, B : \{M_B + 1\}_{K_{AB}}$} |
901 \item \bl{$A \,\text{sends}\, B : \{M_B + 1\}_{K_{AB}}$} |
863 \item \bl{$B \,\text{sends}\, I : \{K^{anew}_{AB}, N^{anew}_B\}_{K_{AB}}$}\;intercepted by \bl{$I$} |
902 \item \bl{$B \,\text{sends}\, I : \{K^{newer}_{AB}, N^{newer}_B\}_{K_{AB}}$}\;intercepted by \bl{$I$} |
864 \item \bl{$I \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\pause |
903 \item \bl{$I \,\text{sends}\, A : \{K^{new}_{AB}, N^{new}_B\}_{K_{AB}}$}\pause |
865 \item \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$} |
904 \item \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$}\;\;\;\;\bl{$I$} can read it also |
866 \end{itemize} |
905 \end{itemize} |
867 \end{minipage} |
906 \end{minipage} |
868 |
907 |
869 \end{frame}} |
908 \end{frame}} |
870 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
909 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
910 |
|
911 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
912 \mode<presentation>{ |
|
913 \begin{frame}[c] |
|
914 \frametitle{Another Challenge-Response} |
|
915 |
|
916 \bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify |
|
917 each other\bigskip |
|
918 |
|
919 \begin{itemize} |
|
920 \item \bl{$A \,\text{sends}\, B : A, N_A$} |
|
921 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$} |
|
922 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$} |
|
923 \end{itemize} |
|
924 \end{frame}} |
|
925 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
926 |
|
927 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
928 \mode<presentation>{ |
|
929 \begin{frame}[c] |
|
930 \frametitle{Another Challenge-Response} |
|
931 |
|
932 \bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify |
|
933 each other\bigskip |
|
934 |
|
935 \begin{itemize} |
|
936 \item \bl{$A \,\text{sends}\, B : A, N_A$} |
|
937 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$} |
|
938 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$} |
|
939 \end{itemize} |
|
940 \end{frame}} |
|
941 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
942 |
|
943 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
944 \mode<presentation>{ |
|
945 \begin{frame}[c] |
|
946 \frametitle{Another Challenge-Response} |
|
947 |
|
948 \bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to identify |
|
949 each other\bigskip |
|
950 |
|
951 \begin{itemize} |
|
952 \item \bl{$A \,\text{sends}\, B : A, N_A$} |
|
953 \item \bl{$B\,\text{sends}\, A : \{N_A, K'_{AB}\}_{K_{AB}}$} |
|
954 \item \bl{$A \,\text{sends}\, B : \{N_A\}_{K'_{AB}}$} |
|
955 \end{itemize} |
|
956 \end{frame}} |
|
957 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
958 |
871 |
959 |
872 \end{document} |
960 \end{document} |
873 |
961 |
874 %%% Local Variables: |
962 %%% Local Variables: |
875 %%% mode: latex |
963 %%% mode: latex |