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