author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46075  0054a9513b37 
child 50705  0e943b33d907 
permissions  rwrr 
41141
ad923cdd4a5d
added example to exercise higherorder reasoning with Sledgehammer and Metis
blanchet
parents:
39260
diff
changeset

1 
(* Title: HOL/Metis_Examples/Message.thy 
43197  2 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 
41144  3 
Author: Jasmin Blanchette, TU Muenchen 
23449  4 

43197  5 
Metis example featuring message authentication. 
23449  6 
*) 
7 

43197  8 
header {* Metis Example Featuring Message Authentication *} 
9 

36553  10 
theory Message 
11 
imports Main 

12 
begin 

23449  13 

42103
6066a35f6678
Metis examples use the new Skolemizer to test it
blanchet
parents:
41144
diff
changeset

14 
declare [[metis_new_skolemizer]] 
6066a35f6678
Metis examples use the new Skolemizer to test it
blanchet
parents:
41144
diff
changeset

15 

23449  16 
lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A" 
36911  17 
by (metis Un_commute Un_left_absorb) 
23449  18 

42463  19 
type_synonym key = nat 
23449  20 

21 
consts 

22 
all_symmetric :: bool {*true if all keys are symmetric*} 

23 
invKey :: "key=>key" {*inverse of a symmetric key*} 

24 

25 
specification (invKey) 

26 
invKey [simp]: "invKey (invKey K) = K" 

27 
invKey_symmetric: "all_symmetric > invKey = id" 

36553  28 
by (metis id_apply) 
23449  29 

30 

31 
text{*The inverse of a symmetric key is itself; that of a public key 

32 
is the private key and vice versa*} 

33 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35109
diff
changeset

34 
definition symKeys :: "key set" where 
23449  35 
"symKeys == {K. invKey K = K}" 
36 

37 
datatype {*We allow any number of friendly agents*} 

38 
agent = Server  Friend nat  Spy 

39 

40 
datatype 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32864
diff
changeset

41 
msg = Agent agent {*Agent names*} 
23449  42 
 Number nat {*Ordinary integers, timestamps, ...*} 
43 
 Nonce nat {*Unguessable nonces*} 

44 
 Key key {*Crypto keys*} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32864
diff
changeset

45 
 Hash msg {*Hashing*} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32864
diff
changeset

46 
 MPair msg msg {*Compound messages*} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32864
diff
changeset

47 
 Crypt key msg {*Encryption, public or sharedkey*} 
23449  48 

49 

50 
text{*Concrete syntax: messages appear as {A,B,NA}, etc...*} 

51 
syntax 

35109  52 
"_MTuple" :: "['a, args] => 'a * 'b" ("(2{_,/ _})") 
23449  53 

54 
syntax (xsymbols) 

35109  55 
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") 
23449  56 

57 
translations 

58 
"{x, y, z}" == "{x, {y, z}}" 

35054  59 
"{x, y}" == "CONST MPair x y" 
23449  60 

61 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35109
diff
changeset

62 
definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where 
23449  63 
{*Message Y paired with a MAC computed with the help of X*} 
64 
"Hash[X] Y == { Hash{X,Y}, Y}" 

65 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35109
diff
changeset

66 
definition keysFor :: "msg set => key set" where 
23449  67 
{*Keys useful to decrypt elements of a message set*} 
68 
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" 

69 

70 

71 
subsubsection{*Inductive Definition of All Parts" of a Message*} 

72 

23755  73 
inductive_set 
74 
parts :: "msg set => msg set" 

75 
for H :: "msg set" 

76 
where 

23449  77 
Inj [intro]: "X \<in> H ==> X \<in> parts H" 
23755  78 
 Fst: "{X,Y} \<in> parts H ==> X \<in> parts H" 
79 
 Snd: "{X,Y} \<in> parts H ==> Y \<in> parts H" 

80 
 Body: "Crypt K X \<in> parts H ==> X \<in> parts H" 

23449  81 

82 
lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)" 

83 
apply auto 

36553  84 
apply (erule parts.induct) 
85 
apply (metis parts.Inj set_rev_mp) 

86 
apply (metis parts.Fst) 

87 
apply (metis parts.Snd) 

88 
by (metis parts.Body) 

23449  89 

90 
text{*Equations hold because constructors are injective.*} 

91 
lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)" 

