# HG changeset patch # User paulson # Date 1250180394 -3600 # Node ID 37d87022cad37733426b6445e82cb841c7975eaa # Parent 9b74d0339c443619fb42b9411bd0edb19f384607# Parent a508148f7c254c4c22d2701ded14fd4504a0cc34 merged diff -r 9b74d0339c44 -r 37d87022cad3 src/HOL/Auth/KerberosIV.thy --- a/src/HOL/Auth/KerberosIV.thy Wed Aug 12 00:26:01 2009 +0200 +++ b/src/HOL/Auth/KerberosIV.thy Thu Aug 13 17:19:54 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 9b74d0339c44 -r 37d87022cad3 src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Wed Aug 12 00:26:01 2009 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Aug 13 17:19:54 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) diff -r 9b74d0339c44 -r 37d87022cad3 src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Wed Aug 12 00:26:01 2009 +0200 +++ b/src/HOL/Auth/Yahalom.thy Thu Aug 13 17:19:54 2009 +0100 @@ -129,8 +129,7 @@ lemma YM4_Key_parts_knows_Spy: "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \ set evs ==> K \ parts (knows Spy evs)" -by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj]) - + by (metis parts.Body parts.Fst parts.Snd Says_imp_knows_Spy parts.Inj) text{*Theorems of the form @{term "X \ parts (knows Spy evs)"} imply that NOBODY sends messages containing X! *} @@ -275,7 +274,7 @@ Notes Spy {|na, nb, Key K|} \ set evs; A \ bad; B \ bad; evs \ yahalom |] ==> Key K \ analz (knows Spy evs)" -by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) + by (metis A_trusts_YM3 secrecy_lemma) subsubsection{* Security Guarantees for B upon receiving YM4 *} @@ -409,9 +408,8 @@ txt{*If @{prop "A \ bad"} then @{term NBa} is known, therefore @{prop "NBa \ NB"}. Previous two steps make the next step faster.*} -apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad - dest: analz.Inj - parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI]) +apply (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def + Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj) done @@ -514,12 +512,7 @@ covered by the quantified Oops assumption.*} apply (clarify, simp add: all_conj_distrib) apply (frule Says_Server_imp_YM2, assumption) -apply (case_tac "NB = NBa") -txt{*If NB=NBa then all other components of the Oops message agree*} -apply (blast dest: Says_unique_NB) -txt{*case @{prop "NB \ NBa"}*} -apply (simp add: single_Nonce_secrecy) -apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\NAa*)) +apply (metis Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1)) done @@ -557,7 +550,7 @@ \k. Notes Spy {|Nonce NA, Nonce NB, k|} \ set evs; A \ bad; B \ bad; evs \ yahalom |] ==> Key K \ analz (knows Spy evs)" -by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) + by (metis B_trusts_YM4 Spy_not_see_encrypted_key) subsection{*Authenticating B to A*} @@ -594,7 +587,8 @@ A \ bad; B \ bad; evs \ yahalom |] ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ set evs" -by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs) + by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst + not_parts_not_analz) subsection{*Authenticating A to B using the certificate @@ -639,7 +633,6 @@ (\NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \ set evs); A \ bad; B \ bad; evs \ yahalom |] ==> \X. Says A B {|X, Crypt K (Nonce NB)|} \ set evs" -by (blast intro!: A_Said_YM3_lemma - dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says) - +atp_minimize [atp=spass] A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz +by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz) end diff -r 9b74d0339c44 -r 37d87022cad3 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Wed Aug 12 00:26:01 2009 +0200 +++ b/src/HOL/Bali/Basis.thy Thu Aug 13 17:19:54 2009 +0100 @@ -7,8 +7,6 @@ theory Basis imports Main begin -declare [[unify_search_bound = 40, unify_trace_bound = 40]] - section "misc" @@ -65,36 +63,36 @@ by (auto intro: r_into_rtrancl rtrancl_trans) lemma triangle_lemma: - "\ \ a b c. \(a,b)\r; (a,c)\r\ \ b=c; (a,x)\r\<^sup>*; (a,y)\r\<^sup>*\ - \ (x,y)\r\<^sup>* \ (y,x)\r\<^sup>*" + "\ \ a b c. \(a,b)\r; (a,c)\r\ \ b=c; (a,x)\r*; (a,y)\r*\ + \ (x,y)\r* \ (y,x)\r*" proof - note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1] note converse_rtranclE = converse_rtranclE [consumes 1] assume unique: "\ a b c. \(a,b)\r; (a,c)\r\ \ b=c" - assume "(a,x)\r\<^sup>*" - then show "(a,y)\r\<^sup>* \ (x,y)\r\<^sup>* \ (y,x)\r\<^sup>*" + assume "(a,x)\r*" + then show "(a,y)\r* \ (x,y)\r* \ (y,x)\r*" proof (induct rule: converse_rtrancl_induct) - assume "(x,y)\r\<^sup>*" + assume "(x,y)\r*" then show ?thesis by blast next fix a v assume a_v_r: "(a, v) \ r" and - v_x_rt: "(v, x) \ r\<^sup>*" and - a_y_rt: "(a, y) \ r\<^sup>*" and - hyp: "(v, y) \ r\<^sup>* \ (x, y) \ r\<^sup>* \ (y, x) \ r\<^sup>*" + v_x_rt: "(v, x) \ r*" and + a_y_rt: "(a, y) \ r*" and + hyp: "(v, y) \ r* \ (x, y) \ r* \ (y, x) \ r*" from a_y_rt - show "(x, y) \ r\<^sup>* \ (y, x) \ r\<^sup>*" + show "(x, y) \ r* \ (y, x) \ r*" proof (cases rule: converse_rtranclE) assume "a=y" - with a_v_r v_x_rt have "(y,x) \ r\<^sup>*" + with a_v_r v_x_rt have "(y,x) \ r*" by (auto intro: r_into_rtrancl rtrancl_trans) then show ?thesis by blast next fix w assume a_w_r: "(a, w) \ r" and - w_y_rt: "(w, y) \ r\<^sup>*" + w_y_rt: "(w, y) \ r*" from a_v_r a_w_r unique have "v=w" by auto @@ -107,7 +105,7 @@ lemma rtrancl_cases [consumes 1, case_names Refl Trancl]: - "\(a,b)\r\<^sup>*; a = b \ P; (a,b)\r\<^sup>+ \ P\ \ P" + "\(a,b)\r*; a = b \ P; (a,b)\r+ \ P\ \ P" apply (erule rtranclE) apply (auto dest: rtrancl_into_trancl1) done diff -r 9b74d0339c44 -r 37d87022cad3 src/HOL/Induct/Com.thy --- a/src/HOL/Induct/Com.thy Wed Aug 12 00:26:01 2009 +0200 +++ b/src/HOL/Induct/Com.thy Thu Aug 13 17:19:54 2009 +0100 @@ -91,8 +91,6 @@ "((\x x' y. ((x, x'), y) \ R) <= (\x x' y. ((x, x'), y) \ S)) = (R <= S)" by (auto simp add: le_fun_def le_bool_def mem_def) -declare [[unify_trace_bound = 30, unify_search_bound = 60]] - text{*Command execution is functional (deterministic) provided evaluation is*} theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)" apply (simp add: single_valued_def) diff -r 9b74d0339c44 -r 37d87022cad3 src/HOL/MicroJava/J/JTypeSafe.thy --- a/src/HOL/MicroJava/J/JTypeSafe.thy Wed Aug 12 00:26:01 2009 +0200 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Aug 13 17:19:54 2009 +0100 @@ -183,8 +183,6 @@ (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)])) *} -declare [[unify_search_bound = 40, unify_trace_bound = 40]] - theorem eval_evals_exec_type_sound: "wf_java_prog G ==> @@ -368,8 +366,6 @@ done -declare [[unify_search_bound = 20, unify_trace_bound = 20]] - lemma eval_type_sound: "!!E s s'. [| wf_java_prog G; G\(x,s) -e\v -> (x',s'); (x,s)::\E; E\e::T; G=prg E |]