src/HOL/Auth/Smartcard/Smartcard.thy
author huffman
Sat Jun 06 09:11:12 2009 -0700 (2009-06-06)
changeset 31488 5691ccb8d6b5
parent 30549 d2d7874648bd
child 32149 ef59550a55d3
permissions -rw-r--r--
generalize tendsto to class topological_space
paulson@18886
     1
(*  ID:         $Id$
paulson@18886
     2
    Author:     Giampaolo Bella, Catania University
paulson@18886
     3
*)
paulson@18886
     4
paulson@18886
     5
header{*Theory of smartcards*}
paulson@18886
     6
paulson@18886
     7
theory Smartcard imports EventSC begin
paulson@18886
     8
paulson@18886
     9
text{*  
paulson@18886
    10
As smartcards handle long-term (symmetric) keys, this theoy extends and 
paulson@18886
    11
supersedes theory Private.thy
paulson@18886
    12
paulson@18886
    13
An agent is bad if she reveals her PIN to the spy, not the shared key that
paulson@18886
    14
is embedded in her card. An agent's being bad implies nothing about her 
paulson@18886
    15
smartcard, which independently may be stolen or cloned.
paulson@18886
    16
*}
paulson@18886
    17
paulson@18886
    18
consts
paulson@18886
    19
  shrK    :: "agent => key"  (*long-term keys saved in smart cards*)
paulson@18886
    20
  crdK    :: "card  => key"  (*smart cards' symmetric keys*)
paulson@18886
    21
  pin     :: "agent => key"  (*pin to activate the smart cards*)
paulson@18886
    22
paulson@18886
    23
  (*Mostly for Shoup-Rubin*)
paulson@18886
    24
  Pairkey :: "agent * agent => nat"
paulson@18886
    25
  pairK   :: "agent * agent => key"
paulson@18886
    26
paulson@18886
    27
axioms
paulson@18886
    28
  inj_shrK: "inj shrK"  --{*No two smartcards store the same key*}
paulson@18886
    29
  inj_crdK: "inj crdK"  --{*Nor do two cards*}
paulson@18886
    30
  inj_pin : "inj pin"   --{*Nor do two agents have the same pin*}
paulson@18886
    31
paulson@18886
    32
  (*pairK is injective on each component, if we assume encryption to be a PRF
paulson@18886
    33
    or at least collision free *)
paulson@18886
    34
  inj_pairK    [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')"
paulson@18886
    35
  comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)"
paulson@18886
    36
paulson@18886
    37
  (*long-term keys differ from each other*)
paulson@18886
    38
  pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C"
paulson@18886
    39
  pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P"
paulson@18886
    40
  pairK_disj_pin [iff]:  "pairK(A,B) \<noteq> pin P"
paulson@18886
    41
  shrK_disj_crdK [iff]:  "shrK P \<noteq> crdK C"
paulson@18886
    42
  shrK_disj_pin [iff]:  "shrK P \<noteq> pin Q"
paulson@18886
    43
  crdK_disj_pin [iff]:   "crdK C \<noteq> pin P"
paulson@18886
    44
paulson@18886
    45
paulson@18886
    46
text{*All keys are symmetric*}
paulson@18886
    47
defs  all_symmetric_def: "all_symmetric == True"
paulson@18886
    48
paulson@18886
    49
lemma isSym_keys: "K \<in> symKeys"	
paulson@18886
    50
by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
paulson@18886
    51
paulson@18886
    52
paulson@18886
    53
constdefs
paulson@18886
    54
  legalUse :: "card => bool" ("legalUse (_)")
paulson@18886
    55
  "legalUse C == C \<notin> stolen"
paulson@18886
    56
paulson@18886
    57
consts  
paulson@18886
    58
  illegalUse :: "card  => bool"
paulson@18886
    59
primrec
paulson@18886
    60
  illegalUse_def: 
paulson@18886
    61
  "illegalUse (Card A) = ( (Card A \<in> stolen \<and> A \<in> bad)  \<or>  Card A \<in> cloned )"
paulson@18886
    62
paulson@18886
    63
paulson@18886
    64
text{*initState must be defined with care*}
paulson@18886
    65
primrec
paulson@18886
    66
(*Server knows all long-term keys; adding cards' keys may be redundant but
paulson@18886
    67
  helps prove crdK_in_initState and crdK_in_used to distinguish cards' keys
paulson@18886
    68
  from fresh (session) keys*)
paulson@18886
    69
  initState_Server:  "initState Server = 
paulson@18886
    70
        (Key`(range shrK \<union> range crdK \<union> range pin \<union> range pairK)) \<union> 
paulson@18886
    71
        (Nonce`(range Pairkey))"
paulson@18886
    72
paulson@18886
    73
(*Other agents know only their own*)
paulson@18886
    74
  initState_Friend:  "initState (Friend i) = {Key (pin (Friend i))}"
paulson@18886
    75
paulson@18886
    76
(*Spy knows bad agents' pins, cloned cards' keys, pairKs, and Pairkeys *)
paulson@18886
    77
  initState_Spy: "initState Spy  = 
paulson@18886
    78
                 (Key`((pin`bad) \<union> (pin `{A. Card A \<in> cloned}) \<union> 
paulson@18886
    79
                                      (shrK`{A. Card A \<in> cloned}) \<union> 
paulson@18886
    80
                        (crdK`cloned) \<union> 
paulson@18886
    81
                        (pairK`{(X,A). Card A \<in> cloned})))
