author  paulson 
Mon, 14 Jul 1997 12:47:21 +0200  
changeset 3519  ab0a9fbed4c0 
parent 3515  d8a71f6eaf40 
child 3672  56e4365a0c99 
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 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

25 
(** We mostly DO NOT unfold the definition of "certificate". The attached 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

26 
lemmas unfold it lazily, when "certificate B KB" occurs in appropriate 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

27 
contexts. 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

28 
**) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

29 

ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

30 
goalw thy [certificate_def] 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

31 
"parts (insert (certificate B KB) H) = \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

32 
\ parts (insert (Crypt (priK Server) {Agent B, Key KB}) H)"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

33 
by (rtac refl 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

34 
qed "parts_insert_certificate"; 
3474  35 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

36 
goalw thy [certificate_def] 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

37 
"analz (insert (certificate B KB) H) = \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

38 
\ analz (insert (Crypt (priK Server) {Agent B, Key KB}) H)"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

39 
by (rtac refl 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

40 
qed "analz_insert_certificate"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

41 
Addsimps [parts_insert_certificate, analz_insert_certificate]; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

42 

ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

43 
goalw thy [certificate_def] 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

44 
"(X = certificate B KB) = (Crypt (priK Server) {Agent B, Key KB} = X)"; 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

45 
by (Blast_tac 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

46 
qed "eq_certificate_iff"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

47 
AddIffs [eq_certificate_iff]; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

48 

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

49 

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

52 

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

54 
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK, 

55 
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

56 

3474  57 

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

59 

60 
goal thy "pubK 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 "pubK_neq_clientK"; 

65 

66 
goal thy "pubK 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 "pubK_neq_serverK"; 

71 

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

73 
br notI 1; 

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

75 
by (Full_simp_tac 1); 

76 
qed "priK_neq_clientK"; 

77 

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

79 
br notI 1; 

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

81 
by (Full_simp_tac 1); 

82 
qed "priK_neq_serverK"; 

83 

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

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

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

86 
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

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

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

89 

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

90 
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

91 
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

92 
AddIffs (keys_distinct @ (keys_distinct RL [not_sym])); 
3474  93 

94 

95 
(**** Protocol Proofs ****) 

96 

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

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

99 

100 
(*Possibility property ending with ServerFinished.*) 

101 
goal thy 

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

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

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

105 
\ Nonce NA, Agent XA, Agent A, \ 

106 
\ Nonce NB, Agent XB, \ 

3500  107 
\ certificate B (pubK B)})) \ 
3474  108 
\ : set evs"; 
109 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

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

111 
RS tls.ServerFinished) 2); 

112 
by possibility_tac; 

113 
result(); 

114 

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

116 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

117 
"!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

118 
\ Says A B (Crypt (clientK(NA,NB,M)) \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

119 
\ (Hash{Hash{Nonce NA, Nonce NB, Nonce M}, \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

124 
RS tls.ClientFinished) 2); 

125 
by possibility_tac; 

126 
result(); 

127 

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

129 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

3474  136 
by possibility_tac; 
137 
result(); 

138 

139 

140 
(**** Inductive proofs about tls ****) 

141 

142 
(*Nobody sends themselves messages*) 

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

144 
by (etac tls.induct 1); 

145 
by (Auto_tac()); 

146 
qed_spec_mp "not_Says_to_self"; 

147 
Addsimps [not_Says_to_self]; 

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

149 

150 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

151 
(*Induction for regularity theorems. If induction formula has the form 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

152 
X ~: analz (sees Spy evs) > ... then it shortens the proof by discarding 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

153 
needless information about analz (insert X (sees Spy evs)) *) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

154 
fun parts_induct_tac i = 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

155 
etac tls.induct i 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

156 
THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

157 
REPEAT (FIRSTGOAL analz_mono_contra_tac) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

158 
THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

159 
fast_tac (!claset addss (!simpset)) i THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

160 
ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

161 

ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

162 

ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

163 
(** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY 
3474  164 
sends messages containing X! **) 
165 

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

167 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

168 
"!!evs. evs : tls ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

169 
by (parts_induct_tac 1); 
3474  170 
by (Fake_parts_insert_tac 1); 
171 
qed "Spy_see_priK"; 

172 
Addsimps [Spy_see_priK]; 

173 

174 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

175 
"!!evs. evs : tls ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)"; 
3474  176 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 
177 
qed "Spy_analz_priK"; 

178 
Addsimps [Spy_analz_priK]; 

179 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

180 
goal thy "!!A. [ Key (priK A) : parts (sees Spy evs); \ 
3474  181 
\ evs : tls ] ==> A:lost"; 
182 
by (blast_tac (!claset addDs [Spy_see_priK]) 1); 

183 
qed "Spy_see_priK_D"; 

184 

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

186 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

187 

188 

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

189 
(*This lemma says that no false certificates exist. One might extend the 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

191 
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

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

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

194 
"!!evs. evs : tls \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

195 
\ ==> certificate B KB : parts (sees Spy evs) > KB = pubK B"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

196 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

197 
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

198 
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

199 

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

200 

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

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

202 
val ClientCertKeyEx_tac = 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

204 
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

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

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

207 

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

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

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

210 
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

211 
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

212 
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

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

214 
(!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

215 
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

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

217 
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

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

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

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

221 

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

222 

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

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

224 

3474  225 
(*Every Nonce that's hashed is already in past traffic. *) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

226 
goal thy "!!evs. [ Hash {Nonce N, X} : parts (sees Spy evs); \ 
3474  227 
\ evs : tls ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

228 
\ ==> Nonce N : parts (sees Spy evs)"; 
3474  229 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

230 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

231 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

232 
by (Fake_parts_insert_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

233 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

234 
addSEs partsEs) 1); 
3474  235 
qed "Hash_imp_Nonce1"; 
236 

237 
(*Lemma needed to prove Hash_Hash_imp_Nonce*) 

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

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

239 
\ : parts (sees Spy evs); \ 
3474  240 
\ evs : tls ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

241 
\ ==> Nonce M : parts (sees Spy evs)"; 
3474  242 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

243 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

244 
by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

245 
by (Fake_parts_insert_tac 1); 
3474  246 
qed "Hash_imp_Nonce2"; 
247 
AddSDs [Hash_imp_Nonce2]; 

248 

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

249 

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

250 
goal thy "!!evs. [ Notes A {Agent B, X} : set evs; evs : tls ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

254 
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

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

256 

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

257 

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

258 
(*NEEDED??*) 
3474  259 
goal thy "!!evs. [ Hash { Hash{Nonce NA, Nonce NB, Nonce M}, X } \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

260 
\ : parts (sees Spy evs); \ 
3474  261 
\ evs : tls ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

262 
\ ==> Nonce M : parts (sees Spy evs)"; 
3474  263 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

264 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

265 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

266 
by (Fake_parts_insert_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

267 
by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees, 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

268 
Says_imp_sees_Spy RS parts.Inj] 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

269 
addSEs partsEs) 1)); 
3474  270 
qed "Hash_Hash_imp_Nonce"; 
271 

272 

273 
(*NEEDED?? 

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

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

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

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

277 
goal thy "!!evs. [ Hash X : parts (sees Spy evs); \ 
3474  278 
\ Nonce N : parts {X}; evs : tls ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

279 
\ ==> Nonce N : parts (sees Spy evs)"; 
3474  280 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

282 
by (step_tac (!claset addSDs [Notes_Crypt_parts_sees, 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

283 
Says_imp_sees_Spy RS parts.Inj] 
3474  284 
addSEs partsEs) 1); 
285 
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees]))); 

286 
by (Fake_parts_insert_tac 1); 

3506  287 
(*CertVerify, ClientFinished, ServerFinished (?)*) 
288 
by (REPEAT (Blast_tac 1)); 

3474  289 
qed "Hash_imp_Nonce_seen"; 
290 

291 

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

293 

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

296 
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

297 
assume A~:lost; otherwise, the Spy can forge A's signature.*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

298 
goal thy 
3506  299 
"!!evs. [ X = Crypt (priK A) \ 
300 
\ (Hash{Nonce NB, certificate B KB, Nonce M}); \ 

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

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

303 
\ : set evs > \ 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

304 
\ X : parts (sees 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

305 
by (hyp_subst_tac 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

306 
by (parts_induct_tac 1); 
3474  307 
by (Fake_parts_insert_tac 1); 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

311 
qed_spec_mp "TrustCertVerify"; 

312 

313 

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

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

316 
"!!evs. [ Crypt (priK A) (Hash{Nonce NB, certificate B KB, Nonce M}) \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

320 
be rev_mp 1; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

321 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

322 
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

323 
qed "UseCertVerify"; 
3474  324 

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

325 

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

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

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

328 
"!!evs. evs : tls ==> \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

331 
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

332 
by (ALLGOALS 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

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

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

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

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

340 

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

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

346 
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

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

348 

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

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

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

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

352 
\ ALL KK. KK <= (range clientK Un range serverK) > \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

353 
\ (Nonce N : analz (Key``KK Un (sees Spy evs))) = \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

357 
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

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

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

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

361 
(asm_simp_tac (analz_image_keys_ss 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

362 
addsimps (analz_image_priK::certificate_def:: 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

364 
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

365 
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

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

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

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

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

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

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

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

373 

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

374 

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

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

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

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

378 
\ ==> Notes A {Agent B, Nonce M} : set evs > \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

379 
\ Nonce M ~: analz (sees Spy evs)"; 
3474  380 
by (analz_induct_tac 1); 
381 
(*ClientHello*) 

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

382 
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

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

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

385 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2); 
3474  386 
(*Fake*) 
387 
by (spy_analz_tac 1); 

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

389 
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

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

391 
impOfSubs analz_subset_parts, 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

392 
Says_imp_sees_Spy RS analz.Inj]) 1)); 
3474  393 
bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp)); 
394 

