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