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