author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 8741  61bc5ed22b62 
child 10833  c0844a30ea4e 
permissions  rwrr 
5053  1 
(* Title: HOL/Auth/Kerberos_BAN 
2 
ID: $Id$ 

3 
Author: Giampaolo Bella, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6 
The Kerberos protocol, BAN version. 

7 

8 
From page 251 of 

9 
Burrows, Abadi and Needham. A Logic of Authentication. 

10 
Proc. Royal Soc. 426 (1989) 

5064  11 

5223
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5114
diff
changeset

12 
Confidentiality (secrecy) and authentication properties rely on 
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5114
diff
changeset

13 
temporal checks: strong guarantees in a little abstracted  but 
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5114
diff
changeset

14 
very realistic  model (see .thy). 
5053  15 

5223
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5114
diff
changeset

16 
Tidied by lcp. 
5053  17 
*) 
18 

19 
AddEs spies_partsEs; 

20 
AddDs [impOfSubs analz_subset_parts]; 

21 
AddDs [impOfSubs Fake_parts_insert]; 

22 

5064  23 
AddIffs [SesKeyLife_LB, AutLife_LB]; 
5053  24 

25 

26 
(*A "possibility property": there are traces that reach the end.*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

27 
Goal "EX Timestamp K. EX evs: kerberos_ban. \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

28 
\ Says B A (Crypt K (Number Timestamp)) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

29 
\ : set evs"; 
5352  30 
by (cut_facts_tac [SesKeyLife_LB] 1); 
5053  31 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
32 
by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS 

33 
kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2); 

34 
by possibility_tac; 

5352  35 
by (ALLGOALS Asm_simp_tac); 
5053  36 
result(); 
37 

38 

39 

40 
(**** Inductive proofs about kerberos_ban ****) 

41 

42 
(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

43 
Goal "Says S A (Crypt KA {Timestamp, B, K, X}) : set evs \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

44 
\ ==> X : parts (spies evs)"; 
5053  45 
by (Blast_tac 1); 
46 
qed "Kb3_msg_in_parts_spies"; 

47 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

48 
Goal "Says Server A (Crypt (shrK A) {Timestamp, B, K, X}) : set evs \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

49 
\ ==> K : parts (spies evs)"; 
5053  50 
by (Blast_tac 1); 
51 
qed "Oops_parts_spies"; 

52 

53 
(*For proving the easier theorems about X ~: parts (spies evs).*) 

54 
fun parts_induct_tac i = 

55 
etac kerberos_ban.induct i THEN 

7499  56 
ftac Oops_parts_spies (i+6) THEN 
57 
ftac Kb3_msg_in_parts_spies (i+4) THEN 

5053  58 
prove_simple_subgoals_tac i; 
59 

60 

61 
(*Spy never sees another agent's shared key! (unless it's bad at start)*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

62 
Goal "evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; 
5053  63 
by (parts_induct_tac 1); 
64 
by (ALLGOALS Blast_tac); 

65 
qed "Spy_see_shrK"; 

66 
Addsimps [Spy_see_shrK]; 

67 

68 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

69 
Goal "evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
5053  70 
by Auto_tac; 
71 
qed "Spy_analz_shrK"; 

72 
Addsimps [Spy_analz_shrK]; 

73 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

74 
Goal "[ Key (shrK A) : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

75 
\ evs : kerberos_ban ] ==> A:bad"; 
5053  76 
by (blast_tac (claset() addDs [Spy_see_shrK]) 1); 
77 
qed "Spy_see_shrK_D"; 

78 

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

80 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

81 

82 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

84 
Goal "evs : kerberos_ban ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

85 
\ Key K ~: used evs > K ~: keysFor (parts (spies evs))"; 
5053  86 
by (parts_induct_tac 1); 
87 
(*Fake*) 

88 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 

89 
(*Kb2, Kb3, Kb4*) 

90 
by (ALLGOALS Blast_tac); 

91 
qed_spec_mp "new_keys_not_used"; 

92 

93 
bind_thm ("new_keys_not_analzd", 

94 
[analz_subset_parts RS keysFor_mono, 

95 
new_keys_not_used] MRS contra_subsetD); 

96 

97 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

98 

99 

100 
(** Lemmas concerning the form of items passed in messages **) 

101 

