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