39260  92 
by (metis agent.inject image_iff) 
23449  93 

36553  94 
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x \<in> A)" 
95 
by (metis image_iff msg.inject(4)) 

23449  96 

36553  97 
lemma Nonce_Key_image_eq [simp]: "Nonce x \<notin> Key`A" 
98 
by (metis image_iff msg.distinct(23)) 

23449  99 

100 

101 
subsubsection{*Inverse of keys *} 

102 

36553  103 
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K = K')" 
23449  104 
by (metis invKey) 
105 

106 

107 
subsection{*keysFor operator*} 

108 

109 
lemma keysFor_empty [simp]: "keysFor {} = {}" 

110 
by (unfold keysFor_def, blast) 

111 

112 
lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'" 

113 
by (unfold keysFor_def, blast) 

114 

115 
lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))" 

116 
by (unfold keysFor_def, blast) 

117 

118 
text{*Monotonicity*} 

119 
lemma keysFor_mono: "G \<subseteq> H ==> keysFor(G) \<subseteq> keysFor(H)" 

120 
by (unfold keysFor_def, blast) 

121 

122 
lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H" 

123 
by (unfold keysFor_def, auto) 

124 

125 
lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H" 

126 
by (unfold keysFor_def, auto) 

127 

128 
lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H" 

129 
by (unfold keysFor_def, auto) 

130 

131 
lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H" 

132 
by (unfold keysFor_def, auto) 

133 

134 
lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H" 

135 
by (unfold keysFor_def, auto) 

136 

137 
lemma keysFor_insert_MPair [simp]: "keysFor (insert {X,Y} H) = keysFor H" 

138 
by (unfold keysFor_def, auto) 

139 

43197  140 
lemma keysFor_insert_Crypt [simp]: 
23449  141 
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)" 
142 
by (unfold keysFor_def, auto) 

143 

144 
lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}" 

145 
by (unfold keysFor_def, auto) 

146 

147 
lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H ==> invKey K \<in> keysFor H" 

148 
by (unfold keysFor_def, blast) 

149 

150 

151 
subsection{*Inductive relation "parts"*} 

152 

153 
lemma MPair_parts: 

43197  154 
"[ {X,Y} \<in> parts H; 
23449  155 
[ X \<in> parts H; Y \<in> parts H ] ==> P ] ==> P" 
43197  156 
by (blast dest: parts.Fst parts.Snd) 
23449  157 

36553  158 
declare MPair_parts [elim!] parts.Body [dest!] 
23449  159 
text{*NB These two rules are UNSAFE in the formal sense, as they discard the 
43197  160 
compound message. They work well on THIS FILE. 
23449  161 
@{text MPair_parts} is left as SAFE because it speeds up proofs. 
162 
The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*} 

163 

164 
lemma parts_increasing: "H \<subseteq> parts(H)" 

165 
by blast 

166 

45605  167 
lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD] 
23449  168 

169 
lemma parts_empty [simp]: "parts{} = {}" 

170 
apply safe 

171 
apply (erule parts.induct) 

172 
apply blast+ 

173 
done 

174 

175 
lemma parts_emptyE [elim!]: "X\<in> parts{} ==> P" 

176 
by simp 

177 

178 
text{*WARNING: loops if H = {Y}, therefore must not be repeated!*} 

179 
lemma parts_singleton: "X\<in> parts H ==> \<exists>Y\<in>H. X\<in> parts {Y}" 

180 
apply (erule parts.induct) 

26807
4cd176ea28dc
Replaced blast by fast in proof of parts_singleton, since blast looped
berghofe
parents:
25710
diff
changeset

181 
apply fast+ 
23449  182 
done 
183 

184 

185 
subsubsection{*Unions *} 

186 

187 
lemma parts_Un_subset1: "parts(G) \<union> parts(H) \<subseteq> parts(G \<union> H)" 

188 
by (intro Un_least parts_mono Un_upper1 Un_upper2) 

189 

190 
lemma parts_Un_subset2: "parts(G \<union> H) \<subseteq> parts(G) \<union> parts(H)" 

191 
apply (rule subsetI) 

192 
apply (erule parts.induct, blast+) 

193 
done 

194 

195 
lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)" 

196 
by (intro equalityI parts_Un_subset1 parts_Un_subset2) 

197 

198 
lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H" 

199 
apply (subst insert_is_Un [of _ H]) 

