author | paulson |
Tue, 20 Aug 1996 17:46:24 +0200 | |
changeset 1929 | f0839bab4b00 |
parent 1913 | 2809adb15eb0 |
child 1930 | cdf9bcd53749 |
permissions | -rw-r--r-- |
1839 | 1 |
(* Title: HOL/Auth/Message |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Datatype of events; |
|
7 |
inductive relation "traces" for Needham-Schroeder (shared keys) |
|
1852 | 8 |
|
9 |
Rewrites should not refer to initState (Friend i) -- not in normal form |
|
1839 | 10 |
*) |
11 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
12 |
Addsimps [parts_cut_eq]; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
13 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
14 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
15 |
(*INSTALLED ON NAT.ML*) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
16 |
goalw Nat.thy [le_def] "(m <= n) = (m < Suc n)"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
17 |
by (rtac not_less_eq 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
18 |
qed "le_eq_less_Suc"; |
1839 | 19 |
|
1885 | 20 |
proof_timing:=true; |
21 |
||
22 |
(*FOR LIST.ML??*) |
|
1913 | 23 |
goal List.thy "x : set_of_list (x#xs)"; |
1885 | 24 |
by (Simp_tac 1); |
1913 | 25 |
qed "set_of_list_I1"; |
1885 | 26 |
|
1913 | 27 |
goal List.thy "!!x. xs = x#xs' ==> x : set_of_list xs"; |
1885 | 28 |
by (Asm_simp_tac 1); |
1913 | 29 |
qed "set_of_list_eqI1"; |
1885 | 30 |
|
1913 | 31 |
goal List.thy "set_of_list l <= set_of_list (x#l)"; |
1893 | 32 |
by (Simp_tac 1); |
33 |
by (Fast_tac 1); |
|
1913 | 34 |
qed "set_of_list_subset_Cons"; |
1893 | 35 |
|
1885 | 36 |
(*Not for Addsimps -- it can cause goals to blow up!*) |
37 |
goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))"; |
|
38 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
39 |
qed "mem_if"; |
|
40 |
||
1913 | 41 |
(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*) |
1885 | 42 |
goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})"; |
43 |
by (fast_tac (!claset addEs [equalityE]) 1); |
|
44 |
val subset_range_iff = result(); |
|
45 |
||
46 |
||
1839 | 47 |
open Event; |
48 |
||
1885 | 49 |
Addsimps [Un_insert_left, Un_insert_right]; |
50 |
||
51 |
(*By default only o_apply is built-in. But in the presence of eta-expansion |
|
52 |
this means that some terms displayed as (f o g) will be rewritten, and others |
|
53 |
will not!*) |
|
54 |
Addsimps [o_def]; |
|
1852 | 55 |
|
56 |
(*** Basic properties of serverKey and newK ***) |
|
57 |
||
1839 | 58 |
(* invKey (serverKey A) = serverKey A *) |
59 |
bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey); |
|
60 |
||
1852 | 61 |
(* invKey (newK evs) = newK evs *) |
1839 | 62 |
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK); |
63 |
Addsimps [invKey_serverKey, invKey_newK]; |
|
64 |
||
65 |
||
66 |
(*New keys and nonces are fresh*) |
|
67 |
val serverKey_inject = inj_serverKey RS injD; |
|
1852 | 68 |
val newN_inject = inj_newN RS injD |
69 |
and newK_inject = inj_newK RS injD; |
|
1839 | 70 |
AddSEs [serverKey_inject, newN_inject, newK_inject, |
71 |
fresh_newK RS notE, fresh_newN RS notE]; |
|
72 |
Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq]; |
|
73 |
Addsimps [fresh_newN, fresh_newK]; |
|
74 |
||
1852 | 75 |
goal thy "newK evs ~= serverKey B"; |
76 |
by (subgoal_tac "newK evs = serverKey B --> \ |
|
77 |
\ Key (newK evs) : parts (initState B)" 1); |
|
1839 | 78 |
by (Fast_tac 1); |
79 |
by (agent.induct_tac "B" 1); |
|
80 |
by (auto_tac (!claset addIs [range_eqI], !simpset)); |
|
81 |
qed "newK_neq_serverKey"; |
|
82 |
||
83 |
Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym]; |
|
84 |
||
85 |
(*Good for talking about Server's initial state*) |
|
1885 | 86 |
goal thy "!!H. H <= Key``E ==> parts H = H"; |
87 |
by (Auto_tac ()); |
|
1839 | 88 |
be parts.induct 1; |
89 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
|
1885 | 90 |
qed "parts_image_subset"; |
1839 | 91 |
|
1885 | 92 |
bind_thm ("parts_image_Key", subset_refl RS parts_image_subset); |
93 |
||
1913 | 94 |
goal thy "!!H. H <= Key``E ==> analz H = H"; |
1885 | 95 |
by (Auto_tac ()); |
1913 | 96 |
be analz.induct 1; |
1839 | 97 |
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
1913 | 98 |
qed "analz_image_subset"; |
1839 | 99 |
|
1913 | 100 |
bind_thm ("analz_image_Key", subset_refl RS analz_image_subset); |
1885 | 101 |
|
1913 | 102 |
Addsimps [parts_image_Key, analz_image_Key]; |
1839 | 103 |
|
104 |
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}"; |
|
105 |
by (agent.induct_tac "C" 1); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
106 |
by (auto_tac (!claset addIs [range_eqI] delrules partsEs, !simpset)); |
1839 | 107 |
qed "keysFor_parts_initState"; |
108 |
Addsimps [keysFor_parts_initState]; |
|
109 |
||
1885 | 110 |
goalw thy [keysFor_def] "keysFor (Key``E) = {}"; |
111 |
by (Auto_tac ()); |
|
112 |
qed "keysFor_image_Key"; |
|
113 |
Addsimps [keysFor_image_Key]; |
|
114 |
||
115 |
goal thy "serverKey A ~: newK``E"; |
|
116 |
by (agent.induct_tac "A" 1); |
|
117 |
by (Auto_tac ()); |
|
118 |
qed "serverKey_notin_image_newK"; |
|
119 |
Addsimps [serverKey_notin_image_newK]; |
|
120 |
||
121 |
||
122 |
(*Agents see their own serverKeys!*) |
|
1913 | 123 |
goal thy "Key (serverKey A) : analz (sees A evs)"; |
1885 | 124 |
by (list.induct_tac "evs" 1); |
1913 | 125 |
by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2); |
1885 | 126 |
by (agent.induct_tac "A" 1); |
127 |
by (auto_tac (!claset addIs [range_eqI], !simpset)); |
|
1913 | 128 |
qed "analz_own_serverKey"; |
1885 | 129 |
|
130 |
bind_thm ("parts_own_serverKey", |
|
1913 | 131 |
[analz_subset_parts, analz_own_serverKey] MRS subsetD); |
1885 | 132 |
|
1913 | 133 |
Addsimps [analz_own_serverKey, parts_own_serverKey]; |
1885 | 134 |
|
135 |
||
1839 | 136 |
|
137 |
(**** Inductive relation "traces" -- basic properties ****) |
|
138 |
||
139 |
val mk_cases = traces.mk_cases (list.simps @ agent.simps @ event.simps); |
|
140 |
||
141 |
val Says_tracesE = mk_cases "Says A B X # evs: traces"; |
|
142 |
val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces"; |
|
143 |
val Says_Enemy_tracesE = mk_cases "Says Enemy B X # evs: traces"; |
|
144 |
val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces"; |
|
145 |
val Notes_tracesE = mk_cases "Notes A X # evs: traces"; |
|
146 |
||
147 |
(*The tail of a trace is a trace*) |
|
148 |
goal thy "!!ev evs. ev#evs : traces ==> evs : traces"; |
|
149 |
by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1); |
|
150 |
qed "traces_ConsE"; |
|
151 |
||
1885 | 152 |
goal thy "!!ev evs. [| evs = ev#evs'; evs : traces |] ==> evs' : traces"; |
153 |
by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1); |
|
154 |
qed "traces_eq_ConsE"; |
|
155 |
||
156 |
||
1839 | 157 |
(** Specialized rewrite rules for (sees A (Says...#evs)) **) |
158 |
||
159 |
goal thy "sees A (Says A B X # evs) = insert X (sees A evs)"; |
|
160 |
by (Simp_tac 1); |
|
161 |
qed "sees_own"; |
|
162 |
||
163 |
goal thy "!!A. Server ~= A ==> \ |
|
164 |
\ sees Server (Says A B X # evs) = sees Server evs"; |
|
165 |
by (Asm_simp_tac 1); |
|
166 |
qed "sees_Server"; |
|
167 |
||
168 |
goal thy "!!A. Friend i ~= A ==> \ |
|
169 |
\ sees (Friend i) (Says A B X # evs) = sees (Friend i) evs"; |
|
170 |
by (Asm_simp_tac 1); |
|
171 |
qed "sees_Friend"; |
|
172 |
||
173 |
goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)"; |
|
174 |
by (Simp_tac 1); |
|
175 |
qed "sees_Enemy"; |
|
176 |
||
177 |
goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)"; |
|
178 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
179 |
by (Fast_tac 1); |
|
1852 | 180 |
qed "sees_Says_subset_insert"; |
181 |
||
182 |
goal thy "sees A evs <= sees A (Says A' B X # evs)"; |
|
183 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
184 |
by (Fast_tac 1); |
|
185 |
qed "sees_subset_sees_Says"; |
|
1839 | 186 |
|
187 |
(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*) |
|
188 |
goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \ |
|
189 |
\ parts {Y} Un (UN A. parts (sees A evs))"; |
|
190 |
by (Step_tac 1); |
|
191 |
be rev_mp 1; (*for some reason, split_tac does not work on assumptions*) |
|
192 |
val ss = (!simpset addsimps [parts_Un, sees_Cons] |
|
193 |
setloop split_tac [expand_if]); |
|
194 |
by (ALLGOALS (fast_tac (!claset addss ss))); |
|
195 |
qed "UN_parts_sees_Says"; |
|
196 |
||
1913 | 197 |
goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs"; |
1885 | 198 |
by (list.induct_tac "evs" 1); |
199 |
by (Auto_tac ()); |
|
200 |
qed_spec_mp "Says_imp_sees_Enemy"; |
|
201 |
||
202 |
Addsimps [Says_imp_sees_Enemy]; |
|
203 |
AddIs [Says_imp_sees_Enemy]; |
|
1839 | 204 |
|
1893 | 205 |
goal thy "initState C <= Key `` range serverKey"; |
206 |
by (agent.induct_tac "C" 1); |
|
207 |
by (Auto_tac ()); |
|
208 |
qed "initState_subset"; |
|
209 |
||
210 |
goal thy "X : sees C evs --> \ |
|
1913 | 211 |
\ (EX A B. Says A B X : set_of_list evs) | \ |
212 |
\ (EX A. Notes A X : set_of_list evs) | \ |
|
1893 | 213 |
\ (EX A. X = Key (serverKey A))"; |
214 |
by (list.induct_tac "evs" 1); |
|
215 |
by (ALLGOALS Asm_simp_tac); |
|
216 |
by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1); |
|
217 |
br conjI 1; |
|
218 |
by (Fast_tac 2); |
|
219 |
by (event.induct_tac "a" 1); |
|
220 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if]))); |
|
221 |
by (ALLGOALS Fast_tac); |
|
222 |
qed_spec_mp "seesD"; |
|
223 |
||
224 |
||
1839 | 225 |
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy]; |
1852 | 226 |
Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) |
1839 | 227 |
|
228 |
||
229 |
(**** Inductive proofs about traces ****) |
|
230 |
||
231 |
(*The Enemy can see more than anybody else, except for their initial state*) |
|
232 |
goal thy |
|
233 |
"!!evs. evs : traces ==> \ |
|
234 |
\ sees A evs <= initState A Un sees Enemy evs"; |
|
235 |
be traces.induct 1; |
|
1852 | 236 |
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
1839 | 237 |
addss (!simpset)))); |
238 |
qed "sees_agent_subset_sees_Enemy"; |
|
239 |
||
240 |
||
1885 | 241 |
(*Nobody sends themselves messages*) |
1913 | 242 |
goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: set_of_list evs"; |
1852 | 243 |
be traces.induct 1; |
244 |
by (Auto_tac()); |
|
245 |
qed_spec_mp "not_Says_to_self"; |
|
246 |
Addsimps [not_Says_to_self]; |
|
247 |
AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
248 |
||
1913 | 249 |
goal thy "!!evs. evs : traces ==> Notes A X ~: set_of_list evs"; |
1893 | 250 |
be traces.induct 1; |
251 |
by (Auto_tac()); |
|
252 |
qed "not_Notes"; |
|
253 |
Addsimps [not_Notes]; |
|
254 |
AddSEs [not_Notes RSN (2, rev_notE)]; |
|
255 |
||
1852 | 256 |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
257 |
goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \ |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
258 |
\ X : parts (sees Enemy evs)"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
259 |
by (fast_tac (!claset addSEs partsEs |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
260 |
addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
261 |
qed "NS3_msg_in_parts_sees_Enemy"; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
262 |
|
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
263 |
|
1839 | 264 |
(*** Server keys are not betrayed ***) |
265 |
||
1852 | 266 |
(*Enemy never sees another agent's server key!*) |
1839 | 267 |
goal thy |
1852 | 268 |
"!!evs. [| evs : traces; A ~= Enemy |] ==> \ |
269 |
\ Key (serverKey A) ~: parts (sees Enemy evs)"; |
|
1839 | 270 |
be traces.induct 1; |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
271 |
bd NS3_msg_in_parts_sees_Enemy 5; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
272 |
by (Auto_tac()); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
273 |
(*Deals with Fake message*) |
1913 | 274 |
by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
275 |
impOfSubs synth_analz_parts_insert_subset_Un]) 1); |
1839 | 276 |
qed "Enemy_not_see_serverKey"; |
277 |
||
1913 | 278 |
bind_thm ("Enemy_not_analz_serverKey", |
279 |
[analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD); |
|
1852 | 280 |
|
1885 | 281 |
Addsimps [Enemy_not_see_serverKey, |
282 |
not_sym RSN (2, Enemy_not_see_serverKey), |
|
1913 | 283 |
Enemy_not_analz_serverKey, |
284 |
not_sym RSN (2, Enemy_not_analz_serverKey)]; |
|
1852 | 285 |
|
1893 | 286 |
(*We go to some trouble to preserve R in the 3rd subgoal*) |
287 |
val major::prems = |
|
288 |
goal thy "[| Key (serverKey A) : parts (sees Enemy evs); \ |
|
289 |
\ evs : traces; \ |
|
290 |
\ A=Enemy ==> R \ |
|
291 |
\ |] ==> R"; |
|
292 |
br ccontr 1; |
|
293 |
br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1; |
|
294 |
by (swap_res_tac prems 2); |
|
295 |
by (ALLGOALS (fast_tac (!claset addIs prems))); |
|
296 |
qed "Enemy_see_serverKey_E"; |
|
297 |
||
1913 | 298 |
bind_thm ("Enemy_analz_serverKey_E", |
299 |
analz_subset_parts RS subsetD RS Enemy_see_serverKey_E); |
|
1893 | 300 |
|
301 |
(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) |
|
1913 | 302 |
AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E]; |
1893 | 303 |
|
1839 | 304 |
|
1852 | 305 |
(*No Friend will ever see another agent's server key |
1885 | 306 |
(excluding the Enemy, who might transmit his). |
307 |
The Server, of course, knows all server keys.*) |
|
1839 | 308 |
goal thy |
1852 | 309 |
"!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ |
310 |
\ Key (serverKey A) ~: parts (sees (Friend j) evs)"; |
|
311 |
br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; |
|
312 |
by (ALLGOALS Asm_simp_tac); |
|
313 |
qed "Friend_not_see_serverKey"; |
|
1839 | 314 |
|
315 |
||
1885 | 316 |
(*Not for Addsimps -- it can cause goals to blow up!*) |
317 |
goal thy |
|
318 |
"!!evs. evs : traces ==> \ |
|
319 |
\ (Key (serverKey A) \ |
|
1913 | 320 |
\ : analz (insert (Key (serverKey B)) (sees Enemy evs))) = \ |
1885 | 321 |
\ (A=B | A=Enemy)"; |
1913 | 322 |
by (best_tac (!claset addDs [impOfSubs analz_subset_parts] |
323 |
addIs [impOfSubs (subset_insertI RS analz_mono)] |
|
1885 | 324 |
addss (!simpset)) 1); |
1913 | 325 |
qed "serverKey_mem_analz"; |
1885 | 326 |
|
327 |
||
328 |
||
329 |
||
1839 | 330 |
(*** Future keys can't be seen or used! ***) |
331 |
||
332 |
(*Nobody can have SEEN keys that will be generated in the future. |
|
333 |
This has to be proved anew for each protocol description, |
|
334 |
but should go by similar reasoning every time. Hardest case is the |
|
335 |
standard Fake rule. |
|
336 |
The length comparison, and Union over C, are essential for the |
|
337 |
induction! *) |
|
338 |
goal thy "!!evs. evs : traces ==> \ |
|
339 |
\ length evs <= length evs' --> \ |
|
1852 | 340 |
\ Key (newK evs') ~: (UN C. parts (sees C evs))"; |
1839 | 341 |
be traces.induct 1; |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
342 |
bd NS3_msg_in_parts_sees_Enemy 5; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
343 |
(*auto_tac does not work here, as it performs safe_tac first*) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
344 |
by (ALLGOALS Asm_simp_tac); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
345 |
by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
346 |
impOfSubs parts_insert_subset_Un, |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
347 |
Suc_leD] |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
348 |
addss (!simpset)))); |
1839 | 349 |
val lemma = result(); |
350 |
||
351 |
(*Variant needed for the main theorem below*) |
|
352 |
goal thy |
|
353 |
"!!evs. [| evs : traces; length evs <= length evs' |] ==> \ |
|
1852 | 354 |
\ Key (newK evs') ~: parts (sees C evs)"; |
1839 | 355 |
by (fast_tac (!claset addDs [lemma]) 1); |
356 |
qed "new_keys_not_seen"; |
|
1893 | 357 |
Addsimps [new_keys_not_seen]; |
1839 | 358 |
|
1893 | 359 |
(*Another variant: old messages must contain old keys!*) |
360 |
goal thy |
|
1913 | 361 |
"!!evs. [| Says A B X : set_of_list evs; \ |
1893 | 362 |
\ Key (newK evt) : parts {X}; \ |
363 |
\ evs : traces \ |
|
364 |
\ |] ==> length evt < length evs"; |
|
365 |
br ccontr 1; |
|
366 |
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy] |
|
367 |
addIs [impOfSubs parts_mono, leI]) 1); |
|
368 |
qed "Says_imp_old_keys"; |
|
369 |
||
1885 | 370 |
|
1852 | 371 |
goal thy "!!K. newK evs = invKey K ==> newK evs = K"; |
1839 | 372 |
br (invKey_eq RS iffD1) 1; |
373 |
by (Simp_tac 1); |
|
374 |
val newK_invKey = result(); |
|
375 |
||
1852 | 376 |
|
377 |
val keysFor_parts_mono = parts_mono RS keysFor_mono; |
|
378 |
||
1839 | 379 |
(*Nobody can have USED keys that will be generated in the future. |
380 |
...very like new_keys_not_seen*) |
|
381 |
goal thy "!!evs. evs : traces ==> \ |
|
382 |
\ length evs <= length evs' --> \ |
|
1852 | 383 |
\ newK evs' ~: keysFor (UN C. parts (sees C evs))"; |
1839 | 384 |
be traces.induct 1; |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
385 |
bd NS3_msg_in_parts_sees_Enemy 5; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
386 |
by (ALLGOALS Asm_simp_tac); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
387 |
by (ALLGOALS |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
388 |
(best_tac |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
389 |
(!claset addSDs [newK_invKey] |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
390 |
addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
391 |
impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
392 |
Suc_leD] |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
393 |
addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)] |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
394 |
addss (!simpset)))); |
1839 | 395 |
val lemma = result(); |
396 |
||
397 |
goal thy |
|
398 |
"!!evs. [| evs : traces; length evs <= length evs' |] ==> \ |
|
1852 | 399 |
\ newK evs' ~: keysFor (parts (sees C evs))"; |
1839 | 400 |
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
401 |
qed "new_keys_not_used"; |
|
402 |
||
1913 | 403 |
bind_thm ("new_keys_not_analzd", |
404 |
[analz_subset_parts RS keysFor_mono, |
|
1839 | 405 |
new_keys_not_used] MRS contra_subsetD); |
406 |
||
1913 | 407 |
Addsimps [new_keys_not_used, new_keys_not_analzd]; |
1852 | 408 |
|
409 |
||
1885 | 410 |
(** Rewrites to push in Key and Crypt messages, so that other messages can |
1913 | 411 |
be pulled out using the analz_insert rules **) |
1885 | 412 |
|
413 |
fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] |
|
414 |
insert_commute; |
|
1839 | 415 |
|
1885 | 416 |
val pushKeys = map (insComm "Key ?K") |
417 |
["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"]; |
|
418 |
||
419 |
val pushCrypts = map (insComm "Crypt ?X ?K") |
|
420 |
["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"]; |
|
421 |
||
422 |
(*Cannot be added with Addsimps -- we don't always want to re-order messages*) |
|
423 |
val pushes = pushKeys@pushCrypts; |
|
424 |
||
425 |
val pushKey_newK = insComm "Key (newK ?evs)" "Key (serverKey ?C)"; |
|
1839 | 426 |
|
1852 | 427 |
|
1839 | 428 |
(** Lemmas concerning the form of items passed in messages **) |
429 |
||
1885 | 430 |
(*Describes the form *and age* of K, and the form of X, |
431 |
when the following message is sent*) |
|
1839 | 432 |
goal thy |
1913 | 433 |
"!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \ |
1885 | 434 |
\ evs : traces \ |
1893 | 435 |
\ |] ==> (EX evt:traces. \ |
436 |
\ K = Key(newK evt) & \ |
|
437 |
\ X = (Crypt {|K, Agent A|} (serverKey B)) & \ |
|
438 |
\ K' = serverKey A & \ |
|
439 |
\ length evt < length evs)"; |
|
1839 | 440 |
be rev_mp 1; |
441 |
be traces.induct 1; |
|
442 |
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); |
|
1885 | 443 |
qed "Says_Server_message_form"; |
1839 | 444 |
|
1913 | 445 |
(* c ~: keysFor (parts H) ==> c ~: keysFor (analz H) *) |
446 |
bind_thm ("not_parts_not_keysFor_analz", |
|
447 |
analz_subset_parts RS keysFor_mono RS contra_subsetD); |
|
1852 | 448 |
|
449 |
||
1885 | 450 |
|
451 |
(*USELESS for NS3, case 1, as the ind hyp says the same thing! |
|
452 |
goal thy |
|
453 |
"!!evs. [| evs = Says Server (Friend i) \ |
|
454 |
\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
|
455 |
\ evs : traces; i~=k \ |
|
456 |
\ |] ==> \ |
|
1913 | 457 |
\ K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; |
1885 | 458 |
be rev_mp 1; |
459 |
be traces.induct 1; |
|
460 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
461 |
by (Step_tac 1); |
|
1913 | 462 |
by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
1885 | 463 |
val Enemy_not_see_encrypted_key_lemma = result(); |
464 |
*) |
|
465 |
||
466 |
||
467 |
(*Describes the form of X when the following message is sent*) |
|
468 |
goal thy |
|
469 |
"!!evs. evs : traces ==> \ |
|
470 |
\ ALL A NA B K X. \ |
|
471 |
\ (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
|
472 |
\ : parts (sees Enemy evs) & A ~= Enemy --> \ |
|
473 |
\ (EX evt:traces. K = newK evt & \ |
|
474 |
\ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
|
475 |
be traces.induct 1; |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
476 |
bd NS3_msg_in_parts_sees_Enemy 5; |
1885 | 477 |
by (Step_tac 1); |
478 |
by (ALLGOALS Asm_full_simp_tac); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
479 |
(*Remaining cases are Fake and NS2*) |
1885 | 480 |
by (fast_tac (!claset addSDs [spec]) 2); |
481 |
(*Now for the Fake case*) |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
482 |
by (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
483 |
impOfSubs synth_analz_parts_insert_subset_Un] |
1885 | 484 |
addss (!simpset)) 1); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
485 |
qed_spec_mp "encrypted_form"; |
1885 | 486 |
|
487 |
||
488 |
(*For eliminating the A ~= Enemy condition from the previous result*) |
|
489 |
goal thy |
|
490 |
"!!evs. evs : traces ==> \ |
|
491 |
\ ALL S A NA B K X. \ |
|
492 |
\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
|
1913 | 493 |
\ : set_of_list evs --> \ |
1885 | 494 |
\ S = Server | S = Enemy"; |
495 |
be traces.induct 1; |
|
1893 | 496 |
by (ALLGOALS Asm_simp_tac); |
1885 | 497 |
(*We are left with NS3*) |
498 |
by (subgoal_tac "S = Server | S = Enemy" 1); |
|
499 |
(*First justify this assumption!*) |
|
500 |
by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2); |
|
501 |
by (Step_tac 1); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
502 |
bd Says_Server_message_form 1; |
1885 | 503 |
by (ALLGOALS Full_simp_tac); |
504 |
(*Final case. Clear out needless quantifiers to speed the following step*) |
|
505 |
by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
506 |
bd encrypted_form 1; |
1885 | 507 |
br (parts.Inj RS conjI) 1; |
508 |
auto(); |
|
509 |
qed_spec_mp "Server_or_Enemy"; |
|
510 |
||
511 |
||
512 |
(*Describes the form of X when the following message is sent; |
|
513 |
use Says_Server_message_form if applicable*) |
|
514 |
goal thy |
|
515 |
"!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ |
|
1913 | 516 |
\ : set_of_list evs; \ |
1885 | 517 |
\ evs : traces \ |
1893 | 518 |
\ |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \ |
1885 | 519 |
\ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
520 |
by (forward_tac [Server_or_Enemy] 1); |
|
521 |
ba 1; |
|
522 |
by (Step_tac 1); |
|
523 |
by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
524 |
by (forward_tac [encrypted_form] 1); |
1885 | 525 |
br (parts.Inj RS conjI) 1; |
1893 | 526 |
by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset)); |
1885 | 527 |
qed "Says_S_message_form"; |
528 |
||
529 |
goal thy |
|
530 |
"!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} \ |
|
531 |
\ (serverKey A)) # evs'; \ |
|
532 |
\ evs : traces \ |
|
1893 | 533 |
\ |] ==> (EX evt:traces. evs' : traces & length evt < length evs & \ |
1885 | 534 |
\ K = newK evt & \ |
535 |
\ X = (Crypt {|Key K, Agent A|} (serverKey B)))"; |
|
536 |
by (forward_tac [traces_eq_ConsE] 1); |
|
1913 | 537 |
by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2); |
1885 | 538 |
by (Auto_tac()); |
539 |
qed "Says_S_message_form_eq"; |
|
540 |
||
541 |
||
542 |
||
543 |
||
544 |
(**** |
|
545 |
The following is to prove theorems of the form |
|
546 |
||
1913 | 547 |
Key K : analz (insert (Key (newK evt)) |
1885 | 548 |
(insert (Key (serverKey C)) (sees Enemy evs))) ==> |
1913 | 549 |
Key K : analz (insert (Key (serverKey C)) (sees Enemy evs)) |
1885 | 550 |
|
551 |
A more general formula must be proved inductively. |
|
552 |
||
553 |
****) |
|
554 |
||
555 |
||
556 |
(*Not useful in this form, but it says that session keys are not used |
|
557 |
to encrypt messages containing other keys, in the actual protocol. |
|
558 |
We require that agents should behave like this subsequently also.*) |
|
559 |
goal thy |
|
560 |
"!!evs. evs : traces ==> \ |
|
561 |
\ (Crypt X (newK evt)) : parts (sees Enemy evs) & \ |
|
562 |
\ Key K : parts {X} --> Key K : parts (sees Enemy evs)"; |
|
563 |
be traces.induct 1; |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
564 |
bd NS3_msg_in_parts_sees_Enemy 5; |
1893 | 565 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
1885 | 566 |
(*Deals with Faked messages*) |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
567 |
by (best_tac (!claset addSEs partsEs |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
568 |
addDs [impOfSubs analz_subset_parts, |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
569 |
impOfSubs parts_insert_subset_Un] |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
570 |
addss (!simpset)) 1); |
1885 | 571 |
result(); |
572 |
||
573 |
||
1893 | 574 |
(** Specialized rewriting for this proof **) |
1885 | 575 |
|
576 |
Delsimps [image_insert]; |
|
577 |
Addsimps [image_insert RS sym]; |
|
578 |
||
579 |
goal thy "insert (Key (newK x)) (sees A evs) = \ |
|
580 |
\ Key `` (newK``{x}) Un (sees A evs)"; |
|
581 |
by (Fast_tac 1); |
|
582 |
val insert_Key_singleton = result(); |
|
583 |
||
584 |
goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \ |
|
585 |
\ Key `` (f `` (insert x E)) Un C"; |
|
586 |
by (Fast_tac 1); |
|
587 |
val insert_Key_image = result(); |
|
588 |
||
589 |
||
1893 | 590 |
(** Session keys are not used to encrypt other session keys **) |
591 |
||
1885 | 592 |
goal thy |
593 |
"!!evs. evs : traces ==> \ |
|
1913 | 594 |
\ ALL K E. (Key K : analz (insert (Key (serverKey C)) \ |
1885 | 595 |
\ (Key``(newK``E) Un (sees Enemy evs)))) = \ |
596 |
\ (K : newK``E | \ |
|
1913 | 597 |
\ Key K : analz (insert (Key (serverKey C)) \ |
1885 | 598 |
\ (sees Enemy evs)))"; |
599 |
be traces.induct 1; |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
600 |
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
1885 | 601 |
by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5)); |
602 |
by (ALLGOALS |
|
1893 | 603 |
(asm_simp_tac |
1885 | 604 |
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] |
605 |
@ pushes) |
|
606 |
setloop split_tac [expand_if]))); |
|
607 |
(*Cases NS2 and NS3!! Simple, thanks to auto case splits*) |
|
608 |
by (REPEAT (Fast_tac 3)); |
|
609 |
(*Base case*) |
|
610 |
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
|
611 |
(** LEVEL 7 **) |
|
612 |
(*Fake case*) |
|
613 |
by (REPEAT (Safe_step_tac 1)); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
614 |
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2); |
1885 | 615 |
by (subgoal_tac |
1913 | 616 |
"Key K : analz \ |
617 |
\ (synth \ |
|
618 |
\ (analz (insert (Key (serverKey C)) \ |
|
1885 | 619 |
\ (Key``(newK``E) Un (sees Enemy evsa)))))" 1); |
620 |
(*First, justify this subgoal*) |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
621 |
(*Discard formulae for better speed*) |
1885 | 622 |
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
623 |
by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2); |
|
1913 | 624 |
by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)] |
625 |
addSEs [impOfSubs analz_mono]) 2); |
|
1885 | 626 |
by (Asm_full_simp_tac 1); |
1913 | 627 |
by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1); |
628 |
qed_spec_mp "analz_image_newK"; |
|
1885 | 629 |
|
630 |
||
631 |
goal thy |
|
632 |
"!!evs. evs : traces ==> \ |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
633 |
\ Key K : analz (insert (Key (newK evt)) \ |
1885 | 634 |
\ (insert (Key (serverKey C)) \ |
635 |
\ (sees Enemy evs))) = \ |
|
636 |
\ (K = newK evt | \ |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
637 |
\ Key K : analz (insert (Key (serverKey C)) \ |
1885 | 638 |
\ (sees Enemy evs)))"; |
1913 | 639 |
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
1885 | 640 |
insert_Key_singleton]) 1); |
641 |
by (Fast_tac 1); |
|
1913 | 642 |
qed "analz_insert_Key_newK"; |
1885 | 643 |
|
644 |
||
645 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
646 |
(*This says that the Key, K, uniquely identifies the message. |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
647 |
But if C=Enemy then he could send all sorts of nonsense.*) |
1893 | 648 |
goal thy |
649 |
"!!evs. evs : traces ==> \ |
|
650 |
\ EX X'. ALL C S A Y N B X. \ |
|
651 |
\ C ~= Enemy --> \ |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
652 |
\ Says S A Y : set_of_list evs --> \ |
1893 | 653 |
\ ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \ |
654 |
\ (X = X'))"; |
|
655 |
be traces.induct 1; |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
656 |
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
1893 | 657 |
by (ALLGOALS |
658 |
(asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); |
|
659 |
(*NS2: Case split propagates some context to other subgoal...*) |
|
660 |
by (excluded_middle_tac "K = newK evsa" 2); |
|
661 |
by (Asm_simp_tac 2); |
|
662 |
(*...we assume X is a very new message, and handle this case by contradiction*) |
|
663 |
by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)] |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
664 |
addSEs partsEs |
1893 | 665 |
addEs [Says_imp_old_keys RS less_irrefl] |
666 |
addss (!simpset)) 2); |
|
667 |
(*NS3: No relevant messages*) |
|
668 |
by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2); |
|
669 |
(*Fake*) |
|
670 |
by (Step_tac 1); |
|
671 |
br exI 1; |
|
672 |
br conjI 1; |
|
673 |
ba 2; |
|
674 |
by (Step_tac 1); |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
675 |
(** LEVEL 12 **) |
1893 | 676 |
by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \ |
677 |
\ : parts (sees Enemy evsa)" 1); |
|
678 |
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
|
1913 | 679 |
by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] |
1893 | 680 |
addDs [impOfSubs parts_insert_subset_Un] |
681 |
addss (!simpset)) 2); |
|
682 |
by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1); |
|
683 |
bd parts_singleton 1; |
|
684 |
by (Step_tac 1); |
|
685 |
bd seesD 1; |
|
686 |
by (Step_tac 1); |
|
687 |
by (Full_simp_tac 2); |
|
688 |
by (fast_tac (!claset addSDs [spec]) 1); |
|
689 |
val lemma = result(); |
|
1885 | 690 |
|
691 |
||
1893 | 692 |
(*In messages of this form, the session key uniquely identifies the rest*) |
1885 | 693 |
goal thy |
694 |
"!!evs. [| Says S A \ |
|
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
695 |
\ (Crypt {|N, Agent B, Key K, X|} (serverKey C)) \ |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
696 |
\ : set_of_list evs; \ |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
697 |
\ Says S' A' \ |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
698 |
\ (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \ |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
699 |
\ : set_of_list evs; \ |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
700 |
\ evs : traces; C ~= Enemy; C' ~= Enemy |] ==> X = X'"; |
1893 | 701 |
bd lemma 1; |
702 |
be exE 1; |
|
703 |
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); |
|
704 |
by (Fast_tac 1); |
|
705 |
qed "unique_session_keys"; |
|
1885 | 706 |
|
707 |
||
708 |
||
709 |
(*Crucial security property: Enemy does not see the keys sent in msg NS2 |
|
710 |
-- even if another key is compromised*) |
|
711 |
goal thy |
|
712 |
"!!evs. [| Says Server (Friend i) \ |
|
1913 | 713 |
\ (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs; \ |
1885 | 714 |
\ evs : traces; Friend i ~= C; Friend j ~= C \ |
715 |
\ |] ==> \ |
|
1913 | 716 |
\ K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))"; |
1885 | 717 |
be rev_mp 1; |
718 |
be traces.induct 1; |
|
1893 | 719 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
1885 | 720 |
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *) |
721 |
by (REPEAT_FIRST (resolve_tac [conjI, impI])); |
|
722 |
by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); |
|
723 |
by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
|
724 |
by (ALLGOALS |
|
725 |
(asm_full_simp_tac |
|
1913 | 726 |
(!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
727 |
analz_insert_Key_newK] @ pushes) |
|
1885 | 728 |
setloop split_tac [expand_if]))); |
729 |
(*NS2*) |
|
1893 | 730 |
by (fast_tac (!claset addSEs [less_irrefl]) 2); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
731 |
(** LEVEL 8 **) |
1885 | 732 |
(*Now for the Fake case*) |
733 |
br notI 1; |
|
734 |
by (subgoal_tac |
|
1893 | 735 |
"Key (newK evt) : \ |
1913 | 736 |
\ analz (synth (analz (insert (Key (serverKey C)) \ |
1885 | 737 |
\ (sees Enemy evsa))))" 1); |
1913 | 738 |
be (impOfSubs analz_mono) 2; |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
739 |
by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD), |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
740 |
impOfSubs synth_increasing, |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
741 |
impOfSubs analz_increasing]) 0 2); |
1885 | 742 |
(*Proves the Fake goal*) |
743 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
744 |
||
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
745 |
(**LEVEL 13**) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
746 |
(*NS3: that message from the Server was sent earlier*) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
747 |
by (mp_tac 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
748 |
by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1); |
1885 | 749 |
by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac)); |
1893 | 750 |
by (asm_full_simp_tac |
1913 | 751 |
(!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
752 |
by (Step_tac 1); |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
753 |
(**LEVEL 18 **) |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
754 |
bd unique_session_keys 1; |
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
755 |
by (REPEAT_FIRST assume_tac); |
1893 | 756 |
by (ALLGOALS Full_simp_tac); |
1929
f0839bab4b00
Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset
|
757 |
by (Step_tac 1); |
1913 | 758 |
by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1); |
1893 | 759 |
qed "Enemy_not_see_encrypted_key"; |
1885 | 760 |
|
761 |
||
762 |
||
763 |
||
1893 | 764 |
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
1885 | 765 |
|
766 |
||
1893 | 767 |
goals_limit:=4; |
1885 | 768 |
|
769 |
||
770 |
||
1893 | 771 |
goal thy |
772 |
"!!evs. [| Says Server (Friend i) \ |
|
1913 | 773 |
\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \ |
1893 | 774 |
\ evs : traces; i~=j \ |
1913 | 775 |
\ |] ==> K ~: analz (sees (Friend j) evs)"; |
776 |
br (sees_agent_subset_sees_Enemy RS analz_mono RS contra_subsetD) 1; |
|
1893 | 777 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key]))); |
778 |
qed "Friend_not_see_encrypted_key"; |
|
1885 | 779 |
|
1893 | 780 |
goal thy |
781 |
"!!evs. [| Says Server (Friend i) \ |
|
1913 | 782 |
\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \ |
1893 | 783 |
\ A ~: {Friend i, Server}; \ |
784 |
\ evs : traces \ |
|
1913 | 785 |
\ |] ==> K ~: analz (sees A evs)"; |
1893 | 786 |
by (eres_inst_tac [("P", "A~:?X")] rev_mp 1); |
787 |
by (agent.induct_tac "A" 1); |
|
788 |
by (ALLGOALS Simp_tac); |
|
789 |
by (asm_simp_tac (!simpset addsimps [eq_sym_conv, |
|
790 |
Friend_not_see_encrypted_key]) 1); |
|
1913 | 791 |
br ([analz_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1; |
1893 | 792 |
(* hyp_subst_tac would deletes the equality assumption... *) |
793 |
by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac)); |
|
794 |
qed "Agent_not_see_encrypted_key"; |
|
1885 | 795 |
|
796 |
||
1893 | 797 |
(*Neatly packaged, perhaps in a useless form*) |
798 |
goalw thy [knownBy_def] |
|
799 |
"!!evs. [| Says Server (Friend i) \ |
|
1913 | 800 |
\ (Crypt {|N, Agent B, K|} K') : set_of_list evs; \ |
1893 | 801 |
\ evs : traces \ |
802 |
\ |] ==> knownBy evs K <= {Friend i, Server}"; |
|
1885 | 803 |
|
1893 | 804 |
by (Step_tac 1); |
805 |
br ccontr 1; |
|
806 |
by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1); |
|
807 |
qed "knownBy_encrypted_key"; |
|
1885 | 808 |
|
809 |
||
810 |
||
811 |
||
812 |
||
813 |
||
814 |
||
815 |
push_proof(); |
|
816 |
goal thy |
|
817 |
"!!evs. [| evs = Says S (Friend i) \ |
|
818 |
\ (Crypt {|N, Agent(Friend j), K, X|} K') # evs'; \ |
|
819 |
\ evs : traces; i~=k \ |
|
820 |
\ |] ==> \ |
|
1913 | 821 |
\ K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))"; |
1885 | 822 |
be rev_mp 1; |
823 |
be traces.induct 1; |
|
824 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes))); |
|
825 |
by (Step_tac 1); |
|
1913 | 826 |
by (asm_full_simp_tac (!simpset addsimps[analz_subset_parts RS contra_subsetD]) 1); |
1885 | 827 |
val Enemy_not_see_encrypted_key_lemma = result(); |
828 |
||
829 |
||
830 |
||
831 |
||
832 |
||
833 |
||
834 |
||
1913 | 835 |
(*Precisely formulated as needed below. Perhaps redundant, as simplification |
836 |
with the aid of analz_subset_parts RS contra_subsetD might do the |
|
837 |
same thing.*) |
|
838 |
goal thy |
|
839 |
"!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ |
|
840 |
\ Key (serverKey A) ~: \ |
|
841 |
\ analz (insert (Key (serverKey (Friend j))) (sees Enemy evs))"; |
|
842 |
br (analz_subset_parts RS contra_subsetD) 1; |
|
843 |
by (Asm_simp_tac 1); |
|
844 |
qed "insert_not_analz_serverKey"; |
|
1885 | 845 |
|
846 |
||
847 |
||
848 |
||
849 |
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; |
|
850 |
proof_timing:=true; |
|
851 |
||
1852 | 852 |
|
853 |
||
854 |
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; |
|
855 |
||
856 |
||
857 |
||
858 |
(*If a message is sent, encrypted with a Friend's server key, then either |
|
859 |
that Friend or the Server originally sent it.*) |
|
860 |
goal thy |
|
861 |
"!!evs. evs : traces ==> \ |
|
862 |
\ ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \ |
|
1913 | 863 |
\ : set_of_list evs --> \ |
864 |
\ (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : set_of_list evs | \ |
|
865 |
\ Says (Friend i) B' (Crypt X (serverKey (Friend i))) : set_of_list evs)"; |
|
1852 | 866 |
be traces.induct 1; |
867 |
by (Step_tac 1); |
|
868 |
by (ALLGOALS Asm_full_simp_tac); |
|
869 |
(*Remaining cases are Fake, NS2 and NS3*) |
|
870 |
by (Fast_tac 2); (*Proves the NS2 case*) |
|
871 |
||
872 |
by (REPEAT (dtac spec 2)); |
|
873 |
fe conjE; |
|
874 |
bd mp 2; |
|
875 |
||
876 |
by (REPEAT (resolve_tac [refl, conjI] 2)); |
|
877 |
by (ALLGOALS Asm_full_simp_tac); |
|
878 |
||
879 |
||
880 |
||
881 |
||
882 |
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
|
883 |
be conjE 2; |
|
884 |
by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2); |
|
885 |
||
886 |
(*The NS3 case needs the induction hypothesis twice! |
|
887 |
One application is to the X component of the most recent message.*) |
|
888 |
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2); |
|
889 |
by (Fast_tac 3); |
|
890 |
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); |
|
891 |
be conjE 2; |
|
892 |
(*DELETE the first quantified formula: it's now useless*) |
|
893 |
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); |
|
894 |
by (fast_tac (!claset addss (!simpset)) 2); |
|
895 |
(*Now for the Fake case*) |
|
896 |
be disjE 1; |
|
897 |
(*The subcase of Fake, where the message in question is NOT the most recent*) |
|
898 |
by (Best_tac 2); |
|
899 |
||
900 |
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); |
|
1913 | 901 |
be Crypt_synth 1; |
902 |
be Key_synth 2; |
|
1852 | 903 |
|
1913 | 904 |
(*Split up the possibilities of that message being synthd...*) |
1852 | 905 |
by (Step_tac 1); |
906 |
by (Best_tac 6); |
|
907 |
||
908 |
||
909 |
||
910 |
||
911 |
||
1839 | 912 |
(*NEEDED??*) |
913 |
||
914 |
goal thy "!!A. X ~= Y ==> (X : sees A (Says B C Y # evs)) = (X : sees A evs)"; |
|
915 |
by (asm_simp_tac (!simpset addsimps [sees_Cons] |
|
916 |
setloop split_tac [expand_if]) 1); |
|
917 |
qed "in_sees_Says"; |
|
918 |
||
919 |
goal thy "!!A. X ~: parts {Y} ==> \ |
|
920 |
\ (X : parts (sees A (Says B C Y # evs))) = \ |
|
921 |
\ (X : parts (sees A evs))"; |
|
922 |
by (asm_simp_tac (!simpset addsimps [sees_Cons] |
|
923 |
setloop split_tac [expand_if]) 1); |
|
924 |
by (asm_simp_tac (!simpset addsimps [parts_Un]) 1); |
|
925 |
qed "in_parts_sees_Says"; |
|
926 |
||
1852 | 927 |
goal thy "!!evs. length evs < length evs' ==> newK evs ~= newK (A',evs')"; |
1839 | 928 |
by (fast_tac (!claset addSEs [less_irrefl]) 1); |
929 |
qed "length_less_newK_neq"; |
|
930 |
||
931 |
||
932 |
||
933 |
||
934 |
||
935 |
||
936 |
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; |
|
937 |
||
938 |
goalw thy [keysFor_def] |
|
939 |
"!!X. Crypt X K: H ==> invKey K : keysFor H"; |
|
940 |
by (Fast_tac 1); |
|
941 |
qed "keysFor_I"; |
|
942 |
AddSIs [keysFor_I]; |
|
943 |
||
944 |
goalw thy [keysFor_def] |
|
945 |
"!!K. K : keysFor H ==> EX X K'. K=invKey K' & Crypt X K': H"; |
|
946 |
by (Fast_tac 1); |
|
947 |
qed "keysFor_D"; |
|
948 |
AddSDs [keysFor_D]; |
|
949 |
||
950 |