60 def prove1(j: Judgement, sc: () => Unit) : Unit = |
60 def prove1(j: Judgement, sc: () => Unit) : Unit = |
61 j.rhs match { |
61 j.rhs match { |
62 case True => sc () |
62 case True => sc () |
63 case False => () |
63 case False => () |
64 case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) |
64 case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) |
|
65 case Says(p, Enc(f1, f2)) => |
|
66 prove(j.lhs |- Says(p, f1), |
|
67 () => prove(j.lhs |- Says(p, f2), sc)) |
65 case Says(p, f1) => prove(j.lhs |- f1, sc) |
68 case Says(p, f1) => prove(j.lhs |- f1, sc) |
66 case Or(f1, f2) => |
69 case Or(f1, f2) => |
67 { prove(j.lhs |- f1, sc); |
70 { prove(j.lhs |- f1, sc); |
68 prove(j.lhs |- f2, sc) } |
71 prove(j.lhs |- f2, sc) } |
69 case And(f1, f2) => |
72 case And(f1, f2) => |
70 prove(j.lhs |- f1, |
73 prove(j.lhs |- f1, |
71 () => prove(j.lhs |- f2, sc)) |
74 () => prove(j.lhs |- f2, sc)) |
72 case Sends(p, q, f) => prove(j.lhs + (p says f) |- (q says f), sc) |
75 case Sends(p, q, f) => prove(j.lhs + (p says f) |- (q says f), sc) |
73 case Enc(f1, f2) => prove(j.lhs + f1 |- f2, sc) |
|
74 case _ => () |
76 case _ => () |
75 } |
77 } |
76 |
78 |
77 def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = |
79 def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = |
78 f match { |
80 f match { |
90 prove(lhs_rest |- f1, |
92 prove(lhs_rest |- f1, |
91 () => prove(lhs_rest + f2 |- rhs, sc)) |
93 () => prove(lhs_rest + f2 |- rhs, sc)) |
92 case Or(f1, f2) => |
94 case Or(f1, f2) => |
93 prove(lhs_rest + f1 |- rhs, |
95 prove(lhs_rest + f1 |- rhs, |
94 () => prove(lhs_rest + f2 |- rhs, sc)) |
96 () => prove(lhs_rest + f2 |- rhs, sc)) |
|
97 case Says(p, Enc(f1, f2)) => |
|
98 prove(lhs_rest |- Says(p, f2), |
|
99 () => prove(lhs_rest + Says(p, f1) |- rhs, sc)) |
95 case Says(p, Imp(f1, f2)) => |
100 case Says(p, Imp(f1, f2)) => |
96 prove(lhs_rest |- Says(p, f1), |
101 prove(lhs_rest |- Says(p, f1), |
97 () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) |
102 () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) |
98 |
103 |
99 case _ => () |
104 case _ => () |
139 |
144 |
140 run (Set[Form](AtLib, Policy_HoD, Policy_Lib) |- Email) |
145 run (Set[Form](AtLib, Policy_HoD, Policy_Lib) |- Email) |
141 |
146 |
142 println("Server Example") |
147 println("Server Example") |
143 |
148 |
144 val Alice = "Alice" |
|
145 //val Bob = "Bob" -- already defined |
|
146 val Server = "Server" |
|
147 |
|
148 def Connect(p: String, q: String) : Form = |
149 def Connect(p: String, q: String) : Form = |
149 Pred("Connect", List(Var(p), Var(q))) |
150 Pred("Connect", List(Var(p), Var(q))) |
150 |
151 |
151 |
152 |
152 val A = "A" |
153 val A = "A" |