src/HOL/Auth/Shared.thy
author paulson
Sat Apr 26 12:38:42 2003 +0200 (2003-04-26)
changeset 13926 6e62e5357a10
parent 13907 2bc462b99e70
child 13956 8fe7e12290e1
permissions -rw-r--r--
converting more HOL-Auth to new-style theories
paulson@1934
     1
(*  Title:      HOL/Auth/Shared
paulson@1934
     2
    ID:         $Id$
paulson@1934
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1934
     4
    Copyright   1996  University of Cambridge
paulson@1934
     5
paulson@1934
     6
Theory of Shared Keys (common to all symmetric-key protocols)
paulson@1934
     7
paulson@3512
     8
Shared, long-term keys; initial states of agents
paulson@1934
     9
*)
paulson@1934
    10
paulson@13926
    11
theory Shared = Event:
paulson@1934
    12
paulson@1934
    13
consts
paulson@11104
    14
  shrK    :: "agent => key"  (*symmetric keys*)
paulson@1967
    15
paulson@11104
    16
axioms
paulson@11270
    17
  isSym_keys: "K \<in> symKeys"	(*All keys are symmetric*)
paulson@11104
    18
  inj_shrK:   "inj shrK"	(*No two agents have the same long-term key*)
paulson@1934
    19
berghofe@5183
    20
primrec
paulson@2319
    21
        (*Server knows all long-term keys; other agents know only their own*)
paulson@11104
    22
  initState_Server:  "initState Server     = Key ` range shrK"
paulson@11104
    23
  initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
paulson@11104
    24
  initState_Spy:     "initState Spy        = Key`shrK`bad"
paulson@2032
    25
paulson@1934
    26
paulson@13926
    27
subsection{*Basic properties of shrK*}
paulson@13926
    28
paulson@13926
    29
(*Injectiveness: Agents' long-term keys are distinct.*)
paulson@13926
    30
declare inj_shrK [THEN inj_eq, iff]
paulson@13926
    31
paulson@13926
    32
lemma invKey_K [simp]: "invKey K = K"
paulson@13926
    33
apply (insert isSym_keys)
paulson@13926
    34
apply (simp add: symKeys_def) 
paulson@13926
    35
done
paulson@13926
    36
paulson@13926
    37
paulson@13926
    38
lemma analz_Decrypt' [dest]:
paulson@13926
    39
     "[| Crypt K X \<in> analz H;  Key K  \<in> analz H |] ==> X \<in> analz H"
paulson@13926
    40
by auto
paulson@13926
    41
paulson@13926
    42
text{*Now cancel the @{text dest} attribute given to
paulson@13926
    43
 @{text analz.Decrypt} in its declaration.*}
paulson@13926
    44
ML
paulson@13926
    45
{*
paulson@13926
    46
Delrules [analz.Decrypt];
paulson@13926
    47
*}
paulson@13926
    48
paulson@13926
    49
text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
paulson@13926
    50
  that expression is not in normal form.*}
paulson@13926
    51
paulson@13926
    52
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
paulson@13926
    53
apply (unfold keysFor_def)
paulson@13926
    54
apply (induct_tac "C", auto)
paulson@13926
    55
done
paulson@13926
    56
paulson@13926
    57
(*Specialized to shared-key model: no @{term invKey}*)
paulson@13926
    58
lemma keysFor_parts_insert:
paulson@13926
    59
     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] \
paulson@13926
    60
\     ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
paulson@13926
    61
by (force dest: Event.keysFor_parts_insert)  
paulson@13926
    62
paulson@13926
    63
lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"
paulson@13926
    64
by (drule Crypt_imp_invKey_keysFor, simp)
paulson@13926
    65
paulson@13926
    66
paulson@13926
    67
subsection{*Function "knows"*}
paulson@13926
    68
paulson@13926
    69
(*Spy sees shared keys of agents!*)
paulson@13926
    70
lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs"
paulson@13926
    71
apply (induct_tac "evs")
paulson@13926
    72
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
paulson@13926
    73
done
paulson@13926
    74
paulson@13926
    75
(*For case analysis on whether or not an agent is compromised*)
paulson@13926
    76
lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs);  A: bad |]  
paulson@13926
    77
      ==> X \<in> analz (knows Spy evs)"
