src/HOL/Auth/Event.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 32404 da3ca3c6ec81
child 37936 1e4c5015a72e
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
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@3683
     6
Datatype of events; function "spies"; freshness
paulson@3678
     7
paulson@3683
     8
"bad" agents have been broken by the Spy; their private keys and internal
paulson@3678
     9
    stores are visible to him
paulson@3512
    10
*)
paulson@3512
    11
paulson@13956
    12
header{*Theory of Events for Security Protocols*}
paulson@13956
    13
haftmann@16417
    14
theory Event imports Message begin
paulson@11104
    15
paulson@3512
    16
consts  (*Initial states of agents -- parameter of the construction*)
paulson@11104
    17
  initState :: "agent => msg set"
paulson@3512
    18
paulson@6399
    19
datatype
paulson@3512
    20
  event = Says  agent agent msg
paulson@6399
    21
        | Gets  agent       msg
paulson@3512
    22
        | Notes agent       msg
paulson@6308
    23
       
paulson@6308
    24
consts 
wenzelm@32960
    25
  bad    :: "agent set"                         -- {* compromised agents *}
paulson@11104
    26
  knows  :: "agent => event list => msg set"
paulson@3512
    27
paulson@6308
    28
paulson@14126
    29
text{*The constant "spies" is retained for compatibility's sake*}
wenzelm@20768
    30
wenzelm@20768
    31
abbreviation (input)
wenzelm@21404
    32
  spies  :: "event list => msg set" where
wenzelm@20768
    33
  "spies == knows Spy"
paulson@6308
    34
paulson@14126
    35
text{*Spy has access to his own key for spoof messages, but Server is secure*}
paulson@14126
    36
specification (bad)
paulson@14200
    37
  Spy_in_bad     [iff]: "Spy \<in> bad"
paulson@14200
    38
  Server_not_bad [iff]: "Server \<notin> bad"
paulson@14126
    39
    by (rule exI [of _ "{Spy}"], simp)
paulson@6308
    40
berghofe@5183
    41
primrec
paulson@11104
    42
  knows_Nil:   "knows A [] = initState A"
paulson@11104
    43
  knows_Cons:
paulson@6399
    44
    "knows A (ev # evs) =
paulson@6399
    45
       (if A = Spy then 
wenzelm@32960
    46
        (case ev of
wenzelm@32960
    47
           Says A' B X => insert X (knows Spy evs)
wenzelm@32960
    48
         | Gets A' X => knows Spy evs
wenzelm@32960
    49
         | Notes A' X  => 
wenzelm@32960
    50
             if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
wenzelm@32960
    51
        else
wenzelm@32960
    52
        (case ev of
wenzelm@32960
    53
           Says A' B X => 
wenzelm@32960
    54
             if A'=A then insert X (knows A evs) else knows A evs
wenzelm@32960
    55
         | Gets A' X    => 
wenzelm@32960
    56
             if A'=A then insert X (knows A evs) else knows A evs
wenzelm@32960
    57
         | Notes A' X    => 
wenzelm@32960
    58
             if A'=A then insert X (knows A evs) else knows A evs))"
paulson@6308
    59
paulson@6308
    60
(*
paulson@6308
    61
  Case A=Spy on the Gets event
paulson@6308
    62
  enforces the fact that if a message is received then it must have been sent,
paulson@6308
    63
  therefore the oops case must use Notes
paulson@6308
    64
*)
paulson@3678
    65
paulson@3683
    66
consts
paulson@3683
    67
  (*Set of items that might be visible to somebody:
paulson@3683
    68
    complement of the set of fresh items*)
paulson@11104
    69
  used :: "event list => msg set"
paulson@3512
    70
berghofe@5183
    71
primrec
paulson@11104
    72
  used_Nil:   "used []         = (UN B. parts (initState B))"
paulson@11104
    73
  used_Cons:  "used (ev # evs) =
wenzelm@32960
    74
                     (case ev of
wenzelm@32960
    75
                        Says A B X => parts {X} \<union> used evs
wenzelm@32960
    76
                      | Gets A X   => used evs
wenzelm@32960
    77
                      | Notes A X  => parts {X} \<union> used evs)"
paulson@13935
    78
    --{*The case for @{term Gets} seems anomalous, but @{term Gets} always
paulson@13935
    79
        follows @{term Says} in real protocols.  Seems difficult to change.
paulson@13935
    80
        See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}
paulson@6308
    81
paulson@13926
    82
lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
paulson@13926
    83
apply (induct_tac evs)
paulson@11463
    84
apply (auto split: event.split) 
paulson@11463
    85
done
paulson@11463
    86
paulson@13926
    87
lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs"
paulson@13926
    88
apply (induct_tac evs)
paulson@11463
    89
apply (auto split: event.split) 
paulson@11463
    90
done
paulson@11463
    91
paulson@13926
    92
paulson@13926
    93
subsection{*Function @{term knows}*}
paulson@13926
    94
paulson@13956
    95
(*Simplifying   
paulson@13956
    96
 parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
paulson@13956
    97
  This version won't loop with the simplifier.*)
paulson@13935
    98
lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
paulson@13926
    99
paulson@13926
   100
lemma knows_Spy_Says [simp]:
paulson@13926
   101
     "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
paulson@13926
   102
by simp
paulson@13926
   103
paulson@14200
   104
text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
paulson@14200
   105
      on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
paulson@13926
   106
lemma knows_Spy_Notes [simp]:
paulson@13926
   107
     "knows Spy (Notes A X # evs) =  
paulson@13926
   108
          (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
paulson@13926
   109
by simp
paulson@13926
   110
paulson@13926
   111
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
paulson@13926
   112
by simp
paulson@13926
   113
paulson@13926
   114
lemma knows_Spy_subset_knows_Spy_Says:
paulson@13935
   115
     "knows Spy evs \<subseteq> knows Spy (Says A B X # evs)"
paulson@13926
   116
by (simp add: subset_insertI)
paulson@13926
   117
paulson@13926
   118
lemma knows_Spy_subset_knows_Spy_Notes:
paulson@13935
   119
     "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)"
paulson@13926
   120
by force
paulson@13926
   121
paulson@13926
   122
lemma knows_Spy_subset_knows_Spy_Gets:
paulson@13935
   123
     "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)"
paulson@13926
   124
by (simp add: subset_insertI)
paulson@13926
   125
paulson@13926
   126
text{*Spy sees what is sent on the traffic*}
paulson@13926
   127
lemma Says_imp_knows_Spy [rule_format]:
paulson@13926
   128
     "Says A B X \<in> set evs --> X \<in> knows Spy evs"
paulson@13926
   129
apply (induct_tac "evs")
paulson@13926
   130
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   131
done
paulson@13926
   132
paulson@13926
   133
lemma Notes_imp_knows_Spy [rule_format]:
paulson@13926
   134
     "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
paulson@13926
   135
apply (induct_tac "evs")
paulson@13926
   136
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   137
done
paulson@13926
   138
paulson@13926
   139
paulson@13926
   140
text{*Elimination rules: derive contradictions from old Says events containing
paulson@13926
   141
  items known to be fresh*}
paulson@32404
   142
lemmas Says_imp_parts_knows_Spy = 
paulson@32404
   143
       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
paulson@32404
   144
paulson@13926
   145
lemmas knows_Spy_partsEs =
paulson@32404
   146
     Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard]
paulson@13926
   147
paulson@18570
   148
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
paulson@18570
   149
paulson@13926
   150
text{*Compatibility for the old "spies" function*}
paulson@13926
   151
lemmas spies_partsEs = knows_Spy_partsEs
paulson@13926
   152
lemmas Says_imp_spies = Says_imp_knows_Spy
paulson@13935
   153
lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy]
paulson@13926
   154
paulson@13926
   155
paulson@13926
   156
subsection{*Knowledge of Agents*}
paulson@13926
   157
paulson@13926
   158
lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
paulson@13926
   159
by simp
paulson@13926
   160
paulson@13926
   161
lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
paulson@13926
   162
by simp
paulson@13926
   163
paulson@13926
   164
lemma knows_Gets:
paulson@13926
   165
     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
paulson@13926
   166
by simp
paulson@13926
   167
paulson@13926
   168
paulson@13935
   169
lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
paulson@13935
   170
by (simp add: subset_insertI)
paulson@13926
   171
paulson@13935
   172
lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)"
paulson@13935
   173
by (simp add: subset_insertI)
paulson@13926
   174
paulson@13935
   175
lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)"
paulson@13935
   176
by (simp add: subset_insertI)
paulson@13926
   177
paulson@13926
   178
text{*Agents know what they say*}
paulson@13926
   179
lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
paulson@13926
   180
apply (induct_tac "evs")
paulson@13926
   181
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   182
apply blast
paulson@13926
   183
done
paulson@13926
   184
paulson@13926
   185
text{*Agents know what they note*}
paulson@13926
   186
lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
paulson@13926
   187
apply (induct_tac "evs")
paulson@13926
   188
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   189
apply blast
paulson@13926
   190
done
paulson@13926
   191
paulson@13926
   192
text{*Agents know what they receive*}
paulson@13926
   193
lemma Gets_imp_knows_agents [rule_format]:
paulson@13926
   194
     "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
paulson@13926
   195
apply (induct_tac "evs")
paulson@13926
   196
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   197
done
paulson@13926
   198
paulson@13926
   199
paulson@13926
   200
text{*What agents DIFFERENT FROM Spy know 
paulson@13926
   201
  was either said, or noted, or got, or known initially*}
paulson@13926
   202
lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
paulson@13926
   203
     "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.  
paulson@13926
   204
  Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
paulson@13926
   205
apply (erule rev_mp)
paulson@13926
   206
apply (induct_tac "evs")
paulson@13926
   207
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   208
apply blast
paulson@13926
   209
done
paulson@13926
   210
paulson@13926
   211
text{*What the Spy knows -- for the time being --
paulson@13926
   212
  was either said or noted, or known initially*}
paulson@13926
   213
lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
paulson@13926
   214
     "[| X \<in> knows Spy evs |] ==> EX A B.  
paulson@13926
   215
  Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
paulson@13926
   216
apply (erule rev_mp)
paulson@13926
   217
apply (induct_tac "evs")
paulson@13926
   218
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   219
apply blast
paulson@13926
   220
done
paulson@13926
   221
paulson@13935
   222
lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
paulson@13935
   223
apply (induct_tac "evs", force)  
paulson@13935
   224
apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) 
paulson@13926
   225
done
paulson@13926
   226
paulson@13926
   227
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
paulson@13926
   228
paulson@13926
   229
lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
paulson@13926
   230
apply (induct_tac "evs")
paulson@13935
   231
apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
paulson@13926
   232
done
paulson@13926
   233
paulson@13926
   234
lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
paulson@13926
   235
by simp
paulson@13926
   236
paulson@13926
   237
lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
paulson@13926
   238
by simp
paulson@13926
   239
paulson@13926
   240
lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
paulson@13926
   241
by simp
paulson@13926
   242
paulson@13935
   243
lemma used_nil_subset: "used [] \<subseteq> used evs"
paulson@13935
   244
apply simp
paulson@13926
   245
apply (blast intro: initState_into_used)
paulson@13926
   246
done
paulson@13926
   247
paulson@13926
   248
text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
paulson@13935
   249
declare knows_Cons [simp del]
paulson@13935
   250
        used_Nil [simp del] used_Cons [simp del]
paulson@13926
   251
paulson@13926
   252
paulson@13926
   253
text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
paulson@13926
   254
  New events added by induction to "evs" are discarded.  Provided 
paulson@13926
   255
  this information isn't needed, the proof will be much shorter, since
paulson@13926
   256
  it will omit complicated reasoning about @{term analz}.*}
