author  paulson 
Fri, 11 Jul 1997 13:30:01 +0200  
changeset 3515  d8a71f6eaf40 
parent 3506  a36e0a49d2cd 
child 3519  ab0a9fbed4c0 
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 

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

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

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

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

9 

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

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

11 
message is optional!) 
3474  12 

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

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

14 

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

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

16 
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

17 
rollback attacks). 
3474  18 
*) 
19 

20 
open TLS; 

21 

22 
proof_timing:=true; 

23 
HOL_quantifiers := false; 

24 

25 
AddIffs [Spy_in_lost, Server_not_lost]; 

3500  26 
Addsimps [certificate_def]; 
3474  27 

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

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

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

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

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

32 

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

35 

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

37 
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK, 

38 
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

39 

3474  40 

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

42 
val Says_imp_sees_Spy' = 

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

44 

45 

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

47 

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

49 
br notI 1; 

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

51 
by (Full_simp_tac 1); 

52 
qed "pubK_neq_clientK"; 

53 

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

55 
br notI 1; 

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

57 
by (Full_simp_tac 1); 

58 
qed "pubK_neq_serverK"; 

59 

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

61 
br notI 1; 

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

63 
by (Full_simp_tac 1); 

64 
qed "priK_neq_clientK"; 

65 

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

67 
br notI 1; 

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

69 
by (Full_simp_tac 1); 

70 
qed "priK_neq_serverK"; 

71 

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

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

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

74 
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

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

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

77 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

78 
val keys_distinct = [pubK_neq_clientK, pubK_neq_serverK, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

79 
priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK]; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

80 
AddIffs (keys_distinct @ (keys_distinct RL [not_sym])); 
3474  81 

82 

83 
(**** Protocol Proofs ****) 

84 

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

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

87 

88 
(*Possibility property ending with ServerFinished.*) 

89 
goal thy 

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

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

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

93 
\ Nonce NA, Agent XA, Agent A, \ 

94 
\ Nonce NB, Agent XB, \ 

3500  95 
\ certificate B (pubK B)})) \ 
3474  96 
\ : set evs"; 
97 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

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

99 
RS tls.ServerFinished) 2); 

100 
by possibility_tac; 

101 
result(); 

102 

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

104 
goal thy 

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

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

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

108 
\ Nonce NA, Agent XA, \ 

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

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

113 
RS tls.ClientFinished) 2); 

114 
by possibility_tac; 

115 
result(); 

116 

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

118 
goal thy 

3506  119 
"!!A B. A ~= B ==> EX NB M. EX evs: tls. \ 
3474  120 
\ Says A B (Crypt (priK A) \ 
3506  121 
\ (Hash{Nonce NB, certificate B (pubK B), Nonce M})) : set evs"; 
3474  122 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
3506  123 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx 
124 
RS tls.CertVerify) 2); 

3474  125 
by possibility_tac; 
126 
result(); 

127 

128 

129 
(**** Inductive proofs about tls ****) 

130 

131 
(*Nobody sends themselves messages*) 

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

133 
by (etac tls.induct 1); 

134 
by (Auto_tac()); 

135 
qed_spec_mp "not_Says_to_self"; 

136 
Addsimps [not_Says_to_self]; 

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

138 

139 

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

141 
sends messages containing X! **) 

142 

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

144 
goal thy 

145 
"!!evs. evs : tls \ 

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

147 
by (etac tls.induct 1); 

148 
by (prove_simple_subgoals_tac 1); 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

149 
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 2); 
3474  150 
by (Fake_parts_insert_tac 1); 
151 
qed "Spy_see_priK"; 

152 
Addsimps [Spy_see_priK]; 

153 

154 
goal thy 

155 
"!!evs. evs : tls \ 

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

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

158 
qed "Spy_analz_priK"; 

159 
Addsimps [Spy_analz_priK]; 

160 

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

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

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

164 
qed "Spy_see_priK_D"; 

165 

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

167 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

168 

169 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

170 
(*This lemma says that no false certificates exist. One might extend the 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

171 
model to include bogus certificates for the lost agents, but there seems 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

172 
little point in doing so: the loss of their private keys is a worse 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

173 
breach of security.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

174 
goalw thy [certificate_def] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

175 
"!!evs. evs : tls \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

176 
\ ==> certificate B KB : parts (sees lost Spy evs) > KB = pubK B"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

177 
by (etac tls.induct 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

178 
by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]))); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

