src/HOL/Auth/Shared.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 60754 02924903a6fd
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
wenzelm@37936
     1
(*  Title:      HOL/Auth/Shared.thy
paulson@1934
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1934
     3
    Copyright   1996  University of Cambridge
paulson@1934
     4
paulson@1934
     5
Theory of Shared Keys (common to all symmetric-key protocols)
paulson@1934
     6
paulson@3512
     7
Shared, long-term keys; initial states of agents
paulson@1934
     8
*)
paulson@1934
     9
haftmann@32631
    10
theory Shared
haftmann@32631
    11
imports Event All_Symmetric
haftmann@32631
    12
begin
paulson@1934
    13
paulson@1934
    14
consts
paulson@39216
    15
  shrK    :: "agent => key"  (*symmetric keys*)
paulson@14126
    16
paulson@14126
    17
specification (shrK)
paulson@14126
    18
  inj_shrK: "inj shrK"
paulson@14126
    19
  --{*No two agents have the same long-term key*}
blanchet@55416
    20
   apply (rule exI [of _ "case_agent 0 (\<lambda>n. n + 2) 1"]) 
paulson@14126
    21
   apply (simp add: inj_on_def split: agent.split) 
paulson@14126
    22
   done
paulson@1967
    23
paulson@14126
    24
text{*Server knows all long-term keys; other agents know only their own*}
haftmann@39246
    25
haftmann@39246
    26
overloading
haftmann@39246
    27
  initState \<equiv> initState
haftmann@39246
    28
begin
haftmann@39246
    29
haftmann@39246
    30
primrec initState where
paulson@11104
    31
  initState_Server:  "initState Server     = Key ` range shrK"
haftmann@39246
    32
| initState_Friend:  "initState (Friend i) = {Key (shrK (Friend i))}"
haftmann@39246
    33
| initState_Spy:     "initState Spy        = Key`shrK`bad"
haftmann@39246
    34
haftmann@39246
    35
end
paulson@2032
    36
paulson@1934
    37
paulson@13926
    38
subsection{*Basic properties of shrK*}
paulson@13926
    39
paulson@13926
    40
(*Injectiveness: Agents' long-term keys are distinct.*)
paulson@18749
    41
lemmas shrK_injective = inj_shrK [THEN inj_eq]
paulson@18749
    42
declare shrK_injective [iff]
paulson@13926
    43
paulson@13926
    44
lemma invKey_K [simp]: "invKey K = K"
paulson@13926
    45
apply (insert isSym_keys)
paulson@13926
    46
apply (simp add: symKeys_def) 
paulson@13926
    47
done
paulson@13926
    48
paulson@13926
    49
paulson@13926
    50
lemma analz_Decrypt' [dest]:
paulson@13926
    51
     "[| Crypt K X \<in> analz H;  Key K  \<in> analz H |] ==> X \<in> analz H"
paulson@13926
    52
by auto
paulson@13926
    53
paulson@13926
    54
text{*Now cancel the @{text dest} attribute given to
paulson@13926
    55
 @{text analz.Decrypt} in its declaration.*}
paulson@14200
    56
declare analz.Decrypt [rule del]
paulson@13926
    57
paulson@13926
    58
text{*Rewrites should not refer to  @{term "initState(Friend i)"} because
paulson@13926
    59
  that expression is not in normal form.*}
paulson@13926
    60
paulson@13926
    61
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
paulson@13926
    62
apply (unfold keysFor_def)
paulson@13926
    63
apply (induct_tac "C", auto)
paulson@13926
    64
done
paulson@13926
    65
paulson@13926
    66
(*Specialized to shared-key model: no @{term invKey}*)
paulson@13926
    67
lemma keysFor_parts_insert:
wenzelm@14983
    68
     "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |]
paulson@39216
    69
      ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
paulson@41693
    70
by (metis invKey_K keysFor_parts_insert)
paulson@13926
    71
paulson@13926
    72
lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"
paulson@41693
    73
by (metis Crypt_imp_invKey_keysFor invKey_K)
paulson@13926
    74
paulson@13926
    75
paulson@13926
    76
subsection{*Function "knows"*}
paulson@13926
    77
paulson@13926
    78
(*Spy sees shared keys of agents!*)
paulson@13926
    79
lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs"
paulson@13926
    80
apply (induct_tac "evs")
paulson@13926
    81
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
paulson@13926
    82
done
paulson@13926
    83
paulson@13926
    84
(*For case analysis on whether or not an agent is compromised*)
paulson@13926
    85
lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs);  A: bad |]  
paulson@13926
    86
      ==> X \<in> analz (knows Spy evs)"