102 
(*Describes the form of K, X and K' when the Server sends this message.*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

103 
Goal "[ Says Server A (Crypt K' {Number Ts, Agent B, Key K, X}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

104 
\ : set evs; evs : kerberos_ban ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

105 
\ ==> K ~: range shrK & \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

106 
\ X = (Crypt (shrK B) {Number Ts, Agent A, Key K}) & \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

107 
\ K' = shrK A"; 
5053  108 
by (etac rev_mp 1); 
109 
by (etac kerberos_ban.induct 1); 

110 
by Auto_tac; 

111 
qed "Says_Server_message_form"; 

112 

113 

114 
(*If the encrypted message appears then it originated with the Server 

115 
PROVIDED that A is NOT compromised! 

116 

117 
This shows implicitly the FRESHNESS OF THE SESSION KEY to A 

118 
*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

119 
Goal "[ Crypt (shrK A) {Number Ts, Agent B, Key K, X} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

120 
\ : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

121 
\ A ~: bad; evs : kerberos_ban ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

122 
\ ==> Says Server A (Crypt (shrK A) {Number Ts, Agent B, Key K, X}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

123 
\ : set evs"; 
5053  124 
by (etac rev_mp 1); 
125 
by (parts_induct_tac 1); 

126 
by (Blast_tac 1); 

127 
qed "A_trusts_K_by_Kb2"; 

128 

129 

130 
(*If the TICKET appears then it originated with the Server*) 

131 
(*FRESHNESS OF THE SESSION KEY to B*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

132 
Goal "[ Crypt (shrK B) {Number Ts, Agent A, Key K} : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

133 
\ B ~: bad; evs : kerberos_ban ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

134 
\ ==> Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

135 
\ (Crypt (shrK A) {Number Ts, Agent B, Key K, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

136 
\ Crypt (shrK B) {Number Ts, Agent A, Key K}}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

137 
\ : set evs"; 
5053  138 
by (etac rev_mp 1); 
139 
by (parts_induct_tac 1); 

140 
by (Blast_tac 1); 

141 
qed "B_trusts_K_by_Kb3"; 

142 

143 

144 
(*EITHER describes the form of X when the following message is sent, 

145 
OR reduces it to the Fake case. 

146 
Use Says_Server_message_form if applicable.*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

147 
Goal "[ Says S A (Crypt (shrK A) {Number Ts, Agent B, Key K, X}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

148 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

149 
\ evs : kerberos_ban ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

150 
\==> (K ~: range shrK & X = (Crypt (shrK B) {Number Ts, Agent A, Key K}))\ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

151 
\  X : analz (spies evs)"; 
5053  152 
by (case_tac "A : bad" 1); 
153 
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] 

154 
addss (simpset())) 1); 

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

156 
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, 

157 
Says_Server_message_form]) 1); 

158 
qed "Says_S_message_form"; 

159 

160 

161 
(*For proofs involving analz.*) 

162 
val analz_spies_tac = 

7499  163 
ftac Says_Server_message_form 7 THEN 
164 
ftac Says_S_message_form 5 THEN 

5053  165 
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); 
166 

167 

168 
(**** 

169 
The following is to prove theorems of the form 

170 

171 
Key K : analz (insert (Key KAB) (spies evs)) ==> 

172 
Key K : analz (spies evs) 

173 

174 
A more general formula must be proved inductively. 

175 

176 
****) 

177 

178 

179 
(** Session keys are not used to encrypt other session keys **) 

180 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

181 
Goal "evs : kerberos_ban ==> \ 
5492  182 
\ ALL K KK. KK <=  (range shrK) > \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

183 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

184 
\ (K : KK  Key K : analz (spies evs))"; 
5053  185 
by (etac kerberos_ban.induct 1); 
186 
by analz_spies_tac; 

187 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 

188 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); 

189 
(*Takes 5 secs*) 

190 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 

191 
(*Fake*) 

192 
by (spy_analz_tac 1); 

193 
qed_spec_mp "analz_image_freshK"; 

194 

195 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

196 
Goal "[ evs : kerberos_ban; KAB ~: range shrK ] ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

197 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

198 
\ (K = KAB  Key K : analz (spies evs))"; 
5053  199 
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); 
200 
qed "analz_insert_freshK"; 

201 

202 

203 
(** The session key K uniquely identifies the message **) 

204 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

205 
Goal "evs : kerberos_ban ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

