# HG changeset patch
# User paulson
# Date 875526393 -7200
# Node ID 6be7cf5086abe3391a936ceb47b5d0d6937c07fa
# Parent  f92594f65af6e7d0421d8c55df658f425e7bcc66
Renamed XA, XB to PA, PB and removed the certificate from Client Verify

diff -r f92594f65af6 -r 6be7cf5086ab src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Mon Sep 29 11:45:52 1997 +0200
+++ b/src/HOL/Auth/TLS.ML	Mon Sep 29 11:46:33 1997 +0200
@@ -13,7 +13,7 @@
 * A upon receiving ServerFinished knows that B is present
 
 * Each party who has received a FINISHED message can trust that the other
-  party agrees on all message components, including XA and XB (thus foiling
+  party agrees on all message components, including PA and PB (thus foiling
   rollback attacks).
 *)
 
@@ -102,7 +102,7 @@
 (*And one for ServerAccepts.  Either FINISHED message may come first.*)
 goal thy 
  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
-\           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
+\           A ~= B |] ==> EX SID NA PA NB PB M. EX evs: tls.    \
 \  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
@@ -115,8 +115,7 @@
 goal thy 
  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
 \           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
-\  Says A B (Crypt (priK A)                 \
-\            (Hash{|Nonce NB, certificate B (pubK B), Nonce PMS|})) : set evs";
+\  Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
 	  RS tls.CertVerify) 2);
@@ -130,11 +129,11 @@
 \           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
 \           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
 \           ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
-\           A ~= B |] ==> EX NA XA NB XB. EX evs: tls.    \
+\           A ~= B |] ==> EX NA PA NB PB. EX evs: tls.    \
 \  Says A B (Crypt (clientK(NA,NB,M))                           \
 \            (Hash{|Nonce M, Number SID,             \
-\                   Nonce NA, Number XA, Agent A,      \
-\                   Nonce NB, Number XB, Agent B|})) : set evs";
+\                   Nonce NA, Number PA, Agent A,      \
+\                   Nonce NB, Number PB, Agent B|})) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2);
 by possibility_tac;
@@ -301,10 +300,9 @@
   message is Fake.  We don't need guarantees for the Spy anyway.  We must
   assume A~:bad; otherwise, the Spy can forge A's signature.*)
 goal thy
- "!!evs. [| X = Crypt (priK A)                                        \
-\                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
+ "!!evs. [| X = Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|});      \
 \           evs : tls;  A ~: bad;  B ~= Spy |]                       \
-\    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
+\    ==> Says B A {|Nonce NB, Number SID, Number PB, certificate B KB|}  \
 \          : set evs --> \
 \        X : parts (spies evs) --> Says A B X : set evs";
 by (hyp_subst_tac 1);
@@ -318,7 +316,7 @@
 
 (*If CertVerify is present then A has chosen PMS.*)
 goal thy
- "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
+ "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})  \
 \             : parts (spies evs);                                \
 \           evs : tls;  A ~: bad |]                                      \
 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
@@ -692,8 +690,8 @@
 
 
 (*** Protocol goals: if A receives ServerFinished, then B is present 
-     and has used the quoted values XA, XB, etc.  Note that it is up to A
-     to compare XA with what she originally sent.
+     and has used the quoted values PA, PB, etc.  Note that it is up to A
+     to compare PA with what she originally sent.
 ***)
 
 (*The mention of her name (A) in X assures A that B knows who she is.*)
@@ -701,8 +699,8 @@
  "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
 \           X = Crypt (serverK(Na,Nb,M))                  \
 \                 (Hash{|Nonce M, Number SID,             \
-\                        Nonce NA, Number XA, Agent A,    \
-\                        Nonce NB, Number XB, Agent B|}); \
+\                        Nonce NA, Number PA, Agent A,    \
+\                        Nonce NB, Number PB, Agent B|}); \
 \           M = PRF(PMS,NA,NB);                           \
 \           evs : tls;  A ~: bad;  B ~: bad |]          \
 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
