author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45605  a89b4bc311a5 
child 51702  dcfab8e87621 
permissions  rwrr 
33028  1 
(* Title: HOL/SET_Protocol/Message_SET.thy 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32149
diff
changeset

2 
Author: Giampaolo Bella 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32149
diff
changeset

3 
Author: Fabio Massacci 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32149
diff
changeset

4 
Author: Lawrence C Paulson 
14199  5 
*) 
6 

7 
header{*The Message Theory, Modified for SET*} 

8 

33028  9 
theory Message_SET 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
36866
diff
changeset

10 
imports Main "~~/src/HOL/Library/Nat_Bijection" 
25592  11 
begin 
14199  12 

13 
subsection{*General Lemmas*} 

14 

15 
text{*Needed occasionally with @{text spy_analz_tac}, e.g. in 

16 
@{text analz_insert_Key_newK}*} 

17 

18 
lemma Un_absorb3 [simp] : "A \<union> (B \<union> A) = B \<union> A" 

19 
by blast 

20 

21 
text{*Collapses redundant cases in the huge protocol proofs*} 

22 
lemmas disj_simps = disj_comms disj_left_absorb disj_assoc 

23 

24 
text{*Effective with assumptions like @{term "K \<notin> range pubK"} and 

25 
@{term "K \<notin> invKey`range pubK"}*} 

26 
lemma notin_image_iff: "(y \<notin> f`I) = (\<forall>i\<in>I. f i \<noteq> y)" 

27 
by blast 

28 

29 
text{*Effective with the assumption @{term "KK \<subseteq>  (range(invKey o pubK))"} *} 

30 
lemma disjoint_image_iff: "(A <=  (f`I)) = (\<forall>i\<in>I. f i \<notin> A)" 

31 
by blast 

32 

33 

34 

42463  35 
type_synonym key = nat 
14199  36 

37 
consts 

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

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

40 

41 
specification (invKey) 

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

43 
invKey_symmetric: "all_symmetric > invKey = id" 

44 
by (rule exI [of _ id], auto) 

45 

46 

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

48 
is the private key and vice versa*} 

49 

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

50 
definition symKeys :: "key set" where 
14199  51 
"symKeys == {K. invKey K = K}" 
52 

53 
text{*Agents. We allow any number of certification authorities, cardholders 

54 
merchants, and payment gateways.*} 

55 
datatype 

56 
agent = CA nat  Cardholder nat  Merchant nat  PG nat  Spy 

57 

58 
text{*Messages*} 

59 
datatype 

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

60 
msg = Agent agent {*Agent names*} 
14199  61 
 Number nat {*Ordinary integers, timestamps, ...*} 
62 
 Nonce nat {*Unguessable nonces*} 

63 
 Pan nat {*Unguessable Primary Account Numbers (??)*} 

64 
 Key key {*Crypto keys*} 

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

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

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

67 
 Crypt key msg {*Encryption, public or sharedkey*} 
14199  68 

69 

70 
(*Concrete syntax: messages appear as {A,B,NA}, etc...*) 

71 
syntax 

35068  72 
"_MTuple" :: "['a, args] => 'a * 'b" ("(2{_,/ _})") 
14199  73 

74 
syntax (xsymbols) 

35068  75 
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") 
14199  76 

77 
translations 

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

35068  79 
"{x, y}" == "CONST MPair x y" 
14199  80 

81 

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

82 
definition nat_of_agent :: "agent => nat" where 
35703
29cb504abbb5
convert SET_Protocol to use Nat_Bijection library
huffman
parents:
35416
diff
changeset

83 
"nat_of_agent == agent_case (curry prod_encode 0) 
29cb504abbb5
convert SET_Protocol to use Nat_Bijection library
huffman
parents:
35416
diff
changeset

84 
(curry prod_encode 1) 
29cb504abbb5
convert SET_Protocol to use Nat_Bijection library
huffman
parents:
35416
diff
changeset

85 
(curry prod_encode 2) 
29cb504abbb5
convert SET_Protocol to use Nat_Bijection library
huffman
parents:
35416
diff
changeset

