src/HOL/Auth/Event.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6399 4a9040b85e2e
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     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 
     7 AddIffs [Spy_in_bad, Server_not_bad];
     8 
     9 Addsimps [knows_Cons, used_Cons];
    10 
    11 (**** Function "knows" ****)
    12 
    13 (** Simplifying   parts (insert X (knows Spy evs))
    14       = parts {X} Un parts (knows Spy evs) -- since general case loops*)
    15 
    16 bind_thm ("parts_insert_knows_Spy",
    17 	  parts_insert |> 
    18 	  read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]);
    19 
    20 
    21 Goal "P(event_case sf gf nf ev) = \
    22 \      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
    23 \       (ALL A X. ev = Gets A X --> P(gf A X)) & \
    24 \       (ALL A X. ev = Notes A X --> P(nf A X)))";
    25 by (induct_tac "ev" 1);
    26 by Auto_tac;
    27 qed "expand_event_case";
    28 
    29 Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)";
    30 by (Simp_tac 1);
    31 qed "knows_Spy_Says";
    32 
    33 (*The point of letting the Spy see "bad" agents' notes is to prevent
    34   redundant case-splits on whether A=Spy and whether A:bad*)
    35 Goal "knows Spy (Notes A X # evs) = \
    36 \         (if A:bad then insert X (knows Spy evs) else knows Spy evs)";
    37 by (Simp_tac 1);
    38 qed "knows_Spy_Notes";
    39 
    40 Goal "knows Spy (Gets A X # evs) = knows Spy evs";
    41 by (Simp_tac 1);
    42 qed "knows_Spy_Gets";
    43 
    44 Goal "knows Spy evs <= knows Spy (Says A B X # evs)";
    45 by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    46 qed "knows_Spy_subset_knows_Spy_Says";
    47 
    48 Goal "knows Spy evs <= knows Spy (Notes A X # evs)";
    49 by (Simp_tac 1);
    50 by (Fast_tac 1);
    51 qed "knows_Spy_subset_knows_Spy_Notes";
    52 
    53 Goal "knows Spy evs <= knows Spy (Gets A X # evs)";
    54 by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    55 qed "knows_Spy_subset_knows_Spy_Gets";
    56 
    57 (*Spy sees what is sent on the traffic*)
    58 Goal "Says A B X : set evs --> X : knows Spy evs";
    59 by (induct_tac "evs" 1);
    60 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    61 qed_spec_mp "Says_imp_knows_Spy";
    62 
    63 Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs";
    64 by (induct_tac "evs" 1);
    65 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    66 qed_spec_mp "Notes_imp_knows_Spy";
    67 
    68 
    69 (*Use with addSEs to derive contradictions from old Says events containing
    70   items known to be fresh*)
    71 val knows_Spy_partsEs = make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs;
    72 
    73 Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets];
    74 
    75 
    76 (*Begin lemmas about agents' knowledge*)
    77 
    78 Goal "knows A (Says A B X # evs) = insert X (knows A evs)";
    79 by (Simp_tac 1);
    80 qed "knows_Says";
    81 
    82 Goal "knows A (Notes A X # evs) = insert X (knows A evs)";
    83 by (Simp_tac 1);
    84 qed "knows_Notes";
    85 
    86 Goal "A ~= Spy --> knows A (Gets A X # evs) = insert X (knows A evs)";
    87 by (Simp_tac 1);
    88 qed "knows_Gets";
    89 
    90 
    91 Goal "knows A evs <= knows A (Says A B X # evs)";
    92 by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    93 qed "knows_subset_knows_Says";
    94 
    95 Goal "knows A evs <= knows A (Notes A X # evs)";
    96 by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    97 qed "knows_subset_knows_Notes";
    98 
    99 Goal "knows A evs <= knows A (Gets A X # evs)";
   100 by (simp_tac (simpset() addsimps [subset_insertI]) 1);
   101 qed "knows_subset_knows_Gets";
   102 
   103 (*Agents know what they say*)
   104 Goal "Says A B X : set evs --> X : knows A evs";
   105 by (induct_tac "evs" 1);
   106 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   107 by (Blast_tac 1);
   108 qed_spec_mp "Says_imp_knows";
   109 
   110 (*Agents know what they note*)
   111 Goal "Notes A X : set evs --> X : knows A evs";
   112 by (induct_tac "evs" 1);
   113 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   114 by (Blast_tac 1);
   115 qed_spec_mp "Notes_imp_knows";
   116 
   117 (*Agents know what they receive*)
   118 Goal "A ~= Spy --> Gets A X : set evs --> X : knows A evs";
   119 by (induct_tac "evs" 1);
   120 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   121 qed_spec_mp "Gets_imp_knows_agents";
   122 
   123 
   124 (*What agents DIFFERENT FROM Spy know 
   125   was either said, or noted, or got, or known initially*)
   126 Goal "[| X : knows A evs; A ~= Spy |] ==> EX B. \
   127 \ Says A B X : set evs | Gets A X : set evs | Notes A X : set evs | X : initState A";
   128 by (etac rev_mp 1);
   129 by (induct_tac "evs" 1);
   130 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   131 by (Blast_tac 1);
   132 qed_spec_mp "knows_imp_Says_Gets_Notes_initState";
   133 
   134 (*What the Spy knows -- for the time being --
   135   was either said or noted, or known initially*)
   136 Goal "[| X : knows Spy evs |] ==> EX A B. \
   137 \ Says A B X : set evs | Notes A X : set evs | X : initState Spy";
   138 by (etac rev_mp 1);
   139 by (induct_tac "evs" 1);
   140 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
   141 by (Blast_tac 1);
   142 qed_spec_mp "knows_Spy_imp_Says_Notes_initState";
   143 
   144 (*END lemmas about agents' knowledge*)
   145 
   146 
   147 
   148 (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
   149 Delsimps [knows_Cons];   
   150 
   151 
   152 (*** Fresh nonces ***)
   153 
   154 Goal "parts (knows Spy evs) <= used evs";
   155 by (induct_tac "evs" 1);
   156 by (ALLGOALS (asm_simp_tac
   157 	      (simpset() addsimps [parts_insert_knows_Spy]
   158 	                addsplits [expand_event_case])));
   159 by (ALLGOALS Blast_tac);
   160 qed "parts_knows_Spy_subset_used";
   161 
   162 bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used);
   163 AddIs [usedI];
   164 
   165 Goal "parts (initState B) <= used evs";
   166 by (induct_tac "evs" 1);
   167 by (ALLGOALS (asm_simp_tac
   168 	      (simpset() addsimps [parts_insert_knows_Spy]
   169 	                addsplits [expand_event_case])));
   170 by (ALLGOALS Blast_tac);
   171 bind_thm ("initState_into_used", impOfSubs (result()));
   172 
   173 Goal "used (Says A B X # evs) = parts{X} Un used evs";
   174 by (Simp_tac 1);
   175 qed "used_Says";
   176 Addsimps [used_Says];
   177 
   178 Goal "used (Notes A X # evs) = parts{X} Un used evs";
   179 by (Simp_tac 1);
   180 qed "used_Notes";
   181 Addsimps [used_Notes];
   182 
   183 Goal "used (Gets A X # evs) = used evs";
   184 by (Simp_tac 1);
   185 qed "used_Gets";
   186 Addsimps [used_Gets];
   187 
   188 Goal "used [] <= used evs";
   189 by (Simp_tac 1);
   190 by (blast_tac (claset() addIs [initState_into_used]) 1);
   191 qed "used_nil_subset";
   192 
   193 (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
   194 Delsimps [used_Nil, used_Cons];   
   195 
   196 
   197 (*For proving theorems of the form X ~: analz (knows Spy evs) --> P
   198   New events added by induction to "evs" are discarded.  Provided 
   199   this information isn't needed, the proof will be much shorter, since
   200   it will omit complicated reasoning about analz.*)
   201 val analz_mono_contra_tac = 
   202   let val analz_impI = read_instantiate_sg (sign_of thy)
   203                 [("P", "?Y ~: analz (knows Spy ?evs)")] impI;
   204   in
   205     rtac analz_impI THEN' 
   206     REPEAT1 o 
   207       (dresolve_tac 
   208        [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
   209         knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
   210 	knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD])
   211     THEN'
   212     mp_tac
   213   end;
   214 
   215 fun Reception_tac i =
   216     blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj, 
   217                                impOfSubs (parts_insert RS equalityD1), 
   218 			       parts_trans,
   219                                Says_imp_knows_Spy RS analz.Inj,
   220                                impOfSubs analz_mono, analz_cut] 
   221                         addIs [less_SucI]) i;
   222 
   223 
   224 (*Compatibility for the old "spies" function*)
   225 val spies_partsEs = knows_Spy_partsEs;
   226 val Says_imp_spies = Says_imp_knows_Spy;
   227 val parts_insert_spies = parts_insert_knows_Spy;