paulson@18886
    82
           \<union> (Nonce`(Pairkey`{(A,B). Card A \<in> cloned & Card B \<in> cloned}))"
paulson@18886
    83
paulson@18886
    84
paulson@18886
    85
text{*Still relying on axioms*}
paulson@18886
    86
axioms
paulson@18886
    87
  Key_supply_ax:  "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs"
paulson@18886
    88
paulson@18886
    89
  (*Needed because of Spy's knowledge of Pairkeys*)
paulson@18886
    90
  Nonce_supply_ax: "finite NN \<Longrightarrow> \<exists> N. N \<notin> NN & Nonce N \<notin> used evs"
paulson@18886
    91
paulson@18886
    92
paulson@18886
    93
paulson@18886
    94
paulson@18886
    95
paulson@18886
    96
paulson@18886
    97
paulson@18886
    98
subsection{*Basic properties of shrK*}
paulson@18886
    99
paulson@18886
   100
(*Injectiveness: Agents' long-term keys are distinct.*)
paulson@18886
   101
declare inj_shrK [THEN inj_eq, iff]
paulson@18886
   102
declare inj_crdK [THEN inj_eq, iff]
paulson@18886
   103
declare inj_pin  [THEN inj_eq, iff]
paulson@18886
   104
paulson@18886
   105
lemma invKey_K [simp]: "invKey K = K"
paulson@18886
   106
apply (insert isSym_keys)
paulson@18886
   107
apply (simp add: symKeys_def) 
paulson@18886
   108
done
paulson@18886
   109
paulson@18886
   110
paulson@18886
   111
lemma analz_Decrypt' [dest]:
paulson@18886
   112
     "\<lbrakk> Crypt K X \<in> analz H;  Key K  \<in> analz H \<rbrakk> \<Longrightarrow> X \<in> analz H"
paulson@18886
   113
by auto
paulson@18886
   114
paulson@18886
   115
text{*Now cancel the @{text dest} attribute given to
paulson@18886
   116
 @{text analz.Decrypt} in its declaration.*}
paulson@18886
   117
declare analz.Decrypt [rule del]
paulson@18886
   118
paulson@18886
   119
text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
paulson@18886
   120
  that expression is not in normal form.*}
paulson@18886
   121
paulson@18886
   122
text{*Added to extend initstate with set of nonces*}
paulson@18886
   123
lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N"
paulson@18886
   124
apply auto
paulson@18886
   125
apply (erule parts.induct)
paulson@18886
   126
apply auto
paulson@18886
   127
done
paulson@18886
   128
paulson@18886
   129
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
paulson@18886
   130
apply (unfold keysFor_def)
paulson@18886
   131
apply (induct_tac "C", auto)
paulson@18886
   132
done
paulson@18886
   133
paulson@18886
   134
(*Specialized to shared-key model: no @{term invKey}*)
paulson@18886
   135
lemma keysFor_parts_insert:
paulson@18886
   136
     "\<lbrakk> K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) \<rbrakk> 
paulson@18886
   137
     \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
paulson@18886
   138
by (force dest: EventSC.keysFor_parts_insert)  
paulson@18886
   139
paulson@18886
   140
lemma Crypt_imp_keysFor: "Crypt K X \<in> H \<Longrightarrow> K \<in> keysFor H"
paulson@18886
   141
by (drule Crypt_imp_invKey_keysFor, simp)
paulson@18886
   142
paulson@18886
   143
paulson@18886
   144
subsection{*Function "knows"*}
paulson@18886
   145
paulson@18886
   146
(*Spy knows the pins of bad agents!*)
paulson@18886
   147
lemma Spy_knows_bad [intro!]: "A \<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
paulson@18886
   148
apply (induct_tac "evs")
paulson@18886
   149
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
paulson@18886
   150
done
paulson@18886
   151
paulson@18886
   152
(*Spy knows the long-term keys of cloned cards!*)
paulson@18886
   153
lemma Spy_knows_cloned [intro!]: 
paulson@18886
   154
     "Card A \<in> cloned \<Longrightarrow>  Key (crdK (Card A)) \<in> knows Spy evs &   
paulson@18886
   155
                           Key (shrK A) \<in> knows Spy evs &  
paulson@18886
   156
                           Key (pin A)  \<in> knows Spy evs &  
paulson@18886
   157
                          (\<forall> B. Key (pairK(B,A)) \<in> knows Spy evs)"
paulson@18886
   158
apply (induct_tac "evs")
paulson@18886
   159
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
paulson@18886
   160
done
paulson@18886
   161
paulson@18886
   162
lemma Spy_knows_cloned1 [intro!]: "C \<in> cloned \<Longrightarrow> Key (crdK C) \<in> knows Spy evs"
paulson@18886
   163
apply (induct_tac "evs")
paulson@18886
   164
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
paulson@18886
   165
done
paulson@18886
   166
paulson@18886
   167
lemma Spy_knows_cloned2 [intro!]: "\<lbrakk> Card A \<in> cloned; Card B \<in> cloned \<rbrakk>  
paulson@18886
   168
   \<Longrightarrow> Nonce (Pairkey(A,B))\<in> knows Spy evs"
paulson@18886
   169
apply (induct_tac "evs")
paulson@18886
   170
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
paulson@18886
   171
done
paulson@18886
   172
paulson@18886
   173
(*Spy only knows pins of bad agents!*)
paulson@18886
   174
lemma Spy_knows_Spy_bad [intro!]: "A\<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
paulson@18886
   175
apply (induct_tac "evs")
paulson@18886
   176
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
paulson@18886
   177
done
paulson@18886
   178
paulson@18886
   179
paulson@18886
   180
(*For case analysis on whether or not an agent is compromised*)
paulson@18886
   181
lemma Crypt_Spy_analz_bad: 
paulson@18886
   182
  "\<lbrakk> Crypt (pin A) X \<in> analz (knows Spy evs);  A\<in>bad \<rbrakk>   
paulson@18886
   183
      \<Longrightarrow> X \<in> analz (knows Spy evs)"
paulson@18886
   184
apply (force dest!: analz.Decrypt)
paulson@18886
   185
done
paulson@18886
   186
paulson@18886
   187
(** Fresh keys never clash with other keys **)
paulson@18886
   188
paulson@18886
   189
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState Server"
paulson@18886
   190
apply (induct_tac "A")
paulson@18886
   191
apply auto
paulson@18886
   192
done
paulson@18886
   193
paulson@18886
   194
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
paulson@18886
   195
apply (rule initState_into_used)
paulson@18886
   196
apply blast
paulson@18886
   197
done
paulson@18886
   198
paulson@18886
   199
lemma crdK_in_initState [iff]: "Key (crdK A) \<in> initState Server"
paulson@18886
   200
apply (induct_tac "A")
paulson@18886
   201
apply auto
paulson@18886
   202
done
paulson@18886
   203
paulson@18886
   204
lemma crdK_in_used [iff]: "Key (crdK A) \<in> used evs"
paulson@18886
   205
apply (rule initState_into_used)
paulson@18886
   206
apply blast
paulson@18886
   207
done
paulson@18886
   208
paulson@18886
   209
lemma pin_in_initState [iff]: "Key (pin A) \<in> initState A"
paulson@18886
   210
apply (induct_tac "A")
paulson@18886
   211
apply auto
paulson@18886
   212
done
paulson@18886
   213
paulson@18886
   214
lemma pin_in_used [iff]: "Key (pin A) \<in> used evs"
paulson@18886
   215
apply (rule initState_into_used)
paulson@18886
   216
apply blast
paulson@18886
   217
done
paulson@18886
   218
paulson@18886
   219
lemma pairK_in_initState [iff]: "Key (pairK X) \<in> initState Server"
paulson@18886
   220
apply (induct_tac "X")
paulson@18886
   221
apply auto
paulson@18886
   222
done
paulson@18886
   223
paulson@18886
   224
lemma pairK_in_used [iff]: "Key (pairK X) \<in> used evs"
paulson@18886
   225
apply (rule initState_into_used)
paulson@18886
   226
apply blast
paulson@18886
   227
done
paulson@18886
   228
paulson@18886
   229
paulson@18886
   230
paulson@18886
   231
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
paulson@18886
   232
  from long-term shared keys*)
