src/HOL/Auth/TLS.thy
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3506 a36e0a49d2cd
child 3515 d8a71f6eaf40
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/TLS
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     2
    ID:         $Id$
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     5
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     6
Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     7
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     8
An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
     9
to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    10
global signing authority.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    11
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    12
A is the client and B is the server, not to be confused with the constant
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    13
Server, who is in charge of all public keys.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    14
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    15
The model assumes that no fraudulent certificates are present, but it does
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    16
assume that some private keys are lost to the spy.
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    17
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    18
Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    19
Allen, Transport Layer Security Working Group, 21 May 1997,
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    20
INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    21
*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    22
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    23
TLS = Public + 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    24
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    25
consts
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    26
  (*Client, server write keys.  They implicitly include the MAC secrets.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    27
  clientK, serverK :: "nat*nat*nat => key"
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    28
  certificate      :: "[agent,key] => msg"
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    29
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    30
defs
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    31
  certificate_def
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    32
    "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    33
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    34
rules
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    35
  (*clientK is collision-free and makes symmetric keys*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    36
  inj_clientK   "inj clientK"	
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    37
  isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    38
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    39
  (*serverK is similar*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    40
  inj_serverK   "inj serverK"	
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    41
  isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    42
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    43
  (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    44
  clientK_range "range clientK <= Compl (range serverK)"
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    45
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    46
  (*Spy has access to his own key for spoof messages, but Server is secure*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    47
  Spy_in_lost     "Spy: lost"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    48
  Server_not_lost "Server ~: lost"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    49
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    50
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    51
consts  lost :: agent set        (*No need for it to be a variable*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    52
	tls  :: event list set
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    53
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    54
inductive tls
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    55
  intrs 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    56
    Nil  (*Initial trace is empty*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    57
         "[]: tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    58
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    59
    Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    60
         "[| evs: tls;  B ~= Spy;  
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    61
             X: synth (analz (sees lost Spy evs)) |]
3480
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    62
          ==> Says Spy B X # evs : tls"
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    63
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    64
    SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    65
         "[| evs: tls;
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    66
	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evs |]
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    67
          ==> Says Spy B {| Key (clientK(NA,NB,M)),
d59bbf053258 More realistic model: the Spy can compute clientK and serverK
paulson
parents: 3474
diff changeset
    68
			    Key (serverK(NA,NB,M)) |} # evs : tls"
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    69
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    70
    ClientHello
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    71
	 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    72
	   It is uninterpreted but will be confirmed in the FINISHED messages.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    73
	   As an initial simplification, SESSION_ID is identified with NA
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    74
           and reuse of sessions is not supported.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    75
         "[| evs: tls;  A ~= B;  Nonce NA ~: used evs |]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    76
          ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs  :  tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    77
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    78
    ServerHello
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    79
         (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    80
	   Na is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    81
	   implied and a SERVER CERTIFICATE is always present.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    82
         "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    83
             Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    84
          ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
    85
			 certificate B (pubK B)|}
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    86
                # evs  :  tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    87
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    88
    ClientCertKeyEx
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    89
         (*CLIENT CERTIFICATE and KEY EXCHANGE.  M is the pre-master-secret.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    90
           Note that A encrypts using the supplied KB, not pubK B.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    91
         "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
    92
             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
    93
	       : set evs |]
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
    94
          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    95
                # evs  :  tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    96
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    97
    CertVerify
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
    98
	(*The optional CERTIFICATE VERIFY message contains the specific
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
    99
          components listed in the security analysis, Appendix F.1.1.2;
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   100
          it also contains the pre-master-secret.  Checking the signature,
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   101
          which is the only use of A's certificate, assures B of A's presence*)
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   102
         "[| evs: tls;  A ~= B;  
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   103
             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   104
	       : set evs;
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   105
	     Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   106
	       : set evs |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   107
          ==> Says A B (Crypt (priK A)
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   108
			(Hash{|Nonce NB, certificate B KB, Nonce M|}))
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   109
                # evs  :  tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   110
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   111
	(*Finally come the FINISHED messages, confirming XA and XB among
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   112
          other things.  The master-secret is the hash of NA, NB and M.
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   113
          Either party may sent its message first.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   114
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   115
    ClientFinished
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   116
         "[| evs: tls;  A ~= B;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   117
	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
3506
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   118
             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   119
	       : set evs;
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   120
             Says A  B {|certificate A (pubK A), Crypt KB (Nonce M)|}
a36e0a49d2cd New proofs involving CERTIFICATE VERIFY
paulson
parents: 3500
diff changeset
   121
	       : set evs |]
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   122
          ==> Says A B (Crypt (clientK(NA,NB,M))
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   123
			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   124
			       Nonce NA, Agent XA,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   125
			       certificate A (pubK A), 
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   126
			       Nonce NB, Agent XB, Agent B|}))
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   127
                # evs  :  tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   128
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   129
	(*Keeping A' and A'' distinct means B cannot even check that the
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   130
          two messages originate from the same source.*)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   131
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   132
    ServerFinished
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   133
         "[| evs: tls;  A ~= B;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   134
	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   135
	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   136
		 	  certificate B (pubK B)|}
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   137
	       : set evs;
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   138
	     Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |]
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   139
          ==> Says B A (Crypt (serverK(NA,NB,M))
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   140
			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   141
			       Nonce NA, Agent XA, Agent A, 
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   142
			       Nonce NB, Agent XB,
3500
0d8ad2f192d8 New constant "certificate"--just an abbreviation
paulson
parents: 3480
diff changeset
   143
			       certificate B (pubK B)|}))
3474
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   144
                # evs  :  tls"
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   145
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   146
  (**Oops message??**)
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   147
44249bba00ec Baby TLS. Proofs work, but model seems unrealistic
paulson
parents:
diff changeset
   148
end