src/HOL/Auth/TLS.thy
author paulson
Tue Sep 16 14:40:01 1997 +0200 (1997-09-16)
changeset 3676 cbaec955056b
parent 3672 56e4365a0c99
child 3677 f2569416d18b
permissions -rw-r--r--
Addition of SessionIDs to the Hello and Finished messages
     1 (*  Title:      HOL/Auth/TLS
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
     7 This protocol is essentially the same as SSL 3.0.
     8 
     9 Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
    10 Allen, Transport Layer Security Working Group, 21 May 1997,
    11 INTERNET-DRAFT draft-ietf-tls-protocol-03.txt.  Section numbers below refer
    12 to that memo.
    13 
    14 An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
    15 to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
    16 global signing authority.
    17 
    18 A is the client and B is the server, not to be confused with the constant
    19 Server, who is in charge of all public keys.
    20 
    21 The model assumes that no fraudulent certificates are present, but it does
    22 assume that some private keys are to the spy.
    23 
    24 REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
    25 CertVerify, ClientFinished to record that A knows M.  It is a note from A to
    26 herself.  Nobody else can see it.  In ClientCertKeyEx, the Spy can substitute
    27 his own certificate for A's, but he cannot replace A's note by one for himself.
    28 
    29 The Note event avoids a weakness in the public-key model.  Each
    30 agent's state is recorded as the trace of messages.  When the true client (A)
    31 invents PMS, he encrypts PMS with B's public key before sending it.  The model
    32 does not distinguish the original occurrence of such a message from a replay.
    33 
    34 In the shared-key model, the ability to encrypt implies the ability to
    35 decrypt, so the problem does not arise.
    36 *)
    37 
    38 TLS = Public + 
    39 
    40 consts
    41   (*Pseudo-random function of Section 5*)
    42   PRF  :: "nat*nat*nat => nat"
    43 
    44   (*Client, server write keys implicitly include the MAC secrets.*)
    45   clientK, serverK :: "nat*nat*nat => key"
    46 
    47   certificate      :: "[agent,key] => msg"
    48 
    49 defs
    50   certificate_def
    51     "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    52 
    53 rules
    54   inj_PRF       "inj PRF"	
    55 
    56   (*clientK is collision-free and makes symmetric keys*)
    57   inj_clientK   "inj clientK"	
    58   isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
    59 
    60   (*serverK is similar*)
    61   inj_serverK   "inj serverK"	
    62   isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
    63 
    64   (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
    65   clientK_range "range clientK <= Compl (range serverK)"
    66 
    67 
    68 consts    tls :: event list set
    69 inductive tls
    70   intrs 
    71     Nil  (*Initial trace is empty*)
    72          "[]: tls"
    73 
    74     Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
    75          "[| evs: tls;  B ~= Spy;  
    76              X: synth (analz (sees Spy evs)) |]
    77           ==> Says Spy B X # evs : tls"
    78 
    79     SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
    80          "[| evsSK: tls;
    81 	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
    82           ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
    83 			    Key (clientK(NA,NB,M)),
    84 			    Key (serverK(NA,NB,M)) |} # evsSK : tls"
    85 
    86     ClientHello
    87 	 (*(7.4.1.2)
    88 	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    89 	   It is uninterpreted but will be confirmed in the FINISHED messages.
    90 	   NA is CLIENT RANDOM, while SID is SESSION_ID.
    91            UNIX TIME is omitted because the protocol doesn't use it.
    92            May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
    93 	   while MASTER SECRET is 48 byptes*)
    94          "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    95           ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
    96 	        # evsCH  :  tls"
    97 
    98     ServerHello
    99          (*7.4.1.3 of the TLS Internet-Draft
   100 	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
   101            SERVER CERTIFICATE (7.4.2) is always present.
   102            CERTIFICATE_REQUEST (7.4.4) is implied.*)
   103          "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
   104              Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
   105 	       : set evsSH |]
   106           ==> Says B A {|Nonce NB, Number SID, Number XB,
   107 			 certificate B (pubK B)|}
   108                 # evsSH  :  tls"
   109 
   110     ClientCertKeyEx
   111          (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
   112            The client, A, chooses PMS, the PREMASTER SECRET.
   113            She encrypts PMS using the supplied KB, which ought to be pubK B.
   114            We assume PMS ~: range PRF because a clash betweem the PMS
   115            and another MASTER SECRET is highly unlikely (even though
   116 	   both items have the same length, 48 bytes).
   117            The Note event records in the trace that she knows PMS
   118                (see REMARK at top).*)
   119          "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
   120              Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
   121 	       : set evsCX |]
   122           ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
   123 	      # Notes A {|Agent B, Nonce PMS|}
   124 	      # evsCX  :  tls"
   125 
   126     CertVerify
   127 	(*The optional CERTIFICATE VERIFY (7.4.8) message contains the
   128           specific components listed in the security analysis, F.1.1.2.
   129           It adds the pre-master-secret, which is also essential!
   130           Checking the signature, which is the only use of A's certificate,
   131           assures B of A's presence*)
   132          "[| evsCV: tls;  A ~= B;  
   133              Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
   134 	       : set evsCV;
   135 	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
   136           ==> Says A B (Crypt (priK A)
   137 			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
   138               # evsCV  :  tls"
   139 
   140 	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
   141           among other things.  The master-secret is PRF(PMS,NA,NB).
   142           Either party may sent its message first.*)
   143 
   144         (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
   145           rule's applying when the Spy has satisfied the "Says A B" by
   146           repaying messages sent by the true client; in that case, the
   147           Spy does not know PMS and could not sent CLIENT FINISHED.  One
   148           could simply put A~=Spy into the rule, but one should not
   149           expect the spy to be well-behaved.*)
   150     ClientFinished
   151          "[| evsCF: tls;  
   152 	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
   153 	       : set evsCF;
   154              Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
   155 	       : set evsCF;
   156              Notes A {|Agent B, Nonce PMS|} : set evsCF;
   157 	     M = PRF(PMS,NA,NB) |]
   158           ==> Says A B (Crypt (clientK(NA,NB,M))
   159 			(Hash{|Nonce M, Number SID,
   160 			       Nonce NA, Number XA, Agent A, 
   161 			       Nonce NB, Number XB, Agent B|}))
   162               # evsCF  :  tls"
   163 
   164 	(*Keeping A' and A'' distinct means B cannot even check that the
   165           two messages originate from the same source. *)
   166     ServerFinished
   167          "[| evsSF: tls;
   168 	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
   169 	       : set evsSF;
   170 	     Says B  A  {|Nonce NB, Number SID, Number XB,
   171 		 	  certificate B (pubK B)|}
   172 	       : set evsSF;
   173 	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   174 	       : set evsSF;
   175 	     M = PRF(PMS,NA,NB) |]
   176           ==> Says B A (Crypt (serverK(NA,NB,M))
   177 			(Hash{|Nonce M, Number SID,
   178 			       Nonce NA, Number XA, Agent A, 
   179 			       Nonce NB, Number XB, Agent B|}))
   180               # evsSF  :  tls"
   181 
   182   (**Oops message??**)
   183 
   184 end