paulson@18886
   233
lemma Key_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range shrK"
paulson@18886
   234
by blast
paulson@18886
   235
paulson@18886
   236
lemma shrK_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> shrK B \<noteq> K"
paulson@18886
   237
by blast
paulson@18886
   238
paulson@18886
   239
lemma crdK_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range crdK"
paulson@18886
   240
apply clarify
paulson@18886
   241
done
paulson@18886
   242
paulson@18886
   243
lemma crdK_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> crdK C \<noteq> K"
paulson@18886
   244
apply clarify
paulson@18886
   245
done
paulson@18886
   246
paulson@18886
   247
lemma pin_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range pin"
paulson@18886
   248
apply clarify
paulson@18886
   249
done
paulson@18886
   250
paulson@18886
   251
lemma pin_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> pin A \<noteq> K"
paulson@18886
   252
apply clarify
paulson@18886
   253
done
paulson@18886
   254
paulson@18886
   255
lemma pairK_not_used [simp]: "Key K \<notin> used evs \<Longrightarrow> K \<notin> range pairK"
paulson@18886
   256
apply clarify
paulson@18886
   257
done
paulson@18886
   258
paulson@18886
   259
lemma pairK_neq [simp]: "Key K \<notin> used evs \<Longrightarrow> pairK(A,B) \<noteq> K"
paulson@18886
   260
