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