author  wenzelm 
Tue, 07 Sep 1999 10:40:58 +0200  
changeset 7499  23e090051cb8 
parent 7494  45905028bb1d 
child 8741  61bc5ed22b62 
permissions  rwrr 
6452  1 
(* Title: HOL/Auth/KerberosIV 
2 
ID: $Id$ 

3 
Author: Giampaolo Bella, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6 
The Kerberos protocol, version IV. 

7 
*) 

8 

9 
Pretty.setdepth 20; 

10 
proof_timing:=true; 

11 

12 
AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad]; 

13 

14 

15 
(** Reversed traces **) 

16 

17 
Goal "spies (evs @ [Says A B X]) = insert X (spies evs)"; 

18 
by (induct_tac "evs" 1); 

19 
by (induct_tac "a" 2); 

20 
by Auto_tac; 

21 
qed "spies_Says_rev"; 

22 

23 
Goal "spies (evs @ [Gets A X]) = spies evs"; 

24 
by (induct_tac "evs" 1); 

25 
by (induct_tac "a" 2); 

26 
by Auto_tac; 

27 
qed "spies_Gets_rev"; 

28 

29 
Goal "spies (evs @ [Notes A X]) = \ 

30 
\ (if A:bad then insert X (spies evs) else spies evs)"; 

31 
by (induct_tac "evs" 1); 

32 
by (induct_tac "a" 2); 

33 
by Auto_tac; 

34 
qed "spies_Notes_rev"; 

35 

36 
Goal "spies evs = spies (rev evs)"; 

37 
by (induct_tac "evs" 1); 

38 
by (induct_tac "a" 2); 

39 
by (ALLGOALS 

40 
(asm_simp_tac (simpset() addsimps [spies_Says_rev, spies_Gets_rev, 

41 
spies_Notes_rev]))); 

42 
qed "spies_evs_rev"; 

43 
bind_thm ("parts_spies_evs_revD2", spies_evs_rev RS equalityD2 RS parts_mono); 

44 

45 
Goal "spies (takeWhile P evs) <= spies evs"; 

46 
by (induct_tac "evs" 1); 

47 
by (induct_tac "a" 2); 

48 
by Auto_tac; 

49 
(* Resembles "used_subset_append" in Event.ML*) 

50 
qed "spies_takeWhile"; 

51 
bind_thm ("parts_spies_takeWhile_mono", spies_takeWhile RS parts_mono); 

52 

53 
Goal "~P(x) > takeWhile P (xs @ [x]) = takeWhile P xs"; 

54 
by (induct_tac "xs" 1); 

55 
by Auto_tac; 

56 
qed "takeWhile_tail"; 

57 

58 

59 
(*****************LEMMAS ABOUT AuthKeys****************) 

60 

61 
Goalw [AuthKeys_def] "AuthKeys [] = {}"; 

62 
by (Simp_tac 1); 

63 
qed "AuthKeys_empty"; 

64 

65 
Goalw [AuthKeys_def] 

66 
"(ALL A Tk akey Peer. \ 

67 
\ ev ~= Says Kas A (Crypt (shrK A) {akey, Agent Peer, Tk, \ 

68 
\ (Crypt (shrK Peer) {Agent A, Agent Peer, akey, Tk})}))\ 

69 
\ ==> AuthKeys (ev # evs) = AuthKeys evs"; 

70 
by Auto_tac; 

71 
qed "AuthKeys_not_insert"; 

72 

73 
Goalw [AuthKeys_def] 

74 
"AuthKeys \ 

75 
\ (Says Kas A (Crypt (shrK A) {Key K, Agent Peer, Number Tk, \ 

76 
\ (Crypt (shrK Peer) {Agent A, Agent Peer, Key K, Number Tk})}) # evs) \ 

77 
\ = insert K (AuthKeys evs)"; 

78 
by Auto_tac; 

79 
qed "AuthKeys_insert"; 

80 

81 
Goalw [AuthKeys_def] 

82 
"K : AuthKeys \ 

83 
\ (Says Kas A (Crypt (shrK A) {Key K', Agent Peer, Number Tk, \ 

84 
\ (Crypt (shrK Peer) {Agent A, Agent Peer, Key K', Number Tk})}) # evs) \ 

85 
\ ==> K = K'  K : AuthKeys evs"; 

86 
by Auto_tac; 

87 
qed "AuthKeys_simp"; 

88 

89 
Goalw [AuthKeys_def] 

90 
"Says Kas A (Crypt (shrK A) {Key K, Agent Tgs, Number Tk, \ 

91 
\ (Crypt (shrK Tgs) {Agent A, Agent Tgs, Key K, Number Tk})}) : set evs \ 

92 
\ ==> K : AuthKeys evs"; 

93 
by Auto_tac; 

94 
qed "AuthKeysI"; 

95 

96 
Goalw [AuthKeys_def] "K : AuthKeys evs ==> Key K : used evs"; 

97 
by (Simp_tac 1); 

98 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

99 
qed "AuthKeys_used"; 

100 

101 

102 
(**** FORWARDING LEMMAS ****) 

103 

104 
(*For reasoning about the encrypted portion of message K3*) 

105 
Goal "Says Kas' A (Crypt KeyA {AuthKey, Peer, Tk, AuthTicket}) \ 

106 
\ : set evs ==> AuthTicket : parts (spies evs)"; 

107 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

108 
qed "K3_msg_in_parts_spies"; 

109 

110 
Goal "Says Kas A (Crypt KeyA {AuthKey, Peer, Tk, AuthTicket}) \ 

111 
\ : set evs ==> AuthKey : parts (spies evs)"; 

112 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

113 
qed "Oops_parts_spies1"; 

114 

115 
Goal "[ Says Kas A (Crypt KeyA {Key AuthKey, Peer, Tk, AuthTicket}) \ 

116 
\ : set evs ;\ 

117 
\ evs : kerberos ] ==> AuthKey ~: range shrK"; 

118 
by (etac rev_mp 1); 

119 
by (etac kerberos.induct 1); 

120 
by Auto_tac; 

121 
qed "Oops_range_spies1"; 

122 

123 
(*For reasoning about the encrypted portion of message K5*) 

124 
Goal "Says Tgs' A (Crypt AuthKey {ServKey, Agent B, Tt, ServTicket})\ 

125 
\ : set evs ==> ServTicket : parts (spies evs)"; 

126 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

127 
qed "K5_msg_in_parts_spies"; 

128 

129 
Goal "Says Tgs A (Crypt AuthKey {ServKey, Agent B, Tt, ServTicket})\ 

130 
\ : set evs ==> ServKey : parts (spies evs)"; 

131 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

132 
qed "Oops_parts_spies2"; 

133 

134 
Goal "[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket}) \ 

135 
\ : set evs ;\ 

136 
\ evs : kerberos ] ==> ServKey ~: range shrK"; 

137 
by (etac rev_mp 1); 

138 
by (etac kerberos.induct 1); 

139 
by Auto_tac; 

140 
qed "Oops_range_spies2"; 

141 

142 
Goal "Says S A (Crypt K {SesKey, B, TimeStamp, Ticket}) : set evs \ 

143 
\ ==> Ticket : parts (spies evs)"; 

144 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

145 
qed "Says_ticket_in_parts_spies"; 

146 
(*Replaces both K3_msg_in_parts_spies and K5_msg_in_parts_spies*) 

147 

148 
fun parts_induct_tac i = 

149 
etac kerberos.induct i THEN 

150 
REPEAT (FIRSTGOAL analz_mono_contra_tac) THEN 

7499  151 
ftac K3_msg_in_parts_spies (i+4) THEN 
152 
ftac K5_msg_in_parts_spies (i+6) THEN 

153 
ftac Oops_parts_spies1 (i+8) THEN 

154 
ftac Oops_parts_spies2 (i+9) THEN 

6452  155 
prove_simple_subgoals_tac 1; 
156 

157 

158 
(*Spy never sees another agent's shared key! (unless it's lost at start)*) 

159 
Goal "evs : kerberos ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; 

160 
by (parts_induct_tac 1); 

161 
by (Fake_parts_insert_tac 1); 

162 
by (ALLGOALS Blast_tac); 

163 
qed "Spy_see_shrK"; 

164 
Addsimps [Spy_see_shrK]; 

165 

166 
Goal "evs : kerberos ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 

167 
by (auto_tac (claset() addDs [impOfSubs analz_subset_parts], simpset())); 

168 
qed "Spy_analz_shrK"; 

169 
Addsimps [Spy_analz_shrK]; 

170 

171 
Goal "[ Key (shrK A) : parts (spies evs); evs : kerberos ] ==> A:bad"; 

172 
by (blast_tac (claset() addDs [Spy_see_shrK]) 1); 

173 
qed "Spy_see_shrK_D"; 

174 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 

175 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

176 

177 
(*Nobody can have used nonexistent keys!*) 

178 
Goal "evs : kerberos ==> \ 

179 
\ Key K ~: used evs > K ~: keysFor (parts (spies evs))"; 

180 
by (parts_induct_tac 1); 

181 
(*Fake*) 

182 
by (best_tac 

183 
(claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 

184 
addIs [impOfSubs analz_subset_parts] 

185 
addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] 

186 
addss (simpset())) 1); 

187 
(*Others*) 

188 
by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs))); 

