src/HOL/SET_Protocol/Purchase.thy

           # evsPReqU \<in> set_pur"
 
 | PReqS:
       \<comment> \<open>SIGNED Purchase request.  Page 77 of Formal Protocol Desc.
           We could specify the equation
-          @{term "PIReqSigned = \<lbrace> PIDualSigned, OIDualSigned \<rbrace>"}, since the
+          \<^term>\<open>PIReqSigned = \<lbrace> PIDualSigned, OIDualSigned \<rbrace>\<close>, since the
           Formal Desc. gives PIHead the same format in the unsigned case.
           However, there's little point, as P treats the signed and 
           unsigned cases differently.\<close>
    "!!C Chall_C Chall_M EKj HOD KC2 LID_M M OIData
       OIDualSigned OrderDesc P PANData PIData PIDualSigned

 lemma parts_image_priEK:
      "[|Key (priEK C) \<in> parts (Key`KK \<union> (knows Spy evs));
         evs \<in> set_pur|] ==> priEK C \<in> KK | C \<in> bad"
 by auto
 
-text\<open>trivial proof because @{term"priEK C"} never appears even in
-  @{term "parts evs"}.\<close>
+text\<open>trivial proof because \<^term>\<open>priEK C\<close> never appears even in
+  \<^term>\<open>parts evs\<close>.\<close>
 lemma analz_image_priEK:
      "evs \<in> set_pur ==>
           (Key (priEK C) \<in> analz (Key`KK \<union> (knows Spy evs))) =
           (priEK C \<in> KK | C \<in> bad)"
 by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])

 lemma M_Notes_PG:
      "[|Notes M \<lbrace>Number LID_M, Agent P, Agent M, Agent C, etc\<rbrace> \<in> set evs;
         evs \<in> set_pur|] ==> \<exists>j. P = PG j"
 by (erule rev_mp, erule set_pur.induct, simp_all)
 
-text\<open>If we trust M, then @{term LID_M} determines his choice of P
+text\<open>If we trust M, then \<^term>\<open>LID_M\<close> determines his choice of P
       (Payment Gateway)\<close>
 lemma goodM_gives_correct_PG:
      "[| MsgPInitRes = 
             \<lbrace>Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)\<rbrace>;
          Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);

 text\<open>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.)  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
+  the digital envelope weakens the link between \<^term>\<open>MsgAuthRes\<close> and
+  \<^term>\<open>priSK M\<close>.  Changing the precondition to refer to 
+  \<^term>\<open>Crypt K (sign SK M)\<close> requires assuming \<^term>\<open>K\<close> to be secure, since
   otherwise the Spy could create that message.\<close>
 theorem M_verifies_AuthRes:
   "[| MsgAuthRes = \<lbrace>\<lbrace>Number LID_M, Number XID, Number PurchAmt\<rbrace>, 
                      Hash authCode\<rbrace>;
       Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);

 apply auto
 apply (blast dest: Gets_imp_Says Says_C_PInitRes)
 done
 
 
-text\<open>Unicity of @{term LID_M} between Merchant and Cardholder notes\<close>
+text\<open>Unicity of \<^term>\<open>LID_M\<close> between Merchant and Cardholder notes\<close>
 lemma unique_LID_M:
      "[|Notes (Merchant i) \<lbrace>Number LID_M, Agent P, Trans\<rbrace> \<in> set evs;
         Notes C \<lbrace>Number LID_M, Agent M, Agent C, Number OD,
              Number PA\<rbrace> \<in> set evs;
         evs \<in> set_pur|]

 apply (erule rev_mp)
 apply (erule set_pur.induct, simp_all)
 apply (force dest!: Notes_imp_parts_subset_used)
 done
 
-text\<open>Unicity of @{term LID_M}, for two Merchant Notes events\<close>
+text\<open>Unicity of \<^term>\<open>LID_M\<close>, for two Merchant Notes events\<close>
 lemma unique_LID_M2:
      "[|Notes M \<lbrace>Number LID_M, Trans\<rbrace> \<in> set evs;
         Notes M \<lbrace>Number LID_M, Trans'\<rbrace> \<in> set evs;
         evs \<in> set_pur|] ==> Trans' = Trans"
 apply (erule rev_mp)

 apply (erule set_pur.induct, simp_all)
 apply (force dest!: Notes_imp_parts_subset_used)
 done
 
 text\<open>Lemma needed below: for the case that
-  if PRes is present, then @{term LID_M} has been used.\<close>
+  if PRes is present, then \<^term>\<open>LID_M\<close> has been used.\<close>
 lemma signed_imp_used:
      "[| Crypt (priSK M) (Hash X) \<in> parts (knows Spy evs);
          M \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
 apply (erule rev_mp)
 apply (erule set_pur.induct)

 apply (blast dest!: Notes_Cardholder_self_False)
 done
 
 text\<open>When P sees a dual signature, he knows that it originated with C.
   and was intended for M. This guarantee isn't useful to M, who never gets
-  PIData. I don't see how to link @{term "PG j"} and \<open>LID_M\<close> without
-  assuming @{term "M \<notin> bad"}.\<close>
+  PIData. I don't see how to link \<^term>\<open>PG j\<close> and \<open>LID_M\<close> without
+  assuming \<^term>\<open>M \<notin> bad\<close>.\<close>
 theorem P_verifies_Signed_PReq:
      "[| MsgDualSign = \<lbrace>Hash PIData, HOIData\<rbrace>;
          PIData = \<lbrace>PIHead, PANData\<rbrace>;
          PIHead = \<lbrace>Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
                     TransStain\<rbrace>;

 done
 
 text\<open>When P receives an AuthReq and a dual signature, he knows that C and M
   agree on the essential details.  PurchAmt however is never sent by M to
   P; instead C and M both send 
-     @{term "HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>"}
+     \<^term>\<open>HOD = Hash\<lbrace>Number OrderDesc, Number PurchAmt\<rbrace>\<close>
   and P compares the two copies of HOD.
 
   Agreement can't be proved for some things, including the symmetric keys
   used in the digital envelopes.  On the other hand, M knows the true identity
   of PG (namely j'), and sends AReq there; he can't, however, check that