src/HOL/Auth/Guard/GuardK.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
wenzelm@41775
     1
(*  Title:      HOL/Auth/Guard/GuardK.thy
wenzelm@41775
     2
    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
wenzelm@41775
     3
    Copyright   2002  University of Cambridge
wenzelm@41775
     4
wenzelm@41775
     5
Very similar to Guard except:
paulson@13508
     6
- Guard is replaced by GuardK, guard by guardK, Nonce by Key
paulson@13508
     7
- some scripts are slightly modified (+ keyset_in, kparts_parts)
paulson@13508
     8
- the hypothesis Key n ~:G (keyset G) is added
wenzelm@41775
     9
*)
paulson@13508
    10
wenzelm@58889
    11
section{*protocol-independent confidentiality theorem on keys*}
paulson@13508
    12
haftmann@27108
    13
theory GuardK
haftmann@27108
    14
imports Analz Extensions
haftmann@27108
    15
begin
paulson@13508
    16
paulson@13508
    17
(******************************************************************************
paulson@13508
    18
messages where all the occurrences of Key n are
paulson@13508
    19
in a sub-message of the form Crypt (invKey K) X with K:Ks
paulson@13508
    20
******************************************************************************)
paulson@13508
    21
berghofe@23746
    22
inductive_set
berghofe@23746
    23
  guardK :: "nat => key set => msg set"
berghofe@23746
    24
  for n :: nat and Ks :: "key set"
berghofe@23746
    25
where
berghofe@23746
    26
  No_Key [intro]: "Key n ~:parts {X} ==> X:guardK n Ks"
berghofe@23746
    27
| Guard_Key [intro]: "invKey K:Ks ==> Crypt K X:guardK n Ks"
berghofe@23746
    28
| Crypt [intro]: "X:guardK n Ks ==> Crypt K X:guardK n Ks"
berghofe@23746
    29
| Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> {|X,Y|}:guardK n Ks"
paulson@13508
    30
paulson@13508
    31
subsection{*basic facts about @{term guardK}*}
paulson@13508
    32
paulson@13508
    33
lemma Nonce_is_guardK [iff]: "Nonce p:guardK n Ks"
paulson@13508
    34
by auto
paulson@13508
    35
paulson@13508
    36
lemma Agent_is_guardK [iff]: "Agent A:guardK n Ks"
paulson@13508
    37
by auto
paulson@13508
    38
paulson@13508
    39
lemma Number_is_guardK [iff]: "Number r:guardK n Ks"
paulson@13508
    40
by auto
paulson@13508
    41
paulson@13508
    42
lemma Key_notin_guardK: "X:guardK n Ks ==> X ~= Key n"
paulson@13508
    43
by (erule guardK.induct, auto)
paulson@13508
    44
paulson@13508
    45
lemma Key_notin_guardK_iff [iff]: "Key n ~:guardK n Ks"
paulson@13508
    46
by (auto dest: Key_notin_guardK)
paulson@13508
    47
paulson@13508
    48
lemma guardK_has_Crypt [rule_format]: "X:guardK n Ks ==> Key n:parts {X}
paulson@13508
    49
--> (EX K Y. Crypt K Y:kparts {X} & Key n:parts {Y})"
paulson@13508
    50
by (erule guardK.induct, auto)
paulson@13508
    51
paulson@13508
    52
lemma Key_notin_kparts_msg: "X:guardK n Ks ==> Key n ~:kparts {X}"
paulson@13508
    53
by (erule guardK.induct, auto dest: kparts_parts)
paulson@13508
    54
paulson@13508
    55
lemma Key_in_kparts_imp_no_guardK: "Key n:kparts H
paulson@13508
    56
==> EX X. X:H & X ~:guardK n Ks"
paulson@13508
    57
apply (drule in_kparts, clarify)
paulson@13508
    58
apply (rule_tac x=X in exI, clarify)
paulson@13508
    59
by (auto dest: Key_notin_kparts_msg)
paulson@13508
    60
paulson@13508
    61
lemma guardK_kparts [rule_format]: "X:guardK n Ks ==>
paulson@13508
    62
Y:kparts {X} --> Y:guardK n Ks"
paulson@13508
    63
by (erule guardK.induct, auto dest: kparts_parts parts_sub)
paulson@13508
    64
paulson@13508
    65
lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks"
haftmann@56681
    66
  by (ind_cases "Crypt K Y:guardK n Ks") (auto intro!: image_eqI)