paulson@13926
   257
paulson@13926
   258
lemmas analz_mono_contra =
paulson@13926
   259
       knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
paulson@13926
   260
       knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
paulson@13926
   261
       knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
paulson@13926
   262
paulson@11104
   263
paulson@13922
   264
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
paulson@13922
   265
by (induct e, auto simp: knows_Cons)
paulson@13922
   266
paulson@13935
   267
lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
paulson@13926
   268
apply (induct_tac evs, simp) 
paulson@13922
   269
apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
paulson@13922
   270
done
paulson@13922
   271
paulson@13922
   272
paulson@13926
   273
text{*For proving @{text new_keys_not_used}*}
paulson@13922
   274
lemma keysFor_parts_insert:
paulson@13926
   275
     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
paulson@13926
   276
      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
paulson@13922
   277
by (force 
paulson@13922
   278
    dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
paulson@13922
   279
           analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
paulson@13922
   280
    intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
paulson@13922
   281
wenzelm@24122
   282
wenzelm@27225
   283
lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
wenzelm@27225
   284
wenzelm@24122
   285
ML
wenzelm@24122
   286
{*
wenzelm@24122
   287
val analz_mono_contra_tac = 
wenzelm@27225
   288
  rtac @{thm analz_impI} THEN' 
wenzelm@27225
   289
  REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
wenzelm@27225
   290
  THEN' mp_tac
wenzelm@24122
   291
*}
wenzelm@24122
   292
paulson@11104
   293
method_setup analz_mono_contra = {*
wenzelm@30549
   294
    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
paulson@13922
   295
    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
paulson@13922
   296
paulson@13922
   297
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
paulson@13922
   298
wenzelm@27225
   299
lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
wenzelm@27225
   300
paulson@13922
   301
ML
paulson@13922
   302
{*
paulson@13922
   303
val synth_analz_mono_contra_tac = 
wenzelm@27225
   304
  rtac @{thm syan_impI} THEN'
wenzelm@27225
   305
  REPEAT1 o 
wenzelm@27225
   306
    (dresolve_tac 
wenzelm@27225
   307
     [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
wenzelm@27225
   308
      @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
wenzelm@27225
   309
      @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
wenzelm@27225
   310
  THEN'
wenzelm@27225
   311
  mp_tac
paulson@13922
   312
*}
paulson@13922
   313
paulson@13922
   314
method_setup synth_analz_mono_contra = {*
wenzelm@30549
   315
    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
paulson@13922
   316
    "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
paulson@3512
   317
paulson@3512
   318
end