doc-src/TutorialI/Protocol/NS_Public.thy
changeset 32960 69916a850301
parent 32891 d403b99287ff
child 35503 7bba12c3b7b6
--- a/doc-src/TutorialI/Protocol/NS_Public.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/doc-src/TutorialI/Protocol/NS_Public.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -221,8 +221,8 @@
 lemma A_trusts_NS2_lemma [rule_format]:
    "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
     \<Longrightarrow> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow>
-	Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
-	Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
+        Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
+        Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
 apply (erule ns_public.induct, simp_all)
 (*Fake, NS1*)
 apply (blast dest: Spy_not_see_NA)+
@@ -240,8 +240,8 @@
 lemma B_trusts_NS1 [rule_format]:
      "evs \<in> ns_public
       \<Longrightarrow> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow>
-	  Nonce NA \<notin> analz (knows Spy evs) \<longrightarrow>
-	  Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
+          Nonce NA \<notin> analz (knows Spy evs) \<longrightarrow>
+          Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
 apply (erule ns_public.induct, simp_all)
 (*Fake*)
 apply (blast intro!: analz_insertI)