author  wenzelm 
Fri, 19 Dec 1997 10:28:33 +0100  
changeset 4449  df30e75f670f 
parent 4423  a129b817b58a 
child 4472  cfa3bd184bc1 
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 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset

16 
party agrees on all message components, including PA and PB (thus foiling 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

17 
rollback attacks). 
3474  18 
*) 
19 

3961  20 
open TLS; 
3704  21 

4449  22 
set proof_timing; 
3474  23 
HOL_quantifiers := false; 
24 

3772  25 
(*Automatically unfold the definition of "certificate"*) 
26 
Addsimps [certificate_def]; 

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

27 

3474  28 
(*Injectiveness of keygenerating functions*) 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

29 
AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq]; 
3474  30 

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

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

32 
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

33 

3474  34 

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

36 

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

37 
goal thy "pubK A ~= sessionK arg"; 
4423  38 
by (rtac notI 1); 
3474  39 
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); 
40 
by (Full_simp_tac 1); 

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

41 
qed "pubK_neq_sessionK"; 
3474  42 

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

43 
goal thy "priK A ~= sessionK arg"; 
4423  44 
by (rtac notI 1); 
3474  45 
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); 
46 
by (Full_simp_tac 1); 

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

47 
qed "priK_neq_sessionK"; 
3474  48 

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

49 
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

50 
AddIffs (keys_distinct @ (keys_distinct RL [not_sym])); 
3474  51 

52 

53 
(**** Protocol Proofs ****) 

54 

3772  55 
(*Possibility properties state that some traces run the protocol to the end. 
56 
Four paths and 12 rules are considered.*) 

3474  57 

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

58 

3772  59 
(** These proofs assume that the Nonce_supply nonces 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

60 
(which have the form @ N. Nonce N ~: used evs) 
3772  61 
lie outside the range of PRF. It seems reasonable, but as it is needed 
62 
only for the possibility theorems, it is not taken as an axiom. 

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

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

64 

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

65 

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

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

68 
"!!A B. [ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

69 
\ A ~= B ] \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

70 
\ ==> EX SID M. EX evs: tls. \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

71 
\ Notes A {Number SID, Agent A, Agent B, Nonce M} : set evs"; 
3474  72 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

73 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

74 
tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

77 
by (REPEAT (Blast_tac 1)); 
3474  78 
result(); 
79 

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

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

82 
"!!A B. [ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

83 
\ A ~= B ] \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

84 
\ ==> EX SID NA PA NB PB M. EX evs: tls. \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

85 
\ Notes B {Number SID, Agent A, Agent B, Nonce M} : set evs"; 
3474  86 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

87 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

88 
tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

91 
by (REPEAT (Blast_tac 1)); 
3474  92 
result(); 
93 

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

95 
goal thy 

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

96 
"!!A B. [ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

97 
\ A ~= B ] \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

98 
\ ==> EX NB PMS. EX evs: tls. \ 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset

99 
\ Says A B (Crypt (priK A) (Hash{Nonce NB, Agent B, Nonce PMS})) : set evs"; 
3474  100 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

101 
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

102 
tls.ClientKeyExch RS tls.CertVerify) 2); 
3474  103 
by possibility_tac; 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

104 
by (REPEAT (Blast_tac 1)); 
3474  105 
result(); 
106 

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

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

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

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

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

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

112 
\ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

113 
\ A ~= B ] ==> EX NA PA NB PB X. EX evs: tls. \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

114 
\ X = Hash{Number SID, Nonce M, \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

115 
\ Nonce NA, Number PA, Agent A, \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

116 
\ Nonce NB, Number PB, Agent B} & \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

117 
\ Says A B (Crypt (clientK(NA,NB,M)) X) : set evs & \ 
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

118 
\ Says B A (Crypt (serverK(NA,NB,M)) X) : set evs"; 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

119 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

120 
by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

121 
tls.ClientResume) 2); 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

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

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

125 

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

126 

3474  127 