apply clarify
paulson@18886
   261
done
paulson@18886
   262
paulson@18886
   263
declare shrK_neq [THEN not_sym, simp]
paulson@18886
   264
declare crdK_neq [THEN not_sym, simp]
paulson@18886
   265
declare pin_neq [THEN not_sym, simp]
paulson@18886
   266
declare pairK_neq [THEN not_sym, simp]
paulson@18886
   267
paulson@18886
   268
paulson@18886
   269
subsection{*Fresh nonces*}
paulson@18886
   270
paulson@18886
   271
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState (Friend i))"
paulson@18886
   272
by auto
paulson@18886
   273
paulson@18886
   274
paulson@18886
   275
(*This lemma no longer holds of smartcard protocols, where the cards can store
paulson@18886
   276
  nonces.
paulson@18886
   277
paulson@18886
   278
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
paulson@18886
   279
apply (simp (no_asm) add: used_Nil)
paulson@18886
   280
done
paulson@18886
   281
paulson@18886
   282
So, we must use old-style supply fresh nonce theorems relying on the appropriate axiom*)
paulson@18886
   283
paulson@18886
   284
paulson@18886
   285
subsection{*Supply fresh nonces for possibility theorems.*}
paulson@18886
   286
paulson@18886
   287
paulson@18886
   288
lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
berghofe@22265
   289
apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE], blast)
paulson@18886
   290
done
paulson@18886
   291
paulson@18886
   292
lemma Nonce_supply2: 
paulson@18886
   293
  "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
berghofe@22265
   294
apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
paulson@18886
   295
apply (erule exE)
berghofe@22265
   296
