src/HOL/Auth/TLS.thy

 	       : set evsCF;
              Says B' A {|Nonce NB, Number SID, Number PB|} : 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, Number SID,
+			(Hash{|Number SID, Nonce M,
 			       Nonce NA, Number PA, Agent A, 
 			       Nonce NB, Number PB, Agent B|}))
               # evsCF  :  tls"
 
     ServerFinished

 	       : set evsSF;
 	     Says B  A  {|Nonce NB, Number SID, Number PB|} : set evsSF;
 	     Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF;
 	     M = PRF(PMS,NA,NB) |]
           ==> Says B A (Crypt (serverK(NA,NB,M))
-			(Hash{|Nonce M, Number SID,
+			(Hash{|Number SID, Nonce M,
 			       Nonce NA, Number PA, Agent A, 
 			       Nonce NB, Number PB, Agent B|}))
               # evsSF  :  tls"
 
     ClientAccepts

           needed to resume this session.  The "Notes A ..." premise is
           used to prove Notes_master_imp_Crypt_PMS.*)
          "[| evsCA: tls;
 	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
 	     M = PRF(PMS,NA,NB);  
-	     X = Hash{|Nonce M, Number SID,
+	     X = Hash{|Number SID, Nonce M,
 	               Nonce NA, Number PA, Agent A, 
 		       Nonce NB, Number PB, Agent B|};
              Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
              Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
           ==> 

           needed to resume this session.  The "Says A'' B ..." premise is
           used to prove Notes_master_imp_Crypt_PMS.*)
          "[| evsSA: tls;
              Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
 	     M = PRF(PMS,NA,NB);  
-	     X = Hash{|Nonce M, Number SID,
+	     X = Hash{|Number SID, Nonce M,
 	               Nonce NA, Number PA, Agent A, 
 		       Nonce NB, Number PB, Agent B|};
              Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
              Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
           ==> 

          "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
              Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
 	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
 	       : set evsSR |]
           ==> Says B A (Crypt (serverK(NA,NB,M))
-			(Hash{|Nonce M, Number SID,
+			(Hash{|Number SID, Nonce M,
 			       Nonce NA, Number PA, Agent A, 
 			       Nonce NB, Number PB, Agent B|})) # evsSR
 	        :  tls"
 
     ClientResume

 	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
 	       : set evsCR;
              Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
              Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
           ==> Says A B (Crypt (clientK(NA,NB,M))
-			(Hash{|Nonce M, Number SID,
+			(Hash{|Number SID, Nonce M,
 			       Nonce NA, Number PA, Agent A, 
 			       Nonce NB, Number PB, Agent B|}))
               # evsCR  :  tls"
 
     Oops