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";