128 
(**** Inductive proofs about tls ****) 

129 

130 
(*Nobody sends themselves messages*) 

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

132 
by (etac tls.induct 1); 

133 
by (Auto_tac()); 

134 
qed_spec_mp "not_Says_to_self"; 

135 
Addsimps [not_Says_to_self]; 

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

137 

138 

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

139 
(*Induction for regularity theorems. If induction formula has the form 
3683  140 
X ~: analz (spies evs) > ... then it shortens the proof by discarding 
141 
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

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

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

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

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

146 
THEN 
4091  147 
fast_tac (claset() addss (simpset())) i THEN 
148 
ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])); 

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

149 

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

150 

3683  151 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
3474  152 
sends messages containing X! **) 
153 

3683  154 
(*Spy never sees another agent's private key! (unless it's bad at start)*) 
3474  155 
goal thy 
3683  156 
"!!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

157 
by (parts_induct_tac 1); 
3474  158 
by (Fake_parts_insert_tac 1); 
159 
qed "Spy_see_priK"; 

160 
Addsimps [Spy_see_priK]; 

161 

162 
goal thy 

3683  163 
"!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; 
4091  164 
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); 
3474  165 
qed "Spy_analz_priK"; 
166 
Addsimps [Spy_analz_priK]; 

167 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

168 
goal thy "!!A. [ Key (priK A) : parts (spies evs); evs : tls ] ==> A:bad"; 
4091  169 
by (blast_tac (claset() addDs [Spy_see_priK]) 1); 
3474  170 
qed "Spy_see_priK_D"; 
171 

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

173 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

174 

175 

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

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

177 
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

178 
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

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

180 
goalw thy [certificate_def] 
3772  181 
"!!evs. [ certificate B KB : parts (spies evs); evs : tls ] \ 
182 
\ ==> pubK B = KB"; 

183 
by (etac rev_mp 1); 

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

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

185 
by (Fake_parts_insert_tac 1); 
3772  186 
qed "certificate_valid"; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

187 

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

188 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

189 
(*Replace key KB in ClientKeyExch by (pubK B) *) 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

190 
val ClientKeyExch_tac = 
3772  191 
forward_tac [Says_imp_spies RS parts.Inj RS certificate_valid] 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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

194 

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

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

196 
etac tls.induct i THEN 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

197 
ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*) 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

