496 \frametitle{Access Control Logic}

   497 

   498 Ross Anderson about the use of Logic:\bigskip

   499 

   500 \begin{quote}\rm

   501 ``Formal methods can be an excellent way of finding 

   502 bugs in security protocol designs as they force the designer 

   503 to make everything explicit and thus confront difficult design 

   504 choices that might otherwise be fudged.'' 

   505 \end{quote}

   506 

   507 \end{frame}

   508 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   509 

   510 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   511   \begin{frame}[t]

   512   \frametitle{Access Control Logic}

   513   

   514   \begin{center}

   515   \begin{tabular}[t]{rcl@ {\hspace{10mm}}l}

   516    \bl{$F$} & \bl{$::=$} & \bl{$\textit{true}$}\\

   517             & \bl{$|$} & \bl{$\textit{false}$}\\

   518             & \bl{$|$} & \bl{$a(t_1,\ldots,t_n)$}\\

   519             & \bl{$|$} & \bl{$F_1 \wedge F_2$}\\

   520             & \bl{$|$} & \bl{$F_1 \vee F_2$}\\

   521             & \bl{$|$} & \bl{$F_1 \Rightarrow F_2$}\\

   522             & \bl{$|$} & \alert{$P\;\textit{says}\; F$}\\

   523   \end{tabular}

   524   \end{center}

   525   

   526   where \bl{$P = Alice, Bob, Christian$} 

   527   

   528   \begin{itemize}

   529   \item \bl{$HoD\;\textit{says}\;\textit{is\_staff}(Christian)$}

   530   \end{itemize}

   531   \end{frame}

   532 

   533 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   534   \begin{frame}[t]

   535   \frametitle{Access Control Logic}

   536 

   537 \ldots can be used for answering the following questions:

   538 

   539 \begin{itemize}

   540 \item To what conclusions does this protocol come?

   541 \item What assumptions are needed for this protocol?

   542 \item Does the protocol uses unnecessary actions, which can be left out?

   543 \item Does the protocol encrypt anything which could be sent in plain, without

   544 weakening the security?

   545 \end{itemize}

   546 

   547 \end{frame}

   548 

   549 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   550 \begin{frame}[c]