paulson@13508
    67
paulson@13508
    68
lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks)
paulson@13508
    69
= (X:guardK n Ks & Y:guardK n Ks)"
paulson@13508
    70
by (auto, (ind_cases "{|X,Y|}:guardK n Ks", auto)+)
paulson@13508
    71
paulson@13508
    72
lemma guardK_not_guardK [rule_format]: "X:guardK n Ks ==>
paulson@13508
    73
Crypt K Y:kparts {X} --> Key n:kparts {Y} --> Y ~:guardK n Ks"
paulson@13508
    74
by (erule guardK.induct, auto dest: guardK_kparts)
paulson@13508
    75
paulson@13508
    76
lemma guardK_extand: "[| X:guardK n Ks; Ks <= Ks';
paulson@13508
    77
[| K:Ks'; K ~:Ks |] ==> Key K ~:parts {X} |] ==> X:guardK n Ks'"
paulson@13508
    78
by (erule guardK.induct, auto)
paulson@13508
    79
paulson@13508
    80
subsection{*guarded sets*}
paulson@13508
    81
haftmann@35416
    82
definition GuardK :: "nat => key set => msg set => bool" where
paulson@13508
    83
"GuardK n Ks H == ALL X. X:H --> X:guardK n Ks"
paulson@13508
    84
paulson@13508
    85
subsection{*basic facts about @{term GuardK}*}
paulson@13508
    86
paulson@13508
    87
lemma GuardK_empty [iff]: "GuardK n Ks {}"
paulson@13508
    88
by (simp add: GuardK_def)
paulson@13508
    89
paulson@13508
    90
lemma Key_notin_kparts [simplified]: "GuardK n Ks H ==> Key n ~:kparts H"
paulson@13508
    91
by (auto simp: GuardK_def dest: in_kparts Key_notin_kparts_msg)
paulson@13508
    92
paulson@13508
    93
lemma GuardK_must_decrypt: "[| GuardK n Ks H; Key n:analz H |] ==>
paulson@13508
    94
EX K Y. Crypt K Y:kparts H & Key (invKey K):kparts H"
paulson@13508
    95
apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp)
paulson@13508
    96
by (drule must_decrypt, auto dest: Key_notin_kparts)
paulson@13508
    97
paulson@13508
    98
lemma GuardK_kparts [intro]: "GuardK n Ks H ==> GuardK n Ks (kparts H)"
paulson@13508
    99
by (auto simp: GuardK_def dest: in_kparts guardK_kparts)
paulson@13508
   100
paulson@13508
   101
lemma GuardK_mono: "[| GuardK n Ks H; G <= H |] ==> GuardK n Ks G"
paulson@13508
   102
by (auto simp: GuardK_def)
paulson@13508
   103
paulson@13508
   104
lemma GuardK_insert [iff]: "GuardK n Ks (insert X H)
paulson@13508
   105
= (GuardK n Ks H & X:guardK n Ks)"
paulson@13508
   106
by (auto simp: GuardK_def)
paulson@13508
   107
paulson@13508
   108
lemma GuardK_Un [iff]: "GuardK n Ks (G Un H) = (GuardK n Ks G & GuardK n Ks H)"
paulson@13508
   109
by (auto simp: GuardK_def)
paulson@13508
   110
paulson@13508
   111
lemma GuardK_synth [intro]: "GuardK n Ks G ==> GuardK n Ks (synth G)"
paulson@13508
   112
by (auto simp: GuardK_def, erule synth.induct, auto)
paulson@13508
   113
paulson@13508
   114
lemma GuardK_analz [intro]: "[| GuardK n Ks G; ALL K. K:Ks --> Key K ~:analz G |]
paulson@13508
   115
==> GuardK n Ks (analz G)"
paulson@13508
   116
apply (auto simp: GuardK_def)
paulson@13508
   117
apply (erule analz.induct, auto)
berghofe@23746
   118
by (ind_cases "Crypt K Xa:guardK n Ks" for K Xa, auto)
paulson@13508
   119
paulson@13508
   120
lemma in_GuardK [dest]: "[| X:G; GuardK n Ks G |] ==> X:guardK n Ks"
paulson@13508
   121
by (auto simp: GuardK_def)
paulson@13508
   122
paulson@13508
   123
lemma in_synth_GuardK: "[| X:synth G; GuardK n Ks G |] ==> X:guardK n Ks"
paulson@13508
   124
