author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 8054  2ce57ef2a4aa 
child 10833  c0844a30ea4e 
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 

5433  20 
AddEs spies_partsEs; 
21 
AddDs [impOfSubs analz_subset_parts]; 

22 
AddDs [impOfSubs Fake_parts_insert]; 

23 

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

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

26 

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

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

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

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

31 
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

32 

3474  33 

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

35 

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

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

40 
qed "pubK_neq_sessionK"; 
3474  41 

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

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

46 
qed "priK_neq_sessionK"; 
3474  47 

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

48 
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

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

51 

52 
(**** Protocol Proofs ****) 

53 

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

3474  56 

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

57 

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

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

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

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

65 
(*Possibility property ending with ClientAccepts.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

66 
Goal "[ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

67 
\ A ~= B ] \ 
5433  68 
\ ==> EX SID M. EX evs: tls. \ 
69 
\ Notes A {Number SID, Agent A, Agent B, Nonce M} : set evs"; 

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

71 
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

72 
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

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

75 
by (REPEAT (Blast_tac 1)); 
3474  76 
result(); 
77 

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

78 
(*And one for ServerAccepts. Either FINISHED message may come first.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

79 
Goal "[ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

80 
\ A ~= B ] \ 
5433  81 
\ ==> EX SID NA PA NB PB M. EX evs: tls. \ 
82 
\ Notes B {Number SID, Agent A, Agent B, Nonce M} : set evs"; 

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

84 
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

85 
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

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

88 
by (REPEAT (Blast_tac 1)); 
3474  89 
result(); 
90 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

92 
Goal "[ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

97 
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

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

100 
by (REPEAT (Blast_tac 1)); 
3474  101 
result(); 
102 

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

103 
(*Another one, for session resumption (both ServerResume and ClientResume) *) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

104 
Goal "[ evs0 : tls; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

105 
\ Notes A {Number SID, Agent A, Agent B, Nonce M} : set evs0; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

106 
\ Notes B {Number SID, Agent A, Agent B, Nonce M} : set evs0; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

107 
\ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ 
5433  108 
\ A ~= B ] \ 
109 
\ ==> EX NA PA NB PB X. EX evs: tls. \ 

110 
\ X = Hash{Number SID, Nonce M, \ 

111 
\ Nonce NA, Number PA, Agent A, \ 

112 
\ Nonce NB, Number PB, Agent B} & \ 

113 
\ Says A B (Crypt (clientK(NA,NB,M)) X) : set evs & \ 

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

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

116 
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

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

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

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

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

121 

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

122 

3474  123 

124 
(**** Inductive proofs about tls ****) 

125 

126 

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

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

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

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

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

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

134 
THEN 
4091  135 
fast_tac (claset() addss (simpset())) i THEN 
4686  136 
ALLGOALS Asm_simp_tac; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

137 

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

138 

3683  139 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
3474  140 
sends messages containing X! **) 
141 

3683  142 
(*Spy never sees another agent's private key! (unless it's bad at start)*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

143 
Goal "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

144 
by (parts_induct_tac 1); 
5433  145 
by (Blast_tac 1); 
3474  146 
qed "Spy_see_priK"; 
147 
Addsimps [Spy_see_priK]; 

148 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

149 
Goal "evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; 
5433  150 
by Auto_tac; 
3474  151 
qed "Spy_analz_priK"; 
152 
Addsimps [Spy_analz_priK]; 

153 

4472  154 
AddSDs [Spy_see_priK RSN (2, rev_iffD1), 
155 
Spy_analz_priK RSN (2, rev_iffD1)]; 

3474  156 

157 

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

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

159 
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

160 
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

161 
breach of security.*) 
5076  162 
Goalw [certificate_def] 
5359  163 
"[ certificate B KB : parts (spies evs); evs : tls ] ==> pubK B = KB"; 
3772  164 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

165 
by (parts_induct_tac 1); 
5433  166 
by (Blast_tac 1); 
3772  167 
qed "certificate_valid"; 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

