author  paulson 
Fri, 20 Dec 1996 10:25:26 +0100  
changeset 2455  9c4444bfd44e 
parent 2451  ce85a2aafc7a 
child 2481  ee461c8bc9c3 
permissions  rwrr 
2449  1 
(* Title: HOL/Auth/Recur 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "recur" for the Recursive Authentication protocol. 

7 
*) 

8 

9 
open Recur; 

10 

11 
proof_timing:=true; 

12 
HOL_quantifiers := false; 

13 
Pretty.setdepth 25; 

14 

15 

16 
(** Possibility properties: traces that reach the end 

17 
ONE theorem would be more elegant and faster! 

18 
By induction on a list of agents (no repetitions) 

19 
**) 

20 

21 
(*Simplest case: Alice goes directly to the server*) 

22 
goal thy 

23 
"!!A. A ~= Server \ 

24 
\ ==> EX K NA. EX evs: recur lost. \ 

25 
\ Says Server A {Agent A, \ 

26 
\ Crypt (shrK A) {Key K, Agent Server, Nonce NA}, \ 

27 
\ Agent Server} \ 

28 
\ : set_of_list evs"; 

29 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

30 
by (rtac (recur.Nil RS recur.RA1 RS 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

31 
(respond.One RSN (4,recur.RA3))) 2); 
2449  32 
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); 
33 
by (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])); 

34 
result(); 

35 

36 

37 
(*Case two: Alice, Bob and the server*) 

38 
goal thy 

39 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 

40 
\ ==> EX K. EX NA. EX evs: recur lost. \ 

41 
\ Says B A {Agent A, Crypt (shrK A) {Key K, Agent B, Nonce NA}, \ 

42 
\ Agent Server} \ 

43 
\ : set_of_list evs"; 

44 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

45 
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

46 
(respond.One RS respond.Cons RSN (4,recur.RA3)) RS 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

47 
recur.RA4) 2); 
2449  48 
by (REPEAT 
49 
(REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]) 

50 
THEN 

51 
ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver)))); 

52 
result(); 

53 

54 

55 
(*Case three: Alice, Bob, Charlie and the server*) 

56 
goal thy 

57 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 

58 
\ ==> EX K. EX NA. EX evs: recur lost. \ 

59 
\ Says B A {Agent A, Crypt (shrK A) {Key K, Agent B, Nonce NA}, \ 

60 
\ Agent Server} \ 

61 
\ : set_of_list evs"; 

62 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

63 
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
2449  64 
(respond.One RS respond.Cons RS respond.Cons RSN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

65 
(4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); 
2449  66 
by (REPEAT (*SLOW: 37 seconds*) 
67 
(REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]) 

68 
THEN 

69 
ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver)))); 

70 
by (ALLGOALS 

71 
(SELECT_GOAL (DEPTH_SOLVE 

72 
(swap_res_tac [refl, conjI, disjI1, disjI2] 1 APPEND 

73 
etac not_sym 1)))); 

74 
result(); 

75 

76 

77 

78 
(**** Inductive proofs about recur ****) 

79 

80 
(*Monotonicity*) 

81 
goal thy "!!evs. lost' <= lost ==> recur lost' <= recur lost"; 

82 
by (rtac subsetI 1); 

83 
by (etac recur.induct 1); 

84 
by (REPEAT_FIRST 

85 
(best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) 

86 
:: recur.intrs)))); 

87 
qed "recur_mono"; 

88 

89 
(*Nobody sends themselves messages*) 

90 
goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set_of_list evs"; 

91 
by (etac recur.induct 1); 

92 
by (Auto_tac()); 

93 
qed_spec_mp "not_Says_to_self"; 

94 
Addsimps [not_Says_to_self]; 

95 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 

96 

97 

98 
(*Simple inductive reasoning about responses*) 

99 
goal thy "!!j. (j,PA,RB) : respond i ==> RB : responses i"; 

100 
by (etac respond.induct 1); 

101 
by (REPEAT (ares_tac responses.intrs 1)); 

102 
qed "respond_imp_responses"; 

103 

104 

105 
(** For reasoning about the encrypted portion of messages **) 

106 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

107 
val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj > standard; 
2449  108 

109 
goal thy "!!evs. Says C' B {Agent B, X, Agent B, X', RA} : set_of_list evs \ 

110 
\ ==> RA : analz (sees lost Spy evs)"; 