189 
qed_spec_mp "new_keys_not_used"; 

190 

191 
bind_thm ("new_keys_not_analzd", 

192 
[analz_subset_parts RS keysFor_mono, 

193 
new_keys_not_used] MRS contra_subsetD); 

194 

195 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

196 

197 

198 
(*********************** REGULARITY LEMMAS ***********************) 

199 
(* concerning the form of items passed in messages *) 

200 
(*****************************************************************) 

201 

202 
(*Describes the form of AuthKey, AuthTicket, and K sent by Kas*) 

203 
Goal "[ Says Kas A (Crypt K {Key AuthKey, Agent Peer, Tk, AuthTicket}) \ 

204 
\ : set evs; \ 

205 
\ evs : kerberos ] \ 

206 
\ ==> AuthKey ~: range shrK & AuthKey : AuthKeys evs & \ 

207 
\ AuthTicket = (Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk} ) &\ 

208 
\ K = shrK A & Peer = Tgs"; 

209 
by (etac rev_mp 1); 

210 
by (etac kerberos.induct 1); 

211 
by (ALLGOALS (simp_tac (simpset() addsimps [AuthKeys_def, AuthKeys_insert]))); 

212 
by (ALLGOALS Blast_tac); 

213 
qed "Says_Kas_message_form"; 

214 

215 
(*This lemma is essential for proving Says_Tgs_message_form: 

216 

217 
the session key AuthKey 

218 
supplied by Kas in the authentication ticket 

219 
cannot be a longterm key! 

220 

221 
Generalised to any session keys (both AuthKey and ServKey). 

222 
*) 

223 
Goal "[ Crypt (shrK Tgs_B) {Agent A, Agent Tgs_B, Key SesKey, Number T}\ 

224 
\ : parts (spies evs); Tgs_B ~: bad;\ 

225 
\ evs : kerberos ] \ 

226 
\ ==> SesKey ~: range shrK"; 

227 
by (etac rev_mp 1); 

228 
by (parts_induct_tac 1); 

229 
by (Fake_parts_insert_tac 1); 

230 
qed "SesKey_is_session_key"; 

231 

232 
Goal "[ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk} \ 

233 
\ : parts (spies evs); \ 

234 
\ evs : kerberos ] \ 

235 
\ ==> Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Tk, \ 

236 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}}) \ 

237 
\ : set evs"; 

238 
by (etac rev_mp 1); 

239 
by (parts_induct_tac 1); 

240 
(*Fake*) 

241 
by (Fake_parts_insert_tac 1); 

242 
(*K4*) 

243 
by (Blast_tac 1); 

244 
qed "A_trusts_AuthTicket"; 

245 

246 
Goal "[ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}\ 

247 
\ : parts (spies evs);\ 

248 
\ evs : kerberos ] \ 

249 
\ ==> AuthKey : AuthKeys evs"; 

7499  250 
by (ftac A_trusts_AuthTicket 1); 
6452  251 
by (assume_tac 1); 
252 
by (simp_tac (simpset() addsimps [AuthKeys_def]) 1); 

253 
by (Blast_tac 1); 

254 
qed "AuthTicket_crypt_AuthKey"; 

255 

256 
(*Describes the form of ServKey, ServTicket and AuthKey sent by Tgs*) 

257 
Goal "[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket})\ 

258 
\ : set evs; \ 

259 
\ evs : kerberos ] \ 

260 
\ ==> B ~= Tgs & ServKey ~: range shrK & ServKey ~: AuthKeys evs &\ 

261 
\ ServTicket = (Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt} ) & \ 

262 
\ AuthKey ~: range shrK & AuthKey : AuthKeys evs"; 

263 
by (etac rev_mp 1); 

264 
by (etac kerberos.induct 1); 

265 
by (ALLGOALS 

266 
(asm_full_simp_tac 

267 
(simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert, 

268 
AuthKeys_empty, AuthKeys_simp]))); 

269 
by (blast_tac (claset() addEs spies_partsEs) 1); 

270 
by Auto_tac; 

271 
by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1); 

272 
by (blast_tac (claset() addSDs [SesKey_is_session_key] 

273 
addEs spies_partsEs) 1); 

274 
by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey] 

275 
addEs spies_partsEs) 1); 

276 
qed "Says_Tgs_message_form"; 

277 

278 
(*If a certain encrypted message appears then it originated with Kas*) 

279 
Goal "[ Crypt (shrK A) {Key AuthKey, Peer, Tk, AuthTicket} \ 

280 
\ : parts (spies evs); \ 

281 
\ A ~: bad; evs : kerberos ] \ 

282 
\ ==> Says Kas A (Crypt (shrK A) {Key AuthKey, Peer, Tk, AuthTicket}) \ 

283 
\ : set evs"; 

284 
by (etac rev_mp 1); 

285 
by (parts_induct_tac 1); 

286 
(*Fake*) 

287 
by (Fake_parts_insert_tac 1); 

288 
(*K4*) 

289 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst, 

290 
A_trusts_AuthTicket RS Says_Kas_message_form]) 

291 
1); 

292 
qed "A_trusts_AuthKey"; 

293 

294 

295 
(*If a certain encrypted message appears then it originated with Tgs*) 

296 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket} \ 

297 
\ : parts (spies evs); \ 

298 
\ Key AuthKey ~: analz (spies evs); \ 

299 
\ AuthKey ~: range shrK; \ 

300 
\ evs : kerberos ] \ 

301 
\==> EX A. Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket})\ 

302 
\ : set evs"; 

303 
by (etac rev_mp 1); 

304 
by (etac rev_mp 1); 

305 
by (parts_induct_tac 1); 

306 
(*Fake*) 

307 
by (Fake_parts_insert_tac 1); 

308 
(*K2*) 

309 
by (Blast_tac 1); 

310 
(*K4*) 

311 
by Auto_tac; 

312 
qed "A_trusts_K4"; 

313 

314 
Goal "[ Crypt (shrK A) {Key AuthKey, Agent Tgs, Tk, AuthTicket} \ 

315 
\ : parts (spies evs); \ 

316 
\ A ~: bad; \ 

317 
\ evs : kerberos ] \ 

318 
\ ==> AuthKey ~: range shrK & \ 

319 
\ AuthTicket = Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}"; 

320 
by (etac rev_mp 1); 

321 
by (parts_induct_tac 1); 

322 
by (Fake_parts_insert_tac 1); 

323 
by (Blast_tac 1); 

324 
qed "AuthTicket_form"; 

325 

326 
(* This form holds also over an AuthTicket, but is not needed below. *) 

327 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket} \ 

328 
\ : parts (spies evs); \ 

329 
\ Key AuthKey ~: analz (spies evs); \ 

330 
\ evs : kerberos ] \ 

331 
\ ==> ServKey ~: range shrK & \ 

332 
\ (EX A. ServTicket = Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt})"; 

333 
by (etac rev_mp 1); 

334 
by (etac rev_mp 1); 

335 
by (parts_induct_tac 1); 

336 
by (Fake_parts_insert_tac 1); 

337 
qed "ServTicket_form"; 

338 

339 
Goal "[ Says Kas' A (Crypt (shrK A) \ 

340 
\ {Key AuthKey, Agent Tgs, Tk, AuthTicket} ) : set evs; \ 

341 
\ evs : kerberos ] \ 

342 
\ ==> AuthKey ~: range shrK & \ 

343 
\ AuthTicket = \ 

344 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}\ 

345 
\  AuthTicket : analz (spies evs)"; 

346 
by (case_tac "A : bad" 1); 

347 
by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1); 

348 
by (forward_tac [Says_imp_spies RS parts.Inj] 1); 

349 
by (blast_tac (claset() addSDs [AuthTicket_form]) 1); 

350 
qed "Says_kas_message_form"; 

351 
(* Essentially the same as AuthTicket_form *) 

352 

353 
Goal "[ Says Tgs' A (Crypt AuthKey \ 

354 
\ {Key ServKey, Agent B, Tt, ServTicket} ) : set evs; \ 

355 
\ evs : kerberos ] \ 

356 
\ ==> ServKey ~: range shrK & \ 

357 
\ (EX A. ServTicket = \ 

358 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}) \ 

359 
\  ServTicket : analz (spies evs)"; 

360 
by (case_tac "Key AuthKey : analz (spies evs)" 1); 

361 
by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1); 

362 
by (forward_tac [Says_imp_spies RS parts.Inj] 1); 

