133 inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H" |
133 inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H" |
134 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H" |
134 inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H" |
135 |
135 |
136 use "Message_lemmas.ML" |
136 use "Message_lemmas.ML" |
137 |
137 |
|
138 lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A" |
|
139 by auto |
|
140 |
|
141 lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A" |
|
142 by auto |
|
143 |
|
144 lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))" |
|
145 by (simp add: synth_mono analz_mono) |
|
146 |
|
147 lemma Fake_analz_eq [simp]: |
|
148 "X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)" |
|
149 apply (drule Fake_analz_insert[of _ _ "H"]) |
|
150 apply (simp add: synth_increasing[THEN Un_absorb2]) |
|
151 apply (drule synth_mono) |
|
152 apply (simp add: synth_idem) |
|
153 apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) |
|
154 done |
|
155 |
|
156 |
138 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard] |
157 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard] |
139 |
158 |
140 lemma Fake_parts_insert_in_Un: |
159 lemma Fake_parts_insert_in_Un: |
141 "[|Z \<in> parts (insert X H); X: synth (analz H)|] |
160 "[|Z \<in> parts (insert X H); X: synth (analz H)|] |
142 ==> Z \<in> synth (analz H) \<union> parts H"; |
161 ==> Z \<in> synth (analz H) \<union> parts H"; |
143 by (blast dest: Fake_parts_insert [THEN subsetD, dest]) |
162 by (blast dest: Fake_parts_insert [THEN subsetD, dest]) |
|
163 |
|
164 text{*Two generalizations of @{text analz_insert_eq}*} |
|
165 lemma gen_analz_insert_eq [rule_format]: |
|
166 "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"; |
|
167 by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD]) |
|
168 |
|
169 lemma synth_analz_insert_eq [rule_format]: |
|
170 "X \<in> synth (analz H) |
|
171 ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"; |
|
172 apply (erule synth.induct) |
|
173 apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) |
|
174 done |
|
175 |
|
176 lemma Fake_parts_sing: |
|
177 "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) Un parts H"; |
|
178 apply (rule subset_trans) |
|
179 apply (erule_tac [2] Fake_parts_insert) |
|
180 apply (simp add: parts_mono) |
|
181 done |
144 |
182 |
145 method_setup spy_analz = {* |
183 method_setup spy_analz = {* |
146 Method.ctxt_args (fn ctxt => |
184 Method.ctxt_args (fn ctxt => |
147 Method.METHOD (fn facts => |
185 Method.METHOD (fn facts => |
148 gen_spy_analz_tac (Classical.get_local_claset ctxt, |
186 gen_spy_analz_tac (Classical.get_local_claset ctxt, |