src/HOL/Auth/OtwayRees.ML
changeset 3121 cbb6c0c1c58a
parent 3102 4d01cdc119d2
child 3207 fe79ad367d77
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed May 07 12:50:26 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Wed May 07 13:01:43 1997 +0200
     1.3 @@ -18,8 +18,7 @@
     1.4  HOL_quantifiers := false;
     1.5  
     1.6  (*Replacing the variable by a constant improves search speed by 50%!*)
     1.7 -val Says_imp_sees_Spy' = 
     1.8 -    read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
     1.9 +val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
    1.10  
    1.11  
    1.12  (*A "possibility property": there are traces that reach the end*)
    1.13 @@ -81,35 +80,30 @@
    1.14  bind_thm ("OR4_parts_sees_Spy",
    1.15            OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.16  
    1.17 -(*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    1.18 -  harder to complete, since simplification does less for us.*)
    1.19 -val parts_Fake_tac = 
    1.20 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    1.21 +  We instantiate the variable to "lost" since leaving it as a Var would
    1.22 +  interfere with simplification.*)
    1.23 +val parts_induct_tac = 
    1.24      let val tac = forw_inst_tac [("lost","lost")] 
    1.25 -    in  tac OR2_parts_sees_Spy     4 THEN 
    1.26 +    in  etac otway.induct	   1 THEN 
    1.27 +	tac OR2_parts_sees_Spy     4 THEN 
    1.28          tac OR4_parts_sees_Spy     6 THEN
    1.29 -        tac Oops_parts_sees_Spy    7
    1.30 +        tac Oops_parts_sees_Spy    7 THEN
    1.31 +	prove_simple_subgoals_tac  1
    1.32      end;
    1.33  
    1.34 -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.35 -fun parts_induct_tac i = SELECT_GOAL
    1.36 -    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    1.37 -             (*Fake message*)
    1.38 -             TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.39 -                                           impOfSubs Fake_parts_insert]
    1.40 -                            unsafe_addss (!simpset)) 2)) THEN
    1.41 -     (*Base case*)
    1.42 -     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
    1.43 -     ALLGOALS Asm_simp_tac) i;
    1.44  
    1.45  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.46      sends messages containing X! **)
    1.47  
    1.48 +
    1.49  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.50  goal thy 
    1.51   "!!evs. evs : otway lost \
    1.52  \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.53 -by (parts_induct_tac 1);
    1.54 -by (Auto_tac());
    1.55 +by parts_induct_tac;
    1.56 +by (Fake_parts_insert_tac 1);
    1.57 +by (Blast_tac 1);
    1.58  qed "Spy_see_shrK";
    1.59  Addsimps [Spy_see_shrK];
    1.60  
    1.61 @@ -132,7 +126,7 @@
    1.62  (*Nobody can have used non-existent keys!*)
    1.63  goal thy "!!evs. evs : otway lost ==>          \
    1.64  \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
    1.65 -by (parts_induct_tac 1);
    1.66 +by parts_induct_tac;
    1.67  (*Fake*)
    1.68  by (best_tac
    1.69        (!claset addIs [impOfSubs analz_subset_parts]
    1.70 @@ -167,7 +161,7 @@
    1.71  
    1.72  
    1.73  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
    1.74 -val analz_Fake_tac = 
    1.75 +val analz_sees_tac = 
    1.76      dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
    1.77      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
    1.78      forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
    1.79 @@ -194,7 +188,7 @@
    1.80  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
    1.81  \            (K : KK | Key K : analz (sees lost Spy evs))";
    1.82  by (etac otway.induct 1);
    1.83 -by analz_Fake_tac;
    1.84 +by analz_sees_tac;
    1.85  by (REPEAT_FIRST (resolve_tac [allI, impI]));
    1.86  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
    1.87  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    1.88 @@ -254,7 +248,8 @@
    1.89  \            Says A B {|NA, Agent A, Agent B,                      \
    1.90  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    1.91  \             : set_of_list evs";
    1.92 -by (parts_induct_tac 1);
    1.93 +by parts_induct_tac;
    1.94 +by (Fake_parts_insert_tac 1);
    1.95  qed_spec_mp "Crypt_imp_OR1";
    1.96  
    1.97  
    1.98 @@ -265,7 +260,8 @@
    1.99  \ ==> EX B'. ALL B.    \
   1.100  \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
   1.101  \        --> B = B'";
   1.102 -by (parts_induct_tac 1);
   1.103 +by parts_induct_tac;
   1.104 +by (Fake_parts_insert_tac 1);
   1.105  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.106  (*OR1: creation of new Nonce.  Move assertion into global context*)
   1.107  by (expand_case_tac "NA = ?y" 1);
   1.108 @@ -290,7 +286,8 @@
   1.109  \             : parts (sees lost Spy evs) -->                    \
   1.110  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   1.111  \             ~: parts (sees lost Spy evs)";
   1.112 -by (parts_induct_tac 1);
   1.113 +by parts_induct_tac;
   1.114 +by (Fake_parts_insert_tac 1);
   1.115  by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
   1.116                                 addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   1.117  qed_spec_mp"no_nonce_OR1_OR2";
   1.118 @@ -309,7 +306,8 @@
   1.119  \                   Crypt (shrK A) {|NA, Key K|},                      \
   1.120  \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   1.121  \                   : set_of_list evs)";
   1.122 -by (parts_induct_tac 1);
   1.123 +by parts_induct_tac;
   1.124 +by (Fake_parts_insert_tac 1);
   1.125  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.126  by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   1.127  (*OR3 and OR4*) 
   1.128 @@ -364,7 +362,7 @@
   1.129  \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   1.130  \            Key K ~: analz (sees lost Spy evs)";
   1.131  by (etac otway.induct 1);
   1.132 -by analz_Fake_tac;
   1.133 +by analz_sees_tac;
   1.134  by (ALLGOALS
   1.135      (asm_simp_tac (!simpset addcongs [conj_cong] 
   1.136                              addsimps [not_parts_not_analz, analz_insert_freshK]
   1.137 @@ -418,7 +416,8 @@
   1.138  \             {|NA, Agent A, Agent B, X,                       \
   1.139  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   1.140  \             : set_of_list evs)";
   1.141 -by (parts_induct_tac 1);
   1.142 +by parts_induct_tac;
   1.143 +by (Fake_parts_insert_tac 1);
   1.144  by (ALLGOALS Blast_tac);
   1.145  bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   1.146  
   1.147 @@ -430,7 +429,8 @@
   1.148  \ ==> EX NA' A'. ALL NA A.                               \
   1.149  \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
   1.150  \      --> NA = NA' & A = A'";
   1.151 -by (parts_induct_tac 1);
   1.152 +by parts_induct_tac;
   1.153 +by (Fake_parts_insert_tac 1);
   1.154  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.155  (*OR2: creation of new Nonce.  Move assertion into global context*)
   1.156  by (expand_case_tac "NB = ?y" 1);
   1.157 @@ -461,7 +461,8 @@
   1.158  \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   1.159  \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   1.160  \                   : set_of_list evs)";
   1.161 -by (parts_induct_tac 1);
   1.162 +by parts_induct_tac;
   1.163 +by (Fake_parts_insert_tac 1);
   1.164  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.165  by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   1.166  (*OR4*)