src/HOL/Auth/Event.thy
changeset 13922 75ae4244a596
parent 11463 96b5b27da55c
child 13926 6e62e5357a10
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Apr 23 18:09:48 2003 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Fri Apr 25 11:18:14 2003 +0200
     1.3 @@ -37,8 +37,8 @@
     1.4  
     1.5  axioms
     1.6    (*Spy has access to his own key for spoof messages, but Server is secure*)
     1.7 -  Spy_in_bad     [iff] :    "Spy \\<in> bad"
     1.8 -  Server_not_bad [iff] : "Server \\<notin> bad"
     1.9 +  Spy_in_bad     [iff] :    "Spy \<in> bad"
    1.10 +  Server_not_bad [iff] : "Server \<notin> bad"
    1.11  
    1.12  primrec
    1.13    knows_Nil:   "knows A [] = initState A"
    1.14 @@ -49,7 +49,7 @@
    1.15  	   Says A' B X => insert X (knows Spy evs)
    1.16  	 | Gets A' X => knows Spy evs
    1.17  	 | Notes A' X  => 
    1.18 -	     if A' \\<in> bad then insert X (knows Spy evs) else knows Spy evs)
    1.19 +	     if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
    1.20  	else
    1.21  	(case ev of
    1.22  	   Says A' B X => 
    1.23 @@ -97,9 +97,53 @@
    1.24  
    1.25  use "Event_lemmas.ML"
    1.26  
    1.27 +lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
    1.28 +by (induct e, auto simp: knows_Cons)
    1.29 +
    1.30 +lemma initState_subset_knows: "initState A <= knows A evs"
    1.31 +apply (induct_tac evs)
    1.32 +apply (simp add: ); 
    1.33 +apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
    1.34 +done
    1.35 +
    1.36 +
    1.37 +(*For proving new_keys_not_used*)
    1.38 +lemma keysFor_parts_insert:
    1.39 +     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] \
    1.40 +\     ==> K \<in> keysFor (parts (G Un H)) | Key (invKey K) \<in> parts H"; 
    1.41 +by (force 
    1.42 +    dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
    1.43 +           analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
    1.44 +    intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
    1.45 +
    1.46  method_setup analz_mono_contra = {*
    1.47      Method.no_args
    1.48        (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
    1.49 -    "for proving theorems of the form X \\<notin> analz (knows Spy evs) --> P"
    1.50 +    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    1.51 +
    1.52 +subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    1.53 +
    1.54 +ML
    1.55 +{*
    1.56 +val synth_analz_mono = thm "synth_analz_mono";
    1.57 +
    1.58 +val synth_analz_mono_contra_tac = 
    1.59 +  let val syan_impI = inst "P" "?Y ~: synth (analz (knows Spy ?evs))" impI
    1.60 +  in
    1.61 +    rtac syan_impI THEN' 
    1.62 +    REPEAT1 o 
    1.63 +      (dresolve_tac 
    1.64 +       [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
    1.65 +        knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
    1.66 +	knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
    1.67 +    THEN'
    1.68 +    mp_tac
    1.69 +  end;
    1.70 +*}
    1.71 +
    1.72 +method_setup synth_analz_mono_contra = {*
    1.73 +    Method.no_args
    1.74 +      (Method.METHOD (fn facts => REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    1.75 +    "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
    1.76  
    1.77  end