src/HOL/Auth/OtwayRees.ML
changeset 2045 ae1030e66745
parent 2032 1bbf1bdcaf56
child 2048 bb54fbba0071
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Sep 30 11:04:14 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Sep 30 11:10:22 1996 +0200
     1.3 @@ -43,7 +43,6 @@
     1.4                                :: otway.intrs))));
     1.5  qed "otway_mono";
     1.6  
     1.7 -
     1.8  (*The Spy can see more than anybody else, except for their initial state*)
     1.9  goal thy 
    1.10   "!!evs. evs : otway lost ==> \
    1.11 @@ -301,37 +300,6 @@
    1.12  result();
    1.13  
    1.14  
    1.15 -(** Specialized rewriting for this proof **)
    1.16 -
    1.17 -Delsimps [image_insert];
    1.18 -Addsimps [image_insert RS sym];
    1.19 -
    1.20 -Delsimps [image_Un];
    1.21 -Addsimps [image_Un RS sym];
    1.22 -
    1.23 -goal thy "insert (Key (newK x)) (sees lost A evs) = \
    1.24 -\         Key `` (newK``{x}) Un (sees lost A evs)";
    1.25 -by (Fast_tac 1);
    1.26 -val insert_Key_singleton = result();
    1.27 -
    1.28 -goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
    1.29 -\         Key `` (f `` (insert x E)) Un C";
    1.30 -by (Fast_tac 1);
    1.31 -val insert_Key_image = result();
    1.32 -
    1.33 -
    1.34 -(*This lets us avoid analyzing the new message -- unless we have to!*)
    1.35 -(*NEEDED??*)
    1.36 -goal thy "synth (analz (sees lost Spy evs)) <=   \
    1.37 -\         synth (analz (sees lost Spy (Says A B X # evs)))";
    1.38 -by (Simp_tac 1);
    1.39 -by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
    1.40 -qed "synth_analz_thin";
    1.41 -
    1.42 -AddIs [impOfSubs synth_analz_thin];
    1.43 -
    1.44 -
    1.45 -
    1.46  (** Session keys are not used to encrypt other session keys **)
    1.47  
    1.48  (*Describes the form of Key K when the following message is sent.  The use of
    1.49 @@ -358,7 +326,8 @@
    1.50  goal thy 
    1.51   "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
    1.52  \           evs : otway lost |]                      \
    1.53 -\        ==> (EX evt: otway lost. K = newK evt) | Key K : analz (sees lost Spy evs)";
    1.54 +\        ==> (EX evt: otway lost. K = newK evt)          \
    1.55 +\          | Key K : analz (sees lost Spy evs)";
    1.56  by (excluded_middle_tac "A : lost" 1);
    1.57  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    1.58                        addss (!simpset)) 2);
    1.59 @@ -369,15 +338,6 @@
    1.60  qed "Reveal_message_form";
    1.61  
    1.62  
    1.63 -(*Lemma for the trivial direction of the if-and-only-if*)
    1.64 -goal thy  
    1.65 - "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
    1.66 -\         (K : nE | Key K : analz sEe)  ==>     \
    1.67 -\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
    1.68 -by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
    1.69 -val lemma = result();
    1.70 -
    1.71 -
    1.72  (*The equality makes the induction hypothesis easier to apply*)
    1.73  goal thy  
    1.74   "!!evs. evs : otway lost ==> \
    1.75 @@ -387,7 +347,7 @@
    1.76  by (dtac OR2_analz_sees_Spy 4);
    1.77  by (dtac OR4_analz_sees_Spy 6);
    1.78  by (dtac Reveal_message_form 7);
    1.79 -by (REPEAT_FIRST (ares_tac [allI, lemma]));
    1.80 +by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
    1.81  by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
    1.82  by (ALLGOALS (*Takes 28 secs*)
    1.83      (asm_simp_tac