198 
ALLGOALS (asm_simp_tac 
4091  199 
(simpset() addcongs [if_weak_cong] 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

200 
addsimps (expand_ifs@pushes) 
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

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

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

203 
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

204 
ALLGOALS (asm_simp_tac 
4091  205 
(simpset() addcongs [if_weak_cong] 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

206 
addsimps [insert_absorb] 
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

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

208 

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

209 

3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset

210 
(*** Properties of items found in Notes ***) 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

211 

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

212 
goal thy "!!evs. [ Notes A {Agent B, X} : set evs; evs : tls ] \ 
3683  213 
\ ==> 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

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

215 
by (analz_induct_tac 1); 
4091  216 
by (blast_tac (claset() addIs [parts_insertI]) 1); 
3683  217 
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

218 

3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset

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

220 
goal thy 
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset

221 
"!!evs. [ Notes C {s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))} : set evs; \ 
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset

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

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

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

225 
by (parts_induct_tac 1); 
3711  226 
by (ALLGOALS Clarify_tac); 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

227 
(*Fake*) 
4091  228 
by (blast_tac (claset() addIs [parts_insertI]) 1); 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

229 
(*Client, Server Accept*) 
4091  230 
by (REPEAT (blast_tac (claset() addSEs spies_partsEs 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

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

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

233 

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

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

235 
goal thy 
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset

236 
"!!evs. [ Notes A {s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))} : set evs;\ 
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset

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

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

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

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

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

242 
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

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

244 

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

245 

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

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

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

248 
(*B can check A's signature if he has received A's certificate.*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

249 
goal thy 
3772  250 
"!!evs. [ X : parts (spies evs); \ 
251 
\ X = Crypt (priK A) (Hash{nb, Agent B, pms}); \ 

252 
\ evs : tls; A ~: bad ] \ 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

253 
\ ==> Says A B X : set evs"; 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

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

256 
by (parts_induct_tac 1); 
3474  257 
by (Fake_parts_insert_tac 1); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

258 
val lemma = result(); 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

259 

4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

260 
(*Final version: B checks X using the distributed KA instead of priK A*) 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

261 
goal thy 
3772  262 
"!!evs. [ X : parts (spies evs); \ 
263 
\ X = Crypt (invKey KA) (Hash{nb, Agent B, pms}); \ 

264 
\ certificate A KA : parts (spies evs); \ 

265 
\ evs : tls; A ~: bad ] \ 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

266 
\ ==> Says A B X : set evs"; 
4091  267 
by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

268 
qed "TrustCertVerify"; 
3474  269 

270 

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

271 
(*If CertVerify is present then A has chosen PMS.*) 
3506  272 
goal thy 
3772  273 
"!!evs. [ Crypt (priK A) (Hash{nb, Agent B, Nonce PMS}) \ 
274 
\ : parts (spies evs); \ 

275 
\ evs : tls; A ~: bad ] \ 

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

276 
\ ==> Notes A {Agent B, Nonce PMS} : set evs"; 
4423  277 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

279 
by (Fake_parts_insert_tac 1); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

280 
val lemma = result(); 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

281 

4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

282 
(*Final version using the distributed KA instead of priK A*) 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

283 
goal thy 
3772  284 
"!!evs. [ Crypt (invKey KA) (Hash{nb, Agent B, Nonce PMS}) \ 
285 
\ : parts (spies evs); \ 

286 
\ certificate A KA : parts (spies evs); \ 

287 
\ evs : tls; A ~: bad ] \ 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

288 
\ ==> Notes A {Agent B, Nonce PMS} : set evs"; 
4091  289 
by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

290 
qed "UseCertVerify"; 
3474  291 

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

292 

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

293 
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

294 
by (parts_induct_tac 1); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

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

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

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

299 

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

300 

3683  301 
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

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

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

305 
by (parts_induct_tac 1); 
4091  306 
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

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

308 
(*Six others, all trivial or by freshness*) 
4091  309 
by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies] 
4201  310 
addSEs spies_partsEs) 1)); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

313 

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

314 

3474  315 

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

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

317 

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

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

319 
goal thy 
3683  320 
"!!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

321 
\ ==> EX B'. ALL B. \ 
3683  322 
\ 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

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

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

325 
by (Fake_parts_insert_tac 1); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

326 
(*ClientKeyExch*) 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

327 
by (ClientKeyExch_tac 1); 
4091  328 
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

