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