src/HOL/Auth/OtwayRees_Bad.thy

               \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] otway.Nil
                     [THEN otway.OR1, THEN otway.Reception,
                      THEN otway.OR2, THEN otway.Reception,
-                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
-apply possibility
+                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
 done
 
 lemma Gets_imp_Says [dest!]:
      "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
 apply (erule rev_mp)
-apply (erule otway.induct)
-apply auto
+apply (erule otway.induct, auto)
 done
 
 
 (**** Inductive proofs about otway ****)
 

 
 (*Spy never sees a good agent's shared key!*)
 lemma Spy_see_shrK [simp]:
      "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 lemma Spy_analz_shrK [simp]:
      "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
 by auto

 lemma Says_Server_message_form:
      "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
          evs \<in> otway |]
       ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
 apply (erule rev_mp)
-apply (erule otway.induct, simp_all)
-apply blast
+apply (erule otway.induct, simp_all, blast)
 done
 
 
 (****
  The following is to prove theorems of the form

           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
           (K \<in> KK | Key K \<in> 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 (drule_tac [4] OR2_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
 done
 
 lemma analz_insert_freshK:
   "[| evs \<in> otway;  KAB \<notin> range shrK |] ==>
       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =

       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 (drule_tac [4] OR2_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
-apply spy_analz  (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
 (*OR3, OR4, Oops*)
 apply (blast dest: unique_session_keys)+
 done
 
 

      "[| A \<notin> bad;  A \<noteq> B;  evs \<in> otway |]
       ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
           Says A B {|NA, Agent A, Agent B,
                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \<in> set evs"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
 done
 
 
 (*Crucial property: If the encrypted message appears, and A has used NA
   to start a run, then it originated with the Server!

            (\<exists>B NB. Says Server B
                 {|NA,
                   Crypt (shrK A) {|NA, Key K|},
                   Crypt (shrK B) {|NB, Key K|}|}  \<in> set evs)"
 apply (erule otway.induct, force,
-       drule_tac [4] OR2_parts_knows_Spy)
-apply simp_all
+       drule_tac [4] OR2_parts_knows_Spy, simp_all)
 (*Fake*)
 apply blast
 (*OR1: it cannot be a new Nonce, contradiction.*)
 apply blast
 (*OR3 and OR4*)