13508
|
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)"
|
14307
|
171 |
apply (drule_tac P="%H. Nonce n:analz H" in ssubst [OF insert_Diff])
|
|
172 |
apply assumption
|
|
173 |
apply (simp only: analz_Crypt_if, simp)
|
|
174 |
done
|
13508
|
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 |