author  paulson 
Tue, 01 Jul 1997 17:37:42 +0200  
changeset 3480  d59bbf053258 
parent 3474  44249bba00ec 
child 3500  0d8ad2f192d8 
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 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

8 
Client and invents M, then he sends contains M encrypted with B's public key. 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

9 
This message gives no evidence that the spy knows M, and yet the spy actually 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

10 
chose M! So, in any property concerning the secrecy of some item, one must 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

11 
establish that the spy didn't choose the item. Guarantees normally assume 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

12 
that the other party is uncompromised (otherwise, one can prove little). 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

13 

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

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

15 
* 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

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

17 

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

18 
* 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

19 
message is optional!) 
3474  20 

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

21 
* 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

22 

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

23 
* 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

24 
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

25 
rollback attacks). 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

26 

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

27 
A curious property found in these proofs is that CERTIFICATE VERIFY actually 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

28 
gives weaker authentication than CLIENT FINISHED. The theorem for CERTIFICATE 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

29 
VERIFY is subject to A~:lost, since if A's private key is known to the spy 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

30 
then he can forge A's signature. But the theorem for CLIENT FINISHED merely 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

31 
assumes that A is not the spy himself, since the model assumes that all other 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

32 
agents tell the truth. 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

33 

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

34 
In the real world, there are agents who are not active attackers, and yet 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

35 
still cannot be trusted to identify themselves. There may well be more such 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

36 
agents than there are compromised private keys. 
3474  37 
*) 
38 

39 
open TLS; 

40 

41 
proof_timing:=true; 

42 
HOL_quantifiers := false; 

43 

44 
AddIffs [Spy_in_lost, Server_not_lost]; 

45 

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

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

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

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

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

50 

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

53 

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

55 
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK, 

56 
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

57 

3474  58 

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

60 
val Says_imp_sees_Spy' = 

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

62 

63 

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

65 

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

67 
br notI 1; 

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

69 
by (Full_simp_tac 1); 

70 
qed "pubK_neq_clientK"; 

71 

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

73 
br notI 1; 

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

75 
by (Full_simp_tac 1); 

76 
qed "pubK_neq_serverK"; 

77 

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

79 
br notI 1; 

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

81 
by (Full_simp_tac 1); 

82 
qed "priK_neq_clientK"; 

83 

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

85 
br notI 1; 

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

87 
by (Full_simp_tac 1); 

88 
qed "priK_neq_serverK"; 

89 

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

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

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

92 
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

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

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

95 

3474  96 
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

97 
priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK]; 
3474  98 
AddIffs (ths @ (ths RL [not_sym])); 
99 

100 

101 
(**** Protocol Proofs ****) 

102 

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

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

105 

106 
(*Possibility property ending with ServerFinished.*) 

107 
goal thy 

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

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

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

111 
\ Nonce NA, Agent XA, Agent A, \ 

112 
\ Nonce NB, Agent XB, \ 

113 
\ Crypt (priK Server) {Agent B, Key (pubK B)}})) \ 

114 
\ : set evs"; 

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

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

117 
RS tls.ServerFinished) 2); 

118 
by possibility_tac; 

119 
result(); 

120 

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

122 
goal thy 

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

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

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

126 
\ Nonce NA, Agent XA, \ 

127 
\ Crypt (priK Server) {Agent A, Key (pubK A)}, \ 

128 
\ Nonce NB, Agent XB, Agent B})) : set evs"; 

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

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

131 
RS tls.ClientFinished) 2); 

132 
by possibility_tac; 

133 
result(); 

134 

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

136 
goal thy 

137 
"!!A B. A ~= B ==> EX NB. EX evs: tls. \ 

138 
\ Says A B (Crypt (priK A) \ 

139 
\ (Hash{Nonce NB, \ 

140 
\ Crypt (priK Server) \ 

141 
\ {Agent B, Key (pubK B)}})) : set evs"; 

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

143 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2); 

144 
by possibility_tac; 

145 
result(); 

146 

147 

148 
(**** Inductive proofs about tls ****) 

149 

150 
(*Nobody sends themselves messages*) 

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

152 
by (etac tls.induct 1); 

153 
by (Auto_tac()); 

154 
qed_spec_mp "not_Says_to_self"; 

