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