author  nipkow 
Tue, 08 Oct 2002 08:20:17 +0200  
changeset 13630  a013a9dd370f 
parent 11655  923e4d0d36d5 
child 13926  6e62e5357a10 
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 

11222  6 
The Kerberos protocol, version IV. Proofs streamlined by lcp. 
6452  7 
*) 
8 

11222  9 

10 
AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; 

11 
AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; 

12 

6452  13 
Pretty.setdepth 20; 
9000  14 
set timing; 
6452  15 

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

17 

18 

19 
(** Reversed traces **) 

20 

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

22 
by (induct_tac "evs" 1); 

23 
by (induct_tac "a" 2); 

24 
by Auto_tac; 

25 
qed "spies_Says_rev"; 

26 

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

28 
by (induct_tac "evs" 1); 

29 
by (induct_tac "a" 2); 

30 
by Auto_tac; 

31 
qed "spies_Gets_rev"; 

32 

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

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

35 
by (induct_tac "evs" 1); 

36 
by (induct_tac "a" 2); 

37 
by Auto_tac; 

38 
qed "spies_Notes_rev"; 

39 

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

41 
by (induct_tac "evs" 1); 

42 
by (induct_tac "a" 2); 

43 
by (ALLGOALS 

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

45 
spies_Notes_rev]))); 

46 
qed "spies_evs_rev"; 

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

48 

11288  49 
Goal "spies (takeWhile P evs) <= spies evs"; 
6452  50 
by (induct_tac "evs" 1); 
51 
by (induct_tac "a" 2); 

52 
by Auto_tac; 

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

54 
qed "spies_takeWhile"; 

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

56 

57 

58 
(*****************LEMMAS ABOUT AuthKeys****************) 

59 

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

61 
by (Simp_tac 1); 

62 
qed "AuthKeys_empty"; 

63 

64 
Goalw [AuthKeys_def] 

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

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

