src/HOL/Auth/Event.thy
author paulson
Sat Apr 26 12:38:42 2003 +0200 (2003-04-26)
changeset 13926 6e62e5357a10
parent 13922 75ae4244a596
child 13935 4822d9597d1e
permissions -rw-r--r--
converting more HOL-Auth to new-style theories
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@13926
    14
theory Event = Message:
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 
paulson@11104
    25
  bad    :: "agent set"				(*compromised agents*)
paulson@11104
    26
  knows  :: "agent => event list => msg set"
paulson@3512
    27
paulson@6308
    28
paulson@11310
    29
(*"spies" is retained for compatibility's sake*)
paulson@6308
    30
syntax
paulson@11104
    31
  spies  :: "event list => msg set"
paulson@3519
    32
paulson@6308
    33
translations
paulson@6308
    34
  "spies"   => "knows Spy"
paulson@6308
    35
paulson@6308
    36
paulson@11104
    37
axioms
paulson@3519
    38
  (*Spy has access to his own key for spoof messages, but Server is secure*)
paulson@13922
    39
  Spy_in_bad     [iff] :    "Spy \<in> bad"
paulson@13922
    40
  Server_not_bad [iff] : "Server \<notin> bad"
paulson@3512
    41
berghofe@5183
    42
primrec
paulson@11104
    43
  knows_Nil:   "knows A [] = initState A"
paulson@11104
    44
  knows_Cons:
paulson@6399
    45
    "knows A (ev # evs) =
paulson@6399
    46
       (if A = Spy then 
paulson@6399
    47
	(case ev of
paulson@6399
    48
	   Says A' B X => insert X (knows Spy evs)
paulson@6399
    49
	 | Gets A' X => knows Spy evs
paulson@6399
    50
	 | Notes A' X  => 
paulson@13922
    51
	     if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
paulson@6399
    52
	else
paulson@6399
    53
	(case ev of
paulson@6399
    54
	   Says A' B X => 
paulson@6399
    55
	     if A'=A then insert X (knows A evs) else knows A evs
paulson@6399
    56
	 | Gets A' X    => 
paulson@6399
    57
	     if A'=A then insert X (knows A evs) else knows A evs
paulson@6399
    58
	 | Notes A' X    => 
paulson@6399
    59
	     if A'=A then insert X (knows A evs) else knows A evs))"
paulson@6308
    60
paulson@6308
    61
(*
paulson@6308
    62
  Case A=Spy on the Gets event
paulson@6308
    63
  enforces the fact that if a message is received then it must have been sent,
paulson@6308
    64
  therefore the oops case must use Notes
paulson@6308
    65
*)
paulson@3678
    66
paulson@3683
    67
consts
paulson@3683
    68
  (*Set of items that might be visible to somebody:
paulson@3683
    69
    complement of the set of fresh items*)
paulson@11104
    70
  used :: "event list => msg set"
paulson@3512
    71
berghofe@5183
    72
primrec
paulson@11104
    73
  used_Nil:   "used []         = (UN B. parts (initState B))"
paulson@11104
    74
  used_Cons:  "used (ev # evs) =
paulson@11104
    75
		     (case ev of
paulson@13926
    76
			Says A B X => parts {X} \<union> (used evs)
paulson@11104
    77
		      | Gets A X   => used evs
paulson@13926
    78
		      | Notes A X  => parts {X} \<union> (used evs))"
paulson@6308
    79
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@11463
    91
lemma MPair_used [rule_format]:
paulson@13926
    92
     "MPair X Y \<in> used evs --> X \<in> used evs & Y \<in> used evs"
paulson@13926
    93
apply (induct_tac evs)
paulson@11463
    94
apply (auto split: event.split) 
paulson@11463
    95
done
paulson@11463
    96
paulson@13926
    97
paulson@13926
    98
subsection{*Function @{term knows}*}
paulson@13926
    99
paulson@13926
   100
text{*Simplifying   @term{"parts (insert X (knows Spy evs))
paulson@13926
   101
      = parts {X} \<union> parts (knows Spy evs)"}.  The general case loops.*)
paulson@13926
   102
paulson@13926
   103
text{*This version won't loop with the simplifier.*}
paulson@13926
   104
lemmas parts_insert_knows_Spy = parts_insert [of _ "knows Spy evs", standard]
paulson@13926
   105
paulson@13926
   106
lemma knows_Spy_Says [simp]:
paulson@13926
   107
     "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
paulson@13926
   108
by simp
paulson@13926
   109
paulson@13926
   110
text{*The point of letting the Spy see "bad" agents' notes is to prevent
paulson@13926
   111
  redundant case-splits on whether A=Spy and whether A:bad*}
paulson@13926
   112
lemma knows_Spy_Notes [simp]:
paulson@13926
   113
     "knows Spy (Notes A X # evs) =  
paulson@13926
   114
          (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
paulson@13926
   115
by simp
paulson@13926
   116
paulson@13926
   117
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
paulson@13926
   118
by simp
paulson@13926
   119
paulson@13926
   120
lemma knows_Spy_subset_knows_Spy_Says:
paulson@13926
   121
     "knows Spy evs <= knows Spy (Says A B X # evs)"
paulson@13926
   122
by (simp add: subset_insertI)
paulson@13926
   123
paulson@13926
   124
lemma knows_Spy_subset_knows_Spy_Notes:
paulson@13926
   125
     "knows Spy evs <= knows Spy (Notes A X # evs)"
paulson@13926
   126
by force
paulson@13926
   127
paulson@13926
   128
lemma knows_Spy_subset_knows_Spy_Gets:
paulson@13926
   129
     "knows Spy evs <= knows Spy (Gets A X # evs)"
paulson@13926
   130
by (simp add: subset_insertI)
paulson@13926
   131
paulson@13926
   132
text{*Spy sees what is sent on the traffic*}
paulson@13926
   133
lemma Says_imp_knows_Spy [rule_format]:
paulson@13926
   134
     "Says A B X \<in> set evs --> 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
lemma Notes_imp_knows_Spy [rule_format]:
paulson@13926
   140
     "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
paulson@13926
   141
apply (induct_tac "evs")
paulson@13926
   142
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   143
done
paulson@13926
   144
paulson@13926
   145
paulson@13926
   146
text{*Elimination rules: derive contradictions from old Says events containing
paulson@13926
   147
  items known to be fresh*}
paulson@13926
   148
lemmas knows_Spy_partsEs =
paulson@13926
   149
     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
paulson@13926
   150
     parts.Body [THEN revcut_rl, standard]
paulson@13926
   151
paulson@13926
   152
text{*Compatibility for the old "spies" function*}
paulson@13926
   153
lemmas spies_partsEs = knows_Spy_partsEs
paulson@13926
   154
lemmas Says_imp_spies = Says_imp_knows_Spy
paulson@13926
   155
lemmas parts_insert_spies = parts_insert_knows_Spy
paulson@13926
   156
paulson@13926
   157
paulson@13926
   158
subsection{*Knowledge of Agents*}
paulson@13926
   159
paulson@13926
   160
lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
paulson@13926
   161
by simp
paulson@13926
   162
paulson@13926
   163
lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
paulson@13926
   164
by simp
paulson@13926
   165
paulson@13926
   166
lemma knows_Gets:
paulson@13926
   167
     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
paulson@13926
   168
by simp
paulson@13926
   169
paulson@13926
   170
paulson@13926
   171
lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A' B X # evs)"
paulson@13926
   172
apply (simp add: subset_insertI)
paulson@13926
   173
done
paulson@13926
   174
paulson@13926
   175
lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A' X # evs)"
paulson@13926
   176
apply (simp add: subset_insertI)
paulson@13926
   177
done
paulson@13926
   178
paulson@13926
   179
lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A' X # evs)"
paulson@13926
   180
apply (simp add: subset_insertI)
paulson@13926
   181
done
paulson@13926
   182
paulson@13926
   183
text{*Agents know what they say*}
paulson@13926
   184
lemma Says_imp_knows [rule_format]: "Says A B 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 note*}
paulson@13926
   191
lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
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{*Agents know what they receive*}
paulson@13926
   198
lemma Gets_imp_knows_agents [rule_format]:
paulson@13926
   199
     "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
paulson@13926
   200
apply (induct_tac "evs")
paulson@13926
   201
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   202
done
paulson@13926
   203
paulson@13926
   204
paulson@13926
   205
text{*What agents DIFFERENT FROM Spy know 
paulson@13926
   206
  was either said, or noted, or got, or known initially*}
paulson@13926
   207
lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
paulson@13926
   208
     "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.  
paulson@13926
   209
  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
   210
apply (erule rev_mp)
paulson@13926
   211
apply (induct_tac "evs")
paulson@13926
   212
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   213
apply blast
paulson@13926
   214
done
paulson@13926
   215
paulson@13926
   216
text{*What the Spy knows -- for the time being --
paulson@13926
   217
  was either said or noted, or known initially*}
paulson@13926
   218
lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
paulson@13926
   219
     "[| X \<in> knows Spy evs |] ==> EX A B.  
paulson@13926
   220
  Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
paulson@13926
   221
apply (erule rev_mp)
paulson@13926
   222
apply (induct_tac "evs")
paulson@13926
   223
apply (simp_all (no_asm_simp) split add: event.split)
paulson@13926
   224
apply blast
paulson@13926
   225
done
paulson@13926
   226
paulson@13926
   227
paulson@13926
   228
paulson@13926
   229
paulson@13926
   230
text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
paulson@13926
   231
declare knows_Cons [simp del]
paulson@13926
   232
paulson@13926
   233
paulson@13926
   234
subsection{*Fresh Nonces*}
paulson@13926
   235
paulson@13926
   236
lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs"
paulson@13926
   237
apply (induct_tac "evs")
paulson@13926
   238
apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
paulson@13926
   239
apply blast+
paulson@13926
   240
done
paulson@13926
   241
paulson@13926
   242
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
paulson@13926
   243
paulson@13926
   244
lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
paulson@13926
   245
apply (induct_tac "evs")
paulson@13926
   246
apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split)
paulson@13926
   247
apply blast
paulson@13926
   248
done
paulson@13926
   249
paulson@13926
   250
lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
paulson@13926
   251
by simp
paulson@13926
   252
paulson@13926
   253
lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
paulson@13926
   254
by simp
paulson@13926
   255
paulson@13926
   256
lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
paulson@13926
   257
by simp
paulson@13926
   258
paulson@13926
   259
lemma used_nil_subset: "used [] <= used evs"
paulson@13926
   260
apply (simp)
paulson@13926
   261
apply (blast intro: initState_into_used)
paulson@13926
   262
done
paulson@13926
   263
paulson@13926
   264
text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
paulson@13926
   265
declare used_Nil [simp del] used_Cons [simp del]
paulson@13926
   266
paulson@13926
   267
paulson@13926
   268
text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
paulson@13926
   269
  New events added by induction to "evs" are discarded.  Provided 
paulson@13926
   270
  this information isn't needed, the proof will be much shorter, since
paulson@13926
   271
  it will omit complicated reasoning about @{term analz}.*}
paulson@13926
   272
paulson@13926
   273
lemmas analz_mono_contra =
paulson@13926
   274
       knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
paulson@13926
   275
       knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
paulson@13926
   276
       knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
paulson@13926
   277
paulson@13926
   278
ML
paulson@13926
   279
{*
paulson@13926
   280
val analz_mono_contra_tac = 
paulson@13926
   281
  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
paulson@13926
   282
  in
paulson@13926
   283
    rtac analz_impI THEN' 
paulson@13926
   284
    REPEAT1 o 
paulson@13926
   285
      (dresolve_tac (thms"analz_mono_contra"))
paulson@13926
   286
    THEN' mp_tac
paulson@13926
   287
  end
paulson@13926
   288
*}
paulson@13926
   289
paulson@11104
   290
paulson@13922
   291
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
paulson@13922
   292
by (induct e, auto simp: knows_Cons)
paulson@13922
   293
paulson@13922
   294
lemma initState_subset_knows: "initState A <= knows A evs"
paulson@13926
   295
apply (induct_tac evs, simp) 
paulson@13922
   296
apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
paulson@13922
   297
done
paulson@13922
   298
paulson@13922
   299
paulson@13926
   300
text{*For proving @{text new_keys_not_used}*}
paulson@13922
   301
lemma keysFor_parts_insert:
paulson@13926
   302
     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
paulson@13926
   303
      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
paulson@13922
   304
by (force 
paulson@13922
   305
    dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
paulson@13922
   306
           analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
paulson@13922
   307
    intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
paulson@13922
   308
paulson@11104
   309
method_setup analz_mono_contra = {*
paulson@11104
   310
    Method.no_args
paulson@11104
   311
      (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
paulson@13922
   312
    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
paulson@13922
   313
paulson@13922
   314
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
paulson@13922
   315
paulson@13922
   316
ML
paulson@13922
   317
{*
paulson@13926
   318
val knows_Cons     = thm "knows_Cons"
paulson@13926
   319
val used_Nil       = thm "used_Nil"
paulson@13926
   320
val used_Cons      = thm "used_Cons"
paulson@13926
   321
paulson@13926
   322
val Notes_imp_used = thm "Notes_imp_used";
paulson@13926
   323
val Says_imp_used = thm "Says_imp_used";
paulson@13926
   324
val MPair_used = thm "MPair_used";
paulson@13926
   325
val parts_insert_knows_Spy = thm "parts_insert_knows_Spy";
paulson@13926
   326
val knows_Spy_Says = thm "knows_Spy_Says";
paulson@13926
   327
val knows_Spy_Notes = thm "knows_Spy_Notes";
paulson@13926
   328
val knows_Spy_Gets = thm "knows_Spy_Gets";
paulson@13926
   329
val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
paulson@13926
   330
val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
paulson@13926
   331
val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
paulson@13926
   332
val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
paulson@13926
   333
val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
paulson@13926
   334
val knows_Spy_partsEs = thms "knows_Spy_partsEs";
paulson@13926
   335
val spies_partsEs = thms "spies_partsEs";
paulson@13926
   336
val Says_imp_spies = thm "Says_imp_spies";
paulson@13926
   337
val parts_insert_spies = thm "parts_insert_spies";
paulson@13926
   338
val knows_Says = thm "knows_Says";
paulson@13926
   339
val knows_Notes = thm "knows_Notes";
paulson@13926
   340
val knows_Gets = thm "knows_Gets";
paulson@13926
   341
val knows_subset_knows_Says = thm "knows_subset_knows_Says";
paulson@13926
   342
val knows_subset_knows_Notes = thm "knows_subset_knows_Notes";
paulson@13926
   343
val knows_subset_knows_Gets = thm "knows_subset_knows_Gets";
paulson@13926
   344
val Says_imp_knows = thm "Says_imp_knows";
paulson@13926
   345
val Notes_imp_knows = thm "Notes_imp_knows";
paulson@13926
   346
val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
paulson@13926
   347
val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
paulson@13926
   348
val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
paulson@13926
   349
val parts_knows_Spy_subset_used = thm "parts_knows_Spy_subset_used";
paulson@13926
   350
val usedI = thm "usedI";
paulson@13926
   351
val initState_into_used = thm "initState_into_used";
paulson@13926
   352
val used_Says = thm "used_Says";
paulson@13926
   353
val used_Notes = thm "used_Notes";
paulson@13926
   354
val used_Gets = thm "used_Gets";
paulson@13926
   355
val used_nil_subset = thm "used_nil_subset";
paulson@13926
   356
val analz_mono_contra = thms "analz_mono_contra";
paulson@13926
   357
val knows_subset_knows_Cons = thm "knows_subset_knows_Cons";
paulson@13926
   358
val initState_subset_knows = thm "initState_subset_knows";
paulson@13926
   359
val keysFor_parts_insert = thm "keysFor_parts_insert";
paulson@13926
   360
paulson@13926
   361
paulson@13922
   362
val synth_analz_mono = thm "synth_analz_mono";
paulson@13922
   363
paulson@13922
   364
val synth_analz_mono_contra_tac = 
paulson@13926
   365
  let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
paulson@13922
   366
  in
paulson@13922
   367
    rtac syan_impI THEN' 
paulson@13922
   368
    REPEAT1 o 
paulson@13922
   369
      (dresolve_tac 
paulson@13922
   370
       [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
paulson@13922
   371
        knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
paulson@13922
   372
	knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
paulson@13922
   373
    THEN'
paulson@13922
   374
    mp_tac
paulson@13922
   375
  end;
paulson@13922
   376
*}
paulson@13922
   377
paulson@13922
   378
method_setup synth_analz_mono_contra = {*
paulson@13922
   379
    Method.no_args
paulson@13922
   380
      (Method.METHOD (fn facts => REPEAT_FIRST synth_analz_mono_contra_tac)) *}
paulson@13922
   381
    "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
paulson@3512
   382
paulson@3512
   383
end