168 

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

169 

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

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

171 
val ClientKeyExch_tac = 
3772  172 
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

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

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

175 

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

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

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

178 
ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*) 
6915  179 
ALLGOALS (asm_simp_tac (simpset() addsimps split_ifs @ pushes)) THEN 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

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

181 
Combining the two simplifier calls makes them run extremely slowly.*) 
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset

182 
ALLGOALS (asm_simp_tac (simpset() addsimps [image_eq_UN, insert_absorb])); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

183 

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

184 

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

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

186 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

187 
Goal "[ Notes A {Agent B, X} : set evs; evs : tls ] \ 
5359  188 
\ ==> 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

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

190 
by (analz_induct_tac 1); 
4091  191 
by (blast_tac (claset() addIs [parts_insertI]) 1); 
3683  192 
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

193 

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

194 
(*C may be either A or B*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

195 
Goal "[ Notes C {s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))} : set evs; \ 
5359  196 
\ evs : tls ] \ 
197 
\ ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; 

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

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

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

201 
(*Fake*) 
4091  202 
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

203 
(*Client, Server Accept*) 
5433  204 
by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies]) 1)); 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

206 

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

207 
(*Compared with the theorem above, both premise and conclusion are stronger*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

208 
Goal "[ Notes A {s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))} : set evs;\ 
5359  209 
\ evs : tls ] \ 
210 
\ ==> Notes A {Agent B, Nonce PMS} : set evs"; 

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

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

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

213 
(*ServerAccepts*) 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

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

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

216 

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

217 

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

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

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

220 
(*B can check A's signature if he has received A's certificate.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

221 
Goal "[ X : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

222 
\ X = Crypt (priK A) (Hash{nb, Agent B, pms}); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

223 
\ evs : tls; A ~: bad ] \ 
5359  224 
\ ==> Says A B X : set evs"; 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

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

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

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

230 

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

231 
(*Final version: B checks X using the distributed KA instead of priK A*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

232 
Goal "[ X : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

233 
\ X = Crypt (invKey KA) (Hash{nb, Agent B, pms}); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

234 
\ certificate A KA : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

235 
\ evs : tls; A ~: bad ] \ 
5359  236 
\ ==> Says A B X : set evs"; 
4091  237 
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

238 
qed "TrustCertVerify"; 
3474  239 

240 

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

