--- a/progs/prove.scala	Sun Nov 17 19:22:57 2013 +0000
+++ b/progs/prove.scala	Tue Nov 19 03:05:48 2013 +0000
@@ -15,6 +15,8 @@
 case class Says(p: String, f: Form) extends Form 
 case class And(f1: Form, f2: Form) extends Form 
 case class Or(f1: Form, f2: Form) extends Form 
+case class Sends(p: String, q: String, f: Form) extends Form
+case class Enc(f1: Form, f2: Form) extends Form
 
 case class Judgement(gamma: Set[Form], f: Form) {
   def lhs = gamma
@@ -67,6 +69,8 @@
     case And(f1, f2) => 
       prove(j.lhs |- f1, 
             () => prove(j.lhs |- f2, sc))
+    case Sends(p, q, f) => prove(j.lhs + (p says f) |- (q says f), sc)
+    case Enc(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
     case _ => ()
   }
 
@@ -79,12 +83,19 @@
     case Imp(f1, f2) => 
       prove(lhs_rest |- f1, 
             () => prove(lhs_rest + f2 |- rhs, sc))
+    case Sends(p, q, f) => 
+      prove(lhs_rest |- (p says f), 
+            () => prove(lhs_rest + (q says f) |- rhs, sc))
+    case Enc(f1, f2) => 
+      prove(lhs_rest |- f1, 
+            () => prove(lhs_rest + f2 |- rhs, sc))
     case Or(f1, f2) => 
       prove(lhs_rest + f1 |- rhs, 
             () => prove(lhs_rest + f2 |- rhs, sc))
     case Says(p, Imp(f1, f2)) => 
       prove(lhs_rest |- Says(p, f1), 
-            () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) 
+            () => prove(lhs_rest + Says(p, f2) |- rhs, sc))
+     
     case _ => ()
   }
 
@@ -128,4 +139,40 @@
 
 run (Set[Form](AtLib, Policy_HoD, Policy_Lib) |- Email)
 
+println("Server Example")
 
+val Alice = "Alice"
+//val Bob = "Bob"  -- already defined
+val Server = "Server"
+
+def Connect(p: String, q: String) : Form =
+  Pred("Connect", List(Var(p), Var(q)))
+
+
+val A = "A"
+val B = "B"
+val S = "S"
+val CAB = Connect(A, B)
+val Msg = Pred("Msg", Nil)
+val KAS = Pred("Kas", Nil)
+val KBS = Pred("Kbs", Nil)
+val KAB = Pred("Kab", Nil)
+
+val Gamma_big : Set[Form] = 
+  Set( A says CAB,
+       Sends(A, S, CAB), 
+       S says (CAB -> Enc(KAB, KAS)),
+       S says (CAB -> Enc(Enc(KAB, KBS), KAS)),
+       Sends(S, A, Enc(KAB, KAS)),
+       Sends(S, A, Enc(Enc(KAB, KBS), KAS)),
+       Sends(A, B, Enc(KAB, KBS)),
+       Sends(A, B, Enc(Msg, KAB)),
+       A says KAS,
+       B says KBS,
+       S says KAS,
+       A says (Enc(Msg, KAB))
+     )
+
+run (Gamma_big |- (B says Msg))
+
+