--- a/programs/prove1.scala	Tue Oct 30 07:11:42 2012 +0000
+++ b/programs/prove1.scala	Tue Oct 30 14:27:59 2012 +0000
@@ -1,10 +1,12 @@
 
-abstract class Term
+abstract class Term 
 case class Var(s: String) extends Term 
 case class Const(s: String) extends Term 
 case class Fun(s: String, ts: List[Term]) extends Term
 
-abstract class Form
+abstract class Form {
+  def -> (that: Form) = Imp(this, that)
+}
 case object True extends Form
 case object False extends Form
 case class Pred(s: String, ts: List[Term]) extends Form
@@ -24,8 +26,8 @@
 
 
 val Gamma = 
-  List( Imp(Says(Admin, Del), Del),
-        Says(Admin, Imp(Says(Bob, Del), Del)),
+  List( Says(Admin, Del) -> Del,
+        Says(Admin, Says(Bob, Del) -> Del),
         Says(Bob, Del) )
 
 val goal = Judgement(Gamma, Del) // request: provable or not?
@@ -82,7 +84,7 @@
 run (goal)
 
 
-run (Judgement(Nil, Imp(Del, Del)))
+run (Judgement(Nil, Del -> Del))
 
 val Chr = "Christian"
 val HoD = "Michael Luck"
@@ -90,8 +92,8 @@
 val AtLib = Pred("is_at_library", List(Const(Chr)))
 val Chr_Staff = Pred("is_staff", List(Const(Chr)))
 
-val Policy_HoD = Imp(Says(HoD, Chr_Staff), Chr_Staff)
-val Policy_Lib = Imp(And(Chr_Staff, AtLib), Email)
+val Policy_HoD = Says(HoD, Chr_Staff) -> Chr_Staff
+val Policy_Lib = And(Chr_Staff, AtLib) -> Email
 val HoD_says = Says(HoD, Chr_Staff)
 
 run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email))

Binary file slides06.pdf has changed

--- a/slides06.tex	Tue Oct 30 07:11:42 2012 +0000
+++ b/slides06.tex	Tue Oct 30 14:27:59 2012 +0000
@@ -283,7 +283,16 @@
 \begin{frame}[c]
 \frametitle{Proofs}
 
-
+\begin{center}
+\bl{
+\infer{\Gamma \vdash F}
+         {\infer{\hspace{1cm}:\hspace{1cm}}
+             {\infer{\hspace{1cm}:\hspace{1cm}}{:}
+               &
+              \infer{\hspace{1cm}:\hspace{1cm}}{:\quad :}
+           }}
+}
+\end{center}
 
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
@@ -322,21 +331,21 @@
   Recall the following scenario:
 
   \begin{itemize}
-  \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} 
+  \item If \textcolor{blue}{Admin} says that \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{} {}}} 
   should be deleted, then this file must be deleted.
   \item \textcolor{blue}{Admin} trusts \textcolor{blue}{Bob} to decide whether 
-  \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}} should be deleted.
-  \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}.
+  \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}} should be deleted.
+  \item \textcolor{blue}{Bob} wants to delete \textcolor{blue}{\isa{file\isaliteral{5C3C5E697375623E}{}}}.
   \end{itemize}\bigskip
 
   \small
   \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{3D}{\isacharequal}}}\small\begin{tabular}{l}
-  \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}},\\
-  \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
-  \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}\\
+  \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}},\\
+  \isa{{\isaliteral{28}{\isacharparenleft}}Admin\ says\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}},\\
+  \isa{Bob\ says\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}\\
   \end{tabular}}\medskip
 
-  \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}}
+  \textcolor{blue}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ del{\isaliteral{5F}{\isacharunderscore}}file\isaliteral{5C3C5E697375623E}{}}}
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -420,12 +429,125 @@
 \begin{center}
 \bl{$F_2, \Gamma \vdash \text{Pred}$}
 \end{center}
+\end{enumerate}
 
-\end{enumerate}
+\only<4>{
+\begin{textblock}{11}(1,10.5)
+\bl{\infer{\Gamma\vdash F_2}{\Gamma\vdash F_1\Rightarrow F_2 & \Gamma\vdash F_1}}
+\end{textblock}}
+
 
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
 
+\begin{itemize}
+\item \bl{$P$} is entitled to do \bl{$F$}\smallskip\\ 
+\bl{$P \,\text{controls}\, F \,\dn\, (P\,\text{says}\, F) \Rightarrow F$}\medskip
+
+\begin{center}
+\bl{\infer{\Gamma \vdash F}{\Gamma \vdash P\,\text{controls}\, F & \Gamma \vdash P\,\text{says}\,F}}
+\end{center}
+
+\item \bl{$P$} speaks for \bl{$Q$}\smallskip\\
+\bl{$P \mapsto Q \,\dn\, \forall F. (P\,\text{says}\, F) \Rightarrow (Q \,\text{says}\,F)$}\medskip
+
+\begin{center}
+\bl{\infer{\Gamma \vdash Q\,\text{says}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash P\,\text{says}\,F}}
+\medskip\\
+\bl{\infer{\Gamma \vdash P\,\text{controls}\,F}{\Gamma \vdash P\mapsto Q & \Gamma \vdash Q\,\text{controls}\,F}}\\
+
+\end{center}
+\end{itemize}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Protocol Specifications}
+
+The Needham-Schroeder Protocol:
+
+\begin{center}
+\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}
+Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B, N_A$}\\
+Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{N_A, B, K_{AB},\{K_{AB}, A\}_{K_{BS}} \}_{K_{AS}}$}\\
+Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}, A\}_{K_{BS}} $}\\
+Message 4 & \bl{$B \rightarrow A :$} & \bl{$\{N_B\}_{K_{AB}}$}\\
+Message 5 & \bl{$A \rightarrow B :$} & \bl{$\{N_B-1\}_{K_{AB}}$}\\
+\end{tabular}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Trusted Third Party}
+
+Simple protocol for establishing a secure connection via a mutually
+trusted 3rd party (server):
+
+\begin{center}
+\begin{tabular}{@ {\hspace{-7mm}}l@{\hspace{2mm}}r@ {\hspace{1mm}}l}
+Message 1 & \bl{$A \rightarrow S :$} & \bl{$A, B$}\\
+Message 2 & \bl{$S \rightarrow A :$} & \bl{$\{K_{AB}\}_{K_{AS}}$} and \bl{$\{\{K_{AB}\}_{K_{BS}} \}_{K_{AS}}$}\\
+Message 3 & \bl{$A \rightarrow B :$} & \bl{$\{K_{AB}\}_{K_{BS}} $}\\
+Message 4 & \bl{$A \rightarrow B :$} & \bl{$\{m\}_{K_{AB}}$}\\
+\end{tabular}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Sending Messages}
+
+  \begin{itemize}
+  \item Alice sends a message \bl{$m$}
+  \begin{center}
+  \bl{Alice says $m$}
+  \end{center}\medskip\pause
+
+  \item Alice sends an encrypted message \bl{$m$}\\ (with key \bl{$K$})
+  \begin{center}
+  \bl{Alice says $\{m\}_K$}
+  \end{center}\medskip\pause
+
+  \item Decryption of Alice's message\smallskip
+  \begin{center}
+  \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;m}
+              {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash K}}}
+  \end{center}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+  
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Encryption}
+
+  \begin{itemize}
+  \item Encryption of a message\smallskip
+  \begin{center}
+  \bl{\mbox{\infer{\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K}
+              {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash K}}}
+  \end{center}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+  
 \end{document}
 
 %%% Local Variables: