Last working version prior to introduction of "lost"
authorpaulson
Wed Sep 25 17:15:18 1996 +0200 (1996-09-25)
changeset 20260df5a96bf77e
parent 2025 9acc10ac1e1d
child 2027 0f11f625063b
Last working version prior to introduction of "lost"
src/HOL/Auth/Message.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/Yahalom.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Wed Sep 25 15:03:13 1996 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Wed Sep 25 17:15:18 1996 +0200
     1.3 @@ -252,6 +252,15 @@
     1.4  	  parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
     1.5  
     1.6  
     1.7 +goal thy "parts (Key``N) = Key``N";
     1.8 +by (Auto_tac());
     1.9 +be parts.induct 1;
    1.10 +by (Auto_tac());
    1.11 +qed "parts_image_Key";
    1.12 +
    1.13 +Addsimps [parts_image_Key];
    1.14 +
    1.15 +
    1.16  (**** Inductive relation "analz" ****)
    1.17  
    1.18  val major::prems = 
    1.19 @@ -420,6 +429,15 @@
    1.20  qed "analz_insert_Crypt_subset";
    1.21  
    1.22  
    1.23 +goal thy "analz (Key``N) = Key``N";
    1.24 +by (Auto_tac());
    1.25 +be analz.induct 1;
    1.26 +by (Auto_tac());
    1.27 +qed "analz_image_Key";
    1.28 +
    1.29 +Addsimps [analz_image_Key];
    1.30 +
    1.31 +
    1.32  (** Idempotence and transitivity **)
    1.33  
    1.34  goal thy "!!H. X: analz (analz H) ==> X: analz H";
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed Sep 25 15:03:13 1996 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Wed Sep 25 17:15:18 1996 +0200
     2.3 @@ -13,16 +13,6 @@
     2.4  *)
     2.5  
     2.6  
     2.7 -(*MAY DELETE**)
     2.8 -Delsimps [parts_insert_sees];
     2.9 -AddIffs [le_refl];
    2.10 -val disj_cong = 
    2.11 -  let val th = prove_goal HOL.thy 
    2.12 -                "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
    2.13 -		(fn _=> [fast_tac HOL_cs 1])
    2.14 -  in  standard (impI RSN (2, th RS mp RS mp))  end;
    2.15 -
    2.16 -
    2.17  open OtwayRees;
    2.18  
    2.19  proof_timing:=true;
    2.20 @@ -147,9 +137,9 @@
    2.21  (*auto_tac does not work here, as it performs safe_tac first*)
    2.22  by (ALLGOALS Asm_simp_tac);
    2.23  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    2.24 -				       impOfSubs parts_insert_subset_Un,
    2.25 -				       Suc_leD]
    2.26 -			        addss (!simpset))));
    2.27 +					   impOfSubs parts_insert_subset_Un,
    2.28 +					   Suc_leD]
    2.29 +			            addss (!simpset))));
    2.30  val lemma = result();
    2.31  
    2.32  (*Variant needed for the main theorem below*)
    2.33 @@ -277,8 +267,7 @@
    2.34  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
    2.35  (*Deals with Faked messages*)
    2.36  by (best_tac (!claset addSEs partsEs
    2.37 -		      addDs [impOfSubs analz_subset_parts,
    2.38 -                             impOfSubs parts_insert_subset_Un]
    2.39 +		      addDs [impOfSubs parts_insert_subset_Un]
    2.40                        addss (!simpset)) 2);
    2.41  (*Base case and Reveal*)
    2.42  by (Auto_tac());
    2.43 @@ -395,7 +384,7 @@
    2.44  qed "analz_insert_Key_newK";
    2.45  
    2.46  
    2.47 -(** The Key K uniquely identifies the Server's  message. **)
    2.48 +(*** The Key K uniquely identifies the Server's  message. **)
    2.49  
    2.50  fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
    2.51  
    2.52 @@ -477,7 +466,7 @@
    2.53  (*Base case*)
    2.54  by (fast_tac (!claset addss (!simpset)) 1);
    2.55  by (Step_tac 1);
    2.56 -(*OR1: creation of new Nonce*)
    2.57 +(*OR1: creation of new Nonce.  Move assertion into global context*)
    2.58  by (excluded_middle_tac "NA = Nonce (newN evsa)" 1);
    2.59  by (Asm_simp_tac 1);
    2.60  by (Fast_tac 1);
    2.61 @@ -521,8 +510,7 @@
    2.62  			    addss  (!simpset))));
    2.63  by (REPEAT_FIRST (fast_tac (!claset 
    2.64  			      addSEs (partsEs@[nonce_not_seen_now])
    2.65 -                              addSDs  [impOfSubs analz_subset_parts,
    2.66 -                                      impOfSubs parts_insert_subset_Un]
    2.67 +                              addSDs  [impOfSubs parts_insert_subset_Un]
    2.68                                addss (!simpset))));
    2.69  qed_spec_mp"no_nonce_OR1_OR2";
    2.70  
    2.71 @@ -531,15 +519,15 @@
    2.72  (*If the encrypted message appears, and A has used Nonce NA to start a run,
    2.73    then it originated with the Server!*)
    2.74  goal thy 
    2.75 - "!!evs. [| A ~: bad;  evs : otway |]                                 \
    2.76 + "!!evs. [| A ~: bad;  evs : otway |]                                        \
    2.77  \        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
    2.78 -\            Says A B {|Nonce NA, Agent A, Agent B,  \
    2.79 -\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
    2.80 -\             : set_of_list evs --> \
    2.81 -\            (EX NB. Says Server B               \
    2.82 -\                 {|Nonce NA,               \
    2.83 -\                   Crypt {|Nonce NA, Key K|} (shrK A),              \
    2.84 -\                   Crypt {|Nonce NB, Key K|} (shrK B)|}             \
    2.85 +\            Says A B {|Nonce NA, Agent A, Agent B,                          \
    2.86 +\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}      \
    2.87 +\             : set_of_list evs -->                                          \
    2.88 +\            (EX NB. Says Server B                                           \
    2.89 +\                 {|Nonce NA,                                                \
    2.90 +\                   Crypt {|Nonce NA, Key K|} (shrK A),                      \
    2.91 +\                   Crypt {|Nonce NB, Key K|} (shrK B)|}                     \
    2.92  \                   : set_of_list evs)";
    2.93  be otway.induct 1;
    2.94  by parts_Fake_tac;
    2.95 @@ -681,66 +669,37 @@
    2.96  
    2.97  
    2.98  
    2.99 -(*** Session keys are issued at most once, and identify the principals ***)
   2.100 -
   2.101 -(** First, two lemmas for the Fake, OR2 and OR4 cases **)
   2.102 -
   2.103 -goal thy 
   2.104 - "!!evs. [| X : synth (analz (sees Enemy evs));                \
   2.105 -\           Crypt X' (shrK C) : parts{X};                      \
   2.106 -\           C ~: bad;  evs : otway |]  \
   2.107 -\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   2.108 -by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   2.109 -	              addDs [impOfSubs parts_insert_subset_Un]
   2.110 -                      addss (!simpset)) 1);
   2.111 -qed "Crypt_Fake_parts";
   2.112 -
   2.113 +(** A session key uniquely identifies a pair of senders in the message
   2.114 +    encrypted by a good agent C. **)
   2.115  goal thy 
   2.116 - "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
   2.117 -\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   2.118 -\            Crypt X' K : parts {Y}";
   2.119 -bd parts_singleton 1;
   2.120 -by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   2.121 -qed "Crypt_parts_singleton";
   2.122 -
   2.123 -(*The Key K uniquely identifies a pair of senders in the message encrypted by
   2.124 -  C, but if C=Enemy then he could send all sorts of nonsense.*)
   2.125 -goal thy 
   2.126 - "!!evs. evs : otway ==>                                     \
   2.127 -\      EX A B. ALL C.                                        \
   2.128 -\         C ~: bad -->                                       \
   2.129 -\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   2.130 -\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   2.131 -by (Simp_tac 1);
   2.132 + "!!evs. evs : otway ==>                                           \
   2.133 +\      EX A B. ALL C N.                                            \
   2.134 +\         C ~: bad -->                                             \
   2.135 +\         Crypt {|N, Key K|} (shrK C) : parts (sees Enemy evs) --> \
   2.136 +\         C=A | C=B";
   2.137 +by (Simp_tac 1);	(*Miniscoping*)
   2.138  be otway.induct 1;
   2.139  bd OR2_analz_sees_Enemy 4;
   2.140  bd OR4_analz_sees_Enemy 6;
   2.141 +(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   2.142  by (ALLGOALS 
   2.143 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   2.144 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
   2.145 +				      imp_conj_distrib, parts_insert_sees,
   2.146 +				      parts_insert2])));
   2.147  by (REPEAT_FIRST (etac exE));
   2.148 -(*OR4*)
   2.149 -by (ex_strip_tac 4);
   2.150 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   2.151 -			      Crypt_parts_singleton]) 4);
   2.152 -(*OR3: Case split propagates some context to other subgoal...*)
   2.153 -	(** LEVEL 8 **)
   2.154 -by (excluded_middle_tac "K = newK evsa" 3);
   2.155 -by (Asm_simp_tac 3);
   2.156 -by (REPEAT (ares_tac [exI] 3));
   2.157 +(*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
   2.158 +by (excluded_middle_tac "K = newK evsa" 4);
   2.159 +by (Asm_simp_tac 4);
   2.160 +by (REPEAT (ares_tac [exI] 4));
   2.161  (*...we prove this case by contradiction: the key is too new!*)
   2.162 -by (fast_tac (!claset addIs [parts_insertI]
   2.163 -		      addSEs partsEs
   2.164 +by (fast_tac (!claset addSEs partsEs
   2.165  		      addEs [Says_imp_old_keys RS less_irrefl]
   2.166 -	              addss (!simpset)) 3);
   2.167 -(*OR2*) (** LEVEL 12 **)
   2.168 -(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   2.169 -by (ex_strip_tac 2);
   2.170 -by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 2);
   2.171 -by (Simp_tac 2);
   2.172 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   2.173 -			      Crypt_parts_singleton]) 2);
   2.174 -(*Fake*) (** LEVEL 16 **)
   2.175 -by (ex_strip_tac 1);
   2.176 -by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   2.177 +	              addss (!simpset)) 4);
   2.178 +(*Base, Fake, OR2, OR4*)
   2.179 +by (REPEAT_FIRST ex_strip_tac);
   2.180 +bd synth.Inj 4;
   2.181 +bd synth.Inj 3;
   2.182 +(*Now in effect there are three Fake cases*)
   2.183 +by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
   2.184 +			            addss (!simpset))));
   2.185  qed "key_identifies_senders";
   2.186 -
     3.1 --- a/src/HOL/Auth/Shared.ML	Wed Sep 25 15:03:13 1996 +0200
     3.2 +++ b/src/HOL/Auth/Shared.ML	Wed Sep 25 17:15:18 1996 +0200
     3.3 @@ -120,6 +120,12 @@
     3.4  
     3.5  AddIffs [Enemy_in_bad];
     3.6  
     3.7 +goal thy "!!A. A ~: bad ==> A ~= Enemy";
     3.8 +by (Fast_tac 1);
     3.9 +qed "not_bad_imp_not_Enemy";
    3.10 +
    3.11 +AddIffs [Enemy_in_bad];
    3.12 +
    3.13  (** Specialized rewrite rules for (sees A (Says...#evs)) **)
    3.14  
    3.15  goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
     4.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Sep 25 15:03:13 1996 +0200
     4.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed Sep 25 17:15:18 1996 +0200
     4.3 @@ -166,10 +166,10 @@
     4.4    contradicting new_keys_not_seen*)
     4.5  by (ALLGOALS
     4.6       (best_tac
     4.7 -      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
     4.8 +      (!claset addDs [impOfSubs analz_subset_parts,
     4.9 +		      impOfSubs (analz_subset_parts RS keysFor_mono),
    4.10  		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    4.11  		      Suc_leD]
    4.12 -	       addDs [impOfSubs analz_subset_parts]
    4.13  	       addEs [new_keys_not_seen RSN(2,rev_notE)]
    4.14  	       addss (!simpset))));
    4.15  val lemma = result();
    4.16 @@ -214,8 +214,7 @@
    4.17  (*Deals with Faked messages*)
    4.18  by (EVERY 
    4.19      (map (best_tac (!claset addSEs partsEs
    4.20 -			    addDs [impOfSubs analz_subset_parts,
    4.21 -				   impOfSubs parts_insert_subset_Un]
    4.22 +			    addDs [impOfSubs parts_insert_subset_Un]
    4.23  			    addss (!simpset)))
    4.24       [3,2]));
    4.25  (*Base case*)