src/HOL/Auth/NS_Shared.thy
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 13926 6e62e5357a10
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -85,8 +85,7 @@
     1.4  apply (intro exI bexI)
     1.5  apply (rule_tac [2] ns_shared.Nil
     1.6         [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
     1.7 -	THEN ns_shared.NS4, THEN ns_shared.NS5])
     1.8 -apply possibility
     1.9 +	THEN ns_shared.NS4, THEN ns_shared.NS5], possibility)
    1.10  done
    1.11  
    1.12  (*This version is similar, while instantiating ?K and ?N to epsilon-terms
    1.13 @@ -116,9 +115,7 @@
    1.14  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.15  lemma Spy_see_shrK [simp]:
    1.16       "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"
    1.17 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.18 -apply simp_all
    1.19 -apply blast+;
    1.20 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
    1.21  done
    1.22  
    1.23  lemma Spy_analz_shrK [simp]:
    1.24 @@ -129,8 +126,7 @@
    1.25  (*Nobody can have used non-existent keys!*)
    1.26  lemma new_keys_not_used [rule_format, simp]:
    1.27      "evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))"
    1.28 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.29 -apply simp_all
    1.30 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
    1.31  (*Fake, NS2, NS4, NS5*)
    1.32  apply (blast dest!: keysFor_parts_insert)+
    1.33  done
    1.34 @@ -154,8 +150,7 @@
    1.35         A \\<notin> bad;  evs \\<in> ns_shared\\<rbrakk>
    1.36        \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs"
    1.37  apply (erule rev_mp)
    1.38 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.39 -apply auto
    1.40 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
    1.41  done
    1.42  
    1.43  lemma cert_A_form:
    1.44 @@ -182,7 +177,7 @@
    1.45     \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs
    1.46         \\<or> X \\<in> analz (spies evs)"
    1.47  apply (case_tac "A \\<in> bad")
    1.48 -apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]);
    1.49 +apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
    1.50  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
    1.51  *)
    1.52  
    1.53 @@ -202,8 +197,7 @@
    1.54  lemma  "\\<lbrakk>evs \\<in> ns_shared;  Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
    1.55           (Crypt KAB X) \\<in> parts (spies evs) \\<and>
    1.56           Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)"
    1.57 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.58 -apply simp_all
    1.59 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
    1.60  (*Fake*)
    1.61  apply (blast dest: parts_insert_subset_Un)
    1.62  (*Base, NS4 and NS5*)
    1.63 @@ -222,9 +216,7 @@
    1.64               (K \\<in> KK \\<or> Key K \\<in> analz (spies evs))"
    1.65  apply (erule ns_shared.induct, force)
    1.66  apply (drule_tac [7] Says_Server_message_form)
    1.67 -apply (erule_tac [4] Says_S_message_form [THEN disjE])
    1.68 -apply analz_freshK
    1.69 -apply spy_analz
    1.70 +apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
    1.71  done
    1.72  
    1.73  
    1.74 @@ -242,9 +234,7 @@
    1.75       "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
    1.76         Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs;
    1.77         evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'"
    1.78 -apply (erule rev_mp, erule rev_mp, erule ns_shared.induct)
    1.79 -apply simp_all
    1.80 -apply blast+
    1.81 +apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
    1.82  done
    1.83  
    1.84  
    1.85 @@ -263,8 +253,7 @@
    1.86  apply (frule_tac [7] Says_Server_message_form)
    1.87  apply (frule_tac [4] Says_S_message_form)
    1.88  apply (erule_tac [5] disjE)
    1.89 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
    1.90 -apply spy_analz  (*Fake*)
    1.91 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)  (*Fake*)
    1.92  apply blast      (*NS2*)
    1.93  (*NS3, Server sub-case*) (**LEVEL 8 **)
    1.94  apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
    1.95 @@ -295,8 +284,7 @@
    1.96                                   Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
    1.97                \\<in> set evs"
    1.98  apply (erule rev_mp)
    1.99 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.100 -apply auto
   1.101 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   1.102  done
   1.103  
   1.104  
   1.105 @@ -307,12 +295,10 @@
   1.106        Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
   1.107        Says B A (Crypt K (Nonce NB)) \\<in> set evs"
   1.108  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.109 -apply (analz_mono_contra, simp_all)
   1.110 -apply blast     (*Fake*)
   1.111 +apply (analz_mono_contra, simp_all, blast)     (*Fake*)
   1.112  (*NS2: contradiction from the assumptions
   1.113    Key K \\<notin> used evs2  and Crypt K (Nonce NB) \\<in> parts (spies evs2) *)
   1.114 -apply (force dest!: Crypt_imp_keysFor)
   1.115 -apply blast     (*NS3*)
   1.116 +apply (force dest!: Crypt_imp_keysFor, blast)     (*NS3*)
   1.117  (*NS4*)
   1.118  apply (blast dest!: B_trusts_NS3
   1.119  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.120 @@ -338,10 +324,8 @@
   1.121       Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
   1.122       Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
   1.123       (\\<exists>A'. Says A' B X \\<in> set evs)"
   1.124 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.125 -apply analz_mono_contra
   1.126 -apply (simp_all add: ex_disj_distrib)
   1.127 -apply blast  (*Fake*)
   1.128 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
   1.129 +apply (simp_all add: ex_disj_distrib, blast)  (*Fake*)
   1.130  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   1.131  apply blast  (*NS3*)
   1.132  (*NS4*)
   1.133 @@ -359,10 +343,7 @@
   1.134  			    Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow>
   1.135       Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow>
   1.136       Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
   1.137 -apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.138 -apply analz_mono_contra
   1.139 -apply simp_all
   1.140 -apply blast  (*Fake*)
   1.141 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)  (*Fake*)
   1.142  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   1.143  apply (blast dest!: cert_A_form) (*NS3*)
   1.144  (*NS5*)