395 

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

397 

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

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

399 
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

400 

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

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

402 
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

403 

3474  404 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

405 
"!!evs. [ Nonce M ~: analz (sees Spy evs); evs : tls ] \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

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

410 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

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

415 
by (Blast_tac 1); 
3474  416 
qed "clientK_notin_parts"; 
417 

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

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

419 
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

420 

3474  421 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

422 
"!!evs. [ Nonce M ~: analz (sees Spy evs); evs : tls ] \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

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

427 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

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

432 
by (Blast_tac 1); 
3474  433 
qed "serverK_notin_parts"; 
434 

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

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

436 
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

437 

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

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

439 
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

440 
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

441 

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

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

443 
"!!evs. [ Nonce M ~: used evs; evs : tls ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

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

448 
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

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

450 
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

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

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

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

454 

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

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

456 
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

457 

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

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

459 
"!!evs. [ Nonce M ~: used evs; evs : tls ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

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

464 
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

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

466 
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

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

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

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

470 

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

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

472 
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

473 

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

474 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

477 
"!!evs. [ Says A B {certA, Crypt KB (Nonce M)} : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

481 
qed "A_Crypt_pubB"; 
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 

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

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

485 

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

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

487 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

489 
\ ==> EX B'. ALL B. \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

491 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

492 
by (parts_induct_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

493 
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

494 
(*ClientCertKeyEx*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

495 
by (ClientCertKeyEx_tac 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

496 
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

497 
by (expand_case_tac "M = ?y" 1 THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

500 

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

501 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

502 
"!!evs. [ Crypt(pubK B) (Nonce M) : parts (sees Spy evs); \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

503 
\ Crypt(pubK B') (Nonce M) : parts (sees Spy evs); \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

507 
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

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

509 

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

510 

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

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

512 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

516 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

518 
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

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

520 
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

521 
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

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

523 

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

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

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

526 
\ Notes A' {Agent B', Nonce M} : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

530 
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

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

532 

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

533 

3474  534 

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

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

537 
to compare XA with what she originally sent. 

538 
***) 

539 

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

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

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

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

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

544 
\ Nonce NA, Agent XA, Agent A, \ 
3506  545 
\ 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

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

547 
\ ==> Notes A {Agent B, Nonce M} : set evs > \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

549 
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

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

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

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

553 
by (REPEAT (rtac impI 1)); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

555 
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

556 
not_parts_not_analz]) 2); 
3474  557 
by (Fake_parts_insert_tac 1); 
558 
qed_spec_mp "TrustServerFinished"; 

559 

560 

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

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

562 
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

563 
have changed A's identity in all other messages, so we can't be sure 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

564 
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

565 
to bind A's identify with M, then we could replace A' by A below.*) 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

566 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

567 
"!!evs. [ evs : tls; A ~: lost; B ~: lost ] \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

568 
\ ==> Notes A {Agent B, Nonce M} : set evs > \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

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

573 
(*Fake: the Spy doesn't have the critical session key!*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

575 
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

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

577 
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

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

579 
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

580 
(*...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

581 
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

582 
by (Step_tac 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

584 
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

585 
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

586 
addDs [Notes_Crypt_parts_sees, 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

590 

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

591 

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

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

593 
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

594 
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

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

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

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

599 
\ ==> Notes A {Agent B, Nonce M} : set evs > \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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

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

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

604 
(*Fake: the Spy doesn't have the critical session key!*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

606 
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

607 
not_parts_not_analz]) 2); 
3474  608 
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

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

610 
by (step_tac (!claset delrules [conjI]) 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

612 
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

613 
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

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

615 
qed_spec_mp "TrustClientMsg"; 
3506  616 

617 

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

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

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

621 
***) 

622 
goal thy 

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

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

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

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

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

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

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

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

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

631 
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

632 
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

633 
qed "AuthClientFinished"; 