131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
import scala.language.implicitConversions
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
import scala.language.reflectiveCalls
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
import scala.util._
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
abstract class Term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
case class Var(s: String) extends Term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
case class Const(s: String) extends Term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
case class Fun(s: String, ts: List[Term]) extends Term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
abstract class Form
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
case object True extends Form
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
case object False extends Form
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
case class Pred(s: String, ts: List[Term]) extends Form
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
case class Imp(f1: Form, f2: Form) extends Form
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
case class Says(p: String, f: Form) extends Form
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
case class And(f1: Form, f2: Form) extends Form
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
case class Or(f1: Form, f2: Form) extends Form
|
135
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
case class Sends(p: String, q: String, f: Form) extends Form
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
case class Enc(f1: Form, f2: Form) extends Form
|
131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
case class Judgement(gamma: Set[Form], f: Form) {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
def lhs = gamma
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
def rhs = f
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
// some syntactic sugar
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
implicit def FormOps(f1: Form) = new {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
def -> (f2: Form) = Imp(f1, f2)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
implicit def StringOps(p: String) = new {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
def says (f: Form) = Says(p, f)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
implicit def SetFormOps(gamma: Set[Form]) = new {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
def |- (f: Form) : Judgement = Judgement(gamma, f)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
val Admin = "Admin"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
val Bob = "Bob"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
val Del = Pred("del_file", Nil)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
val Gamma: Set[Form] =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
Set( (Admin says Del) -> Del,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
Admin says ((Bob says Del) -> Del),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
Bob says Del )
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
val goal = Gamma |- Del // request: provable or not?
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
def partitions[A](s: Set[A]): Set[(A, Set[A])] =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
s.map (e => (e, s - e))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
def prove(j: Judgement, sc: () => Unit) : Unit = {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
if (j.lhs.contains(j.rhs)) sc () // Axiom rule
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
else {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
prove1(j, sc);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
for ((f, lhs_rest) <- partitions(j.lhs)) prove2(f, lhs_rest, j.rhs, sc)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
def prove1(j: Judgement, sc: () => Unit) : Unit =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
j.rhs match {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
case True => sc ()
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
case False => ()
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc)
|
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
case Says(p, Enc(f1, f2)) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
prove(j.lhs |- Says(p, f1),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
() => prove(j.lhs |- Says(p, f2), sc))
|
131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
case Says(p, f1) => prove(j.lhs |- f1, sc)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
case Or(f1, f2) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
{ prove(j.lhs |- f1, sc);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
prove(j.lhs |- f2, sc) }
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
case And(f1, f2) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
73 |
prove(j.lhs |- f1,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
() => prove(j.lhs |- f2, sc))
|
135
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
case Sends(p, q, f) => prove(j.lhs + (p says f) |- (q says f), sc)
|
131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
76 |
case _ => ()
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
77 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
78 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
79 |
def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
80 |
f match {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
81 |
case True => prove(lhs_rest |- rhs, sc)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
82 |
case False => sc ()
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
case And(f1, f2) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
84 |
prove(lhs_rest + f1 + f2 |- rhs, sc)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
85 |
case Imp(f1, f2) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
86 |
prove(lhs_rest |- f1,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
87 |
() => prove(lhs_rest + f2 |- rhs, sc))
|
135
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
88 |
case Sends(p, q, f) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
prove(lhs_rest |- (p says f),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
() => prove(lhs_rest + (q says f) |- rhs, sc))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
case Enc(f1, f2) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
92 |
prove(lhs_rest |- f1,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
() => prove(lhs_rest + f2 |- rhs, sc))
|
131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
94 |
case Or(f1, f2) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
95 |
prove(lhs_rest + f1 |- rhs,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
96 |
() => prove(lhs_rest + f2 |- rhs, sc))
|
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
case Says(p, Enc(f1, f2)) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
prove(lhs_rest |- Says(p, f2),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
99 |
() => prove(lhs_rest + Says(p, f1) |- rhs, sc))
|
131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
100 |
case Says(p, Imp(f1, f2)) =>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
prove(lhs_rest |- Says(p, f1),
|
135
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
102 |
() => prove(lhs_rest + Says(p, f2) |- rhs, sc))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
103 |
|
131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
104 |
case _ => ()
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
105 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
106 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
107 |
// function that calls prove and returns immediately once a proof is found
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
108 |
def run (j : Judgement) : Unit = {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
109 |
def sc () = { println ("Yes!"); throw new Exception }
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
Try(prove(j, sc)) getOrElse ()
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
112 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
113 |
run (goal)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
114 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
run (Set[Form]() |- False -> Del)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
116 |
run (Set[Form]() |- True -> Del)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
117 |
run (Set[Form]() |- Del -> True)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
118 |
run (Set[Form]() |- Del -> Del)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
119 |
run (Set[Form]() |- Del -> Or(False, Del))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
120 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
121 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
122 |
val Gamma1 : Set[Form] =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
123 |
Set( Admin says ((Bob says Del) -> Del),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
124 |
Bob says Del )
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
125 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
126 |
val goal1 = Gamma1 |- Del // not provable
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
127 |
run (goal1)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
128 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
129 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
130 |
val f1 = "P" says Pred("F1", Nil)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
131 |
val f2 = "Q" says Pred("F2", Nil)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
132 |
run (Set[Form](And(f1, f2)) |- And(f2, f1))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
133 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
134 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
135 |
val Chr = "Christian"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
136 |
val HoD = "Peter"
|
132
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
137 |
val Email = Pred("may_obtain_email", List(Const(Chr)))
|
131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
138 |
val AtLib = Pred("is_at_library", List(Const(Chr)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
139 |
val Chr_Staff = Pred("is_staff", List(Const(Chr)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
140 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
141 |
val Policy_HoD = (HoD says Chr_Staff) -> Chr_Staff
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
142 |
val Policy_Lib = And(Chr_Staff, AtLib) -> Email
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
143 |
val HoD_says = HoD says Chr_Staff
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
144 |
|
132
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
run (Set[Form](AtLib, Policy_HoD, Policy_Lib) |- Email)
|
131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
146 |
|
135
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
147 |
println("Server Example")
|
131
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
148 |
|
135
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
149 |
def Connect(p: String, q: String) : Form =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
150 |
Pred("Connect", List(Var(p), Var(q)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
151 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
152 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
153 |
val A = "A"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
154 |
val B = "B"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
155 |
val S = "S"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
156 |
val CAB = Connect(A, B)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
157 |
val Msg = Pred("Msg", Nil)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
158 |
val KAS = Pred("Kas", Nil)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
159 |
val KBS = Pred("Kbs", Nil)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
160 |
val KAB = Pred("Kab", Nil)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
161 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
162 |
val Gamma_big : Set[Form] =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
163 |
Set( A says CAB,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
164 |
Sends(A, S, CAB),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
165 |
S says (CAB -> Enc(KAB, KAS)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
166 |
S says (CAB -> Enc(Enc(KAB, KBS), KAS)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
167 |
Sends(S, A, Enc(KAB, KAS)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
168 |
Sends(S, A, Enc(Enc(KAB, KBS), KAS)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
169 |
Sends(A, B, Enc(KAB, KBS)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
170 |
Sends(A, B, Enc(Msg, KAB)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
171 |
A says KAS,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
172 |
B says KBS,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
173 |
S says KAS,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
174 |
A says (Enc(Msg, KAB))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
175 |
)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
176 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
177 |
run (Gamma_big |- (B says Msg))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
178 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
179 |
|