86 
(curry prod_encode 3) 
29cb504abbb5
convert SET_Protocol to use Nat_Bijection library
huffman
parents:
35416
diff
changeset

87 
(prod_encode (4,0))" 
14199  88 
{*maps each agent to a unique natural number, for specifications*} 
89 

90 
text{*The function is indeed injective*} 

91 
lemma inj_nat_of_agent: "inj nat_of_agent" 

35703
29cb504abbb5
convert SET_Protocol to use Nat_Bijection library
huffman
parents:
35416
diff
changeset

92 
by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split) 
14199  93 

94 

36866  95 
definition 
14199  96 
(*Keys useful to decrypt elements of a message set*) 
97 
keysFor :: "msg set => key set" 

36866  98 
where "keysFor H = invKey ` {K. \<exists>X. Crypt K X \<in> H}" 
14199  99 

100 
subsubsection{*Inductive definition of all "parts" of a message.*} 

101 

23755  102 
inductive_set 
103 
parts :: "msg set => msg set" 

104 
for H :: "msg set" 

105 
where 

14199  106 
Inj [intro]: "X \<in> H ==> X \<in> parts H" 
23755  107 
 Fst: "{X,Y} \<in> parts H ==> X \<in> parts H" 
108 
 Snd: "{X,Y} \<in> parts H ==> Y \<in> parts H" 

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

14199  110 

111 

112 
(*Monotonicity*) 

113 
lemma parts_mono: "G<=H ==> parts(G) <= parts(H)" 

114 
apply auto 

115 
apply (erule parts.induct) 

116 
apply (auto dest: Fst Snd Body) 

117 
done 

118 

119 

120 
subsubsection{*Inverse of keys*} 

121 

122 
(*Equations hold because constructors are injective; cannot prove for all f*) 

123 
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)" 

124 
by auto 

125 

126 
lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)" 

127 
by auto 

128 

129 
lemma Cardholder_image_eq [simp]: "(Cardholder x \<in> Cardholder`A) = (x \<in> A)" 

130 
by auto 

131 

132 
lemma CA_image_eq [simp]: "(CA x \<in> CA`A) = (x \<in> A)" 

133 
by auto 

134 

135 
lemma Pan_image_eq [simp]: "(Pan x \<in> Pan`A) = (x \<in> A)" 

136 
by auto 

137 

138 
lemma Pan_Key_image_eq [simp]: "(Pan x \<notin> Key`A)" 

139 
by auto 

140 

141 
lemma Nonce_Pan_image_eq [simp]: "(Nonce x \<notin> Pan`A)" 

142 
by auto 

143 

144 
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')" 

145 
apply safe 

146 
apply (drule_tac f = invKey in arg_cong, simp) 

147 
done 

148 

149 

150 
subsection{*keysFor operator*} 

151 

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

153 
by (unfold keysFor_def, blast) 

154 

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

156 
by (unfold keysFor_def, blast) 

157 

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

159 
by (unfold keysFor_def, blast) 

160 

161 
(*Monotonicity*) 

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

163 
by (unfold keysFor_def, blast) 

164 

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

166 
by (unfold keysFor_def, auto) 

167 

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

169 
by (unfold keysFor_def, auto) 

170 

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

172 
by (unfold keysFor_def, auto) 

173 

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

175 
by (unfold keysFor_def, auto) 

176 

177 
lemma keysFor_insert_Pan [simp]: "keysFor (insert (Pan A) H) = keysFor H" 

178 
by (unfold keysFor_def, auto) 

179 

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

181 
by (unfold keysFor_def, auto) 

182 

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

184 
by (unfold keysFor_def, auto) 

185 

186 
lemma keysFor_insert_Crypt [simp]: 

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

188 
by (unfold keysFor_def, auto) 

189 

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

191 
by (unfold keysFor_def, auto) 

192 

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

194 
by (unfold keysFor_def, blast) 

195 

196 

197 
subsection{*Inductive relation "parts"*} 

