13 case class Pred(s: String, ts: List[Term]) extends Form |
13 case class Pred(s: String, ts: List[Term]) extends Form |
14 case class Imp(f1: Form, f2: Form) extends Form |
14 case class Imp(f1: Form, f2: Form) extends Form |
15 case class Says(p: String, f: Form) extends Form |
15 case class Says(p: String, f: Form) extends Form |
16 case class And(f1: Form, f2: Form) extends Form |
16 case class And(f1: Form, f2: Form) extends Form |
17 case class Or(f1: Form, f2: Form) extends Form |
17 case class Or(f1: Form, f2: Form) extends Form |
|
18 case class Sends(p: String, q: String, f: Form) extends Form |
|
19 case class Enc(f1: Form, f2: Form) extends Form |
18 |
20 |
19 case class Judgement(gamma: Set[Form], f: Form) { |
21 case class Judgement(gamma: Set[Form], f: Form) { |
20 def lhs = gamma |
22 def lhs = gamma |
21 def rhs = f |
23 def rhs = f |
22 } |
24 } |
65 { prove(j.lhs |- f1, sc); |
67 { prove(j.lhs |- f1, sc); |
66 prove(j.lhs |- f2, sc) } |
68 prove(j.lhs |- f2, sc) } |
67 case And(f1, f2) => |
69 case And(f1, f2) => |
68 prove(j.lhs |- f1, |
70 prove(j.lhs |- f1, |
69 () => prove(j.lhs |- f2, sc)) |
71 () => prove(j.lhs |- f2, sc)) |
|
72 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) |
70 case _ => () |
74 case _ => () |
71 } |
75 } |
72 |
76 |
73 def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = |
77 def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = |
74 f match { |
78 f match { |
77 case And(f1, f2) => |
81 case And(f1, f2) => |
78 prove(lhs_rest + f1 + f2 |- rhs, sc) |
82 prove(lhs_rest + f1 + f2 |- rhs, sc) |
79 case Imp(f1, f2) => |
83 case Imp(f1, f2) => |
80 prove(lhs_rest |- f1, |
84 prove(lhs_rest |- f1, |
81 () => prove(lhs_rest + f2 |- rhs, sc)) |
85 () => prove(lhs_rest + f2 |- rhs, sc)) |
|
86 case Sends(p, q, f) => |
|
87 prove(lhs_rest |- (p says f), |
|
88 () => prove(lhs_rest + (q says f) |- rhs, sc)) |
|
89 case Enc(f1, f2) => |
|
90 prove(lhs_rest |- f1, |
|
91 () => prove(lhs_rest + f2 |- rhs, sc)) |
82 case Or(f1, f2) => |
92 case Or(f1, f2) => |
83 prove(lhs_rest + f1 |- rhs, |
93 prove(lhs_rest + f1 |- rhs, |
84 () => prove(lhs_rest + f2 |- rhs, sc)) |
94 () => prove(lhs_rest + f2 |- rhs, sc)) |
85 case Says(p, Imp(f1, f2)) => |
95 case Says(p, Imp(f1, f2)) => |
86 prove(lhs_rest |- Says(p, f1), |
96 prove(lhs_rest |- Says(p, f1), |
87 () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) |
97 () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) |
|
98 |
88 case _ => () |
99 case _ => () |
89 } |
100 } |
90 |
101 |
91 // function that calls prove and returns immediately once a proof is found |
102 // function that calls prove and returns immediately once a proof is found |
92 def run (j : Judgement) : Unit = { |
103 def run (j : Judgement) : Unit = { |
126 val Policy_Lib = And(Chr_Staff, AtLib) -> Email |
137 val Policy_Lib = And(Chr_Staff, AtLib) -> Email |
127 val HoD_says = HoD says Chr_Staff |
138 val HoD_says = HoD says Chr_Staff |
128 |
139 |
129 run (Set[Form](AtLib, Policy_HoD, Policy_Lib) |- Email) |
140 run (Set[Form](AtLib, Policy_HoD, Policy_Lib) |- Email) |
130 |
141 |
|
142 println("Server Example") |
131 |
143 |
|
144 val Alice = "Alice" |
|
145 //val Bob = "Bob" -- already defined |
|
146 val Server = "Server" |
|
147 |
|
148 def Connect(p: String, q: String) : Form = |
|
149 Pred("Connect", List(Var(p), Var(q))) |
|
150 |
|
151 |
|
152 val A = "A" |
|
153 val B = "B" |
|
154 val S = "S" |
|
155 val CAB = Connect(A, B) |
|
156 val Msg = Pred("Msg", Nil) |
|
157 val KAS = Pred("Kas", Nil) |
|
158 val KBS = Pred("Kbs", Nil) |
|
159 val KAB = Pred("Kab", Nil) |
|
160 |
|
161 val Gamma_big : Set[Form] = |
|
162 Set( A says CAB, |
|
163 Sends(A, S, CAB), |
|
164 S says (CAB -> Enc(KAB, KAS)), |
|
165 S says (CAB -> Enc(Enc(KAB, KBS), KAS)), |
|
166 Sends(S, A, Enc(KAB, KAS)), |
|
167 Sends(S, A, Enc(Enc(KAB, KBS), KAS)), |
|
168 Sends(A, B, Enc(KAB, KBS)), |
|
169 Sends(A, B, Enc(Msg, KAB)), |
|
170 A says KAS, |
|
171 B says KBS, |
|
172 S says KAS, |
|
173 A says (Enc(Msg, KAB)) |
|
174 ) |
|
175 |
|
176 run (Gamma_big |- (B says Msg)) |
|
177 |
|
178 |