diff -r 53e7d51dbc10 -r 20d0a65b47f2 slides07.tex --- a/slides07.tex Tue Nov 13 11:53:40 2012 +0000 +++ b/slides07.tex Tue Nov 13 14:10:23 2012 +0000 @@ -331,15 +331,54 @@ \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?\pause{} Completely irrelevant!\pause +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\medskip +\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 @@ -534,13 +573,13 @@ \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 \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 (Stanford) + \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} @@ -653,8 +692,8 @@ 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 -\item he received 88\% for the project and won the prize for the best 7CCSMPRJ project +\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} @@ -753,6 +792,7 @@ \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}} @@ -828,7 +868,7 @@ \begin{frame}[c] \frametitle{Exchange of a Fresh Key} -\bl{$A$} and \bl{$B$} share the key \bl{$K_{AB}$} and want to share another 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 @@ -839,7 +879,6 @@ \item<2> \bl{$A \,\text{sends}\, B : \{msg\}_{K^{new}_{AB}}$} \end{itemize}\bigskip - \bl{$N^{new}_B$} is to be used in future messages\\ Assume \bl{$K^{new}_{AB}$} is compromised by \bl{$I$} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -860,15 +899,64 @@ \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^{anew}_{AB}, N^{anew}_B\}_{K_{AB}}$}\;intercepted by \bl{$I$} + \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}}$} + \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} + +\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}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + \end{document} %%% Local Variables: