author  paulson 
Tue, 27 Feb 2001 16:13:23 +0100  
changeset 11185  1b737b4c2108 
parent 11104  f2024fed9f0c 
child 11204  bb01189f0565 
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] 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

66 
"(\\<forall>A Tk akey Peer. \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

67 
\ ev \\<noteq> Says Kas A (Crypt (shrK A) {akey, Agent Peer, Tk, \ 
6452  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] 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

82 
"K \\<in> AuthKeys \ 
6452  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) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

85 
\ ==> K = K'  K \\<in> AuthKeys evs"; 
6452  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, \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

91 
\ (Crypt (shrK Tgs) {Agent A, Agent Tgs, Key K, Number Tk})}) \\<in> set evs \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

92 
\ ==> K \\<in> AuthKeys evs"; 
6452  93 
by Auto_tac; 
94 
qed "AuthKeysI"; 

95 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

96 
Goalw [AuthKeys_def] "K \\<in> AuthKeys evs ==> Key K \\<in> used evs"; 
6452  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}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

106 
\ \\<in> set evs ==> AuthTicket \\<in> parts (spies evs)"; 
6452  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}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

111 
\ \\<in> set evs ==> AuthKey \\<in> parts (spies evs)"; 
6452  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}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

116 
\ \\<in> set evs ;\ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

117 
\ evs \\<in> kerberos ] ==> AuthKey \\<notin> range shrK"; 
6452  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})\ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

125 
\ \\<in> set evs ==> ServTicket \\<in> parts (spies evs)"; 
6452  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})\ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

130 
\ \\<in> set evs ==> ServKey \\<in> parts (spies evs)"; 
6452  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}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

135 
\ \\<in> set evs ;\ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

136 
\ evs \\<in> kerberos ] ==> ServKey \\<notin> range shrK"; 
6452  137 
by (etac rev_mp 1); 
138 
by (etac kerberos.induct 1); 

139 
by Auto_tac; 

140 
qed "Oops_range_spies2"; 

141 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

142 
Goal "Says S A (Crypt K {SesKey, B, TimeStamp, Ticket}) \\<in> set evs \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

143 
\ ==> Ticket \\<in> parts (spies evs)"; 
6452  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)*) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

159 
Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"; 
6452  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 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

166 
Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)"; 
6452  167 
by (auto_tac (claset() addDs [impOfSubs analz_subset_parts], simpset())); 
168 
qed "Spy_analz_shrK"; 

169 
Addsimps [Spy_analz_shrK]; 

170 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

171 
Goal "[ Key (shrK A) \\<in> parts (spies evs); evs \\<in> kerberos ] ==> A:bad"; 
6452  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!*) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

178 
Goal "evs \\<in> kerberos ==> \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

179 
\ Key K \\<notin> used evs > K \\<notin> keysFor (parts (spies evs))"; 
6452  180 
by (parts_induct_tac 1); 
181 
(*Fake*) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

182 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
6452  183 
(*Others*) 
184 
by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs))); 

185 
qed_spec_mp "new_keys_not_used"; 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

186 
Addsimps [new_keys_not_used]; 
6452  187 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

188 
(*Earlier, \\<forall>protocol proofs declared this theorem. 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

189 
But Yahalom and Kerberos IV are the only ones that need it!*) 
6452  190 
bind_thm ("new_keys_not_analzd", 
191 
[analz_subset_parts RS keysFor_mono, 

192 
new_keys_not_used] MRS contra_subsetD); 

193 

194 

195 
(*********************** REGULARITY LEMMAS ***********************) 

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

197 
(*****************************************************************) 

198 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

201 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

202 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

203 
\ ==> AuthKey \\<notin> range shrK & AuthKey \\<in> AuthKeys evs & \ 
6452  204 
\ AuthTicket = (Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk} ) &\ 
205 
\ K = shrK A & Peer = Tgs"; 

206 
by (etac rev_mp 1); 

207 
by (etac kerberos.induct 1); 

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

209 
by (ALLGOALS Blast_tac); 

210 
qed "Says_Kas_message_form"; 

211 

212 
(*This lemma is essential for proving Says_Tgs_message_form: 

213 

214 
the session key AuthKey 

215 
supplied by Kas in the authentication ticket 

216 
cannot be a longterm key! 

217 

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

219 
*) 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

221 
\ \\<in> parts (spies evs); Tgs_B \\<notin> bad;\ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

222 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

223 
\ ==> SesKey \\<notin> range shrK"; 
6452  224 
by (etac rev_mp 1); 
225 
by (parts_induct_tac 1); 

226 
by (Fake_parts_insert_tac 1); 

227 
qed "SesKey_is_session_key"; 

228 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

230 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

231 
\ evs \\<in> kerberos ] \ 
6452  232 
\ ==> Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Tk, \ 
233 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

234 
\ \\<in> set evs"; 
6452  235 
by (etac rev_mp 1); 
236 
by (parts_induct_tac 1); 

237 
(*Fake*) 

238 
by (Fake_parts_insert_tac 1); 

239 
(*K4*) 

240 
by (Blast_tac 1); 

241 
qed "A_trusts_AuthTicket"; 

242 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

244 
\ \\<in> parts (spies evs);\ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

245 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

246 
\ ==> AuthKey \\<in> AuthKeys evs"; 
7499  247 
by (ftac A_trusts_AuthTicket 1); 
6452  248 
by (assume_tac 1); 
249 
by (simp_tac (simpset() addsimps [AuthKeys_def]) 1); 

250 
by (Blast_tac 1); 

251 
qed "AuthTicket_crypt_AuthKey"; 

252 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

255 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

256 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

257 
\ ==> B \\<noteq> Tgs & ServKey \\<notin> range shrK & ServKey \\<notin> AuthKeys evs &\ 
6452  258 
\ ServTicket = (Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt} ) & \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

259 
\ AuthKey \\<notin> range shrK & AuthKey \\<in> AuthKeys evs"; 
6452  260 
by (etac rev_mp 1); 
261 
by (etac kerberos.induct 1); 

262 
by (ALLGOALS 

263 
(asm_full_simp_tac 

264 
(simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert, 

265 
AuthKeys_empty, AuthKeys_simp]))); 

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

267 
by Auto_tac; 

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

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

270 
addEs spies_partsEs) 1); 

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

