42 |
42 |
43 |
43 |
44 (** For reasoning about the encrypted portion of messages **) |
44 (** For reasoning about the encrypted portion of messages **) |
45 |
45 |
46 goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \ |
46 goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \ |
47 \ X : analz (sees Spy evs)"; |
47 \ X : analz (spies evs)"; |
48 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
48 by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1); |
49 qed "OR4_analz_sees_Spy"; |
49 qed "OR4_analz_spies"; |
50 |
50 |
51 goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \ |
51 goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \ |
52 \ : set evs ==> K : parts (sees Spy evs)"; |
52 \ : set evs ==> K : parts (spies evs)"; |
53 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
53 by (blast_tac (!claset addSEs spies_partsEs) 1); |
54 qed "Oops_parts_sees_Spy"; |
54 qed "Oops_parts_spies"; |
55 |
55 |
56 (*OR4_analz_sees_Spy lets us treat those cases using the same |
56 (*OR4_analz_spies lets us treat those cases using the same |
57 argument as for the Fake case. This is possible for most, but not all, |
57 argument as for the Fake case. This is possible for most, but not all, |
58 proofs, since Fake messages originate from the Spy. *) |
58 proofs, since Fake messages originate from the Spy. *) |
59 |
59 |
60 bind_thm ("OR4_parts_sees_Spy", |
60 bind_thm ("OR4_parts_spies", |
61 OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
61 OR4_analz_spies RS (impOfSubs analz_subset_parts)); |
62 |
62 |
63 (*For proving the easier theorems about X ~: parts (sees Spy evs).*) |
63 (*For proving the easier theorems about X ~: parts (spies evs).*) |
64 fun parts_induct_tac i = |
64 fun parts_induct_tac i = |
65 etac otway.induct i THEN |
65 etac otway.induct i THEN |
66 forward_tac [Oops_parts_sees_Spy] (i+6) THEN |
66 forward_tac [Oops_parts_spies] (i+6) THEN |
67 forward_tac [OR4_parts_sees_Spy] (i+5) THEN |
67 forward_tac [OR4_parts_spies] (i+5) THEN |
68 prove_simple_subgoals_tac i; |
68 prove_simple_subgoals_tac i; |
69 |
69 |
70 |
70 |
71 (** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY |
71 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
72 sends messages containing X! **) |
72 sends messages containing X! **) |
73 |
73 |
74 (*Spy never sees another agent's shared key! (unless it's lost at start)*) |
74 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
75 goal thy |
75 goal thy |
76 "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)"; |
76 "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
77 by (parts_induct_tac 1); |
77 by (parts_induct_tac 1); |
78 by (Fake_parts_insert_tac 1); |
78 by (Fake_parts_insert_tac 1); |
79 by (Blast_tac 1); |
79 by (Blast_tac 1); |
80 qed "Spy_see_shrK"; |
80 qed "Spy_see_shrK"; |
81 Addsimps [Spy_see_shrK]; |
81 Addsimps [Spy_see_shrK]; |
82 |
82 |
83 goal thy |
83 goal thy |
84 "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)"; |
84 "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
85 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
85 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
86 qed "Spy_analz_shrK"; |
86 qed "Spy_analz_shrK"; |
87 Addsimps [Spy_analz_shrK]; |
87 Addsimps [Spy_analz_shrK]; |
88 |
88 |
89 goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \ |
89 goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad"; |
90 \ evs : otway |] ==> A:lost"; |
|
91 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
90 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
92 qed "Spy_see_shrK_D"; |
91 qed "Spy_see_shrK_D"; |
93 |
92 |
94 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
93 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
95 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
94 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
96 |
95 |
97 |
96 |
98 (*Nobody can have used non-existent keys!*) |
97 (*Nobody can have used non-existent keys!*) |
99 goal thy "!!evs. evs : otway ==> \ |
98 goal thy "!!evs. evs : otway ==> \ |
100 \ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))"; |
99 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
101 by (parts_induct_tac 1); |
100 by (parts_induct_tac 1); |
102 (*Fake*) |
101 (*Fake*) |
103 by (best_tac |
102 by (best_tac |
104 (!claset addIs [impOfSubs analz_subset_parts] |
103 (!claset addIs [impOfSubs analz_subset_parts] |
105 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
104 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
156 |
155 |
157 (*The equality makes the induction hypothesis easier to apply*) |
156 (*The equality makes the induction hypothesis easier to apply*) |
158 goal thy |
157 goal thy |
159 "!!evs. evs : otway ==> \ |
158 "!!evs. evs : otway ==> \ |
160 \ ALL K KK. KK <= Compl (range shrK) --> \ |
159 \ ALL K KK. KK <= Compl (range shrK) --> \ |
161 \ (Key K : analz (Key``KK Un (sees Spy evs))) = \ |
160 \ (Key K : analz (Key``KK Un (spies evs))) = \ |
162 \ (K : KK | Key K : analz (sees Spy evs))"; |
161 \ (K : KK | Key K : analz (spies evs))"; |
163 by (etac otway.induct 1); |
162 by (etac otway.induct 1); |
164 by analz_sees_tac; |
163 by analz_spies_tac; |
165 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
164 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
166 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
165 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
167 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
166 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
168 (*Fake*) |
167 (*Fake*) |
169 by (spy_analz_tac 2); |
168 by (spy_analz_tac 2); |
221 |
220 |
222 (**** Authenticity properties relating to NA ****) |
221 (**** Authenticity properties relating to NA ****) |
223 |
222 |
224 (*If the encrypted message appears then it originated with the Server!*) |
223 (*If the encrypted message appears then it originated with the Server!*) |
225 goal thy |
224 goal thy |
226 "!!evs. [| A ~: lost; evs : otway |] \ |
225 "!!evs. [| A ~: bad; evs : otway |] \ |
227 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \ |
226 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \ |
228 \ : parts (sees Spy evs) \ |
|
229 \ --> (EX NB. Says Server B \ |
227 \ --> (EX NB. Says Server B \ |
230 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
228 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
231 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
229 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
232 \ : set evs)"; |
230 \ : set evs)"; |
233 by (parts_induct_tac 1); |
231 by (parts_induct_tac 1); |
241 (*Corollary: if A receives B's OR4 message then it originated with the Server. |
239 (*Corollary: if A receives B's OR4 message then it originated with the Server. |
242 Freshness may be inferred from nonce NA.*) |
240 Freshness may be inferred from nonce NA.*) |
243 goal thy |
241 goal thy |
244 "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ |
242 "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ |
245 \ : set evs; \ |
243 \ : set evs; \ |
246 \ A ~: lost; evs : otway |] \ |
244 \ A ~: bad; evs : otway |] \ |
247 \ ==> EX NB. Says Server B \ |
245 \ ==> EX NB. Says Server B \ |
248 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
246 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
249 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
247 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
250 \ : set evs"; |
248 \ : set evs"; |
251 by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] |
249 by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] |
252 addEs sees_Spy_partsEs) 1); |
250 addEs spies_partsEs) 1); |
253 qed "A_trusts_OR4"; |
251 qed "A_trusts_OR4"; |
254 |
252 |
255 |
253 |
256 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
254 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
257 Does not in itself guarantee security: an attack could violate |
255 Does not in itself guarantee security: an attack could violate |
258 the premises, e.g. by having A=Spy **) |
256 the premises, e.g. by having A=Spy **) |
259 |
257 |
260 goal thy |
258 goal thy |
261 "!!evs. [| A ~: lost; B ~: lost; evs : otway |] \ |
259 "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \ |
262 \ ==> Says Server B \ |
260 \ ==> Says Server B \ |
263 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
261 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
264 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
262 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
265 \ : set evs --> \ |
263 \ : set evs --> \ |
266 \ Says B Spy {|NA, NB, Key K|} ~: set evs --> \ |
264 \ Says B Spy {|NA, NB, Key K|} ~: set evs --> \ |
267 \ Key K ~: analz (sees Spy evs)"; |
265 \ Key K ~: analz (spies evs)"; |
268 by (etac otway.induct 1); |
266 by (etac otway.induct 1); |
269 by analz_sees_tac; |
267 by analz_spies_tac; |
270 by (ALLGOALS |
268 by (ALLGOALS |
271 (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] |
269 (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] |
272 addsimps [analz_insert_eq, analz_insert_freshK] |
270 addsimps [analz_insert_eq, analz_insert_freshK] |
273 setloop split_tac [expand_if]))); |
271 setloop split_tac [expand_if]))); |
274 (*Oops*) |
272 (*Oops*) |
275 by (blast_tac (!claset addSDs [unique_session_keys]) 4); |
273 by (blast_tac (!claset addSDs [unique_session_keys]) 4); |
276 (*OR4*) |
274 (*OR4*) |
277 by (Blast_tac 3); |
275 by (Blast_tac 3); |
278 (*OR3*) |
276 (*OR3*) |
279 by (blast_tac (!claset addSEs sees_Spy_partsEs |
277 by (blast_tac (!claset addSEs spies_partsEs |
280 addIs [impOfSubs analz_subset_parts]) 2); |
278 addIs [impOfSubs analz_subset_parts]) 2); |
281 (*Fake*) |
279 (*Fake*) |
282 by (spy_analz_tac 1); |
280 by (spy_analz_tac 1); |
283 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
281 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
284 |
282 |
286 "!!evs. [| Says Server B \ |
284 "!!evs. [| Says Server B \ |
287 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
285 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
288 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
286 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
289 \ : set evs; \ |
287 \ : set evs; \ |
290 \ Says B Spy {|NA, NB, Key K|} ~: set evs; \ |
288 \ Says B Spy {|NA, NB, Key K|} ~: set evs; \ |
291 \ A ~: lost; B ~: lost; evs : otway |] \ |
289 \ A ~: bad; B ~: bad; evs : otway |] \ |
292 \ ==> Key K ~: analz (sees Spy evs)"; |
290 \ ==> Key K ~: analz (spies evs)"; |
293 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
291 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
294 by (blast_tac (!claset addSEs [lemma]) 1); |
292 by (blast_tac (!claset addSEs [lemma]) 1); |
295 qed "Spy_not_see_encrypted_key"; |
293 qed "Spy_not_see_encrypted_key"; |
296 |
294 |
297 |
295 |
298 (**** Authenticity properties relating to NB ****) |
296 (**** Authenticity properties relating to NB ****) |
299 |
297 |
300 (*If the encrypted message appears then it originated with the Server!*) |
298 (*If the encrypted message appears then it originated with the Server!*) |
301 goal thy |
299 goal thy |
302 "!!evs. [| B ~: lost; evs : otway |] \ |
300 "!!evs. [| B ~: bad; evs : otway |] \ |
303 \ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \ |
301 \ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \ |
304 \ : parts (sees Spy evs) \ |
|
305 \ --> (EX NA. Says Server B \ |
302 \ --> (EX NA. Says Server B \ |
306 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
303 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
307 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
304 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
308 \ : set evs)"; |
305 \ : set evs)"; |
309 by (parts_induct_tac 1); |
306 by (parts_induct_tac 1); |
315 |
312 |
316 |
313 |
317 (*Guarantee for B: if it gets a well-formed certificate then the Server |
314 (*Guarantee for B: if it gets a well-formed certificate then the Server |
318 has sent the correct message in round 3.*) |
315 has sent the correct message in round 3.*) |
319 goal thy |
316 goal thy |
320 "!!evs. [| B ~: lost; evs : otway; \ |
317 "!!evs. [| B ~: bad; evs : otway; \ |
321 \ Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
318 \ Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
322 \ : set evs |] \ |
319 \ : set evs |] \ |
323 \ ==> EX NA. Says Server B \ |
320 \ ==> EX NA. Says Server B \ |
324 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
321 \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ |
325 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
322 \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ |
326 \ : set evs"; |
323 \ : set evs"; |
327 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] |
324 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] |
328 addEs sees_Spy_partsEs) 1); |
325 addEs spies_partsEs) 1); |
329 qed "B_trusts_OR3"; |
326 qed "B_trusts_OR3"; |