src/HOL/Auth/TLS.thy
changeset 3729 6be7cf5086ab
parent 3710 ea830f6e3c2d
child 3745 4c5d3b1ddc75
     1.1 --- a/src/HOL/Auth/TLS.thy	Mon Sep 29 11:45:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Mon Sep 29 11:46:33 1997 +0200
     1.3 @@ -93,25 +93,25 @@
     1.4  
     1.5      ClientHello
     1.6  	 (*(7.4.1.2)
     1.7 -	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
     1.8 +	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
     1.9  	   It is uninterpreted but will be confirmed in the FINISHED messages.
    1.10  	   NA is CLIENT RANDOM, while SID is SESSION_ID.
    1.11             UNIX TIME is omitted because the protocol doesn't use it.
    1.12             May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
    1.13  	   while MASTER SECRET is 48 byptes*)
    1.14           "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    1.15 -          ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
    1.16 +          ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.17  	        # evsCH  :  tls"
    1.18  
    1.19      ServerHello
    1.20           (*7.4.1.3 of the TLS Internet-Draft
    1.21 -	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.22 +	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.23             SERVER CERTIFICATE (7.4.2) is always present.
    1.24             CERTIFICATE_REQUEST (7.4.4) is implied.*)
    1.25           "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
    1.26 -             Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
    1.27 +             Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.28  	       : set evsSH |]
    1.29 -          ==> Says B A {|Nonce NB, Number SID, Number XB,
    1.30 +          ==> Says B A {|Nonce NB, Number SID, Number PB,
    1.31  			 certificate B (pubK B)|}
    1.32                  # evsSH  :  tls"
    1.33  
    1.34 @@ -125,7 +125,7 @@
    1.35             The Note event records in the trace that she knows PMS
    1.36                 (see REMARK at top). *)
    1.37           "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    1.38 -             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    1.39 +             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    1.40  	       : set evsCX |]
    1.41            ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
    1.42  	      # Notes A {|Agent B, Nonce PMS|}
    1.43 @@ -138,14 +138,13 @@
    1.44            Checking the signature, which is the only use of A's certificate,
    1.45            assures B of A's presence*)
    1.46           "[| evsCV: tls;  A ~= B;  
    1.47 -             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    1.48 +             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    1.49  	       : set evsCV;
    1.50  	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
    1.51 -          ==> Says A B (Crypt (priK A)
    1.52 -			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
    1.53 +          ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
    1.54                # evsCV  :  tls"
    1.55  
    1.56 -	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
    1.57 +	(*Finally come the FINISHED messages (7.4.8), confirming PA and PB
    1.58            among other things.  The master-secret is PRF(PMS,NA,NB).
    1.59            Either party may sent its message first.*)
    1.60  
    1.61 @@ -157,25 +156,25 @@
    1.62            could simply put A~=Spy into the rule, but one should not
    1.63            expect the spy to be well-behaved.*)
    1.64           "[| evsCF: tls;  
    1.65 -	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
    1.66 +	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.67  	       : set evsCF;
    1.68 -             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    1.69 +             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    1.70  	       : set evsCF;
    1.71               Notes A {|Agent B, Nonce PMS|} : set evsCF;
    1.72  	     M = PRF(PMS,NA,NB) |]
    1.73            ==> Says A B (Crypt (clientK(NA,NB,M))
    1.74  			(Hash{|Nonce M, Number SID,
    1.75 -			       Nonce NA, Number XA, Agent A, 
    1.76 -			       Nonce NB, Number XB, Agent B|}))
    1.77 +			       Nonce NA, Number PA, Agent A, 
    1.78 +			       Nonce NB, Number PB, Agent B|}))
    1.79                # evsCF  :  tls"
    1.80  
    1.81      ServerFinished
    1.82  	(*Keeping A' and A'' distinct means B cannot even check that the
    1.83            two messages originate from the same source. *)
    1.84           "[| evsSF: tls;
    1.85 -	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
    1.86 +	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
    1.87  	       : set evsSF;
    1.88 -	     Says B  A  {|Nonce NB, Number SID, Number XB,
    1.89 +	     Says B  A  {|Nonce NB, Number SID, Number PB,
    1.90  		 	  certificate B (pubK B)|}
    1.91  	       : set evsSF;
    1.92  	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
    1.93 @@ -183,8 +182,8 @@
    1.94  	     M = PRF(PMS,NA,NB) |]
    1.95            ==> Says B A (Crypt (serverK(NA,NB,M))
    1.96  			(Hash{|Nonce M, Number SID,
    1.97 -			       Nonce NA, Number XA, Agent A, 
    1.98 -			       Nonce NB, Number XB, Agent B|}))
    1.99 +			       Nonce NA, Number PA, Agent A, 
   1.100 +			       Nonce NB, Number PB, Agent B|}))
   1.101                # evsSF  :  tls"
   1.102  
   1.103      ClientAccepts
   1.104 @@ -196,8 +195,8 @@
   1.105  	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
   1.106  	     M = PRF(PMS,NA,NB);  
   1.107  	     X = Hash{|Nonce M, Number SID,
   1.108 -	               Nonce NA, Number XA, Agent A, 
   1.109 -		       Nonce NB, Number XB, Agent B|};
   1.110 +	               Nonce NA, Number PA, Agent A, 
   1.111 +		       Nonce NB, Number PB, Agent B|};
   1.112               Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
   1.113               Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
   1.114            ==> 
   1.115 @@ -213,8 +212,8 @@
   1.116  	       : set evsSA;
   1.117  	     M = PRF(PMS,NA,NB);  
   1.118  	     X = Hash{|Nonce M, Number SID,
   1.119 -	               Nonce NA, Number XA, Agent A, 
   1.120 -		       Nonce NB, Number XB, Agent B|};
   1.121 +	               Nonce NA, Number PA, Agent A, 
   1.122 +		       Nonce NB, Number PB, Agent B|};
   1.123               Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
   1.124               Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
   1.125            ==> 
   1.126 @@ -226,26 +225,26 @@
   1.127             previously stored MASTER SECRET*)
   1.128           "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
   1.129               Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
   1.130 -	     Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
   1.131 +	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
   1.132  	       : set evsSR |]
   1.133            ==> Says B A (Crypt (serverK(NA,NB,M))
   1.134  			(Hash{|Nonce M, Number SID,
   1.135 -			       Nonce NA, Number XA, Agent A, 
   1.136 -			       Nonce NB, Number XB, Agent B|}))
   1.137 -              # Says B A {|Nonce NB, Number SID, Number XB|} # evsSR  :  tls"
   1.138 +			       Nonce NA, Number PA, Agent A, 
   1.139 +			       Nonce NB, Number PB, Agent B|}))
   1.140 +              # Says B A {|Nonce NB, Number SID, Number PB|} # evsSR  :  tls"
   1.141  
   1.142      ClientResume
   1.143           (*If the response to ClientHello is ServerResume then send
   1.144             a FINISHED message using the new nonces and stored MASTER SECRET.*)
   1.145           "[| evsCR: tls;  
   1.146 -	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
   1.147 +	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
   1.148  	       : set evsCR;
   1.149 -             Says B' A {|Nonce NB, Number SID, Number XB|} : set evsCR;
   1.150 +             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
   1.151               Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
   1.152            ==> Says A B (Crypt (clientK(NA,NB,M))
   1.153  			(Hash{|Nonce M, Number SID,
   1.154 -			       Nonce NA, Number XA, Agent A, 
   1.155 -			       Nonce NB, Number XB, Agent B|}))
   1.156 +			       Nonce NA, Number PA, Agent A, 
   1.157 +			       Nonce NB, Number PB, Agent B|}))
   1.158                # evsCR  :  tls"
   1.159  
   1.160      Oops