src/HOL/Auth/Event.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4266 dab1833cb26d
child 4686 74a12e86b20b
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
     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() addsplits [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() addsplits [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() addsplits [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 	                addsplits [expand_event_case, expand_if])));
    84 by (ALLGOALS Blast_tac);
    85 qed "parts_spies_subset_used";
    86 
    87 bind_thm ("usedI", impOfSubs parts_spies_subset_used);
    88 AddIs [usedI];
    89 
    90 goal thy "parts (initState B) <= used evs";
    91 by (induct_tac "evs" 1);
    92 by (ALLGOALS (asm_simp_tac
    93 	      (simpset() addsimps [parts_insert_spies]
    94 	                addsplits [expand_event_case, expand_if])));
    95 by (ALLGOALS Blast_tac);
    96 bind_thm ("initState_into_used", impOfSubs (result()));
    97 
    98 goal thy "used (Says A B X # evs) = parts{X} Un used evs";
    99 by (Simp_tac 1);
   100 qed "used_Says";
   101 Addsimps [used_Says];
   102 
   103 goal thy "used (Notes A X # evs) = parts{X} Un used evs";
   104 by (Simp_tac 1);
   105 qed "used_Notes";
   106 Addsimps [used_Notes];
   107 
   108 goal thy "used [] <= used evs";
   109 by (Simp_tac 1);
   110 by (blast_tac (claset() addIs [initState_into_used]) 1);
   111 qed "used_nil_subset";
   112 
   113 (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
   114 Delsimps [used_Nil, used_Cons];   
   115 
   116 
   117 (*currently unused*)
   118 goal thy "used evs <= used (evs@evs')";
   119 by (induct_tac "evs" 1);
   120 by (simp_tac (simpset() addsimps [used_nil_subset]) 1);
   121 by (induct_tac "a" 1);
   122 by (ALLGOALS Asm_simp_tac);
   123 by (ALLGOALS Blast_tac);
   124 qed "used_subset_append";
   125 
   126 
   127 (*For proving theorems of the form X ~: analz (spies evs) --> P
   128   New events added by induction to "evs" are discarded.  Provided 
   129   this information isn't needed, the proof will be much shorter, since
   130   it will omit complicated reasoning about analz.*)
   131 val analz_mono_contra_tac = 
   132   let val analz_impI = read_instantiate_sg (sign_of thy)
   133                 [("P", "?Y ~: analz (spies ?evs)")] impI;
   134   in
   135     rtac analz_impI THEN' 
   136     REPEAT1 o 
   137       (dresolve_tac 
   138        [spies_subset_spies_Says  RS analz_mono RS contra_subsetD,
   139 	spies_subset_spies_Notes RS analz_mono RS contra_subsetD])
   140     THEN'
   141     mp_tac
   142   end;