200 
apply (simp only: parts_Un) 

201 
done 

202 

203 
lemma parts_insert2: 

204 
"parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H" 

25710
4cdf7de81e1b
Replaced refs by config params; finer critical section in mets method
paulson
parents:
25457
diff
changeset

205 
by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un) 
23449  206 

207 

208 
lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)" 

209 
by (intro UN_least parts_mono UN_upper) 

210 

211 
lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))" 

212 
apply (rule subsetI) 

213 
apply (erule parts.induct, blast+) 

214 
done 

215 

216 
lemma parts_UN [simp]: "parts(\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts(H x))" 

217 
by (intro equalityI parts_UN_subset1 parts_UN_subset2) 

218 

219 
text{*Added to simplify arguments to parts, analz and synth. 

220 
NOTE: the UN versions are no longer used!*} 

221 

222 

43197  223 
text{*This allows @{text blast} to simplify occurrences of 
23449  224 
@{term "parts(G\<union>H)"} in the assumption.*} 
43197  225 
lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 
23449  226 
declare in_parts_UnE [elim!] 
227 

228 
lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)" 

229 
by (blast intro: parts_mono [THEN [2] rev_subsetD]) 

230 

231 
subsubsection{*Idempotence and transitivity *} 

232 

233 
lemma parts_partsD [dest!]: "X\<in> parts (parts H) ==> X\<in> parts H" 

234 
by (erule parts.induct, blast+) 

235 

236 
lemma parts_idem [simp]: "parts (parts H) = parts H" 

237 
by blast 

238 

239 
lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)" 

43197  240 
apply (rule iffI) 
23449  241 
apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing) 
25710
4cdf7de81e1b
Replaced refs by config params; finer critical section in mets method
paulson
parents:
25457
diff
changeset

242 
apply (metis parts_idem parts_mono) 
23449  243 
done 
244 

245 
lemma parts_trans: "[ X\<in> parts G; G \<subseteq> parts H ] ==> X\<in> parts H" 

45503  246 
by (blast dest: parts_mono) 
23449  247 

46075
0054a9513b37
reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
blanchet
parents:
45970
diff
changeset

248 
lemma parts_cut: "[Y\<in> parts (insert X G); X\<in> parts H] ==> Y\<in> parts(G \<union> H)" 
0054a9513b37
reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
blanchet
parents:
45970
diff
changeset

249 
by (metis (no_types) Un_insert_left Un_insert_right insert_absorb le_supE 
0054a9513b37
reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
blanchet
parents:
45970
diff
changeset

250 
parts_Un parts_idem parts_increasing parts_trans) 
23449  251 

252 
subsubsection{*Rewrite rules for pulling out atomic messages *} 

253 

254 
lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset] 

255 

256 

257 
lemma parts_insert_Agent [simp]: 

258 
"parts (insert (Agent agt) H) = insert (Agent agt) (parts H)" 

43197  259 
apply (rule parts_insert_eq_I) 
260 
apply (erule parts.induct, auto) 

23449  261 
done 
262 

263 
lemma parts_insert_Nonce [simp]: 

264 
"parts (insert (Nonce N) H) = insert (Nonce N) (parts H)" 

43197  265 
apply (rule parts_insert_eq_I) 
266 
apply (erule parts.induct, auto) 

23449  267 
done 
268 

269 
lemma parts_insert_Number [simp]: 

270 
"parts (insert (Number N) H) = insert (Number N) (parts H)" 

43197  271 
apply (rule parts_insert_eq_I) 
272 
apply (erule parts.induct, auto) 

23449  273 
done 
274 

275 
lemma parts_insert_Key [simp]: 

276 
"parts (insert (Key K) H) = insert (Key K) (parts H)" 

43197  277 
apply (rule parts_insert_eq_I) 
278 
apply (erule parts.induct, auto) 

23449  279 
done 
280 

281 
lemma parts_insert_Hash [simp]: 

282 
"parts (insert (Hash X) H) = insert (Hash X) (parts H)" 

43197  283 
apply (rule parts_insert_eq_I) 
284 
apply (erule parts.induct, auto) 

23449  285 
done 
286 

287 
lemma parts_insert_Crypt [simp]: 

43197  288 
"parts (insert (Crypt K X) H) = 
23449  289 
insert (Crypt K X) (parts (insert X H))" 
290 
apply (rule equalityI) 

