src/HOL/Auth/TLS.thy
changeset 3474 44249bba00ec
child 3480 d59bbf053258
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/TLS.thy	Tue Jul 01 11:11:42 1997 +0200
     1.3 @@ -0,0 +1,141 @@
     1.4 +(*  Title:      HOL/Auth/TLS
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1997  University of Cambridge
     1.8 +
     1.9 +Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
    1.10 +
    1.11 +An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
    1.12 +to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
    1.13 +global signing authority.
    1.14 +
    1.15 +A is the client and B is the server, not to be confused with the constant
    1.16 +Server, who is in charge of all public keys.
    1.17 +
    1.18 +The model assumes that no fraudulent certificates are present.
    1.19 +
    1.20 +Protocol goals: 
    1.21 +* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
    1.22 +     parties (though A is not necessarily authenticated).
    1.23 +
    1.24 +* B upon receiving CERTIFICATE VERIFY knows that A is present (But this
    1.25 +    message is optional!)
    1.26 +
    1.27 +* A upon receiving SERVER FINISHED knows that B is present
    1.28 +
    1.29 +* Each party who has received a FINISHED message can trust that the other
    1.30 +  party agrees on all message components, including XA and XB (thus foiling
    1.31 +  rollback attacks).
    1.32 +*)
    1.33 +
    1.34 +TLS = Public + 
    1.35 +
    1.36 +consts
    1.37 +  (*Client, server write keys.  They implicitly include the MAC secrets.*)
    1.38 +  clientK, serverK :: "nat*nat*nat => key"
    1.39 +
    1.40 +rules
    1.41 +  (*clientK is collision-free and makes symmetric keys*)
    1.42 +  inj_clientK   "inj clientK"	
    1.43 +  isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
    1.44 +
    1.45 +  inj_serverK   "inj serverK"	
    1.46 +  isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
    1.47 +
    1.48 +  (*Spy has access to his own key for spoof messages, but Server is secure*)
    1.49 +  Spy_in_lost     "Spy: lost"
    1.50 +  Server_not_lost "Server ~: lost"
    1.51 +
    1.52 +
    1.53 +consts  lost :: agent set        (*No need for it to be a variable*)
    1.54 +	tls  :: event list set
    1.55 +
    1.56 +inductive tls
    1.57 +  intrs 
    1.58 +    Nil  (*Initial trace is empty*)
    1.59 +         "[]: tls"
    1.60 +
    1.61 +    Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
    1.62 +         "[| evs: tls;  B ~= Spy;  
    1.63 +             X: synth (analz (sees lost Spy evs)) |]
    1.64 +          ==> Says Spy B X  # evs : tls"
    1.65 +
    1.66 +    ClientHello
    1.67 +	 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    1.68 +	   It is uninterpreted but will be confirmed in the FINISHED messages.
    1.69 +	   As an initial simplification, SESSION_ID is identified with NA
    1.70 +           and reuse of sessions is not supported.*)
    1.71 +         "[| evs: tls;  A ~= B;  Nonce NA ~: used evs |]
    1.72 +          ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs  :  tls"
    1.73 +
    1.74 +    ServerHello
    1.75 +         (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.76 +	   Na is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
    1.77 +	   implied and a SERVER CERTIFICATE is always present.*)
    1.78 +         "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
    1.79 +             Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
    1.80 +          ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
    1.81 +			 Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
    1.82 +                # evs  :  tls"
    1.83 +
    1.84 +    ClientCertKeyEx
    1.85 +         (*CLIENT CERTIFICATE and KEY EXCHANGE.  M is the pre-master-secret.
    1.86 +           Note that A encrypts using the supplied KB, not pubK B.*)
    1.87 +         "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
    1.88 +             Says B' A {|Nonce NA, Nonce NB, Agent XB,
    1.89 +			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
    1.90 +          ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
    1.91 +			 Crypt KB (Nonce M)|}
    1.92 +                # evs  :  tls"
    1.93 +
    1.94 +    CertVerify
    1.95 +	(*The optional CERTIFICATE VERIFY message contains the specific
    1.96 +          components listed in the security analysis, Appendix F.1.1.2.
    1.97 +          By checking the signature, B is assured of A's existence:
    1.98 +          the only use of A's certificate.*)
    1.99 +         "[| evs: tls;  A ~= B;  
   1.100 +             Says B' A {|Nonce NA, Nonce NB, Agent XB,
   1.101 +			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs |]
   1.102 +          ==> Says A B (Crypt (priK A)
   1.103 +			(Hash{|Nonce NB,
   1.104 +	 		       Crypt (priK Server) {|Agent B, Key KB|}|}))
   1.105 +                # evs  :  tls"
   1.106 +
   1.107 +	(*Finally come the FINISHED messages, confirming XA and XB among
   1.108 +          other things.  The master-secret is the hash of NA, NB and M.
   1.109 +          Either party may sent its message first.*)
   1.110 +
   1.111 +    ClientFinished
   1.112 +         "[| evs: tls;  A ~= B;
   1.113 +	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
   1.114 +             Says B' A {|Nonce NA, Nonce NB, Agent XB, 
   1.115 +			 Crypt (priK Server) {|Agent B, Key KB|}|} : set evs;
   1.116 +             Says A  B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},
   1.117 +		         Crypt KB (Nonce M)|} : set evs |]
   1.118 +          ==> Says A B (Crypt (clientK(NA,NB,M))
   1.119 +			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   1.120 +			       Nonce NA, Agent XA,
   1.121 +			       Crypt (priK Server) {|Agent A, Key(pubK A)|}, 
   1.122 +			       Nonce NB, Agent XB, Agent B|}))
   1.123 +                # evs  :  tls"
   1.124 +
   1.125 +	(*Keeping A' and A'' distinct means B cannot even check that the
   1.126 +          two messages originate from the same source.*)
   1.127 +
   1.128 +    ServerFinished
   1.129 +         "[| evs: tls;  A ~= B;
   1.130 +	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
   1.131 +	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
   1.132 +		 	  Crypt (priK Server) {|Agent B, Key (pubK B)|}|}
   1.133 +	       : set evs;
   1.134 +	     Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |]
   1.135 +          ==> Says B A (Crypt (serverK(NA,NB,M))
   1.136 +			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   1.137 +			       Nonce NA, Agent XA, Agent A, 
   1.138 +			       Nonce NB, Agent XB,
   1.139 +			       Crypt (priK Server) {|Agent B, Key(pubK B)|}|}))
   1.140 +                # evs  :  tls"
   1.141 +
   1.142 +  (**Oops message??**)
   1.143 +
   1.144 +end