author  paulson 
Fri, 19 Sep 1997 16:12:21 +0200  
changeset 3685  5b8c0c8f576e 
parent 3683  aafe719dff14 
child 3686  4b484805b4c4 
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 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

11 
message is optional!) 
3474  12 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

14 

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

15 
* 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*) 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

51 
AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq]; 
3474  52 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

53 
(* invKey(sessionK x) = sessionK x*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

54 
Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK]; 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

55 

3474  56 

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

58 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

59 
goal thy "pubK A ~= sessionK arg"; 
3474  60 
br notI 1; 
61 
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); 

62 
by (Full_simp_tac 1); 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

63 
qed "pubK_neq_sessionK"; 
3474  64 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

65 
goal thy "priK A ~= sessionK arg"; 
3474  66 
br notI 1; 
67 
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); 

68 
by (Full_simp_tac 1); 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

69 
qed "priK_neq_sessionK"; 
3474  70 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

71 
val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK]; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

72 
AddIffs (keys_distinct @ (keys_distinct RL [not_sym])); 
3474  73 

74 

75 
(**** Protocol Proofs ****) 

76 

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

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

79 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

80 

56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

81 
(** These proofs make the further assumption that the Nonce_supply nonces 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

82 
(which have the form @ N. Nonce N ~: used evs) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

83 
lie outside the range of PRF. This assumption seems reasonable, but 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

84 
as it is needed only for the possibility theorems, it is not taken 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

85 
as an axiom. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

86 
**) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

87 

56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

88 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

89 
(*Possibility property ending with ClientAccepts.*) 
3474  90 
goal thy 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

91 
"!!A B. [ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

92 
\ A ~= B ] ==> EX SID M. EX evs: tls. \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

93 
\ Notes A {Number SID, Agent A, Agent B, Nonce M} : set evs"; 
3474  94 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
95 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

96 
RS tls.ClientFinished RS tls.ServerFinished RS tls.ClientAccepts) 2); 
3474  97 
by possibility_tac; 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

98 
by (REPEAT (Blast_tac 1)); 
3474  99 
result(); 
100 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

101 
(*And one for ServerAccepts. Either FINISHED message may come first.*) 
3474  102 
goal thy 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

103 
"!!A B. [ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

104 
\ A ~= B ] ==> EX SID NA XA NB XB M. EX evs: tls. \ 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

105 
\ Notes B {Number SID, Agent A, Agent B, Nonce M} : set evs"; 
3474  106 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
107 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

108 
RS tls.ServerFinished RS tls.ClientFinished RS tls.ServerAccepts) 2); 
3474  109 
by possibility_tac; 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

110 
by (REPEAT (Blast_tac 1)); 
3474  111 
result(); 
112 

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

114 
goal thy 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

115 
"!!A B. [ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

116 
\ A ~= B ] ==> EX NB PMS. EX evs: tls. \ 
3474  117 
\ Says A B (Crypt (priK A) \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

118 
\ (Hash{Nonce NB, certificate B (pubK B), Nonce PMS})) : set evs"; 
3474  119 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
3506  120 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx 
121 
RS tls.CertVerify) 2); 

3474  122 
by possibility_tac; 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

123 
by (REPEAT (Blast_tac 1)); 
3474  124 
result(); 
125 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

126 
(*Another one, for session resumption (both ServerResume and ClientResume) *) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

127 
goal thy 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

128 
"!!A B. [ evs0 : tls; \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

129 
\ Notes A {Number SID, Agent A, Agent B, Nonce M} : set evs0; \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

130 
\ Notes B {Number SID, Agent A, Agent B, Nonce M} : set evs0; \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

131 
\ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

132 
\ A ~= B ] ==> EX NA XA NB XB. EX evs: tls. \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

133 
\ Says A B (Crypt (clientK(NA,NB,M)) \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

134 
\ (Hash{Nonce M, Number SID, \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

135 
\ Nonce NA, Number XA, Agent A, \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

136 
\ Nonce NB, Number XB, Agent B})) : set evs"; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

137 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

138 
by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

139 
by possibility_tac; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

140 
by (REPEAT (Blast_tac 1)); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

141 
result(); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

142 

5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

143 

3474  144 