paulson@41693
    87
by (metis Spy_knows_Spy_bad analz.Inj analz_Decrypt')
paulson@13926
    88
paulson@13926
    89
paulson@13926
    90
(** Fresh keys never clash with long-term shared keys **)
paulson@13926
    91
paulson@13926
    92
(*Agents see their own shared keys!*)
paulson@13926
    93
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A"
paulson@13926
    94
by (induct_tac "A", auto)
paulson@13926
    95
paulson@13926
    96
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
paulson@13926
    97
by (rule initState_into_used, blast)
paulson@13926
    98
paulson@13926
    99
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
paulson@13926
   100
  from long-term shared keys*)
paulson@13926
   101
lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK"
paulson@13926
   102
by blast
paulson@13926
   103
paulson@13926
   104
lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K"
paulson@13926
   105
by blast
paulson@13926
   106
paulson@17744
   107
lemmas shrK_sym_neq = shrK_neq [THEN not_sym]
paulson@17744
   108
declare shrK_sym_neq [simp]
paulson@13926
   109
paulson@13926
   110
paulson@13926
   111
subsection{*Fresh nonces*}
paulson@13926
   112
paulson@13926
   113
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
paulson@13926
   114
by (induct_tac "B", auto)
paulson@13926
   115
paulson@13926
   116
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
paulson@41693
   117
by (simp add: used_Nil)
paulson@13926
   118
paulson@13926
   119
paulson@13926
   120
subsection{*Supply fresh nonces for possibility theorems.*}
paulson@13926
   121
paulson@13926
   122
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
paulson@13926
   123
lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs"
paulson@13926
   124
apply (induct_tac "evs")
paulson@13926
   125
apply (rule_tac x = 0 in exI)
paulson@13926
   126
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
paulson@41693
   127
apply (metis le_sup_iff msg_Nonce_supply)
paulson@13926
   128
done
paulson@13926
   129
paulson@13926
   130
lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs"
paulson@41693
   131
by (metis Nonce_supply_lemma order_eq_iff)
paulson@13926
   132
paulson@13926
   133
lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'"
paulson@13926
   134
apply (cut_tac evs = evs in Nonce_supply_lemma)
paulson@13926
   135
apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify)
paulson@41693
   136
apply (metis Suc_n_not_le_n nat_le_linear)
paulson@13926
   137
done
paulson@13926
   138
paulson@13926
   139
lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' &  
paulson@13926
   140
                    Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''"
paulson@13926
   141
apply (cut_tac evs = evs in Nonce_supply_lemma)
paulson@13926
   142
apply (cut_tac evs = "evs'" in Nonce_supply_lemma)
paulson@13926
   143
apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify)
paulson@13926
   144
apply (rule_tac x = N in exI)
paulson@14200
   145
apply (rule_tac x = "Suc (N+Na)" in exI)
paulson@13926
   146
apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI)
paulson@13926
   147
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le)
paulson@13926
   148
done
paulson@13926
   149
paulson@13926
   150
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
paulson@13926
   151
apply (rule Nonce_supply_lemma [THEN exE])
paulson@13926
   152
apply (rule someI, blast)
paulson@13926
   153
done
paulson@13926
   154
paulson@14200
   155
text{*Unlike the corresponding property of nonces, we cannot prove
paulson@14200
   156
    @{term "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs"}.
paulson@2516
   157
    We have infinitely many agents and there is nothing to stop their
paulson@14200
   158
    long-term keys from exhausting all the natural numbers.  Instead,
paulson@14200
   159
    possibility theorems must assume the existence of a few keys.*}
paulson@13926
   160
paulson@13926
   161
paulson@13956
   162
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
paulson@13926
   163
paulson@13926
   164
lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A"
paulson@13926
   165
by blast
paulson@13926
   166
paulson@13926
   167
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H"
paulson@13926
   168
by blast
paulson@13926
   169
