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