1 (* Title: HOL/Auth/Event |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 *) |
|
6 |
|
7 AddIffs [Spy_in_bad, Server_not_bad]; |
|
8 |
|
9 Addsimps [knows_Cons, used_Cons]; |
|
10 |
|
11 (**** Function "knows" ****) |
|
12 |
|
13 (** Simplifying parts (insert X (knows Spy evs)) |
|
14 = parts {X} Un parts (knows Spy evs) -- since general case loops*) |
|
15 |
|
16 bind_thm ("parts_insert_knows_Spy", |
|
17 parts_insert |> |
|
18 read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]); |
|
19 |
|
20 |
|
21 Goal "P(event_case sf gf nf ev) = \ |
|
22 \ ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \ |
|
23 \ (ALL A X. ev = Gets A X --> P(gf A X)) & \ |
|
24 \ (ALL A X. ev = Notes A X --> P(nf A X)))"; |
|
25 by (induct_tac "ev" 1); |
|
26 by Auto_tac; |
|
27 qed "expand_event_case"; |
|
28 |
|
29 Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"; |
|
30 by (Simp_tac 1); |
|
31 qed "knows_Spy_Says"; |
|
32 |
|
33 (*The point of letting the Spy see "bad" agents' notes is to prevent |
|
34 redundant case-splits on whether A=Spy and whether A:bad*) |
|
35 Goal "knows Spy (Notes A X # evs) = \ |
|
36 \ (if A:bad then insert X (knows Spy evs) else knows Spy evs)"; |
|
37 by (Simp_tac 1); |
|
38 qed "knows_Spy_Notes"; |
|
39 |
|
40 Goal "knows Spy (Gets A X # evs) = knows Spy evs"; |
|
41 by (Simp_tac 1); |
|
42 qed "knows_Spy_Gets"; |
|
43 |
|
44 Goal "knows Spy evs <= knows Spy (Says A B X # evs)"; |
|
45 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
|
46 qed "knows_Spy_subset_knows_Spy_Says"; |
|
47 |
|
48 Goal "knows Spy evs <= knows Spy (Notes A X # evs)"; |
|
49 by (Simp_tac 1); |
|
50 by (Fast_tac 1); |
|
51 qed "knows_Spy_subset_knows_Spy_Notes"; |
|
52 |
|
53 Goal "knows Spy evs <= knows Spy (Gets A X # evs)"; |
|
54 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
|
55 qed "knows_Spy_subset_knows_Spy_Gets"; |
|
56 |
|
57 (*Spy sees what is sent on the traffic*) |
|
58 Goal "Says A B X : set evs --> X : knows Spy evs"; |
|
59 by (induct_tac "evs" 1); |
|
60 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
|
61 qed_spec_mp "Says_imp_knows_Spy"; |
|
62 |
|
63 Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs"; |
|
64 by (induct_tac "evs" 1); |
|
65 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
|
66 qed_spec_mp "Notes_imp_knows_Spy"; |
|
67 |
|
68 |
|
69 (*Use with addSEs to derive contradictions from old Says events containing |
|
70 items known to be fresh*) |
|
71 val knows_Spy_partsEs = make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs; |
|
72 |
|
73 Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets]; |
|
74 |
|
75 |
|
76 (*Begin lemmas about agents' knowledge*) |
|
77 |
|
78 Goal "knows A (Says A B X # evs) = insert X (knows A evs)"; |
|
79 by (Simp_tac 1); |
|
80 qed "knows_Says"; |
|
81 |
|
82 Goal "knows A (Notes A X # evs) = insert X (knows A evs)"; |
|
83 by (Simp_tac 1); |
|
84 qed "knows_Notes"; |
|
85 |
|
86 Goal "A ~= Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"; |
|
87 by (Simp_tac 1); |
|
88 qed "knows_Gets"; |
|
89 |
|
90 |
|
91 Goal "knows A evs <= knows A (Says A B X # evs)"; |
|
92 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
|
93 qed "knows_subset_knows_Says"; |
|
94 |
|
95 Goal "knows A evs <= knows A (Notes A X # evs)"; |
|
96 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
|
97 qed "knows_subset_knows_Notes"; |
|
98 |
|
99 Goal "knows A evs <= knows A (Gets A X # evs)"; |
|
100 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
|
101 qed "knows_subset_knows_Gets"; |
|
102 |
|
103 (*Agents know what they say*) |
|
104 Goal "Says A B X : set evs --> X : knows A evs"; |
|
105 by (induct_tac "evs" 1); |
|
106 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
|
107 by (Blast_tac 1); |
|
108 qed_spec_mp "Says_imp_knows"; |
|
109 |
|
110 (*Agents know what they note*) |
|
111 Goal "Notes A X : set evs --> X : knows A evs"; |
|
112 by (induct_tac "evs" 1); |
|
113 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
|
114 by (Blast_tac 1); |
|
115 qed_spec_mp "Notes_imp_knows"; |
|
116 |
|
117 (*Agents know what they receive*) |
|
118 Goal "A ~= Spy --> Gets A X : set evs --> X : knows A evs"; |
|
119 by (induct_tac "evs" 1); |
|
120 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
|
121 qed_spec_mp "Gets_imp_knows_agents"; |
|
122 |
|
123 |
|
124 (*What agents DIFFERENT FROM Spy know |
|
125 was either said, or noted, or got, or known initially*) |
|
126 Goal "[| X : knows A evs; A ~= Spy |] ==> EX B. \ |
|
127 \ Says A B X : set evs | Gets A X : set evs | Notes A X : set evs | X : initState A"; |
|
128 by (etac rev_mp 1); |
|
129 by (induct_tac "evs" 1); |
|
130 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
|
131 by (Blast_tac 1); |
|
132 qed_spec_mp "knows_imp_Says_Gets_Notes_initState"; |
|
133 |
|
134 (*What the Spy knows -- for the time being -- |
|
135 was either said or noted, or known initially*) |
|
136 Goal "[| X : knows Spy evs |] ==> EX A B. \ |
|
137 \ Says A B X : set evs | Notes A X : set evs | X : initState Spy"; |
|
138 by (etac rev_mp 1); |
|
139 by (induct_tac "evs" 1); |
|
140 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
|
141 by (Blast_tac 1); |
|
142 qed_spec_mp "knows_Spy_imp_Says_Notes_initState"; |
|
143 |
|
144 (*END lemmas about agents' knowledge*) |
|
145 |
|
146 |
|
147 |
|
148 (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****) |
|
149 Delsimps [knows_Cons]; |
|
150 |
|
151 |
|
152 (*** Fresh nonces ***) |
|
153 |
|
154 Goal "parts (knows Spy evs) <= used evs"; |
|
155 by (induct_tac "evs" 1); |
|
156 by (ALLGOALS (asm_simp_tac |
|
157 (simpset() addsimps [parts_insert_knows_Spy] |
|
158 addsplits [expand_event_case]))); |
|
159 by (ALLGOALS Blast_tac); |
|
160 qed "parts_knows_Spy_subset_used"; |
|
161 |
|
162 bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used); |
|
163 AddIs [usedI]; |
|
164 |
|
165 Goal "parts (initState B) <= used evs"; |
|
166 by (induct_tac "evs" 1); |
|
167 by (ALLGOALS (asm_simp_tac |
|
168 (simpset() addsimps [parts_insert_knows_Spy] |
|
169 addsplits [expand_event_case]))); |
|
170 by (ALLGOALS Blast_tac); |
|
171 bind_thm ("initState_into_used", impOfSubs (result())); |
|
172 |
|
173 Goal "used (Says A B X # evs) = parts{X} Un used evs"; |
|
174 by (Simp_tac 1); |
|
175 qed "used_Says"; |
|
176 Addsimps [used_Says]; |
|
177 |
|
178 Goal "used (Notes A X # evs) = parts{X} Un used evs"; |
|
179 by (Simp_tac 1); |
|
180 qed "used_Notes"; |
|
181 Addsimps [used_Notes]; |
|
182 |
|
183 Goal "used (Gets A X # evs) = used evs"; |
|
184 by (Simp_tac 1); |
|
185 qed "used_Gets"; |
|
186 Addsimps [used_Gets]; |
|
187 |
|
188 Goal "used [] <= used evs"; |
|
189 by (Simp_tac 1); |
|
190 by (blast_tac (claset() addIs [initState_into_used]) 1); |
|
191 qed "used_nil_subset"; |
|
192 |
|
193 (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****) |
|
194 Delsimps [used_Nil, used_Cons]; |
|
195 |
|
196 |
|
197 (*For proving theorems of the form X ~: analz (knows Spy evs) --> P |
|
198 New events added by induction to "evs" are discarded. Provided |
|
199 this information isn't needed, the proof will be much shorter, since |
|
200 it will omit complicated reasoning about analz.*) |
|
201 val analz_mono_contra_tac = |
|
202 let val analz_impI = read_instantiate_sg (sign_of thy) |
|
203 [("P", "?Y ~: analz (knows Spy ?evs)")] impI; |
|
204 in |
|
205 rtac analz_impI THEN' |
|
206 REPEAT1 o |
|
207 (dresolve_tac |
|
208 [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD, |
|
209 knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD, |
|
210 knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD]) |
|
211 THEN' |
|
212 mp_tac |
|
213 end; |
|
214 |
|
215 fun Reception_tac i = |
|
216 blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj, |
|
217 impOfSubs (parts_insert RS equalityD1), |
|
218 parts_trans, |
|
219 Says_imp_knows_Spy RS analz.Inj, |
|
220 impOfSubs analz_mono, analz_cut] |
|
221 addIs [less_SucI]) i; |
|
222 |
|
223 |
|
224 (*Compatibility for the old "spies" function*) |
|
225 val spies_partsEs = knows_Spy_partsEs; |
|
226 val Says_imp_spies = Says_imp_knows_Spy; |
|
227 val parts_insert_spies = parts_insert_knows_Spy; |
|