author | wenzelm |
Mon, 13 Apr 2020 22:08:14 +0200 | |
changeset 71751 | abf3e80bd815 |
parent 69597 | ff784d5a5bfb |
child 76287 | cdc14f94c754 |
permissions | -rw-r--r-- |
41775 | 1 |
(* Title: HOL/Auth/Guard/Extensions.thy |
2 |
Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 |
Copyright 2001 University of Cambridge |
|
4 |
*) |
|
13508 | 5 |
|
61830 | 6 |
section \<open>Extensions to Standard Theories\<close> |
13508 | 7 |
|
32695 | 8 |
theory Extensions |
9 |
imports "../Event" |
|
10 |
begin |
|
13508 | 11 |
|
61830 | 12 |
subsection\<open>Extensions to Theory \<open>Set\<close>\<close> |
13508 | 13 |
|
67613 | 14 |
lemma eq: "[| \<And>x. x\<in>A \<Longrightarrow> x\<in>B; \<And>x. x\<in>B \<Longrightarrow> x\<in>A |] ==> A=B" |
13508 | 15 |
by auto |
16 |
||
67613 | 17 |
lemma insert_Un: "P ({x} \<union> A) \<Longrightarrow> P (insert x A)" |
13508 | 18 |
by simp |
19 |
||
67613 | 20 |
lemma in_sub: "x\<in>A \<Longrightarrow> {x}\<subseteq>A" |
13508 | 21 |
by auto |
22 |
||
23 |
||
61830 | 24 |
subsection\<open>Extensions to Theory \<open>List\<close>\<close> |
13508 | 25 |
|
61830 | 26 |
subsubsection\<open>"remove l x" erase the first element of "l" equal to "x"\<close> |
13508 | 27 |
|
39246 | 28 |
primrec remove :: "'a list => 'a => 'a list" where |
29 |
"remove [] y = []" | |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18557
diff
changeset
|
30 |
"remove (x#xs) y = (if x=y then xs else x # remove xs y)" |
13508 | 31 |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18557
diff
changeset
|
32 |
lemma set_remove: "set (remove l x) <= set l" |
13508 | 33 |
by (induct l, auto) |
34 |
||
61830 | 35 |
subsection\<open>Extensions to Theory \<open>Message\<close>\<close> |
13508 | 36 |
|
61830 | 37 |
subsubsection\<open>declarations for tactics\<close> |
13508 | 38 |
|
39 |
declare analz_subset_parts [THEN subsetD, dest] |
|
40 |
declare parts_insert2 [simp] |
|
41 |
declare analz_cut [dest] |
|
62390 | 42 |
declare if_split_asm [split] |
13508 | 43 |
declare analz_insertI [intro] |
44 |
declare Un_Diff [simp] |
|
45 |
||
61830 | 46 |
subsubsection\<open>extract the agent number of an Agent message\<close> |
13508 | 47 |
|
35418 | 48 |
primrec agt_nb :: "msg => agent" where |
13508 | 49 |
"agt_nb (Agent A) = A" |
50 |
||
61830 | 51 |
subsubsection\<open>messages that are pairs\<close> |
13508 | 52 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
53 |
definition is_MPair :: "msg => bool" where |
67613 | 54 |
"is_MPair X == \<exists>Y Z. X = \<lbrace>Y,Z\<rbrace>" |
13508 | 55 |
|
56 |
declare is_MPair_def [simp] |
|
57 |
||
61956 | 58 |
lemma MPair_is_MPair [iff]: "is_MPair \<lbrace>X,Y\<rbrace>" |
13508 | 59 |
by simp |
60 |
||
61 |
lemma Agent_isnt_MPair [iff]: "~ is_MPair (Agent A)" |
|
62 |
by simp |
|
63 |
||
64 |
lemma Number_isnt_MPair [iff]: "~ is_MPair (Number n)" |
|
65 |
by simp |
|
66 |
||
67 |
lemma Key_isnt_MPair [iff]: "~ is_MPair (Key K)" |
|
68 |
by simp |
|
69 |
||
70 |
lemma Nonce_isnt_MPair [iff]: "~ is_MPair (Nonce n)" |
|
71 |
by simp |
|
72 |
||
73 |
lemma Hash_isnt_MPair [iff]: "~ is_MPair (Hash X)" |
|
74 |
by simp |
|
75 |
||
76 |
lemma Crypt_isnt_MPair [iff]: "~ is_MPair (Crypt K X)" |
|
77 |
by simp |
|
78 |
||
20768 | 79 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
80 |
not_MPair :: "msg => bool" where |
20768 | 81 |
"not_MPair X == ~ is_MPair X" |
13508 | 82 |
|
83 |
lemma is_MPairE: "[| is_MPair X ==> P; not_MPair X ==> P |] ==> P" |
|
84 |
by auto |
|
85 |
||
86 |
declare is_MPair_def [simp del] |
|
87 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
88 |
definition has_no_pair :: "msg set => bool" where |
67613 | 89 |
"has_no_pair H == \<forall>X Y. \<lbrace>X,Y\<rbrace> \<notin> H" |
13508 | 90 |
|
91 |
declare has_no_pair_def [simp] |
|
92 |
||
61830 | 93 |
subsubsection\<open>well-foundedness of messages\<close> |
13508 | 94 |
|
95 |
lemma wf_Crypt1 [iff]: "Crypt K X ~= X" |
|
96 |
by (induct X, auto) |
|
97 |
||
98 |
lemma wf_Crypt2 [iff]: "X ~= Crypt K X" |
|
99 |
by (induct X, auto) |
|
100 |
||
67613 | 101 |
lemma parts_size: "X \<in> parts {Y} \<Longrightarrow> X=Y \<or> size X < size Y" |
13508 | 102 |
by (erule parts.induct, auto) |
103 |
||
67613 | 104 |
lemma wf_Crypt_parts [iff]: "Crypt K X \<notin> parts {X}" |
13508 | 105 |
by (auto dest: parts_size) |
106 |
||
61830 | 107 |
subsubsection\<open>lemmas on keysFor\<close> |
13508 | 108 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
109 |
definition usekeys :: "msg set => key set" where |
67613 | 110 |
"usekeys G \<equiv> {K. \<exists>Y. Crypt K Y \<in> G}" |
13508 | 111 |
|
112 |
lemma finite_keysFor [intro]: "finite G ==> finite (keysFor G)" |
|
113 |
apply (simp add: keysFor_def) |
|
56681 | 114 |
apply (rule finite_imageI) |
115 |
apply (induct G rule: finite_induct) |
|
116 |
apply auto |
|
67613 | 117 |
apply (case_tac "\<exists>K X. x = Crypt K X", clarsimp) |
118 |
apply (subgoal_tac "{Ka. \<exists>Xa. (Ka=K \<and> Xa=X) \<or> Crypt Ka Xa \<in> F} |
|
13508 | 119 |
= insert K (usekeys F)", auto simp: usekeys_def) |
67613 | 120 |
by (subgoal_tac "{K. \<exists>X. Crypt K X = x \<or> Crypt K X \<in> F} = usekeys F", |
13508 | 121 |
auto simp: usekeys_def) |
122 |
||
61830 | 123 |
subsubsection\<open>lemmas on parts\<close> |
13508 | 124 |
|
67613 | 125 |
lemma parts_sub: "[| X \<in> parts G; G \<subseteq> H |] ==> X \<in> parts H" |
13508 | 126 |
by (auto dest: parts_mono) |
127 |
||
67613 | 128 |
lemma parts_Diff [dest]: "X \<in> parts (G - H) \<Longrightarrow> X \<in> parts G" |
13508 | 129 |
by (erule parts_sub, auto) |
130 |
||
67613 | 131 |
lemma parts_Diff_notin: "[| Y \<notin> H; Nonce n \<notin> parts (H - {Y}) |] |
132 |
==> Nonce n \<notin> parts H" |
|
13508 | 133 |
by simp |
134 |
||
135 |
lemmas parts_insert_substI = parts_insert [THEN ssubst] |
|
136 |
lemmas parts_insert_substD = parts_insert [THEN sym, THEN ssubst] |
|
137 |
||
138 |
lemma finite_parts_msg [iff]: "finite (parts {X})" |
|
139 |
by (induct X, auto) |
|
140 |
||
67613 | 141 |
lemma finite_parts [intro]: "finite H \<Longrightarrow> finite (parts H)" |
13508 | 142 |
apply (erule finite_induct, simp) |
143 |
by (rule parts_insert_substI, simp) |
|
144 |
||
67613 | 145 |
lemma parts_parts: "[| X \<in> parts {Y}; Y \<in> parts G |] ==> X \<in> parts G" |
17689
a04b5b43625e
streamlined theory; conformance to recent publication
paulson
parents:
16417
diff
changeset
|
146 |
by (frule parts_cut, auto) |
a04b5b43625e
streamlined theory; conformance to recent publication
paulson
parents:
16417
diff
changeset
|
147 |
|
13508 | 148 |
|
67613 | 149 |
lemma parts_parts_parts: "[| X \<in> parts {Y}; Y \<in> parts {Z}; Z \<in> parts G |] ==> X \<in> parts G" |
13508 | 150 |
by (auto dest: parts_parts) |
151 |
||
67613 | 152 |
lemma parts_parts_Crypt: "[| Crypt K X \<in> parts G; Nonce n \<in> parts {X} |] |
153 |
==> Nonce n \<in> parts G" |
|
13508 | 154 |
by (blast intro: parts.Body dest: parts_parts) |
155 |
||
61830 | 156 |
subsubsection\<open>lemmas on synth\<close> |
13508 | 157 |
|
67613 | 158 |
lemma synth_sub: "[| X \<in> synth G; G \<subseteq> H |] ==> X \<in> synth H" |
13508 | 159 |
by (auto dest: synth_mono) |
160 |
||
67613 | 161 |
lemma Crypt_synth [rule_format]: "[| X \<in> synth G; Key K \<notin> G |] ==> |
162 |
Crypt K Y \<in> parts {X} \<longrightarrow> Crypt K Y \<in> parts G" |
|
13508 | 163 |
by (erule synth.induct, auto dest: parts_sub) |
164 |
||
61830 | 165 |
subsubsection\<open>lemmas on analz\<close> |
13508 | 166 |
|
67613 | 167 |
lemma analz_UnI1 [intro]: "X \<in> analz G ==> X \<in> analz (G \<union> H)" |
32695 | 168 |
by (subgoal_tac "G <= G Un H") (blast dest: analz_mono)+ |
13508 | 169 |
|
67613 | 170 |
lemma analz_sub: "[| X \<in> analz G; G \<subseteq> H |] ==> X \<in> analz H" |
13508 | 171 |
by (auto dest: analz_mono) |
172 |
||
67613 | 173 |
lemma analz_Diff [dest]: "X \<in> analz (G - H) \<Longrightarrow> X \<in> analz G" |
13508 | 174 |
by (erule analz.induct, auto) |
175 |
||
176 |
lemmas in_analz_subset_cong = analz_subset_cong [THEN subsetD] |
|
177 |
||
178 |
lemma analz_eq: "A=A' ==> analz A = analz A'" |
|
179 |
by auto |
|
180 |
||
181 |
lemmas insert_commute_substI = insert_commute [THEN ssubst] |
|
182 |
||
14307 | 183 |
lemma analz_insertD: |
67613 | 184 |
"[| Crypt K Y \<in> H; Key (invKey K) \<in> H |] ==> analz (insert Y H) = analz H" |
14307 | 185 |
by (blast intro: analz.Decrypt analz_insert_eq) |
13508 | 186 |
|
67613 | 187 |
lemma must_decrypt [rule_format,dest]: "[| X \<in> analz H; has_no_pair H |] ==> |
188 |
X \<notin> H \<longrightarrow> (\<exists>K Y. Crypt K Y \<in> H \<and> Key (invKey K) \<in> H)" |
|
13508 | 189 |
by (erule analz.induct, auto) |
190 |
||
67613 | 191 |
lemma analz_needs_only_finite: "X \<in> analz H \<Longrightarrow> \<exists>G. G \<subseteq> H \<and> finite G" |
13508 | 192 |
by (erule analz.induct, auto) |
193 |
||
67613 | 194 |
lemma notin_analz_insert: "X \<notin> analz (insert Y G) \<Longrightarrow> X \<notin> analz G" |
13508 | 195 |
by auto |
196 |
||
61830 | 197 |
subsubsection\<open>lemmas on parts, synth and analz\<close> |
13508 | 198 |
|
67613 | 199 |
lemma parts_invKey [rule_format,dest]:"X \<in> parts {Y} \<Longrightarrow> |
200 |
X \<in> analz (insert (Crypt K Y) H) \<longrightarrow> X \<notin> analz H \<longrightarrow> Key (invKey K) \<in> analz H" |
|
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
45600
diff
changeset
|
201 |
by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body) |
13508 | 202 |
|
67613 | 203 |
lemma in_analz: "Y \<in> analz H \<Longrightarrow> \<exists>X. X \<in> H \<and> Y \<in> parts {X}" |
13508 | 204 |
by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body) |
205 |
||
206 |
lemmas in_analz_subset_parts = analz_subset_parts [THEN subsetD] |
|
207 |
||
67613 | 208 |
lemma Crypt_synth_insert: "[| Crypt K X \<in> parts (insert Y H); |
209 |
Y \<in> synth (analz H); Key K \<notin> analz H |] ==> Crypt K X \<in> parts H" |
|
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
45600
diff
changeset
|
210 |
apply (drule parts_insert_substD, clarify) |
13508 | 211 |
apply (frule in_sub) |
212 |
apply (frule parts_mono) |
|
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
45600
diff
changeset
|
213 |
apply auto |
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
45600
diff
changeset
|
214 |
done |
13508 | 215 |
|
61830 | 216 |
subsubsection\<open>greatest nonce used in a message\<close> |
13508 | 217 |
|
35418 | 218 |
fun greatest_msg :: "msg => nat" |
219 |
where |
|
220 |
"greatest_msg (Nonce n) = n" |
|
61956 | 221 |
| "greatest_msg \<lbrace>X,Y\<rbrace> = max (greatest_msg X) (greatest_msg Y)" |
35418 | 222 |
| "greatest_msg (Crypt K X) = greatest_msg X" |
223 |
| "greatest_msg other = 0" |
|
13508 | 224 |
|
67613 | 225 |
lemma greatest_msg_is_greatest: "Nonce n \<in> parts {X} \<Longrightarrow> n \<le> greatest_msg X" |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19233
diff
changeset
|
226 |
by (induct X, auto) |
13508 | 227 |
|
61830 | 228 |
subsubsection\<open>sets of keys\<close> |
13508 | 229 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
230 |
definition keyset :: "msg set => bool" where |
67613 | 231 |
"keyset G \<equiv> \<forall>X. X \<in> G \<longrightarrow> (\<exists>K. X = Key K)" |
13508 | 232 |
|
67613 | 233 |
lemma keyset_in [dest]: "[| keyset G; X \<in> G |] ==> \<exists>K. X = Key K" |
13508 | 234 |
by (auto simp: keyset_def) |
235 |
||
61956 | 236 |
lemma MPair_notin_keyset [simp]: "keyset G ==> \<lbrace>X,Y\<rbrace> \<notin> G" |
13508 | 237 |
by auto |
238 |
||
67613 | 239 |
lemma Crypt_notin_keyset [simp]: "keyset G \<Longrightarrow> Crypt K X \<notin> G" |
13508 | 240 |
by auto |
241 |
||
67613 | 242 |
lemma Nonce_notin_keyset [simp]: "keyset G \<Longrightarrow> Nonce n \<notin> G" |
13508 | 243 |
by auto |
244 |
||
245 |
lemma parts_keyset [simp]: "keyset G ==> parts G = G" |
|
246 |
by (auto, erule parts.induct, auto) |
|
247 |
||
61830 | 248 |
subsubsection\<open>keys a priori necessary for decrypting the messages of G\<close> |
13508 | 249 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
250 |
definition keysfor :: "msg set => msg set" where |
13508 | 251 |
"keysfor G == Key ` keysFor (parts G)" |
252 |
||
253 |
lemma keyset_keysfor [iff]: "keyset (keysfor G)" |
|
254 |
by (simp add: keyset_def keysfor_def, blast) |
|
255 |
||
256 |
lemma keyset_Diff_keysfor [simp]: "keyset H ==> keyset (H - keysfor G)" |
|
257 |
by (auto simp: keyset_def) |
|
258 |
||
67613 | 259 |
lemma keysfor_Crypt: "Crypt K X \<in> parts G \<Longrightarrow> Key (invKey K) \<in> keysfor G" |
13508 | 260 |
by (auto simp: keysfor_def Crypt_imp_invKey_keysFor) |
261 |
||
67613 | 262 |
lemma no_key_no_Crypt: "Key K \<notin> keysfor G \<Longrightarrow> Crypt (invKey K) X \<notin> parts G" |
13508 | 263 |
by (auto dest: keysfor_Crypt) |
264 |
||
265 |
lemma finite_keysfor [intro]: "finite G ==> finite (keysfor G)" |
|
266 |
by (auto simp: keysfor_def intro: finite_UN_I) |
|
267 |
||
61830 | 268 |
subsubsection\<open>only the keys necessary for G are useful in analz\<close> |
13508 | 269 |
|
270 |
lemma analz_keyset: "keyset H ==> |
|
271 |
analz (G Un H) = H - keysfor G Un (analz (G Un (H Int keysfor G)))" |
|
272 |
apply (rule eq) |
|
273 |
apply (erule analz.induct, blast) |
|
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
17689
diff
changeset
|
274 |
apply (simp, blast) |
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
17689
diff
changeset
|
275 |
apply (simp, blast) |
67613 | 276 |
apply (case_tac "Key (invKey K) \<in> H - keysfor G", clarsimp) |
13508 | 277 |
apply (drule_tac X=X in no_key_no_Crypt) |
278 |
by (auto intro: analz_sub) |
|
279 |
||
280 |
lemmas analz_keyset_substD = analz_keyset [THEN sym, THEN ssubst] |
|
281 |
||
282 |
||
61830 | 283 |
subsection\<open>Extensions to Theory \<open>Event\<close>\<close> |
13508 | 284 |
|
285 |
||
61830 | 286 |
subsubsection\<open>general protocol properties\<close> |
13508 | 287 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
288 |
definition is_Says :: "event => bool" where |
67613 | 289 |
"is_Says ev == (\<exists>A B X. ev = Says A B X)" |
13508 | 290 |
|
291 |
lemma is_Says_Says [iff]: "is_Says (Says A B X)" |
|
292 |
by (simp add: is_Says_def) |
|
293 |
||
294 |
(* one could also require that Gets occurs after Says |
|
295 |
but this is sufficient for our purpose *) |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
296 |
definition Gets_correct :: "event list set => bool" where |
67613 | 297 |
"Gets_correct p == \<forall>evs B X. evs \<in> p \<longrightarrow> Gets B X \<in> set evs |
298 |
\<longrightarrow> (\<exists>A. Says A B X \<in> set evs)" |
|
13508 | 299 |
|
67613 | 300 |
lemma Gets_correct_Says: "[| Gets_correct p; Gets B X # evs \<in> p |] |
301 |
==> \<exists>A. Says A B X \<in> set evs" |
|
13508 | 302 |
apply (simp add: Gets_correct_def) |
303 |
by (drule_tac x="Gets B X # evs" in spec, auto) |
|
304 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
305 |
definition one_step :: "event list set => bool" where |
67613 | 306 |
"one_step p == \<forall>evs ev. ev#evs \<in> p \<longrightarrow> evs \<in> p" |
13508 | 307 |
|
67613 | 308 |
lemma one_step_Cons [dest]: "[| one_step p; ev#evs \<in> p |] ==> evs \<in> p" |
13508 | 309 |
by (unfold one_step_def, blast) |
310 |
||
67613 | 311 |
lemma one_step_app: "[| evs@evs' \<in> p; one_step p; [] \<in> p |] ==> evs' \<in> p" |
13508 | 312 |
by (induct evs, auto) |
313 |
||
67613 | 314 |
lemma trunc: "[| evs @ evs' \<in> p; one_step p |] ==> evs' \<in> p" |
13508 | 315 |
by (induct evs, auto) |
316 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
317 |
definition has_only_Says :: "event list set => bool" where |
67613 | 318 |
"has_only_Says p \<equiv> \<forall>evs ev. evs \<in> p \<longrightarrow> ev \<in> set evs |
319 |
\<longrightarrow> (\<exists>A B X. ev = Says A B X)" |
|
13508 | 320 |
|
67613 | 321 |
lemma has_only_SaysD: "[| ev \<in> set evs; evs \<in> p; has_only_Says p |] |
322 |
==> \<exists>A B X. ev = Says A B X" |
|
13508 | 323 |
by (unfold has_only_Says_def, blast) |
324 |
||
67613 | 325 |
lemma in_has_only_Says [dest]: "[| has_only_Says p; evs \<in> p; ev \<in> set evs |] |
326 |
==> \<exists>A B X. ev = Says A B X" |
|
13508 | 327 |
by (auto simp: has_only_Says_def) |
328 |
||
329 |
lemma has_only_Says_imp_Gets_correct [simp]: "has_only_Says p |
|
330 |
==> Gets_correct p" |
|
331 |
by (auto simp: has_only_Says_def Gets_correct_def) |
|
332 |
||
61830 | 333 |
subsubsection\<open>lemma on knows\<close> |
13508 | 334 |
|
67613 | 335 |
lemma Says_imp_spies2: "Says A B \<lbrace>X,Y\<rbrace> \<in> set evs \<Longrightarrow> Y \<in> parts (spies evs)" |
13508 | 336 |
by (drule Says_imp_spies, drule parts.Inj, drule parts.Snd, simp) |
337 |
||
67613 | 338 |
lemma Says_not_parts: "[| Says A B X \<in> set evs; Y \<notin> parts (spies evs) |] |
339 |
==> Y \<notin> parts {X}" |
|
13508 | 340 |
by (auto dest: Says_imp_spies parts_parts) |
341 |
||
61830 | 342 |
subsubsection\<open>knows without initState\<close> |
13508 | 343 |
|
39246 | 344 |
primrec knows' :: "agent => event list => msg set" where |
345 |
knows'_Nil: "knows' A [] = {}" | |
|
346 |
knows'_Cons0: |
|
14307 | 347 |
"knows' A (ev # evs) = ( |
348 |
if A = Spy then ( |
|
349 |
case ev of |
|
350 |
Says A' B X => insert X (knows' A evs) |
|
351 |
| Gets A' X => knows' A evs |
|
67613 | 352 |
| Notes A' X => if A' \<in> bad then insert X (knows' A evs) else knows' A evs |
14307 | 353 |
) else ( |
354 |
case ev of |
|
355 |
Says A' B X => if A=A' then insert X (knows' A evs) else knows' A evs |
|
356 |
| Gets A' X => if A=A' then insert X (knows' A evs) else knows' A evs |
|
357 |
| Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs |
|
358 |
))" |
|
13508 | 359 |
|
20768 | 360 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
361 |
spies' :: "event list => msg set" where |
20768 | 362 |
"spies' == knows' Spy" |
13508 | 363 |
|
61830 | 364 |
subsubsection\<open>decomposition of knows into knows' and initState\<close> |
13508 | 365 |
|
366 |
lemma knows_decomp: "knows A evs = knows' A evs Un (initState A)" |
|
367 |
by (induct evs, auto split: event.split simp: knows.simps) |
|
368 |
||
369 |
lemmas knows_decomp_substI = knows_decomp [THEN ssubst] |
|
370 |
lemmas knows_decomp_substD = knows_decomp [THEN sym, THEN ssubst] |
|
371 |
||
372 |
lemma knows'_sub_knows: "knows' A evs <= knows A evs" |
|
373 |
by (auto simp: knows_decomp) |
|
374 |
||
375 |
lemma knows'_Cons: "knows' A (ev#evs) = knows' A [ev] Un knows' A evs" |
|
376 |
by (induct ev, auto) |
|
377 |
||
378 |
lemmas knows'_Cons_substI = knows'_Cons [THEN ssubst] |
|
379 |
lemmas knows'_Cons_substD = knows'_Cons [THEN sym, THEN ssubst] |
|
380 |
||
381 |
lemma knows_Cons: "knows A (ev#evs) = initState A Un knows' A [ev] |
|
382 |
Un knows A evs" |
|
383 |
apply (simp only: knows_decomp) |
|
384 |
apply (rule_tac s="(knows' A [ev] Un knows' A evs) Un initState A" in trans) |
|
14307 | 385 |
apply (simp only: knows'_Cons [of A ev evs] Un_ac) |
386 |
apply blast |
|
387 |
done |
|
388 |
||
13508 | 389 |
|
390 |
lemmas knows_Cons_substI = knows_Cons [THEN ssubst] |
|
391 |
lemmas knows_Cons_substD = knows_Cons [THEN sym, THEN ssubst] |
|
392 |
||
67613 | 393 |
lemma knows'_sub_spies': "[| evs \<in> p; has_only_Says p; one_step p |] |
394 |
==> knows' A evs \<subseteq> spies' evs" |
|
13508 | 395 |
by (induct evs, auto split: event.splits) |
396 |
||
61830 | 397 |
subsubsection\<open>knows' is finite\<close> |
13508 | 398 |
|
399 |
lemma finite_knows' [iff]: "finite (knows' A evs)" |
|
400 |
by (induct evs, auto split: event.split simp: knows.simps) |
|
401 |
||
61830 | 402 |
subsubsection\<open>monotonicity of knows\<close> |
13508 | 403 |
|
404 |
lemma knows_sub_Cons: "knows A evs <= knows A (ev#evs)" |
|
13596 | 405 |
by(cases A, induct evs, auto simp: knows.simps split:event.split) |
13508 | 406 |
|
67613 | 407 |
lemma knows_ConsI: "X \<in> knows A evs \<Longrightarrow> X \<in> knows A (ev#evs)" |
13508 | 408 |
by (auto dest: knows_sub_Cons [THEN subsetD]) |
409 |
||
410 |
lemma knows_sub_app: "knows A evs <= knows A (evs @ evs')" |
|
411 |
apply (induct evs, auto) |
|
412 |
apply (simp add: knows_decomp) |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
46008
diff
changeset
|
413 |
apply (rename_tac a b c) |
13508 | 414 |
by (case_tac a, auto simp: knows.simps) |
415 |
||
61830 | 416 |
subsubsection\<open>maximum knowledge an agent can have |
417 |
includes messages sent to the agent\<close> |
|
13508 | 418 |
|
39246 | 419 |
primrec knows_max' :: "agent => event list => msg set" where |
420 |
knows_max'_def_Nil: "knows_max' A [] = {}" | |
|
13508 | 421 |
knows_max'_def_Cons: "knows_max' A (ev # evs) = ( |
422 |
if A=Spy then ( |
|
423 |
case ev of |
|
424 |
Says A' B X => insert X (knows_max' A evs) |
|
425 |
| Gets A' X => knows_max' A evs |
|
426 |
| Notes A' X => |
|
67613 | 427 |
if A' \<in> bad then insert X (knows_max' A evs) else knows_max' A evs |
13508 | 428 |
) else ( |
429 |
case ev of |
|
430 |
Says A' B X => |
|
431 |
if A=A' | A=B then insert X (knows_max' A evs) else knows_max' A evs |
|
432 |
| Gets A' X => |
|
433 |
if A=A' then insert X (knows_max' A evs) else knows_max' A evs |
|
434 |
| Notes A' X => |
|
435 |
if A=A' then insert X (knows_max' A evs) else knows_max' A evs |
|
436 |
))" |
|
437 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
438 |
definition knows_max :: "agent => event list => msg set" where |
13508 | 439 |
"knows_max A evs == knows_max' A evs Un initState A" |
440 |
||
20768 | 441 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
442 |
spies_max :: "event list => msg set" where |
20768 | 443 |
"spies_max evs == knows_max Spy evs" |
13508 | 444 |
|
69597 | 445 |
subsubsection\<open>basic facts about \<^term>\<open>knows_max\<close>\<close> |
13508 | 446 |
|
447 |
lemma spies_max_spies [iff]: "spies_max evs = spies evs" |
|
448 |
by (induct evs, auto simp: knows_max_def split: event.splits) |
|
449 |
||
450 |
lemma knows_max'_Cons: "knows_max' A (ev#evs) |
|
451 |
= knows_max' A [ev] Un knows_max' A evs" |
|
452 |
by (auto split: event.splits) |
|
453 |
||
454 |
lemmas knows_max'_Cons_substI = knows_max'_Cons [THEN ssubst] |
|
455 |
lemmas knows_max'_Cons_substD = knows_max'_Cons [THEN sym, THEN ssubst] |
|
456 |
||
457 |
lemma knows_max_Cons: "knows_max A (ev#evs) |
|
458 |
= knows_max' A [ev] Un knows_max A evs" |
|
459 |
apply (simp add: knows_max_def del: knows_max'_def_Cons) |
|
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
44890
diff
changeset
|
460 |
apply (rule_tac evs=evs in knows_max'_Cons_substI) |
13508 | 461 |
by blast |
462 |
||
463 |
lemmas knows_max_Cons_substI = knows_max_Cons [THEN ssubst] |
|
464 |
lemmas knows_max_Cons_substD = knows_max_Cons [THEN sym, THEN ssubst] |
|
465 |
||
466 |
lemma finite_knows_max' [iff]: "finite (knows_max' A evs)" |
|
467 |
by (induct evs, auto split: event.split) |
|
468 |
||
67613 | 469 |
lemma knows_max'_sub_spies': "[| evs \<in> p; has_only_Says p; one_step p |] |
470 |
==> knows_max' A evs \<subseteq> spies' evs" |
|
13508 | 471 |
by (induct evs, auto split: event.splits) |
472 |
||
67613 | 473 |
lemma knows_max'_in_spies' [dest]: "[| evs \<in> p; X \<in> knows_max' A evs; |
474 |
has_only_Says p; one_step p |] ==> X \<in> spies' evs" |
|
13508 | 475 |
by (rule knows_max'_sub_spies' [THEN subsetD], auto) |
476 |
||
477 |
lemma knows_max'_app: "knows_max' A (evs @ evs') |
|
478 |
= knows_max' A evs Un knows_max' A evs'" |
|
479 |
by (induct evs, auto split: event.splits) |
|
480 |
||
67613 | 481 |
lemma Says_to_knows_max': "Says A B X \<in> set evs \<Longrightarrow> X \<in> knows_max' B evs" |
13508 | 482 |
by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app) |
483 |
||
67613 | 484 |
lemma Says_from_knows_max': "Says A B X \<in> set evs \<Longrightarrow> X \<in> knows_max' A evs" |
13508 | 485 |
by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app) |
486 |
||
61830 | 487 |
subsubsection\<open>used without initState\<close> |
13508 | 488 |
|
39246 | 489 |
primrec used' :: "event list => msg set" where |
490 |
"used' [] = {}" | |
|
13508 | 491 |
"used' (ev # evs) = ( |
492 |
case ev of |
|
493 |
Says A B X => parts {X} Un used' evs |
|
494 |
| Gets A X => used' evs |
|
495 |
| Notes A X => parts {X} Un used' evs |
|
496 |
)" |
|
497 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32695
diff
changeset
|
498 |
definition init :: "msg set" where |
13508 | 499 |
"init == used []" |
500 |
||
501 |
lemma used_decomp: "used evs = init Un used' evs" |
|
502 |
by (induct evs, auto simp: init_def split: event.split) |
|
503 |
||
67613 | 504 |
lemma used'_sub_app: "used' evs \<subseteq> used' (evs@evs')" |
13508 | 505 |
by (induct evs, auto split: event.split) |
506 |
||
67613 | 507 |
lemma used'_parts [rule_format]: "X \<in> used' evs \<Longrightarrow> Y \<in> parts {X} \<longrightarrow> Y \<in> used' evs" |
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
46008
diff
changeset
|
508 |
apply (induct evs, simp) |
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
46008
diff
changeset
|
509 |
apply (rename_tac a b) |
13508 | 510 |
apply (case_tac a, simp_all) |
58860 | 511 |
apply (blast dest: parts_trans)+ |
13508 | 512 |
done |
513 |
||
61830 | 514 |
subsubsection\<open>monotonicity of used\<close> |
13508 | 515 |
|
516 |
lemma used_sub_Cons: "used evs <= used (ev#evs)" |
|
517 |
by (induct evs, (induct ev, auto)+) |
|
518 |
||
67613 | 519 |
lemma used_ConsI: "X \<in> used evs \<Longrightarrow> X \<in> used (ev#evs)" |
13508 | 520 |
by (auto dest: used_sub_Cons [THEN subsetD]) |
521 |
||
67613 | 522 |
lemma notin_used_ConsD: "X \<notin> used (ev#evs) \<Longrightarrow> X \<notin> used evs" |
13508 | 523 |
by (auto dest: used_sub_Cons [THEN subsetD]) |
524 |
||
67613 | 525 |
lemma used_appD [dest]: "X \<in> used (evs @ evs') \<Longrightarrow> X \<in> used evs \<or> X \<in> used evs'" |
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
46008
diff
changeset
|
526 |
by (induct evs, auto, rename_tac a b, case_tac a, auto) |
13508 | 527 |
|
67613 | 528 |
lemma used_ConsD: "X \<in> used (ev#evs) \<Longrightarrow> X \<in> used [ev] \<or> X \<in> used evs" |
13508 | 529 |
by (case_tac ev, auto) |
530 |
||
531 |
lemma used_sub_app: "used evs <= used (evs@evs')" |
|
532 |
by (auto simp: used_decomp dest: used'_sub_app [THEN subsetD]) |
|
533 |
||
67613 | 534 |
lemma used_appIL: "X \<in> used evs \<Longrightarrow> X \<in> used (evs' @ evs)" |
13508 | 535 |
by (induct evs', auto intro: used_ConsI) |
536 |
||
67613 | 537 |
lemma used_appIR: "X \<in> used evs \<Longrightarrow> X \<in> used (evs @ evs')" |
13508 | 538 |
by (erule used_sub_app [THEN subsetD]) |
539 |
||
67613 | 540 |
lemma used_parts: "[| X \<in> parts {Y}; Y \<in> used evs |] ==> X \<in> used evs" |
13508 | 541 |
apply (auto simp: used_decomp dest: used'_parts) |
542 |
by (auto simp: init_def used_Nil dest: parts_trans) |
|
543 |
||
67613 | 544 |
lemma parts_Says_used: "[| Says A B X \<in> set evs; Y \<in> parts {X} |] ==> Y \<in> used evs" |
13508 | 545 |
by (induct evs, simp_all, safe, auto intro: used_ConsI) |
546 |
||
67613 | 547 |
lemma parts_used_app: "X \<in> parts {Y} \<Longrightarrow> X \<in> used (evs @ Says A B Y # evs')" |
13508 | 548 |
apply (drule_tac evs="[Says A B Y]" in used_parts, simp, blast) |
549 |
apply (drule_tac evs'=evs' in used_appIR) |
|
550 |
apply (drule_tac evs'=evs in used_appIL) |
|
551 |
by simp |
|
552 |
||
61830 | 553 |
subsubsection\<open>lemmas on used and knows\<close> |
13508 | 554 |
|
67613 | 555 |
lemma initState_used: "X \<in> parts (initState A) \<Longrightarrow> X \<in> used evs" |
13508 | 556 |
by (induct evs, auto simp: used.simps split: event.split) |
557 |
||
67613 | 558 |
lemma Says_imp_used: "Says A B X \<in> set evs \<Longrightarrow> parts {X} \<subseteq> used evs" |
13508 | 559 |
by (induct evs, auto intro: used_ConsI) |
560 |
||
67613 | 561 |
lemma not_used_not_spied: "X \<notin> used evs \<Longrightarrow> X \<notin> parts (spies evs)" |
13508 | 562 |
by (induct evs, auto simp: used_Nil) |
563 |
||
67613 | 564 |
lemma not_used_not_parts: "[| Y \<notin> used evs; Says A B X \<in> set evs |] |
565 |
==> Y \<notin> parts {X}" |
|
13508 | 566 |
by (induct evs, auto intro: used_ConsI) |
567 |
||
67613 | 568 |
lemma not_used_parts_false: "[| X \<notin> used evs; Y \<in> parts (spies evs) |] |
569 |
==> X \<notin> parts {Y}" |
|
13508 | 570 |
by (auto dest: parts_parts) |
571 |
||
67613 | 572 |
lemma known_used [rule_format]: "[| evs \<in> p; Gets_correct p; one_step p |] |
573 |
==> X \<in> parts (knows A evs) \<longrightarrow> X \<in> used evs" |
|
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
17689
diff
changeset
|
574 |
apply (case_tac "A=Spy", blast) |
13508 | 575 |
apply (induct evs) |
576 |
apply (simp add: used.simps, blast) |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
46008
diff
changeset
|
577 |
apply (rename_tac a evs) |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14307
diff
changeset
|
578 |
apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify) |
67613 | 579 |
apply (drule_tac P="\<lambda>G. X \<in> parts G" in knows_Cons_substD, safe) |
13508 | 580 |
apply (erule initState_used) |
581 |
apply (case_tac a, auto) |
|
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
56681
diff
changeset
|
582 |
apply (rename_tac msg) |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14307
diff
changeset
|
583 |
apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says) |
13508 | 584 |
by (auto dest: Says_imp_used intro: used_ConsI) |
585 |
||
67613 | 586 |
lemma known_max_used [rule_format]: "[| evs \<in> p; Gets_correct p; one_step p |] |
587 |
==> X \<in> parts (knows_max A evs) \<longrightarrow> X \<in> used evs" |
|
13508 | 588 |
apply (case_tac "A=Spy") |
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
17689
diff
changeset
|
589 |
apply force |
13508 | 590 |
apply (induct evs) |
591 |
apply (simp add: knows_max_def used.simps, blast) |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
46008
diff
changeset
|
592 |
apply (rename_tac a evs) |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14307
diff
changeset
|
593 |
apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify) |
67613 | 594 |
apply (drule_tac P="\<lambda>G. X \<in> parts G" in knows_max_Cons_substD, safe) |
13508 | 595 |
apply (case_tac a, auto) |
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
56681
diff
changeset
|
596 |
apply (rename_tac msg) |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14307
diff
changeset
|
597 |
apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says) |
13508 | 598 |
by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI) |
599 |
||
67613 | 600 |
lemma not_used_not_known: "[| evs \<in> p; X \<notin> used evs; |
601 |
Gets_correct p; one_step p |] ==> X \<notin> parts (knows A evs)" |
|
13508 | 602 |
by (case_tac "A=Spy", auto dest: not_used_not_spied known_used) |
603 |
||
67613 | 604 |
lemma not_used_not_known_max: "[| evs \<in> p; X \<notin> used evs; |
605 |
Gets_correct p; one_step p |] ==> X \<notin> parts (knows_max A evs)" |
|
13508 | 606 |
by (case_tac "A=Spy", auto dest: not_used_not_spied known_max_used) |
607 |
||
61830 | 608 |
subsubsection\<open>a nonce or key in a message cannot equal a fresh nonce or key\<close> |
13508 | 609 |
|
67613 | 610 |
lemma Nonce_neq [dest]: "[| Nonce n' \<notin> used evs; |
611 |
Says A B X \<in> set evs; Nonce n \<in> parts {X} |] ==> n \<noteq> n'" |
|
13508 | 612 |
by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub) |
613 |
||
67613 | 614 |
lemma Key_neq [dest]: "[| Key n' \<notin> used evs; |
615 |
Says A B X \<in> set evs; Key n \<in> parts {X} |] ==> n ~= n'" |
|
13508 | 616 |
by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub) |
617 |
||
61830 | 618 |
subsubsection\<open>message of an event\<close> |
13508 | 619 |
|
35418 | 620 |
primrec msg :: "event => msg" |
621 |
where |
|
622 |
"msg (Says A B X) = X" |
|
623 |
| "msg (Gets A X) = X" |
|
624 |
| "msg (Notes A X) = X" |
|
13508 | 625 |
|
67613 | 626 |
lemma used_sub_parts_used: "X \<in> used (ev # evs) ==> X \<in> parts {msg ev} \<union> used evs" |
13508 | 627 |
by (induct ev, auto) |
628 |
||
629 |
end |