author  paulson 
Mon, 07 Jul 1997 10:49:14 +0200  
changeset 3506  a36e0a49d2cd 
parent 3500  0d8ad2f192d8 
child 3515  d8a71f6eaf40 
permissions  rwrr 
3474  1 
(* Title: HOL/Auth/TLS 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

6 
The publickey model has a weakness, especially concerning anonymous sessions. 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

7 
The Spy's state is recorded as the trace of message. But if he himself is the 
3500  8 
Client and invents M, then he encrypts M with B's public key before sending 
9 
it. This message gives no evidence that the spy knows M, and yet the spy 

10 
actually chose M! So, in any property concerning the secrecy of some item, 

11 
one must establish that the spy didn't choose the item. Guarantees normally 

12 
assume that the other party is uncompromised (otherwise, one can prove 

13 
little). 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

14 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

15 
Protocol goals: 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

16 
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

17 
parties (though A is not necessarily authenticated). 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

18 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

19 
* B upon receiving CERTIFICATE VERIFY knows that A is present (But this 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

20 
message is optional!) 
3474  21 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

22 
* A upon receiving SERVER FINISHED knows that B is present 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

23 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

24 
* Each party who has received a FINISHED message can trust that the other 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

25 
party agrees on all message components, including XA and XB (thus foiling 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

26 
rollback attacks). 
3474  27 
*) 
28 

29 
open TLS; 

30 

31 
proof_timing:=true; 

32 
HOL_quantifiers := false; 

33 

34 
AddIffs [Spy_in_lost, Server_not_lost]; 

3500  35 
Addsimps [certificate_def]; 
3474  36 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

37 
goal thy "!!A. A ~: lost ==> A ~= Spy"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

38 
by (Blast_tac 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

39 
qed "not_lost_not_eq_Spy"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

40 
Addsimps [not_lost_not_eq_Spy]; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

41 

3474  42 
(*Injectiveness of keygenerating functions*) 
43 
AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq]; 

44 

45 
(* invKey(clientK x) = clientK x and similarly for serverK*) 

46 
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK, 

47 
isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK]; 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

48 

3474  49 

50 
(*Replacing the variable by a constant improves search speed by 50%!*) 

51 
val Says_imp_sees_Spy' = 

52 
read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; 

53 

54 

55 
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***) 

56 

57 
goal thy "pubK A ~= clientK arg"; 

58 
br notI 1; 

59 
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); 

60 
by (Full_simp_tac 1); 

61 
qed "pubK_neq_clientK"; 

62 

63 
goal thy "pubK A ~= serverK arg"; 

64 
br notI 1; 

65 
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); 

66 
by (Full_simp_tac 1); 

67 
qed "pubK_neq_serverK"; 

68 

69 
goal thy "priK A ~= clientK arg"; 

70 
br notI 1; 

71 
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); 

72 
by (Full_simp_tac 1); 

73 
qed "priK_neq_clientK"; 

74 

75 
goal thy "priK A ~= serverK arg"; 

76 
br notI 1; 

77 
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); 

78 
by (Full_simp_tac 1); 

79 
qed "priK_neq_serverK"; 

80 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

81 
(*clientK and serverK have disjoint ranges*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

82 
goal thy "clientK arg ~= serverK arg'"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

83 
by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

84 
by (Blast_tac 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

85 
qed "clientK_neq_serverK"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

86 

3474  87 
val ths = [pubK_neq_clientK, pubK_neq_serverK, 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

88 
priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK]; 
3474  89 
AddIffs (ths @ (ths RL [not_sym])); 
90 

91 

92 
(**** Protocol Proofs ****) 

93 

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

95 
This protocol has three end points and six messages to consider.*) 

96 

97 
(*Possibility property ending with ServerFinished.*) 

98 
goal thy 

99 
"!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \ 

100 
\ Says B A (Crypt (serverK(NA,NB,M)) \ 

101 
\ (Hash{Hash{Nonce NA, Nonce NB, Nonce M}, \ 

102 
\ Nonce NA, Agent XA, Agent A, \ 

103 
\ Nonce NB, Agent XB, \ 

3500  104 
\ certificate B (pubK B)})) \ 
3474  105 
\ : set evs"; 
106 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

107 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx 

108 
RS tls.ServerFinished) 2); 

109 
by possibility_tac; 

110 
result(); 

111 

112 
(*And one for ClientFinished. Either FINISHED message may come first.*) 

113 
goal thy 

114 
"!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \ 

