src/HOL/Auth/TLS.thy
author paulson
Tue Jul 01 11:11:42 1997 +0200 (1997-07-01)
changeset 3474 44249bba00ec
child 3480 d59bbf053258
permissions -rw-r--r--
Baby TLS. Proofs work, but model seems unrealistic
     1 (*  Title:      HOL/Auth/TLS
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
     7 
     8 An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
     9 to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
    10 global signing authority.
    11 
    12 A is the client and B is the server, not to be confused with the constant
    13 Server, who is in charge of all public keys.
    14 
    15 The model assumes that no fraudulent certificates are present.
    16 
    17 Protocol goals: 
    18 * M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
    19      parties (though A is not necessarily authenticated).
    20 
    21 * B upon receiving CERTIFICATE VERIFY knows that A is present (But this
    22     message is optional!)
    23 
    24 * A upon receiving SERVER FINISHED knows that B is present
    25 
    26 * Each party who has received a FINISHED message can trust that the other
    27   party agrees on all message components, including XA and XB (thus foiling
    28   rollback attacks).
    29 *)
    30 
    31 TLS = Public + 
    32 
    33 consts
    34   (*Client, server write keys.  They implicitly include the MAC secrets.*)
    35   clientK, serverK :: "nat*nat*nat => key"
    36 
    37 rules
    38   (*clientK is collision-free and makes symmetric keys*)
    39   inj_clientK   "inj clientK"	
    40   isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
    41 
    42   inj_serverK   "inj serverK"	
    43   isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
    44 
    45   (*Spy has access to his own key for spoof messages, but Server is secure*)
    46   Spy_in_lost     "Spy: lost"
    47   Server_not_lost "Server ~: lost"
    48 
    49 
    50 consts  lost :: agent set        (*No need for it to be a variable*)
    51 	tls  :: event list set
    52 
    53 inductive tls
    54   intrs 
    55     Nil  (*Initial trace is empty*)
    56          "[]: tls"
    57 
    58     Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
    59          "[| evs: tls;  B ~= Spy;  
    60              X: synth (analz (sees lost Spy evs)) |]
    61           ==> Says Spy B X  # evs : tls"
    62 
    63     ClientHello
    64 	 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    65 	   It is uninterpreted but will be confirmed in the FINISHED messages.
    66 	   As an initial simplification, SESSION_ID is identified with NA
    67            and reuse of sessions is not supported.*)
    68          "[| evs: tls;  A ~= B;  Nonce NA ~: used evs |]
    69           ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs  :  tls"
    70 
    71     ServerHello
    72          (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    73 	   Na is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
    74 	   implied and a SERVER CERTIFICATE is always present.*)
    75          "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
    76              Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
    77           ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
    78 			 Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
    79                 # evs  :  tls"
    80 
    81     ClientCertKeyEx
    82          (*CLIENT CERTIFICATE and KEY EXCHANGE.  M is the pre-master-secret.
    83            Note that A encrypts using the supplied KB, not pubK B.*)
    84          "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
    85              Says B' A {|Nonce NA, Nonce NB, Agent XB,
    86 			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
    87           ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
    88 			 Crypt KB (Nonce M)|}
    89                 # evs  :  tls"
    90 
    91     CertVerify
    92 	(*The optional CERTIFICATE VERIFY message contains the specific
    93           components listed in the security analysis, Appendix F.1.1.2.
    94           By checking the signature, B is assured of A's existence:
    95           the only use of A's certificate.*)
    96          "[| evs: tls;  A ~= B;  
    97              Says B' A {|Nonce NA, Nonce NB, Agent XB,
    98 			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
    99           ==> Says A B (Crypt (priK A)
   100 			(Hash{|Nonce NB,
   101 	 		       Crypt (priK Server) {|Agent B, Key KB|}|}))
   102                 # evs  :  tls"
   103 
   104 	(*Finally come the FINISHED messages, confirming XA and XB among
   105           other things.  The master-secret is the hash of NA, NB and M.
   106           Either party may sent its message first.*)
   107 
   108     ClientFinished
   109          "[| evs: tls;  A ~= B;
   110 	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
   111              Says B' A {|Nonce NA, Nonce NB, Agent XB, 
   112 			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs;
   113              Says A  B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
   114 		         Crypt KB (Nonce M)|} : set evs |]
   115           ==> Says A B (Crypt (clientK(NA,NB,M))
   116 			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   117 			       Nonce NA, Agent XA,
   118 			       Crypt (priK Server) {|Agent A, Key(pubK A)|}, 
   119 			       Nonce NB, Agent XB, Agent B|}))
   120                 # evs  :  tls"
   121 
   122 	(*Keeping A' and A'' distinct means B cannot even check that the
   123           two messages originate from the same source.*)
   124 
   125     ServerFinished
   126          "[| evs: tls;  A ~= B;
   127 	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
   128 	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
   129 		 	  Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
   130 	       : set evs;
   131 	     Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |]
   132           ==> Says B A (Crypt (serverK(NA,NB,M))
   133 			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   134 			       Nonce NA, Agent XA, Agent A, 
   135 			       Nonce NB, Agent XB,
   136 			       Crypt (priK Server) {|Agent B, Key(pubK B)|}|}))
   137                 # evs  :  tls"
   138 
   139   (**Oops message??**)
   140 
   141 end