src/HOL/Auth/Smartcard/EventSC.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58860 fee7cfa69c50
child 61830 4f5ab843cf5b
permissions -rw-r--r--
modernized header uniformly as section;
wenzelm@58889
     1
section{*Theory of Events for Security Protocols that use smartcards*}
paulson@18886
     2
noschinl@53428
     3
theory EventSC
noschinl@53428
     4
imports
noschinl@53428
     5
  "../Message"
noschinl@53428
     6
  "~~/src/HOL/Library/Simps_Case_Conv"
noschinl@53428
     7
begin
paulson@18886
     8
paulson@18886
     9
consts  (*Initial states of agents -- parameter of the construction*)
paulson@18886
    10
  initState :: "agent => msg set"
paulson@18886
    11
blanchet@58310
    12
datatype card = Card agent
paulson@18886
    13
paulson@18886
    14
text{*Four new events express the traffic between an agent and his card*}
blanchet@58310
    15
datatype  
paulson@18886
    16
  event = Says  agent agent msg
paulson@18886
    17
        | Notes agent       msg
paulson@18886
    18
        | Gets  agent       msg
paulson@18886
    19
        | Inputs agent card msg (*Agent sends to card and\<dots>*)
paulson@18886
    20
        | C_Gets card       msg (*\<dots> card receives it*) 
paulson@18886
    21
        | Outpts card agent msg (*Card sends to agent and\<dots>*)
paulson@18886
    22
        | A_Gets agent      msg (*agent receives it*)
paulson@18886
    23
    
paulson@18886
    24
consts 
paulson@18886
    25
 bad     :: "agent set"  (*compromised agents*)
paulson@18886
    26
 stolen    :: "card set" (* stolen smart cards *)
paulson@18886
    27
 cloned  :: "card set"   (* cloned smart cards*)
paulson@18886
    28
 secureM :: "bool"(*assumption of secure means between agents and their cards*)
paulson@18886
    29
wenzelm@20768
    30
abbreviation
wenzelm@21404
    31
  insecureM :: bool where (*certain protocols make no assumption of secure means*)
wenzelm@20768
    32
  "insecureM == \<not>secureM"
paulson@18886
    33
paulson@18886
    34
paulson@18886
    35
text{*Spy has access to his own key for spoof messages, but Server is secure*}
paulson@18886
    36
specification (bad)
paulson@18886
    37
  Spy_in_bad     [iff]: "Spy \<in> bad"
paulson@18886
    38
  Server_not_bad [iff]: "Server \<notin> bad"
paulson@18886
    39
  apply (rule exI [of _ "{Spy}"], simp) done
paulson@18886
    40
paulson@18886
    41
