--- a/src/HOL/Auth/Kerberos_BAN.thy Thu Sep 09 17:23:08 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Thu Sep 09 17:58:11 2010 +0200
@@ -171,21 +171,21 @@
text{*Lemmas for reasoning about predicate "before"*}
-lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)";
+lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)";
+lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs";
+lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Thu Sep 09 17:23:08 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Thu Sep 09 17:58:11 2010 +0200
@@ -157,10 +157,7 @@
lemma Gets_imp_knows:
"\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> knows B evs"
-apply (case_tac "B = Spy")
-apply (blast dest!: Gets_imp_knows_Spy)
-apply (blast dest!: Gets_imp_knows_agents)
-done
+by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
lemma Gets_imp_knows_analz:
"\<lbrakk> Gets B X \<in> set evs; evs \<in> bankerb_gets \<rbrakk> \<Longrightarrow> X \<in> analz (knows B evs)"
@@ -168,21 +165,21 @@
done
text{*Lemmas for reasoning about predicate "before"*}
-lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)";
+lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)";
+lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
apply auto
done
-lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs";
+lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
apply (induct_tac "evs")
apply simp
apply (induct_tac "a")
--- a/src/HOL/Auth/OtwayReesBella.thy Thu Sep 09 17:23:08 2010 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy Thu Sep 09 17:58:11 2010 +0200
@@ -104,11 +104,7 @@
lemma Gets_imp_knows:
"\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk> \<Longrightarrow> X \<in> knows B evs"
-apply (case_tac "B = Spy")
-apply (blast dest!: Gets_imp_knows_Spy)
-apply (blast dest!: Gets_imp_knows_agents)
-done
-
+by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
lemma OR2_analz_knows_Spy:
"\<lbrakk>Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> orb\<rbrakk>
@@ -218,15 +214,8 @@
evs \<in> orb\<rbrakk>
\<Longrightarrow> (K \<notin> range shrK & (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>)))
| X \<in> analz (knows Spy evs)"
-apply (case_tac "B \<in> bad")
-apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd,
- THEN analz.Decrypt, THEN analz.Fst])
-prefer 3 apply blast
-prefer 3 apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN
- parts.Snd, THEN B_trusts_OR3]
- Says_Server_message_form)
-apply simp_all
-done
+by (metis B_trusts_OR3 Crypt_Spy_analz_bad Gets_imp_Says MPair_analz MPair_parts
+ Says_Server_message_form Says_imp_analz_Spy Says_imp_parts_knows_Spy)
lemma unique_Na: "\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;
Says A B' \<lbrace>Nonce M', Agent A, Agent B', Crypt (shrK A) \<lbrace>Nonce Na, Nonce M', Agent A, Agent B'\<rbrace>\<rbrace> \<in> set evs;
@@ -240,7 +229,7 @@
lemma analz_image_freshCryptK_lemma:
"(Crypt K X \<in> analz (Key`nE \<union> H)) \<longrightarrow> (Crypt K X \<in> analz H) \<Longrightarrow>
- (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)";
+ (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])
ML
@@ -376,8 +365,6 @@
apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
apply (drule analz_hard, assumption, assumption, assumption, assumption)
apply (drule OR4_imp_Gets, assumption, assumption)
-apply (erule exE)
-(*blast doesn't do because it can't infer that Key (shrK P) \<in> (knows P evs)*)
apply (fastsimp dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
done
--- a/src/HOL/Auth/Public.thy Thu Sep 09 17:23:08 2010 +0200
+++ b/src/HOL/Auth/Public.thy Thu Sep 09 17:58:11 2010 +0200
@@ -235,12 +235,10 @@
"\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
apply (induct evs)
prefer 2
- apply (simp add: used_Cons)
- apply (rule ballI)
- apply (case_tac a, auto)
-apply (auto dest!: parts_cut)
+ apply (simp add: used_Cons split: event.split)
+ apply (metis Un_iff empty_subsetI insert_subset le_supI1 le_supI2 parts_subset_iff)
txt{*Base case*}
-apply (simp add: used_Nil)
+apply (auto dest!: parts_cut simp add: used_Nil)
done
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"