src/HOL/Auth/TLS.thy
changeset 3676 cbaec955056b
parent 3672 56e4365a0c99
child 3677 f2569416d18b
     1.1 --- a/src/HOL/Auth/TLS.thy	Tue Sep 16 14:04:10 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 16 14:40:01 1997 +0200
     1.3 @@ -87,22 +87,23 @@
     1.4  	 (*(7.4.1.2)
     1.5  	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
     1.6  	   It is uninterpreted but will be confirmed in the FINISHED messages.
     1.7 -	   As an initial simplification, SESSION_ID is identified with NA
     1.8 -           and reuse of sessions is not supported.
     1.9 -           May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes
    1.10 -	   while MASTER SECRET is 48 byptes (6.1)*)
    1.11 +	   NA is CLIENT RANDOM, while SID is SESSION_ID.
    1.12 +           UNIX TIME is omitted because the protocol doesn't use it.
    1.13 +           May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
    1.14 +	   while MASTER SECRET is 48 byptes*)
    1.15           "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    1.16 -          ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH  :  tls"
    1.17 +          ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
    1.18 +	        # evsCH  :  tls"
    1.19  
    1.20      ServerHello
    1.21           (*7.4.1.3 of the TLS Internet-Draft
    1.22  	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.23 -	   NA is returned in its role as SESSION_ID.
    1.24             SERVER CERTIFICATE (7.4.2) is always present.
    1.25             CERTIFICATE_REQUEST (7.4.4) is implied.*)
    1.26           "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
    1.27 -             Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSH |]
    1.28 -          ==> Says B A {|Nonce NA, Nonce NB, Number XB,
    1.29 +             Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
    1.30 +	       : set evsSH |]
    1.31 +          ==> Says B A {|Nonce NB, Number SID, Number XB,
    1.32  			 certificate B (pubK B)|}
    1.33                  # evsSH  :  tls"
    1.34  
    1.35 @@ -116,7 +117,7 @@
    1.36             The Note event records in the trace that she knows PMS
    1.37                 (see REMARK at top).*)
    1.38           "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    1.39 -             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
    1.40 +             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    1.41  	       : set evsCX |]
    1.42            ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
    1.43  	      # Notes A {|Agent B, Nonce PMS|}
    1.44 @@ -129,12 +130,12 @@
    1.45            Checking the signature, which is the only use of A's certificate,
    1.46            assures B of A's presence*)
    1.47           "[| evsCV: tls;  A ~= B;  
    1.48 -             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
    1.49 +             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    1.50  	       : set evsCV;
    1.51  	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
    1.52            ==> Says A B (Crypt (priK A)
    1.53  			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
    1.54 -                # evsCV  :  tls"
    1.55 +              # evsCV  :  tls"
    1.56  
    1.57  	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
    1.58            among other things.  The master-secret is PRF(PMS,NA,NB).
    1.59 @@ -148,33 +149,35 @@
    1.60            expect the spy to be well-behaved.*)
    1.61      ClientFinished
    1.62           "[| evsCF: tls;  
    1.63 -	     Says A  B {|Agent A, Nonce NA, Number XA|} : set evsCF;
    1.64 -             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
    1.65 +	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
    1.66 +	       : set evsCF;
    1.67 +             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    1.68  	       : set evsCF;
    1.69               Notes A {|Agent B, Nonce PMS|} : set evsCF;
    1.70  	     M = PRF(PMS,NA,NB) |]
    1.71            ==> Says A B (Crypt (clientK(NA,NB,M))
    1.72 -			(Hash{|Nonce M,
    1.73 +			(Hash{|Nonce M, Number SID,
    1.74  			       Nonce NA, Number XA, Agent A, 
    1.75  			       Nonce NB, Number XB, Agent B|}))
    1.76 -                # evsCF  :  tls"
    1.77 +              # evsCF  :  tls"
    1.78  
    1.79  	(*Keeping A' and A'' distinct means B cannot even check that the
    1.80            two messages originate from the same source. *)
    1.81      ServerFinished
    1.82           "[| evsSF: tls;
    1.83 -	     Says A' B  {|Agent A, Nonce NA, Number XA|} : set evsSF;
    1.84 -	     Says B  A  {|Nonce NA, Nonce NB, Number XB,
    1.85 +	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
    1.86 +	       : set evsSF;
    1.87 +	     Says B  A  {|Nonce NB, Number SID, Number XB,
    1.88  		 	  certificate B (pubK B)|}
    1.89  	       : set evsSF;
    1.90  	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
    1.91  	       : set evsSF;
    1.92  	     M = PRF(PMS,NA,NB) |]
    1.93            ==> Says B A (Crypt (serverK(NA,NB,M))
    1.94 -			(Hash{|Nonce M,
    1.95 +			(Hash{|Nonce M, Number SID,
    1.96  			       Nonce NA, Number XA, Agent A, 
    1.97  			       Nonce NB, Number XB, Agent B|}))
    1.98 -                # evsSF  :  tls"
    1.99 +              # evsSF  :  tls"
   1.100  
   1.101    (**Oops message??**)
   1.102