18 |
18 |
19 (*Weak liveness: there are traces that reach the end*) |
19 (*Weak liveness: there are traces that reach the end*) |
20 |
20 |
21 goal thy |
21 goal thy |
22 "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ |
22 "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ |
23 \ ==> EX X NB K. EX evs: yahalom. \ |
23 \ ==> EX X NB K. EX evs: yahalom lost. \ |
24 \ Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs"; |
24 \ Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs"; |
25 by (REPEAT (resolve_tac [exI,bexI] 1)); |
25 by (REPEAT (resolve_tac [exI,bexI] 1)); |
26 br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2; |
26 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2); |
27 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); |
27 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); |
28 by (ALLGOALS Fast_tac); |
28 by (ALLGOALS Fast_tac); |
29 result(); |
29 result(); |
30 |
30 |
31 |
31 |
32 (**** Inductive proofs about yahalom ****) |
32 (**** Inductive proofs about yahalom ****) |
33 |
33 |
34 (*The Enemy can see more than anybody else, except for their initial state*) |
34 (*The Spy can see more than anybody else, except for their initial state*) |
35 goal thy |
35 goal thy |
36 "!!evs. evs : yahalom ==> \ |
36 "!!evs. evs : yahalom lost ==> \ |
37 \ sees A evs <= initState A Un sees Enemy evs"; |
37 \ sees lost A evs <= initState lost A Un sees lost Spy evs"; |
38 be yahalom.induct 1; |
38 by (etac yahalom.induct 1); |
39 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
39 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
40 addss (!simpset)))); |
40 addss (!simpset)))); |
41 qed "sees_agent_subset_sees_Enemy"; |
41 qed "sees_agent_subset_sees_Spy"; |
42 |
42 |
43 |
43 |
44 (*Nobody sends themselves messages*) |
44 (*Nobody sends themselves messages*) |
45 goal thy "!!evs. evs : yahalom ==> ALL A X. Says A A X ~: set_of_list evs"; |
45 goal thy "!!evs. evs : yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs"; |
46 be yahalom.induct 1; |
46 by (etac yahalom.induct 1); |
47 by (Auto_tac()); |
47 by (Auto_tac()); |
48 qed_spec_mp "not_Says_to_self"; |
48 qed_spec_mp "not_Says_to_self"; |
49 Addsimps [not_Says_to_self]; |
49 Addsimps [not_Says_to_self]; |
50 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
50 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
51 |
51 |
52 |
52 |
53 (** For reasoning about the encrypted portion of messages **) |
53 (** For reasoning about the encrypted portion of messages **) |
54 |
54 |
55 (*Lets us treat YM4 using a similar argument as for the Fake case.*) |
55 (*Lets us treat YM4 using a similar argument as for the Fake case.*) |
56 goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \ |
56 goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \ |
57 \ X : analz (sees Enemy evs)"; |
57 \ X : analz (sees lost Spy evs)"; |
58 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1); |
58 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
59 qed "YM4_analz_sees_Enemy"; |
59 qed "YM4_analz_sees_Spy"; |
60 |
60 |
61 goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \ |
61 goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \ |
62 \ : set_of_list evs ==> \ |
62 \ : set_of_list evs ==> \ |
63 \ K : parts (sees Enemy evs)"; |
63 \ K : parts (sees lost Spy evs)"; |
64 by (fast_tac (!claset addSEs partsEs |
64 by (fast_tac (!claset addSEs partsEs |
65 addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1); |
65 addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
66 qed "YM4_parts_sees_Enemy"; |
66 qed "YM4_parts_sees_Spy"; |
67 |
67 |
68 |
68 |
69 |
69 |
70 (** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY |
70 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
71 sends messages containing X! **) |
71 sends messages containing X! **) |
72 |
72 |
73 (*Enemy never sees another agent's shared key! (unless it is leaked at start)*) |
73 (*Spy never sees lost another agent's shared key! (unless it is leaked at start)*) |
74 goal thy |
74 goal thy |
75 "!!evs. [| evs : yahalom; A ~: bad |] \ |
75 "!!evs. [| evs : yahalom lost; A ~: lost |] \ |
76 \ ==> Key (shrK A) ~: parts (sees Enemy evs)"; |
76 \ ==> Key (shrK A) ~: parts (sees lost Spy evs)"; |
77 be yahalom.induct 1; |
77 by (etac yahalom.induct 1); |
78 bd (YM4_analz_sees_Enemy RS synth.Inj) 6; |
78 by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6); |
79 by (ALLGOALS Asm_simp_tac); |
79 by (ALLGOALS Asm_simp_tac); |
80 by (stac insert_commute 3); |
80 by (stac insert_commute 3); |
81 by (Auto_tac()); |
81 by (Auto_tac()); |
82 (*Fake and YM4 are similar*) |
82 (*Fake and YM4 are similar*) |
83 by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts, |
83 by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts, |
84 impOfSubs Fake_parts_insert]))); |
84 impOfSubs Fake_parts_insert]))); |
85 qed "Enemy_not_see_shrK"; |
85 qed "Spy_not_see_shrK"; |
86 |
86 |
87 bind_thm ("Enemy_not_analz_shrK", |
87 bind_thm ("Spy_not_analz_shrK", |
88 [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD); |
88 [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD); |
89 |
89 |
90 Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK]; |
90 Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK]; |
91 |
91 |
92 (*We go to some trouble to preserve R in the 3rd and 4th subgoals |
92 (*We go to some trouble to preserve R in the 3rd and 4th subgoals |
93 As usual fast_tac cannot be used because it uses the equalities too soon*) |
93 As usual fast_tac cannot be used because it uses the equalities too soon*) |
94 val major::prems = |
94 val major::prems = |
95 goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ |
95 goal thy "[| Key (shrK A) : parts (sees lost Spy evs); \ |
96 \ evs : yahalom; \ |
96 \ evs : yahalom lost; \ |
97 \ A:bad ==> R \ |
97 \ A:lost ==> R \ |
98 \ |] ==> R"; |
98 \ |] ==> R"; |
99 br ccontr 1; |
99 by (rtac ccontr 1); |
100 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; |
100 by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1); |
101 by (swap_res_tac prems 2); |
101 by (swap_res_tac prems 2); |
102 by (ALLGOALS (fast_tac (!claset addIs prems))); |
102 by (ALLGOALS (fast_tac (!claset addIs prems))); |
103 qed "Enemy_see_shrK_E"; |
103 qed "Spy_see_shrK_E"; |
104 |
104 |
105 bind_thm ("Enemy_analz_shrK_E", |
105 bind_thm ("Spy_analz_shrK_E", |
106 analz_subset_parts RS subsetD RS Enemy_see_shrK_E); |
106 analz_subset_parts RS subsetD RS Spy_see_shrK_E); |
107 |
107 |
108 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E]; |
108 AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E]; |
109 |
109 |
110 |
110 |
111 (*** Future keys can't be seen or used! ***) |
111 (*** Future keys can't be seen or used! ***) |
112 |
112 |
113 (*Nobody can have SEEN keys that will be generated in the future. |
113 (*Nobody can have SEEN keys that will be generated in the future. |
114 This has to be proved anew for each protocol description, |
114 This has to be proved anew for each protocol description, |
115 but should go by similar reasoning every time. Hardest case is the |
115 but should go by similar reasoning every time. Hardest case is the |
116 standard Fake rule. |
116 standard Fake rule. |
117 The length comparison, and Union over C, are essential for the |
117 The length comparison, and Union over C, are essential for the |
118 induction! *) |
118 induction! *) |
119 goal thy "!!evs. evs : yahalom ==> \ |
119 goal thy "!!evs. evs : yahalom lost ==> \ |
120 \ length evs <= length evs' --> \ |
120 \ length evs <= length evs' --> \ |
121 \ Key (newK evs') ~: (UN C. parts (sees C evs))"; |
121 \ Key (newK evs') ~: (UN C. parts (sees lost C evs))"; |
122 be yahalom.induct 1; |
122 by (etac yahalom.induct 1); |
123 bd (YM4_analz_sees_Enemy RS synth.Inj) 6; |
123 by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6); |
124 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
124 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
125 impOfSubs parts_insert_subset_Un, |
125 impOfSubs parts_insert_subset_Un, |
126 Suc_leD] |
126 Suc_leD] |
127 addss (!simpset)))); |
127 addss (!simpset)))); |
128 val lemma = result(); |
128 val lemma = result(); |
129 |
129 |
130 (*Variant needed for the main theorem below*) |
130 (*Variant needed for the main theorem below*) |
131 goal thy |
131 goal thy |
132 "!!evs. [| evs : yahalom; length evs <= length evs' |] \ |
132 "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \ |
133 \ ==> Key (newK evs') ~: parts (sees C evs)"; |
133 \ ==> Key (newK evs') ~: parts (sees lost C evs)"; |
134 by (fast_tac (!claset addDs [lemma]) 1); |
134 by (fast_tac (!claset addDs [lemma]) 1); |
135 qed "new_keys_not_seen"; |
135 qed "new_keys_not_seen"; |
136 Addsimps [new_keys_not_seen]; |
136 Addsimps [new_keys_not_seen]; |
137 |
137 |
138 (*Another variant: old messages must contain old keys!*) |
138 (*Another variant: old messages must contain old keys!*) |
139 goal thy |
139 goal thy |
140 "!!evs. [| Says A B X : set_of_list evs; \ |
140 "!!evs. [| Says A B X : set_of_list evs; \ |
141 \ Key (newK evt) : parts {X}; \ |
141 \ Key (newK evt) : parts {X}; \ |
142 \ evs : yahalom \ |
142 \ evs : yahalom lost \ |
143 \ |] ==> length evt < length evs"; |
143 \ |] ==> length evt < length evs"; |
144 br ccontr 1; |
144 by (rtac ccontr 1); |
145 bd leI 1; |
145 by (dtac leI 1); |
146 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy] |
146 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] |
147 addIs [impOfSubs parts_mono]) 1); |
147 addIs [impOfSubs parts_mono]) 1); |
148 qed "Says_imp_old_keys"; |
148 qed "Says_imp_old_keys"; |
149 |
149 |
150 |
150 |
151 (*Nobody can have USED keys that will be generated in the future. |
151 (*Nobody can have USED keys that will be generated in the future. |
152 ...very like new_keys_not_seen*) |
152 ...very like new_keys_not_seen*) |
153 goal thy "!!evs. evs : yahalom ==> \ |
153 goal thy "!!evs. evs : yahalom lost ==> \ |
154 \ length evs <= length evs' --> \ |
154 \ length evs <= length evs' --> \ |
155 \ newK evs' ~: keysFor (UN C. parts (sees C evs))"; |
155 \ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; |
156 be yahalom.induct 1; |
156 by (etac yahalom.induct 1); |
157 by (forward_tac [YM4_parts_sees_Enemy] 6); |
157 by (forward_tac [YM4_parts_sees_Spy] 6); |
158 bd (YM4_analz_sees_Enemy RS synth.Inj) 6; |
158 by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6); |
159 by (ALLGOALS Asm_full_simp_tac); |
159 by (ALLGOALS Asm_full_simp_tac); |
160 (*YM1, YM2 and YM3*) |
160 (*YM1, YM2 and YM3*) |
161 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2])); |
161 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2])); |
162 (*Fake and YM4: these messages send unknown (X) components*) |
162 (*Fake and YM4: these messages send unknown (X) components*) |
163 by (stac insert_commute 2); |
163 by (stac insert_commute 2); |
165 (*YM4: the only way K could have been used is if it had been seen, |
165 (*YM4: the only way K could have been used is if it had been seen, |
166 contradicting new_keys_not_seen*) |
166 contradicting new_keys_not_seen*) |
167 by (ALLGOALS |
167 by (ALLGOALS |
168 (best_tac |
168 (best_tac |
169 (!claset addDs [impOfSubs analz_subset_parts, |
169 (!claset addDs [impOfSubs analz_subset_parts, |
170 impOfSubs (analz_subset_parts RS keysFor_mono), |
170 impOfSubs (analz_subset_parts RS keysFor_mono), |
171 impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
171 impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
172 Suc_leD] |
172 Suc_leD] |
173 addEs [new_keys_not_seen RSN(2,rev_notE)] |
173 addEs [new_keys_not_seen RSN(2,rev_notE)] |
174 addss (!simpset)))); |
174 addss (!simpset)))); |
175 val lemma = result(); |
175 val lemma = result(); |
176 |
176 |
177 goal thy |
177 goal thy |
178 "!!evs. [| evs : yahalom; length evs <= length evs' |] \ |
178 "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \ |
179 \ ==> newK evs' ~: keysFor (parts (sees C evs))"; |
179 \ ==> newK evs' ~: keysFor (parts (sees lost C evs))"; |
180 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
180 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); |
181 qed "new_keys_not_used"; |
181 qed "new_keys_not_used"; |
182 |
182 |
183 bind_thm ("new_keys_not_analzd", |
183 bind_thm ("new_keys_not_analzd", |
184 [analz_subset_parts RS keysFor_mono, |
184 [analz_subset_parts RS keysFor_mono, |
185 new_keys_not_used] MRS contra_subsetD); |
185 new_keys_not_used] MRS contra_subsetD); |
186 |
186 |
187 Addsimps [new_keys_not_used, new_keys_not_analzd]; |
187 Addsimps [new_keys_not_used, new_keys_not_analzd]; |
188 |
188 |
189 |
189 |
190 (** Lemmas concerning the form of items passed in messages **) |
190 (** Lemmas concerning the form of items passed in messages **) |
191 |
191 |
192 |
192 |
193 (**** |
193 (**** |
194 The following is to prove theorems of the form |
194 The following is to prove theorems of the form |
195 |
195 |
196 Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==> |
196 Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==> |
197 Key K : analz (sees Enemy evs) |
197 Key K : analz (sees lost Spy evs) |
198 |
198 |
199 A more general formula must be proved inductively. |
199 A more general formula must be proved inductively. |
200 |
200 |
201 ****) |
201 ****) |
202 |
202 |
203 |
203 |
204 (*NOT useful in this form, but it says that session keys are not used |
204 (*NOT useful in this form, but it says that session keys are not used |
205 to encrypt messages containing other keys, in the actual protocol. |
205 to encrypt messages containing other keys, in the actual protocol. |
206 We require that agents should behave like this subsequently also.*) |
206 We require that agents should behave like this subsequently also.*) |
207 goal thy |
207 goal thy |
208 "!!evs. evs : yahalom ==> \ |
208 "!!evs. evs : yahalom lost ==> \ |
209 \ (Crypt X (newK evt)) : parts (sees Enemy evs) & \ |
209 \ (Crypt X (newK evt)) : parts (sees lost Spy evs) & \ |
210 \ Key K : parts {X} --> Key K : parts (sees Enemy evs)"; |
210 \ Key K : parts {X} --> Key K : parts (sees lost Spy evs)"; |
211 be yahalom.induct 1; |
211 by (etac yahalom.induct 1); |
212 bd (YM4_analz_sees_Enemy RS synth.Inj) 6; |
212 by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6); |
213 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
213 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); |
214 (*Deals with Faked messages*) |
214 (*Deals with Faked messages*) |
215 by (EVERY |
215 by (EVERY |
216 (map (best_tac (!claset addSEs partsEs |
216 (map (best_tac (!claset addSEs partsEs |
217 addDs [impOfSubs parts_insert_subset_Un] |
217 addDs [impOfSubs parts_insert_subset_Un] |
218 addss (!simpset))) |
218 addss (!simpset))) |
219 [3,2])); |
219 [3,2])); |
220 (*Base case*) |
220 (*Base case*) |
221 by (Auto_tac()); |
221 by (Auto_tac()); |
222 result(); |
222 result(); |
223 |
223 |
263 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); |
263 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); |
264 val lemma = result(); |
264 val lemma = result(); |
265 |
265 |
266 |
266 |
267 goal thy |
267 goal thy |
268 "!!evs. evs : yahalom ==> \ |
268 "!!evs. evs : yahalom lost ==> \ |
269 \ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \ |
269 \ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ |
270 \ (K : newK``E | Key K : analz (sees Enemy evs))"; |
270 \ (K : newK``E | Key K : analz (sees lost Spy evs))"; |
271 be yahalom.induct 1; |
271 by (etac yahalom.induct 1); |
272 bd YM4_analz_sees_Enemy 6; |
272 by (dtac YM4_analz_sees_Spy 6); |
273 by (REPEAT_FIRST (resolve_tac [allI, lemma])); |
273 by (REPEAT_FIRST (resolve_tac [allI, lemma])); |
274 by (ALLGOALS |
274 by (ALLGOALS |
275 (asm_simp_tac |
275 (asm_simp_tac |
276 (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] |
276 (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] |
277 @ pushes) |
277 @ pushes) |
278 setloop split_tac [expand_if]))); |
278 setloop split_tac [expand_if]))); |
279 (*YM4*) |
279 (*YM4*) |
280 by (enemy_analz_tac 4); |
280 by (spy_analz_tac 4); |
281 (*YM3*) |
281 (*YM3*) |
282 by (Fast_tac 3); |
282 by (Fast_tac 3); |
283 (*Fake case*) |
283 (*Fake case*) |
284 by (enemy_analz_tac 2); |
284 by (spy_analz_tac 2); |
285 (*Base case*) |
285 (*Base case*) |
286 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
286 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); |
287 qed_spec_mp "analz_image_newK"; |
287 qed_spec_mp "analz_image_newK"; |
288 |
288 |
289 goal thy |
289 goal thy |
290 "!!evs. evs : yahalom ==> \ |
290 "!!evs. evs : yahalom lost ==> \ |
291 \ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \ |
291 \ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ |
292 \ (K = newK evt | Key K : analz (sees Enemy evs))"; |
292 \ (K = newK evt | Key K : analz (sees lost Spy evs))"; |
293 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
293 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, |
294 insert_Key_singleton]) 1); |
294 insert_Key_singleton]) 1); |
295 by (Fast_tac 1); |
295 by (Fast_tac 1); |
296 qed "analz_insert_Key_newK"; |
296 qed "analz_insert_Key_newK"; |
297 |
297 |
298 |
298 |
299 (*Describes the form of K when the Server sends this message.*) |
299 (*Describes the form of K when the Server sends this message.*) |
300 goal thy |
300 goal thy |
301 "!!evs. [| Says Server A \ |
301 "!!evs. [| Says Server A \ |
302 \ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \ |
302 \ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \ |
303 \ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \ |
303 \ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \ |
304 \ evs : yahalom |] \ |
304 \ evs : yahalom lost |] \ |
305 \ ==> (EX evt:yahalom. K = Key(newK evt))"; |
305 \ ==> (EX evt: yahalom lost. K = Key(newK evt))"; |
306 be rev_mp 1; |
306 by (etac rev_mp 1); |
307 be yahalom.induct 1; |
307 by (etac yahalom.induct 1); |
308 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
308 by (ALLGOALS (fast_tac (!claset addss (!simpset)))); |
309 qed "Says_Server_message_form"; |
309 qed "Says_Server_message_form"; |
310 |
310 |
311 |
311 |
312 (** Crucial secrecy property: Enemy does not see the keys sent in msg YM3 |
312 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 |
313 As with Otway-Rees, proof does not need uniqueness of session keys. **) |
313 As with Otway-Rees, proof does not need uniqueness of session keys. **) |
314 |
314 |
315 goal thy |
315 goal thy |
316 "!!evs. [| A ~: bad; B ~: bad; evs : yahalom; evt : yahalom |] \ |
316 "!!evs. [| A ~: lost; B ~: lost; evs : yahalom lost; evt : yahalom lost |] \ |
317 \ ==> Says Server A \ |
317 \ ==> Says Server A \ |
318 \ {|Crypt {|Agent B, Key(newK evt), NA, NB|} (shrK A), \ |
318 \ {|Crypt {|Agent B, Key(newK evt), NA, NB|} (shrK A), \ |
319 \ Crypt {|Agent A, Key(newK evt)|} (shrK B)|} \ |
319 \ Crypt {|Agent A, Key(newK evt)|} (shrK B)|} \ |
320 \ : set_of_list evs --> \ |
320 \ : set_of_list evs --> \ |
321 \ Key(newK evt) ~: analz (sees Enemy evs)"; |
321 \ Key(newK evt) ~: analz (sees lost Spy evs)"; |
322 be yahalom.induct 1; |
322 by (etac yahalom.induct 1); |
323 bd YM4_analz_sees_Enemy 6; |
323 by (dtac YM4_analz_sees_Spy 6); |
324 by (ALLGOALS |
324 by (ALLGOALS |
325 (asm_simp_tac |
325 (asm_simp_tac |
326 (!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
326 (!simpset addsimps ([analz_subset_parts RS contra_subsetD, |
327 analz_insert_Key_newK] @ pushes) |
327 analz_insert_Key_newK] @ pushes) |
328 setloop split_tac [expand_if]))); |
328 setloop split_tac [expand_if]))); |
329 (*YM4*) |
329 (*YM4*) |
330 by (enemy_analz_tac 3); |
330 by (spy_analz_tac 3); |
331 (*YM3*) |
331 (*YM3*) |
332 by (fast_tac (!claset addIs [parts_insertI] |
332 by (fast_tac (!claset addIs [parts_insertI] |
333 addEs [Says_imp_old_keys RS less_irrefl] |
333 addEs [Says_imp_old_keys RS less_irrefl] |
334 addss (!simpset)) 2); |
334 addss (!simpset)) 2); |
335 (*Fake*) (** LEVEL 10 **) |
335 (*Fake*) (** LEVEL 10 **) |
336 by (enemy_analz_tac 1); |
336 by (spy_analz_tac 1); |
337 val lemma = result() RS mp RSN(2,rev_notE); |
337 val lemma = result() RS mp RSN(2,rev_notE); |
338 |
338 |
339 |
339 |
340 (*Final version: Server's message in the most abstract form*) |
340 (*Final version: Server's message in the most abstract form*) |
341 goal thy |
341 goal thy |
342 "!!evs. [| Says Server A \ |
342 "!!evs. [| Says Server A \ |
343 \ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \ |
343 \ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \ |
344 \ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \ |
344 \ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \ |
345 \ A ~: bad; B ~: bad; evs : yahalom |] ==> \ |
345 \ A ~: lost; B ~: lost; evs : yahalom lost |] ==> \ |
346 \ K ~: analz (sees Enemy evs)"; |
346 \ K ~: analz (sees lost Spy evs)"; |
347 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
347 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
348 by (fast_tac (!claset addSEs [lemma]) 1); |
348 by (fast_tac (!claset addSEs [lemma]) 1); |
349 qed "Enemy_not_see_encrypted_key"; |
349 qed "Spy_not_see_encrypted_key"; |
350 |
350 |
351 |
351 |
352 (** Towards proofs of stronger authenticity properties **) |
352 (** Towards proofs of stronger authenticity properties **) |
353 |
353 |
354 goal thy |
354 goal thy |
355 "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees Enemy evs); \ |
355 "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \ |
356 \ B ~: bad; evs : yahalom |] \ |
356 \ B ~: lost; evs : yahalom lost |] \ |
357 \ ==> EX NA NB. Says Server A \ |
357 \ ==> EX NA NB. Says Server A \ |
358 \ {|Crypt {|Agent B, Key K, \ |
358 \ {|Crypt {|Agent B, Key K, \ |
359 \ Nonce NA, Nonce NB|} (shrK A), \ |
359 \ Nonce NA, Nonce NB|} (shrK A), \ |
360 \ Crypt {|Agent A, Key K|} (shrK B)|} \ |
360 \ Crypt {|Agent A, Key K|} (shrK B)|} \ |
361 \ : set_of_list evs"; |
361 \ : set_of_list evs"; |
362 be rev_mp 1; |
362 by (etac rev_mp 1); |
363 be yahalom.induct 1; |
363 by (etac yahalom.induct 1); |
364 bd (YM4_analz_sees_Enemy RS synth.Inj) 6; |
364 by (dtac (YM4_analz_sees_Spy RS synth.Inj) 6); |
365 by (ALLGOALS Asm_simp_tac); |
365 by (ALLGOALS Asm_simp_tac); |
366 (*YM3*) |
366 (*YM3*) |
367 by (Fast_tac 3); |
367 by (Fast_tac 3); |
368 (*Base case*) |
368 (*Base case*) |
369 by (fast_tac (!claset addss (!simpset)) 1); |
369 by (fast_tac (!claset addss (!simpset)) 1); |
370 (*Prepare YM4*) |
370 (*Prepare YM4*) |
371 by (stac insert_commute 2 THEN Simp_tac 2); |
371 by (stac insert_commute 2 THEN Simp_tac 2); |
372 (*Fake and YM4 are similar*) |
372 (*Fake and YM4 are similar*) |
373 by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts, |
373 by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts, |
374 impOfSubs Fake_parts_insert]))); |
374 impOfSubs Fake_parts_insert]))); |
375 qed "Crypt_imp_Server_msg"; |
375 qed "Crypt_imp_Server_msg"; |
376 |
376 |
377 |
377 |
378 (*What can B deduce from receipt of YM4? |
378 (*What can B deduce from receipt of YM4? |
379 NOT THAT THE NONCES AGREE (in this version). But what does the Nonce |
379 NOT THAT THE NONCES AGREE (in this version). But what does the Nonce |
380 give us??*) |
380 give us??*) |
381 goal thy |
381 goal thy |
382 "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B), \ |
382 "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B), \ |
383 \ Crypt (Nonce NB) K|} : set_of_list evs; \ |
383 \ Crypt (Nonce NB) K|} : set_of_list evs; \ |
384 \ B ~: bad; evs : yahalom |] \ |
384 \ B ~: lost; evs : yahalom lost |] \ |
385 \ ==> EX NA NB. Says Server A \ |
385 \ ==> EX NA NB. Says Server A \ |
386 \ {|Crypt {|Agent B, Key K, \ |
386 \ {|Crypt {|Agent B, Key K, \ |
387 \ Nonce NA, Nonce NB|} (shrK A), \ |
387 \ Nonce NA, Nonce NB|} (shrK A), \ |
388 \ Crypt {|Agent A, Key K|} (shrK B)|} \ |
388 \ Crypt {|Agent A, Key K|} (shrK B)|} \ |
389 \ : set_of_list evs"; |
389 \ : set_of_list evs"; |
390 be rev_mp 1; |
390 by (etac rev_mp 1); |
391 be yahalom.induct 1; |
391 by (etac yahalom.induct 1); |
392 by (dresolve_tac [YM4_analz_sees_Enemy] 6); |
392 by (dtac YM4_analz_sees_Spy 6); |
393 by (ALLGOALS Asm_simp_tac); |
393 by (ALLGOALS Asm_simp_tac); |
394 by (ALLGOALS (fast_tac (!claset addSDs [impOfSubs analz_subset_parts RS |
394 by (ALLGOALS (fast_tac (!claset addSDs [impOfSubs analz_subset_parts RS |
395 Crypt_imp_Server_msg]))); |
395 Crypt_imp_Server_msg]))); |
396 qed "YM4_imp_Says_Server_A"; |
396 qed "YM4_imp_Says_Server_A"; |
397 |
397 |
398 |
398 |
399 |
399 |
400 goal thy |
400 goal thy |
401 "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B), \ |
401 "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B), \ |
402 \ Crypt (Nonce NB) K|} : set_of_list evs; \ |
402 \ Crypt (Nonce NB) K|} : set_of_list evs; \ |
403 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
403 \ A ~: lost; B ~: lost; evs : yahalom lost |] \ |
404 \ ==> Key K ~: analz (sees Enemy evs)"; |
404 \ ==> Key K ~: analz (sees lost Spy evs)"; |
405 by (fast_tac (!claset addSDs [YM4_imp_Says_Server_A, |
405 by (fast_tac (!claset addSDs [YM4_imp_Says_Server_A, |
406 Enemy_not_see_encrypted_key]) 1); |
406 Spy_not_see_encrypted_key]) 1); |
407 qed "B_gets_secure_key"; |
407 qed "B_gets_secure_key"; |