author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9000  c20d58286a51 
child 10833  c0844a30ea4e 
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; 

9000  10 
set timing; 
6452  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 

8954
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

658 
(*For the Oops2 case of the next theorem*) 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

659 
Goal "[ evs : kerberos; \ 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

660 
\ Says Tgs A (Crypt AuthKey \ 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

661 
\ {Key ServKey, Agent B, Number Tt, ServTicket}) \ 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

662 
\ : set evs ] \ 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

663 
\ ==> ~ KeyCryptKey ServKey SK evs"; 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

664 
by (blast_tac (claset() addDs [KeyCryptKeyI, KeyCryptKey_not_KeyCryptKey]) 1); 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

665 
qed "Oops2_not_KeyCryptKey"; 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

666 

4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

667 

6452  668 
(* Big simplification law for keys SK that are not crypted by keys in KK *) 
669 
(* It helps prove three, otherwise hard, facts about keys. These facts are *) 

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

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

8954
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

672 
(* [simplified by LCP] *) 
6452  673 
Goal "evs : kerberos ==> \ 
674 
\ (ALL SK KK. KK <= (range shrK) > \ 

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

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

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

678 
by (etac kerberos.induct 1); 

679 
by analz_sees_tac; 

680 
by (REPEAT_FIRST (rtac allI)); 

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

8954
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

682 
(*Casesplits for Oops1 & 5: the negated case simplifies using the ind hyp*) 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

683 
by (case_tac "KeyCryptKey AuthKey SK evsO1" 11); 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

684 
by (case_tac "KeyCryptKey ServKey SK evs5" 8); 
6452  685 
by (ALLGOALS 
686 
(asm_simp_tac 

687 
(analz_image_freshK_ss addsimps 

8954
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

688 
[KeyCryptKey_Says, shrK_not_KeyCryptKey, Oops2_not_KeyCryptKey, 
6452  689 
Auth_fresh_not_KeyCryptKey, Serv_fresh_not_KeyCryptKey, 
690 
Says_Tgs_KeyCryptKey, Spy_analz_shrK]))); 

691 
(*Fake*) 

692 
by (spy_analz_tac 1); 

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

694 
(*K3*) 

695 
by (Blast_tac 1); 

696 
(*K4*) 

697 
by (blast_tac (claset() addEs spies_partsEs 

698 
addSDs [AuthKey_not_KeyCryptKey]) 1); 

699 
(*K5*) 

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

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

702 
by (asm_simp_tac 

703 
(simpset() addsimps [analz_insert_eq, 

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

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

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

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

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

8954
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

709 
(** Level 13: Oops1 **) 
4fbdda40bb5f
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
paulson
parents:
8741
diff
changeset

710 
by (Asm_full_simp_tac 1); 
6452  711 
by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1); 
712 
qed_spec_mp "Key_analz_image_Key"; 

713 

714 

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

716 
(* authentication keys or shared keys. *) 

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

718 
\ SesKey ~: range shrK ] \ 

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

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

7499  721 
by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1); 
6452  722 
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); 
723 
qed "analz_insert_freshK1"; 

724 

725 

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

727 
(* any other keys. *) 

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

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

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

7499  731 
by (ftac not_AuthKeys_not_KeyCryptKey 1 
6452  732 
THEN assume_tac 1 
733 
THEN assume_tac 1); 

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

735 
qed "analz_insert_freshK2"; 

736 

737 

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

739 
(* encrypts a certain service key. *) 

740 
Goal 

741 
"[ Says Tgs A \ 

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

743 
\ : set evs; \ 

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

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

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

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

748 
by (Blast_tac 1); 

749 
by (assume_tac 1); 

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

751 
qed "analz_insert_freshK3"; 

752 

753 

754 
(*a weakness of the protocol*) 

755 
Goal "[ Says Tgs A \ 

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

757 
\ : set evs; \ 

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

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

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

761 
analz.Decrypt RS analz.Fst], 

762 
simpset()) 1); 

763 
qed "AuthKey_compromises_ServKey"; 

764 

765 

766 
(********************** Guarantees for Kas *****************************) 

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

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

769 
\ : parts (spies evs); \ 

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

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

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

773 
by (etac rev_mp 1); 

774 
by (etac rev_mp 1); 

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

776 
by (parts_induct_tac 1); 

777 
by (Fake_parts_insert_tac 1); 

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

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

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

781 

782 

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

784 
the Key has expired **) 

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

786 
\ ==> Says Kas A \ 

787 
\ (Crypt (shrK A) \ 

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

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

790 
\ : set evs > \ 

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

792 
\ ExpirAuth Tk evs"; 

793 
by (etac kerberos.induct 1); 

794 
by analz_sees_tac; 

795 
by (ALLGOALS 

796 
(asm_simp_tac 

8741
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
7499
diff
changeset

797 
(simpset() addsimps ([Says_Kas_message_form, less_SucI, 
6452  798 
analz_insert_eq, not_parts_not_analz, 
799 
analz_insert_freshK1] @ pushes)))); 

800 
(*Fake*) 

801 
by (spy_analz_tac 1); 

802 
(*K2*) 

803 
by (blast_tac (claset() addSEs spies_partsEs 

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

805 
(*K4*) 

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

807 
(*Level 8: K5*) 

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

809 
addDs [Says_Kas_message_form, 

810 
Says_imp_spies RS parts.Inj] 

811 
addIs [less_SucI]) 1); 

812 
(*Oops1*) 

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

814 
(*Oops2*) 

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

816 
Says_Kas_message_form]) 1); 

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

818 

819 

820 
Goal "[ Says Kas A \ 

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

822 
\ : set evs; \ 

823 
\ ~ ExpirAuth Tk evs; \ 

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

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

7499  826 
by (ftac Says_Kas_message_form 1 THEN assume_tac 1); 
6452  827 
by (blast_tac (claset() addSDs [lemma]) 1); 
828 
qed "Confidentiality_Kas"; 

829 

830 

831 

832 

833 

834 

835 
(********************** Guarantees for Tgs *****************************) 

836 

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

838 
the Key has expired **) 

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

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

841 
\ Says Tgs A \ 

842 
\ (Crypt AuthKey \ 

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

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

845 
\ : set evs > \ 

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

847 
\ ExpirServ Tt evs"; 

848 
by (etac kerberos.induct 1); 

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

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

851 
conclude AuthKey ~= AuthKeya.*) 

852 
by (Clarify_tac 9); 

853 
by analz_sees_tac; 

854 
by (rotate_tac ~1 11); 

855 
by (ALLGOALS 

856 
(asm_full_simp_tac 

8741
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
7499
diff
changeset

857 
(simpset() addsimps [less_SucI, 
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
7499
diff
changeset

858 
Says_Kas_message_form, Says_Tgs_message_form, 
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
7499
diff
changeset

859 
analz_insert_eq, not_parts_not_analz, 
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
7499
diff
changeset

860 
analz_insert_freshK1, analz_insert_freshK2] 
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
7499
diff
changeset

861 
@ pushes))); 
6452  862 
(*Fake*) 
863 
by (spy_analz_tac 1); 

864 
(*K2*) 

865 
by (blast_tac (claset() addSEs spies_partsEs 

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

867 
(*K4*) 

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

869 
by (blast_tac (claset() addSEs spies_partsEs 

870 
addIs [less_SucI]) 1); 

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

872 
A_trusts_AuthTicket, 

873 
Confidentiality_Kas, 

874 
impOfSubs analz_subset_parts]) 1); 

875 
by (ALLGOALS Clarify_tac); 

876 
(*Oops2*) 

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

878 
Key_unique_SesKey] addIs [less_SucI]) 3); 

879 
(** Level 12 **) 

880 
(*Oops1*) 