291 
apply (rule subsetI) 

292 
apply (erule parts.induct, auto) 

293 
apply (blast intro: parts.Body) 

294 
done 

295 

296 
lemma parts_insert_MPair [simp]: 

43197  297 
"parts (insert {X,Y} H) = 
23449  298 
insert {X,Y} (parts (insert X (insert Y H)))" 
299 
apply (rule equalityI) 

300 
apply (rule subsetI) 

301 
apply (erule parts.induct, auto) 

302 
apply (blast intro: parts.Fst parts.Snd)+ 

303 
done 

304 

305 
lemma parts_image_Key [simp]: "parts (Key`N) = Key`N" 

306 
apply auto 

307 
apply (erule parts.induct, auto) 

308 
done 

309 

310 
lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n > Nonce n \<notin> parts {msg}" 

43197  311 
apply (induct_tac "msg") 
23449  312 
apply (simp_all add: parts_insert2) 
313 
apply (metis Suc_n_not_le_n) 

314 
apply (metis le_trans linorder_linear) 

315 
done 

316 

317 
subsection{*Inductive relation "analz"*} 

318 

319 
text{*Inductive definition of "analz"  what can be broken down from a set of 

320 
messages, including keys. A form of downward closure. Pairs can 

321 
be taken apart; messages decrypted with known keys. *} 

322 

23755  323 
inductive_set 
324 
analz :: "msg set => msg set" 

325 
for H :: "msg set" 

326 
where 

23449  327 
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" 
23755  328 
 Fst: "{X,Y} \<in> analz H ==> X \<in> analz H" 
329 
 Snd: "{X,Y} \<in> analz H ==> Y \<in> analz H" 

43197  330 
 Decrypt [dest]: 
23449  331 
"[Crypt K X \<in> analz H; Key(invKey K): analz H] ==> X \<in> analz H" 
332 

333 

334 
text{*Monotonicity; Lemma 1 of Lowe's paper*} 

335 
lemma analz_mono: "G\<subseteq>H ==> analz(G) \<subseteq> analz(H)" 

336 
apply auto 

43197  337 
apply (erule analz.induct) 
338 
apply (auto dest: analz.Fst analz.Snd) 

23449  339 
done 
340 

341 
text{*Making it safe speeds up proofs*} 

342 
lemma MPair_analz [elim!]: 

43197  343 
"[ {X,Y} \<in> analz H; 
344 
[ X \<in> analz H; Y \<in> analz H ] ==> P 

23449  345 
] ==> P" 
346 
by (blast dest: analz.Fst analz.Snd) 

347 

348 
lemma analz_increasing: "H \<subseteq> analz(H)" 

349 
by blast 

350 

351 
lemma analz_subset_parts: "analz H \<subseteq> parts H" 

352 
apply (rule subsetI) 

353 
apply (erule analz.induct, blast+) 

354 
done 

355 

45605  356 
lemmas analz_into_parts = analz_subset_parts [THEN subsetD] 
23449  357 

45605  358 
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD] 
23449  359 

360 
lemma parts_analz [simp]: "parts (analz H) = parts H" 

361 
apply (rule equalityI) 

362 
apply (metis analz_subset_parts parts_subset_iff) 

363 
apply (metis analz_increasing parts_mono) 

364 
done 

365 

366 

367 
lemma analz_parts [simp]: "analz (parts H) = parts H" 

368 
apply auto 

369 
apply (erule analz.induct, auto) 

370 
done 

371 

45605  372 
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD] 
23449  373 

374 
subsubsection{*General equational properties *} 

375 

376 
lemma analz_empty [simp]: "analz{} = {}" 

377 
apply safe 

378 
apply (erule analz.induct, blast+) 

379 
done 

380 

43197  381 
text{*Converse fails: we can analz more from the union than from the 
23449  382 
separate parts, as a key in one might decrypt a message in the other*} 
383 
lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)" 

384 
by (intro Un_least analz_mono Un_upper1 Un_upper2) 

385 

386 
lemma analz_insert: "insert X (analz H) \<subseteq> analz(insert X H)" 

387 
by (blast intro: analz_mono [THEN [2] rev_subsetD]) 

388 

389 
subsubsection{*Rewrite rules for pulling out atomic messages *} 

390 

391 
lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert] 

392 

