src/HOL/Auth/Public.thy
author haftmann
Fri Jan 02 08:12:46 2009 +0100 (2009-01-02)
changeset 29332 edc1e2a56398
parent 24122 fc7f857d33c8
child 30510 4120fc59dd85
permissions -rw-r--r--
named code theorem for Fract_norm
paulson@2318
     1
(*  Title:      HOL/Auth/Public
paulson@2318
     2
    ID:         $Id$
paulson@2318
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2318
     4
    Copyright   1996  University of Cambridge
paulson@2318
     5
paulson@3512
     6
Theory of Public Keys (common to all public-key protocols)
paulson@2318
     7
paulson@3512
     8
Private and public keys; initial states of agents
paulson@2318
     9
*)
paulson@2318
    10
haftmann@16417
    11
theory Public imports Event begin
paulson@13922
    12
paulson@14207
    13
lemma invKey_K: "K \<in> symKeys ==> invKey K = K"
paulson@14207
    14
by (simp add: symKeys_def)
paulson@14207
    15
paulson@13922
    16
subsection{*Asymmetric Keys*}
paulson@2318
    17
paulson@18749
    18
datatype keymode = Signature | Encryption
paulson@18749
    19
paulson@2318
    20
consts
paulson@18749
    21
  publicKey :: "[keymode,agent] => key"
paulson@2318
    22
wenzelm@20768
    23
abbreviation
wenzelm@21404
    24
  pubEK :: "agent => key" where
wenzelm@20768
    25
  "pubEK == publicKey Encryption"
paulson@13922
    26
wenzelm@21404
    27
abbreviation
wenzelm@21404
    28
  pubSK :: "agent => key" where
wenzelm@20768
    29
  "pubSK == publicKey Signature"
paulson@13922
    30
wenzelm@21404
    31
abbreviation
wenzelm@21404
    32
  privateKey :: "[keymode, agent] => key" where
wenzelm@20768
    33
  "privateKey b A == invKey (publicKey b A)"
paulson@13922
    34
wenzelm@21404
    35
abbreviation
paulson@13922
    36
  (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
wenzelm@21404
    37
  priEK :: "agent => key" where
wenzelm@20768
    38
  "priEK A == privateKey Encryption A"
wenzelm@21404
    39
wenzelm@21404
    40
abbreviation
wenzelm@21404
    41
  priSK :: "agent => key" where
wenzelm@20768
    42
  "priSK A == privateKey Signature A"
paulson@13922
    43
paulson@13922
    44
wenzelm@20768
    45
text{*These abbreviations give backward compatibility.  They represent the
paulson@13922
    46
simple situation where the signature and encryption keys are the same.*}
wenzelm@20768
    47
wenzelm@20768
    48
abbreviation
wenzelm@21404
    49
  pubK :: "agent => key" where
wenzelm@20768
    50
  "pubK A == pubEK A"
wenzelm@20768
    51
wenzelm@21404
    52
abbreviation
wenzelm@21404
    53
  priK :: "agent => key" where
wenzelm@20768
    54
  "priK A == invKey (pubEK A)"
paulson@13922
    55
paulson@13922
    56
paulson@14126
    57
text{*By freeness of agents, no two agents have the same key.  Since
paulson@14126
    58
  @{term "True\<noteq>False"}, no agent has identical signing and encryption keys*}
paulson@14126
    59
specification (publicKey)
paulson@13922
    60
  injective_publicKey:
paulson@13922
    61
    "publicKey b A = publicKey c A' ==> b=c & A=A'"
paulson@18749
    62
   apply (rule exI [of _ 
paulson@18749
    63
       "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + keymode_case 0 1 b"])
paulson@18749
    64
   apply (auto simp add: inj_on_def split: agent.split keymode.split)
chaieb@23315
    65
   apply presburger
chaieb@23315
    66
   apply presburger
paulson@14126
    67
   done                       
paulson@13922
    68
paulson@14126
    69
paulson@14126
    70
axioms
paulson@13922
    71
  (*No private key equals any public key (essential to ensure that private
paulson@13922
    72
    keys are private!) *)
paulson@13922
    73
  privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
paulson@13922
    74
paulson@18749
    75
lemmas publicKey_neq_privateKey = privateKey_neq_publicKey [THEN not_sym]
paulson@18749
    76
declare publicKey_neq_privateKey [iff]
paulson@13922
    77
paulson@13922
    78
paulson@13926
    79
subsection{*Basic properties of @{term pubK} and @{term priK}*}
paulson@13922
    80
paulson@18570
    81
lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')"
paulson@13922
    82
by (blast dest!: injective_publicKey) 
paulson@13922
    83
paulson@13922
    84
lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys"
paulson@13926
    85
by (simp add: symKeys_def)
paulson@13922
    86
paulson@13922
    87
lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys"
paulson@13926
    88
by (simp add: symKeys_def)
paulson@13922
    89
paulson@13922
    90
lemma symKey_neq_priEK: "K \<in> symKeys ==> K \<noteq> priEK A"
paulson@13922
    91
by auto
paulson@13922
    92
paulson@13922
    93
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
paulson@13926
    94
by blast
paulson@13922
    95
paulson@13922
    96
lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
paulson@13926
    97
by (unfold symKeys_def, auto)
paulson@2318
    98
paulson@13922
    99
lemma analz_symKeys_Decrypt:
paulson@13922
   100
     "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]  
paulson@13922
   101
      ==> X \<in> analz H"
paulson@13922
   102
by (auto simp add: symKeys_def)
paulson@13922
   103
paulson@13922
   104
paulson@13922
   105
paulson@13922
   106
subsection{*"Image" equations that hold for injective functions*}
paulson@13922
   107
paulson@13922
   108
lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)"
paulson@13926
   109
