39 |
39 |
40 consts |
40 consts |
41 (*Pseudo-random function of Section 5*) |
41 (*Pseudo-random function of Section 5*) |
42 PRF :: "nat*nat*nat => nat" |
42 PRF :: "nat*nat*nat => nat" |
43 |
43 |
44 (*Client, server write keys implicitly include the MAC secrets.*) |
44 (*Client, server write keys generated uniformly by function sessionK |
45 clientK, serverK :: "nat*nat*nat => key" |
45 to avoid duplicating their properties. |
|
46 Theyimplicitly include the MAC secrets.*) |
|
47 sessionK :: "bool*nat*nat*nat => key" |
46 |
48 |
47 certificate :: "[agent,key] => msg" |
49 certificate :: "[agent,key] => msg" |
48 |
50 |
49 defs |
51 defs |
50 certificate_def |
52 certificate_def |
51 "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}" |
53 "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}" |
52 |
54 |
|
55 syntax |
|
56 clientK, serverK :: "nat*nat*nat => key" |
|
57 |
|
58 translations |
|
59 "clientK x" == "sessionK(True,x)" |
|
60 "serverK x" == "sessionK(False,x)" |
|
61 |
53 rules |
62 rules |
54 inj_PRF "inj PRF" |
63 inj_PRF "inj PRF" |
55 |
64 |
56 (*clientK is collision-free and makes symmetric keys*) |
65 (*sessionK is collision-free and makes symmetric keys*) |
57 inj_clientK "inj clientK" |
66 inj_sessionK "inj sessionK" |
58 isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*) |
67 |
|
68 isSym_sessionK "isSymKey (sessionK x)" |
59 |
69 |
60 (*serverK is similar*) |
70 (*serverK is similar*) |
61 inj_serverK "inj serverK" |
71 inj_serverK "inj serverK" |
62 isSym_serverK "isSymKey (serverK x)" (*server write keys are symmetric*) |
72 isSym_serverK "isSymKey (serverK x)" |
63 |
73 |
64 (*Clashes with pubK and priK are impossible, but this axiom is needed.*) |
74 (*Clashes with pubK and priK are impossible, but this axiom is needed.*) |
65 clientK_range "range clientK <= Compl (range serverK)" |
75 clientK_range "range clientK <= Compl (range serverK)" |
66 |
76 |
67 |
77 |
177 (Hash{|Nonce M, Number SID, |
187 (Hash{|Nonce M, Number SID, |
178 Nonce NA, Number XA, Agent A, |
188 Nonce NA, Number XA, Agent A, |
179 Nonce NB, Number XB, Agent B|})) |
189 Nonce NB, Number XB, Agent B|})) |
180 # evsSF : tls" |
190 # evsSF : tls" |
181 |
191 |
|
192 (*Having transmitted CLIENT FINISHED and received an identical |
|
193 message encrypted with serverK, the client stores the parameters |
|
194 needed to resume this session.*) |
|
195 ClientAccepts |
|
196 "[| evsCA: tls; |
|
197 Notes A {|Agent B, Nonce PMS|} : set evsCA; |
|
198 M = PRF(PMS,NA,NB); |
|
199 X = Hash{|Nonce M, Number SID, |
|
200 Nonce NA, Number XA, Agent A, |
|
201 Nonce NB, Number XB, Agent B|}; |
|
202 Says A B (Crypt (clientK(NA,NB,M)) X) : set evsCA; |
|
203 Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |] |
|
204 ==> |
|
205 Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA : tls" |
|
206 |
|
207 (*Having transmitted SERVER FINISHED and received an identical |
|
208 message encrypted with clientK, the server stores the parameters |
|
209 needed to resume this session.*) |
|
210 ServerAccepts |
|
211 "[| evsSA: tls; |
|
212 Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|} |
|
213 : set evsSA; |
|
214 M = PRF(PMS,NA,NB); |
|
215 X = Hash{|Nonce M, Number SID, |
|
216 Nonce NA, Number XA, Agent A, |
|
217 Nonce NB, Number XB, Agent B|}; |
|
218 Says B A (Crypt (serverK(NA,NB,M)) X) : set evsSA; |
|
219 Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |] |
|
220 ==> |
|
221 Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA : tls" |
|
222 |
182 (**Oops message??**) |
223 (**Oops message??**) |
183 |
224 |
184 end |
225 end |