206 
\ EX A' Ts' B' X'. ALL A Ts B X. \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

207 
\ Says Server A (Crypt (shrK A) {Number Ts, Agent B, Key K, X}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

208 
\ : set evs \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

209 
\ > A=A' & Ts=Ts' & B=B' & X=X'"; 
5053  210 
by (etac kerberos_ban.induct 1); 
211 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 

212 
by Safe_tac; 

213 
(*Kb2: it can't be a new key*) 

214 
by (expand_case_tac "K = ?y" 1); 

215 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

216 
by (blast_tac (claset() delrules [conjI]) 1); 

217 
val lemma = result(); 

218 

219 
(*In messages of this form, the session key uniquely identifies the rest*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

220 
Goal "[ Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

221 
\ (Crypt (shrK A) {Number Ts, Agent B, Key K, X}) : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

222 
\ Says Server A' \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

223 
\ (Crypt (shrK A') {Number Ts', Agent B', Key K, X'}) : set evs;\ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

224 
\ evs : kerberos_ban ] ==> A=A' & Ts=Ts' & B=B' & X = X'"; 
5053  225 
by (prove_unique_tac lemma 1); 
226 
qed "unique_session_keys"; 

227 

228 

229 
(** Lemma: the session key sent in msg Kb2 would be EXPIRED 

230 
if the spy could see it! 

231 
**) 

232 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

233 
Goal "[ A ~: bad; B ~: bad; evs : kerberos_ban ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

234 
\ ==> Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

235 
\ (Crypt (shrK A) {Number Ts, Agent B, Key K, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

236 
\ Crypt (shrK B) {Number Ts, Agent A, Key K}})\ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

237 
\ : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

238 
\ Key K : analz (spies evs) > Expired Ts evs"; 
5053  239 
by (etac kerberos_ban.induct 1); 
240 
by analz_spies_tac; 

241 
by (ALLGOALS 

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

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

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

244 
@ pushes))); 
5053  245 
(*Oops*) 
246 
by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4); 

247 
(*Kb2*) 

5064  248 
by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2); 
5053  249 
(*Fake*) 
250 
by (spy_analz_tac 1); 

251 
(**LEVEL 6 **) 

5064  252 
(*Kb3*) 
5053  253 
by (case_tac "Aa : bad" 1); 
5064  254 
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2); 
255 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, 

256 
Crypt_Spy_analz_bad, analz.Fst, analz.Snd] 

5053  257 
addIs [less_SucI]) 1); 
5479  258 
qed_spec_mp "lemma2"; 
5053  259 

260 

261 
(** CONFIDENTIALITY for the SERVER: 

262 
Spy does not see the keys sent in msg Kb2 

263 
as long as they have NOT EXPIRED 

264 
**) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

265 
Goal "[ Says Server A \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

266 
\ (Crypt K' {Number T, Agent B, Key K, X}) : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

267 
\ ~ Expired T evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

268 
\ A ~: bad; B ~: bad; evs : kerberos_ban \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

269 
\ ] ==> Key K ~: analz (spies evs)"; 
7499  270 
by (ftac Says_Server_message_form 1 THEN assume_tac 1); 
5479  271 
by (blast_tac (claset() addIs [lemma2]) 1); 
5053  272 
qed "Confidentiality_S"; 
273 

274 
(**** THE COUNTERPART OF CONFIDENTIALITY 

275 
[...; Expired Ts evs; ...] ==> Key K : analz (spies evs) 

276 
WOULD HOLD ONLY IF AN OOPS OCCURRED! > Nothing to prove! ****) 

277 

278 

279 
(** CONFIDENTIALITY for ALICE: **) 

280 
(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

281 
Goal "[ Crypt (shrK A) {Number T, Agent B, Key K, X} : parts (spies evs);\ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

282 
\ ~ Expired T evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

283 
\ A ~: bad; B ~: bad; evs : kerberos_ban \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

284 
\ ] ==> Key K ~: analz (spies evs)"; 
5064  285 
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1); 
5053  286 
qed "Confidentiality_A"; 
287 

288 

289 
(** CONFIDENTIALITY for BOB: **) 

290 
(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

291 
Goal "[ Crypt (shrK B) {Number Tk, Agent A, Key K} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

292 
\ : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

293 
\ ~ Expired Tk evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

294 
\ A ~: bad; B ~: bad; evs : kerberos_ban \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

295 
\ ] ==> Key K ~: analz (spies evs)"; 
5053  296 
by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, 
297 
Confidentiality_S]) 1); 