363 
by (blast_tac (claset() addSDs [ServTicket_form]) 1); 

364 
qed "Says_tgs_message_form"; 

365 
(* This form MUST be used in analz_sees_tac below *) 

366 

367 

368 
(*****************UNICITY THEOREMS****************) 

369 

370 
(* The session key, if secure, uniquely identifies the Ticket 

371 
whether AuthTicket or ServTicket. As a matter of fact, one can read 

372 
also Tgs in the place of B. *) 

373 
Goal "evs : kerberos ==> \ 

374 
\ Key SesKey ~: analz (spies evs) > \ 

375 
\ (EX A B T. ALL A' B' T'. \ 

376 
\ Crypt (shrK B') {Agent A', Agent B', Key SesKey, T'} \ 

377 
\ : parts (spies evs) > A'=A & B'=B & T'=T)"; 

378 
by (parts_induct_tac 1); 

379 
by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*) 

380 
THEN Fake_parts_insert_tac 1); 

381 
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 

382 
by (expand_case_tac "SesKey = ?y" 1); 

383 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

384 
by (expand_case_tac "SesKey = ?y" 1); 

385 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

386 
val lemma = result(); 

387 

388 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key SesKey, T} \ 

389 
\ : parts (spies evs); \ 

390 
\ Crypt (shrK B') {Agent A', Agent B', Key SesKey, T'} \ 

391 
\ : parts (spies evs); \ 

392 
\ evs : kerberos; Key SesKey ~: analz (spies evs) ] \ 

393 
\ ==> A=A' & B=B' & T=T'"; 

394 
by (prove_unique_tac lemma 1); 

395 
qed "unique_CryptKey"; 

396 

397 
Goal "evs : kerberos \ 

398 
\ ==> Key SesKey ~: analz (spies evs) > \ 

399 
\ (EX K' B' T' Ticket'. ALL K B T Ticket. \ 

400 
\ Crypt K {Key SesKey, Agent B, T, Ticket} \ 

401 
\ : parts (spies evs) > K=K' & B=B' & T=T' & Ticket=Ticket')"; 

402 
by (parts_induct_tac 1); 

403 
by (REPEAT (etac (exI RSN (2,exE)) 1) THEN Fake_parts_insert_tac 1); 

404 
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 

405 
by (expand_case_tac "SesKey = ?y" 1); 

406 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

407 
by (expand_case_tac "SesKey = ?y" 1); 

408 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

409 
val lemma = result(); 

410 

411 
(*An AuthKey is encrypted by one and only one Shared key. 

412 
A ServKey is encrypted by one and only one AuthKey. 

413 
*) 

414 
Goal "[ Crypt K {Key SesKey, Agent B, T, Ticket} \ 

415 
\ : parts (spies evs); \ 

416 
\ Crypt K' {Key SesKey, Agent B', T', Ticket'} \ 

417 
\ : parts (spies evs); \ 

418 
\ evs : kerberos; Key SesKey ~: analz (spies evs) ] \ 

419 
\ ==> K=K' & B=B' & T=T' & Ticket=Ticket'"; 

420 
by (prove_unique_tac lemma 1); 

421 
qed "Key_unique_SesKey"; 

422 

423 

424 
(* 

425 
At reception of any message mentioning A, Kas associates shrK A with 

426 
a new AuthKey. Realistic, as the user gets a new AuthKey at each login. 

427 
Similarly, at reception of any message mentioning an AuthKey 

428 
(a legitimate user could make several requests to Tgs  by K3), Tgs 

429 
associates it with a new ServKey. 

430 

431 
Therefore, a goal like 

432 

433 
"evs : kerberos \ 

434 
\ ==> Key Kc ~: analz (spies evs) > \ 

435 
\ (EX K' B' T' Ticket'. ALL K B T Ticket. \ 

436 
\ Crypt Kc {Key K, Agent B, T, Ticket} \ 

437 
\ : parts (spies evs) > K=K' & B=B' & T=T' & Ticket=Ticket')"; 

438 

439 
would fail on the K2 and K4 cases. 

440 
*) 

441 

442 
(* AuthKey uniquely identifies the message from Kas *) 

443 
Goal "evs : kerberos ==> \ 

444 
\ EX A' Ka' Tk' X'. ALL A Ka Tk X. \ 

445 
\ Says Kas A (Crypt Ka {Key AuthKey, Agent Tgs, Tk, X}) \ 

446 
\ : set evs > A=A' & Ka=Ka' & Tk=Tk' & X=X'"; 

447 
by (etac kerberos.induct 1); 

448 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

449 
by (Step_tac 1); 

450 
(*K2: it can't be a new key*) 

451 
by (expand_case_tac "AuthKey = ?y" 1); 

452 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

453 
by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*) 

454 
addSEs spies_partsEs) 1); 

455 
val lemma = result(); 

456 

457 
Goal "[ Says Kas A \ 

458 
\ (Crypt Ka {Key AuthKey, Agent Tgs, Tk, X}) : set evs; \ 

459 
\ Says Kas A' \ 

460 
\ (Crypt Ka' {Key AuthKey, Agent Tgs, Tk', X'}) : set evs; \ 

461 
\ evs : kerberos ] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'"; 

462 
by (prove_unique_tac lemma 1); 

463 
qed "unique_AuthKeys"; 

464 

465 
(* ServKey uniquely identifies the message from Tgs *) 

466 
Goal "evs : kerberos ==> \ 

467 
\ EX A' B' AuthKey' Tk' X'. ALL A B AuthKey Tk X. \ 

468 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tk, X}) \ 

469 
\ : set evs > A=A' & B=B' & AuthKey=AuthKey' & Tk=Tk' & X=X'"; 

470 
by (etac kerberos.induct 1); 

471 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

472 
by (Step_tac 1); 

473 
(*K4: it can't be a new key*) 

474 
by (expand_case_tac "ServKey = ?y" 1); 

475 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

476 
by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*) 

477 
addSEs spies_partsEs) 1); 

478 
val lemma = result(); 

479 

480 
Goal "[ Says Tgs A \ 

481 
\ (Crypt K {Key ServKey, Agent B, Tt, X}) : set evs; \ 

482 
\ Says Tgs A' \ 

483 
\ (Crypt K' {Key ServKey, Agent B', Tt', X'}) : set evs; \ 

484 
\ evs : kerberos ] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'"; 

485 
by (prove_unique_tac lemma 1); 

486 
qed "unique_ServKeys"; 

487 

488 

489 
(*****************LEMMAS ABOUT the predicate KeyCryptKey****************) 

490 

491 
Goalw [KeyCryptKey_def] "~ KeyCryptKey AuthKey ServKey []"; 

492 
by (Simp_tac 1); 

493 
qed "not_KeyCryptKey_Nil"; 

494 
AddIffs [not_KeyCryptKey_Nil]; 

495 

496 
Goalw [KeyCryptKey_def] 

497 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, tt, X }) \ 

498 
\ : set evs; \ 

499 
\ evs : kerberos ] ==> KeyCryptKey AuthKey ServKey evs"; 

7499  500 
by (ftac Says_Tgs_message_form 1); 
6452  501 
by (assume_tac 1); 
502 
by (Blast_tac 1); 

503 
qed "KeyCryptKeyI"; 

504 

505 
Goalw [KeyCryptKey_def] 

506 
"KeyCryptKey AuthKey ServKey (Says S A X # evs) = \ 

507 
\ (Tgs = S & \ 

508 
\ (EX B tt. X = Crypt AuthKey \ 

509 
\ {Key ServKey, Agent B, tt, \ 

510 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, tt} }) \ 

511 
\  KeyCryptKey AuthKey ServKey evs)"; 

512 
by (Simp_tac 1); 

513 
by (Blast_tac 1); 

514 
qed "KeyCryptKey_Says"; 

515 
Addsimps [KeyCryptKey_Says]; 

516 

517 
(*A fresh AuthKey cannot be associated with any other 

518 
(with respect to a given trace). *) 

519 
Goalw [KeyCryptKey_def] 

520 
"[ Key AuthKey ~: used evs; evs : kerberos ] \ 

521 
\ ==> ~ KeyCryptKey AuthKey ServKey evs"; 

522 
by (etac rev_mp 1); 

523 
by (parts_induct_tac 1); 

524 
by (Asm_full_simp_tac 1); 

525 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

526 
qed "Auth_fresh_not_KeyCryptKey"; 

527 

528 
(*A fresh ServKey cannot be associated with any other 

529 
(with respect to a given trace). *) 

530 
Goalw [KeyCryptKey_def] 

531 
"Key ServKey ~: used evs ==> ~ KeyCryptKey AuthKey ServKey evs"; 

532 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

533 
qed "Serv_fresh_not_KeyCryptKey"; 

534 

535 
Goalw [KeyCryptKey_def] 

536 
"[ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, tk}\ 