111 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

112 
qed "RA4_analz_sees_Spy"; 
2449  113 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

114 
(*RA2_analz... and RA4_analz... let us treat those cases using the same 
2449  115 
argument as for the Fake case. This is possible for most, but not all, 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

116 
proofs: Fake does not invent new nonces (as in RA2), and of course Fake 
2449  117 
messages originate from the Spy. *) 
118 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

119 
bind_thm ("RA2_parts_sees_Spy", 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

120 
RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

121 
bind_thm ("RA4_parts_sees_Spy", 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

122 
RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 
2449  123 

124 
(*We instantiate the variable to "lost". Leaving it as a Var makes proofs 

125 
harder to complete, since simplification does less for us.*) 

126 
val parts_Fake_tac = 

127 
let val tac = forw_inst_tac [("lost","lost")] 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

128 
in tac RA2_parts_sees_Spy 4 THEN 
2449  129 
forward_tac [respond_imp_responses] 5 THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

130 
tac RA4_parts_sees_Spy 6 
2449  131 
end; 
132 

133 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) 

134 
fun parts_induct_tac i = SELECT_GOAL 

135 
(DETERM (etac recur.induct 1 THEN parts_Fake_tac THEN 

136 
(*Fake message*) 

137 
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, 

138 
impOfSubs Fake_parts_insert] 

139 
addss (!simpset)) 2)) THEN 

140 
(*Base case*) 

141 
fast_tac (!claset addss (!simpset)) 1 THEN 

142 
ALLGOALS Asm_simp_tac) i; 

143 

144 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 

145 
sends messages containing X! **) 

146 

147 

148 
(** Spy never sees another agent's longterm key (unless initially lost) **) 

149 

150 
goal thy 

151 
"!!evs. (j,PB,RB) : respond i \ 

152 
\ ==> Key K : parts {RB} > (EX j'. K = newK2(i,j') & j<=j')"; 

153 
be respond.induct 1; 

154 
by (Auto_tac()); 

155 
by (best_tac (!claset addDs [Suc_leD]) 1); 

156 
qed_spec_mp "Key_in_parts_respond"; 

157 

158 
goal thy 

159 
"!!evs. evs : recur lost \ 

160 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 

161 
by (parts_induct_tac 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

162 
(*RA2*) 
2449  163 
by (best_tac (!claset addSEs partsEs addSDs [parts_cut] 
164 
addss (!simpset)) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

165 
(*RA3*) 
2449  166 
by (fast_tac (!claset addDs [Key_in_parts_respond] 
167 
addss (!simpset addsimps [parts_insert_sees])) 1); 

168 
qed "Spy_see_shrK"; 

169 
Addsimps [Spy_see_shrK]; 

170 

171 
goal thy 

172 
"!!evs. evs : recur lost \ 

173 
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; 

174 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 

175 
qed "Spy_analz_shrK"; 

176 
Addsimps [Spy_analz_shrK]; 

177 

178 
goal thy "!!A. [ Key (shrK A) : parts (sees lost Spy evs); \ 

179 
\ evs : recur lost ] ==> A:lost"; 

180 
by (fast_tac (!claset addDs [Spy_see_shrK]) 1); 

181 
qed "Spy_see_shrK_D"; 

182 

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

184 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

185 

186 

187 
(*** Future keys can't be seen or used! ***) 

188 

189 
(*Nobody can have SEEN keys that will be generated in the future. *) 

190 
goal thy "!!evs. evs : recur lost ==> \ 

191 
\ length evs <= i > \ 

192 
\ Key (newK2(i,j)) ~: parts (sees lost Spy evs)"; 

193 
by (parts_induct_tac 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

194 
(*RA2*) 
2449  195 
by (best_tac (!claset addSEs partsEs 
196 
addSDs [parts_cut] 

197 
addDs [Suc_leD] 

198 
addss (!simpset addsimps [parts_insert2])) 3); 

199 
(*Fake*) 

200 
by (best_tac (!claset addDs [impOfSubs analz_subset_parts, 

201 
impOfSubs parts_insert_subset_Un, 

202 
Suc_leD] 

203 
addss (!simpset)) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

204 
(*For RA3*) 
2449  205 
by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

206 
(*RA1RA4*) 
2449  207 
by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD] 
208 
addss (!simpset)) 1)); 

209 
qed_spec_mp "new_keys_not_seen"; 

210 
Addsimps [new_keys_not_seen]; 

211 

212 
(*Variant: old messages must contain old keys!*) 

213 
goal thy 

214 
"!!evs. [ Says A B X : set_of_list evs; \ 

215 
\ Key (newK2(i,j)) : parts {X}; \ 

216 
\ evs : recur lost \ 

217 
\ ] ==> i < length evs"; 

