author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 67613 | ce654b0e6d69 |
child 76287 | cdc14f94c754 |
permissions | -rw-r--r-- |
41775 | 1 |
(* Title: HOL/Auth/Guard/Analz.thy |
2 |
Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 |
Copyright 2001 University of Cambridge |
|
4 |
*) |
|
13508 | 5 |
|
61830 | 6 |
section\<open>Decomposition of Analz into two parts\<close> |
13508 | 7 |
|
16417 | 8 |
theory Analz imports Extensions begin |
13508 | 9 |
|
69597 | 10 |
text\<open>decomposition of \<^term>\<open>analz\<close> into two parts: |
11 |
\<^term>\<open>pparts\<close> (for pairs) and analz of \<^term>\<open>kparts\<close>\<close> |
|
13508 | 12 |
|
61830 | 13 |
subsection\<open>messages that do not contribute to analz\<close> |
13508 | 14 |
|
23746 | 15 |
inductive_set |
16 |
pparts :: "msg set => msg set" |
|
17 |
for H :: "msg set" |
|
18 |
where |
|
67613 | 19 |
Inj [intro]: "[| X \<in> H; is_MPair X |] ==> X \<in> pparts H" |
20 |
| Fst [dest]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; is_MPair X |] ==> X \<in> pparts H" |
|
21 |
| Snd [dest]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; is_MPair Y |] ==> Y \<in> pparts H" |
|
13508 | 22 |
|
69597 | 23 |
subsection\<open>basic facts about \<^term>\<open>pparts\<close>\<close> |
13508 | 24 |
|
67613 | 25 |
lemma pparts_is_MPair [dest]: "X \<in> pparts H \<Longrightarrow> is_MPair X" |
13508 | 26 |
by (erule pparts.induct, auto) |
27 |
||
67613 | 28 |
lemma Crypt_notin_pparts [iff]: "Crypt K X \<notin> pparts H" |
13508 | 29 |
by auto |
30 |
||
67613 | 31 |
lemma Key_notin_pparts [iff]: "Key K \<notin> pparts H" |
13508 | 32 |
by auto |
33 |
||
67613 | 34 |
lemma Nonce_notin_pparts [iff]: "Nonce n \<notin> pparts H" |
13508 | 35 |
by auto |
36 |
||
67613 | 37 |
lemma Number_notin_pparts [iff]: "Number n \<notin> pparts H" |
13508 | 38 |
by auto |
39 |
||
67613 | 40 |
lemma Agent_notin_pparts [iff]: "Agent A \<notin> pparts H" |
13508 | 41 |
by auto |
42 |
||
43 |
lemma pparts_empty [iff]: "pparts {} = {}" |
|
44 |
by (auto, erule pparts.induct, auto) |
|
45 |
||
67613 | 46 |
lemma pparts_insertI [intro]: "X \<in> pparts H \<Longrightarrow> X \<in> pparts (insert Y H)" |
13508 | 47 |
by (erule pparts.induct, auto) |
48 |
||
67613 | 49 |
lemma pparts_sub: "[| X \<in> pparts G; G \<subseteq> H |] ==> X \<in> pparts H" |
13508 | 50 |
by (erule pparts.induct, auto) |
51 |
||
52 |
lemma pparts_insert2 [iff]: "pparts (insert X (insert Y H)) |
|
53 |
= pparts {X} Un pparts {Y} Un pparts H" |
|
54 |
by (rule eq, (erule pparts.induct, auto)+) |
|
55 |
||
61956 | 56 |
lemma pparts_insert_MPair [iff]: "pparts (insert \<lbrace>X,Y\<rbrace> H) |
57 |
= insert \<lbrace>X,Y\<rbrace> (pparts ({X,Y} \<union> H))" |
|
13508 | 58 |
apply (rule eq, (erule pparts.induct, auto)+) |
59 |
apply (rule_tac Y=Y in pparts.Fst, auto) |
|
60 |
apply (erule pparts.induct, auto) |
|
61 |
by (rule_tac X=X in pparts.Snd, auto) |
|
62 |
||
63 |
lemma pparts_insert_Nonce [iff]: "pparts (insert (Nonce n) H) = pparts H" |
|
64 |
by (rule eq, erule pparts.induct, auto) |
|
65 |
||
66 |
lemma pparts_insert_Crypt [iff]: "pparts (insert (Crypt K X) H) = pparts H" |
|
67 |
by (rule eq, erule pparts.induct, auto) |
|
68 |
||
69 |
lemma pparts_insert_Key [iff]: "pparts (insert (Key K) H) = pparts H" |
|
70 |
by (rule eq, erule pparts.induct, auto) |
|
71 |
||
72 |
lemma pparts_insert_Agent [iff]: "pparts (insert (Agent A) H) = pparts H" |
|
73 |
by (rule eq, erule pparts.induct, auto) |
|
74 |
||
75 |
lemma pparts_insert_Number [iff]: "pparts (insert (Number n) H) = pparts H" |
|
76 |
by (rule eq, erule pparts.induct, auto) |
|
77 |
||
78 |
lemma pparts_insert_Hash [iff]: "pparts (insert (Hash X) H) = pparts H" |
|
79 |
by (rule eq, erule pparts.induct, auto) |
|
80 |
||
67613 | 81 |
lemma pparts_insert: "X \<in> pparts (insert Y H) \<Longrightarrow> X \<in> pparts {Y} \<union> pparts H" |
13508 | 82 |
by (erule pparts.induct, blast+) |
83 |
||
67613 | 84 |
lemma insert_pparts: "X \<in> pparts {Y} \<union> pparts H \<Longrightarrow> X \<in> pparts (insert Y H)" |
13508 | 85 |
by (safe, erule pparts.induct, auto) |
86 |
||
67613 | 87 |
lemma pparts_Un [iff]: "pparts (G \<union> H) = pparts G \<union> pparts H" |
13508 | 88 |
by (rule eq, erule pparts.induct, auto dest: pparts_sub) |
89 |
||
90 |
lemma pparts_pparts [iff]: "pparts (pparts H) = pparts H" |
|
91 |
by (rule eq, erule pparts.induct, auto) |
|
92 |
||
93 |
lemma pparts_insert_eq: "pparts (insert X H) = pparts {X} Un pparts H" |
|
94 |
by (rule_tac A=H in insert_Un, rule pparts_Un) |
|
95 |
||
96 |
lemmas pparts_insert_substI = pparts_insert_eq [THEN ssubst] |
|
97 |
||
67613 | 98 |
lemma in_pparts: "Y \<in> pparts H \<Longrightarrow> \<exists>X. X \<in> H \<and> Y \<in> pparts {X}" |
13508 | 99 |
by (erule pparts.induct, auto) |
100 |
||
69597 | 101 |
subsection\<open>facts about \<^term>\<open>pparts\<close> and \<^term>\<open>parts\<close>\<close> |
13508 | 102 |
|
67613 | 103 |
lemma pparts_no_Nonce [dest]: "[| X \<in> pparts {Y}; Nonce n \<notin> parts {Y} |] |
104 |
==> Nonce n \<notin> parts {X}" |
|
13508 | 105 |
by (erule pparts.induct, simp_all) |
106 |
||
69597 | 107 |
subsection\<open>facts about \<^term>\<open>pparts\<close> and \<^term>\<open>analz\<close>\<close> |
13508 | 108 |
|
67613 | 109 |
lemma pparts_analz: "X \<in> pparts H \<Longrightarrow> X \<in> analz H" |
13508 | 110 |
by (erule pparts.induct, auto) |
111 |
||
67613 | 112 |
lemma pparts_analz_sub: "[| X \<in> pparts G; G \<subseteq> H |] ==> X \<in> analz H" |
13508 | 113 |
by (auto dest: pparts_sub pparts_analz) |
114 |
||
61830 | 115 |
subsection\<open>messages that contribute to analz\<close> |
13508 | 116 |
|
23746 | 117 |
inductive_set |
118 |
kparts :: "msg set => msg set" |
|
119 |
for H :: "msg set" |
|
120 |
where |
|
67613 | 121 |
Inj [intro]: "[| X \<in> H; not_MPair X |] ==> X \<in> kparts H" |
122 |
| Fst [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair X |] ==> X \<in> kparts H" |
|
123 |
| Snd [intro]: "[| \<lbrace>X,Y\<rbrace> \<in> pparts H; not_MPair Y |] ==> Y \<in> kparts H" |
|
13508 | 124 |
|
69597 | 125 |
subsection\<open>basic facts about \<^term>\<open>kparts\<close>\<close> |
13508 | 126 |
|
67613 | 127 |
lemma kparts_not_MPair [dest]: "X \<in> kparts H \<Longrightarrow> not_MPair X" |
13508 | 128 |
by (erule kparts.induct, auto) |
129 |
||
130 |
lemma kparts_empty [iff]: "kparts {} = {}" |
|
131 |
by (rule eq, erule kparts.induct, auto) |
|
132 |
||
67613 | 133 |
lemma kparts_insertI [intro]: "X \<in> kparts H \<Longrightarrow> X \<in> kparts (insert Y H)" |
13508 | 134 |
by (erule kparts.induct, auto dest: pparts_insertI) |
135 |
||
136 |
lemma kparts_insert2 [iff]: "kparts (insert X (insert Y H)) |
|
67613 | 137 |
= kparts {X} \<union> kparts {Y} \<union> kparts H" |
13508 | 138 |
by (rule eq, (erule kparts.induct, auto)+) |
139 |
||
61956 | 140 |
lemma kparts_insert_MPair [iff]: "kparts (insert \<lbrace>X,Y\<rbrace> H) |
141 |
= kparts ({X,Y} \<union> H)" |
|
13508 | 142 |
by (rule eq, (erule kparts.induct, auto)+) |
143 |
||
144 |
lemma kparts_insert_Nonce [iff]: "kparts (insert (Nonce n) H) |
|
145 |
= insert (Nonce n) (kparts H)" |
|
146 |
by (rule eq, erule kparts.induct, auto) |
|
147 |
||
148 |
lemma kparts_insert_Crypt [iff]: "kparts (insert (Crypt K X) H) |
|
149 |
= insert (Crypt K X) (kparts H)" |
|
150 |
by (rule eq, erule kparts.induct, auto) |
|
151 |
||
152 |
lemma kparts_insert_Key [iff]: "kparts (insert (Key K) H) |
|
153 |
= insert (Key K) (kparts H)" |
|
154 |
by (rule eq, erule kparts.induct, auto) |
|
155 |
||
156 |
lemma kparts_insert_Agent [iff]: "kparts (insert (Agent A) H) |
|
157 |
= insert (Agent A) (kparts H)" |
|
158 |
by (rule eq, erule kparts.induct, auto) |
|
159 |
||
160 |
lemma kparts_insert_Number [iff]: "kparts (insert (Number n) H) |
|
161 |
= insert (Number n) (kparts H)" |
|
162 |
by (rule eq, erule kparts.induct, auto) |
|
163 |
||
164 |
lemma kparts_insert_Hash [iff]: "kparts (insert (Hash X) H) |
|
165 |
= insert (Hash X) (kparts H)" |
|
166 |
by (rule eq, erule kparts.induct, auto) |
|
167 |
||
67613 | 168 |
lemma kparts_insert: "X \<in> kparts (insert X H) \<Longrightarrow> X \<in> kparts {X} \<union> kparts H" |
13508 | 169 |
by (erule kparts.induct, (blast dest: pparts_insert)+) |
170 |
||
67613 | 171 |
lemma kparts_insert_fst [rule_format,dest]: "X \<in> kparts (insert Z H) \<Longrightarrow> |
172 |
X \<notin> kparts H \<longrightarrow> X \<in> kparts {Z}" |
|
13508 | 173 |
by (erule kparts.induct, (blast dest: pparts_insert)+) |
174 |
||
67613 | 175 |
lemma kparts_sub: "[| X \<in> kparts G; G \<subseteq> H |] ==> X \<in> kparts H" |
13508 | 176 |
by (erule kparts.induct, auto dest: pparts_sub) |
177 |
||
67613 | 178 |
lemma kparts_Un [iff]: "kparts (G \<union> H) = kparts G \<union> kparts H" |
13508 | 179 |
by (rule eq, erule kparts.induct, auto dest: kparts_sub) |
180 |
||
181 |
lemma pparts_kparts [iff]: "pparts (kparts H) = {}" |
|
182 |
by (rule eq, erule pparts.induct, auto) |
|
183 |
||
184 |
lemma kparts_kparts [iff]: "kparts (kparts H) = kparts H" |
|
185 |
by (rule eq, erule kparts.induct, auto) |
|
186 |
||
67613 | 187 |
lemma kparts_insert_eq: "kparts (insert X H) = kparts {X} \<union> kparts H" |
13508 | 188 |
by (rule_tac A=H in insert_Un, rule kparts_Un) |
189 |
||
190 |
lemmas kparts_insert_substI = kparts_insert_eq [THEN ssubst] |
|
191 |
||
67613 | 192 |
lemma in_kparts: "Y \<in> kparts H \<Longrightarrow> \<exists>X. X \<in> H \<and> Y \<in> kparts {X}" |
13508 | 193 |
by (erule kparts.induct, auto dest: in_pparts) |
194 |
||
195 |
lemma kparts_has_no_pair [iff]: "has_no_pair (kparts H)" |
|
196 |
by auto |
|
197 |
||
69597 | 198 |
subsection\<open>facts about \<^term>\<open>kparts\<close> and \<^term>\<open>parts\<close>\<close> |
13508 | 199 |
|
67613 | 200 |
lemma kparts_no_Nonce [dest]: "[| X \<in> kparts {Y}; Nonce n \<notin> parts {Y} |] |
201 |
==> Nonce n \<notin> parts {X}" |
|
13508 | 202 |
by (erule kparts.induct, auto) |
203 |
||
67613 | 204 |
lemma kparts_parts: "X \<in> kparts H \<Longrightarrow> X \<in> parts H" |
13508 | 205 |
by (erule kparts.induct, auto dest: pparts_analz) |
206 |
||
67613 | 207 |
lemma parts_kparts: "X \<in> parts (kparts H) \<Longrightarrow> X \<in> parts H" |
13508 | 208 |
by (erule parts.induct, auto dest: kparts_parts |
209 |
intro: parts.Fst parts.Snd parts.Body) |
|
210 |
||
67613 | 211 |
lemma Crypt_kparts_Nonce_parts [dest]: "[| Crypt K Y \<in> kparts {Z}; |
212 |
Nonce n \<in> parts {Y} |] ==> Nonce n \<in> parts {Z}" |
|
13508 | 213 |
by auto |
214 |
||
69597 | 215 |
subsection\<open>facts about \<^term>\<open>kparts\<close> and \<^term>\<open>analz\<close>\<close> |
13508 | 216 |
|
67613 | 217 |
lemma kparts_analz: "X \<in> kparts H \<Longrightarrow> X \<in> analz H" |
13508 | 218 |
by (erule kparts.induct, auto dest: pparts_analz) |
219 |
||
67613 | 220 |
lemma kparts_analz_sub: "[| X \<in> kparts G; G \<subseteq> H |] ==> X \<in> analz H" |
13508 | 221 |
by (erule kparts.induct, auto dest: pparts_analz_sub) |
222 |
||
67613 | 223 |
lemma analz_kparts [rule_format,dest]: "X \<in> analz H \<Longrightarrow> |
224 |
Y \<in> kparts {X} \<longrightarrow> Y \<in> analz H" |
|
13508 | 225 |
by (erule analz.induct, auto dest: kparts_analz_sub) |
226 |
||
67613 | 227 |
lemma analz_kparts_analz: "X \<in> analz (kparts H) \<Longrightarrow> X \<in> analz H" |
13508 | 228 |
by (erule analz.induct, auto dest: kparts_analz) |
229 |
||
67613 | 230 |
lemma analz_kparts_insert: "X \<in> analz (kparts (insert Z H)) \<Longrightarrow> X \<in> analz (kparts {Z} \<union> kparts H)" |
13508 | 231 |
by (rule analz_sub, auto) |
232 |
||
67613 | 233 |
lemma Nonce_kparts_synth [rule_format]: "Y \<in> synth (analz G) |
234 |
\<Longrightarrow> Nonce n \<in> kparts {Y} \<longrightarrow> Nonce n \<in> analz G" |
|
13508 | 235 |
by (erule synth.induct, auto) |
236 |
||
67613 | 237 |
lemma kparts_insert_synth: "[| Y \<in> parts (insert X G); X \<in> synth (analz G); |
238 |
Nonce n \<in> kparts {Y}; Nonce n \<notin> analz G |] ==> Y \<in> parts G" |
|
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
41775
diff
changeset
|
239 |
apply (drule parts_insert_substD, clarify) |
13508 | 240 |
apply (drule in_sub, drule_tac X=Y in parts_sub, simp) |
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
41775
diff
changeset
|
241 |
apply (auto dest: Nonce_kparts_synth) |
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
41775
diff
changeset
|
242 |
done |
13508 | 243 |
|
39216 | 244 |
lemma Crypt_insert_synth: |
67613 | 245 |
"[| Crypt K Y \<in> parts (insert X G); X \<in> synth (analz G); Nonce n \<in> kparts {Y}; Nonce n \<notin> analz G |] |
246 |
==> Crypt K Y \<in> parts G" |
|
39216 | 247 |
by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5)) |
248 |
||
13508 | 249 |
|
61830 | 250 |
subsection\<open>analz is pparts + analz of kparts\<close> |
13508 | 251 |
|
67613 | 252 |
lemma analz_pparts_kparts: "X \<in> analz H \<Longrightarrow> X \<in> pparts H \<or> X \<in> analz (kparts H)" |
39216 | 253 |
by (erule analz.induct, auto) |
13508 | 254 |
|
255 |
lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)" |
|
256 |
by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz) |
|
257 |
||
258 |
lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst] |
|
39216 | 259 |
lemmas analz_pparts_kparts_substD = analz_pparts_kparts_eq [THEN sym, THEN ssubst] |
13508 | 260 |
|
261 |
end |