241 
(*If CertVerify is present then A has chosen PMS.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

242 
Goal "[ Crypt (priK A) (Hash{nb, Agent B, Nonce PMS}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

243 
\ : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

244 
\ evs : tls; A ~: bad ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

250 

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

251 
(*Final version using the distributed KA instead of priK A*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

252 
Goal "[ Crypt (invKey KA) (Hash{nb, Agent B, Nonce PMS}) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

253 
\ : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

254 
\ certificate A KA : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

255 
\ evs : tls; A ~: bad ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

256 
\ ==> Notes A {Agent B, Nonce PMS} : set evs"; 
4091  257 
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

258 
qed "UseCertVerify"; 
3474  259 

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

260 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

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

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

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

267 

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

268 

5359  269 
Goal "[ Nonce (PRF (PMS,NA,NB)) : parts (spies evs); evs : tls ] \ 
270 
\ ==> Nonce PMS : parts (spies evs)"; 

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

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

272 
by (parts_induct_tac 1); 
5433  273 
(*Easy, e.g. by freshness*) 
274 
by (REPEAT (blast_tac (claset() addDs [Notes_Crypt_parts_spies]) 2)); 

275 
(*Fake*) 

276 
by (blast_tac (claset() addIs [parts_insertI]) 1); 

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

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

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

279 

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

280 

3474  281 

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

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

283 

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

284 
(*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

285 
Goal "[ Nonce PMS ~: analz (spies evs); evs : tls ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

286 
\ ==> EX B'. ALL B. \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

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

292 
by (ClientKeyExch_tac 1); 
4091  293 
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

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

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

297 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

298 
Goal "[ Crypt(pubK B) (Nonce PMS) : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

299 
\ Crypt(pubK B') (Nonce PMS) : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

300 
\ Nonce PMS ~: analz (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

301 
\ evs : tls ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

303 
by (prove_unique_tac lemma 1); 
3704  304 
qed "Crypt_unique_PMS"; 
305 

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

306 

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

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

310 
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

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

312 

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

313 
(*In A's internal Note, PMS determines A and B.*) 
5359  314 
Goal "evs : tls ==> EX A' B'. ALL A B. \ 
315 
\ 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

316 
by (parts_induct_tac 1); 
4091  317 
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

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

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

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

322 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

323 
Goal "[ Notes A {Agent B, Nonce PMS} : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

324 
\ Notes A' {Agent B', Nonce PMS} : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

325 
\ evs : tls ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

329 

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

330 

3474  331 

3772  332 
(**** Secrecy Theorems ****) 
333 

334 
(*Key compromise lemma needed to prove analz_image_keys. 

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

5359  336 
Goal "evs : tls \ 
337 
\ ==> ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ 

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

3772  339 
by (etac tls.induct 1); 
340 
by (ALLGOALS 

341 
(asm_simp_tac (analz_image_keys_ss 

5535  342 
addsimps certificate_def::keys_distinct))); 
3772  343 
(*Fake*) 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset

344 
by (spy_analz_tac 1); 
3772  345 
qed_spec_mp "analz_image_priK"; 
346 

347 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

349 
Goal "KK <= range sessionK ==> priK B ~: KK"; 
3772  350 
by (Blast_tac 1); 
351 
val range_sessionkeys_not_priK = result(); 

352 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

354 
Goal "(X : analz (G Un H)) > (X : analz H) ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

355 
\ (X : analz (G Un H)) = (X : analz H)"; 
4091  356 
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); 
3961  357 
val analz_image_keys_lemma = result(); 
3772  358 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

360 
\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

361 
\ (Nonce N : analz (spies evs))"; 
3772  362 
**) 
363 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

364 
Goal "evs : tls ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

365 
\ ALL KK. KK <= range sessionK > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

366 
\ (Nonce N : analz (Key``KK Un (spies evs))) = \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

367 
\ (Nonce N : analz (spies evs))"; 
3772  368 
by (etac tls.induct 1); 
369 
by (ClientKeyExch_tac 7); 

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

3961  371 
by (REPEAT_FIRST (rtac analz_image_keys_lemma)); 
5076  372 
by (ALLGOALS (*4.5 seconds*) 
3772  373 
(asm_simp_tac (analz_image_keys_ss 
5535  374 
addsimps split_ifs @ pushes @ 
375 
[range_sessionkeys_not_priK, 

376 
analz_image_priK, certificate_def]))); 

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

379 
by (spy_analz_tac 1); 
3772  380 
qed_spec_mp "analz_image_keys"; 
381 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

383 
Goal "evs : tls ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

384 
\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

385 
\ (Nonce N : analz (spies evs))"; 
3772  386 
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1); 
387 
qed "analz_insert_key"; 

388 
Addsimps [analz_insert_key]; 

389 

390 

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

392 

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

394 

395 

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

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

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

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

400 
Goal "[ Nonce PMS ~: parts (spies evs); \ 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

401 
\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role); \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

402 
\ evs : tls ] \ 
3772  403 
\ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))"; 
404 
by (etac rev_mp 1); 

405 
by (hyp_subst_tac 1); 

406 
by (analz_induct_tac 1); 

407 
(*SpyKeys*) 

8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset

408 
by (Blast_tac 2); 
3772  409 
(*Fake*) 
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset

410 
by (blast_tac (claset() addIs [parts_insertI]) 1); 
3772  411 
(** LEVEL 6 **) 
412 
(*Oops*) 