179 
by (Fake_parts_insert_tac 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

180 
by (Blast_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

181 
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp)); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

182 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

183 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

184 
(*Replace key KB in ClientCertKeyEx by (pubK B) *) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

185 
val ClientCertKeyEx_tac = 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

186 
forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

187 
parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

188 
THEN' assume_tac 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

189 
THEN' hyp_subst_tac; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

190 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

191 
fun analz_induct_tac i = 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

192 
etac tls.induct i THEN 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

193 
ClientCertKeyEx_tac (i+7) THEN (*ClientFinished*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

194 
ClientCertKeyEx_tac (i+6) THEN (*CertVerify*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

195 
ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

196 
rewrite_goals_tac [certificate_def] THEN 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

197 
ALLGOALS (asm_simp_tac 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

198 
(!simpset addsimps [not_parts_not_analz] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

199 
setloop split_tac [expand_if])) THEN 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

200 
(*Remove instances of pubK B: the Spy already knows all public keys. 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

201 
Combining the two simplifier calls makes them run extremely slowly.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

202 
ALLGOALS (asm_simp_tac 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

203 
(!simpset addsimps [insert_absorb] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

204 
setloop split_tac [expand_if])); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

205 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

206 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

207 
(*** Hashing of nonces ***) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

208 

3474  209 
(*Every Nonce that's hashed is already in past traffic. *) 
210 
goal thy "!!evs. [ Hash {Nonce N, X} : parts (sees lost Spy evs); \ 

211 
\ evs : tls ] \ 

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

213 
by (etac rev_mp 1); 

214 
by (etac tls.induct 1); 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

215 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

216 
setloop split_tac [expand_if]))); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

217 
by (Fake_parts_insert_tac 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

218 
by (REPEAT (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

219 
addSEs partsEs) 1)); 
3474  220 
qed "Hash_imp_Nonce1"; 
221 

222 
(*Lemma needed to prove Hash_Hash_imp_Nonce*) 

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

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

225 
\ evs : tls ] \ 

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

227 
by (etac rev_mp 1); 

228 
by (etac tls.induct 1); 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

229 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

230 
setloop split_tac [expand_if]))); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

231 
by (Fake_parts_insert_tac 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

232 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

233 
addSEs partsEs) 1); 
3474  234 
qed "Hash_imp_Nonce2"; 
235 
AddSDs [Hash_imp_Nonce2]; 

236 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

237 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

238 
goal thy "!!evs. [ Notes A {Agent B, X} : set evs; evs : tls ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

239 
\ ==> Crypt (pubK B) X : parts (sees lost Spy evs)"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

240 
by (etac rev_mp 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

241 
by (analz_induct_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

242 
by (blast_tac (!claset addIs [parts_insertI]) 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

243 
qed "Notes_Crypt_parts_sees"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

244 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

245 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

246 
(*NEEDED??*) 
3474  247 
goal thy "!!evs. [ Hash { Hash{Nonce NA, Nonce NB, Nonce M}, X } \ 
248 
\ : parts (sees lost Spy evs); \ 

249 
\ evs : tls ] \ 

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

251 
by (etac rev_mp 1); 

252 
by (etac tls.induct 1); 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

253 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

254 
setloop split_tac [expand_if]))); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

255 
by (Fake_parts_insert_tac 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

256 
by (step_tac (!claset addSDs [Notes_Crypt_parts_sees, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

257 
Says_imp_sees_Spy' RS parts.Inj] 
3474  258 
addSEs partsEs) 1); 
259 
qed "Hash_Hash_imp_Nonce"; 

260 

261 

262 
(*NEEDED?? 

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

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

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

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

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

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

269 
by (etac rev_mp 1); 

270 
by (etac tls.induct 1); 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

271 
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

272 
by (step_tac (!claset addSDs [Notes_Crypt_parts_sees, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

273 
Says_imp_sees_Spy' RS parts.Inj] 
3474  274 
addSEs partsEs) 1); 
275 
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees]))); 

276 
by (Fake_parts_insert_tac 1); 

3506  277 
(*CertVerify, ClientFinished, ServerFinished (?)*) 
278 
by (REPEAT (Blast_tac 1)); 