by auto
paulson@13922
   110
paulson@13922
   111
(*holds because invKey is injective*)
paulson@13922
   112
lemma publicKey_image_eq [simp]:
paulson@13922
   113
     "(publicKey b x \<in> publicKey c ` AA) = (b=c & x \<in> AA)"
paulson@13922
   114
by auto
paulson@13922
   115
paulson@13922
   116
lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA"
paulson@13926
   117
by auto
paulson@13922
   118
paulson@13922
   119
lemma privateKey_image_eq [simp]:
paulson@13922
   120
     "(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)"
paulson@13922
   121
by auto
paulson@13922
   122
paulson@13922
   123
lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> invKey ` publicKey c ` AS"
paulson@13926
   124
by auto
paulson@13922
   125
paulson@13922
   126
paulson@13922
   127
subsection{*Symmetric Keys*}
paulson@13922
   128
paulson@13922
   129
text{*For some protocols, it is convenient to equip agents with symmetric as
paulson@13922
   130
well as asymmetric keys.  The theory @{text Shared} assumes that all keys
paulson@13922
   131
are symmetric.*}
paulson@13922
   132
paulson@13922
   133
consts
paulson@13922
   134
  shrK    :: "agent => key"    --{*long-term shared keys*}
paulson@13922
   135
paulson@14126
   136
specification (shrK)
paulson@14126
   137
  inj_shrK: "inj shrK"
paulson@14126
   138
  --{*No two agents have the same long-term key*}
paulson@14126
   139
   apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
paulson@14126
   140
   apply (simp add: inj_on_def split: agent.split) 
paulson@14126
   141
   done
paulson@14126
   142
paulson@13922
   143
axioms
paulson@13922
   144
  sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
paulson@13922
   145
paulson@18570
   146
