1 (* Title: HOL/Auth/Event_lemmas |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 *) |
|
6 |
|
7 |
|
8 val knows_Cons = thm "knows_Cons"; |
|
9 val used_Nil = thm "used_Nil"; |
|
10 val used_Cons = thm "used_Cons"; |
|
11 |
|
12 |
|
13 (*Inserted by default but later removed. This declaration lets the file |
|
14 be re-loaded.*) |
|
15 Addsimps [knows_Cons, used_Nil, used_Cons]; |
|
16 |
|
17 (**** Function "knows" ****) |
|
18 |
|
19 (** Simplifying parts (insert X (knows Spy evs)) |
|
20 = parts {X} Un parts (knows Spy evs) -- since general case loops*) |
|
21 |
|
22 bind_thm ("parts_insert_knows_Spy", |
|
23 inst "H" "knows Spy evs" parts_insert); |
|
24 |
|
25 |
|
26 val expand_event_case = thm "event.split"; |
|
27 |
|
28 Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"; |
|
29 by (Simp_tac 1); |
|
30 qed "knows_Spy_Says"; |
|
31 |
|
32 (*The point of letting the Spy see "bad" agents' notes is to prevent |
|
33 redundant case-splits on whether A=Spy and whether A:bad*) |
|
34 Goal "knows Spy (Notes A X # evs) = \ |
|
35 \ (if A:bad then insert X (knows Spy evs) else knows Spy evs)"; |
|
36 by (Simp_tac 1); |
|
37 qed "knows_Spy_Notes"; |
|
38 |
|
39 Goal "knows Spy (Gets A X # evs) = knows Spy evs"; |
|
40 by (Simp_tac 1); |
|
41 qed "knows_Spy_Gets"; |
|
42 |
|
43 Goal "knows Spy evs <= knows Spy (Says A B X # evs)"; |
|
44 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
|
45 qed "knows_Spy_subset_knows_Spy_Says"; |
|
46 |
|
47 Goal "knows Spy evs <= knows Spy (Notes A X # evs)"; |
|
48 by (Simp_tac 1); |
|
49 by (Fast_tac 1); |
|
50 qed "knows_Spy_subset_knows_Spy_Notes"; |
|
51 |
|
52 Goal "knows Spy evs <= knows Spy (Gets A X # evs)"; |
|
53 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
|
54 qed "knows_Spy_subset_knows_Spy_Gets"; |
|
55 |
|
56 (*Spy sees what is sent on the traffic*) |
|
57 Goal "Says A B X : set evs --> X : knows Spy evs"; |
|
58 by (induct_tac "evs" 1); |
|
59 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
|
60 qed_spec_mp "Says_imp_knows_Spy"; |
|
61 |
|
62 Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs"; |
|
63 by (induct_tac "evs" 1); |
|
64 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
|
65 qed_spec_mp "Notes_imp_knows_Spy"; |
|
66 |
|
67 |
|
68 (*Use with addSEs to derive contradictions from old Says events containing |
|
69 items known to be fresh*) |
|
70 bind_thms ("knows_Spy_partsEs", |
|
71 map make_elim [Says_imp_knows_Spy RS parts.Inj, parts.Body]); |
|
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 |
|
202 bind_thms ("analz_mono_contra", |
|
203 [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD, |
|
204 knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD, |
|
205 knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD]); |
|
206 |
|
207 val analz_mono_contra_tac = |
|
208 let val analz_impI = inst "P" "?Y ~: analz (knows Spy ?evs)" impI |
|
209 in |
|
210 rtac analz_impI THEN' |
|
211 REPEAT1 o |
|
212 (dresolve_tac |
|
213 [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD, |
|
214 knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD, |
|
215 knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD]) |
|
216 THEN' |
|
217 mp_tac |
|
218 end; |
|
219 |
|
220 fun Reception_tac i = |
|
221 blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj, |
|
222 impOfSubs (parts_insert RS equalityD1), |
|
223 parts_trans, |
|
224 Says_imp_knows_Spy RS analz.Inj, |
|
225 impOfSubs analz_mono, analz_cut] |
|
226 addIs [less_SucI]) i; |
|
227 |
|
228 |
|
229 (*Compatibility for the old "spies" function*) |
|
230 bind_thms ("spies_partsEs", knows_Spy_partsEs); |
|
231 bind_thm ("Says_imp_spies", Says_imp_knows_Spy); |
|
232 bind_thm ("parts_insert_spies", parts_insert_knows_Spy); |
|