src/HOL/Auth/TLS.ML
changeset 3685 5b8c0c8f576e
parent 3683 aafe719dff14
child 3686 4b484805b4c4
     1.1 --- a/src/HOL/Auth/TLS.ML	Fri Sep 19 16:11:24 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Fri Sep 19 16:12:21 1997 +0200
     1.3 @@ -7,10 +7,10 @@
     1.4  * M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
     1.5       parties (though A is not necessarily authenticated).
     1.6  
     1.7 -* B upon receiving CERTIFICATE VERIFY knows that A is present (But this
     1.8 +* B upon receiving CertVerify knows that A is present (But this
     1.9      message is optional!)
    1.10  
    1.11 -* A upon receiving SERVER FINISHED knows that B is present
    1.12 +* A upon receiving ServerFinished knows that B is present
    1.13  
    1.14  * Each party who has received a FINISHED message can trust that the other
    1.15    party agrees on all message components, including XA and XB (thus foiling
    1.16 @@ -86,34 +86,26 @@
    1.17  **)
    1.18  
    1.19  
    1.20 -
    1.21 -(*Possibility property ending with ServerFinished.*)
    1.22 +(*Possibility property ending with ClientAccepts.*)
    1.23  goal thy 
    1.24   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.25 -\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
    1.26 -\  Says B A (Crypt (serverK(NA,NB,M))                       \
    1.27 -\            (Hash{|Nonce M, Number SID,             \
    1.28 -\                   Nonce NA, Number XA, Agent A,      \
    1.29 -\                   Nonce NB, Number XB, Agent B|})) \
    1.30 -\    : set evs";
    1.31 +\           A ~= B |] ==> EX SID M. EX evs: tls.    \
    1.32 +\  Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    1.33  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.34  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.35 -	  RS tls.ServerFinished) 2);
    1.36 +	RS tls.ClientFinished RS tls.ServerFinished RS tls.ClientAccepts) 2);
    1.37  by possibility_tac;
    1.38  by (REPEAT (Blast_tac 1));
    1.39  result();
    1.40  
    1.41 -(*And one for ClientFinished.  Either FINISHED message may come first.*)
    1.42 +(*And one for ServerAccepts.  Either FINISHED message may come first.*)
    1.43  goal thy 
    1.44   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.45  \           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
    1.46 -\  Says A B (Crypt (clientK(NA,NB,M))                           \
    1.47 -\            (Hash{|Nonce M, Number SID,             \
    1.48 -\                   Nonce NA, Number XA, Agent A,      \
    1.49 -\                   Nonce NB, Number XB, Agent B|})) : set evs";
    1.50 +\  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    1.51  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.52  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.53 -	  RS tls.ClientFinished) 2);
    1.54 +	  RS tls.ServerFinished RS tls.ClientFinished RS tls.ServerAccepts) 2);
    1.55  by possibility_tac;
    1.56  by (REPEAT (Blast_tac 1));
    1.57  result();
    1.58 @@ -131,6 +123,24 @@
    1.59  by (REPEAT (Blast_tac 1));
    1.60  result();
    1.61  
    1.62 +(*Another one, for session resumption (both ServerResume and ClientResume) *)
    1.63 +goal thy 
    1.64 + "!!A B. [| evs0 : tls;     \
    1.65 +\           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
    1.66 +\           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
    1.67 +\           ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.68 +\           A ~= B |] ==> EX NA XA NB XB. EX evs: tls.    \
    1.69 +\  Says A B (Crypt (clientK(NA,NB,M))                           \
    1.70 +\            (Hash{|Nonce M, Number SID,             \
    1.71 +\                   Nonce NA, Number XA, Agent A,      \
    1.72 +\                   Nonce NB, Number XB, Agent B|})) : set evs";
    1.73 +by (REPEAT (resolve_tac [exI,bexI] 1));
    1.74 +by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2);
    1.75 +by possibility_tac;
    1.76 +by (REPEAT (Blast_tac 1));
    1.77 +result();
    1.78 +
    1.79 +
    1.80  
    1.81  (**** Inductive proofs about tls ****)
    1.82  
    1.83 @@ -216,24 +226,7 @@
    1.84                          setloop split_tac [expand_if]));
    1.85  
    1.86  
    1.87 -(*** Hashing of nonces ***)
    1.88 -
    1.89 -(*Every Nonce that's hashed is already in past traffic.  
    1.90 -  This event occurs in CERTIFICATE VERIFY*)
    1.91 -goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (spies evs);  \
    1.92 -\                   NB ~: range PRF;  evs : tls |]  \
    1.93 -\                ==> Nonce NB : parts (spies evs)";
    1.94 -by (etac rev_mp 1);
    1.95 -by (etac rev_mp 1);
    1.96 -by (parts_induct_tac 1);
    1.97 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
    1.98 -by (Fake_parts_insert_tac 1);
    1.99 -(*FINISHED messages are trivial because M : range PRF*)
   1.100 -by (REPEAT (Blast_tac 2));
   1.101 -(*CERTIFICATE VERIFY is the only interesting case*)
   1.102 -by (blast_tac (!claset addSEs spies_partsEs) 1);
   1.103 -qed "Hash_Nonce_CV";
   1.104 -
   1.105 +(*** Notes are made under controlled circumstances ***)
   1.106  
   1.107  goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   1.108  \                ==> Crypt (pubK B) X : parts (spies evs)";
   1.109 @@ -242,8 +235,65 @@
   1.110  by (blast_tac (!claset addIs [parts_insertI]) 1);
   1.111  qed "Notes_Crypt_parts_spies";
   1.112  
   1.113 +(*C might be either A or B*)
   1.114 +goal thy
   1.115 +    "!!evs. [| Notes C {|Number SID, Agent A, Agent B, Nonce M|} : set evs;  \
   1.116 +\              evs : tls     \
   1.117 +\           |] ==> M : range PRF";
   1.118 +by (etac rev_mp 1);
   1.119 +by (parts_induct_tac 1);
   1.120 +by (Auto_tac());
   1.121 +qed "Notes_master_range_PRF";
   1.122  
   1.123 -(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
   1.124 +(*C might be either A or B*)
   1.125 +goal thy
   1.126 + "!!evs. [| Notes C {|Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \
   1.127 +\             : set evs;     evs : tls     \
   1.128 +\        |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
   1.129 +by (etac rev_mp 1);
   1.130 +by (parts_induct_tac 1);
   1.131 +(*Fake*)
   1.132 +by (blast_tac (!claset addIs [parts_insertI]) 1);
   1.133 +(*Client, Server Accept*)
   1.134 +by (Step_tac 1);
   1.135 +by (REPEAT (blast_tac (!claset addSEs spies_partsEs
   1.136 +                               addSDs [Notes_Crypt_parts_spies]) 1));
   1.137 +qed "Notes_master_imp_Crypt_PMS";
   1.138 +
   1.139 +(*Compared with the theorem above, both premise and conclusion are stronger*)
   1.140 +goal thy
   1.141 + "!!evs. [| Notes A {|Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \
   1.142 +\             : set evs;     evs : tls     \
   1.143 +\        |] ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   1.144 +by (etac rev_mp 1);
   1.145 +by (parts_induct_tac 1);
   1.146 +(*ServerAccepts*)
   1.147 +by (Fast_tac 1);	(*Blast_tac's very slow here*)
   1.148 +qed "Notes_master_imp_Notes_PMS";
   1.149 +
   1.150 +
   1.151 +(*Every Nonce that's hashed is already in past traffic; this event
   1.152 +  occurs in CertVerify.  The condition NB ~: range PRF excludes the 
   1.153 +  MASTER SECRET from consideration; it is created using PRF.*)
   1.154 +goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (spies evs);  \
   1.155 +\                   NB ~: range PRF;  evs : tls |]  \
   1.156 +\                ==> Nonce NB : parts (spies evs)";
   1.157 +by (etac rev_mp 1);
   1.158 +by (etac rev_mp 1);
   1.159 +by (parts_induct_tac 1);
   1.160 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
   1.161 +(*Server/Client Resume: wrong sort of nonce!*)
   1.162 +by (REPEAT (blast_tac (!claset addSDs [Notes_master_range_PRF]) 5));
   1.163 +(*FINISHED messages are trivial because M : range PRF*)
   1.164 +by (REPEAT (Blast_tac 3));
   1.165 +(*CertVerify is the only interesting case*)
   1.166 +by (blast_tac (!claset addSEs spies_partsEs) 2);
   1.167 +by (Fake_parts_insert_tac 1);
   1.168 +qed "Hash_Nonce_CV";
   1.169 +
   1.170 +
   1.171 +
   1.172 +(*** Protocol goal: if B receives CertVerify, then A sent it ***)
   1.173  
   1.174  (*B can check A's signature if he has received A's certificate.
   1.175    Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
   1.176 @@ -265,7 +315,7 @@
   1.177  qed_spec_mp "TrustCertVerify";
   1.178  
   1.179  
   1.180 -(*If CERTIFICATE VERIFY is present then A has chosen PMS.*)
   1.181 +(*If CertVerify is present then A has chosen PMS.*)
   1.182  goal thy
   1.183   "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
   1.184  \             : parts (spies evs);                                \
   1.185 @@ -392,12 +442,14 @@
   1.186  (*Fake*)
   1.187  by (asm_simp_tac (!simpset addsimps [parts_insert_spies]) 2);
   1.188  by (Fake_parts_insert_tac 2);
   1.189 -(*Base, ClientFinished, ServerFinished: trivial, e.g. by freshness*)
   1.190 +(*Base, ClientFinished, ServerFinished, ClientResume: 
   1.191 +  trivial, e.g. by freshness*)
   1.192  by (REPEAT 
   1.193 -    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
   1.194 +    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
   1.195 +				Notes_master_imp_Crypt_PMS]
   1.196                          addSEs spies_partsEs) 1));
   1.197  qed "Crypt_sessionK_notin_parts";
   1.198 -
   1.199 +				                               
   1.200  Addsimps [Crypt_sessionK_notin_parts];
   1.201  AddEs [Crypt_sessionK_notin_parts RSN (2, rev_notE)];
   1.202  
   1.203 @@ -437,6 +489,11 @@
   1.204  by (prove_unique_tac lemma 1);
   1.205  qed "unique_PMS";
   1.206  
   1.207 +(** It is frustrating that we need two versions of the unicity results.
   1.208 +    But Notes A {|Agent B, Nonce PMS|} determines both A and B, while
   1.209 +    Crypt(pubK B) (Nonce PMS) determines only B, and sometimes only
   1.210 +    this weaker item is available.
   1.211 +**)
   1.212  
   1.213  (*In A's internal Note, PMS determines A and B.*)
   1.214  goal thy 
   1.215 @@ -467,7 +524,7 @@
   1.216   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   1.217  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   1.218  \            Nonce PMS ~: analz (spies evs)";
   1.219 -by (analz_induct_tac 1);   (*30 seconds???*)
   1.220 +by (analz_induct_tac 1);   (*30 seconds??*)
   1.221  (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
   1.222  by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
   1.223  (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.224 @@ -486,7 +543,15 @@
   1.225  bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   1.226  
   1.227  
   1.228 -
   1.229 +(*Another way of showing unicity*)
   1.230 +goal thy 
   1.231 + "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   1.232 +\           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   1.233 +\           A ~: bad;  B ~: bad;                         \
   1.234 +\           evs : tls |]                                 \
   1.235 +\        ==> A=A' & B=B'";
   1.236 +by (REPEAT (ares_tac [Notes_unique_PMS, Spy_not_see_PMS] 1));
   1.237 +qed "good_Notes_unique_PMS";
   1.238  
   1.239  
   1.240  (*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
   1.241 @@ -516,12 +581,12 @@
   1.242  bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   1.243  
   1.244  
   1.245 -(*** Protocol goals: if A receives SERVER FINISHED, then B is present 
   1.246 +(*** Protocol goals: if A receives ServerFinished, then B is present 
   1.247       and has used the quoted values XA, XB, etc.  Note that it is up to A
   1.248       to compare XA with what she originally sent.
   1.249  ***)
   1.250  
   1.251 -(*The mention of her name (A) in X assumes A that B knows who she is.*)
   1.252 +(*The mention of her name (A) in X assures A that B knows who she is.*)
   1.253  goal thy
   1.254   "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   1.255  \                 (Hash{|Nonce M, Number SID,             \
   1.256 @@ -533,6 +598,8 @@
   1.257  \        X : parts (spies evs) --> Says B A X : set evs";
   1.258  by (hyp_subst_tac 1);
   1.259  by (analz_induct_tac 1);	(*16 seconds*)
   1.260 +(*ServerResume is trivial, but Blast_tac is too slow*)
   1.261 +by (Best_tac 3);
   1.262  (*ClientCertKeyEx*)
   1.263  by (Blast_tac 2);
   1.264  (*Fake: the Spy doesn't have the critical session key!*)
   1.265 @@ -544,8 +611,8 @@
   1.266  qed_spec_mp "TrustServerFinished";
   1.267  
   1.268  
   1.269 -(*This version refers not to SERVER FINISHED but to any message from B.
   1.270 -  We don't assume B has received CERTIFICATE VERIFY, and an intruder could
   1.271 +(*This version refers not to ServerFinished but to any message from B.
   1.272 +  We don't assume B has received CertVerify, and an intruder could
   1.273    have changed A's identity in all other messages, so we can't be sure
   1.274    that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   1.275    to bind A's identity with M, then we could replace A' by A below.*)
   1.276 @@ -558,6 +625,17 @@
   1.277  by (hyp_subst_tac 1);
   1.278  by (analz_induct_tac 1);	(*12 seconds*)
   1.279  by (REPEAT_FIRST (rtac impI));
   1.280 +(*ServerResume, by unicity of PMS*)
   1.281 +by (blast_tac (!claset addSEs [MPair_parts]
   1.282 +		       addDs  [Spy_not_see_PMS, 
   1.283 +			       Notes_Crypt_parts_spies,
   1.284 +			       Notes_master_imp_Crypt_PMS, unique_PMS]) 4);
   1.285 +(*ServerFinished, by unicity of PMS (10 seconds)*)
   1.286 +by (blast_tac (!claset addSEs [MPair_parts]
   1.287 +		       addDs  [Spy_not_see_PMS, 
   1.288 +			       Notes_Crypt_parts_spies,
   1.289 +			       Says_imp_spies RS parts.Inj,
   1.290 +			       unique_PMS]) 3);
   1.291  (*ClientCertKeyEx*)
   1.292  by (Blast_tac 2);
   1.293  (*Fake: the Spy doesn't have the critical session key!*)
   1.294 @@ -565,24 +643,13 @@
   1.295  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.296  				     not_parts_not_analz]) 2);
   1.297  by (Fake_parts_insert_tac 1);
   1.298 -(*ServerFinished.  If the message is old then apply induction hypothesis...*)
   1.299 -by (rtac conjI 1 THEN Blast_tac 2);
   1.300 -(*...otherwise delete induction hyp and use unicity of PMS.*)
   1.301 -by (thin_tac "?PP-->?QQ" 1);
   1.302 -by (Step_tac 1);
   1.303 -by (subgoal_tac "Nonce PMS ~: analz(spies evsSF)" 1);
   1.304 -by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
   1.305 -by (blast_tac (!claset addSEs [MPair_parts]
   1.306 -		       addDs  [Notes_Crypt_parts_spies,
   1.307 -			       Says_imp_spies RS parts.Inj,
   1.308 -			       unique_PMS]) 1);
   1.309  qed_spec_mp "TrustServerMsg";
   1.310  
   1.311  
   1.312  (*** Protocol goal: if B receives any message encrypted with clientK
   1.313       then A has sent it, ASSUMING that A chose PMS.  Authentication is
   1.314       assumed here; B cannot verify it.  But if the message is
   1.315 -     CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
   1.316 +     ClientFinished, then B can then check the quoted values XA, XB, etc.
   1.317  ***)
   1.318  goal thy
   1.319   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
   1.320 @@ -598,17 +665,21 @@
   1.321  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.322  				     not_parts_not_analz]) 2);
   1.323  by (Fake_parts_insert_tac 1);
   1.324 -(*ClientFinished.  If the message is old then apply induction hypothesis...*)
   1.325 -by (step_tac (!claset delrules [conjI]) 1);
   1.326 -by (subgoal_tac "Nonce PMS ~: analz (spies evsCF)" 1);
   1.327 -by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
   1.328 -by (blast_tac (!claset addSEs [MPair_parts]
   1.329 -		       addDs  [Notes_unique_PMS]) 1);
   1.330 +(*ClientResume: by unicity of PMS*)
   1.331 +by (blast_tac (!claset delrules [conjI]
   1.332 +		       addSEs [MPair_parts]
   1.333 +                       addSDs [Notes_master_imp_Notes_PMS]
   1.334 +	 	       addDs  [good_Notes_unique_PMS]) 2);
   1.335 +(*ClientFinished: by unicity of PMS*)
   1.336 +by (blast_tac (!claset delrules [conjI]
   1.337 +		       addSEs [MPair_parts]
   1.338 +		       addDs  [good_Notes_unique_PMS]) 1);
   1.339  qed_spec_mp "TrustClientMsg";
   1.340  
   1.341  
   1.342 -(*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to
   1.343 -     check a CERTIFICATE VERIFY from A, then A has used the quoted
   1.344 +
   1.345 +(*** Protocol goal: if B receives ClientFinished, and if B is able to
   1.346 +     check a CertVerify from A, then A has used the quoted
   1.347       values XA, XB, etc.  Even this one requires A to be uncompromised.
   1.348   ***)
   1.349  goal thy