src/HOL/Auth/Yahalom.ML
changeset 2377 ad9d2dedaeaa
parent 2322 fbe6dd4abddc
child 2451 ce85a2aafc7a
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Dec 13 10:42:58 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Dec 13 10:57:50 1996 +0100
     1.3 @@ -331,13 +331,13 @@
     1.4  by analz_Fake_tac;
     1.5  by (ALLGOALS
     1.6      (asm_simp_tac 
     1.7 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
     1.8 +     (!simpset addsimps ([not_parts_not_analz,
     1.9                            analz_insert_Key_newK] @ pushes)
    1.10                 setloop split_tac [expand_if])));
    1.11  (*YM3*)
    1.12  by (Fast_tac 2);  (*uses Says_too_new_key*)
    1.13  (*OR4, Fake*) 
    1.14 -by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    1.15 +by (REPEAT_FIRST spy_analz_tac);
    1.16  (*Oops*) (** LEVEL 6 **)
    1.17  by (fast_tac (!claset delrules [disjE] 
    1.18                        addDs [unique_session_keys]
    1.19 @@ -451,6 +451,7 @@
    1.20  by (fast_tac (!claset addSDs [spec]) 1);
    1.21  qed "unique_NB";
    1.22  
    1.23 +(*OLD VERSION
    1.24  fun lost_tac s =
    1.25      case_tac ("(" ^ s ^ ") : lost") THEN'
    1.26      SELECT_GOAL 
    1.27 @@ -458,6 +459,7 @@
    1.28         REPEAT_DETERM (etac MPair_analz 1) THEN
    1.29         dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN
    1.30         assume_tac 1 THEN Fast_tac 1);
    1.31 +*)
    1.32  
    1.33  fun lost_tac s =
    1.34      case_tac ("(" ^ s ^ ") : lost") THEN'
    1.35 @@ -610,7 +612,7 @@
    1.36     (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
    1.37      assume_tac ORELSE'
    1.38      depth_tac (!claset delrules [conjI]
    1.39 -                       addSIs [exI, impOfSubs (subset_insertI RS analz_mono),
    1.40 +                       addSIs [exI, analz_insertI,
    1.41                                 impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
    1.42  
    1.43  (*The only nonces that can be found with the help of session keys are
    1.44 @@ -627,7 +629,7 @@
    1.45  by analz_Fake_tac;
    1.46  by (ALLGOALS  (*28 seconds*)
    1.47      (asm_simp_tac 
    1.48 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
    1.49 +     (!simpset addsimps ([not_parts_not_analz,
    1.50                            analz_image_newK,
    1.51                            insert_Key_singleton, insert_Key_image]
    1.52                           @ pushes)
    1.53 @@ -649,8 +651,7 @@
    1.54  (*YM4*)
    1.55  (** LEVEL 11 **)
    1.56  by (rtac (impI RS allI) 1);
    1.57 -by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1 THEN 
    1.58 -    Fast_tac 1);
    1.59 +by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
    1.60  by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
    1.61  by (asm_simp_tac (!simpset addsimps [analz_image_newK]
    1.62                             setloop split_tac [expand_if]) 1);
    1.63 @@ -662,7 +663,7 @@
    1.64      THEN REPEAT (assume_tac 1));
    1.65  by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
    1.66  by (fast_tac (!claset delrules [conjI]
    1.67 -                      addIs [impOfSubs (subset_insertI RS analz_mono)]
    1.68 +                      addIs [analz_insertI]
    1.69                        addss (!simpset)) 1);
    1.70  val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
    1.71  
    1.72 @@ -695,14 +696,14 @@
    1.73  by analz_Fake_tac;
    1.74  by (ALLGOALS
    1.75      (asm_simp_tac 
    1.76 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
    1.77 +     (!simpset addsimps ([not_parts_not_analz,
    1.78                            analz_insert_Key_newK] @ pushes)
    1.79                 setloop split_tac [expand_if])));
    1.80  by (fast_tac (!claset addSIs [parts_insertI]
    1.81                        addSEs partsEs
    1.82                        addEs [Says_imp_old_nonces RS less_irrefl]
    1.83                        addss (!simpset)) 2);
    1.84 -(*Proof of YM2*) (** LEVEL 5 **)
    1.85 +(*Proof of YM2*) (** LEVEL 4 **)
    1.86  by (REPEAT (Safe_step_tac 2 ORELSE Fast_tac 2)); 
    1.87  by (fast_tac (!claset addIs [parts_insertI]
    1.88                        addSEs partsEs
    1.89 @@ -712,21 +713,21 @@
    1.90  (*Prove YM3 by showing that no NB can also be an NA*)
    1.91  by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
    1.92  by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
    1.93 -(*Fake*) (** LEVEL 10 **)
    1.94 -by (SELECT_GOAL (REPEAT (Safe_step_tac 1 ORELSE spy_analz_tac 1)) 1);
    1.95 -(*YM4*)
    1.96 +(*Fake*)
    1.97 +by (spy_analz_tac 1);
    1.98 +(*YM4*) (** LEVEL 10 **)
    1.99  by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
   1.100  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.101 -by (SELECT_GOAL (REPEAT_FIRST (Safe_step_tac ORELSE' spy_analz_tac)) 1);
   1.102 -(** LEVEL 14 **)
   1.103 +by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1);
   1.104 +(** LEVEL 13 **)
   1.105  by (lost_tac "Aa" 1);
   1.106  by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   1.107  by (forward_tac [Says_Server_message_form] 3);
   1.108  by (forward_tac [Says_Server_imp_YM2] 4);
   1.109  by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
   1.110  by (Full_simp_tac 1);
   1.111 +by (REPEAT_FIRST hyp_subst_tac);
   1.112  (** LEVEL 20 **)
   1.113 -by (REPEAT_FIRST hyp_subst_tac);
   1.114  by (lost_tac "Ba" 1);
   1.115  by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
   1.116  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.117 @@ -735,7 +736,7 @@
   1.118  by (dtac Spy_not_see_encrypted_key 1);
   1.119  by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
   1.120  by (spy_analz_tac 1);
   1.121 -(*Oops case*) (** LEVEL 28 **)
   1.122 +(*Oops case*) (** LEVEL 27 **)
   1.123  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.124  by (step_tac (!claset delrules [disjE, conjI]) 1);
   1.125  by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   1.126 @@ -743,7 +744,7 @@
   1.127  by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
   1.128  by (rtac conjI 1);
   1.129  by (no_nonce_tac 1);
   1.130 -(** LEVEL 35 **)
   1.131 +(** LEVEL 34 **)
   1.132  by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
   1.133  by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
   1.134  val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
   1.135 @@ -777,5 +778,3 @@
   1.136  by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
   1.137  qed "B_trusts_YM4";
   1.138  
   1.139 -
   1.140 -