author  paulson 
Wed, 14 Mar 2001 08:50:55 +0100  
changeset 11204  bb01189f0565 
parent 11185  1b737b4c2108 
child 11222  72c5997e1145 
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 

11204  188 
(*Earlier, all protocol proofs declared this theorem. 
189 
But few of them actually need it! (Another is Yahalom) *) 

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 

11204  495 
Goal 
6452  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*) 

11204  504 
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2); 
6452  505 
by (blast_tac (claset() addEs spies_partsEs) 2); 
506 
by (Fake_parts_insert_tac 1); 

507 
qed "AuthKey_not_KeyCryptKey"; 

508 

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

11204  510 
Goal 
511 
"[ Crypt (shrK B) {Agent A, Agent B, Key SK, tt} \\<in> parts (spies evs); \ 

512 
\ Key SK \\<notin> analz (spies evs); \ 

513 
\ B \\<noteq> Tgs; evs \\<in> kerberos ] \ 

514 
\ ==> ~ KeyCryptKey SK K evs"; 

6452  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*) 

11204  520 
by Auto_tac; 
6452  521 
(*ServKey can't have been enclosed in two certificates*) 
522 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] 

523 
addSEs [MPair_parts] 

524 
addDs [unique_CryptKey]) 4); 

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

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

527 
Crypt_imp_invKey_keysFor], 

11204  528 
simpset() addsimps [KeyCryptKey_def]) 2); 
6452  529 
(*Others by freshness*) 
530 
by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); 

531 
qed "ServKey_not_KeyCryptKey"; 

532 

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

534 
Goalw [KeyCryptKey_def] 

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

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

538 

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

540 
other key AuthKey.*) 

541 
Goalw [KeyCryptKey_def] 

542 
"[ 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

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

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

547 
qed "Says_Tgs_KeyCryptKey"; 

548 

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

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

552 
by (parts_induct_tac 1); 

553 
by (Step_tac 1); 

554 
by (ALLGOALS Asm_full_simp_tac); 

555 
(*K4 splits into subcases*) 

556 
by (blast_tac (claset() addEs spies_partsEs 

557 
addSDs [AuthKey_not_KeyCryptKey]) 4); 

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

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

560 
Crypt_imp_invKey_keysFor], 

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

562 
(*Others by freshness*) 

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

564 
qed "KeyCryptKey_not_KeyCryptKey"; 

565 

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

567 
those sent by Tgs in step K4. *) 

568 

569 
(*We take some pains to express the property 

570 
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

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

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

576 

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

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

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

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

582 
by Auto_tac; 

583 
qed "KeyCryptKey_analz_insert"; 

584 

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

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

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

589 
qed "AuthKeys_are_not_KeyCryptKey"; 

590 

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

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

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

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

596 
qed "not_AuthKeys_not_KeyCryptKey"; 

597 

598 

599 
(*****************SECRECY THEOREMS****************) 

600 

601 
(*For proofs involving analz.*) 

602 
val analz_sees_tac = 

603 
EVERY 

604 
[REPEAT (FIRSTGOAL analz_mono_contra_tac), 

7499  605 
ftac Oops_range_spies2 10, 
606 
ftac Oops_range_spies1 9, 

607 
ftac Says_tgs_message_form 7, 

608 
ftac Says_kas_message_form 5, 

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

611 

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

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

613 
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

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

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

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

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

618 
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

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

620 

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

621 

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

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

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

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

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

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

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

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

631 
\ (SK \\<in> KK  Key SK \\<in> analz (spies evs)))"; 
6452  632 
by (etac kerberos.induct 1); 
633 
by analz_sees_tac; 

634 
by (REPEAT_FIRST (rtac allI)); 

635 
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

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

637 
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

638 
by (case_tac "KeyCryptKey ServKey SK evs5" 8); 
6452  639 
by (ALLGOALS 
640 
(asm_simp_tac 

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

642 
[KeyCryptKey_Says, shrK_not_KeyCryptKey, Oops2_not_KeyCryptKey, 
6452  643 
Auth_fresh_not_KeyCryptKey, Serv_fresh_not_KeyCryptKey, 
644 
Says_Tgs_KeyCryptKey, Spy_analz_shrK]))); 

