--- a/src/HOL/Auth/Guard/Analz.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Guard/Analz.thy Wed Sep 08 13:30:41 2010 +0100
@@ -233,8 +233,7 @@
lemma analz_kparts_analz: "X:analz (kparts H) ==> X:analz H"
by (erule analz.induct, auto dest: kparts_analz)
-lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==>
-X:analz (kparts {Z} Un kparts H)"
+lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> X:analz (kparts {Z} Un kparts H)"
by (rule analz_sub, auto)
lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G)
@@ -247,26 +246,21 @@
apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
by (auto dest: Nonce_kparts_synth)
-lemma Crypt_insert_synth: "[| Crypt K Y:parts (insert X G); X:synth (analz G);
-Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Crypt K Y:parts G"
-apply (drule parts_insert_substD [where P="%S. Crypt K Y : S"], clarify)
-apply (drule in_sub, drule_tac X="Crypt K Y" in parts_sub, simp, clarsimp)
-apply (ind_cases "Crypt K Y:synth (analz G)")
-by (auto dest: Nonce_kparts_synth)
+lemma Crypt_insert_synth:
+ "[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |]
+ ==> Crypt K Y:parts G"
+by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5))
+
subsection{*analz is pparts + analz of kparts*}
lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)"
-apply (erule analz.induct)
-apply (rule_tac X=X in is_MPairE, blast, blast)
-apply (erule disjE, rule_tac X=X in is_MPairE, blast, blast, blast)
-by (erule disjE, rule_tac X=Y in is_MPairE, blast+)
+by (erule analz.induct, auto)
lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)"
by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz)
lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst]
-lemmas analz_pparts_kparts_substD
-= analz_pparts_kparts_eq [THEN sym, THEN ssubst]
+lemmas analz_pparts_kparts_substD = analz_pparts_kparts_eq [THEN sym, THEN ssubst]
end
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Wed Sep 08 13:30:41 2010 +0100
@@ -11,7 +11,7 @@
header{*Yahalom Protocol*}
-theory Guard_Yahalom imports Guard_Shared begin
+theory Guard_Yahalom imports "../Shared" Guard_Shared begin
subsection{*messages used in the protocol*}
--- a/src/HOL/Auth/Guard/P1.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Guard/P1.thy Wed Sep 08 13:30:41 2010 +0100
@@ -15,7 +15,7 @@
header{*Protocol P1*}
-theory P1 imports Guard_Public List_Msg begin
+theory P1 imports "../Public" Guard_Public List_Msg begin
subsection{*Protocol Definition*}
--- a/src/HOL/Auth/Message.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Message.thy Wed Sep 08 13:30:41 2010 +0100
@@ -582,12 +582,13 @@
text{*NO @{text Agent_synth}, as any Agent name can be synthesized.
The same holds for @{term Number}*}
-inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
-inductive_cases Key_synth [elim!]: "Key K \<in> synth H"
-inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H"
-inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
-inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
+inductive_simps synth_simps [iff]:
+ "Nonce n \<in> synth H"
+ "Key K \<in> synth H"
+ "Hash X \<in> synth H"
+ "{|X,Y|} \<in> synth H"
+ "Crypt K X \<in> synth H"
lemma synth_increasing: "H \<subseteq> synth(H)"
by blast
@@ -605,7 +606,7 @@
subsubsection{*Idempotence and transitivity *}
lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
-by (erule synth.induct, blast+)
+by (erule synth.induct, auto)
lemma synth_idem: "synth (synth H) = synth H"
by blast
@@ -782,7 +783,7 @@
"X \<notin> synth (analz H)
==> (Hash[X] Y \<in> synth (analz H)) =
(Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
-by (simp add: HPair_def)
+by (auto simp add: HPair_def)
text{*We do NOT want Crypt... messages broken up in protocols!!*}
--- a/src/HOL/Auth/Shared.thy Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Auth/Shared.thy Wed Sep 08 13:30:41 2010 +0100
@@ -12,7 +12,7 @@
begin
consts
- shrK :: "agent => key" (*symmetric keys*);
+ shrK :: "agent => key" (*symmetric keys*)
specification (shrK)
inj_shrK: "inj shrK"
@@ -59,7 +59,7 @@
(*Specialized to shared-key model: no @{term invKey}*)
lemma keysFor_parts_insert:
"[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |]
- ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
+ ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
by (force dest: Event.keysFor_parts_insert)
lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"