# HG changeset patch
# User paulson
# Date 874413601 -7200
# Node ID cbaec955056b5e829fb94360ea7c467d9bb1ff12
# Parent  70dd312b70b2be767297f81a78c5f3b4fc0f5d63
Addition of SessionIDs to the Hello and Finished messages

diff -r 70dd312b70b2 -r cbaec955056b src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Tue Sep 16 14:04:10 1997 +0200
+++ b/src/HOL/Auth/TLS.ML	Tue Sep 16 14:40:01 1997 +0200
@@ -110,9 +110,10 @@
 (*Possibility property ending with ServerFinished.*)
 goal thy 
  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
-\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
+\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
 \  Says B A (Crypt (serverK(NA,NB,M))                       \
-\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A,      \
+\            (Hash{|Nonce M, Number SID,             \
+\                   Nonce NA, Number XA, Agent A,      \
 \                   Nonce NB, Number XB, Agent B|})) \
 \    : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -125,9 +126,10 @@
 (*And one for ClientFinished.  Either FINISHED message may come first.*)
 goal thy 
  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
-\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
+\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
 \  Says A B (Crypt (clientK(NA,NB,M))                           \
-\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
+\            (Hash{|Nonce M, Number SID,             \
+\                   Nonce NA, Number XA, Agent A,      \
 \                   Nonce NB, Number XB, Agent B|})) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
@@ -292,7 +294,7 @@
  "!!evs. [| X = Crypt (priK A)                                        \
 \                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
 \           evs : tls;  A ~: lost;  B ~= Spy |]                       \
-\    ==> Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
+\    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
 \          : set evs --> \
 \        X : parts (sees Spy evs) --> Says A B X : set evs";
 by (hyp_subst_tac 1);
@@ -588,12 +590,13 @@
 
 (*The mention of her name (A) in X assumes A that B knows who she is.*)
 goal thy
- "!!evs. [| X = Crypt (serverK(Na,Nb,M))                                \
-\                 (Hash{|Nonce M, Nonce NA, Number XA, Agent A,         \
+ "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
+\                 (Hash{|Nonce M, Number SID,             \
+\                        Nonce NA, Number XA, Agent A,    \
 \                        Nonce NB, Number XB, Agent B|}); \
-\           M = PRF(PMS,NA,NB); \
-\           evs : tls;  A ~: lost;  B ~: lost |]                        \
-\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                 \
+\           M = PRF(PMS,NA,NB);                           \
+\           evs : tls;  A ~: lost;  B ~: lost |]          \
+\        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
 \        X : parts (sees Spy evs) --> Says B A X : set evs";
 by (hyp_subst_tac 1);
 by (analz_induct_tac 1);
@@ -674,7 +677,7 @@
  ***)
 goal thy
  "!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
-\           Says B  A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
+\           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
 \             : set evs;                                                  \
 \           Says A'' B (Crypt (priK A)                                    \
 \                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
diff -r 70dd312b70b2 -r cbaec955056b src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Tue Sep 16 14:04:10 1997 +0200
+++ b/src/HOL/Auth/TLS.thy	Tue Sep 16 14:40:01 1997 +0200
@@ -87,22 +87,23 @@
 	 (*(7.4.1.2)
 	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
 	   It is uninterpreted but will be confirmed in the FINISHED messages.
-	   As an initial simplification, SESSION_ID is identified with NA
-           and reuse of sessions is not supported.
-           May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes
-	   while MASTER SECRET is 48 byptes (6.1)*)
+	   NA is CLIENT RANDOM, while SID is SESSION_ID.
+           UNIX TIME is omitted because the protocol doesn't use it.
+           May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
+	   while MASTER SECRET is 48 byptes*)
          "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
-          ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH  :  tls"
+          ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
+	        # evsCH  :  tls"
 
     ServerHello
          (*7.4.1.3 of the TLS Internet-Draft
 	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
-	   NA is returned in its role as SESSION_ID.
            SERVER CERTIFICATE (7.4.2) is always present.
            CERTIFICATE_REQUEST (7.4.4) is implied.*)
          "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
-             Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSH |]
-          ==> Says B A {|Nonce NA, Nonce NB, Number XB,
+             Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
+	       : set evsSH |]
+          ==> Says B A {|Nonce NB, Number SID, Number XB,
 			 certificate B (pubK B)|}
                 # evsSH  :  tls"
 
@@ -116,7 +117,7 @@
            The Note event records in the trace that she knows PMS
                (see REMARK at top).*)
          "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
-             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
+             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
 	       : set evsCX |]
           ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
 	      # Notes A {|Agent B, Nonce PMS|}
@@ -129,12 +130,12 @@
           Checking the signature, which is the only use of A's certificate,
           assures B of A's presence*)
          "[| evsCV: tls;  A ~= B;  
-             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
+             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
 	       : set evsCV;
 	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
           ==> Says A B (Crypt (priK A)
 			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
-                # evsCV  :  tls"
+              # evsCV  :  tls"
 
 	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
           among other things.  The master-secret is PRF(PMS,NA,NB).
@@ -148,33 +149,35 @@
           expect the spy to be well-behaved.*)
     ClientFinished
          "[| evsCF: tls;  
-	     Says A  B {|Agent A, Nonce NA, Number XA|} : set evsCF;
-             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
+	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
+	       : set evsCF;
+             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
 	       : set evsCF;
              Notes A {|Agent B, Nonce PMS|} : set evsCF;
 	     M = PRF(PMS,NA,NB) |]
           ==> Says A B (Crypt (clientK(NA,NB,M))
-			(Hash{|Nonce M,
+			(Hash{|Nonce M, Number SID,
 			       Nonce NA, Number XA, Agent A, 
 			       Nonce NB, Number XB, Agent B|}))
-                # evsCF  :  tls"
+              # evsCF  :  tls"
 
 	(*Keeping A' and A'' distinct means B cannot even check that the
           two messages originate from the same source. *)
     ServerFinished
          "[| evsSF: tls;
-	     Says A' B  {|Agent A, Nonce NA, Number XA|} : set evsSF;
-	     Says B  A  {|Nonce NA, Nonce NB, Number XB,
+	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
+	       : set evsSF;
+	     Says B  A  {|Nonce NB, Number SID, Number XB,
 		 	  certificate B (pubK B)|}
 	       : set evsSF;
 	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
 	       : set evsSF;
 	     M = PRF(PMS,NA,NB) |]
           ==> Says B A (Crypt (serverK(NA,NB,M))
-			(Hash{|Nonce M,
+			(Hash{|Nonce M, Number SID,
 			       Nonce NA, Number XA, Agent A, 
 			       Nonce NB, Number XB, Agent B|}))
-                # evsSF  :  tls"
+              # evsSF  :  tls"
 
   (**Oops message??**)