--- 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!]:
"\<lbrakk> Key (shrK A) \<in> parts (spies evs); evs \<in> kerbIV \<rbrakk> \<Longrightarrow> 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:
"\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
\<Longrightarrow> \<not> 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 \<in> 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 @@
\<in> set evs; authK \<in> symKeys;
Key authK \<in> analz (spies evs); evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> Key servK \<in> 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:
"\<lbrakk> Crypt authK \<lbrace>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 \<in> 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:
"\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> \<forall> A B Y. A \<notin> bad \<longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> 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:
"\<lbrakk> Crypt K \<lbrace>Agent A, Number T\<rbrace> \<in> parts (spies evs);
--- 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|} \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Key K \<notin> 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 @@
\<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
-by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
+ by (metis A_trusts_OR4 secrecy_lemma)
--- 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|} \<in> set evs
==> K \<in> 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 \<notin> parts (knows Spy evs)"} imply
that NOBODY sends messages containing X! *}
@@ -275,7 +274,7 @@
Notes Spy {|na, nb, Key K|} \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> 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 \<in> bad"} then @{term NBa} is known, therefore
@{prop "NBa \<noteq> 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 \<noteq> NBa"}*}
-apply (simp add: single_Nonce_secrecy)
-apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>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 @@
\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> 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 \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
\<in> 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 @@
(\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> 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
--- 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:
- "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk>
- \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
+ "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r*; (a,y)\<in>r*\<rbrakk>
+ \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
proof -
note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
note converse_rtranclE = converse_rtranclE [consumes 1]
assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
- assume "(a,x)\<in>r\<^sup>*"
- then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
+ assume "(a,x)\<in>r*"
+ then show "(a,y)\<in>r* \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
proof (induct rule: converse_rtrancl_induct)
- assume "(x,y)\<in>r\<^sup>*"
+ assume "(x,y)\<in>r*"
then show ?thesis
by blast
next
fix a v
assume a_v_r: "(a, v) \<in> r" and
- v_x_rt: "(v, x) \<in> r\<^sup>*" and
- a_y_rt: "(a, y) \<in> r\<^sup>*" and
- hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
+ v_x_rt: "(v, x) \<in> r*" and
+ a_y_rt: "(a, y) \<in> r*" and
+ hyp: "(v, y) \<in> r* \<Longrightarrow> (x, y) \<in> r* \<or> (y, x) \<in> r*"
from a_y_rt
- show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
+ show "(x, y) \<in> r* \<or> (y, x) \<in> r*"
proof (cases rule: converse_rtranclE)
assume "a=y"
- with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
+ with a_v_r v_x_rt have "(y,x) \<in> r*"
by (auto intro: r_into_rtrancl rtrancl_trans)
then show ?thesis
by blast
next
fix w
assume a_w_r: "(a, w) \<in> r" and
- w_y_rt: "(w, y) \<in> r\<^sup>*"
+ w_y_rt: "(w, y) \<in> 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]:
- "\<lbrakk>(a,b)\<in>r\<^sup>*; a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ "\<lbrakk>(a,b)\<in>r*; a = b \<Longrightarrow> P; (a,b)\<in>r+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
apply (erule rtranclE)
apply (auto dest: rtrancl_into_trancl1)
done
--- 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 @@
"((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> 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)
--- 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\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]