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