src/HOL/Auth/OtwayRees_Bad.thy
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 14200 d8598e24f8fa
     1.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -98,15 +98,13 @@
     1.4  apply (rule_tac [2] otway.Nil
     1.5                      [THEN otway.OR1, THEN otway.Reception,
     1.6                       THEN otway.OR2, THEN otway.Reception,
     1.7 -                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
     1.8 -apply possibility
     1.9 +                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
    1.10  done
    1.11  
    1.12  lemma Gets_imp_Says [dest!]:
    1.13       "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
    1.14  apply (erule rev_mp)
    1.15 -apply (erule otway.induct)
    1.16 -apply auto
    1.17 +apply (erule otway.induct, auto)
    1.18  done
    1.19  
    1.20  
    1.21 @@ -142,8 +140,7 @@
    1.22  lemma Spy_see_shrK [simp]:
    1.23       "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
    1.24  apply (erule otway.induct, force,
    1.25 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    1.26 -apply blast+
    1.27 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    1.28  done
    1.29  
    1.30  lemma Spy_analz_shrK [simp]:
    1.31 @@ -164,8 +161,7 @@
    1.32           evs \<in> otway |]
    1.33        ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
    1.34  apply (erule rev_mp)
    1.35 -apply (erule otway.induct, simp_all)
    1.36 -apply blast
    1.37 +apply (erule otway.induct, simp_all, blast)
    1.38  done
    1.39  
    1.40  
    1.41 @@ -190,9 +186,7 @@
    1.42  apply (erule otway.induct, force)
    1.43  apply (frule_tac [7] Says_Server_message_form)
    1.44  apply (drule_tac [6] OR4_analz_knows_Spy)
    1.45 -apply (drule_tac [4] OR2_analz_knows_Spy)
    1.46 -apply analz_freshK
    1.47 -apply spy_analz
    1.48 +apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
    1.49  done
    1.50  
    1.51  lemma analz_insert_freshK:
    1.52 @@ -231,8 +225,7 @@
    1.53  apply (frule_tac [7] Says_Server_message_form)
    1.54  apply (drule_tac [6] OR4_analz_knows_Spy)
    1.55  apply (drule_tac [4] OR2_analz_knows_Spy)
    1.56 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
    1.57 -apply spy_analz  (*Fake*)
    1.58 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
    1.59  (*OR3, OR4, Oops*)
    1.60  apply (blast dest: unique_session_keys)+
    1.61  done
    1.62 @@ -259,8 +252,7 @@
    1.63            Says A B {|NA, Agent A, Agent B,
    1.64                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \<in> set evs"
    1.65  apply (erule otway.induct, force,
    1.66 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    1.67 -apply blast+
    1.68 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    1.69  done
    1.70  
    1.71  
    1.72 @@ -279,8 +271,7 @@
    1.73                    Crypt (shrK A) {|NA, Key K|},
    1.74                    Crypt (shrK B) {|NB, Key K|}|}  \<in> set evs)"
    1.75  apply (erule otway.induct, force,
    1.76 -       drule_tac [4] OR2_parts_knows_Spy)
    1.77 -apply simp_all
    1.78 +       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    1.79  (*Fake*)
    1.80  apply blast
    1.81  (*OR1: it cannot be a new Nonce, contradiction.*)