218 
by (rtac ccontr 1); 

219 
by (dtac leI 1); 

220 
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] 

221 
addIs [impOfSubs parts_mono]) 1); 

222 
qed "Says_imp_old_keys"; 

223 

224 

225 
(*** Future nonces can't be seen or used! ***) 

226 

227 
goal thy 

228 
"!!evs. (j, PB, RB) : respond i \ 

229 
\ ==> Nonce N : parts {RB} > Nonce N : parts {PB}"; 

230 
be respond.induct 1; 

231 
by (Auto_tac()); 

232 
qed_spec_mp "Nonce_in_parts_respond"; 

233 

234 

235 
goal thy "!!i. evs : recur lost ==> \ 

236 
\ length evs <= i > Nonce(newN i) ~: parts (sees lost Spy evs)"; 

237 
by (parts_induct_tac 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

238 
(*For RA3*) 
2449  239 
by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 4); 
240 
by (deepen_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] 

241 
addDs [Nonce_in_parts_respond, parts_cut, Suc_leD] 

242 
addss (!simpset)) 0 4); 

243 
(*Fake*) 

244 
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts, 

245 
impOfSubs parts_insert_subset_Un, 

246 
Suc_leD] 

247 
addss (!simpset)) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

248 
(*RA1, RA2, RA4*) 
2449  249 
by (REPEAT_FIRST (fast_tac (!claset 
250 
addSEs partsEs 

251 
addEs [leD RS notE] 

252 
addDs [Suc_leD] 

253 
addss (!simpset)))); 

254 
qed_spec_mp "new_nonces_not_seen"; 

255 
Addsimps [new_nonces_not_seen]; 

256 

257 
(*Variant: old messages must contain old nonces!*) 

258 
goal thy "!!evs. [ Says A B X : set_of_list evs; \ 

259 
\ Nonce (newN i) : parts {X}; \ 

260 
\ evs : recur lost \ 

261 
\ ] ==> i < length evs"; 

262 
by (rtac ccontr 1); 

263 
by (dtac leI 1); 

264 
by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy] 

265 
addIs [impOfSubs parts_mono]) 1); 

266 
qed "Says_imp_old_nonces"; 

267 

268 

269 
(** Nobody can have USED keys that will be generated in the future. **) 

270 

271 
goal thy 

272 
"!!evs. (j,PB,RB) : respond i \ 

273 
\ ==> K : keysFor (parts {RB}) > (EX A. K = shrK A)"; 

274 
be (respond_imp_responses RS responses.induct) 1; 

275 
by (Auto_tac()); 

276 
qed_spec_mp "Key_in_keysFor_parts_respond"; 

277 

278 

279 
goal thy "!!i. evs : recur lost ==> \ 

280 
\ length evs <= i > newK2(i,j) ~: keysFor (parts (sees lost Spy evs))"; 

281 
by (parts_induct_tac 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

282 
(*RA3*) 
2449  283 
by (fast_tac (!claset addDs [Key_in_keysFor_parts_respond, Suc_leD] 
284 
addss (!simpset addsimps [parts_insert_sees])) 4); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

285 
(*RA2*) 
2449  286 
by (fast_tac (!claset addSEs partsEs 
287 
addDs [Suc_leD] addss (!simpset)) 3); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

288 
(*Fake, RA1, RA4*) 
2449  289 
by (REPEAT 
290 
(best_tac 

291 
(!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), 

292 
impOfSubs (parts_insert_subset_Un RS keysFor_mono), 

293 
Suc_leD] 

294 
addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] 

295 
addss (!simpset)) 1)); 

296 
qed_spec_mp "new_keys_not_used"; 

297 

298 

299 
bind_thm ("new_keys_not_analzd", 

300 
[analz_subset_parts RS keysFor_mono, 

301 
new_keys_not_used] MRS contra_subsetD); 

302 

303 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

304 

305 

306 

307 
(*** Proofs involving analz ***) 

308 

309 
(*For proofs involving analz. We again instantiate the variable to "lost".*) 