paulson@13926
    78
apply (force dest!: analz.Decrypt)
paulson@13926
    79
done
paulson@13926
    80
paulson@13926
    81
paulson@13926
    82
(** Fresh keys never clash with long-term shared keys **)
paulson@13926
    83
paulson@13926
    84
(*Agents see their own shared keys!*)
paulson@13926
    85
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
paulson@13926
    86
by (induct_tac "A", auto)
paulson@13926
    87
paulson@13926
    88
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
paulson@13926
    89
by (rule initState_into_used, blast)
paulson@13926
    90
paulson@13926
    91
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
paulson@13926
    92
  from long-term shared keys*)
paulson@13926
    93
lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK"
paulson@13926
    94
by blast
paulson@13926
    95
paulson@13926
    96
lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K"
paulson@13926
    97
by blast
paulson@13926
    98
paulson@13926
    99
declare shrK_neq [THEN not_sym, simp]
paulson@13926
   100
paulson@13926
   101
paulson@13926
   102
subsection{*Fresh nonces*}
paulson@13926
   103
paulson@13926
   104
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
paulson@13926
   105
by (induct_tac "B", auto)
paulson@13926
   106
paulson@13926
   107
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
paulson@13926
   108
apply (simp (no_asm) add: used_Nil)
paulson@13926
   109
done
paulson@13926
   110
paulson@13926
   111
paulson@13926
   112
subsection{*Supply fresh nonces for possibility theorems.*}
paulson@13926
   113
paulson@13926
   114
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
paulson@13926
   115
lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs"
paulson@13926
   116
apply (induct_tac "evs")
paulson@13926
   117
apply (rule_tac x = 0 in exI)
paulson@13926
   118
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
paulson@13926
   119
apply safe
paulson@13926
   120
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
paulson@13926
   121
done
paulson@13926
   122
paulson@13926
   123
lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
paulson@13926
   124
by (rule Nonce_supply_lemma [THEN exE], blast)
paulson@13926
   125
paulson@13926
   126
lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
paulson@13926
   127
apply (cut_tac evs = evs in Nonce_supply_lemma)
paulson@13926
   128
apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
paulson@13926
   129
apply (rule_tac x = N in exI)
paulson@13926
   130
apply (rule_tac x = "Suc (N+Na) " in exI)
paulson@13926
   131
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
paulson@13926
   132
done
paulson@13926
   133
paulson@13926
   134
lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &  
paulson@13926
   135
                    Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
paulson@13926
   136
apply (cut_tac evs = evs in Nonce_supply_lemma)
paulson@13926
   137
apply (cut_tac evs = "evs'" in Nonce_supply_lemma)
paulson@13926
   138
apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify)
paulson@13926
   139
apply (rule_tac x = N in exI)
paulson@13926
   140
apply (rule_tac x = "Suc (N+Na) " in exI)
paulson@13926
   141
apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI)
paulson@13926
   142
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
paulson@13926
   143
done
paulson@13926
   144
paulson@13926
   145
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
paulson@13926
   146
apply (rule Nonce_supply_lemma [THEN exE])
paulson@13926
   147
apply (rule someI, blast)
paulson@13926
   148
done
paulson@13926
   149
paulson@13926
   150
subsection{*Supply fresh keys for possibility theorems.*}
paulson@13926
   151
paulson@11104
   152
axioms
paulson@13926
   153
  Key_supply_ax:  "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"
paulson@13926
   154
  --{*Unlike the corresponding property of nonces, this cannot be proved.
paulson@2516
   155
    We have infinitely many agents and there is nothing to stop their
paulson@2516
   156
    long-term keys from exhausting all the natural numbers.  The axiom
paulson@2516
   157
    assumes that their keys are dispersed so as to leave room for infinitely
paulson@2516
   158
    many fresh session keys.  We could, alternatively, restrict agents to
paulson@13926
   159
    an unspecified finite number.  We could however replace @{term"used evs"} 
paulson@13926
   160
    by @{term "used []"}.*}
paulson@13926
   161
paulson@13926
   162
lemma Key_supply1: "\<exists>K. Key K \<notin> used evs"
paulson@13926
   163
by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast)
paulson@13926
   164
paulson@13926
   165
lemma Key_supply2: "\<exists>K K'. Key K \<notin> used evs & Key K' \<notin> used evs' & K \<noteq> K'"
paulson@13926
   166
apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
paulson@13926
   167
apply (erule exE)
paulson@13926
   168
apply (cut_tac evs="evs'" in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax], auto) 
paulson@13926
   169
done
paulson@13926
   170
paulson@13926
   171
lemma Key_supply3: "\<exists>K K' K''. Key K \<notin> used evs & Key K' \<notin> used evs' &  
paulson@13926
   172
                       Key K'' \<notin> used evs'' & K \<noteq> K' & K' \<noteq> K'' & K \<noteq> K''"
paulson@13926
   173
apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax])
paulson@13926
   174
apply (erule exE)
paulson@13926
   175
(*Blast_tac requires instantiation of the keys for some reason*)
paulson@13926
   176
apply (cut_tac evs="evs'" and a1 = K in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax])
paulson@13926
   177
apply (erule exE)
paulson@13926
   178
apply (cut_tac evs = "evs''" and a1 = Ka and a2 = K 
paulson@13926
   179
       in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Key_supply_ax], blast)
paulson@13926
   180
done
paulson@13926
   181
paulson@13926
   182
lemma Key_supply: "Key (@ K. Key K \<notin> used evs) \<notin> used evs"
paulson@13926
   183
apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE])
paulson@13926
   184
apply (rule someI, blast)
paulson@13926
   185
done
paulson@13926
   186
paulson@13926
   187
subsection{*Tactics for possibility theorems*}
paulson@13926
   188
paulson@13926
   189
ML
paulson@13926
   190
{*
paulson@13926
   191
val inj_shrK      = thm "inj_shrK";
paulson@13926
   192
val isSym_keys    = thm "isSym_keys";
paulson@13926
   193
val Key_supply_ax = thm "Key_supply_ax";
paulson@13926
   194
val Key_supply = thm "Key_supply";
paulson@13926
   195
val Nonce_supply = thm "Nonce_supply";
paulson@13926
   196
val invKey_K = thm "invKey_K";
paulson@13926
   197
val analz_Decrypt' = thm "analz_Decrypt'";
paulson@13926
   198
val keysFor_parts_initState = thm "keysFor_parts_initState";
paulson@13926
   199
val keysFor_parts_insert = thm "keysFor_parts_insert";
paulson@13926
   200
val Crypt_imp_keysFor = thm "Crypt_imp_keysFor";
paulson@13926
   201
val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad";
paulson@13926
   202
val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad";
paulson@13926
   203
val shrK_in_initState = thm "shrK_in_initState";
paulson@13926
   204
val shrK_in_used = thm "shrK_in_used";
paulson@13926
   205
val Key_not_used = thm "Key_not_used";
paulson@13926
   206
val shrK_neq = thm "shrK_neq";
paulson@13926
   207
val Nonce_notin_initState = thm "Nonce_notin_initState";
paulson@13926
   208
val Nonce_notin_used_empty = thm "Nonce_notin_used_empty";
paulson@13926
   209
val Nonce_supply_lemma = thm "Nonce_supply_lemma";
paulson@13926
   210
val Nonce_supply1 = thm "Nonce_supply1";
paulson@13926
   211
val Nonce_supply2 = thm "Nonce_supply2";
paulson@13926
   212
val Nonce_supply3 = thm "Nonce_supply3";
paulson@13926
   213
val Nonce_supply = thm "Nonce_supply";
paulson@13926
   214
val Key_supply1 = thm "Key_supply1";
paulson@13926
   215
val Key_supply2 = thm "Key_supply2";
paulson@13926
   216
val Key_supply3 = thm "Key_supply3";
paulson@13926
   217
val Key_supply = thm "Key_supply";
paulson@13926
   218
*}
paulson@13926
   219
paulson@11104
   220
paulson@13926
   221