@@ -727,8 +725,8 @@
 goal thy
  "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
 \                 (Hash{|Nonce M, Number SID,             \
-\                        Nonce NA, Number XA, Agent A,    \
-\                        Nonce NB, Number XB, Agent B|}); \
+\                        Nonce NA, Number PA, Agent A,    \
+\                        Nonce NB, Number PB, Agent B|}); \
 \           M = PRF(PMS,NA,NB);                           \
 \           X : parts (spies evs);                        \
 \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
@@ -794,7 +792,7 @@
 (*** Protocol goal: if B receives any message encrypted with clientK
      then A has sent it, ASSUMING that A chose PMS.  Authentication is
      assumed here; B cannot verify it.  But if the message is
-     ClientFinished, then B can then check the quoted values XA, XB, etc.
+     ClientFinished, then B can then check the quoted values PA, PB, etc.
 ***)
 
 goal thy
@@ -834,15 +832,14 @@
 
 (*** Protocol goal: if B receives ClientFinished, and if B is able to
      check a CertVerify from A, then A has used the quoted
-     values XA, XB, etc.  Even this one requires A to be uncompromised.
+     values PA, PB, etc.  Even this one requires A to be uncompromised.
  ***)
 goal thy
  "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
 \           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
-\           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
+\           Says B  A {|Nonce NB, Number SID, Number PB, certificate B KB|}  \
 \             : set evs;                                                  \
-\           Says A'' B (Crypt (priK A)                                    \
-\                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
+\           Says A'' B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))\
 \             : set evs;                                                  \
 \        evs : tls;  A ~: bad;  B ~: bad |]                             \
 \     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
diff -r f92594f65af6 -r 6be7cf5086ab src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Mon Sep 29 11:45:52 1997 +0200
+++ b/src/HOL/Auth/TLS.thy	Mon Sep 29 11:46:33 1997 +0200
@@ -93,25 +93,25 @@
 
     ClientHello
 	 (*(7.4.1.2)
-	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
+	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
 	   It is uninterpreted but will be confirmed in the FINISHED messages.
 	   NA is CLIENT RANDOM, while SID is SESSION_ID.
            UNIX TIME is omitted because the protocol doesn't use it.
            May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
 	   while MASTER SECRET is 48 byptes*)
          "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
-          ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}
+          ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
 	        # evsCH  :  tls"
 
     ServerHello
          (*7.4.1.3 of the TLS Internet-Draft
-	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
+	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
            SERVER CERTIFICATE (7.4.2) is always present.
            CERTIFICATE_REQUEST (7.4.4) is implied.*)
          "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
-             Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
+             Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
 	       : set evsSH |]
-          ==> Says B A {|Nonce NB, Number SID, Number XB,
+          ==> Says B A {|Nonce NB, Number SID, Number PB,
 			 certificate B (pubK B)|}
                 # evsSH  :  tls"
 
@@ -125,7 +125,7 @@
            The Note event records in the trace that she knows PMS
                (see REMARK at top). *)
          "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
-             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
+             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
 	       : set evsCX |]
           ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
 	      # Notes A {|Agent B, Nonce PMS|}
@@ -138,14 +138,13 @@
           Checking the signature, which is the only use of A's certificate,
           assures B of A's presence*)
          "[| evsCV: tls;  A ~= B;  
-             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
+             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
 	       : set evsCV;
 	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
-          ==> Says A B (Crypt (priK A)
-			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
+          ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
               # evsCV  :  tls"
 
-	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
+	(*Finally come the FINISHED messages (7.4.8), confirming PA and PB
           among other things.  The master-secret is PRF(PMS,NA,NB).
           Either party may sent its message first.*)
 
@@ -157,25 +156,25 @@
           could simply put A~=Spy into the rule, but one should not
           expect the spy to be well-behaved.*)
          "[| evsCF: tls;  
-	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
+	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
 	       : set evsCF;
