author  paulson 
Fri, 03 Oct 1997 10:32:50 +0200  
changeset 3772  6ee707a73248 
parent 3760  77f71f650433 
child 3919  c036caebfc75 
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 

3704  20 

3474  21 
open TLS; 
22 

23 
proof_timing:=true; 

24 
HOL_quantifiers := false; 

25 

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

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

28 

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

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

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

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

33 
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

34 

3474  35 

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

37 

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

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

41 
by (Full_simp_tac 1); 

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

42 
qed "pubK_neq_sessionK"; 
3474  43 

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

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

47 
by (Full_simp_tac 1); 

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

48 
qed "priK_neq_sessionK"; 
3474  49 

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

50 
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

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

53 

54 
(**** Protocol Proofs ****) 

55 

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

3474  58 

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

59 

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

61 
(which have the form @ N. Nonce N ~: used evs) 
3772  62 
lie outside the range of PRF. It seems reasonable, but as it is needed 
63 
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

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

65 

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

66 

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

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

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

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

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

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

74 
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

75 
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

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

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

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

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

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

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

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

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

88 
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

89 
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

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

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

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

96 
goal thy 

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

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

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

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

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

102 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

121 
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

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

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

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

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

126 

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

127 

3474  128 

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

130 

131 
(*Nobody sends themselves messages*) 

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

133 
by (etac tls.induct 1); 

134 
by (Auto_tac()); 

135 
qed_spec_mp "not_Says_to_self"; 

136 
Addsimps [not_Says_to_self]; 

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

138 

139 

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

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

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

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

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

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

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

148 
fast_tac (!claset addss (!simpset)) i THEN 
3704  149 
ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

150 

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

151 

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

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

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

161 
Addsimps [Spy_see_priK]; 

162 

163 
goal thy 

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

167 
Addsimps [Spy_analz_priK]; 

168 

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

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

172 

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

174 
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; 

175 

176 

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

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

178 
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

179 
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

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

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

184 
by (etac rev_mp 1); 

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

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

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

188 

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

189 

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

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

191 
val ClientKeyExch_tac = 
3772  192 
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

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

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

195 

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

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

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

198 
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

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

200 
(!simpset addcongs [if_weak_cong] 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

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 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

207 
setloop split_tac [expand_if])); 
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); 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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*) 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

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

230 
by (REPEAT (blast_tac (!claset addSEs spies_partsEs 
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"; 
3772  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"; 
3772  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); 
3683  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*) 
3683  309 
by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_spies] 
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); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

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

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 
3683  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)"; 

398 
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); 

399 
val lemma = result(); 

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])); 

414 
by (REPEAT_FIRST (rtac lemma)); 

415 
by (ALLGOALS (*24 seconds*) 

416 
(asm_simp_tac (analz_image_keys_ss 

417 
addsimps [range_sessionkeys_not_priK, 

418 
analz_image_priK, certificate_def]))); 

419 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb]))); 

420 
(*Fake*) 

421 
by (spy_analz_tac 2); 

422 
(*Base*) 

423 
by (Blast_tac 1); 

424 
qed_spec_mp "analz_image_keys"; 

425 

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

427 
goal thy 

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

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

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

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

432 
qed "analz_insert_key"; 

433 
Addsimps [analz_insert_key]; 

434 

435 

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

437 

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

439 

440 

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

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

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

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

445 
goal thy 

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

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

448 
\ evs : tls ] \ 

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

450 
by (etac rev_mp 1); 

451 
by (hyp_subst_tac 1); 

452 
by (analz_induct_tac 1); 

453 
(*SpyKeys*) 

454 
by (blast_tac (!claset addSEs spies_partsEs) 3); 

455 
(*Fake*) 

456 
by (simp_tac (!simpset addsimps [parts_insert_spies]) 2); 

457 
by (Fake_parts_insert_tac 2); 

458 
(** LEVEL 6 **) 

459 
(*Oops*) 

460 
by (fast_tac (!claset addSEs [MPair_parts] 

461 
addDs [Says_imp_spies RS parts.Inj] 

462 
addss (!simpset)) 6); 

463 
by (REPEAT 

464 
(blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 

465 
Notes_master_imp_Crypt_PMS] 

466 
addSEs spies_partsEs) 1)); 

467 
val lemma = result(); 

468 

469 
goal thy 

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

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

472 
by (blast_tac (!claset addDs [lemma]) 1); 

473 
qed "PMS_sessionK_not_spied"; 

474 
bind_thm ("PMS_sessionK_spiedE", 

475 
PMS_sessionK_not_spied RSN (2,rev_notE)); 

476 

477 
goal thy 

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

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

480 
by (blast_tac (!claset addDs [lemma]) 1); 

481 
qed "PMS_Crypt_sessionK_not_spied"; 

482 
bind_thm ("PMS_Crypt_sessionK_spiedE", 

483 
PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)); 

