# HG changeset patch
# User wenzelm
# Date 1126797415 -7200
# Node ID 664434175578f2b87822565452da78407ece35ee
# Parent  1e2c8c38ca1d861a24e7f5dedacab10bdbbbbb86
fixed document;

diff -r 1e2c8c38ca1d -r 664434175578 src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Thu Sep 15 17:16:54 2005 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Thu Sep 15 17:16:55 2005 +0200
@@ -238,7 +238,7 @@
 
 text{*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
-  over-simplified version of this protocol: see OtwayRees_Bad.*}
+  over-simplified version of this protocol: see @{text OtwayRees_Bad}.*}
 lemma no_nonce_OR1_OR2:
    "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
        A \<notin> bad;  evs \<in> otway |]
@@ -270,7 +270,7 @@
 text{*Corollary: if A receives B's OR4 message and the nonce NA agrees
   then the key really did come from the Server!  CANNOT prove this of the
   bad form of this protocol, even though we can prove
-  Spy_not_see_encrypted_key*}
+  @{text Spy_not_see_encrypted_key} *}
 lemma A_trusts_OR4:
      "[| Says A  B {|NA, Agent A, Agent B,
                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
diff -r 1e2c8c38ca1d -r 664434175578 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Thu Sep 15 17:16:54 2005 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Thu Sep 15 17:16:55 2005 +0200
@@ -297,10 +297,12 @@
 apply blast+
 done
 
-text{*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  Nonce NB \<notin> analz(knows Spy evs)  must
-  be the FIRST antecedent of the induction formula.*}
+text{*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
+  induction formula.*}
+
 lemma B_trusts_YM4_newK [rule_format]:
      "[|Crypt K (Nonce NB) \<in> parts (knows Spy evs);
         Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
@@ -392,9 +394,10 @@
             analz_image_freshK fresh_not_KeyWithNonce
             imp_disj_not1               (*Moves NBa\<noteq>NB to the front*)
             Says_Server_KeyWithNonce)
-txt{*For Oops, simplification proves NBa\<noteq>NB.  By Says_Server_KeyWithNonce,
-  we get (~ KeyWithNonce K NB evs); then simplification can apply the
-  induction hypothesis with KK = {K}.*}
+txt{*For Oops, simplification proves @{prop "NBa\<noteq>NB"}.  By
+  @{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB
+  evs"}; then simplification can apply the induction hypothesis with
+  @{term "KK = {K}"}.*}
 txt{*Fake*}
 apply spy_analz
 txt{*YM2*}
@@ -403,8 +406,9 @@
 apply blast
 txt{*YM4*}
 apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
-txt{*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB.  Previous two steps 
-   make the next step faster.*}
+txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore
+  @{prop "NBa \<noteq> NB"}.  Previous two steps make the next step
+  faster.*}
 apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
          dest: analz.Inj
            parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI])
@@ -501,7 +505,7 @@
 apply (clarify, simp add: all_conj_distrib)
 txt{*YM4: key K is visible to Spy, contradicting session key secrecy theorem*}
 txt{*Case analysis on Aa:bad; PROOF FAILED problems
-  use Says_unique_NB to identify message components: Aa=A, Ba=B*}
+  use @{text Says_unique_NB} to identify message components: @{term "Aa=A"}, @{term "Ba=B"}*}
 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
@@ -513,7 +517,7 @@
 apply (case_tac "NB = NBa")
 txt{*If NB=NBa then all other components of the Oops message agree*}
 apply (blast dest: Says_unique_NB)
-txt{*case NB \<noteq> NBa*}
+txt{*case @{prop "NB \<noteq> NBa"}*}
 apply (simp add: single_Nonce_secrecy)
 apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*))
 done
@@ -521,7 +525,7 @@
 
 text{*B's session key guarantee from YM4.  The two certificates contribute to a
   single conclusion about the Server's message.  Note that the "Notes Spy"
-  assumption must quantify over \<forall>POSSIBLE keys instead of our particular K.
+  assumption must quantify over @{text \<forall>} POSSIBLE keys instead of our particular K.
   If this run is broken and the spy substitutes a certificate containing an
   old key, B has no means of telling.*}
 lemma B_trusts_YM4: