src/Doc/Tutorial/Protocol/Event.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 55142 378ae9e46175
child 58889 5b7a9633cfa8
permissions -rw-r--r--
eliminated spurious semicolons;
wenzelm@49322
     1
(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11250
     2
    Copyright   1996  University of Cambridge
paulson@11250
     3
paulson@11250
     4
Datatype of events; function "spies"; freshness
paulson@11250
     5
paulson@11250
     6
"bad" agents have been broken by the Spy; their private keys and internal
paulson@11250
     7
    stores are visible to him
berghofe@23925
     8
*)(*<*)
paulson@11250
     9
berghofe@23925
    10
header{*Theory of Events for Security Protocols*}
berghofe@23925
    11
berghofe@23925
    12
theory Event imports Message begin
paulson@11250
    13
paulson@11250
    14
consts  (*Initial states of agents -- parameter of the construction*)
paulson@11250
    15
  initState :: "agent => msg set"
paulson@11250
    16
paulson@11250
    17
datatype
paulson@11250
    18
  event = Says  agent agent msg
paulson@11250
    19
        | Gets  agent       msg
paulson@11250
    20
        | Notes agent       msg
paulson@11250
    21
       
paulson@11250
    22
consts 
wenzelm@32960
    23
  bad    :: "agent set"                         -- {* compromised agents *}
paulson@11250
    24
paulson@11250
    25
berghofe@23925
    26
text{*The constant "spies" is retained for compatibility's sake*}
berghofe@23925
    27
paulson@11250
    28
primrec
haftmann@39795
    29
  knows :: "agent => event list => msg set"
haftmann@39795
    30
where
paulson@11250
    31
  knows_Nil:   "knows A [] = initState A"
haftmann@39795
    32
| knows_Cons:
paulson@11250
    33
    "knows A (ev # evs) =
paulson@11250
    34
       (if A = Spy then 
wenzelm@32960
    35
        (case ev of
wenzelm@32960
    36
           Says A' B X => insert X (knows Spy evs)
wenzelm@32960
    37
         | Gets A' X => knows Spy evs
wenzelm@32960
    38
         | Notes A' X  => 
wenzelm@32960
    39
             if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
wenzelm@32960
    40
        else
wenzelm@32960
    41
        (case ev of
wenzelm@32960
    42
           Says A' B X => 
wenzelm@32960
    43
             if A'=A then insert X (knows A evs) else knows A evs
wenzelm@32960
    44
         | Gets A' X    => 
wenzelm@32960
    45
             if A'=A then insert X (knows A evs) else knows A evs
wenzelm@32960
    46
         | Notes A' X    => 
wenzelm@32960
    47
             if A'=A then insert X (knows A evs) else knows A evs))"
paulson@11250
    48
haftmann@39795
    49
abbreviation (input)
haftmann@39795
    50
  spies  :: "event list => msg set" where
haftmann@39795
    51
  "spies == knows Spy"
haftmann@39795
    52
haftmann@39795
    53
text{*Spy has access to his own key for spoof messages, but Server is secure*}
haftmann@39795
    54
specification (bad)
haftmann@39795
    55
  Spy_in_bad     [iff]: "Spy \<in> bad"
haftmann@39795
    56
  Server_not_bad [iff]: "Server \<notin> bad"
haftmann@39795
    57
    by (rule exI [of _ "{Spy}"], simp)
haftmann@39795
    58
paulson@11250
    59
(*
paulson@11250
    60
  Case A=Spy on the Gets event
paulson@11250
    61
  enforces the fact that if a message is received then it must have been sent,
paulson@11250
    62
  therefore the oops case must use Notes
paulson@11250
    63
*)
paulson@11250
    64
haftmann@39795
    65
primrec
paulson@11250
    66
  (*Set of items that might be visible to somebody:
paulson@11250
    67
    complement of the set of fresh items*)
paulson@11250
    68
  used :: "event list => msg set"
haftmann@39795
    69
where
paulson@11250
    70
  used_Nil:   "used []         = (UN B. parts (initState B))"
haftmann@39795
    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)"
berghofe@23925
    76
    --{*The case for @{term Gets} seems anomalous, but @{term Gets} always
berghofe@23925
    77
        follows @{term Says} in real protocols.  Seems difficult to change.
berghofe@23925
    78
        See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}
berghofe@23925
    79
berghofe@23925
    80
lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
berghofe@23925
    81
apply (induct_tac evs)
berghofe@23925
    82
apply (auto split: event.split) 
berghofe@23925
    83
done
berghofe@23925
    84
berghofe@23925
    85
lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs"
berghofe@23925
    86
apply (induct_tac evs)
berghofe@23925
    87
apply (auto split: event.split) 
berghofe@23925
    88
done
berghofe@23925
    89
berghofe@23925
    90
berghofe@23925
    91
subsection{*Function @{term knows}*}
berghofe@23925
    92
berghofe@23925
    93
(*Simplifying   
berghofe@23925
    94
 parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
berghofe@23925
    95
  This version won't loop with the simplifier.*)
wenzelm@55142
    96
lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
berghofe@23925
    97
berghofe@23925
    98
lemma knows_Spy_Says [simp]:
berghofe@23925
    99
     "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
berghofe@23925
   100
by simp
berghofe@23925
   101
berghofe@23925
   102
text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
berghofe@23925
   103
      on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
berghofe@23925
   104
lemma knows_Spy_Notes [simp]:
berghofe@23925
   105
     "knows Spy (Notes A X # evs) =  
berghofe@23925
   106
          (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
berghofe@23925
   107
by simp
berghofe@23925
   108
berghofe@23925
   109
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
berghofe@23925
   110
by simp
berghofe@23925
   111
berghofe@23925
   112
lemma knows_Spy_subset_knows_Spy_Says:
berghofe@23925
   113
     "knows Spy evs \<subseteq> knows Spy (Says A B X # evs)"
berghofe@23925
   114
by (simp add: subset_insertI)
berghofe@23925
   115
berghofe@23925
   116
lemma knows_Spy_subset_knows_Spy_Notes:
berghofe@23925
   117
     "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)"
berghofe@23925
   118
by force
berghofe@23925
   119
berghofe@23925
   120
lemma knows_Spy_subset_knows_Spy_Gets:
berghofe@23925
   121
     "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)"
berghofe@23925
   122
by (simp add: subset_insertI)
berghofe@23925
   123
berghofe@23925
   124
text{*Spy sees what is sent on the traffic*}
berghofe@23925
   125
lemma Says_imp_knows_Spy [rule_format]:
berghofe@23925
   126
     "Says A B X \<in> set evs --> X \<in> knows Spy evs"
berghofe@23925
   127
apply (induct_tac "evs")
berghofe@23925
   128
apply (simp_all (no_asm_simp) split add: event.split)
berghofe@23925
   129
done
berghofe@23925
   130
berghofe@23925
   131
lemma Notes_imp_knows_Spy [rule_format]:
berghofe@23925
   132
     "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
berghofe@23925
   133
apply (induct_tac "evs")
berghofe@23925
   134
apply (simp_all (no_asm_simp) split add: event.split)
berghofe@23925
   135
done
berghofe@23925
   136
berghofe@23925
   137
berghofe@23925
   138
text{*Elimination rules: derive contradictions from old Says events containing
berghofe@23925
   139
  items known to be fresh*}
berghofe@23925
   140
lemmas knows_Spy_partsEs =
wenzelm@46471
   141
     Says_imp_knows_Spy [THEN parts.Inj, elim_format] 
wenzelm@46471
   142
     parts.Body [elim_format]
berghofe@23925
   143
berghofe@23925
   144
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
berghofe@23925
   145
berghofe@23925
   146
text{*Compatibility for the old "spies" function*}
berghofe@23925
   147
lemmas spies_partsEs = knows_Spy_partsEs
berghofe@23925
   148
lemmas Says_imp_spies = Says_imp_knows_Spy
berghofe@23925
   149
lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy]
berghofe@23925
   150
berghofe@23925
   151
berghofe@23925
   152
subsection{*Knowledge of Agents*}
berghofe@23925
   153
berghofe@23925
   154
lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
berghofe@23925
   155
by simp
berghofe@23925
   156
berghofe@23925
   157
lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
berghofe@23925
   158
by simp
berghofe@23925
   159
berghofe@23925
   160
lemma knows_Gets:
berghofe@23925
   161
     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
berghofe@23925
   162
by simp
berghofe@23925
   163
berghofe@23925
   164
berghofe@23925
   165
lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
berghofe@23925
   166
by (simp add: subset_insertI)
berghofe@23925
   167
berghofe@23925
   168
lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)"
berghofe@23925
   169
by (simp add: subset_insertI)
berghofe@23925
   170
berghofe@23925
   171
lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)"
berghofe@23925
   172
by (simp add: subset_insertI)
berghofe@23925
   173
berghofe@23925
   174
text{*Agents know what they say*}
berghofe@23925
   175
lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
berghofe@23925
   176
apply (induct_tac "evs")
berghofe@23925
   177
apply (simp_all (no_asm_simp) split add: event.split)
berghofe@23925
   178
apply blast
berghofe@23925
   179
done
berghofe@23925
   180
berghofe@23925
   181
text{*Agents know what they note*}
berghofe@23925
   182
lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
berghofe@23925
   183
apply (induct_tac "evs")
berghofe@23925
   184
apply (simp_all (no_asm_simp) split add: event.split)
berghofe@23925
   185
apply blast
berghofe@23925
   186
done
berghofe@23925
   187
berghofe@23925
   188
text{*Agents know what they receive*}
berghofe@23925
   189
lemma Gets_imp_knows_agents [rule_format]:
berghofe@23925
   190
     "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
berghofe@23925
   191
apply (induct_tac "evs")
berghofe@23925
   192
apply (simp_all (no_asm_simp) split add: event.split)
berghofe@23925
   193
done
paulson@11250
   194
paulson@11250
   195
berghofe@23925
   196
text{*What agents DIFFERENT FROM Spy know 
berghofe@23925
   197
  was either said, or noted, or got, or known initially*}
berghofe@23925
   198
lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
berghofe@23925
   199
     "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.  
berghofe@23925
   200
  Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
berghofe@23925
   201
apply (erule rev_mp)
berghofe@23925
   202
apply (induct_tac "evs")
berghofe@23925
   203
apply (simp_all (no_asm_simp) split add: event.split)
berghofe@23925
   204
apply blast
berghofe@23925
   205
done
berghofe@23925
   206
berghofe@23925
   207
text{*What the Spy knows -- for the time being --
berghofe@23925
   208
  was either said or noted, or known initially*}
berghofe@23925
   209
lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
berghofe@23925
   210
     "[| X \<in> knows Spy evs |] ==> EX A B.  
berghofe@23925
   211
  Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
berghofe@23925
   212
apply (erule rev_mp)
berghofe@23925
   213
apply (induct_tac "evs")
berghofe@23925
   214
apply (simp_all (no_asm_simp) split add: event.split)
berghofe@23925
   215
apply blast
berghofe@23925
   216
done
berghofe@23925
   217
berghofe@23925
   218
lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
berghofe@23925
   219
apply (induct_tac "evs", force)  
berghofe@23925
   220
apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) 
berghofe@23925
   221
done
berghofe@23925
   222
berghofe@23925
   223
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
berghofe@23925
   224
berghofe@23925
   225
lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
berghofe@23925
   226
apply (induct_tac "evs")
berghofe@23925
   227
apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
berghofe@23925
   228
done
berghofe@23925
   229
berghofe@23925
   230
lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
berghofe@23925
   231
by simp
berghofe@23925
   232
berghofe@23925
   233
lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
berghofe@23925
   234
by simp
berghofe@23925
   235
berghofe@23925
   236
lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
berghofe@23925
   237
by simp
berghofe@23925
   238
berghofe@23925
   239
lemma used_nil_subset: "used [] \<subseteq> used evs"
berghofe@23925
   240
apply simp
berghofe@23925
   241
apply (blast intro: initState_into_used)
berghofe@23925
   242
done
berghofe@23925
   243
berghofe@23925
   244
text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
berghofe@23925
   245
declare knows_Cons [simp del]
berghofe@23925
   246
        used_Nil [simp del] used_Cons [simp del]
berghofe@23925
   247
berghofe@23925
   248
berghofe@23925
   249
text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
berghofe@23925
   250
  New events added by induction to "evs" are discarded.  Provided 
berghofe@23925
   251
  this information isn't needed, the proof will be much shorter, since
berghofe@23925
   252
  it will omit complicated reasoning about @{term analz}.*}
