Renamed XA, XB to PA, PB and removed the certificate from Client Verify
authorpaulson
Mon Sep 29 11:46:33 1997 +0200 (1997-09-29)
changeset 37296be7cf5086ab
parent 3728 f92594f65af6
child 3730 6933d20f335f
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Mon Sep 29 11:45:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Mon Sep 29 11:46:33 1997 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  * A upon receiving ServerFinished knows that B is present
     1.5  
     1.6  * Each party who has received a FINISHED message can trust that the other
     1.7 -  party agrees on all message components, including XA and XB (thus foiling
     1.8 +  party agrees on all message components, including PA and PB (thus foiling
     1.9    rollback attacks).
    1.10  *)
    1.11  
    1.12 @@ -102,7 +102,7 @@
    1.13  (*And one for ServerAccepts.  Either FINISHED message may come first.*)
    1.14  goal thy 
    1.15   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.16 -\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
    1.17 +\           A ~= B |] ==> EX SID NA PA NB PB M. EX evs: tls.    \
    1.18  \  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    1.19  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.20  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.21 @@ -115,8 +115,7 @@
    1.22  goal thy 
    1.23   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.24  \           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
    1.25 -\  Says A B (Crypt (priK A)                 \
    1.26 -\            (Hash{|Nonce NB, certificate B (pubK B), Nonce PMS|})) : set evs";
    1.27 +\  Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
    1.28  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.29  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.30  	  RS tls.CertVerify) 2);
    1.31 @@ -130,11 +129,11 @@
    1.32  \           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
    1.33  \           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
    1.34  \           ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.35 -\           A ~= B |] ==> EX NA XA NB XB. EX evs: tls.    \
    1.36 +\           A ~= B |] ==> EX NA PA NB PB. EX evs: tls.    \
    1.37  \  Says A B (Crypt (clientK(NA,NB,M))                           \
    1.38  \            (Hash{|Nonce M, Number SID,             \
    1.39 -\                   Nonce NA, Number XA, Agent A,      \
    1.40 -\                   Nonce NB, Number XB, Agent B|})) : set evs";
    1.41 +\                   Nonce NA, Number PA, Agent A,      \
    1.42 +\                   Nonce NB, Number PB, Agent B|})) : set evs";
    1.43  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.44  by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2);
    1.45  by possibility_tac;
    1.46 @@ -301,10 +300,9 @@
    1.47    message is Fake.  We don't need guarantees for the Spy anyway.  We must
    1.48    assume A~:bad; otherwise, the Spy can forge A's signature.*)
    1.49  goal thy
    1.50 - "!!evs. [| X = Crypt (priK A)                                        \
    1.51 -\                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
    1.52 + "!!evs. [| X = Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|});      \
    1.53  \           evs : tls;  A ~: bad;  B ~= Spy |]                       \
    1.54 -\    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
    1.55 +\    ==> Says B A {|Nonce NB, Number SID, Number PB, certificate B KB|}  \
    1.56  \          : set evs --> \
    1.57  \        X : parts (spies evs) --> Says A B X : set evs";
    1.58  by (hyp_subst_tac 1);
    1.59 @@ -318,7 +316,7 @@
    1.60  
    1.61  (*If CertVerify is present then A has chosen PMS.*)
    1.62  goal thy
    1.63 - "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
    1.64 + "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})  \
    1.65  \             : parts (spies evs);                                \
    1.66  \           evs : tls;  A ~: bad |]                                      \
    1.67  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
    1.68 @@ -692,8 +690,8 @@
    1.69  
    1.70  
    1.71  (*** Protocol goals: if A receives ServerFinished, then B is present 
    1.72 -     and has used the quoted values XA, XB, etc.  Note that it is up to A
    1.73 -     to compare XA with what she originally sent.
    1.74 +     and has used the quoted values PA, PB, etc.  Note that it is up to A
    1.75 +     to compare PA with what she originally sent.
    1.76  ***)
    1.77  
    1.78  (*The mention of her name (A) in X assures A that B knows who she is.*)
    1.79 @@ -701,8 +699,8 @@
    1.80   "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
    1.81  \           X = Crypt (serverK(Na,Nb,M))                  \
    1.82  \                 (Hash{|Nonce M, Number SID,             \
    1.83 -\                        Nonce NA, Number XA, Agent A,    \
    1.84 -\                        Nonce NB, Number XB, Agent B|}); \
    1.85 +\                        Nonce NA, Number PA, Agent A,    \
    1.86 +\                        Nonce NB, Number PB, Agent B|}); \
    1.87  \           M = PRF(PMS,NA,NB);                           \
    1.88  \           evs : tls;  A ~: bad;  B ~: bad |]          \
    1.89  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
    1.90 @@ -727,8 +725,8 @@
    1.91  goal thy
    1.92   "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
    1.93  \                 (Hash{|Nonce M, Number SID,             \
    1.94 -\                        Nonce NA, Number XA, Agent A,    \
    1.95 -\                        Nonce NB, Number XB, Agent B|}); \
    1.96 +\                        Nonce NA, Number PA, Agent A,    \
    1.97 +\                        Nonce NB, Number PB, Agent B|}); \
    1.98  \           M = PRF(PMS,NA,NB);                           \
    1.99  \           X : parts (spies evs);                        \
   1.100  \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   1.101 @@ -794,7 +792,7 @@
   1.102  (*** Protocol goal: if B receives any message encrypted with clientK
   1.103       then A has sent it, ASSUMING that A chose PMS.  Authentication is
   1.104       assumed here; B cannot verify it.  But if the message is
   1.105 -     ClientFinished, then B can then check the quoted values XA, XB, etc.
   1.106 +     ClientFinished, then B can then check the quoted values PA, PB, etc.
   1.107  ***)
   1.108  
   1.109  goal thy
   1.110 @@ -834,15 +832,14 @@
   1.111  
   1.112  (*** Protocol goal: if B receives ClientFinished, and if B is able to
   1.113       check a CertVerify from A, then A has used the quoted
   1.114 -     values XA, XB, etc.  Even this one requires A to be uncompromised.
   1.115 +     values PA, PB, etc.  Even this one requires A to be uncompromised.
   1.116   ***)
   1.117  goal thy
   1.118   "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   1.119  \           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   1.120 -\           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
   1.121 +\           Says B  A {|Nonce NB, Number SID, Number PB, certificate B KB|}  \
   1.122  \             : set evs;                                                  \
   1.123 -\           Says A'' B (Crypt (priK A)                                    \
   1.124 -\                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
   1.125 +\           Says A'' B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))\
   1.126  \             : set evs;                                                  \
   1.127  \        evs : tls;  A ~: bad;  B ~: bad |]                             \
   1.128  \     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
     2.1 --- a/src/HOL/Auth/TLS.thy	Mon Sep 29 11:45:52 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Mon Sep 29 11:46:33 1997 +0200
     2.3 @@ -93,25 +93,25 @@
     2.4  
     2.5      ClientHello
     2.6  	 (*(7.4.1.2)
     2.7 -	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
     2.8 +	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
     2.9  	   It is uninterpreted but will be confirmed in the FINISHED messages.
    2.10  	   NA is CLIENT RANDOM, while SID is SESSION_ID.
    2.11             UNIX TIME is omitted because the protocol doesn't use it.
    2.12             May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
    2.13  	   while MASTER SECRET is 48 byptes*)
    2.14           "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    2.15 -          ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
    2.16 +          ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
    2.17  	        # evsCH  :  tls"
    2.18  
    2.19      ServerHello
    2.20           (*7.4.1.3 of the TLS Internet-Draft
    2.21 -	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    2.22 +	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    2.23             SERVER CERTIFICATE (7.4.2) is always present.
    2.24             CERTIFICATE_REQUEST (7.4.4) is implied.*)
    2.25           "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
    2.26 -             Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
    2.27 +             Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    2.28  	       : set evsSH |]
    2.29 -          ==> Says B A {|Nonce NB, Number SID, Number XB,
    2.30 +          ==> Says B A {|Nonce NB, Number SID, Number PB,
    2.31  			 certificate B (pubK B)|}
    2.32                  # evsSH  :  tls"
    2.33  
    2.34 @@ -125,7 +125,7 @@
    2.35             The Note event records in the trace that she knows PMS
    2.36                 (see REMARK at top). *)
    2.37           "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    2.38 -             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    2.39 +             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    2.40  	       : set evsCX |]
    2.41            ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
    2.42  	      # Notes A {|Agent B, Nonce PMS|}
    2.43 @@ -138,14 +138,13 @@
    2.44            Checking the signature, which is the only use of A's certificate,
    2.45            assures B of A's presence*)
    2.46           "[| evsCV: tls;  A ~= B;  
    2.47 -             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    2.48 +             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    2.49  	       : set evsCV;
    2.50  	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
    2.51 -          ==> Says A B (Crypt (priK A)
    2.52 -			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
    2.53 +          ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
    2.54                # evsCV  :  tls"
    2.55  
    2.56 -	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
    2.57 +	(*Finally come the FINISHED messages (7.4.8), confirming PA and PB
    2.58            among other things.  The master-secret is PRF(PMS,NA,NB).
    2.59            Either party may sent its message first.*)
    2.60  
    2.61 @@ -157,25 +156,25 @@
    2.62            could simply put A~=Spy into the rule, but one should not
    2.63            expect the spy to be well-behaved.*)
    2.64           "[| evsCF: tls;  
    2.65 -	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
    2.66 +	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
    2.67  	       : set evsCF;
    2.68 -             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    2.69 +             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    2.70  	       : set evsCF;
    2.71               Notes A {|Agent B, Nonce PMS|} : set evsCF;
    2.72  	     M = PRF(PMS,NA,NB) |]
    2.73            ==> Says A B (Crypt (clientK(NA,NB,M))
    2.74  			(Hash{|Nonce M, Number SID,
    2.75 -			       Nonce NA, Number XA, Agent A, 
    2.76 -			       Nonce NB, Number XB, Agent B|}))
    2.77 +			       Nonce NA, Number PA, Agent A, 
    2.78 +			       Nonce NB, Number PB, Agent B|}))
    2.79                # evsCF  :  tls"
    2.80  
    2.81      ServerFinished
    2.82  	(*Keeping A' and A'' distinct means B cannot even check that the
    2.83            two messages originate from the same source. *)
    2.84           "[| evsSF: tls;
    2.85 -	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
    2.86 +	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
    2.87  	       : set evsSF;
    2.88 -	     Says B  A  {|Nonce NB, Number SID, Number XB,
    2.89 +	     Says B  A  {|Nonce NB, Number SID, Number PB,
    2.90  		 	  certificate B (pubK B)|}
    2.91  	       : set evsSF;
    2.92  	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
    2.93 @@ -183,8 +182,8 @@
    2.94  	     M = PRF(PMS,NA,NB) |]
    2.95            ==> Says B A (Crypt (serverK(NA,NB,M))
    2.96  			(Hash{|Nonce M, Number SID,
    2.97 -			       Nonce NA, Number XA, Agent A, 
    2.98 -			       Nonce NB, Number XB, Agent B|}))
    2.99 +			       Nonce NA, Number PA, Agent A, 
   2.100 +			       Nonce NB, Number PB, Agent B|}))
   2.101                # evsSF  :  tls"
   2.102  
   2.103      ClientAccepts
   2.104 @@ -196,8 +195,8 @@
   2.105  	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
   2.106  	     M = PRF(PMS,NA,NB);  
   2.107  	     X = Hash{|Nonce M, Number SID,
   2.108 -	               Nonce NA, Number XA, Agent A, 
   2.109 -		       Nonce NB, Number XB, Agent B|};
   2.110 +	               Nonce NA, Number PA, Agent A, 
   2.111 +		       Nonce NB, Number PB, Agent B|};
   2.112               Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
   2.113               Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
   2.114            ==> 
   2.115 @@ -213,8 +212,8 @@
   2.116  	       : set evsSA;
   2.117  	     M = PRF(PMS,NA,NB);  
   2.118  	     X = Hash{|Nonce M, Number SID,
   2.119 -	               Nonce NA, Number XA, Agent A, 
   2.120 -		       Nonce NB, Number XB, Agent B|};
   2.121 +	               Nonce NA, Number PA, Agent A, 
   2.122 +		       Nonce NB, Number PB, Agent B|};
   2.123               Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
   2.124               Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
   2.125            ==> 
   2.126 @@ -226,26 +225,26 @@
   2.127             previously stored MASTER SECRET*)
   2.128           "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
   2.129               Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
   2.130 -	     Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
   2.131 +	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
   2.132  	       : set evsSR |]
   2.133            ==> Says B A (Crypt (serverK(NA,NB,M))
   2.134  			(Hash{|Nonce M, Number SID,
   2.135 -			       Nonce NA, Number XA, Agent A, 
   2.136 -			       Nonce NB, Number XB, Agent B|}))
   2.137 -              # Says B A {|Nonce NB, Number SID, Number XB|} # evsSR  :  tls"
   2.138 +			       Nonce NA, Number PA, Agent A, 
   2.139 +			       Nonce NB, Number PB, Agent B|}))
   2.140 +              # Says B A {|Nonce NB, Number SID, Number PB|} # evsSR  :  tls"
   2.141  
   2.142      ClientResume
   2.143           (*If the response to ClientHello is ServerResume then send
   2.144             a FINISHED message using the new nonces and stored MASTER SECRET.*)
   2.145           "[| evsCR: tls;  
   2.146 -	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
   2.147 +	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
   2.148  	       : set evsCR;
   2.149 -             Says B' A {|Nonce NB, Number SID, Number XB|} : set evsCR;
   2.150 +             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
   2.151               Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
   2.152            ==> Says A B (Crypt (clientK(NA,NB,M))
   2.153  			(Hash{|Nonce M, Number SID,
   2.154 -			       Nonce NA, Number XA, Agent A, 
   2.155 -			       Nonce NB, Number XB, Agent B|}))
   2.156 +			       Nonce NA, Number PA, Agent A, 
   2.157 +			       Nonce NB, Number PB, Agent B|}))
   2.158                # evsCR  :  tls"
   2.159  
   2.160      Oops