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
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)";
paulson@3683
    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)";
paulson@3512
    49
by (simp_tac (!simpset setloop split_tac [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
paulson@3683
    57
	      (!simpset setloop split_tac [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
paulson@3683
    64
	      (!simpset setloop split_tac [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
paulson@3683
    82
	      (!simpset addsimps [parts_insert_spies]
paulson@3683
    83
	                setloop split_tac [expand_event_case, expand_if])));
paulson@3683
    84
by (ALLGOALS Blast_tac);
paulson@3683
    85
bind_thm ("usedI", impOfSubs (result()));
paulson@3512
    86
AddIs [usedI];
paulson@3512
    87
paulson@3683
    88
goal thy "parts (initState B) <= used evs";
paulson@3683
    89
by (induct_tac "evs" 1);
paulson@3683
    90
by (ALLGOALS (asm_simp_tac
paulson@3683
    91
	      (!simpset addsimps [parts_insert_spies]
paulson@3683
    92
	                setloop split_tac [expand_event_case, expand_if])));
paulson@3683
    93
by (ALLGOALS Blast_tac);
paulson@3683
    94
bind_thm ("initState_into_used", impOfSubs (result()));
paulson@3683
    95
paulson@3512
    96
goal thy "used (Says A B X # evs) = parts{X} Un used evs";
paulson@3683
    97
by (Simp_tac 1);
paulson@3512
    98
qed "used_Says";
paulson@3512
    99
Addsimps [used_Says];
paulson@3512
   100
paulson@3512
   101
goal thy "used (Notes A X # evs) = parts{X} Un used evs";
paulson@3683
   102
by (Simp_tac 1);
paulson@3512
   103
qed "used_Notes";
paulson@3512
   104
Addsimps [used_Notes];
paulson@3512
   105
paulson@3683
   106
goal thy "used [] <= used evs";
paulson@3683
   107
by (Simp_tac 1);
paulson@3683
   108
by (blast_tac (!claset addIs [initState_into_used]) 1);
paulson@3512
   109
qed "used_nil_subset";
paulson@3512
   110
paulson@3683
   111
(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
paulson@3683
   112
Delsimps [used_Nil, used_Cons];   
paulson@3683
   113
paulson@3683
   114
paulson@3683
   115
(*currently unused*)
paulson@3683
   116
goal thy "used evs <= used (evs@evs')";
paulson@3683
   117
by (induct_tac "evs" 1);
paulson@3512
   118
by (simp_tac (!simpset addsimps [used_nil_subset]) 1);
paulson@3667
   119
by (induct_tac "a" 1);
paulson@3512
   120
by (ALLGOALS Asm_simp_tac);
paulson@3512
   121
by (ALLGOALS Blast_tac);
paulson@3512
   122
qed "used_subset_append";
paulson@3512
   123
paulson@3512
   124
paulson@3683
   125
(*For proving theorems of the form X ~: analz (spies evs) --> P
paulson@3512
   126
  New events added by induction to "evs" are discarded.  Provided 
paulson@3512
   127
  this information isn't needed, the proof will be much shorter, since
paulson@3512
   128
  it will omit complicated reasoning about analz.*)
paulson@3512
   129
val analz_mono_contra_tac = 
paulson@3512
   130
  let val impI' = read_instantiate_sg (sign_of thy)
paulson@3519
   131
                [("P", "?Y ~: analz (sees ?A ?evs)")] impI;
paulson@3512
   132
  in
paulson@3512
   133
    rtac impI THEN' 
paulson@3512
   134
    REPEAT1 o 
paulson@3512
   135
      (dresolve_tac 
paulson@3683
   136
       [spies_subset_spies_Says  RS analz_mono RS contra_subsetD,
paulson@3683
   137
	spies_subset_spies_Notes RS analz_mono RS contra_subsetD])
paulson@3512
   138
    THEN'
paulson@3512
   139
    mp_tac
paulson@3512
   140
  end;