author  paulson 
Tue, 08 May 2001 15:57:13 +0200  
changeset 11288  7fe6593133d4 
parent 11222  72c5997e1145 
child 11655  923e4d0d36d5 
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 ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

648 
\ ==> Key K \\<in> analz (insert (Key SesKey) (spies evs)) = \ 
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]\ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

658 
\ ==> Key K \\<in> analz (insert (Key ServKey) (spies evs)) = \ 
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 ] \ 
1b737b4c2108
Some Xsymbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11104
diff
changeset

674 
\ ==> Key ServKey \\<in> analz (insert (Key AuthKey') (spies evs)) = \ 
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 (rotate_tac ~1 11); 

776 
by (ALLGOALS 

777 
(asm_full_simp_tac 

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

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

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

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

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

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

786 
(*K2*) 

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

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

793 
Key_unique_SesKey] addIs [less_SucI]) 3); 

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

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

799 
simplification step.*) 

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

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

803 
by (rotate_tac ~1 1); 

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

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

11288  807 
qed_spec_mp "Confidentiality_lemma"; 
6452  808 

809 

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

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

815 
\ ~ ExpirServ Tt evs; \ 

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

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

818 
by (blast_tac 

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

6452  820 
qed "Confidentiality_Tgs1"; 
821 

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

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

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

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

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

6452  832 
by (blast_tac (claset() addSDs [Confidentiality_Kas, 
833 
Confidentiality_Tgs1]) 1); 

834 
qed "Confidentiality_Tgs2"; 

835 

836 
(*Most general form*) 

837 
val Confidentiality_Tgs3 = A_trusts_AuthTicket RS Confidentiality_Tgs2; 

838 

839 

840 
(********************** Guarantees for Alice *****************************) 

841 

842 
val Confidentiality_Auth_A = A_trusts_AuthKey RS Confidentiality_Kas; 

843 

844 
Goal 

845 
"[ Says Kas A \ 

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

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

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

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

850 
\ evs \\<in> kerberos ] \ 
6452  851 
\==> 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

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

856 
by (etac rev_mp 1); 

857 
by (parts_induct_tac 1); 

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

863 
qed "A_trusts_K4_bis"; 

864 

865 

866 
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

867 
\ \\<in> parts (spies evs); \ 
6452  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> parts (spies 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 (dtac A_trusts_AuthKey 1); 
874 
by (assume_tac 1); 

875 
by (assume_tac 1); 

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

877 
Says_Kas_message_form, 

878 
A_trusts_K4_bis, Confidentiality_Tgs2]) 1); 

879 
qed "Confidentiality_Serv_A"; 

880 

881 

882 
(********************** Guarantees for Bob *****************************) 

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

884 

885 
Goal 

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

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

889 
\ (Crypt (shrK A) \ 

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

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

895 
by Auto_tac; 

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

11288  897 
A_trusts_AuthTicket]) 1); 
6452  898 
qed "K4_imp_K2"; 
899 

900 
Goal 

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

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

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

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

908 
by (parts_induct_tac 1); 

909 
by Auto_tac; 

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

11288  911 
A_trusts_AuthTicket]) 1); 
6452  912 
qed "K4_imp_K2_refined"; 
913 

914 
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

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

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

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

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

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

11222  923 
by (ALLGOALS Blast_tac); 
6452  924 
qed "B_trusts_ServKey"; 
925 

926 
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

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

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

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

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

933 
\ \\<in> set evs"; 

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

936 

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

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

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

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

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

945 
qed "B_trusts_ServTicket_Kas_refined"; 

946 

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

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

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

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

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

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

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

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

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

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

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

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

974 

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

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

979 

980 

981 
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

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

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

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

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

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

992 
by (ftac B_trusts_ServTicket 6); 

11222  993 
by (blast_tac (claset() addSDs [Confidentiality_Tgs2] 
994 
addDs [Says_Kas_message_form, A_trusts_K4, 

995 
unique_ServKeys, unique_AuthKeys]) 9); 

6452  996 
by (ALLGOALS assume_tac); 
997 
(* 

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

1001 
unique_ServKeys, unique_AuthKeys, 

1002 
Confidentiality_Kas, 

1003 
Confidentiality_Tgs2]) 1); 

1004 
*) 

1005 
qed "Confidentiality_B"; 

1006 

1007 

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

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

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

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

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

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

1016 
Confidentiality_Tgs2]) 1); 

1017 
qed "Confidentiality_B_refined"; 

1018 

1019 

1020 
(********************** Authenticity theorems *****************************) 

1021 

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

1023 

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

1025 

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

