author | wenzelm |
Fri, 18 Feb 2011 16:07:32 +0100 | |
changeset 41775 | 6214816d79d3 |
parent 39216 | 62332b382dba |
child 46008 | c296c75f4cf4 |
permissions | -rw-r--r-- |
41775 | 1 |
(* Title: HOL/Auth/Guard/Analz.thy |
2 |
Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 |
Copyright 2001 University of Cambridge |
|
4 |
*) |
|
13508 | 5 |
|
6 |
header{*Decomposition of Analz into two parts*} |
|
7 |
||
16417 | 8 |
theory Analz imports Extensions begin |
13508 | 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 |
||
23746 | 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" |
|
13508 | 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 |
||
23746 | 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" |
|
13508 | 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 |
||
39216 | 230 |
lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> X:analz (kparts {Z} Un kparts H)" |
13508 | 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" |
|
26808
d334a6d69598
Instantiated parts_insert_substD to avoid problems with HO unification
berghofe
parents:
23746
diff
changeset
|
239 |
apply (drule parts_insert_substD [where P="%S. Y : S"], clarify) |
13508 | 240 |
apply (drule in_sub, drule_tac X=Y in parts_sub, simp) |
241 |
by (auto dest: Nonce_kparts_synth) |
|
242 |
||
39216 | 243 |
lemma Crypt_insert_synth: |
244 |
"[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |] |
|
245 |
==> Crypt K Y:parts G" |
|
246 |
by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5)) |
|
247 |
||
13508 | 248 |
|
249 |
subsection{*analz is pparts + analz of kparts*} |
|
250 |
||
251 |
lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)" |
|
39216 | 252 |
by (erule analz.induct, auto) |
13508 | 253 |
|
254 |
lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)" |
|
255 |
by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz) |
|
256 |
||
257 |
lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst] |
|
39216 | 258 |
lemmas analz_pparts_kparts_substD = analz_pparts_kparts_eq [THEN sym, THEN ssubst] |
13508 | 259 |
|
260 |
end |