author  paulson 
Fri, 04 Jul 1997 17:34:55 +0200  
changeset 3500  0d8ad2f192d8 
parent 3480  d59bbf053258 
child 3506  a36e0a49d2cd 
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 

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

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

3500  130 
\ (Hash{Nonce NB, certificate B (pubK B)})) : set evs"; 
3474  131 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
132 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2); 

133 
by possibility_tac; 

134 
result(); 

135 

136 

137 
(**** Inductive proofs about tls ****) 

138 

139 
(*Nobody sends themselves messages*) 

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

141 
by (etac tls.induct 1); 

142 
by (Auto_tac()); 

143 
qed_spec_mp "not_Says_to_self"; 

144 
Addsimps [not_Says_to_self]; 

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

146 

147 

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

149 
sends messages containing X! **) 

150 

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

152 
goal thy 

153 
"!!evs. evs : tls \ 

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

155 
by (etac tls.induct 1); 

156 
by (prove_simple_subgoals_tac 1); 

157 
by (Fake_parts_insert_tac 1); 

158 
qed "Spy_see_priK"; 

159 
Addsimps [Spy_see_priK]; 

160 

161 
goal thy 

162 
"!!evs. evs : tls \ 

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

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

165 
qed "Spy_analz_priK"; 

166 
Addsimps [Spy_analz_priK]; 

167 

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

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

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

171 
qed "Spy_see_priK_D"; 

172 

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

174 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

175 

176 

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

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

179 
\ evs : tls ] \ 

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

181 
by (etac rev_mp 1); 

182 
by (etac tls.induct 1); 

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

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

185 
addSEs partsEs) 1); 

186 
by (Fake_parts_insert_tac 1); 

187 
qed "Hash_imp_Nonce1"; 

188 

189 
(*Lemma needed to prove Hash_Hash_imp_Nonce*) 

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

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

192 
\ evs : tls ] \ 

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

194 
by (etac rev_mp 1); 

195 
by (etac tls.induct 1); 

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

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

198 
addSEs partsEs) 1); 

199 
by (Fake_parts_insert_tac 1); 

200 
qed "Hash_imp_Nonce2"; 

201 
AddSDs [Hash_imp_Nonce2]; 

202 

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

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

205 
\ evs : tls ] \ 

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

207 
by (etac rev_mp 1); 

208 
by (etac tls.induct 1); 

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

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

211 
addSEs partsEs) 1); 

212 
by (Fake_parts_insert_tac 1); 

213 
qed "Hash_Hash_imp_Nonce"; 

214 

215 

216 
(*NEEDED?? 

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

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

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

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

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

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

223 
by (etac rev_mp 1); 

224 
by (etac tls.induct 1); 

225 
by (ALLGOALS Asm_simp_tac); 

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

227 
addSEs partsEs) 1); 

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

229 
(*ServerFinished*) 

230 
by (Blast_tac 3); 

231 
(*ClientFinished*) 

232 
by (Blast_tac 2); 

233 
by (Fake_parts_insert_tac 1); 

234 
qed "Hash_imp_Nonce_seen"; 

235 

236 

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

238 

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] 
3474  243 
"!!evs. [ X = Crypt (priK A) \ 
244 
\ (Hash{Nonce NB, \ 

3500  245 
\ certificate B KB}); \ 
3474  246 
\ evs : tls; A ~: lost; B ~= Spy ] \ 
247 
\ ==> Says B A {Nonce NA, Nonce NB, Agent XB, \ 

3500  248 
\ certificate B KB} : set evs > \ 
3474  249 
\ 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

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

253 
by (Fake_parts_insert_tac 1); 

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

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

257 
qed_spec_mp "TrustCertVerify"; 

258 

259 

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

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

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

263 
breach of security.*) 

3500  264 
goalw thy [certificate_def] 
3474  265 
"!!evs. evs : tls \ 
3500  266 
\ ==> certificate B KB : parts (sees lost Spy evs) \ 
3474  267 
\ > KB = pubK B"; 
268 
by (etac tls.induct 1); 

269 
by (ALLGOALS Asm_simp_tac); 

