src/HOL/Auth/TLS.thy
changeset 3672 56e4365a0c99
parent 3519 ab0a9fbed4c0
child 3676 cbaec955056b
     1.1 --- a/src/HOL/Auth/TLS.thy	Fri Sep 12 10:45:51 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 16 13:32:22 1997 +0200
     1.3 @@ -4,6 +4,12 @@
     1.4      Copyright   1997  University of Cambridge
     1.5  
     1.6  Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
     1.7 +This protocol is essentially the same as SSL 3.0.
     1.8 +
     1.9 +Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
    1.10 +Allen, Transport Layer Security Working Group, 21 May 1997,
    1.11 +INTERNET-DRAFT draft-ietf-tls-protocol-03.txt.  Section numbers below refer
    1.12 +to that memo.
    1.13  
    1.14  An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
    1.15  to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
    1.16 @@ -15,18 +21,14 @@
    1.17  The model assumes that no fraudulent certificates are present, but it does
    1.18  assume that some private keys are to the spy.
    1.19  
    1.20 -Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
    1.21 -Allen, Transport Layer Security Working Group, 21 May 1997,
    1.22 -INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
    1.23 -
    1.24 -NOTE.  The event "Notes A {|Agent B, Nonce M|}" appears in ClientCertKeyEx,
    1.25 +REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
    1.26  CertVerify, ClientFinished to record that A knows M.  It is a note from A to
    1.27  herself.  Nobody else can see it.  In ClientCertKeyEx, the Spy can substitute
    1.28  his own certificate for A's, but he cannot replace A's note by one for himself.
    1.29  
    1.30 -The note is needed because of a weakness in the public-key model.  Each
    1.31 +The Note event avoids a weakness in the public-key model.  Each
    1.32  agent's state is recorded as the trace of messages.  When the true client (A)
    1.33 -invents M, he encrypts M with B's public key before sending it.  The model
    1.34 +invents PMS, he encrypts PMS with B's public key before sending it.  The model
    1.35  does not distinguish the original occurrence of such a message from a replay.
    1.36  
    1.37  In the shared-key model, the ability to encrypt implies the ability to
    1.38 @@ -36,8 +38,12 @@
    1.39  TLS = Public + 
    1.40  
    1.41  consts
    1.42 -  (*Client, server write keys.  They implicitly include the MAC secrets.*)
    1.43 +  (*Pseudo-random function of Section 5*)
    1.44 +  PRF  :: "nat*nat*nat => nat"
    1.45 +
    1.46 +  (*Client, server write keys implicitly include the MAC secrets.*)
    1.47    clientK, serverK :: "nat*nat*nat => key"
    1.48 +
    1.49    certificate      :: "[agent,key] => msg"
    1.50  
    1.51  defs
    1.52 @@ -45,6 +51,8 @@
    1.53      "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    1.54  
    1.55  rules
    1.56 +  inj_PRF       "inj PRF"	
    1.57 +
    1.58    (*clientK is collision-free and makes symmetric keys*)
    1.59    inj_clientK   "inj clientK"	
    1.60    isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
    1.61 @@ -68,95 +76,105 @@
    1.62               X: synth (analz (sees Spy evs)) |]
    1.63            ==> Says Spy B X # evs : tls"
    1.64  
    1.65 -    SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
    1.66 -         "[| evs: tls;
    1.67 -	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evs |]
    1.68 -          ==> Says Spy B {| Key (clientK(NA,NB,M)),
    1.69 -			    Key (serverK(NA,NB,M)) |} # evs : tls"
    1.70 +    SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
    1.71 +         "[| evsSK: tls;
    1.72 +	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
    1.73 +          ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
    1.74 +			    Key (clientK(NA,NB,M)),
    1.75 +			    Key (serverK(NA,NB,M)) |} # evsSK : tls"
    1.76  
    1.77      ClientHello
    1.78 -	 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    1.79 +	 (*(7.4.1.2)
    1.80 +	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    1.81  	   It is uninterpreted but will be confirmed in the FINISHED messages.
    1.82  	   As an initial simplification, SESSION_ID is identified with NA
    1.83 -           and reuse of sessions is not supported.*)
    1.84 -         "[| evs: tls;  A ~= B;  Nonce NA ~: used evs |]
    1.85 -          ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs  :  tls"
    1.86 +           and reuse of sessions is not supported.
    1.87 +           May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes
    1.88 +	   while MASTER SECRET is 48 byptes (6.1)*)
    1.89 +         "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    1.90 +          ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH  :  tls"
    1.91  
    1.92      ServerHello
    1.93 -         (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.94 -	   NA is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
    1.95 -	   implied and a SERVER CERTIFICATE is always present.*)
    1.96 -         "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
    1.97 -             Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
    1.98 -          ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
    1.99 +         (*7.4.1.3 of the TLS Internet-Draft
   1.100 +	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
   1.101 +	   NA is returned in its role as SESSION_ID.
   1.102 +           SERVER CERTIFICATE (7.4.2) is always present.
   1.103 +           CERTIFICATE_REQUEST (7.4.4) is implied.*)
   1.104 +         "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
   1.105 +             Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSH |]
   1.106 +          ==> Says B A {|Nonce NA, Nonce NB, Number XB,
   1.107  			 certificate B (pubK B)|}
   1.108 -                # evs  :  tls"
   1.109 +                # evsSH  :  tls"
   1.110  
   1.111      ClientCertKeyEx
   1.112 -         (*CLIENT CERTIFICATE and KEY EXCHANGE.  The client, A, chooses M,
   1.113 -           the pre-master-secret.  She encrypts M using the supplied KB,
   1.114 -           which ought to be pubK B, and also with her own public key,
   1.115 -           to record in the trace that she knows M (see NOTE at top).*)
   1.116 -         "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
   1.117 -             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
   1.118 -	       : set evs |]
   1.119 -          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
   1.120 -	      # Notes A {|Agent B, Nonce M|}
   1.121 -	      # evs  :  tls"
   1.122 +         (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
   1.123 +           The client, A, chooses PMS, the PREMASTER SECRET.
   1.124 +           She encrypts PMS using the supplied KB, which ought to be pubK B.
   1.125 +           We assume PMS ~: range PRF because a clash betweem the PMS
   1.126 +           and another MASTER SECRET is highly unlikely (even though
   1.127 +	   both items have the same length, 48 bytes).
   1.128 +           The Note event records in the trace that she knows PMS
   1.129 +               (see REMARK at top).*)
   1.130 +         "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
   1.131 +             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
   1.132 +	       : set evsCX |]
   1.133 +          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
   1.134 +	      # Notes A {|Agent B, Nonce PMS|}
   1.135 +	      # evsCX  :  tls"
   1.136  
   1.137      CertVerify
   1.138 -	(*The optional CERTIFICATE VERIFY message contains the specific
   1.139 -          components listed in the security analysis, Appendix F.1.1.2;
   1.140 -          it also contains the pre-master-secret.  Checking the signature,
   1.141 -          which is the only use of A's certificate, assures B of A's presence*)
   1.142 -         "[| evs: tls;  A ~= B;  
   1.143 -             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
   1.144 -	       : set evs;
   1.145 -	     Notes A {|Agent B, Nonce M|} : set evs |]
   1.146 +	(*The optional CERTIFICATE VERIFY (7.4.8) message contains the
   1.147 +          specific components listed in the security analysis, F.1.1.2.
   1.148 +          It adds the pre-master-secret, which is also essential!
   1.149 +          Checking the signature, which is the only use of A's certificate,
   1.150 +          assures B of A's presence*)
   1.151 +         "[| evsCV: tls;  A ~= B;  
   1.152 +             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
   1.153 +	       : set evsCV;
   1.154 +	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
   1.155            ==> Says A B (Crypt (priK A)
   1.156 -			(Hash{|Nonce NB, certificate B KB, Nonce M|}))
   1.157 -                # evs  :  tls"
   1.158 +			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
   1.159 +                # evsCV  :  tls"
   1.160  
   1.161 -	(*Finally come the FINISHED messages, confirming XA and XB among
   1.162 -          other things.  The master-secret is the hash of NA, NB and M.
   1.163 +	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
   1.164 +          among other things.  The master-secret is PRF(PMS,NA,NB).
   1.165            Either party may sent its message first.*)
   1.166  
   1.167 -        (*The occurrence of Crypt (pubK A) {|Agent B, Nonce M|} stops the 
   1.168 +        (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
   1.169            rule's applying when the Spy has satisfied the "Says A B" by
   1.170            repaying messages sent by the true client; in that case, the
   1.171 -          Spy does not know M and could not sent CLIENT FINISHED.  One
   1.172 +          Spy does not know PMS and could not sent CLIENT FINISHED.  One
   1.173            could simply put A~=Spy into the rule, but one should not
   1.174            expect the spy to be well-behaved.*)
   1.175      ClientFinished
   1.176 -         "[| evs: tls;  A ~= B;
   1.177 -	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
   1.178 -             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
   1.179 -	       : set evs;
   1.180 -             Notes A {|Agent B, Nonce M|} : set evs |]
   1.181 +         "[| evsCF: tls;  
   1.182 +	     Says A  B {|Agent A, Nonce NA, Number XA|} : set evsCF;
   1.183 +             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
   1.184 +	       : set evsCF;
   1.185 +             Notes A {|Agent B, Nonce PMS|} : set evsCF;
   1.186 +	     M = PRF(PMS,NA,NB) |]
   1.187            ==> Says A B (Crypt (clientK(NA,NB,M))
   1.188 -			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   1.189 -			       Nonce NA, Agent XA,
   1.190 -			       certificate A (pubK A), 
   1.191 -			       Nonce NB, Agent XB, Agent B|}))
   1.192 -                # evs  :  tls"
   1.193 +			(Hash{|Nonce M,
   1.194 +			       Nonce NA, Number XA, Agent A, 
   1.195 +			       Nonce NB, Number XB, Agent B|}))
   1.196 +                # evsCF  :  tls"
   1.197  
   1.198  	(*Keeping A' and A'' distinct means B cannot even check that the
   1.199 -          two messages originate from the same source.  B does not attempt
   1.200 -          to read A's encrypted "note to herself".*)
   1.201 +          two messages originate from the same source. *)
   1.202      ServerFinished
   1.203 -         "[| evs: tls;  A ~= B;
   1.204 -	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
   1.205 -	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
   1.206 +         "[| evsSF: tls;
   1.207 +	     Says A' B  {|Agent A, Nonce NA, Number XA|} : set evsSF;
   1.208 +	     Says B  A  {|Nonce NA, Nonce NB, Number XB,
   1.209  		 	  certificate B (pubK B)|}
   1.210 -	       : set evs;
   1.211 -	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce M)|}
   1.212 -	       : set evs |]
   1.213 +	       : set evsSF;
   1.214 +	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   1.215 +	       : set evsSF;
   1.216 +	     M = PRF(PMS,NA,NB) |]
   1.217            ==> Says B A (Crypt (serverK(NA,NB,M))
   1.218 -			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   1.219 -			       Nonce NA, Agent XA, Agent A, 
   1.220 -			       Nonce NB, Agent XB,
   1.221 -			       certificate B (pubK B)|}))
   1.222 -                # evs  :  tls"
   1.223 +			(Hash{|Nonce M,
   1.224 +			       Nonce NA, Number XA, Agent A, 
   1.225 +			       Nonce NB, Number XB, Agent B|}))
   1.226 +                # evsSF  :  tls"
   1.227  
   1.228    (**Oops message??**)
   1.229