src/HOL/Auth/TLS.thy
author paulson
Fri Sep 19 16:12:21 1997 +0200 (1997-09-19)
changeset 3685 5b8c0c8f576e
parent 3683 aafe719dff14
child 3686 4b484805b4c4
permissions -rw-r--r--
Full version of TLS including session resumption, but no Oops
paulson@3474
     1
(*  Title:      HOL/Auth/TLS
paulson@3474
     2
    ID:         $Id$
paulson@3474
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3474
     4
    Copyright   1997  University of Cambridge
paulson@3474
     5
paulson@3474
     6
Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
paulson@3672
     7
This protocol is essentially the same as SSL 3.0.
paulson@3672
     8
paulson@3672
     9
Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
paulson@3672
    10
Allen, Transport Layer Security Working Group, 21 May 1997,
paulson@3672
    11
INTERNET-DRAFT draft-ietf-tls-protocol-03.txt.  Section numbers below refer
paulson@3672
    12
to that memo.
paulson@3474
    13
paulson@3474
    14
An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
paulson@3474
    15
to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
paulson@3474
    16
global signing authority.
paulson@3474
    17
paulson@3474
    18
A is the client and B is the server, not to be confused with the constant
paulson@3474
    19
Server, who is in charge of all public keys.
paulson@3474
    20
paulson@3480
    21
The model assumes that no fraudulent certificates are present, but it does
paulson@3519
    22
assume that some private keys are to the spy.
paulson@3474
    23
paulson@3672
    24
REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
paulson@3515
    25
CertVerify, ClientFinished to record that A knows M.  It is a note from A to
paulson@3515
    26
herself.  Nobody else can see it.  In ClientCertKeyEx, the Spy can substitute
paulson@3515
    27
his own certificate for A's, but he cannot replace A's note by one for himself.
paulson@3515
    28
paulson@3672
    29
The Note event avoids a weakness in the public-key model.  Each
paulson@3515
    30
agent's state is recorded as the trace of messages.  When the true client (A)
paulson@3672
    31
invents PMS, he encrypts PMS with B's public key before sending it.  The model
paulson@3515
    32
does not distinguish the original occurrence of such a message from a replay.
paulson@3515
    33
In the shared-key model, the ability to encrypt implies the ability to
paulson@3515
    34
decrypt, so the problem does not arise.
paulson@3685
    35
paulson@3685
    36
Proofs would be simpler if ClientCertKeyEx included A's name within
paulson@3685
    37
Crypt KB (Nonce PMS).  As things stand, there is much overlap between proofs
paulson@3685
    38
about that message (which B receives) and the stronger event
paulson@3685
    39
	Notes A {|Agent B, Nonce PMS|}.
paulson@3474
    40
*)
paulson@3474
    41
paulson@3474
    42
TLS = Public + 
paulson@3474
    43
paulson@3474
    44
consts
paulson@3672
    45
  (*Pseudo-random function of Section 5*)
paulson@3672
    46
  PRF  :: "nat*nat*nat => nat"
paulson@3672
    47
paulson@3677
    48
  (*Client, server write keys generated uniformly by function sessionK
paulson@3677
    49
    to avoid duplicating their properties.
paulson@3677
    50
    Theyimplicitly include the MAC secrets.*)
paulson@3677
    51
  sessionK :: "bool*nat*nat*nat => key"
paulson@3672
    52
paulson@3500
    53
  certificate      :: "[agent,key] => msg"
paulson@3500
    54
paulson@3500
    55
defs
paulson@3500
    56
  certificate_def
paulson@3500
    57
    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
paulson@3474
    58
paulson@3677
    59
syntax
paulson@3677
    60
    clientK, serverK :: "nat*nat*nat => key"
paulson@3677
    61
paulson@3677
    62
translations
paulson@3685
    63
  "clientK (x)"	== "sessionK(True,x)"
paulson@3685
    64
  "serverK (x)"	== "sessionK(False,x)"
paulson@3677
    65
paulson@3474
    66
rules
paulson@3672
    67
  inj_PRF       "inj PRF"	
paulson@3672
    68
paulson@3677
    69
  (*sessionK is collision-free and makes symmetric keys*)
paulson@3677
    70
  inj_sessionK  "inj sessionK"	
paulson@3677
    71
paulson@3677
    72
  isSym_sessionK "isSymKey (sessionK x)"
paulson@3474
    73
paulson@3480
    74
  (*serverK is similar*)
paulson@3474
    75
  inj_serverK   "inj serverK"	
paulson@3677
    76
  isSym_serverK "isSymKey (serverK x)"
paulson@3474
    77
paulson@3480
    78
  (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
paulson@3480
    79
  clientK_range "range clientK <= Compl (range serverK)"
paulson@3480
    80
paulson@3474
    81
paulson@3519
    82
consts    tls :: event list set
paulson@3474
    83
inductive tls
paulson@3474
    84
  intrs 
paulson@3474
    85
    Nil  (*Initial trace is empty*)
paulson@3474
    86
         "[]: tls"
paulson@3474
    87
paulson@3474
    88
    Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
paulson@3474
    89
         "[| evs: tls;  B ~= Spy;  
paulson@3683
    90
             X: synth (analz (spies evs)) |]