3474  279 
qed "Hash_imp_Nonce_seen"; 
280 

281 

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

283 

3506  284 
(*B can check A's signature if he has received A's certificate. 
285 
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

286 
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

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

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

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

293 
\ : set evs > \ 

3474  294 
\ 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

295 
by (hyp_subst_tac 1); 
3474  296 
by (etac tls.induct 1); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

297 
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); 
3474  298 
by (Fake_parts_insert_tac 1); 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

302 
qed_spec_mp "TrustCertVerify"; 

303 

304 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

305 
(*If CERTIFICATE VERIFY is present then A has chosen M.*) 
3506  306 
goal thy 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

307 
"!!evs. [ Crypt (priK A) (Hash{Nonce NB, certificate B KB, Nonce M}) \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

308 
\ : parts (sees lost Spy evs); \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

309 
\ evs : tls; A ~: lost ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

310 
\ ==> Notes A {Agent B, Nonce M} : set evs"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

311 
be rev_mp 1; 
3506  312 
by (etac tls.induct 1); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

313 
by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]))); 
3474  314 
by (Fake_parts_insert_tac 2); 
315 
by (Blast_tac 1); 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

316 
qed "UseCertVerify"; 
3474  317 

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

318 

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

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

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

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

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

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

324 
by (etac tls.induct 1); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

325 
by (ALLGOALS 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

326 
(asm_simp_tac (analz_image_keys_ss 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

327 
addsimps (certificate_def::keys_distinct)))); 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

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

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

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

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

333 

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 
(*Lemma for the trivial direction of the ifandonlyif*) 
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. (X : analz (G Un H)) > (X : analz H) ==> \ 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

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

341 

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

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

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

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

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

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

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

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

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

350 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

351 
by (REPEAT_FIRST (rtac lemma)); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

352 
writeln"SLOW simplification: 50 secs!??"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

353 
by (ALLGOALS 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

354 
(asm_simp_tac (analz_image_keys_ss 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

355 
addsimps (analz_image_priK::certificate_def:: 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

356 
keys_distinct)))); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

357 
by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK]))); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

358 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb]))); 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

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

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

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

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

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

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

366 

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

367 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

