src/HOL/SET_Protocol/Cardholder_Registration.thy

   \<comment> \<open>Says is the only important case.
     1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
     2nd case: CR5, where KC3 encrypts NC3;
     3rd case: CR6, where KC2 encrypts NC3;
     4th case: CR6, where KC2 encrypts NonceCCA;
-    5th case: any use of @{term "priEK C"} (including CardSecret).
+    5th case: any use of \<^term>\<open>priEK C\<close> (including CardSecret).
     NB the only Nonces we need to keep secret are CardSecret and NonceCCA.
     But we can't prove \<open>Nonce_compromise\<close> unless the relation covers ALL
         nonces that the protocol keeps secret.\<close>
   "KeyCryptNonce DK N (ev # evs) =
    (KeyCryptNonce DK N evs |

     - certificates are an encryption certificate (flag is onlyEnc) and a
       signature certificate (flag is onlySig);
     - certificates pertain to the CA that C contacted (this is done by
       checking the signature).
    C generates a fresh symmetric key KC1.
-   The point of encrypting @{term "\<lbrace>Agent C, Nonce NC2, Hash (Pan(pan C))\<rbrace>"}
+   The point of encrypting \<^term>\<open>\<lbrace>Agent C, Nonce NC2, Hash (Pan(pan C))\<rbrace>\<close>
    is not clear.\<close>
 "[| evs3 \<in> set_cr;  C = Cardholder k;
     Nonce NC2 \<notin> used evs3;
     Key KC1 \<notin> used evs3; KC1 \<in> symKeys;
     Gets C \<lbrace>sign (invKey SKi) \<lbrace>Agent X, Nonce NC1\<rbrace>,

        # evs3 \<in> set_cr"
 
 | SET_CR4:
     \<comment> \<open>RegFormRes:
     CA responds sending NC2 back with a new nonce NCA, after checking that
-     - the digital envelope is correctly encrypted by @{term "pubEK (CA i)"}
+     - the digital envelope is correctly encrypted by \<^term>\<open>pubEK (CA i)\<close>
      - the entire message is encrypted with the same key found inside the
        envelope (here, KC1)\<close>
 "[| evs4 \<in> set_cr;
     Nonce NCA \<notin> used evs4;  KC1 \<in> symKeys;
     Gets (CA i) (EXHcrypt KC1 EKi \<lbrace>Agent C, Nonce NC2\<rbrace> (Pan(pan X)))

 
   \<comment> \<open>CertRes: CA responds sending NC3 back with its half of the secret value,
    its signature certificate and the new cardholder signature
    certificate.  CA checks to have never certified the key proposed by C.
    NOTE: In Merchant Registration, the corresponding rule (4)
-   uses the "sign" primitive. The encryption below is actually @{term EncK}, 
-   which is just @{term "Crypt K (sign SK X)"}.\<close>
+   uses the "sign" primitive. The encryption below is actually \<^term>\<open>EncK\<close>, 
+   which is just \<^term>\<open>Crypt K (sign SK X)\<close>.\<close>
 
 | SET_CR6:
 "[| evs6 \<in> set_cr;
     Nonce NonceCCA \<notin> used evs6;
     KC2 \<in> symKeys;  KC3 \<in> symKeys;  cardSK \<notin> symKeys;

 apply (auto simp add: parts_insert2 split: event.split)
 done
 
 
 text\<open>This holds because if (priEK (CA i)) appears in any traffic then it must
-  be known to the Spy, by @{term Spy_see_private_Key}\<close>
+  be known to the Spy, by \<^term>\<open>Spy_see_private_Key\<close>\<close>
 lemma cardSK_neq_priEK:
      "[|Key cardSK \<notin> analz (knows Spy evs);
         Key cardSK \<in> parts (knows Spy evs);
         evs \<in> set_cr|] ==> cardSK \<noteq> priEK C"
 by blast

 subsection\<open>Rewriting Rule for PANs\<close>
 
 text\<open>Lemma for message 6: either cardSK isn't a CA's private encryption key,
   or if it is then (because it appears in traffic) that CA is bad,
   and so the Spy knows that key already.  Either way, we can simplify
-  the expression @{term "analz (insert (Key cardSK) X)"}.\<close>
+  the expression \<^term>\<open>analz (insert (Key cardSK) X)\<close>.\<close>
 lemma msg6_cardSK_disj:
      "[|Gets A \<lbrace>Crypt K \<lbrace>c, n, k', Key cardSK, X\<rbrace>, Y\<rbrace>
           \<in> set evs;  evs \<in> set_cr |]
       ==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
 by auto

 by (simp del: image_insert image_Un
          add: analz_image_keys_simps analz_image_pan)
 
 
 text\<open>Confidentiality of the PAN\@.  Maybe we could combine the statements of
-  this theorem with @{term analz_image_pan}, requiring a single induction but
+  this theorem with \<^term>\<open>analz_image_pan\<close>, requiring a single induction but
   a much more difficult proof.\<close>
 lemma pan_confidentiality:
      "[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs \<in> set_cr|]
     ==> \<exists>i X K HN.
         Says C (CA i) \<lbrace>X, Crypt (pubEK (CA i)) \<lbrace>Key K, Pan (pan C), HN\<rbrace> \<rbrace>