1027 
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

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

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

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

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

6452  1036 
qed "A_trusts_ServKey"; 
1037 
(*Note: requires a temporal check*) 

1038 

1039 

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

1041 

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

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

1044 

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

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

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

1048 

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

1050 
"A_authenticity_refined" *) 

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

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

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

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

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

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

1059 
by (etac rev_mp 1); 

1060 
by (etac kerberos.induct 1); 

7499  1061 
by (ftac Says_ticket_in_parts_spies 5); 
1062 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1063 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1064 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

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

1070 
(*K4*) 

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

1072 
(*K5*) 

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

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

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

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

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

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

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

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

1090 
B_trusts_ServKey]) 1); 

6452  1091 
qed "A_Authenticity"; 
1092 

1093 
(*Stronger form in the refined model*) 

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

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

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

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

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

1103 
addIs [Says_Auth]) 1); 

6452  1104 
qed "A_Authenticity_refined"; 
1105 

1106 

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

1108 

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

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

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

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

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

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

1117 
by (etac rev_mp 1); 

1118 
by (etac kerberos.induct 1); 

7499  1119 
by (ftac Says_ticket_in_parts_spies 5); 
1120 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1121 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1122 
by (ALLGOALS Asm_simp_tac); 

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

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

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

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

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

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

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

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

1139 
by (parts_induct_tac 1); 

11288  1140 
by (ALLGOALS Blast_tac); 
6452  1141 
qed "K4_trustworthy"; 
1142 

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

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

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

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

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

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

1153 
by (ftac Confidentiality_Kas 4); 

1154 
by (ftac K4_trustworthy 7); 

6452  1155 
by (Blast_tac 8); 
1156 
by (etac exE 9); 

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

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

1164 

1165 

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

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

1168 

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

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

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

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

1174 
by (rtac exI 1); 

1175 
by (rtac conjI 1); 

1176 
by (assume_tac 1); 

1177 
by (Simp_tac 1); 

1178 
by (etac rev_mp 1); 

1179 
by (etac rev_mp 1); 

1180 
by (etac kerberos.induct 1); 

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

6452  1183 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1184 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

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

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

1189 
impOfSubs parts_spies_takeWhile_mono, 

1190 
impOfSubs parts_spies_evs_revD2] 

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

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

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

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

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

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

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

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

11288  1207 
B_Knows_B_Knows_ServKey_lemma]) 1); 
6452  1208 
qed "B_Knows_B_Knows_ServKey"; 
1209 

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

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

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

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

1217 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1218 
qed "B_Knows_B_Knows_ServKey_refined"; 

1219 

1220 

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

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

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

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

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

1230 
B_Knows_B_Knows_ServKey_lemma]) 1); 

1231 
qed "A_Knows_B_Knows_ServKey"; 

1232 

1233 
Goal "[ Says A Tgs \ 

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

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

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

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

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

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

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

1245 
A_trusts_AuthKey]) 1); 

1246 
qed "K3_imp_K2"; 

1247 

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

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

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

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

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

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

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

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

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

1260 
by (etac rev_mp 1); 

1261 
by (parts_induct_tac 1); 

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

1265 
A_trusts_AuthTicket, unique_AuthKeys]) 1); 

1266 
qed "K4_trustworthy'"; 

1267 

1268 
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

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

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

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

1274 
by (rtac exI 1); 

1275 
by (rtac conjI 1); 

1276 
by (assume_tac 1); 

1277 
by (Simp_tac 1); 

1278 
by (etac rev_mp 1); 

1279 
by (etac rev_mp 1); 

1280 
by (etac kerberos.induct 1); 

7499  1281 
by (ftac Says_ticket_in_parts_spies 5); 
1282 
by (ftac Says_ticket_in_parts_spies 7); 

6452  1283 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
1284 
by (ALLGOALS Asm_simp_tac); 

1285 
by (Clarify_tac 1); 

1286 
(*K6*) 

1287 
by Auto_tac; 

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

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

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

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

6452  1293 
impOfSubs parts_spies_takeWhile_mono, 
1294 
impOfSubs parts_spies_evs_revD2] 

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

1298 

1299 
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

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

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

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

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

1309 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1310 
qed "A_Knows_A_Knows_ServKey"; 

1311 

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

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

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

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

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

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

1323 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1324 
qed "B_Knows_A_Knows_ServKey"; 

1325 

1326 

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

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

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

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

1334 
Confidentiality_B_refined, 

1335 
A_Knows_A_Knows_ServKey_lemma]) 1); 

1336 
qed "B_Knows_A_Knows_ServKey_refined"; 