apply (cut_tac evs = evs' in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax]) 
paulson@18886
   297
apply auto
paulson@18886
   298
done
paulson@18886
   299
paulson@18886
   300
paulson@18886
   301
lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &  
paulson@18886
   302
                    Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
berghofe@22265
   303
apply (cut_tac evs = evs in finite.emptyI [THEN Nonce_supply_ax])
paulson@18886
   304
apply (erule exE)
berghofe@22265
   305
apply (cut_tac evs = evs' and a1 = N in finite.emptyI [THEN finite.insertI, THEN Nonce_supply_ax]) 
paulson@18886
   306
apply (erule exE)
berghofe@22265
   307
apply (cut_tac evs = evs'' and a1 = Na and a2 = N in finite.emptyI [THEN finite.insertI, THEN finite.insertI, THEN Nonce_supply_ax]) 
paulson@18886
   308
apply blast
paulson@18886
   309
done
paulson@18886
   310
paulson@18886
   311
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
berghofe@22265
   312
apply (rule finite.emptyI [THEN Nonce_supply_ax, THEN exE])
paulson@18886
   313
apply (rule someI, blast)
paulson@18886
   314
done
paulson@18886
   315
paulson@18886
   316
paulson@18886
   317
paulson@18886
   318
text{*Unlike the corresponding property of nonces, we cannot prove
paulson@18886
   319
    @{term "finite KK \<Longrightarrow> \<exists>K. K \<notin> KK & Key K \<notin> used evs"}.
paulson@18886
   320
    We have infinitely many agents and there is nothing to stop their
paulson@18886
   321
    long-term keys from exhausting all the natural numbers.  Instead,
paulson@18886
   322
    possibility theorems must assume the existence of a few keys.*}
paulson@18886
   323
paulson@18886
   324
paulson@18886
   325
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
paulson@18886
   326
paulson@18886
   327
lemma subset_Compl_range_shrK: "A \<subseteq> - (range shrK) \<Longrightarrow> shrK x \<notin> A"
paulson@18886
   328
by blast
paulson@18886
   329
paulson@18886
   330
lemma subset_Compl_range_crdK: "A \<subseteq> - (range crdK) \<Longrightarrow> crdK x \<notin> A"
paulson@18886
   331
apply blast
paulson@18886
   332
done
paulson@18886
   333
paulson@18886
   334
lemma subset_Compl_range_pin: "A \<subseteq> - (range pin) \<Longrightarrow> pin x \<notin> A"
paulson@18886
   335
apply blast
paulson@18886
   336
done
paulson@18886
   337
paulson@18886
   338
lemma subset_Compl_range_pairK: "A \<subseteq> - (range pairK) \<Longrightarrow> pairK x \<notin> A"
paulson@18886
   339
apply blast
paulson@18886
   340
done
paulson@18886
   341
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
paulson@18886
   342
by blast
paulson@18886
   343
paulson@18886
   344
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C"
paulson@18886
   345
by blast
paulson@18886
   346
paulson@18886
   347
(** Reverse the normal simplification of "image" to build up (not break down)
paulson@18886
   348
    the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
paulson@18886
   349
    erase occurrences of forwarded message components (X). **)
paulson@18886
   350
paulson@18886
   351
lemmas analz_image_freshK_simps =
paulson@18886
   352
       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
paulson@18886
   353
       disj_comms 
paulson@18886
   354
       image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
paulson@18886
   355
       analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
paulson@18886
   356
       insert_Key_singleton subset_Compl_range_shrK subset_Compl_range_crdK
paulson@18886
   357
       subset_Compl_range_pin subset_Compl_range_pairK
paulson@18886
   358
       Key_not_used insert_Key_image Un_assoc [THEN sym]
paulson@18886
   359
paulson@18886
   360
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@18886
   361
lemma analz_image_freshK_lemma:
paulson@18886
   362
     "(Key K \<in> analz (Key`nE \<union> H)) \<longrightarrow> (K \<in> nE | Key K \<in> analz H)  \<Longrightarrow>  
paulson@18886
   363
         (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
paulson@18886
   364
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@18886
   365
wenzelm@24122
   366
wenzelm@24122
   367
subsection{*Tactics for possibility theorems*}
wenzelm@24122
   368
paulson@18886
   369
ML
paulson@18886
   370
{*
wenzelm@24122
   371
structure Smartcard =
wenzelm@24122
   372
struct
wenzelm@24122
   373
wenzelm@24122
   374
(*Omitting used_Says makes the tactic much faster: it leaves expressions
wenzelm@24122
   375
    such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
wenzelm@24122
   376
fun possibility_tac ctxt =
wenzelm@24122
   377
   (REPEAT 
wenzelm@24122
   378
    (ALLGOALS (simp_tac (local_simpset_of ctxt
wenzelm@24122
   379
      delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets},
wenzelm@24122
   380
        @{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}] 
wenzelm@24122
   381
      setSolver safe_solver))
wenzelm@24122
   382
     THEN
wenzelm@24122
   383
     REPEAT_FIRST (eq_assume_tac ORELSE' 
wenzelm@24122
   384
                   resolve_tac [refl, conjI, @{thm Nonce_supply}])))
wenzelm@24122
   385
wenzelm@24122
   386
(*For harder protocols (such as Recur) where we have to set up some
wenzelm@24122
   387
  nonces and keys initially*)
wenzelm@24122
   388
fun basic_possibility_tac ctxt =
wenzelm@24122
   389
    REPEAT 
wenzelm@24122
   390
    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
wenzelm@24122
   391
     THEN
wenzelm@24122
   392
     REPEAT_FIRST (resolve_tac [refl, conjI]))
paulson@18886
   393
paulson@18886
   394
val analz_image_freshK_ss = 
wenzelm@23894
   395
     @{simpset} delsimps [image_insert, image_Un]
wenzelm@23894
   396
	       delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
wenzelm@24122
   397
	       addsimps @{thms analz_image_freshK_simps}
wenzelm@24122
   398
end
paulson@18886
   399
*}
paulson@18886
   400
paulson@18886
   401
paulson@18886
   402
(*Lets blast_tac perform this step without needing the simplifier*)
paulson@18886
   403
lemma invKey_shrK_iff [iff]:
paulson@18886
   404
     "(Key (invKey K) \<in> X) = (Key K \<in> X)"
paulson@18886
   405
by auto
paulson@18886
   406
paulson@18886
   407
(*Specialized methods*)
paulson@18886
   408
paulson@18886
   409
method_setup analz_freshK = {*
wenzelm@30549
   410
    Scan.succeed (fn ctxt =>
wenzelm@30510
   411
     (SIMPLE_METHOD
wenzelm@21588
   412
      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
wenzelm@24122
   413
          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
wenzelm@24122
   414
          ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss))]))) *}