-             Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}
+             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
 	       : set evsCF;
              Notes A {|Agent B, Nonce PMS|} : set evsCF;
 	     M = PRF(PMS,NA,NB) |]
           ==> Says A B (Crypt (clientK(NA,NB,M))
 			(Hash{|Nonce M, Number SID,
-			       Nonce NA, Number XA, Agent A, 
-			       Nonce NB, Number XB, Agent B|}))
+			       Nonce NA, Number PA, Agent A, 
+			       Nonce NB, Number PB, Agent B|}))
               # evsCF  :  tls"
 
     ServerFinished
 	(*Keeping A' and A'' distinct means B cannot even check that the
           two messages originate from the same source. *)
          "[| evsSF: tls;
-	     Says A' B  {|Agent A, Nonce NA, Number SID, Number XA|}
+	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
 	       : set evsSF;
-	     Says B  A  {|Nonce NB, Number SID, Number XB,
+	     Says B  A  {|Nonce NB, Number SID, Number PB,
 		 	  certificate B (pubK B)|}
 	       : set evsSF;
 	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
@@ -183,8 +182,8 @@
 	     M = PRF(PMS,NA,NB) |]
           ==> Says B A (Crypt (serverK(NA,NB,M))
 			(Hash{|Nonce M, Number SID,
-			       Nonce NA, Number XA, Agent A, 
-			       Nonce NB, Number XB, Agent B|}))
+			       Nonce NA, Number PA, Agent A, 
+			       Nonce NB, Number PB, Agent B|}))
               # evsSF  :  tls"
 
     ClientAccepts
@@ -196,8 +195,8 @@
 	     Notes A {|Agent B, Nonce PMS|} : set evsCA;
 	     M = PRF(PMS,NA,NB);  
 	     X = Hash{|Nonce M, Number SID,
-	               Nonce NA, Number XA, Agent A, 
-		       Nonce NB, Number XB, Agent B|};
+	               Nonce NA, Number PA, Agent A, 
+		       Nonce NB, Number PB, Agent B|};
              Says A  B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
              Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
           ==> 
@@ -213,8 +212,8 @@
 	       : set evsSA;
 	     M = PRF(PMS,NA,NB);  
 	     X = Hash{|Nonce M, Number SID,
-	               Nonce NA, Number XA, Agent A, 
-		       Nonce NB, Number XB, Agent B|};
+	               Nonce NA, Number PA, Agent A, 
+		       Nonce NB, Number PB, Agent B|};
              Says B  A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
              Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
           ==> 
@@ -226,26 +225,26 @@
            previously stored MASTER SECRET*)
          "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
              Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
-	     Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}
+	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
 	       : set evsSR |]
           ==> Says B A (Crypt (serverK(NA,NB,M))
 			(Hash{|Nonce M, Number SID,
-			       Nonce NA, Number XA, Agent A, 
-			       Nonce NB, Number XB, Agent B|}))
-              # Says B A {|Nonce NB, Number SID, Number XB|} # evsSR  :  tls"
+			       Nonce NA, Number PA, Agent A, 
+			       Nonce NB, Number PB, Agent B|}))
+              # Says B A {|Nonce NB, Number SID, Number PB|} # evsSR  :  tls"
 
     ClientResume
          (*If the response to ClientHello is ServerResume then send
            a FINISHED message using the new nonces and stored MASTER SECRET.*)
          "[| evsCR: tls;  
-	     Says A  B {|Agent A, Nonce NA, Number SID, Number XA|}
+	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
 	       : set evsCR;
-             Says B' A {|Nonce NB, Number SID, Number XB|} : set evsCR;
+             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCR;
              Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]
           ==> Says A B (Crypt (clientK(NA,NB,M))
 			(Hash{|Nonce M, Number SID,
-			       Nonce NA, Number XA, Agent A, 
-			       Nonce NB, Number XB, Agent B|}))
+			       Nonce NA, Number PA, Agent A, 
+			       Nonce NB, Number PB, Agent B|}))
               # evsCR  :  tls"
 
     Oops