text{*Injectiveness: Agents' long-term keys are distinct.*}
paulson@18570
   147
lemmas shrK_injective = inj_shrK [THEN inj_eq]
paulson@18570
   148
declare shrK_injective [iff]
paulson@13922
   149
paulson@14207
   150
lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A"
paulson@14207
   151
by (simp add: invKey_K) 
paulson@14207
   152
paulson@14207
   153
lemma analz_shrK_Decrypt:
paulson@14207
   154
     "[| Crypt (shrK A) X \<in> analz H; Key(shrK A) \<in> analz H |] ==> X \<in> analz H"
paulson@14207
   155
by auto
paulson@14207
   156
paulson@14207
   157
lemma analz_Decrypt':
paulson@14207
   158
     "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] ==> X \<in> analz H"
paulson@14207
   159
by (auto simp add: invKey_K)
paulson@14207
   160
paulson@13922
   161
lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C"
paulson@13926
   162
by (simp add: symKeys_neq_imp_neq)
paulson@13922
   163
paulson@18749
   164
lemmas shrK_neq_priK = priK_neq_shrK [THEN not_sym]
paulson@18749
   165
declare shrK_neq_priK [simp]
paulson@13922
   166
paulson@13922
   167
lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C"
paulson@13926
   168
by (simp add: symKeys_neq_imp_neq)
paulson@13922
   169
paulson@18749
   170
lemmas shrK_neq_pubK = pubK_neq_shrK [THEN not_sym]
paulson@18749
   171
declare shrK_neq_pubK [simp]
paulson@13922
   172
paulson@13922
   173
lemma priEK_noteq_shrK [simp]: "priEK A \<noteq> shrK B" 
paulson@13922
   174
by auto
paulson@13922
   175
paulson@13922
   176
lemma publicKey_notin_image_shrK [simp]: "publicKey b x \<notin> shrK ` AA"
paulson@13922
   177
by auto
paulson@13922
   178
paulson@13922
   179
lemma privateKey_notin_image_shrK [simp]: "privateKey b x \<notin> shrK ` AA"
paulson@13922
   180
by auto
paulson@13922
   181
paulson@13922
   182
lemma shrK_notin_image_publicKey [simp]: "shrK x \<notin> publicKey b ` AA"
paulson@13922
   183
by auto
paulson@13922
   184
paulson@13922
   185
lemma shrK_notin_image_privateKey [simp]: "shrK x \<notin> invKey ` publicKey b ` AA" 
paulson@13922
   186
by auto
paulson@13922
   187
paulson@13922
   188
lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)"
paulson@13922
   189
by auto
paulson@13922
   190
paulson@14207
   191
text{*For some reason, moving this up can make some proofs loop!*}
paulson@14207
   192
declare invKey_K [simp]
paulson@14207
   193
paulson@13922
   194
paulson@13922
   195
subsection{*Initial States of Agents*}
paulson@13922
   196
paulson@13922
   197
text{*Note: for all practical purposes, all that matters is the initial
paulson@13922
   198
knowledge of the Spy.  All other agents are automata, merely following the
paulson@13922
   199
protocol.*}
paulson@2318
   200
berghofe@5183
   201
primrec
paulson@2318
   202
        (*Agents know their private key and all public keys*)
paulson@13922
   203
  initState_Server:
paulson@13922
   204
    "initState Server     =    
paulson@13922
   205
       {Key (priEK Server), Key (priSK Server)} \<union> 
paulson@13922
   206
       (Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)"
paulson@13922
   207
paulson@13922
   208
  initState_Friend:
paulson@13922
   209
    "initState (Friend i) =    
