src/HOL/Auth/Yahalom.thy

                 # evs3 \<in> yahalom"
 
  | YM4:  
        \<comment> \<open>Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.  The premise
-           @{term "A \<noteq> Server"} is needed for \<open>Says_Server_not_range\<close>.
+           \<^term>\<open>A \<noteq> Server\<close> is needed for \<open>Says_Server_not_range\<close>.
            Alice can check that K is symmetric by its length.\<close>
          "\<lbrakk>evs4 \<in> yahalom;  A \<noteq> Server;  K \<in> symKeys;
              Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace>
                 \<in> set evs4;
              Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4\<rbrakk>

 lemma YM4_Key_parts_knows_Spy:
      "Says Server A \<lbrace>Crypt (shrK A) \<lbrace>B,K,NA,NB\<rbrace>, X\<rbrace> \<in> set evs
       \<Longrightarrow> K \<in> parts (knows Spy evs)"
   by (metis parts.Body parts.Fst parts.Snd  Says_imp_knows_Spy parts.Inj)
 
-text\<open>Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
+text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (knows Spy evs)\<close> imply 
 that NOBODY sends messages containing X!\<close>
 
 text\<open>Spy never sees a good agent's shared key!\<close>
 lemma Spy_see_shrK [simp]:
      "evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"

 apply blast+
 done
 
 text\<open>B knows, by the second part of A's message, that the Server
   distributed the key quoting nonce NB.  This part says nothing about
-  agent names.  Secrecy of NB is crucial.  Note that @{term "Nonce NB
-  \<notin> analz(knows Spy evs)"} must be the FIRST antecedent of the
+  agent names.  Secrecy of NB is crucial.  Note that \<^term>\<open>Nonce NB
+  \<notin> analz(knows Spy evs)\<close> must be the FIRST antecedent of the
   induction formula.\<close>
 
 lemma B_trusts_YM4_newK [rule_format]:
      "\<lbrakk>Crypt K (Nonce NB) \<in> parts (knows Spy evs);
         Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom\<rbrakk>

        add: analz_image_freshK_simps split_ifs
             all_conj_distrib ball_conj_distrib
             analz_image_freshK fresh_not_KeyWithNonce
             imp_disj_not1               (*Moves NBa\<noteq>NB to the front*)
             Says_Server_KeyWithNonce)
-txt\<open>For Oops, simplification proves @{prop "NBa\<noteq>NB"}.  By
-  @{term Says_Server_KeyWithNonce}, we get @{prop "\<not> KeyWithNonce K NB
-  evs"}; then simplification can apply the induction hypothesis with
-  @{term "KK = {K}"}.\<close>
+txt\<open>For Oops, simplification proves \<^prop>\<open>NBa\<noteq>NB\<close>.  By
+  \<^term>\<open>Says_Server_KeyWithNonce\<close>, we get \<^prop>\<open>\<not> KeyWithNonce K NB
+  evs\<close>; then simplification can apply the induction hypothesis with
+  \<^term>\<open>KK = {K}\<close>.\<close>
   subgoal \<comment> \<open>Fake\<close> by spy_analz
   subgoal \<comment> \<open>YM2\<close> by blast
   subgoal \<comment> \<open>YM3\<close> by blast
-  subgoal \<comment> \<open>YM4: If @{prop "A \<in> bad"} then @{term NBa} is known, therefore @{prop "NBa \<noteq> NB"}.\<close>
+  subgoal \<comment> \<open>YM4: If \<^prop>\<open>A \<in> bad\<close> then \<^term>\<open>NBa\<close> is known, therefore \<^prop>\<open>NBa \<noteq> NB\<close>.\<close>
     by (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def
         Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj)
 done
 
 

   subgoal \<comment> \<open>YM2\<close> by blast
   subgoal \<comment> \<open>YM3: because no NB can also be an NA\<close> 
     by (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
   subgoal \<comment> \<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close>
     \<comment> \<open>Case analysis on whether Aa is bad;
-            use \<open>Says_unique_NB\<close> to identify message components: @{term "Aa=A"}, @{term "Ba=B"}\<close>
+            use \<open>Says_unique_NB\<close> to identify message components: \<^term>\<open>Aa=A\<close>, \<^term>\<open>Ba=B\<close>\<close>
     apply clarify
     apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
                         parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
                  dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
                        Spy_not_see_encrypted_key)

   by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst
          not_parts_not_analz)
 
 
 subsection\<open>Authenticating A to B using the certificate 
-  @{term "Crypt K (Nonce NB)"}\<close>
+  \<^term>\<open>Crypt K (Nonce NB)\<close>\<close>
 
 text\<open>Assuming the session key is secure, if both certificates are present then
   A has said NB.  We can't be sure about the rest of A's message, but only
   NB matters for freshness.\<close>
 theorem A_Said_YM3_lemma [rule_format]:

           (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
 apply (erule yahalom.induct, force,
        frule_tac [6] YM4_parts_knows_Spy)
 apply (analz_mono_contra, simp_all)
   subgoal \<comment> \<open>Fake\<close> by blast
-  subgoal \<comment> \<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
+  subgoal \<comment> \<open>YM3 because the message \<^term>\<open>Crypt K (Nonce NB)\<close> could not exist\<close>
      by (force dest!: Crypt_imp_keysFor)
-   subgoal \<comment> \<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
+   subgoal \<comment> \<open>YM4: was \<^term>\<open>Crypt K (Nonce NB)\<close> the very last message? If not, use the induction hypothesis,
                otherwise by unicity of session keys\<close>
      by (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK Crypt_Spy_analz_bad
              dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
 done