src/HOL/Auth/TLS.thy
author paulson
Tue Nov 11 11:16:18 1997 +0100 (1997-11-11)
changeset 4198 c63639beeff1
parent 3759 3d1ac6b82b28
child 4421 88639289be39
permissions -rw-r--r--
Fixed spelling error
     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 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 ClientKeyExch,
    25 CertVerify, ClientFinished to record that A knows M.  It is a note from A to
    26 herself.  Nobody else can see it.  In ClientKeyExch, 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 In the shared-key model, the ability to encrypt implies the ability to
    34 decrypt, so the problem does not arise.
    35 
    36 Proofs would be simpler if ClientKeyExch included A's name within
    37 Crypt KB (Nonce PMS).  As things stand, there is much overlap between proofs
    38 about that message (which B receives) and the stronger event
    39 	Notes A {|Agent B, Nonce PMS|}.
    40 *)
    41 
    42 TLS = Public + 
    43 
    44 consts
    45   (*Pseudo-random function of Section 5*)
    46   PRF  :: "nat*nat*nat => nat"
    47 
    48   (*Client, server write keys are generated uniformly by function sessionK
    49     to avoid duplicating their properties.  They are indexed by a further
    50     natural number, not a bool, to avoid the peculiarities of if-and-only-if.
    51     Session keys implicitly include MAC secrets.*)
    52   sessionK :: "(nat*nat*nat)*nat => key"
    53 
    54   certificate      :: "[agent,key] => msg"
    55 
    56 defs
    57   certificate_def
    58     "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    59 
    60 syntax
    61     clientK, serverK :: "nat*nat*nat => key"
    62 
    63 translations
    64   "clientK (nonces)"	== "sessionK(nonces,0)"
    65   "serverK (nonces)"	== "sessionK(nonces,1)"
    66 
    67 rules
    68   (*the pseudo-random function is collision-free*)
    69   inj_PRF       "inj PRF"	
    70 
    71   (*sessionK is collision-free; also, no clientK clashes with any serverK.*)
    72   inj_sessionK  "inj sessionK"	
    73 
    74   (*sessionK makes symmetric keys*)
    75   isSym_sessionK "isSymKey (sessionK nonces)"
    76 
    77 
    78 consts    tls :: event list set
    79 inductive tls
    80   intrs 
    81     Nil  (*Initial trace is empty*)
    82          "[]: tls"
    83 
    84     Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
    85          "[| evs: tls;  B ~= Spy;  
    86              X: synth (analz (spies evs)) |]
    87           ==> Says Spy B X # evs : tls"
    88 
    89     SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
    90          "[| evsSK: tls;
    91 	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
    92           ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
    93 			    Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
    94 
    95     ClientHello
    96 	 (*(7.4.1.2)
    97 	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    98 	   It is uninterpreted but will be confirmed in the FINISHED messages.
    99 	   NA is CLIENT RANDOM, while SID is SESSION_ID.
   100            UNIX TIME is omitted because the protocol doesn't use it.
   101            May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
   102 	   while MASTER SECRET is 48 bytes*)
   103          "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
   104           ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
   105 	        # evsCH  :  tls"
   106 
   107     ServerHello
   108          (*7.4.1.3 of the TLS Internet-Draft
   109 	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
   110            SERVER CERTIFICATE (7.4.2) is always present.
   111            CERTIFICATE_REQUEST (7.4.4) is implied.*)
   112          "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
   113              Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
   114 	       : set evsSH |]
   115           ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  :  tls"
   116 
   117     Certificate
   118          (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
   119          "[| evsC: tls;  A ~= B |]
   120           ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
   121 
   122     ClientKeyExch
   123          (*CLIENT KEY EXCHANGE (7.4.7).
   124            The client, A, chooses PMS, the PREMASTER SECRET.
   125            She encrypts PMS using the supplied KB, which ought to be pubK B.
   126            We assume PMS ~: range PRF because a clash betweem the PMS
   127            and another MASTER SECRET is highly unlikely (even though
   128 	   both items have the same length, 48 bytes).
   129            The Note event records in the trace that she knows PMS
   130                (see REMARK at top). *)
   131          "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
   132              Says B'  A {|Nonce NB, Number SID, Number PB|} : set evsCX;
   133              Says B'' A (certificate B KB) : set evsCX |]
   134           ==> Says A B (Crypt KB (Nonce PMS))
   135 	      # Notes A {|Agent B, Nonce PMS|}
   136 	      # evsCX  :  tls"
   137 
   138     CertVerify
   139 	(*The optional Certificate Verify (7.4.8) message contains the
   140           specific components listed in the security analysis, F.1.1.2.
   141           It adds the pre-master-secret, which is also essential!
   142           Checking the signature, which is the only use of A's certificate,
   143           assures B of A's presence*)
   144          "[| evsCV: tls;  A ~= B;  
   145              Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
   146 	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
   147           ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
   148               # evsCV  :  tls"
   149 
   150 	(*Finally come the FINISHED messages (7.4.8), confirming PA and PB
   151           among other things.  The master-secret is PRF(PMS,NA,NB).
   152           Either party may sent its message first.*)
   153 
   154     ClientFinished
   155         (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
   156           rule's applying when the Spy has satisfied the "Says A B" by
   157           repaying messages sent by the true client; in that case, the
   158           Spy does not know PMS and could not sent ClientFinished.  One
   159           could simply put A~=Spy into the rule, but one should not
   160           expect the spy to be well-behaved.*)
   161          "[| evsCF: tls;  
   162 	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
   163 	       : set evsCF;
   164              Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCF;
   165              Notes A {|Agent B, Nonce PMS|} : set evsCF;
   166 	     M = PRF(PMS,NA,NB) |]
   167           ==> Says A B (Crypt (clientK(NA,NB,M))
   168 			(Hash{|Number SID, Nonce M,
   169 			       Nonce NA, Number PA, Agent A, 
   170 			       Nonce NB, Number PB, Agent B|}))
   171               # evsCF  :  tls"
   172 
   173     ServerFinished
   174 	(*Keeping A' and A'' distinct means B cannot even check that the
   175           two messages originate from the same source. *)
   176          "[| evsSF: tls;
   177 	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
   178 	       : set evsSF;
   179 	     Says B  A  {|Nonce NB, Number SID, Number PB|} : set evsSF;
   180 	     Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF;
   181 	     M = PRF(PMS,NA,NB) |]
   182           ==> Says B A (Crypt (serverK(NA,NB,M))
   183 			(Hash{|Number SID, Nonce M,
   184 			       Nonce NA, Number PA, Agent A, 
   185 			       Nonce NB, Number PB, Agent B|}))
   186               # evsSF  :  tls"
   187 
   188     ClientAccepts
   189 	(*Having transmitted ClientFinished and received an identical
   190           message encrypted with serverK, the client stores the parameters
   191           needed to resume this session.  The "Notes A ..." premise is
   192           used to prove Notes_master_imp_Crypt_PMS.*)
   193          "[| evsCA: tls;
   194 	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
   195 	     M = PRF(PMS,NA,NB);  
   196 	     X = Hash{|Number SID, Nonce M,
   197 	               Nonce NA, Number PA, Agent A, 
   198 		       Nonce NB, Number PB, Agent B|};
   199              Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
   200              Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
   201           ==> 
   202              Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  :  tls"
   203 
   204     ServerAccepts
   205 	(*Having transmitted ServerFinished and received an identical
   206           message encrypted with clientK, the server stores the parameters
   207           needed to resume this session.  The "Says A'' B ..." premise is
   208           used to prove Notes_master_imp_Crypt_PMS.*)
   209          "[| evsSA: tls;
   210              Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
   211 	     M = PRF(PMS,NA,NB);  
   212 	     X = Hash{|Number SID, Nonce M,
   213 	               Nonce NA, Number PA, Agent A, 
   214 		       Nonce NB, Number PB, Agent B|};
   215              Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
   216              Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
   217           ==> 
   218              Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
   219 
   220     ClientResume
   221          (*If A recalls the SESSION_ID, then she sends a FINISHED message
   222            using the new nonces and stored MASTER SECRET.*)
   223          "[| evsCR: tls;  
   224 	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;
   225              Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
   226              Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
   227           ==> Says A B (Crypt (clientK(NA,NB,M))
   228 			(Hash{|Number SID, Nonce M,
   229 			       Nonce NA, Number PA, Agent A, 
   230 			       Nonce NB, Number PB, Agent B|}))
   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"
   245 
   246     Oops 
   247          (*The most plausible compromise is of an old session key.  Losing
   248            the MASTER SECRET or PREMASTER SECRET is more serious but
   249            rather unlikely.*)
   250          "[| evso: tls;  A ~= Spy;  
   251 	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
   252           ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
   253 
   254 end