src/HOL/Auth/OtwayRees_AN.thy

      "[| Says Server B
             \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
               Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
            \<in> set evs;
          evs \<in> otway |]
-      ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
+      ==> K \<notin> range shrK \<and> (\<exists>i. NA = Nonce i) \<and> (\<exists>j. NB = Nonce j)"
 apply (erule rev_mp)
 apply (erule otway.induct, auto)
 done
 
 

 text\<open>Session keys are not used to encrypt other session keys\<close>
 
 text\<open>The equality makes the induction hypothesis easier to apply\<close>
 lemma analz_image_freshK [rule_format]:
  "evs \<in> otway ==>
-   \<forall>K KK. KK <= -(range shrK) -->
-          (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
+   \<forall>K KK. KK \<subseteq> -(range shrK) \<longrightarrow>
+          (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) =
           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
 apply (erule otway.induct) 
 apply (frule_tac [8] Says_Server_message_form)
 apply (drule_tac [7] OR4_analz_knows_Spy, analz_freshK, spy_analz, auto) 
 done

         Says Server B'
           \<lbrace>Crypt (shrK A') \<lbrace>NA', Agent A', Agent B', K\<rbrace>,
             Crypt (shrK B') \<lbrace>NB', Agent A', Agent B', K\<rbrace>\<rbrace>
          \<in> set evs;
         evs \<in> otway |]
-     ==> A=A' & B=B' & NA=NA' & NB=NB'"
+     ==> A=A' \<and> B=B' \<and> NA=NA' \<and> NB=NB'"
 apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all)
 apply blast+  \<comment> \<open>OR3 and OR4\<close>
 done
 
 

 
 text\<open>If the encrypted message appears then it originated with the Server!\<close>
 lemma NA_Crypt_imp_Server_msg [rule_format]:
     "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
      ==> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace> \<in> parts (knows Spy evs)
-       --> (\<exists>NB. Says Server B
+       \<longrightarrow> (\<exists>NB. Says Server B
                     \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
                       Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
                     \<in> set evs)"
 apply (erule otway.induct, force)
 apply (simp_all add: ex_disj_distrib)

 lemma secrecy_lemma:
      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> otway |]
       ==> Says Server B
            \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
              Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
-          \<in> set evs -->
-          Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs -->
+          \<in> set evs \<longrightarrow>
+          Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs \<longrightarrow>
           Key K \<notin> analz (knows Spy evs)"
 apply (erule otway.induct, force)
 apply (frule_tac [7] Says_Server_message_form)
 apply (drule_tac [6] OR4_analz_knows_Spy)
 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)

 
 text\<open>If the encrypted message appears then it originated with the Server!\<close>
 lemma NB_Crypt_imp_Server_msg [rule_format]:
  "[| B \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
   ==> Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace> \<in> parts (knows Spy evs)
-      --> (\<exists>NA. Says Server B
+      \<longrightarrow> (\<exists>NA. Says Server B
                    \<lbrace>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B, Key K\<rbrace>,
                      Crypt (shrK B) \<lbrace>NB, Agent A, Agent B, Key K\<rbrace>\<rbrace>
                    \<in> set evs)"
 apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
 apply blast+  \<comment> \<open>Fake, OR3\<close>