145 
(**** Inductive proofs about tls ****) 

146 

147 
(*Nobody sends themselves messages*) 

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

149 
by (etac tls.induct 1); 

150 
by (Auto_tac()); 

151 
qed_spec_mp "not_Says_to_self"; 

152 
Addsimps [not_Says_to_self]; 

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

154 

155 

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

156 
(*Induction for regularity theorems. If induction formula has the form 
3683  157 
X ~: analz (spies evs) > ... then it shortens the proof by discarding 
158 
needless information about analz (insert X (spies evs)) *) 

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

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

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

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

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

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

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

165 
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

166 

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

167 

3683  168 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
3474  169 
sends messages containing X! **) 
170 

3683  171 
(*Spy never sees another agent's private key! (unless it's bad at start)*) 
3474  172 
goal thy 
3683  173 
"!!evs. evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

174 
by (parts_induct_tac 1); 
3474  175 
by (Fake_parts_insert_tac 1); 
176 
qed "Spy_see_priK"; 

177 
Addsimps [Spy_see_priK]; 

178 

179 
goal thy 

3683  180 
"!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; 
3474  181 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 
182 
qed "Spy_analz_priK"; 

183 
Addsimps [Spy_analz_priK]; 

184 

3683  185 
goal thy "!!A. [ Key (priK A) : parts (spies evs); \ 
186 
\ evs : tls ] ==> A:bad"; 

3474  187 
by (blast_tac (!claset addDs [Spy_see_priK]) 1); 
188 
qed "Spy_see_priK_D"; 

189 

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

191 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

192 

193 

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

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

195 
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

196 
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

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

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

199 
"!!evs. evs : tls \ 
3683  200 
\ ==> certificate B KB : parts (spies evs) > KB = pubK B"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

202 
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

203 
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

204 

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

207 
val ClientCertKeyEx_tac = 
3683  208 
forward_tac [Says_imp_spies RS parts.Inj RS 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

209 
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

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

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

212 

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

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

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

215 
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

216 
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

217 
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

218 
ALLGOALS (asm_simp_tac 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

219 
(!simpset addcongs [if_weak_cong] 
3515
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])) THEN 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

222 
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