310 
val analz_Fake_tac = 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

311 
dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
2449  312 
forward_tac [respond_imp_responses] 5 THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

313 
dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6; 
2449  314 

315 

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

317 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

318 
(*Version for "responses" relation. Handles case RA3 in the theorem below. 
2449  319 
Note that it holds for *any* set H (not just "sees lost Spy evs") 
320 
satisfying the inductive hypothesis.*) 

321 
goal thy 

322 
"!!evs. [ RB : responses i; \ 

323 
\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \ 

324 
\ (K : newK``I  Key K : analz H) ] \ 

325 
\ ==> ALL K I. (Key K : analz (insert RB (Key``(newK``I) Un H))) = \ 

326 
\ (K : newK``I  Key K : analz (insert RB H))"; 

327 
be responses.induct 1; 

328 
by (ALLGOALS 

329 
(asm_simp_tac 

330 
(!simpset addsimps [insert_Key_singleton, insert_Key_image, 

331 
Un_assoc RS sym, pushKey_newK] 

332 
setloop split_tac [expand_if]))); 

333 
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); 

334 
qed "resp_analz_image_newK_lemma"; 

335 

336 
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) 

337 
goal thy 

338 
"!!evs. evs : recur lost ==> \ 

339 
\ ALL K I. (Key K : analz (Key``(newK``I) Un (sees lost Spy evs))) = \ 

340 
\ (K : newK``I  Key K : analz (sees lost Spy evs))"; 

341 
by (etac recur.induct 1); 

342 
by analz_Fake_tac; 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

343 
be ssubst 4; (*RA2: DELETE needless definition of PA!*) 
2449  344 
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); 
345 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma]))); 

346 
(*Base*) 

347 
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

348 
(*RA4, RA2, Fake*) 
2449  349 
by (REPEAT (spy_analz_tac 1)); 
350 
val raw_analz_image_newK = result(); 

351 
qed_spec_mp "analz_image_newK"; 

352 

353 

354 
(*Instance of the lemma with H replaced by (sees lost Spy evs): 

355 
[ RB : responses i; evs : recur lost ] 

356 
==> Key xa : analz (insert RB (Key``newK``x Un sees lost Spy evs)) = 

357 
(xa : newK``x  Key xa : analz (insert RB (sees lost Spy evs))) 

358 
*) 

359 
bind_thm ("resp_analz_image_newK", 

360 
raw_analz_image_newK RSN 

361 
(2, resp_analz_image_newK_lemma) RS spec RS spec); 

362 

363 
goal thy 

364 
"!!evs. evs : recur lost ==> \ 

365 
\ Key K : analz (insert (Key (newK x)) (sees lost Spy evs)) = \ 

366 
\ (K = newK x  Key K : analz (sees lost Spy evs))"; 

367 
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 

368 
insert_Key_singleton]) 1); 

369 
by (Fast_tac 1); 

370 
qed "analz_insert_Key_newK"; 

371 

372 

373 
(** Nonces cannot appear before their time, even hashed! 

374 
One is tempted to add the rule 

375 
"Hash X : parts H ==> X : parts H" 

376 
but we'd then lose theorems like Spy_see_shrK 

377 
***) 

378 

379 
goal thy "!!i. evs : recur lost ==> \ 

380 
\ length evs <= i > \ 

381 
\ (Nonce (newN i) : parts {X} > \ 

382 
\ Hash X ~: parts (sees lost Spy evs))"; 

383 
be recur.induct 1; 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

384 
be ssubst 4; (*RA2: DELETE needless definition of PA!*) 
2449  385 
by parts_Fake_tac; 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

386 
(*RA3 requires a further induction*) 
2449  387 
be responses.induct 5; 
388 
by (ALLGOALS Asm_simp_tac); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

389 
(*RA2*) 
2449  390 
by (best_tac (!claset addDs [Suc_leD, parts_cut] 
391 
addEs [leD RS notE, 

392 
new_nonces_not_seen RSN(2,rev_notE)] 

393 
addss (!simpset)) 4); 

394 
(*Fake*) 

395 
by (best_tac (!claset addSDs [impOfSubs analz_subset_parts, 

396 
impOfSubs parts_insert_subset_Un, 

397 
Suc_leD] 

398 
addss (!simpset)) 2); 

399 
(*Five others!*) 

400 
by (REPEAT (fast_tac (!claset addEs [leD RS notE] 

401 
addDs [Suc_leD] 

402 
addss (!simpset)) 1)); 

