author  paulson 
Tue, 11 Nov 1997 16:04:14 +0100  
changeset 4201  858b3ec2c9db 
parent 4091  771b1f6422a8 
child 4422  21238c9d363e 
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 

3474  22 
proof_timing:=true; 
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"; 
3474  38 
br notI 1; 
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"; 
3474  44 
br notI 1; 
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] 
3961  200 
addsimps (expand_ifs@pushes) 
3919  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] 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

206 
addsimps [insert_absorb] 
3919  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 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

231 
addSDs [Notes_Crypt_parts_spies]) 1)); 
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"; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

277 
be 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*) 

383 
by (spy_analz_tac 2); 

384 
(*Base*) 

385 
by (Blast_tac 1); 

386 
qed_spec_mp "analz_image_priK"; 

387 

388 

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

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

391 
by (Blast_tac 1); 

392 
val range_sessionkeys_not_priK = result(); 

393 

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

395 
goal thy 

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

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

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

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

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

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

404 
**) 

405 

406 
goal thy 

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

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

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

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

411 
by (etac tls.induct 1); 

412 
by (ClientKeyExch_tac 7); 

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

3961  414 
by (REPEAT_FIRST (rtac analz_image_keys_lemma)); 
415 
by (ALLGOALS (*15 seconds*) 

3772  416 
(asm_simp_tac (analz_image_keys_ss 
3961  417 
addsimps (expand_ifs@pushes) 
3772  418 
addsimps [range_sessionkeys_not_priK, 
419 
analz_image_priK, certificate_def]))); 

4091  420 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]))); 
3772  421 
(*Fake*) 
422 
by (spy_analz_tac 2); 

423 
(*Base*) 

424 
by (Blast_tac 1); 

425 
qed_spec_mp "analz_image_keys"; 

426 

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

428 
goal thy 

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

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

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

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

433 
qed "analz_insert_key"; 

434 
Addsimps [analz_insert_key]; 

435 

436 

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

438 

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

440 

441 

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

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

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

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

446 
goal thy 

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

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

449 
\ evs : tls ] \ 

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

451 
by (etac rev_mp 1); 

452 
by (hyp_subst_tac 1); 

453 
by (analz_induct_tac 1); 

454 
(*SpyKeys*) 

4091  455 
by (blast_tac (claset() addSEs spies_partsEs) 3); 
3772  456 
(*Fake*) 
4091  457 
by (simp_tac (simpset() addsimps [parts_insert_spies]) 2); 
3772  458 
by (Fake_parts_insert_tac 2); 
459 
(** LEVEL 6 **) 

460 
(*Oops*) 

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

3772  468 
val lemma = result(); 
469 

470 
goal thy 

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

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

4091  473 
by (blast_tac (claset() addDs [lemma]) 1); 
3772  474 
qed "PMS_sessionK_not_spied"; 
475 
bind_thm ("PMS_sessionK_spiedE", 

476 
PMS_sessionK_not_spied RSN (2,rev_notE)); 

477 

478 
goal thy 

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

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

4091  481 
by (blast_tac (claset() addDs [lemma]) 1); 
3772  482 
qed "PMS_Crypt_sessionK_not_spied"; 
483 
bind_thm ("PMS_Crypt_sessionK_spiedE", 

484 
PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)); 

485 

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

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

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

489 
with some effort.*) 

490 
goal thy 

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

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

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

494 
by (etac rev_mp 1); 

495 
by (etac rev_mp 1); 

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

497 
(*Oops*) 

498 
by (Blast_tac 4); 

499 
(*SpyKeys*) 

4091  500 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3); 
3772  501 
(*Fake*) 
502 
by (spy_analz_tac 2); 

503 
(*Base*) 

504 
by (Blast_tac 1); 

505 
qed "sessionK_not_spied"; 

506 
Addsimps [sessionK_not_spied]; 

507 

508 

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

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

510 
goal thy 
3683  511 
"!!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

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

514 
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

515 
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*) 
4091  516 
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

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