paulson@3480
    91
          ==> Says Spy B X # evs : tls"
paulson@3480
    92
paulson@3672
    93
    SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
paulson@3672
    94
         "[| evsSK: tls;
paulson@3672
    95
	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
paulson@3672
    96
          ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
paulson@3672
    97
			    Key (clientK(NA,NB,M)),
paulson@3672
    98
			    Key (serverK(NA,NB,M)) |} # evsSK : tls"
paulson@3474
    99
paulson@3474
   100
    ClientHello
paulson@3672
   101
	 (*(7.4.1.2)
paulson@3672
   102
	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
paulson@3474
   103
	   It is uninterpreted but will be confirmed in the FINISHED messages.
paulson@3676
   104
	   NA is CLIENT RANDOM, while SID is SESSION_ID.
paulson@3676
   105
           UNIX TIME is omitted because the protocol doesn't use it.
paulson@3676
   106
           May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
paulson@3676
   107
	   while MASTER SECRET is 48 byptes*)
paulson@3672
   108
         "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
paulson@3676
   109
          ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3676
   110
	        # evsCH  :  tls"
paulson@3474
   111
paulson@3474
   112
    ServerHello
paulson@3672
   113
         (*7.4.1.3 of the TLS Internet-Draft
paulson@3672
   114
	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
paulson@3672
   115
           SERVER CERTIFICATE (7.4.2) is always present.
paulson@3672
   116
           CERTIFICATE_REQUEST (7.4.4) is implied.*)
paulson@3672
   117
         "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
paulson@3676
   118
             Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3676
   119
	       : set evsSH |]
paulson@3676
   120
          ==> Says B A {|Nonce NB, Number SID, Number XB,
paulson@3500
   121
			 certificate B (pubK B)|}
paulson@3672
   122
                # evsSH  :  tls"
paulson@3474
   123
paulson@3474
   124
    ClientCertKeyEx
paulson@3672
   125
         (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
paulson@3672
   126
           The client, A, chooses PMS, the PREMASTER SECRET.
paulson@3672
   127
           She encrypts PMS using the supplied KB, which ought to be pubK B.
paulson@3672
   128
           We assume PMS ~: range PRF because a clash betweem the PMS
paulson@3672
   129
           and another MASTER SECRET is highly unlikely (even though
paulson@3672
   130
	   both items have the same length, 48 bytes).
paulson@3672
   131
           The Note event records in the trace that she knows PMS
paulson@3685
   132
               (see REMARK at top). *)
paulson@3672
   133
         "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
paulson@3676
   134
             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
paulson@3672
   135
	       : set evsCX |]
paulson@3672
   136
          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
paulson@3672
   137
	      # Notes A {|Agent B, Nonce PMS|}
paulson@3672
   138
	      # evsCX  :  tls"
paulson@3474
   139
paulson@3474
   140
    CertVerify
paulson@3685
   141
	(*The optional Certificate Verify (7.4.8) message contains the
paulson@3672
   142
          specific components listed in the security analysis, F.1.1.2.
paulson@3672
   143
          It adds the pre-master-secret, which is also essential!
paulson@3672
   144
          Checking the signature, which is the only use of A's certificate,
paulson@3672
   145
          assures B of A's presence*)
paulson@3672
   146
         "[| evsCV: tls;  A ~= B;  
paulson@3676
   147
             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
paulson@3672
   148
	       : set evsCV;
paulson@3672
   149
	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
paulson@3474
   150
          ==> Says A B (Crypt (priK A)
paulson@3672
   151
			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
paulson@3676
   152
              # evsCV  :  tls"
paulson@3474
   153
paulson@3672
   154
	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
paulson@3672
   155
          among other things.  The master-secret is PRF(PMS,NA,NB).
paulson@3474
   156
          Either party may sent its message first.*)
paulson@3474
   157
paulson@3685
   158
    ClientFinished
paulson@3672
   159
        (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
paulson@3515
   160
          rule's applying when the Spy has satisfied the "Says A B" by
paulson@3515
   161
          repaying messages sent by the true client; in that case, the
paulson@3685
   162
          Spy does not know PMS and could not sent ClientFinished.  One
paulson@3515
   163
          could simply put A~=Spy into the rule, but one should not
paulson@3515
   164
          expect the spy to be well-behaved.*)
paulson@3672
   165
         "[| evsCF: tls;  
paulson@3676
   166
	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3676
   167
	       : set evsCF;
paulson@3676
   168
             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
paulson@3672
   169
	       : set evsCF;
paulson@3672
   170
             Notes A {|Agent B, Nonce PMS|} : set evsCF;
paulson@3672
   171
	     M = PRF(PMS,NA,NB) |]