403 
bind_thm ("Hash_new_nonces_not_seen", 

404 
result() RS mp RS mp RSN (2, rev_notE)); 

405 

406 

407 
(** The Nonce NA uniquely identifies A's message. 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

408 
This theorem applies to rounds RA1 and RA2! 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

409 

9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

410 
Unicity is not used in other proofs but is desirable in its own right. 
2449  411 
**) 
412 

413 
goal thy 

414 
"!!evs. [ evs : recur lost; A ~: lost ] \ 

415 
\ ==> EX B' P'. ALL B P. \ 

416 
\ Hash {Key(shrK A), Agent A, Agent B, Nonce NA, P} \ 

417 
\ : parts (sees lost Spy evs) > B=B' & P=P'"; 

418 
be recur.induct 1; 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

419 
be ssubst 4; (*RA2: DELETE needless definition of PA!*) 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

420 
(*For better simplification of RA2*) 
2449  421 
by (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 4); 
422 
by parts_Fake_tac; 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

423 
(*RA3 requires a further induction*) 
2449  424 
be responses.induct 5; 
425 
by (ALLGOALS Asm_simp_tac); 

426 
by (step_tac (!claset addSEs partsEs) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

427 
(*RA3: inductive case*) 
2449  428 
by (best_tac (!claset addss (!simpset)) 5); 
429 
(*Fake*) 

430 
by (best_tac (!claset addSIs [exI] 

431 
addDs [impOfSubs analz_subset_parts, 

432 
impOfSubs Fake_parts_insert] 

433 
addss (!simpset)) 2); 

434 
(*Base*) 

435 
by (fast_tac (!claset addss (!simpset)) 1); 

436 

437 
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

438 
(*RA1: creation of new Nonce. Move assertion into global context*) 
2449  439 
by (expand_case_tac "NA = ?y" 1); 
440 
by (best_tac (!claset addSIs [exI] 

441 
addEs [Hash_new_nonces_not_seen] 

442 
addss (!simpset)) 1); 

443 
by (best_tac (!claset addss (!simpset)) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

444 
(*RA2: creation of new Nonce*) 
2449  445 
by (expand_case_tac "NA = ?y" 1); 
446 
by (best_tac (!claset addSIs [exI] 

447 
addDs [parts_cut] 

448 
addEs [Hash_new_nonces_not_seen] 

449 
addss (!simpset)) 1); 

450 
by (best_tac (!claset addss (!simpset)) 1); 

451 
val lemma = result(); 

452 

453 
goal thy 

454 
"!!evs.[ Hash {Key(shrK A), Agent A, Agent B, Nonce NA, P} \ 

455 
\ : parts (sees lost Spy evs); \ 

456 
\ Hash {Key(shrK A), Agent A, Agent B', Nonce NA, P'} \ 

457 
\ : parts (sees lost Spy evs); \ 

458 
\ evs : recur lost; A ~: lost ] \ 

459 
\ ==> B=B' & P=P'"; 

460 
by (prove_unique_tac lemma 1); 

461 
qed "unique_NA"; 

462 

463 

464 
(*** Lemmas concerning the Server's response 

465 
(relations "respond" and "responses") 

466 
***) 

467 

468 
(*The response never contains Hashes*) 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

469 
(*NEEDED????????????????*) 
2449  470 
goal thy 
471 
"!!evs. (j,PB,RB) : respond i \ 

472 
\ ==> Hash {Key (shrK B), M} : parts (insert RB H) > \ 

473 
\ Hash {Key (shrK B), M} : parts H"; 

474 
be (respond_imp_responses RS responses.induct) 1; 

475 
by (Auto_tac()); 

476 
bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp)); 

477 

478 

479 
goal thy 

480 
"!!evs. [ RB : responses i; evs : recur lost ] \ 

481 
\ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)"; 

482 
be responses.induct 1; 

483 
by (ALLGOALS 

484 
(asm_simp_tac 

485 
(!simpset addsimps [resp_analz_image_newK, insert_Key_singleton] 

486 
setloop split_tac [expand_if]))); 

487 
qed "shrK_in_analz_respond"; 

488 
Addsimps [shrK_in_analz_respond]; 

489 

490 

491 
goal thy 

492 
"!!evs. [ RB : responses i; \ 

493 
\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \ 

