src/HOL/Auth/WooLam.thy
changeset 13507 febb8e5d2a9d
parent 11251 a6816d47f41d
child 14207 f20fbb141673
     1.1 --- a/src/HOL/Auth/WooLam.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -74,8 +74,7 @@
     1.4  apply (intro exI bexI)
     1.5  apply (rule_tac [2] woolam.Nil
     1.6                      [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
     1.7 -                     THEN woolam.WL4, THEN woolam.WL5])
     1.8 -apply possibility
     1.9 +                     THEN woolam.WL4, THEN woolam.WL5], possibility)
    1.10  done
    1.11  
    1.12  (*Could prove forwarding lemmas for WL4, but we do not need them!*)
    1.13 @@ -88,8 +87,7 @@
    1.14  (*Spy never sees a good agent's shared key!*)
    1.15  lemma Spy_see_shrK [simp]:
    1.16       "evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
    1.17 -apply (erule woolam.induct, force, simp_all)
    1.18 -apply blast+
    1.19 +apply (erule woolam.induct, force, simp_all, blast+)
    1.20  done
    1.21  
    1.22  lemma Spy_analz_shrK [simp]:
    1.23 @@ -110,8 +108,7 @@
    1.24       "[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
    1.25           A \<notin> bad;  evs \<in> woolam |]
    1.26        ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
    1.27 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
    1.28 -apply blast+
    1.29 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.30  done
    1.31  
    1.32  (*Guarantee for Server: if it gets a message containing a certificate from
    1.33 @@ -133,8 +130,7 @@
    1.34           evs \<in> woolam |]
    1.35        ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
    1.36               \<in> set evs"
    1.37 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
    1.38 -apply blast+
    1.39 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.40  done
    1.41  
    1.42  (*If the encrypted message appears then it originated with the Server!*)
    1.43 @@ -142,8 +138,7 @@
    1.44       "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
    1.45           B \<notin> bad;  evs \<in> woolam |]
    1.46        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
    1.47 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
    1.48 -apply blast+
    1.49 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.50  done
    1.51  
    1.52  (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
    1.53 @@ -161,8 +156,7 @@
    1.54  lemma B_said_WL2:
    1.55       "[| Says B A (Nonce NB) \<in> set evs;  B \<noteq> Spy;  evs \<in> woolam |]
    1.56        ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
    1.57 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
    1.58 -apply blast+
    1.59 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
    1.60  done
    1.61  
    1.62  
    1.63 @@ -171,9 +165,7 @@
    1.64    ==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) &
    1.65        Says B A (Nonce NB) \<in> set evs
    1.66        --> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
    1.67 -apply (erule rev_mp, erule woolam.induct, force, simp_all)
    1.68 -apply blast
    1.69 -apply auto
    1.70 +apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto)
    1.71  oops
    1.72  
    1.73  end