paulson@13922
   210
       {Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union> 
paulson@13922
   211
       (Key ` range pubEK) \<union> (Key ` range pubSK)"
paulson@13922
   212
paulson@13922
   213
  initState_Spy:
paulson@13922
   214
    "initState Spy        =    
paulson@13922
   215
       (Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union> 
paulson@13922
   216
       (Key ` shrK ` bad) \<union> 
paulson@13922
   217
       (Key ` range pubEK) \<union> (Key ` range pubSK)"
paulson@13922
   218
paulson@13922
   219
paulson@13922
   220
text{*These lemmas allow reasoning about @{term "used evs"} rather than
paulson@13935
   221
   @{term "knows Spy evs"}, which is useful when there are private Notes. 
paulson@13935
   222
   Because they depend upon the definition of @{term initState}, they cannot
paulson@13935
   223
   be moved up.*}
paulson@13922
   224
paulson@13922
   225
lemma used_parts_subset_parts [rule_format]:
paulson@13922
   226
     "\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
paulson@13922
   227
apply (induct evs) 
paulson@13922
   228
 prefer 2
paulson@13922
   229
 apply (simp add: used_Cons)
paulson@13922
   230
 apply (rule ballI)  
paulson@13935
   231
 apply (case_tac a, auto)  
paulson@13935
   232
apply (auto dest!: parts_cut) 
paulson@13922
   233
txt{*Base case*}
paulson@13935
   234
apply (simp add: used_Nil) 
paulson@13922
   235
done
paulson@13922
   236
paulson@13922
   237
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"
paulson@13922
   238
by (drule used_parts_subset_parts, simp, blast)
paulson@13922
   239
paulson@17990
   240
text{*There was a similar theorem in Event.thy, so perhaps this one can
paulson@17990
   241
  be moved up if proved directly by induction.*}
paulson@13922
   242
lemma MPair_used [elim!]:
paulson@13922
   243
     "[| {|X,Y|} \<in> used H;
paulson@13922
   244
         [| X \<in> used H; Y \<in> used H |] ==> P |] 
paulson@13922
   245
      ==> P"
paulson@13922
   246
by (blast dest: MPair_used_D) 
paulson@13922
   247
paulson@13922
   248
paulson@13922
   249
text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
paulson@13922
   250
  that expression is not in normal form.*}
paulson@13922
   251
paulson@13922
   252
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
paulson@13922
   253
apply (unfold keysFor_def)
paulson@13922
   254
apply (induct_tac "C")
paulson@13922
   255
apply (auto intro: range_eqI)
paulson@13922
   256
done
paulson@13922
   257
paulson@13922
   258
lemma Crypt_notin_initState: "Crypt K X \<notin> parts (initState B)"
paulson@13922
   259
by (induct B, auto)
paulson@13922
   260
paulson@13935
   261
lemma Crypt_notin_used_empty [simp]: "Crypt K X \<notin> used []"
paulson@13935
   262
by (simp add: Crypt_notin_initState used_Nil)
paulson@13935
   263
paulson@13922
   264
(*** Basic properties of shrK ***)
paulson@13922
   265
paulson@13922
   266
(*Agents see their own shared keys!*)
paulson@13922
   267
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
paulson@13926
   268
by (induct_tac "A", auto)
paulson@13922
   269
paulson@13922
   270
lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs"
paulson@13922
   271
by (simp add: initState_subset_knows [THEN subsetD])
paulson@13922
   272
paulson@13922
   273
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
paulson@13926
   274
by (rule initState_into_used, blast)
paulson@13922
   275
paulson@14207
   276
paulson@13922
   277
(** Fresh keys never clash with long-term shared keys **)
paulson@13922
   278
paulson@13922
   279
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
paulson@13922
   280
  from long-term shared keys*)
paulson@14207
   281
lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK"
paulson@13926
   282
by blast
paulson@13922
   283
paulson@13922
   284
lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K"
paulson@13926
   285
by blast
paulson@13922
   286
paulson@18749
   287
lemmas neq_shrK = shrK_neq [THEN not_sym]
paulson@18749
   288
declare neq_shrK [simp]
paulson@2318
   289
paulson@2318
   290
paulson@13922
   291
subsection{*Function @{term spies} *}
paulson@13922
   292
paulson@18749
   293
lemma not_SignatureE [elim!]: "b \<noteq> Signature \<Longrightarrow> b = Encryption"
paulson@18749
   294
  by (cases b, auto) 
paulson@18749
   295
paulson@13922
   296
text{*Agents see their own private keys!*}
paulson@13922
   297
lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A"
paulson@18749
   298
  by (cases A, auto)
paulson@13922
   299
paulson@13922
   300