413 
by (REPEAT 

7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

414 
(force_tac (claset() addSDs [Notes_Crypt_parts_spies, 
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

415 
Notes_master_imp_Crypt_PMS], 
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

416 
simpset()) 1)); 
3772  417 
val lemma = result(); 
418 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

419 
Goal "[ Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) : parts (spies evs); \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

420 
\ evs : tls ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

421 
\ ==> Nonce PMS : parts (spies evs)"; 
4091  422 
by (blast_tac (claset() addDs [lemma]) 1); 
3772  423 
qed "PMS_sessionK_not_spied"; 
424 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

425 
Goal "[ Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

426 
\ : parts (spies evs); evs : tls ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

427 
\ ==> Nonce PMS : parts (spies evs)"; 
4091  428 
by (blast_tac (claset() addDs [lemma]) 1); 
3772  429 
qed "PMS_Crypt_sessionK_not_spied"; 
430 

5433  431 
(*Write keys are never sent if M (MASTER SECRET) is secure. 
432 
Converse fails; betraying M doesn't force the keys to be sent! 

3772  433 
The strong Oops condition can be weakened later by unicity reasoning, 
5433  434 
with some effort. 
435 
NO LONGER USED: see clientK_not_spied and serverK_not_spied*) 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

436 
Goal "[ ALL A. Says A Spy (Key (sessionK((NA,NB,M),role))) ~: set evs; \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

437 
\ Nonce M ~: analz (spies evs); evs : tls ] \ 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

438 
\ ==> Key (sessionK((NA,NB,M),role)) ~: parts (spies evs)"; 
3772  439 
by (etac rev_mp 1); 
440 
by (etac rev_mp 1); 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

441 
by (analz_induct_tac 1); (*5 seconds*) 
3772  442 
(*SpyKeys*) 
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset

443 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 2); 
3772  444 
(*Fake*) 
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset

445 
by (spy_analz_tac 1); 
3772  446 
qed "sessionK_not_spied"; 
447 

448 

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

449 
(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

450 
Goal "[ evs : tls; A ~: bad; B ~: bad ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

451 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

452 
\ Nonce PMS ~: analz (spies evs)"; 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

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

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

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

457 
mostly freshness reasoning*) 
4091  458 
by (REPEAT (blast_tac (claset() addSEs partsEs 
4201  459 
addDs [Notes_Crypt_parts_spies, 
460 
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

461 
(*SpyKeys*) 
4091  462 
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

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

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

465 
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

466 

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

467 

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

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

469 
will stay secret.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

470 
Goal "[ evs : tls; A ~: bad; B ~: bad ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

471 
\ ==> Notes A {Agent B, Nonce PMS} : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

472 
\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)"; 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

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

474 
(*ClientAccepts and ServerAccepts: because PMS was already visible*) 
4091  475 
by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
4201  476 
Says_imp_spies RS analz.Inj, 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
6284
diff
changeset

477 
Notes_imp_knows_Spy RS analz.Inj]) 6)); 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

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

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

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

482 
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

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

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

485 
(*ServerHello and ClientKeyExch: mostly freshness reasoning*) 
4091  486 
by (REPEAT (blast_tac (claset() addSEs partsEs 
4201  487 
addDs [Notes_Crypt_parts_spies, 
488 
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

489 
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

490 

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

491 

3704  492 
(*** Weakening the Oops conditions for leakage of clientK ***) 
493 

5433  494 
(*If A created PMS then nobody else (except the Spy in replays) 
495 
would send a message using a clientK generated from that PMS.*) 

496 
Goal "[ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \ 

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

498 
\ evs : tls; A' ~= Spy ] \ 

499 
\ ==> A = A'"; 

500 
by (etac rev_mp 1); 

501 
by (etac rev_mp 1); 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

502 
by (analz_induct_tac 1); 
3711  503 
by (ALLGOALS Clarify_tac); 
3704  504 
(*ClientFinished, ClientResume: by unicity of PMS*) 
505 
by (REPEAT 

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

508 
(*ClientKeyExch*) 
4472  509 
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied, 
510 
Says_imp_spies RS parts.Inj]) 1); 

5433  511 
qed "Says_clientK_unique"; 
3704  512 

513 

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

5433  515 
then it is completely secure: not even in parts!*) 
516 
Goal "[ Notes A {Agent B, Nonce PMS} : set evs; \ 

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

518 
\ A ~: bad; B ~: bad; \ 

519 
\ evs : tls ] \ 

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

