Addition of SessionIDs to the Hello and Finished messages
authorpaulson
Tue Sep 16 14:40:01 1997 +0200 (1997-09-16)
changeset 3676cbaec955056b
parent 3675 70dd312b70b2
child 3677 f2569416d18b
Addition of SessionIDs to the Hello and Finished messages
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Tue Sep 16 14:04:10 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Sep 16 14:40:01 1997 +0200
     1.3 @@ -110,9 +110,10 @@
     1.4  (*Possibility property ending with ServerFinished.*)
     1.5  goal thy 
     1.6   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
     1.7 -\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
     1.8 +\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
     1.9  \  Says B A (Crypt (serverK(NA,NB,M))                       \
    1.10 -\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A,      \
    1.11 +\            (Hash{|Nonce M, Number SID,             \
    1.12 +\                   Nonce NA, Number XA, Agent A,      \
    1.13  \                   Nonce NB, Number XB, Agent B|})) \
    1.14  \    : set evs";
    1.15  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.16 @@ -125,9 +126,10 @@
    1.17  (*And one for ClientFinished.  Either FINISHED message may come first.*)
    1.18  goal thy 
    1.19   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.20 -\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
    1.21 +\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
    1.22  \  Says A B (Crypt (clientK(NA,NB,M))                           \
    1.23 -\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
    1.24 +\            (Hash{|Nonce M, Number SID,             \
    1.25 +\                   Nonce NA, Number XA, Agent A,      \
    1.26  \                   Nonce NB, Number XB, Agent B|})) : set evs";
    1.27  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.28  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.29 @@ -292,7 +294,7 @@
    1.30   "!!evs. [| X = Crypt (priK A)                                        \
    1.31  \                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
    1.32  \           evs : tls;  A ~: lost;  B ~= Spy |]                       \
    1.33 -\    ==> Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
    1.34 +\    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
    1.35  \          : set evs --> \
    1.36  \        X : parts (sees Spy evs) --> Says A B X : set evs";
    1.37  by (hyp_subst_tac 1);
    1.38 @@ -588,12 +590,13 @@
    1.39  
    1.40  (*The mention of her name (A) in X assumes A that B knows who she is.*)
    1.41  goal thy
    1.42 - "!!evs. [| X = Crypt (serverK(Na,Nb,M))                                \
    1.43 -\                 (Hash{|Nonce M, Nonce NA, Number XA, Agent A,         \
    1.44 + "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
    1.45 +\                 (Hash{|Nonce M, Number SID,             \
    1.46 +\                        Nonce NA, Number XA, Agent A,    \
    1.47  \                        Nonce NB, Number XB, Agent B|}); \
    1.48 -\           M = PRF(PMS,NA,NB); \
    1.49 -\           evs : tls;  A ~: lost;  B ~: lost |]                        \
    1.50 -\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                 \
    1.51 +\           M = PRF(PMS,NA,NB);                           \
    1.52 +\           evs : tls;  A ~: lost;  B ~: lost |]          \
    1.53 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
    1.54  \        X : parts (sees Spy evs) --> Says B A X : set evs";
    1.55  by (hyp_subst_tac 1);
    1.56  by (analz_induct_tac 1);
    1.57 @@ -674,7 +677,7 @@
    1.58   ***)
    1.59  goal thy
    1.60   "!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
    1.61 -\           Says B  A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
    1.62 +\           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
    1.63  \             : set evs;                                                  \
    1.64  \           Says A'' B (Crypt (priK A)                                    \
    1.65  \                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
     2.1 --- a/src/HOL/Auth/TLS.thy	Tue Sep 16 14:04:10 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 16 14:40:01 1997 +0200
     2.3 @@ -87,22 +87,23 @@
     2.4  	 (*(7.4.1.2)
     2.5  	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
     2.6  	   It is uninterpreted but will be confirmed in the FINISHED messages.
     2.7 -	   As an initial simplification, SESSION_ID is identified with NA
     2.8 -           and reuse of sessions is not supported.
     2.9 -           May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes
    2.10 -	   while MASTER SECRET is 48 byptes (6.1)*)
    2.11 +	   NA is CLIENT RANDOM, while SID is SESSION_ID.
    2.12 +           UNIX TIME is omitted because the protocol doesn't use it.
    2.13 +           May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
    2.14 +	   while MASTER SECRET is 48 byptes*)
    2.15           "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    2.16 -          ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH  :  tls"
    2.17 +          ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
    2.18 +	        # evsCH  :  tls"
    2.19  
    2.20      ServerHello
    2.21           (*7.4.1.3 of the TLS Internet-Draft
    2.22  	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    2.23 -	   NA is returned in its role as SESSION_ID.
    2.24             SERVER CERTIFICATE (7.4.2) is always present.
    2.25             CERTIFICATE_REQUEST (7.4.4) is implied.*)
    2.26           "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
    2.27 -             Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSH |]
    2.28 -          ==> Says B A {|Nonce NA, Nonce NB, Number XB,
    2.29 +             Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
    2.30 +	       : set evsSH |]
    2.31 +          ==> Says B A {|Nonce NB, Number SID, Number XB,
    2.32  			 certificate B (pubK B)|}
    2.33                  # evsSH  :  tls"
    2.34  
    2.35 @@ -116,7 +117,7 @@
    2.36             The Note event records in the trace that she knows PMS
    2.37                 (see REMARK at top).*)
    2.38           "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    2.39 -             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
    2.40 +             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    2.41  	       : set evsCX |]
    2.42            ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
    2.43  	      # Notes A {|Agent B, Nonce PMS|}
    2.44 @@ -129,12 +130,12 @@
    2.45            Checking the signature, which is the only use of A's certificate,
    2.46            assures B of A's presence*)
    2.47           "[| evsCV: tls;  A ~= B;  
    2.48 -             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
    2.49 +             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    2.50  	       : set evsCV;
    2.51  	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
    2.52            ==> Says A B (Crypt (priK A)
    2.53  			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
    2.54 -                # evsCV  :  tls"
    2.55 +              # evsCV  :  tls"
    2.56  
    2.57  	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
    2.58            among other things.  The master-secret is PRF(PMS,NA,NB).
    2.59 @@ -148,33 +149,35 @@
    2.60            expect the spy to be well-behaved.*)
    2.61      ClientFinished
    2.62           "[| evsCF: tls;  
    2.63 -	     Says A  B {|Agent A, Nonce NA, Number XA|} : set evsCF;
    2.64 -             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
    2.65 +	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
    2.66 +	       : set evsCF;
    2.67 +             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    2.68  	       : set evsCF;
    2.69               Notes A {|Agent B, Nonce PMS|} : set evsCF;
    2.70  	     M = PRF(PMS,NA,NB) |]
    2.71            ==> Says A B (Crypt (clientK(NA,NB,M))
    2.72 -			(Hash{|Nonce M,
    2.73 +			(Hash{|Nonce M, Number SID,
    2.74  			       Nonce NA, Number XA, Agent A, 
    2.75  			       Nonce NB, Number XB, Agent B|}))
    2.76 -                # evsCF  :  tls"
    2.77 +              # evsCF  :  tls"
    2.78  
    2.79  	(*Keeping A' and A'' distinct means B cannot even check that the
    2.80            two messages originate from the same source. *)
    2.81      ServerFinished
    2.82           "[| evsSF: tls;
    2.83 -	     Says A' B  {|Agent A, Nonce NA, Number XA|} : set evsSF;
    2.84 -	     Says B  A  {|Nonce NA, Nonce NB, Number XB,
    2.85 +	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
    2.86 +	       : set evsSF;
    2.87 +	     Says B  A  {|Nonce NB, Number SID, Number XB,
    2.88  		 	  certificate B (pubK B)|}
    2.89  	       : set evsSF;
    2.90  	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
    2.91  	       : set evsSF;
    2.92  	     M = PRF(PMS,NA,NB) |]
    2.93            ==> Says B A (Crypt (serverK(NA,NB,M))
    2.94 -			(Hash{|Nonce M,
    2.95 +			(Hash{|Nonce M, Number SID,
    2.96  			       Nonce NA, Number XA, Agent A, 
    2.97  			       Nonce NB, Number XB, Agent B|}))
    2.98 -                # evsSF  :  tls"
    2.99 +              # evsSF  :  tls"
   2.100  
   2.101    (**Oops message??**)
   2.102