66 
\ ev \\<noteq> Says Kas A (Crypt (shrK A) {akey, Agent Peer, Tk, \ 
6452  67 
\ (Crypt (shrK Peer) {Agent A, Agent Peer, akey, Tk})}))\ 
68 
\ ==> AuthKeys (ev # evs) = AuthKeys evs"; 

69 
by Auto_tac; 

70 
qed "AuthKeys_not_insert"; 

71 

72 
Goalw [AuthKeys_def] 

73 
"AuthKeys \ 

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

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

76 
\ = insert K (AuthKeys evs)"; 

77 
by Auto_tac; 

78 
qed "AuthKeys_insert"; 

79 

80 
Goalw [AuthKeys_def] 

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

81 
"K \\<in> AuthKeys \ 
6452  82 
\ (Says Kas A (Crypt (shrK A) {Key K', Agent Peer, Number Tk, \ 
83 
\ (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

84 
\ ==> K = K'  K \\<in> AuthKeys evs"; 
6452  85 
by Auto_tac; 
86 
qed "AuthKeys_simp"; 

87 

88 
Goalw [AuthKeys_def] 

89 
"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

90 
\ (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

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

94 

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

95 
Goalw [AuthKeys_def] "K \\<in> AuthKeys evs ==> Key K \\<in> used evs"; 
6452  96 
by (Simp_tac 1); 
11222  97 
by (Blast_tac 1); 
6452  98 
qed "AuthKeys_used"; 
99 

100 

101 
(**** FORWARDING LEMMAS ****) 

102 

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

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

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

105 
\ \\<in> set evs ==> AuthTicket \\<in> parts (spies evs)"; 
11222  106 
by (Blast_tac 1); 
6452  107 
qed "K3_msg_in_parts_spies"; 
108 

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

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

110 
\ \\<in> set evs ==> AuthKey \\<in> parts (spies evs)"; 
11222  111 
by (Blast_tac 1); 
6452  112 
qed "Oops_parts_spies1"; 
113 

114 
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

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

116 
\ evs \\<in> kerberos ] ==> AuthKey \\<notin> range shrK"; 
6452  117 
by (etac rev_mp 1); 
118 
by (etac kerberos.induct 1); 

119 
by Auto_tac; 

120 
qed "Oops_range_spies1"; 

121 

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

123 
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

124 
\ \\<in> set evs ==> ServTicket \\<in> parts (spies evs)"; 
11222  125 
by (Blast_tac 1); 
6452  126 
qed "K5_msg_in_parts_spies"; 
127 

128 
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

129 
\ \\<in> set evs ==> ServKey \\<in> parts (spies evs)"; 
11222  130 
by (Blast_tac 1); 
6452  131 
qed "Oops_parts_spies2"; 
132 

133 
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

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

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

138 
by Auto_tac; 

139 
qed "Oops_range_spies2"; 

140 

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

141 
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

142 
\ ==> Ticket \\<in> parts (spies evs)"; 
11222  143 
by (Blast_tac 1); 
6452  144 
qed "Says_ticket_in_parts_spies"; 
145 
(*Replaces both K3_msg_in_parts_spies and K5_msg_in_parts_spies*) 

146 

147 
fun parts_induct_tac i = 

148 
etac kerberos.induct i THEN 

149 
REPEAT (FIRSTGOAL analz_mono_contra_tac) THEN 

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

152 
ftac Oops_parts_spies1 (i+8) THEN 

153 
ftac Oops_parts_spies2 (i+9) THEN 

6452  154 
prove_simple_subgoals_tac 1; 
155 

156 

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

158 
Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"; 
6452  159 
by (parts_induct_tac 1); 
160 
by (ALLGOALS Blast_tac); 

161 
qed "Spy_see_shrK"; 

162 
Addsimps [Spy_see_shrK]; 

163 

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

164 
Goal "evs \\<in> kerberos ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)"; 
11222  165 
by Auto_tac; 
6452  166 
qed "Spy_analz_shrK"; 
167 
Addsimps [Spy_analz_shrK]; 

168 

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

169 
Goal "[ Key (shrK A) \\<in> parts (spies evs); evs \\<in> kerberos ] ==> A:bad"; 
6452  170 
by (blast_tac (claset() addDs [Spy_see_shrK]) 1); 
171 
qed "Spy_see_shrK_D"; 

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

173 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

174 

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

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

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

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

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

180 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
6452  181 
(*Others*) 
11222  182 
by (ALLGOALS Blast_tac); 
6452  183 
qed_spec_mp "new_keys_not_used"; 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

184 
Addsimps [new_keys_not_used]; 
6452  185 

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

6452  188 
bind_thm ("new_keys_not_analzd", 
189 
[analz_subset_parts RS keysFor_mono, 

190 
new_keys_not_used] MRS contra_subsetD); 

191 

192 

193 
(*********************** REGULARITY LEMMAS ***********************) 

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

195 
(*****************************************************************) 

196 

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

198 
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

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

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

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

204 
by (etac rev_mp 1); 

205 
by (etac kerberos.induct 1); 

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

207 
by (ALLGOALS Blast_tac); 

208 
qed "Says_Kas_message_form"; 

209 

210 
(*This lemma is essential for proving Says_Tgs_message_form: 

211 

212 
the session key AuthKey 

213 
supplied by Kas in the authentication ticket 

214 
cannot be a longterm key! 

215 

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

217 
*) 

218 
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

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

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

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

11222  224 
by (Blast_tac 1); 
6452  225 
qed "SesKey_is_session_key"; 
226 

227 
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

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

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

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

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

11222  235 
(*Fake, K4*) 
236 
by (ALLGOALS Blast_tac); 

6452  237 
qed "A_trusts_AuthTicket"; 
238 

239 
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

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

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

242 
\ ==> AuthKey \\<in> AuthKeys evs"; 
7499  243 
by (ftac A_trusts_AuthTicket 1); 
6452  244 
by (assume_tac 1); 
245 
by (simp_tac (simpset() addsimps [AuthKeys_def]) 1); 

246 
by (Blast_tac 1); 

247 
qed "AuthTicket_crypt_AuthKey"; 

248 

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

250 
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

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

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

253 
\ ==> B \\<noteq> Tgs & ServKey \\<notin> range shrK & ServKey \\<notin> AuthKeys evs &\ 
6452  254 
\ 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

255 
\ AuthKey \\<notin> range shrK & AuthKey \\<in> AuthKeys evs"; 
6452  256 
by (etac rev_mp 1); 
257 
by (etac kerberos.induct 1); 

258 
by (ALLGOALS 

259 
(asm_full_simp_tac 

260 
(simpset() addsimps [AuthKeys_insert, AuthKeys_not_insert, 

261 
AuthKeys_empty, AuthKeys_simp]))); 

11288  262 
by (Blast_tac 1); 
6452  263 
by Auto_tac; 
11288  264 
(*Three subcases of Message 4*) 
6452  265 
by (blast_tac (claset() addSDs [AuthKeys_used, Says_Kas_message_form]) 1); 
11222  266 
by (blast_tac (claset() addSDs [SesKey_is_session_key]) 1); 
267 
by (blast_tac (claset() addDs [AuthTicket_crypt_AuthKey]) 1); 

6452  268 
qed "Says_Tgs_message_form"; 
269 

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

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

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

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

273 
\ A \\<notin> bad; evs \\<in> kerberos ] \ 
6452  274 
\ ==> 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

275 
\ \\<in> set evs"; 
6452  276 
by (etac rev_mp 1); 
277 
by (parts_induct_tac 1); 

278 
(*Fake*) 

11222  279 
by (Blast_tac 1); 
6452  280 
(*K4*) 
11222  281 
by (blast_tac (claset() addSDs [A_trusts_AuthTicket RS Says_Kas_message_form]) 
6452  282 
1); 
283 
qed "A_trusts_AuthKey"; 

284 

285 

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

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

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

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

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

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

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

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

293 
\ \\<in> set evs"; 
6452  294 
by (etac rev_mp 1); 
295 
by (etac rev_mp 1); 

296 
by (parts_induct_tac 1); 

297 
(*Fake*) 

11222  298 
by (Blast_tac 1); 
6452  299 
(*K2*) 
300 
by (Blast_tac 1); 

301 
(*K4*) 

302 
by Auto_tac; 

303 
qed "A_trusts_K4"; 

304 

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

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

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

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

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

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

312 
by (parts_induct_tac 1); 

11222  313 
by (ALLGOALS Blast_tac); 
6452  314 
qed "AuthTicket_form"; 
315 

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

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

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

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

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

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

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

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

325 
by (parts_induct_tac 1); 

11222  326 
by (Blast_tac 1); 
6452  327 
qed "ServTicket_form"; 
328 

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

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

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

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

332 
\ ==> AuthKey \\<notin> range shrK & \ 
6452  333 
\ AuthTicket = \ 
334 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Tk}\ 

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

335 
\  AuthTicket \\<in> analz (spies evs)"; 
11222  336 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, 
337 
AuthTicket_form]) 1); 

