# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1351631616 0
# Node ID e8071a3f13b216c8bc24485894764ff61fff4031
# Parent  31de247cfb5bf155ea107e092d81900f96ca6f72
tuned

diff -r 31de247cfb5b -r e8071a3f13b2 programs/prove1.scala
--- a/programs/prove1.scala	Tue Oct 30 14:48:13 2012 +0000
+++ b/programs/prove1.scala	Tue Oct 30 21:13:36 2012 +0000
@@ -24,7 +24,6 @@
 val Bob = "Bob"
 val Del = Pred("del_file", Nil)
 
-
 val Gamma = 
   List( Says(Admin, Del) -> Del,
         Says(Admin, Says(Bob, Del) -> Del),
@@ -37,11 +36,13 @@
   else prove1(j.lhs, j.rhs, sc) 
 }
 
-def partitions(ls: List[Form]): List[(Form, List[Form])]  = 
+def partitions[A](ls: List[A]): List[(A, List[A])]  = 
   ls.map (s => (s, ls - s))
 
 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 
   rhs match {
+    case True => sc()
+    case False => ()
     case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) 
     case Says(p, f1) => prove(Judgement(lhs, f1), sc) 
     case Or(f1, f2) => 
@@ -56,6 +57,8 @@
 
 def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = 
   f match {
+    case True => prove(Judgement(lhs_rest, rhs), sc)
+    case False => sc()
     case And(f1, f2) =>
       prove(Judgement(f1::f2::lhs_rest, rhs), sc)
     case Imp(f1, f2) => 
@@ -81,11 +84,25 @@
   catch { case e: Exception => () }
 } 
 
+run (Judgement (Nil, False -> Del))
+run (Judgement (Nil, True -> Del))
+run (Judgement (Nil, Del -> True))
+
 run (goal)
 
+val Gamma1 = 
+  List( Says(Admin, Says(Bob, Del) -> Del),
+        Says(Bob, Del) )
+
+val goal1 = Judgement(Gamma1, Del) // not provable
+
+run (goal1)
 
 run (Judgement(Nil, Del -> Del))
 
+run (Judgement(Nil, Del -> Or(False, Del)))
+
+
 val Chr = "Christian"
 val HoD = "Michael Luck"
 val Email = Pred("may_btain_email", List(Const(Chr)))
diff -r 31de247cfb5b -r e8071a3f13b2 slides06.pdf
Binary file slides06.pdf has changed
diff -r 31de247cfb5b -r e8071a3f13b2 slides06.tex
--- a/slides06.tex	Tue Oct 30 14:48:13 2012 +0000
+++ b/slides06.tex	Tue Oct 30 21:13:36 2012 +0000
@@ -256,7 +256,7 @@
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}[c]
 \frametitle{Inference Rules}
@@ -264,7 +264,7 @@
 \begin{center}
 \bl{\infer{\Gamma, F\vdash F}{}}\bigskip\\
 
-\bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_2}}
+\bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1 \Rightarrow F_2 \quad \Gamma \vdash F_1}}
 \qquad
 \bl{\infer{\Gamma \vdash F_1 \Rightarrow F_2}{F_1, \Gamma \vdash F_2}}\bigskip\\
 
@@ -525,7 +525,7 @@
   \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}}}
+              {\Gamma \vdash \text{Alice}\;\text{says}\;\{m\}_K & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
   \end{center}
   \end{itemize}
 
@@ -541,7 +541,7 @@
   \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}}}
+              {\Gamma \vdash \text{Alice}\;\text{says}\;m & \Gamma \vdash \text{Alice}\,\text{says}\,K}}}
   \end{center}
   \end{itemize}
 
@@ -616,7 +616,7 @@
   $A$ sends $S$ : $\textit{Connect}(A,B)$\\  
   \bl{$S \,\text{says}\, (\textit{Connect}(A,B) \Rightarrow$}\\ 
   \hspace{2.5cm}\bl{$\{K_{AB}\}_{K_{AS}} \wedge 
-  \{\{K_{AB}\}_{K_{BS}}\}\_{K_{AS}})$}\\
+  \{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}})$}\\
  $S$ sends $A$ : $\{K_{AB}\}_{K_{AS}}$ \bl{$\wedge$} $\{\{K_{AB}\}_{K_{BS}}\}_{K_{AS}}$\\
   $A$ sends $B$ : $\{K_{AB}\}_{K_{BS}}$\\
   $A$ sends $B$ : $\{m\}_{K_{AB}}$