src/HOL/Auth/Yahalom_Bad.thy
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 13926 6e62e5357a10
     1.1 --- a/src/HOL/Auth/Yahalom_Bad.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom_Bad.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -76,8 +76,7 @@
     1.4                      [THEN yahalom.YM1, THEN yahalom.Reception,
     1.5                       THEN yahalom.YM2, THEN yahalom.Reception,
     1.6                       THEN yahalom.YM3, THEN yahalom.Reception,
     1.7 -                     THEN yahalom.YM4])
     1.8 -apply possibility
     1.9 +                     THEN yahalom.YM4], possibility)
    1.10  done
    1.11  
    1.12  lemma Gets_imp_Says:
    1.13 @@ -113,8 +112,7 @@
    1.14  lemma Spy_see_shrK [simp]:
    1.15       "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
    1.16  apply (erule yahalom.induct, force,
    1.17 -       drule_tac [6] YM4_parts_knows_Spy, simp_all)
    1.18 -apply blast+
    1.19 +       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
    1.20  done
    1.21  
    1.22  lemma Spy_analz_shrK [simp]:
    1.23 @@ -152,9 +150,7 @@
    1.24            (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
    1.25            (K \<in> KK | Key K \<in> analz (knows Spy evs))"
    1.26  apply (erule yahalom.induct, force,
    1.27 -       drule_tac [6] YM4_analz_knows_Spy)
    1.28 -apply analz_freshK
    1.29 -apply spy_analz
    1.30 +       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
    1.31  done
    1.32  
    1.33  lemma analz_insert_freshK: "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
    1.34 @@ -189,8 +185,7 @@
    1.35             \<in> set evs -->
    1.36            Key K \<notin> analz (knows Spy evs)"
    1.37  apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy)
    1.38 -apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
    1.39 -apply spy_analz  (*Fake*)
    1.40 +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
    1.41  apply (blast dest: unique_session_keys)  (*YM3*)
    1.42  done
    1.43