by (drule GuardK_synth, auto)
paulson@13508
   125
paulson@13508
   126
lemma in_analz_GuardK: "[| X:analz G; GuardK n Ks G;
paulson@13508
   127
ALL K. K:Ks --> Key K ~:analz G |] ==> X:guardK n Ks"
paulson@13508
   128
by (drule GuardK_analz, auto)
paulson@13508
   129
paulson@13508
   130
lemma GuardK_keyset [simp]: "[| keyset G; Key n ~:G |] ==> GuardK n Ks G"
paulson@13508
   131
by (simp only: GuardK_def, clarify, drule keyset_in, auto)
paulson@13508
   132
paulson@13508
   133
lemma GuardK_Un_keyset: "[| GuardK n Ks G; keyset H; Key n ~:H |]
paulson@13508
   134
==> GuardK n Ks (G Un H)"
paulson@13508
   135
by auto
paulson@13508
   136
paulson@13508
   137
lemma in_GuardK_kparts: "[| X:G; GuardK n Ks G; Y:kparts {X} |] ==> Y:guardK n Ks"
paulson@13508
   138
by blast
paulson@13508
   139
paulson@13508
   140
lemma in_GuardK_kparts_neq: "[| X:G; GuardK n Ks G; Key n':kparts {X} |]
paulson@13508
   141
==> n ~= n'"
paulson@13508
   142
by (blast dest: in_GuardK_kparts)
paulson@13508
   143
paulson@13508
   144
lemma in_GuardK_kparts_Crypt: "[| X:G; GuardK n Ks G; is_MPair X;
paulson@13508
   145
Crypt K Y:kparts {X}; Key n:kparts {Y} |] ==> invKey K:Ks"
paulson@13508
   146
apply (drule in_GuardK, simp)
paulson@13508
   147
apply (frule guardK_not_guardK, simp+)
paulson@13508
   148
apply (drule guardK_kparts, simp)
paulson@13508
   149
by (ind_cases "Crypt K Y:guardK n Ks", auto)
paulson@13508
   150
paulson@13508
   151
lemma GuardK_extand: "[| GuardK n Ks G; Ks <= Ks';
paulson@13508
   152
[| K:Ks'; K ~:Ks |] ==> Key K ~:parts G |] ==> GuardK n Ks' G"
paulson@13508
   153
by (auto simp: GuardK_def dest: guardK_extand parts_sub)
paulson@13508
   154
paulson@13508
   155
subsection{*set obtained by decrypting a message*}
paulson@13508
   156
wenzelm@20768
   157
abbreviation (input)
wenzelm@21404
   158
  decrypt :: "msg set => key => msg => msg set" where
wenzelm@20768
   159
  "decrypt H K Y == insert Y (H - {Crypt K Y})"
paulson@13508
   160
paulson@13508
   161
lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |]
paulson@13508
   162
==> Key n:analz (decrypt H K Y)"
paulson@14307
   163
apply (drule_tac P="%H. Key n:analz H" in ssubst [OF insert_Diff])
paulson@14307
   164
apply assumption 
paulson@14307
   165
apply (simp only: analz_Crypt_if, simp)
paulson@14307
   166
done
paulson@13508
   167
paulson@13508
   168
lemma parts_decrypt: "[| Crypt K Y:H; X:parts (decrypt H K Y) |] ==> X:parts H"
paulson@13508
   169
by (erule parts.induct, auto intro: parts.Fst parts.Snd parts.Body)
paulson@13508
   170
paulson@13508
   171
