# HG changeset patch
# User paulson
# Date 875700427 -7200
# Node ID 7524781c5c83c0e88f6d63c301db6bb02097e74f
# Parent  5617a56983453da143e9031cfcdce7cab7e57b81
Exchanged the M and SID fields of the FINISHED messages to simplify proofs

diff -r 5617a5698345 -r 7524781c5c83 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Wed Oct 01 11:30:55 1997 +0200
+++ b/src/HOL/Auth/TLS.thy	Wed Oct 01 12:07:07 1997 +0200
@@ -165,7 +165,7 @@
              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"
@@ -180,7 +180,7 @@
 	     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"
@@ -193,7 +193,7 @@
          "[| 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;
@@ -209,7 +209,7 @@
          "[| 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;
@@ -225,7 +225,7 @@
 	     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"
@@ -239,7 +239,7 @@
              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"