198 

199 
lemma MPair_parts: 

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

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

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

203 

204 
declare MPair_parts [elim!] parts.Body [dest!] 

205 
text{*NB These two rules are UNSAFE in the formal sense, as they discard the 

206 
compound message. They work well on THIS FILE. 

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

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

209 

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

211 
by blast 

212 

45605  213 
lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD] 
14199  214 

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

216 
apply safe 

217 
apply (erule parts.induct, blast+) 

218 
done 

219 

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

221 
by simp 

222 

223 
(*WARNING: loops if H = {Y}, therefore must not be repeated!*) 

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

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

225 
by (erule parts.induct, fast+) 
14199  226 

227 

228 
subsubsection{*Unions*} 

229 

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

231 
by (intro Un_least parts_mono Un_upper1 Un_upper2) 

232 

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

234 
apply (rule subsetI) 

235 
apply (erule parts.induct, blast+) 

236 
done 

237 

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

239 
by (intro equalityI parts_Un_subset1 parts_Un_subset2) 

240 

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

242 
apply (subst insert_is_Un [of _ H]) 

243 
apply (simp only: parts_Un) 

244 
done 

245 

246 
(*TWO inserts to avoid looping. This rewrite is better than nothing. 

247 
Not suitable for Addsimps: its behaviour can be strange.*) 

248 
lemma parts_insert2: 

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

250 
apply (simp add: Un_assoc) 

251 
apply (simp add: parts_insert [symmetric]) 

252 
done 

253 

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

255 
by (intro UN_least parts_mono UN_upper) 

256 

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

258 
apply (rule subsetI) 

259 
apply (erule parts.induct, blast+) 

260 
done 

261 

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

263 
by (intro equalityI parts_UN_subset1 parts_UN_subset2) 

264 

265 
(*Added to simplify arguments to parts, analz and synth. 

266 
NOTE: the UN versions are no longer used!*) 

267 

268 

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

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

271 
declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!] 

272 

273 

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

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

276 

277 
subsubsection{*Idempotence and transitivity*} 

278 

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

280 
by (erule parts.induct, blast+) 

281 

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

283 
by blast 

284 

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

286 
by (drule parts_mono, blast) 

287 

288 
(*Cut*) 

289 
lemma parts_cut: 

290 
"[ Y\<in> parts (insert X G); X\<in> parts H ] ==> Y\<in> parts (G \<union> H)" 

291 
by (erule parts_trans, auto) 

292 

293 
lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H" 

294 
by (force dest!: parts_cut intro: parts_insertI) 

295 

296 

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

298 

299 
lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset] 

300 

301 

302 
lemma parts_insert_Agent [simp]: 

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

304 
apply (rule parts_insert_eq_I) 

305 
apply (erule parts.induct, auto) 

306 
done 

307 

308 
lemma parts_insert_Nonce [simp]: 

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

310 
apply (rule parts_insert_eq_I) 

311 
apply (erule parts.induct, auto) 

312 
done 

313 

314 
lemma parts_insert_Number [simp]: 

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

316 
apply (rule parts_insert_eq_I) 

317 
apply (erule parts.induct, auto) 

318 
done 

319 

320 
lemma parts_insert_Key [simp]: 

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

322 
apply (rule parts_insert_eq_I) 

323 
apply (erule parts.induct, auto) 

324 
done 

325 

326 
lemma parts_insert_Pan [simp]: 

327 
"parts (insert (Pan A) H) = insert (Pan A) (parts H)" 

328 
apply (rule parts_insert_eq_I) 

329 
apply (erule parts.induct, auto) 

330 
done 

331 

332 
lemma parts_insert_Hash [simp]: 

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

334 
apply (rule parts_insert_eq_I) 

335 
apply (erule parts.induct, auto) 

336 
done 

337 

338 
lemma parts_insert_Crypt [simp]: 

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

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

341 
apply (rule equalityI) 

342 
apply (rule subsetI) 

343 
apply (erule parts.induct, auto) 

