93 |
93 |
94 |
94 |
95 (*Unicity for NS1: nonce NA identifies agents A and B*) |
95 (*Unicity for NS1: nonce NA identifies agents A and B*) |
96 goal thy |
96 goal thy |
97 "!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
97 "!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
98 \ ==> EX A' B'. ALL A B. \ |
98 \ ==> EX A' B'. ALL A B. \ |
99 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ |
99 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ |
100 \ A=A' & B=B'"; |
100 \ A=A' & B=B'"; |
101 by (etac rev_mp 1); |
101 by (etac rev_mp 1); |
102 by (parts_induct_tac 1); |
102 by (parts_induct_tac 1); |
103 by (ALLGOALS |
103 by (ALLGOALS |
104 (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]))); |
104 (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]))); |
105 (*NS1*) |
105 (*NS1*) |
106 by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); |
106 by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); |
107 (*Fake*) |
107 (*Fake*) |
108 by (step_tac (!claset addSIs [analz_insertI]) 1); |
108 by (Clarify_tac 1); |
109 by (ex_strip_tac 1); |
109 by (ex_strip_tac 1); |
110 by (Fake_parts_insert_tac 1); |
110 by (Fake_parts_insert_tac 1); |
111 val lemma = result(); |
111 val lemma = result(); |
112 |
112 |
113 goal thy |
113 goal thy |
189 |
189 |
190 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B |
190 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B |
191 [unicity of B makes Lowe's fix work] |
191 [unicity of B makes Lowe's fix work] |
192 [proof closely follows that for unique_NA] *) |
192 [proof closely follows that for unique_NA] *) |
193 goal thy |
193 goal thy |
194 "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \ |
194 "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \ |
195 \ ==> EX A' NA' B'. ALL A NA B. \ |
195 \ ==> EX A' NA' B'. ALL A NA B. \ |
196 \ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \ |
196 \ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \ |
197 \ --> A=A' & NA=NA' & B=B'"; |
197 \ --> A=A' & NA=NA' & B=B'"; |
198 by (etac rev_mp 1); |
198 by (etac rev_mp 1); |
199 by (parts_induct_tac 1); |
199 by (parts_induct_tac 1); |
200 by (ALLGOALS |
200 by (ALLGOALS |
201 (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]))); |
201 (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]))); |
202 (*NS2*) |
202 (*NS2*) |
203 by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); |
203 by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); |
204 (*Fake*) |
204 (*Fake*) |
205 by (step_tac (!claset addSIs [analz_insertI]) 1); |
205 by (Clarify_tac 1); |
206 by (ex_strip_tac 1); |
206 by (ex_strip_tac 1); |
207 by (Fake_parts_insert_tac 1); |
207 by (Fake_parts_insert_tac 1); |
208 val lemma = result(); |
208 val lemma = result(); |
209 |
209 |
210 goal thy |
210 goal thy |
211 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
211 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
212 \ : parts(spies evs); \ |
212 \ : parts(spies evs); \ |
213 \ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ |
213 \ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ |
214 \ : parts(spies evs); \ |
214 \ : parts(spies evs); \ |
215 \ Nonce NB ~: analz (spies evs); \ |
215 \ Nonce NB ~: analz (spies evs); \ |
216 \ evs : ns_public |] \ |
216 \ evs : ns_public |] \ |
217 \ ==> A=A' & NA=NA' & B=B'"; |
217 \ ==> A=A' & NA=NA' & B=B'"; |
218 by (prove_unique_tac lemma 1); |
218 by (prove_unique_tac lemma 1); |
219 qed "unique_NB"; |
219 qed "unique_NB"; |
220 |
220 |
227 \ ==> Nonce NB ~: analz (spies evs)"; |
227 \ ==> Nonce NB ~: analz (spies evs)"; |
228 by (etac rev_mp 1); |
228 by (etac rev_mp 1); |
229 by (analz_induct_tac 1); |
229 by (analz_induct_tac 1); |
230 (*NS3*) |
230 (*NS3*) |
231 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4); |
231 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4); |
|
232 (*NS2: by freshness and unicity of NB*) |
|
233 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] |
|
234 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] |
|
235 addEs partsEs |
|
236 addIs [impOfSubs analz_subset_parts]) 3); |
232 (*NS1*) |
237 (*NS1*) |
233 by (blast_tac (!claset addSEs spies_partsEs) 2); |
238 by (blast_tac (!claset addSEs spies_partsEs) 2); |
234 (*Fake*) |
239 (*Fake*) |
235 by (spy_analz_tac 1); |
240 by (spy_analz_tac 1); |
236 (*NS2*) |
|
237 by (Step_tac 1); |
|
238 by (blast_tac (!claset addSEs spies_partsEs) 3); |
|
239 by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj] |
|
240 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2); |
|
241 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); |
|
242 qed "Spy_not_see_NB"; |
241 qed "Spy_not_see_NB"; |
243 |
242 |
244 |
243 |
245 (*Authentication for B: if he receives message 3 and has used NB |
244 (*Authentication for B: if he receives message 3 and has used NB |
246 in message 2, then A has sent message 3.*) |
245 in message 2, then A has sent message 3.*) |
252 \ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
251 \ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
253 by (etac rev_mp 1); |
252 by (etac rev_mp 1); |
254 (*prepare induction over Crypt (pubK B) NB : parts H*) |
253 (*prepare induction over Crypt (pubK B) NB : parts H*) |
255 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
254 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
256 by (parts_induct_tac 1); |
255 by (parts_induct_tac 1); |
257 (*NS1*) |
256 by (ALLGOALS Clarify_tac); |
|
257 (*NS3: because NB determines A*) |
|
258 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, |
|
259 Spy_not_see_NB, unique_NB]) 3); |
|
260 (*NS1: by freshness*) |
258 by (blast_tac (!claset addSEs spies_partsEs) 2); |
261 by (blast_tac (!claset addSEs spies_partsEs) 2); |
259 (*Fake*) |
262 (*Fake*) |
260 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
263 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
261 addDs [Spy_not_see_NB, |
264 addDs [Spy_not_see_NB, |
262 impOfSubs analz_subset_parts]) 1); |
265 impOfSubs analz_subset_parts]) 1); |
263 (*NS3; not clear why blast_tac needs to be preceeded by Step_tac*) |
|
264 by (Step_tac 1); |
|
265 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, |
|
266 Spy_not_see_NB, unique_NB]) 1); |
|
267 qed "B_trusts_NS3"; |
266 qed "B_trusts_NS3"; |
268 |
267 |
269 |
268 |
270 (**** Overall guarantee for B*) |
269 (**** Overall guarantee for B*) |
271 |
270 |
285 by (etac rev_mp 1); |
284 by (etac rev_mp 1); |
286 (*prepare induction over Crypt (pubK B) {|NB|} : parts H*) |
285 (*prepare induction over Crypt (pubK B) {|NB|} : parts H*) |
287 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
286 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
288 by (etac ns_public.induct 1); |
287 by (etac ns_public.induct 1); |
289 by (ALLGOALS Asm_simp_tac); |
288 by (ALLGOALS Asm_simp_tac); |
290 (*Fake, NS2, NS3*) |
289 by (ALLGOALS Clarify_tac); |
|
290 (*NS3: because NB determines A*) |
|
291 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, |
|
292 Spy_not_see_NB, unique_NB]) 3); |
291 (*NS1*) |
293 (*NS1*) |
292 by (blast_tac (!claset addSEs spies_partsEs) 2); |
294 by (blast_tac (!claset addSEs spies_partsEs) 2); |
293 (*Fake*) |
295 (*Fake*) |
294 by (REPEAT_FIRST (resolve_tac [impI, conjI])); |
296 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
295 by (Blast_tac 1); |
297 addDs [Spy_not_see_NB, |
296 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); |
298 impOfSubs analz_subset_parts]) 1); |
297 by (blast_tac (!claset addSIs [disjI2] |
|
298 addDs [impOfSubs analz_subset_parts, |
|
299 impOfSubs Fake_parts_insert]) 1); |
|
300 (*NS3*) |
|
301 by (Step_tac 1); |
|
302 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); |
|
303 by (blast_tac (!claset addSDs [Says_imp_spies' RS parts.Inj] |
|
304 addDs [unique_NB]) 1); |
|
305 qed "B_trusts_protocol"; |
299 qed "B_trusts_protocol"; |
306 |
300 |