diff -r f69fb37dc769 -r 8796d5edd29c src/HOL/Auth/Guard/Guard_Shared.thy
--- a/src/HOL/Auth/Guard/Guard_Shared.thy	Wed Dec 23 23:15:42 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Thu Dec 24 12:50:12 2015 +0100
@@ -168,14 +168,34 @@
 apply (frule_tac A=A in shrK_analz_iff_bad)
 by (simp add: knows_decomp)+
 
-lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p;
-shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)"
-apply (clarify, simp only: knows_decomp)
-apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps image_eq_UN)
-apply clarify
-apply (drule in_good, simp)
-apply (drule in_shrK_set, simp+, clarify)
-apply (frule_tac A=A in shrK_analz_iff_bad)
-by (simp add: knows_decomp)+
+lemma GuardK_Key_analz:
+  assumes "GuardK n Ks (spies evs)" "evs \<in> p" "shrK_set Ks"
+    "good Ks" "regular p" "n \<notin> range shrK"
+  shows "Key n \<notin> analz (spies evs)"
+proof (rule ccontr)
+  assume "\<not> Key n \<notin> analz (knows Spy evs)"
+  then have *: "Key n \<in> analz (spies' evs \<union> initState Spy)"
+    by (simp add: knows_decomp)
+  from \<open>GuardK n Ks (spies evs)\<close>
+  have "GuardK n Ks (spies' evs \<union> initState Spy)"
+    by (simp add: knows_decomp)  
+  then have "GuardK n Ks (spies' evs)"
+    and "finite (spies' evs)" "keyset (initState Spy)"
+    by simp_all
+  moreover have "Key n \<notin> initState Spy"
+    using \<open>n \<notin> range shrK\<close> by (simp add: image_iff initState_Spy)
+  ultimately obtain K
+    where "K \<in> Ks" and **: "Key K \<in> analz (spies' evs \<union> initState Spy)"
+    using * by (auto dest: GuardK_invKey_keyset)
+  from \<open>K \<in> Ks\<close> and \<open>good Ks\<close> have "agt K \<notin> bad"
+    by (auto dest: in_good)
+  from \<open>K \<in> Ks\<close> \<open>shrK_set Ks\<close> obtain A
+    where "K = shrK A"
+    by (auto dest: in_shrK_set)
+  then have "agt K \<in> bad"
+    using ** \<open>evs \<in> p\<close> \<open>regular p\<close> shrK_analz_iff_bad [of evs p "agt K"]
+    by (simp add: knows_decomp)
+  with \<open>agt K \<notin> bad\<close> show False by simp
+qed
 
 end
\ No newline at end of file