Simplified SpyKeys to use sessionK instead of clientK and serverK
authorpaulson
Mon Sep 22 13:17:29 1997 +0200 (1997-09-22)
changeset 3687fb7d096d7884
parent 3686 4b484805b4c4
child 3688 530e4ebd2564
Simplified SpyKeys to use sessionK instead of clientK and serverK
Proved and used analz_insert_key, shortening scripts
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Fri Sep 19 18:27:31 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Mon Sep 22 13:17:29 1997 +0200
     1.3 @@ -327,11 +327,12 @@
     1.4  qed "UseCertVerify";
     1.5  
     1.6  
     1.7 -(*No collection of keys can help the spy get new private keys*)
     1.8 +(*Key compromise lemma needed to prove analz_image_keys.
     1.9 +  No collection of keys can help the spy get new private keys.*)
    1.10  goal thy  
    1.11   "!!evs. evs : tls ==>                                    \
    1.12  \  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) =  \
    1.13 -\            (priK B : KK | B : bad)";
    1.14 +\          (priK B : KK | B : bad)";
    1.15  by (etac tls.induct 1);
    1.16  by (ALLGOALS
    1.17      (asm_simp_tac (analz_image_keys_ss
    1.18 @@ -355,7 +356,16 @@
    1.19  by (Blast_tac 1);
    1.20  val range_sessionkeys_not_priK = result();
    1.21  
    1.22 -(*Knowing some session keys is no help in getting new nonces*)
    1.23 +(** It is a mystery to me why the following formulation is actually slower
    1.24 +    in simplification:
    1.25 +
    1.26 +\    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
    1.27 +\           (Nonce N : analz (spies evs))";
    1.28 +
    1.29 +More so as it can take advantage of unconditional rewrites such as 
    1.30 +     priK B ~: sessionK``Z
    1.31 +**)
    1.32 +
    1.33  goal thy  
    1.34   "!!evs. evs : tls ==>                                 \
    1.35  \    ALL KK. KK <= range sessionK -->           \
    1.36 @@ -378,6 +388,14 @@
    1.37  by (Blast_tac 1);
    1.38  qed_spec_mp "analz_image_keys";
    1.39  
    1.40 +(*Knowing some session keys is no help in getting new nonces*)
    1.41 +goal thy
    1.42 + "!!evs. evs : tls ==>          \
    1.43 +\        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
    1.44 +\        (Nonce N : analz (spies evs))";
    1.45 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
    1.46 +qed "analz_insert_key";
    1.47 +Addsimps [analz_insert_key];
    1.48  
    1.49  goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
    1.50  by (parts_induct_tac 1);
    1.51 @@ -417,10 +435,8 @@
    1.52  by (etac rev_mp 1);
    1.53  by (analz_induct_tac 1);	(*30 seconds??*)
    1.54  (*Oops*)
    1.55 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 4);
    1.56  by (Blast_tac 4);
    1.57  (*SpyKeys*)
    1.58 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
    1.59  by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
    1.60  (*Fake*) 
    1.61  by (spy_analz_tac 2);
    1.62 @@ -533,20 +549,15 @@
    1.63  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
    1.64  \            Nonce PMS ~: analz (spies evs)";
    1.65  by (analz_induct_tac 1);   (*30 seconds??*)
    1.66 -(*oops*)
    1.67 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 9);
    1.68  (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
    1.69  by (EVERY (map (fast_tac (!claset addss (!simpset))) [7,6]));
    1.70 -(*ServerHello, ClientCertKeyEx, ServerResume: mostly freshness reasoning*)
    1.71 +(*ClientHello, ServerHello, ClientCertKeyEx, ServerResume: 
    1.72 +  mostly freshness reasoning*)
    1.73  by (REPEAT (blast_tac (!claset addSEs partsEs
    1.74  			       addDs  [Notes_Crypt_parts_spies,
    1.75  				       impOfSubs analz_subset_parts,
    1.76 -				       Says_imp_spies RS analz.Inj]) 4));
    1.77 -(*ClientHello*)
    1.78 -by (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
    1.79 -                       addSEs spies_partsEs) 3);
    1.80 +				       Says_imp_spies RS analz.Inj]) 3));
    1.81  (*SpyKeys*)
    1.82 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
    1.83  by (fast_tac (!claset addss (!simpset)) 2);
    1.84  (*Fake*)
    1.85  by (spy_analz_tac 1);
    1.86 @@ -571,8 +582,6 @@
    1.87  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
    1.88  \            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
    1.89  by (analz_induct_tac 1);   (*35 seconds*)
    1.90 -(*Oops*)
    1.91 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 9);
    1.92  (*ClientAccepts and ServerAccepts: because PMS was already visible*)
    1.93  by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
    1.94  				      Says_imp_spies RS analz.Inj,
    1.95 @@ -580,7 +589,6 @@
    1.96  (*ClientHello*)
    1.97  by (Blast_tac 3);
    1.98  (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
    1.99 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   1.100  by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
   1.101  			       Says_imp_spies RS analz.Inj]) 2);
   1.102  (*Fake*)
   1.103 @@ -712,3 +720,5 @@
   1.104  by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
   1.105                         addDs  [Says_imp_spies RS parts.Inj]) 1);
   1.106  qed "AuthClientFinished";
   1.107 +
   1.108 +(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
     2.1 --- a/src/HOL/Auth/TLS.thy	Fri Sep 19 18:27:31 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Mon Sep 22 13:17:29 1997 +0200
     2.3 @@ -66,7 +66,8 @@
     2.4  rules
     2.5    inj_PRF       "inj PRF"	
     2.6  
     2.7 -  (*sessionK is collision-free and makes symmetric keys*)
     2.8 +  (*sessionK is collision-free and makes symmetric keys.  Also, no clientK
     2.9 +    clashes with any serverK.*)
    2.10    inj_sessionK  "inj sessionK"	
    2.11  
    2.12    isSym_sessionK "isSymKey (sessionK x)"
    2.13 @@ -75,9 +76,6 @@
    2.14    inj_serverK   "inj serverK"	
    2.15    isSym_serverK "isSymKey (serverK x)"
    2.16  
    2.17 -  (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
    2.18 -  clientK_range "range clientK <= Compl (range serverK)"
    2.19 -
    2.20  
    2.21  consts    tls :: event list set
    2.22  inductive tls
    2.23 @@ -90,12 +88,11 @@
    2.24               X: synth (analz (spies evs)) |]
    2.25            ==> Says Spy B X # evs : tls"
    2.26  
    2.27 -    SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
    2.28 +    SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
    2.29           "[| evsSK: tls;
    2.30  	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
    2.31            ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
    2.32 -			    Key (clientK(NA,NB,M)),
    2.33 -			    Key (serverK(NA,NB,M)) |} # evsSK : tls"
    2.34 +			    Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
    2.35  
    2.36      ClientHello
    2.37  	 (*(7.4.1.2)
    2.38 @@ -196,7 +193,8 @@
    2.39      ClientAccepts
    2.40  	(*Having transmitted ClientFinished and received an identical
    2.41            message encrypted with serverK, the client stores the parameters
    2.42 -          needed to resume this session.*)
    2.43 +          needed to resume this session.  The "Notes A ..." premise is
    2.44 +          used to prove Notes_master_imp_Crypt_PMS.*)
    2.45           "[| evsCA: tls;
    2.46  	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
    2.47  	     M = PRF(PMS,NA,NB);  
    2.48 @@ -211,7 +209,8 @@
    2.49      ServerAccepts
    2.50  	(*Having transmitted ServerFinished and received an identical
    2.51            message encrypted with clientK, the server stores the parameters
    2.52 -          needed to resume this session.*)
    2.53 +          needed to resume this session.  The "Says A'' B ..." premise is
    2.54 +          used to prove Notes_master_imp_Crypt_PMS.*)
    2.55           "[| evsSA: tls;
    2.56               Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
    2.57  	       : set evsSA;