diff -r b24c820a0b85 -r c3c0208988c0 src/HOL/SET-Protocol/Purchase.thy
--- a/src/HOL/SET-Protocol/Purchase.thy	Mon Jun 20 15:54:22 2005 +0200
+++ b/src/HOL/SET-Protocol/Purchase.thy	Mon Jun 20 15:54:39 2005 +0200
@@ -814,19 +814,26 @@
 text{*When M receives AuthRes, he knows that P signed it, including
   the identifying tags and the purchase amount, which he can verify.
   (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they
-   send the same message to M.)*}
+   send the same message to M.)  The conclusion is weak: M is existentially
+  quantified! That is because Authorization Response does not refer to M, while
+  the digital envelope weakens the link between @{term MsgAuthRes} and
+  @{term"priSK M"}.  Changing the precondition to refer to 
+  @{term "Crypt K (sign SK M)"} requires assuming @{term K} to be secure, since
+  otherwise the Spy could create that message.*}
 theorem M_verifies_AuthRes:
-  "[| MsgAuthRes = {|Number LID_M, Number XID, Number PurchAmt|};
+  "[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|}, 
+                     Hash authCode|};
       Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);
-      evs \<in> set_pur;  PG j \<notin> bad|]
-   ==> \<exists>i KM HOIData HOD P_I.
+      PG j \<notin> bad;  evs \<in> set_pur|]
+   ==> \<exists>M KM KP HOIData HOD P_I.
 	Gets (PG j)
-	   (EncB (priSK (Merchant i)) KM (pubEK (PG j))
+	   (EncB (priSK M) KM (pubEK (PG j))
 		    {|Number LID_M, Number XID, HOIData, HOD|}
 		    P_I) \<in> set evs &
-	Says (PG j) (Merchant i)
-	     (Crypt (pubEK (Merchant i)) (sign (priSK (PG j)) MsgAuthRes))
-          \<in> set evs"
+	Says (PG j) M
+	     (EncB (priSK (PG j)) KP (pubEK M)
+	      {|Number LID_M, Number XID, Number PurchAmt|}
+	      authCode) \<in> set evs"
 apply clarify
 apply (erule rev_mp)
 apply (erule set_pur.induct)