521 
by (etac rev_mp 1); 

522 
by (etac rev_mp 1); 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

523 
by (analz_induct_tac 1); (*4 seconds*) 
3704  524 
(*Oops*) 
5433  525 
by (blast_tac (claset() addIs [Says_clientK_unique]) 4); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

526 
(*ClientKeyExch*) 
5433  527 
by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]) 3); 
528 
(*SpyKeys*) 

529 
by (blast_tac (claset() addSEs [Spy_not_see_MS RSN (2,rev_notE)]) 2); 

530 
(*Fake*) 

531 
by (spy_analz_tac 1); 

532 
qed "clientK_not_spied"; 

3704  533 

534 

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

536 

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

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

5433  539 
Goal "[ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \ 
540 
\ Notes A {Agent B, Nonce PMS} : set evs; \ 

541 
\ evs : tls; A ~: bad; B ~: bad; B' ~= Spy ] \ 

542 
\ ==> B = B'"; 

543 
by (etac rev_mp 1); 

544 
by (etac rev_mp 1); 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

545 
by (analz_induct_tac 1); 
3711  546 
by (ALLGOALS Clarify_tac); 
3704  547 
(*ServerResume, ServerFinished: by unicity of PMS*) 
548 
by (REPEAT 

5433  549 
(blast_tac (claset() addSDs [Notes_master_imp_Crypt_PMS] 
4201  550 
addDs [Spy_not_see_PMS, 
551 
Notes_Crypt_parts_spies, 

552 
Crypt_unique_PMS]) 2)); 

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

553 
(*ClientKeyExch*) 
4472  554 
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied, 
555 
Says_imp_spies RS parts.Inj]) 1); 

5433  556 
qed "Says_serverK_unique"; 
3704  557 

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

5433  559 
then it is completely secure: not even in parts!*) 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

560 
Goal "[ Notes A {Agent B, Nonce PMS} : set evs; \ 
5433  561 
\ Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs; \ 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

562 
\ A ~: bad; B ~: bad; evs : tls ] \ 
5433  563 
\ ==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: parts (spies evs)"; 
564 
by (etac rev_mp 1); 

565 
by (etac rev_mp 1); 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

566 
by (analz_induct_tac 1); 
3704  567 
(*Oops*) 
5433  568 
by (blast_tac (claset() addIs [Says_serverK_unique]) 4); 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

569 
(*ClientKeyExch*) 
5433  570 
by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]) 3); 
571 
(*SpyKeys*) 

572 
by (blast_tac (claset() addSEs [Spy_not_see_MS RSN (2,rev_notE)]) 2); 

573 
(*Fake*) 

574 
by (spy_analz_tac 1); 

575 
qed "serverK_not_spied"; 

3704  576 

577 

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

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

579 
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

580 
to compare PA with what she originally sent. 
3474  581 
***) 
582 

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

583 
(*The mention of her name (A) in X assures A that B knows who she is.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

584 
Goal "[ X = Crypt (serverK(Na,Nb,M)) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

585 
\ (Hash{Number SID, Nonce M, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

586 
\ Nonce Na, Number PA, Agent A, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

587 
\ Nonce Nb, Number PB, Agent B}); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

588 
\ M = PRF(PMS,NA,NB); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

589 
\ evs : tls; A ~: bad; B ~: bad ] \ 
5433  590 
\ ==> Says B Spy (Key(serverK(Na,Nb,M))) ~: set evs > \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

