author  paulson 
Wed, 21 Jul 1999 15:22:11 +0200  
changeset 7057  b9ddbb925939 
parent 6915  4ab8e31a8421 
child 8054  2ce57ef2a4aa 
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.*) 
6915  182 
ALLGOALS (asm_simp_tac (simpset() addsimps [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*) 

5433  408 
by (Blast_tac 3); 
3772  409 
(*Fake*) 
5433  410 
by (blast_tac (claset() addIs [parts_insertI]) 2); 
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*) 
4091  443 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3); 
3772  444 
(*Fake*) 
445 
by (spy_analz_tac 2); 

446 
(*Base*) 

447 
by (Blast_tac 1); 

448 
qed "sessionK_not_spied"; 

449 

450 

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

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

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

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

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

455 
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

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

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

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

463 
(*SpyKeys*) 
4091  464 
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

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

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

467 
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

468 

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

469 

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

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

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

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

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

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

475 
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

476 
(*ClientAccepts and ServerAccepts: because PMS was already visible*) 
4091  477 
by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
4201  478 
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

479 
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

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

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

482 
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*) 
4091  483 
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

484 
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

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

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

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

491 
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

492 

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

493 

3704  494 
(*** Weakening the Oops conditions for leakage of clientK ***) 
495 

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

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

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

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

501 
\ ==> A = A'"; 

502 
by (etac rev_mp 1); 

503 
by (etac rev_mp 1); 

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

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

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

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

5433  513 
qed "Says_clientK_unique"; 
3704  514 

515 

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

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

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

520 
\ A ~: bad; B ~: bad; \ 

521 
\ evs : tls ] \ 

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

523 
by (etac rev_mp 1); 

524 
by (etac rev_mp 1); 

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

525 
by (analz_induct_tac 1); (*4 seconds*) 
3704  526 
(*Oops*) 
5433  527 
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

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

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

532 
(*Fake*) 

533 
by (spy_analz_tac 1); 

534 
qed "clientK_not_spied"; 

3704  535 

536 

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

538 

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

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

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

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

544 
\ ==> B = B'"; 

545 
by (etac rev_mp 1); 

546 
by (etac rev_mp 1); 

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

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

5433  551 
(blast_tac (claset() addSDs [Notes_master_imp_Crypt_PMS] 
4201  552 
addDs [Spy_not_see_PMS, 
553 
Notes_Crypt_parts_spies, 

554 
Crypt_unique_PMS]) 2)); 

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

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

5433  558 
qed "Says_serverK_unique"; 
3704  559 

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

5433  561 
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

562 
Goal "[ Notes A {Agent B, Nonce PMS} : set evs; \ 
5433  563 
\ 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

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

567 
by (etac rev_mp 1); 

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

568 
by (analz_induct_tac 1); 
3704  569 
(*Oops*) 
5433  570 
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

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

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

575 
(*Fake*) 

576 
by (spy_analz_tac 1); 

577 
qed "serverK_not_spied"; 

3704  578 

579 

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

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

581 
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

582 
to compare PA with what she originally sent. 
3474  583 
***) 
584 

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

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

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

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

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

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

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

591 
\ evs : tls; A ~: bad; B ~: bad ] \ 
5433  592 
\ ==> 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

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

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

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

596 
by (analz_induct_tac 1); (*7 seconds*) 
4091  597 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3711  598 
by (ALLGOALS Clarify_tac); 
4472  599 
(*ClientKeyExch*) 
600 
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

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

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

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

606 
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

607 
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

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

610 
Goal "[ M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad ] \ 
5433  611 
\ ==> 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

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

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

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

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

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

5433  621 
(blast_tac (claset() addSDs [Notes_master_imp_Crypt_PMS] 
4201  622 
addDs [Spy_not_see_PMS, 
623 
Notes_Crypt_parts_spies, 

624 
Crypt_unique_PMS]) 3)); 

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

625 
(*ClientKeyExch*) 
4472  626 
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

627 
(*Fake: the Spy doesn't have the critical session key!*) 
5433  628 
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

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

630 

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

631 

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

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

633 
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

634 
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

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

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

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

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

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

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

4472  650 
(*ClientKeyExch*) 
651 
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

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

3506  655 

656 

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

657 

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

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

659 
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

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

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

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

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

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

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

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

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

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

673 

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

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

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

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

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

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

681 
back to 621s on albatross?*) 

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

682 

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

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

684 
down to 433s on albatross*) 