subsection{*number of Crypt's in a message*}
paulson@13508
   172
krauss@35418
   173
fun crypt_nb :: "msg => nat" where
krauss@35418
   174
"crypt_nb (Crypt K X) = Suc (crypt_nb X)" |
krauss@35418
   175
"crypt_nb {|X,Y|} = crypt_nb X + crypt_nb Y" |
paulson@13508
   176
"crypt_nb X = 0" (* otherwise *)
paulson@13508
   177
paulson@13508
   178
subsection{*basic facts about @{term crypt_nb}*}
paulson@13508
   179
nipkow@25134
   180
lemma non_empty_crypt_msg: "Crypt K Y:parts {X} ==> crypt_nb X \<noteq> 0"
paulson@13508
   181
by (induct X, simp_all, safe, simp_all)
paulson@13508
   182
paulson@13508
   183
subsection{*number of Crypt's in a message list*}
paulson@13508
   184
krauss@35418
   185
primrec cnb :: "msg list => nat" where
krauss@35418
   186
"cnb [] = 0" |
paulson@13508
   187
"cnb (X#l) = crypt_nb X + cnb l"
paulson@13508
   188
paulson@13508
   189
subsection{*basic facts about @{term cnb}*}
paulson@13508
   190
paulson@13508
   191
lemma cnb_app [simp]: "cnb (l @ l') = cnb l + cnb l'"
paulson@13508
   192
by (induct l, auto)
paulson@13508
   193
haftmann@37596
   194
lemma mem_cnb_minus: "x \<in> set l ==> cnb l = crypt_nb x + (cnb l - crypt_nb x)"
paulson@13508
   195
by (induct l, auto)
paulson@13508
   196
paulson@13508
   197
lemmas mem_cnb_minus_substI = mem_cnb_minus [THEN ssubst]
paulson@13508
   198
haftmann@37596
   199
lemma cnb_minus [simp]: "x \<in> set l ==> cnb (remove l x) = cnb l - crypt_nb x"
paulson@13508
   200
apply (induct l, auto)
wenzelm@45600
   201
by (erule_tac l=l and x=x in mem_cnb_minus_substI, simp)
paulson@13508
   202
paulson@13508
   203
lemma parts_cnb: "Z:parts (set l) ==>
paulson@13508
   204
cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
paulson@13508
   205
by (erule parts.induct, auto simp: in_set_conv_decomp)
paulson@13508
   206
nipkow@25134
   207
lemma non_empty_crypt: "Crypt K Y:parts (set l) ==> cnb l \<noteq> 0"
paulson@13508
   208
by (induct l, auto dest: non_empty_crypt_msg parts_insert_substD)
paulson@13508
   209
paulson@13508
   210
subsection{*list of kparts*}
paulson@13508
   211
paulson@13508
   212
lemma kparts_msg_set: "EX l. kparts {X} = set l & cnb l = crypt_nb X"
paulson@13508
   213
apply (induct X, simp_all)
blanchet@58250
   214
apply (rename_tac agent, rule_tac x="[Agent agent]" in exI, simp)
blanchet@58250
   215
apply (rename_tac nat, rule_tac x="[Number nat]" in exI, simp)
blanchet@58250
   216
apply (rename_tac nat, rule_tac x="[Nonce nat]" in exI, simp)
blanchet@58250
   217
apply (rename_tac nat, rule_tac x="[Key nat]" in exI, simp)
nipkow@15236
   218
apply (rule_tac x="[Hash X]" in exI, simp)
paulson@13508
   219
apply (clarify, rule_tac x="l@la" in exI, simp)
blanchet@58250
   220
by (clarify, rename_tac nat X y, rule_tac x="[Crypt nat X]" in exI, simp)
paulson@13508
   221
paulson@13508
   222
lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
paulson@13508
   223
apply (induct l)
paulson@13508
   224
apply (rule_tac x="[]" in exI, simp, clarsimp)
blanchet@55417
   225
apply (rename_tac a b l')
nipkow@15236
   226
apply (subgoal_tac "EX l''.  kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
nipkow@15236
   227
apply (rule_tac x="l''@l'" in exI, simp)
paulson@13508
   228
apply (rule kparts_insert_substI, simp)
paulson@13508
   229
by (rule kparts_msg_set)
paulson@13508
   230
paulson@13508
   231
subsection{*list corresponding to "decrypt"*}
paulson@13508
   232
haftmann@35416
   233
definition decrypt' :: "msg list => key => msg => msg list" where
haftmann@19233
   234
"decrypt' l K Y == Y # remove l (Crypt K Y)"
paulson@13508
   235
paulson@13508
   236
declare decrypt'_def [simp]
paulson@13508
   237
paulson@13508
   238
subsection{*basic facts about @{term decrypt'}*}
paulson@13508
   239
paulson@13508
   240
lemma decrypt_minus: "decrypt (set l) K Y <= set (decrypt' l K Y)"
paulson@13508
   241
by (induct l, auto)
paulson@13508
   242
paulson@13508
   243
text{*if the analysis of a finite guarded set gives n then it must also give
paulson@13508
   244
one of the keys of Ks*}
paulson@13508
   245
paulson@13508
   246
lemma GuardK_invKey_by_list [rule_format]: "ALL l. cnb l = p
paulson@13508
   247
--> GuardK n Ks (set l) --> Key n:analz (set l)
paulson@13508
   248
--> (EX K. K:Ks & Key K:analz (set l))"
paulson@13508
   249
apply (induct p)
paulson@13508
   250
(* case p=0 *)
paulson@13508
   251
apply (clarify, drule GuardK_must_decrypt, simp, clarify)
paulson@13508
   252
apply (drule kparts_parts, drule non_empty_crypt, simp)
paulson@13508
   253
(* case p>0 *)
paulson@13508
   254
apply (clarify, frule GuardK_must_decrypt, simp, clarify)
paulson@13508
   255
apply (drule_tac P="%G. Key n:G" in analz_pparts_kparts_substD, simp)
paulson@13508
   256
apply (frule analz_decrypt, simp_all)
paulson@13508
   257
apply (subgoal_tac "EX l'. kparts (set l) = set l' & cnb l' = cnb l", clarsimp)
paulson@13508
   258
apply (drule_tac G="insert Y (set l' - {Crypt K Y})"
paulson@13508
   259
and H="set (decrypt' l' K Y)" in analz_sub, rule decrypt_minus)
paulson@13508
   260
apply (rule_tac analz_pparts_kparts_substI, simp)
paulson@13508
   261
apply (case_tac "K:invKey`Ks")
paulson@13508
   262
(* K:invKey`Ks *)
paulson@13508
   263
apply (clarsimp, blast)
paulson@13508
   264
(* K ~:invKey`Ks *)
paulson@13508
   265
apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))")
haftmann@37596
   266
apply (drule_tac x="decrypt' l' K Y" in spec, simp)
paulson@13508
   267
apply (subgoal_tac "Crypt K Y:parts (set l)")
paulson@13508
   268
apply (drule parts_cnb, rotate_tac -1, simp)
paulson@13508
   269
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
haftmann@19233
   270
apply (rule insert_mono, rule set_remove)
paulson@13508
   271
apply (simp add: analz_insertD, blast)
paulson@13508
   272
(* Crypt K Y:parts (set l) *)
paulson@13508
   273
apply (blast dest: kparts_parts)
paulson@13508
   274
(* GuardK n Ks (set (decrypt' l' K Y)) *)
paulson@13508
   275
apply (rule_tac H="insert Y (set l')" in GuardK_mono)
paulson@13508
   276
apply (subgoal_tac "GuardK n Ks (set l')", simp)
paulson@13508
   277
apply (rule_tac K=K in guardK_Crypt, simp add: GuardK_def, simp)
paulson@13508
   278
apply (drule_tac t="set l'" in sym, simp)
paulson@13508
   279
apply (rule GuardK_kparts, simp, simp)
haftmann@19233
   280
apply (rule_tac B="set l'" in subset_trans, rule set_remove, blast)
paulson@13508
   281
by (rule kparts_set)
paulson@13508
   282
paulson@13508
   283
lemma GuardK_invKey_finite: "[| Key n:analz G; GuardK n Ks G; finite G |]
paulson@13508
   284
==> EX K. K:Ks & Key K:analz G"
paulson@13508
   285
apply (drule finite_list, clarify)
paulson@13508
   286
by (rule GuardK_invKey_by_list, auto)
paulson@13508
   287
paulson@13508
   288
lemma GuardK_invKey: "[| Key n:analz G; GuardK n Ks G |]
paulson@13508
   289
==> EX K. K:Ks & Key K:analz G"
paulson@13508
   290
by (auto dest: analz_needs_only_finite GuardK_invKey_finite)
paulson@13508
   291
paulson@13508
   292
text{*if the analyse of a finite guarded set and a (possibly infinite) set of
paulson@13508
   293
keys gives n then it must also gives Ks*}
paulson@13508
   294
paulson@13508
   295
lemma GuardK_invKey_keyset: "[| Key n:analz (G Un H); GuardK n Ks G; finite G;
paulson@13508
   296
keyset H; Key n ~:H |] ==> EX K. K:Ks & Key K:analz (G Un H)"
wenzelm@45600
   297
apply (frule_tac P="%G. Key n:G" and G=G in analz_keyset_substD, simp_all)
paulson@13508
   298
apply (drule_tac G="G Un (H Int keysfor G)" in GuardK_invKey_finite)
paulson@13508
   299
apply (auto simp: GuardK_def intro: analz_sub)
paulson@13508
   300
by (drule keyset_in, auto)
paulson@13508
   301
paulson@13508
   302
end