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.*)
```