537 
\ : parts (spies evs); evs : kerberos ] \ 

538 
\ ==> ~ KeyCryptKey K AuthKey evs"; 

539 
by (etac rev_mp 1); 

540 
by (parts_induct_tac 1); 

541 
(*K4*) 

542 
by (blast_tac (claset() addEs spies_partsEs) 3); 

543 
(*K2: by freshness*) 

544 
by (blast_tac (claset() addEs spies_partsEs) 2); 

545 
by (Fake_parts_insert_tac 1); 

546 
qed "AuthKey_not_KeyCryptKey"; 

547 

548 
(*A secure serverkey cannot have been used to encrypt others*) 

549 
Goalw [KeyCryptKey_def] 

550 
"[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, tt} \ 

551 
\ : parts (spies evs); \ 

552 
\ Key ServKey ~: analz (spies evs); \ 

553 
\ B ~= Tgs; evs : kerberos ] \ 

554 
\ ==> ~ KeyCryptKey ServKey K evs"; 

555 
by (etac rev_mp 1); 

556 
by (etac rev_mp 1); 

557 
by (parts_induct_tac 1); 

558 
by (Fake_parts_insert_tac 1); 

559 
(*K4 splits into distinct subcases*) 

560 
by (Step_tac 1); 

561 
by (ALLGOALS Asm_full_simp_tac); 

562 
(*ServKey can't have been enclosed in two certificates*) 

563 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] 

564 
addSEs [MPair_parts] 

565 
addDs [unique_CryptKey]) 4); 

566 
(*ServKey is fresh and so could not have been used, by new_keys_not_used*) 

567 
by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj, 

568 
Crypt_imp_invKey_keysFor], 

569 
simpset()) 2); 

570 
(*Others by freshness*) 

571 
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); 

572 
qed "ServKey_not_KeyCryptKey"; 

573 

574 
(*Long term keys are not issued as ServKeys*) 

575 
Goalw [KeyCryptKey_def] 

576 
"evs : kerberos ==> ~ KeyCryptKey K (shrK A) evs"; 

577 
by (parts_induct_tac 1); 

578 
qed "shrK_not_KeyCryptKey"; 

579 

580 
(*The Tgs message associates ServKey with AuthKey and therefore not with any 

581 
other key AuthKey.*) 

582 
Goalw [KeyCryptKey_def] 

583 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, tt, X }) \ 

584 
\ : set evs; \ 

585 
\ AuthKey' ~= AuthKey; evs : kerberos ] \ 

586 
\ ==> ~ KeyCryptKey AuthKey' ServKey evs"; 

587 
by (blast_tac (claset() addDs [unique_ServKeys]) 1); 

588 
qed "Says_Tgs_KeyCryptKey"; 

589 

590 
Goal "[ KeyCryptKey AuthKey ServKey evs; evs : kerberos ] \ 

591 
\ ==> ~ KeyCryptKey ServKey K evs"; 

592 
by (etac rev_mp 1); 

593 
by (parts_induct_tac 1); 

594 
by (Step_tac 1); 

595 
by (ALLGOALS Asm_full_simp_tac); 

596 
(*K4 splits into subcases*) 

597 
by (blast_tac (claset() addEs spies_partsEs 

598 
addSDs [AuthKey_not_KeyCryptKey]) 4); 

599 
(*ServKey is fresh and so could not have been used, by new_keys_not_used*) 

600 
by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj, 

601 
Crypt_imp_invKey_keysFor], 

602 
simpset() addsimps [KeyCryptKey_def]) 2); 

603 
(*Others by freshness*) 

604 
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); 

605 
qed "KeyCryptKey_not_KeyCryptKey"; 

606 

607 
(*The only session keys that can be found with the help of session keys are 

608 
those sent by Tgs in step K4. *) 

609 

610 
(*We take some pains to express the property 

611 
as a logical equivalence so that the simplifier can apply it.*) 

612 
Goal "P > (Key K : analz (Key``KK Un H)) > (K:KK  Key K : analz H) \ 

613 
\ ==> \ 

614 
\ P > (Key K : analz (Key``KK Un H)) = (K:KK  Key K : analz H)"; 

615 
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); 

616 
qed "Key_analz_image_Key_lemma"; 

617 

618 
Goal "[ KeyCryptKey K K' evs; evs : kerberos ] \ 

619 
\ ==> Key K' : analz (insert (Key K) (spies evs))"; 

620 
by (full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1); 

621 
by (Clarify_tac 1); 

622 
by (dresolve_tac [Says_imp_spies RS analz.Inj RS analz_insertI] 1); 

623 
by Auto_tac; 

624 
qed "KeyCryptKey_analz_insert"; 

625 

626 
Goal "[ K : AuthKeys evs Un range shrK; evs : kerberos ] \ 

627 
\ ==> ALL SK. ~ KeyCryptKey SK K evs"; 

628 
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1); 

629 
by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1); 

630 
qed "AuthKeys_are_not_KeyCryptKey"; 

631 

632 
Goal "[ K ~: AuthKeys evs; \ 

633 
\ K ~: range shrK; evs : kerberos ] \ 

634 
\ ==> ALL SK. ~ KeyCryptKey K SK evs"; 

635 
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1); 

636 
by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1); 

637 
qed "not_AuthKeys_not_KeyCryptKey"; 

638 

639 

640 
(*****************SECRECY THEOREMS****************) 

641 

642 
(*For proofs involving analz.*) 

643 
val analz_sees_tac = 

644 
EVERY 

645 
[REPEAT (FIRSTGOAL analz_mono_contra_tac), 

7499  646 
ftac Oops_range_spies2 10, 
647 
ftac Oops_range_spies1 9, 

648 
ftac Says_tgs_message_form 7, 

649 
ftac Says_kas_message_form 5, 

6452  650 
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE] 
651 
ORELSE' hyp_subst_tac)]; 

652 

653 
Goal "[ KK <= (range shrK); Key K : analz (spies evs); evs: kerberos ] \ 

654 
\ ==> Key K : analz (Key `` KK Un spies evs)"; 

655 
by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1); 

656 
qed "analz_mono_KK"; 

657 

658 
(* Big simplification law for keys SK that are not crypted by keys in KK *) 

659 
(* It helps prove three, otherwise hard, facts about keys. These facts are *) 

660 
(* exploited as simplification laws for analz, and also "limit the damage" *) 

661 
(* in case of loss of a key to the spy. See ESORICS98. *) 

662 
Goal "evs : kerberos ==> \ 

663 
\ (ALL SK KK. KK <= (range shrK) > \ 

664 
\ (ALL K: KK. ~ KeyCryptKey K SK evs) > \ 

665 
\ (Key SK : analz (Key``KK Un (spies evs))) = \ 

666 
\ (SK : KK  Key SK : analz (spies evs)))"; 

667 
by (etac kerberos.induct 1); 

668 
by analz_sees_tac; 

669 
by (REPEAT_FIRST (rtac allI)); 

670 
by (REPEAT_FIRST (rtac (Key_analz_image_Key_lemma RS impI))); 

671 
by (ALLGOALS 

672 
(asm_simp_tac 

673 
(analz_image_freshK_ss addsimps 

674 
[KeyCryptKey_Says, shrK_not_KeyCryptKey, 

675 
Auth_fresh_not_KeyCryptKey, Serv_fresh_not_KeyCryptKey, 

676 
Says_Tgs_KeyCryptKey, Spy_analz_shrK]))); 

677 
(*Fake*) 

678 
by (spy_analz_tac 1); 

679 
(* Base + K2 done by the simplifier! *) 

680 
(*K3*) 

681 
by (Blast_tac 1); 

682 
(*K4*) 

683 
by (blast_tac (claset() addEs spies_partsEs 

684 
addSDs [AuthKey_not_KeyCryptKey]) 1); 

685 
(*K5*) 

686 
by (rtac impI 1); 

687 
by (case_tac "Key ServKey : analz (spies evs5)" 1); 

688 
(*If ServKey is compromised then the result follows directly...*) 

689 
by (asm_simp_tac 

690 
(simpset() addsimps [analz_insert_eq, 

691 
impOfSubs (Un_upper2 RS analz_mono)]) 1); 

692 
(*...therefore ServKey is uncompromised.*) 

693 
by (case_tac "KeyCryptKey ServKey SK evs5" 1); 

694 
by (asm_simp_tac analz_image_freshK_ss 2); 

695 
(*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*) 

696 
by (blast_tac (claset() addSEs [ServKey_not_KeyCryptKey RSN(2, rev_notE)] 

697 
addEs spies_partsEs delrules [allE, ballE]) 1); 

698 
(** Level 14: Oops1 and Oops2 **) 

699 
by (ALLGOALS Clarify_tac); 

700 
(*Oops 2*) 

701 
by (case_tac "Key ServKey : analz (spies evsO2)" 2); 

702 
by (ALLGOALS Asm_full_simp_tac); 

