src/HOL/Auth/TLS.thy
changeset 3759 3d1ac6b82b28
parent 3757 7524781c5c83
child 4198 c63639beeff1
equal deleted inserted replaced
3758:188a4fbfaf55 3759:3d1ac6b82b28
     1 (*  Title:      HOL/Auth/TLS
     1 (*  Title:      HOL/Auth/TLS
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     4     Copyright   1997  University of Cambridge
     5 
     5 
     6 Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
     6 Inductive relation "tls" for the TLS (Transport Layer Security) protocol.
     7 This protocol is essentially the same as SSL 3.0.
     7 This protocol is essentially the same as SSL 3.0.
     8 
     8 
     9 Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
     9 Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
    10 Allen, Transport Layer Security Working Group, 21 May 1997,
    10 Allen, Transport Layer Security Working Group, 21 May 1997,
    11 INTERNET-DRAFT draft-ietf-tls-protocol-03.txt.  Section numbers below refer
    11 INTERNET-DRAFT draft-ietf-tls-protocol-03.txt.  Section numbers below refer
   215              Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
   215              Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
   216              Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
   216              Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
   217           ==> 
   217           ==> 
   218              Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
   218              Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
   219 
   219 
   220     ServerResume
       
   221          (*Resumption (7.3):  If B finds the SESSION_ID then he can send
       
   222            a FINISHED message using the recovered MASTER SECRET*)
       
   223          "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
       
   224              Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
       
   225 	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
       
   226 	       : set evsSR |]
       
   227           ==> Says B A (Crypt (serverK(NA,NB,M))
       
   228 			(Hash{|Number SID, Nonce M,
       
   229 			       Nonce NA, Number PA, Agent A, 
       
   230 			       Nonce NB, Number PB, Agent B|})) # evsSR
       
   231 	        :  tls"
       
   232 
       
   233     ClientResume
   220     ClientResume
   234          (*If A recalls the SESSION_ID, then she sends a FINISHED message
   221          (*If A recalls the SESSION_ID, then she sends a FINISHED message
   235            using the new nonces and stored MASTER SECRET.*)
   222            using the new nonces and stored MASTER SECRET.*)
   236          "[| evsCR: tls;  
   223          "[| evsCR: tls;  
   237 	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
   224 	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
   238 	       : set evsCR;
       
   239              Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
   225              Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
   240              Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
   226              Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
   241           ==> Says A B (Crypt (clientK(NA,NB,M))
   227           ==> Says A B (Crypt (clientK(NA,NB,M))
   242 			(Hash{|Number SID, Nonce M,
   228 			(Hash{|Number SID, Nonce M,
   243 			       Nonce NA, Number PA, Agent A, 
   229 			       Nonce NA, Number PA, Agent A, 
   244 			       Nonce NB, Number PB, Agent B|}))
   230 			       Nonce NB, Number PB, Agent B|}))
   245               # evsCR  :  tls"
   231               # evsCR  :  tls"
       
   232 
       
   233     ServerResume
       
   234          (*Resumption (7.3):  If B finds the SESSION_ID then he can send
       
   235            a FINISHED message using the recovered MASTER SECRET*)
       
   236          "[| evsSR: tls;
       
   237 	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;
       
   238 	     Says B  A {|Nonce NB, Number SID, Number PB|} : set evsSR;  
       
   239              Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR |]
       
   240           ==> Says B A (Crypt (serverK(NA,NB,M))
       
   241 			(Hash{|Number SID, Nonce M,
       
   242 			       Nonce NA, Number PA, Agent A, 
       
   243 			       Nonce NB, Number PB, Agent B|})) # evsSR
       
   244 	        :  tls"
   246 
   245 
   247     Oops 
   246     Oops 
   248          (*The most plausible compromise is of an old session key.  Losing
   247          (*The most plausible compromise is of an old session key.  Losing
   249            the MASTER SECRET or PREMASTER SECRET is more serious but
   248            the MASTER SECRET or PREMASTER SECRET is more serious but
   250            rather unlikely.*)
   249            rather unlikely.*)