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