author  blanchet 
Fri, 14 May 2010 11:24:49 +0200  
changeset 36911  0e2818493775 
parent 36580  d23a3a4d1849 
child 39260  f94c53d9b8fb 
permissions  rwrr 
23449  1 
(* Title: HOL/MetisTest/Message.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 

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

4 
Testing the metis method. 
23449  5 
*) 
6 

36553  7 
theory Message 
8 
imports Main 

9 
begin 

23449  10 

11 
lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A" 

36911  12 
by (metis Un_commute Un_left_absorb) 
23449  13 

14 
types 

15 
key = nat 

16 

17 
consts 

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

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

20 

21 
specification (invKey) 

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

23 
invKey_symmetric: "all_symmetric > invKey = id" 

36553  24 
by (metis id_apply) 
23449  25 

26 

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

28 
is the private key and vice versa*} 

29 

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

30 
definition symKeys :: "key set" where 
23449  31 
"symKeys == {K. invKey K = K}" 
32 

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

34 
agent = Server  Friend nat  Spy 

35 

36 
datatype 

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

37 
msg = Agent agent {*Agent names*} 
23449  38 
 Number nat {*Ordinary integers, timestamps, ...*} 
39 
 Nonce nat {*Unguessable nonces*} 

40 
 Key key {*Crypto keys*} 

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

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

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

43 
 Crypt key msg {*Encryption, public or sharedkey*} 
23449  44 

45 

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

47 
syntax 

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

50 
syntax (xsymbols) 

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

53 
translations 

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

35054  55 
"{x, y}" == "CONST MPair x y" 
23449  56 

57 

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

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

61 

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

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

65 

66 

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

68 

23755  69 
inductive_set 
70 
parts :: "msg set => msg set" 

71 
for H :: "msg set" 

72 
where 

23449  73 
Inj [intro]: "X \<in> H ==> X \<in> parts H" 
23755  74 
 Fst: "{X,Y} \<in> parts H ==> X \<in> parts H" 
75 
 Snd: "{X,Y} \<in> parts H ==> Y \<in> parts H" 

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

23449  77 

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

79 
apply auto 

36553  80 
apply (erule parts.induct) 
81 
apply (metis parts.Inj set_rev_mp) 

82 
apply (metis parts.Fst) 

83 
apply (metis parts.Snd) 

84 
by (metis parts.Body) 

23449  85 

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

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

36553  88 
by (metis agent.inject imageI image_iff) 
23449  89 

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

23449  92 

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

23449  95 

96 

97 
subsubsection{*Inverse of keys *} 

98 

36553  99 
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K = K')" 
23449  100 
by (metis invKey) 
101 

102 

103 
subsection{*keysFor operator*} 

104 

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

106 
by (unfold keysFor_def, blast) 

107 

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

109 
by (unfold keysFor_def, blast) 

110 

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

112 
by (unfold keysFor_def, blast) 

113 

114 
text{*Monotonicity*} 

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

116 
by (unfold keysFor_def, blast) 

117 

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

119 
by (unfold keysFor_def, auto) 

120 

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

122 
by (unfold keysFor_def, auto) 

123 

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

125 
by (unfold keysFor_def, auto) 

126 

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

128 
by (unfold keysFor_def, auto) 

129 

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

131 
by (unfold keysFor_def, auto) 

132 

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

134 
by (unfold keysFor_def, auto) 

135 

136 
lemma keysFor_insert_Crypt [simp]: 

137 
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)" 

138 
by (unfold keysFor_def, auto) 

139 

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

141 
by (unfold keysFor_def, auto) 

142 

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

144 
by (unfold keysFor_def, blast) 

145 

146 

147 
subsection{*Inductive relation "parts"*} 

148 

149 
lemma MPair_parts: 

150 
"[ {X,Y} \<in> parts H; 

151 
[ X \<in> parts H; Y \<in> parts H ] ==> P ] ==> P" 

152 
by (blast dest: parts.Fst parts.Snd) 