specification (stolen)
paulson@18886
    42
  (*The server's card is secure by assumption\<dots>*)
paulson@18886
    43
  Card_Server_not_stolen [iff]: "Card Server \<notin> stolen"
wenzelm@32960
    44
  Card_Spy_not_stolen    [iff]: "Card Spy \<notin> stolen"
paulson@18886
    45
  apply blast done
paulson@18886
    46
paulson@18886
    47
specification (cloned)
paulson@18886
    48
  (*\<dots> the spy's card is secure because she already can use it freely*)
paulson@18886
    49
  Card_Server_not_cloned [iff]: "Card Server \<notin> cloned"
wenzelm@32960
    50
  Card_Spy_not_cloned    [iff]: "Card Spy \<notin> cloned"
paulson@18886
    51
  apply blast done
paulson@18886
    52
paulson@18886
    53
primrec (*This definition is extended over the new events, subject to the 
paulson@18886
    54
          assumption of secure means*)
haftmann@39246
    55
  knows   :: "agent => event list => msg set" (*agents' knowledge*) where
haftmann@39246
    56
  knows_Nil:   "knows A [] = initState A" |
paulson@18886
    57
  knows_Cons:  "knows A (ev # evs) =
wenzelm@32960
    58
         (case ev of
wenzelm@32960
    59
            Says A' B X => 
paulson@18886
    60
                if (A=A' | A=Spy) then insert X (knows A evs) else knows A evs
wenzelm@32960
    61
          | Notes A' X  => 
wenzelm@32960
    62
                if (A=A' | (A=Spy & A'\<in>bad)) then insert X (knows A evs) 
paulson@18886
    63
                                             else knows A evs 
paulson@18886
    64
          | Gets A' X   =>
wenzelm@32960
    65
                if (A=A' & A \<noteq> Spy) then insert X (knows A evs) 
paulson@18886
    66
                                     else knows A evs
paulson@18886
    67
          | Inputs A' C X =>
wenzelm@32960
    68
              if secureM then
paulson@18886
    69
                if A=A' then insert X (knows A evs) else knows A evs
wenzelm@32960
    70
              else
wenzelm@32960
    71
                if (A=A' | A=Spy) then insert X (knows A evs) else knows A evs
paulson@18886
    72
          | C_Gets C X   => knows A evs
paulson@18886
    73
          | Outpts C A' X =>
wenzelm@32960
    74
              if secureM then
paulson@18886
    75
                if A=A' then insert X (knows A evs) else knows A evs
paulson@18886
    76
              else
wenzelm@32960
    77
                if A=Spy then insert X (knows A evs) else knows A evs
paulson@18886
    78
          | A_Gets A' X   =>
wenzelm@32960
    79
                if (A=A' & A \<noteq> Spy) then insert X (knows A evs) 
paulson@18886
    80
                                     else knows A evs)"
paulson@18886
    81
paulson@18886
    82
paulson@18886
    83
haftmann@39246
    84
primrec
paulson@18886
    85
  (*The set of items that might be visible to someone is easily extended 
paulson@18886
    86
    over the new events*)
haftmann@39246
    87
  used :: "event list => msg set" where
haftmann@39246
    88
  used_Nil:   "used []         = (UN B. parts (initState B))" |
paulson@18886
    89
  used_Cons:  "used (ev # evs) =
wenzelm@32960
    90
                 (case ev of
wenzelm@32960
    91
                    Says A B X => parts {X} \<union> (used evs)
wenzelm@32960
    92
                  | Notes A X  => parts {X} \<union> (used evs)
wenzelm@32960
    93
                  | Gets A X   => used evs
paulson@18886
    94
                  | Inputs A C X  => parts{X} \<union> (used evs) 
wenzelm@32960
    95
                  | C_Gets C X   => used evs
paulson@18886
    96
                  | Outpts C A X  => parts{X} \<union> (used evs)
wenzelm@32960
    97
                  | A_Gets A X   => used evs)"
paulson@18886
    98
    --{*@{term Gets} always follows @{term Says} in real protocols. 
paulson@18886
    99
       Likewise, @{term C_Gets} will always have to follow @{term Inputs}
paulson@18886
   100
       and @{term A_Gets} will always have to follow @{term Outpts}*}
paulson@18886
   101
paulson@18886
   102
lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> used evs"
paulson@18886
   103
apply (induct_tac evs)
paulson@18886
   104
apply (auto split: event.split) 
paulson@18886
   105
done
paulson@18886
   106
paulson@18886
   107
lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> used evs"
paulson@18886
   108
apply (induct_tac evs)
paulson@18886
   109
apply (auto split: event.split) 
paulson@18886
   110
done
paulson@18886
   111
paulson@18886
   112
lemma MPair_used [rule_format]:
paulson@18886
   113
     "MPair X Y \<in> used evs \<longrightarrow> X \<in> used evs & Y \<in> used evs"
paulson@18886
   114
apply (induct_tac evs)
paulson@18886
   115
apply (auto split: event.split) 
paulson@18886
   116
done
paulson@18886
   117
paulson@18886
   118
paulson@18886
   119
subsection{*Function @{term knows}*}
paulson@18886
   120
paulson@18886
   121
(*Simplifying   
paulson@18886
   122
 parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
paulson@18886
   123
  This version won't loop with the simplifier.*)
wenzelm@45605
   124
lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
paulson@18886
   125
paulson@18886
   126
lemma knows_Spy_Says [simp]:
paulson@18886
   127
     "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
paulson@18886
   128
by simp
paulson@18886
   129
paulson@18886
   130
text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
paulson@18886
   131
      on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
paulson@18886
   132
lemma knows_Spy_Notes [simp]:
paulson@18886
   133
     "knows Spy (Notes A X # evs) =  
paulson@18886
   134
          (if A\<in>bad then insert X (knows Spy evs) else knows Spy evs)"
paulson@18886
   135
by simp
paulson@18886
   136
paulson@18886
   137
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
paulson@18886
   138
by simp
paulson@18886
   139
paulson@18886
   140
lemma knows_Spy_Inputs_secureM [simp]: 
paulson@18886
   141
     "secureM \<Longrightarrow> knows Spy (Inputs A C X # evs) =  
paulson@18886
   142
        (if A=Spy then insert X (knows Spy evs) else knows Spy evs)"
paulson@18886
   143
by simp
paulson@18886
   144
paulson@18886
   145
lemma knows_Spy_Inputs_insecureM [simp]: 
paulson@18886
   146
     "insecureM \<Longrightarrow> knows Spy (Inputs A C X # evs) = insert X (knows Spy evs)"
paulson@18886
   147
by simp
paulson@18886
   148
paulson@18886
   149
lemma knows_Spy_C_Gets [simp]: "knows Spy (C_Gets C X # evs) = knows Spy evs"
paulson@18886
   150
by simp
paulson@18886
   151
paulson@18886
   152
lemma knows_Spy_Outpts_secureM [simp]: 
paulson@18886
   153
      "secureM \<Longrightarrow> knows Spy (Outpts C A X # evs) = 
paulson@18886
   154
         (if A=Spy then insert X (knows Spy evs) else knows Spy evs)"
paulson@18886
   155
by simp
paulson@18886
   156
paulson@18886
   157
lemma knows_Spy_Outpts_insecureM [simp]: 
paulson@18886
   158
      "insecureM \<Longrightarrow> knows Spy (Outpts C A X # evs) = insert X (knows Spy evs)"
paulson@18886
   159
by simp
paulson@18886
   160
paulson@18886
   161
lemma knows_Spy_A_Gets [simp]: "knows Spy (A_Gets A X # evs) = knows Spy evs"
paulson@18886
   162
by simp
paulson@18886
   163
paulson@18886
   164
paulson@18886
   165
paulson@18886
   166
paulson@18886
   167
lemma knows_Spy_subset_knows_Spy_Says:
paulson@18886
   168
     "knows Spy evs \<subseteq> knows Spy (Says A B X # evs)"
paulson@18886
   169
by (simp add: subset_insertI)
paulson@18886
   170
paulson@18886
   171
lemma knows_Spy_subset_knows_Spy_Notes:
paulson@18886
   172
     "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)"
paulson@18886
   173
by force
paulson@18886
   174
paulson@18886
   175
lemma knows_Spy_subset_knows_Spy_Gets:
paulson@18886
   176
     "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)"
paulson@18886
   177
by (simp add: subset_insertI)
paulson@18886
   178
paulson@18886
   179
lemma knows_Spy_subset_knows_Spy_Inputs: 
paulson@18886
   180
     "knows Spy evs \<subseteq> knows Spy (Inputs A C X # evs)"
paulson@18886
   181
by auto
paulson@18886
   182
paulson@18886
   183
lemma knows_Spy_equals_knows_Spy_Gets: 
paulson@18886
   184
     "knows Spy evs = knows Spy (C_Gets C X # evs)"
paulson@18886
   185
by (simp add: subset_insertI)
paulson@18886
   186
paulson@18886
   187
lemma knows_Spy_subset_knows_Spy_Outpts: "knows Spy evs \<subseteq> knows Spy (Outpts C A X # evs)"
paulson@18886
   188
by auto
paulson@18886
   189
paulson@18886
   190
lemma knows_Spy_subset_knows_Spy_A_Gets: "knows Spy evs \<subseteq> knows Spy (A_Gets A X # evs)"
paulson@18886
   191
by (simp add: subset_insertI)
paulson@18886
   192
paulson@18886
   193
paulson@18886
   194
paulson@18886
   195
text{*Spy sees what is sent on the traffic*}
paulson@18886
   196
lemma Says_imp_knows_Spy [rule_format]:
paulson@18886
   197
     "Says A B X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
paulson@18886
   198
apply (induct_tac "evs")
paulson@18886
   199
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   200
done
paulson@18886
   201
paulson@18886
   202
lemma Notes_imp_knows_Spy [rule_format]:
paulson@18886
   203
     "Notes A X \<in> set evs \<longrightarrow> A\<in> bad \<longrightarrow> X \<in> knows Spy evs"
paulson@18886
   204
apply (induct_tac "evs")
paulson@18886
   205
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   206
done
paulson@18886
   207
paulson@18886
   208
(*Nothing can be stated on a Gets event*)
paulson@18886
   209
paulson@18886
   210
lemma Inputs_imp_knows_Spy_secureM [rule_format (no_asm)]: 
paulson@18886
   211
     "Inputs Spy C X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs"
paulson@18886
   212
apply (induct_tac "evs")
paulson@18886
   213
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   214
done
paulson@18886
   215
paulson@18886
   216
lemma Inputs_imp_knows_Spy_insecureM [rule_format (no_asm)]:
paulson@18886
   217
     "Inputs A C X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs"
paulson@18886
   218
apply (induct_tac "evs")
paulson@18886
   219
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   220
done
paulson@18886
   221
paulson@18886
   222
(*Nothing can be stated on a C_Gets event*)
paulson@18886
   223
paulson@18886
   224
lemma Outpts_imp_knows_Spy_secureM [rule_format (no_asm)]: 
paulson@18886
   225
     "Outpts C Spy X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs"
paulson@18886
   226
apply (induct_tac "evs")
paulson@18886
   227
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   228
done
paulson@18886
   229
paulson@18886
   230
lemma Outpts_imp_knows_Spy_insecureM [rule_format (no_asm)]:
paulson@18886
   231
     "Outpts C A X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs"
paulson@18886
   232
apply (induct_tac "evs")
paulson@18886
   233
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   234
done
paulson@18886
   235
paulson@18886
   236
(*Nothing can be stated on an A_Gets event*)
paulson@18886
   237
paulson@18886
   238
paulson@18886
   239
paulson@18886
   240
text{*Elimination rules: derive contradictions from old Says events containing
paulson@18886
   241
  items known to be fresh*}
paulson@18886
   242
lemmas knows_Spy_partsEs =
wenzelm@46471
   243
     Says_imp_knows_Spy [THEN parts.Inj, elim_format]
wenzelm@46471
   244
     parts.Body [elim_format]
paulson@18886
   245
paulson@18886
   246
paulson@18886
   247
paulson@18886
   248
subsection{*Knowledge of Agents*}
paulson@18886
   249
paulson@18886
   250
lemma knows_Inputs: "knows A (Inputs A C X # evs) = insert X (knows A evs)"
paulson@18886
   251
by simp
paulson@18886
   252
paulson@18886
   253
lemma knows_C_Gets: "knows A (C_Gets C X # evs) = knows A evs"
paulson@18886
   254
by simp
paulson@18886
   255
paulson@18886
   256
lemma knows_Outpts_secureM: 
paulson@18886
   257
      "secureM \<longrightarrow> knows A (Outpts C A X # evs) = insert X (knows A evs)"
paulson@18886
   258
by simp
paulson@18886
   259
wenzelm@26302
   260
lemma knows_Outpts_insecureM: 
paulson@18886
   261
      "insecureM \<longrightarrow> knows Spy (Outpts C A X # evs) = insert X (knows Spy evs)"
paulson@18886
   262
by simp
paulson@18886
   263
(*somewhat equivalent to knows_Spy_Outpts_insecureM*)
paulson@18886
   264
paulson@18886
   265
paulson@18886
   266
paulson@18886
   267
paulson@18886
   268
lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
paulson@18886
   269
by (simp add: subset_insertI)
paulson@18886
   270
paulson@18886
   271
lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)"
paulson@18886
   272
by (simp add: subset_insertI)
paulson@18886
   273
paulson@18886
   274
lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)"
paulson@18886
   275
by (simp add: subset_insertI)
paulson@18886
   276
paulson@18886
   277
lemma knows_subset_knows_Inputs: "knows A evs \<subseteq> knows A (Inputs A' C X # evs)"
paulson@18886
   278
by (simp add: subset_insertI)
paulson@18886
   279
paulson@18886
   280
lemma knows_subset_knows_C_Gets: "knows A evs \<subseteq> knows A (C_Gets C X # evs)"
paulson@18886
   281
by (simp add: subset_insertI)
paulson@18886
   282
paulson@18886
   283
lemma knows_subset_knows_Outpts: "knows A evs \<subseteq> knows A (Outpts C A' X # evs)"
paulson@18886
   284
by (simp add: subset_insertI)
paulson@18886
   285
wenzelm@26302
   286
lemma knows_subset_knows_A_Gets: "knows A evs \<subseteq> knows A (A_Gets A' X # evs)"
paulson@18886
   287
by (simp add: subset_insertI)
paulson@18886
   288
paulson@18886
   289
paulson@18886
   290
text{*Agents know what they say*}
paulson@18886
   291
lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> knows A evs"
paulson@18886
   292
apply (induct_tac "evs")
paulson@18886
   293
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   294
apply blast
paulson@18886
   295
done
paulson@18886
   296
paulson@18886
   297
text{*Agents know what they note*}
paulson@18886
   298
lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
paulson@18886
   299
apply (induct_tac "evs")
paulson@18886
   300
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   301
apply blast
paulson@18886
   302
done
paulson@18886
   303
paulson@18886
   304
text{*Agents know what they receive*}
paulson@18886
   305
lemma Gets_imp_knows_agents [rule_format]:
paulson@18886
   306
     "A \<noteq> Spy \<longrightarrow> Gets A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
paulson@18886
   307
apply (induct_tac "evs")
paulson@18886
   308
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   309
done
paulson@18886
   310
paulson@18886
   311
(*Agents know what they input to their smart card*)
paulson@18886
   312
lemma Inputs_imp_knows_agents [rule_format (no_asm)]: 
paulson@18886
   313
     "Inputs A (Card A) X \<in> set evs \<longrightarrow> X \<in> knows A evs"
paulson@18886
   314
apply (induct_tac "evs")
paulson@18886
   315
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   316
apply blast
paulson@18886
   317
done
paulson@18886
   318
paulson@18886
   319
(*Nothing to prove about C_Gets*)
paulson@18886
   320
paulson@18886
   321
(*Agents know what they obtain as output of their smart card,
paulson@18886
   322
  if the means is secure...*)
paulson@18886
   323
lemma Outpts_imp_knows_agents_secureM [rule_format (no_asm)]: 
paulson@18886
   324
     "secureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
paulson@18886
   325
apply (induct_tac "evs")
paulson@18886
   326
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   327
done
paulson@18886
   328
paulson@18886
   329
(*otherwise only the spy knows the outputs*)
paulson@18886
   330
lemma Outpts_imp_knows_agents_insecureM [rule_format (no_asm)]: 
paulson@18886
   331
      "insecureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
paulson@18886
   332
apply (induct_tac "evs")
paulson@18886
   333
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   334
done
paulson@18886
   335
paulson@18886
   336
(*end lemmas about agents' knowledge*)
paulson@18886
   337
paulson@18886
   338
paulson@18886
   339
paulson@18886
   340
lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
paulson@18886
   341
apply (induct_tac "evs", force)  
noschinl@53428
   342
apply (simp add: parts_insert_knows_A add: event.split, blast)
paulson@18886
   343
done
paulson@18886
   344
paulson@18886
   345
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
paulson@18886
   346
paulson@18886
   347
lemma initState_into_used: "X \<in> parts (initState B) \<Longrightarrow> X \<in> used evs"
paulson@18886
   348
apply (induct_tac "evs")
paulson@18886
   349
apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
paulson@18886
   350
done
paulson@18886
   351
noschinl@53428
   352
simps_of_case used_Cons_simps[simp]: used_Cons
paulson@18886
   353
paulson@18886
   354
lemma used_nil_subset: "used [] \<subseteq> used evs"
paulson@18886
   355
apply simp
paulson@18886
   356
apply (blast intro: initState_into_used)
paulson@18886
   357
done
paulson@18886
   358
paulson@18886
   359
paulson@18886
   360
paulson@18886
   361
(*Novel lemmas*)
paulson@18886
   362
lemma Says_parts_used [rule_format (no_asm)]: 
paulson@18886
   363
     "Says A B X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
paulson@18886
   364
apply (induct_tac "evs")
paulson@18886
   365
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   366
apply blast
paulson@18886
   367
done
paulson@18886
   368
paulson@18886
   369
lemma Notes_parts_used [rule_format (no_asm)]: 
paulson@18886
   370
     "Notes A X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
paulson@18886
   371
apply (induct_tac "evs")
paulson@18886
   372
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   373
apply blast
paulson@18886
   374
done
paulson@18886
   375
paulson@18886
   376
lemma Outpts_parts_used [rule_format (no_asm)]: 
paulson@18886
   377
     "Outpts C A X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
paulson@18886
   378
apply (induct_tac "evs")
paulson@18886
   379
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   380
apply blast
paulson@18886
   381
done
paulson@18886
   382
paulson@18886
   383
lemma Inputs_parts_used [rule_format (no_asm)]: 
paulson@18886
   384
     "Inputs A C X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
paulson@18886
   385
apply (induct_tac "evs")
paulson@18886
   386
apply (simp_all (no_asm_simp) split add: event.split)
paulson@18886
   387
apply blast
paulson@18886
   388
done
paulson@18886
   389
paulson@18886
   390
paulson@18886
   391
paulson@18886
   392
paulson@18886
   393
text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
paulson@18886
   394
declare knows_Cons [simp del]
paulson@18886
   395
        used_Nil [simp del] used_Cons [simp del]
paulson@18886
   396
paulson@18886
   397
paulson@18886
   398
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
noschinl@53428
   399
by (cases e, auto simp: knows_Cons)
paulson@18886
   400
paulson@18886
   401
lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
paulson@18886
   402
apply (induct_tac evs, simp) 
paulson@18886
   403
apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
paulson@18886
   404
done
paulson@18886
   405
paulson@18886
   406
paulson@18886
   407
text{*For proving @{text new_keys_not_used}*}
paulson@18886
   408
lemma keysFor_parts_insert:
paulson@18886
   409
     "\<lbrakk> K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) \<rbrakk>   
wenzelm@58860
   410
      \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) \<or> Key (invKey K) \<in> parts H" 
paulson@18886
   411
by (force 
paulson@18886
   412
    dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
paulson@18886
   413
           analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
paulson@18886
   414
    intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
paulson@18886
   415
paulson@18886
   416
end