src/HOL/Auth/TLS.thy
author paulson
Thu Sep 18 13:24:04 1997 +0200 (1997-09-18)
changeset 3683 aafe719dff14
parent 3677 f2569416d18b
child 3685 5b8c0c8f576e
permissions -rw-r--r--
Global change: lost->bad and sees Spy->spies
First change just gives a more sensible name.
Second change eliminates the agent parameter of "sees" to simplify
definitions and theorems
     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 generated uniformly by function sessionK
    45     to avoid duplicating their properties.
    46     Theyimplicitly include the MAC secrets.*)
    47   sessionK :: "bool*nat*nat*nat => key"
    48 
    49   certificate      :: "[agent,key] => msg"
    50 
    51 defs
    52   certificate_def
    53     "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    54 
    55 syntax
    56     clientK, serverK :: "nat*nat*nat => key"
    57 
    58 translations
    59   "clientK x"	== "sessionK(True,x)"
    60   "serverK x"	== "sessionK(False,x)"
    61 
    62 rules
    63   inj_PRF       "inj PRF"	
    64 
    65   (*sessionK is collision-free and makes symmetric keys*)
    66   inj_sessionK  "inj sessionK"	
    67 
    68   isSym_sessionK "isSymKey (sessionK x)"
    69 
    70   (*serverK is similar*)
    71   inj_serverK   "inj serverK"	
    72   isSym_serverK "isSymKey (serverK x)"
    73 
    74   (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
    75   clientK_range "range clientK <= Compl (range serverK)"
    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, clientK & serverK 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 (clientK(NA,NB,M)),
    94 			    Key (serverK(NA,NB,M)) |} # evsSK : tls"
    95 
    96     ClientHello
    97 	 (*(7.4.1.2)
    98 	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    99 	   It is uninterpreted but will be confirmed in the FINISHED messages.
   100 	   NA is CLIENT RANDOM, while SID is SESSION_ID.
   101            UNIX TIME is omitted because the protocol doesn't use it.
   102            May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
   103 	   while MASTER SECRET is 48 byptes*)
   104          "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
   105           ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
   106 	        # evsCH  :  tls"
   107 
   108     ServerHello
   109          (*7.4.1.3 of the TLS Internet-Draft
   110 	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
   111            SERVER CERTIFICATE (7.4.2) is always present.
   112            CERTIFICATE_REQUEST (7.4.4) is implied.*)
   113          "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
   114              Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
   115 	       : set evsSH |]
   116           ==> Says B A {|Nonce NB, Number SID, Number XB,
   117 			 certificate B (pubK B)|}
   118                 # evsSH  :  tls"
   119 
   120     ClientCertKeyEx
   121          (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
   122            The client, A, chooses PMS, the PREMASTER SECRET.
   123            She encrypts PMS using the supplied KB, which ought to be pubK B.
   124            We assume PMS ~: range PRF because a clash betweem the PMS
   125            and another MASTER SECRET is highly unlikely (even though
   126 	   both items have the same length, 48 bytes).
   127            The Note event records in the trace that she knows PMS
   128                (see REMARK at top).*)
   129          "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
   130              Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
   131 	       : set evsCX |]
   132           ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
   133 	      # Notes A {|Agent B, Nonce PMS|}
   134 	      # evsCX  :  tls"
   135 
   136     CertVerify
   137 	(*The optional CERTIFICATE VERIFY (7.4.8) message contains the
   138           specific components listed in the security analysis, F.1.1.2.
   139           It adds the pre-master-secret, which is also essential!
   140           Checking the signature, which is the only use of A's certificate,
   141           assures B of A's presence*)
   142          "[| evsCV: tls;  A ~= B;  
   143              Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
   144 	       : set evsCV;
   145 	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
   146           ==> Says A B (Crypt (priK A)
   147 			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
   148               # evsCV  :  tls"
   149 
   150 	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
   151           among other things.  The master-secret is PRF(PMS,NA,NB).
   152           Either party may sent its message first.*)
   153 
   154         (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
   155           rule's applying when the Spy has satisfied the "Says A B" by
   156           repaying messages sent by the true client; in that case, the
   157           Spy does not know PMS and could not sent CLIENT FINISHED.  One
   158           could simply put A~=Spy into the rule, but one should not
   159           expect the spy to be well-behaved.*)
   160     ClientFinished
   161          "[| evsCF: tls;  
   162 	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
   163 	       : set evsCF;
   164              Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
   165 	       : set evsCF;
   166              Notes A {|Agent B, Nonce PMS|} : set evsCF;
   167 	     M = PRF(PMS,NA,NB) |]
   168           ==> Says A B (Crypt (clientK(NA,NB,M))
   169 			(Hash{|Nonce M, Number SID,
   170 			       Nonce NA, Number XA, Agent A, 
   171 			       Nonce NB, Number XB, Agent B|}))
   172               # evsCF  :  tls"
   173 
   174 	(*Keeping A' and A'' distinct means B cannot even check that the
   175           two messages originate from the same source. *)
   176     ServerFinished
   177          "[| evsSF: tls;
   178 	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
   179 	       : set evsSF;
   180 	     Says B  A  {|Nonce NB, Number SID, Number XB,
   181 		 	  certificate B (pubK B)|}
   182 	       : set evsSF;
   183 	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   184 	       : set evsSF;
   185 	     M = PRF(PMS,NA,NB) |]
   186           ==> Says B A (Crypt (serverK(NA,NB,M))
   187 			(Hash{|Nonce M, Number SID,
   188 			       Nonce NA, Number XA, Agent A, 
   189 			       Nonce NB, Number XB, Agent B|}))
   190               # evsSF  :  tls"
   191 
   192 	(*Having transmitted CLIENT FINISHED and received an identical
   193           message encrypted with serverK, the client stores the parameters
   194           needed to resume this session.*)
   195     ClientAccepts
   196          "[| evsCA: tls;
   197              Notes A {|Agent B, Nonce PMS|} : set evsCA;
   198 	     M = PRF(PMS,NA,NB);  
   199 	     X = Hash{|Nonce M, Number SID,
   200 	               Nonce NA, Number XA, Agent A, 
   201 		       Nonce NB, Number XB, Agent B|};
   202              Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
   203              Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
   204           ==> 
   205              Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  :  tls"
   206 
   207 	(*Having transmitted SERVER FINISHED and received an identical
   208           message encrypted with clientK, the server stores the parameters
   209           needed to resume this session.*)
   210     ServerAccepts
   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   (**Oops message??**)
   224 
   225 end