src/HOL/Auth/Yahalom.ML
changeset 2045 ae1030e66745
parent 2032 1bbf1bdcaf56
child 2051 067bf19a71b7
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Mon Sep 30 11:04:14 1996 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Mon Sep 30 11:10:22 1996 +0200
     1.3 @@ -31,6 +31,14 @@
     1.4  
     1.5  (**** Inductive proofs about yahalom ****)
     1.6  
     1.7 +goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
     1.8 +by (rtac subsetI 1);
     1.9 +by (etac yahalom.induct 1);
    1.10 +by (REPEAT_FIRST
    1.11 +    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    1.12 +                              :: yahalom.intrs))));
    1.13 +qed "yahalom_mono";
    1.14 +
    1.15  (*The Spy can see more than anybody else, except for their initial state*)
    1.16  goal thy 
    1.17   "!!evs. evs : yahalom lost ==> \
    1.18 @@ -40,6 +48,15 @@
    1.19                                  addss (!simpset))));
    1.20  qed "sees_agent_subset_sees_Spy";
    1.21  
    1.22 +(*The Spy can see more than anybody else who's lost their key!*)
    1.23 +goal thy 
    1.24 + "!!evs. evs : yahalom lost ==> \
    1.25 +\        A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
    1.26 +by (etac yahalom.induct 1);
    1.27 +by (agent.induct_tac "A" 1);
    1.28 +by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
    1.29 +qed_spec_mp "sees_lost_agent_subset_sees_Spy";
    1.30 +
    1.31  
    1.32  (*Nobody sends themselves messages*)
    1.33  goal thy "!!evs. evs : yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
    1.34 @@ -222,55 +239,15 @@
    1.35  result();
    1.36  
    1.37  
    1.38 -(** Specialized rewriting for this proof **)
    1.39 -
    1.40 -Delsimps [image_insert];
    1.41 -Addsimps [image_insert RS sym];
    1.42 -
    1.43 -Delsimps [image_Un];
    1.44 -Addsimps [image_Un RS sym];
    1.45 -
    1.46 -goal thy "insert (Key (newK x)) (sees lost A evs) = \
    1.47 -\         Key `` (newK``{x}) Un (sees lost A evs)";
    1.48 -by (Fast_tac 1);
    1.49 -val insert_Key_singleton = result();
    1.50 -
    1.51 -goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
    1.52 -\         Key `` (f `` (insert x E)) Un C";
    1.53 -by (Fast_tac 1);
    1.54 -val insert_Key_image = result();
    1.55 -
    1.56 -
    1.57 -(*This lets us avoid analyzing the new message -- unless we have to!*)
    1.58 -(*NEEDED??*)
    1.59 -goal thy "synth (analz (sees lost Spy evs)) <=   \
    1.60 -\         synth (analz (sees lost Spy (Says A B X # evs)))";
    1.61 -by (Simp_tac 1);
    1.62 -by (rtac (subset_insertI RS analz_mono RS synth_mono) 1);
    1.63 -qed "synth_analz_thin";
    1.64 -
    1.65 -AddIs [impOfSubs synth_analz_thin];
    1.66 -
    1.67 -
    1.68 -
    1.69  (** Session keys are not used to encrypt other session keys **)
    1.70  
    1.71 -(*Lemma for the trivial direction of the if-and-only-if*)
    1.72 -goal thy  
    1.73 - "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
    1.74 -\         (K : nE | Key K : analz sEe)  ==>     \
    1.75 -\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
    1.76 -by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
    1.77 -val lemma = result();
    1.78 -
    1.79 -
    1.80  goal thy  
    1.81   "!!evs. evs : yahalom lost ==> \
    1.82  \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
    1.83  \           (K : newK``E | Key K : analz (sees lost Spy evs))";
    1.84  by (etac yahalom.induct 1);
    1.85  by (dtac YM4_analz_sees_Spy 6);
    1.86 -by (REPEAT_FIRST (resolve_tac [allI, lemma]));
    1.87 +by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
    1.88  by (ALLGOALS 
    1.89      (asm_simp_tac 
    1.90       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
    1.91 @@ -349,6 +326,20 @@
    1.92  qed "Spy_not_see_encrypted_key";
    1.93  
    1.94  
    1.95 +goal thy 
    1.96 + "!!evs. [| C ~: {A,B,Server};                                          \
    1.97 +\           Says Server A                                               \
    1.98 +\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
    1.99 +\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
   1.100 +\           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
   1.101 +\     K ~: analz (sees lost C evs)";
   1.102 +by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.103 +by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   1.104 +by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   1.105 +by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
   1.106 +qed "Agent_not_see_encrypted_key";
   1.107 +
   1.108 +
   1.109  (** Towards proofs of stronger authenticity properties **)
   1.110  
   1.111  goal thy