161 (*This lemma says that no false certificates exist. One might extend the |
161 (*This lemma says that no false certificates exist. One might extend the |
162 model to include bogus certificates for the agents, but there seems |
162 model to include bogus certificates for the agents, but there seems |
163 little point in doing so: the loss of their private keys is a worse |
163 little point in doing so: the loss of their private keys is a worse |
164 breach of security.*) |
164 breach of security.*) |
165 Goalw [certificate_def] |
165 Goalw [certificate_def] |
166 "[| certificate B KB : parts (spies evs); evs : tls |] \ |
166 "[| certificate B KB : parts (spies evs); evs : tls |] ==> pubK B = KB"; |
167 \ ==> pubK B = KB"; |
|
168 by (etac rev_mp 1); |
167 by (etac rev_mp 1); |
169 by (parts_induct_tac 1); |
168 by (parts_induct_tac 1); |
170 by (Fake_parts_insert_tac 1); |
169 by (Fake_parts_insert_tac 1); |
171 qed "certificate_valid"; |
170 qed "certificate_valid"; |
172 |
171 |
191 |
190 |
192 |
191 |
193 (*** Properties of items found in Notes ***) |
192 (*** Properties of items found in Notes ***) |
194 |
193 |
195 Goal "[| Notes A {|Agent B, X|} : set evs; evs : tls |] \ |
194 Goal "[| Notes A {|Agent B, X|} : set evs; evs : tls |] \ |
196 \ ==> Crypt (pubK B) X : parts (spies evs)"; |
195 \ ==> Crypt (pubK B) X : parts (spies evs)"; |
197 by (etac rev_mp 1); |
196 by (etac rev_mp 1); |
198 by (analz_induct_tac 1); |
197 by (analz_induct_tac 1); |
199 by (blast_tac (claset() addIs [parts_insertI]) 1); |
198 by (blast_tac (claset() addIs [parts_insertI]) 1); |
200 qed "Notes_Crypt_parts_spies"; |
199 qed "Notes_Crypt_parts_spies"; |
201 |
200 |
202 (*C may be either A or B*) |
201 (*C may be either A or B*) |
203 Goal "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \ |
202 Goal "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \ |
204 \ evs : tls \ |
203 \ evs : tls |] \ |
205 \ |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; |
204 \ ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; |
206 by (etac rev_mp 1); |
205 by (etac rev_mp 1); |
207 by (parts_induct_tac 1); |
206 by (parts_induct_tac 1); |
208 by (ALLGOALS Clarify_tac); |
207 by (ALLGOALS Clarify_tac); |
209 (*Fake*) |
208 (*Fake*) |
210 by (blast_tac (claset() addIs [parts_insertI]) 1); |
209 by (blast_tac (claset() addIs [parts_insertI]) 1); |
213 addSDs [Notes_Crypt_parts_spies]) 1)); |
212 addSDs [Notes_Crypt_parts_spies]) 1)); |
214 qed "Notes_master_imp_Crypt_PMS"; |
213 qed "Notes_master_imp_Crypt_PMS"; |
215 |
214 |
216 (*Compared with the theorem above, both premise and conclusion are stronger*) |
215 (*Compared with the theorem above, both premise and conclusion are stronger*) |
217 Goal "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\ |
216 Goal "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\ |
218 \ evs : tls \ |
217 \ evs : tls |] \ |
219 \ |] ==> Notes A {|Agent B, Nonce PMS|} : set evs"; |
218 \ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; |
220 by (etac rev_mp 1); |
219 by (etac rev_mp 1); |
221 by (parts_induct_tac 1); |
220 by (parts_induct_tac 1); |
222 (*ServerAccepts*) |
221 (*ServerAccepts*) |
223 by (Fast_tac 1); (*Blast_tac's very slow here*) |
222 by (Fast_tac 1); (*Blast_tac's very slow here*) |
224 qed "Notes_master_imp_Notes_PMS"; |
223 qed "Notes_master_imp_Notes_PMS"; |
228 |
227 |
229 (*B can check A's signature if he has received A's certificate.*) |
228 (*B can check A's signature if he has received A's certificate.*) |
230 Goal "[| X : parts (spies evs); \ |
229 Goal "[| X : parts (spies evs); \ |
231 \ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \ |
230 \ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \ |
232 \ evs : tls; A ~: bad |] \ |
231 \ evs : tls; A ~: bad |] \ |
233 \ ==> Says A B X : set evs"; |
232 \ ==> Says A B X : set evs"; |
234 by (etac rev_mp 1); |
233 by (etac rev_mp 1); |
235 by (hyp_subst_tac 1); |
234 by (hyp_subst_tac 1); |
236 by (parts_induct_tac 1); |
235 by (parts_induct_tac 1); |
237 by (Fake_parts_insert_tac 1); |
236 by (Fake_parts_insert_tac 1); |
238 val lemma = result(); |
237 val lemma = result(); |
240 (*Final version: B checks X using the distributed KA instead of priK A*) |
239 (*Final version: B checks X using the distributed KA instead of priK A*) |
241 Goal "[| X : parts (spies evs); \ |
240 Goal "[| X : parts (spies evs); \ |
242 \ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \ |
241 \ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \ |
243 \ certificate A KA : parts (spies evs); \ |
242 \ certificate A KA : parts (spies evs); \ |
244 \ evs : tls; A ~: bad |] \ |
243 \ evs : tls; A ~: bad |] \ |
245 \ ==> Says A B X : set evs"; |
244 \ ==> Says A B X : set evs"; |
246 by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); |
245 by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); |
247 qed "TrustCertVerify"; |
246 qed "TrustCertVerify"; |
248 |
247 |
249 |
248 |
250 (*If CertVerify is present then A has chosen PMS.*) |
249 (*If CertVerify is present then A has chosen PMS.*) |
273 by (Blast_tac 1); |
272 by (Blast_tac 1); |
274 qed "no_Notes_A_PRF"; |
273 qed "no_Notes_A_PRF"; |
275 Addsimps [no_Notes_A_PRF]; |
274 Addsimps [no_Notes_A_PRF]; |
276 |
275 |
277 |
276 |
278 Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); \ |
277 Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); evs : tls |] \ |
279 \ evs : tls |] \ |
278 \ ==> Nonce PMS : parts (spies evs)"; |
280 \ ==> Nonce PMS : parts (spies evs)"; |
279 by (etac rev_mp 1); |
281 by (etac rev_mp 1); |
280 by (parts_induct_tac 1); |
282 by (parts_induct_tac 1); |
281 by (Fake_parts_insert_tac 1); |
283 by (Fake_parts_insert_tac 1); |
282 (*SpyKeys*) |
|
283 by (blast_tac (claset() addDs [impOfSubs analz_subset_parts]) 1); |
284 (*Six others, all trivial or by freshness*) |
284 (*Six others, all trivial or by freshness*) |
285 by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies] |
285 by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies] |
286 addSEs spies_partsEs) 1)); |
286 addSEs spies_partsEs) 1)); |
287 qed "MS_imp_PMS"; |
287 qed "MS_imp_PMS"; |
288 AddSDs [MS_imp_PMS]; |
288 AddSDs [MS_imp_PMS]; |
319 we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which |
319 we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which |
320 determines B alone, and only if PMS is secret. |
320 determines B alone, and only if PMS is secret. |
321 **) |
321 **) |
322 |
322 |
323 (*In A's internal Note, PMS determines A and B.*) |
323 (*In A's internal Note, PMS determines A and B.*) |
324 Goal "evs : tls \ |
324 Goal "evs : tls ==> EX A' B'. ALL A B. \ |
325 \ ==> EX A' B'. ALL A B. \ |
325 \ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'"; |
326 \ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'"; |
|
327 by (parts_induct_tac 1); |
326 by (parts_induct_tac 1); |
328 by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); |
327 by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); |
329 (*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*) |
328 (*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*) |
330 by (expand_case_tac "PMS = ?y" 1 THEN |
329 by (expand_case_tac "PMS = ?y" 1 THEN |
331 blast_tac (claset() addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1); |
330 blast_tac (claset() addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1); |
342 |
341 |
343 (**** Secrecy Theorems ****) |
342 (**** Secrecy Theorems ****) |
344 |
343 |
345 (*Key compromise lemma needed to prove analz_image_keys. |
344 (*Key compromise lemma needed to prove analz_image_keys. |
346 No collection of keys can help the spy get new private keys.*) |
345 No collection of keys can help the spy get new private keys.*) |
347 Goal "evs : tls ==> \ |
346 Goal "evs : tls \ |
348 \ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ |
347 \ ==> ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ |
349 \ (priK B : KK | B : bad)"; |
348 \ (priK B : KK | B : bad)"; |
350 by (etac tls.induct 1); |
349 by (etac tls.induct 1); |
351 by (ALLGOALS |
350 by (ALLGOALS |
352 (asm_simp_tac (analz_image_keys_ss |
351 (asm_simp_tac (analz_image_keys_ss |
353 addsimps (certificate_def::keys_distinct)))); |
352 addsimps (certificate_def::keys_distinct)))); |
354 (*Fake*) |
353 (*Fake*) |
414 \ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))"; |
413 \ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))"; |
415 by (etac rev_mp 1); |
414 by (etac rev_mp 1); |
416 by (hyp_subst_tac 1); |
415 by (hyp_subst_tac 1); |
417 by (analz_induct_tac 1); |
416 by (analz_induct_tac 1); |
418 (*SpyKeys*) |
417 (*SpyKeys*) |
419 by (blast_tac (claset() addSEs spies_partsEs) 3); |
418 by (blast_tac (claset() addDs [impOfSubs analz_subset_parts]) 3); |
420 (*Fake*) |
419 (*Fake*) |
421 by (Fake_parts_insert_tac 2); |
420 by (Fake_parts_insert_tac 2); |
422 (** LEVEL 6 **) |
421 (** LEVEL 6 **) |
423 (*Oops*) |
422 (*Oops*) |
424 by (fast_tac (claset() addSEs [MPair_parts] |
423 by (fast_tac (claset() addSEs [MPair_parts] |
510 (*** Weakening the Oops conditions for leakage of clientK ***) |
509 (*** Weakening the Oops conditions for leakage of clientK ***) |
511 |
510 |
512 (*If A created PMS then nobody other than the Spy would send a message |
511 (*If A created PMS then nobody other than the Spy would send a message |
513 using a clientK generated from that PMS.*) |
512 using a clientK generated from that PMS.*) |
514 Goal "[| evs : tls; A' ~= Spy |] \ |
513 Goal "[| evs : tls; A' ~= Spy |] \ |
515 \ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
514 \ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
516 \ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ |
515 \ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ |
517 \ A = A'"; |
516 \ A = A'"; |
518 by (analz_induct_tac 1); (*8 seconds*) |
517 by (analz_induct_tac 1); (*8 seconds*) |
519 by (ALLGOALS Clarify_tac); |
518 by (ALLGOALS Clarify_tac); |
520 (*ClientFinished, ClientResume: by unicity of PMS*) |
519 (*ClientFinished, ClientResume: by unicity of PMS*) |
521 by (REPEAT |
520 by (REPEAT |
522 (blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS] |
521 (blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS] |
529 |
528 |
530 |
529 |
531 (*If A created PMS and has not leaked her clientK to the Spy, |
530 (*If A created PMS and has not leaked her clientK to the Spy, |
532 then nobody has.*) |
531 then nobody has.*) |
533 Goal "evs : tls \ |
532 Goal "evs : tls \ |
534 \ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \ |
533 \ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \ |
535 \ Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
534 \ Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
536 \ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) "; |
535 \ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs)"; |
537 by (etac tls.induct 1); |
536 by (etac tls.induct 1); |
538 (*This roundabout proof sequence avoids looping in simplification*) |
537 (*This roundabout proof sequence avoids looping in simplification*) |
539 by (ALLGOALS Simp_tac); |
538 by (ALLGOALS Simp_tac); |
540 by (ALLGOALS Clarify_tac); |
539 by (ALLGOALS Clarify_tac); |
541 by (Fake_parts_insert_tac 1); |
540 by (Fake_parts_insert_tac 1); |
552 (*** Weakening the Oops conditions for leakage of serverK ***) |
551 (*** Weakening the Oops conditions for leakage of serverK ***) |
553 |
552 |
554 (*If A created PMS for B, then nobody other than B or the Spy would |
553 (*If A created PMS for B, then nobody other than B or the Spy would |
555 send a message using a serverK generated from that PMS.*) |
554 send a message using a serverK generated from that PMS.*) |
556 Goal "[| evs : tls; A ~: bad; B ~: bad; B' ~= Spy |] \ |
555 Goal "[| evs : tls; A ~: bad; B ~: bad; B' ~= Spy |] \ |
557 \ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
556 \ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
558 \ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ |
557 \ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ |
559 \ B = B'"; |
558 \ B = B'"; |
560 by (analz_induct_tac 1); (*9 seconds*) |
559 by (analz_induct_tac 1); (*9 seconds*) |
561 by (ALLGOALS Clarify_tac); |
560 by (ALLGOALS Clarify_tac); |
562 (*ServerResume, ServerFinished: by unicity of PMS*) |
561 (*ServerResume, ServerFinished: by unicity of PMS*) |
563 by (REPEAT |
562 by (REPEAT |
564 (blast_tac (claset() addSEs [MPair_parts] |
563 (blast_tac (claset() addSEs [MPair_parts] |
688 assumed here; B cannot verify it. But if the message is |
687 assumed here; B cannot verify it. But if the message is |
689 ClientFinished, then B can then check the quoted values PA, PB, etc. |
688 ClientFinished, then B can then check the quoted values PA, PB, etc. |
690 ***) |
689 ***) |
691 |
690 |
692 Goal "[| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \ |
691 Goal "[| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \ |
693 \ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \ |
692 \ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \ |
694 \ Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
693 \ Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
695 \ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \ |
694 \ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \ |
696 \ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; |
695 \ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; |
697 by (hyp_subst_tac 1); |
696 by (hyp_subst_tac 1); |
698 by (analz_induct_tac 1); (*15 seconds*) |
697 by (analz_induct_tac 1); (*15 seconds*) |
699 by (ALLGOALS Clarify_tac); |
698 by (ALLGOALS Clarify_tac); |
700 (*ClientFinished, ClientResume: by unicity of PMS*) |
699 (*ClientFinished, ClientResume: by unicity of PMS*) |
701 by (REPEAT (blast_tac (claset() delrules [conjI] |
700 by (REPEAT (blast_tac (claset() delrules [conjI] |
714 Goal "[| M = PRF(PMS,NA,NB); \ |
713 Goal "[| M = PRF(PMS,NA,NB); \ |
715 \ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs); \ |
714 \ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs); \ |
716 \ Notes A {|Agent B, Nonce PMS|} : set evs; \ |
715 \ Notes A {|Agent B, Nonce PMS|} : set evs; \ |
717 \ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \ |
716 \ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \ |
718 \ evs : tls; A ~: bad; B ~: bad |] \ |
717 \ evs : tls; A ~: bad; B ~: bad |] \ |
719 \ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; |
718 \ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; |
720 by (blast_tac (claset() addIs [lemma] |
719 by (blast_tac (claset() addIs [lemma] |
721 addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1); |
720 addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1); |
722 qed "TrustClientMsg"; |
721 qed "TrustClientMsg"; |
723 |
722 |
724 |
723 |
731 \ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\ |
730 \ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\ |
732 \ Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \ |
731 \ Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \ |
733 \ certificate A KA : parts (spies evs); \ |
732 \ certificate A KA : parts (spies evs); \ |
734 \ Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\ |
733 \ Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\ |
735 \ : set evs; \ |
734 \ : set evs; \ |
736 \ evs : tls; A ~: bad; B ~: bad |] \ |
735 \ evs : tls; A ~: bad; B ~: bad |] \ |
737 \ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; |
736 \ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; |
738 by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify] |
737 by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify] |
739 addDs [Says_imp_spies RS parts.Inj]) 1); |
738 addDs [Says_imp_spies RS parts.Inj]) 1); |
740 qed "AuthClientFinished"; |
739 qed "AuthClientFinished"; |
741 |
740 |
742 (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) |
741 (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) |