344 
apply (erule parts.induct) 

345 
apply (blast intro: parts.Body)+ 

346 
done 

347 

348 
lemma parts_insert_MPair [simp]: 

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

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

351 
apply (rule equalityI) 

352 
apply (rule subsetI) 

353 
apply (erule parts.induct, auto) 

354 
apply (erule parts.induct) 

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

356 
done 

357 

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

359 
apply auto 

360 
apply (erule parts.induct, auto) 

361 
done 

362 

363 
lemma parts_image_Pan [simp]: "parts (Pan`A) = Pan`A" 

364 
apply auto 

365 
apply (erule parts.induct, auto) 

366 
done 

367 

368 

369 
(*In any message, there is an upper bound N on its greatest nonce.*) 

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

371 
apply (induct_tac "msg") 

372 
apply (simp_all (no_asm_simp) add: exI parts_insert2) 

373 
(*MPair case: blast_tac works out the necessary sum itself!*) 

374 
prefer 2 apply (blast elim!: add_leE) 

375 
(*Nonce case*) 

376 
apply (rule_tac x = "N + Suc nat" in exI) 

377 
apply (auto elim!: add_leE) 

378 
done 

379 

380 
(* Ditto, for numbers.*) 

381 
lemma msg_Number_supply: "\<exists>N. \<forall>n. N<=n > Number n \<notin> parts {msg}" 

382 
apply (induct_tac "msg") 

383 
apply (simp_all (no_asm_simp) add: exI parts_insert2) 

384 
prefer 2 apply (blast elim!: add_leE) 

385 
apply (rule_tac x = "N + Suc nat" in exI, auto) 

386 
done 

387 

388 
subsection{*Inductive relation "analz"*} 

389 

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

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

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

393 

23755  394 
inductive_set 
395 
analz :: "msg set => msg set" 

396 
for H :: "msg set" 

397 
where 

14199  398 
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" 
23755  399 
 Fst: "{X,Y} \<in> analz H ==> X \<in> analz H" 
400 
 Snd: "{X,Y} \<in> analz H ==> Y \<in> analz H" 

401 
 Decrypt [dest]: 

14199  402 
"[Crypt K X \<in> analz H; Key(invKey K): analz H] ==> X \<in> analz H" 
403 

404 

405 
(*Monotonicity; Lemma 1 of Lowe's paper*) 

406 
lemma analz_mono: "G<=H ==> analz(G) <= analz(H)" 

407 
apply auto 

408 
apply (erule analz.induct) 

409 
apply (auto dest: Fst Snd) 

410 
done 

411 

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

413 
lemma MPair_analz [elim!]: 

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

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

416 
] ==> P" 

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

418 

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

420 
by blast 

421 

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

423 
apply (rule subsetI) 

424 
apply (erule analz.induct, blast+) 

425 
done 

426 

45605  427 
lemmas analz_into_parts = analz_subset_parts [THEN subsetD] 
14199  428 

45605  429 
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD] 
14199  430 

431 

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

433 
apply (rule equalityI) 

434 
apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp) 

435 
apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD]) 

436 
done 

437 

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

439 
apply auto 

440 
apply (erule analz.induct, auto) 

441 
done 

442 

45605  443 
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD] 
14199  444 

445 
subsubsection{*General equational properties*} 

446 

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

448 
apply safe 

449 
apply (erule analz.induct, blast+) 

450 
done 

451 

452 
(*Converse fails: we can analz more from the union than from the 

453 
separate parts, as a key in one might decrypt a message in the other*) 

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

455 
by (intro Un_least analz_mono Un_upper1 Un_upper2) 

456 

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

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

459 

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

461 

462 
lemmas analz_insert_eq_I = equalityI [OF subsetI analz_insert] 

463 

464 
lemma analz_insert_Agent [simp]: 

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

466 
apply (rule analz_insert_eq_I) 

467 
apply (erule analz.induct, auto) 

468 
done 

469 

470 
lemma analz_insert_Nonce [simp]: 

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