7499  881 
by (ftac Says_Kas_message_form 2); 
6452  882 
by (assume_tac 2); 
883 
by (blast_tac (claset() addDs [analz_insert_freshK3, 

884 
Says_Kas_message_form, Says_Tgs_message_form] 

885 
addIs [less_SucI]) 2); 

886 
(** Level 16 **) 

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

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

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

890 
by (rotate_tac ~1 1); 

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

892 
by (etac disjE 1); 

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

894 
Key_unique_SesKey]) 1); 

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

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

897 

898 

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

900 
Goal 

901 
"[ Says Tgs A \ 

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

903 
\ : set evs; \ 

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

905 
\ ~ ExpirServ Tt evs; \ 

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

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

7499  908 
by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); 
6452  909 
by (blast_tac (claset() addDs [lemma]) 1); 
910 
qed "Confidentiality_Tgs1"; 

911 

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

913 
Goal 

914 
"[ Says Kas A \ 

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

916 
\ : set evs; \ 

917 
\ Says Tgs A \ 

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

919 
\ : set evs; \ 

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

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

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

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

924 
Confidentiality_Tgs1]) 1); 

925 
qed "Confidentiality_Tgs2"; 

926 

927 
(*Most general form*) 

928 
val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2; 

929 

930 

931 
(********************** Guarantees for Alice *****************************) 

932 

933 
val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas; 

934 

935 
Goal 

936 
"[ Says Kas A \ 

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

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

939 
\ : parts (spies evs); \ 

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

941 
\ evs : kerberos ] \ 

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

943 
\ : set evs"; 

7499  944 
by (ftac Says_Kas_message_form 1 THEN assume_tac 1); 
6452  945 
by (etac rev_mp 1); 
946 
by (etac rev_mp 1); 

947 
by (etac rev_mp 1); 

948 
by (parts_induct_tac 1); 

949 
by (Fake_parts_insert_tac 1); 

950 
(*K2 and K4 remain*) 

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

952 
addSDs [unique_CryptKey]) 2); 

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

954 
AuthKeys_used]) 1); 

955 
qed "A_trusts_K4_bis"; 

956 

957 

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

959 
\ : parts (spies evs); \ 

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

961 
\ : parts (spies evs); \ 

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

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

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

965 
by (dtac A_trusts_AuthKey 1); 

966 
by (assume_tac 1); 

967 
by (assume_tac 1); 

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

969 
Says_Kas_message_form, 

970 
A_trusts_K4_bis, Confidentiality_Tgs2]) 1); 

971 
qed "Confidentiality_Serv_A"; 

972 

973 

974 
(********************** Guarantees for Bob *****************************) 

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

976 

977 
Goal 

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

979 
\ : set evs; evs : kerberos] \ 

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

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

982 
\ : set evs"; 

983 
by (etac rev_mp 1); 

984 
by (parts_induct_tac 1); 

985 
by Auto_tac; 

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

987 
A_trusts_AuthTicket]) 1); 

988 
qed "K4_imp_K2"; 

989 

990 
Goal 

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

992 
\ : set evs; evs : kerberos] \ 

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

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

995 
\ : set evs \ 

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

997 
by (etac rev_mp 1); 

998 
by (parts_induct_tac 1); 

999 
by Auto_tac; 

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

1001 
A_trusts_AuthTicket]) 1); 

1002 
qed "K4_imp_K2_refined"; 

1003 

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

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

1006 
\ evs : kerberos ] \ 

1007 
\==> EX AuthKey. \ 

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

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

1010 
\ : set evs"; 

1011 
by (etac rev_mp 1); 

1012 
by (parts_induct_tac 1); 

1013 
by (Fake_parts_insert_tac 1); 

1014 
by (Blast_tac 1); 

1015 
qed "B_trusts_ServKey"; 

1016 

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

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

1019 
\ evs : kerberos ] \ 

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

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

1022 
\ : set evs"; 

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