7499  703 
by (ftac analz_mono_KK 2 
6452  704 
THEN assume_tac 2 
705 
THEN assume_tac 2); 

7499  706 
by (ftac analz_cut 2 THEN assume_tac 2); 
6452  707 
by (blast_tac (claset() addDs [analz_cut, impOfSubs analz_mono]) 2); 
708 
by (dres_inst_tac [("x","SK")] spec 2); 

709 
by (dres_inst_tac [("x","insert ServKey KK")] spec 2); 

7499  710 
by (ftac Says_Tgs_message_form 2 THEN assume_tac 2); 
6452  711 
by (Clarify_tac 2); 
712 
by (forward_tac [Says_imp_spies RS parts.Inj RS parts.Body 

713 
RS parts.Snd RS parts.Snd RS parts.Snd] 2); 

714 
by (Asm_full_simp_tac 2); 

715 
by (blast_tac (claset() addSDs [ServKey_not_KeyCryptKey] 

7494
45905028bb1d
added theorems le_maxI1 and le_maxI2, also in claset
oheimb
parents:
7239
diff
changeset

716 
delrules [le_maxI1, le_maxI2] 
6452  717 
addDs [impOfSubs analz_mono]) 2); 
7494
45905028bb1d
added theorems le_maxI1 and le_maxI2, also in claset
oheimb
parents:
7239
diff
changeset

718 
(*Level 27: Oops 1*) 
6452  719 
by (dres_inst_tac [("x","SK")] spec 1); 
720 
by (dres_inst_tac [("x","insert AuthKey KK")] spec 1); 

721 
by (case_tac "KeyCryptKey AuthKey SK evsO1" 1); 

722 
by (ALLGOALS Asm_full_simp_tac); 

723 
by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1); 

7494
45905028bb1d
added theorems le_maxI1 and le_maxI2, also in claset
oheimb
parents:
7239
diff
changeset

724 
by (blast_tac (claset() delrules [le_maxI1, le_maxI2] 
45905028bb1d
added theorems le_maxI1 and le_maxI2, also in claset
oheimb
parents:
7239
diff
changeset

725 
addDs [impOfSubs analz_mono]) 1); 
6452  726 
qed_spec_mp "Key_analz_image_Key"; 
727 

728 

729 
(* First simplification law for analz: no session keys encrypt *) 

730 
(* authentication keys or shared keys. *) 

731 
Goal "[ evs : kerberos; K : (AuthKeys evs) Un range shrK; \ 

732 
\ SesKey ~: range shrK ] \ 

733 
\ ==> Key K : analz (insert (Key SesKey) (spies evs)) = \ 

734 
\ (K = SesKey  Key K : analz (spies evs))"; 

7499  735 
by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1); 
6452  736 
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); 
737 
qed "analz_insert_freshK1"; 

738 

739 

740 
(* Second simplification law for analz: no service keys encrypt *) 

741 
(* any other keys. *) 

742 
Goal "[ evs : kerberos; ServKey ~: (AuthKeys evs); ServKey ~: range shrK]\ 

743 
\ ==> Key K : analz (insert (Key ServKey) (spies evs)) = \ 

744 
\ (K = ServKey  Key K : analz (spies evs))"; 

7499  745 
by (ftac not_AuthKeys_not_KeyCryptKey 1 
6452  746 
THEN assume_tac 1 
747 
THEN assume_tac 1); 

748 
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); 

749 
qed "analz_insert_freshK2"; 

750 

751 

752 
(* Third simplification law for analz: only one authentication key *) 

753 
(* encrypts a certain service key. *) 

754 
Goal 

755 
"[ Says Tgs A \ 

756 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \ 

757 
\ : set evs; \ 

758 
\ AuthKey ~= AuthKey'; AuthKey' ~: range shrK; evs : kerberos ] \ 

759 
\ ==> Key ServKey : analz (insert (Key AuthKey') (spies evs)) = \ 

760 
\ (ServKey = AuthKey'  Key ServKey : analz (spies evs))"; 

761 
by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1); 

762 
by (Blast_tac 1); 

763 
by (assume_tac 1); 

764 
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); 

765 
qed "analz_insert_freshK3"; 

766 

767 

768 
(*a weakness of the protocol*) 

769 
Goal "[ Says Tgs A \ 

770 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \ 

771 
\ : set evs; \ 

772 
\ Key AuthKey : analz (spies evs); evs : kerberos ] \ 

773 
\ ==> Key ServKey : analz (spies evs)"; 

774 
by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 

775 
analz.Decrypt RS analz.Fst], 

776 
simpset()) 1); 

777 
qed "AuthKey_compromises_ServKey"; 

778 

779 

780 
(********************** Guarantees for Kas *****************************) 

781 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, Tt, \ 

782 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}}\ 

783 
\ : parts (spies evs); \ 

784 
\ Key ServKey ~: analz (spies evs); \ 

785 
\ B ~= Tgs; evs : kerberos ] \ 

786 
\ ==> ServKey ~: AuthKeys evs"; 

787 
by (etac rev_mp 1); 

788 
by (etac rev_mp 1); 

789 
by (asm_full_simp_tac (simpset() addsimps [AuthKeys_def]) 1); 

790 
by (parts_induct_tac 1); 

791 
by (Fake_parts_insert_tac 1); 

792 
by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs))); 

793 
bind_thm ("ServKey_notin_AuthKeys", result() RSN (2, rev_notE)); 

794 
bind_thm ("ServKey_notin_AuthKeysD", result()); 

795 

796 

797 
(** If Spy sees the Authentication Key sent in msg K2, then 

798 
the Key has expired **) 

799 
Goal "[ A ~: bad; evs : kerberos ] \ 

800 
\ ==> Says Kas A \ 

801 
\ (Crypt (shrK A) \ 

802 
\ {Key AuthKey, Agent Tgs, Number Tk, \ 

803 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

804 
\ : set evs > \ 

805 
\ Key AuthKey : analz (spies evs) > \ 

806 
\ ExpirAuth Tk evs"; 

807 
by (etac kerberos.induct 1); 

808 
by analz_sees_tac; 

809 
by (ALLGOALS 

810 
(asm_simp_tac 

811 
(simpset() addsimps ([Says_Kas_message_form, 

812 
analz_insert_eq, not_parts_not_analz, 

813 
analz_insert_freshK1] @ pushes)))); 

814 
(*Fake*) 

815 
by (spy_analz_tac 1); 

816 
(*K2*) 

817 
by (blast_tac (claset() addSEs spies_partsEs 

818 
addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1); 

819 
(*K4*) 

820 
by (blast_tac (claset() addSEs spies_partsEs) 1); 

821 
(*Level 8: K5*) 

822 
by (blast_tac (claset() addEs [ServKey_notin_AuthKeys] 

823 
addDs [Says_Kas_message_form, 

824 
Says_imp_spies RS parts.Inj] 

825 
addIs [less_SucI]) 1); 

826 
(*Oops1*) 

827 
by (blast_tac (claset() addDs [unique_AuthKeys] addIs [less_SucI]) 1); 

828 
(*Oops2*) 

829 
by (blast_tac (claset() addDs [Says_Tgs_message_form, 

830 
Says_Kas_message_form]) 1); 

831 
val lemma = result() RS mp RS mp RSN(1,rev_notE); 

832 

833 

834 
Goal "[ Says Kas A \ 

835 
\ (Crypt Ka {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}) \ 

836 
\ : set evs; \ 

837 
\ ~ ExpirAuth Tk evs; \ 

838 
\ A ~: bad; evs : kerberos ] \ 

839 
\ ==> Key AuthKey ~: analz (spies evs)"; 

7499  840 
by (ftac Says_Kas_message_form 1 THEN assume_tac 1); 
6452  841 
by (blast_tac (claset() addSDs [lemma]) 1); 
842 
qed "Confidentiality_Kas"; 

843 

844 

845 

846 

847 

848 

849 
(********************** Guarantees for Tgs *****************************) 

850 

851 
(** If Spy sees the Service Key sent in msg K4, then 

852 
the Key has expired **) 

853 
Goal "[ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

854 
\ ==> Key AuthKey ~: analz (spies evs) > \ 

855 
\ Says Tgs A \ 

856 
\ (Crypt AuthKey \ 

857 
\ {Key ServKey, Agent B, Number Tt, \ 

858 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}})\ 

859 
\ : set evs > \ 

860 
\ Key ServKey : analz (spies evs) > \ 

861 
\ ExpirServ Tt evs"; 

862 
by (etac kerberos.induct 1); 

863 
(*The Oops1 case is unusual: must simplify Authkey ~: analz (spies (ev#evs)) 

864 
rather than weakening it to Authkey ~: analz (spies evs), for we then 

865 
conclude AuthKey ~= AuthKeya.*) 

866 
by (Clarify_tac 9); 

867 
by analz_sees_tac; 

868 
by (rotate_tac ~1 11); 

869 
by (ALLGOALS 

870 
(asm_full_simp_tac 

871 
(simpset() addsimps ([Says_Kas_message_form, Says_Tgs_message_form, 

872 
analz_insert_eq, not_parts_not_analz, 

873 
analz_insert_freshK1, analz_insert_freshK2] @ pushes)))); 

874 
(*Fake*) 

875 
by (spy_analz_tac 1); 

876 
(*K2*) 

877 
by (blast_tac (claset() addSEs spies_partsEs 

878 
addIs [parts_insertI, impOfSubs analz_subset_parts, less_SucI]) 1); 

879 
(*K4*) 

880 
by (case_tac "A ~= Aa" 1); 

881 
by (blast_tac (claset() addSEs spies_partsEs 

882 
addIs [less_SucI]) 1); 

883 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst, 

884 
A_trusts_AuthTicket, 

885 
Confidentiality_Kas, 

886 
impOfSubs analz_subset_parts]) 1); 