472 
apply (rule analz_insert_eq_I) 

473 
apply (erule analz.induct, auto) 

474 
done 

475 

476 
lemma analz_insert_Number [simp]: 

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

478 
apply (rule analz_insert_eq_I) 

479 
apply (erule analz.induct, auto) 

480 
done 

481 

482 
lemma analz_insert_Hash [simp]: 

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

484 
apply (rule analz_insert_eq_I) 

485 
apply (erule analz.induct, auto) 

486 
done 

487 

488 
(*Can only pull out Keys if they are not needed to decrypt the rest*) 

489 
lemma analz_insert_Key [simp]: 

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

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

492 
apply (unfold keysFor_def) 

493 
apply (rule analz_insert_eq_I) 

494 
apply (erule analz.induct, auto) 

495 
done 

496 

497 
lemma analz_insert_MPair [simp]: 

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

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

500 
apply (rule equalityI) 

501 
apply (rule subsetI) 

502 
apply (erule analz.induct, auto) 

503 
apply (erule analz.induct) 

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

505 
done 

506 

507 
(*Can pull out enCrypted message if the Key is not known*) 

508 
lemma analz_insert_Crypt: 

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

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

511 
apply (rule analz_insert_eq_I) 

512 
apply (erule analz.induct, auto) 

513 
done 

514 

515 
lemma analz_insert_Pan [simp]: 

516 
"analz (insert (Pan A) H) = insert (Pan A) (analz H)" 

517 
apply (rule analz_insert_eq_I) 

518 
apply (erule analz.induct, auto) 

519 
done 

520 

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

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

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

524 
apply (rule subsetI) 

23755  525 
apply (erule_tac x = x in analz.induct, auto) 
14199  526 
done 
527 

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

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

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

531 
apply auto 

23755  532 
apply (erule_tac x = x in analz.induct, auto) 
14199  533 
apply (blast intro: analz_insertI analz.Decrypt) 
534 
done 

535 

536 
lemma analz_insert_Decrypt: 

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

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

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

540 
by (intro equalityI lemma1 lemma2) 

541 

542 
(*Case analysis: either the message is secure, or it is not! 

543 
Effective, but can cause subgoals to blow up! 

544 
Use with split_if; apparently split_tac does not cope with patterns 

545 
such as "analz (insert (Crypt K X) H)" *) 

546 
lemma analz_Crypt_if [simp]: 

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

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

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

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

551 
by (simp add: analz_insert_Crypt analz_insert_Decrypt) 

552 

553 

554 
(*This rule supposes "for the sake of argument" that we have the key.*) 

555 
lemma analz_insert_Crypt_subset: 

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

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

558 
apply (rule subsetI) 

559 
apply (erule analz.induct, auto) 

560 
done 

561 

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

563 
apply auto 

564 
apply (erule analz.induct, auto) 

565 
done 

566 

567 
lemma analz_image_Pan [simp]: "analz (Pan`A) = Pan`A" 

568 
apply auto 

569 
apply (erule analz.induct, auto) 

570 
done 

571 

572 

573 
subsubsection{*Idempotence and transitivity*} 

574 

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

576 
by (erule analz.induct, blast+) 

577 

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

579 
by blast 

580 

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

582 
by (drule analz_mono, blast) 

583 

584 
(*Cut; Lemma 2 of Lowe*) 

585 
lemma analz_cut: "[ Y\<in> analz (insert X H); X\<in> analz H ] ==> Y\<in> analz H" 

586 
by (erule analz_trans, blast) 

587 

588 
(*Cut can be proved easily by induction on 

589 
"Y: analz (insert X H) ==> X: analz H > Y: analz H" 

590 
*) 

591 

592 
(*This rewrite rule helps in the simplification of messages that involve 

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

594 
of X can be very complicated. *) 

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

596 
by (blast intro: analz_cut analz_insertI) 

597 

598 

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

600 

601 
lemma analz_subset_cong: 

602 
"[ analz G \<subseteq> analz G'; analz H \<subseteq> analz H' 

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

