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