115 
\ Says A B (Crypt (clientK(NA,NB,M)) \ 

116 
\ (Hash{Hash{Nonce NA, Nonce NB, Nonce M}, \ 

117 
\ Nonce NA, Agent XA, \ 

3500  118 
\ certificate A (pubK A), \ 
3474  119 
\ Nonce NB, Agent XB, Agent B})) : set evs"; 
120 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

121 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx 

122 
RS tls.ClientFinished) 2); 

123 
by possibility_tac; 

124 
result(); 

125 

126 
(*Another one, for CertVerify (which is optional)*) 

127 
goal thy 

3506  128 
"!!A B. A ~= B ==> EX NB M. EX evs: tls. \ 
3474  129 
\ Says A B (Crypt (priK A) \ 
3506  130 
\ (Hash{Nonce NB, certificate B (pubK B), Nonce M})) : set evs"; 
3474  131 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
3506  132 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx 
133 
RS tls.CertVerify) 2); 

3474  134 
by possibility_tac; 
135 
result(); 

136 

137 

138 
(**** Inductive proofs about tls ****) 

139 

140 
(*Nobody sends themselves messages*) 

141 
goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs"; 

142 
by (etac tls.induct 1); 

143 
by (Auto_tac()); 

144 
qed_spec_mp "not_Says_to_self"; 

145 
Addsimps [not_Says_to_self]; 

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

147 

148 

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

150 
sends messages containing X! **) 

151 

152 
(*Spy never sees another agent's private key! (unless it's lost at start)*) 

153 
goal thy 

154 
"!!evs. evs : tls \ 

155 
\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; 

156 
by (etac tls.induct 1); 

157 
by (prove_simple_subgoals_tac 1); 

158 
by (Fake_parts_insert_tac 1); 

159 
qed "Spy_see_priK"; 

160 
Addsimps [Spy_see_priK]; 

161 

162 
goal thy 

163 
"!!evs. evs : tls \ 

164 
\ ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)"; 

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

166 
qed "Spy_analz_priK"; 

167 
Addsimps [Spy_analz_priK]; 

168 

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

170 
\ evs : tls ] ==> A:lost"; 

171 
by (blast_tac (!claset addDs [Spy_see_priK]) 1); 

172 
qed "Spy_see_priK_D"; 

173 

174 
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); 

175 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

176 

177 

178 
(*Every Nonce that's hashed is already in past traffic. *) 

179 
goal thy "!!evs. [ Hash {Nonce N, X} : parts (sees lost Spy evs); \ 

180 
\ evs : tls ] \ 

181 
\ ==> Nonce N : parts (sees lost Spy evs)"; 

182 
by (etac rev_mp 1); 

183 
by (etac tls.induct 1); 

184 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); 

185 
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 

186 
addSEs partsEs) 1); 

187 
by (Fake_parts_insert_tac 1); 

188 
qed "Hash_imp_Nonce1"; 

189 

190 
(*Lemma needed to prove Hash_Hash_imp_Nonce*) 

191 
goal thy "!!evs. [ Hash{Nonce NA, Nonce NB, Nonce M} \ 

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

193 
\ evs : tls ] \ 

194 
\ ==> Nonce M : parts (sees lost Spy evs)"; 

195 
by (etac rev_mp 1); 

196 
by (etac tls.induct 1); 

197 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); 

198 
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 

199 
addSEs partsEs) 1); 

200 
by (Fake_parts_insert_tac 1); 

201 
qed "Hash_imp_Nonce2"; 

202 
AddSDs [Hash_imp_Nonce2]; 

203 

204 
goal thy "!!evs. [ Hash { Hash{Nonce NA, Nonce NB, Nonce M}, X } \ 

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

206 
\ evs : tls ] \ 

207 
\ ==> Nonce M : parts (sees lost Spy evs)"; 

208 
by (etac rev_mp 1); 

209 
by (etac tls.induct 1); 

210 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); 

211 
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 

212 
addSEs partsEs) 1); 

213 
by (Fake_parts_insert_tac 1); 

214 
qed "Hash_Hash_imp_Nonce"; 

215 

216 

217 
(*NEEDED?? 

218 
Every Nonce that's hashed is already in past traffic. 

219 
This general formulation is tricky to prove and hard to use, since the 

220 
2nd premise is typically proved by simplification.*) 

221 
goal thy "!!evs. [ Hash X : parts (sees lost Spy evs); \ 

222 
\ Nonce N : parts {X}; evs : tls ] \ 

223 
\ ==> Nonce N : parts (sees lost Spy evs)"; 

224 
by (etac rev_mp 1); 