329 
by (expand_case_tac "PMS = ?y" 1 THEN 
4091  330 
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

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

332 

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

333 
goal thy 
3683  334 
"!!evs. [ Crypt(pubK B) (Nonce PMS) : parts (spies evs); \ 
335 
\ Crypt(pubK B') (Nonce PMS) : parts (spies evs); \ 

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

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

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

339 
by (prove_unique_tac lemma 1); 
3704  340 
qed "Crypt_unique_PMS"; 
341 

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

342 

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

343 
(** It is frustrating that we need two versions of the unicity results. 
3704  344 
But Notes A {Agent B, Nonce PMS} determines both A and B. Sometimes 
345 
we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which 

346 
determines B alone, and only if PMS is secret. 

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

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

348 

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

349 
(*In A's internal Note, PMS determines A and B.*) 
3704  350 
goal thy "!!evs. evs : tls \ 
351 
\ ==> EX A' B'. ALL A B. \ 

352 
\ Notes A {Agent B, Nonce PMS} : set evs > A=A' & B=B'"; 

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

353 
by (parts_induct_tac 1); 
4091  354 
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

356 
by (expand_case_tac "PMS = ?y" 1 THEN 
4091  357 
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

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

359 

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

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

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

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

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

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

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

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

367 

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

368 

3474  369 

3772  370 
(**** Secrecy Theorems ****) 
371 

372 
(*Key compromise lemma needed to prove analz_image_keys. 

373 
No collection of keys can help the spy get new private keys.*) 

374 
goal thy 

375 
"!!evs. evs : tls ==> \ 

376 
\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ 

377 
\ (priK B : KK  B : bad)"; 

378 
by (etac tls.induct 1); 

379 
by (ALLGOALS 

380 
(asm_simp_tac (analz_image_keys_ss 

381 
addsimps (certificate_def::keys_distinct)))); 

382 
(*Fake*) 

4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

383 
by (spy_analz_tac 1); 
3772  384 
qed_spec_mp "analz_image_priK"; 
385 

386 

387 
(*slightly speeds up the big simplification below*) 

388 
goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK"; 

389 
by (Blast_tac 1); 

390 
val range_sessionkeys_not_priK = result(); 

391 

392 
(*Lemma for the trivial direction of the ifandonlyif*) 

393 
goal thy 

394 
"!!evs. (X : analz (G Un H)) > (X : analz H) ==> \ 

395 
\ (X : analz (G Un H)) = (X : analz H)"; 

4091  396 
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); 
3961  397 
val analz_image_keys_lemma = result(); 
3772  398 

399 
(** Strangely, the following version doesn't work: 

400 
\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \ 

401 
\ (Nonce N : analz (spies evs))"; 

402 
**) 

403 

404 
goal thy 

405 
"!!evs. evs : tls ==> \ 

406 
\ ALL KK. KK <= range sessionK > \ 

407 
\ (Nonce N : analz (Key``KK Un (spies evs))) = \ 

408 
\ (Nonce N : analz (spies evs))"; 

409 
by (etac tls.induct 1); 

410 
by (ClientKeyExch_tac 7); 

411 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 

3961  412 
by (REPEAT_FIRST (rtac analz_image_keys_lemma)); 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

413 
by (ALLGOALS (*18 seconds*) 
3772  414 
(asm_simp_tac (analz_image_keys_ss 
3961  415 
addsimps (expand_ifs@pushes) 
3772  416 
addsimps [range_sessionkeys_not_priK, 
417 
analz_image_priK, certificate_def]))); 

4091  418 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]))); 
3772  419 
(*Fake*) 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

420 
by (spy_analz_tac 1); 
3772  421 
qed_spec_mp "analz_image_keys"; 
422 

423 
(*Knowing some session keys is no help in getting new nonces*) 

424 
goal thy 

425 
"!!evs. evs : tls ==> \ 

426 
\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \ 

427 
\ (Nonce N : analz (spies evs))"; 

428 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1); 

429 
qed "analz_insert_key"; 

430 
Addsimps [analz_insert_key]; 

431 

432 

433 
(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***) 

434 

435 
(** Some lemmas about session keys, comprising clientK and serverK **) 

436 

437 

438 
(*Lemma: session keys are never used if PMS is fresh. 

439 
Nonces don't have to agree, allowing session resumption. 

440 
Converse doesn't hold; revealing PMS doesn't force the keys to be sent. 

441 
THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*) 

442 
goal thy 

443 
"!!evs. [ Nonce PMS ~: parts (spies evs); \ 

444 
\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \ 

445 
\ evs : tls ] \ 

446 
\ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))"; 

447 
by (etac rev_mp 1); 

448 
by (hyp_subst_tac 1); 

449 
by (analz_induct_tac 1); 

450 
(*SpyKeys*) 

4091  451 
by (blast_tac (claset() addSEs spies_partsEs) 3); 
3772  452 
(*Fake*) 
4091  453 
by (simp_tac (simpset() addsimps [parts_insert_spies]) 2); 
3772  454 
by (Fake_parts_insert_tac 2); 
455 
(** LEVEL 6 **) 

