295 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
295 frule_tac [6] YM4_parts_knows_Spy, simp_all) |
296 txt{*Fake, YM3*} |
296 txt{*Fake, YM3*} |
297 apply blast+ |
297 apply blast+ |
298 done |
298 done |
299 |
299 |
300 text{*B knows, by the second part of A's message, that the Server distributed |
300 text{*B knows, by the second part of A's message, that the Server |
301 the key quoting nonce NB. This part says nothing about agent names. |
301 distributed the key quoting nonce NB. This part says nothing about |
302 Secrecy of NB is crucial. Note that Nonce NB \<notin> analz(knows Spy evs) must |
302 agent names. Secrecy of NB is crucial. Note that @{term "Nonce NB |
303 be the FIRST antecedent of the induction formula.*} |
303 \<notin> analz(knows Spy evs)"} must be the FIRST antecedent of the |
|
304 induction formula.*} |
|
305 |
304 lemma B_trusts_YM4_newK [rule_format]: |
306 lemma B_trusts_YM4_newK [rule_format]: |
305 "[|Crypt K (Nonce NB) \<in> parts (knows Spy evs); |
307 "[|Crypt K (Nonce NB) \<in> parts (knows Spy evs); |
306 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
308 Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|] |
307 ==> \<exists>A B NA. Says Server A |
309 ==> \<exists>A B NA. Says Server A |
308 {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, |
310 {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, |
390 add: analz_image_freshK_simps split_ifs |
392 add: analz_image_freshK_simps split_ifs |
391 all_conj_distrib ball_conj_distrib |
393 all_conj_distrib ball_conj_distrib |
392 analz_image_freshK fresh_not_KeyWithNonce |
394 analz_image_freshK fresh_not_KeyWithNonce |
393 imp_disj_not1 (*Moves NBa\<noteq>NB to the front*) |
395 imp_disj_not1 (*Moves NBa\<noteq>NB to the front*) |
394 Says_Server_KeyWithNonce) |
396 Says_Server_KeyWithNonce) |
395 txt{*For Oops, simplification proves NBa\<noteq>NB. By Says_Server_KeyWithNonce, |
397 txt{*For Oops, simplification proves @{prop "NBa\<noteq>NB"}. By |
396 we get (~ KeyWithNonce K NB evs); then simplification can apply the |
398 @{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB |
397 induction hypothesis with KK = {K}.*} |
399 evs"}; then simplification can apply the induction hypothesis with |
|
400 @{term "KK = {K}"}.*} |
398 txt{*Fake*} |
401 txt{*Fake*} |
399 apply spy_analz |
402 apply spy_analz |
400 txt{*YM2*} |
403 txt{*YM2*} |
401 apply blast |
404 apply blast |
402 txt{*YM3*} |
405 txt{*YM3*} |
403 apply blast |
406 apply blast |
404 txt{*YM4*} |
407 txt{*YM4*} |
405 apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify) |
408 apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify) |
406 txt{*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB. Previous two steps |
409 txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore |
407 make the next step faster.*} |
410 @{prop "NBa \<noteq> NB"}. Previous two steps make the next step |
|
411 faster.*} |
408 apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad |
412 apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad |
409 dest: analz.Inj |
413 dest: analz.Inj |
410 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI]) |
414 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI]) |
411 done |
415 done |
412 |
416 |
499 apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) |
503 apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) |
500 txt{*LEVEL 7: YM4 and Oops remain*} |
504 txt{*LEVEL 7: YM4 and Oops remain*} |
501 apply (clarify, simp add: all_conj_distrib) |
505 apply (clarify, simp add: all_conj_distrib) |
502 txt{*YM4: key K is visible to Spy, contradicting session key secrecy theorem*} |
506 txt{*YM4: key K is visible to Spy, contradicting session key secrecy theorem*} |
503 txt{*Case analysis on Aa:bad; PROOF FAILED problems |
507 txt{*Case analysis on Aa:bad; PROOF FAILED problems |
504 use Says_unique_NB to identify message components: Aa=A, Ba=B*} |
508 use @{text Says_unique_NB} to identify message components: @{term "Aa=A"}, @{term "Ba=B"}*} |
505 apply (blast dest!: Says_unique_NB analz_shrK_Decrypt |
509 apply (blast dest!: Says_unique_NB analz_shrK_Decrypt |
506 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] |
510 parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] |
507 dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 |
511 dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 |
508 Spy_not_see_encrypted_key) |
512 Spy_not_see_encrypted_key) |
509 txt{*Oops case: if the nonce is betrayed now, show that the Oops event is |
513 txt{*Oops case: if the nonce is betrayed now, show that the Oops event is |
511 apply (clarify, simp add: all_conj_distrib) |
515 apply (clarify, simp add: all_conj_distrib) |
512 apply (frule Says_Server_imp_YM2, assumption) |
516 apply (frule Says_Server_imp_YM2, assumption) |
513 apply (case_tac "NB = NBa") |
517 apply (case_tac "NB = NBa") |
514 txt{*If NB=NBa then all other components of the Oops message agree*} |
518 txt{*If NB=NBa then all other components of the Oops message agree*} |
515 apply (blast dest: Says_unique_NB) |
519 apply (blast dest: Says_unique_NB) |
516 txt{*case NB \<noteq> NBa*} |
520 txt{*case @{prop "NB \<noteq> NBa"}*} |
517 apply (simp add: single_Nonce_secrecy) |
521 apply (simp add: single_Nonce_secrecy) |
518 apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*)) |
522 apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*)) |
519 done |
523 done |
520 |
524 |
521 |
525 |
522 text{*B's session key guarantee from YM4. The two certificates contribute to a |
526 text{*B's session key guarantee from YM4. The two certificates contribute to a |
523 single conclusion about the Server's message. Note that the "Notes Spy" |
527 single conclusion about the Server's message. Note that the "Notes Spy" |
524 assumption must quantify over \<forall>POSSIBLE keys instead of our particular K. |
528 assumption must quantify over @{text \<forall>} POSSIBLE keys instead of our particular K. |
525 If this run is broken and the spy substitutes a certificate containing an |
529 If this run is broken and the spy substitutes a certificate containing an |
526 old key, B has no means of telling.*} |
530 old key, B has no means of telling.*} |
527 lemma B_trusts_YM4: |
531 lemma B_trusts_YM4: |
528 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
532 "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, |
529 Crypt K (Nonce NB)|} \<in> set evs; |
533 Crypt K (Nonce NB)|} \<in> set evs; |