src/HOL/Auth/Event.thy
author paulson
Fri Apr 25 11:18:14 2003 +0200 (2003-04-25)
changeset 13922 75ae4244a596
parent 11463 96b5b27da55c
child 13926 6e62e5357a10
permissions -rw-r--r--
Changes required by the certified email protocol

Public-key model now provides separate signature/encryption keys and also
long-term symmetric 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@3683
     8
Datatype of events; function "spies"; freshness
paulson@3678
     9
paulson@3683
    10
"bad" agents have been broken by the Spy; their private keys and internal
paulson@3678
    11
    stores are visible to him
paulson@3512
    12
*)
paulson@3512
    13
paulson@11104
    14
theory Event = Message
paulson@11104
    15
files ("Event_lemmas.ML"):
paulson@11104
    16
paulson@3512
    17
consts  (*Initial states of agents -- parameter of the construction*)
paulson@11104
    18
  initState :: "agent => msg set"
paulson@3512
    19
paulson@6399
    20
datatype
paulson@3512
    21
  event = Says  agent agent msg
paulson@6399
    22
        | Gets  agent       msg
paulson@3512
    23
        | Notes agent       msg
paulson@6308
    24
       
paulson@6308
    25
consts 
paulson@11104
    26
  bad    :: "agent set"				(*compromised agents*)
paulson@11104
    27
  knows  :: "agent => event list => msg set"
paulson@3512
    28
paulson@6308
    29
paulson@11310
    30
(*"spies" is retained for compatibility's sake*)
paulson@6308
    31
syntax
paulson@11104
    32
  spies  :: "event list => msg set"
paulson@3519
    33
paulson@6308
    34
translations
paulson@6308
    35
  "spies"   => "knows Spy"
paulson@6308
    36
paulson@6308
    37
paulson@11104
    38
axioms
paulson@3519
    39
  (*Spy has access to his own key for spoof messages, but Server is secure*)
paulson@13922
    40
  Spy_in_bad     [iff] :    "Spy \<in> bad"
paulson@13922
    41
  Server_not_bad [iff] : "Server \<notin> bad"
paulson@3512
    42
berghofe@5183
    43
primrec
paulson@11104
    44
  knows_Nil:   "knows A [] = initState A"
paulson@11104
    45
  knows_Cons:
paulson@6399
    46
    "knows A (ev # evs) =
paulson@6399
    47
       (if A = Spy then 
paulson@6399
    48
	(case ev of
paulson@6399
    49
	   Says A' B X => insert X (knows Spy evs)
paulson@6399
    50
	 | Gets A' X => knows Spy evs
paulson@6399
    51
	 | Notes A' X  => 
paulson@13922
    52
	     if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
paulson@6399
    53
	else
paulson@6399
    54
	(case ev of
paulson@6399
    55
	   Says A' B X => 
paulson@6399
    56
	     if A'=A then insert X (knows A evs) else knows A evs
paulson@6399
    57
	 | Gets A' X    => 
paulson@6399
    58
	     if A'=A then insert X (knows A evs) else knows A evs
paulson@6399
    59
	 | Notes A' X    => 
paulson@6399
    60
	     if A'=A then insert X (knows A evs) else knows A evs))"
paulson@6308
    61
paulson@6308
    62
(*
paulson@6308
    63
  Case A=Spy on the Gets event
paulson@6308
    64
  enforces the fact that if a message is received then it must have been sent,
paulson@6308
    65
  therefore the oops case must use Notes
paulson@6308
    66
*)
paulson@3678
    67
paulson@3683
    68
consts
paulson@3683
    69
  (*Set of items that might be visible to somebody:
paulson@3683
    70
    complement of the set of fresh items*)
paulson@11104
    71
  used :: "event list => msg set"
paulson@3512
    72
berghofe@5183
    73
primrec
paulson@11104
    74
  used_Nil:   "used []         = (UN B. parts (initState B))"
paulson@11104
    75
  used_Cons:  "used (ev # evs) =
paulson@11104
    76
		     (case ev of
paulson@11104
    77
			Says A B X => parts {X} Un (used evs)
paulson@11104
    78
		      | Gets A X   => used evs
paulson@11104
    79
		      | Notes A X  => parts {X} Un (used evs))"
paulson@6308
    80
paulson@6308
    81
paulson@11463
    82
lemma Notes_imp_used [rule_format]: "Notes A X : set evs --> X : used evs"
paulson@11463
    83
apply (induct_tac evs);
paulson@11463
    84
apply (auto split: event.split) 
paulson@11463
    85
done
paulson@11463
    86
paulson@11463
    87
lemma Says_imp_used [rule_format]: "Says A B X : set evs --> X : used evs"
paulson@11463
    88
apply (induct_tac evs);
paulson@11463
    89
apply (auto split: event.split) 
paulson@11463
    90
done
paulson@11463
    91
paulson@11463
    92
lemma MPair_used [rule_format]:
paulson@11463
    93
     "MPair X Y : used evs --> X : used evs & Y : used evs"
paulson@11463
    94
apply (induct_tac evs);
paulson@11463
    95
apply (auto split: event.split) 
paulson@11463
    96
done
paulson@11463
    97
paulson@11104
    98
use "Event_lemmas.ML"
paulson@11104
    99
paulson@13922
   100
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
paulson@13922
   101
by (induct e, auto simp: knows_Cons)
paulson@13922
   102
paulson@13922
   103
lemma initState_subset_knows: "initState A <= knows A evs"
paulson@13922
   104
apply (induct_tac evs)
paulson@13922
   105
apply (simp add: ); 
paulson@13922
   106
apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
paulson@13922
   107
done
paulson@13922
   108
paulson@13922
   109
paulson@13922
   110
(*For proving new_keys_not_used*)
paulson@13922
   111
lemma keysFor_parts_insert:
paulson@13922
   112
     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] \
paulson@13922
   113
\     ==> K \<in> keysFor (parts (G Un H)) | Key (invKey K) \<in> parts H"; 
paulson@13922
   114
by (force 
paulson@13922
   115
    dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
paulson@13922
   116
           analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
paulson@13922
   117
    intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
paulson@13922
   118
paulson@11104
   119
method_setup analz_mono_contra = {*
paulson@11104
   120
    Method.no_args
paulson@11104
   121
      (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
paulson@13922
   122
    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
paulson@13922
   123
paulson@13922
   124
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
paulson@13922
   125
paulson@13922
   126
ML
paulson@13922
   127
{*
paulson@13922
   128
val synth_analz_mono = thm "synth_analz_mono";
paulson@13922
   129
paulson@13922
   130
val synth_analz_mono_contra_tac = 
paulson@13922
   131
  let val syan_impI = inst "P" "?Y ~: synth (analz (knows Spy ?evs))" impI
paulson@13922
   132
  in
paulson@13922
   133
    rtac syan_impI THEN' 
paulson@13922
   134
    REPEAT1 o 
paulson@13922
   135
      (dresolve_tac 
paulson@13922
   136
       [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
paulson@13922
   137
        knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
paulson@13922
   138
	knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
paulson@13922
   139
    THEN'
paulson@13922
   140
    mp_tac
paulson@13922
   141
  end;
paulson@13922
   142
*}
paulson@13922
   143
paulson@13922
   144
method_setup synth_analz_mono_contra = {*
paulson@13922
   145
    Method.no_args
paulson@13922
   146
      (Method.METHOD (fn facts => REPEAT_FIRST synth_analz_mono_contra_tac)) *}
paulson@13922
   147
    "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
paulson@3512
   148
paulson@3512
   149
end