src/HOL/Auth/Yahalom.thy
changeset 69597 ff784d5a5bfb
parent 67613 ce654b0e6d69
--- a/src/HOL/Auth/Yahalom.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -55,7 +55,7 @@
  | 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>
@@ -129,7 +129,7 @@
       \<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>
@@ -299,8 +299,8 @@
 
 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]:
@@ -393,14 +393,14 @@
             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
@@ -491,7 +491,7 @@
     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]
@@ -581,7 +581,7 @@
 
 
 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
@@ -597,9 +597,9 @@
        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)