604 
apply clarify 

605 
apply (erule analz.induct) 

606 
apply (best intro: analz_mono [THEN subsetD])+ 

607 
done 

608 

609 
lemma analz_cong: 

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

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

612 
by (intro equalityI analz_subset_cong, simp_all) 

613 

614 
lemma analz_insert_cong: 

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

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

617 

618 
(*If there are no pairs or encryptions then analz does nothing*) 

619 
lemma analz_trivial: 

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

621 
apply safe 

622 
apply (erule analz.induct, blast+) 

623 
done 

624 

625 
(*These two are obsolete (with a single Spy) but cost little to prove...*) 

626 
lemma analz_UN_analz_lemma: 

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

628 
apply (erule analz.induct) 

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

630 
done 

631 

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

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

634 

635 

636 
subsection{*Inductive relation "synth"*} 

637 

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

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

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

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

642 

23755  643 
inductive_set 
644 
synth :: "msg set => msg set" 

645 
for H :: "msg set" 

646 
where 

14199  647 
Inj [intro]: "X \<in> H ==> X \<in> synth H" 
23755  648 
 Agent [intro]: "Agent agt \<in> synth H" 
649 
 Number [intro]: "Number n \<in> synth H" 

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

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

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

14199  653 

654 
(*Monotonicity*) 

655 
lemma synth_mono: "G<=H ==> synth(G) <= synth(H)" 

656 
apply auto 

657 
apply (erule synth.induct) 

658 
apply (auto dest: Fst Snd Body) 

659 
done 

660 

661 
(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*) 

662 
inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H" 

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

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

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

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

667 
inductive_cases Pan_synth [elim!]: "Pan A \<in> synth H" 

668 

669 

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

671 
by blast 

672 

673 
subsubsection{*Unions*} 

674 

675 
(*Converse fails: we can synth more from the union than from the 

676 
separate parts, building a compound message using elements of each.*) 

677 
lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)" 

678 
by (intro Un_least synth_mono Un_upper1 Un_upper2) 

679 

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

681 
by (blast intro: synth_mono [THEN [2] rev_subsetD]) 

682 

683 
subsubsection{*Idempotence and transitivity*} 

684 

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

686 
by (erule synth.induct, blast+) 

687 

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

689 
by blast 

690 

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

692 
by (drule synth_mono, blast) 

693 

694 
(*Cut; Lemma 2 of Lowe*) 

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

696 
by (erule synth_trans, blast) 

697 

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

699 
by blast 

700 

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

702 
by blast 

703 

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

705 
by blast 

706 

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

708 
by blast 

709 

710 
lemma Crypt_synth_eq [simp]: "Key K \<notin> H ==> (Crypt K X \<in> synth H) = (Crypt K X \<in> H)" 

711 
by blast 

712 

713 
lemma Pan_synth_eq [simp]: "(Pan A \<in> synth H) = (Pan A \<in> H)" 

714 
by blast 

715 

716 
lemma keysFor_synth [simp]: 

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

718 
by (unfold keysFor_def, blast) 

719 

720 

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

722 

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

724 
apply (rule equalityI) 

725 
apply (rule subsetI) 

726 
apply (erule parts.induct) 

727 
apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] 

728 
parts.Fst parts.Snd parts.Body)+ 

729 
done 

730 

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

732 
apply (intro equalityI analz_subset_cong)+ 

733 
apply simp_all 

734 
done 

735 

736 
lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G" 

737 
apply (rule equalityI) 

738 
apply (rule subsetI) 

739 
apply (erule analz.induct) 

740 
prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD]) 

741 
apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+ 

742 
done 

743 

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

745 
apply (cut_tac H = "{}" in analz_synth_Un) 

746 
apply (simp (no_asm_use)) 

747 
done 

748 

749 

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

751 

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

753 
by (rule subset_trans [OF parts_mono parts_Un_subset2], blast) 

754 

755 
(*More specifically for Fake. Very occasionally we could do with a version 

756 
of the form parts{X} \<subseteq> synth (analz H) \<union> parts H *) 

