--- a/slides/slides10.tex Thu Nov 19 20:59:24 2015 +0000
+++ b/slides/slides10.tex Thu Nov 26 09:10:47 2015 +0000
@@ -493,55 +493,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
-\frametitle{Access Control Logic}
-
-Ross Anderson about the use of Logic:\bigskip
-
-\begin{quote}\rm
-``Formal methods can be an excellent way of finding
-bugs in security protocol designs as they force the designer
-to make everything explicit and thus confront difficult design
-choices that might otherwise be fudged.''
-\end{quote}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \begin{frame}[t]
- \frametitle{Access Control Logic}
-
- \begin{center}
- \begin{tabular}[t]{rcl@ {\hspace{10mm}}l}
- \bl{$F$} & \bl{$::=$} & \bl{$\textit{true}$}\\
- & \bl{$|$} & \bl{$\textit{false}$}\\
- & \bl{$|$} & \bl{$a(t_1,\ldots,t_n)$}\\
- & \bl{$|$} & \bl{$F_1 \wedge F_2$}\\
- & \bl{$|$} & \bl{$F_1 \vee F_2$}\\
- & \bl{$|$} & \bl{$F_1 \Rightarrow F_2$}\\
- & \bl{$|$} & \alert{$P\;\textit{says}\; F$}\\
- \end{tabular}
- \end{center}
-
- where \bl{$P = Alice, Bob, Christian$}
-
- \begin{itemize}
- \item \bl{$HoD\;\textit{says}\;\textit{is\_staff}(Christian)$}
- \end{itemize}
- \end{frame}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \begin{frame}[t]
- \frametitle{Access Control Logic}
-
-\ldots can be used for answering the following questions:
\begin{itemize}
\item To what conclusions does this protocol come?
\item What assumptions are needed for this protocol?
\item Does the protocol uses unnecessary actions, which can be left out?
-\item Does the protocol encrypt anything which could be sent in plain, without
weakening the security?
-\end{itemize}
-
-\end{frame}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
\frametitle{5th Lecture: Protocols}
An article in The Guardian from 2013 reveals how GCHQ and the