393 
lemma analz_insert_Agent [simp]: 

394 
"analz (insert (Agent agt) H) = insert (Agent agt) (analz H)" 

43197  395 
apply (rule analz_insert_eq_I) 
396 
apply (erule analz.induct, auto) 

23449  397 
done 
398 

399 
lemma analz_insert_Nonce [simp]: 

400 
"analz (insert (Nonce N) H) = insert (Nonce N) (analz H)" 

43197  401 
apply (rule analz_insert_eq_I) 
402 
apply (erule analz.induct, auto) 

23449  403 
done 
404 

405 
lemma analz_insert_Number [simp]: 

406 
"analz (insert (Number N) H) = insert (Number N) (analz H)" 

43197  407 
apply (rule analz_insert_eq_I) 
408 
apply (erule analz.induct, auto) 

23449  409 
done 
410 

411 
lemma analz_insert_Hash [simp]: 

412 
"analz (insert (Hash X) H) = insert (Hash X) (analz H)" 

43197  413 
apply (rule analz_insert_eq_I) 
414 
apply (erule analz.induct, auto) 

23449  415 
done 
416 

417 
text{*Can only pull out Keys if they are not needed to decrypt the rest*} 

43197  418 
lemma analz_insert_Key [simp]: 
419 
"K \<notin> keysFor (analz H) ==> 

23449  420 
analz (insert (Key K) H) = insert (Key K) (analz H)" 
421 
apply (unfold keysFor_def) 

43197  422 
apply (rule analz_insert_eq_I) 
423 
apply (erule analz.induct, auto) 

23449  424 
done 
425 

426 
lemma analz_insert_MPair [simp]: 

43197  427 
"analz (insert {X,Y} H) = 
23449  428 
insert {X,Y} (analz (insert X (insert Y H)))" 
429 
apply (rule equalityI) 

430 
apply (rule subsetI) 

431 
apply (erule analz.induct, auto) 

432 
apply (erule analz.induct) 

433 
apply (blast intro: analz.Fst analz.Snd)+ 

434 
done 

435 

436 
text{*Can pull out enCrypted message if the Key is not known*} 

437 
lemma analz_insert_Crypt: 

43197  438 
"Key (invKey K) \<notin> analz H 
23449  439 
==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)" 
43197  440 
apply (rule analz_insert_eq_I) 
441 
apply (erule analz.induct, auto) 

23449  442 

443 
done 

444 

43197  445 
lemma lemma1: "Key (invKey K) \<in> analz H ==> 
446 
analz (insert (Crypt K X) H) \<subseteq> 

447 
insert (Crypt K X) (analz (insert X H))" 

23449  448 
apply (rule subsetI) 
23755  449 
apply (erule_tac x = x in analz.induct, auto) 
23449  450 
done 
451 

43197  452 
lemma lemma2: "Key (invKey K) \<in> analz H ==> 
453 
insert (Crypt K X) (analz (insert X H)) \<subseteq> 

23449  454 
analz (insert (Crypt K X) H)" 
455 
apply auto 

23755  456 
apply (erule_tac x = x in analz.induct, auto) 
23449  457 
apply (blast intro: analz_insertI analz.Decrypt) 
458 
done 

459 

460 
lemma analz_insert_Decrypt: 

43197  461 
"Key (invKey K) \<in> analz H ==> 
462 
analz (insert (Crypt K X) H) = 

23449  463 
insert (Crypt K X) (analz (insert X H))" 
464 
by (intro equalityI lemma1 lemma2) 

465 

466 
text{*Case analysis: either the message is secure, or it is not! Effective, 

467 
but can cause subgoals to blow up! Use with @{text "split_if"}; apparently 

468 
@{text "split_tac"} does not cope with patterns such as @{term"analz (insert 

43197  469 
(Crypt K X) H)"} *} 
23449  470 
lemma analz_Crypt_if [simp]: 
43197  471 
"analz (insert (Crypt K X) H) = 
472 
(if (Key (invKey K) \<in> analz H) 

473 
then insert (Crypt K X) (analz (insert X H)) 

23449  474 
else insert (Crypt K X) (analz H))" 
475 
by (simp add: analz_insert_Crypt analz_insert_Decrypt) 

476 

477 

478 
text{*This rule supposes "for the sake of argument" that we have the key.*} 

479 
lemma analz_insert_Crypt_subset: 

43197  480 
"analz (insert (Crypt K X) H) \<subseteq> 
23449  481 
insert (Crypt K X) (analz (insert X H))" 
482 
apply (rule subsetI) 

483 
apply (erule analz.induct, auto) 

484 
done 

485 

486 

487 
lemma analz_image_Key [simp]: "analz (Key`N) = Key`N" 

488 
apply auto 

489 
apply (erule analz.induct, auto) 

490 
done 

491 

492 

493 
subsubsection{*Idempotence and transitivity *} 

494 

495 
lemma analz_analzD [dest!]: "X\<in> analz (analz H) ==> X\<in> analz H" 

496 
by (erule analz.induct, blast+) 

497 

498 
lemma analz_idem [simp]: "analz (analz H) = analz H" 

499 
by blast 

500 

501 
lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)" 