223 
ALLGOALS (asm_simp_tac 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

224 
(!simpset addcongs [if_weak_cong] 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

227 

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

228 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

229 
(*** Notes are made under controlled circumstances ***) 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

230 

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

231 
goal thy "!!evs. [ Notes A {Agent B, X} : set evs; evs : tls ] \ 
3683  232 
\ ==> Crypt (pubK B) X : parts (spies evs)"; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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

235 
by (blast_tac (!claset addIs [parts_insertI]) 1); 
3683  236 
qed "Notes_Crypt_parts_spies"; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

237 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

238 
(*C might be either A or B*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

239 
goal thy 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

240 
"!!evs. [ Notes C {Number SID, Agent A, Agent B, Nonce M} : set evs; \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

241 
\ evs : tls \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

242 
\ ] ==> M : range PRF"; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

243 
by (etac rev_mp 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

244 
by (parts_induct_tac 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

245 
by (Auto_tac()); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

247 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

248 
(*C might be either A or B*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

249 
goal thy 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

250 
"!!evs. [ Notes C {Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))} \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

251 
\ : set evs; evs : tls \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

252 
\ ] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

253 
by (etac rev_mp 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

254 
by (parts_induct_tac 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

255 
(*Fake*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

256 
by (blast_tac (!claset addIs [parts_insertI]) 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

257 
(*Client, Server Accept*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

258 
by (Step_tac 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

259 
by (REPEAT (blast_tac (!claset addSEs spies_partsEs 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

260 
addSDs [Notes_Crypt_parts_spies]) 1)); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

261 
qed "Notes_master_imp_Crypt_PMS"; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

262 

5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

263 
(*Compared with the theorem above, both premise and conclusion are stronger*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

264 
goal thy 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

265 
"!!evs. [ Notes A {Number SID, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))} \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

266 
\ : set evs; evs : tls \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

267 
\ ] ==> Notes A {Agent B, Nonce PMS} : set evs"; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

268 
by (etac rev_mp 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

269 
by (parts_induct_tac 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

270 
(*ServerAccepts*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

271 
by (Fast_tac 1); (*Blast_tac's very slow here*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

272 
qed "Notes_master_imp_Notes_PMS"; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

273 

5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

274 

5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

275 
(*Every Nonce that's hashed is already in past traffic; this event 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

276 
occurs in CertVerify. The condition NB ~: range PRF excludes the 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

277 
MASTER SECRET from consideration; it is created using PRF.*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

278 
goal thy "!!evs. [ Hash {Nonce NB, X} : parts (spies evs); \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

279 
\ NB ~: range PRF; evs : tls ] \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

280 
\ ==> Nonce NB : parts (spies evs)"; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

281 
by (etac rev_mp 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

282 
by (etac rev_mp 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

283 
by (parts_induct_tac 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

284 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies]))); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

285 
(*Server/Client Resume: wrong sort of nonce!*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

286 
by (REPEAT (blast_tac (!claset addSDs [Notes_master_range_PRF]) 5)); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

287 
(*FINISHED messages are trivial because M : range PRF*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

288 
by (REPEAT (Blast_tac 3)); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

289 
(*CertVerify is the only interesting case*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

290 
by (blast_tac (!claset addSEs spies_partsEs) 2); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

291 
by (Fake_parts_insert_tac 1); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

292 
qed "Hash_Nonce_CV"; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

293 

5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

294 

5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

295 

5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

296 
(*** Protocol goal: if B receives CertVerify, then A sent it ***) 
3474  297 

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

300 
message is Fake. We don't need guarantees for the Spy anyway. We must 
3683  301 
assume A~:bad; 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

302 
goal thy 
3506  303 
"!!evs. [ X = Crypt (priK A) \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

304 
\ (Hash{Nonce NB, certificate B KB, Nonce PMS}); \ 
3683  305 
\ evs : tls; A ~: bad; B ~= Spy ] \ 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

306 
\ ==> Says B A {Nonce NB, Number SID, Number XB, certificate B KB} \ 
3506  307 
\ : set evs > \ 
3683  308 
\ X : parts (spies evs) > Says A B X : set evs"; 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

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

312 
(*ServerHello: nonce NB cannot be in X because it's fresh!*) 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

313 
by (blast_tac (!claset addSDs [Hash_Nonce_CV] 
3683  314 
addSEs spies_partsEs) 1); 
3474  315 
qed_spec_mp "TrustCertVerify"; 
316 

317 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

318 
(*If CertVerify is present then A has chosen PMS.*) 
3506  319 
goal thy 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

320 
"!!evs. [ Crypt (priK A) (Hash{Nonce NB, certificate B KB, Nonce PMS}) \ 
3683  321 
\ : parts (spies evs); \ 
322 
\ evs : tls; A ~: bad ] \ 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

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

326 
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

327 
qed "UseCertVerify"; 
3474  328 

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

329 

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

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

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

332 
"!!evs. evs : tls ==> \ 
3683  333 
\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ 
334 
\ (priK B : KK  B : bad)"; 

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

335 
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

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

337 
(asm_simp_tac (analz_image_keys_ss 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

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

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

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

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

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

344 

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

345 

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

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

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

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

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

350 
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

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

352 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

353 
(*slightly speeds up the big simplification below*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

354 
goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK"; 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

355 
by (Blast_tac 1); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

356 
val range_sessionkeys_not_priK = result(); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

357 

f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

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

360 
"!!evs. evs : tls ==> \ 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

361 
\ ALL KK. KK <= range sessionK > \ 
3683  362 
\ (Nonce N : analz (Key``KK Un (spies evs))) = \ 
363 
\ (Nonce N : analz (spies evs))"; 

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

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

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

366 
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

367 
by (REPEAT_FIRST (rtac lemma)); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

368 
writeln"SLOW simplification: 55 secs??"; 
3683  369 
(*ClientCertKeyEx is to blame, causing case splits for A, B: bad*) 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

371 
(asm_simp_tac (analz_image_keys_ss 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

372 
addsimps [range_sessionkeys_not_priK, 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

373 
analz_image_priK, analz_insert_certificate]))); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

374 
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

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

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

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

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

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

380 

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

381 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

382 
goal thy "!!evs. evs : tls ==> Notes A {Agent B, Nonce (PRF x)} ~: set evs"; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

383 
by (parts_induct_tac 1); 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

384 
(*ClientCertKeyEx: PMS is assumed to differ from any PRF.*) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

385 
by (Blast_tac 1); 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

386 
qed "no_Notes_A_PRF"; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

387 
Addsimps [no_Notes_A_PRF]; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

388 

56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

389 

3683  390 
goal thy "!!evs. [ Nonce (PRF (PMS,NA,NB)) : parts (spies evs); \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

391 
\ evs : tls ] \ 
3683  392 
\ ==> Nonce PMS : parts (spies evs)"; 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

393 
by (etac rev_mp 1); 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

394 
by (parts_induct_tac 1); 
3683  395 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies]))); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

396 
by (Fake_parts_insert_tac 1); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

397 
(*Six others, all trivial or by freshness*) 
3683  398 
by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_spies] 
399 
addSEs spies_partsEs) 1)); 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

400 
qed "MS_imp_PMS"; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

401 
AddSDs [MS_imp_PMS]; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

402 

56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

403 

3474  404 

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

406 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

407 
(** Some lemmas about session keys, comprising clientK and serverK **) 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

408 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

410 
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

411 

3474  412 
goal thy 
3683  413 
"!!evs. [ Nonce M ~: analz (spies evs); evs : tls ] \ 
414 
\ ==> Key (sessionK(b,NA,NB,M)) ~: parts (spies evs)"; 

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

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

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

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

418 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); 
3683  419 
by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3); 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

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

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

423 
by (Blast_tac 1); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

424 
qed "sessionK_notin_parts"; 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

425 
bind_thm ("sessionK_in_partsE", sessionK_notin_parts RSN (2, rev_notE)); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

426 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

427 
Addsimps [sessionK_notin_parts]; 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

428 
AddSEs [sessionK_in_partsE, 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

429 
impOfSubs analz_subset_parts RS sessionK_in_partsE]; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

430 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

431 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

432 
(*Lemma: session keys are never used if PMS is fresh. 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

433 
Nonces don't have to agree, allowing session resumption. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

434 
Converse doesn't hold; revealing PMS doesn't force the keys to be sent. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

436 

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

437 
goal thy 
3683  438 
"!!evs. [ Nonce PMS ~: parts (spies evs); evs : tls ] \ 
439 
\ ==> Crypt (sessionK(b, Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (spies evs)"; 

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

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

441 
by (analz_induct_tac 1); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

442 
(*Fake*) 
3683  443 
by (asm_simp_tac (!simpset addsimps [parts_insert_spies]) 2); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

444 
by (Fake_parts_insert_tac 2); 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

445 
(*Base, ClientFinished, ServerFinished, ClientResume: 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

446 
trivial, e.g. by freshness*) 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

447 
by (REPEAT 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

448 
(blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

449 
Notes_master_imp_Crypt_PMS] 
3683  450 
addSEs spies_partsEs) 1)); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

451 
qed "Crypt_sessionK_notin_parts"; 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

452 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

453 
Addsimps [Crypt_sessionK_notin_parts]; 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

455 

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

456 

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

457 
(*NEEDED??*) 
3515
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. [ 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

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

461 
be 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 
qed "A_Crypt_pubB"; 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

464 

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

465 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

467 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

469 
goal thy 
3683  470 
"!!evs. [ Nonce PMS ~: analz (spies evs); evs : tls ] \ 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

471 
\ ==> EX B'. ALL B. \ 
3683  472 
\ Crypt (pubK B) (Nonce PMS) : parts (spies evs) > B=B'"; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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

475 
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

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

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

478 
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

480 
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

481 
val lemma = result(); 
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 
goal thy 
3683  484 
"!!evs. [ Crypt(pubK B) (Nonce PMS) : parts (spies evs); \ 
485 
\ Crypt(pubK B') (Nonce PMS) : parts (spies evs); \ 

486 
\ Nonce PMS ~: analz (spies evs); \ 

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

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

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

489 
by (prove_unique_tac lemma 1); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

491 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

492 
(** It is frustrating that we need two versions of the unicity results. 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

493 
But Notes A {Agent B, Nonce PMS} determines both A and B, while 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

494 
Crypt(pubK B) (Nonce PMS) determines only B, and sometimes only 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

495 
this weaker item is available. 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

497 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

498 
(*In A's internal Note, PMS determines A and B.*) 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

499 
goal thy 
3683  500 
"!!evs. [ Nonce PMS ~: analz (spies evs); evs : tls ] \ 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

501 
\ ==> EX A' B'. ALL A B. \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

504 
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

505 
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

506 
(*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

507 
by (expand_case_tac "PMS = ?y" 1 THEN 
3683  508 
blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

509 
val lemma = result(); 
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 
goal thy 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

512 
"!!evs. [ Notes A {Agent B, Nonce PMS} : set evs; \ 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

513 
\ Notes A' {Agent B', Nonce PMS} : set evs; \ 
3683  514 
\ Nonce PMS ~: analz (spies evs); \ 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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

517 
by (prove_unique_tac lemma 1); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

519 

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

520 

3474  521 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

522 
(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

523 
goal thy 
3683  524 
"!!evs. [ evs : tls; A ~: bad; B ~: bad ] \ 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

525 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
3683  526 
\ Nonce PMS ~: analz (spies evs)"; 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

527 
by (analz_induct_tac 1); (*30 seconds??*) 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

528 
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

529 
by (REPEAT (fast_tac (!claset addss (!simpset)) 6)); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

530 
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

531 
by (REPEAT (blast_tac (!claset addSEs partsEs 
3683  532 
addDs [Notes_Crypt_parts_spies, 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

533 
impOfSubs analz_subset_parts, 
3683  534 
Says_imp_spies RS analz.Inj]) 4)); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

535 
(*ClientHello*) 
3683  536 
by (blast_tac (!claset addSDs [Notes_Crypt_parts_spies] 
537 
addSEs spies_partsEs) 3); 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

538 
(*SpyKeys*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

539 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

540 
by (fast_tac (!claset addss (!simpset)) 2); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

541 
(*Fake*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

542 
by (spy_analz_tac 1); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

543 
bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp)); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

544 

f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

545 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

546 
(*Another way of showing unicity*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

547 
goal thy 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

548 
"!!evs. [ Notes A {Agent B, Nonce PMS} : set evs; \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

549 
\ Notes A' {Agent B', Nonce PMS} : set evs; \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

550 
\ A ~: bad; B ~: bad; \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

551 
\ evs : tls ] \ 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

552 
\ ==> A=A' & B=B'"; 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

553 
by (REPEAT (ares_tac [Notes_unique_PMS, Spy_not_see_PMS] 1)); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

554 
qed "good_Notes_unique_PMS"; 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

555 

f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

556 

f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

557 
(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

558 
will stay secret.*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

559 
goal thy 
3683  560 
"!!evs. [ evs : tls; A ~: bad; B ~: bad ] \ 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

561 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
3683  562 
\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)"; 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

563 
by (analz_induct_tac 1); (*35 seconds*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

564 
(*ClientAccepts and ServerAccepts: because PMS was already visible*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

565 
by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
3683  566 
Says_imp_spies RS analz.Inj, 
567 
Notes_imp_spies RS analz.Inj]) 6)); 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

568 
(*ClientHello*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

569 
by (Blast_tac 3); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

570 
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

571 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

572 
by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
3683  573 
Says_imp_spies RS analz.Inj]) 2); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

574 
(*Fake*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

575 
by (spy_analz_tac 1); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

576 
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

577 
by (REPEAT (blast_tac (!claset addSEs partsEs 
3683  578 
addDs [Notes_Crypt_parts_spies, 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

579 
impOfSubs analz_subset_parts, 
3683  580 
Says_imp_spies RS analz.Inj]) 1)); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

581 
bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp)); 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

582 

f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

583 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

584 
(*** Protocol goals: if A receives ServerFinished, then B is present 
3474  585 
and has used the quoted values XA, XB, etc. Note that it is up to A 
586 
to compare XA with what she originally sent. 

587 
***) 

588 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

590 
goal thy 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

591 
"!!evs. [ X = Crypt (serverK(Na,Nb,M)) \ 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

592 
\ (Hash{Nonce M, Number SID, \ 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

593 
\ Nonce NA, Number XA, Agent A, \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

594 
\ Nonce NB, Number XB, Agent B}); \ 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

595 
\ M = PRF(PMS,NA,NB); \ 
3683  596 
\ evs : tls; A ~: bad; B ~: bad ] \ 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

597 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
3683  598 
\ X : parts (spies evs) > Says B A X : set evs"; 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

599 
by (hyp_subst_tac 1); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

600 
by (analz_induct_tac 1); (*16 seconds*) 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

601 
(*ServerResume is trivial, but Blast_tac is too slow*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

602 
by (Best_tac 3); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

603 
(*ClientCertKeyEx*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

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

606 
by (REPEAT (rtac impI 1)); 
3683  607 
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

609 
not_parts_not_analz]) 2); 
3474  610 
by (Fake_parts_insert_tac 1); 
611 
qed_spec_mp "TrustServerFinished"; 

612 

613 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

614 
(*This version refers not to ServerFinished but to any message from B. 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

616 
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

617 
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

618 
to bind A's identity 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

619 
goal thy 
3683  620 
"!!evs. [ evs : tls; A ~: bad; B ~: bad; \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

621 
\ M = PRF(PMS,NA,NB) ] \ 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

622 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
3683  623 
\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs) > \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

624 
\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)"; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

625 
by (hyp_subst_tac 1); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

627 
by (REPEAT_FIRST (rtac impI)); 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

628 
(*ServerResume, by unicity of PMS*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

629 
by (blast_tac (!claset addSEs [MPair_parts] 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

630 
addDs [Spy_not_see_PMS, 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

631 
Notes_Crypt_parts_spies, 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

632 
Notes_master_imp_Crypt_PMS, unique_PMS]) 4); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

633 
(*ServerFinished, by unicity of PMS (10 seconds)*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

634 
by (blast_tac (!claset addSEs [MPair_parts] 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

635 
addDs [Spy_not_see_PMS, 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

636 
Notes_Crypt_parts_spies, 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

637 
Says_imp_spies RS parts.Inj, 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

638 
unique_PMS]) 3); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

639 
(*ClientCertKeyEx*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

641 
(*Fake: the Spy doesn't have the critical session key!*) 
3683  642 
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

645 
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

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

647 

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

648 

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

649 
(*** Protocol goal: if B receives any message encrypted with clientK 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

651 
assumed here; B cannot verify it. But if the message is 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

654 
goal thy 
3683  655 
"!!evs. [ evs : tls; A ~: bad; B ~: bad ] \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

656 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
3683  657 
\ Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) > \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

658 
\ Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs"; 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

660 
by (REPEAT_FIRST (rtac impI)); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

661 
(*ClientCertKeyEx*) 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

663 
(*Fake: the Spy doesn't have the critical session key!*) 
3683  664 
by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

666 
not_parts_not_analz]) 2); 
3474  667 
by (Fake_parts_insert_tac 1); 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

668 
(*ClientResume: by unicity of PMS*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

669 
by (blast_tac (!claset delrules [conjI] 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

670 
addSEs [MPair_parts] 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

671 
addSDs [Notes_master_imp_Notes_PMS] 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

672 
addDs [good_Notes_unique_PMS]) 2); 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

673 
(*ClientFinished: by unicity of PMS*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

674 
by (blast_tac (!claset delrules [conjI] 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

675 
addSEs [MPair_parts] 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

677 
qed_spec_mp "TrustClientMsg"; 
3506  678 

679 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

680 

5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

681 
(*** Protocol goal: if B receives ClientFinished, and if B is able to 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

682 
check a CertVerify from A, then A has used the quoted 
3506  683 
values XA, XB, etc. Even this one requires A to be uncompromised. 
684 
***) 

685 
goal thy 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

686 
"!!evs. [ Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \ 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

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

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

689 
\ Says A'' B (Crypt (priK A) \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

691 
\ : set evs; \ 
3683  692 
\ evs : tls; A ~: bad; B ~: bad ] \ 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

694 
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify] 
3683  695 
addDs [Says_imp_spies RS parts.Inj]) 1); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

696 
qed "AuthClientFinished"; 