887 
by (ALLGOALS Clarify_tac); 

888 
(*Oops2*) 

889 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 

890 
Key_unique_SesKey] addIs [less_SucI]) 3); 

891 
(** Level 12 **) 

892 
(*Oops1*) 

7499  893 
by (ftac Says_Kas_message_form 2); 
6452  894 
by (assume_tac 2); 
895 
by (blast_tac (claset() addDs [analz_insert_freshK3, 

896 
Says_Kas_message_form, Says_Tgs_message_form] 

897 
addIs [less_SucI]) 2); 

898 
(** Level 16 **) 

899 
by (thin_tac "Says Aa Tgs ?X : set ?evs" 1); 

900 
by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1); 

901 
by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1); 

902 
by (rotate_tac ~1 1); 

903 
by (asm_full_simp_tac (simpset() addsimps [analz_insert_freshK2]) 1); 

904 
by (etac disjE 1); 

905 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 

906 
Key_unique_SesKey]) 1); 

907 
by (blast_tac (claset() addIs [less_SucI]) 1); 

908 
val lemma = result() RS mp RS mp RS mp RSN(1,rev_notE); 

909 

910 

911 
(* In the real world Tgs can't check wheter AuthKey is secure! *) 

912 
Goal 

913 
"[ Says Tgs A \ 

914 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \ 

915 
\ : set evs; \ 

916 
\ Key AuthKey ~: analz (spies evs); \ 

917 
\ ~ ExpirServ Tt evs; \ 

918 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

919 
\ ==> Key ServKey ~: analz (spies evs)"; 

7499  920 
by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); 
6452  921 
by (blast_tac (claset() addDs [lemma]) 1); 
922 
qed "Confidentiality_Tgs1"; 

923 

924 
(* In the real world Tgs CAN check what Kas sends! *) 

925 
Goal 

926 
"[ Says Kas A \ 

927 
\ (Crypt Ka {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}) \ 

928 
\ : set evs; \ 

929 
\ Says Tgs A \ 

930 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \ 

931 
\ : set evs; \ 

932 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ 

933 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

934 
\ ==> Key ServKey ~: analz (spies evs)"; 

935 
by (blast_tac (claset() addSDs [Confidentiality_Kas, 

936 
Confidentiality_Tgs1]) 1); 

937 
qed "Confidentiality_Tgs2"; 

938 

939 
(*Most general form*) 

940 
val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2; 

941 

942 

943 
(********************** Guarantees for Alice *****************************) 

944 

945 
val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas; 

946 

947 
Goal 

948 
"[ Says Kas A \ 

949 
\ (Crypt (shrK A) {Key AuthKey, Agent Tgs, Tk, AuthTicket}) : set evs;\ 

950 
\ Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket} \ 

951 
\ : parts (spies evs); \ 

952 
\ Key AuthKey ~: analz (spies evs); \ 

953 
\ evs : kerberos ] \ 

954 
\==> Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket})\ 

955 
\ : set evs"; 

7499  956 
by (ftac Says_Kas_message_form 1 THEN assume_tac 1); 
6452  957 
by (etac rev_mp 1); 
958 
by (etac rev_mp 1); 

959 
by (etac rev_mp 1); 

960 
by (parts_induct_tac 1); 

961 
by (Fake_parts_insert_tac 1); 

962 
(*K2 and K4 remain*) 

963 
by (blast_tac (claset() addEs spies_partsEs addSEs [MPair_parts] 

964 
addSDs [unique_CryptKey]) 2); 

965 
by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form, 

966 
AuthKeys_used]) 1); 

967 
qed "A_trusts_K4_bis"; 

968 

969 

970 
Goal "[ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket} \ 

971 
\ : parts (spies evs); \ 

972 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 

973 
\ : parts (spies evs); \ 

974 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ 

975 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

976 
\ ==> Key ServKey ~: analz (spies evs)"; 

977 
by (dtac A_trusts_AuthKey 1); 

978 
by (assume_tac 1); 

979 
by (assume_tac 1); 

980 
by (blast_tac (claset() addDs [Confidentiality_Kas, 

981 
Says_Kas_message_form, 

982 
A_trusts_K4_bis, Confidentiality_Tgs2]) 1); 

983 
qed "Confidentiality_Serv_A"; 

984 

985 

986 
(********************** Guarantees for Bob *****************************) 

987 
(* Theorems for the refined model have suffix "refined" *) 

988 

989 
Goal 

990 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket})\ 

991 
\ : set evs; evs : kerberos] \ 

992 
\ ==> EX Tk. Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 

993 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

994 
\ : set evs"; 

995 
by (etac rev_mp 1); 

996 
by (parts_induct_tac 1); 

997 
by Auto_tac; 

998 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 

999 
A_trusts_AuthTicket]) 1); 

1000 
qed "K4_imp_K2"; 

1001 

1002 
Goal 

1003 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket})\ 

1004 
\ : set evs; evs : kerberos] \ 

1005 
\ ==> EX Tk. (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 

1006 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

1007 
\ : set evs \ 

1008 
\ & ServLife + Tt <= AuthLife + Tk)"; 

1009 
by (etac rev_mp 1); 

1010 
by (parts_induct_tac 1); 

1011 
by Auto_tac; 

1012 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 

1013 
A_trusts_AuthTicket]) 1); 

1014 
qed "K4_imp_K2_refined"; 

1015 

1016 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt} \ 

1017 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \ 

1018 
\ evs : kerberos ] \ 

1019 
\==> EX AuthKey. \ 

1020 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, \ 

1021 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}}) \ 

1022 
\ : set evs"; 

1023 
by (etac rev_mp 1); 

1024 
by (parts_induct_tac 1); 

1025 
by (Fake_parts_insert_tac 1); 

1026 
by (Blast_tac 1); 

1027 
qed "B_trusts_ServKey"; 

1028 

1029 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1030 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \ 

1031 
\ evs : kerberos ] \ 

1032 
\ ==> EX AuthKey Tk. Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 

1033 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

1034 
\ : set evs"; 

1035 
by (blast_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1); 

1036 
qed "B_trusts_ServTicket_Kas"; 

1037 

1038 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1039 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \ 

1040 
\ evs : kerberos ] \ 

1041 
\ ==> EX AuthKey Tk. (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 

1042 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

1043 
\ : set evs \ 

1044 
\ & ServLife + Tt <= AuthLife + Tk)"; 

1045 
by (blast_tac (claset() addSDs [B_trusts_ServKey,K4_imp_K2_refined]) 1); 

1046 
qed "B_trusts_ServTicket_Kas_refined"; 

1047 

1048 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1049 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \ 

1050 
\ evs : kerberos ] \ 

1051 
\==> EX Tk AuthKey. \ 

1052 
\ Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, \ 

1053 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

1054 
\ : set evs \ 

1055 
\ & Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 

1056 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}}) \ 

1057 
\ : set evs"; 

7499  1058 
by (ftac B_trusts_ServKey 1); 
6452  1059 
by (etac exE 4); 
7499  1060 
by (ftac K4_imp_K2 4); 
6452  1061 
by (Blast_tac 5); 
1062 
by (ALLGOALS assume_tac); 

1063 
qed "B_trusts_ServTicket"; 

1064 

1065 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1066 
\ : parts (spies evs); B ~= Tgs; B ~: bad; \ 

1067 
\ evs : kerberos ] \ 

1068 
\==> EX Tk AuthKey. \ 

1069 
\ (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, \ 

1070 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

1071 
\ : set evs \ 

1072 
\ & Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 

1073 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}}) \ 

1074 
\ : set evs \ 

1075 
\ & ServLife + Tt <= AuthLife + Tk)"; 

7499  1076 
by (ftac B_trusts_ServKey 1); 
6452  1077 
by (etac exE 4); 
7499  1078 
by (ftac K4_imp_K2_refined 4); 
6452  1079 
by (Blast_tac 5); 
1080 
by (ALLGOALS assume_tac); 