153 

36553  154 
declare MPair_parts [elim!] parts.Body [dest!] 
23449  155 
text{*NB These two rules are UNSAFE in the formal sense, as they discard the 
156 
compound message. They work well on THIS FILE. 

157 
@{text MPair_parts} is left as SAFE because it speeds up proofs. 

158 
The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*} 

159 

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

161 
by blast 

162 

163 
lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard] 

164 

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

166 
apply safe 

167 
apply (erule parts.induct) 

168 
apply blast+ 

169 
done 

170 

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

172 
by simp 

173 

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

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

176 
apply (erule parts.induct) 

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

177 
apply fast+ 
23449  178 
done 
179 

180 

181 
subsubsection{*Unions *} 

182 

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

184 
by (intro Un_least parts_mono Un_upper1 Un_upper2) 

185 

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

187 
apply (rule subsetI) 

188 
apply (erule parts.induct, blast+) 

189 
done 

190 

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

192 
by (intro equalityI parts_Un_subset1 parts_Un_subset2) 

193 

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

195 
apply (subst insert_is_Un [of _ H]) 

196 
apply (simp only: parts_Un) 

197 
done 

198 

199 
lemma parts_insert2: 

200 
"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

201 
by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un) 
23449  202 

203 

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

205 
by (intro UN_least parts_mono UN_upper) 

206 

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

208 
apply (rule subsetI) 

209 
apply (erule parts.induct, blast+) 

210 
done 

211 

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

213 
by (intro equalityI parts_UN_subset1 parts_UN_subset2) 

214 

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

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

217 

218 

219 
text{*This allows @{text blast} to simplify occurrences of 

220 
@{term "parts(G\<union>H)"} in the assumption.*} 

221 
lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 

222 
declare in_parts_UnE [elim!] 

223 

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

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

226 

227 
subsubsection{*Idempotence and transitivity *} 

228 

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

230 
by (erule parts.induct, blast+) 

231 

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

233 
by blast 

234 

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

236 
apply (rule iffI) 

237 
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

238 
apply (metis parts_idem parts_mono) 
23449  239 
done 
240 

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

242 
by (blast dest: parts_mono); 

243 

244 
lemma parts_cut: "[Y\<in> parts(insert X G); X\<in> parts H] ==> Y\<in> parts(G \<union> H)" 

35095  245 
by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI) 
23449  246 

247 

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

249 

250 
lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset] 

251 

252 

253 
lemma parts_insert_Agent [simp]: 

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

255 
apply (rule parts_insert_eq_I) 

256 
apply (erule parts.induct, auto) 

257 
done 

258 

259 
lemma parts_insert_Nonce [simp]: 

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

261 
apply (rule parts_insert_eq_I) 

262 
apply (erule parts.induct, auto) 

263 
done 

264 

265 
lemma parts_insert_Number [simp]: 

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

267 
apply (rule parts_insert_eq_I) 

268 
apply (erule parts.induct, auto) 

269 
done 

270 

271 
lemma parts_insert_Key [simp]: 

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

273 
apply (rule parts_insert_eq_I) 

274 
apply (erule parts.induct, auto) 

275 
done 

276 

277 
lemma parts_insert_Hash [simp]: 

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

279 
apply (rule parts_insert_eq_I) 

280 
apply (erule parts.induct, auto) 

281 
done 

282 

283 
lemma parts_insert_Crypt [simp]: 

284 
"parts (insert (Crypt K X) H) = 

285 
insert (Crypt K X) (parts (insert X H))" 

286 
apply (rule equalityI) 

287 
apply (rule subsetI) 

288 
apply (erule parts.induct, auto) 

289 
apply (blast intro: parts.Body) 

290 
done 

291 

292 
lemma parts_insert_MPair [simp]: 

293 
"parts (insert {X,Y} H) = 

294 
insert {X,Y} (parts (insert X (insert Y H)))" 

295 
apply (rule equalityI) 