ML
paulson@13926
   222
{*
paulson@13926
   223
(*Omitting used_Says makes the tactic much faster: it leaves expressions
paulson@13926
   224
    such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
paulson@13926
   225
fun gen_possibility_tac ss state = state |>
paulson@13926
   226
   (REPEAT 
paulson@13926
   227
    (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets] 
paulson@13926
   228
                         setSolver safe_solver))
paulson@13926
   229
     THEN
paulson@13926
   230
     REPEAT_FIRST (eq_assume_tac ORELSE' 
paulson@13926
   231
                   resolve_tac [refl, conjI, Nonce_supply, Key_supply])))
paulson@13926
   232
paulson@13926
   233
(*Tactic for possibility theorems (ML script version)*)
paulson@13926
   234
fun possibility_tac state = gen_possibility_tac (simpset()) state
paulson@13926
   235
paulson@13926
   236
(*For harder protocols (such as Recur) where we have to set up some
paulson@13926
   237
  nonces and keys initially*)
paulson@13926
   238
fun basic_possibility_tac st = st |>
paulson@13926
   239
    REPEAT 
paulson@13926
   240
    (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
paulson@13926
   241
     THEN
paulson@13926
   242
     REPEAT_FIRST (resolve_tac [refl, conjI]))
paulson@13926
   243
*}
paulson@13926
   244
paulson@13926
   245
subsection{*Specialized rewriting for analz_insert_freshK*}
paulson@13926
   246
paulson@13926
   247
lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A"
paulson@13926
   248
by blast
paulson@13926
   249
paulson@13926
   250
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
paulson@13926
   251
by blast
paulson@13926
   252
paulson@13926
   253
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C"
paulson@13926
   254
by blast
paulson@13926
   255
paulson@13926
   256
(** Reverse the normal simplification of "image" to build up (not break down)
paulson@13926
   257
    the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
paulson@13926
   258
    erase occurrences of forwarded message components (X). **)
paulson@13926
   259
paulson@13926
   260
lemmas analz_image_freshK_simps =
paulson@13926
   261
       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
paulson@13926
   262
       disj_comms 
paulson@13926
   263
       image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
paulson@13926
   264
       analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
paulson@13926
   265
       insert_Key_singleton subset_Compl_range
paulson@13926
   266
       Key_not_used insert_Key_image Un_assoc [THEN sym]
paulson@13926
   267
paulson@13926
   268
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@13926
   269
lemma analz_image_freshK_lemma:
paulson@13926
   270
     "(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H)  ==>  
paulson@13926
   271
         (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
paulson@13926
   272
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@13926
   273
paulson@13926
   274
ML
paulson@13926
   275
{*
paulson@13926
   276
val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
paulson@13926
   277
paulson@13926
   278
val analz_image_freshK_ss = 
paulson@13926
   279
     simpset() delsimps [image_insert, image_Un]
paulson@13926
   280
	       delsimps [imp_disjL]    (*reduces blow-up*)
paulson@13926
   281
	       addsimps thms "analz_image_freshK_simps"
paulson@13926
   282
*}
paulson@13926
   283
paulson@13926
   284
paulson@11104
   285
paulson@11104
   286
(*Lets blast_tac perform this step without needing the simplifier*)
paulson@11104
   287
lemma invKey_shrK_iff [iff]:
paulson@11270
   288
     "(Key (invKey K) \<in> X) = (Key K \<in> X)"
paulson@13507
   289
by auto
paulson@11104
   290
paulson@11104
   291
(*Specialized methods*)
paulson@11104
   292
paulson@11104
   293
method_setup analz_freshK = {*
paulson@11104
   294
    Method.no_args
paulson@11104
   295
     (Method.METHOD
paulson@13907
   296
      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
paulson@11104
   297
                          REPEAT_FIRST (rtac analz_image_freshK_lemma),
paulson@11104
   298
                          ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
paulson@11104
   299
    "for proving the Session Key Compromise theorem"
paulson@11104
   300
paulson@11104
   301
method_setup possibility = {*
paulson@11270
   302
    Method.ctxt_args (fn ctxt =>
paulson@11270
   303
        Method.METHOD (fn facts =>
paulson@11270
   304
            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
paulson@11104
   305
    "for proving possibility theorems"
paulson@2516
   306
paulson@12415
   307
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
paulson@12415
   308
by (induct e, auto simp: knows_Cons)
paulson@12415
   309
paulson@1934
   310
end