272 
addEs spies_partsEs) 1); 

273 
qed "Says_Tgs_message_form"; 

274 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

277 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

278 
\ A \\<notin> bad; evs \\<in> kerberos ] \ 
6452  279 
\ ==> Says Kas A (Crypt (shrK A) {Key AuthKey, Peer, Tk, AuthTicket}) \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

280 
\ \\<in> set evs"; 
6452  281 
by (etac rev_mp 1); 
282 
by (parts_induct_tac 1); 

283 
(*Fake*) 

284 
by (Fake_parts_insert_tac 1); 

285 
(*K4*) 

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

287 
A_trusts_AuthTicket RS Says_Kas_message_form]) 

288 
1); 

289 
qed "A_trusts_AuthKey"; 

290 

291 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

294 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

295 
\ Key AuthKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

296 
\ AuthKey \\<notin> range shrK; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

297 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

298 
\==> \\<exists>A. Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket})\ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

299 
\ \\<in> set evs"; 
6452  300 
by (etac rev_mp 1); 
301 
by (etac rev_mp 1); 

302 
by (parts_induct_tac 1); 

303 
(*Fake*) 

304 
by (Fake_parts_insert_tac 1); 

305 
(*K2*) 

306 
by (Blast_tac 1); 

307 
(*K4*) 

308 
by Auto_tac; 

309 
qed "A_trusts_K4"; 

310 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

312 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

313 
\ A \\<notin> bad; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

314 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

315 
\ ==> AuthKey \\<notin> range shrK & \ 
6452  316 
\ AuthTicket = Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}"; 
317 
by (etac rev_mp 1); 

318 
by (parts_induct_tac 1); 

319 
by (Fake_parts_insert_tac 1); 

320 
by (Blast_tac 1); 

321 
qed "AuthTicket_form"; 

322 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

325 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

326 
\ Key AuthKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

327 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

328 
\ ==> ServKey \\<notin> range shrK & \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

329 
\ (\\<exists>A. ServTicket = Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt})"; 
6452  330 
by (etac rev_mp 1); 
331 
by (etac rev_mp 1); 

332 
by (parts_induct_tac 1); 

333 
by (Fake_parts_insert_tac 1); 

334 
qed "ServTicket_form"; 

335 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

337 
\ {Key AuthKey, Agent Tgs, Tk, AuthTicket} ) \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

338 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

339 
\ ==> AuthKey \\<notin> range shrK & \ 
6452  340 
\ AuthTicket = \ 
341 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}\ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

342 
\  AuthTicket \\<in> analz (spies evs)"; 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

343 
by (case_tac "A \\<in> bad" 1); 
6452  344 
by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1); 
345 
by (forward_tac [Says_imp_spies RS parts.Inj] 1); 

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

347 
qed "Says_kas_message_form"; 

348 
(* Essentially the same as AuthTicket_form *) 

349 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

351 
\ {Key ServKey, Agent B, Tt, ServTicket} ) \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

352 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

353 
\ ==> ServKey \\<notin> range shrK & \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

354 
\ (\\<exists>A. ServTicket = \ 
6452  355 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}) \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

356 
\  ServTicket \\<in> analz (spies evs)"; 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

357 
by (case_tac "Key AuthKey \\<in> analz (spies evs)" 1); 
11104  358 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 1); 
6452  359 
by (forward_tac [Says_imp_spies RS parts.Inj] 1); 
360 
by (blast_tac (claset() addSDs [ServTicket_form]) 1); 

361 
qed "Says_tgs_message_form"; 

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

363 

364 

365 
(*****************UNICITY THEOREMS****************) 

366 

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

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

369 
also Tgs in the place of B. *) 

370 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

372 
\ \\<in> parts (spies evs); \ 
6452  373 
\ Crypt (shrK B') {Agent A', Agent B', Key SesKey, T'} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

374 
\ \\<in> parts (spies evs); Key SesKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

375 
\ evs \\<in> kerberos ] \ 
6452  376 
\ ==> A=A' & B=B' & T=T'"; 
11104  377 
by (etac rev_mp 1); 
378 
by (etac rev_mp 1); 

379 
by (etac rev_mp 1); 

380 
by (parts_induct_tac 1); 

381 
(*Fake, K2, K4*) 

382 
by (Fake_parts_insert_tac 1); 

383 
by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); 

6452  384 
qed "unique_CryptKey"; 
385 

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

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

388 
*) 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

390 
\ \\<in> parts (spies evs); \ 
6452  391 
\ Crypt K' {Key SesKey, Agent B', T', Ticket'} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

392 
\ \\<in> parts (spies evs); Key SesKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

393 
\ evs \\<in> kerberos ] \ 
6452  394 
\ ==> K=K' & B=B' & T=T' & Ticket=Ticket'"; 
11104  395 
by (etac rev_mp 1); 
396 
by (etac rev_mp 1); 

397 
by (etac rev_mp 1); 

398 
by (parts_induct_tac 1); 

399 
(*Fake, K2, K4*) 

400 
by (Fake_parts_insert_tac 1); 

401 
by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1)); 

6452  402 
qed "Key_unique_SesKey"; 
403 

404 

405 
(* 

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

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

408 
Similarly, at reception of any message mentioning an AuthKey 

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

410 
associates it with a new ServKey. 

411 

412 
Therefore, a goal like 

413 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

414 
"evs \\<in> kerberos \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

415 
\ ==> Key Kc \\<notin> analz (spies evs) > \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

416 
\ (\\<exists>K' B' T' Ticket'. \\<forall>K B T Ticket. \ 
6452  417 
\ Crypt Kc {Key K, Agent B, T, Ticket} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

418 
\ \\<in> parts (spies evs) > K=K' & B=B' & T=T' & Ticket=Ticket')"; 
6452  419 

420 
would fail on the K2 and K4 cases. 

421 
*) 

422 

423 
Goal "[ Says Kas A \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

424 
\ (Crypt Ka {Key AuthKey, Agent Tgs, Tk, X}) \\<in> set evs; \ 
6452  425 
\ Says Kas A' \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

426 
\ (Crypt Ka' {Key AuthKey, Agent Tgs, Tk', X'}) \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

427 
\ evs \\<in> kerberos ] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'"; 
11104  428 
by (etac rev_mp 1); 
429 
by (etac rev_mp 1); 

