author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 27108 | e447b3107696 |
child 35418 | 83b0f75810f0 |
permissions | -rw-r--r-- |
13508 | 1 |
(****************************************************************************** |
2 |
very similar to Guard except: |
|
3 |
- Guard is replaced by GuardK, guard by guardK, Nonce by Key |
|
4 |
- some scripts are slightly modified (+ keyset_in, kparts_parts) |
|
5 |
- the hypothesis Key n ~:G (keyset G) is added |
|
6 |
||
7 |
date: march 2002 |
|
8 |
author: Frederic Blanqui |
|
9 |
email: blanqui@lri.fr |
|
10 |
webpage: http://www.lri.fr/~blanqui/ |
|
11 |
||
12 |
University of Cambridge, Computer Laboratory |
|
13 |
William Gates Building, JJ Thomson Avenue |
|
14 |
Cambridge CB3 0FD, United Kingdom |
|
15 |
******************************************************************************) |
|
16 |
||
17 |
header{*protocol-independent confidentiality theorem on keys*} |
|
18 |
||
27108 | 19 |
theory GuardK |
20 |
imports Analz Extensions |
|
21 |
begin |
|
13508 | 22 |
|
23 |
(****************************************************************************** |
|
24 |
messages where all the occurrences of Key n are |
|
25 |
in a sub-message of the form Crypt (invKey K) X with K:Ks |
|
26 |
******************************************************************************) |
|
27 |
||
23746 | 28 |
inductive_set |
29 |
guardK :: "nat => key set => msg set" |
|
30 |
for n :: nat and Ks :: "key set" |
|
31 |
where |
|
32 |
No_Key [intro]: "Key n ~:parts {X} ==> X:guardK n Ks" |
|
33 |
| Guard_Key [intro]: "invKey K:Ks ==> Crypt K X:guardK n Ks" |
|
34 |
| Crypt [intro]: "X:guardK n Ks ==> Crypt K X:guardK n Ks" |
|
35 |
| Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> {|X,Y|}:guardK n Ks" |
|
13508 | 36 |
|
37 |
subsection{*basic facts about @{term guardK}*} |
|
38 |
||
39 |
lemma Nonce_is_guardK [iff]: "Nonce p:guardK n Ks" |
|
40 |
by auto |
|
41 |
||
42 |
lemma Agent_is_guardK [iff]: "Agent A:guardK n Ks" |
|
43 |
by auto |
|
44 |
||
45 |
lemma Number_is_guardK [iff]: "Number r:guardK n Ks" |
|
46 |
by auto |
|
47 |
||
48 |
lemma Key_notin_guardK: "X:guardK n Ks ==> X ~= Key n" |
|
49 |
by (erule guardK.induct, auto) |
|
50 |
||
51 |
lemma Key_notin_guardK_iff [iff]: "Key n ~:guardK n Ks" |
|
52 |
by (auto dest: Key_notin_guardK) |
|
53 |
||
54 |
lemma guardK_has_Crypt [rule_format]: "X:guardK n Ks ==> Key n:parts {X} |
|
55 |
--> (EX K Y. Crypt K Y:kparts {X} & Key n:parts {Y})" |
|
56 |
by (erule guardK.induct, auto) |
|
57 |
||
58 |
lemma Key_notin_kparts_msg: "X:guardK n Ks ==> Key n ~:kparts {X}" |
|
59 |
by (erule guardK.induct, auto dest: kparts_parts) |
|
60 |
||
61 |
lemma Key_in_kparts_imp_no_guardK: "Key n:kparts H |
|
62 |
==> EX X. X:H & X ~:guardK n Ks" |
|
63 |
apply (drule in_kparts, clarify) |
|
64 |
apply (rule_tac x=X in exI, clarify) |
|
65 |
by (auto dest: Key_notin_kparts_msg) |
|
66 |
||
67 |
lemma guardK_kparts [rule_format]: "X:guardK n Ks ==> |
|
68 |
Y:kparts {X} --> Y:guardK n Ks" |
|
69 |
by (erule guardK.induct, auto dest: kparts_parts parts_sub) |
|
70 |
||
71 |
lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks" |
|
72 |
by (ind_cases "Crypt K Y:guardK n Ks", auto) |
|
73 |
||
74 |
lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks) |
|
75 |
= (X:guardK n Ks & Y:guardK n Ks)" |
|
76 |
by (auto, (ind_cases "{|X,Y|}:guardK n Ks", auto)+) |
|
77 |
||
78 |
lemma guardK_not_guardK [rule_format]: "X:guardK n Ks ==> |
|
79 |
Crypt K Y:kparts {X} --> Key n:kparts {Y} --> Y ~:guardK n Ks" |
|
80 |
by (erule guardK.induct, auto dest: guardK_kparts) |
|
81 |
||
82 |
lemma guardK_extand: "[| X:guardK n Ks; Ks <= Ks'; |
|
83 |
[| K:Ks'; K ~:Ks |] ==> Key K ~:parts {X} |] ==> X:guardK n Ks'" |
|
84 |
by (erule guardK.induct, auto) |
|
85 |
||
86 |
subsection{*guarded sets*} |
|
87 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27108
diff
changeset
|
88 |
definition GuardK :: "nat => key set => msg set => bool" where |
13508 | 89 |
"GuardK n Ks H == ALL X. X:H --> X:guardK n Ks" |
90 |
||
91 |
subsection{*basic facts about @{term GuardK}*} |
|
92 |
||
93 |
lemma GuardK_empty [iff]: "GuardK n Ks {}" |
|
94 |
by (simp add: GuardK_def) |
|
95 |
||
96 |
lemma Key_notin_kparts [simplified]: "GuardK n Ks H ==> Key n ~:kparts H" |
|
97 |
by (auto simp: GuardK_def dest: in_kparts Key_notin_kparts_msg) |
|
98 |
||
99 |
lemma GuardK_must_decrypt: "[| GuardK n Ks H; Key n:analz H |] ==> |
|
100 |
EX K Y. Crypt K Y:kparts H & Key (invKey K):kparts H" |
|
101 |
apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp) |
|
102 |
by (drule must_decrypt, auto dest: Key_notin_kparts) |
|
103 |
||
104 |
lemma GuardK_kparts [intro]: "GuardK n Ks H ==> GuardK n Ks (kparts H)" |
|
105 |
by (auto simp: GuardK_def dest: in_kparts guardK_kparts) |
|
106 |
||
107 |
lemma GuardK_mono: "[| GuardK n Ks H; G <= H |] ==> GuardK n Ks G" |
|
108 |
by (auto simp: GuardK_def) |
|
109 |
||
110 |
lemma GuardK_insert [iff]: "GuardK n Ks (insert X H) |
|
111 |
= (GuardK n Ks H & X:guardK n Ks)" |
|
112 |
by (auto simp: GuardK_def) |
|
113 |
||
114 |
lemma GuardK_Un [iff]: "GuardK n Ks (G Un H) = (GuardK n Ks G & GuardK n Ks H)" |
|
115 |
by (auto simp: GuardK_def) |
|
116 |
||
117 |
lemma GuardK_synth [intro]: "GuardK n Ks G ==> GuardK n Ks (synth G)" |
|
118 |
by (auto simp: GuardK_def, erule synth.induct, auto) |
|
119 |
||
120 |
lemma GuardK_analz [intro]: "[| GuardK n Ks G; ALL K. K:Ks --> Key K ~:analz G |] |
|
121 |
==> GuardK n Ks (analz G)" |
|
122 |
apply (auto simp: GuardK_def) |
|
123 |
apply (erule analz.induct, auto) |
|
23746 | 124 |
by (ind_cases "Crypt K Xa:guardK n Ks" for K Xa, auto) |
13508 | 125 |
|
126 |
lemma in_GuardK [dest]: "[| X:G; GuardK n Ks G |] ==> X:guardK n Ks" |
|
127 |
by (auto simp: GuardK_def) |
|
128 |
||
129 |
lemma in_synth_GuardK: "[| X:synth G; GuardK n Ks G |] ==> X:guardK n Ks" |
|
130 |
by (drule GuardK_synth, auto) |
|
131 |
||
132 |
lemma in_analz_GuardK: "[| X:analz G; GuardK n Ks G; |
|
133 |
ALL K. K:Ks --> Key K ~:analz G |] ==> X:guardK n Ks" |
|
134 |
by (drule GuardK_analz, auto) |
|
135 |
||
136 |
lemma GuardK_keyset [simp]: "[| keyset G; Key n ~:G |] ==> GuardK n Ks G" |
|
137 |
by (simp only: GuardK_def, clarify, drule keyset_in, auto) |
|
138 |
||
139 |
lemma GuardK_Un_keyset: "[| GuardK n Ks G; keyset H; Key n ~:H |] |
|
140 |
==> GuardK n Ks (G Un H)" |
|
141 |
by auto |
|
142 |
||
143 |
lemma in_GuardK_kparts: "[| X:G; GuardK n Ks G; Y:kparts {X} |] ==> Y:guardK n Ks" |
|
144 |
by blast |
|
145 |
||
146 |
lemma in_GuardK_kparts_neq: "[| X:G; GuardK n Ks G; Key n':kparts {X} |] |
|
147 |
==> n ~= n'" |
|
148 |
by (blast dest: in_GuardK_kparts) |
|
149 |
||
150 |
lemma in_GuardK_kparts_Crypt: "[| X:G; GuardK n Ks G; is_MPair X; |
|
151 |
Crypt K Y:kparts {X}; Key n:kparts {Y} |] ==> invKey K:Ks" |
|
152 |
apply (drule in_GuardK, simp) |
|
153 |
apply (frule guardK_not_guardK, simp+) |
|
154 |
apply (drule guardK_kparts, simp) |
|
155 |
by (ind_cases "Crypt K Y:guardK n Ks", auto) |
|
156 |
||
157 |
lemma GuardK_extand: "[| GuardK n Ks G; Ks <= Ks'; |
|
158 |
[| K:Ks'; K ~:Ks |] ==> Key K ~:parts G |] ==> GuardK n Ks' G" |
|
159 |
by (auto simp: GuardK_def dest: guardK_extand parts_sub) |
|
160 |
||
161 |
subsection{*set obtained by decrypting a message*} |
|
162 |
||
20768 | 163 |
abbreviation (input) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
164 |
decrypt :: "msg set => key => msg => msg set" where |
20768 | 165 |
"decrypt H K Y == insert Y (H - {Crypt K Y})" |
13508 | 166 |
|
167 |
lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |] |
|
168 |
==> Key n:analz (decrypt H K Y)" |
|
14307 | 169 |
apply (drule_tac P="%H. Key n:analz H" in ssubst [OF insert_Diff]) |
170 |
apply assumption |
|
171 |
apply (simp only: analz_Crypt_if, simp) |
|
172 |
done |
|
13508 | 173 |
|
174 |
lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H" |
|
175 |
by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body) |
|
176 |
||
177 |
subsection{*number of Crypt's in a message*} |
|
178 |
||
179 |
consts crypt_nb :: "msg => nat" |
|
180 |
||
181 |
recdef crypt_nb "measure size" |
|
182 |
"crypt_nb (Crypt K X) = Suc (crypt_nb X)" |
|
183 |
"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y" |
|
184 |
"crypt_nb X = 0" (* otherwise *) |
|
185 |
||
186 |
subsection{*basic facts about @{term crypt_nb}*} |
|
187 |
||
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
23746
diff
changeset
|
188 |
lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0" |
13508 | 189 |
by (induct X, simp_all, safe, simp_all) |
190 |
||
191 |
subsection{*number of Crypt's in a message list*} |
|
192 |
||
193 |
consts cnb :: "msg list => nat" |
|
194 |
||
195 |
recdef cnb "measure size" |
|
196 |
"cnb [] = 0" |
|
197 |
"cnb (X#l) = crypt_nb X + cnb l" |
|
198 |
||
199 |
subsection{*basic facts about @{term cnb}*} |
|
200 |
||
201 |
lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'" |
|
202 |
by (induct l, auto) |
|
203 |
||
204 |
lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)" |
|
205 |
by (induct l, auto) |
|
206 |
||
207 |
lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst] |
|
208 |
||
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17087
diff
changeset
|
209 |
lemma cnb_minus [simp]: "x mem l ==> cnb (remove l x) = cnb l - crypt_nb x" |
13508 | 210 |
apply (induct l, auto) |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14307
diff
changeset
|
211 |
by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp) |
13508 | 212 |
|
213 |
lemma parts_cnb: "Z:parts (set l) ==> |
|
214 |
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z" |
|
215 |
by (erule parts.induct, auto simp: in_set_conv_decomp) |
|
216 |
||
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
23746
diff
changeset
|
217 |
lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0" |
13508 | 218 |
by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD) |
219 |
||
220 |
subsection{*list of kparts*} |
|
221 |
||
222 |
lemma kparts_msg_set: "EX l. kparts {X} = set l & cnb l = crypt_nb X" |
|
223 |
apply (induct X, simp_all) |
|
224 |
apply (rule_tac x="[Agent agent]" in exI, simp) |
|
225 |
apply (rule_tac x="[Number nat]" in exI, simp) |
|
226 |
apply (rule_tac x="[Nonce nat]" in exI, simp) |
|
227 |
apply (rule_tac x="[Key nat]" in exI, simp) |
|
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14307
diff
changeset
|
228 |
apply (rule_tac x="[Hash X]" in exI, simp) |
13508 | 229 |
apply (clarify, rule_tac x="l@la" in exI, simp) |
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14307
diff
changeset
|
230 |
by (clarify, rule_tac x="[Crypt nat X]" in exI, simp) |
13508 | 231 |
|
232 |
lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l" |
|
233 |
apply (induct l) |
|
234 |
apply (rule_tac x="[]" in exI, simp, clarsimp) |
|
15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14307
diff
changeset
|
235 |
apply (subgoal_tac "EX l''. kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify) |
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
14307
diff
changeset
|
236 |
apply (rule_tac x="l''@l'" in exI, simp) |
13508 | 237 |
apply (rule kparts_insert_substI, simp) |
238 |
by (rule kparts_msg_set) |
|
239 |
||
240 |
subsection{*list corresponding to "decrypt"*} |
|
241 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
27108
diff
changeset
|
242 |
definition decrypt' :: "msg list => key => msg => msg list" where |
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17087
diff
changeset
|
243 |
"decrypt' l K Y == Y # remove l (Crypt K Y)" |
13508 | 244 |
|
245 |
declare decrypt'_def [simp] |
|
246 |
||
247 |
subsection{*basic facts about @{term decrypt'}*} |
|
248 |
||
249 |
lemma decrypt_minus: "decrypt (set l) K Y <= set (decrypt' l K Y)" |
|
250 |
by (induct l, auto) |
|
251 |
||
252 |
text{*if the analysis of a finite guarded set gives n then it must also give |
|
253 |
one of the keys of Ks*} |
|
254 |
||
255 |
lemma GuardK_invKey_by_list [rule_format]: "ALL l. cnb l = p |
|
256 |
--> GuardK n Ks (set l) --> Key n:analz (set l) |
|
257 |
--> (EX K. K:Ks & Key K:analz (set l))" |
|
258 |
apply (induct p) |
|
259 |
(* case p=0 *) |
|
260 |
apply (clarify, drule GuardK_must_decrypt, simp, clarify) |
|
261 |
apply (drule kparts_parts, drule non_empty_crypt, simp) |
|
262 |
(* case p>0 *) |
|
263 |
apply (clarify, frule GuardK_must_decrypt, simp, clarify) |
|
264 |
apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp) |
|
265 |
apply (frule analz_decrypt, simp_all) |
|
266 |
apply (subgoal_tac "EX l'. kparts (set l) = set l' & cnb l' = cnb l", clarsimp) |
|
267 |
apply (drule_tac G="insert Y (set l' - {Crypt K Y})" |
|
268 |
and H="set (decrypt' l' K Y)" in analz_sub, rule decrypt_minus) |
|
269 |
apply (rule_tac analz_pparts_kparts_substI, simp) |
|
270 |
apply (case_tac "K:invKey`Ks") |
|
271 |
(* K:invKey`Ks *) |
|
272 |
apply (clarsimp, blast) |
|
273 |
(* K ~:invKey`Ks *) |
|
274 |
apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))") |
|
17087 | 275 |
apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff) |
13508 | 276 |
apply (subgoal_tac "Crypt K Y:parts (set l)") |
277 |
apply (drule parts_cnb, rotate_tac -1, simp) |
|
278 |
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17087
diff
changeset
|
279 |
apply (rule insert_mono, rule set_remove) |
13508 | 280 |
apply (simp add: analz_insertD, blast) |
281 |
(* Crypt K Y:parts (set l) *) |
|
282 |
apply (blast dest: kparts_parts) |
|
283 |
(* GuardK n Ks (set (decrypt' l' K Y)) *) |
|
284 |
apply (rule_tac H="insert Y (set l')" in GuardK_mono) |
|
285 |
apply (subgoal_tac "GuardK n Ks (set l')", simp) |
|
286 |
apply (rule_tac K=K in guardK_Crypt, simp add: GuardK_def, simp) |
|
287 |
apply (drule_tac t="set l'" in sym, simp) |
|
288 |
apply (rule GuardK_kparts, simp, simp) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17087
diff
changeset
|
289 |
apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast) |
13508 | 290 |
by (rule kparts_set) |
291 |
||
292 |
lemma GuardK_invKey_finite: "[| Key n:analz G; GuardK n Ks G; finite G |] |
|
293 |
==> EX K. K:Ks & Key K:analz G" |
|
294 |
apply (drule finite_list, clarify) |
|
295 |
by (rule GuardK_invKey_by_list, auto) |
|
296 |
||
297 |
lemma GuardK_invKey: "[| Key n:analz G; GuardK n Ks G |] |
|
298 |
==> EX K. K:Ks & Key K:analz G" |
|
299 |
by (auto dest: analz_needs_only_finite GuardK_invKey_finite) |
|
300 |
||
301 |
text{*if the analyse of a finite guarded set and a (possibly infinite) set of |
|
302 |
keys gives n then it must also gives Ks*} |
|
303 |
||
304 |
lemma GuardK_invKey_keyset: "[| Key n:analz (G Un H); GuardK n Ks G; finite G; |
|
305 |
keyset H; Key n ~:H |] ==> EX K. K:Ks & Key K:analz (G Un H)" |
|
306 |
apply (frule_tac P="%G. Key n:G" and G2=G in analz_keyset_substD, simp_all) |
|
307 |
apply (drule_tac G="G Un (H Int keysfor G)" in GuardK_invKey_finite) |
|
308 |
apply (auto simp: GuardK_def intro: analz_sub) |
|
309 |
by (drule keyset_in, auto) |
|
310 |
||
311 |
end |