502 
apply (rule iffI) 

43197  503 
apply (iprover intro: subset_trans analz_increasing) 
504 
apply (frule analz_mono, simp) 

23449  505 
done 
506 

507 
lemma analz_trans: "[ X\<in> analz G; G \<subseteq> analz H ] ==> X\<in> analz H" 

508 
by (drule analz_mono, blast) 

509 

510 

36553  511 
declare analz_trans[intro] 
512 

23449  513 
lemma analz_cut: "[ Y\<in> analz (insert X H); X\<in> analz H ] ==> Y\<in> analz H" 
46075
0054a9513b37
reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
blanchet
parents:
45970
diff
changeset

514 
by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) 
23449  515 

516 
text{*This rewrite rule helps in the simplification of messages that involve 

517 
the forwarding of unknown components (X). Without it, removing occurrences 

518 
of X can be very complicated. *} 

519 
lemma analz_insert_eq: "X\<in> analz H ==> analz (insert X H) = analz H" 

520 
by (blast intro: analz_cut analz_insertI) 

521 

522 

523 
text{*A congruence rule for "analz" *} 

524 

525 
lemma analz_subset_cong: 

43197  526 
"[ analz G \<subseteq> analz G'; analz H \<subseteq> analz H' ] 
23449  527 
==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')" 
528 
apply simp 

529 
apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono) 

530 
done 

531 

532 

533 
lemma analz_cong: 

43197  534 
"[ analz G = analz G'; analz H = analz H' 
23449  535 
] ==> analz (G \<union> H) = analz (G' \<union> H')" 
43197  536 
by (intro equalityI analz_subset_cong, simp_all) 
23449  537 

538 
lemma analz_insert_cong: 

539 
"analz H = analz H' ==> analz(insert X H) = analz(insert X H')" 

540 
by (force simp only: insert_def intro!: analz_cong) 

541 

542 
text{*If there are no pairs or encryptions then analz does nothing*} 

543 
lemma analz_trivial: 

544 
"[ \<forall>X Y. {X,Y} \<notin> H; \<forall>X K. Crypt K X \<notin> H ] ==> analz H = H" 

545 
apply safe 

546 
apply (erule analz.induct, blast+) 

547 
done 

548 

549 
text{*These two are obsolete (with a single Spy) but cost little to prove...*} 

550 
lemma analz_UN_analz_lemma: 

551 
"X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)" 

552 
apply (erule analz.induct) 

553 
apply (blast intro: analz_mono [THEN [2] rev_subsetD])+ 

554 
done 

555 

556 
lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)" 

557 
by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD]) 

558 

559 

560 
subsection{*Inductive relation "synth"*} 

561 

562 
text{*Inductive definition of "synth"  what can be built up from a set of 

563 
messages. A form of upward closure. Pairs can be built, messages 

564 
encrypted with known keys. Agent names are public domain. 

565 
Numbers can be guessed, but Nonces cannot be. *} 

566 

23755  567 
inductive_set 
568 
synth :: "msg set => msg set" 

569 
for H :: "msg set" 

570 
where 

23449  571 
Inj [intro]: "X \<in> H ==> X \<in> synth H" 
23755  572 
 Agent [intro]: "Agent agt \<in> synth H" 
573 
 Number [intro]: "Number n \<in> synth H" 

574 
 Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H" 

575 
 MPair [intro]: "[X \<in> synth H; Y \<in> synth H] ==> {X,Y} \<in> synth H" 

576 
 Crypt [intro]: "[X \<in> synth H; Key(K) \<in> H] ==> Crypt K X \<in> synth H" 