456 
(*Oops*) 

4091  457 
by (fast_tac (claset() addSEs [MPair_parts] 
3772  458 
addDs [Says_imp_spies RS parts.Inj] 
4091  459 
addss (simpset())) 6); 
3772  460 
by (REPEAT 
4091  461 
(blast_tac (claset() addSDs [Notes_Crypt_parts_spies, 
4201  462 
Notes_master_imp_Crypt_PMS] 
463 
addSEs spies_partsEs) 1)); 

3772  464 
val lemma = result(); 
465 

466 
goal thy 

467 
"!!evs. [ Nonce PMS ~: parts (spies evs); evs : tls ] \ 

468 
\ ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)"; 

4091  469 
by (blast_tac (claset() addDs [lemma]) 1); 
3772  470 
qed "PMS_sessionK_not_spied"; 
471 
bind_thm ("PMS_sessionK_spiedE", 

472 
PMS_sessionK_not_spied RSN (2,rev_notE)); 

473 

474 
goal thy 

475 
"!!evs. [ Nonce PMS ~: parts (spies evs); evs : tls ] \ 

476 
\ ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)"; 

4091  477 
by (blast_tac (claset() addDs [lemma]) 1); 
3772  478 
qed "PMS_Crypt_sessionK_not_spied"; 
479 
bind_thm ("PMS_Crypt_sessionK_spiedE", 

480 
PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)); 

481 

482 
(*Lemma: write keys are never sent if M (MASTER SECRET) is secure. 

483 
Converse doesn't hold; betraying M doesn't force the keys to be sent! 

484 
The strong Oops condition can be weakened later by unicity reasoning, 

485 
with some effort.*) 

486 
goal thy 

487 
"!!evs. [ ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \ 

488 
\ Nonce M ~: analz (spies evs); evs : tls ] \ 

489 
\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)"; 

490 
by (etac rev_mp 1); 

491 
by (etac rev_mp 1); 

492 
by (analz_induct_tac 1); (*17 seconds*) 

493 
(*Oops*) 

494 
by (Blast_tac 4); 

495 
(*SpyKeys*) 

4091  496 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3); 
3772  497 
(*Fake*) 
498 
by (spy_analz_tac 2); 

499 
(*Base*) 

500 
by (Blast_tac 1); 

501 
qed "sessionK_not_spied"; 

502 
Addsimps [sessionK_not_spied]; 

503 

504 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

506 
goal thy 
3683  507 
"!!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

508 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
3683  509 
\ Nonce PMS ~: analz (spies evs)"; 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

511 
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*) 
4091  512 
by (REPEAT (fast_tac (claset() addss (simpset())) 6)); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

513 
(*ClientHello, ServerHello, ClientKeyExch, ServerResume: 
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

514 
mostly freshness reasoning*) 
4091  515 
by (REPEAT (blast_tac (claset() addSEs partsEs 
4201  516 
addDs [Notes_Crypt_parts_spies, 
517 
impOfSubs analz_subset_parts, 

518 
Says_imp_spies RS analz.Inj]) 3)); 

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

519 
(*SpyKeys*) 
4091  520 
by (fast_tac (claset() addss (simpset())) 2); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

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

523 
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

524 

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

525 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

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

528 
goal thy 
3683  529 
"!!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

530 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
3683  531 
\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)"; 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

533 
(*ClientAccepts and ServerAccepts: because PMS was already visible*) 
4091  534 
by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
4201  535 
Says_imp_spies RS analz.Inj, 
536 
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

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

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