225 
by (etac tls.induct 1); 

226 
by (ALLGOALS Asm_simp_tac); 

227 
by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 

228 
addSEs partsEs) 1); 

229 
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees]))); 

230 
by (Fake_parts_insert_tac 1); 

3506  231 
(*CertVerify, ClientFinished, ServerFinished (?)*) 
232 
by (REPEAT (Blast_tac 1)); 

3474  233 
qed "Hash_imp_Nonce_seen"; 
234 

235 

236 
(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***) 

237 

3506  238 
(*B can check A's signature if he has received A's certificate. 
239 
Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

240 
message is Fake. We don't need guarantees for the Spy anyway. We must 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

241 
assume A~:lost; otherwise, the Spy can forge A's signature.*) 
3500  242 
goalw thy [certificate_def] 
3506  243 
"!!evs. [ X = Crypt (priK A) \ 
244 
\ (Hash{Nonce NB, certificate B KB, Nonce M}); \ 

245 
\ evs : tls; A ~: lost; B ~= Spy ] \ 

246 
\ ==> Says B A {Nonce NA, Nonce NB, Agent XB, certificate B KB} \ 

247 
\ : set evs > \ 

3474  248 
\ X : parts (sees lost Spy evs) > Says A B X : set evs"; 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

249 
by (hyp_subst_tac 1); 
3474  250 
by (etac tls.induct 1); 
251 
by (ALLGOALS Asm_simp_tac); 

252 
by (Fake_parts_insert_tac 1); 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

253 
(*ServerHello: nonce NB cannot be in X because it's fresh!*) 
3474  254 
by (blast_tac (!claset addSDs [Hash_imp_Nonce1] 
255 
addSEs sees_Spy_partsEs) 1); 

256 
qed_spec_mp "TrustCertVerify"; 

257 

258 

3506  259 
goal thy 
260 
"!!evs. [ evs : tls; A ~= Spy ] \ 

261 
\ ==> Says A B (Crypt (priK A) \ 

262 
\ (Hash{Nonce NB, certificate B KB, Nonce M})) : set evs \ 

263 
\ > Says A B {certificate A (pubK A), Crypt KB (Nonce M)} : set evs"; 

264 
by (etac tls.induct 1); 

265 
by (ALLGOALS Asm_full_simp_tac); 

266 
bind_thm ("UseCertVerify", result() RSN (2, rev_mp)); 

267 

268 

3474  269 
(*This lemma says that no false certificates exist. One might extend the 
270 
model to include bogus certificates for the lost agents, but there seems 

271 
little point in doing so: the loss of their private keys is a worse 

272 
breach of security.*) 

3500  273 
goalw thy [certificate_def] 
3474  274 
"!!evs. evs : tls \ 
3506  275 
\ ==> certificate B KB : parts (sees lost Spy evs) > KB = pubK B"; 
3474  276 
by (etac tls.induct 1); 
277 
by (ALLGOALS Asm_simp_tac); 

278 
by (Fake_parts_insert_tac 2); 

279 
by (Blast_tac 1); 

280 
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp)); 

281 

282 

283 
(*Replace key KB in ClientCertKeyEx by (pubK B) *) 

284 
val ClientCertKeyEx_tac = 

285 
forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 

286 
parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB] 

287 
THEN' assume_tac 

288 
THEN' hyp_subst_tac; 

289 

290 
fun analz_induct_tac i = 

291 
etac tls.induct i THEN 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

292 
ClientCertKeyEx_tac (i+5) THEN 
3474  293 
ALLGOALS (asm_simp_tac 
294 
(!simpset addsimps [not_parts_not_analz] 

295 
setloop split_tac [expand_if])) THEN 

296 
(*Remove instances of pubK B: the Spy already knows all public keys. 

297 
Combining the two simplifier calls makes them run extremely slowly.*) 

298 
ALLGOALS (asm_simp_tac 

299 
(!simpset addsimps [insert_absorb] 

300 
setloop split_tac [expand_if])); 

301 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

302 
(*** Specialized rewriting for the analz_image_... theorems ***) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

303 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

304 
goal thy "insert (Key K) H = Key `` {K} Un H"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