paulson@18886
   415
    "for proving the Session Key Compromise theorem"
paulson@18886
   416
paulson@18886
   417
method_setup possibility = {*
wenzelm@30549
   418
    Scan.succeed (fn ctxt =>
wenzelm@30510
   419
        SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
wenzelm@23894
   420
    "for proving possibility theorems"
wenzelm@23894
   421
wenzelm@23894
   422
method_setup basic_possibility = {*
wenzelm@30549
   423
    Scan.succeed (fn ctxt =>
wenzelm@30510
   424
        SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
paulson@18886
   425
    "for proving possibility theorems"
paulson@18886
   426
paulson@18886
   427
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
wenzelm@23894
   428
by (induct e) (auto simp: knows_Cons)
paulson@18886
   429
paulson@18886
   430
(*Needed for actual protocols that will follow*)
paulson@18886
   431
declare shrK_disj_crdK[THEN not_sym, iff]
paulson@18886
   432
declare shrK_disj_pin[THEN not_sym, iff]
paulson@18886
   433
declare pairK_disj_shrK[THEN not_sym, iff]
paulson@18886
   434
declare pairK_disj_crdK[THEN not_sym, iff]
paulson@18886
   435
declare pairK_disj_pin[THEN not_sym, iff]
paulson@18886
   436
declare crdK_disj_pin[THEN not_sym, iff]
paulson@18886
   437
paulson@18886
   438
declare legalUse_def [iff] illegalUse_def [iff]
paulson@18886
   439
paulson@18886
   440
end