296 
apply (rule subsetI) 

297 
apply (erule parts.induct, auto) 

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

299 
done 

300 

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

302 
apply auto 

303 
apply (erule parts.induct, auto) 

304 
done 

305 

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

307 
apply (induct_tac "msg") 

308 
apply (simp_all add: parts_insert2) 

309 
apply (metis Suc_n_not_le_n) 

310 
apply (metis le_trans linorder_linear) 

311 
done 

312 

313 
subsection{*Inductive relation "analz"*} 

314 

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

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

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

318 

23755  319 
inductive_set 
320 
analz :: "msg set => msg set" 

321 
for H :: "msg set" 

322 
where 

23449  323 
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" 
23755  324 
 Fst: "{X,Y} \<in> analz H ==> X \<in> analz H" 
325 
 Snd: "{X,Y} \<in> analz H ==> Y \<in> analz H" 

326 
 Decrypt [dest]: 

23449  327 
"[Crypt K X \<in> analz H; Key(invKey K): analz H] ==> X \<in> analz H" 
328 

329 

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

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

332 
apply auto 

333 
apply (erule analz.induct) 

334 
apply (auto dest: analz.Fst analz.Snd) 

335 
done 

336 

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

338 
lemma MPair_analz [elim!]: 

339 
"[ {X,Y} \<in> analz H; 

340 
[ X \<in> analz H; Y \<in> analz H ] ==> P 

341 
] ==> P" 

342 
by (blast dest: analz.Fst analz.Snd) 

343 

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

345 
by blast 

346 

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

348 
apply (rule subsetI) 

349 
apply (erule analz.induct, blast+) 

350 
done 

351 

352 
lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard] 

353 

354 
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard] 

355 

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

357 
apply (rule equalityI) 

358 
apply (metis analz_subset_parts parts_subset_iff) 

359 
apply (metis analz_increasing parts_mono) 

360 
done 

361 

362 

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

364 
apply auto 

365 
apply (erule analz.induct, auto) 

366 
done 

367 

368 
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard] 

369 

370 
subsubsection{*General equational properties *} 

371 

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

373 
apply safe 

374 
apply (erule analz.induct, blast+) 

375 
done 

376 

377 
text{*Converse fails: we can analz more from the union than from the 

378 
separate parts, as a key in one might decrypt a message in the other*} 

379 
lemma analz_Un: "analz(G) \<union> analz(H) \<subseteq> analz(G \<union> H)" 

380 
by (intro Un_least analz_mono Un_upper1 Un_upper2) 

381 

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

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

384 

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

386 

387 
lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert] 

388 

389 
lemma analz_insert_Agent [simp]: 

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

391 
apply (rule analz_insert_eq_I) 

392 
apply (erule analz.induct, auto) 

393 
done 

394 

395 
lemma analz_insert_Nonce [simp]: 

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

397 
apply (rule analz_insert_eq_I) 

398 
apply (erule analz.induct, auto) 

399 
done 

400 

401 
lemma analz_insert_Number [simp]: 

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

403 
apply (rule analz_insert_eq_I) 

404 
apply (erule analz.induct, auto) 

405 
done 

406 

407 
lemma analz_insert_Hash [simp]: 

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

409 
apply (rule analz_insert_eq_I) 

410 
apply (erule analz.induct, auto) 

411 
done 

412 

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

414 
lemma analz_insert_Key [simp]: 

415 
"K \<notin> keysFor (analz H) ==> 

416 
analz (insert (Key K) H) = insert (Key K) (analz H)" 

417 
apply (unfold keysFor_def) 

418 
apply (rule analz_insert_eq_I) 

419 
apply (erule analz.induct, auto) 

420 
done 

421 

422 
lemma analz_insert_MPair [simp]: 

423 
"analz (insert {X,Y} H) = 

424 
insert {X,Y} (analz (insert X (insert Y H)))" 

425 
apply (rule equalityI) 

426 
apply (rule subsetI) 

