src/HOL/Auth/TLS.thy
changeset 3685 5b8c0c8f576e
parent 3683 aafe719dff14
child 3686 4b484805b4c4
     1.1 --- a/src/HOL/Auth/TLS.thy	Fri Sep 19 16:11:24 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Fri Sep 19 16:12:21 1997 +0200
     1.3 @@ -30,9 +30,13 @@
     1.4  agent's state is recorded as the trace of messages.  When the true client (A)
     1.5  invents PMS, he encrypts PMS with B's public key before sending it.  The model
     1.6  does not distinguish the original occurrence of such a message from a replay.
     1.7 -
     1.8  In the shared-key model, the ability to encrypt implies the ability to
     1.9  decrypt, so the problem does not arise.
    1.10 +
    1.11 +Proofs would be simpler if ClientCertKeyEx included A's name within
    1.12 +Crypt KB (Nonce PMS).  As things stand, there is much overlap between proofs
    1.13 +about that message (which B receives) and the stronger event
    1.14 +	Notes A {|Agent B, Nonce PMS|}.
    1.15  *)
    1.16  
    1.17  TLS = Public + 
    1.18 @@ -56,8 +60,8 @@
    1.19      clientK, serverK :: "nat*nat*nat => key"
    1.20  
    1.21  translations
    1.22 -  "clientK x"	== "sessionK(True,x)"
    1.23 -  "serverK x"	== "sessionK(False,x)"
    1.24 +  "clientK (x)"	== "sessionK(True,x)"
    1.25 +  "serverK (x)"	== "sessionK(False,x)"
    1.26  
    1.27  rules
    1.28    inj_PRF       "inj PRF"	
    1.29 @@ -125,7 +129,7 @@
    1.30             and another MASTER SECRET is highly unlikely (even though
    1.31  	   both items have the same length, 48 bytes).
    1.32             The Note event records in the trace that she knows PMS
    1.33 -               (see REMARK at top).*)
    1.34 +               (see REMARK at top). *)
    1.35           "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    1.36               Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
    1.37  	       : set evsCX |]
    1.38 @@ -134,7 +138,7 @@
    1.39  	      # evsCX  :  tls"
    1.40  
    1.41      CertVerify
    1.42 -	(*The optional CERTIFICATE VERIFY (7.4.8) message contains the
    1.43 +	(*The optional Certificate Verify (7.4.8) message contains the
    1.44            specific components listed in the security analysis, F.1.1.2.
    1.45            It adds the pre-master-secret, which is also essential!
    1.46            Checking the signature, which is the only use of A's certificate,
    1.47 @@ -151,13 +155,13 @@
    1.48            among other things.  The master-secret is PRF(PMS,NA,NB).
    1.49            Either party may sent its message first.*)
    1.50  
    1.51 +    ClientFinished
    1.52          (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
    1.53            rule's applying when the Spy has satisfied the "Says A B" by
    1.54            repaying messages sent by the true client; in that case, the
    1.55 -          Spy does not know PMS and could not sent CLIENT FINISHED.  One
    1.56 +          Spy does not know PMS and could not sent ClientFinished.  One
    1.57            could simply put A~=Spy into the rule, but one should not
    1.58            expect the spy to be well-behaved.*)
    1.59 -    ClientFinished
    1.60           "[| evsCF: tls;  
    1.61  	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
    1.62  	       : set evsCF;
    1.63 @@ -171,9 +175,9 @@
    1.64  			       Nonce NB, Number XB, Agent B|}))
    1.65                # evsCF  :  tls"
    1.66  
    1.67 +    ServerFinished
    1.68  	(*Keeping A' and A'' distinct means B cannot even check that the
    1.69            two messages originate from the same source. *)
    1.70 -    ServerFinished
    1.71           "[| evsSF: tls;
    1.72  	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
    1.73  	       : set evsSF;
    1.74 @@ -189,12 +193,12 @@
    1.75  			       Nonce NB, Number XB, Agent B|}))
    1.76                # evsSF  :  tls"
    1.77  
    1.78 -	(*Having transmitted CLIENT FINISHED and received an identical
    1.79 +    ClientAccepts
    1.80 +	(*Having transmitted ClientFinished and received an identical
    1.81            message encrypted with serverK, the client stores the parameters
    1.82            needed to resume this session.*)
    1.83 -    ClientAccepts
    1.84           "[| evsCA: tls;
    1.85 -             Notes A {|Agent B, Nonce PMS|} : set evsCA;
    1.86 +	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
    1.87  	     M = PRF(PMS,NA,NB);  
    1.88  	     X = Hash{|Nonce M, Number SID,
    1.89  	               Nonce NA, Number XA, Agent A, 
    1.90 @@ -204,10 +208,10 @@
    1.91            ==> 
    1.92               Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  :  tls"
    1.93  
    1.94 -	(*Having transmitted SERVER FINISHED and received an identical
    1.95 +    ServerAccepts
    1.96 +	(*Having transmitted ServerFinished and received an identical
    1.97            message encrypted with clientK, the server stores the parameters
    1.98            needed to resume this session.*)
    1.99 -    ServerAccepts
   1.100           "[| evsSA: tls;
   1.101               Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   1.102  	       : set evsSA;
   1.103 @@ -220,6 +224,34 @@
   1.104            ==> 
   1.105               Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
   1.106  
   1.107 +    ServerResume
   1.108 +         (*Resumption is described in 7.3.  If B finds the SESSION_ID
   1.109 +           then he sends HELLO and FINISHED messages, using the
   1.110 +           previously stored MASTER SECRET*)
   1.111 +         "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
   1.112 +             Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
   1.113 +	     Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
   1.114 +	       : set evsSR |]
   1.115 +          ==> Says B A (Crypt (serverK(NA,NB,M))
   1.116 +			(Hash{|Nonce M, Number SID,
   1.117 +			       Nonce NA, Number XA, Agent A, 
   1.118 +			       Nonce NB, Number XB, Agent B|}))
   1.119 +              # Says B A {|Nonce NB, Number SID, Number XB|} # evsSR  :  tls"
   1.120 +
   1.121 +    ClientResume
   1.122 +         (*If the response to ClientHello is ServerResume then send
   1.123 +           a FINISHED message using the new nonces and stored MASTER SECRET.*)
   1.124 +         "[| evsCR: tls;  
   1.125 +	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
   1.126 +	       : set evsCR;
   1.127 +             Says B' A {|Nonce NB, Number SID, Number XB|} : set evsCR;
   1.128 +             Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
   1.129 +          ==> Says A B (Crypt (clientK(NA,NB,M))
   1.130 +			(Hash{|Nonce M, Number SID,
   1.131 +			       Nonce NA, Number XA, Agent A, 
   1.132 +			       Nonce NB, Number XB, Agent B|}))
   1.133 +              # evsCR  :  tls"
   1.134 +
   1.135    (**Oops message??**)
   1.136  
   1.137  end