src/HOL/Auth/TLS.thy
author paulson
Tue Sep 16 14:40:01 1997 +0200 (1997-09-16)
changeset 3676 cbaec955056b
parent 3672 56e4365a0c99
child 3677 f2569416d18b
permissions -rw-r--r--
Addition of SessionIDs to the Hello and Finished messages
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
paulson@3515
    34
In the shared-key model, the ability to encrypt implies the ability to
paulson@3515
    35
decrypt, so the problem does not arise.
paulson@3474
    36
*)
paulson@3474
    37
paulson@3474
    38
TLS = Public + 
paulson@3474
    39
paulson@3474
    40
consts
paulson@3672
    41
  (*Pseudo-random function of Section 5*)
paulson@3672
    42
  PRF  :: "nat*nat*nat => nat"
paulson@3672
    43
paulson@3672
    44
  (*Client, server write keys implicitly include the MAC secrets.*)
paulson@3474
    45
  clientK, serverK :: "nat*nat*nat => key"
paulson@3672
    46
paulson@3500
    47
  certificate      :: "[agent,key] => msg"
paulson@3500
    48
paulson@3500
    49
defs
paulson@3500
    50
  certificate_def
paulson@3500
    51
    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
paulson@3474
    52
paulson@3474
    53
rules
paulson@3672
    54
  inj_PRF       "inj PRF"	
paulson@3672
    55
paulson@3474
    56
  (*clientK is collision-free and makes symmetric keys*)
paulson@3474
    57
  inj_clientK   "inj clientK"	
paulson@3474
    58
  isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
paulson@3474
    59
paulson@3480
    60
  (*serverK is similar*)
paulson@3474
    61
  inj_serverK   "inj serverK"	
paulson@3474
    62
  isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
paulson@3474
    63
paulson@3480
    64
  (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
paulson@3480
    65
  clientK_range "range clientK <= Compl (range serverK)"
paulson@3480
    66
paulson@3474
    67
paulson@3519
    68
consts    tls :: event list set
paulson@3474
    69
inductive tls
paulson@3474
    70
  intrs 
paulson@3474
    71
    Nil  (*Initial trace is empty*)
paulson@3474
    72
         "[]: tls"
paulson@3474
    73
paulson@3474
    74
    Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
paulson@3474
    75
         "[| evs: tls;  B ~= Spy;  
paulson@3519
    76
             X: synth (analz (sees Spy evs)) |]
paulson@3480
    77
          ==> Says Spy B X # evs : tls"
paulson@3480
    78
paulson@3672
    79
    SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
paulson@3672
    80
         "[| evsSK: tls;
paulson@3672
    81
	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
paulson@3672
    82
          ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
paulson@3672
    83
			    Key (clientK(NA,NB,M)),
paulson@3672
    84
			    Key (serverK(NA,NB,M)) |} # evsSK : tls"
paulson@3474
    85
paulson@3474
    86
    ClientHello
paulson@3672
    87
	 (*(7.4.1.2)
paulson@3672
    88
	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
paulson@3474
    89
	   It is uninterpreted but will be confirmed in the FINISHED messages.
paulson@3676
    90
	   NA is CLIENT RANDOM, while SID is SESSION_ID.
paulson@3676
    91
           UNIX TIME is omitted because the protocol doesn't use it.
paulson@3676
    92
           May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
paulson@3676
    93
	   while MASTER SECRET is 48 byptes*)
paulson@3672
    94
         "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
paulson@3676
    95
          ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3676
    96
	        # evsCH  :  tls"
paulson@3474
    97
paulson@3474
    98
    ServerHello
paulson@3672
    99
         (*7.4.1.3 of the TLS Internet-Draft
paulson@3672
   100
	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
paulson@3672
   101
           SERVER CERTIFICATE (7.4.2) is always present.
paulson@3672
   102
           CERTIFICATE_REQUEST (7.4.4) is implied.*)
paulson@3672
   103
         "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
paulson@3676
   104
             Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3676
   105
	       : set evsSH |]
paulson@3676
   106
          ==> Says B A {|Nonce NB, Number SID, Number XB,
paulson@3500
   107
			 certificate B (pubK B)|}
paulson@3672
   108
                # evsSH  :  tls"
paulson@3474
   109
paulson@3474
   110
    ClientCertKeyEx