494 
\ (K : newK``I  Key K : analz H) ] \ 

495 
\ ==> (Key K : analz (insert RB H)) > \ 

496 
\ (Key K : parts{RB}  Key K : analz H)"; 

497 
be responses.induct 1; 

498 
by (ALLGOALS 

499 
(asm_simp_tac 

500 
(!simpset addsimps [read_instantiate [("H", "?ff``?xx")] parts_insert, 

501 
resp_analz_image_newK_lemma, 

502 
insert_Key_singleton, insert_Key_image, 

503 
Un_assoc RS sym, pushKey_newK] 

504 
setloop split_tac [expand_if]))); 

505 
(*The "Message" simpset gives the standard treatment of "image"*) 

506 
by (simp_tac (simpset_of "Message") 1); 

507 
by (fast_tac (!claset delrules [allE]) 1); 

508 
qed "resp_analz_insert_lemma"; 

509 

510 
bind_thm ("resp_analz_insert", 

511 
raw_analz_image_newK RSN 

512 
(2, resp_analz_insert_lemma) RSN(2, rev_mp)); 

513 

514 

515 
(*The Server does not send such messages. This theorem lets us avoid 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

516 
assuming B~=Server in RA4.*) 
2449  517 
goal thy 
518 
"!!evs. evs : recur lost \ 

519 
\ ==> ALL C X Y P. Says Server C {X, Agent Server, Agent C, Y, P} \ 

520 
\ ~: set_of_list evs"; 

521 
by (etac recur.induct 1); 

522 
be (respond.induct) 5; 

523 
by (Auto_tac()); 

524 
qed_spec_mp "Says_Server_not"; 

525 
AddSEs [Says_Server_not RSN (2,rev_notE)]; 

526 

527 

528 
goal thy 

529 
"!!i. (j,PB,RB) : respond i \ 

530 
\ ==> EX A' B'. ALL A B N. \ 

531 
\ Crypt (shrK A) {Key K, Agent B, N} : parts {RB} \ 

532 
\ > (A'=A & B'=B)  (A'=B & B'=A)"; 

533 
be respond.induct 1; 

534 
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 

535 
(*Base case*) 

536 
by (Fast_tac 1); 

537 
by (Step_tac 1); 

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

539 
by (best_tac (!claset addSIs [exI] 

540 
addSEs partsEs 

541 
addDs [Key_in_parts_respond] 

542 
addss (!simpset)) 1); 

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

544 
by (REPEAT (ares_tac [exI] 2)); 

545 
by (ex_strip_tac 1); 

546 
be respond.elim 1; 