23449  577 

578 
text{*Monotonicity*} 

579 
lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)" 

43197  580 
by (auto, erule synth.induct, auto) 
23449  581 

43197  582 
text{*NO @{text Agent_synth}, as any Agent name can be synthesized. 
23449  583 
The same holds for @{term Number}*} 
584 
inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H" 

585 
inductive_cases Key_synth [elim!]: "Key K \<in> synth H" 

586 
inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H" 

587 
inductive_cases MPair_synth [elim!]: "{X,Y} \<in> synth H" 

588 
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H" 

589 

590 

591 
lemma synth_increasing: "H \<subseteq> synth(H)" 

592 
by blast 

593 

594 
subsubsection{*Unions *} 

595 

43197  596 
text{*Converse fails: we can synth more from the union than from the 
23449  597 
separate parts, building a compound message using elements of each.*} 
598 
lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)" 

599 
by (intro Un_least synth_mono Un_upper1 Un_upper2) 

600 

601 
lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)" 

602 
by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono) 

603 

604 
subsubsection{*Idempotence and transitivity *} 

605 

606 
lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H" 

607 
by (erule synth.induct, blast+) 

608 

609 
lemma synth_idem: "synth (synth H) = synth H" 

610 
by blast 

611 

612 
lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)" 

613 
apply (rule iffI) 

43197  614 
apply (iprover intro: subset_trans synth_increasing) 
615 
apply (frule synth_mono, simp add: synth_idem) 

23449  616 
done 
617 

618 
lemma synth_trans: "[ X\<in> synth G; G \<subseteq> synth H ] ==> X\<in> synth H" 

619 
by (drule synth_mono, blast) 

620 

621 
lemma synth_cut: "[ Y\<in> synth (insert X H); X\<in> synth H ] ==> Y\<in> synth H" 

622 
by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono) 

623 

624 
lemma Agent_synth [simp]: "Agent A \<in> synth H" 

625 
by blast 

626 

627 
lemma Number_synth [simp]: "Number n \<in> synth H" 

628 
by blast 

629 

630 
lemma Nonce_synth_eq [simp]: "(Nonce N \<in> synth H) = (Nonce N \<in> H)" 

631 
by blast 

632 

633 
lemma Key_synth_eq [simp]: "(Key K \<in> synth H) = (Key K \<in> H)" 

634 
by blast 

635 

636 
lemma Crypt_synth_eq [simp]: 

637 
"Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)" 

638 
by blast 

639 

640 

43197  641 
lemma keysFor_synth [simp]: 
23449  642 
"keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}" 
643 
by (unfold keysFor_def, blast) 

644 

645 

646 
subsubsection{*Combinations of parts, analz and synth *} 

647 

648 
lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H" 

649 
apply (rule equalityI) 

650 
apply (rule subsetI) 

651 
apply (erule parts.induct) 

652 
apply (metis UnCI) 

653 
apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Fst parts_increasing) 

654 
apply (metis MPair_synth UnCI UnE insert_absorb insert_subset parts.Snd parts_increasing) 

655 
apply (metis Body Crypt_synth UnCI UnE insert_absorb insert_subset parts_increasing) 

656 
apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing) 

657 
done 

658 

659 
lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)" 

45503  660 
apply (rule equalityI) 
23449  661 
apply (metis analz_idem analz_subset_cong order_eq_refl) 
662 
apply (metis analz_increasing analz_subset_cong order_eq_refl) 

663 
done 

664 

36553  665 
declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro] 
666 

23449  667 
lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G" 
668 
apply (rule equalityI) 

669 
apply (rule subsetI) 

670 
apply (erule analz.induct) 

671 
apply (metis UnCI UnE Un_commute analz.Inj) 

45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45605
diff
changeset

672 
apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj) 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45605
diff
changeset

673 
apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd) 
23449  674 
apply (blast intro: analz.Decrypt) 
24759  675 
apply blast 
23449  676 
done 
677 

678 
lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H" 

36553  679 
proof  
36911  680 
have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)" by (metis Un_commute analz_synth_Un) 
681 
hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> {})" by (metis Un_empty_right) 

682 
hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)" by (metis Un_empty_right) 

683 
hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)" by (metis Un_commute) 