1024 
qed "B_trusts_ServTicket_Kas"; 

1025 

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

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

1028 
\ evs : kerberos ] \ 

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

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

1031 
\ : set evs \ 

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

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

1034 
qed "B_trusts_ServTicket_Kas_refined"; 

1035 

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

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

1038 
\ evs : kerberos ] \ 

1039 
\==> EX Tk AuthKey. \ 

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

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

1042 
\ : set evs \ 

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

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

1045 
\ : set evs"; 

7499  1046 
by (ftac B_trusts_ServKey 1); 
6452  1047 
by (etac exE 4); 
7499  1048 
by (ftac K4_imp_K2 4); 
6452  1049 
by (Blast_tac 5); 
1050 
by (ALLGOALS assume_tac); 

1051 
qed "B_trusts_ServTicket"; 

1052 

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

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

1055 
\ evs : kerberos ] \ 

1056 
\==> EX Tk AuthKey. \ 

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

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

1059 
\ : set evs \ 

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

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

1062 
\ : set evs \ 

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

7499  1064 
by (ftac B_trusts_ServKey 1); 
6452  1065 
by (etac exE 4); 
7499  1066 
by (ftac K4_imp_K2_refined 4); 
6452  1067 
by (Blast_tac 5); 
1068 
by (ALLGOALS assume_tac); 

1069 
qed "B_trusts_ServTicket_refined"; 

1070 

1071 

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

1073 
\ ==> ~ ExpirAuth Tk evs"; 

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

1075 
qed "NotExpirServ_NotExpirAuth_refined"; 

1076 

1077 

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

1079 
\ : parts (spies evs); \ 

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

1081 
\ : parts (spies evs); \ 

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

1083 
\ : parts (spies evs); \ 

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

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

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

7499  1087 
by (ftac A_trusts_AuthKey 1); 
1088 
by (ftac Confidentiality_Kas 3); 

1089 
by (ftac B_trusts_ServTicket 6); 

6452  1090 
by (etac exE 9); 
1091 
by (etac exE 9); 

7499  1092 
by (ftac Says_Kas_message_form 9); 
6452  1093 
by (blast_tac (claset() addDs [A_trusts_K4, 
1094 
unique_ServKeys, unique_AuthKeys, 

1095 
Confidentiality_Tgs2]) 10); 

1096 
by (ALLGOALS assume_tac); 

1097 
(* 

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

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

1100 
Says_Kas_message_form, B_trusts_ServTicket, 

1101 
unique_ServKeys, unique_AuthKeys, 

1102 
Confidentiality_Kas, 

1103 
Confidentiality_Tgs2]) 1); 

1104 
*) 

1105 
qed "Confidentiality_B"; 

1106 

1107 

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

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

1110 
\ : parts (spies evs); \ 

1111 
\ ~ ExpirServ Tt evs; \ 

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

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

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

1115 
NotExpirServ_NotExpirAuth_refined, 

1116 
Confidentiality_Tgs2]) 1); 

1117 
qed "Confidentiality_B_refined"; 

1118 

1119 

1120 
(********************** Authenticity theorems *****************************) 

1121 

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

1123 

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

1125 

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

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

1128 
\ : parts (spies evs); \ 

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

1130 
\ : parts (spies evs); \ 

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

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

1133 
\ : set evs"; 

7499  1134 
by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1); 
6452  1135 
by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1); 
1136 
qed "A_trusts_ServKey"; 

1137 
(*Note: requires a temporal check*) 

1138 

1139 

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

1141 

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

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

1144 

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

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

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

1148 

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

1150 
"A_authenticity_refined" *) 

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

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

1153 
\ ServTicket}) : set evs; \ 

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

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

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

1157 
by (etac rev_mp 1); 

1158 
by (etac rev_mp 1); 

1159 
by (etac rev_mp 1); 

1160 
by (etac kerberos.induct 1); 