757 
lemma Fake_parts_insert: "X \<in> synth (analz H) ==> 

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

759 
apply (drule parts_insert_subset_Un) 

760 
apply (simp (no_asm_use)) 

761 
apply blast 

762 
done 

763 

764 
lemma Fake_parts_insert_in_Un: 

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

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

767 
by (blast dest: Fake_parts_insert [THEN subsetD, dest]) 

768 

769 
(*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*) 

770 
lemma Fake_analz_insert: 

771 
"X\<in> synth (analz G) ==> 

772 
analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)" 

773 
apply (rule subsetI) 

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

775 
prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD]) 

776 
apply (simp (no_asm_use)) 

777 
apply blast 

778 
done 

779 

780 
lemma analz_conj_parts [simp]: 

781 
"(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)" 

782 
by (blast intro: analz_subset_parts [THEN subsetD]) 

783 

784 
lemma analz_disj_parts [simp]: 

785 
"(X \<in> analz H  X \<in> parts H) = (X \<in> parts H)" 

786 
by (blast intro: analz_subset_parts [THEN subsetD]) 

787 

788 
(*Without this equation, other rules for synth and analz would yield 

789 
redundant cases*) 

790 
lemma MPair_synth_analz [iff]: 

791 
"({X,Y} \<in> synth (analz H)) = 

792 
(X \<in> synth (analz H) & Y \<in> synth (analz H))" 

793 
by blast 

794 

795 
lemma Crypt_synth_analz: 

796 
"[ Key K \<in> analz H; Key (invKey K) \<in> analz H ] 

797 
==> (Crypt K X \<in> synth (analz H)) = (X \<in> synth (analz H))" 

798 
by blast 

799 

800 

801 
lemma Hash_synth_analz [simp]: 

802 
"X \<notin> synth (analz H) 

803 
==> (Hash{X,Y} \<in> synth (analz H)) = (Hash{X,Y} \<in> analz H)" 

804 
by blast 

805 

806 

807 
(*We do NOT want Crypt... messages broken up in protocols!!*) 

808 
declare parts.Body [rule del] 

809 

810 

811 
text{*Rewrites to push in Key and Crypt messages, so that other messages can 

812 
be pulled out using the @{text analz_insert} rules*} 

813 

45605  814 
lemmas pushKeys = 
27225  815 
insert_commute [of "Key K" "Agent C"] 
816 
insert_commute [of "Key K" "Nonce N"] 

817 
insert_commute [of "Key K" "Number N"] 

818 
insert_commute [of "Key K" "Pan PAN"] 

819 
insert_commute [of "Key K" "Hash X"] 

820 
insert_commute [of "Key K" "MPair X Y"] 

821 
insert_commute [of "Key K" "Crypt X K'"] 

45605  822 
for K C N PAN X Y K' 
14199  823 

45605  824 
lemmas pushCrypts = 
27225  825 
insert_commute [of "Crypt X K" "Agent C"] 
826 
insert_commute [of "Crypt X K" "Nonce N"] 

827 
insert_commute [of "Crypt X K" "Number N"] 

828 
insert_commute [of "Crypt X K" "Pan PAN"] 

829 
insert_commute [of "Crypt X K" "Hash X'"] 

830 
insert_commute [of "Crypt X K" "MPair X' Y"] 

45605  831 
for X K C N PAN X' Y 
14199  832 

833 
text{*Cannot be added with @{text "[simp]"}  messages should not always be 

834 
reordered.*} 

835 
lemmas pushes = pushKeys pushCrypts 

836 

837 

838 
subsection{*Tactics useful for many protocol proofs*} 

14218  839 
(*<*) 
14199  840 
ML 
841 
{* 

842 
(*Analysis of Fake cases. Also works for messages that forward unknown parts, 

843 
but this application is no longer necessary if analz_insert_eq is used. 

844 
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset 

845 
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) 

846 

32117
0762b9ad83df
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
haftmann
parents:
30607
diff
changeset

847 
fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) 
0762b9ad83df
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
haftmann
parents:
30607
diff
changeset