1081 
qed "B_trusts_ServTicket_refined"; 

1082 

1083 

1084 
Goal "[ ~ ExpirServ Tt evs; ServLife + Tt <= AuthLife + Tk ] \ 

1085 
\ ==> ~ ExpirAuth Tk evs"; 

1086 
by (blast_tac (claset() addDs [leI,le_trans] addEs [leE]) 1); 

1087 
qed "NotExpirServ_NotExpirAuth_refined"; 

1088 

1089 

1090 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1091 
\ : parts (spies evs); \ 

1092 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 

1093 
\ : parts (spies evs); \ 

1094 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 

1095 
\ : parts (spies evs); \ 

1096 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \ 

1097 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

1098 
\ ==> Key ServKey ~: analz (spies evs)"; 

7499  1099 
by (ftac A_trusts_AuthKey 1); 
1100 
by (ftac Confidentiality_Kas 3); 

1101 
by (ftac B_trusts_ServTicket 6); 

6452  1102 
by (etac exE 9); 
1103 
by (etac exE 9); 

7499  1104 
by (ftac Says_Kas_message_form 9); 
6452  1105 
by (blast_tac (claset() addDs [A_trusts_K4, 
1106 
unique_ServKeys, unique_AuthKeys, 

1107 
Confidentiality_Tgs2]) 10); 

1108 
by (ALLGOALS assume_tac); 

1109 
(* 

1110 
The proof above executes in 8 secs. It can be done in one command in 50 secs: 

1111 
by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4, 

1112 
Says_Kas_message_form, B_trusts_ServTicket, 

1113 
unique_ServKeys, unique_AuthKeys, 

1114 
Confidentiality_Kas, 

1115 
Confidentiality_Tgs2]) 1); 

1116 
*) 

1117 
qed "Confidentiality_B"; 

1118 

1119 

1120 
(*Most general form  only for refined model! *) 

1121 
Goal "[ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1122 
\ : parts (spies evs); \ 

1123 
\ ~ ExpirServ Tt evs; \ 

1124 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

1125 
\ ==> Key ServKey ~: analz (spies evs)"; 

1126 
by (blast_tac (claset() addDs [B_trusts_ServTicket_refined, 

1127 
NotExpirServ_NotExpirAuth_refined, 

1128 
Confidentiality_Tgs2]) 1); 

1129 
qed "Confidentiality_B_refined"; 

1130 

1131 

1132 
(********************** Authenticity theorems *****************************) 

1133 

1134 
(***1. Session Keys authenticity: they originated with servers.***) 

1135 

1136 
(*Authenticity of AuthKey for A: "A_trusts_AuthKey"*) 

1137 

1138 
(*Authenticity of ServKey for A: "A_trusts_ServKey"*) 

1139 
Goal "[ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket} \ 

1140 
\ : parts (spies evs); \ 

1141 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 

1142 
\ : parts (spies evs); \ 

1143 
\ ~ ExpirAuth Tk evs; A ~: bad; evs : kerberos ] \ 

1144 
\==>Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket})\ 

1145 
\ : set evs"; 

7499  1146 
by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1); 
6452  1147 
by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1); 
1148 
qed "A_trusts_ServKey"; 

1149 
(*Note: requires a temporal check*) 

1150 

1151 

1152 
(*Authenticity of ServKey for B: "B_trusts_ServKey"*) 

1153 

1154 
(***2. Parties authenticity: each party verifies "the identity of 

1155 
another party who generated some data" (quoted from Neuman & Ts'o).***) 

1156 

1157 
(*These guarantees don't assess whether two parties agree on 

1158 
the same session key: sending a message containing a key 

1159 
doesn't a priori state knowledge of the key.***) 

1160 

1161 
(*B checks authenticity of A: theorems "A_Authenticity", 

1162 
"A_authenticity_refined" *) 

1163 
Goal "[ Crypt ServKey {Agent A, Number Ta} : parts (spies evs); \ 

1164 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 

1165 
\ ServTicket}) : set evs; \ 

1166 
\ Key ServKey ~: analz (spies evs); \ 

1167 
\ A ~: bad; B ~: bad; evs : kerberos ] \ 

1168 
\==> Says A B {ServTicket, Crypt ServKey {Agent A, Number Ta}} : set evs"; 

1169 
by (etac rev_mp 1); 

1170 
by (etac rev_mp 1); 

1171 
by (etac rev_mp 1); 

1172 
by (etac kerberos.induct 1); 

7499  1173 
by (ftac Says_ticket_in_parts_spies 5); 
1174 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1175 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1176 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

1177 
by (Fake_parts_insert_tac 1); 

1178 
(*K3*) 

1179 
by (blast_tac (claset() addEs spies_partsEs 

1180 
addDs [A_trusts_AuthKey, 

1181 
Says_Kas_message_form, 

1182 
Says_Tgs_message_form]) 1); 

1183 
(*K4*) 

1184 
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 

1185 
(*K5*) 

1186 
by (blast_tac (claset() addDs [Key_unique_SesKey] addEs spies_partsEs) 1); 

1187 
qed "Says_Auth"; 

1188 

1189 
(*The second assumption tells B what kind of key ServKey is.*) 

1190 
Goal "[ Crypt ServKey {Agent A, Number Ta} : parts (spies evs); \ 

1191 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1192 
\ : parts (spies evs); \ 

1193 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 

1194 
\ : parts (spies evs); \ 

1195 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket} \ 

1196 
\ : parts (spies evs); \ 

1197 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \ 

1198 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \ 

1199 
\ ==> Says A B {Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt},\ 

1200 
\ Crypt ServKey {Agent A, Number Ta} } : set evs"; 

7499  1201 
by (ftac Confidentiality_B 1); 
1202 
by (ftac B_trusts_ServKey 9); 

6452  1203 
by (etac exE 12); 
1204 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 

1205 
addSIs [Says_Auth]) 12); 

1206 
by (ALLGOALS assume_tac); 

1207 
qed "A_Authenticity"; 

1208 

1209 
(*Stronger form in the refined model*) 

1210 
Goal "[ Crypt ServKey {Agent A, Number Ta2} : parts (spies evs); \ 

1211 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1212 
\ : parts (spies evs); \ 

1213 
\ ~ ExpirServ Tt evs; \ 

1214 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \ 

1215 
\ ==> Says A B {Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt},\ 

1216 
\ Crypt ServKey {Agent A, Number Ta2} } : set evs"; 

7499  1217 
by (ftac Confidentiality_B_refined 1); 
1218 
by (ftac B_trusts_ServKey 6); 

6452  1219 
by (etac exE 9); 
1220 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 

1221 
addSIs [Says_Auth]) 9); 

1222 
by (ALLGOALS assume_tac); 

1223 
qed "A_Authenticity_refined"; 

1224 

1225 

1226 
(*A checks authenticity of B: theorem "B_authenticity"*) 

1227 

1228 
Goal "[ Crypt ServKey (Number Ta) : parts (spies evs); \ 

1229 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 

1230 
\ ServTicket}) : set evs; \ 

1231 
\ Key ServKey ~: analz (spies evs); \ 

1232 
\ A ~: bad; B ~: bad; evs : kerberos ] \ 

1233 
\ ==> Says B A (Crypt ServKey (Number Ta)) : set evs"; 

1234 
by (etac rev_mp 1); 

1235 
by (etac rev_mp 1); 

1236 
by (etac rev_mp 1); 

1237 
by (etac kerberos.induct 1); 

7499  1238 
by (ftac Says_ticket_in_parts_spies 5); 
1239 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1240 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1241 
by (ALLGOALS Asm_simp_tac); 

1242 
by (Fake_parts_insert_tac 1); 

1243 
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 

1244 
by (Clarify_tac 1); 

7499  1245 
by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); 
6452  1246 
by (Clarify_tac 1); (*PROOF FAILED if omitted*) 
1247 
by (blast_tac (claset() addDs [unique_CryptKey] addEs spies_partsEs) 1); 

1248 
qed "Says_K6"; 

1249 

1250 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, T, ServTicket} \ 

1251 
\ : parts (spies evs); \ 

1252 
\ Key AuthKey ~: analz (spies evs); AuthKey ~: range shrK; \ 

1253 
\ evs : kerberos ] \ 

1254 
\ ==> EX A. Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, T, ServTicket})\ 

1255 
\ : set evs"; 

1256 
by (etac rev_mp 1); 

1257 
by (etac rev_mp 1); 

1258 
by (parts_induct_tac 1); 

1259 
by (Fake_parts_insert_tac 1); 

1260 
by (Blast_tac 1); 

1261 
by (Blast_tac 1); 

1262 
qed "K4_trustworthy"; 

1263 

1264 
Goal "[ Crypt ServKey (Number Ta) : parts (spies evs); \ 

1265 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 

1266 
\ : parts (spies evs); \ 

