A further tidying
authorpaulson
Tue Sep 03 19:06:00 1996 +0200 (1996-09-03)
changeset 194520ca9cf90e69
parent 1944 ea0f573b222b
child 1946 b59a3d686436
A further tidying
src/HOL/Auth/OtwayRees.ML
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Sep 03 18:30:15 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Sep 03 19:06:00 1996 +0200
     1.3 @@ -351,82 +351,6 @@
     1.4  qed "analz_insert_Key_newK";
     1.5  
     1.6  
     1.7 -(*** Session keys are issued at most once, and identify the principals ***)
     1.8 -
     1.9 -(*NOW WE HAVE... 
    1.10 -          Says S B
    1.11 -           {|Nonce NA, Crypt {|Nonce NA, Key (newK evta)|} (shrK A),
    1.12 -            Crypt {|Nonce NB, Key (newK evta)|} (shrK B)|} 
    1.13 -AND
    1.14 -          Says Server (Friend j)
    1.15 -           {|Ni, Crypt {|Ni, Key (newK evta)|} (shrK (Friend i)),
    1.16 -            Crypt {|Nj, Key (newK evta)|} (shrK (Friend j))|} 
    1.17 -THUS
    1.18 -          A = Friend i | A = Friend j
    1.19 -AND THIS LETS US PROVE IT!!
    1.20 -*)
    1.21 -
    1.22 -goal thy 
    1.23 - "!!evs. [| X : synth (analz (sees Enemy evs));       \
    1.24 -\           Crypt X' (shrK C) : parts{X};             \
    1.25 -\           C ~= Enemy;   evs : otway |]              \
    1.26 -\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
    1.27 -by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
    1.28 -	              addDs [impOfSubs parts_insert_subset_Un]
    1.29 -                      addss (!simpset)) 1);
    1.30 -qed "Crypt_Fake_parts";
    1.31 -
    1.32 -goal thy 
    1.33 - "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
    1.34 -\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
    1.35 -\            Crypt X' K : parts {Y}";
    1.36 -bd parts_singleton 1;
    1.37 -by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
    1.38 -qed "Crypt_parts_singleton";
    1.39 -
    1.40 -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
    1.41 -
    1.42 -(*The Key K uniquely identifies a pair of senders in the message encrypted by
    1.43 -  C, but if C=Enemy then he could send all sorts of nonsense.*)
    1.44 -goal thy 
    1.45 - "!!evs. evs : otway ==>                        \
    1.46 -\      EX A B. ALL C S S' X NA.                    \
    1.47 -\         C ~= Enemy -->                        \
    1.48 -\         Says S S' X : set_of_list evs -->     \
    1.49 -\           (Crypt {|NA, Key K|} (shrK C) : parts{X} --> C=A | C=B)";
    1.50 -be otway.induct 1;
    1.51 -bd OR2_analz_sees_Enemy 4;
    1.52 -bd OR4_analz_sees_Enemy 6;
    1.53 -by (ALLGOALS 
    1.54 -    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
    1.55 -by (REPEAT_FIRST (etac exE));
    1.56 -(*OR4*)
    1.57 -by (ex_strip_tac 4);
    1.58 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
    1.59 -			      Crypt_parts_singleton]) 4);
    1.60 -(*OR3: Case split propagates some context to other subgoal...*)
    1.61 -	(** LEVEL 8 **)
    1.62 -by (excluded_middle_tac "K = newK evsa" 3);
    1.63 -by (Asm_simp_tac 3);
    1.64 -by (REPEAT (ares_tac [exI] 3));
    1.65 -(*...we prove this case by contradiction: the key is too new!*)
    1.66 -by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
    1.67 -		      addSEs partsEs
    1.68 -		      addEs [Says_imp_old_keys RS less_irrefl]
    1.69 -	              addss (!simpset)) 3);
    1.70 -(*OR2*) (** LEVEL 12 **)
    1.71 -by (ex_strip_tac 2);
    1.72 -by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
    1.73 -    (insert_commute RS ssubst) 2);
    1.74 -by (Simp_tac 2);
    1.75 -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
    1.76 -			      Crypt_parts_singleton]) 2);
    1.77 -(*Fake*) (** LEVEL 16 **)
    1.78 -by (ex_strip_tac 1);
    1.79 -by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
    1.80 -qed "unique_session_keys";
    1.81 -
    1.82 -
    1.83  (*Describes the form *and age* of K when the following message is sent*)
    1.84  goal thy 
    1.85   "!!evs. [| Says Server B \
    1.86 @@ -479,3 +403,72 @@
    1.87  by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.88  by (enemy_analz_tac 1);
    1.89  qed "Enemy_not_see_encrypted_key";
    1.90 +
    1.91 +
    1.92 +
    1.93 +(*** Session keys are issued at most once, and identify the principals ***)
    1.94 +
    1.95 +(** First, two lemmas for the Fake, OR2 and OR4 cases **)
    1.96 +
    1.97 +goal thy 
    1.98 + "!!evs. [| X : synth (analz (sees Enemy evs));       \
    1.99 +\           Crypt X' (shrK C) : parts{X};             \
   1.100 +\           C ~= Enemy;   evs : otway |]              \
   1.101 +\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   1.102 +by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.103 +	              addDs [impOfSubs parts_insert_subset_Un]
   1.104 +                      addss (!simpset)) 1);
   1.105 +qed "Crypt_Fake_parts";
   1.106 +
   1.107 +goal thy 
   1.108 + "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
   1.109 +\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   1.110 +\            Crypt X' K : parts {Y}";
   1.111 +bd parts_singleton 1;
   1.112 +by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   1.113 +qed "Crypt_parts_singleton";
   1.114 +
   1.115 +fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.116 +
   1.117 +(*The Key K uniquely identifies a pair of senders in the message encrypted by
   1.118 +  C, but if C=Enemy then he could send all sorts of nonsense.*)
   1.119 +goal thy 
   1.120 + "!!evs. evs : otway ==>                        \
   1.121 +\      EX A B. ALL C.                    \
   1.122 +\         C ~= Enemy -->                        \
   1.123 +\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   1.124 +\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   1.125 +by (Simp_tac 1);
   1.126 +be otway.induct 1;
   1.127 +bd OR2_analz_sees_Enemy 4;
   1.128 +bd OR4_analz_sees_Enemy 6;
   1.129 +by (ALLGOALS 
   1.130 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   1.131 +by (REPEAT_FIRST (etac exE));
   1.132 +(*OR4*)
   1.133 +by (ex_strip_tac 4);
   1.134 +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.135 +			      Crypt_parts_singleton]) 4);
   1.136 +(*OR3: Case split propagates some context to other subgoal...*)
   1.137 +	(** LEVEL 8 **)
   1.138 +by (excluded_middle_tac "K = newK evsa" 3);
   1.139 +by (Asm_simp_tac 3);
   1.140 +by (REPEAT (ares_tac [exI] 3));
   1.141 +(*...we prove this case by contradiction: the key is too new!*)
   1.142 +by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   1.143 +		      addSEs partsEs
   1.144 +		      addEs [Says_imp_old_keys RS less_irrefl]
   1.145 +	              addss (!simpset)) 3);
   1.146 +(*OR2*) (** LEVEL 12 **)
   1.147 +by (ex_strip_tac 2);
   1.148 +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.149 +    (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);
   1.153 +(*Fake*) (** LEVEL 16 **)
   1.154 +by (ex_strip_tac 1);
   1.155 +by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   1.156 +qed "unique_session_keys";
   1.157 +
   1.158 +(*It seems strange but this theorem is NOT needed to prove the main result!*)