src/HOL/Auth/OtwayRees.thy
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 13907 2bc462b99e70
     1.1 --- a/src/HOL/Auth/OtwayRees.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.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 @@ -141,8 +139,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 @@ -162,8 +159,7 @@
    1.32       "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
    1.33           evs \<in> otway |]
    1.34        ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
    1.35 -apply (erule rev_mp, erule otway.induct, simp_all)
    1.36 -apply blast
    1.37 +apply (erule rev_mp, erule otway.induct, simp_all, blast)
    1.38  done
    1.39  
    1.40  
    1.41 @@ -188,9 +184,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  
    1.52 @@ -225,8 +219,7 @@
    1.53                   Crypt (shrK A) {|NA, Agent A, Agent B|}|}
    1.54          \<in> set evs"
    1.55  apply (erule otway.induct, force,
    1.56 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    1.57 -apply blast+
    1.58 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    1.59  done
    1.60  
    1.61  lemma Crypt_imp_OR1_Gets:
    1.62 @@ -248,8 +241,7 @@
    1.63        ==> B = C"
    1.64  apply (erule rev_mp, erule rev_mp)
    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 @@ -262,8 +254,7 @@
    1.73      ==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)"
    1.74  apply (erule rev_mp)
    1.75  apply (erule otway.induct, force,
    1.76 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    1.77 -apply blast+
    1.78 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
    1.79  done
    1.80  
    1.81  (*Crucial property: If the encrypted message appears, and A has used NA
    1.82 @@ -278,8 +269,7 @@
    1.83                             Crypt (shrK A) {|NA, Key K|},
    1.84                             Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
    1.85  apply (erule otway.induct, force,
    1.86 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
    1.87 -apply blast
    1.88 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
    1.89  (*OR1: it cannot be a new Nonce, contradiction.*)
    1.90  apply blast
    1.91  (*OR3*)
    1.92 @@ -321,8 +311,7 @@
    1.93  apply (frule_tac [7] Says_Server_message_form)
    1.94  apply (drule_tac [6] OR4_analz_knows_Spy)
    1.95  apply (drule_tac [4] OR2_analz_knows_Spy)
    1.96 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
    1.97 -apply spy_analz  (*Fake*)
    1.98 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz)  (*Fake*)
    1.99  (*OR3, OR4, Oops*)
   1.100  apply (blast dest: unique_session_keys)+
   1.101  done
   1.102 @@ -363,8 +352,7 @@
   1.103                   \<in> set evs"
   1.104  apply (erule rev_mp)
   1.105  apply (erule otway.induct, force,
   1.106 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
   1.107 -apply blast+
   1.108 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
   1.109  done
   1.110  
   1.111  
   1.112 @@ -397,8 +385,7 @@
   1.113                      \<in> set evs)"
   1.114  apply simp
   1.115  apply (erule otway.induct, force,
   1.116 -       drule_tac [4] OR2_parts_knows_Spy, simp_all)
   1.117 -apply blast
   1.118 +       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
   1.119  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.120  (*OR2*)
   1.121  apply blast