src/HOL/Auth/Event.thy
author paulson
Fri Apr 25 11:18:14 2003 +0200 (2003-04-25)
changeset 13922 75ae4244a596
parent 11463 96b5b27da55c
child 13926 6e62e5357a10
permissions -rw-r--r--
Changes required by the certified email protocol

Public-key model now provides separate signature/encryption keys and also
long-term symmetric keys.
     1 (*  Title:      HOL/Auth/Event
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Theory of events for security protocols
     7 
     8 Datatype of events; function "spies"; freshness
     9 
    10 "bad" agents have been broken by the Spy; their private keys and internal
    11     stores are visible to him
    12 *)
    13 
    14 theory Event = Message
    15 files ("Event_lemmas.ML"):
    16 
    17 consts  (*Initial states of agents -- parameter of the construction*)
    18   initState :: "agent => msg set"
    19 
    20 datatype
    21   event = Says  agent agent msg
    22         | Gets  agent       msg
    23         | Notes agent       msg
    24        
    25 consts 
    26   bad    :: "agent set"				(*compromised agents*)
    27   knows  :: "agent => event list => msg set"
    28 
    29 
    30 (*"spies" is retained for compatibility's sake*)
    31 syntax
    32   spies  :: "event list => msg set"
    33 
    34 translations
    35   "spies"   => "knows Spy"
    36 
    37 
    38 axioms
    39   (*Spy has access to his own key for spoof messages, but Server is secure*)
    40   Spy_in_bad     [iff] :    "Spy \<in> bad"
    41   Server_not_bad [iff] : "Server \<notin> bad"
    42 
    43 primrec
    44   knows_Nil:   "knows A [] = initState A"
    45   knows_Cons:
    46     "knows A (ev # evs) =
    47        (if A = Spy then 
    48 	(case ev of
    49 	   Says A' B X => insert X (knows Spy evs)
    50 	 | Gets A' X => knows Spy evs
    51 	 | Notes A' X  => 
    52 	     if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
    53 	else
    54 	(case ev of
    55 	   Says A' B X => 
    56 	     if A'=A then insert X (knows A evs) else knows A evs
    57 	 | Gets A' X    => 
    58 	     if A'=A then insert X (knows A evs) else knows A evs
    59 	 | Notes A' X    => 
    60 	     if A'=A then insert X (knows A evs) else knows A evs))"
    61 
    62 (*
    63   Case A=Spy on the Gets event
    64   enforces the fact that if a message is received then it must have been sent,
    65   therefore the oops case must use Notes
    66 *)
    67 
    68 consts
    69   (*Set of items that might be visible to somebody:
    70     complement of the set of fresh items*)
    71   used :: "event list => msg set"
    72 
    73 primrec
    74   used_Nil:   "used []         = (UN B. parts (initState B))"
    75   used_Cons:  "used (ev # evs) =
    76 		     (case ev of
    77 			Says A B X => parts {X} Un (used evs)
    78 		      | Gets A X   => used evs
    79 		      | Notes A X  => parts {X} Un (used evs))"
    80 
    81 
    82 lemma Notes_imp_used [rule_format]: "Notes A X : set evs --> X : used evs"
    83 apply (induct_tac evs);
    84 apply (auto split: event.split) 
    85 done
    86 
    87 lemma Says_imp_used [rule_format]: "Says A B X : set evs --> X : used evs"
    88 apply (induct_tac evs);
    89 apply (auto split: event.split) 
    90 done
    91 
    92 lemma MPair_used [rule_format]:
    93      "MPair X Y : used evs --> X : used evs & Y : used evs"
    94 apply (induct_tac evs);
    95 apply (auto split: event.split) 
    96 done
    97 
    98 use "Event_lemmas.ML"
    99 
   100 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
   101 by (induct e, auto simp: knows_Cons)
   102 
   103 lemma initState_subset_knows: "initState A <= knows A evs"
   104 apply (induct_tac evs)
   105 apply (simp add: ); 
   106 apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
   107 done
   108 
   109 
   110 (*For proving new_keys_not_used*)
   111 lemma keysFor_parts_insert:
   112      "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] \
   113 \     ==> K \<in> keysFor (parts (G Un H)) | Key (invKey K) \<in> parts H"; 
   114 by (force 
   115     dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
   116            analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
   117     intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
   118 
   119 method_setup analz_mono_contra = {*
   120     Method.no_args
   121       (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
   122     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   123 
   124 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
   125 
   126 ML
   127 {*
   128 val synth_analz_mono = thm "synth_analz_mono";
   129 
   130 val synth_analz_mono_contra_tac = 
   131   let val syan_impI = inst "P" "?Y ~: synth (analz (knows Spy ?evs))" impI
   132   in
   133     rtac syan_impI THEN' 
   134     REPEAT1 o 
   135       (dresolve_tac 
   136        [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
   137         knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
   138 	knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
   139     THEN'
   140     mp_tac
   141   end;
   142 *}
   143 
   144 method_setup synth_analz_mono_contra = {*
   145     Method.no_args
   146       (Method.METHOD (fn facts => REPEAT_FIRST synth_analz_mono_contra_tac)) *}
   147     "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
   148 
   149 end