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