645 
(*Fake*) 

646 
by (spy_analz_tac 1); 

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

648 
(*K3*) 

649 
by (Blast_tac 1); 

650 
(*K4*) 

651 
by (blast_tac (claset() addEs spies_partsEs 

652 
addSDs [AuthKey_not_KeyCryptKey]) 1); 

653 
(*K5*) 

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

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

657 
(simpset() addsimps [analz_insert_eq, 

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

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

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

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

662 
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

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

664 
by (Asm_full_simp_tac 1); 
6452  665 
by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1); 
666 
qed_spec_mp "Key_analz_image_Key"; 

667 

668 

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

670 
(* authentication keys or shared keys. *) 

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

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

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

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

674 
\ (K = SesKey  Key K \\<in> analz (spies evs))"; 
7499  675 
by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1); 
6452  676 
by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); 
677 
qed "analz_insert_freshK1"; 

678 

679 

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

681 
(* any other keys. *) 

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

682 
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

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

684 
\ (K = ServKey  Key K \\<in> analz (spies evs))"; 
7499  685 
by (ftac not_AuthKeys_not_KeyCryptKey 1 
6452  686 
THEN assume_tac 1 
687 
THEN assume_tac 1); 

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

689 
qed "analz_insert_freshK2"; 

690 

691 

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

693 
(* encrypts a certain service key. *) 

694 
Goal 

695 
"[ Says Tgs A \ 

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

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

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

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

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

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

703 
by (assume_tac 1); 

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

705 
qed "analz_insert_freshK3"; 

706 

707 

708 
(*a weakness of the protocol*) 

709 
Goal "[ Says Tgs A \ 

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

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

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

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

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

716 
simpset()) 1); 

717 
qed "AuthKey_compromises_ServKey"; 

718 

719 

720 
(********************** Guarantees for Kas *****************************) 

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

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

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

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

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

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

726 
\ ==> ServKey \\<notin> AuthKeys evs"; 
6452  727 
by (etac rev_mp 1); 
728 
by (etac rev_mp 1); 

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

730 
by (parts_induct_tac 1); 

731 
by (Fake_parts_insert_tac 1); 

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

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

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

735 

736 

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

738 
the Key has expired **) 

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

739 
Goal "[ A \\<notin> bad; evs \\<in> kerberos ] \ 
6452  740 
\ ==> Says Kas A \ 
741 
\ (Crypt (shrK A) \ 

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

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

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

745 
\ Key AuthKey \\<in> analz (spies evs) > \ 
6452  746 
\ ExpirAuth Tk evs"; 
747 
by (etac kerberos.induct 1); 

748 
by analz_sees_tac; 

749 
by (ALLGOALS 

750 
(asm_simp_tac 

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

751 
(simpset() addsimps ([Says_Kas_message_form, less_SucI, 
6452  752 
analz_insert_eq, not_parts_not_analz, 
753 
analz_insert_freshK1] @ pushes)))); 

754 
(*Fake*) 

755 
by (spy_analz_tac 1); 

756 
(*K2*) 

757 
by (blast_tac (claset() addSEs spies_partsEs 

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

759 
(*K4*) 

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

761 
(*Level 8: K5*) 

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

763 
addDs [Says_Kas_message_form, 

764 
Says_imp_spies RS parts.Inj] 

765 
addIs [less_SucI]) 1); 

766 
(*Oops1*) 

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

768 
(*Oops2*) 

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

770 
Says_Kas_message_form]) 1); 

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

772 

773 

774 
Goal "[ Says Kas A \ 

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

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

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

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

779 
\ ==> Key AuthKey \\<notin> analz (spies evs)"; 
7499  780 
by (ftac Says_Kas_message_form 1 THEN assume_tac 1); 
6452  781 
by (blast_tac (claset() addSDs [lemma]) 1); 
782 
qed "Confidentiality_Kas"; 

783 

784 

785 
(********************** Guarantees for Tgs *****************************) 

