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