848 

14199  849 
(*Apply rules to break down assumptions of the form 
850 
Y \<in> parts(insert X H) and Y \<in> analz(insert X H) 

851 
*) 

852 
val Fake_insert_tac = 

24123  853 
dresolve_tac [impOfSubs @{thm Fake_analz_insert}, 
854 
impOfSubs @{thm Fake_parts_insert}] THEN' 

855 
eresolve_tac [asm_rl, @{thm synth.Inj}]; 

14199  856 

857 
fun Fake_insert_simp_tac ss i = 

42793  858 
REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; 
14199  859 

42474  860 
fun atomic_spy_analz_tac ctxt = 
42793  861 
SELECT_GOAL 
862 
(Fake_insert_simp_tac (simpset_of ctxt) 1 THEN 

863 
IF_UNSOLVED 

864 
(Blast.depth_tac (ctxt addIs [@{thm analz_insertI}, 

865 
impOfSubs @{thm analz_subset_parts}]) 4 1)); 

14199  866 

42474  867 
fun spy_analz_tac ctxt i = 
42793  868 
DETERM 
869 
(SELECT_GOAL 

870 
(EVERY 

871 
[ (*push in occurrences of X...*) 

872 
(REPEAT o CHANGED) 

873 
(res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), 

874 
(*...allowing further simplifications*) 

875 
simp_tac (simpset_of ctxt) 1, 

876 
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), 

877 
DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); 

14199  878 
*} 
14218  879 
(*>*) 
880 

14199  881 

882 
(*By default only o_apply is builtin. But in the presence of etaexpansion 

883 
this means that some terms displayed as (f o g) will be rewritten, and others 

884 
will not!*) 

885 
declare o_def [simp] 

886 

887 

888 
lemma Crypt_notin_image_Key [simp]: "Crypt K X \<notin> Key ` A" 

889 
by auto 

890 

891 
lemma Hash_notin_image_Key [simp] :"Hash X \<notin> Key ` A" 

892 
by auto 

893 

894 
lemma synth_analz_mono: "G<=H ==> synth (analz(G)) <= synth (analz(H))" 

895 
by (simp add: synth_mono analz_mono) 

896 

897 
lemma Fake_analz_eq [simp]: 

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

899 
apply (drule Fake_analz_insert[of _ _ "H"]) 

900 
apply (simp add: synth_increasing[THEN Un_absorb2]) 

901 
apply (drule synth_mono) 

902 
apply (simp add: synth_idem) 

903 
apply (blast intro: synth_analz_mono [THEN [2] rev_subsetD]) 

904 
done 

905 

906 
text{*Two generalizations of @{text analz_insert_eq}*} 

907 
lemma gen_analz_insert_eq [rule_format]: 

908 
"X \<in> analz H ==> ALL G. H \<subseteq> G > analz (insert X G) = analz G"; 

909 
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD]) 

910 

911 
lemma synth_analz_insert_eq [rule_format]: 

912 
"X \<in> synth (analz H) 

913 
==> ALL G. H \<subseteq> G > (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"; 

914 
apply (erule synth.induct) 

915 
apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) 

916 
done 

917 

918 
lemma Fake_parts_sing: 

919 
"X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"; 

920 
apply (rule subset_trans) 

921 
apply (erule_tac [2] Fake_parts_insert) 

922 
apply (simp add: parts_mono) 

923 
done 

924 

925 
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] 

926 

927 
method_setup spy_analz = {* 

42474  928 
Scan.succeed (SIMPLE_METHOD' o spy_analz_tac) *} 
14199  929 
"for proving the Fake case when analz is involved" 
930 

931 
method_setup atomic_spy_analz = {* 

42474  932 
Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac) *} 
14199  933 
"for debugging spy_analz" 
934 

935 
method_setup Fake_insert_simp = {* 

42474  936 
Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *} 
14199  937 
"for debugging spy_analz" 
938 

939 
end 