# HG changeset patch # User paulson # Date 1251287521 -3600 # Node ID 9c1b3e2f1b889ebfa126a02864dc7a58a6cff916 # Parent 5731300da417ce914576d7673a27498c6882a59e# Parent 9ea59bd1397a2a81ea7d3b2781281951e818b9e7 merged diff -r 5731300da417 -r 9c1b3e2f1b88 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Wed Aug 26 11:40:28 2009 +0200 +++ b/src/HOL/Auth/Event.thy Wed Aug 26 12:52:01 2009 +0100 @@ -139,9 +139,11 @@ text{*Elimination rules: derive contradictions from old Says events containing items known to be fresh*} +lemmas Says_imp_parts_knows_Spy = + Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] + lemmas knows_Spy_partsEs = - Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] - parts.Body [THEN revcut_rl, standard] + Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard] lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj] diff -r 5731300da417 -r 9c1b3e2f1b88 src/HOL/Auth/KerberosV.thy --- a/src/HOL/Auth/KerberosV.thy Wed Aug 26 11:40:28 2009 +0200 +++ b/src/HOL/Auth/KerberosV.thy Wed Aug 26 12:52:01 2009 +0100 @@ -697,9 +697,7 @@ txt{*K4*} apply (force dest!: Crypt_imp_keysFor, clarify) txt{*K6*} -apply (drule Says_imp_spies [THEN parts.Inj, THEN parts.Fst]) -apply (drule Says_imp_spies [THEN parts.Inj, THEN parts.Snd]) -apply (blast dest!: unique_CryptKey) +apply (metis Says_imp_spies Says_ticket_parts analz.Fst analz.Inj analz_conj_parts unique_CryptKey) done text{*Needs a unicity theorem, hence moved here*} @@ -841,13 +839,10 @@ apply (erule kerbV.induct, analz_mono_contra) apply (frule_tac [7] Says_ticket_parts) apply (frule_tac [5] Says_ticket_parts, 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_invKey_keysFor Says_ticket_analz + analz.Fst invKey_K new_keys_not_analzd parts.Fst Says_imp_parts_knows_Spy + unique_CryptKey) done text{*Long term keys are not issued as servKeys*} @@ -981,9 +976,7 @@ txt{*K4*} apply (blast dest!: authK_not_AKcryptSK) txt{*Oops1*} -apply clarify -apply simp -apply (blast dest!: AKcryptSK_analz_insert) +apply (metis AKcryptSK_analz_insert insert_Key_singleton) done text{* First simplification law for analz: no session keys encrypt @@ -1039,8 +1032,8 @@ \ set evs; authK \ symKeys; Key authK \ analz (spies evs); evs \ kerbV \ \ Key servK \ analz (spies evs)" -apply (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Fst]) -done + by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt') + text{*lemma @{text servK_notin_authKeysD} not needed in version V*} @@ -1112,16 +1105,16 @@ apply (frule_tac [5] Says_ticket_analz) 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 -txt{*K2*} -apply (blast intro: parts_insertI less_SucI) -txt{*K4*} -apply (blast dest: authTicket_authentic Confidentiality_Kas) -txt{*Oops1*} + txt{*Fake*} + apply spy_analz + txt{*K2*} + apply (blast intro: parts_insertI less_SucI) + txt{*K4*} + apply (blast dest: authTicket_authentic Confidentiality_Kas) + txt{*Oops1*} 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) +apply (metis Suc_le_eq linorder_linear linorder_not_le msg.simps(2) unique_servKeys) done @@ -1270,17 +1263,7 @@ Key authK \ analz (spies evs); Key servK \ analz (spies evs); A \ bad; B \ bad; evs \ kerbV \ \ Says B A (Crypt servK (Number T3)) \ set evs" -apply (frule authK_authentic) -apply assumption+ -apply (frule servK_authentic) -prefer 2 apply (blast dest: authK_authentic Says_Kas_message_form) -apply assumption+ -apply clarify -apply (blast dest: K4_imp_K2 Key_unique_SesKey intro!: Says_K6) -(*Single command proof: much slower! -apply (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro!: Says_K6) -*) -done + by (metis authK_authentic Oops_range_spies1 Says_K6 servK_authentic u_K4_imp_K2 unique_authKeys) lemma A_authenticates_B_r: "\ Crypt servK (Number T3) \ parts (spies evs); @@ -1301,8 +1284,7 @@ apply (erule_tac [9] exE) apply (frule_tac [9] K4_imp_K2) apply assumption+ -apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs -) +apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs) done @@ -1478,7 +1460,7 @@ ...expands as follows - including extra exE because of new form of lemmas*) apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE) apply (case_tac "Key authK \ analz (spies evs5)") -apply (drule Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Fst, THEN analz_Decrypt', THEN analz.Fst], assumption, assumption, simp) + apply (metis Says_imp_analz_Spy analz.Fst analz_Decrypt') apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE) apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst]) apply (frule servK_authentic_ter, blast, assumption+) diff -r 5731300da417 -r 9c1b3e2f1b88 src/HOL/Auth/Kerberos_BAN.thy --- a/src/HOL/Auth/Kerberos_BAN.thy Wed Aug 26 11:40:28 2009 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.thy Wed Aug 26 12:52:01 2009 +0100 @@ -288,15 +288,8 @@ on evs)" apply (unfold before_def) apply (erule rev_mp) -apply (erule bankerberos.induct, simp_all) -txt{*We need this simplification only for Message 2*} -apply (simp (no_asm) add: takeWhile_tail) -apply auto -txt{*Two subcases of Message 2. 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 (erule bankerberos.induct, simp_all add: takeWhile_tail) +apply (metis length_rev set_rev takeWhile_void used_evs_rev) done @@ -492,6 +485,7 @@ txt{*BK3*} apply (blast dest: Kab_authentic unique_session_keys) done + lemma lemma_B [rule_format]: "\ B \ bad; evs \ bankerberos \ \ Key K \ analz (spies evs) \ @@ -585,9 +579,8 @@ txt{*BK2*} apply (blast intro: parts_insertI less_SucI) txt{*BK3*} -apply (case_tac "Aa \ bad") - prefer 2 apply (blast dest: Kab_authentic unique_session_keys) -apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI) +apply (metis Crypt_Spy_analz_bad Kab_authentic Says_imp_analz_Spy + Says_imp_parts_knows_Spy analz.Snd less_SucI unique_session_keys) txt{*Oops: PROOF FAILS if unsafe intro below*} apply (blast dest: unique_session_keys intro!: less_SucI) done diff -r 5731300da417 -r 9c1b3e2f1b88 src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Wed Aug 26 11:40:28 2009 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Wed Aug 26 12:52:01 2009 +0100 @@ -273,11 +273,11 @@ apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz) txt{*NS2*} apply blast -txt{*NS3, Server sub-case*} +txt{*NS3*} apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2 dest: Says_imp_knows_Spy analz.Inj unique_session_keys) -txt{*NS3, Spy sub-case; also Oops*} -apply (blast dest: unique_session_keys)+ +txt{*Oops*} +apply (blast dest: unique_session_keys) done diff -r 5731300da417 -r 9c1b3e2f1b88 src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Wed Aug 26 11:40:28 2009 +0200 +++ b/src/HOL/Auth/Recur.thy Wed Aug 26 12:52:01 2009 +0100 @@ -419,15 +419,10 @@ apply spy_analz txt{*RA2*} apply blast -txt{*RA3 remains*} +txt{*RA3*} apply (simp add: parts_insert_spies) -txt{*Now we split into two cases. A single blast could do it, but it would take - a CPU minute.*} -apply (safe del: impCE) -txt{*RA3, case 1: use lemma previously proved by induction*} -apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key]) -txt{*RA3, case 2: K is an old key*} -apply (blast dest: resp_analz_insert dest: Key_in_parts_respond) +apply (metis Key_in_parts_respond parts.Body parts.Fst resp_analz_insert + respond_Spy_not_see_session_key usedI) txt{*RA4*} apply blast done diff -r 5731300da417 -r 9c1b3e2f1b88 src/HOL/SET-Protocol/Cardholder_Registration.thy --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Wed Aug 26 11:40:28 2009 +0200 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Wed Aug 26 12:52:01 2009 +0100 @@ -715,6 +715,7 @@ ==> P --> (Nonce N \ analz (Key`KK Un H)) = (Nonce N \ analz H)" by (blast intro: analz_mono [THEN [2] rev_subsetD]) + text{*The @{text "(no_asm)"} attribute is essential, since it retains the quantifier and allows the simprule's condition to itself be simplified.*} lemma Nonce_compromise [rule_format (no_asm)]: @@ -741,12 +742,11 @@ apply blast --{*3*} apply blast --{*5*} txt{*Message 6*} -apply (force del: allE ballE impCE simp add: symKey_compromise) +apply (metis symKey_compromise) --{*cardSK compromised*} txt{*Simplify again--necessary because the previous simplification introduces - some logical connectives*} -apply (force del: allE ballE impCE - simp del: image_insert image_Un imp_disjL + some logical connectives*} +apply (force simp del: image_insert image_Un imp_disjL simp add: analz_image_keys_simps symKey_compromise) done diff -r 5731300da417 -r 9c1b3e2f1b88 src/HOL/SET-Protocol/Purchase.thy --- a/src/HOL/SET-Protocol/Purchase.thy Wed Aug 26 11:40:28 2009 +0200 +++ b/src/HOL/SET-Protocol/Purchase.thy Wed Aug 26 12:52:01 2009 +0100 @@ -1040,9 +1040,8 @@ apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply blast -apply (force dest!: signed_Hash_imp_used) -apply (clarify) --{*speeds next step*} -apply (blast dest: unique_LID_M) +apply (metis subsetD insert_subset parts.Fst parts_increasing signed_Hash_imp_used) +apply (metis unique_LID_M) apply (blast dest!: Notes_Cardholder_self_False) done