Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
authorpaulson
Fri Sep 13 13:20:22 1996 +0200 (1996-09-13)
changeset 199633c42cae3dd0
parent 1995 c80e58e78d9c
child 1997 6efba890341e
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
Weak liveness
src/HOL/Auth/OtwayRees.ML
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 13:16:57 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Sep 13 13:20:22 1996 +0200
     1.3 @@ -15,6 +15,22 @@
     1.4  proof_timing:=true;
     1.5  HOL_quantifiers := false;
     1.6  
     1.7 +
     1.8 +(** Weak liveness: there are traces that reach the end **)
     1.9 +
    1.10 +goal thy 
    1.11 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.12 +\        ==> EX K. EX evs: otway.          \
    1.13 +\               Says A B (Crypt (Agent A) K) : set_of_list evs";
    1.14 +by (REPEAT (resolve_tac [exI,bexI] 1));
    1.15 +br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4 RS 
    1.16 +    otway.OR5) 2;
    1.17 +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.18 +by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    1.19 +by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    1.20 +qed "weak_liveness";
    1.21 +
    1.22 +
    1.23  (**** Inductive proofs about otway ****)
    1.24  
    1.25  (*The Enemy can see more than anybody else, except for their initial state*)
    1.26 @@ -45,17 +61,17 @@
    1.27  
    1.28  (** For reasoning about the encrypted portion of messages **)
    1.29  
    1.30 -goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
    1.31 +goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
    1.32  \                X : analz (sees Enemy evs)";
    1.33  by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.34  qed "OR2_analz_sees_Enemy";
    1.35  
    1.36 -goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
    1.37 +goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
    1.38  \                X : analz (sees Enemy evs)";
    1.39  by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.40  qed "OR4_analz_sees_Enemy";
    1.41  
    1.42 -goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
    1.43 +goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
    1.44  \                K : parts (sees Enemy evs)";
    1.45  by (fast_tac (!claset addSEs partsEs
    1.46  	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.47 @@ -165,18 +181,16 @@
    1.48  by (EVERY 
    1.49      (map
    1.50       (best_tac
    1.51 -      (!claset addSDs [newK_invKey]
    1.52 -	       addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.53 +      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.54  		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    1.55  		      Suc_leD]
    1.56  	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
    1.57  	       addss (!simpset)))
    1.58       [3,2,1]));
    1.59  (*OR5: dummy message*)
    1.60 -by (best_tac (!claset addSDs [newK_invKey]
    1.61 -		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
    1.62 -			addIs  [less_SucI, impOfSubs keysFor_mono]
    1.63 -			addss (!simpset addsimps [le_def])) 1);
    1.64 +by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
    1.65 +		      addIs  [less_SucI, impOfSubs keysFor_mono]
    1.66 +		      addss (!simpset addsimps [le_def])) 1);
    1.67  val lemma = result();
    1.68  
    1.69  goal thy 
    1.70 @@ -259,19 +273,6 @@
    1.71  
    1.72  (** Session keys are not used to encrypt other session keys **)
    1.73  
    1.74 -(*Could generalize this so that the X component doesn't have to be first
    1.75 -  in the message?*)
    1.76 -val enemy_analz_tac =
    1.77 -  SELECT_GOAL 
    1.78 -   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
    1.79 -	   dtac (impOfSubs Fake_analz_insert) 1,
    1.80 -	   eresolve_tac [asm_rl, synth.Inj] 1,
    1.81 -	   Fast_tac 1,
    1.82 -	   Asm_full_simp_tac 1,
    1.83 -	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
    1.84 -	   ]);
    1.85 -
    1.86 -
    1.87  (*Lemma for the trivial direction of the if-and-only-if*)
    1.88  goal thy  
    1.89   "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
    1.90 @@ -294,22 +295,11 @@
    1.91       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
    1.92  			 @ pushes)
    1.93                 setloop split_tac [expand_if])));
    1.94 -(*OR4*) 
    1.95 -by (enemy_analz_tac 5);
    1.96 +(*OR4, OR2, Fake*) 
    1.97 +by (EVERY (map enemy_analz_tac [5,3,2]));
    1.98  (*OR3*)
    1.99 -by (Fast_tac 4);
   1.100 -(*OR2*) (** LEVEL 7 **)
   1.101 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
   1.102 -    (insert_commute RS ssubst) 3);
   1.103 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.104 -    (insert_commute RS ssubst) 3);
   1.105 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
   1.106 -by (enemy_analz_tac 3);
   1.107 -(*Fake case*) (** LEVEL 11 **)
   1.108 -by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
   1.109 -    (insert_commute RS ssubst) 2);
   1.110 -by (enemy_analz_tac 2);
   1.111 -(*Base case*)
   1.112 +by (Fast_tac 2);
   1.113 +(*Base case*) 
   1.114  by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.115  qed_spec_mp "analz_image_newK";
   1.116  
   1.117 @@ -360,20 +350,10 @@
   1.118       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.119  			  analz_insert_Key_newK] @ pushes)
   1.120                 setloop split_tac [expand_if])));
   1.121 +(*OR4, OR2, Fake*) 
   1.122 +by (EVERY (map enemy_analz_tac [4,2,1]));
   1.123  (*OR3*)
   1.124 -by (fast_tac (!claset addSEs [less_irrefl]) 3);
   1.125 -(*Fake*) (** LEVEL 10 **)
   1.126 -by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
   1.127 -by (enemy_analz_tac 1);
   1.128 -(*OR4*)
   1.129 -by (mp_tac 2);
   1.130 -by (enemy_analz_tac 2);
   1.131 -(*OR2*)
   1.132 -by (mp_tac 1);
   1.133 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.134 -    (insert_commute RS ssubst) 1);
   1.135 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.136 -by (enemy_analz_tac 1);
   1.137 +by (fast_tac (!claset addSEs [less_irrefl]) 1);
   1.138  qed "Enemy_not_see_encrypted_key";
   1.139  
   1.140  
   1.141 @@ -432,9 +412,9 @@
   1.142  		      addEs [Says_imp_old_keys RS less_irrefl]
   1.143  	              addss (!simpset)) 3);
   1.144  (*OR2*) (** LEVEL 12 **)
   1.145 +(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   1.146  by (ex_strip_tac 2);
   1.147 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.148 -    (insert_commute RS ssubst) 2);
   1.149 +by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 2);
   1.150  by (Simp_tac 2);
   1.151  by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.152  			      Crypt_parts_singleton]) 2);