paulson@3672
   111
         (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
paulson@3672
   112
           The client, A, chooses PMS, the PREMASTER SECRET.
paulson@3672
   113
           She encrypts PMS using the supplied KB, which ought to be pubK B.
paulson@3672
   114
           We assume PMS ~: range PRF because a clash betweem the PMS
paulson@3672
   115
           and another MASTER SECRET is highly unlikely (even though
paulson@3672
   116
	   both items have the same length, 48 bytes).
paulson@3672
   117
           The Note event records in the trace that she knows PMS
paulson@3672
   118
               (see REMARK at top).*)
paulson@3672
   119
         "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
paulson@3676
   120
             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
paulson@3672
   121
	       : set evsCX |]
paulson@3672
   122
          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
paulson@3672
   123
	      # Notes A {|Agent B, Nonce PMS|}
paulson@3672
   124
	      # evsCX  :  tls"
paulson@3474
   125
paulson@3474
   126
    CertVerify
paulson@3672
   127
	(*The optional CERTIFICATE VERIFY (7.4.8) message contains the
paulson@3672
   128
          specific components listed in the security analysis, F.1.1.2.
paulson@3672
   129
          It adds the pre-master-secret, which is also essential!
paulson@3672
   130
          Checking the signature, which is the only use of A's certificate,
paulson@3672
   131
          assures B of A's presence*)
paulson@3672
   132
         "[| evsCV: tls;  A ~= B;  
paulson@3676
   133
             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
paulson@3672
   134
	       : set evsCV;
paulson@3672
   135
	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
paulson@3474
   136
          ==> Says A B (Crypt (priK A)
paulson@3672
   137
			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
paulson@3676
   138
              # evsCV  :  tls"
paulson@3474
   139
paulson@3672
   140
	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
paulson@3672
   141
          among other things.  The master-secret is PRF(PMS,NA,NB).
paulson@3474
   142
          Either party may sent its message first.*)
paulson@3474
   143
paulson@3672
   144
        (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
paulson@3515
   145
          rule's applying when the Spy has satisfied the "Says A B" by
paulson@3515
   146
          repaying messages sent by the true client; in that case, the
paulson@3672
   147
          Spy does not know PMS and could not sent CLIENT FINISHED.  One
paulson@3515
   148
          could simply put A~=Spy into the rule, but one should not
paulson@3515
   149
          expect the spy to be well-behaved.*)
paulson@3474
   150
    ClientFinished
paulson@3672
   151
         "[| evsCF: tls;  
paulson@3676
   152
	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3676
   153
	       : set evsCF;
paulson@3676
   154
             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
paulson@3672
   155
	       : set evsCF;
paulson@3672
   156
             Notes A {|Agent B, Nonce PMS|} : set evsCF;
paulson@3672
   157
	     M = PRF(PMS,NA,NB) |]
paulson@3474
   158
          ==> Says A B (Crypt (clientK(NA,NB,M))
paulson@3676
   159
			(Hash{|Nonce M, Number SID,
paulson@3672
   160
			       Nonce NA, Number XA, Agent A, 
paulson@3672
   161
			       Nonce NB, Number XB, Agent B|}))
paulson@3676
   162
              # evsCF  :  tls"
paulson@3474
   163
paulson@3474
   164
	(*Keeping A' and A'' distinct means B cannot even check that the
paulson@3672
   165
          two messages originate from the same source. *)
paulson@3474
   166
    ServerFinished
paulson@3672
   167
         "[| evsSF: tls;
paulson@3676
   168
	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
paulson@3676
   169
	       : set evsSF;
paulson@3676
   170
	     Says B  A  {|Nonce NB, Number SID, Number XB,
paulson@3500
   171
		 	  certificate B (pubK B)|}
paulson@3672
   172
	       : set evsSF;
paulson@3672
   173
	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
paulson@3672
   174
	       : set evsSF;
paulson@3672
   175
	     M = PRF(PMS,NA,NB) |]
paulson@3474
   176
          ==> Says B A (Crypt (serverK(NA,NB,M))
paulson@3676
   177
			(Hash{|Nonce M, Number SID,
paulson@3672
   178
			       Nonce NA, Number XA, Agent A, 
paulson@3672
   179
			       Nonce NB, Number XB, Agent B|}))
paulson@3676
   180
              # evsSF  :  tls"
paulson@3474
   181
paulson@3474
   182
  (**Oops message??**)
paulson@3474
   183
paulson@3474
   184
end