368 
(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

369 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

370 
"!!evs. [ evs : tls; A ~: lost; B ~: lost ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

371 
\ ==> Notes A {Agent B, Nonce M} : set evs > \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

372 
\ Nonce M ~: analz (sees lost Spy evs)"; 
3474  373 
by (analz_induct_tac 1); 
374 
(*ClientHello*) 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

375 
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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

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

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

382 
by (REPEAT (blast_tac (!claset addSEs partsEs 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

383 
addDs [Notes_Crypt_parts_sees, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

384 
impOfSubs analz_subset_parts, 
3474  385 
Says_imp_sees_Spy' RS analz.Inj]) 1)); 
386 
bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp)); 

387 

388 

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

390 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

391 
(** First, some lemmas about those write keys. The proofs for serverK are 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

392 
nearly identical to those for clientK. **) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

393 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

394 
(*Lemma: those write keys are never sent if M is secure. 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

395 
Converse doesn't hold; betraying M doesn't force the keys to be sent!*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

396 

3474  397 
goal thy 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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

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

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

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

403 
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

404 
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

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

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

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

408 
by (Blast_tac 1); 
3474  409 
qed "clientK_notin_parts"; 
410 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

411 
Addsimps [clientK_notin_parts]; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

412 
AddSEs [clientK_notin_parts RSN (2, rev_notE)]; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

413 

3474  414 
goal thy 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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

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

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

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

420 
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

421 
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

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

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

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

425 
by (Blast_tac 1); 
3474  426 
qed "serverK_notin_parts"; 
427 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

428 
Addsimps [serverK_notin_parts]; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

429 
AddSEs [serverK_notin_parts RSN (2, rev_notE)]; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

430 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

431 
(*Lemma: those write keys are never used if M is fresh. 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

432 
Converse doesn't hold; betraying M doesn't force the keys to be sent! 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

433 
NOT suitable as safe elim rules.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

434 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

435 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

436 
"!!evs. [ Nonce M ~: used evs; evs : tls ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

437 
\ ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees lost Spy evs)"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

438 
by (etac rev_mp 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

439 
by (analz_induct_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

440 
(*ClientFinished: since M is fresh, a different instance of clientK was used.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

441 
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

442 
addSEs sees_Spy_partsEs) 3); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

443 
by (Fake_parts_insert_tac 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

444 
(*Base*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

445 
by (Blast_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

446 
qed "Crypt_clientK_notin_parts"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

447 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

448 
Addsimps [Crypt_clientK_notin_parts]; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

449 
AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)]; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

450 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

451 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

452 
"!!evs. [ Nonce M ~: used evs; evs : tls ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

453 
\ ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees lost Spy evs)"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

454 
by (etac rev_mp 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

455 
by (analz_induct_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

456 
(*ServerFinished: since M is fresh, a different instance of serverK was used.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

457 
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

458 
addSEs sees_Spy_partsEs) 3); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

459 
by (Fake_parts_insert_tac 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

460 
(*Base*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

461 
by (Blast_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

462 
qed "Crypt_serverK_notin_parts"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

463 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

464 
Addsimps [Crypt_serverK_notin_parts]; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

465 
AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)]; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

466 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

467 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

468 
(*Weakening A~:lost to A~=Spy would complicate later uses of the rule*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

469 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

470 
"!!evs. [ Says A B {certA, Crypt KB (Nonce M)} : set evs; \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

471 
\ A ~: lost; evs : tls ] ==> KB = pubK B"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

472 
be rev_mp 1; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

473 
by (analz_induct_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

474 
qed "A_Crypt_pubB"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

475 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

476 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

477 
(*** Unicity results for M, the premastersecret ***) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

478 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

479 
(*Induction for theorems of the form X ~: analz (sees lost Spy evs) > ... 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

480 
It simplifies the proof by discarding needless information about 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

481 
analz (insert X (sees lost Spy evs)) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

482 
*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

483 
fun analz_mono_parts_induct_tac i = 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

484 
etac tls.induct i THEN 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

485 
ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

486 
REPEAT_FIRST analz_mono_contra_tac; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

487 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

488 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

489 
(*M determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

490 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

491 
"!!evs. [ Nonce M ~: analz (sees lost Spy evs); evs : tls ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

492 
\ ==> EX B'. ALL B. \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

493 
\ Crypt (pubK B) (Nonce M) : parts (sees lost Spy evs) > B=B'"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

494 
by (etac rev_mp 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

495 
by (analz_mono_parts_induct_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

496 
by (prove_simple_subgoals_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

497 
by (asm_simp_tac (!simpset addsimps [all_conj_distrib] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

498 
setloop split_tac [expand_if]) 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

499 
(*ClientCertKeyEx*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

500 
by (expand_case_tac "M = ?y" 2 THEN 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

501 
REPEAT (blast_tac (!claset addSEs partsEs) 2)); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

502 
by (Fake_parts_insert_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

503 
val lemma = result(); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

504 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

505 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

506 
"!!evs. [ Crypt(pubK B) (Nonce M) : parts (sees lost Spy evs); \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

507 
\ Crypt(pubK B') (Nonce M) : parts (sees lost Spy evs); \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

508 
\ Nonce M ~: analz (sees lost Spy evs); \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

509 
\ evs : tls ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

510 
\ ==> B=B'"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

511 
by (prove_unique_tac lemma 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

512 
qed "unique_M"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

513 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

514 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

515 
(*In A's note to herself, M determines A and B.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

516 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

517 
"!!evs. [ Nonce M ~: analz (sees lost Spy evs); evs : tls ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

518 
\ ==> EX A' B'. ALL A B. \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

519 
\ Notes A {Agent B, Nonce M} : set evs > A=A' & B=B'"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

520 
by (etac rev_mp 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

521 
by (analz_mono_parts_induct_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

522 
by (prove_simple_subgoals_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

523 
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

524 
(*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

525 
by (expand_case_tac "M = ?y" 1 THEN 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

526 
blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

527 
val lemma = result(); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

528 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

529 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

530 
"!!evs. [ Notes A {Agent B, Nonce M} : set evs; \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

531 
\ Notes A' {Agent B', Nonce M} : set evs; \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

532 
\ Nonce M ~: analz (sees lost Spy evs); \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

533 
\ evs : tls ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

534 
\ ==> A=A' & B=B'"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

535 
by (prove_unique_tac lemma 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

536 
qed "Notes_unique_M"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

537 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

538 

3474  539 

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

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

542 
to compare XA with what she originally sent. 

543 
***) 

544 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

545 
(*The mention of her name (A) in X assumes A that B knows who she is.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

546 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

547 
"!!evs. [ X = Crypt (serverK(NA,NB,M)) \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

548 
\ (Hash{Hash{Nonce NA, Nonce NB, Nonce M}, \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

549 
\ Nonce NA, Agent XA, Agent A, \ 
3506  550 
\ Nonce NB, Agent XB, certificate B (pubK B)}); \ 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

551 
\ evs : tls; A ~: lost; B ~: lost ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

552 
\ ==> Notes A {Agent B, Nonce M} : set evs > \ 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

554 
by (hyp_subst_tac 1); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

555 
by (analz_induct_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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

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

559 
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

560 
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

561 
not_parts_not_analz]) 2); 
3474  562 
by (Fake_parts_insert_tac 1); 
563 
qed_spec_mp "TrustServerFinished"; 

564 

565 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

566 
(*This version refers not to SERVER FINISHED but to any message from B. 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

567 
We don't assume B has received CERTIFICATE VERIFY, and an intruder could 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

568 
have changed A's identity in all other messages, so we can't be sure 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

569 
that B sends his message to A.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

570 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

571 
"!!evs. [ evs : tls; A ~: lost; B ~: lost ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

572 
\ ==> Notes A {Agent B, Nonce M} : set evs > \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

573 
\ Crypt (serverK(NA,NB,M)) Y : parts (sees lost Spy evs) > \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

574 
\ (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

575 
by (analz_induct_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

576 
by (REPEAT_FIRST (rtac impI)); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

577 
(*Fake: the Spy doesn't have the critical session key!*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

578 
by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

579 
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

580 
not_parts_not_analz]) 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

581 
by (Fake_parts_insert_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

582 
(*ServerFinished. If the message is old then apply induction hypothesis...*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

583 
by (rtac conjI 1 THEN Blast_tac 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

584 
(*...otherwise delete induction hyp and use unicity of M.*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

585 
by (thin_tac "?PP>?QQ" 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

586 
by (Step_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

587 
by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

588 
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

589 
by (blast_tac (!claset addSEs [MPair_parts] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

590 
addDs [Notes_Crypt_parts_sees, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

591 
Says_imp_sees_Spy' RS parts.Inj, 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

592 
unique_M]) 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

593 
qed_spec_mp "TrustServerMsg"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

594 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

595 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

596 
(*** Protocol goal: if B receives any message encrypted with clientK 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

597 
then A has sent it, ASSUMING that A chose M. Authentication is 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

598 
assumed here; B cannot verify it. But if the message is 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

599 
CLIENT FINISHED, then B can then check the quoted values XA, XB, etc. 
3506  600 
***) 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

601 
goal thy 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

602 
"!!evs. [ evs : tls; A ~: lost; B ~: lost ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

603 
\ ==> Notes A {Agent B, Nonce M} : set evs > \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

604 
\ Crypt (clientK(NA,NB,M)) Y : parts (sees lost Spy evs) > \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

605 
\ Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

606 
by (analz_induct_tac 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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

609 
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

610 
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

611 
not_parts_not_analz]) 2); 
3474  612 
by (Fake_parts_insert_tac 1); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

613 
(*ClientFinished. If the message is old then apply induction hypothesis...*) 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

614 
by (step_tac (!claset delrules [conjI]) 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

615 
by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

616 
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

617 
by (blast_tac (!claset addSEs [MPair_parts] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

618 
addDs [Notes_unique_M]) 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

619 
qed_spec_mp "TrustClientMsg"; 
3506  620 

621 

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

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

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

625 
***) 

626 
goal thy 

3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

627 
"!!evs. [ Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs; \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

628 
\ Says B A {Nonce NA, Nonce NB, Agent XB, certificate B KB} \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

629 
\ : set evs; \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

630 
\ Says A'' B (Crypt (priK A) \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

631 
\ (Hash{Nonce NB, certificate B KB, Nonce M})) \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

632 
\ : set evs; \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

633 
\ evs : tls; A ~: lost; B ~: lost ] \ 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

634 
\ ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

635 
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify] 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

636 
addDs [Says_imp_sees_Spy RS parts.Inj]) 1); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

637 
qed "AuthClientFinished"; 