paulson@13956
   170
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C"
paulson@13926
   171
by blast
paulson@13926
   172
paulson@13926
   173
(** Reverse the normal simplification of "image" to build up (not break down)
paulson@13926
   174
    the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
paulson@13926
   175
    erase occurrences of forwarded message components (X). **)
paulson@13926
   176
paulson@13926
   177
lemmas analz_image_freshK_simps =
paulson@13926
   178
       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
paulson@13926
   179
       disj_comms 
paulson@13926
   180
       image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
paulson@13926
   181
       analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD]
paulson@13926
   182
       insert_Key_singleton subset_Compl_range
paulson@13926
   183
       Key_not_used insert_Key_image Un_assoc [THEN sym]
paulson@13926
   184
paulson@13926
   185
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@13926
   186
lemma analz_image_freshK_lemma:
paulson@13926
   187
     "(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H)  ==>  
paulson@13926
   188
         (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
paulson@13926
   189
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@13926
   190
wenzelm@24122
   191
wenzelm@24122
   192
subsection{*Tactics for possibility theorems*}
wenzelm@24122
   193
paulson@13926
   194
ML
paulson@13926
   195
{*
wenzelm@24122
   196
structure Shared =
wenzelm@24122
   197
struct
wenzelm@24122
   198
wenzelm@24122
   199
(*Omitting used_Says makes the tactic much faster: it leaves expressions
wenzelm@24122
   200
    such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
wenzelm@24122
   201
fun possibility_tac ctxt =
wenzelm@24122
   202
   (REPEAT 
wenzelm@51717
   203
    (ALLGOALS (simp_tac (ctxt
wenzelm@24122
   204
          delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}] 
wenzelm@24122
   205
          setSolver safe_solver))
wenzelm@24122
   206
     THEN
wenzelm@24122
   207
     REPEAT_FIRST (eq_assume_tac ORELSE' 
wenzelm@59498
   208
                   resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}])))
paulson@13926
   209
wenzelm@24122
   210
(*For harder protocols (such as Recur) where we have to set up some
wenzelm@24122
   211
  nonces and keys initially*)
wenzelm@24122
   212
fun basic_possibility_tac ctxt =
wenzelm@24122
   213
    REPEAT 
wenzelm@51717
   214
    (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
wenzelm@24122
   215
     THEN
wenzelm@59498
   216
     REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
wenzelm@24122
   217
wenzelm@24122
   218
wenzelm@24122
   219
val analz_image_freshK_ss =
wenzelm@51717
   220
  simpset_of
wenzelm@51717
   221
   (@{context} delsimps [image_insert, image_Un]
wenzelm@24122
   222
      delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
wenzelm@51717
   223
      addsimps @{thms analz_image_freshK_simps})
wenzelm@24122
   224
wenzelm@24122
   225
end
paulson@13926
   226
*}
paulson@13926
   227
paulson@13926
   228
paulson@11104
   229
paulson@11104
   230
(*Lets blast_tac perform this step without needing the simplifier*)
paulson@11104
   231
lemma invKey_shrK_iff [iff]:
paulson@11270
   232
     "(Key (invKey K) \<in> X) = (Key K \<in> X)"
paulson@13507
   233
by auto
paulson@11104
   234
paulson@11104
   235
(*Specialized methods*)
paulson@11104
   236
paulson@11104
   237
method_setup analz_freshK = {*
wenzelm@30549
   238
    Scan.succeed (fn ctxt =>
wenzelm@30510
   239
     (SIMPLE_METHOD
wenzelm@59498
   240
      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
wenzelm@60754
   241
          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
wenzelm@51717
   242
          ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))]))) *}
paulson@11104
   243
    "for proving the Session Key Compromise theorem"
paulson@11104
   244
paulson@11104
   245
method_setup possibility = {*
wenzelm@30549
   246
    Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
wenzelm@23894
   247
    "for proving possibility theorems"
wenzelm@23894
   248
wenzelm@23894
   249
method_setup basic_possibility = {*
wenzelm@30549
   250
    Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
paulson@11104
   251
    "for proving possibility theorems"
paulson@2516
   252
paulson@12415
   253
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
noschinl@53428
   254
by (cases e) (auto simp: knows_Cons)
paulson@12415
   255
paulson@1934
   256
end