591 
\ Notes A {Agent B, Nonce PMS} : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

593 
by (hyp_subst_tac 1); 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

594 
by (analz_induct_tac 1); (*7 seconds*) 
4091  595 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3711  596 
by (ALLGOALS Clarify_tac); 
4472  597 
(*ClientKeyExch*) 
598 
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); 

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

599 
(*Fake: the Spy doesn't have the critical session key!*) 
5433  600 
by (blast_tac (claset() addEs [serverK_not_spied RSN (2,rev_notE)]) 1); 
3474  601 
qed_spec_mp "TrustServerFinished"; 
602 

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

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

604 
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

605 
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

606 
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented 
3704  607 
to bind A's identity with PMS, then we could replace A' by A below.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

608 
Goal "[ M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad ] \ 
5433  609 
\ ==> Says B Spy (Key(serverK(Na,Nb,M))) ~: set evs > \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

610 
\ Notes A {Agent B, Nonce PMS} : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

611 
\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs) > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

613 
by (hyp_subst_tac 1); 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

614 
by (analz_induct_tac 1); (*6 seconds*) 
4091  615 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 
3711  616 
by (ALLGOALS Clarify_tac); 
3704  617 
(*ServerResume, ServerFinished: by unicity of PMS*) 
618 
by (REPEAT 

5433  619 
(blast_tac (claset() addSDs [Notes_master_imp_Crypt_PMS] 
4201  620 
addDs [Spy_not_see_PMS, 
621 
Notes_Crypt_parts_spies, 

622 
Crypt_unique_PMS]) 3)); 

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

623 
(*ClientKeyExch*) 
4472  624 
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

625 
(*Fake: the Spy doesn't have the critical session key!*) 
5433  626 
by (blast_tac (claset() addEs [serverK_not_spied 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

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

628 

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

629 

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

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

631 
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

632 
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

633 
ClientFinished, then B can then check the quoted values PA, PB, etc. 
3506  634 
***) 
3704  635 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

636 
Goal "[ M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad ] \ 
5433  637 
\ ==> Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs > \ 
5359  638 
\ Notes A {Agent B, Nonce PMS} : set evs > \ 
639 
\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) > \ 

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

3772  641 
by (hyp_subst_tac 1); 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

642 
by (analz_induct_tac 1); (*6 seconds*) 
3711  643 
by (ALLGOALS Clarify_tac); 
3704  644 
(*ClientFinished, ClientResume: by unicity of PMS*) 
4091  645 
by (REPEAT (blast_tac (claset() delrules [conjI] 
4201  646 
addSDs [Notes_master_imp_Notes_PMS] 
647 
addDs [Notes_unique_PMS]) 3)); 

4472  648 
(*ClientKeyExch*) 
649 
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); 

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

650 
(*Fake: the Spy doesn't have the critical session key!*) 
5433  651 
by (blast_tac (claset() addEs [clientK_not_spied RSN (2,rev_notE)]) 1); 
652 
qed_spec_mp "TrustClientMsg"; 

3506  653 

654 

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

655 

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

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

657 
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

658 
values PA, PB, etc. Even this one requires A to be uncompromised. 
3506  659 
***) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

660 
Goal "[ M = PRF(PMS,NA,NB); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

661 
\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

662 
\ Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

663 
\ certificate A KA : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

664 
\ Says A'' B (Crypt (invKey KA) (Hash{nb, Agent B, Nonce PMS}))\ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

665 
\ : set evs; \ 
5359  666 
\ evs : tls; A ~: bad; B ~: bad ] \ 
667 
\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; 

4091  668 
by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify] 
4201  669 
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

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

671 

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

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

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

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

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

678 
(*08/9/97: loads in 189s (pike), after much reorganization, 

679 
back to 621s on albatross?*) 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

680 

147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

681 
(*10/2/99: loads in 139s (pike) 
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

682 
down to 433s on albatross*) 