Exchanged the M and SID fields of the FINISHED messages to simplify proofs
authorpaulson
Wed Oct 01 12:07:07 1997 +0200 (1997-10-01)
changeset 37577524781c5c83
parent 3756 5617a5698345
child 3758 188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.thy	Wed Oct 01 11:30:55 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Wed Oct 01 12:07:07 1997 +0200
     1.3 @@ -165,7 +165,7 @@
     1.4               Notes A {|Agent B, Nonce PMS|} : set evsCF;
     1.5  	     M = PRF(PMS,NA,NB) |]
     1.6            ==> Says A B (Crypt (clientK(NA,NB,M))
     1.7 -			(Hash{|Nonce M, Number SID,
     1.8 +			(Hash{|Number SID, Nonce M,
     1.9  			       Nonce NA, Number PA, Agent A, 
    1.10  			       Nonce NB, Number PB, Agent B|}))
    1.11                # evsCF  :  tls"
    1.12 @@ -180,7 +180,7 @@
    1.13  	     Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF;
    1.14  	     M = PRF(PMS,NA,NB) |]
    1.15            ==> Says B A (Crypt (serverK(NA,NB,M))
    1.16 -			(Hash{|Nonce M, Number SID,
    1.17 +			(Hash{|Number SID, Nonce M,
    1.18  			       Nonce NA, Number PA, Agent A, 
    1.19  			       Nonce NB, Number PB, Agent B|}))
    1.20                # evsSF  :  tls"
    1.21 @@ -193,7 +193,7 @@
    1.22           "[| evsCA: tls;
    1.23  	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
    1.24  	     M = PRF(PMS,NA,NB);  
    1.25 -	     X = Hash{|Nonce M, Number SID,
    1.26 +	     X = Hash{|Number SID, Nonce M,
    1.27  	               Nonce NA, Number PA, Agent A, 
    1.28  		       Nonce NB, Number PB, Agent B|};
    1.29               Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
    1.30 @@ -209,7 +209,7 @@
    1.31           "[| evsSA: tls;
    1.32               Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
    1.33  	     M = PRF(PMS,NA,NB);  
    1.34 -	     X = Hash{|Nonce M, Number SID,
    1.35 +	     X = Hash{|Number SID, Nonce M,
    1.36  	               Nonce NA, Number PA, Agent A, 
    1.37  		       Nonce NB, Number PB, Agent B|};
    1.38               Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
    1.39 @@ -225,7 +225,7 @@
    1.40  	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.41  	       : set evsSR |]
    1.42            ==> Says B A (Crypt (serverK(NA,NB,M))
    1.43 -			(Hash{|Nonce M, Number SID,
    1.44 +			(Hash{|Number SID, Nonce M,
    1.45  			       Nonce NA, Number PA, Agent A, 
    1.46  			       Nonce NB, Number PB, Agent B|})) # evsSR
    1.47  	        :  tls"
    1.48 @@ -239,7 +239,7 @@
    1.49               Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
    1.50               Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
    1.51            ==> Says A B (Crypt (clientK(NA,NB,M))
    1.52 -			(Hash{|Nonce M, Number SID,
    1.53 +			(Hash{|Number SID, Nonce M,
    1.54  			       Nonce NA, Number PA, Agent A, 
    1.55  			       Nonce NB, Number PB, Agent B|}))
    1.56                # evsCR  :  tls"