93 (**** Authenticity properties obtained from NS2 ****) |
93 (**** Authenticity properties obtained from NS2 ****) |
94 |
94 |
95 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
95 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
96 is secret. (Honest users generate fresh nonces.)*) |
96 is secret. (Honest users generate fresh nonces.)*) |
97 goal thy |
97 goal thy |
98 "!!evs. evs : ns_public \ |
98 "!!evs. [| Nonce NA ~: analz (sees lost Spy evs); \ |
99 \ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ |
99 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \ |
100 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
100 \ evs : ns_public |] \ |
101 \ Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)"; |
101 \ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)"; |
|
102 by (etac rev_mp 1); |
|
103 by (etac rev_mp 1); |
102 by (analz_induct_tac 1); |
104 by (analz_induct_tac 1); |
103 (*NS3*) |
105 (*NS3*) |
104 by (fast_tac (!claset addSEs partsEs) 4); |
106 by (fast_tac (!claset addSEs partsEs) 4); |
105 (*NS2*) |
107 (*NS2*) |
106 by (fast_tac (!claset addSEs partsEs) 3); |
108 by (fast_tac (!claset addSEs partsEs) 3); |
107 (*Fake*) |
109 (*Fake*) |
108 by (best_tac (!claset addIs [analz_insertI] |
110 by (deepen_tac (!claset addSIs [analz_insertI] |
109 addDs [impOfSubs analz_subset_parts, |
111 addDs [impOfSubs analz_subset_parts, |
110 impOfSubs Fake_parts_insert] |
112 impOfSubs Fake_parts_insert] |
111 addss (!simpset)) 2); |
113 addss (!simpset)) 0 2); |
112 (*Base*) |
114 (*Base*) |
113 by (fast_tac (!claset addss (!simpset)) 1); |
115 by (fast_tac (!claset addss (!simpset)) 1); |
114 bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp)); |
116 qed "no_nonce_NS1_NS2"; |
115 |
117 |
116 |
118 |
117 (*Unicity for NS1: nonce NA identifies agents A and B*) |
119 (*Unicity for NS1: nonce NA identifies agents A and B*) |
118 goal thy |
120 goal thy |
119 "!!evs. evs : ns_public \ |
121 "!!evs. [| Nonce NA ~: analz (sees lost Spy evs); evs : ns_public |] \ |
120 \ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ |
122 \ ==> EX A' B'. ALL A B. \ |
121 \ (EX A' B'. ALL A B. \ |
|
122 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
123 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
123 \ A=A' & B=B')"; |
124 \ A=A' & B=B'"; |
|
125 by (etac rev_mp 1); |
124 by (analz_induct_tac 1); |
126 by (analz_induct_tac 1); |
125 (*NS1*) |
127 (*NS1*) |
126 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); |
128 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); |
127 by (expand_case_tac "NA = ?y" 3 THEN |
129 by (expand_case_tac "NA = ?y" 3 THEN |
128 REPEAT (fast_tac (!claset addSEs partsEs) 3)); |
130 REPEAT (fast_tac (!claset addSEs partsEs) 3)); |
148 qed "unique_NA"; |
150 qed "unique_NA"; |
149 |
151 |
150 |
152 |
151 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
153 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
152 goal thy |
154 goal thy |
153 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
155 "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set_of_list evs; \ |
154 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ |
156 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
155 \ --> Nonce NA ~: analz (sees lost Spy evs)"; |
157 \ ==> Nonce NA ~: analz (sees lost Spy evs)"; |
|
158 by (etac rev_mp 1); |
156 by (analz_induct_tac 1); |
159 by (analz_induct_tac 1); |
157 (*NS3*) |
160 (*NS3*) |
158 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
161 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
159 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); |
162 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); |
160 (*NS1*) |
163 (*NS2*) |
161 by (fast_tac (!claset addSEs partsEs |
164 by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
162 addSDs [Says_imp_sees_Spy' RS parts.Inj] |
165 addSEs [MPair_parts] |
|
166 addDs [parts.Body, unique_NA]) 0 3); |
|
167 (*NS1*) |
|
168 by (fast_tac (!claset addSEs sees_Spy_partsEs |
163 addIs [impOfSubs analz_subset_parts]) 2); |
169 addIs [impOfSubs analz_subset_parts]) 2); |
164 (*Fake*) |
170 (*Fake*) |
165 by (spy_analz_tac 1); |
171 by (spy_analz_tac 1); |
166 (*NS2*) |
172 qed "Spy_not_see_NA"; |
167 by (Step_tac 1); |
|
168 by (fast_tac (!claset addSEs partsEs |
|
169 addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
170 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
|
171 addDs [unique_NA]) 1); |
|
172 bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp)); |
|
173 |
173 |
174 |
174 |
175 (*Authentication for A: if she receives message 2 and has used NA |
175 (*Authentication for A: if she receives message 2 and has used NA |
176 to start a run, then B has sent message 2.*) |
176 to start a run, then B has sent message 2.*) |
177 goal thy |
177 goal thy |
178 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
178 "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\ |
179 \ ==> Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \ |
179 \ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs;\ |
180 \ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ |
180 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
181 \ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs"; |
181 \ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs"; |
182 by (analz_induct_tac 1); |
182 by (etac rev_mp 1); |
|
183 (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*) |
|
184 by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1); |
|
185 by (etac ns_public.induct 1); |
183 by (ALLGOALS Asm_simp_tac); |
186 by (ALLGOALS Asm_simp_tac); |
184 (*NS1*) |
187 (*NS1*) |
185 by (fast_tac (!claset addSEs partsEs |
188 by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); |
186 addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
187 (*Fake*) |
189 (*Fake*) |
188 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
190 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
189 by (fast_tac (!claset addss (!simpset)) 1); |
191 by (fast_tac (!claset addss (!simpset)) 1); |
190 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); |
192 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); |
191 by (best_tac (!claset addSIs [disjI2] |
193 by (best_tac (!claset addSIs [disjI2] |
193 addDs [impOfSubs analz_subset_parts] |
195 addDs [impOfSubs analz_subset_parts] |
194 addss (!simpset)) 1); |
196 addss (!simpset)) 1); |
195 (*NS2*) |
197 (*NS2*) |
196 by (Step_tac 1); |
198 by (Step_tac 1); |
197 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); |
199 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); |
198 (*11 seconds*) |
200 by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
199 by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
201 addDs [unique_NA]) 1 1); |
200 addDs [unique_NA]) 1); |
|
201 qed_spec_mp "NA_decrypt_imp_B_msg"; |
|
202 |
|
203 (*Corollary: if A receives B's message NS2 and the nonce NA agrees |
|
204 then that message really originated with B.*) |
|
205 goal thy |
|
206 "!!evs. [| Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs;\ |
|
207 \ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\ |
|
208 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
|
209 \ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs"; |
|
210 by (fast_tac (!claset addSIs [NA_decrypt_imp_B_msg] |
|
211 addEs partsEs |
|
212 addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); |
|
213 qed "A_trusts_NS2"; |
202 qed "A_trusts_NS2"; |
214 |
203 |
215 (*If the encrypted message appears then it originated with Alice in NS1*) |
204 (*If the encrypted message appears then it originated with Alice in NS1*) |
216 goal thy |
205 goal thy |
217 "!!evs. evs : ns_public \ |
206 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs); \ |
218 \ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ |
207 \ Nonce NA ~: analz (sees lost Spy evs); \ |
219 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ |
208 \ evs : ns_public |] \ |
220 \ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; |
209 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; |
|
210 by (etac rev_mp 1); |
|
211 by (etac rev_mp 1); |
221 by (analz_induct_tac 1); |
212 by (analz_induct_tac 1); |
222 (*Fake*) |
213 (*Fake*) |
223 by (best_tac (!claset addSIs [disjI2] |
214 by (best_tac (!claset addSIs [disjI2] |
224 addSDs [impOfSubs Fake_parts_insert] |
215 addSDs [impOfSubs Fake_parts_insert] |
225 addIs [analz_insertI] |
216 addIs [analz_insertI] |
234 (**** Authenticity properties obtained from NS2 ****) |
225 (**** Authenticity properties obtained from NS2 ****) |
235 |
226 |
236 (*Unicity for NS2: nonce NB identifies agent A and nonce NA |
227 (*Unicity for NS2: nonce NB identifies agent A and nonce NA |
237 [proof closely follows that for unique_NA] *) |
228 [proof closely follows that for unique_NA] *) |
238 goal thy |
229 goal thy |
239 "!!evs. evs : ns_public \ |
230 "!!evs. [| Nonce NB ~: analz (sees lost Spy evs); evs : ns_public |] \ |
240 \ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ |
231 \ ==> EX A' NA'. ALL A NA. \ |
241 \ (EX A' NA'. ALL A NA. \ |
232 \ Crypt (pubK A) {|Nonce NA, Nonce NB|} \ |
242 \ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (sees lost Spy evs) --> \ |
233 \ : parts (sees lost Spy evs) --> A=A' & NA=NA'"; |
243 \ A=A' & NA=NA')"; |
234 by (etac rev_mp 1); |
244 by (analz_induct_tac 1); |
235 by (analz_induct_tac 1); |
245 (*NS2*) |
236 (*NS2*) |
246 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); |
237 by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); |
247 by (expand_case_tac "NB = ?y" 3 THEN |
238 by (expand_case_tac "NB = ?y" 3 THEN |
248 REPEAT (fast_tac (!claset addSEs partsEs) 3)); |
239 REPEAT (fast_tac (!claset addSEs partsEs) 3)); |
268 qed "unique_NB"; |
259 qed "unique_NB"; |
269 |
260 |
270 |
261 |
271 (*NB remains secret PROVIDED Alice never responds with round 3*) |
262 (*NB remains secret PROVIDED Alice never responds with round 3*) |
272 goal thy |
263 goal thy |
273 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
264 "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs;\ |
274 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs --> \ |
265 \ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set_of_list evs); \ |
275 \ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set_of_list evs) --> \ |
266 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
276 \ Nonce NB ~: analz (sees lost Spy evs)"; |
267 \ ==> Nonce NB ~: analz (sees lost Spy evs)"; |
277 by (analz_induct_tac 1); |
268 by (etac rev_mp 1); |
278 (*NS1*) |
269 by (etac rev_mp 1); |
279 by (fast_tac (!claset addSEs partsEs |
270 by (analz_induct_tac 1); |
280 addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); |
271 (*NS1*) |
|
272 by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); |
281 (*Fake*) |
273 (*Fake*) |
282 by (spy_analz_tac 1); |
274 by (spy_analz_tac 1); |
283 (*NS2 and NS3*) |
275 (*NS2 and NS3*) |
284 by (Step_tac 1); |
276 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
285 by (TRYALL (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]))); |
277 by (step_tac (!claset delrules [allI]) 1); |
286 (*NS2*) |
278 by (Fast_tac 5); |
287 by (fast_tac (!claset addSEs partsEs |
279 by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); |
288 addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); |
280 (*NS2*) |
|
281 by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); |
289 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
282 by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
290 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); |
283 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); |
291 (*NS3*) |
284 (*NS3*) |
292 by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 |
285 by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 |
293 THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); |
286 THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); |
294 by (Fast_tac 1); |
287 by (Fast_tac 1); |
295 bind_thm ("Spy_not_see_NB", result() RSN (2, rev_mp) RS mp); |
288 qed "Spy_not_see_NB"; |
296 |
289 |
297 |
290 |
298 |
291 |
299 (*Authentication for B: if he receives message 3 and has used NB |
292 (*Authentication for B: if he receives message 3 and has used NB |
300 in message 2, then A has sent message 3.*) |
293 in message 2, then A has sent message 3--to somebody....*) |
301 goal thy |
294 goal thy |
302 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
295 "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \ |
303 \ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \ |
296 \ : set_of_list evs; \ |
304 \ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \ |
297 \ Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \ |
305 \ --> (EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs)"; |
298 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
|
299 \ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs"; |
|
300 by (etac rev_mp 1); |
|
301 (*prepare induction over Crypt (pubK B) NB : parts H*) |
|
302 by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1); |
306 by (analz_induct_tac 1); |
303 by (analz_induct_tac 1); |
307 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
304 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
308 by (ALLGOALS Asm_simp_tac); |
305 (*NS1*) |
309 (*NS1*) |
306 by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); |
310 by (fast_tac (!claset addSEs partsEs |
|
311 addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); |
|
312 (*Fake*) |
307 (*Fake*) |
313 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
308 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
314 by (fast_tac (!claset addss (!simpset)) 1); |
309 by (fast_tac (!claset addss (!simpset)) 1); |
315 by (rtac (ccontr RS disjI2) 1); |
310 by (rtac (ccontr RS disjI2) 1); |
316 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); |
311 by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac) |
317 by (Fast_tac 1); |
312 THEN Fast_tac 1); |
318 by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
313 by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
319 addDs [impOfSubs analz_subset_parts] |
314 addDs [impOfSubs analz_subset_parts] |
320 addss (!simpset)) 1); |
315 addss (!simpset)) 1); |
321 (*NS3*) |
316 (*NS3*) |
322 by (Step_tac 1); |
317 by (Step_tac 1); |
323 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT1 (assume_tac 1)); |
318 by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac) |
324 by (Fast_tac 1); |
319 THEN Fast_tac 1); |
325 by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
320 by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
326 addDs [unique_NB]) 1); |
321 addDs [unique_NB]) 1); |
327 qed_spec_mp "NB_decrypt_imp_A_msg"; |
|
328 |
|
329 |
|
330 (*Corollary: if B receives message NS3 and the nonce NB agrees |
|
331 then A sent NB to somebody....*) |
|
332 goal thy |
|
333 "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \ |
|
334 \ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \ |
|
335 \ : set_of_list evs; \ |
|
336 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
|
337 \ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs"; |
|
338 by (fast_tac (!claset addSIs [NB_decrypt_imp_A_msg] |
|
339 addEs partsEs |
|
340 addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); |
|
341 qed "B_trusts_NS3"; |
322 qed "B_trusts_NS3"; |
342 |
323 |
343 |
324 |
344 (*Can we strengthen the secrecy theorem? NO*) |
325 (*Can we strengthen the secrecy theorem? NO*) |
345 goal thy |
326 goal thy |