6452  338 
qed "Says_kas_message_form"; 
339 
(* Essentially the same as AuthTicket_form *) 

340 

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

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

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

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

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

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

347 
\  ServTicket \\<in> analz (spies evs)"; 
11222  348 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, 
349 
ServTicket_form]) 1); 

6452  350 
qed "Says_tgs_message_form"; 
351 
(* This form MUST be used in analz_sees_tac below *) 

352 

353 

354 
(*****************UNICITY THEOREMS****************) 

355 

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

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

358 
also Tgs in the place of B. *) 

359 

360 
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

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

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

364 
\ evs \\<in> kerberos ] \ 
6452  365 
\ ==> A=A' & B=B' & T=T'"; 
11104  366 
by (etac rev_mp 1); 
367 
by (etac rev_mp 1); 

368 
by (etac rev_mp 1); 

369 
by (parts_induct_tac 1); 

370 
(*Fake, K2, K4*) 

11222  371 
by (ALLGOALS Blast_tac); 
6452  372 
qed "unique_CryptKey"; 
373 

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

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

376 
*) 

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

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

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

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

381 
\ evs \\<in> kerberos ] \ 
6452  382 
\ ==> K=K' & B=B' & T=T' & Ticket=Ticket'"; 
11104  383 
by (etac rev_mp 1); 
384 
by (etac rev_mp 1); 

385 
by (etac rev_mp 1); 

386 
by (parts_induct_tac 1); 

387 
(*Fake, K2, K4*) 

11222  388 
by (ALLGOALS Blast_tac); 
6452  389 
qed "Key_unique_SesKey"; 
390 

391 

392 
(* 

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

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

395 
Similarly, at reception of any message mentioning an AuthKey 

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

397 
associates it with a new ServKey. 

398 

399 
Therefore, a goal like 

400 

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

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

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

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

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

407 
would fail on the K2 and K4 cases. 

408 
*) 

409 

410 
Goal "[ Says Kas A \ 

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

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

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

414 
\ evs \\<in> kerberos ] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'"; 
11104  415 
by (etac rev_mp 1); 
416 
by (etac rev_mp 1); 

417 
by (parts_induct_tac 1); 

418 
(*K2*) 

11222  419 
by (Blast_tac 1); 
6452  420 
qed "unique_AuthKeys"; 
421 

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

423 
Goal "[ Says Tgs A \ 

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

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

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

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

430 
by (parts_induct_tac 1); 

431 
(*K4*) 

11222  432 
by (Blast_tac 1); 
6452  433 
qed "unique_ServKeys"; 
434 

435 

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

437 

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

439 
by (Simp_tac 1); 

440 
qed "not_KeyCryptKey_Nil"; 

441 
AddIffs [not_KeyCryptKey_Nil]; 

442 

443 
Goalw [KeyCryptKey_def] 

11288  444 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, tt, X }) \\<in> set evs; \ 
445 
\ evs \\<in> kerberos ] ==> KeyCryptKey AuthKey ServKey evs"; 

11222  446 
by (blast_tac (claset() addDs [Says_Tgs_message_form]) 1); 
6452  447 
qed "KeyCryptKeyI"; 
448 

449 
Goalw [KeyCryptKey_def] 

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

451 
\ (Tgs = S & \ 

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

452 
\ (\\<exists>B tt. X = Crypt AuthKey \ 
6452  453 
\ {Key ServKey, Agent B, tt, \ 
454 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, tt} }) \ 

455 
\  KeyCryptKey AuthKey ServKey evs)"; 

456 
by (Simp_tac 1); 

457 
by (Blast_tac 1); 

458 
qed "KeyCryptKey_Says"; 

459 
Addsimps [KeyCryptKey_Says]; 

460 

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

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

463 
Goalw [KeyCryptKey_def] 

11288  464 
"[ Key AuthKey \\<notin> used evs; evs \\<in> kerberos ] \ 
465 
\ ==> ~ KeyCryptKey AuthKey ServKey evs"; 

6452  466 
by (etac rev_mp 1); 
467 
by (parts_induct_tac 1); 

468 
by (Asm_full_simp_tac 1); 

11222  469 
by (Blast_tac 1); 
6452  470 
qed "Auth_fresh_not_KeyCryptKey"; 
471 

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

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

474 
Goalw [KeyCryptKey_def] 

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

475 
"Key ServKey \\<notin> used evs ==> ~ KeyCryptKey AuthKey ServKey evs"; 
11222  476 
by (Blast_tac 1); 
6452  477 
qed "Serv_fresh_not_KeyCryptKey"; 
478 

11288  479 
Goal "[ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, tk}\ 
480 
\ \\<in> parts (spies evs); evs \\<in> kerberos ] \ 

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

6452  482 
by (etac rev_mp 1); 
483 
by (parts_induct_tac 1); 

484 
(*K4*) 

11222  485 
by (Blast_tac 3); 
6452  486 
(*K2: by freshness*) 
11204  487 
by (asm_full_simp_tac (simpset() addsimps [KeyCryptKey_def]) 2); 
11222  488 
by (ALLGOALS Blast_tac); 
6452  489 
qed "AuthKey_not_KeyCryptKey"; 
490 

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

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

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

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

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