547 
by (REPEAT_FIRST (etac Pair_inject ORELSE' hyp_subst_tac)); 

548 
by (ALLGOALS (asm_full_simp_tac 

549 
(!simpset addsimps [all_conj_distrib, ex_disj_distrib]))); 

550 
by (Fast_tac 1); 

551 
by (Fast_tac 1); 

552 
val lemma = result(); 

553 

554 
goal thy 

555 
"!!RB. [ Crypt (shrK A) {Key K, Agent B, N} : parts {RB}; \ 

556 
\ Crypt (shrK A') {Key K, Agent B', N'} : parts {RB}; \ 

557 
\ (j,PB,RB) : respond i ] \ 

558 
\ ==> (A'=A & B'=B)  (A'=B & B'=A)"; 

559 
by (prove_unique_tac lemma 1); (*33 seconds, due to the disjunctions*) 

560 
qed "unique_session_keys"; 

561 

562 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

563 
(** Crucial secrecy property: Spy does not see the keys sent in msg RA3 
2449  564 
Does not in itself guarantee security: an attack could violate 
565 
the premises, e.g. by having A=Spy **) 

566 

567 
goal thy 

568 
"!!j. (j, {Hash {Key(shrK A), Agent A, B, NA, P}, X}, RA) : respond i \ 

569 
\ ==> Crypt (shrK A) {Key (newK2 (i,j)), B, NA} : parts {RA}"; 

570 
be respond.elim 1; 

571 
by (ALLGOALS Asm_full_simp_tac); 

572 
qed "newK2_respond_lemma"; 

573 

574 

575 
goal thy 

576 
"!!evs. [ (j,PB,RB) : respond (length evs); evs : recur lost ] \ 

577 
\ ==> ALL A A' N. A ~: lost & A' ~: lost > \ 

578 
\ Crypt (shrK A) {Key K, Agent A', N} : parts{RB} > \ 

579 
\ Key K ~: analz (insert RB (sees lost Spy evs))"; 

580 
be respond.induct 1; 

581 
by (forward_tac [respond_imp_responses] 2); 

582 
by (ALLGOALS 

583 
(asm_simp_tac 

584 
(!simpset addsimps 

585 
([analz_image_newK, not_parts_not_analz, 

586 
read_instantiate [("H", "?ff``?xx")] parts_insert, 

587 
Un_assoc RS sym, resp_analz_image_newK, 

588 
insert_Key_singleton, analz_insert_Key_newK]) 

589 
setloop split_tac [expand_if]))); 

590 
by (ALLGOALS (simp_tac (simpset_of "Message"))); 

591 
by (Fast_tac 1); 

592 
by (step_tac (!claset addSEs [MPair_parts]) 1); 

593 
(** LEVEL 6 **) 

594 
by (fast_tac (!claset addDs [resp_analz_insert, Key_in_parts_respond] 

595 
addSEs [new_keys_not_seen RS not_parts_not_analz 

596 
RSN(2,rev_notE)] 

597 
addss (!simpset)) 4); 

598 
by (fast_tac (!claset addSDs [newK2_respond_lemma]) 3); 

599 
by (best_tac (!claset addSEs partsEs 

600 
addDs [Key_in_parts_respond] 

601 
addss (!simpset)) 2); 

602 
by (thin_tac "ALL x.?P(x)" 1); 

603 
be respond.elim 1; 

604 
by (fast_tac (!claset addss (!simpset)) 1); 

605 
by (step_tac (!claset addss (!simpset)) 1); 

606 
by (best_tac (!claset addSEs partsEs 

607 
addDs [Key_in_parts_respond] 

608 
addss (!simpset)) 1); 

609 
qed_spec_mp "respond_Spy_not_see_encrypted_key"; 

610 

611 

612 
goal thy 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

613 
"!!evs. [ A ~: lost; A' ~: lost; evs : recur lost ] \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

614 
\ ==> Says Server B RB : set_of_list evs > \ 
2449  615 
\ Crypt (shrK A) {Key K, Agent A', N} : parts{RB} > \ 
616 
\ Key K ~: analz (sees lost Spy evs)"; 

617 
by (etac recur.induct 1); 

618 
by analz_Fake_tac; 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

619 
be ssubst 4; (*RA2: DELETE needless definition of PA!*) 
2449  620 
by (ALLGOALS 
621 
(asm_simp_tac 

622 
(!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK] 

623 
setloop split_tac [expand_if]))); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

624 
(*RA4*) 
2449  625 
by (spy_analz_tac 4); 
626 
(*Fake*) 

627 
by (spy_analz_tac 1); 

628 
by (step_tac (!claset delrules [impCE]) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

629 
(*RA2*) 
2449  630 
by (spy_analz_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

631 
(*RA3, case 2: K is an old key*) 
2449  632 
by (fast_tac (!claset addSDs [resp_analz_insert] 
633 
addSEs partsEs 

634 
addDs [Key_in_parts_respond] 

635 
addEs [Says_imp_old_keys RS less_irrefl]) 2); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

636 
(*RA3, case 1: use lemma previously proved by induction*) 
2449  637 
by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN 
638 
(2,rev_notE)]) 1); 

639 
bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp)); 

640 

641 

642 
goal thy 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

643 
"!!evs. [ Says Server B RB : set_of_list evs; \ 
2449  644 
\ Crypt (shrK A) {Key K, Agent A', N} : parts{RB}; \ 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

645 
\ C ~: {A,A',Server}; \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

646 
\ A ~: lost; A' ~: lost; evs : recur lost ] \ 
2449  647 
\ ==> Key K ~: analz (sees lost C evs)"; 
648 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 

649 
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); 

650 
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); 

651 
by (REPEAT_FIRST (fast_tac (!claset addIs [recur_mono RS subsetD]))); 

652 
qed "Agent_not_see_encrypted_key"; 

653 

654 

655 
(**** Authenticity properties for Agents ****) 

656 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

657 
(*NEEDED????????????????*) 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

658 
(*Only RA1 or RA2 can have caused such a part of a message to appear.*) 
2449  659 
goal thy 
660 
"!!evs. [ Hash {Key(shrK A), Agent A, Agent B, NA, P} \ 