1267 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 

1268 
\ : parts (spies evs); \ 

1269 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ 

1270 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

1271 
\ ==> Says B A (Crypt ServKey (Number Ta)) : set evs"; 

7499  1272 
by (ftac A_trusts_AuthKey 1); 
1273 
by (ftac Says_Kas_message_form 3); 

1274 
by (ftac Confidentiality_Kas 4); 

1275 
by (ftac K4_trustworthy 7); 

6452  1276 
by (Blast_tac 8); 
1277 
by (etac exE 9); 

7499  1278 
by (ftac K4_imp_K2 9); 
6452  1279 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 
1280 
addSIs [Says_K6] 

1281 
addSEs [Confidentiality_Tgs1 RSN (2,rev_notE)]) 10); 

1282 
by (ALLGOALS assume_tac); 

1283 
qed "B_Authenticity"; 

1284 

1285 

1286 
(***3. Parties' knowledge of session keys. A knows a session key if she 

1287 
used it to build a cipher.***) 

1288 

1289 
Goal "[ Says B A (Crypt ServKey (Number Ta)) : set evs; \ 

1290 
\ Key ServKey ~: analz (spies evs); \ 

1291 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

1292 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"; 

1293 
by (simp_tac (simpset() addsimps [Issues_def]) 1); 

1294 
by (rtac exI 1); 

1295 
by (rtac conjI 1); 

1296 
by (assume_tac 1); 

1297 
by (Simp_tac 1); 

1298 
by (etac rev_mp 1); 

1299 
by (etac rev_mp 1); 

1300 
by (etac kerberos.induct 1); 

7499  1301 
by (ftac Says_ticket_in_parts_spies 5); 
1302 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1303 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1304 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

1305 
by (Fake_parts_insert_tac 1); 

1306 
(*K6 requires numerous lemmas*) 

1307 
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1); 

1308 
by (blast_tac (claset() addDs [B_trusts_ServTicket, 

1309 
impOfSubs parts_spies_takeWhile_mono, 

1310 
impOfSubs parts_spies_evs_revD2] 

1311 
addIs [Says_K6] 

1312 
addEs spies_partsEs) 1); 

1313 
qed "B_Knows_B_Knows_ServKey_lemma"; 

1314 
(*Key ServKey ~: analz (spies evs) could be relaxed by Confidentiality_B 

1315 
but this is irrelevant because B knows what he knows! *) 

1316 

1317 
Goal "[ Says B A (Crypt ServKey (Number Ta)) : set evs; \ 

1318 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}\ 

1319 
\ : parts (spies evs);\ 

1320 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}\ 

1321 
\ : parts (spies evs);\ 

1322 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 

1323 
\ : parts (spies evs); \ 

1324 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \ 

1325 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

1326 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"; 

1327 
by (blast_tac (claset() addSDs [Confidentiality_B, 

1328 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1329 
qed "B_Knows_B_Knows_ServKey"; 

1330 

1331 
Goal "[ Says B A (Crypt ServKey (Number Ta)) : set evs; \ 

1332 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}\ 

1333 
\ : parts (spies evs);\ 

1334 
\ ~ ExpirServ Tt evs; \ 

1335 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

1336 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"; 

1337 
by (blast_tac (claset() addSDs [Confidentiality_B_refined, 

1338 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1339 
qed "B_Knows_B_Knows_ServKey_refined"; 

1340 

1341 

1342 
Goal "[ Crypt ServKey (Number Ta) : parts (spies evs); \ 

1343 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 

1344 
\ : parts (spies evs); \ 

1345 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 

1346 
\ : parts (spies evs); \ 

1347 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ 

1348 
\ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos ] \ 

1349 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"; 

1350 
by (blast_tac (claset() addSDs [B_Authenticity, Confidentiality_Serv_A, 

1351 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1352 
qed "A_Knows_B_Knows_ServKey"; 

1353 

1354 
Goal "[ Says A Tgs \ 

1355 
\ {AuthTicket, Crypt AuthKey {Agent A, Number Ta}, Agent B}\ 

1356 
\ : set evs; \ 

1357 
\ A ~: bad; evs : kerberos ] \ 

1358 
\ ==> EX Tk. Says Kas A (Crypt (shrK A) \ 

1359 
\ {Key AuthKey, Agent Tgs, Tk, AuthTicket}) \ 

1360 
\ : set evs"; 

1361 
by (etac rev_mp 1); 

1362 
by (parts_induct_tac 1); 

1363 
by (Fake_parts_insert_tac 1); 

1364 
by (Blast_tac 1); 

1365 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS 

1366 
A_trusts_AuthKey]) 1); 

1367 
qed "K3_imp_K2"; 

1368 

1369 
Goal "[ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 

1370 
\ : parts (spies evs); \ 

1371 
\ Says Kas A (Crypt (shrK A) \ 

1372 
\ {Key AuthKey, Agent Tgs, Tk, AuthTicket}) \ 

1373 
\ : set evs; \ 

1374 
\ Key AuthKey ~: analz (spies evs); \ 

1375 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \ 

1376 
\ ==> Says Tgs A (Crypt AuthKey \ 

1377 
\ {Key ServKey, Agent B, Number Tt, ServTicket}) \ 

1378 
\ : set evs"; 

1379 
by (etac rev_mp 1); 

1380 
by (etac rev_mp 1); 

1381 
by (etac rev_mp 1); 

1382 
by (parts_induct_tac 1); 

1383 
by (Fake_parts_insert_tac 1); 

1384 
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 

1385 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 

1386 
A_trusts_AuthTicket, unique_AuthKeys]) 1); 

1387 
qed "K4_trustworthy'"; 

1388 

1389 
Goal "[ Says A B {ServTicket, Crypt ServKey {Agent A, Number Ta}} \ 

1390 
\ : set evs; \ 

1391 
\ Key ServKey ~: analz (spies evs); \ 

1392 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \ 

1393 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs"; 

1394 
by (simp_tac (simpset() addsimps [Issues_def]) 1); 

1395 
by (rtac exI 1); 

1396 
by (rtac conjI 1); 

1397 
by (assume_tac 1); 

1398 
by (Simp_tac 1); 

1399 
by (etac rev_mp 1); 

1400 
by (etac rev_mp 1); 

1401 
by (etac kerberos.induct 1); 

7499  1402 
by (ftac Says_ticket_in_parts_spies 5); 
1403 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1404 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1405 
by (ALLGOALS Asm_simp_tac); 

1406 
by (Clarify_tac 1); 

1407 
(*K6*) 

1408 
by Auto_tac; 

1409 
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1); 

1410 
(*Level 15: case study necessary because the assumption doesn't state 

1411 
the form of ServTicket. The guarantee becomes stronger.*) 

1412 
by (case_tac "Key AuthKey : analz (spies evs5)" 1); 

1413 
by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 

1414 
analz.Decrypt RS analz.Fst], 

1415 
simpset()) 1); 

1416 
by (blast_tac (claset() addDs [K3_imp_K2, K4_trustworthy', 

1417 
impOfSubs parts_spies_takeWhile_mono, 

1418 
impOfSubs parts_spies_evs_revD2] 

1419 
addIs [Says_Auth] 

1420 
addEs spies_partsEs) 1); 

1421 
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1); 

1422 
qed "A_Knows_A_Knows_ServKey_lemma"; 

1423 

1424 
Goal "[ Says A B {ServTicket, Crypt ServKey {Agent A, Number Ta}} \ 

1425 
\ : set evs; \ 

1426 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 

1427 
\ : parts (spies evs);\ 

1428 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}\ 

1429 
\ : parts (spies evs); \ 

1430 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;\ 

1431 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \ 

1432 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs"; 

1433 
by (blast_tac (claset() addSDs [Confidentiality_Serv_A, 

1434 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1435 
qed "A_Knows_A_Knows_ServKey"; 

1436 

1437 
Goal "[ Crypt ServKey {Agent A, Number Ta} : parts (spies evs); \ 

1438 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1439 
\ : parts (spies evs); \ 

1440 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 

1441 
\ : parts (spies evs); \ 

1442 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket} \ 

1443 
\ : parts (spies evs); \ 

1444 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \ 

1445 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \ 

1446 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs"; 

1447 
by (blast_tac (claset() addDs [A_Authenticity, Confidentiality_B, 

1448 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1449 
qed "B_Knows_A_Knows_ServKey"; 

1450 

1451 

1452 
Goal "[ Crypt ServKey {Agent A, Number Ta} : parts (spies evs); \ 

1453 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 

1454 
\ : parts (spies evs); \ 

1455 
\ ~ ExpirServ Tt evs; \ 

1456 
\ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos ] \ 

1457 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs"; 

1458 
by (blast_tac (claset() addDs [A_Authenticity_refined, 

1459 
Confidentiality_B_refined, 

1460 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1461 
qed "B_Knows_A_Knows_ServKey_refined"; 