539 
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*) 
4091  540 
by (blast_tac (claset() addSDs [Spy_not_see_PMS, 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

541 
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

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

543 
by (spy_analz_tac 1); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

544 
(*ServerHello and ClientKeyExch: mostly freshness reasoning*) 
4091  545 
by (REPEAT (blast_tac (claset() addSEs partsEs 
4201  546 
addDs [Notes_Crypt_parts_spies, 
547 
impOfSubs analz_subset_parts, 

548 
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

549 
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

550 

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

551 

3704  552 
(*** Weakening the Oops conditions for leakage of clientK ***) 
553 

554 
(*If A created PMS then nobody other than the Spy would send a message 

555 
using a clientK generated from that PMS.*) 

556 
goal thy 

557 
"!!evs. [ evs : tls; A' ~= Spy ] \ 

558 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 

559 
\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs > \ 

560 
\ A = A'"; 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

561 
by (analz_induct_tac 1); (*8 seconds*) 
3711  562 
by (ALLGOALS Clarify_tac); 
3704  563 
(*ClientFinished, ClientResume: by unicity of PMS*) 
564 
by (REPEAT 

4091  565 
(blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS] 
4201  566 
addIs [Notes_unique_PMS RS conjunct1]) 2)); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

567 
(*ClientKeyExch*) 
4091  568 
by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE] 
4201  569 
addSDs [Says_imp_spies RS parts.Inj]) 1); 
3704  570 
bind_thm ("Says_clientK_unique", 
571 
result() RSN(2,rev_mp) RSN(2,rev_mp)); 

572 

573 

574 
(*If A created PMS and has not leaked her clientK to the Spy, 

575 
then nobody has.*) 

576 
goal thy 

577 
"!!evs. evs : tls \ 

578 
\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs > \ 

579 
\ Notes A {Agent B, Nonce PMS} : set evs > \ 

580 
\ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) "; 

581 
by (etac tls.induct 1); 

582 
(*This roundabout proof sequence avoids looping in simplification*) 

583 
by (ALLGOALS Simp_tac); 

3711  584 
by (ALLGOALS Clarify_tac); 
3704  585 
by (Fake_parts_insert_tac 1); 
586 
by (ALLGOALS Asm_simp_tac); 

587 
(*Oops*) 

4091  588 
by (blast_tac (claset() addIs [Says_clientK_unique]) 2); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

589 
(*ClientKeyExch*) 
4091  590 
by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1); 
3704  591 
qed_spec_mp "clientK_Oops_ALL"; 
592 

593 

594 

595 
(*** Weakening the Oops conditions for leakage of serverK ***) 

596 

597 
(*If A created PMS for B, then nobody other than B or the Spy would 

598 
send a message using a serverK generated from that PMS.*) 

599 
goal thy 

600 
"!!evs. [ evs : tls; A ~: bad; B ~: bad; B' ~= Spy ] \ 

601 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 

602 
\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs > \ 

603 
\ B = B'"; 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

604 
by (analz_induct_tac 1); (*9 seconds*) 
3711  605 
by (ALLGOALS Clarify_tac); 
3704  606 
(*ServerResume, ServerFinished: by unicity of PMS*) 
607 
by (REPEAT 

4091  608 
(blast_tac (claset() addSEs [MPair_parts] 
4201  609 
addSDs [Notes_master_imp_Crypt_PMS, 
610 
Says_imp_spies RS parts.Inj] 

611 
addDs [Spy_not_see_PMS, 

612 
Notes_Crypt_parts_spies, 

613 
Crypt_unique_PMS]) 2)); 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

614 
(*ClientKeyExch*) 
4091  615 
by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE] 
4201  616 
addSDs [Says_imp_spies RS parts.Inj]) 1); 
3704  617 
bind_thm ("Says_serverK_unique", 
618 
result() RSN(2,rev_mp) RSN(2,rev_mp)); 

619 

620 
(*If A created PMS for B, and B has not leaked his serverK to the Spy, 

621 
then nobody has.*) 

622 
goal thy 

623 
"!!evs. [ evs : tls; A ~: bad; B ~: bad ] \ 

624 
\ ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs > \ 

625 
\ Notes A {Agent B, Nonce PMS} : set evs > \ 

626 
\ (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) "; 

