src/HOL/Auth/TLS.thy
changeset 3515 d8a71f6eaf40
parent 3506 a36e0a49d2cd
child 3519 ab0a9fbed4c0
     1.1 --- a/src/HOL/Auth/TLS.thy	Fri Jul 11 13:28:53 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Fri Jul 11 13:30:01 1997 +0200
     1.3 @@ -18,6 +18,19 @@
     1.4  Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
     1.5  Allen, Transport Layer Security Working Group, 21 May 1997,
     1.6  INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
     1.7 +
     1.8 +NOTE.  The event "Notes A {|Agent B, Nonce M|}" appears in ClientCertKeyEx,
     1.9 +CertVerify, ClientFinished to record that A knows M.  It is a note from A to
    1.10 +herself.  Nobody else can see it.  In ClientCertKeyEx, the Spy can substitute
    1.11 +his own certificate for A's, but he cannot replace A's note by one for himself.
    1.12 +
    1.13 +The note is needed because of a weakness in the public-key model.  Each
    1.14 +agent's state is recorded as the trace of messages.  When the true client (A)
    1.15 +invents M, he encrypts M with B's public key before sending it.  The model
    1.16 +does not distinguish the original occurrence of such a message from a replay.
    1.17 +
    1.18 +In the shared-key model, the ability to encrypt implies the ability to
    1.19 +decrypt, so the problem does not arise.
    1.20  *)
    1.21  
    1.22  TLS = Public + 
    1.23 @@ -77,7 +90,7 @@
    1.24  
    1.25      ServerHello
    1.26           (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    1.27 -	   Na is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
    1.28 +	   NA is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
    1.29  	   implied and a SERVER CERTIFICATE is always present.*)
    1.30           "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
    1.31               Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
    1.32 @@ -86,13 +99,16 @@
    1.33                  # evs  :  tls"
    1.34  
    1.35      ClientCertKeyEx
    1.36 -         (*CLIENT CERTIFICATE and KEY EXCHANGE.  M is the pre-master-secret.
    1.37 -           Note that A encrypts using the supplied KB, not pubK B.*)
    1.38 +         (*CLIENT CERTIFICATE and KEY EXCHANGE.  The client, A, chooses M,
    1.39 +           the pre-master-secret.  She encrypts M using the supplied KB,
    1.40 +           which ought to be pubK B, and also with her own public key,
    1.41 +           to record in the trace that she knows M (see NOTE at top).*)
    1.42           "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
    1.43               Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
    1.44  	       : set evs |]
    1.45            ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
    1.46 -                # evs  :  tls"
    1.47 +	      # Notes A {|Agent B, Nonce M|}
    1.48 +	      # evs  :  tls"
    1.49  
    1.50      CertVerify
    1.51  	(*The optional CERTIFICATE VERIFY message contains the specific
    1.52 @@ -102,8 +118,7 @@
    1.53           "[| evs: tls;  A ~= B;  
    1.54               Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
    1.55  	       : set evs;
    1.56 -	     Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
    1.57 -	       : set evs |]
    1.58 +	     Notes A {|Agent B, Nonce M|} : set evs |]
    1.59            ==> Says A B (Crypt (priK A)
    1.60  			(Hash{|Nonce NB, certificate B KB, Nonce M|}))
    1.61                  # evs  :  tls"
    1.62 @@ -112,13 +127,18 @@
    1.63            other things.  The master-secret is the hash of NA, NB and M.
    1.64            Either party may sent its message first.*)
    1.65  
    1.66 +        (*The occurrence of Crypt (pubK A) {|Agent B, Nonce M|} stops the 
    1.67 +          rule's applying when the Spy has satisfied the "Says A B" by
    1.68 +          repaying messages sent by the true client; in that case, the
    1.69 +          Spy does not know M and could not sent CLIENT FINISHED.  One
    1.70 +          could simply put A~=Spy into the rule, but one should not
    1.71 +          expect the spy to be well-behaved.*)
    1.72      ClientFinished
    1.73           "[| evs: tls;  A ~= B;
    1.74  	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
    1.75               Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
    1.76  	       : set evs;
    1.77 -             Says A  B {|certificate A (pubK A), Crypt KB (Nonce M)|}
    1.78 -	       : set evs |]
    1.79 +             Notes A {|Agent B, Nonce M|} : set evs |]
    1.80            ==> Says A B (Crypt (clientK(NA,NB,M))
    1.81  			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
    1.82  			       Nonce NA, Agent XA,
    1.83 @@ -127,15 +147,16 @@
    1.84                  # evs  :  tls"
    1.85  
    1.86  	(*Keeping A' and A'' distinct means B cannot even check that the
    1.87 -          two messages originate from the same source.*)
    1.88 -
    1.89 +          two messages originate from the same source.  B does not attempt
    1.90 +          to read A's encrypted "note to herself".*)
    1.91      ServerFinished
    1.92           "[| evs: tls;  A ~= B;
    1.93  	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
    1.94  	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
    1.95  		 	  certificate B (pubK B)|}
    1.96  	       : set evs;
    1.97 -	     Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |]
    1.98 +	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce M)|}
    1.99 +	       : set evs |]
   1.100            ==> Says B A (Crypt (serverK(NA,NB,M))
   1.101  			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   1.102  			       Nonce NA, Agent XA, Agent A,