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