270 
by (Fake_parts_insert_tac 2); 

271 
by (Blast_tac 1); 

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

273 

274 

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

276 
val ClientCertKeyEx_tac = 

277 
forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 

278 
parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB] 

279 
THEN' assume_tac 

280 
THEN' hyp_subst_tac; 

281 

282 
fun analz_induct_tac i = 

283 
etac tls.induct i THEN 

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

284 
ClientCertKeyEx_tac (i+5) THEN 
3474  285 
ALLGOALS (asm_simp_tac 
286 
(!simpset addsimps [not_parts_not_analz] 

287 
setloop split_tac [expand_if])) THEN 

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

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

290 
ALLGOALS (asm_simp_tac 

291 
(!simpset addsimps [insert_absorb] 

292 
setloop split_tac [expand_if])); 

293 

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

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

295 

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

296 
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

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

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

299 

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

300 
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

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

302 
qed "insert_Key_image"; 
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 
(*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

305 
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

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

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

308 
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

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

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

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

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

313 

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

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

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

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

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

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

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

320 
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

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

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

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

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

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

326 

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

327 

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

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

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

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

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

332 
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

333 
val lemma = result(); 
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 
(*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

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

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

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

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

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

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

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

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

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

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

346 
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

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

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

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

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

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

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

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

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

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

356 

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

357 

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

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

359 
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

360 
here.*) 
3500  361 
goalw thy [certificate_def] 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

362 
"!!evs. [ evs : tls; A~=Spy; B ~: lost ] \ 
3500  363 
\ ==> Says A B {certificate A (pubK A), \ 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

365 
\ Nonce M ~: analz (sees lost Spy evs)"; 
3474  366 
by (analz_induct_tac 1); 
367 
(*ClientHello*) 

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

368 
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

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

370 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2); 
3474  371 
(*Fake*) 
372 
by (spy_analz_tac 1); 

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

374 
by (REPEAT (blast_tac (!claset addSEs partsEs 

375 
addDs [impOfSubs analz_subset_parts, 

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

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

378 

379 

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

381 

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

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

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

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

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

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

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

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

390 
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

391 
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

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

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

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

395 
by (Blast_tac 1); 
3474  396 
qed "clientK_notin_parts"; 
397 

398 
goal thy 

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

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

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

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

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

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

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

405 
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

406 
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

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

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

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

410 
by (Blast_tac 1); 
3474  411 
qed "serverK_notin_parts"; 
412 

413 

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

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

416 
to compare XA with what she originally sent. 

417 
***) 

418 

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

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

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

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

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

425 
\ evs : tls; A~=Spy; B ~: lost ] \ 
3500  426 
\ ==> Says A B {certificate A (pubK A), \ 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

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

429 
by (hyp_subst_tac 1); 
3474  430 
by (etac tls.induct 1); 
431 
by (ALLGOALS Asm_simp_tac); 

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

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

433 
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

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

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

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

437 
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

438 
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

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

440 
not_parts_not_analz]) 2); 
3474  441 
by (Fake_parts_insert_tac 1); 
442 
qed_spec_mp "TrustServerFinished"; 

443 

444 

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

447 
B has no way of knowing that A is the sender of CERTIFICATE VERIFY 

448 
***) 

449 
goalw thy [certificate_def] 

3474  450 
"!!evs. [ X = Crypt (clientK(NA,NB,M)) \ 
451 
\ (Hash{Hash{Nonce NA, Nonce NB, Nonce M}, \ 

452 
\ Nonce NA, Agent XA, \ 

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

455 
\ evs : tls; A~=Spy; B ~: lost ] \ 
3500  456 
\ ==> Says A B {certificate A (pubK A), \ 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

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

459 
by (hyp_subst_tac 1); 
3474  460 
by (etac tls.induct 1); 
461 
by (ALLGOALS Asm_simp_tac); 

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

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

463 
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

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

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

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

467 
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

468 
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

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

470 
not_parts_not_analz]) 2); 
3474  471 
by (Fake_parts_insert_tac 1); 
472 
qed_spec_mp "TrustClientFinished"; 