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