155 
Addsimps [not_Says_to_self]; 

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

157 

158 

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

160 
sends messages containing X! **) 

161 

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

163 
goal thy 

164 
"!!evs. evs : tls \ 

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

166 
by (etac tls.induct 1); 

167 
by (prove_simple_subgoals_tac 1); 

168 
by (Fake_parts_insert_tac 1); 

169 
qed "Spy_see_priK"; 

170 
Addsimps [Spy_see_priK]; 

171 

172 
goal thy 

173 
"!!evs. evs : tls \ 

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

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

176 
qed "Spy_analz_priK"; 

177 
Addsimps [Spy_analz_priK]; 

178 

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

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

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

182 
qed "Spy_see_priK_D"; 

183 

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

185 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

186 

187 

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

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

190 
\ evs : tls ] \ 

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

192 
by (etac rev_mp 1); 

193 
by (etac tls.induct 1); 

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

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

196 
addSEs partsEs) 1); 

197 
by (Fake_parts_insert_tac 1); 

198 
qed "Hash_imp_Nonce1"; 

199 

200 
(*Lemma needed to prove Hash_Hash_imp_Nonce*) 

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

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

203 
\ evs : tls ] \ 

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

205 
by (etac rev_mp 1); 

206 
by (etac tls.induct 1); 

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

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

209 
addSEs partsEs) 1); 

210 
by (Fake_parts_insert_tac 1); 

211 
qed "Hash_imp_Nonce2"; 

212 
AddSDs [Hash_imp_Nonce2]; 

213 

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

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

216 
\ evs : tls ] \ 

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

218 
by (etac rev_mp 1); 

219 
by (etac tls.induct 1); 

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

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

222 
addSEs partsEs) 1); 

223 
by (Fake_parts_insert_tac 1); 

224 
qed "Hash_Hash_imp_Nonce"; 

225 

226 

227 
(*NEEDED?? 

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

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

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

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

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

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

234 
by (etac rev_mp 1); 

235 
by (etac tls.induct 1); 

236 
by (ALLGOALS Asm_simp_tac); 

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

238 
addSEs partsEs) 1); 

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

240 
(*ServerFinished*) 

241 
by (Blast_tac 3); 

242 
(*ClientFinished*) 

243 
by (Blast_tac 2); 

244 
by (Fake_parts_insert_tac 1); 

245 
qed "Hash_imp_Nonce_seen"; 

246 

247 

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

249 

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

251 
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

252 
assume A~:lost; otherwise, the Spy can forge A's signature.*) 
3474  253 
goal thy 
254 
"!!evs. [ X = Crypt (priK A) \ 

255 
\ (Hash{Nonce NB, \ 

256 
\ Crypt (priK Server) {Agent B, Key KB}}); \ 

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

258 
\ ==> Says B A {Nonce NA, Nonce NB, Agent XB, \ 

259 
\ Crypt (priK Server) {Agent B, Key KB}} : set evs > \ 

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

261 
by (hyp_subst_tac 1); 
3474  262 
by (etac tls.induct 1); 
263 
by (ALLGOALS Asm_simp_tac); 

264 
by (Fake_parts_insert_tac 1); 

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

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

268 
qed_spec_mp "TrustCertVerify"; 

269 

270 

271 
(*This lemma says that no false certificates exist. One might extend the 

272 
model to include bogus certificates for the lost agents, but there seems 

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

274 
breach of security.*) 

275 
goal thy 

276 
"!!evs. evs : tls \ 

277 
\ ==> Crypt (priK Server) {Agent B, Key KB} : parts (sees lost Spy evs) \ 

278 
\ > KB = pubK B"; 

279 
by (etac tls.induct 1); 

280 
by (ALLGOALS Asm_simp_tac); 

281 
by (Fake_parts_insert_tac 2); 

282 
by (Blast_tac 1); 

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

284 

285 

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

287 
val ClientCertKeyEx_tac = 

288 
forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 

289 
parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB] 

290 
THEN' assume_tac 

291 
THEN' hyp_subst_tac; 

292 

293 
fun analz_induct_tac i = 

294 
etac tls.induct i THEN 

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

295 
ClientCertKeyEx_tac (i+5) THEN 
3474  296 
ALLGOALS (asm_simp_tac 
297 
(!simpset addsimps [not_parts_not_analz] 

298 
setloop split_tac [expand_if])) THEN 

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

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