427 
apply (erule analz.induct, auto) 

428 
apply (erule analz.induct) 

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

430 
done 

431 

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

433 
lemma analz_insert_Crypt: 

434 
"Key (invKey K) \<notin> analz H 

435 
==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)" 

436 
apply (rule analz_insert_eq_I) 

437 
apply (erule analz.induct, auto) 

438 

439 
done 

440 

441 
lemma lemma1: "Key (invKey K) \<in> analz H ==> 

442 
analz (insert (Crypt K X) H) \<subseteq> 

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

444 
apply (rule subsetI) 

23755  445 
apply (erule_tac x = x in analz.induct, auto) 
23449  446 
done 
447 

448 
lemma lemma2: "Key (invKey K) \<in> analz H ==> 

449 
insert (Crypt K X) (analz (insert X H)) \<subseteq> 

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

451 
apply auto 

23755  452 
apply (erule_tac x = x in analz.induct, auto) 
23449  453 
apply (blast intro: analz_insertI analz.Decrypt) 
454 
done 

455 

456 
lemma analz_insert_Decrypt: 

457 
"Key (invKey K) \<in> analz H ==> 

458 
analz (insert (Crypt K X) H) = 

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

460 
by (intro equalityI lemma1 lemma2) 

461 

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

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

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

465 
(Crypt K X) H)"} *} 

466 
lemma analz_Crypt_if [simp]: 

467 
"analz (insert (Crypt K X) H) = 

468 
(if (Key (invKey K) \<in> analz H) 

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

470 
else insert (Crypt K X) (analz H))" 

471 
by (simp add: analz_insert_Crypt analz_insert_Decrypt) 

472 

473 

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

475 
lemma analz_insert_Crypt_subset: 

476 
"analz (insert (Crypt K X) H) \<subseteq> 

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

478 
apply (rule subsetI) 

479 
apply (erule analz.induct, auto) 

480 
done 

481 

482 

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

484 
apply auto 

485 
apply (erule analz.induct, auto) 

486 
done 

487 

488 

489 
subsubsection{*Idempotence and transitivity *} 

490 

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

492 
by (erule analz.induct, blast+) 

493 

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

495 
by blast 

496 

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

498 
apply (rule iffI) 

499 
apply (iprover intro: subset_trans analz_increasing) 

500 
apply (frule analz_mono, simp) 

501 
done 

502 

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

504 
by (drule analz_mono, blast) 

505 

506 

36553  507 
declare analz_trans[intro] 
508 

23449  509 
lemma analz_cut: "[ Y\<in> analz (insert X H); X\<in> analz H ] ==> Y\<in> analz H" 
510 
(*TOO SLOW 

511 
by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) {*317s*} 

512 
??*) 

513 
by (erule analz_trans, blast) 

514 

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: 

526 
"[ analz G \<subseteq> analz G'; analz H \<subseteq> analz H' ] 

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: 

534 
"[ analz G = analz G'; analz H = analz H' 

535 
] ==> analz (G \<union> H) = analz (G' \<union> H')" 

536 
by (intro equalityI analz_subset_cong, simp_all) 

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)" 

580 
by (auto, erule synth.induct, auto) 

581 

582 
text{*NO @{text Agent_synth}, as any Agent name can be synthesized. 

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 

596 
text{*Converse fails: we can synth more from the union than from the 

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) 

614 
apply (iprover intro: subset_trans synth_increasing) 

615 
apply (frule synth_mono, simp add: synth_idem) 

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 
(*TOO SLOW 

623 
by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono) 

624 
*) 

625 
by (erule synth_trans, blast) 

626 

627 

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

629 
by blast 

630 

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

632 
by blast 

633 

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

635 
by blast 

636 

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

638 
by blast 

639 

640 
lemma Crypt_synth_eq [simp]: 

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

642 
by blast 

643 

644 

645 
lemma keysFor_synth [simp]: 

646 
"keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}" 

647 
by (unfold keysFor_def, blast) 