786 

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

788 
the Key has expired **) 

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

789 
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

790 
\ ==> Key AuthKey \\<notin> analz (spies evs) > \ 
6452  791 
\ Says Tgs A \ 
792 
\ (Crypt AuthKey \ 

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

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

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

796 
\ Key ServKey \\<in> analz (spies evs) > \ 
6452  797 
\ ExpirServ Tt evs"; 
798 
by (etac kerberos.induct 1); 

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

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

800 
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

801 
conclude AuthKey \\<noteq> AuthKeya.*) 
6452  802 
by (Clarify_tac 9); 
803 
by analz_sees_tac; 

804 
by (rotate_tac ~1 11); 

805 
by (ALLGOALS 

806 
(asm_full_simp_tac 

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

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

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

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

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

811 
@ pushes))); 
6452  812 
(*Fake*) 
813 
by (spy_analz_tac 1); 

814 
(*K2*) 

815 
by (blast_tac (claset() addSEs spies_partsEs 

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

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

818 
by (case_tac "A \\<noteq> Aa" 1); 
6452  819 
by (blast_tac (claset() addSEs spies_partsEs 
820 
addIs [less_SucI]) 1); 

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

822 
A_trusts_AuthTicket, 

823 
Confidentiality_Kas, 

824 
impOfSubs analz_subset_parts]) 1); 

825 
by (ALLGOALS Clarify_tac); 

826 
(*Oops2*) 

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

828 
Key_unique_SesKey] addIs [less_SucI]) 3); 

829 
(** Level 12 **) 

830 
(*Oops1*) 

7499  831 
by (ftac Says_Kas_message_form 2); 
6452  832 
by (assume_tac 2); 
833 
by (blast_tac (claset() addDs [analz_insert_freshK3, 

834 
Says_Kas_message_form, Says_Tgs_message_form] 

835 
addIs [less_SucI]) 2); 

836 
(** Level 16 **) 

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

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

840 
by (rotate_tac ~1 1); 

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

842 
by (etac disjE 1); 

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

844 
Key_unique_SesKey]) 1); 

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

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

847 

848 

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

850 
Goal 

851 
"[ Says Tgs A \ 

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

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

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

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

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

857 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
7499  858 
by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); 
6452  859 
by (blast_tac (claset() addDs [lemma]) 1); 
860 
qed "Confidentiality_Tgs1"; 

861 

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

863 
Goal 

864 
"[ Says Kas A \ 

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

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

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

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

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

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

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

875 
qed "Confidentiality_Tgs2"; 

876 

877 
(*Most general form*) 

878 
val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2; 

879 

880 

881 
(********************** Guarantees for Alice *****************************) 

882 

883 
val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas; 

884 

885 
Goal 

886 
"[ Says Kas A \ 

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

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

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

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

891 
\ evs \\<in> kerberos ] \ 
6452  892 
\==> 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

893 
\ \\<in> set evs"; 
7499  894 
by (ftac Says_Kas_message_form 1 THEN assume_tac 1); 
6452  895 
by (etac rev_mp 1); 
896 
by (etac rev_mp 1); 

897 
by (etac rev_mp 1); 

898 
by (parts_induct_tac 1); 

899 
by (Fake_parts_insert_tac 1); 

900 
(*K2 and K4 remain*) 

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

902 
addSDs [unique_CryptKey]) 2); 

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

904 
AuthKeys_used]) 1); 

905 
qed "A_trusts_K4_bis"; 

906 

907 

908 
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

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

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

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

914 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
6452  915 
by (dtac A_trusts_AuthKey 1); 
916 
by (assume_tac 1); 

917 
by (assume_tac 1); 

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

919 
Says_Kas_message_form, 

920 
A_trusts_K4_bis, Confidentiality_Tgs2]) 1); 

921 
qed "Confidentiality_Serv_A"; 

922 

923 

924 
(********************** Guarantees for Bob *****************************) 

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

926 

927 
Goal 

928 
"[ 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

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

930 
\ ==> \\<exists>Tk. Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 
6452  931 
\ 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

