89 |
89 |
90 |
90 |
91 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
91 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
92 sends messages containing X! **) |
92 sends messages containing X! **) |
93 |
93 |
94 (*Spy never sees another agent's shared key! (unless it is leaked at start)*) |
94 (*Spy never sees another agent's shared key! (unless it's lost at start)*) |
95 goal thy |
95 goal thy |
96 "!!evs. [| evs : yahalom lost; A ~: lost |] \ |
96 "!!evs. evs : yahalom lost \ |
97 \ ==> Key (shrK A) ~: parts (sees lost Spy evs)"; |
97 \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; |
98 by (parts_induct_tac 1); |
98 by (parts_induct_tac 1); |
99 by (Auto_tac()); |
99 by (Auto_tac()); |
100 qed "Spy_not_see_shrK"; |
100 qed "Spy_see_shrK"; |
101 |
101 Addsimps [Spy_see_shrK]; |
102 bind_thm ("Spy_not_analz_shrK", |
102 |
103 [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD); |
103 goal thy |
104 |
104 "!!evs. evs : yahalom lost \ |
105 Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK]; |
105 \ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; |
106 |
106 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
107 (*We go to some trouble to preserve R in the 3rd and 4th subgoals |
107 qed "Spy_analz_shrK"; |
108 As usual fast_tac cannot be used because it uses the equalities too soon*) |
108 Addsimps [Spy_analz_shrK]; |
109 val major::prems = |
109 |
110 goal thy "[| Key (shrK A) : parts (sees lost Spy evs); \ |
110 goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
111 \ evs : yahalom lost; \ |
111 \ evs : yahalom lost |] ==> A:lost"; |
112 \ A:lost ==> R \ |
112 by (fast_tac (!claset addDs [Spy_see_shrK]) 1); |
113 \ |] ==> R"; |
113 qed "Spy_see_shrK_D"; |
114 by (rtac ccontr 1); |
114 |
115 by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1); |
115 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
116 by (swap_res_tac prems 2); |
116 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
117 by (ALLGOALS (fast_tac (!claset addIs prems))); |
117 |
118 qed "Spy_see_shrK_E"; |
118 |
119 |
119 (*Nobody can have used non-existent keys!*) |
120 bind_thm ("Spy_analz_shrK_E", |
120 goal thy "!!evs. evs : yahalom lost ==> \ |
121 analz_subset_parts RS subsetD RS Spy_see_shrK_E); |
121 \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; |
122 |
|
123 AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E]; |
|
124 |
|
125 |
|
126 (*** Future keys can't be seen or used! ***) |
|
127 |
|
128 (*Nobody can have SEEN keys that will be generated in the future. *) |
|
129 goal thy "!!i. evs : yahalom lost ==> \ |
|
130 \ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)"; |
|
131 by (parts_induct_tac 1); |
122 by (parts_induct_tac 1); |
132 by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE] |
123 (*YM4: Key K is not fresh!*) |
133 addDs [impOfSubs analz_subset_parts, |
124 by (fast_tac (!claset addSEs sees_Spy_partsEs) 3); |
134 impOfSubs parts_insert_subset_Un, |
125 (*YM3*) |
135 Suc_leD] |
126 by (fast_tac (!claset addss (!simpset)) 2); |
136 addss (!simpset)))); |
127 (*Fake*) |
137 qed_spec_mp "new_keys_not_seen"; |
128 by (best_tac |
138 Addsimps [new_keys_not_seen]; |
129 (!claset addIs [impOfSubs analz_subset_parts] |
139 |
130 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
140 (*Variant: old messages must contain old keys!*) |
131 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
141 goal thy |
132 addss (!simpset)) 1); |
142 "!!evs. [| Says A B X : set_of_list evs; \ |
|
143 \ Key (newK i) : parts {X}; \ |
|
144 \ evs : yahalom lost \ |
|
145 \ |] ==> i < length evs"; |
|
146 by (rtac ccontr 1); |
|
147 by (dtac leI 1); |
|
148 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] |
|
149 addIs [impOfSubs parts_mono]) 1); |
|
150 qed "Says_imp_old_keys"; |
|
151 |
|
152 |
|
153 (*Nobody can have USED keys that will be generated in the future. |
|
154 ...very like new_keys_not_seen*) |
|
155 goal thy "!!i. evs : yahalom lost ==> \ |
|
156 \ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))"; |
|
157 by (parts_induct_tac 1); |
|
158 by (dtac YM4_Key_parts_sees_Spy 5); |
|
159 (*YM1, YM2 and YM3*) |
|
160 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2])); |
|
161 (*Fake and Oops: these messages send unknown (X) components*) |
|
162 by (EVERY |
|
163 (map (fast_tac |
|
164 (!claset addDs [impOfSubs analz_subset_parts, |
|
165 impOfSubs (analz_subset_parts RS keysFor_mono), |
|
166 impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
|
167 Suc_leD] |
|
168 addss (!simpset))) [3,1])); |
|
169 (*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*) |
|
170 by (fast_tac |
|
171 (!claset addSEs partsEs |
|
172 addSDs [Says_imp_sees_Spy RS parts.Inj] |
|
173 addEs [new_keys_not_seen RSN(2,rev_notE)] |
|
174 addDs [Suc_leD]) 1); |
|
175 qed_spec_mp "new_keys_not_used"; |
133 qed_spec_mp "new_keys_not_used"; |
176 |
134 |
177 bind_thm ("new_keys_not_analzd", |
135 bind_thm ("new_keys_not_analzd", |
178 [analz_subset_parts RS keysFor_mono, |
136 [analz_subset_parts RS keysFor_mono, |
179 new_keys_not_used] MRS contra_subsetD); |
137 new_keys_not_used] MRS contra_subsetD); |
182 |
140 |
183 |
141 |
184 (*Describes the form of K when the Server sends this message. Useful for |
142 (*Describes the form of K when the Server sends this message. Useful for |
185 Oops as well as main secrecy property.*) |
143 Oops as well as main secrecy property.*) |
186 goal thy |
144 goal thy |
187 "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \ |
145 "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \ |
188 \ : set_of_list evs; \ |
146 \ : set_of_list evs; \ |
189 \ evs : yahalom lost |] \ |
147 \ evs : yahalom lost |] \ |
190 \ ==> (EX i. K = Key(newK i)) & A ~= B"; |
148 \ ==> K ~: range shrK & A ~= B"; |
191 by (etac rev_mp 1); |
149 by (etac rev_mp 1); |
192 by (etac yahalom.induct 1); |
150 by (etac yahalom.induct 1); |
193 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
151 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
194 qed "Says_Server_message_form"; |
152 qed "Says_Server_message_form"; |
195 |
153 |
196 |
154 |
197 (*For proofs involving analz. We again instantiate the variable to "lost".*) |
155 (*For proofs involving analz. We again instantiate the variable to "lost".*) |
198 val analz_Fake_tac = |
156 val analz_Fake_tac = |
199 dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN |
157 dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN |
200 forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN |
158 forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN |
201 assume_tac 7 THEN Full_simp_tac 7 THEN |
159 assume_tac 7 THEN |
202 REPEAT ((eresolve_tac [exE,conjE] ORELSE' hyp_subst_tac) 7); |
160 REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7); |
203 |
161 |
204 |
162 |
205 (**** |
163 (**** |
206 The following is to prove theorems of the form |
164 The following is to prove theorems of the form |
207 |
165 |
208 Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==> |
166 Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> |
209 Key K : analz (sees lost Spy evs) |
167 Key K : analz (sees lost Spy evs) |
210 |
168 |
211 A more general formula must be proved inductively. |
169 A more general formula must be proved inductively. |
212 |
170 |
213 ****) |
171 ****) |
214 |
172 |
215 (** Session keys are not used to encrypt other session keys **) |
173 (** Session keys are not used to encrypt other session keys **) |
216 |
174 |
217 goal thy |
175 goal thy |
218 "!!evs. evs : yahalom lost ==> \ |
176 "!!evs. evs : yahalom lost ==> \ |
219 \ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ |
177 \ ALL K KK. KK <= Compl (range shrK) --> \ |
220 \ (K : newK``E | Key K : analz (sees lost Spy evs))"; |
178 \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ |
|
179 \ (K : KK | Key K : analz (sees lost Spy evs))"; |
221 by (etac yahalom.induct 1); |
180 by (etac yahalom.induct 1); |
222 by analz_Fake_tac; |
181 by analz_Fake_tac; |
223 by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma])); |
182 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
224 by (ALLGOALS (*Takes 11 secs*) |
183 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
225 (asm_simp_tac |
184 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
226 (!simpset addsimps [Un_assoc RS sym, |
185 (*Base*) |
227 insert_Key_singleton, insert_Key_image, pushKey_newK] |
186 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
228 setloop split_tac [expand_if]))); |
|
229 (*YM4, Fake*) |
187 (*YM4, Fake*) |
230 by (EVERY (map spy_analz_tac [4, 2])); |
188 by (REPEAT (spy_analz_tac 1)); |
231 (*Oops, YM3, Base*) |
189 qed_spec_mp "analz_image_freshK"; |
232 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); |
|
233 qed_spec_mp "analz_image_newK"; |
|
234 |
190 |
235 goal thy |
191 goal thy |
236 "!!evs. evs : yahalom lost ==> \ |
192 "!!evs. [| evs : yahalom lost; KAB ~: range shrK |] ==> \ |
237 \ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) = \ |
193 \ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ |
238 \ (K = newK i | Key K : analz (sees lost Spy evs))"; |
194 \ (K = KAB | Key K : analz (sees lost Spy evs))"; |
239 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
195 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
240 insert_Key_singleton]) 1); |
196 qed "analz_insert_freshK"; |
241 by (Fast_tac 1); |
|
242 qed "analz_insert_Key_newK"; |
|
243 |
197 |
244 |
198 |
245 (*** The Key K uniquely identifies the Server's message. **) |
199 (*** The Key K uniquely identifies the Server's message. **) |
246 |
200 |
247 goal thy |
201 goal thy |
254 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
208 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
255 by (Step_tac 1); |
209 by (Step_tac 1); |
256 (*Remaining case: YM3*) |
210 (*Remaining case: YM3*) |
257 by (expand_case_tac "K = ?y" 1); |
211 by (expand_case_tac "K = ?y" 1); |
258 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
212 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
259 (*...we assume X is a very new message, and handle this case by contradiction*) |
213 (*...we assume X is a recent message and handle this case by contradiction*) |
260 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] |
214 by (fast_tac (!claset addSEs sees_Spy_partsEs |
261 delrules [conjI] (*prevent split-up into 4 subgoals*) |
215 delrules [conjI] (*prevent split-up into 4 subgoals*) |
262 addss (!simpset addsimps [parts_insertI])) 1); |
216 addss (!simpset addsimps [parts_insertI])) 1); |
263 val lemma = result(); |
217 val lemma = result(); |
264 |
218 |
265 goal thy |
219 goal thy |
288 \ Key K ~: analz (sees lost Spy evs)"; |
242 \ Key K ~: analz (sees lost Spy evs)"; |
289 by (etac yahalom.induct 1); |
243 by (etac yahalom.induct 1); |
290 by analz_Fake_tac; |
244 by analz_Fake_tac; |
291 by (ALLGOALS |
245 by (ALLGOALS |
292 (asm_simp_tac |
246 (asm_simp_tac |
293 (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] |
247 (!simpset addsimps [not_parts_not_analz, analz_insert_freshK] |
294 setloop split_tac [expand_if]))); |
248 setloop split_tac [expand_if]))); |
295 (*YM3*) |
249 (*YM3*) |
296 by (fast_tac (!claset addIs [parts_insertI] |
250 by (fast_tac (!claset delrules [impCE] |
297 addEs [Says_imp_old_keys RS less_irrefl] |
251 addSEs sees_Spy_partsEs |
298 addss (!simpset)) 2); |
252 addIs [impOfSubs analz_subset_parts] |
|
253 addss (!simpset addsimps [parts_insert2])) 2); |
299 (*OR4, Fake*) |
254 (*OR4, Fake*) |
300 by (REPEAT_FIRST spy_analz_tac); |
255 by (REPEAT_FIRST spy_analz_tac); |
301 (*Oops*) |
256 (*Oops*) |
302 by (fast_tac (!claset delrules [disjE] |
257 by (fast_tac (!claset delrules [disjE] |
303 addDs [unique_session_keys] |
258 addDs [unique_session_keys] |
306 |
261 |
307 |
262 |
308 (*Final version: Server's message in the most abstract form*) |
263 (*Final version: Server's message in the most abstract form*) |
309 goal thy |
264 goal thy |
310 "!!evs. [| Says Server A \ |
265 "!!evs. [| Says Server A \ |
311 \ {|NB, Crypt (shrK A) {|Agent B, K, NA|}, \ |
266 \ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \ |
312 \ Crypt (shrK B) {|NB, K, Agent A|}|} \ |
267 \ Crypt (shrK B) {|NB, Key K, Agent A|}|} \ |
313 \ : set_of_list evs; \ |
268 \ : set_of_list evs; \ |
314 \ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \ |
269 \ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \ |
315 \ A ~: lost; B ~: lost; evs : yahalom lost |] \ |
270 \ A ~: lost; B ~: lost; evs : yahalom lost |] \ |
316 \ ==> K ~: analz (sees lost Spy evs)"; |
271 \ ==> Key K ~: analz (sees lost Spy evs)"; |
317 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
272 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
318 by (fast_tac (!claset addSEs [lemma]) 1); |
273 by (fast_tac (!claset addSEs [lemma]) 1); |
319 qed "Spy_not_see_encrypted_key"; |
274 qed "Spy_not_see_encrypted_key"; |
320 |
275 |
321 |
276 |
322 goal thy |
277 goal thy |
323 "!!evs. [| C ~: {A,B,Server}; \ |
278 "!!evs. [| C ~: {A,B,Server}; \ |
324 \ Says Server A \ |
279 \ Says Server A \ |
325 \ {|NB, Crypt (shrK A) {|Agent B, K, NA|}, \ |
280 \ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \ |
326 \ Crypt (shrK B) {|NB, K, Agent A|}|} \ |
281 \ Crypt (shrK B) {|NB, Key K, Agent A|}|} \ |
327 \ : set_of_list evs; \ |
282 \ : set_of_list evs; \ |
328 \ Says A Spy {|NA, NB, K|} ~: set_of_list evs; \ |
283 \ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \ |
329 \ A ~: lost; B ~: lost; evs : yahalom lost |] \ |
284 \ A ~: lost; B ~: lost; evs : yahalom lost |] \ |
330 \ ==> K ~: analz (sees lost C evs)"; |
285 \ ==> Key K ~: analz (sees lost C evs)"; |
331 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); |
286 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); |
332 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); |
287 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); |
333 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); |
288 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); |
334 by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD]))); |
289 by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD]))); |
335 qed "Agent_not_see_encrypted_key"; |
290 qed "Agent_not_see_encrypted_key"; |