430 
by (parts_induct_tac 1); 

431 
(*K2*) 

432 
by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 

6452  433 
qed "unique_AuthKeys"; 
434 

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

436 
Goal "[ Says Tgs A \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

437 
\ (Crypt K {Key ServKey, Agent B, Tt, X}) \\<in> set evs; \ 
6452  438 
\ Says Tgs A' \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

439 
\ (Crypt K' {Key ServKey, Agent B', Tt', X'}) \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

440 
\ evs \\<in> kerberos ] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'"; 
11104  441 
by (etac rev_mp 1); 
442 
by (etac rev_mp 1); 

443 
by (parts_induct_tac 1); 

444 
(*K4*) 

445 
by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 

6452  446 
qed "unique_ServKeys"; 
447 

448 

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

450 

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

452 
by (Simp_tac 1); 

453 
qed "not_KeyCryptKey_Nil"; 

454 
AddIffs [not_KeyCryptKey_Nil]; 

455 

456 
Goalw [KeyCryptKey_def] 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

458 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

459 
\ evs \\<in> kerberos ] ==> KeyCryptKey AuthKey ServKey evs"; 
7499  460 
by (ftac Says_Tgs_message_form 1); 
6452  461 
by (assume_tac 1); 
462 
by (Blast_tac 1); 

463 
qed "KeyCryptKeyI"; 

464 

465 
Goalw [KeyCryptKey_def] 

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

467 
\ (Tgs = S & \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

468 
\ (\\<exists>B tt. X = Crypt AuthKey \ 
6452  469 
\ {Key ServKey, Agent B, tt, \ 
470 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, tt} }) \ 

471 
\  KeyCryptKey AuthKey ServKey evs)"; 

472 
by (Simp_tac 1); 

473 
by (Blast_tac 1); 

474 
qed "KeyCryptKey_Says"; 

475 
Addsimps [KeyCryptKey_Says]; 

476 

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

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

479 
Goalw [KeyCryptKey_def] 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

480 
"[ Key AuthKey \\<notin> used evs; evs \\<in> kerberos ] \ 
6452  481 
\ ==> ~ KeyCryptKey AuthKey ServKey evs"; 
482 
by (etac rev_mp 1); 

483 
by (parts_induct_tac 1); 

484 
by (Asm_full_simp_tac 1); 

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

486 
qed "Auth_fresh_not_KeyCryptKey"; 

487 

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

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

490 
Goalw [KeyCryptKey_def] 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

491 
"Key ServKey \\<notin> used evs ==> ~ KeyCryptKey AuthKey ServKey evs"; 
6452  492 
by (blast_tac (claset() addSEs spies_partsEs) 1); 
493 
qed "Serv_fresh_not_KeyCryptKey"; 

494 

495 
Goalw [KeyCryptKey_def] 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

497 
\ \\<in> parts (spies evs); evs \\<in> kerberos ] \ 
6452  498 
\ ==> ~ KeyCryptKey K AuthKey evs"; 
499 
by (etac rev_mp 1); 

500 
by (parts_induct_tac 1); 

501 
(*K4*) 

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

503 
(*K2: by freshness*) 

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

505 
by (Fake_parts_insert_tac 1); 

506 
qed "AuthKey_not_KeyCryptKey"; 

507 

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

509 
Goalw [KeyCryptKey_def] 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

511 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

512 
\ Key ServKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

513 
\ B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
6452  514 
\ ==> ~ KeyCryptKey ServKey K evs"; 
515 
by (etac rev_mp 1); 

516 
by (etac rev_mp 1); 

517 
by (parts_induct_tac 1); 

518 
by (Fake_parts_insert_tac 1); 

519 
(*K4 splits into distinct subcases*) 

520 
by (Step_tac 1); 

521 
by (ALLGOALS Asm_full_simp_tac); 

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

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

524 
addSEs [MPair_parts] 

525 
addDs [unique_CryptKey]) 4); 

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

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

528 
Crypt_imp_invKey_keysFor], 

529 
simpset()) 2); 

530 
(*Others by freshness*) 

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

532 
qed "ServKey_not_KeyCryptKey"; 

533 

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

535 
Goalw [KeyCryptKey_def] 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

536 
"evs \\<in> kerberos ==> ~ KeyCryptKey K (shrK A) evs"; 
6452  537 
by (parts_induct_tac 1); 
538 
qed "shrK_not_KeyCryptKey"; 

539 

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

541 
other key AuthKey.*) 

542 
Goalw [KeyCryptKey_def] 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

544 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

545 
\ AuthKey' \\<noteq> AuthKey; evs \\<in> kerberos ] \ 
6452  546 
\ ==> ~ KeyCryptKey AuthKey' ServKey evs"; 
547 
by (blast_tac (claset() addDs [unique_ServKeys]) 1); 

548 
qed "Says_Tgs_KeyCryptKey"; 

549 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

550 
Goal "[ KeyCryptKey AuthKey ServKey evs; evs \\<in> kerberos ] \ 
6452  551 
\ ==> ~ KeyCryptKey ServKey K evs"; 
552 
by (etac rev_mp 1); 

553 
by (parts_induct_tac 1); 

554 
by (Step_tac 1); 

555 
by (ALLGOALS Asm_full_simp_tac); 

556 
(*K4 splits into subcases*) 

557 
by (blast_tac (claset() addEs spies_partsEs 

558 
addSDs [AuthKey_not_KeyCryptKey]) 4); 

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

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

561 
Crypt_imp_invKey_keysFor], 

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

563 
(*Others by freshness*) 

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

565 
qed "KeyCryptKey_not_KeyCryptKey"; 

566 

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

568 
those sent by Tgs in step K4. *) 

569 

