src/HOL/Auth/Yahalom.thy
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 13926 6e62e5357a10
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -94,8 +94,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 @@ -135,8 +134,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 @@ -170,8 +168,7 @@
    1.24       "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}  
    1.25             \<in> set evs;   evs \<in> yahalom |]                                 
    1.26        ==> K \<notin> range shrK"
    1.27 -apply (erule rev_mp, erule yahalom.induct, simp_all)
    1.28 -apply blast
    1.29 +apply (erule rev_mp, erule yahalom.induct, simp_all, blast)
    1.30  done
    1.31  
    1.32  
    1.33 @@ -197,9 +194,7 @@
    1.34            (Key K \<in> analz (Key`KK Un (knows Spy evs))) =   
    1.35            (K \<in> KK | Key K \<in> analz (knows Spy evs))"
    1.36  apply (erule yahalom.induct, force, 
    1.37 -       drule_tac [6] YM4_analz_knows_Spy)
    1.38 -apply analz_freshK
    1.39 -apply spy_analz
    1.40 +       drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
    1.41  apply (simp only: Says_Server_not_range analz_image_freshK_simps)
    1.42  done
    1.43  
    1.44 @@ -238,8 +233,7 @@
    1.45            Key K \<notin> analz (knows Spy evs)"
    1.46  apply (erule yahalom.induct, force, 
    1.47         drule_tac [6] YM4_analz_knows_Spy)
    1.48 -apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
    1.49 -apply spy_analz  (*Fake*)
    1.50 +apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)  (*Fake*)
    1.51  apply (blast dest: unique_session_keys)+  (*YM3, Oops*)
    1.52  done
    1.53  
    1.54 @@ -401,8 +395,7 @@
    1.55  (*Fake*) 
    1.56  apply spy_analz
    1.57  (*YM4*)  (** LEVEL 6 **)
    1.58 -apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl)
    1.59 -apply clarify
    1.60 +apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
    1.61  (*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB.  Previous two steps make
    1.62    the next step faster.*)
    1.63  apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
    1.64 @@ -423,7 +416,7 @@
    1.65            (Nonce NB \<in> analz (knows Spy evs))"
    1.66  by (simp_all del: image_insert image_Un imp_disjL
    1.67               add: analz_image_freshK_simps split_ifs
    1.68 -                  Nonce_secrecy Says_Server_KeyWithNonce);
    1.69 +                  Nonce_secrecy Says_Server_KeyWithNonce)
    1.70  
    1.71  
    1.72  (*** The Nonce NB uniquely identifies B's message. ***)
    1.73 @@ -474,8 +467,7 @@
    1.74           evs \<in> yahalom |]                                              
    1.75        ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}  
    1.76               \<in> set evs"
    1.77 -apply (erule rev_mp, erule yahalom.induct)
    1.78 -apply auto
    1.79 +apply (erule rev_mp, erule yahalom.induct, auto)
    1.80  done
    1.81  
    1.82