932 
\ \\<in> set evs"; 
6452  933 
by (etac rev_mp 1); 
934 
by (parts_induct_tac 1); 

935 
by Auto_tac; 

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

937 
A_trusts_AuthTicket]) 1); 

938 
qed "K4_imp_K2"; 

939 

940 
Goal 

941 
"[ 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

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

943 
\ ==> \\<exists>Tk. (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 
6452  944 
\ 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

945 
\ \\<in> set evs \ 
6452  946 
\ & ServLife + Tt <= AuthLife + Tk)"; 
947 
by (etac rev_mp 1); 

948 
by (parts_induct_tac 1); 

949 
by Auto_tac; 

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

951 
A_trusts_AuthTicket]) 1); 

952 
qed "K4_imp_K2_refined"; 

953 

954 
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

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

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

957 
\==> \\<exists>AuthKey. \ 
6452  958 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, \ 
959 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}}) \ 

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

960 
\ \\<in> set evs"; 
6452  961 
by (etac rev_mp 1); 
962 
by (parts_induct_tac 1); 

963 
by (Fake_parts_insert_tac 1); 

964 
by (Blast_tac 1); 

965 
qed "B_trusts_ServKey"; 

966 

967 
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

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

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

970 
\ ==> \\<exists>AuthKey Tk. Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 
6452  971 
\ 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

972 
\ \\<in> set evs"; 
6452  973 
by (blast_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1); 
974 
qed "B_trusts_ServTicket_Kas"; 

975 

976 
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

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

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

979 
\ ==> \\<exists>AuthKey Tk. (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk,\ 
6452  980 
\ 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

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

984 
qed "B_trusts_ServTicket_Kas_refined"; 

985 

986 
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

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

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

989 
\==> \\<exists>Tk AuthKey. \ 
6452  990 
\ Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, \ 
991 
\ 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

992 
\ \\<in> set evs \ 
6452  993 
\ & Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 
994 
\ 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

995 
\ \\<in> set evs"; 
7499  996 
by (ftac B_trusts_ServKey 1); 
6452  997 
by (etac exE 4); 
7499  998 
by (ftac K4_imp_K2 4); 
6452  999 
by (Blast_tac 5); 
1000 
by (ALLGOALS assume_tac); 

1001 
qed "B_trusts_ServTicket"; 

1002 

1003 
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

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

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

1006 
\==> \\<exists>Tk AuthKey. \ 
6452  1007 
\ (Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, \ 
1008 
\ 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

1009 
\ \\<in> set evs \ 
6452  1010 
\ & Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Number Tt, \ 
1011 
\ 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

1012 
\ \\<in> set evs \ 
6452  1013 
\ & ServLife + Tt <= AuthLife + Tk)"; 
7499  1014 
by (ftac B_trusts_ServKey 1); 
6452  1015 
by (etac exE 4); 
7499  1016 
by (ftac K4_imp_K2_refined 4); 
6452  1017 
by (Blast_tac 5); 
1018 
by (ALLGOALS assume_tac); 

1019 
qed "B_trusts_ServTicket_refined"; 

1020 

1021 

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

1023 
\ ==> ~ ExpirAuth Tk evs"; 

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

1025 
qed "NotExpirServ_NotExpirAuth_refined"; 

1026 

1027 

1028 
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

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

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

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

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

1036 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
7499  1037 
by (ftac A_trusts_AuthKey 1); 
1038 
by (ftac Confidentiality_Kas 3); 

1039 
by (ftac B_trusts_ServTicket 6); 

6452  1040 
by (etac exE 9); 
1041 
by (etac exE 9); 

7499  1042 
by (ftac Says_Kas_message_form 9); 
6452  1043 
by (blast_tac (claset() addDs [A_trusts_K4, 
1044 
unique_ServKeys, unique_AuthKeys, 

1045 
Confidentiality_Tgs2]) 10); 

1046 
by (ALLGOALS assume_tac); 

1047 
(* 

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

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

1050 
Says_Kas_message_form, B_trusts_ServTicket, 

1051 
unique_ServKeys, unique_AuthKeys, 

1052 
Confidentiality_Kas, 

1053 
Confidentiality_Tgs2]) 1); 