6452  497 
by (etac rev_mp 1); 
498 
by (etac rev_mp 1); 

499 
by (parts_induct_tac 1); 

11222  500 
by (Blast_tac 1); 
6452  501 
(*K4 splits into distinct subcases*) 
11204  502 
by Auto_tac; 
6452  503 
(*ServKey can't have been enclosed in two certificates*) 
11222  504 
by (blast_tac (claset() addDs [unique_CryptKey]) 2); 
6452  505 
(*ServKey is fresh and so could not have been used, by new_keys_not_used*) 
11222  506 
by (force_tac (claset() addSDs [Crypt_imp_invKey_keysFor], 
507 
simpset() addsimps [KeyCryptKey_def]) 1); 

6452  508 
qed "ServKey_not_KeyCryptKey"; 
509 

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

511 
Goalw [KeyCryptKey_def] 

11288  512 
"evs \\<in> kerberos ==> ~ KeyCryptKey K (shrK A) evs"; 
6452  513 
by (parts_induct_tac 1); 
514 
qed "shrK_not_KeyCryptKey"; 

515 

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

517 
other key AuthKey.*) 

518 
Goalw [KeyCryptKey_def] 

11288  519 
"[ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, tt, X }) \ 
520 
\ \\<in> set evs; \ 

521 
\ AuthKey' \\<noteq> AuthKey; evs \\<in> kerberos ] \ 

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

6452  523 
by (blast_tac (claset() addDs [unique_ServKeys]) 1); 
524 
qed "Says_Tgs_KeyCryptKey"; 

525 

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

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

529 
by (parts_induct_tac 1); 

11288  530 
by Safe_tac; 
531 
(*K4 splits into subcases*) 

6452  532 
by (ALLGOALS Asm_full_simp_tac); 
11222  533 
by (blast_tac (claset() addSDs [AuthKey_not_KeyCryptKey]) 4); 
6452  534 
(*ServKey is fresh and so could not have been used, by new_keys_not_used*) 
535 
by (force_tac (claset() addSDs [Says_imp_spies RS parts.Inj, 

536 
Crypt_imp_invKey_keysFor], 

11222  537 
simpset() addsimps [KeyCryptKey_def]) 2); 
6452  538 
(*Others by freshness*) 
11222  539 
by (ALLGOALS Blast_tac); 
6452  540 
qed "KeyCryptKey_not_KeyCryptKey"; 
541 

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

543 
those sent by Tgs in step K4. *) 

544 

545 
(*We take some pains to express the property 

546 
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

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

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

552 

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

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

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

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

558 
by Auto_tac; 

559 
qed "KeyCryptKey_analz_insert"; 

560 

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

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

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

565 
qed "AuthKeys_are_not_KeyCryptKey"; 

566 

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

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

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

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

572 
qed "not_AuthKeys_not_KeyCryptKey"; 

573 

574 

575 
(*****************SECRECY THEOREMS****************) 

576 

577 
(*For proofs involving analz.*) 

578 
val analz_sees_tac = 

579 
EVERY 

580 
[REPEAT (FIRSTGOAL analz_mono_contra_tac), 

7499  581 
ftac Oops_range_spies2 10, 
582 
ftac Oops_range_spies1 9, 

583 
ftac Says_tgs_message_form 7, 

584 
ftac Says_kas_message_form 5, 

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

587 

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

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

589 
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

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

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

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

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

594 
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

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

596 

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

597 

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

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

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

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

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

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

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

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

607 
\ (SK \\<in> KK  Key SK \\<in> analz (spies evs)))"; 
6452  608 
by (etac kerberos.induct 1); 
609 
by analz_sees_tac; 

610 
by (REPEAT_FIRST (rtac allI)); 

611 
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

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

613 
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

614 
by (case_tac "KeyCryptKey ServKey SK evs5" 8); 
6452  615 
by (ALLGOALS 
616 
(asm_simp_tac 

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

618 
[KeyCryptKey_Says, shrK_not_KeyCryptKey, Oops2_not_KeyCryptKey, 
6452  619 
Auth_fresh_not_KeyCryptKey, Serv_fresh_not_KeyCryptKey, 
620 
Says_Tgs_KeyCryptKey, Spy_analz_shrK]))); 

621 
(*Fake*) 

622 
by (spy_analz_tac 1); 

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

624 
(*K3*) 

625 
by (Blast_tac 1); 

626 
(*K4*) 

11222  627 
by (blast_tac (claset() addSDs [AuthKey_not_KeyCryptKey]) 1); 
6452  628 
(*K5*) 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

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

632 
(simpset() addsimps [analz_insert_eq, 

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

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

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

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

11222  637 
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

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

639 
by (Asm_full_simp_tac 1); 
6452  640 
by (blast_tac (claset() addSDs [KeyCryptKey_analz_insert]) 1); 
641 
qed_spec_mp "Key_analz_image_Key"; 

642 

643 

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

645 
(* authentication keys or shared keys. *) 

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

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

647 
\ SesKey \\<notin> range shrK ] \ 
11655  648 
\ ==> (Key K \\<in> analz (insert (Key SesKey) (spies evs))) = \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

649 
\ (K = SesKey  Key K \\<in> analz (spies evs))"; 
7499  650 
by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1); 
11288  651 
by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); 
6452  652 
qed "analz_insert_freshK1"; 
653 