7499  1161 
by (ftac Says_ticket_in_parts_spies 5); 
1162 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1163 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1164 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

1165 
by (Fake_parts_insert_tac 1); 

1166 
(*K3*) 

1167 
by (blast_tac (claset() addEs spies_partsEs 

1168 
addDs [A_trusts_AuthKey, 

1169 
Says_Kas_message_form, 

1170 
Says_Tgs_message_form]) 1); 

1171 
(*K4*) 

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

1173 
(*K5*) 

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

1175 
qed "Says_Auth"; 

1176 

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

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

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

1180 
\ : parts (spies evs); \ 

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

1182 
\ : parts (spies evs); \ 

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

1184 
\ : parts (spies evs); \ 

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

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

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

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

7499  1189 
by (ftac Confidentiality_B 1); 
1190 
by (ftac B_trusts_ServKey 9); 

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

1193 
addSIs [Says_Auth]) 12); 

1194 
by (ALLGOALS assume_tac); 

1195 
qed "A_Authenticity"; 

1196 

1197 
(*Stronger form in the refined model*) 

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

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

1200 
\ : parts (spies evs); \ 

1201 
\ ~ ExpirServ Tt evs; \ 

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

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

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

7499  1205 
by (ftac Confidentiality_B_refined 1); 
1206 
by (ftac B_trusts_ServKey 6); 

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

1209 
addSIs [Says_Auth]) 9); 

1210 
by (ALLGOALS assume_tac); 

1211 
qed "A_Authenticity_refined"; 

1212 

1213 

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

1215 

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

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

1218 
\ ServTicket}) : set evs; \ 

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

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

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

1222 
by (etac rev_mp 1); 

1223 
by (etac rev_mp 1); 

1224 
by (etac rev_mp 1); 

1225 
by (etac kerberos.induct 1); 

7499  1226 
by (ftac Says_ticket_in_parts_spies 5); 
1227 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1228 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1229 
by (ALLGOALS Asm_simp_tac); 

1230 
by (Fake_parts_insert_tac 1); 

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

1232 
by (Clarify_tac 1); 

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

1236 
qed "Says_K6"; 

1237 

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

1239 
\ : parts (spies evs); \ 

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

1241 
\ evs : kerberos ] \ 

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

1243 
\ : set evs"; 

1244 
by (etac rev_mp 1); 

1245 
by (etac rev_mp 1); 

1246 
by (parts_induct_tac 1); 

1247 
by (Fake_parts_insert_tac 1); 

1248 
by (Blast_tac 1); 

1249 
by (Blast_tac 1); 

1250 
qed "K4_trustworthy"; 

1251 

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

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

1254 
\ : parts (spies evs); \ 

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

1256 
\ : parts (spies evs); \ 

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

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

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

7499  1260 
by (ftac A_trusts_AuthKey 1); 
1261 
by (ftac Says_Kas_message_form 3); 

1262 
by (ftac Confidentiality_Kas 4); 

1263 
by (ftac K4_trustworthy 7); 

6452  1264 
by (Blast_tac 8); 
1265 
by (etac exE 9); 

7499  1266 
by (ftac K4_imp_K2 9); 
6452  1267 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 
1268 
addSIs [Says_K6] 

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

1270 
by (ALLGOALS assume_tac); 

1271 
qed "B_Authenticity"; 

1272 

1273 

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

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

1276 

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

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

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

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

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

1282 
by (rtac exI 1); 

1283 
by (rtac conjI 1); 

1284 
by (assume_tac 1); 

1285 
by (Simp_tac 1); 

1286 
by (etac rev_mp 1); 

1287 
by (etac rev_mp 1); 

1288 
by (etac kerberos.induct 1); 

7499  1289 
by (ftac Says_ticket_in_parts_spies 5); 
1290 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1291 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1292 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

1293 
by (Fake_parts_insert_tac 1); 

1294 
(*K6 requires numerous lemmas*) 

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

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

1297 
impOfSubs parts_spies_takeWhile_mono, 