570 
(*We take some pains to express the property 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

572 
Goal "P > (Key K \\<in> analz (Key`KK Un H)) > (K:KK  Key K \\<in> analz H) \ 
6452  573 
\ ==> \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

574 
\ P > (Key K \\<in> analz (Key`KK Un H)) = (K:KK  Key K \\<in> analz H)"; 
6452  575 
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); 
576 
qed "Key_analz_image_Key_lemma"; 

577 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

578 
Goal "[ KeyCryptKey K K' evs; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

579 
\ ==> Key K' \\<in> analz (insert (Key K) (spies evs))"; 
6452  580 
by (full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1); 
581 
by (Clarify_tac 1); 

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

583 
by Auto_tac; 

584 
qed "KeyCryptKey_analz_insert"; 

585 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

586 
Goal "[ K \\<in> AuthKeys evs Un range shrK; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

587 
\ ==> \\<forall>SK. ~ KeyCryptKey SK K evs"; 
6452  588 
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1); 
589 
by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1); 

590 
qed "AuthKeys_are_not_KeyCryptKey"; 

591 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

592 
Goal "[ K \\<notin> AuthKeys evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

593 
\ K \\<notin> range shrK; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

594 
\ ==> \\<forall>SK. ~ KeyCryptKey K SK evs"; 
6452  595 
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 1); 
596 
by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1); 

597 
qed "not_AuthKeys_not_KeyCryptKey"; 

598 

599 

600 
(*****************SECRECY THEOREMS****************) 

601 

602 
(*For proofs involving analz.*) 

603 
val analz_sees_tac = 

604 
EVERY 

605 
[REPEAT (FIRSTGOAL analz_mono_contra_tac), 

7499  606 
ftac Oops_range_spies2 10, 
607 
ftac Oops_range_spies1 9, 

608 
ftac Says_tgs_message_form 7, 

609 
ftac Says_kas_message_form 5, 

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

612 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

613 
Goal "[ KK <= (range shrK); Key K \\<in> analz (spies evs); evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

614 
\ ==> Key K \\<in> analz (Key ` KK Un spies evs)"; 
6452  615 
by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1); 
616 
qed "analz_mono_KK"; 

617 

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

618 
(*For the Oops2 case of the next theorem*) 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

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

620 
\ 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

621 
\ {Key ServKey, Agent B, Number Tt, ServTicket}) \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

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

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

624 
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

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

626 

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

627 

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

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

