src/HOL/Auth/TLS.thy
author paulson
Fri Jul 11 13:30:01 1997 +0200 (1997-07-11)
changeset 3515 d8a71f6eaf40
parent 3506 a36e0a49d2cd
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Now uses the Notes constructor to distinguish the Client (who has chosen M)
from the Spy (who may have replayed her 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@3474
     7
paulson@3474
     8
An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
paulson@3474
     9
to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
paulson@3474
    10
global signing authority.
paulson@3474
    11
paulson@3474
    12
A is the client and B is the server, not to be confused with the constant
paulson@3474
    13
Server, who is in charge of all public keys.
paulson@3474
    14
paulson@3480
    15
The model assumes that no fraudulent certificates are present, but it does
paulson@3480
    16
assume that some private keys are lost to the spy.
paulson@3474
    17
paulson@3480
    18
Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
paulson@3480
    19
Allen, Transport Layer Security Working Group, 21 May 1997,
paulson@3480
    20
INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
paulson@3515
    21
paulson@3515
    22
NOTE.  The event "Notes A {|Agent B, Nonce M|}" appears in ClientCertKeyEx,
paulson@3515
    23
CertVerify, ClientFinished to record that A knows M.  It is a note from A to
paulson@3515
    24
herself.  Nobody else can see it.  In ClientCertKeyEx, the Spy can substitute
paulson@3515
    25
his own certificate for A's, but he cannot replace A's note by one for himself.
paulson@3515
    26
paulson@3515
    27
The note is needed because of a weakness in the public-key model.  Each
paulson@3515
    28
agent's state is recorded as the trace of messages.  When the true client (A)
paulson@3515
    29
invents M, he encrypts M with B's public key before sending it.  The model
paulson@3515
    30
does not distinguish the original occurrence of such a message from a replay.
paulson@3515
    31
paulson@3515
    32
In the shared-key model, the ability to encrypt implies the ability to
paulson@3515
    33
decrypt, so the problem does not arise.
paulson@3474
    34
*)
paulson@3474
    35
paulson@3474
    36
TLS = Public + 
paulson@3474
    37
paulson@3474
    38
consts
paulson@3474
    39
  (*Client, server write keys.  They implicitly include the MAC secrets.*)
paulson@3474
    40
  clientK, serverK :: "nat*nat*nat => key"
paulson@3500
    41
  certificate      :: "[agent,key] => msg"
paulson@3500
    42
paulson@3500
    43
defs
paulson@3500
    44
  certificate_def
paulson@3500
    45
    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
paulson@3474
    46
paulson@3474
    47
rules
paulson@3474
    48
  (*clientK is collision-free and makes symmetric keys*)
paulson@3474
    49
  inj_clientK   "inj clientK"	
paulson@3474
    50
  isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
paulson@3474
    51
paulson@3480
    52
  (*serverK is similar*)
paulson@3474
    53
  inj_serverK   "inj serverK"	
paulson@3474
    54
  isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
paulson@3474
    55
paulson@3480
    56
  (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
paulson@3480
    57
  clientK_range "range clientK <= Compl (range serverK)"
paulson@3480
    58
paulson@3474
    59
  (*Spy has access to his own key for spoof messages, but Server is secure*)
paulson@3474
    60
  Spy_in_lost     "Spy: lost"
paulson@3474
    61
  Server_not_lost "Server ~: lost"
paulson@3474
    62
paulson@3474
    63
paulson@3474
    64
consts  lost :: agent set        (*No need for it to be a variable*)
paulson@3474
    65
	tls  :: event list set
paulson@3474
    66
paulson@3474
    67
inductive tls
paulson@3474
    68
  intrs 
paulson@3474
    69
    Nil  (*Initial trace is empty*)
paulson@3474
    70
         "[]: tls"
paulson@3474
    71
paulson@3474
    72
    Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
paulson@3474
    73
         "[| evs: tls;  B ~= Spy;  
paulson@3474
    74
             X: synth (analz (sees lost Spy evs)) |]
paulson@3480
    75
          ==> Says Spy B X # evs : tls"
paulson@3480
    76
paulson@3480
    77
    SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
paulson@3480
    78
         "[| evs: tls;
paulson@3480
    79
	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evs |]
paulson@3480
    80
          ==> Says Spy B {| Key (clientK(NA,NB,M)),
paulson@3480
    81
			    Key (serverK(NA,NB,M)) |} # evs : tls"
paulson@3474
    82
paulson@3474
    83
    ClientHello
paulson@3474
    84
	 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
paulson@3474
    85
	   It is uninterpreted but will be confirmed in the FINISHED messages.
paulson@3474
    86
	   As an initial simplification, SESSION_ID is identified with NA
paulson@3474
    87
           and reuse of sessions is not supported.*)
paulson@3474
    88
         "[| evs: tls;  A ~= B;  Nonce NA ~: used evs |]