627 
by (etac tls.induct 1); 

628 
(*This roundabout proof sequence avoids looping in simplification*) 

629 
by (ALLGOALS Simp_tac); 

3711  630 
by (ALLGOALS Clarify_tac); 
3704  631 
by (Fake_parts_insert_tac 1); 
632 
by (ALLGOALS Asm_simp_tac); 

633 
(*Oops*) 

4091  634 
by (blast_tac (claset() addIs [Says_serverK_unique]) 2); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

635 
(*ClientKeyExch*) 
4091  636 
by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1); 
3704  637 
qed_spec_mp "serverK_Oops_ALL"; 
638 

639 

640 

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

641 
(*** Protocol goals: if A receives ServerFinished, then B is present 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset

642 
and has used the quoted values PA, PB, etc. Note that it is up to A 
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset

643 
to compare PA with what she originally sent. 
3474  644 
***) 
645 

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

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

647 
goal thy 
3772  648 
"!!evs. [ X = Crypt (serverK(Na,Nb,M)) \ 
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset

649 
\ (Hash{Number SID, Nonce M, \ 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

650 
\ Nonce Na, Number PA, Agent A, \ 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

652 
\ M = PRF(PMS,NA,NB); \ 
3772  653 
\ evs : tls; A ~: bad; B ~: bad ] \ 
654 
\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) > \ 

655 
\ Notes A {Agent B, Nonce PMS} : set evs > \ 

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

657 
by (hyp_subst_tac 1); 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

658 
by (analz_induct_tac 1); (*26 seconds*) 
4091  659 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3711  660 
(*proves ServerResume*) 
661 
by (ALLGOALS Clarify_tac); 

4201  662 
(*ClientKeyExch: blast_tac gives PROOF FAILED*) 
663 
by (fast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2); 

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

664 
(*Fake: the Spy doesn't have the critical session key!*) 
3683  665 
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); 
4091  666 
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

667 
not_parts_not_analz]) 2); 
3474  668 
by (Fake_parts_insert_tac 1); 
3772  669 
val lemma = normalize_thm [RSmp] (result()); 
3704  670 

671 
(*Final version*) 

672 
goal thy 

673 
"!!evs. [ X = Crypt (serverK(Na,Nb,M)) \ 

3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset

674 
\ (Hash{Number SID, Nonce M, \ 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

675 
\ Nonce Na, Number PA, Agent A, \ 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

676 
\ Nonce Nb, Number PB, Agent B}); \ 
3704  677 
\ M = PRF(PMS,NA,NB); \ 
678 
\ X : parts (spies evs); \ 

679 
\ Notes A {Agent B, Nonce PMS} : set evs; \ 

680 
\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ 

681 
\ evs : tls; A ~: bad; B ~: bad ] \ 

682 
\ ==> Says B A X : set evs"; 

4091  683 
by (blast_tac (claset() addIs [lemma] 
4201  684 
addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1); 
3474  685 
qed_spec_mp "TrustServerFinished"; 
686 

687 

3704  688 

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

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

690 
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

691 
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

692 
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented 
3704  693 
to bind A's identity with PMS, 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

694 
goal thy 
3772  695 
"!!evs. [ M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad ] \ 
696 
\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) > \ 

697 
\ Notes A {Agent B, Nonce PMS} : set evs > \ 

3683  698 
\ 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

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

700 
by (hyp_subst_tac 1); 
3686
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset

701 
by (analz_induct_tac 1); (*20 seconds*) 
4091  702 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 
3711  703 
by (ALLGOALS Clarify_tac); 
3704  704 
(*ServerResume, ServerFinished: by unicity of PMS*) 
705 
by (REPEAT 

4091  706 
(blast_tac (claset() addSEs [MPair_parts] 
4201  707 
addSDs [Notes_master_imp_Crypt_PMS, 
708 
Says_imp_spies RS parts.Inj] 

709 
addDs [Spy_not_see_PMS, 

710 
Notes_Crypt_parts_spies, 

711 
Crypt_unique_PMS]) 3)); 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

