First working version with Oops event for session keys
authorpaulson
Fri Sep 19 18:27:31 1997 +0200 (1997-09-19)
changeset 36864b484805b4c4
parent 3685 5b8c0c8f576e
child 3687 fb7d096d7884
First working version with Oops event for session keys
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Fri Sep 19 16:12:21 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Fri Sep 19 18:27:31 1997 +0200
     1.3 @@ -410,10 +410,15 @@
     1.4    Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
     1.5  
     1.6  goal thy 
     1.7 - "!!evs. [| Nonce M ~: analz (spies evs);  evs : tls |]   \
     1.8 -\        ==> Key (sessionK(b,NA,NB,M)) ~: parts (spies evs)";
     1.9 + "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
    1.10 +\           Nonce M ~: analz (spies evs);  evs : tls |]   \
    1.11 +\        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
    1.12 +by (etac rev_mp 1);
    1.13  by (etac rev_mp 1);
    1.14 -by (analz_induct_tac 1);
    1.15 +by (analz_induct_tac 1);	(*30 seconds??*)
    1.16 +(*Oops*)
    1.17 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 4);
    1.18 +by (Blast_tac 4);
    1.19  (*SpyKeys*)
    1.20  by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
    1.21  by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
    1.22 @@ -435,12 +440,15 @@
    1.23    They are NOT suitable as safe elim rules.*)
    1.24  
    1.25  goal thy 
    1.26 - "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
    1.27 -\  ==> Crypt (sessionK(b, Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (spies evs)";
    1.28 + "!!evs. [| ALL A. Says A Spy (Key (sessionK((Na, Nb, PRF(PMS,NA,NB)),b))) \
    1.29 +\                    ~: set evs; \
    1.30 +\           Nonce PMS ~: parts (spies evs);  evs : tls |]             \
    1.31 +\  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
    1.32 +by (etac rev_mp 1);
    1.33  by (etac rev_mp 1);
    1.34  by (analz_induct_tac 1);
    1.35  (*Fake*)
    1.36 -by (asm_simp_tac (!simpset addsimps [parts_insert_spies]) 2);
    1.37 +by (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]) 2);
    1.38  by (Fake_parts_insert_tac 2);
    1.39  (*Base, ClientFinished, ServerFinished, ClientResume: 
    1.40    trivial, e.g. by freshness*)
    1.41 @@ -449,7 +457,7 @@
    1.42  				Notes_master_imp_Crypt_PMS]
    1.43                          addSEs spies_partsEs) 1));
    1.44  qed "Crypt_sessionK_notin_parts";
    1.45 -				                               
    1.46 +
    1.47  Addsimps [Crypt_sessionK_notin_parts];
    1.48  AddEs [Crypt_sessionK_notin_parts RSN (2, rev_notE)];
    1.49  
    1.50 @@ -525,16 +533,18 @@
    1.51  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
    1.52  \            Nonce PMS ~: analz (spies evs)";
    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]) 9);
    1.56  (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
    1.57 -by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
    1.58 -(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
    1.59 +by (EVERY (map (fast_tac (!claset addss (!simpset))) [7,6]));
    1.60 +(*ServerHello, ClientCertKeyEx, ServerResume: mostly freshness reasoning*)
    1.61  by (REPEAT (blast_tac (!claset addSEs partsEs
    1.62  			       addDs  [Notes_Crypt_parts_spies,
    1.63  				       impOfSubs analz_subset_parts,
    1.64  				       Says_imp_spies RS analz.Inj]) 4));
    1.65  (*ClientHello*)
    1.66  by (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
    1.67 -                               addSEs spies_partsEs) 3);
    1.68 +                       addSEs spies_partsEs) 3);
    1.69  (*SpyKeys*)
    1.70  by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
    1.71  by (fast_tac (!claset addss (!simpset)) 2);
    1.72 @@ -561,6 +571,8 @@
    1.73  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
    1.74  \            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
    1.75  by (analz_induct_tac 1);   (*35 seconds*)
    1.76 +(*Oops*)
    1.77 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 9);
    1.78  (*ClientAccepts and ServerAccepts: because PMS was already visible*)
    1.79  by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
    1.80  				      Says_imp_spies RS analz.Inj,
    1.81 @@ -588,7 +600,8 @@
    1.82  
    1.83  (*The mention of her name (A) in X assures A that B knows who she is.*)
    1.84  goal thy
    1.85 - "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
    1.86 + "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
    1.87 +\           X = Crypt (serverK(Na,Nb,M))                  \
    1.88  \                 (Hash{|Nonce M, Number SID,             \
    1.89  \                        Nonce NA, Number XA, Agent A,    \
    1.90  \                        Nonce NB, Number XB, Agent B|}); \
    1.91 @@ -596,6 +609,7 @@
    1.92  \           evs : tls;  A ~: bad;  B ~: bad |]          \
    1.93  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
    1.94  \        X : parts (spies evs) --> Says B A X : set evs";
    1.95 +by (etac rev_mp 1);
    1.96  by (hyp_subst_tac 1);
    1.97  by (analz_induct_tac 1);	(*16 seconds*)
    1.98  (*ServerResume is trivial, but Blast_tac is too slow*)
    1.99 @@ -617,13 +631,15 @@
   1.100    that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   1.101    to bind A's identity with M, then we could replace A' by A below.*)
   1.102  goal thy
   1.103 - "!!evs. [| evs : tls;  A ~: bad;  B ~: bad;                 \
   1.104 + "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   1.105 +\           evs : tls;  A ~: bad;  B ~: bad;                 \
   1.106  \           M = PRF(PMS,NA,NB) |]            \
   1.107  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   1.108  \            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
   1.109  \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   1.110 +by (etac rev_mp 1);
   1.111  by (hyp_subst_tac 1);
   1.112 -by (analz_induct_tac 1);	(*12 seconds*)
   1.113 +by (analz_induct_tac 1);	(*20 seconds*)
   1.114  by (REPEAT_FIRST (rtac impI));
   1.115  (*ServerResume, by unicity of PMS*)
   1.116  by (blast_tac (!claset addSEs [MPair_parts]
   1.117 @@ -653,11 +669,21 @@
   1.118  ***)
   1.119  goal thy
   1.120   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
   1.121 -\  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.122 +\  ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
   1.123 +\      Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.124  \      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
   1.125  \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.126 -by (analz_induct_tac 1);	(*13 seconds*)
   1.127 +by (analz_induct_tac 1);	(*23 seconds*)
   1.128  by (REPEAT_FIRST (rtac impI));
   1.129 +(*ClientResume: by unicity of PMS*)
   1.130 +by (blast_tac (!claset delrules [conjI]
   1.131 +		       addSEs [MPair_parts]
   1.132 +                       addSDs [Notes_master_imp_Notes_PMS]
   1.133 +	 	       addDs  [good_Notes_unique_PMS]) 4);
   1.134 +(*ClientFinished: by unicity of PMS*)
   1.135 +by (blast_tac (!claset delrules [conjI]
   1.136 +		       addSEs [MPair_parts]
   1.137 +		       addDs  [good_Notes_unique_PMS]) 3);
   1.138  (*ClientCertKeyEx*)
   1.139  by (Blast_tac 2);
   1.140  (*Fake: the Spy doesn't have the critical session key!*)
   1.141 @@ -665,15 +691,6 @@
   1.142  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.143  				     not_parts_not_analz]) 2);
   1.144  by (Fake_parts_insert_tac 1);
   1.145 -(*ClientResume: by unicity of PMS*)
   1.146 -by (blast_tac (!claset delrules [conjI]
   1.147 -		       addSEs [MPair_parts]
   1.148 -                       addSDs [Notes_master_imp_Notes_PMS]
   1.149 -	 	       addDs  [good_Notes_unique_PMS]) 2);
   1.150 -(*ClientFinished: by unicity of PMS*)
   1.151 -by (blast_tac (!claset delrules [conjI]
   1.152 -		       addSEs [MPair_parts]
   1.153 -		       addDs  [good_Notes_unique_PMS]) 1);
   1.154  qed_spec_mp "TrustClientMsg";
   1.155  
   1.156  
   1.157 @@ -683,7 +700,8 @@
   1.158       values XA, XB, etc.  Even this one requires A to be uncompromised.
   1.159   ***)
   1.160  goal thy
   1.161 - "!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   1.162 + "!!evs. [| ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   1.163 +\           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   1.164  \           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
   1.165  \             : set evs;                                                  \
   1.166  \           Says A'' B (Crypt (priK A)                                    \
     2.1 --- a/src/HOL/Auth/TLS.thy	Fri Sep 19 16:12:21 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Fri Sep 19 18:27:31 1997 +0200
     2.3 @@ -48,7 +48,7 @@
     2.4    (*Client, server write keys generated uniformly by function sessionK
     2.5      to avoid duplicating their properties.
     2.6      Theyimplicitly include the MAC secrets.*)
     2.7 -  sessionK :: "bool*nat*nat*nat => key"
     2.8 +  sessionK :: "(nat*nat*nat)*bool => key"
     2.9  
    2.10    certificate      :: "[agent,key] => msg"
    2.11  
    2.12 @@ -60,8 +60,8 @@
    2.13      clientK, serverK :: "nat*nat*nat => key"
    2.14  
    2.15  translations
    2.16 -  "clientK (x)"	== "sessionK(True,x)"
    2.17 -  "serverK (x)"	== "sessionK(False,x)"
    2.18 +  "clientK (x)"	== "sessionK(x,True)"
    2.19 +  "serverK (x)"	== "sessionK(x,False)"
    2.20  
    2.21  rules
    2.22    inj_PRF       "inj PRF"	
    2.23 @@ -252,6 +252,12 @@
    2.24  			       Nonce NB, Number XB, Agent B|}))
    2.25                # evsCR  :  tls"
    2.26  
    2.27 -  (**Oops message??**)
    2.28 +    Oops 
    2.29 +         (*The most plausible compromise is of an old session key.  Losing
    2.30 +           the MASTER SECRET or PREMASTER SECRET is more serious but
    2.31 +           rather unlikely.*)
    2.32 +         "[| evso: tls;  A ~= Spy;  
    2.33 +	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
    2.34 +          ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
    2.35  
    2.36  end