berghofe@23925
   253
berghofe@23925
   254
lemmas analz_mono_contra =
berghofe@23925
   255
       knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
berghofe@23925
   256
       knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
berghofe@23925
   257
       knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
berghofe@23925
   258
wenzelm@55142
   259
lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
wenzelm@27225
   260
berghofe@23925
   261
ML
berghofe@23925
   262
{*
berghofe@23925
   263
val analz_mono_contra_tac = 
wenzelm@27225
   264
  rtac @{thm analz_impI} THEN' 
wenzelm@27225
   265
  REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
wenzelm@27225
   266
  THEN' mp_tac
berghofe@23925
   267
*}
berghofe@23925
   268
berghofe@23925
   269
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
berghofe@23925
   270
by (induct e, auto simp: knows_Cons)
berghofe@23925
   271
berghofe@23925
   272
lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
berghofe@23925
   273
apply (induct_tac evs, simp) 
berghofe@23925
   274
apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
berghofe@23925
   275
done
berghofe@23925
   276
berghofe@23925
   277
berghofe@23925
   278
text{*For proving @{text new_keys_not_used}*}
berghofe@23925
   279
lemma keysFor_parts_insert:
berghofe@23925
   280
     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
wenzelm@58860
   281
      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H" 
berghofe@23925
   282