648 

649 

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

651 

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

653 
apply (rule equalityI) 

654 
apply (rule subsetI) 

655 
apply (erule parts.induct) 

656 
apply (metis UnCI) 

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

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

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

660 
apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing) 

661 
done 

662 

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

664 
apply (rule equalityI); 

665 
apply (metis analz_idem analz_subset_cong order_eq_refl) 

666 
apply (metis analz_increasing analz_subset_cong order_eq_refl) 

667 
done 

668 

36553  669 
declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro] 
670 

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

673 
apply (rule subsetI) 

674 
apply (erule analz.induct) 

675 
apply (metis UnCI UnE Un_commute analz.Inj) 

35095  676 
apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj mem_def) 
677 
apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd mem_def) 

23449  678 
apply (blast intro: analz.Decrypt) 
24759  679 
apply blast 
23449  680 
done 
681 

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

36553  683 
proof  
36911  684 
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) 
685 
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) 

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

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

36553  688 
thus "analz (synth H) = analz H \<union> synth H" by metis 
23449  689 
qed 
690 

691 

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

693 

694 
lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H" 

36553  695 
proof  
696 
assume "X \<in> G" 

36911  697 
hence "G X" by (metis mem_def) 
698 
hence "\<forall>x\<^isub>1. G \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 X" by (metis predicate1D) 

699 
hence "\<forall>x\<^isub>1. (G \<union> x\<^isub>1) X" by (metis Un_upper1) 

700 
hence "\<forall>x\<^isub>1. X \<in> G \<union> x\<^isub>1" by (metis mem_def) 

701 
hence "insert X H \<subseteq> G \<union> H" by (metis Un_upper2 insert_subset) 

702 
hence "parts (insert X H) \<subseteq> parts (G \<union> H)" by (metis parts_mono) 

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

23449  704 
qed 
705 

706 
lemma Fake_parts_insert: 

707 
"X \<in> synth (analz H) ==> 

708 
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H" 

36553  709 
proof  
710 
assume A1: "X \<in> synth (analz H)" 

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

712 
by (metis analz_idem analz_synth) 

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

714 
by (metis parts_analz parts_synth) 

715 
have F3: "synth (analz H) X" using A1 by (metis mem_def) 

716 
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)) 

717 
hence F4: "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" by (metis analz_synth) 

718 
have F5: "X \<in> synth (analz H)" using F3 by (metis mem_def) 

719 
have "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> synth (analz x\<^isub>1) 

720 
\<longrightarrow> analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)" 

721 
using F1 by (metis subset_Un_eq) 

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

723 
by (metis synth_increasing) 

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

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

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

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

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

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

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

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

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

23449  733 
qed 
734 

735 
lemma Fake_parts_insert_in_Un: 

736 
"[Z \<in> parts (insert X H); X: synth (analz H)] 

737 
==> Z \<in> synth (analz H) \<union> parts H"; 

36553  738 
by (blast dest: Fake_parts_insert [THEN subsetD, dest]) 
23449  739 

36553  740 
declare analz_mono [intro] synth_mono [intro] 
741 

23449  742 
lemma Fake_analz_insert: 
36553  743 
"X \<in> synth (analz G) ==> 
23449  744 
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)" 
36553  745 
by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un 
746 
analz_mono analz_synth_Un insert_absorb) 

23449  747 

36553  748 
(* Simpler problems? BUT METIS CAN'T PROVE THE LAST STEP 
23449  749 
lemma Fake_analz_insert_simpler: 
36553  750 
"X \<in> synth (analz G) ==> 
23449  751 
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)" 
752 
apply (rule subsetI) 

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

754 
apply (metis Un_commute analz_analz_Un analz_synth_Un) 

755 
apply (metis Un_commute Un_upper1 Un_upper2 analz_cut analz_increasing analz_mono insert_absorb insert_mono insert_subset) 

756 
done 

757 
*) 

758 

759 
end 