298 
qed "Confidentiality_B"; 

299 

300 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

301 
Goal "[ B ~: bad; evs : kerberos_ban ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

302 
\ ==> Key K ~: analz (spies evs) > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

303 
\ Says Server A (Crypt (shrK A) {Number Ts, Agent B, Key K, X}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

304 
\ : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

305 
\ Crypt K (Number Ta) : parts (spies evs) > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

306 
\ Says B A (Crypt K (Number Ta)) : set evs"; 
5053  307 
by (etac kerberos_ban.induct 1); 
7499  308 
by (ftac Says_S_message_form 5 THEN assume_tac 5); 
5053  309 
by (dtac Kb3_msg_in_parts_spies 5); 
7499  310 
by (ftac Oops_parts_spies 7); 
5064  311 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
5053  312 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
5064  313 
(**LEVEL 6**) 
5053  314 
by (Blast_tac 1); 
5064  315 
by (Clarify_tac 1); 
5053  316 
(* 
317 
Subgoal 1: contradiction from the assumptions 

318 
Key K ~: used evs2 and Crypt K (Number Ta) : parts (spies evs2) 

319 
*) 

320 
by (dtac Crypt_imp_invKey_keysFor 1); 

321 
by (Asm_full_simp_tac 1); 

5064  322 
(* the two tactics above detect the contradiction*) 
5053  323 
by (case_tac "Ba : bad" 1); (*splits up the subgoal by the stated case*) 
324 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS 

325 
B_trusts_K_by_Kb3, 

326 
unique_session_keys]) 2); 

327 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS 

328 
Crypt_Spy_analz_bad]) 1); 

329 
val lemma_B = result(); 

330 

331 

332 
(*AUTHENTICATION OF B TO A*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

333 
Goal "[ Crypt K (Number Ta) : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

334 
\ Crypt (shrK A) {Number Ts, Agent B, Key K, X} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

335 
\ : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

336 
\ ~ Expired Ts evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

337 
\ A ~: bad; B ~: bad; evs : kerberos_ban ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

338 
\ ==> Says B A (Crypt K (Number Ta)) : set evs"; 
5053  339 
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2] 
340 
addSIs [lemma_B RS mp RS mp RS mp] 

341 
addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); 

342 
qed "Authentication_B"; 

343 

344 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

345 
Goal "[ A ~: bad; B ~: bad; evs : kerberos_ban ] ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

346 
\ Key K ~: analz (spies evs) > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

347 
\ Says Server A (Crypt (shrK A) {Number Ts, Agent B, Key K, X}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

348 
\ : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

349 
\ Crypt K {Agent A, Number Ta} : parts (spies evs) >\ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

350 
\ Says A B {X, Crypt K {Agent A, Number Ta}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

351 
\ : set evs"; 
5053  352 
by (etac kerberos_ban.induct 1); 
7499  353 
by (ftac Says_S_message_form 5 THEN assume_tac 5); 
354 
by (ftac Kb3_msg_in_parts_spies 5); 

355 
by (ftac Oops_parts_spies 7); 

5064  356 
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); 
5053  357 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
5064  358 
(**LEVEL 6**) 
5053  359 
by (Blast_tac 1); 
5064  360 
by (Clarify_tac 1); 
5053  361 
by (dtac Crypt_imp_invKey_keysFor 1); 
362 
by (Asm_full_simp_tac 1); 

5064  363 
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1); 
5053  364 
val lemma_A = result(); 
365 

366 

367 
(*AUTHENTICATION OF A TO B*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

368 
Goal "[ Crypt K {Agent A, Number Ta} : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

369 
\ Crypt (shrK B) {Number Ts, Agent A, Key K} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

370 
\ : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

371 
\ ~ Expired Ts evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

372 
\ A ~: bad; B ~: bad; evs : kerberos_ban ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

373 
\ ==> Says A B {Crypt (shrK B) {Number Ts, Agent A, Key K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

374 
\ Crypt K {Agent A, Number Ta}} : set evs"; 
5053  375 
by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3] 
376 
addSIs [lemma_A RS mp RS mp RS mp] 

377 
addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); 

378 
qed "Authentication_A"; 