518 
mostly freshness reasoning*) 
4091  519 
by (REPEAT (blast_tac (claset() addSEs partsEs 
4201  520 
addDs [Notes_Crypt_parts_spies, 
521 
impOfSubs analz_subset_parts, 

522 
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

523 
(*SpyKeys*) 
4091  524 
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

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

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

527 
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

528 

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

529 

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

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

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

532 
goal thy 
3683  533 
"!!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

534 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
3683  535 
\ 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

536 
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

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

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

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

543 
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*) 
4091  544 
by (blast_tac (claset() addSDs [Spy_not_see_PMS, 
3683  545 
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

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

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

548 
(*ServerHello and ClientKeyExch: mostly freshness reasoning*) 
4091  549 
by (REPEAT (blast_tac (claset() addSEs partsEs 
4201  550 
addDs [Notes_Crypt_parts_spies, 
551 
impOfSubs analz_subset_parts, 

552 
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

553 
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

554 

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

555 

3704  556 
(*** Weakening the Oops conditions for leakage of clientK ***) 
557 

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

559 
using a clientK generated from that PMS.*) 

560 
goal thy 

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

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

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

564 
\ A = A'"; 

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

565 
by (analz_induct_tac 1); (*8 seconds*) 
3711  566 
by (ALLGOALS Clarify_tac); 
3704  567 
(*ClientFinished, ClientResume: by unicity of PMS*) 
568 
by (REPEAT 

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

571 
(*ClientKeyExch*) 
4091  572 
by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE] 
4201  573 
addSDs [Says_imp_spies RS parts.Inj]) 1); 
3704  574 
bind_thm ("Says_clientK_unique", 
575 
result() RSN(2,rev_mp) RSN(2,rev_mp)); 

576 

577 

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

579 
then nobody has.*) 

580 
goal thy 

581 
"!!evs. evs : tls \ 

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

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

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

585 
by (etac tls.induct 1); 

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

587 
by (ALLGOALS Simp_tac); 

3711  588 
by (ALLGOALS Clarify_tac); 
3704  589 
by (Fake_parts_insert_tac 1); 
590 
by (ALLGOALS Asm_simp_tac); 

591 
(*Oops*) 

4091  592 
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

593 
(*ClientKeyExch*) 
4091  594 
by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1); 
3704  595 
qed_spec_mp "clientK_Oops_ALL"; 
596 

597 

598 

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

600 

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

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

603 
goal thy 

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

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

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

607 
\ B = B'"; 

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

608 
by (analz_induct_tac 1); (*9 seconds*) 
3711  609 
by (ALLGOALS Clarify_tac); 
3704  610 
(*ServerResume, ServerFinished: by unicity of PMS*) 
611 
by (REPEAT 

4091  612 
(blast_tac (claset() addSEs [MPair_parts] 
4201  613 
addSDs [Notes_master_imp_Crypt_PMS, 
614 
Says_imp_spies RS parts.Inj] 

615 
addDs [Spy_not_see_PMS, 

616 
Notes_Crypt_parts_spies, 

617 
Crypt_unique_PMS]) 2)); 

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

618 
(*ClientKeyExch*) 
4091  619 
by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE] 
4201  620 
addSDs [Says_imp_spies RS parts.Inj]) 1); 
3704  621 
bind_thm ("Says_serverK_unique", 
622 
result() RSN(2,rev_mp) RSN(2,rev_mp)); 

623 

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

625 
then nobody has.*) 

626 
goal thy 

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

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

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

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

631 
by (etac tls.induct 1); 

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

633 
by (ALLGOALS Simp_tac); 

3711  634 
by (ALLGOALS Clarify_tac); 
3704  635 
by (Fake_parts_insert_tac 1); 
636 
by (ALLGOALS Asm_simp_tac); 

637 
(*Oops*) 

4091  638 
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

639 
(*ClientKeyExch*) 
4091  640 
by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1); 
3704  641 
qed_spec_mp "serverK_Oops_ALL"; 
642 

643 

644 

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

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

646 
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

647 
to compare PA with what she originally sent. 
3474  648 
***) 
649 

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

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

651 
goal thy 
3772  652 
"!!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

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

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

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

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

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

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

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

662 
by (analz_induct_tac 1); (*22 seconds*) 
4091  663 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3711  664 
(*proves ServerResume*) 
665 
by (ALLGOALS Clarify_tac); 

4201  666 
(*ClientKeyExch: blast_tac gives PROOF FAILED*) 
667 
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

668 
(*Fake: the Spy doesn't have the critical session key!*) 
3683  669 
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); 
4091  670 
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

671 
not_parts_not_analz]) 2); 
3474  672 
by (Fake_parts_insert_tac 1); 
3772  673 
val lemma = normalize_thm [RSmp] (result()); 
3704  674 

675 
(*Final version*) 

676 
goal thy 

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

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

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

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

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

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

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

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

4091  687 
by (blast_tac (claset() addIs [lemma] 
4201  688 
addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1); 
3474  689 
qed_spec_mp "TrustServerFinished"; 
690 

691 

3704  692 

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

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

694 
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

695 
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

696 
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented 
3704  697 
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

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

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

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

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

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

705 
by (analz_induct_tac 1); (*20 seconds*) 
4091  706 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 
3711  707 
by (ALLGOALS Clarify_tac); 
3704  708 
(*ServerResume, ServerFinished: by unicity of PMS*) 
709 
by (REPEAT 

4091  710 
(blast_tac (claset() addSEs [MPair_parts] 
4201  711 
addSDs [Notes_master_imp_Crypt_PMS, 
712 
Says_imp_spies RS parts.Inj] 

713 
addDs [Spy_not_see_PMS, 

714 
Notes_Crypt_parts_spies, 

715 
Crypt_unique_PMS]) 3)); 

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

716 
(*ClientKeyExch*) 
4201  717 
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

718 
(*Fake: the Spy doesn't have the critical session key!*) 
3683  719 
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); 
4091  720 
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
4201  721 
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

722 
by (Fake_parts_insert_tac 1); 
3772  723 
val lemma = normalize_thm [RSmp] (result()); 
3704  724 

725 
(*Final version*) 

726 
goal thy 

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

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

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

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

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

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

4091  733 
by (blast_tac (claset() addIs [lemma] 
3704  734 
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

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

736 

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

737 

3704  738 

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

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

740 
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

741 
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

742 
ClientFinished, then B can then check the quoted values PA, PB, etc. 
3506  743 
***) 
3704  744 

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

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

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

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

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

751 
by (hyp_subst_tac 1); 

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

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

758 
(*ClientKeyExch: blast_tac gives PROOF FAILED*) 

759 
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

760 
(*Fake: the Spy doesn't have the critical session key!*) 
3683  761 
by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1); 
4091  762 
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

763 
not_parts_not_analz]) 2); 
3474  764 
by (Fake_parts_insert_tac 1); 
3772  765 
val lemma = normalize_thm [RSmp] (result()); 
3704  766 

767 
(*Final version*) 

768 
goal thy 

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

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

779 

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

780 

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

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

782 
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

783 
values PA, PB, etc. Even this one requires A to be uncompromised. 
3506  784 
***) 
785 
goal thy 

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

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

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

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

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

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

797 

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

798 
(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) 
3711  799 
(*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

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

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

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