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 |
|
|
12 |
|
|
13 |
open Event;
|
|
14 |
|
1852
|
15 |
(*Rewrite using {a} Un A = insert a A *)
|
|
16 |
Addsimps [insert_is_Un RS sym];
|
|
17 |
|
|
18 |
|
|
19 |
(*** Basic properties of serverKey and newK ***)
|
|
20 |
|
1839
|
21 |
(* invKey (serverKey A) = serverKey A *)
|
|
22 |
bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
|
|
23 |
|
1852
|
24 |
(* invKey (newK evs) = newK evs *)
|
1839
|
25 |
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
|
|
26 |
Addsimps [invKey_serverKey, invKey_newK];
|
|
27 |
|
|
28 |
|
|
29 |
(*New keys and nonces are fresh*)
|
|
30 |
val serverKey_inject = inj_serverKey RS injD;
|
1852
|
31 |
val newN_inject = inj_newN RS injD
|
|
32 |
and newK_inject = inj_newK RS injD;
|
1839
|
33 |
AddSEs [serverKey_inject, newN_inject, newK_inject,
|
|
34 |
fresh_newK RS notE, fresh_newN RS notE];
|
|
35 |
Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
|
|
36 |
Addsimps [fresh_newN, fresh_newK];
|
|
37 |
|
1852
|
38 |
goal thy "newK evs ~= serverKey B";
|
|
39 |
by (subgoal_tac "newK evs = serverKey B --> \
|
|
40 |
\ Key (newK evs) : parts (initState B)" 1);
|
1839
|
41 |
by (Fast_tac 1);
|
|
42 |
by (agent.induct_tac "B" 1);
|
|
43 |
by (auto_tac (!claset addIs [range_eqI], !simpset));
|
|
44 |
qed "newK_neq_serverKey";
|
|
45 |
|
|
46 |
Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
|
|
47 |
|
|
48 |
(*Good for talking about Server's initial state*)
|
|
49 |
goal thy "parts (range (Key o f)) = range (Key o f)";
|
|
50 |
by (auto_tac (!claset addIs [range_eqI], !simpset));
|
|
51 |
be parts.induct 1;
|
|
52 |
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
|
|
53 |
qed "parts_range_Key";
|
|
54 |
|
|
55 |
goal thy "analyze (range (Key o f)) = range (Key o f)";
|
|
56 |
by (auto_tac (!claset addIs [range_eqI], !simpset));
|
|
57 |
be analyze.induct 1;
|
|
58 |
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
|
|
59 |
qed "analyze_range_Key";
|
|
60 |
|
|
61 |
Addsimps [parts_range_Key, analyze_range_Key];
|
|
62 |
|
|
63 |
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
|
|
64 |
by (agent.induct_tac "C" 1);
|
|
65 |
by (auto_tac (!claset addIs [range_eqI], !simpset));
|
|
66 |
qed "keysFor_parts_initState";
|
|
67 |
Addsimps [keysFor_parts_initState];
|
|
68 |
|
|
69 |
|
|
70 |
(**** Inductive relation "traces" -- basic properties ****)
|
|
71 |
|
|
72 |
val mk_cases = traces.mk_cases (list.simps @ agent.simps @ event.simps);
|
|
73 |
|
|
74 |
val Says_tracesE = mk_cases "Says A B X # evs: traces";
|
|
75 |
val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces";
|
|
76 |
val Says_Enemy_tracesE = mk_cases "Says Enemy B X # evs: traces";
|
|
77 |
val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces";
|
|
78 |
val Notes_tracesE = mk_cases "Notes A X # evs: traces";
|
|
79 |
|
|
80 |
|
|
81 |
(*The tail of a trace is a trace*)
|
|
82 |
goal thy "!!ev evs. ev#evs : traces ==> evs : traces";
|
|
83 |
by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
|
|
84 |
qed "traces_ConsE";
|
|
85 |
|
|
86 |
(** Specialized rewrite rules for (sees A (Says...#evs)) **)
|
|
87 |
|
|
88 |
goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
|
|
89 |
by (Simp_tac 1);
|
|
90 |
qed "sees_own";
|
|
91 |
|
|
92 |
goal thy "!!A. Server ~= A ==> \
|
|
93 |
\ sees Server (Says A B X # evs) = sees Server evs";
|
|
94 |
by (Asm_simp_tac 1);
|
|
95 |
qed "sees_Server";
|
|
96 |
|
|
97 |
goal thy "!!A. Friend i ~= A ==> \
|
|
98 |
\ sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
|
|
99 |
by (Asm_simp_tac 1);
|
|
100 |
qed "sees_Friend";
|
|
101 |
|
|
102 |
goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
|
|
103 |
by (Simp_tac 1);
|
|
104 |
qed "sees_Enemy";
|
|
105 |
|
|
106 |
goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
|
|
107 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
|
|
108 |
by (Fast_tac 1);
|
1852
|
109 |
qed "sees_Says_subset_insert";
|
|
110 |
|
|
111 |
goal thy "sees A evs <= sees A (Says A' B X # evs)";
|
|
112 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
|
|
113 |
by (Fast_tac 1);
|
|
114 |
qed "sees_subset_sees_Says";
|
1839
|
115 |
|
|
116 |
(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
|
|
117 |
goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
|
|
118 |
\ parts {Y} Un (UN A. parts (sees A evs))";
|
|
119 |
by (Step_tac 1);
|
|
120 |
be rev_mp 1; (*for some reason, split_tac does not work on assumptions*)
|
|
121 |
val ss = (!simpset addsimps [parts_Un, sees_Cons]
|
|
122 |
setloop split_tac [expand_if]);
|
|
123 |
by (ALLGOALS (fast_tac (!claset addss ss)));
|
|
124 |
qed "UN_parts_sees_Says";
|
|
125 |
|
|
126 |
|
|
127 |
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
|
1852
|
128 |
Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****)
|
1839
|
129 |
|
|
130 |
|
|
131 |
(**** Inductive proofs about traces ****)
|
|
132 |
|
|
133 |
(*The Enemy can see more than anybody else, except for their initial state*)
|
|
134 |
goal thy
|
|
135 |
"!!evs. evs : traces ==> \
|
|
136 |
\ sees A evs <= initState A Un sees Enemy evs";
|
|
137 |
be traces.induct 1;
|
1852
|
138 |
be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*)
|
|
139 |
be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*)
|
|
140 |
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD]
|
1839
|
141 |
addss (!simpset))));
|
|
142 |
qed "sees_agent_subset_sees_Enemy";
|
|
143 |
|
|
144 |
|
1852
|
145 |
goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList evs";
|
|
146 |
be traces.induct 1;
|
|
147 |
by (Auto_tac());
|
|
148 |
qed_spec_mp "not_Says_to_self";
|
|
149 |
Addsimps [not_Says_to_self];
|
|
150 |
AddSEs [not_Says_to_self RSN (2, rev_notE)];
|
|
151 |
|
|
152 |
|
1839
|
153 |
(*** Server keys are not betrayed ***)
|
|
154 |
|
1852
|
155 |
(*Enemy never sees another agent's server key!*)
|
1839
|
156 |
goal thy
|
1852
|
157 |
"!!evs. [| evs : traces; A ~= Enemy |] ==> \
|
|
158 |
\ Key (serverKey A) ~: parts (sees Enemy evs)";
|
1839
|
159 |
be traces.induct 1;
|
1852
|
160 |
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
|
|
161 |
by (auto_tac(!claset, !simpset addsimps [parts_insert2]));
|
1839
|
162 |
(*Deals with Faked messages*)
|
1852
|
163 |
by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
|
|
164 |
impOfSubs parts_insert_subset_Un]
|
1839
|
165 |
addss (!simpset)) 1);
|
|
166 |
qed "Enemy_not_see_serverKey";
|
|
167 |
|
1852
|
168 |
bind_thm ("Enemy_not_analyze_serverKey",
|
|
169 |
[analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
|
|
170 |
|
|
171 |
Addsimps [Enemy_not_see_serverKey, Enemy_not_analyze_serverKey];
|
|
172 |
|
1839
|
173 |
|
1852
|
174 |
(*No Friend will ever see another agent's server key
|
|
175 |
(excluding the Enemy, who might transmit his).*)
|
1839
|
176 |
goal thy
|
1852
|
177 |
"!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \
|
|
178 |
\ Key (serverKey A) ~: parts (sees (Friend j) evs)";
|
|
179 |
br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
|
|
180 |
by (ALLGOALS Asm_simp_tac);
|
|
181 |
qed "Friend_not_see_serverKey";
|
1839
|
182 |
|
|
183 |
|
|
184 |
(*** Future keys can't be seen or used! ***)
|
|
185 |
|
|
186 |
(*Nobody can have SEEN keys that will be generated in the future.
|
|
187 |
This has to be proved anew for each protocol description,
|
|
188 |
but should go by similar reasoning every time. Hardest case is the
|
|
189 |
standard Fake rule.
|
|
190 |
The length comparison, and Union over C, are essential for the
|
|
191 |
induction! *)
|
|
192 |
goal thy "!!evs. evs : traces ==> \
|
|
193 |
\ length evs <= length evs' --> \
|
1852
|
194 |
\ Key (newK evs') ~: (UN C. parts (sees C evs))";
|
1839
|
195 |
be traces.induct 1;
|
1852
|
196 |
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
|
1839
|
197 |
by (ALLGOALS (asm_full_simp_tac
|
|
198 |
(!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
|
|
199 |
(*Initial state? New keys cannot clash*)
|
|
200 |
by (Fast_tac 1);
|
|
201 |
(*Rule NS1 in protocol*)
|
|
202 |
by (fast_tac (!claset addDs [less_imp_le]) 2);
|
|
203 |
(*Rule NS2 in protocol*)
|
|
204 |
by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
|
1852
|
205 |
(*Rule NS3 in protocol*)
|
|
206 |
by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
|
1839
|
207 |
(*Rule Fake: where an Enemy agent can say practically anything*)
|
1852
|
208 |
by (best_tac (!claset addDs [impOfSubs analyze_subset_parts,
|
|
209 |
impOfSubs parts_insert_subset_Un,
|
1839
|
210 |
less_imp_le]
|
|
211 |
addss (!simpset)) 1);
|
|
212 |
val lemma = result();
|
|
213 |
|
|
214 |
(*Variant needed for the main theorem below*)
|
|
215 |
goal thy
|
|
216 |
"!!evs. [| evs : traces; length evs <= length evs' |] ==> \
|
1852
|
217 |
\ Key (newK evs') ~: parts (sees C evs)";
|
1839
|
218 |
by (fast_tac (!claset addDs [lemma]) 1);
|
|
219 |
qed "new_keys_not_seen";
|
|
220 |
|
1852
|
221 |
goal thy "!!K. newK evs = invKey K ==> newK evs = K";
|
1839
|
222 |
br (invKey_eq RS iffD1) 1;
|
|
223 |
by (Simp_tac 1);
|
|
224 |
val newK_invKey = result();
|
|
225 |
|
1852
|
226 |
|
|
227 |
val keysFor_parts_mono = parts_mono RS keysFor_mono;
|
|
228 |
|
1839
|
229 |
(*Nobody can have USED keys that will be generated in the future.
|
|
230 |
...very like new_keys_not_seen*)
|
|
231 |
goal thy "!!evs. evs : traces ==> \
|
|
232 |
\ length evs <= length evs' --> \
|
1852
|
233 |
\ newK evs' ~: keysFor (UN C. parts (sees C evs))";
|
1839
|
234 |
be traces.induct 1;
|
1852
|
235 |
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
|
1839
|
236 |
by (ALLGOALS (asm_full_simp_tac
|
|
237 |
(!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
|
|
238 |
(*Rule NS1 in protocol*)
|
|
239 |
by (fast_tac (!claset addDs [less_imp_le]) 2);
|
|
240 |
(*Rule NS2 in protocol*)
|
|
241 |
by (fast_tac (!claset addDs [less_imp_le]) 2);
|
|
242 |
(*Rule Fake: where an Enemy agent can say practically anything*)
|
|
243 |
by (best_tac
|
|
244 |
(!claset addSDs [newK_invKey]
|
1852
|
245 |
addDs [impOfSubs (analyze_subset_parts RS keysFor_mono),
|
|
246 |
impOfSubs (parts_insert_subset_Un RS keysFor_mono),
|
1839
|
247 |
less_imp_le]
|
|
248 |
addEs [new_keys_not_seen RS not_parts_not_analyze RSN (2,rev_notE)]
|
|
249 |
addss (!simpset)) 1);
|
1852
|
250 |
(*Rule NS3: quite messy...*)
|
|
251 |
by (hyp_subst_tac 1);
|
|
252 |
by (full_simp_tac (!simpset addcongs [conj_cong]) 1);
|
|
253 |
br impI 1;
|
|
254 |
bd mp 1;
|
|
255 |
by (fast_tac (!claset addDs [less_imp_le]) 1);
|
|
256 |
by (best_tac (!claset addIs
|
|
257 |
[impOfSubs (sees_subset_sees_Says RS keysFor_parts_mono),
|
|
258 |
impOfSubs (sees_own RS equalityD2 RS keysFor_parts_mono),
|
|
259 |
impOfSubs (empty_subsetI RS insert_mono RS keysFor_parts_mono)]
|
|
260 |
addss (!simpset)) 1);
|
1839
|
261 |
val lemma = result();
|
|
262 |
|
|
263 |
goal thy
|
|
264 |
"!!evs. [| evs : traces; length evs <= length evs' |] ==> \
|
1852
|
265 |
\ newK evs' ~: keysFor (parts (sees C evs))";
|
1839
|
266 |
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
|
|
267 |
qed "new_keys_not_used";
|
1852
|
268 |
Addsimps [new_keys_not_used];
|
1839
|
269 |
|
1852
|
270 |
bind_thm ("new_keys_not_analyzed",
|
1839
|
271 |
[analyze_subset_parts RS keysFor_mono,
|
|
272 |
new_keys_not_used] MRS contra_subsetD);
|
|
273 |
|
|
274 |
|
1852
|
275 |
(*Maybe too specific to be of much use...*)
|
|
276 |
goal thy
|
|
277 |
"!!evs. [| Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} \
|
|
278 |
\ (serverKey A)) \
|
|
279 |
\ : setOfList evs; \
|
|
280 |
\ evs : traces \
|
|
281 |
\ |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
|
|
282 |
be rev_mp 1;
|
|
283 |
be traces.induct 1;
|
|
284 |
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
|
|
285 |
be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*)
|
|
286 |
by (ALLGOALS Asm_full_simp_tac);
|
|
287 |
by (Fast_tac 1); (*Proves the NS2 case*)
|
|
288 |
qed "Says_Server_imp_X_eq_Crypt";
|
|
289 |
|
|
290 |
|
1839
|
291 |
(*Pushes Crypt events in so that others might be pulled out*)
|
|
292 |
goal thy "insert (Crypt X K) (insert y evs) = \
|
|
293 |
\ insert y (insert (Crypt X K) evs)";
|
|
294 |
by (Fast_tac 1);
|
|
295 |
qed "insert_Crypt_delay";
|
|
296 |
|
|
297 |
goal thy "insert (Key K) (insert y evs) = \
|
|
298 |
\ insert y (insert (Key K) evs)";
|
|
299 |
by (Fast_tac 1);
|
|
300 |
qed "insert_Key_delay";
|
|
301 |
|
1852
|
302 |
|
1839
|
303 |
(** Lemmas concerning the form of items passed in messages **)
|
|
304 |
|
|
305 |
(*Describes the form *and age* of K when the following message is sent*)
|
|
306 |
goal thy
|
1852
|
307 |
"!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') \
|
1839
|
308 |
\ : setOfList evs; \
|
|
309 |
\ evs : traces \
|
1852
|
310 |
\ |] ==> (EX evs'. K = Key (newK evs') & length evs' < length evs)";
|
1839
|
311 |
be rev_mp 1;
|
|
312 |
be traces.induct 1;
|
1852
|
313 |
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
|
1839
|
314 |
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
|
|
315 |
qed "Says_Server_imp_Key_newK";
|
|
316 |
|
1852
|
317 |
(* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *)
|
|
318 |
bind_thm ("not_parts_not_keysFor_analyze",
|
|
319 |
analyze_subset_parts RS keysFor_mono RS contra_subsetD);
|
|
320 |
|
|
321 |
|
|
322 |
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
|
1839
|
323 |
|
1852
|
324 |
ZZZZZZZZZZZZZZZZ;
|
|
325 |
|
|
326 |
|
|
327 |
(*Fake case below may need something like this...*)
|
|
328 |
goal thy
|
|
329 |
"!!evs. evs : traces ==> \
|
|
330 |
\ ALL B X. Crypt X (serverKey B) : analyze (sees Enemy evs) --> \
|
|
331 |
\ (EX A A'. Says A A' (Crypt X (serverKey B)) : setOfList evs";
|
1839
|
332 |
|
|
333 |
goal thy
|
1852
|
334 |
"!!evs. evs : traces ==> \
|
|
335 |
\ ALL NA B K X. Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B) :
|
|
336 |
analyze (sees Enemy evs) --> \
|
|
337 |
\ (EX A A'. Says A A' (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B)) : setOfList evs";
|
|
338 |
|
|
339 |
|
|
340 |
|
|
341 |
(*Describes the form of X when the following message is sent*)
|
|
342 |
goal thy
|
|
343 |
"!!evs. evs : traces ==> \
|
|
344 |
\ ALL S A NA B K X. \
|
|
345 |
\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
|
|
346 |
\ : setOfList evs --> \
|
|
347 |
\ (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
|
1839
|
348 |
be traces.induct 1;
|
1852
|
349 |
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
|
|
350 |
by (Step_tac 1);
|
|
351 |
by (ALLGOALS Asm_full_simp_tac);
|
|
352 |
(*Remaining cases are Fake, NS2 and NS3*)
|
|
353 |
by (Fast_tac 2); (*Solves the NS2 case*)
|
|
354 |
(*The NS3 case needs the induction hypothesis twice!
|
|
355 |
One application is to the X component of the most recent message.*)
|
|
356 |
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
|
|
357 |
be conjE 2;
|
|
358 |
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent (Friend i)|} (serverKey B)" 2);
|
|
359 |
by (eres_inst_tac [("V","?P|?Q")] thin_rl 3); (*speeds the following step*)
|
|
360 |
by (Fast_tac 3);
|
|
361 |
(*DELETE the first quantified formula: it's now useless*)
|
|
362 |
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
|
|
363 |
by (fast_tac (!claset addss (!simpset)) 2);
|
|
364 |
(*Now for the Fake case*)
|
|
365 |
be disjE 1;
|
|
366 |
(*The subcase of Fake, where the message in question is NOT the most recent*)
|
|
367 |
by (Best_tac 2);
|
|
368 |
(*The subcase of Fake proved because server keys are kept secret*)
|
|
369 |
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
|
|
370 |
be Crypt_synthesize 1;
|
|
371 |
be Key_synthesize 2;
|
|
372 |
by (Asm_full_simp_tac 2);
|
|
373 |
|
|
374 |
|
|
375 |
|
|
376 |
1. !!evs B X evsa S A NA Ba K Xa.
|
|
377 |
[| evsa : traces;
|
|
378 |
! S A NA B K X.
|
|
379 |
Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) :
|
|
380 |
setOfList evsa -->
|
|
381 |
(? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B));
|
|
382 |
B ~= Enemy;
|
|
383 |
Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey B) :
|
|
384 |
analyze (sees Enemy evsa) |] ==>
|
|
385 |
? evs'. Xa = Crypt {|Key (newK evs'), Agent B|} (serverKey Ba)
|
|
386 |
|
|
387 |
|
|
388 |
(*Split up the possibilities of that message being synthesized...*)
|
|
389 |
by (Step_tac 1);
|
|
390 |
by (Best_tac 6);
|
|
391 |
|
|
392 |
|
|
393 |
|
|
394 |
|
|
395 |
by (Safe_step_tac 1);
|
|
396 |
by (Safe_step_tac 2);
|
1839
|
397 |
by (ALLGOALS Asm_full_simp_tac);
|
1852
|
398 |
by (REPEAT_FIRST (etac disjE));
|
|
399 |
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
|
|
400 |
|
|
401 |
|
|
402 |
by (hyp_subst_tac 5);
|
|
403 |
|
|
404 |
|
|
405 |
|
|
406 |
|
|
407 |
|
|
408 |
by (REPEAT (dtac spec 3));
|
|
409 |
fe conjE;
|
|
410 |
fe mp ;
|
|
411 |
by (REPEAT (resolve_tac [refl, conjI] 3));
|
|
412 |
by (REPEAT_FIRST (etac conjE));
|
|
413 |
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
|
|
414 |
|
|
415 |
|
|
416 |
by (subgoal_tac "? evs'. Xa = Crypt {|Key (newK evs'), Agent Aa|} (serverKey Ba)" 2);
|
|
417 |
by (Fast_tac 3);
|
|
418 |
|
|
419 |
|
|
420 |
|
|
421 |
be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*)
|
|
422 |
|
|
423 |
|
|
424 |
auto();
|
|
425 |
by (ALLGOALS
|
|
426 |
(asm_full_simp_tac (!simpset addsimps [de_Morgan_disj,de_Morgan_conj])));
|
|
427 |
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
|
|
428 |
|
|
429 |
by (REPEAT (Safe_step_tac 1));
|
|
430 |
|
|
431 |
qed "Says_Crypt_Nonce_imp_msg_Crypt";
|
|
432 |
|
|
433 |
goal thy
|
|
434 |
"!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
|
|
435 |
\ : setOfList evs; \
|
|
436 |
\ evs : traces \
|
|
437 |
\ |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))";
|
|
438 |
|
|
439 |
|
|
440 |
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
|
|
441 |
|
|
442 |
|
|
443 |
WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
|
|
444 |
|
|
445 |
(*If a message is sent, encrypted with a Friend's server key, then either
|
|
446 |
that Friend or the Server originally sent it.*)
|
|
447 |
goal thy
|
|
448 |
"!!evs. evs : traces ==> \
|
|
449 |
\ ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \
|
|
450 |
\ : setOfList evs --> \
|
|
451 |
\ (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : setOfList evs | \
|
|
452 |
\ Says (Friend i) B' (Crypt X (serverKey (Friend i))) : setOfList evs)";
|
|
453 |
be traces.induct 1;
|
|
454 |
be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*)
|
|
455 |
by (Step_tac 1);
|
|
456 |
by (ALLGOALS Asm_full_simp_tac);
|
|
457 |
(*Remaining cases are Fake, NS2 and NS3*)
|
|
458 |
by (Fast_tac 2); (*Proves the NS2 case*)
|
|
459 |
|
|
460 |
by (REPEAT (dtac spec 2));
|
|
461 |
fe conjE;
|
|
462 |
bd mp 2;
|
|
463 |
|
|
464 |
by (REPEAT (resolve_tac [refl, conjI] 2));
|
|
465 |
by (ALLGOALS Asm_full_simp_tac);
|
|
466 |
|
|
467 |
|
|
468 |
|
|
469 |
|
|
470 |
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
|
|
471 |
be conjE 2;
|
|
472 |
by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2);
|
|
473 |
|
|
474 |
(*The NS3 case needs the induction hypothesis twice!
|
|
475 |
One application is to the X component of the most recent message.*)
|
|
476 |
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2);
|
|
477 |
by (Fast_tac 3);
|
|
478 |
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
|
|
479 |
be conjE 2;
|
|
480 |
(*DELETE the first quantified formula: it's now useless*)
|
|
481 |
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
|
|
482 |
by (fast_tac (!claset addss (!simpset)) 2);
|
|
483 |
(*Now for the Fake case*)
|
|
484 |
be disjE 1;
|
|
485 |
(*The subcase of Fake, where the message in question is NOT the most recent*)
|
|
486 |
by (Best_tac 2);
|
|
487 |
|
|
488 |
by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac));
|
|
489 |
be Crypt_synthesize 1;
|
|
490 |
be Key_synthesize 2;
|
|
491 |
|
|
492 |
(*Split up the possibilities of that message being synthesized...*)
|
|
493 |
by (Step_tac 1);
|
|
494 |
by (Best_tac 6);
|
|
495 |
|
|
496 |
|
|
497 |
|
|
498 |
|
|
499 |
|
|
500 |
(*The NS3 case needs the induction hypothesis twice!
|
|
501 |
One application is to the X component of the most recent message.*)
|
|
502 |
|
|
503 |
????????????????????????????????????????????????????????????????
|
|
504 |
by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 1);
|
|
505 |
by (Fast_tac 2);
|
|
506 |
|
|
507 |
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
|
|
508 |
|
|
509 |
be conjE 1;
|
|
510 |
(*DELETE the first quantified formula: it's now useless*)
|
|
511 |
by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 1);
|
|
512 |
by (fast_tac (!claset addss (!simpset)) 1);
|
|
513 |
|
|
514 |
|
|
515 |
(*Now for the Fake case*)
|
|
516 |
be disjE 1;
|
|
517 |
(*The subcase of Fake, where the message in question is NOT the most recent*)
|
|
518 |
by (Best_tac 2);
|
|
519 |
|
|
520 |
WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
|
|
521 |
|
|
522 |
|
|
523 |
Addsimps [new_keys_not_seen];
|
|
524 |
|
|
525 |
(*Crucial security property: Enemy does not see the keys sent in msg NS2
|
|
526 |
-- even if another friend's key is compromised*)
|
|
527 |
goal thy
|
|
528 |
"!!evs. [| Says Server (Friend i) \
|
|
529 |
\ (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \
|
|
530 |
\ evs : traces; i~=j |] ==> \
|
|
531 |
\ \
|
|
532 |
\ K ~: analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
|
|
533 |
be rev_mp 1;
|
|
534 |
be traces.induct 1;
|
|
535 |
be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*)
|
|
536 |
by (ALLGOALS Asm_full_simp_tac);
|
|
537 |
(*The two simplifications cannot be combined -- they loop!*)
|
|
538 |
by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay])));
|
|
539 |
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
|
1839
|
540 |
br conjI 3;
|
|
541 |
by (REPEAT_FIRST (resolve_tac [impI]));
|
|
542 |
by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
|
|
543 |
(*NS1, subgoal concerns "(Says A Server
|
1852
|
544 |
{|Agent A, Agent B, Nonce (newN evsa)|}"*)
|
1839
|
545 |
(*... thus it cannot equal any components of A's message above.*)
|
|
546 |
by (fast_tac (!claset addss (!simpset)) 2);
|
|
547 |
(*NS2, the subcase where that message was the most recently sent;
|
1852
|
548 |
it holds because here K' = serverKey(Friend i), which Enemies can't see,
|
|
549 |
AND because nobody can know about a brand new key*)
|
|
550 |
by (fast_tac (!claset addss (!simpset addsimps [not_parts_not_analyze])) 2);
|
|
551 |
(*NS2, other subcase. K is an old key, and thus not in the latest message.*)
|
1839
|
552 |
by (fast_tac
|
|
553 |
(!claset addSEs [less_irrefl]
|
1852
|
554 |
addDs [impOfSubs analyze_insert_Crypt_subset]
|
|
555 |
addss (!simpset addsimps [not_parts_not_keysFor_analyze])) 2);
|
1839
|
556 |
(*Now for the Fake case*)
|
|
557 |
be exE 1;
|
|
558 |
br notI 1;
|
|
559 |
by (REPEAT (etac conjE 1));
|
|
560 |
by (REPEAT (hyp_subst_tac 1));
|
1852
|
561 |
by (subgoal_tac
|
|
562 |
"Key (newK evs') : \
|
|
563 |
\ analyze (synthesize (analyze (insert (Key (serverKey (Friend j))) \
|
|
564 |
\ (sees Enemy evsa))))" 1);
|
|
565 |
be (impOfSubs analyze_mono) 2;
|
1839
|
566 |
by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN
|
|
567 |
(2,rev_subsetD),
|
1852
|
568 |
impOfSubs synthesize_increasing,
|
|
569 |
impOfSubs analyze_increasing]) 2);
|
1839
|
570 |
(*Proves the Fake goal*)
|
|
571 |
by (Auto_tac());
|
1852
|
572 |
qed "Enemy_not_see_encrypted_key";
|
|
573 |
|
|
574 |
|
|
575 |
goal thy
|
|
576 |
"!!evs. [| Says Server (Friend i) \
|
|
577 |
\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \
|
|
578 |
\ evs : traces; i~=j \
|
|
579 |
\ |] ==> K ~: analyze (sees (Friend j) evs)";
|
|
580 |
br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1;
|
|
581 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key])));
|
|
582 |
qed "Friend_not_see_encrypted_key";
|
|
583 |
|
|
584 |
goal thy
|
|
585 |
"!!evs. [| Says Server (Friend i) \
|
|
586 |
\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \
|
|
587 |
\ A ~: {Friend i, Server}; \
|
|
588 |
\ evs : traces \
|
|
589 |
\ |] ==> K ~: analyze (sees A evs)";
|
|
590 |
by (eres_inst_tac [("P", "A~:?X")] rev_mp 1);
|
|
591 |
by (agent.induct_tac "A" 1);
|
|
592 |
by (ALLGOALS Simp_tac);
|
|
593 |
by (asm_simp_tac (!simpset addsimps [eq_sym_conv,
|
|
594 |
Friend_not_see_encrypted_key]) 1);
|
|
595 |
br ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1;
|
|
596 |
(* hyp_subst_tac would deletes the equality assumption... *)
|
|
597 |
by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac));
|
|
598 |
qed "Agent_not_see_encrypted_key";
|
|
599 |
|
|
600 |
|
|
601 |
(*Neatly packaged, perhaps in a useless form*)
|
|
602 |
goalw thy [knownBy_def]
|
|
603 |
"!!evs. [| Says Server (Friend i) \
|
|
604 |
\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \
|
|
605 |
\ evs : traces \
|
|
606 |
\ |] ==> knownBy evs K <= {Friend i, Server}";
|
|
607 |
|
|
608 |
by (Step_tac 1);
|
|
609 |
br ccontr 1;
|
|
610 |
by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1);
|
|
611 |
qed "knownBy_encrypted_key";
|
|
612 |
|
1839
|
613 |
|
|
614 |
|
|
615 |
|
|
616 |
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
|
|
617 |
|
1852
|
618 |
|
1839
|
619 |
|
|
620 |
|
|
621 |
|
|
622 |
goal thy
|
1852
|
623 |
"!!evs. evs : traces ==> \
|
|
624 |
\ Says Server A \
|
|
625 |
\ (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs \
|
|
626 |
\ --> (EX evs'. N = Nonce (newN evs'))";
|
1839
|
627 |
be traces.induct 1;
|
1852
|
628 |
by (ALLGOALS Asm_simp_tac);
|
|
629 |
by (Fast_tac 1);
|
|
630 |
val Says_Server_lemma = result();
|
1839
|
631 |
|
|
632 |
|
|
633 |
(*NEEDED??*)
|
|
634 |
|
|
635 |
goal thy "!!A. X ~= Y ==> (X : sees A (Says B C Y # evs)) = (X : sees A evs)";
|
|
636 |
by (asm_simp_tac (!simpset addsimps [sees_Cons]
|
|
637 |
setloop split_tac [expand_if]) 1);
|
|
638 |
qed "in_sees_Says";
|
|
639 |
|
|
640 |
goal thy "!!A. X ~: parts {Y} ==> \
|
|
641 |
\ (X : parts (sees A (Says B C Y # evs))) = \
|
|
642 |
\ (X : parts (sees A evs))";
|
|
643 |
by (asm_simp_tac (!simpset addsimps [sees_Cons]
|
|
644 |
setloop split_tac [expand_if]) 1);
|
|
645 |
by (asm_simp_tac (!simpset addsimps [parts_Un]) 1);
|
|
646 |
qed "in_parts_sees_Says";
|
|
647 |
|
1852
|
648 |
goal thy "!!evs. length evs < length evs' ==> newK evs ~= newK (A',evs')";
|
1839
|
649 |
by (fast_tac (!claset addSEs [less_irrefl]) 1);
|
|
650 |
qed "length_less_newK_neq";
|
|
651 |
|
|
652 |
|
|
653 |
|
|
654 |
goal thy "insert (Crypt x) (insert {|X,Y|} evs) = \
|
|
655 |
\ insert {|X,Y|} (insert (Crypt x) evs)";
|
|
656 |
by (Fast_tac 1);
|
|
657 |
qed "insert_Crypt_MPair_delay";
|
|
658 |
|
|
659 |
|
|
660 |
|
|
661 |
YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
|
|
662 |
|
|
663 |
goalw thy [keysFor_def]
|
|
664 |
"!!X. Crypt X K: H ==> invKey K : keysFor H";
|
|
665 |
by (Fast_tac 1);
|
|
666 |
qed "keysFor_I";
|
|
667 |
AddSIs [keysFor_I];
|
|
668 |
|
|
669 |
goalw thy [keysFor_def]
|
|
670 |
"!!K. K : keysFor H ==> EX X K'. K=invKey K' & Crypt X K': H";
|
|
671 |
by (Fast_tac 1);
|
|
672 |
qed "keysFor_D";
|
|
673 |
AddSDs [keysFor_D];
|
|
674 |
|
|
675 |
|