631 
(* 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

632 
(* [simplified by LCP] *) 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

633 
Goal "evs \\<in> kerberos ==> \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

634 
\ (\\<forall>SK KK. KK <= (range shrK) > \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

635 
\ (\\<forall>K \\<in> KK. ~ KeyCryptKey K SK evs) > \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

636 
\ (Key SK \\<in> analz (Key`KK Un (spies evs))) = \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

637 
\ (SK \\<in> KK  Key SK \\<in> analz (spies evs)))"; 
6452  638 
by (etac kerberos.induct 1); 
639 
by analz_sees_tac; 

640 
by (REPEAT_FIRST (rtac allI)); 

641 
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

642 
(*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

643 
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

644 
by (case_tac "KeyCryptKey ServKey SK evs5" 8); 
6452  645 
by (ALLGOALS 
646 
(asm_simp_tac 

647 
(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

648 
[KeyCryptKey_Says, shrK_not_KeyCryptKey, Oops2_not_KeyCryptKey, 
6452  649 
Auth_fresh_not_KeyCryptKey, Serv_fresh_not_KeyCryptKey, 
650 
Says_Tgs_KeyCryptKey, Spy_analz_shrK]))); 

651 
(*Fake*) 

652 
by (spy_analz_tac 1); 

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

654 
(*K3*) 

655 
by (Blast_tac 1); 

656 
(*K4*) 

657 
by (blast_tac (claset() addEs spies_partsEs 

658 
addSDs [AuthKey_not_KeyCryptKey]) 1); 

659 
(*K5*) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

660 
by (case_tac "Key ServKey \\<in> analz (spies evs5)" 1); 
6452  661 
(*If ServKey is compromised then the result follows directly...*) 
662 
by (asm_simp_tac 

663 
(simpset() addsimps [analz_insert_eq, 

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

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

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

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

668 
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

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

670 
by (Asm_full_simp_tac 1); 
6452  671 
by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1); 
672 
qed_spec_mp "Key_analz_image_Key"; 

673 

674 

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

676 
(* authentication keys or shared keys. *) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

677 
Goal "[ evs \\<in> kerberos; K \\<in> (AuthKeys evs) Un range shrK; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

678 
\ SesKey \\<notin> range shrK ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

679 
\ ==> Key K \\<in> analz (insert (Key SesKey) (spies evs)) = \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

680 
\ (K = SesKey  Key K \\<in> analz (spies evs))"; 
7499  681 
by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1); 
6452  682 
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); 
683 
qed "analz_insert_freshK1"; 

684 

685 

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

687 
(* any other keys. *) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

688 
Goal "[ evs \\<in> kerberos; ServKey \\<notin> (AuthKeys evs); ServKey \\<notin> range shrK]\ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

689 
\ ==> Key K \\<in> analz (insert (Key ServKey) (spies evs)) = \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

690 
\ (K = ServKey  Key K \\<in> analz (spies evs))"; 
7499  691 
by (ftac not_AuthKeys_not_KeyCryptKey 1 
6452  692 
THEN assume_tac 1 
693 
THEN assume_tac 1); 

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

695 
qed "analz_insert_freshK2"; 

696 

697 

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

699 
(* encrypts a certain service key. *) 

700 
Goal 

701 
"[ Says Tgs A \ 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

703 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

704 
\ AuthKey \\<noteq> AuthKey'; AuthKey' \\<notin> range shrK; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

705 
\ ==> Key ServKey \\<in> analz (insert (Key AuthKey') (spies evs)) = \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

706 
\ (ServKey = AuthKey'  Key ServKey \\<in> analz (spies evs))"; 
6452  707 
by (dres_inst_tac [("AuthKey'","AuthKey'")] Says_Tgs_KeyCryptKey 1); 
708 
by (Blast_tac 1); 

709 
by (assume_tac 1); 

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

711 
qed "analz_insert_freshK3"; 

712 

713 

714 
(*a weakness of the protocol*) 

715 
Goal "[ Says Tgs A \ 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

717 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

718 
\ Key AuthKey \\<in> analz (spies evs); evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

719 
\ ==> Key ServKey \\<in> analz (spies evs)"; 
6452  720 
by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
721 
analz.Decrypt RS analz.Fst], 

722 
simpset()) 1); 

723 
qed "AuthKey_compromises_ServKey"; 

724 

725 

726 
(********************** Guarantees for Kas *****************************) 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

729 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

730 
\ Key ServKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

731 
\ B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

732 
\ ==> ServKey \\<notin> AuthKeys evs"; 
6452  733 
by (etac rev_mp 1); 
734 
by (etac rev_mp 1); 

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

736 
by (parts_induct_tac 1); 

737 
by (Fake_parts_insert_tac 1); 

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

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

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

741 

742 

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

744 
the Key has expired **) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

745 
Goal "[ A \\<notin> bad; evs \\<in> kerberos ] \ 
6452  746 
\ ==> Says Kas A \ 
747 
\ (Crypt (shrK A) \ 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

750 
\ \\<in> set evs > \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

751 
\ Key AuthKey \\<in> analz (spies evs) > \ 
6452  752 
\ ExpirAuth Tk evs"; 
753 
by (etac kerberos.induct 1); 

754 
by analz_sees_tac; 

755 
by (ALLGOALS 

756 
(asm_simp_tac 

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

757 
(simpset() addsimps ([Says_Kas_message_form, less_SucI, 
6452  758 
analz_insert_eq, not_parts_not_analz, 
759 
analz_insert_freshK1] @ pushes)))); 

760 
(*Fake*) 

761 
by (spy_analz_tac 1); 

762 
(*K2*) 

763 
by (blast_tac (claset() addSEs spies_partsEs 

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

765 
(*K4*) 

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

767 
(*Level 8: K5*) 

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

769 
addDs [Says_Kas_message_form, 

770 
Says_imp_spies RS parts.Inj] 

771 
addIs [less_SucI]) 1); 

772 
(*Oops1*) 

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

774 
(*Oops2*) 

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

776 
Says_Kas_message_form]) 1); 

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

778 

779 

780 
Goal "[ Says Kas A \ 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

782 
\ \\<in> set evs; \ 
6452  783 
\ ~ ExpirAuth Tk evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

784 
\ A \\<notin> bad; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

785 
\ ==> Key AuthKey \\<notin> analz (spies evs)"; 
7499  786 
by (ftac Says_Kas_message_form 1 THEN assume_tac 1); 
6452  787 
by (blast_tac (claset() addSDs [lemma]) 1); 
788 
qed "Confidentiality_Kas"; 

789 

790 

791 
(********************** Guarantees for Tgs *****************************) 

792 

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

794 
the Key has expired **) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

795 
Goal "[ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

796 
\ ==> Key AuthKey \\<notin> analz (spies evs) > \ 
6452  797 
\ Says Tgs A \ 
798 
\ (Crypt AuthKey \ 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

801 
\ \\<in> set evs > \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

802 
\ Key ServKey \\<in> analz (spies evs) > \ 
6452  803 
\ ExpirServ Tt evs"; 
804 
by (etac kerberos.induct 1); 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

805 
(*The Oops1 case is unusual: must simplify Authkey \\<notin> analz (spies (ev#evs)) 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

806 
rather than weakening it to Authkey \\<notin> analz (spies evs), for we then 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

807 
conclude AuthKey \\<noteq> AuthKeya.*) 
6452  808 
by (Clarify_tac 9); 
809 
by analz_sees_tac; 

810 
by (rotate_tac ~1 11); 

811 
by (ALLGOALS 

812 
(asm_full_simp_tac 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

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

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

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

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

817 
@ pushes))); 
6452  818 
(*Fake*) 
819 
by (spy_analz_tac 1); 

820 
(*K2*) 

821 
by (blast_tac (claset() addSEs spies_partsEs 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

822 
addIs [parts_insertI, less_SucI]) 1); 
6452  823 
(*K4*) 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

824 
by (case_tac "A \\<noteq> Aa" 1); 
6452  825 
by (blast_tac (claset() addSEs spies_partsEs 
826 
addIs [less_SucI]) 1); 

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

828 
A_trusts_AuthTicket, 

829 
Confidentiality_Kas, 

830 
impOfSubs analz_subset_parts]) 1); 

831 
by (ALLGOALS Clarify_tac); 

832 
(*Oops2*) 

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

834 
Key_unique_SesKey] addIs [less_SucI]) 3); 

835 
(** Level 12 **) 

836 
(*Oops1*) 

7499  837 
by (ftac Says_Kas_message_form 2); 
6452  838 
by (assume_tac 2); 
839 
by (blast_tac (claset() addDs [analz_insert_freshK3, 

840 
Says_Kas_message_form, Says_Tgs_message_form] 

841 
addIs [less_SucI]) 2); 

842 
(** Level 16 **) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

843 
by (thin_tac "Says Aa Tgs ?X \\<in> set ?evs" 1); 
6452  844 
by (forward_tac [Says_imp_spies RS parts.Inj RS ServKey_notin_AuthKeysD] 1); 
845 
by (assume_tac 1 THEN Blast_tac 1 THEN assume_tac 1); 

846 
by (rotate_tac ~1 1); 

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

848 
by (etac disjE 1); 

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

850 
Key_unique_SesKey]) 1); 

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

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

853 

854 

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

856 
Goal 

857 
"[ Says Tgs A \ 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

859 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

860 
\ Key AuthKey \\<notin> analz (spies evs); \ 
6452  861 
\ ~ ExpirServ Tt evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

862 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

863 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
7499  864 
by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); 
6452  865 
by (blast_tac (claset() addDs [lemma]) 1); 
866 
qed "Confidentiality_Tgs1"; 

867 

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

869 
Goal 

870 
"[ Says Kas A \ 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

872 
\ \\<in> set evs; \ 
6452  873 
\ Says Tgs A \ 
874 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

875 
\ \\<in> set evs; \ 
6452  876 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

877 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

878 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
6452  879 
by (blast_tac (claset() addSDs [Confidentiality_Kas, 
880 
Confidentiality_Tgs1]) 1); 

881 
qed "Confidentiality_Tgs2"; 

882 

883 
(*Most general form*) 

884 
val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2; 

885 

886 

887 
(********************** Guarantees for Alice *****************************) 

888 

889 
val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas; 

890 

891 
Goal 

892 
"[ Says Kas A \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

893 
\ (Crypt (shrK A) {Key AuthKey, Agent Tgs, Tk, AuthTicket}) \\<in> set evs;\ 
6452  894 
\ Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

895 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

896 
\ Key AuthKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

897 
\ evs \\<in> kerberos ] \ 
6452  898 
\==> Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, ServTicket})\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

899 
\ \\<in> set evs"; 
7499  900 
by (ftac Says_Kas_message_form 1 THEN assume_tac 1); 
6452  901 
by (etac rev_mp 1); 
902 
by (etac rev_mp 1); 

903 
by (etac rev_mp 1); 

904 
by (parts_induct_tac 1); 

905 
by (Fake_parts_insert_tac 1); 

906 
(*K2 and K4 remain*) 

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

908 
addSDs [unique_CryptKey]) 2); 

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

910 
AuthKeys_used]) 1); 

911 
qed "A_trusts_K4_bis"; 

912 

913 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

915 
\ \\<in> parts (spies evs); \ 
6452  916 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

917 
\ \\<in> parts (spies evs); \ 
6452  918 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

919 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

920 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
6452  921 
by (dtac A_trusts_AuthKey 1); 
922 
by (assume_tac 1); 

923 
by (assume_tac 1); 

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

925 
Says_Kas_message_form, 

926 
A_trusts_K4_bis, Confidentiality_Tgs2]) 1); 

927 
qed "Confidentiality_Serv_A"; 

928 

929 

930 
(********************** Guarantees for Bob *****************************) 

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

932 

933 
Goal 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

935 
\ \\<in> set evs; evs \\<in> kerberos] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

936 
\ ==> \\<exists>Tk. Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 
6452  937 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

938 
\ \\<in> set evs"; 
6452  939 
by (etac rev_mp 1); 
940 
by (parts_induct_tac 1); 

941 
by Auto_tac; 

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

943 
A_trusts_AuthTicket]) 1); 

944 
qed "K4_imp_K2"; 

945 

946 
Goal 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

948 
\ \\<in> set evs; evs \\<in> kerberos] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

949 
\ ==> \\<exists>Tk. (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 
6452  950 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

951 
\ \\<in> set evs \ 
6452  952 
\ & ServLife + Tt <= AuthLife + Tk)"; 
953 
by (etac rev_mp 1); 

954 
by (parts_induct_tac 1); 

955 
by Auto_tac; 

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

957 
A_trusts_AuthTicket]) 1); 

958 
qed "K4_imp_K2_refined"; 

959 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

961 
\ \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

962 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

963 
\==> \\<exists>AuthKey. \ 
6452  964 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, \ 
965 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

966 
\ \\<in> set evs"; 
6452  967 
by (etac rev_mp 1); 
968 
by (parts_induct_tac 1); 

969 
by (Fake_parts_insert_tac 1); 

970 
by (Blast_tac 1); 

971 
qed "B_trusts_ServKey"; 

972 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

974 
\ \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

975 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

976 
\ ==> \\<exists>AuthKey Tk. Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 
6452  977 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

978 
\ \\<in> set evs"; 
6452  979 
by (blast_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1); 
980 
qed "B_trusts_ServTicket_Kas"; 

981 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

983 
\ \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

984 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

985 
\ ==> \\<exists>AuthKey Tk. (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 
6452  986 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

987 
\ \\<in> set evs \ 
6452  988 
\ & ServLife + Tt <= AuthLife + Tk)"; 
989 
by (blast_tac (claset() addSDs [B_trusts_ServKey,K4_imp_K2_refined]) 1); 

990 
qed "B_trusts_ServTicket_Kas_refined"; 

991 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

993 
\ \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

994 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

995 
\==> \\<exists>Tk AuthKey. \ 
6452  996 
\ Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, \ 
997 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

998 
\ \\<in> set evs \ 
6452  999 
\ & Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 
1000 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1001 
\ \\<in> set evs"; 
7499  1002 
by (ftac B_trusts_ServKey 1); 
6452  1003 
by (etac exE 4); 
7499  1004 
by (ftac K4_imp_K2 4); 
6452  1005 
by (Blast_tac 5); 
1006 
by (ALLGOALS assume_tac); 

1007 
qed "B_trusts_ServTicket"; 

1008 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1010 
\ \\<in> parts (spies evs); B \\<noteq> Tgs; B \\<notin> bad; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1011 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1012 
\==> \\<exists>Tk AuthKey. \ 
6452  1013 
\ (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, \ 
1014 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1015 
\ \\<in> set evs \ 
6452  1016 
\ & Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 
1017 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1018 
\ \\<in> set evs \ 
6452  1019 
\ & ServLife + Tt <= AuthLife + Tk)"; 
7499  1020 
by (ftac B_trusts_ServKey 1); 
6452  1021 
by (etac exE 4); 
7499  1022 
by (ftac K4_imp_K2_refined 4); 
6452  1023 
by (Blast_tac 5); 
1024 
by (ALLGOALS assume_tac); 

1025 
qed "B_trusts_ServTicket_refined"; 

1026 

1027 

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

1029 
\ ==> ~ ExpirAuth Tk evs"; 

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

1031 
qed "NotExpirServ_NotExpirAuth_refined"; 

1032 

1033 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1035 
\ \\<in> parts (spies evs); \ 
6452  1036 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1037 
\ \\<in> parts (spies evs); \ 
6452  1038 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1039 
\ \\<in> parts (spies evs); \ 
6452  1040 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1041 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1042 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
7499  1043 
by (ftac A_trusts_AuthKey 1); 
1044 
by (ftac Confidentiality_Kas 3); 

1045 
by (ftac B_trusts_ServTicket 6); 

6452  1046 
by (etac exE 9); 
1047 
by (etac exE 9); 

7499  1048 
by (ftac Says_Kas_message_form 9); 
6452  1049 
by (blast_tac (claset() addDs [A_trusts_K4, 
1050 
unique_ServKeys, unique_AuthKeys, 

1051 
Confidentiality_Tgs2]) 10); 

1052 
by (ALLGOALS assume_tac); 

1053 
(* 

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

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

1056 
Says_Kas_message_form, B_trusts_ServTicket, 

1057 
unique_ServKeys, unique_AuthKeys, 

1058 
Confidentiality_Kas, 

1059 
Confidentiality_Tgs2]) 1); 

1060 
*) 

1061 
qed "Confidentiality_B"; 

1062 

1063 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1066 
\ \\<in> parts (spies evs); \ 
6452  1067 
\ ~ ExpirServ Tt evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1068 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1069 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
6452  1070 
by (blast_tac (claset() addDs [B_trusts_ServTicket_refined, 
1071 
NotExpirServ_NotExpirAuth_refined, 

1072 
Confidentiality_Tgs2]) 1); 

1073 
qed "Confidentiality_B_refined"; 

1074 

1075 

1076 
(********************** Authenticity theorems *****************************) 

1077 

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

1079 

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

1081 

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1084 
\ \\<in> parts (spies evs); \ 
6452  1085 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1086 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1087 
\ ~ ExpirAuth Tk evs; A \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1088 
\==>Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket})\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1089 
\ \\<in> set evs"; 
7499  1090 
by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1); 
6452  1091 
by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1); 
1092 
qed "A_trusts_ServKey"; 

1093 
(*Note: requires a temporal check*) 

1094 

1095 

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

1097 

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

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

1100 

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

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

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

1104 

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

1106 
"A_authenticity_refined" *) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1107 
Goal "[ Crypt ServKey {Agent A, Number Ta} \\<in> parts (spies evs); \ 
6452  1108 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1109 
\ ServTicket}) \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1110 
\ Key ServKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1111 
\ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1112 
\==> Says A B {ServTicket, Crypt ServKey {Agent A, Number Ta}} \\<in> set evs"; 
6452  1113 
by (etac rev_mp 1); 
1114 
by (etac rev_mp 1); 

1115 
by (etac rev_mp 1); 

1116 
by (etac kerberos.induct 1); 

7499  1117 
by (ftac Says_ticket_in_parts_spies 5); 
1118 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1119 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1120 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

1121 
by (Fake_parts_insert_tac 1); 

1122 
(*K3*) 

1123 
by (blast_tac (claset() addEs spies_partsEs 

1124 
addDs [A_trusts_AuthKey, 

1125 
Says_Kas_message_form, 

1126 
Says_Tgs_message_form]) 1); 

1127 
(*K4*) 

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

1129 
(*K5*) 

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

1131 
qed "Says_Auth"; 

1132 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1134 
Goal "[ Crypt ServKey {Agent A, Number Ta} \\<in> parts (spies evs); \ 
6452  1135 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1136 
\ \\<in> parts (spies evs); \ 
6452  1137 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1138 
\ \\<in> parts (spies evs); \ 
6452  1139 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1140 
\ \\<in> parts (spies evs); \ 
6452  1141 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1142 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1143 
\ ==> Says A B {Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt},\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1144 
\ Crypt ServKey {Agent A, Number Ta} } \\<in> set evs"; 
7499  1145 
by (ftac Confidentiality_B 1); 
1146 
by (ftac B_trusts_ServKey 9); 

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

1149 
addSIs [Says_Auth]) 12); 

1150 
by (ALLGOALS assume_tac); 

1151 
qed "A_Authenticity"; 

1152 

1153 
(*Stronger form in the refined model*) 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1154 
Goal "[ Crypt ServKey {Agent A, Number Ta2} \\<in> parts (spies evs); \ 
6452  1155 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1156 
\ \\<in> parts (spies evs); \ 
6452  1157 
\ ~ ExpirServ Tt evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1158 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1159 
\ ==> Says A B {Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt},\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1160 
\ Crypt ServKey {Agent A, Number Ta2} } \\<in> set evs"; 
7499  1161 
by (ftac Confidentiality_B_refined 1); 
1162 
by (ftac B_trusts_ServKey 6); 

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

1165 
addSIs [Says_Auth]) 9); 

1166 
by (ALLGOALS assume_tac); 

1167 
qed "A_Authenticity_refined"; 

1168 

1169 

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

1171 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1172 
Goal "[ Crypt ServKey (Number Ta) \\<in> parts (spies evs); \ 
6452  1173 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1174 
\ ServTicket}) \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1175 
\ Key ServKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1176 
\ A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1177 
\ ==> Says B A (Crypt ServKey (Number Ta)) \\<in> set evs"; 
6452  1178 
by (etac rev_mp 1); 
1179 
by (etac rev_mp 1); 

1180 
by (etac rev_mp 1); 

1181 
by (etac kerberos.induct 1); 

7499  1182 
by (ftac Says_ticket_in_parts_spies 5); 
1183 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1184 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1185 
by (ALLGOALS Asm_simp_tac); 

1186 
by (Fake_parts_insert_tac 1); 

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

1188 
by (Clarify_tac 1); 

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

1192 
qed "Says_K6"; 

1193 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1195 
\ \\<in> parts (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1196 
\ Key AuthKey \\<notin> analz (spies evs); AuthKey \\<notin> range shrK; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1197 
\ evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1198 
\ ==> \\<exists>A. Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, T, ServTicket})\ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1199 
\ \\<in> set evs"; 
6452  1200 
by (etac rev_mp 1); 
1201 
by (etac rev_mp 1); 

1202 
by (parts_induct_tac 1); 

1203 
by (Fake_parts_insert_tac 1); 

1204 
by (Blast_tac 1); 

1205 
by (Blast_tac 1); 

1206 
qed "K4_trustworthy"; 

1207 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1208 
Goal "[ Crypt ServKey (Number Ta) \\<in> parts (spies evs); \ 
6452  1209 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1210 
\ \\<in> parts (spies evs); \ 
6452  1211 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1212 
\ \\<in> parts (spies evs); \ 
6452  1213 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1214 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1215 
\ ==> Says B A (Crypt ServKey (Number Ta)) \\<in> set evs"; 
7499  1216 
by (ftac A_trusts_AuthKey 1); 
1217 
by (ftac Says_Kas_message_form 3); 

1218 
by (ftac Confidentiality_Kas 4); 

1219 
by (ftac K4_trustworthy 7); 

6452  1220 
by (Blast_tac 8); 
1221 
by (etac exE 9); 

7499  1222 
by (ftac K4_imp_K2 9); 
6452  1223 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 
1224 
addSIs [Says_K6] 

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

1226 
by (ALLGOALS assume_tac); 

1227 
qed "B_Authenticity"; 

1228 

1229 

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

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

1232 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1233 
Goal "[ Says B A (Crypt ServKey (Number Ta)) \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1234 
\ Key ServKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1235 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
6452  1236 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"; 
1237 
by (simp_tac (simpset() addsimps [Issues_def]) 1); 

1238 
by (rtac exI 1); 

1239 
by (rtac conjI 1); 

1240 
by (assume_tac 1); 

1241 
by (Simp_tac 1); 

1242 
by (etac rev_mp 1); 

1243 
by (etac rev_mp 1); 

1244 
by (etac kerberos.induct 1); 

7499  1245 
by (ftac Says_ticket_in_parts_spies 5); 
1246 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1247 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1248 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

1249 
by (Fake_parts_insert_tac 1); 

1250 
(*K6 requires numerous lemmas*) 

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

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

1253 
impOfSubs parts_spies_takeWhile_mono, 

1254 
impOfSubs parts_spies_evs_revD2] 

1255 
addIs [Says_K6] 

1256 
addEs spies_partsEs) 1); 

1257 
qed "B_Knows_B_Knows_ServKey_lemma"; 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1258 
(*Key ServKey \\<notin> analz (spies evs) could be relaxed by Confidentiality_B 
6452  1259 
but this is irrelevant because B knows what he knows! *) 
1260 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1261 
Goal "[ Says B A (Crypt ServKey (Number Ta)) \\<in> set evs; \ 
6452  1262 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1263 
\ \\<in> parts (spies evs);\ 
6452  1264 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1265 
\ \\<in> parts (spies evs);\ 
6452  1266 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1267 
\ \\<in> parts (spies evs); \ 
6452  1268 
\ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1269 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
6452  1270 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"; 
1271 
by (blast_tac (claset() addSDs [Confidentiality_B, 

1272 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1273 
qed "B_Knows_B_Knows_ServKey"; 

1274 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1275 
Goal "[ Says B A (Crypt ServKey (Number Ta)) \\<in> set evs; \ 
6452  1276 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt}\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1277 
\ \\<in> parts (spies evs);\ 
6452  1278 
\ ~ ExpirServ Tt evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1279 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
6452  1280 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"; 
1281 
by (blast_tac (claset() addSDs [Confidentiality_B_refined, 

1282 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1283 
qed "B_Knows_B_Knows_ServKey_refined"; 

1284 

1285 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1286 
Goal "[ Crypt ServKey (Number Ta) \\<in> parts (spies evs); \ 
6452  1287 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket} \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1288 
\ \\<in> parts (spies evs); \ 
6452  1289 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1290 
\ \\<in> parts (spies evs); \ 
6452  1291 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1292 
\ A \\<notin> bad; B \\<notin> bad; B \\<noteq> Tgs; evs \\<in> kerberos ] \ 
6452  1293 
\ ==> B Issues A with (Crypt ServKey (Number Ta)) on evs"; 
1294 
by (blast_tac (claset() addSDs [B_Authenticity, Confidentiality_Serv_A, 

1295 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1296 
qed "A_Knows_B_Knows_ServKey"; 

1297 

1298 
Goal "[ Says A Tgs \ 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1300 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1301 
\ A \\<notin> bad; evs \\<in> kerberos ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1302 
\ ==> \\<exists>Tk. Says Kas A (Crypt (shrK A) \ 
6452  1303 
\ {Key AuthKey, Agent Tgs, Tk, AuthTicket}) \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1304 
\ \\<in> set evs"; 
6452  1305 
by (etac rev_mp 1); 
1306 
by (parts_induct_tac 1); 

1307 
by (Fake_parts_insert_tac 1); 

1308 
by (Blast_tac 1); 

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

1310 
A_trusts_AuthKey]) 1); 

1311 
qed "K3_imp_K2"; 

1312 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1314 
\ \\<in> parts (spies evs); \ 
6452  1315 
\ Says Kas A (Crypt (shrK A) \ 
1316 
\ {Key AuthKey, Agent Tgs, Tk, AuthTicket}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1317 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1318 
\ Key AuthKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1319 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1320 
\ ==> Says Tgs A (Crypt AuthKey \ 
1321 
\ {Key ServKey, Agent B, Number Tt, ServTicket}) \ 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1322 
\ \\<in> set evs"; 
6452  1323 
by (etac rev_mp 1); 
1324 
by (etac rev_mp 1); 

1325 
by (etac rev_mp 1); 

1326 
by (parts_induct_tac 1); 

1327 
by (Fake_parts_insert_tac 1); 

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

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

1330 
A_trusts_AuthTicket, unique_AuthKeys]) 1); 

1331 
qed "K4_trustworthy'"; 

1332 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1334 
\ \\<in> set evs; \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1335 
\ Key ServKey \\<notin> analz (spies evs); \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1336 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1337 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs"; 
1338 
by (simp_tac (simpset() addsimps [Issues_def]) 1); 

1339 
by (rtac exI 1); 

1340 
by (rtac conjI 1); 

1341 
by (assume_tac 1); 

1342 
by (Simp_tac 1); 

1343 
by (etac rev_mp 1); 

1344 
by (etac rev_mp 1); 

1345 
by (etac kerberos.induct 1); 

7499  1346 
by (ftac Says_ticket_in_parts_spies 5); 
1347 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1348 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1349 
by (ALLGOALS Asm_simp_tac); 

1350 
by (Clarify_tac 1); 

1351 
(*K6*) 

1352 
by Auto_tac; 

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

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

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1356 
by (case_tac "Key AuthKey \\<in> analz (spies evs5)" 1); 
6452  1357 
by (force_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
1358 
analz.Decrypt RS analz.Fst], 

1359 
simpset()) 1); 

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

1361 
impOfSubs parts_spies_takeWhile_mono, 

1362 
impOfSubs parts_spies_evs_revD2] 

1363 
addIs [Says_Auth] 

1364 
addEs spies_partsEs) 1); 

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

1366 
qed "A_Knows_A_Knows_ServKey_lemma"; 

1367 

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

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1369 
\ \\<in> set evs; \ 
6452  1370 
\ Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1371 
\ \\<in> parts (spies evs);\ 
6452  1372 
\ Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1373 
\ \\<in> parts (spies evs); \ 
6452  1374 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs;\ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1375 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1376 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs"; 
1377 
by (blast_tac (claset() addSDs [Confidentiality_Serv_A, 

1378 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1379 
qed "A_Knows_A_Knows_ServKey"; 

1380 

11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

1381 
Goal "[ Crypt ServKey {Agent A, Number Ta} \\<in> parts (spies evs); \ 
6452  1382 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Number Tt} \ 
11185 