1054 
*) 

1055 
qed "Confidentiality_B"; 

1056 

1057 

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

1059 
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

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

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

1063 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
6452  1064 
by (blast_tac (claset() addDs [B_trusts_ServTicket_refined, 
1065 
NotExpirServ_NotExpirAuth_refined, 

1066 
Confidentiality_Tgs2]) 1); 

1067 
qed "Confidentiality_B_refined"; 

1068 

1069 

1070 
(********************** Authenticity theorems *****************************) 

1071 

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

1073 

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

1075 

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

1077 
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

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

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

1081 
\ ~ ExpirAuth Tk evs; A \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1082 
\==>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

1083 
\ \\<in> set evs"; 
7499  1084 
by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1); 
6452  1085 
by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1); 
1086 
qed "A_trusts_ServKey"; 

1087 
(*Note: requires a temporal check*) 

1088 

1089 

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

1091 

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

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

1094 

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

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

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

1098 

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

1100 
"A_authenticity_refined" *) 

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

1101 
Goal "[ Crypt ServKey {Agent A, Number Ta} \\<in> parts (spies evs); \ 
6452  1102 
\ 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

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

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

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

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

1109 
by (etac rev_mp 1); 

1110 
by (etac kerberos.induct 1); 

7499  1111 
by (ftac Says_ticket_in_parts_spies 5); 
1112 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1113 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1114 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

1115 
by (Fake_parts_insert_tac 1); 

1116 
(*K3*) 

1117 
by (blast_tac (claset() addEs spies_partsEs 

1118 
addDs [A_trusts_AuthKey, 

1119 
Says_Kas_message_form, 

1120 
Says_Tgs_message_form]) 1); 

1121 
(*K4*) 

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

1123 
(*K5*) 

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

1125 
qed "Says_Auth"; 

1126 

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

1128 
Goal "[ Crypt ServKey {Agent A, Number Ta} \\<in> parts (spies evs); \ 
6452  1129 
\ 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

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

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

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

1136 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1137 
\ ==> 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

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

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

1143 
addSIs [Says_Auth]) 12); 

1144 
by (ALLGOALS assume_tac); 

1145 
qed "A_Authenticity"; 

1146 

1147 
(*Stronger form in the refined model*) 

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

1148 
Goal "[ Crypt ServKey {Agent A, Number Ta2} \\<in> parts (spies evs); \ 
6452  1149 
\ 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

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

1152 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1153 
\ ==> 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

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

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

1159 
addSIs [Says_Auth]) 9); 

1160 
by (ALLGOALS assume_tac); 

1161 
qed "A_Authenticity_refined"; 

1162 

1163 

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

1165 

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

1166 
Goal "[ Crypt ServKey (Number Ta) \\<in> parts (spies evs); \ 
6452  1167 
\ 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

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

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

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

1171 
\ ==> Says B A (Crypt ServKey (Number Ta)) \\<in> set evs"; 
6452  1172 
by (etac rev_mp 1); 
1173 
by (etac rev_mp 1); 

1174 
by (etac rev_mp 1); 

1175 
by (etac kerberos.induct 1); 

7499  1176 
by (ftac Says_ticket_in_parts_spies 5); 
1177 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1178 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1179 
by (ALLGOALS Asm_simp_tac); 

1180 
by (Fake_parts_insert_tac 1); 

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

1182 
by (Clarify_tac 1); 

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

1186 
qed "Says_K6"; 

1187 

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

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

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

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

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

1192 
\ ==> \\<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

1193 
\ \\<in> set evs"; 
6452  1194 
by (etac rev_mp 1); 
1195 
by (etac rev_mp 1); 

1196 
by (parts_induct_tac 1); 

1197 
by (Fake_parts_insert_tac 1); 

1198 
by (Blast_tac 1); 

1199 
by (Blast_tac 1); 

1200 
qed "K4_trustworthy"; 

1201 

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

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

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

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

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

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

1212 
by (ftac Confidentiality_Kas 4); 