paulson@3474
   172
          ==> Says A B (Crypt (clientK(NA,NB,M))
paulson@3676
   173
			(Hash{|Nonce M, Number SID,
paulson@3672
   174
			       Nonce NA, Number XA, Agent A, 
paulson@3672
   175
			       Nonce NB, Number XB, Agent B|}))
paulson@3676
   176
              # evsCF  :  tls"
paulson@3474
   177
paulson@3685
   178
    ServerFinished
paulson@3474
   179
	(*Keeping A' and A'' distinct means B cannot even check that the
paulson@3672
   180
          two messages originate from the same source. *)
paulson@3672
   181
         "[| evsSF: tls;
paulson@3676
   182
	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3676
   183
	       : set evsSF;
paulson@3676
   184
	     Says B  A  {|Nonce NB, Number SID, Number XB,
paulson@3500
   185
		 	  certificate B (pubK B)|}
paulson@3672
   186
	       : set evsSF;
paulson@3672
   187
	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
paulson@3672
   188
	       : set evsSF;
paulson@3672
   189
	     M = PRF(PMS,NA,NB) |]
paulson@3474
   190
          ==> Says B A (Crypt (serverK(NA,NB,M))
paulson@3676
   191
			(Hash{|Nonce M, Number SID,
paulson@3672
   192
			       Nonce NA, Number XA, Agent A, 
paulson@3672
   193
			       Nonce NB, Number XB, Agent B|}))
paulson@3676
   194
              # evsSF  :  tls"
paulson@3474
   195
paulson@3685
   196
    ClientAccepts
paulson@3685
   197
	(*Having transmitted ClientFinished and received an identical
paulson@3677
   198
          message encrypted with serverK, the client stores the parameters
paulson@3677
   199
          needed to resume this session.*)
paulson@3677
   200
         "[| evsCA: tls;
paulson@3685
   201
	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
paulson@3677
   202
	     M = PRF(PMS,NA,NB);  
paulson@3677
   203
	     X = Hash{|Nonce M, Number SID,
paulson@3677
   204
	               Nonce NA, Number XA, Agent A, 
paulson@3677
   205
		       Nonce NB, Number XB, Agent B|};
paulson@3677
   206
             Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
paulson@3677
   207
             Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
paulson@3677
   208
          ==> 
paulson@3677
   209
             Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA  :  tls"
paulson@3677
   210
paulson@3685
   211
    ServerAccepts
paulson@3685
   212
	(*Having transmitted ServerFinished and received an identical
paulson@3677
   213
          message encrypted with clientK, the server stores the parameters
paulson@3677
   214
          needed to resume this session.*)
paulson@3677
   215
         "[| evsSA: tls;
paulson@3677
   216
             Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
paulson@3677
   217
	       : set evsSA;
paulson@3677
   218
	     M = PRF(PMS,NA,NB);  
paulson@3677
   219
	     X = Hash{|Nonce M, Number SID,
paulson@3677
   220
	               Nonce NA, Number XA, Agent A, 
paulson@3677
   221
		       Nonce NB, Number XB, Agent B|};
paulson@3677
   222
             Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
paulson@3677
   223
             Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
paulson@3677
   224
          ==> 
paulson@3677
   225
             Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
paulson@3677
   226
paulson@3685
   227
    ServerResume
paulson@3685
   228
         (*Resumption is described in 7.3.  If B finds the SESSION_ID
paulson@3685
   229
           then he sends HELLO and FINISHED messages, using the
paulson@3685
   230
           previously stored MASTER SECRET*)
paulson@3685
   231
         "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
paulson@3685
   232
             Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
paulson@3685
   233
	     Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3685
   234
	       : set evsSR |]
paulson@3685
   235
          ==> Says B A (Crypt (serverK(NA,NB,M))
paulson@3685
   236
			(Hash{|Nonce M, Number SID,
paulson@3685
   237
			       Nonce NA, Number XA, Agent A, 
paulson@3685
   238
			       Nonce NB, Number XB, Agent B|}))
paulson@3685
   239
              # Says B A {|Nonce NB, Number SID, Number XB|} # evsSR  :  tls"
paulson@3685
   240
paulson@3685
   241
    ClientResume
paulson@3685
   242
         (*If the response to ClientHello is ServerResume then send
paulson@3685
   243
           a FINISHED message using the new nonces and stored MASTER SECRET.*)
paulson@3685
   244
         "[| evsCR: tls;  
paulson@3685
   245
	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3685
   246
	       : set evsCR;
paulson@3685
   247
             Says B' A {|Nonce NB, Number SID, Number XB|} : set evsCR;
paulson@3685
   248
             Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
paulson@3685
   249
          ==> Says A B (Crypt (clientK(NA,NB,M))
paulson@3685
   250
			(Hash{|Nonce M, Number SID,
paulson@3685
   251
			       Nonce NA, Number XA, Agent A, 
paulson@3685
   252
			       Nonce NB, Number XB, Agent B|}))
paulson@3685
   253
              # evsCR  :  tls"
paulson@3685
   254
paulson@3474
   255
  (**Oops message??**)
paulson@3474
   256
paulson@3474
   257
end