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