text{*Agents see all public keys!*}
paulson@13922
   301
lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B"
paulson@18749
   302
  by (cases B, auto) 
paulson@13922
   303
paulson@13922
   304
text{*All public keys are visible*}
paulson@13922
   305
lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
paulson@13922
   306
apply (induct_tac "evs")
paulson@18749
   307
apply (auto simp add: imageI knows_Cons split add: event.split)
paulson@13922
   308
done
paulson@13922
   309
paulson@18749
   310
lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj]
paulson@18749
   311
declare analz_spies_pubK [iff]
paulson@13922
   312
paulson@13922
   313
text{*Spy sees private keys of bad agents!*}
paulson@13922
   314
lemma Spy_spies_bad_privateKey [intro!]:
paulson@13922
   315
     "A \<in> bad ==> Key (privateKey b A) \<in> spies evs"
paulson@13922
   316
apply (induct_tac "evs")
paulson@18749
   317
apply (auto simp add: imageI knows_Cons split add: event.split)
paulson@13922
   318
done
paulson@13922
   319
paulson@13922
   320
text{*Spy sees long-term shared keys of bad agents!*}
paulson@13922
   321
lemma Spy_spies_bad_shrK [intro!]:
paulson@13922
   322
     "A \<in> bad ==> Key (shrK A) \<in> spies evs"
paulson@13922
   323
apply (induct_tac "evs")
paulson@13922
   324
apply (simp_all add: imageI knows_Cons split add: event.split)
paulson@13922
   325
done
paulson@13922
   326
paulson@13922
   327
lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs"
paulson@13922
   328
apply (rule initState_into_used)
paulson@13922
   329
apply (rule publicKey_in_initState [THEN parts.Inj])
paulson@13922
   330
done
paulson@13922
   331
paulson@13922
   332
lemma privateKey_into_used [iff]: "Key (privateKey b A) \<in> used evs"
paulson@13922
   333
apply(rule initState_into_used)
paulson@13922
   334
apply(rule priK_in_initState [THEN parts.Inj])
paulson@13922
   335
done
paulson@13922
   336
paulson@14207
   337
(*For case analysis on whether or not an agent is compromised*)
paulson@14207
   338
lemma Crypt_Spy_analz_bad:
paulson@14207
   339
     "[| Crypt (shrK A) X \<in> analz (knows Spy evs);  A \<in> bad |]  
paulson@14207
   340
      ==> X \<in> analz (knows Spy evs)"
paulson@14207
   341
by force
paulson@14207
   342
paulson@13922
   343
paulson@13922
   344
subsection{*Fresh Nonces*}
paulson@13922
   345
paulson@13922
   346
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
paulson@13926
   347
by (induct_tac "B", auto)
paulson@13922
   348
paulson@13922
   349
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
paulson@13926
   350
by (simp add: used_Nil)
paulson@13922
   351
paulson@11104
   352
paulson@13922
   353
subsection{*Supply fresh nonces for possibility theorems*}
paulson@13922
   354
paulson@13922
   355
text{*In any trace, there is an upper bound N on the greatest nonce in use*}
paulson@13922
   356
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
paulson@13922
   357
apply (induct_tac "evs")
paulson@13926
   358
apply (rule_tac x = 0 in exI)
paulson@13922
   359
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
paulson@13922
   360
apply safe
paulson@13922
   361
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
paulson@13922
   362
done
paulson@13922
   363
paulson@13922
   364
lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
paulson@13926
   365
by (rule Nonce_supply_lemma [THEN exE], blast)
paulson@13922
   366
paulson@13922
   367
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
paulson@13922
   368
apply (rule Nonce_supply_lemma [THEN exE])
paulson@13926
   369
apply (rule someI, fast)
paulson@13922
   370
done
paulson@13922
   371
paulson@13956
   372
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
paulson@13922
   373
paulson@13922
   374
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
paulson@13926
   375
by blast
paulson@11104
   376
paulson@13922
   377
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
paulson@13926
   378