1213 
by (ftac K4_trustworthy 7); 

6452  1214 
by (Blast_tac 8); 
1215 
by (etac exE 9); 

7499  1216 
by (ftac K4_imp_K2 9); 
6452  1217 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 
1218 
addSIs [Says_K6] 

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

1220 
by (ALLGOALS assume_tac); 

1221 
qed "B_Authenticity"; 

1222 

1223 

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

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

1226 

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

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

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

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

1232 
by (rtac exI 1); 

1233 
by (rtac conjI 1); 

1234 
by (assume_tac 1); 

1235 
by (Simp_tac 1); 

1236 
by (etac rev_mp 1); 

1237 
by (etac rev_mp 1); 

1238 
by (etac kerberos.induct 1); 

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

6452  1241 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1242 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

1243 
by (Fake_parts_insert_tac 1); 

1244 
(*K6 requires numerous lemmas*) 

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

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

1247 
impOfSubs parts_spies_takeWhile_mono, 

1248 
impOfSubs parts_spies_evs_revD2] 

1249 
addIs [Says_K6] 

1250 
addEs spies_partsEs) 1); 

1251 
qed "B_Knows_B_Knows_ServKey_lemma"; 

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

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

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

1255 
Goal "[ Says B A (Crypt ServKey (Number Ta)) \\<in> set evs; \ 
6452  1256 
\ 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

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

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

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

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

1266 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1267 
qed "B_Knows_B_Knows_ServKey"; 

1268 

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

1269 
Goal "[ Says B A (Crypt ServKey (Number Ta)) \\<in> set evs; \ 
6452  1270 
\ 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

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

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

1276 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1277 
qed "B_Knows_B_Knows_ServKey_refined"; 

1278 

1279 

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

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

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

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

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

1289 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1290 
qed "A_Knows_B_Knows_ServKey"; 

1291 

1292 
Goal "[ Says A Tgs \ 

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

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

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

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

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

1298 
\ \\<in> set evs"; 
6452  1299 
by (etac rev_mp 1); 
1300 
by (parts_induct_tac 1); 

1301 
by (Fake_parts_insert_tac 1); 

1302 
by (Blast_tac 1); 

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

1304 
A_trusts_AuthKey]) 1); 

1305 
qed "K3_imp_K2"; 

1306 

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

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

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

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

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

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

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

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

1316 
\ \\<in> set evs"; 
6452  1317 
by (etac rev_mp 1); 
1318 
by (etac rev_mp 1); 

1319 
by (etac rev_mp 1); 

1320 
by (parts_induct_tac 1); 

1321 
by (Fake_parts_insert_tac 1); 

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

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

1324 
A_trusts_AuthTicket, unique_AuthKeys]) 1); 

1325 
qed "K4_trustworthy'"; 

1326 

1327 
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

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

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

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

1333 
by (rtac exI 1); 

1334 
by (rtac conjI 1); 

1335 
by (assume_tac 1); 

1336 
by (Simp_tac 1); 

1337 
by (etac rev_mp 1); 

1338 
by (etac rev_mp 1); 

1339 
by (etac kerberos.induct 1); 

7499  1340 
by (ftac Says_ticket_in_parts_spies 5); 
1341 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1342 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1343 
by (ALLGOALS Asm_simp_tac); 

1344 
by (Clarify_tac 1); 

1345 
(*K6*) 

1346 
by Auto_tac; 

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

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

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

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

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

1353 
simpset()) 1); 

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

1355 
impOfSubs parts_spies_takeWhile_mono, 

1356 
impOfSubs parts_spies_evs_revD2] 

1357 
addIs [Says_Auth] 

1358 
addEs spies_partsEs) 1); 

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

1360 
qed "A_Knows_A_Knows_ServKey_lemma"; 

1361 

1362 
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

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

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

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

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

1372 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1373 
qed "A_Knows_A_Knows_ServKey"; 

1374 

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

1375 
Goal "[ Crypt ServKey {Agent A, Number Ta} \\<in> parts (spies evs); \ 
6452  1376 
\ 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

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

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

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

1383 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452 