paulson@3474
    89
          ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs  :  tls"
paulson@3474
    90
paulson@3474
    91
    ServerHello
paulson@3474
    92
         (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
paulson@3515
    93
	   NA is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
paulson@3474
    94
	   implied and a SERVER CERTIFICATE is always present.*)
paulson@3474
    95
         "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
paulson@3474
    96
             Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
paulson@3474
    97
          ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
paulson@3500
    98
			 certificate B (pubK B)|}
paulson@3474
    99
                # evs  :  tls"
paulson@3474
   100
paulson@3474
   101
    ClientCertKeyEx
paulson@3515
   102
         (*CLIENT CERTIFICATE and KEY EXCHANGE.  The client, A, chooses M,
paulson@3515
   103
           the pre-master-secret.  She encrypts M using the supplied KB,
paulson@3515
   104
           which ought to be pubK B, and also with her own public key,
paulson@3515
   105
           to record in the trace that she knows M (see NOTE at top).*)
paulson@3474
   106
         "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
paulson@3506
   107
             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
paulson@3506
   108
	       : set evs |]
paulson@3506
   109
          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
paulson@3515
   110
	      # Notes A {|Agent B, Nonce M|}
paulson@3515
   111
	      # evs  :  tls"
paulson@3474
   112
paulson@3474
   113
    CertVerify
paulson@3474
   114
	(*The optional CERTIFICATE VERIFY message contains the specific
paulson@3506
   115
          components listed in the security analysis, Appendix F.1.1.2;
paulson@3506
   116
          it also contains the pre-master-secret.  Checking the signature,
paulson@3506
   117
          which is the only use of A's certificate, assures B of A's presence*)
paulson@3474
   118
         "[| evs: tls;  A ~= B;  
paulson@3506
   119
             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
paulson@3506
   120
	       : set evs;
paulson@3515
   121
	     Notes A {|Agent B, Nonce M|} : set evs |]
paulson@3474
   122
          ==> Says A B (Crypt (priK A)
paulson@3506
   123
			(Hash{|Nonce NB, certificate B KB, Nonce M|}))
paulson@3474
   124
                # evs  :  tls"
paulson@3474
   125
paulson@3474
   126
	(*Finally come the FINISHED messages, confirming XA and XB among
paulson@3474
   127
          other things.  The master-secret is the hash of NA, NB and M.
paulson@3474
   128
          Either party may sent its message first.*)
paulson@3474
   129
paulson@3515
   130
        (*The occurrence of Crypt (pubK A) {|Agent B, Nonce M|} stops the 
paulson@3515
   131
          rule's applying when the Spy has satisfied the "Says A B" by
paulson@3515
   132
          repaying messages sent by the true client; in that case, the
paulson@3515
   133
          Spy does not know M and could not sent CLIENT FINISHED.  One
paulson@3515
   134
          could simply put A~=Spy into the rule, but one should not
paulson@3515
   135
          expect the spy to be well-behaved.*)
paulson@3474
   136
    ClientFinished
paulson@3474
   137
         "[| evs: tls;  A ~= B;
paulson@3474
   138
	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
paulson@3506
   139
             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
paulson@3506
   140
	       : set evs;
paulson@3515
   141
             Notes A {|Agent B, Nonce M|} : set evs |]
paulson@3474
   142
          ==> Says A B (Crypt (clientK(NA,NB,M))
paulson@3474
   143
			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
paulson@3474
   144
			       Nonce NA, Agent XA,
paulson@3500
   145
			       certificate A (pubK A), 
paulson@3474
   146
			       Nonce NB, Agent XB, Agent B|}))
paulson@3474
   147
                # evs  :  tls"
paulson@3474
   148
paulson@3474
   149
	(*Keeping A' and A'' distinct means B cannot even check that the
paulson@3515
   150
          two messages originate from the same source.  B does not attempt
paulson@3515
   151
          to read A's encrypted "note to herself".*)
paulson@3474
   152
    ServerFinished
paulson@3474
   153
         "[| evs: tls;  A ~= B;
paulson@3474
   154
	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
paulson@3474
   155
	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
paulson@3500
   156
		 	  certificate B (pubK B)|}
paulson@3474
   157
	       : set evs;
paulson@3515
   158
	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce M)|}
paulson@3515
   159
	       : set evs |]
paulson@3474
   160
          ==> Says B A (Crypt (serverK(NA,NB,M))
paulson@3474
   161
			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
paulson@3474
   162
			       Nonce NA, Agent XA, Agent A, 
paulson@3474
   163
			       Nonce NB, Agent XB,
paulson@3500
   164
			       certificate B (pubK B)|}))
paulson@3474
   165
                # evs  :  tls"
paulson@3474
   166
paulson@3474
   167
  (**Oops message??**)
paulson@3474
   168
paulson@3474
   169
end