by blast
paulson@13922
   379
paulson@13922
   380
paulson@14207
   381
lemma Crypt_imp_keysFor :"[|Crypt K X \<in> H; K \<in> symKeys|] ==> K \<in> keysFor H"
paulson@13926
   382
by (drule Crypt_imp_invKey_keysFor, simp)
paulson@13922
   383
paulson@14207
   384
text{*Lemma for the trivial direction of the if-and-only-if of the 
paulson@14207
   385
Session Key Compromise Theorem*}
paulson@14207
   386
lemma analz_image_freshK_lemma:
paulson@14207
   387
     "(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H)  ==>  
paulson@14207
   388
         (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
paulson@14207
   389
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@14207
   390
paulson@14207
   391
lemmas analz_image_freshK_simps =
paulson@14207
   392
       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
paulson@14207
   393
       disj_comms 
paulson@14207
   394
       image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
paulson@14207
   395
       analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]
paulson@14207
   396
       insert_Key_singleton 
paulson@14207
   397
       Key_not_used insert_Key_image Un_assoc [THEN sym]
paulson@14207
   398
haftmann@21619
   399
ML {*
wenzelm@24122
   400
structure Public =
wenzelm@24122
   401
struct
paulson@14207
   402
wenzelm@24122
   403
val analz_image_freshK_ss = @{simpset} delsimps [image_insert, image_Un]
wenzelm@24122
   404
  delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
wenzelm@24122
   405
  addsimps @{thms analz_image_freshK_simps}
paulson@13922
   406
wenzelm@23894
   407
(*Tactic for possibility theorems*)
wenzelm@23894
   408
fun possibility_tac ctxt =
paulson@13922
   409
    REPEAT (*omit used_Says so that Nonces start from different traces!*)
wenzelm@24122
   410
    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}]))
paulson@13922
   411
     THEN
paulson@13922
   412
     REPEAT_FIRST (eq_assume_tac ORELSE' 
wenzelm@23894
   413
                   resolve_tac [refl, conjI, @{thm Nonce_supply}]))
paulson@14207
   414
paulson@14207
   415
(*For harder protocols (such as Recur) where we have to set up some
paulson@14207
   416
  nonces and keys initially*)
wenzelm@23894
   417
fun basic_possibility_tac ctxt =
paulson@14207
   418
    REPEAT 
wenzelm@23894
   419
    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
paulson@14207
   420
     THEN
paulson@14207
   421
     REPEAT_FIRST (resolve_tac [refl, conjI]))
wenzelm@24122
   422
wenzelm@24122
   423
end
paulson@13922
   424
*}
paulson@11104
   425
wenzelm@24122
   426
method_setup analz_freshK = {*
wenzelm@24122
   427
    Method.ctxt_args (fn ctxt =>
wenzelm@24122
   428
     (Method.SIMPLE_METHOD
wenzelm@24122
   429
      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
wenzelm@24122
   430
          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
wenzelm@24122
   431
          ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *}
wenzelm@24122
   432
    "for proving the Session Key Compromise theorem"
wenzelm@24122
   433
wenzelm@24122
   434
wenzelm@24122
   435
subsection{*Specialized Methods for Possibility Theorems*}
wenzelm@24122
   436
paulson@11104
   437
method_setup possibility = {*
paulson@11270
   438
    Method.ctxt_args (fn ctxt =>
wenzelm@24122
   439
        Method.SIMPLE_METHOD (Public.possibility_tac ctxt)) *}
wenzelm@23894
   440
    "for proving possibility theorems"
wenzelm@23894
   441
wenzelm@23894
   442
method_setup basic_possibility = {*
wenzelm@23894
   443
    Method.ctxt_args (fn ctxt =>
wenzelm@24122
   444
        Method.SIMPLE_METHOD (Public.basic_possibility_tac ctxt)) *}
paulson@11104
   445
    "for proving possibility theorems"
paulson@2318
   446
paulson@2318
   447
end