Full version of TLS including session resumption, but no Oops
authorpaulson
Fri Sep 19 16:12:21 1997 +0200 (1997-09-19)
changeset 36855b8c0c8f576e
parent 3684 f677f0bc1cdf
child 3686 4b484805b4c4
Full version of TLS including session resumption, but no Oops
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     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
     2.1 --- a/src/HOL/Auth/TLS.thy	Fri Sep 19 16:11:24 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Fri Sep 19 16:12:21 1997 +0200
     2.3 @@ -30,9 +30,13 @@
     2.4  agent's state is recorded as the trace of messages.  When the true client (A)
     2.5  invents PMS, he encrypts PMS with B's public key before sending it.  The model
     2.6  does not distinguish the original occurrence of such a message from a replay.
     2.7 -
     2.8  In the shared-key model, the ability to encrypt implies the ability to
     2.9  decrypt, so the problem does not arise.
    2.10 +
    2.11 +Proofs would be simpler if ClientCertKeyEx included A's name within
    2.12 +Crypt KB (Nonce PMS).  As things stand, there is much overlap between proofs
    2.13 +about that message (which B receives) and the stronger event
    2.14 +	Notes A {|Agent B, Nonce PMS|}.
    2.15  *)
    2.16  
    2.17  TLS = Public + 
    2.18 @@ -56,8 +60,8 @@
    2.19      clientK, serverK :: "nat*nat*nat => key"
    2.20  
    2.21  translations
    2.22 -  "clientK x"	== "sessionK(True,x)"
    2.23 -  "serverK x"	== "sessionK(False,x)"
    2.24 +  "clientK (x)"	== "sessionK(True,x)"
    2.25 +  "serverK (x)"	== "sessionK(False,x)"
    2.26  
    2.27  rules
    2.28    inj_PRF       "inj PRF"	
    2.29 @@ -125,7 +129,7 @@
    2.30             and another MASTER SECRET is highly unlikely (even though
    2.31  	   both items have the same length, 48 bytes).
    2.32             The Note event records in the trace that she knows PMS
    2.33 -               (see REMARK at top).*)
    2.34 +               (see REMARK at top). *)
    2.35           "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    2.36               Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    2.37  	       : set evsCX |]
    2.38 @@ -134,7 +138,7 @@
    2.39  	      # evsCX  :  tls"
    2.40  
    2.41      CertVerify
    2.42 -	(*The optional CERTIFICATE VERIFY (7.4.8) message contains the
    2.43 +	(*The optional Certificate Verify (7.4.8) message contains the
    2.44            specific components listed in the security analysis, F.1.1.2.
    2.45            It adds the pre-master-secret, which is also essential!
    2.46            Checking the signature, which is the only use of A's certificate,
    2.47 @@ -151,13 +155,13 @@
    2.48            among other things.  The master-secret is PRF(PMS,NA,NB).
    2.49            Either party may sent its message first.*)
    2.50  
    2.51 +    ClientFinished
    2.52          (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
    2.53            rule's applying when the Spy has satisfied the "Says A B" by
    2.54            repaying messages sent by the true client; in that case, the
    2.55 -          Spy does not know PMS and could not sent CLIENT FINISHED.  One
    2.56 +          Spy does not know PMS and could not sent ClientFinished.  One
    2.57            could simply put A~=Spy into the rule, but one should not
    2.58            expect the spy to be well-behaved.*)
    2.59 -    ClientFinished
    2.60           "[| evsCF: tls;  
    2.61  	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
    2.62  	       : set evsCF;
    2.63 @@ -171,9 +175,9 @@
    2.64  			       Nonce NB, Number XB, Agent B|}))
    2.65                # evsCF  :  tls"
    2.66  
    2.67 +    ServerFinished
    2.68  	(*Keeping A' and A'' distinct means B cannot even check that the
    2.69            two messages originate from the same source. *)
    2.70 -    ServerFinished
    2.71           "[| evsSF: tls;
    2.72  	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
    2.73  	       : set evsSF;
    2.74 @@ -189,12 +193,12 @@
    2.75  			       Nonce NB, Number XB, Agent B|}))
    2.76                # evsSF  :  tls"
    2.77  
    2.78 -	(*Having transmitted CLIENT FINISHED and received an identical
    2.79 +    ClientAccepts
    2.80 +	(*Having transmitted ClientFinished and received an identical
    2.81            message encrypted with serverK, the client stores the parameters
    2.82            needed to resume this session.*)
    2.83 -    ClientAccepts
    2.84           "[| evsCA: tls;
    2.85 -             Notes A {|Agent B, Nonce PMS|} : set evsCA;
    2.86 +	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
    2.87  	     M = PRF(PMS,NA,NB);  
    2.88  	     X = Hash{|Nonce M, Number SID,
    2.89  	               Nonce NA, Number XA, Agent A, 
    2.90 @@ -204,10 +208,10 @@
    2.91            ==> 
    2.92               Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  :  tls"
    2.93  
    2.94 -	(*Having transmitted SERVER FINISHED and received an identical
    2.95 +    ServerAccepts
    2.96 +	(*Having transmitted ServerFinished and received an identical
    2.97            message encrypted with clientK, the server stores the parameters
    2.98            needed to resume this session.*)
    2.99 -    ServerAccepts
   2.100           "[| evsSA: tls;
   2.101               Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   2.102  	       : set evsSA;
   2.103 @@ -220,6 +224,34 @@
   2.104            ==> 
   2.105               Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
   2.106  
   2.107 +    ServerResume
   2.108 +         (*Resumption is described in 7.3.  If B finds the SESSION_ID
   2.109 +           then he sends HELLO and FINISHED messages, using the
   2.110 +           previously stored MASTER SECRET*)
   2.111 +         "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
   2.112 +             Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
   2.113 +	     Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
   2.114 +	       : set evsSR |]
   2.115 +          ==> Says B A (Crypt (serverK(NA,NB,M))
   2.116 +			(Hash{|Nonce M, Number SID,
   2.117 +			       Nonce NA, Number XA, Agent A, 
   2.118 +			       Nonce NB, Number XB, Agent B|}))
   2.119 +              # Says B A {|Nonce NB, Number SID, Number XB|} # evsSR  :  tls"
   2.120 +
   2.121 +    ClientResume
   2.122 +         (*If the response to ClientHello is ServerResume then send
   2.123 +           a FINISHED message using the new nonces and stored MASTER SECRET.*)
   2.124 +         "[| evsCR: tls;  
   2.125 +	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
   2.126 +	       : set evsCR;
   2.127 +             Says B' A {|Nonce NB, Number SID, Number XB|} : set evsCR;
   2.128 +             Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
   2.129 +          ==> Says A B (Crypt (clientK(NA,NB,M))
   2.130 +			(Hash{|Nonce M, Number SID,
   2.131 +			       Nonce NA, Number XA, Agent A, 
   2.132 +			       Nonce NB, Number XB, Agent B|}))
   2.133 +              # evsCR  :  tls"
   2.134 +
   2.135    (**Oops message??**)
   2.136  
   2.137  end