src/HOL/Auth/TLS.thy
author paulson
Tue Jul 01 17:37:42 1997 +0200 (1997-07-01)
changeset 3480 d59bbf053258
parent 3474 44249bba00ec
child 3500 0d8ad2f192d8
permissions -rw-r--r--
More realistic model: the Spy can compute clientK and serverK
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@3474
    21
*)
paulson@3474
    22
paulson@3474
    23
TLS = Public + 
paulson@3474
    24
paulson@3474
    25
consts
paulson@3474
    26
  (*Client, server write keys.  They implicitly include the MAC secrets.*)
paulson@3474
    27
  clientK, serverK :: "nat*nat*nat => key"
paulson@3474
    28
paulson@3474
    29
rules
paulson@3474
    30
  (*clientK is collision-free and makes symmetric keys*)
paulson@3474
    31
  inj_clientK   "inj clientK"	
paulson@3474
    32
  isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
paulson@3474
    33
paulson@3480
    34
  (*serverK is similar*)
paulson@3474
    35
  inj_serverK   "inj serverK"	
paulson@3474
    36
  isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
paulson@3474
    37
paulson@3480
    38
  (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
paulson@3480
    39
  clientK_range "range clientK <= Compl (range serverK)"
paulson@3480
    40
paulson@3474
    41
  (*Spy has access to his own key for spoof messages, but Server is secure*)
paulson@3474
    42
  Spy_in_lost     "Spy: lost"
paulson@3474
    43
  Server_not_lost "Server ~: lost"
paulson@3474
    44
paulson@3474
    45
paulson@3474
    46
consts  lost :: agent set        (*No need for it to be a variable*)
paulson@3474
    47
	tls  :: event list set
paulson@3474
    48
paulson@3474
    49
inductive tls
paulson@3474
    50
  intrs 
paulson@3474
    51
    Nil  (*Initial trace is empty*)
paulson@3474
    52
         "[]: tls"
paulson@3474
    53
paulson@3474
    54
    Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
paulson@3474
    55
         "[| evs: tls;  B ~= Spy;  
paulson@3474
    56
             X: synth (analz (sees lost Spy evs)) |]
paulson@3480
    57
          ==> Says Spy B X # evs : tls"
paulson@3480
    58
paulson@3480
    59
    SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
paulson@3480
    60
         "[| evs: tls;
paulson@3480
    61
	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evs |]
paulson@3480
    62
          ==> Says Spy B {| Key (clientK(NA,NB,M)),
paulson@3480
    63
			    Key (serverK(NA,NB,M)) |} # evs : tls"
paulson@3474
    64
paulson@3474
    65
    ClientHello
paulson@3474
    66
	 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
paulson@3474
    67
	   It is uninterpreted but will be confirmed in the FINISHED messages.
paulson@3474
    68
	   As an initial simplification, SESSION_ID is identified with NA
paulson@3474
    69
           and reuse of sessions is not supported.*)
paulson@3474
    70
         "[| evs: tls;  A ~= B;  Nonce NA ~: used evs |]
paulson@3474
    71
          ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs  :  tls"
paulson@3474
    72
paulson@3474
    73
    ServerHello
paulson@3474
    74
         (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
paulson@3474
    75
	   Na is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
paulson@3474
    76
	   implied and a SERVER CERTIFICATE is always present.*)
paulson@3474
    77
         "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
paulson@3474
    78
             Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
paulson@3474
    79
          ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
paulson@3474
    80
			 Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
paulson@3474
    81
                # evs  :  tls"
paulson@3474
    82
paulson@3474
    83
    ClientCertKeyEx
paulson@3474
    84
         (*CLIENT CERTIFICATE and KEY EXCHANGE.  M is the pre-master-secret.
paulson@3474
    85
           Note that A encrypts using the supplied KB, not pubK B.*)
paulson@3474
    86
         "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
paulson@3474
    87
             Says B' A {|Nonce NA, Nonce NB, Agent XB,
paulson@3474
    88
			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
paulson@3474
    89
          ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
paulson@3474
    90
			 Crypt KB (Nonce M)|}
paulson@3474
    91
                # evs  :  tls"
paulson@3474
    92
paulson@3474
    93
    CertVerify
paulson@3474
    94
	(*The optional CERTIFICATE VERIFY message contains the specific
paulson@3474
    95
          components listed in the security analysis, Appendix F.1.1.2.
paulson@3474
    96
          By checking the signature, B is assured of A's existence:
paulson@3474
    97
          the only use of A's certificate.*)
paulson@3474
    98
         "[| evs: tls;  A ~= B;  
paulson@3474
    99
             Says B' A {|Nonce NA, Nonce NB, Agent XB,
paulson@3474
   100
			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
paulson@3474
   101
          ==> Says A B (Crypt (priK A)
paulson@3474
   102
			(Hash{|Nonce NB,
paulson@3474
   103
	 		       Crypt (priK Server) {|Agent B, Key KB|}|}))
paulson@3474
   104
                # evs  :  tls"
paulson@3474
   105
paulson@3474
   106
	(*Finally come the FINISHED messages, confirming XA and XB among
paulson@3474
   107
          other things.  The master-secret is the hash of NA, NB and M.
paulson@3474
   108
          Either party may sent its message first.*)
paulson@3474
   109
paulson@3474
   110
    ClientFinished
paulson@3474
   111
         "[| evs: tls;  A ~= B;
paulson@3474
   112
	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
paulson@3474
   113
             Says B' A {|Nonce NA, Nonce NB, Agent XB, 
paulson@3474
   114
			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs;
paulson@3474
   115
             Says A  B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
paulson@3474
   116
		         Crypt KB (Nonce M)|} : set evs |]
paulson@3474
   117
          ==> Says A B (Crypt (clientK(NA,NB,M))
paulson@3474
   118
			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
paulson@3474
   119
			       Nonce NA, Agent XA,
paulson@3474
   120
			       Crypt (priK Server) {|Agent A, Key(pubK A)|}, 
paulson@3474
   121
			       Nonce NB, Agent XB, Agent B|}))
paulson@3474
   122
                # evs  :  tls"
paulson@3474
   123
paulson@3474
   124
	(*Keeping A' and A'' distinct means B cannot even check that the
paulson@3474
   125
          two messages originate from the same source.*)
paulson@3474
   126
paulson@3474
   127
    ServerFinished
paulson@3474
   128
         "[| evs: tls;  A ~= B;
paulson@3474
   129
	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
paulson@3474
   130
	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
paulson@3474
   131
		 	  Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
paulson@3474
   132
	       : set evs;
paulson@3474
   133
	     Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |]
paulson@3474
   134
          ==> Says B A (Crypt (serverK(NA,NB,M))
paulson@3474
   135
			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
paulson@3474
   136
			       Nonce NA, Agent XA, Agent A, 
paulson@3474
   137
			       Nonce NB, Agent XB,
paulson@3474
   138
			       Crypt (priK Server) {|Agent B, Key(pubK B)|}|}))
paulson@3474
   139
                # evs  :  tls"
paulson@3474
   140
paulson@3474
   141
  (**Oops message??**)
paulson@3474
   142
paulson@3474
   143
end