484 

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

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

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

488 
with some effort.*) 

489 
goal thy 

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

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

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

493 
by (etac rev_mp 1); 

494 
by (etac rev_mp 1); 

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

496 
(*Oops*) 

497 
by (Blast_tac 4); 

498 
(*SpyKeys*) 

499 
by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3); 

500 
(*Fake*) 

501 
by (spy_analz_tac 2); 

502 
(*Base*) 

503 
by (Blast_tac 1); 

504 
qed "sessionK_not_spied"; 

505 
Addsimps [sessionK_not_spied]; 

506 

507 

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

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

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

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

513 
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

514 
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*) 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

515 
by (REPEAT (fast_tac (!claset addss (!simpset)) 6)); 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

517 
mostly freshness reasoning*) 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

520 
impOfSubs analz_subset_parts, 
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

521 
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

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

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

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

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

526 
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

527 

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

528 

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

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

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

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

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

535 
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

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

537 
by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
3683  538 
Says_imp_spies RS analz.Inj, 
539 
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

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

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

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

543 
by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
3683  544 
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

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

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

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

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

550 
impOfSubs analz_subset_parts, 
3683  551 
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

552 
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

553 

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

554 

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

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

558 
using a clientK generated from that PMS.*) 

559 
goal thy 

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

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

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

563 
\ A = A'"; 

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

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

568 
(blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS] 

569 
addIs [Notes_unique_PMS RS conjunct1]) 2)); 

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

570 
(*ClientKeyExch*) 
3772  571 
by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE] 
3704  572 
addSDs [Says_imp_spies RS parts.Inj]) 1); 
573 
bind_thm ("Says_clientK_unique", 

574 
result() RSN(2,rev_mp) RSN(2,rev_mp)); 

575 

576 

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

578 
then nobody has.*) 

579 
goal thy 

580 
"!!evs. evs : tls \ 

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

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

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

584 
by (etac tls.induct 1); 

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

586 
by (ALLGOALS Simp_tac); 

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

590 
(*Oops*) 

591 
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

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

596 

597 

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

599 

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

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

602 
goal thy 

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

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

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

606 
\ B = B'"; 

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

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

611 
(blast_tac (!claset addSEs [MPair_parts] 

612 
addSDs [Notes_master_imp_Crypt_PMS, 

613 
Says_imp_spies RS parts.Inj] 

614 
addDs [Spy_not_see_PMS, 

615 
Notes_Crypt_parts_spies, 

616 
Crypt_unique_PMS]) 2)); 

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

617 
(*ClientKeyExch*) 
3772  618 
by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE] 
3704  619 
addSDs [Says_imp_spies RS parts.Inj]) 1); 
620 
bind_thm ("Says_serverK_unique", 

621 
result() RSN(2,rev_mp) RSN(2,rev_mp)); 

622 

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

624 
then nobody has.*) 

625 
goal thy 

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

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

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

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

630 
by (etac tls.induct 1); 

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

632 
by (ALLGOALS Simp_tac); 

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

636 
(*Oops*) 

637 
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

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

642 

643 

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

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

645 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

665 
(*ClientKeyExch*) 
3704  666 
by (fast_tac (*blast_tac gives PROOF FAILED*) 
3772  667 
(!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); 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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"; 

687 
by (blast_tac (!claset addIs [lemma] 

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

710 
(blast_tac (!claset addSEs [MPair_parts] 

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*) 
3704  717 
by (blast_tac 
3772  718 
(!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

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

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

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

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

726 
(*Final version*) 

727 
goal thy 

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

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

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

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

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

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

734 
by (blast_tac (!claset addIs [lemma] 

735 
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

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

737 

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

738 

3704  739 

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

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

741 
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

742 
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

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

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

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

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

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

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

752 
by (hyp_subst_tac 1); 

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

753 
by (analz_induct_tac 1); (*15 seconds*) 
3711  754 
by (ALLGOALS Clarify_tac); 
3704  755 
(*ClientFinished, ClientResume: by unicity of PMS*) 
756 
by (REPEAT (blast_tac (!claset delrules [conjI] 

757 
addSDs [Notes_master_imp_Notes_PMS] 

758 
addDs [Notes_unique_PMS]) 3)); 

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

759 
(*ClientKeyExch*) 
3704  760 
by (fast_tac (*blast_tac gives PROOF FAILED*) 
3772  761 
(!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2); 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

764 
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

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

769 
(*Final version*) 

770 
goal thy 

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

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

3772  779 
qed "TrustClientMsg"; 
3506  780 

781 

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

782 

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

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

784 
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

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

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

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

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

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

793 
\ : set evs; \ 
3683  794 
\ evs : tls; A ~: bad; B ~: bad ] \ 
3772  795 
\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

796 
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify] 
3683  797 
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

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

799 

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

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

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

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

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