36553  684 
thus "analz (synth H) = analz H \<union> synth H" by metis 
23449  685 
qed 
686 

687 

688 
subsubsection{*For reasoning about the Fake rule in traces *} 

689 

45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45605
diff
changeset

690 
lemma parts_insert_subset_Un: "X \<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H" 
36553  691 
proof  
692 
assume "X \<in> G" 

45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45605
diff
changeset

693 
hence "\<forall>x\<^isub>1. G \<subseteq> x\<^isub>1 \<longrightarrow> X \<in> x\<^isub>1 " by auto 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45605
diff
changeset

694 
hence "\<forall>x\<^isub>1. X \<in> G \<union> x\<^isub>1" by (metis Un_upper1) 
36911  695 
hence "insert X H \<subseteq> G \<union> H" by (metis Un_upper2 insert_subset) 
696 
hence "parts (insert X H) \<subseteq> parts (G \<union> H)" by (metis parts_mono) 

697 
thus "parts (insert X H) \<subseteq> parts G \<union> parts H" by (metis parts_Un) 

23449  698 
qed 
699 

700 
lemma Fake_parts_insert: 

43197  701 
"X \<in> synth (analz H) ==> 
23449  702 
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H" 
36553  703 
proof  
704 
assume A1: "X \<in> synth (analz H)" 

705 
have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))" 

706 
by (metis analz_idem analz_synth) 

707 
have F2: "\<forall>x\<^isub>1. parts x\<^isub>1 \<union> synth (analz x\<^isub>1) = parts (synth (analz x\<^isub>1))" 

708 
by (metis parts_analz parts_synth) 

45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45605
diff
changeset

709 
have F3: "X \<in> synth (analz H)" using A1 by metis 
36553  710 
have "\<forall>x\<^isub>2 x\<^isub>1\<Colon>msg set. x\<^isub>1 \<le> sup x\<^isub>1 x\<^isub>2" by (metis inf_sup_ord(3)) 
711 
hence F4: "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" by (metis analz_synth) 

45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45605
diff
changeset

712 
have F5: "X \<in> synth (analz H)" using F3 by metis 
36553  713 
have "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> synth (analz x\<^isub>1) 
714 
\<longrightarrow> analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)" 

715 
using F1 by (metis subset_Un_eq) 

716 
hence F6: "\<forall>x\<^isub>1. analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)" 

717 
by (metis synth_increasing) 

718 
have "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" using F4 by (metis analz_subset_iff) 

719 
hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> analz (synth (analz x\<^isub>1))" by (metis analz_subset_iff) 

720 
hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> synth (analz x\<^isub>1)" using F6 by metis 

721 
hence "H \<subseteq> synth (analz H)" by metis 

722 
hence "H \<subseteq> synth (analz H) \<and> X \<in> synth (analz H)" using F5 by metis 

723 
hence "insert X H \<subseteq> synth (analz H)" by (metis insert_subset) 

724 
hence "parts (insert X H) \<subseteq> parts (synth (analz H))" by (metis parts_mono) 

725 
hence "parts (insert X H) \<subseteq> parts H \<union> synth (analz H)" using F2 by metis 

726 
thus "parts (insert X H) \<subseteq> synth (analz H) \<union> parts H" by (metis Un_commute) 

23449  727 
qed 
728 

729 
lemma Fake_parts_insert_in_Un: 

43197  730 
"[Z \<in> parts (insert X H); X: synth (analz H)] 
45505  731 
==> Z \<in> synth (analz H) \<union> parts H" 
36553  732 
by (blast dest: Fake_parts_insert [THEN subsetD, dest]) 
23449  733 

45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45605
diff
changeset

734 
declare synth_mono [intro] 
36553  735 

23449  736 
lemma Fake_analz_insert: 
36553  737 
"X \<in> synth (analz G) ==> 
23449  738 
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)" 
36553  739 
by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un 
740 
analz_mono analz_synth_Un insert_absorb) 

23449  741 

742 
lemma Fake_analz_insert_simpler: 

43197  743 
"X \<in> synth (analz G) ==> 
23449  744 
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)" 
745 
apply (rule subsetI) 

746 
apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ") 

747 
apply (metis Un_commute analz_analz_Un analz_synth_Un) 

39260  748 
by (metis Un_upper1 Un_upper2 analz_mono insert_absorb insert_subset) 
23449  749 

750 
end 