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