src/HOL/Auth/Event.ML
author paulson
Fri Sep 19 18:27:31 1997 +0200 (1997-09-19)
changeset 3686 4b484805b4c4
parent 3683 aafe719dff14
child 3701 6f0ed3eef1a9
permissions -rw-r--r--
First working version with Oops event for session 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 "sees"; freshness
     9 *)
    10 
    11 open Event;
    12 
    13 AddIffs [Spy_in_bad, Server_not_bad];
    14 
    15 (**** Function "spies" ****)
    16 
    17 (** Simplifying   parts (insert X (spies evs))
    18       = parts {X} Un parts (spies evs) -- since general case loops*)
    19 
    20 bind_thm ("parts_insert_spies",
    21 	  parts_insert |> 
    22 	  read_instantiate_sg (sign_of thy) [("H", "spies evs")]);
    23 
    24 
    25 goal thy
    26     "P(event_case sf nf ev) = \
    27 \      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
    28 \       (ALL A X. ev = Notes A X --> P(nf A X)))";
    29 by (induct_tac "ev" 1);
    30 by (Auto_tac());
    31 qed "expand_event_case";
    32 
    33 goal thy "spies (Says A B X # evs) = insert X (spies evs)";
    34 by (Simp_tac 1);
    35 qed "spies_Says";
    36 
    37 (*The point of letting the Spy see "bad" agents' notes is to prevent
    38   redundant case-splits on whether A=Spy and whether A:bad*)
    39 goal thy "spies (Notes A X # evs) = \
    40 \         (if A:bad then insert X (spies evs) else spies evs)";
    41 by (Simp_tac 1);
    42 qed "spies_Notes";
    43 
    44 goal thy "spies evs <= spies (Says A B X # evs)";
    45 by (simp_tac (!simpset addsimps [subset_insertI]) 1);
    46 qed "spies_subset_spies_Says";
    47 
    48 goal thy "spies evs <= spies (Notes A X # evs)";
    49 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    50 by (Fast_tac 1);
    51 qed "spies_subset_spies_Notes";
    52 
    53 (*Spy sees all traffic*)
    54 goal thy "Says A B X : set evs --> X : spies evs";
    55 by (induct_tac "evs" 1);
    56 by (ALLGOALS (asm_simp_tac
    57 	      (!simpset setloop split_tac [expand_event_case, expand_if])));
    58 qed_spec_mp "Says_imp_spies";
    59 
    60 (*Spy sees Notes of bad agents*)
    61 goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
    62 by (induct_tac "evs" 1);
    63 by (ALLGOALS (asm_simp_tac
    64 	      (!simpset setloop split_tac [expand_event_case, expand_if])));
    65 qed_spec_mp "Notes_imp_spies";
    66 
    67 (*Use with addSEs to derive contradictions from old Says events containing
    68   items known to be fresh*)
    69 val spies_partsEs = make_elim (Says_imp_spies RS parts.Inj) :: partsEs;
    70 
    71 Addsimps [spies_Says, spies_Notes];
    72 
    73 (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
    74 Delsimps [spies_Cons];   
    75 
    76 
    77 (*** Fresh nonces ***)
    78 
    79 goal thy "parts (spies evs) <= used evs";
    80 by (induct_tac "evs" 1);
    81 by (ALLGOALS (asm_simp_tac
    82 	      (!simpset addsimps [parts_insert_spies]
    83 	                setloop split_tac [expand_event_case, expand_if])));
    84 by (ALLGOALS Blast_tac);
    85 bind_thm ("usedI", impOfSubs (result()));
    86 AddIs [usedI];
    87 
    88 goal thy "parts (initState B) <= used evs";
    89 by (induct_tac "evs" 1);
    90 by (ALLGOALS (asm_simp_tac
    91 	      (!simpset addsimps [parts_insert_spies]
    92 	                setloop split_tac [expand_event_case, expand_if])));
    93 by (ALLGOALS Blast_tac);
    94 bind_thm ("initState_into_used", impOfSubs (result()));
    95 
    96 goal thy "used (Says A B X # evs) = parts{X} Un used evs";
    97 by (Simp_tac 1);
    98 qed "used_Says";
    99 Addsimps [used_Says];
   100 
   101 goal thy "used (Notes A X # evs) = parts{X} Un used evs";
   102 by (Simp_tac 1);
   103 qed "used_Notes";
   104 Addsimps [used_Notes];
   105 
   106 goal thy "used [] <= used evs";
   107 by (Simp_tac 1);
   108 by (blast_tac (!claset addIs [initState_into_used]) 1);
   109 qed "used_nil_subset";
   110 
   111 (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
   112 Delsimps [used_Nil, used_Cons];   
   113 
   114 
   115 (*currently unused*)
   116 goal thy "used evs <= used (evs@evs')";
   117 by (induct_tac "evs" 1);
   118 by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
   119 by (induct_tac "a" 1);
   120 by (ALLGOALS Asm_simp_tac);
   121 by (ALLGOALS Blast_tac);
   122 qed "used_subset_append";
   123 
   124 
   125 (*For proving theorems of the form X ~: analz (spies evs) --> P
   126   New events added by induction to "evs" are discarded.  Provided 
   127   this information isn't needed, the proof will be much shorter, since
   128   it will omit complicated reasoning about analz.*)
   129 val analz_mono_contra_tac = 
   130   let val impI' = read_instantiate_sg (sign_of thy)
   131                 [("P", "?Y ~: analz (sees ?A ?evs)")] impI;
   132   in
   133     rtac impI THEN' 
   134     REPEAT1 o 
   135       (dresolve_tac 
   136        [spies_subset_spies_Says  RS analz_mono RS contra_subsetD,
   137 	spies_subset_spies_Notes RS analz_mono RS contra_subsetD])
   138     THEN'
   139     mp_tac
   140   end;