661 
\ : parts (sees lost Spy evs); \ 

662 
\ A ~: lost; evs : recur lost ] \ 

663 
\ ==> Says A B {Hash{Key(shrK A), Agent A, Agent B, NA, P}, \ 

664 
\ Agent A, Agent B, NA, P} \ 

665 
\ : set_of_list evs"; 

666 
be rev_mp 1; 

667 
by (parts_induct_tac 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

668 
(*RA3*) 
2449  669 
by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 2); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

670 
(*RA2*) 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

671 
by ((REPEAT o CHANGED) (*Push in XAfor more simplification*) 
2449  672 
(res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1)); 
673 
by (best_tac (!claset addSEs partsEs 

674 
addDs [parts_cut] 

675 
addss (!simpset)) 1); 

676 
qed_spec_mp "Hash_auth_sender"; 

677 

678 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

679 
(*NEEDED????????????????*) 
2449  680 
goal thy "!!i. {Hash {Key (shrK Server), M}, M} : responses i ==> R"; 
681 
be setup_induction 1; 

682 
be responses.induct 1; 

683 
by (ALLGOALS Asm_simp_tac); 

684 
qed "responses_no_Hash_Server"; 

685 

686 

687 
val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE); 

688 

689 

690 
(** These two results should subsume (for all agents) the guarantees proved 

691 
separately for A and B in the OtwayRees protocol. 

692 
**) 

693 

694 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

695 
(*Encrypted messages can only originate with the Server.*) 
2449  696 
goal thy 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

697 
"!!evs. [ A ~: lost; A ~= Spy; evs : recur lost ] \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

698 
\ ==> Crypt (shrK A) Y : parts (sees lost Spy evs) \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

699 
\ > (EX C RC. Says Server C RC : set_of_list evs & \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

700 
\ Crypt (shrK A) Y : parts {RC})"; 
2449  701 
by (parts_induct_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

702 
(*RA4*) 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

703 
by (Fast_tac 4); 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

704 
(*RA3*) 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

705 
by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

706 
THEN Fast_tac 3); 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

707 
(*RA1*) 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

708 
by (Fast_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

709 
(*RA2: it cannot be a new Nonce, contradiction.*) 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

710 
by ((REPEAT o CHANGED) (*Push in XAfor more simplification*) 
2449  711 
(res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1)); 
712 
by (deepen_tac (!claset delrules [impCE] 

713 
addSIs [disjI2] 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

714 
addSEs [MPair_parts] 
2449  715 
addDs [parts_cut, parts.Body] 
716 
addss (!simpset)) 0 1); 

717 
qed_spec_mp "Crypt_imp_Server_msg"; 

718 

719 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

720 
(*Corollary: if A receives B's message then the key came from the Server*) 
2449  721 
goal thy 
722 
"!!evs. [ Says B' A RA : set_of_list evs; \ 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

723 
\ Crypt (shrK A) {Key K, Agent A', NA} : parts {RA}; \ 
2449  724 
\ A ~: lost; A ~= Spy; evs : recur lost ] \ 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

725 
\ ==> EX C RC. Says Server C RC : set_of_list evs & \ 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

726 
\ Crypt (shrK A) {Key K, Agent A', NA} : parts {RC}"; 
2449  727 
by (best_tac (!claset addSIs [Crypt_imp_Server_msg] 
728 
addDs [Says_imp_sees_Spy RS parts.Inj RSN (2,parts_cut)] 

729 
addss (!simpset)) 1); 

730 
qed "Agent_trust"; 

731 

732 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

733 
(*Overall guarantee: if A receives a certificant mentioning A' 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

734 
then the only other agent who knows the key is A'.*) 
2449  735 
goal thy 
736 
"!!evs. [ Says B' A RA : set_of_list evs; \ 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

737 
\ Crypt (shrK A) {Key K, Agent A', NA} : parts {RA}; \ 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

738 
\ C ~: {A,A',Server}; \ 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

739 
\ A ~: lost; A' ~: lost; A ~= Spy; evs : recur lost ] \ 
2449  740 
\ ==> Key K ~: analz (sees lost C evs)"; 
741 
by (dtac Agent_trust 1 THEN REPEAT_FIRST assume_tac); 

742 
by (fast_tac (!claset addSEs [Agent_not_see_encrypted_key RSN(2,rev_notE)]) 1); 

743 
qed "Agent_secrecy"; 

744 