1298 
impOfSubs parts_spies_evs_revD2] 

1299 
addIs [Says_K6] 

1300 
addEs spies_partsEs) 1); 

1301 
qed "B_Knows_B_Knows_ServKey_lemma"; 

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

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

1304 

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

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

1307 
\ : parts (spies evs);\ 

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

1309 
\ : parts (spies evs);\ 

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

1311 
\ : parts (spies evs); \ 

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

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

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

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

1316 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1317 
qed "B_Knows_B_Knows_ServKey"; 

1318 

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

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

1321 
\ : parts (spies evs);\ 

1322 
\ ~ ExpirServ Tt evs; \ 

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

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

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

1326 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1327 
qed "B_Knows_B_Knows_ServKey_refined"; 

1328 

1329 

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

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

1332 
\ : parts (spies evs); \ 

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

1334 
\ : parts (spies evs); \ 

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

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

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

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

1339 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1340 
qed "A_Knows_B_Knows_ServKey"; 

1341 

1342 
Goal "[ Says A Tgs \ 

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

1344 
\ : set evs; \ 

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

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

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

1348 
\ : set evs"; 

1349 
by (etac rev_mp 1); 

1350 
by (parts_induct_tac 1); 

1351 
by (Fake_parts_insert_tac 1); 

1352 
by (Blast_tac 1); 

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

1354 
A_trusts_AuthKey]) 1); 

1355 
qed "K3_imp_K2"; 

1356 

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

1358 
\ : parts (spies evs); \ 

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

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

1361 
\ : set evs; \ 

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

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

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

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

1366 
\ : set evs"; 

1367 
by (etac rev_mp 1); 

1368 
by (etac rev_mp 1); 

1369 
by (etac rev_mp 1); 

1370 
by (parts_induct_tac 1); 

1371 
by (Fake_parts_insert_tac 1); 

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

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

1374 
A_trusts_AuthTicket, unique_AuthKeys]) 1); 

1375 
qed "K4_trustworthy'"; 

1376 

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

1378 
\ : set evs; \ 

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

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

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

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

1383 
by (rtac exI 1); 

1384 
by (rtac conjI 1); 

1385 
by (assume_tac 1); 

1386 
by (Simp_tac 1); 

1387 
by (etac rev_mp 1); 

1388 
by (etac rev_mp 1); 

1389 
by (etac kerberos.induct 1); 

7499  1390 
by (ftac Says_ticket_in_parts_spies 5); 
1391 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1392 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1393 
by (ALLGOALS Asm_simp_tac); 

1394 
by (Clarify_tac 1); 

1395 
(*K6*) 

1396 
by Auto_tac; 

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

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

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

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

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

1402 
analz.Decrypt RS analz.Fst], 

1403 
simpset()) 1); 

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

1405 
impOfSubs parts_spies_takeWhile_mono, 

1406 
impOfSubs parts_spies_evs_revD2] 

1407 
addIs [Says_Auth] 

1408 
addEs spies_partsEs) 1); 

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

1410 
qed "A_Knows_A_Knows_ServKey_lemma"; 

1411 

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

1413 
\ : set evs; \ 

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

1415 
\ : parts (spies evs);\ 

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

1417 
\ : parts (spies evs); \ 

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

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

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

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

1422 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1423 
qed "A_Knows_A_Knows_ServKey"; 

1424 

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

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

1427 
\ : parts (spies evs); \ 

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

1429 
\ : parts (spies evs); \ 

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

1431 
\ : parts (spies evs); \ 

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

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

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

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

1436 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1437 
qed "B_Knows_A_Knows_ServKey"; 

1438 

1439 

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

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

1442 
\ : parts (spies evs); \ 

1443 
\ ~ ExpirServ Tt evs; \ 

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

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

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

1447 
Confidentiality_B_refined, 

1448 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1449 
qed "B_Knows_A_Knows_ServKey_refined"; 