Fixed ServerResume to check for ServerHello instead of making a new NB
authorpaulson
Wed Oct 01 13:41:38 1997 +0200 (1997-10-01)
changeset 37593d1ac6b82b28
parent 3758 188a4fbfaf55
child 3760 77f71f650433
Fixed ServerResume to check for ServerHello instead of making a new NB
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.thy	Wed Oct 01 12:07:24 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Wed Oct 01 13:41:38 1997 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1997  University of Cambridge
     1.6  
     1.7 -Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
     1.8 +Inductive relation "tls" for the TLS (Transport Layer Security) protocol.
     1.9  This protocol is essentially the same as SSL 3.0.
    1.10  
    1.11  Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
    1.12 @@ -217,25 +217,11 @@
    1.13            ==> 
    1.14               Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
    1.15  
    1.16 -    ServerResume
    1.17 -         (*Resumption (7.3):  If B finds the SESSION_ID then he can send
    1.18 -           a FINISHED message using the recovered MASTER SECRET*)
    1.19 -         "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
    1.20 -             Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
    1.21 -	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.22 -	       : set evsSR |]
    1.23 -          ==> Says B A (Crypt (serverK(NA,NB,M))
    1.24 -			(Hash{|Number SID, Nonce M,
    1.25 -			       Nonce NA, Number PA, Agent A, 
    1.26 -			       Nonce NB, Number PB, Agent B|})) # evsSR
    1.27 -	        :  tls"
    1.28 -
    1.29      ClientResume
    1.30           (*If A recalls the SESSION_ID, then she sends a FINISHED message
    1.31             using the new nonces and stored MASTER SECRET.*)
    1.32           "[| evsCR: tls;  
    1.33 -	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
    1.34 -	       : set evsCR;
    1.35 +	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
    1.36               Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
    1.37               Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
    1.38            ==> Says A B (Crypt (clientK(NA,NB,M))
    1.39 @@ -244,6 +230,19 @@
    1.40  			       Nonce NB, Number PB, Agent B|}))
    1.41                # evsCR  :  tls"
    1.42  
    1.43 +    ServerResume
    1.44 +         (*Resumption (7.3):  If B finds the SESSION_ID then he can send
    1.45 +           a FINISHED message using the recovered MASTER SECRET*)
    1.46 +         "[| evsSR: tls;
    1.47 +	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
    1.48 +	     Says B  A {|Nonce NB, Number SID, Number PB|} : set evsSR;  
    1.49 +             Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR |]
    1.50 +          ==> Says B A (Crypt (serverK(NA,NB,M))
    1.51 +			(Hash{|Number SID, Nonce M,
    1.52 +			       Nonce NA, Number PA, Agent A, 
    1.53 +			       Nonce NB, Number PB, Agent B|})) # evsSR
    1.54 +	        :  tls"
    1.55 +
    1.56      Oops 
    1.57           (*The most plausible compromise is of an old session key.  Losing
    1.58             the MASTER SECRET or PREMASTER SECRET is more serious but