src/HOL/Auth/Guard/Analz.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/Analz.thy
     2     Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
     3     Copyright   2001  University of Cambridge
     4 *)
     5 
     6 section{*Decomposition of Analz into two parts*}
     7 
     8 theory Analz imports Extensions begin
     9 
    10 text{*decomposition of @{term analz} into two parts: 
    11       @{term pparts} (for pairs) and analz of @{term kparts}*}
    12 
    13 subsection{*messages that do not contribute to analz*}
    14 
    15 inductive_set
    16   pparts :: "msg set => msg set"
    17   for H :: "msg set"
    18 where
    19   Inj [intro]: "[| X:H; is_MPair X |] ==> X:pparts H"
    20 | Fst [dest]: "[| {|X,Y|}:pparts H; is_MPair X |] ==> X:pparts H"
    21 | Snd [dest]: "[| {|X,Y|}:pparts H; is_MPair Y |] ==> Y:pparts H"
    22 
    23 subsection{*basic facts about @{term pparts}*}
    24 
    25 lemma pparts_is_MPair [dest]: "X:pparts H ==> is_MPair X"
    26 by (erule pparts.induct, auto)
    27 
    28 lemma Crypt_notin_pparts [iff]: "Crypt K X ~:pparts H"
    29 by auto
    30 
    31 lemma Key_notin_pparts [iff]: "Key K ~:pparts H"
    32 by auto
    33 
    34 lemma Nonce_notin_pparts [iff]: "Nonce n ~:pparts H"
    35 by auto
    36 
    37 lemma Number_notin_pparts [iff]: "Number n ~:pparts H"
    38 by auto
    39 
    40 lemma Agent_notin_pparts [iff]: "Agent A ~:pparts H"
    41 by auto
    42 
    43 lemma pparts_empty [iff]: "pparts {} = {}"
    44 by (auto, erule pparts.induct, auto)
    45 
    46 lemma pparts_insertI [intro]: "X:pparts H ==> X:pparts (insert Y H)"
    47 by (erule pparts.induct, auto)
    48 
    49 lemma pparts_sub: "[| X:pparts G; G<=H |] ==> X:pparts H"
    50 by (erule pparts.induct, auto)
    51 
    52 lemma pparts_insert2 [iff]: "pparts (insert X (insert Y H))
    53 = pparts {X} Un pparts {Y} Un pparts H"
    54 by (rule eq, (erule pparts.induct, auto)+)
    55 
    56 lemma pparts_insert_MPair [iff]: "pparts (insert {|X,Y|} H)
    57 = insert {|X,Y|} (pparts ({X,Y} Un H))"
    58 apply (rule eq, (erule pparts.induct, auto)+)
    59 apply (rule_tac Y=Y in pparts.Fst, auto)
    60 apply (erule pparts.induct, auto)
    61 by (rule_tac X=X in pparts.Snd, auto)
    62 
    63 lemma pparts_insert_Nonce [iff]: "pparts (insert (Nonce n) H) = pparts H"
    64 by (rule eq, erule pparts.induct, auto)
    65 
    66 lemma pparts_insert_Crypt [iff]: "pparts (insert (Crypt K X) H) = pparts H"
    67 by (rule eq, erule pparts.induct, auto)
    68 
    69 lemma pparts_insert_Key [iff]: "pparts (insert (Key K) H) = pparts H"
    70 by (rule eq, erule pparts.induct, auto)
    71 
    72 lemma pparts_insert_Agent [iff]: "pparts (insert (Agent A) H) = pparts H"
    73 by (rule eq, erule pparts.induct, auto)
    74 
    75 lemma pparts_insert_Number [iff]: "pparts (insert (Number n) H) = pparts H"
    76 by (rule eq, erule pparts.induct, auto)
    77 
    78 lemma pparts_insert_Hash [iff]: "pparts (insert (Hash X) H) = pparts H"
    79 by (rule eq, erule pparts.induct, auto)
    80 
    81 lemma pparts_insert: "X:pparts (insert Y H) ==> X:pparts {Y} Un pparts H"
    82 by (erule pparts.induct, blast+)
    83 
    84 lemma insert_pparts: "X:pparts {Y} Un pparts H ==> X:pparts (insert Y H)"
    85 by (safe, erule pparts.induct, auto)
    86 
    87 lemma pparts_Un [iff]: "pparts (G Un H) = pparts G Un pparts H"
    88 by (rule eq, erule pparts.induct, auto dest: pparts_sub)
    89 
    90 lemma pparts_pparts [iff]: "pparts (pparts H) = pparts H"
    91 by (rule eq, erule pparts.induct, auto)
    92 
    93 lemma pparts_insert_eq: "pparts (insert X H) = pparts {X} Un pparts H"
    94 by (rule_tac A=H in insert_Un, rule pparts_Un)
    95 
    96 lemmas pparts_insert_substI = pparts_insert_eq [THEN ssubst]
    97 
    98 lemma in_pparts: "Y:pparts H ==> EX X. X:H & Y:pparts {X}"
    99 by (erule pparts.induct, auto)
   100 
   101 subsection{*facts about @{term pparts} and @{term parts}*}
   102 
   103 lemma pparts_no_Nonce [dest]: "[| X:pparts {Y}; Nonce n ~:parts {Y} |]
   104 ==> Nonce n ~:parts {X}"
   105 by (erule pparts.induct, simp_all)
   106 
   107 subsection{*facts about @{term pparts} and @{term analz}*}
   108 
   109 lemma pparts_analz: "X:pparts H ==> X:analz H"
   110 by (erule pparts.induct, auto)
   111 
   112 lemma pparts_analz_sub: "[| X:pparts G; G<=H |] ==> X:analz H"
   113 by (auto dest: pparts_sub pparts_analz)
   114 
   115 subsection{*messages that contribute to analz*}
   116 
   117 inductive_set
   118   kparts :: "msg set => msg set"
   119   for H :: "msg set"
   120 where
   121   Inj [intro]: "[| X:H; not_MPair X |] ==> X:kparts H"
   122 | Fst [intro]: "[| {|X,Y|}:pparts H; not_MPair X |] ==> X:kparts H"
   123 | Snd [intro]: "[| {|X,Y|}:pparts H; not_MPair Y |] ==> Y:kparts H"
   124 
   125 subsection{*basic facts about @{term kparts}*}
   126 
   127 lemma kparts_not_MPair [dest]: "X:kparts H ==> not_MPair X"
   128 by (erule kparts.induct, auto)
   129 
   130 lemma kparts_empty [iff]: "kparts {} = {}"
   131 by (rule eq, erule kparts.induct, auto)
   132 
   133 lemma kparts_insertI [intro]: "X:kparts H ==> X:kparts (insert Y H)"
   134 by (erule kparts.induct, auto dest: pparts_insertI)
   135 
   136 lemma kparts_insert2 [iff]: "kparts (insert X (insert Y H))
   137 = kparts {X} Un kparts {Y} Un kparts H"
   138 by (rule eq, (erule kparts.induct, auto)+)
   139 
   140 lemma kparts_insert_MPair [iff]: "kparts (insert {|X,Y|} H)
   141 = kparts ({X,Y} Un H)"
   142 by (rule eq, (erule kparts.induct, auto)+)
   143 
   144 lemma kparts_insert_Nonce [iff]: "kparts (insert (Nonce n) H)
   145 = insert (Nonce n) (kparts H)"
   146 by (rule eq, erule kparts.induct, auto)
   147 
   148 lemma kparts_insert_Crypt [iff]: "kparts (insert (Crypt K X) H)
   149 = insert (Crypt K X) (kparts H)"
   150 by (rule eq, erule kparts.induct, auto)
   151 
   152 lemma kparts_insert_Key [iff]: "kparts (insert (Key K) H)
   153 = insert (Key K) (kparts H)"
   154 by (rule eq, erule kparts.induct, auto)
   155 
   156 lemma kparts_insert_Agent [iff]: "kparts (insert (Agent A) H)
   157 = insert (Agent A) (kparts H)"
   158 by (rule eq, erule kparts.induct, auto)
   159 
   160 lemma kparts_insert_Number [iff]: "kparts (insert (Number n) H)
   161 = insert (Number n) (kparts H)"
   162 by (rule eq, erule kparts.induct, auto)
   163 
   164 lemma kparts_insert_Hash [iff]: "kparts (insert (Hash X) H)
   165 = insert (Hash X) (kparts H)"
   166 by (rule eq, erule kparts.induct, auto)
   167 
   168 lemma kparts_insert: "X:kparts (insert X H) ==> X:kparts {X} Un kparts H"
   169 by (erule kparts.induct, (blast dest: pparts_insert)+)
   170 
   171 lemma kparts_insert_fst [rule_format,dest]: "X:kparts (insert Z H) ==>
   172 X ~:kparts H --> X:kparts {Z}"
   173 by (erule kparts.induct, (blast dest: pparts_insert)+)
   174 
   175 lemma kparts_sub: "[| X:kparts G; G<=H |] ==> X:kparts H"
   176 by (erule kparts.induct, auto dest: pparts_sub)
   177 
   178 lemma kparts_Un [iff]: "kparts (G Un H) = kparts G Un kparts H"
   179 by (rule eq, erule kparts.induct, auto dest: kparts_sub)
   180 
   181 lemma pparts_kparts [iff]: "pparts (kparts H) = {}"
   182 by (rule eq, erule pparts.induct, auto)
   183 
   184 lemma kparts_kparts [iff]: "kparts (kparts H) = kparts H"
   185 by (rule eq, erule kparts.induct, auto)
   186 
   187 lemma kparts_insert_eq: "kparts (insert X H) = kparts {X} Un kparts H"
   188 by (rule_tac A=H in insert_Un, rule kparts_Un)
   189 
   190 lemmas kparts_insert_substI = kparts_insert_eq [THEN ssubst]
   191 
   192 lemma in_kparts: "Y:kparts H ==> EX X. X:H & Y:kparts {X}"
   193 by (erule kparts.induct, auto dest: in_pparts)
   194 
   195 lemma kparts_has_no_pair [iff]: "has_no_pair (kparts H)"
   196 by auto
   197 
   198 subsection{*facts about @{term kparts} and @{term parts}*}
   199 
   200 lemma kparts_no_Nonce [dest]: "[| X:kparts {Y}; Nonce n ~:parts {Y} |]
   201 ==> Nonce n ~:parts {X}"
   202 by (erule kparts.induct, auto)
   203 
   204 lemma kparts_parts: "X:kparts H ==> X:parts H"
   205 by (erule kparts.induct, auto dest: pparts_analz)
   206 
   207 lemma parts_kparts: "X:parts (kparts H) ==> X:parts H"
   208 by (erule parts.induct, auto dest: kparts_parts
   209 intro: parts.Fst parts.Snd parts.Body)
   210 
   211 lemma Crypt_kparts_Nonce_parts [dest]: "[| Crypt K Y:kparts {Z};
   212 Nonce n:parts {Y} |] ==> Nonce n:parts {Z}"
   213 by auto
   214 
   215 subsection{*facts about @{term kparts} and @{term analz}*}
   216 
   217 lemma kparts_analz: "X:kparts H ==> X:analz H"
   218 by (erule kparts.induct, auto dest: pparts_analz)
   219 
   220 lemma kparts_analz_sub: "[| X:kparts G; G<=H |] ==> X:analz H"
   221 by (erule kparts.induct, auto dest: pparts_analz_sub)
   222 
   223 lemma analz_kparts [rule_format,dest]: "X:analz H ==>
   224 Y:kparts {X} --> Y:analz H"
   225 by (erule analz.induct, auto dest: kparts_analz_sub)
   226 
   227 lemma analz_kparts_analz: "X:analz (kparts H) ==> X:analz H"
   228 by (erule analz.induct, auto dest: kparts_analz)
   229 
   230 lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> X:analz (kparts {Z} Un kparts H)"
   231 by (rule analz_sub, auto)
   232 
   233 lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G)
   234 ==> Nonce n:kparts {Y} --> Nonce n:analz G"
   235 by (erule synth.induct, auto)
   236 
   237 lemma kparts_insert_synth: "[| Y:parts (insert X G); X:synth (analz G);
   238 Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Y:parts G"
   239 apply (drule parts_insert_substD, clarify)
   240 apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
   241 apply (auto dest: Nonce_kparts_synth)
   242 done
   243 
   244 lemma Crypt_insert_synth:
   245   "[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |] 
   246    ==> Crypt K Y:parts G"
   247 by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5))
   248 
   249 
   250 subsection{*analz is pparts + analz of kparts*}
   251 
   252 lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)"
   253 by (erule analz.induct, auto) 
   254 
   255 lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)"
   256 by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz)
   257 
   258 lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst]
   259 lemmas analz_pparts_kparts_substD = analz_pparts_kparts_eq [THEN sym, THEN ssubst]
   260 
   261 end