by (force 
berghofe@23925
   283
    dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
berghofe@23925
   284
           analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
berghofe@23925
   285
    intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
paulson@11250
   286
paulson@11250
   287
method_setup analz_mono_contra = {*
wenzelm@30548
   288
    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
paulson@11250
   289
    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
paulson@11250
   290
berghofe@23925
   291
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
berghofe@23925
   292
wenzelm@55142
   293
lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
wenzelm@27225
   294
berghofe@23925
   295
ML
berghofe@23925
   296
{*
wenzelm@39282
   297
val knows_Cons = @{thm knows_Cons};
wenzelm@39282
   298
val used_Nil = @{thm used_Nil};
wenzelm@39282
   299
val used_Cons = @{thm used_Cons};
berghofe@23925
   300
wenzelm@39282
   301
val Notes_imp_used = @{thm Notes_imp_used};
wenzelm@39282
   302
val Says_imp_used = @{thm Says_imp_used};
wenzelm@39282
   303
val Says_imp_knows_Spy = @{thm Says_imp_knows_Spy};
wenzelm@39282
   304
val Notes_imp_knows_Spy = @{thm Notes_imp_knows_Spy};
wenzelm@39282
   305
val knows_Spy_partsEs = @{thms knows_Spy_partsEs};
wenzelm@39282
   306
val spies_partsEs = @{thms spies_partsEs};
wenzelm@39282
   307
val Says_imp_spies = @{thm Says_imp_spies};
wenzelm@39282
   308
val parts_insert_spies = @{thm parts_insert_spies};
wenzelm@39282
   309
val Says_imp_knows = @{thm Says_imp_knows};
wenzelm@39282
   310
val Notes_imp_knows = @{thm Notes_imp_knows};
wenzelm@39282
   311
val Gets_imp_knows_agents = @{thm Gets_imp_knows_agents};
wenzelm@39282
   312
val knows_imp_Says_Gets_Notes_initState = @{thm knows_imp_Says_Gets_Notes_initState};
wenzelm@39282
   313
val knows_Spy_imp_Says_Notes_initState = @{thm knows_Spy_imp_Says_Notes_initState};
wenzelm@39282
   314
val usedI = @{thm usedI};
wenzelm@39282
   315
val initState_into_used = @{thm initState_into_used};
wenzelm@39282
   316
val used_Says = @{thm used_Says};
wenzelm@39282
   317
val used_Notes = @{thm used_Notes};
wenzelm@39282
   318
val used_Gets = @{thm used_Gets};
wenzelm@39282
   319
val used_nil_subset = @{thm used_nil_subset};
wenzelm@39282
   320
val analz_mono_contra = @{thms analz_mono_contra};
wenzelm@39282
   321
val knows_subset_knows_Cons = @{thm knows_subset_knows_Cons};
wenzelm@39282
   322
val initState_subset_knows = @{thm initState_subset_knows};
wenzelm@39282
   323
val keysFor_parts_insert = @{thm keysFor_parts_insert};
berghofe@23925
   324
berghofe@23925
   325
wenzelm@39282
   326
val synth_analz_mono = @{thm synth_analz_mono};
berghofe@23925
   327
wenzelm@39282
   328
val knows_Spy_subset_knows_Spy_Says = @{thm knows_Spy_subset_knows_Spy_Says};
wenzelm@39282
   329
val knows_Spy_subset_knows_Spy_Notes = @{thm knows_Spy_subset_knows_Spy_Notes};
wenzelm@39282
   330
val knows_Spy_subset_knows_Spy_Gets = @{thm knows_Spy_subset_knows_Spy_Gets};
berghofe@23925
   331
berghofe@23925
   332
berghofe@23925
   333
val synth_analz_mono_contra_tac = 
wenzelm@27225
   334
  rtac @{thm syan_impI} THEN'
wenzelm@27225
   335
  REPEAT1 o 
wenzelm@27225
   336
    (dresolve_tac 
wenzelm@27225
   337
     [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
wenzelm@27225
   338
      @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
wenzelm@27225
   339
      @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
wenzelm@27225
   340
  THEN'
wenzelm@27225
   341
  mp_tac
berghofe@23925
   342
*}
berghofe@23925
   343
berghofe@23925
   344
method_setup synth_analz_mono_contra = {*
wenzelm@30548
   345
    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
berghofe@23925
   346
    "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
berghofe@23925
   347
(*>*)
berghofe@23925
   348
berghofe@23925
   349
section{* Event Traces \label{sec:events} *}
berghofe@23925
   350
berghofe@23925
   351
text {*
berghofe@23925
   352
The system's behaviour is formalized as a set of traces of
berghofe@23925
   353
\emph{events}.  The most important event, @{text "Says A B X"}, expresses
berghofe@23925
   354
$A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$.
berghofe@23925
   355
A trace is simply a list, constructed in reverse
berghofe@23925
   356
using~@{text "#"}.  Other event types include reception of messages (when
berghofe@23925
   357
we want to make it explicit) and an agent's storing a fact.
berghofe@23925
   358
berghofe@23925
   359
Sometimes the protocol requires an agent to generate a new nonce. The
berghofe@23925
   360
probability that a 20-byte random number has appeared before is effectively
berghofe@23925
   361
zero.  To formalize this important property, the set @{term "used evs"}
berghofe@23925
   362
denotes the set of all items mentioned in the trace~@{text evs}.
berghofe@23925
   363
The function @{text used} has a straightforward
berghofe@23925
   364
recursive definition.  Here is the case for @{text Says} event:
berghofe@23925
   365
@{thm [display,indent=5] used_Says [no_vars]}
berghofe@23925
   366
berghofe@23925
   367
The function @{text knows} formalizes an agent's knowledge.  Mostly we only
berghofe@23925
   368
care about the spy's knowledge, and @{term "knows Spy evs"} is the set of items
berghofe@23925
   369
available to the spy in the trace~@{text evs}.  Already in the empty trace,
berghofe@23925
   370
the spy starts with some secrets at his disposal, such as the private keys
berghofe@23925
   371
of compromised users.  After each @{text Says} event, the spy learns the
berghofe@23925
   372
message that was sent:
berghofe@23925
   373
@{thm [display,indent=5] knows_Spy_Says [no_vars]}
berghofe@23925
   374
Combinations of functions express other important
berghofe@23925
   375
sets of messages derived from~@{text evs}:
berghofe@23925
   376
\begin{itemize}
berghofe@23925
   377
\item @{term "analz (knows Spy evs)"} is everything that the spy could
berghofe@23925
   378
learn by decryption
berghofe@23925
   379
\item @{term "synth (analz (knows Spy evs))"} is everything that the spy
berghofe@23925
   380
could generate
berghofe@23925
   381
\end{itemize}
berghofe@23925
   382
*}
berghofe@23925
   383
berghofe@23925
   384
(*<*)
paulson@11250
   385
end
berghofe@23925
   386
(*>*)