src/HOL/Auth/TLS.ML
changeset 4472 cfa3bd184bc1
parent 4449 df30e75f670f
child 4477 b3e5857d8d99
equal deleted inserted replaced
4471:0abf9d3f4391 4472:cfa3bd184bc1
   163  "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
   163  "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
   164 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   164 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   165 qed "Spy_analz_priK";
   165 qed "Spy_analz_priK";
   166 Addsimps [Spy_analz_priK];
   166 Addsimps [Spy_analz_priK];
   167 
   167 
   168 goal thy  "!!A. [| Key (priK A) : parts (spies evs);  evs : tls |] ==> A:bad";
   168 AddSDs [Spy_see_priK RSN (2, rev_iffD1), 
   169 by (blast_tac (claset() addDs [Spy_see_priK]) 1);
   169 	Spy_analz_priK RSN (2, rev_iffD1)];
   170 qed "Spy_see_priK_D";
       
   171 
       
   172 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
       
   173 AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
       
   174 
   170 
   175 
   171 
   176 (*This lemma says that no false certificates exist.  One might extend the
   172 (*This lemma says that no false certificates exist.  One might extend the
   177   model to include bogus certificates for the agents, but there seems
   173   model to include bogus certificates for the agents, but there seems
   178   little point in doing so: the loss of their private keys is a worse
   174   little point in doing so: the loss of their private keys is a worse
   462 				 Notes_master_imp_Crypt_PMS]
   458 				 Notes_master_imp_Crypt_PMS]
   463                          addSEs spies_partsEs) 1));
   459                          addSEs spies_partsEs) 1));
   464 val lemma = result();
   460 val lemma = result();
   465 
   461 
   466 goal thy 
   462 goal thy 
   467  "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   463  "!!evs. [| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) : parts (spies evs); \
   468 \  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
   464 \           evs : tls |]             \
       
   465 \        ==> Nonce PMS : parts (spies evs)";
   469 by (blast_tac (claset() addDs [lemma]) 1);
   466 by (blast_tac (claset() addDs [lemma]) 1);
   470 qed "PMS_sessionK_not_spied";
   467 qed "PMS_sessionK_not_spied";
   471 bind_thm ("PMS_sessionK_spiedE", 
   468 
   472 	  PMS_sessionK_not_spied RSN (2,rev_notE));
   469 goal thy 
   473 
   470  "!!evs. [| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y  \
   474 goal thy 
   471 \             : parts (spies evs);  evs : tls |]             \
   475  "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   472 \        ==> Nonce PMS : parts (spies evs)";
   476 \  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
       
   477 by (blast_tac (claset() addDs [lemma]) 1);
   473 by (blast_tac (claset() addDs [lemma]) 1);
   478 qed "PMS_Crypt_sessionK_not_spied";
   474 qed "PMS_Crypt_sessionK_not_spied";
   479 bind_thm ("PMS_Crypt_sessionK_spiedE", 
       
   480 	  PMS_Crypt_sessionK_not_spied RSN (2,rev_notE));
       
   481 
   475 
   482 (*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
   476 (*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
   483   Converse doesn't hold; betraying M doesn't force the keys to be sent!
   477   Converse doesn't hold; betraying M doesn't force the keys to be sent!
   484   The strong Oops condition can be weakened later by unicity reasoning, 
   478   The strong Oops condition can be weakened later by unicity reasoning, 
   485 	with some effort.*)
   479 	with some effort.*)
   563 (*ClientFinished, ClientResume: by unicity of PMS*)
   557 (*ClientFinished, ClientResume: by unicity of PMS*)
   564 by (REPEAT 
   558 by (REPEAT 
   565     (blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS]
   559     (blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS]
   566      	 	         addIs  [Notes_unique_PMS RS conjunct1]) 2));
   560      	 	         addIs  [Notes_unique_PMS RS conjunct1]) 2));
   567 (*ClientKeyExch*)
   561 (*ClientKeyExch*)
   568 by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]
   562 by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied,
   569 	                addSDs [Says_imp_spies RS parts.Inj]) 1);
   563 				Says_imp_spies RS parts.Inj]) 1);
   570 bind_thm ("Says_clientK_unique",
   564 bind_thm ("Says_clientK_unique",
   571 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   565 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   572 
   566 
   573 
   567 
   574 (*If A created PMS and has not leaked her clientK to the Spy, 
   568 (*If A created PMS and has not leaked her clientK to the Spy, 
   585 by (Fake_parts_insert_tac 1);
   579 by (Fake_parts_insert_tac 1);
   586 by (ALLGOALS Asm_simp_tac);
   580 by (ALLGOALS Asm_simp_tac);
   587 (*Oops*)
   581 (*Oops*)
   588 by (blast_tac (claset() addIs [Says_clientK_unique]) 2);
   582 by (blast_tac (claset() addIs [Says_clientK_unique]) 2);
   589 (*ClientKeyExch*)
   583 (*ClientKeyExch*)
   590 by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
   584 by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]
       
   585 			addSEs spies_partsEs) 1);
   591 qed_spec_mp "clientK_Oops_ALL";
   586 qed_spec_mp "clientK_Oops_ALL";
   592 
   587 
   593 
   588 
   594 
   589 
   595 (*** Weakening the Oops conditions for leakage of serverK ***)
   590 (*** Weakening the Oops conditions for leakage of serverK ***)
   610 				 Says_imp_spies RS parts.Inj]
   605 				 Says_imp_spies RS parts.Inj]
   611 			 addDs  [Spy_not_see_PMS, 
   606 			 addDs  [Spy_not_see_PMS, 
   612 				 Notes_Crypt_parts_spies,
   607 				 Notes_Crypt_parts_spies,
   613 				 Crypt_unique_PMS]) 2));
   608 				 Crypt_unique_PMS]) 2));
   614 (*ClientKeyExch*)
   609 (*ClientKeyExch*)
   615 by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]
   610 by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied,
   616 	                addSDs [Says_imp_spies RS parts.Inj]) 1);
   611 				Says_imp_spies RS parts.Inj]) 1);
   617 bind_thm ("Says_serverK_unique",
   612 bind_thm ("Says_serverK_unique",
   618 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   613 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   619 
   614 
   620 (*If A created PMS for B, and B has not leaked his serverK to the Spy, 
   615 (*If A created PMS for B, and B has not leaked his serverK to the Spy, 
   621   then nobody has.*)
   616   then nobody has.*)
   631 by (Fake_parts_insert_tac 1);
   626 by (Fake_parts_insert_tac 1);
   632 by (ALLGOALS Asm_simp_tac);
   627 by (ALLGOALS Asm_simp_tac);
   633 (*Oops*)
   628 (*Oops*)
   634 by (blast_tac (claset() addIs [Says_serverK_unique]) 2);
   629 by (blast_tac (claset() addIs [Says_serverK_unique]) 2);
   635 (*ClientKeyExch*)
   630 (*ClientKeyExch*)
   636 by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
   631 by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]
       
   632 			addSEs spies_partsEs) 1);
   637 qed_spec_mp "serverK_Oops_ALL";
   633 qed_spec_mp "serverK_Oops_ALL";
   638 
   634 
   639 
   635 
   640 
   636 
   641 (*** Protocol goals: if A receives ServerFinished, then B is present 
   637 (*** Protocol goals: if A receives ServerFinished, then B is present 
   657 by (hyp_subst_tac 1);
   653 by (hyp_subst_tac 1);
   658 by (analz_induct_tac 1);        (*26 seconds*)
   654 by (analz_induct_tac 1);        (*26 seconds*)
   659 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   655 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   660 (*proves ServerResume*)
   656 (*proves ServerResume*)
   661 by (ALLGOALS Clarify_tac);
   657 by (ALLGOALS Clarify_tac);
   662 (*ClientKeyExch: blast_tac gives PROOF FAILED*)
   658 (*ClientKeyExch*)
   663 by (fast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   659 by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2);
   664 (*Fake: the Spy doesn't have the critical session key!*)
   660 (*Fake: the Spy doesn't have the critical session key!*)
   665 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   661 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   666 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   662 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   667 				      not_parts_not_analz]) 2);
   663 				      not_parts_not_analz]) 2);
   668 by (Fake_parts_insert_tac 1);
   664 by (Fake_parts_insert_tac 1);
   708 				 Says_imp_spies RS parts.Inj]
   704 				 Says_imp_spies RS parts.Inj]
   709 			 addDs  [Spy_not_see_PMS, 
   705 			 addDs  [Spy_not_see_PMS, 
   710 				 Notes_Crypt_parts_spies,
   706 				 Notes_Crypt_parts_spies,
   711 				 Crypt_unique_PMS]) 3));
   707 				 Crypt_unique_PMS]) 3));
   712 (*ClientKeyExch*)
   708 (*ClientKeyExch*)
   713 by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   709 by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2);
   714 (*Fake: the Spy doesn't have the critical session key!*)
   710 (*Fake: the Spy doesn't have the critical session key!*)
   715 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   711 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   716 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   712 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   717 				      not_parts_not_analz]) 2);
   713 				      not_parts_not_analz]) 2);
   718 by (Fake_parts_insert_tac 1);
   714 by (Fake_parts_insert_tac 1);
   749 by (ALLGOALS Clarify_tac);
   745 by (ALLGOALS Clarify_tac);
   750 (*ClientFinished, ClientResume: by unicity of PMS*)
   746 (*ClientFinished, ClientResume: by unicity of PMS*)
   751 by (REPEAT (blast_tac (claset() delrules [conjI]
   747 by (REPEAT (blast_tac (claset() delrules [conjI]
   752 		                addSDs [Notes_master_imp_Notes_PMS]
   748 		                addSDs [Notes_master_imp_Notes_PMS]
   753 	 	                addDs  [Notes_unique_PMS]) 3));
   749 	 	                addDs  [Notes_unique_PMS]) 3));
   754 (*ClientKeyExch: blast_tac gives PROOF FAILED*)
   750 (*ClientKeyExch*)
   755 by (fast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   751 by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2);
   756 (*Fake: the Spy doesn't have the critical session key!*)
   752 (*Fake: the Spy doesn't have the critical session key!*)
   757 by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   753 by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   758 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   754 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   759 				      not_parts_not_analz]) 2);
   755 				      not_parts_not_analz]) 2);
   760 by (Fake_parts_insert_tac 1);
   756 by (Fake_parts_insert_tac 1);