305 
by (Blast_tac 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

306 
qed "insert_Key_singleton"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

307 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

308 
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

309 
by (Blast_tac 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

310 
qed "insert_Key_image"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

311 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

312 
(*Reverse the normal simplification of "image" to build up (not break down) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

313 
the set of keys. Based on analz_image_freshK_ss, but simpler.*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

314 
val analz_image_keys_ss = 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

315 
!simpset delsimps [image_insert, image_Un] 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

316 
addsimps [image_insert RS sym, image_Un RS sym, 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

317 
rangeI, 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

318 
insert_Key_singleton, 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

319 
insert_Key_image, Un_assoc RS sym] 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

320 
setloop split_tac [expand_if]; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

321 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

322 
(*No collection of keys can help the spy get new private keys*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

323 
goal thy 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

324 
"!!evs. evs : tls ==> \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

325 
\ ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) = \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

326 
\ (priK B : KK  B : lost)"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

327 
by (etac tls.induct 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

328 
by (ALLGOALS (asm_simp_tac analz_image_keys_ss)); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

329 
(*Fake*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

330 
by (spy_analz_tac 2); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

331 
(*Base*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

332 
by (Blast_tac 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

333 
qed_spec_mp "analz_image_priK"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

334 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

335 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

336 
(*Lemma for the trivial direction of the ifandonlyif*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

337 
goal thy 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

338 
"!!evs. (X : analz (G Un H)) > (X : analz H) ==> \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

339 
\ (X : analz (G Un H)) = (X : analz H)"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

340 
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

341 
val lemma = result(); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

342 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

343 
(*Knowing some clientKs and serverKs is no help in getting new nonces*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

344 
goal thy 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

345 
"!!evs. evs : tls ==> \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

346 
\ ALL KK. KK <= (range clientK Un range serverK) > \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

347 
\ (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

348 
\ (Nonce N : analz (sees lost Spy evs))"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

349 
by (etac tls.induct 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

350 
by (ClientCertKeyEx_tac 6); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

351 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

352 
by (REPEAT_FIRST (rtac lemma )); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

353 
(*SLOW: 30s!*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

354 
by (ALLGOALS (asm_simp_tac analz_image_keys_ss)); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

355 
by (ALLGOALS (asm_simp_tac 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

356 
(!simpset addsimps [analz_image_priK, insert_absorb]))); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

357 
(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

358 
by (Blast_tac 3); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

359 
(*Fake*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

360 
by (spy_analz_tac 2); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

361 
(*Base*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

362 
by (Blast_tac 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

363 
qed_spec_mp "analz_image_keys"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

364 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

365 

d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

366 
(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret. 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

367 
The assumption is A~=Spy, not A~:lost, since A doesn't use her private key 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

368 
here.*) 
3500  369 
goalw thy [certificate_def] 
3506  370 
"!!evs. [ evs : tls; A~=Spy; B ~: lost ] \ 
371 
\ ==> Says A B {certificate A (pubK A), Crypt KB (Nonce M)} \ 

372 
\ : set evs > Nonce M ~: analz (sees lost Spy evs)"; 

3474  373 
by (analz_induct_tac 1); 
374 
(*ClientHello*) 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

375 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

376 
(*SpyKeys*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

377 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2); 
3474  378 
(*Fake*) 
379 
by (spy_analz_tac 1); 

380 
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*) 

381 
by (REPEAT (blast_tac (!claset addSEs partsEs 

382 
addDs [impOfSubs analz_subset_parts, 

383 
Says_imp_sees_Spy' RS analz.Inj]) 1)); 

384 
bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp)); 

385 

386 

387 
(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***) 

388 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

389 
(*The two proofs are identical*) 
3474  390 
goal thy 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

391 
"!!evs. [ Nonce M ~: analz (sees lost Spy evs); \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

392 
\ evs : tls ] \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

393 
\ ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

394 
by (etac rev_mp 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

395 
by (analz_induct_tac 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

396 
(*SpyKeys*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

397 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

398 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

399 
(*Fake*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

400 
by (spy_analz_tac 2); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

401 
(*Base*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

402 
by (Blast_tac 1); 
3474  403 
qed "clientK_notin_parts"; 
404 

405 
goal thy 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

406 
"!!evs. [ Nonce M ~: analz (sees lost Spy evs); \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

407 
\ evs : tls ] \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

408 
\ ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

409 
by (etac rev_mp 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

410 
by (analz_induct_tac 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

411 
(*SpyKeys*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

412 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

413 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

414 
(*Fake*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

415 
by (spy_analz_tac 2); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

416 
(*Base*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

417 
by (Blast_tac 1); 
3474  418 
qed "serverK_notin_parts"; 
419 

420 

421 
(*** Protocol goals: if A receives SERVER FINISHED, then B is present 

422 
and has used the quoted values XA, XB, etc. Note that it is up to A 

423 
to compare XA with what she originally sent. 

424 
***) 

425 

3500  426 
goalw thy [certificate_def] 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

427 
"!!evs. [ X = Crypt (serverK(NA,NB,M)) \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

428 
\ (Hash{Hash{Nonce NA, Nonce NB, Nonce M}, \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

429 
\ Nonce NA, Agent XA, Agent A, \ 
3506  430 
\ Nonce NB, Agent XB, certificate B (pubK B)}); \ 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

431 
\ evs : tls; A~=Spy; B ~: lost ] \ 
3506  432 
\ ==> Says A B {certificate A (pubK A), Crypt KB (Nonce M)} \ 
433 
\ : set evs > \ 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

434 
\ X : parts (sees lost Spy evs) > Says B A X : set evs"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

435 
by (hyp_subst_tac 1); 
3474  436 
by (etac tls.induct 1); 
437 
by (ALLGOALS Asm_simp_tac); 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

438 
(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

439 
by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce] 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

440 
addSEs sees_Spy_partsEs) 2); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

441 
(*Fake: the Spy doesn't have the critical session key!*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

442 
by (REPEAT (rtac impI 1)); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

443 
by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

444 
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

445 
serverK_notin_parts, 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

446 
not_parts_not_analz]) 2); 
3474  447 
by (Fake_parts_insert_tac 1); 
448 
qed_spec_mp "TrustServerFinished"; 

449 

450 

3500  451 
(*** Protocol goal: if B receives CLIENT FINISHED, then A has used the 
452 
quoted values XA, XB, etc., which B can then check. BUT NOTE: 

3506  453 
B has no way of knowing that A is the sender of CLIENT CERTIFICATE! 
454 
***) 

3500  455 
goalw thy [certificate_def] 
3474  456 
"!!evs. [ X = Crypt (clientK(NA,NB,M)) \ 
457 
\ (Hash{Hash{Nonce NA, Nonce NB, Nonce M}, \ 

458 
\ Nonce NA, Agent XA, \ 

3500  459 
\ certificate A (pubK A), \ 
3474  460 
\ Nonce NB, Agent XB, Agent B}); \ 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

461 
\ evs : tls; A~=Spy; B ~: lost ] \ 
3500  462 
\ ==> Says A B {certificate A (pubK A), \ 
3506  463 
\ Crypt KB (Nonce M)} : set evs > \ 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

464 
\ X : parts (sees lost Spy evs) > Says A B X : set evs"; 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

465 
by (hyp_subst_tac 1); 
3474  466 
by (etac tls.induct 1); 
467 
by (ALLGOALS Asm_simp_tac); 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

468 
(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

469 
by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce] 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

470 
addSEs sees_Spy_partsEs) 2); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

471 
(*Fake: the Spy doesn't have the critical session key!*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

472 
by (REPEAT (rtac impI 1)); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

473 
by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1); 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

474 
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

475 
clientK_notin_parts, 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

476 
not_parts_not_analz]) 2); 
3474  477 
by (Fake_parts_insert_tac 1); 
478 
qed_spec_mp "TrustClientFinished"; 

3506  479 

480 

481 
(*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to 

482 
check a CERTIFICATE VERIFY from A, then A has used the quoted 

483 
values XA, XB, etc. Even this one requires A to be uncompromised. 

484 
***) 

485 
goal thy 

486 
"!!evs. [ X = Crypt (clientK(NA,NB,M)) \ 

487 
\ (Hash{Hash{Nonce NA, Nonce NB, Nonce M}, \ 

488 
\ Nonce NA, Agent XA, \ 

489 
\ certificate A (pubK A), \ 

490 
\ Nonce NB, Agent XB, Agent B}); \ 

491 
\ Says A' B X : set evs; \ 

492 
\ Says B A {Nonce NA, Nonce NB, Agent XB, certificate B KB} \ 

493 
\ : set evs; \ 

494 
\ Says A'' B (Crypt (priK A) \ 

495 
\ (Hash{Nonce NB, certificate B KB, Nonce M})) \ 

496 
\ : set evs; \ 

497 
\ evs : tls; A ~: lost; B ~: lost ] \ 

498 
\ ==> Says A B X : set evs"; 

499 
br TrustClientFinished 1; 

500 
br (TrustCertVerify RS UseCertVerify) 5; 

501 
by (REPEAT_FIRST (ares_tac [refl])); 

502 
by (ALLGOALS 

503 
(asm_full_simp_tac (!simpset addsimps [Says_imp_sees_Spy RS parts.Inj]))); 

504 
qed_spec_mp "AuthClientFinished"; 