301 
ALLGOALS (asm_simp_tac 

302 
(!simpset addsimps [insert_absorb] 

303 
setloop split_tac [expand_if])); 

304 

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

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

306 

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

307 
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

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

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

310 

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

311 
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

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

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

314 

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

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

316 
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

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

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

319 
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

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

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

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

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

324 

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

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

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

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

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

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

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

331 
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

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

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

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

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

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

337 

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

338 

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

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

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

341 
"!!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

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

343 
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

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

345 

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

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

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

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

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

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

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

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

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

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

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

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

357 
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

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

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

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

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

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

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

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

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

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

367 

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

368 

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

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

370 
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

371 
here.*) 
3474  372 
goal thy 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

373 
"!!evs. [ evs : tls; A~=Spy; B ~: lost ] \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

374 
\ ==> Says A B {Crypt (priK Server) {Agent A, Key (pubK A)}, \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

375 
\ Crypt KB (Nonce M)} : set evs > \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

376 
\ Nonce M ~: analz (sees lost Spy evs)"; 
3474  377 
by (analz_induct_tac 1); 
378 
(*ClientHello*) 

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

379 
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

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

381 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2); 
3474  382 
(*Fake*) 
383 
by (spy_analz_tac 1); 

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

385 
by (REPEAT (blast_tac (!claset addSEs partsEs 

386 
addDs [impOfSubs analz_subset_parts, 

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

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

389 

390 

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

392 

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

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

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

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

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

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

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

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

401 
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

402 
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

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

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

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

406 
by (Blast_tac 1); 
3474  407 
qed "clientK_notin_parts"; 
408 

409 
goal thy 

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

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

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

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

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

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

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

416 
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

417 
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

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

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

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

421 
by (Blast_tac 1); 
3474  422 
qed "serverK_notin_parts"; 
423 

424 

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

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

427 
to compare XA with what she originally sent. 

428 
***) 

429 

430 
goal thy 

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

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

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

433 
\ Nonce NA, Agent XA, Agent A, \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

434 
\ Nonce NB, Agent XB, \ 
3474  435 
\ Crypt (priK Server) {Agent B, Key (pubK B)}}); \ 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

436 
\ evs : tls; A~=Spy; B ~: lost ] \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

437 
\ ==> Says A B {Crypt (priK Server) {Agent A, Key (pubK A)}, \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

438 
\ Crypt KB (Nonce M)} : set evs > \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

440 
by (hyp_subst_tac 1); 
3474  441 
by (etac tls.induct 1); 
442 
by (ALLGOALS Asm_simp_tac); 

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

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

444 
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

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

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

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

448 
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

449 
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

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

451 
not_parts_not_analz]) 2); 
3474  452 
by (Fake_parts_insert_tac 1); 
453 
qed_spec_mp "TrustServerFinished"; 

454 

455 

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

456 
(*** Protocol goal: if B receives CLIENT FINISHED, then A is present 
3474  457 
and has used the quoted values XA, XB, etc. Note that it is up to B 
458 
to compare XB with what he originally sent. ***) 

459 

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

460 
(*This result seems too strong: A need not have sent CERTIFICATE VERIFY. 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

461 
But we assume (as always) that the other party is honest...*) 
3474  462 
goal thy 
463 
"!!evs. [ X = Crypt (clientK(NA,NB,M)) \ 

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

465 
\ Nonce NA, Agent XA, \ 

466 
\ Crypt (priK Server) {Agent A, Key (pubK A)}, \ 

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

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

468 
\ evs : tls; A~=Spy; B ~: lost ] \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

469 
\ ==> Says A B {Crypt (priK Server) {Agent A, Key (pubK A)}, \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

470 
\ Crypt KB (Nonce M)} : set evs > \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

472 
by (hyp_subst_tac 1); 
3474  473 
by (etac tls.induct 1); 
474 
by (ALLGOALS Asm_simp_tac); 

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

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

476 
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

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

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

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

480 
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

481 
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

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

483 
not_parts_not_analz]) 2); 
3474  484 
by (Fake_parts_insert_tac 1); 
485 
qed_spec_mp "TrustClientFinished"; 