97 --{*sessionK never clashes with a long-term symmetric key |
97 --{*sessionK never clashes with a long-term symmetric key |
98 (they don't exist in TLS anyway)*} |
98 (they don't exist in TLS anyway)*} |
99 sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A" |
99 sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A" |
100 |
100 |
101 |
101 |
102 consts tls :: "event list set" |
102 inductive_set tls :: "event list set" |
103 inductive tls |
103 where |
104 intros |
|
105 Nil: --{*The initial, empty trace*} |
104 Nil: --{*The initial, empty trace*} |
106 "[] \<in> tls" |
105 "[] \<in> tls" |
107 |
106 |
108 Fake: --{*The Spy may say anything he can say. The sender field is correct, |
107 | Fake: --{*The Spy may say anything he can say. The sender field is correct, |
109 but agents don't use that information.*} |
108 but agents don't use that information.*} |
110 "[| evsf \<in> tls; X \<in> synth (analz (spies evsf)) |] |
109 "[| evsf \<in> tls; X \<in> synth (analz (spies evsf)) |] |
111 ==> Says Spy B X # evsf \<in> tls" |
110 ==> Says Spy B X # evsf \<in> tls" |
112 |
111 |
113 SpyKeys: --{*The spy may apply @{term PRF} and @{term sessionK} |
112 | SpyKeys: --{*The spy may apply @{term PRF} and @{term sessionK} |
114 to available nonces*} |
113 to available nonces*} |
115 "[| evsSK \<in> tls; |
114 "[| evsSK \<in> tls; |
116 {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |] |
115 {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |] |
117 ==> Notes Spy {| Nonce (PRF(M,NA,NB)), |
116 ==> Notes Spy {| Nonce (PRF(M,NA,NB)), |
118 Key (sessionK((NA,NB,M),role)) |} # evsSK \<in> tls" |
117 Key (sessionK((NA,NB,M),role)) |} # evsSK \<in> tls" |
119 |
118 |
120 ClientHello: |
119 | ClientHello: |
121 --{*(7.4.1.2) |
120 --{*(7.4.1.2) |
122 PA represents @{text CLIENT_VERSION}, @{text CIPHER_SUITES} and @{text COMPRESSION_METHODS}. |
121 PA represents @{text CLIENT_VERSION}, @{text CIPHER_SUITES} and @{text COMPRESSION_METHODS}. |
123 It is uninterpreted but will be confirmed in the FINISHED messages. |
122 It is uninterpreted but will be confirmed in the FINISHED messages. |
124 NA is CLIENT RANDOM, while SID is @{text SESSION_ID}. |
123 NA is CLIENT RANDOM, while SID is @{text SESSION_ID}. |
125 UNIX TIME is omitted because the protocol doesn't use it. |
124 UNIX TIME is omitted because the protocol doesn't use it. |
127 28 bytes while MASTER SECRET is 48 bytes*} |
126 28 bytes while MASTER SECRET is 48 bytes*} |
128 "[| evsCH \<in> tls; Nonce NA \<notin> used evsCH; NA \<notin> range PRF |] |
127 "[| evsCH \<in> tls; Nonce NA \<notin> used evsCH; NA \<notin> range PRF |] |
129 ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|} |
128 ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|} |
130 # evsCH \<in> tls" |
129 # evsCH \<in> tls" |
131 |
130 |
132 ServerHello: |
131 | ServerHello: |
133 --{*7.4.1.3 of the TLS Internet-Draft |
132 --{*7.4.1.3 of the TLS Internet-Draft |
134 PB represents @{text CLIENT_VERSION}, @{text CIPHER_SUITE} and @{text COMPRESSION_METHOD}. |
133 PB represents @{text CLIENT_VERSION}, @{text CIPHER_SUITE} and @{text COMPRESSION_METHOD}. |
135 SERVER CERTIFICATE (7.4.2) is always present. |
134 SERVER CERTIFICATE (7.4.2) is always present. |
136 @{text CERTIFICATE_REQUEST} (7.4.4) is implied.*} |
135 @{text CERTIFICATE_REQUEST} (7.4.4) is implied.*} |
137 "[| evsSH \<in> tls; Nonce NB \<notin> used evsSH; NB \<notin> range PRF; |
136 "[| evsSH \<in> tls; Nonce NB \<notin> used evsSH; NB \<notin> range PRF; |
138 Says A' B {|Agent A, Nonce NA, Number SID, Number PA|} |
137 Says A' B {|Agent A, Nonce NA, Number SID, Number PA|} |
139 \<in> set evsSH |] |
138 \<in> set evsSH |] |
140 ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH \<in> tls" |
139 ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH \<in> tls" |
141 |
140 |
142 Certificate: |
141 | Certificate: |
143 --{*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*} |
142 --{*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*} |
144 "evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC \<in> tls" |
143 "evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC \<in> tls" |
145 |
144 |
146 ClientKeyExch: |
145 | ClientKeyExch: |
147 --{*CLIENT KEY EXCHANGE (7.4.7). |
146 --{*CLIENT KEY EXCHANGE (7.4.7). |
148 The client, A, chooses PMS, the PREMASTER SECRET. |
147 The client, A, chooses PMS, the PREMASTER SECRET. |
149 She encrypts PMS using the supplied KB, which ought to be pubK B. |
148 She encrypts PMS using the supplied KB, which ought to be pubK B. |
150 We assume @{term "PMS \<notin> range PRF"} because a clash betweem the PMS |
149 We assume @{term "PMS \<notin> range PRF"} because a clash betweem the PMS |
151 and another MASTER SECRET is highly unlikely (even though |
150 and another MASTER SECRET is highly unlikely (even though |
156 Says B' A (certificate B KB) \<in> set evsCX |] |
155 Says B' A (certificate B KB) \<in> set evsCX |] |
157 ==> Says A B (Crypt KB (Nonce PMS)) |
156 ==> Says A B (Crypt KB (Nonce PMS)) |
158 # Notes A {|Agent B, Nonce PMS|} |
157 # Notes A {|Agent B, Nonce PMS|} |
159 # evsCX \<in> tls" |
158 # evsCX \<in> tls" |
160 |
159 |
161 CertVerify: |
160 | CertVerify: |
162 --{*The optional Certificate Verify (7.4.8) message contains the |
161 --{*The optional Certificate Verify (7.4.8) message contains the |
163 specific components listed in the security analysis, F.1.1.2. |
162 specific components listed in the security analysis, F.1.1.2. |
164 It adds the pre-master-secret, which is also essential! |
163 It adds the pre-master-secret, which is also essential! |
165 Checking the signature, which is the only use of A's certificate, |
164 Checking the signature, which is the only use of A's certificate, |
166 assures B of A's presence*} |
165 assures B of A's presence*} |
172 |
171 |
173 --{*Finally come the FINISHED messages (7.4.8), confirming PA and PB |
172 --{*Finally come the FINISHED messages (7.4.8), confirming PA and PB |
174 among other things. The master-secret is PRF(PMS,NA,NB). |
173 among other things. The master-secret is PRF(PMS,NA,NB). |
175 Either party may send its message first.*} |
174 Either party may send its message first.*} |
176 |
175 |
177 ClientFinished: |
176 | ClientFinished: |
178 --{*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the |
177 --{*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the |
179 rule's applying when the Spy has satisfied the "Says A B" by |
178 rule's applying when the Spy has satisfied the "Says A B" by |
180 repaying messages sent by the true client; in that case, the |
179 repaying messages sent by the true client; in that case, the |
181 Spy does not know PMS and could not send ClientFinished. One |
180 Spy does not know PMS and could not send ClientFinished. One |
182 could simply put @{term "A\<noteq>Spy"} into the rule, but one should not |
181 could simply put @{term "A\<noteq>Spy"} into the rule, but one should not |
191 (Hash{|Number SID, Nonce M, |
190 (Hash{|Number SID, Nonce M, |
192 Nonce NA, Number PA, Agent A, |
191 Nonce NA, Number PA, Agent A, |
193 Nonce NB, Number PB, Agent B|})) |
192 Nonce NB, Number PB, Agent B|})) |
194 # evsCF \<in> tls" |
193 # evsCF \<in> tls" |
195 |
194 |
196 ServerFinished: |
195 | ServerFinished: |
197 --{*Keeping A' and A'' distinct means B cannot even check that the |
196 --{*Keeping A' and A'' distinct means B cannot even check that the |
198 two messages originate from the same source. *} |
197 two messages originate from the same source. *} |
199 "[| evsSF \<in> tls; |
198 "[| evsSF \<in> tls; |
200 Says A' B {|Agent A, Nonce NA, Number SID, Number PA|} |
199 Says A' B {|Agent A, Nonce NA, Number SID, Number PA|} |
201 \<in> set evsSF; |
200 \<in> set evsSF; |
206 (Hash{|Number SID, Nonce M, |
205 (Hash{|Number SID, Nonce M, |
207 Nonce NA, Number PA, Agent A, |
206 Nonce NA, Number PA, Agent A, |
208 Nonce NB, Number PB, Agent B|})) |
207 Nonce NB, Number PB, Agent B|})) |
209 # evsSF \<in> tls" |
208 # evsSF \<in> tls" |
210 |
209 |
211 ClientAccepts: |
210 | ClientAccepts: |
212 --{*Having transmitted ClientFinished and received an identical |
211 --{*Having transmitted ClientFinished and received an identical |
213 message encrypted with serverK, the client stores the parameters |
212 message encrypted with serverK, the client stores the parameters |
214 needed to resume this session. The "Notes A ..." premise is |
213 needed to resume this session. The "Notes A ..." premise is |
215 used to prove @{text Notes_master_imp_Crypt_PMS}.*} |
214 used to prove @{text Notes_master_imp_Crypt_PMS}.*} |
216 "[| evsCA \<in> tls; |
215 "[| evsCA \<in> tls; |
222 Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evsCA; |
221 Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evsCA; |
223 Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA |] |
222 Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA |] |
224 ==> |
223 ==> |
225 Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA \<in> tls" |
224 Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA \<in> tls" |
226 |
225 |
227 ServerAccepts: |
226 | ServerAccepts: |
228 --{*Having transmitted ServerFinished and received an identical |
227 --{*Having transmitted ServerFinished and received an identical |
229 message encrypted with clientK, the server stores the parameters |
228 message encrypted with clientK, the server stores the parameters |
230 needed to resume this session. The "Says A'' B ..." premise is |
229 needed to resume this session. The "Says A'' B ..." premise is |
231 used to prove @{text Notes_master_imp_Crypt_PMS}.*} |
230 used to prove @{text Notes_master_imp_Crypt_PMS}.*} |
232 "[| evsSA \<in> tls; |
231 "[| evsSA \<in> tls; |
239 Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evsSA; |
238 Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evsSA; |
240 Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA |] |
239 Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA |] |
241 ==> |
240 ==> |
242 Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA \<in> tls" |
241 Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA \<in> tls" |
243 |
242 |
244 ClientResume: |
243 | ClientResume: |
245 --{*If A recalls the @{text SESSION_ID}, then she sends a FINISHED |
244 --{*If A recalls the @{text SESSION_ID}, then she sends a FINISHED |
246 message using the new nonces and stored MASTER SECRET.*} |
245 message using the new nonces and stored MASTER SECRET.*} |
247 "[| evsCR \<in> tls; |
246 "[| evsCR \<in> tls; |
248 Says A B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR; |
247 Says A B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR; |
249 Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR; |
248 Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR; |
252 (Hash{|Number SID, Nonce M, |
251 (Hash{|Number SID, Nonce M, |
253 Nonce NA, Number PA, Agent A, |
252 Nonce NA, Number PA, Agent A, |
254 Nonce NB, Number PB, Agent B|})) |
253 Nonce NB, Number PB, Agent B|})) |
255 # evsCR \<in> tls" |
254 # evsCR \<in> tls" |
256 |
255 |
257 ServerResume: |
256 | ServerResume: |
258 --{*Resumption (7.3): If B finds the @{text SESSION_ID} then he can |
257 --{*Resumption (7.3): If B finds the @{text SESSION_ID} then he can |
259 send a FINISHED message using the recovered MASTER SECRET*} |
258 send a FINISHED message using the recovered MASTER SECRET*} |
260 "[| evsSR \<in> tls; |
259 "[| evsSR \<in> tls; |
261 Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR; |
260 Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR; |
262 Says B A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR; |
261 Says B A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR; |
265 (Hash{|Number SID, Nonce M, |
264 (Hash{|Number SID, Nonce M, |
266 Nonce NA, Number PA, Agent A, |
265 Nonce NA, Number PA, Agent A, |
267 Nonce NB, Number PB, Agent B|})) # evsSR |
266 Nonce NB, Number PB, Agent B|})) # evsSR |
268 \<in> tls" |
267 \<in> tls" |
269 |
268 |
270 Oops: |
269 | Oops: |
271 --{*The most plausible compromise is of an old session key. Losing |
270 --{*The most plausible compromise is of an old session key. Losing |
272 the MASTER SECRET or PREMASTER SECRET is more serious but |
271 the MASTER SECRET or PREMASTER SECRET is more serious but |
273 rather unlikely. The assumption @{term "A\<noteq>Spy"} is essential: |
272 rather unlikely. The assumption @{term "A\<noteq>Spy"} is essential: |
274 otherwise the Spy could learn session keys merely by |
273 otherwise the Spy could learn session keys merely by |
275 replaying messages!*} |
274 replaying messages!*} |