# HG changeset patch # User paulson # Date 1250180350 -3600 # Node ID b269b56b6a145144906ab9c4b19d8a30c610a978 # Parent 7887cb2848bbe6b73fc8489e68601a1c25a9f040 Demonstrations of sledgehammer in protocol proofs. diff -r 7887cb2848bb -r b269b56b6a14 src/HOL/Auth/KerberosIV.thy --- a/src/HOL/Auth/KerberosIV.thy Mon Aug 10 17:00:41 2009 +0200 +++ b/src/HOL/Auth/KerberosIV.thy Thu Aug 13 17:19:10 2009 +0100 @@ -379,6 +379,7 @@ lemma Spy_see_shrK_D [dest!]: "\ Key (shrK A) \ parts (spies evs); evs \ kerbIV \ \ A:bad" by (blast dest: Spy_see_shrK) + lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] text{*Nobody can have used non-existent keys!*} @@ -479,21 +480,7 @@ txt{*K2*} apply (simp (no_asm) add: takeWhile_tail) apply (rule conjI) -apply clarify -apply (rule conjI) -apply clarify -apply (rule conjI) -apply blast -apply (rule conjI) -apply clarify -apply (rule conjI) -txt{*subcase: used before*} -apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD] - used_takeWhile_used) -txt{*subcase: CT before*} -apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void]) -apply blast -txt{*rest*} +apply (metis Key_not_used authKeys_used length_rev set_rev takeWhile_void used_evs_rev) apply blast+ done @@ -570,10 +557,9 @@ apply (blast dest: authTicket_crypt_authK) apply (blast dest!: authKeys_used Says_Kas_message_form) txt{*subcase: used before*} -apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD] - used_takeWhile_used) +apply (metis used_evs_rev used_takeWhile_used) txt{*subcase: CT before*} -apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void]) +apply (metis length_rev set_evs_rev takeWhile_void) done lemma authTicket_form: @@ -794,8 +780,7 @@ lemma u_NotexpiredSK_NotexpiredAK: "\ \ expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \ \ \ expiredAK Ta evs" -apply (blast dest: leI le_trans dest: leD) -done + by (metis nat_add_commute le_less_trans) subsection{* Reliability: friendly agents send something if something else happened*} @@ -854,16 +839,8 @@ txt{*K3*} apply (blast dest: Key_unique_SesKey) txt{*K5*} -txt{*If authKa were compromised, so would be authK*} -apply (case_tac "Key authKa \ analz (spies evs5)") -apply (force dest!: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) -txt{*Besides, since authKa originated with Kas anyway...*} -apply (clarify, drule K3_imp_K2, assumption, assumption) -apply (clarify, drule Says_Kas_message_form, assumption) -txt{*...it cannot be a shared key*. Therefore @{text servK_authentic} applies. - Contradition: Tgs used authK as a servkey, - while Kas used it as an authkey*} -apply (blast dest: servK_authentic Says_Tgs_message_form) +apply (metis K3_imp_K2 Key_unique_SesKey Spy_see_shrK parts.Body parts.Fst + Says_imp_knows_Spy [THEN parts.Inj]) done lemma Says_K5: @@ -922,9 +899,12 @@ apply (frule_tac [7] Says_ticket_parts) apply (simp_all (no_asm_simp)) apply blast -apply (force dest!: Crypt_imp_keysFor, clarify) -apply (frule Says_Tgs_message_form, assumption, clarify) (*PROOF FAILED if omitted*) -apply (blast dest: unique_CryptKey) +atp_minimize [atp=spass] Crypt_imp_invKey_keysFor invKey_K new_keys_not_used +apply (metis Crypt_imp_invKey_keysFor invKey_K new_keys_not_used) +apply (clarify) +apply (frule Says_Tgs_message_form, assumption) +apply (metis K3_msg_in_parts_spies parts.Fst Says_imp_knows_Spy [THEN parts.Inj] + unique_CryptKey) done text{*Needs a unicity theorem, hence moved here*} @@ -1099,13 +1079,8 @@ apply (erule kerbIV.induct, analz_mono_contra) apply (frule_tac [7] K5_msg_in_parts_spies) apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast) -txt{*K4 splits into distinct subcases*} -apply auto -txt{*servK can't have been enclosed in two certificates*} - prefer 2 apply (blast dest: unique_CryptKey) -txt{*servK is fresh and so could not have been used, by - @{text new_keys_not_used}*} -apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def) +txt{*K4*} +apply (metis Auth_fresh_not_AKcryptSK Crypt_imp_keysFor new_keys_not_used parts.Fst parts.Snd Says_imp_knows_Spy [THEN parts.Inj] unique_CryptKey) done text{*Long term keys are not issued as servKeys*} @@ -1143,16 +1118,9 @@ apply (erule rev_mp) apply (erule kerbIV.induct) apply (frule_tac [7] K5_msg_in_parts_spies) -apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, safe) -txt{*K4 splits into subcases*} -apply simp_all -prefer 4 apply (blast dest!: authK_not_AKcryptSK) -txt{*servK is fresh and so could not have been used, by - @{text new_keys_not_used}*} - prefer 2 - apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def) -txt{*Others by freshness*} -apply (blast+) +apply (frule_tac [5] K3_msg_in_parts_spies, simp_all) +apply (metis Auth_fresh_not_AKcryptSK Says_imp_spies authK_not_AKcryptSK + authKeys_used authTicket_crypt_authK parts.Fst parts.Inj) done text{*The only session keys that can be found with the help of session keys are @@ -1304,7 +1272,7 @@ \ set evs; authK \ symKeys; Key authK \ analz (spies evs); evs \ kerbIV \ \ Key servK \ analz (spies evs)" -by (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) + by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt') lemma servK_notin_authKeysD: "\ Crypt authK \Key servK, Agent B, Ts, @@ -1348,6 +1316,7 @@ txt{*K4*} apply blast txt{*Level 8: K5*} +atp_minimize [atp=e] Tgs_not_bad authKeysI less_SucI mem_def nat_add_commute servK_notin_authKeysD spies_partsEs(1) apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI) txt{*Oops1*} apply (blast dest!: unique_authKeys intro: less_SucI) @@ -1395,24 +1364,17 @@ apply (safe del: impI conjI impCE) apply (simp_all add: less_SucI new_keys_not_analzd Says_Kas_message_form Says_Tgs_message_form analz_insert_eq not_parts_not_analz analz_insert_freshK1 analz_insert_freshK2 analz_insert_freshK3_bis pushes) txt{*Fake*} -apply spy_analz + apply spy_analz txt{*K2*} -apply (blast intro: parts_insertI less_SucI) + apply (blast intro: parts_insertI less_SucI) txt{*K4*} -apply (blast dest: authTicket_authentic Confidentiality_Kas) -txt{*Oops2*} - prefer 3 - apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI) + apply (blast dest: authTicket_authentic Confidentiality_Kas) +txt{*K5*} + apply (metis Says_imp_spies Says_ticket_parts Tgs_not_bad analz_insert_freshK2 + less_SucI parts.Inj servK_notin_authKeysD unique_CryptKey) txt{*Oops1*} - prefer 2 -apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI) -txt{*K5. Not obvious how this step could be integrated with the main - simplification step. Done in KerberosV.thy *} -apply clarify -apply (erule_tac V = "Says Aa Tgs ?X \ set ?evs" in thin_rl) -apply (frule Says_imp_spies [THEN parts.Inj, THEN servK_notin_authKeysD]) -apply (assumption, blast, assumption) -apply (simp add: analz_insert_freshK2) + apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI) +txt{*Oops2*} apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI) done @@ -1669,9 +1631,7 @@ lemma honest_never_says_current_timestamp_in_auth: "\ (CT evs) = T; Number T \ parts {X}; evs \ kerbIV \ \ \ A B Y. A \ bad \ Says A B \Y, X\ \ set evs" -apply (frule eq_imp_le) -apply (blast dest: honest_never_says_newer_timestamp_in_auth) -done + by (metis eq_imp_le honest_never_says_newer_timestamp_in_auth) lemma A_trusts_secure_authenticator: "\ Crypt K \Agent A, Number T\ \ parts (spies evs); diff -r 7887cb2848bb -r b269b56b6a14 src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Mon Aug 10 17:00:41 2009 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Aug 13 17:19:10 2009 +0100 @@ -246,7 +246,7 @@ Notes Spy {|NA, NB, Key K|} \ set evs; A \ bad; B \ bad; evs \ otway |] ==> Key K \ analz (knows Spy evs)" -by (blast dest: Says_Server_message_form secrecy_lemma) + by (metis secrecy_lemma) text{*A's guarantee. The Oops premise quantifies over NB because A cannot know @@ -256,7 +256,7 @@ \NB. Notes Spy {|NA, NB, Key K|} \ set evs; A \ bad; B \ bad; A \ B; evs \ otway |] ==> Key K \ analz (knows Spy evs)" -by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key) + by (metis A_trusts_OR4 secrecy_lemma)