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 |
|
|
19 |
theory GuardK = Analz + Extensions:
|
|
20 |
|
|
21 |
(******************************************************************************
|
|
22 |
messages where all the occurrences of Key n are
|
|
23 |
in a sub-message of the form Crypt (invKey K) X with K:Ks
|
|
24 |
******************************************************************************)
|
|
25 |
|
|
26 |
consts guardK :: "nat => key set => msg set"
|
|
27 |
|
|
28 |
inductive "guardK n Ks"
|
|
29 |
intros
|
|
30 |
No_Key [intro]: "Key n ~:parts {X} ==> X:guardK n Ks"
|
|
31 |
Guard_Key [intro]: "invKey K:Ks ==> Crypt K X:guardK n Ks"
|
|
32 |
Crypt [intro]: "X:guardK n Ks ==> Crypt K X:guardK n Ks"
|
|
33 |
Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> {|X,Y|}:guardK n Ks"
|
|
34 |
|
|
35 |
subsection{*basic facts about @{term guardK}*}
|
|
36 |
|
|
37 |
lemma Nonce_is_guardK [iff]: "Nonce p:guardK n Ks"
|
|
38 |
by auto
|
|
39 |
|
|
40 |
lemma Agent_is_guardK [iff]: "Agent A:guardK n Ks"
|
|
41 |
by auto
|
|
42 |
|
|
43 |
lemma Number_is_guardK [iff]: "Number r:guardK n Ks"
|
|
44 |
by auto
|
|
45 |
|
|
46 |
lemma Key_notin_guardK: "X:guardK n Ks ==> X ~= Key n"
|
|
47 |
by (erule guardK.induct, auto)
|
|
48 |
|
|
49 |
lemma Key_notin_guardK_iff [iff]: "Key n ~:guardK n Ks"
|
|
50 |
by (auto dest: Key_notin_guardK)
|
|
51 |
|
|
52 |
lemma guardK_has_Crypt [rule_format]: "X:guardK n Ks ==> Key n:parts {X}
|
|
53 |
--> (EX K Y. Crypt K Y:kparts {X} & Key n:parts {Y})"
|
|
54 |
by (erule guardK.induct, auto)
|
|
55 |
|
|
56 |
lemma Key_notin_kparts_msg: "X:guardK n Ks ==> Key n ~:kparts {X}"
|
|
57 |
by (erule guardK.induct, auto dest: kparts_parts)
|
|
58 |
|
|
59 |
lemma Key_in_kparts_imp_no_guardK: "Key n:kparts H
|
|
60 |
==> EX X. X:H & X ~:guardK n Ks"
|
|
61 |
apply (drule in_kparts, clarify)
|
|
62 |
apply (rule_tac x=X in exI, clarify)
|
|
63 |
by (auto dest: Key_notin_kparts_msg)
|
|
64 |
|
|
65 |
lemma guardK_kparts [rule_format]: "X:guardK n Ks ==>
|
|
66 |
Y:kparts {X} --> Y:guardK n Ks"
|
|
67 |
by (erule guardK.induct, auto dest: kparts_parts parts_sub)
|
|
68 |
|
|
69 |
lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks"
|
|
70 |
by (ind_cases "Crypt K Y:guardK n Ks", auto)
|
|
71 |
|
|
72 |
lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks)
|
|
73 |
= (X:guardK n Ks & Y:guardK n Ks)"
|
|
74 |
by (auto, (ind_cases "{|X,Y|}:guardK n Ks", auto)+)
|
|
75 |
|
|
76 |
lemma guardK_not_guardK [rule_format]: "X:guardK n Ks ==>
|
|
77 |
Crypt K Y:kparts {X} --> Key n:kparts {Y} --> Y ~:guardK n Ks"
|
|
78 |
by (erule guardK.induct, auto dest: guardK_kparts)
|
|
79 |
|
|
80 |
lemma guardK_extand: "[| X:guardK n Ks; Ks <= Ks';
|
|
81 |
[| K:Ks'; K ~:Ks |] ==> Key K ~:parts {X} |] ==> X:guardK n Ks'"
|
|
82 |
by (erule guardK.induct, auto)
|
|
83 |
|
|
84 |
subsection{*guarded sets*}
|
|
85 |
|
|
86 |
constdefs GuardK :: "nat => key set => msg set => bool"
|
|
87 |
"GuardK n Ks H == ALL X. X:H --> X:guardK n Ks"
|
|
88 |
|
|
89 |
subsection{*basic facts about @{term GuardK}*}
|
|
90 |
|
|
91 |
lemma GuardK_empty [iff]: "GuardK n Ks {}"
|
|
92 |
by (simp add: GuardK_def)
|
|
93 |
|
|
94 |
lemma Key_notin_kparts [simplified]: "GuardK n Ks H ==> Key n ~:kparts H"
|
|
95 |
by (auto simp: GuardK_def dest: in_kparts Key_notin_kparts_msg)
|
|
96 |
|
|
97 |
lemma GuardK_must_decrypt: "[| GuardK n Ks H; Key n:analz H |] ==>
|
|
98 |
EX K Y. Crypt K Y:kparts H & Key (invKey K):kparts H"
|
|
99 |
apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp)
|
|
100 |
by (drule must_decrypt, auto dest: Key_notin_kparts)
|
|
101 |
|
|
102 |
lemma GuardK_kparts [intro]: "GuardK n Ks H ==> GuardK n Ks (kparts H)"
|
|
103 |
by (auto simp: GuardK_def dest: in_kparts guardK_kparts)
|
|
104 |
|
|
105 |
lemma GuardK_mono: "[| GuardK n Ks H; G <= H |] ==> GuardK n Ks G"
|
|
106 |
by (auto simp: GuardK_def)
|
|
107 |
|
|
108 |
lemma GuardK_insert [iff]: "GuardK n Ks (insert X H)
|
|
109 |
= (GuardK n Ks H & X:guardK n Ks)"
|
|
110 |
by (auto simp: GuardK_def)
|
|
111 |
|
|
112 |
lemma GuardK_Un [iff]: "GuardK n Ks (G Un H) = (GuardK n Ks G & GuardK n Ks H)"
|
|
113 |
by (auto simp: GuardK_def)
|
|
114 |
|
|
115 |
lemma GuardK_synth [intro]: "GuardK n Ks G ==> GuardK n Ks (synth G)"
|
|
116 |
by (auto simp: GuardK_def, erule synth.induct, auto)
|
|
117 |
|
|
118 |
lemma GuardK_analz [intro]: "[| GuardK n Ks G; ALL K. K:Ks --> Key K ~:analz G |]
|
|
119 |
==> GuardK n Ks (analz G)"
|
|
120 |
apply (auto simp: GuardK_def)
|
|
121 |
apply (erule analz.induct, auto)
|
|
122 |
by (ind_cases "Crypt K Xa:guardK n Ks", auto)
|
|
123 |
|
|
124 |
lemma in_GuardK [dest]: "[| X:G; GuardK n Ks G |] ==> X:guardK n Ks"
|
|
125 |
by (auto simp: GuardK_def)
|
|
126 |
|
|
127 |
lemma in_synth_GuardK: "[| X:synth G; GuardK n Ks G |] ==> X:guardK n Ks"
|
|
128 |
by (drule GuardK_synth, auto)
|
|
129 |
|
|
130 |
lemma in_analz_GuardK: "[| X:analz G; GuardK n Ks G;
|
|
131 |
ALL K. K:Ks --> Key K ~:analz G |] ==> X:guardK n Ks"
|
|
132 |
by (drule GuardK_analz, auto)
|
|
133 |
|
|
134 |
lemma GuardK_keyset [simp]: "[| keyset G; Key n ~:G |] ==> GuardK n Ks G"
|
|
135 |
by (simp only: GuardK_def, clarify, drule keyset_in, auto)
|
|
136 |
|
|
137 |
lemma GuardK_Un_keyset: "[| GuardK n Ks G; keyset H; Key n ~:H |]
|
|
138 |
==> GuardK n Ks (G Un H)"
|
|
139 |
by auto
|
|
140 |
|
|
141 |
lemma in_GuardK_kparts: "[| X:G; GuardK n Ks G; Y:kparts {X} |] ==> Y:guardK n Ks"
|
|
142 |
by blast
|
|
143 |
|
|
144 |
lemma in_GuardK_kparts_neq: "[| X:G; GuardK n Ks G; Key n':kparts {X} |]
|
|
145 |
==> n ~= n'"
|
|
146 |
by (blast dest: in_GuardK_kparts)
|
|
147 |
|
|
148 |
lemma in_GuardK_kparts_Crypt: "[| X:G; GuardK n Ks G; is_MPair X;
|
|
149 |
Crypt K Y:kparts {X}; Key n:kparts {Y} |] ==> invKey K:Ks"
|
|
150 |
apply (drule in_GuardK, simp)
|
|
151 |
apply (frule guardK_not_guardK, simp+)
|
|
152 |
apply (drule guardK_kparts, simp)
|
|
153 |
by (ind_cases "Crypt K Y:guardK n Ks", auto)
|
|
154 |
|
|
155 |
lemma GuardK_extand: "[| GuardK n Ks G; Ks <= Ks';
|
|
156 |
[| K:Ks'; K ~:Ks |] ==> Key K ~:parts G |] ==> GuardK n Ks' G"
|
|
157 |
by (auto simp: GuardK_def dest: guardK_extand parts_sub)
|
|
158 |
|
|
159 |
subsection{*set obtained by decrypting a message*}
|
|
160 |
|
|
161 |
syntax decrypt :: "msg set => key => msg => msg set"
|
|
162 |
|
|
163 |
translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})"
|
|
164 |
|
|
165 |
lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |]
|
|
166 |
==> Key n:analz (decrypt H K Y)"
|
|
167 |
by (drule_tac P="%H. Key n:analz H" in insert_Diff_substD, simp_all)
|
|
168 |
|
|
169 |
lemma "[| finite H; Crypt K Y:H |] ==> finite (decrypt H K Y)"
|
|
170 |
by auto
|
|
171 |
|
|
172 |
lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H"
|
|
173 |
by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body)
|
|
174 |
|
|
175 |
subsection{*number of Crypt's in a message*}
|
|
176 |
|
|
177 |
consts crypt_nb :: "msg => nat"
|
|
178 |
|
|
179 |
recdef crypt_nb "measure size"
|
|
180 |
"crypt_nb (Crypt K X) = Suc (crypt_nb X)"
|
|
181 |
"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y"
|
|
182 |
"crypt_nb X = 0" (* otherwise *)
|
|
183 |
|
|
184 |
subsection{*basic facts about @{term crypt_nb}*}
|
|
185 |
|
|
186 |
lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> 0 < crypt_nb X"
|
|
187 |
by (induct X, simp_all, safe, simp_all)
|
|
188 |
|
|
189 |
subsection{*number of Crypt's in a message list*}
|
|
190 |
|
|
191 |
consts cnb :: "msg list => nat"
|
|
192 |
|
|
193 |
recdef cnb "measure size"
|
|
194 |
"cnb [] = 0"
|
|
195 |
"cnb (X#l) = crypt_nb X + cnb l"
|
|
196 |
|
|
197 |
subsection{*basic facts about @{term cnb}*}
|
|
198 |
|
|
199 |
lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
|
|
200 |
by (induct l, auto)
|
|
201 |
|
|
202 |
lemma mem_cnb_minus: "x mem l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
|
|
203 |
by (induct l, auto)
|
|
204 |
|
|
205 |
lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
|
|
206 |
|
|
207 |
lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
|
|
208 |
apply (induct l, auto)
|
|
209 |
by (erule_tac l1=list and x1=x in mem_cnb_minus_substI, simp)
|
|
210 |
|
|
211 |
lemma parts_cnb: "Z:parts (set l) ==>
|
|
212 |
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
|
|
213 |
by (erule parts.induct, auto simp: in_set_conv_decomp)
|
|
214 |
|
|
215 |
lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> 0 < cnb l"
|
|
216 |
by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
|
|
217 |
|
|
218 |
subsection{*list of kparts*}
|
|
219 |
|
|
220 |
lemma kparts_msg_set: "EX l. kparts {X} = set l & cnb l = crypt_nb X"
|
|
221 |
apply (induct X, simp_all)
|
|
222 |
apply (rule_tac x="[Agent agent]" in exI, simp)
|
|
223 |
apply (rule_tac x="[Number nat]" in exI, simp)
|
|
224 |
apply (rule_tac x="[Nonce nat]" in exI, simp)
|
|
225 |
apply (rule_tac x="[Key nat]" in exI, simp)
|
|
226 |
apply (rule_tac x="[Hash msg]" in exI, simp)
|
|
227 |
apply (clarify, rule_tac x="l@la" in exI, simp)
|
|
228 |
by (clarify, rule_tac x="[Crypt nat msg]" in exI, simp)
|
|
229 |
|
|
230 |
lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
|
|
231 |
apply (induct l)
|
|
232 |
apply (rule_tac x="[]" in exI, simp, clarsimp)
|
|
233 |
apply (subgoal_tac "EX l. kparts {a} = set l & cnb l = crypt_nb a", clarify)
|
|
234 |
apply (rule_tac x="l@l'" in exI, simp)
|
|
235 |
apply (rule kparts_insert_substI, simp)
|
|
236 |
by (rule kparts_msg_set)
|
|
237 |
|
|
238 |
subsection{*list corresponding to "decrypt"*}
|
|
239 |
|
|
240 |
constdefs decrypt' :: "msg list => key => msg => msg list"
|
|
241 |
"decrypt' l K Y == Y # minus l (Crypt K Y)"
|
|
242 |
|
|
243 |
declare decrypt'_def [simp]
|
|
244 |
|
|
245 |
subsection{*basic facts about @{term decrypt'}*}
|
|
246 |
|
|
247 |
lemma decrypt_minus: "decrypt (set l) K Y <= set (decrypt' l K Y)"
|
|
248 |
by (induct l, auto)
|
|
249 |
|
|
250 |
text{*if the analysis of a finite guarded set gives n then it must also give
|
|
251 |
one of the keys of Ks*}
|
|
252 |
|
|
253 |
lemma GuardK_invKey_by_list [rule_format]: "ALL l. cnb l = p
|
|
254 |
--> GuardK n Ks (set l) --> Key n:analz (set l)
|
|
255 |
--> (EX K. K:Ks & Key K:analz (set l))"
|
|
256 |
apply (induct p)
|
|
257 |
(* case p=0 *)
|
|
258 |
apply (clarify, drule GuardK_must_decrypt, simp, clarify)
|
|
259 |
apply (drule kparts_parts, drule non_empty_crypt, simp)
|
|
260 |
(* case p>0 *)
|
|
261 |
apply (clarify, frule GuardK_must_decrypt, simp, clarify)
|
|
262 |
apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp)
|
|
263 |
apply (frule analz_decrypt, simp_all)
|
|
264 |
apply (subgoal_tac "EX l'. kparts (set l) = set l' & cnb l' = cnb l", clarsimp)
|
|
265 |
apply (drule_tac G="insert Y (set l' - {Crypt K Y})"
|
|
266 |
and H="set (decrypt' l' K Y)" in analz_sub, rule decrypt_minus)
|
|
267 |
apply (rule_tac analz_pparts_kparts_substI, simp)
|
|
268 |
apply (case_tac "K:invKey`Ks")
|
|
269 |
(* K:invKey`Ks *)
|
|
270 |
apply (clarsimp, blast)
|
|
271 |
(* K ~:invKey`Ks *)
|
|
272 |
apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))")
|
|
273 |
apply (drule_tac x="decrypt' l' K Y" in spec, simp add: set_mem_eq)
|
|
274 |
apply (subgoal_tac "Crypt K Y:parts (set l)")
|
|
275 |
apply (drule parts_cnb, rotate_tac -1, simp)
|
|
276 |
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
|
|
277 |
apply (rule insert_mono, rule set_minus)
|
|
278 |
apply (simp add: analz_insertD, blast)
|
|
279 |
(* Crypt K Y:parts (set l) *)
|
|
280 |
apply (blast dest: kparts_parts)
|
|
281 |
(* GuardK n Ks (set (decrypt' l' K Y)) *)
|
|
282 |
apply (rule_tac H="insert Y (set l')" in GuardK_mono)
|
|
283 |
apply (subgoal_tac "GuardK n Ks (set l')", simp)
|
|
284 |
apply (rule_tac K=K in guardK_Crypt, simp add: GuardK_def, simp)
|
|
285 |
apply (drule_tac t="set l'" in sym, simp)
|
|
286 |
apply (rule GuardK_kparts, simp, simp)
|
|
287 |
apply (rule_tac B="set l'" in subset_trans, rule set_minus, blast)
|
|
288 |
by (rule kparts_set)
|
|
289 |
|
|
290 |
lemma GuardK_invKey_finite: "[| Key n:analz G; GuardK n Ks G; finite G |]
|
|
291 |
==> EX K. K:Ks & Key K:analz G"
|
|
292 |
apply (drule finite_list, clarify)
|
|
293 |
by (rule GuardK_invKey_by_list, auto)
|
|
294 |
|
|
295 |
lemma GuardK_invKey: "[| Key n:analz G; GuardK n Ks G |]
|
|
296 |
==> EX K. K:Ks & Key K:analz G"
|
|
297 |
by (auto dest: analz_needs_only_finite GuardK_invKey_finite)
|
|
298 |
|
|
299 |
text{*if the analyse of a finite guarded set and a (possibly infinite) set of
|
|
300 |
keys gives n then it must also gives Ks*}
|
|
301 |
|
|
302 |
lemma GuardK_invKey_keyset: "[| Key n:analz (G Un H); GuardK n Ks G; finite G;
|
|
303 |
keyset H; Key n ~:H |] ==> EX K. K:Ks & Key K:analz (G Un H)"
|
|
304 |
apply (frule_tac P="%G. Key n:G" and G2=G in analz_keyset_substD, simp_all)
|
|
305 |
apply (drule_tac G="G Un (H Int keysfor G)" in GuardK_invKey_finite)
|
|
306 |
apply (auto simp: GuardK_def intro: analz_sub)
|
|
307 |
by (drule keyset_in, auto)
|
|
308 |
|
|
309 |
end |