
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<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:  




