src/HOL/Auth/OtwayRees.ML
changeset 2026 0df5a96bf77e
parent 2014 5be4c8ca7b25
child 2032 1bbf1bdcaf56
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed Sep 25 15:03:13 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Wed Sep 25 17:15:18 1996 +0200
     1.3 @@ -13,16 +13,6 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -(*MAY DELETE**)
     1.8 -Delsimps [parts_insert_sees];
     1.9 -AddIffs [le_refl];
    1.10 -val disj_cong = 
    1.11 -  let val th = prove_goal HOL.thy 
    1.12 -                "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
    1.13 -		(fn _=> [fast_tac HOL_cs 1])
    1.14 -  in  standard (impI RSN (2, th RS mp RS mp))  end;
    1.15 -
    1.16 -
    1.17  open OtwayRees;
    1.18  
    1.19  proof_timing:=true;
    1.20 @@ -147,9 +137,9 @@
    1.21  (*auto_tac does not work here, as it performs safe_tac first*)
    1.22  by (ALLGOALS Asm_simp_tac);
    1.23  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.24 -				       impOfSubs parts_insert_subset_Un,
    1.25 -				       Suc_leD]
    1.26 -			        addss (!simpset))));
    1.27 +					   impOfSubs parts_insert_subset_Un,
    1.28 +					   Suc_leD]
    1.29 +			            addss (!simpset))));
    1.30  val lemma = result();
    1.31  
    1.32  (*Variant needed for the main theorem below*)
    1.33 @@ -277,8 +267,7 @@
    1.34  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
    1.35  (*Deals with Faked messages*)
    1.36  by (best_tac (!claset addSEs partsEs
    1.37 -		      addDs [impOfSubs analz_subset_parts,
    1.38 -                             impOfSubs parts_insert_subset_Un]
    1.39 +		      addDs [impOfSubs parts_insert_subset_Un]
    1.40                        addss (!simpset)) 2);
    1.41  (*Base case and Reveal*)
    1.42  by (Auto_tac());
    1.43 @@ -395,7 +384,7 @@
    1.44  qed "analz_insert_Key_newK";
    1.45  
    1.46  
    1.47 -(** The Key K uniquely identifies the Server's  message. **)
    1.48 +(*** The Key K uniquely identifies the Server's  message. **)
    1.49  
    1.50  fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
    1.51  
    1.52 @@ -477,7 +466,7 @@
    1.53  (*Base case*)
    1.54  by (fast_tac (!claset addss (!simpset)) 1);
    1.55  by (Step_tac 1);
    1.56 -(*OR1: creation of new Nonce*)
    1.57 +(*OR1: creation of new Nonce.  Move assertion into global context*)
    1.58  by (excluded_middle_tac "NA = Nonce (newN evsa)" 1);
    1.59  by (Asm_simp_tac 1);
    1.60  by (Fast_tac 1);
    1.61 @@ -521,8 +510,7 @@
    1.62  			    addss  (!simpset))));
    1.63  by (REPEAT_FIRST (fast_tac (!claset 
    1.64  			      addSEs (partsEs@[nonce_not_seen_now])
    1.65 -                              addSDs  [impOfSubs analz_subset_parts,
    1.66 -                                      impOfSubs parts_insert_subset_Un]
    1.67 +                              addSDs  [impOfSubs parts_insert_subset_Un]
    1.68                                addss (!simpset))));
    1.69  qed_spec_mp"no_nonce_OR1_OR2";
    1.70  
    1.71 @@ -531,15 +519,15 @@
    1.72  (*If the encrypted message appears, and A has used Nonce NA to start a run,
    1.73    then it originated with the Server!*)
    1.74  goal thy 
    1.75 - "!!evs. [| A ~: bad;  evs : otway |]                                 \
    1.76 + "!!evs. [| A ~: bad;  evs : otway |]                                        \
    1.77  \        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
    1.78 -\            Says A B {|Nonce NA, Agent A, Agent B,  \
    1.79 -\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
    1.80 -\             : set_of_list evs --> \
    1.81 -\            (EX NB. Says Server B               \
    1.82 -\                 {|Nonce NA,               \
    1.83 -\                   Crypt {|Nonce NA, Key K|} (shrK A),              \
    1.84 -\                   Crypt {|Nonce NB, Key K|} (shrK B)|}             \
    1.85 +\            Says A B {|Nonce NA, Agent A, Agent B,                          \
    1.86 +\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}      \
    1.87 +\             : set_of_list evs -->                                          \
    1.88 +\            (EX NB. Says Server B                                           \
    1.89 +\                 {|Nonce NA,                                                \
    1.90 +\                   Crypt {|Nonce NA, Key K|} (shrK A),                      \
    1.91 +\                   Crypt {|Nonce NB, Key K|} (shrK B)|}                     \
    1.92  \                   : set_of_list evs)";
    1.93  be otway.induct 1;
    1.94  by parts_Fake_tac;
    1.95 @@ -681,66 +669,37 @@
    1.96  
    1.97  
    1.98  
    1.99 -(*** Session keys are issued at most once, and identify the principals ***)
   1.100 -
   1.101 -(** First, two lemmas for the Fake, OR2 and OR4 cases **)
   1.102 -
   1.103 -goal thy 
   1.104 - "!!evs. [| X : synth (analz (sees Enemy evs));                \
   1.105 -\           Crypt X' (shrK C) : parts{X};                      \
   1.106 -\           C ~: bad;  evs : otway |]  \
   1.107 -\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   1.108 -by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.109 -	              addDs [impOfSubs parts_insert_subset_Un]
   1.110 -                      addss (!simpset)) 1);
   1.111 -qed "Crypt_Fake_parts";
   1.112 -
   1.113 +(** A session key uniquely identifies a pair of senders in the message
   1.114 +    encrypted by a good agent C. **)
   1.115  goal thy 
   1.116 - "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
   1.117 -\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   1.118 -\            Crypt X' K : parts {Y}";
   1.119 -bd parts_singleton 1;
   1.120 -by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   1.121 -qed "Crypt_parts_singleton";
   1.122 -
   1.123 -(*The Key K uniquely identifies a pair of senders in the message encrypted by
   1.124 -  C, but if C=Enemy then he could send all sorts of nonsense.*)
   1.125 -goal thy 
   1.126 - "!!evs. evs : otway ==>                                     \
   1.127 -\      EX A B. ALL C.                                        \
   1.128 -\         C ~: bad -->                                       \
   1.129 -\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   1.130 -\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   1.131 -by (Simp_tac 1);
   1.132 + "!!evs. evs : otway ==>                                           \
   1.133 +\      EX A B. ALL C N.                                            \
   1.134 +\         C ~: bad -->                                             \
   1.135 +\         Crypt {|N, Key K|} (shrK C) : parts (sees Enemy evs) --> \
   1.136 +\         C=A | C=B";
   1.137 +by (Simp_tac 1);	(*Miniscoping*)
   1.138  be otway.induct 1;
   1.139  bd OR2_analz_sees_Enemy 4;
   1.140  bd OR4_analz_sees_Enemy 6;
   1.141 +(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   1.142  by (ALLGOALS 
   1.143 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   1.144 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
   1.145 +				      imp_conj_distrib, parts_insert_sees,
   1.146 +				      parts_insert2])));
   1.147  by (REPEAT_FIRST (etac exE));
   1.148 -(*OR4*)
   1.149 -by (ex_strip_tac 4);
   1.150 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.151 -			      Crypt_parts_singleton]) 4);
   1.152 -(*OR3: Case split propagates some context to other subgoal...*)
   1.153 -	(** LEVEL 8 **)
   1.154 -by (excluded_middle_tac "K = newK evsa" 3);
   1.155 -by (Asm_simp_tac 3);
   1.156 -by (REPEAT (ares_tac [exI] 3));
   1.157 +(*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
   1.158 +by (excluded_middle_tac "K = newK evsa" 4);
   1.159 +by (Asm_simp_tac 4);
   1.160 +by (REPEAT (ares_tac [exI] 4));
   1.161  (*...we prove this case by contradiction: the key is too new!*)
   1.162 -by (fast_tac (!claset addIs [parts_insertI]
   1.163 -		      addSEs partsEs
   1.164 +by (fast_tac (!claset addSEs partsEs
   1.165  		      addEs [Says_imp_old_keys RS less_irrefl]
   1.166 -	              addss (!simpset)) 3);
   1.167 -(*OR2*) (** LEVEL 12 **)
   1.168 -(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   1.169 -by (ex_strip_tac 2);
   1.170 -by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 2);
   1.171 -by (Simp_tac 2);
   1.172 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.173 -			      Crypt_parts_singleton]) 2);
   1.174 -(*Fake*) (** LEVEL 16 **)
   1.175 -by (ex_strip_tac 1);
   1.176 -by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   1.177 +	              addss (!simpset)) 4);
   1.178 +(*Base, Fake, OR2, OR4*)
   1.179 +by (REPEAT_FIRST ex_strip_tac);
   1.180 +bd synth.Inj 4;
   1.181 +bd synth.Inj 3;
   1.182 +(*Now in effect there are three Fake cases*)
   1.183 +by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
   1.184 +			            addss (!simpset))));
   1.185  qed "key_identifies_senders";
   1.186 -