654 

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

656 
(* any other keys. *) 

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

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

659 
\ (K = ServKey  Key K \\<in> analz (spies evs))"; 
7499  660 
by (ftac not_AuthKeys_not_KeyCryptKey 1 
6452  661 
THEN assume_tac 1 
662 
THEN assume_tac 1); 

11288  663 
by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); 
6452  664 
qed "analz_insert_freshK2"; 
665 

666 

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

668 
(* encrypts a certain service key. *) 

669 
Goal 

670 
"[ Says Tgs A \ 

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

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

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

673 
\ AuthKey \\<noteq> AuthKey'; AuthKey' \\<notin> range shrK; evs \\<in> kerberos ] \ 
11655  674 
\ ==> (Key ServKey \\<in> analz (insert (Key AuthKey') (spies evs))) = \ 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

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

678 
by (assume_tac 1); 

11288  679 
by (asm_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); 
6452  680 
qed "analz_insert_freshK3"; 
681 

682 

683 
(*a weakness of the protocol*) 

684 
Goal "[ Says Tgs A \ 

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

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

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

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

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

691 
simpset()) 1); 

692 
qed "AuthKey_compromises_ServKey"; 

693 

694 

695 
(********************** Guarantees for Kas *****************************) 

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

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

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

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

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

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

701 
\ ==> ServKey \\<notin> AuthKeys evs"; 
6452  702 
by (etac rev_mp 1); 
703 
by (etac rev_mp 1); 

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

705 
by (parts_induct_tac 1); 

11222  706 
by (ALLGOALS Blast_tac); 
11288  707 
qed "ServKey_notin_AuthKeysD"; 
6452  708 

709 

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

711 
the Key has expired **) 

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

712 
Goal "[ A \\<notin> bad; evs \\<in> kerberos ] \ 
6452  713 
\ ==> Says Kas A \ 
714 
\ (Crypt (shrK A) \ 

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

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

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

718 
\ Key AuthKey \\<in> analz (spies evs) > \ 
6452  719 
\ ExpirAuth Tk evs"; 
720 
by (etac kerberos.induct 1); 

721 
by analz_sees_tac; 

722 
by (ALLGOALS 

723 
(asm_simp_tac 

11288  724 
(simpset() addsimps [Says_Kas_message_form, less_SucI, 
725 
analz_insert_eq, not_parts_not_analz, 

726 
analz_insert_freshK1] @ pushes))); 

6452  727 
(*Fake*) 
728 
by (spy_analz_tac 1); 

729 
(*K2*) 

11222  730 
by (Blast_tac 1); 
6452  731 
(*K4*) 
11222  732 
by (Blast_tac 1); 
6452  733 
(*Level 8: K5*) 
11288  734 
by (blast_tac (claset() addDs [ServKey_notin_AuthKeysD, Says_Kas_message_form] 
6452  735 
addIs [less_SucI]) 1); 
736 
(*Oops1*) 

11222  737 
by (blast_tac (claset() addSDs [unique_AuthKeys] addIs [less_SucI]) 1); 
6452  738 
(*Oops2*) 
739 
by (blast_tac (claset() addDs [Says_Tgs_message_form, 

740 
Says_Kas_message_form]) 1); 

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

742 

743 

744 
Goal "[ Says Kas A \ 

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

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

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

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

749 
\ ==> Key AuthKey \\<notin> analz (spies evs)"; 
11222  750 
by (blast_tac (claset() addDs [Says_Kas_message_form, lemma]) 1); 
6452  751 
qed "Confidentiality_Kas"; 
752 

753 

754 
(********************** Guarantees for Tgs *****************************) 

755 

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

757 
the Key has expired **) 

11288  758 
Goal "[ Says Tgs A \ 
6452  759 
\ (Crypt AuthKey \ 
760 
\ {Key ServKey, Agent B, Number Tt, \ 

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

11288  762 
\ \\<in> set evs; \ 
763 
\ Key AuthKey \\<notin> analz (spies evs); \ 

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

765 
\ ==> Key ServKey \\<in> analz (spies evs) > \ 

6452  766 
\ ExpirServ Tt evs"; 
11288  767 
by (etac rev_mp 1); 
768 
by (etac rev_mp 1); 

6452  769 
by (etac kerberos.induct 1); 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

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

771 
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

772 
conclude AuthKey \\<noteq> AuthKeya.*) 
6452  773 
by (Clarify_tac 9); 
774 
by analz_sees_tac; 

775 
by (ALLGOALS 

776 
(asm_full_simp_tac 

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

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

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

779 
analz_insert_eq, not_parts_not_analz, 
11288  780 
analz_insert_freshK1, analz_insert_freshK2, 
781 
analz_insert_freshK3] 

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

782 
@ pushes))); 
6452  783 
(*Fake*) 
784 
by (spy_analz_tac 1); 

785 
(*K2*) 

11288  786 
by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 1); 
6452  787 
(*K4*) 
11222  788 
by (blast_tac (claset() addDs [A_trusts_AuthTicket, Confidentiality_Kas]) 1); 
6452  789 
by (ALLGOALS Clarify_tac); 
790 
(*Oops2*) 

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

792 
Key_unique_SesKey] addIs [less_SucI]) 3); 

11222  793 
(** Level 10 **) 
6452  794 
(*Oops1*) 
11288  795 
by (blast_tac (claset() addDs [Says_Kas_message_form, Says_Tgs_message_form] 
796 
addIs [less_SucI]) 2); 

797 
(*K5. Not clear how this step could be integrated with the main 

798 
simplification step.*) 

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

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

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

11222  803 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] 
804 
addIs [less_SucI]) 1); 

11288  805 
qed_spec_mp "Confidentiality_lemma"; 
6452  806 

807 

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

11288  809 
Goal "[ Says Tgs A \ 
6452  810 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \ 
11288  811 
\ \\<in> set evs; \ 
812 
\ Key AuthKey \\<notin> analz (spies evs); \ 

813 
\ ~ ExpirServ Tt evs; \ 

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

815 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 

816 
by (blast_tac 

817 
(claset() addDs [Says_Tgs_message_form, Confidentiality_lemma]) 1); 

6452  818 
qed "Confidentiality_Tgs1"; 
819 

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

11288  821 
Goal "[ Says Kas A \ 
6452  822 
\ (Crypt Ka {Key AuthKey, Agent Tgs, Number Tk, AuthTicket}) \ 
11288  823 
\ \\<in> set evs; \ 
824 
\ Says Tgs A \ 

6452  825 
\ (Crypt AuthKey {Key ServKey, Agent B, Number Tt, ServTicket}) \ 
11288  826 
\ \\<in> set evs; \ 
827 
\ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ 

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

829 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 

6452  830 
by (blast_tac (claset() addSDs [Confidentiality_Kas, 
831 
Confidentiality_Tgs1]) 1); 

832 
qed "Confidentiality_Tgs2"; 

833 

834 
(*Most general form*) 

835 
val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2; 

836 

837 

838 
(********************** Guarantees for Alice *****************************) 

839 

840 
val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas; 

841 

842 
Goal 

843 
"[ Says Kas A \ 

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

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

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

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

848 
\ evs \\<in> kerberos ] \ 
6452  849 
\==> 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

850 
\ \\<in> set evs"; 
7499  851 
by (ftac Says_Kas_message_form 1 THEN assume_tac 1); 
6452  852 
by (etac rev_mp 1); 
853 
by (etac rev_mp 1); 

854 
by (etac rev_mp 1); 

855 
by (parts_induct_tac 1); 

11222  856 
by (Blast_tac 1); 
6452  857 
(*K2 and K4 remain*) 
11222  858 
by (blast_tac (claset() addSDs [unique_CryptKey]) 2); 
6452  859 
by (blast_tac (claset() addSDs [A_trusts_K4, Says_Tgs_message_form, 
860 
AuthKeys_used]) 1); 

861 
qed "A_trusts_K4_bis"; 

862 

863 

864 
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

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

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

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

870 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
6452  871 
by (dtac A_trusts_AuthKey 1); 
872 
by (assume_tac 1); 

873 
by (assume_tac 1); 

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

875 
Says_Kas_message_form, 

876 
A_trusts_K4_bis, Confidentiality_Tgs2]) 1); 

877 
qed "Confidentiality_Serv_A"; 

878 

879 

880 
(********************** Guarantees for Bob *****************************) 

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

882 

883 
Goal 

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

11288  885 
\ \\<in> set evs; evs \\<in> kerberos] \ 
886 
\ ==> \\<exists>Tk. Says Kas A \ 

887 
\ (Crypt (shrK A) \ 

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

6452  889 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 
11288  890 
\ \\<in> set evs"; 
6452  891 
by (etac rev_mp 1); 
892 
by (parts_induct_tac 1); 

893 
by Auto_tac; 

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

11288  895 
A_trusts_AuthTicket]) 1); 
6452  896 
qed "K4_imp_K2"; 
897 

898 
Goal 

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

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

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

903 
\ \\<in> set evs \ 
6452  904 
\ & ServLife + Tt <= AuthLife + Tk)"; 
905 
by (etac rev_mp 1); 

906 
by (parts_induct_tac 1); 

907 
by Auto_tac; 

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

11288  909 
A_trusts_AuthTicket]) 1); 
6452  910 
qed "K4_imp_K2_refined"; 
911 

912 
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

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

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

915 
\==> \\<exists>AuthKey. \ 
6452  916 
\ Says Tgs A (Crypt AuthKey {Key ServKey, Agent B, Tt, \ 
917 
\ Crypt (shrK B) {Agent A, Agent B, Key ServKey, Tt}}) \ 

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

918 
\ \\<in> set evs"; 
6452  919 
by (etac rev_mp 1); 
920 
by (parts_induct_tac 1); 

11222  921 
by (ALLGOALS Blast_tac); 
6452  922 
qed "B_trusts_ServKey"; 
923 

924 
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

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

926 
\ evs \\<in> kerberos ] \ 
11288  927 
\ ==> \\<exists>AuthKey Tk. \ 
928 
\ Says Kas A \ 

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

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

931 
\ \\<in> set evs"; 

6452  932 
by (blast_tac (claset() addSDs [B_trusts_ServKey, K4_imp_K2]) 1); 
933 
qed "B_trusts_ServTicket_Kas"; 

934 

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

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

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

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

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

943 
qed "B_trusts_ServTicket_Kas_refined"; 

944 

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

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

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

948 
\==> \\<exists>Tk AuthKey. \ 
6452  949 
\ Says Kas A (Crypt (shrK A) {Key AuthKey, Agent Tgs, Number Tk, \ 
950 
\ Crypt (shrK Tgs) {Agent A, Agent Tgs, Key AuthKey, Number Tk}})\ 

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

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

954 
\ \\<in> set evs"; 
11222  955 
by (blast_tac (claset() addDs [B_trusts_ServKey, K4_imp_K2]) 1); 
6452  956 
qed "B_trusts_ServTicket"; 
957 

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

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

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

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

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

967 
\ \\<in> set evs \ 
6452  968 
\ & ServLife + Tt <= AuthLife + Tk)"; 
11222  969 
by (blast_tac (claset() addDs [B_trusts_ServKey, K4_imp_K2_refined]) 1); 
6452  970 
qed "B_trusts_ServTicket_refined"; 
971 

972 

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

11288  974 
\ ==> ~ ExpirAuth Tk evs"; 
6452  975 
by (blast_tac (claset() addDs [leI,le_trans] addEs [leE]) 1); 
976 
qed "NotExpirServ_NotExpirAuth_refined"; 

977 

978 

979 
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

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

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

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

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

987 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
7499  988 
by (ftac A_trusts_AuthKey 1); 
989 
by (ftac Confidentiality_Kas 3); 

990 
by (ftac B_trusts_ServTicket 6); 

11222  991 
by (blast_tac (claset() addSDs [Confidentiality_Tgs2] 
992 
addDs [Says_Kas_message_form, A_trusts_K4, 

993 
unique_ServKeys, unique_AuthKeys]) 9); 

6452  994 
by (ALLGOALS assume_tac); 
995 
(* 

11222  996 
The proof above is fast. It can be done in one command in 50 secs: 
6452  997 
by (blast_tac (claset() addDs [A_trusts_AuthKey, A_trusts_K4, 
998 
Says_Kas_message_form, B_trusts_ServTicket, 

999 
unique_ServKeys, unique_AuthKeys, 

1000 
Confidentiality_Kas, 

1001 
Confidentiality_Tgs2]) 1); 

1002 
*) 

1003 
qed "Confidentiality_B"; 

1004 

1005 

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

1007 
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

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

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

1011 
\ ==> Key ServKey \\<notin> analz (spies evs)"; 
6452  1012 
by (blast_tac (claset() addDs [B_trusts_ServTicket_refined, 
1013 
NotExpirServ_NotExpirAuth_refined, 

1014 
Confidentiality_Tgs2]) 1); 

1015 
qed "Confidentiality_B_refined"; 

1016 

1017 

1018 
(********************** Authenticity theorems *****************************) 

1019 

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

1021 

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

1023 

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

1025 
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

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

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

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

1031 
\ \\<in> set evs"; 
11222  1032 
by (blast_tac (claset() addDs [A_trusts_AuthKey, Confidentiality_Auth_A, 
1033 
A_trusts_K4_bis]) 1); 

6452  1034 
qed "A_trusts_ServKey"; 
1035 
(*Note: requires a temporal check*) 

1036 

1037 

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

1039 

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

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

1042 

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

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

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

1046 

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

1048 
"A_authenticity_refined" *) 

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

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

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

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

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

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

1057 
by (etac rev_mp 1); 

1058 
by (etac kerberos.induct 1); 

7499  1059 
by (ftac Says_ticket_in_parts_spies 5); 
1060 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1061 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1062 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

11222  1063 
by (Blast_tac 1); 
6452  1064 
(*K3*) 
11222  1065 
by (blast_tac (claset() addDs [A_trusts_AuthKey, 
6452  1066 
Says_Kas_message_form, 
1067 
Says_Tgs_message_form]) 1); 

1068 
(*K4*) 

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

1070 
(*K5*) 

11222  1071 
by (blast_tac (claset() addDs [Key_unique_SesKey]) 1); 
6452  1072 
qed "Says_Auth"; 
1073 

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

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

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

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

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

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

1085 
\ Crypt ServKey {Agent A, Number Ta} } \\<in> set evs"; 
11222  1086 
by (blast_tac (claset() addIs [Says_Auth] 
1087 
addDs [Confidentiality_B, Key_unique_SesKey, 

1088 
B_trusts_ServKey]) 1); 

6452  1089 
qed "A_Authenticity"; 
1090 

1091 
(*Stronger form in the refined model*) 

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

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

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

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

1098 
\ Crypt ServKey {Agent A, Number Ta2} } \\<in> set evs"; 
11222  1099 
by (blast_tac (claset() addDs [Confidentiality_B_refined, B_trusts_ServKey, 
1100 
Key_unique_SesKey] 

1101 
addIs [Says_Auth]) 1); 

6452  1102 
qed "A_Authenticity_refined"; 
1103 

1104 

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

1106 

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

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

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

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

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

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

1115 
by (etac rev_mp 1); 

1116 
by (etac kerberos.induct 1); 

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

6452  1119 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1120 
by (ALLGOALS Asm_simp_tac); 

11222  1121 
by (Blast_tac 1); 
6452  1122 
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
1123 
by (Clarify_tac 1); 

7499  1124 
by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); 
6452  1125 
by (Clarify_tac 1); (*PROOF FAILED if omitted*) 
11222  1126 
by (blast_tac (claset() addDs [unique_CryptKey]) 1); 
6452  1127 
qed "Says_K6"; 
1128 

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

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

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

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

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

1134 
\ \\<in> set evs"; 
6452  1135 
by (etac rev_mp 1); 
1136 
by (etac rev_mp 1); 

1137 
by (parts_induct_tac 1); 

11288  1138 
by (ALLGOALS Blast_tac); 
6452  1139 
qed "K4_trustworthy"; 
1140 

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

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

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

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

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

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

1151 
by (ftac Confidentiality_Kas 4); 

1152 
by (ftac K4_trustworthy 7); 

6452  1153 
by (Blast_tac 8); 
1154 
by (etac exE 9); 

7499  1155 
by (ftac K4_imp_K2 9); 
11222  1156 
(*Yes the proof's a mess, but I don't know how to improve it.*) 
1157 
by (blast_tac (claset() addDs [Key_unique_SesKey] 

6452  1158 
addSIs [Says_K6] 
11222  1159 
addDs [Confidentiality_Tgs1]) 10); 
6452  1160 
by (ALLGOALS assume_tac); 
1161 
qed "B_Authenticity"; 

1162 

1163 

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

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

1166 

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

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

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

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

1172 
by (rtac exI 1); 

1173 
by (rtac conjI 1); 

1174 
by (assume_tac 1); 

1175 
by (Simp_tac 1); 

1176 
by (etac rev_mp 1); 

1177 
by (etac rev_mp 1); 

1178 
by (etac kerberos.induct 1); 

7499  1179 
by (ftac Says_ticket_in_parts_spies 5); 
1180 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1181 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1182 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

11222  1183 
by (Blast_tac 1); 
6452  1184 
(*K6 requires numerous lemmas*) 
1185 
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1); 

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

1187 
impOfSubs parts_spies_takeWhile_mono, 

1188 
impOfSubs parts_spies_evs_revD2] 

11222  1189 
addIs [Says_K6]) 1); 
6452  1190 
qed "B_Knows_B_Knows_ServKey_lemma"; 
11185
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

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

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

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

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

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

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

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

11288  1205 
B_Knows_B_Knows_ServKey_lemma]) 1); 
6452  1206 
qed "B_Knows_B_Knows_ServKey"; 
1207 

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

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

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

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

1215 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1216 
qed "B_Knows_B_Knows_ServKey_refined"; 

1217 

1218 

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

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

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

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

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

1228 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1229 
qed "A_Knows_B_Knows_ServKey"; 

1230 

1231 
Goal "[ Says A Tgs \ 

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

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

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

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

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

1237 
\ \\<in> set evs"; 
6452  1238 
by (etac rev_mp 1); 
1239 
by (parts_induct_tac 1); 

11222  1240 
by (Blast_tac 1); 
6452  1241 
by (Blast_tac 1); 
1242 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS 

1243 
A_trusts_AuthKey]) 1); 

1244 
qed "K3_imp_K2"; 

1245 

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

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

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

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

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

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

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

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

1255 
\ \\<in> set evs"; 
6452  1256 
by (etac rev_mp 1); 
1257 
by (etac rev_mp 1); 

1258 
by (etac rev_mp 1); 

1259 
by (parts_induct_tac 1); 

11222  1260 
by (Blast_tac 1); 
6452  1261 
by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
1262 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 

1263 
A_trusts_AuthTicket, unique_AuthKeys]) 1); 

1264 
qed "K4_trustworthy'"; 

1265 

1266 
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

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

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

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

1272 
by (rtac exI 1); 

1273 
by (rtac conjI 1); 

1274 
by (assume_tac 1); 

1275 
by (Simp_tac 1); 

1276 
by (etac rev_mp 1); 

1277 
by (etac rev_mp 1); 

1278 
by (etac kerberos.induct 1); 

7499  1279 
by (ftac Says_ticket_in_parts_spies 5); 
1280 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1281 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1282 
by (ALLGOALS Asm_simp_tac); 

1283 
by (Clarify_tac 1); 

1284 
(*K6*) 

1285 
by Auto_tac; 

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

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

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

11222  1289 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz_Decrypt', 
1290 
K3_imp_K2, K4_trustworthy', 

6452  1291 
impOfSubs parts_spies_takeWhile_mono, 
1292 
impOfSubs parts_spies_evs_revD2] 

11222  1293 
addIs [Says_Auth]) 1); 
6452  1294 
by (asm_full_simp_tac (simpset() addsimps [takeWhile_tail]) 1); 
1295 
qed "A_Knows_A_Knows_ServKey_lemma"; 

1296 

1297 
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

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

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

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

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

1307 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1308 
qed "A_Knows_A_Knows_ServKey"; 

1309 

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

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

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

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

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

1318 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1319 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs"; 
1320 
by (blast_tac (claset() addDs [A_Authenticity, Confidentiality_B, 

1321 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1322 
qed "B_Knows_A_Knows_ServKey"; 

1323 

1324 

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

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

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

1329 
\ B \\<noteq> Tgs; A \\<notin> bad; B \\<notin> bad; evs \\<in> kerberos ] \ 
6452  1330 
\ ==> A Issues B with (Crypt ServKey {Agent A, Number Ta}) on evs"; 
1331 
by (blast_tac (claset() addDs [A_Authenticity_refined, 

1332 
Confidentiality_B_refined, 

1333 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1334 
qed "B_Knows_A_Knows_ServKey_refined"; 