712 
(*ClientKeyExch*) 
4201  713 
by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

714 
(*Fake: the Spy doesn't have the critical session key!*) 
3683  715 
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); 
4091  716 
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
4201  717 
not_parts_not_analz]) 2); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

718 
by (Fake_parts_insert_tac 1); 
3772  719 
val lemma = normalize_thm [RSmp] (result()); 
3704  720 

721 
(*Final version*) 

722 
goal thy 

723 
"!!evs. [ M = PRF(PMS,NA,NB); \ 

724 
\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \ 

725 
\ Notes A {Agent B, Nonce PMS} : set evs; \ 

726 
\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ 

727 
\ evs : tls; A ~: bad; B ~: bad ] \ 

728 
\ ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs"; 

4091  729 
by (blast_tac (claset() addIs [lemma] 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

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

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

732 

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

733 

3704  734 

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

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

736 
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

737 
assumed here; B cannot verify it. But if the message is 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset

738 
ClientFinished, then B can then check the quoted values PA, PB, etc. 
3506  739 
***) 
3704  740 

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

741 
goal thy 
3772  742 
"!!evs. [ M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad ] \ 
743 
\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) > \ 

744 
\ Notes A {Agent B, Nonce PMS} : set evs > \ 

745 
\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) > \ 

746 
\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; 

747 
by (hyp_subst_tac 1); 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

748 
by (analz_induct_tac 1); (*15 seconds*) 
3711  749 
by (ALLGOALS Clarify_tac); 
3704  750 
(*ClientFinished, ClientResume: by unicity of PMS*) 
4091  751 
by (REPEAT (blast_tac (claset() delrules [conjI] 
4201  752 
addSDs [Notes_master_imp_Notes_PMS] 
753 
addDs [Notes_unique_PMS]) 3)); 

754 
(*ClientKeyExch: blast_tac gives PROOF FAILED*) 

755 
by (fast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2); 

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

756 
(*Fake: the Spy doesn't have the critical session key!*) 
3683  757 
by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); 
4091  758 
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

759 
not_parts_not_analz]) 2); 
3474  760 
by (Fake_parts_insert_tac 1); 
3772  761 
val lemma = normalize_thm [RSmp] (result()); 
3704  762 

763 
(*Final version*) 

764 
goal thy 

3772  765 
"!!evs. [ M = PRF(PMS,NA,NB); \ 
766 
\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs); \ 

3704  767 
\ Notes A {Agent B, Nonce PMS} : set evs; \ 
3772  768 
\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \ 
3704  769 
\ evs : tls; A ~: bad; B ~: bad ] \ 
3772  770 
\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; 
4091  771 
by (blast_tac (claset() addIs [lemma] 
4201  772 
addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1); 
3772  773 
qed "TrustClientMsg"; 
3506  774 

775 

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

776 

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

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

778 
check a CertVerify from A, then A has used the quoted 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset

779 
values PA, PB, etc. Even this one requires A to be uncompromised. 
3506  780 
***) 
781 
goal thy 

3772  782 
"!!evs. [ M = PRF(PMS,NA,NB); \ 
783 
\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\ 

784 
\ Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \ 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

785 
\ certificate A KA : parts (spies evs); \ 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

786 
\ Says A'' B (Crypt (invKey KA) (Hash{nb, Agent B, Nonce PMS}))\ 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

787 
\ : set evs; \ 
3683  788 
\ evs : tls; A ~: bad; B ~: bad ] \ 
3772  789 
\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; 
4091  790 
by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify] 
4201  791 
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

792 
qed "AuthClientFinished"; 
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

793 

fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

794 
(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) 
3711  795 
(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*) 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

796 
(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*) 
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset

797 
(*30/9/97: loads in 476s, after removing unused theorems*) 
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset

798 
(*30/9/97: loads in 448s, after fixing ServerResume*) 