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