summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Auth/TLS.thy

author | paulson |

Mon Sep 22 13:17:29 1997 +0200 (1997-09-22) | |

changeset 3687 | fb7d096d7884 |

parent 3686 | 4b484805b4c4 |

child 3704 | 2f99d7a0dccc |

permissions | -rw-r--r-- |

Simplified SpyKeys to use sessionK instead of clientK and serverK

Proved and used analz_insert_key, shortening scripts

Proved and used analz_insert_key, shortening scripts

1 (* Title: HOL/Auth/TLS

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1997 University of Cambridge

6 Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.

7 This protocol is essentially the same as SSL 3.0.

9 Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher

10 Allen, Transport Layer Security Working Group, 21 May 1997,

11 INTERNET-DRAFT draft-ietf-tls-protocol-03.txt. Section numbers below refer

12 to that memo.

14 An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down

15 to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a

16 global signing authority.

18 A is the client and B is the server, not to be confused with the constant

19 Server, who is in charge of all public keys.

21 The model assumes that no fraudulent certificates are present, but it does

22 assume that some private keys are to the spy.

24 REMARK. The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,

25 CertVerify, ClientFinished to record that A knows M. It is a note from A to

26 herself. Nobody else can see it. In ClientCertKeyEx, the Spy can substitute

27 his own certificate for A's, but he cannot replace A's note by one for himself.

29 The Note event avoids a weakness in the public-key model. Each

30 agent's state is recorded as the trace of messages. When the true client (A)

31 invents PMS, he encrypts PMS with B's public key before sending it. The model

32 does not distinguish the original occurrence of such a message from a replay.

33 In the shared-key model, the ability to encrypt implies the ability to

34 decrypt, so the problem does not arise.

36 Proofs would be simpler if ClientCertKeyEx included A's name within

37 Crypt KB (Nonce PMS). As things stand, there is much overlap between proofs

38 about that message (which B receives) and the stronger event

39 Notes A {|Agent B, Nonce PMS|}.

40 *)

42 TLS = Public +

44 consts

45 (*Pseudo-random function of Section 5*)

46 PRF :: "nat*nat*nat => nat"

48 (*Client, server write keys generated uniformly by function sessionK

49 to avoid duplicating their properties.

50 Theyimplicitly include the MAC secrets.*)

51 sessionK :: "(nat*nat*nat)*bool => key"

53 certificate :: "[agent,key] => msg"

55 defs

56 certificate_def

57 "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"

59 syntax

60 clientK, serverK :: "nat*nat*nat => key"

62 translations

63 "clientK (x)" == "sessionK(x,True)"

64 "serverK (x)" == "sessionK(x,False)"

66 rules

67 inj_PRF "inj PRF"

69 (*sessionK is collision-free and makes symmetric keys. Also, no clientK

70 clashes with any serverK.*)

71 inj_sessionK "inj sessionK"

73 isSym_sessionK "isSymKey (sessionK x)"

75 (*serverK is similar*)

76 inj_serverK "inj serverK"

77 isSym_serverK "isSymKey (serverK x)"

80 consts tls :: event list set

81 inductive tls

82 intrs

83 Nil (*Initial trace is empty*)

84 "[]: tls"

86 Fake (*The spy, an active attacker, MAY say anything he CAN say.*)

87 "[| evs: tls; B ~= Spy;

88 X: synth (analz (spies evs)) |]

89 ==> Says Spy B X # evs : tls"

91 SpyKeys (*The spy may apply PRF & sessionK to available nonces*)

92 "[| evsSK: tls;

93 Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]

94 ==> Says Spy B {| Nonce (PRF(M,NA,NB)),

95 Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"

97 ClientHello

98 (*(7.4.1.2)

99 XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.

100 It is uninterpreted but will be confirmed in the FINISHED messages.

101 NA is CLIENT RANDOM, while SID is SESSION_ID.

102 UNIX TIME is omitted because the protocol doesn't use it.

103 May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes

104 while MASTER SECRET is 48 byptes*)

105 "[| evsCH: tls; A ~= B; Nonce NA ~: used evsCH; NA ~: range PRF |]

106 ==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|}

107 # evsCH : tls"

109 ServerHello

110 (*7.4.1.3 of the TLS Internet-Draft

111 XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.

112 SERVER CERTIFICATE (7.4.2) is always present.

113 CERTIFICATE_REQUEST (7.4.4) is implied.*)

114 "[| evsSH: tls; A ~= B; Nonce NB ~: used evsSH; NB ~: range PRF;

115 Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}

116 : set evsSH |]

117 ==> Says B A {|Nonce NB, Number SID, Number XB,

118 certificate B (pubK B)|}

119 # evsSH : tls"

121 ClientCertKeyEx

122 (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).

123 The client, A, chooses PMS, the PREMASTER SECRET.

124 She encrypts PMS using the supplied KB, which ought to be pubK B.

125 We assume PMS ~: range PRF because a clash betweem the PMS

126 and another MASTER SECRET is highly unlikely (even though

127 both items have the same length, 48 bytes).

128 The Note event records in the trace that she knows PMS

129 (see REMARK at top). *)

130 "[| evsCX: tls; A ~= B; Nonce PMS ~: used evsCX; PMS ~: range PRF;

131 Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}

132 : set evsCX |]

133 ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}

134 # Notes A {|Agent B, Nonce PMS|}

135 # evsCX : tls"

137 CertVerify

138 (*The optional Certificate Verify (7.4.8) message contains the

139 specific components listed in the security analysis, F.1.1.2.

140 It adds the pre-master-secret, which is also essential!

141 Checking the signature, which is the only use of A's certificate,

142 assures B of A's presence*)

143 "[| evsCV: tls; A ~= B;

144 Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}

145 : set evsCV;

146 Notes A {|Agent B, Nonce PMS|} : set evsCV |]

147 ==> Says A B (Crypt (priK A)

148 (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))

149 # evsCV : tls"

151 (*Finally come the FINISHED messages (7.4.8), confirming XA and XB

152 among other things. The master-secret is PRF(PMS,NA,NB).

153 Either party may sent its message first.*)

155 ClientFinished

156 (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the

157 rule's applying when the Spy has satisfied the "Says A B" by

158 repaying messages sent by the true client; in that case, the

159 Spy does not know PMS and could not sent ClientFinished. One

160 could simply put A~=Spy into the rule, but one should not

161 expect the spy to be well-behaved.*)

162 "[| evsCF: tls;

163 Says A B {|Agent A, Nonce NA, Number SID, Number XA|}

164 : set evsCF;

165 Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|}

166 : set evsCF;

167 Notes A {|Agent B, Nonce PMS|} : set evsCF;

168 M = PRF(PMS,NA,NB) |]

169 ==> Says A B (Crypt (clientK(NA,NB,M))

170 (Hash{|Nonce M, Number SID,

171 Nonce NA, Number XA, Agent A,

172 Nonce NB, Number XB, Agent B|}))

173 # evsCF : tls"

175 ServerFinished

176 (*Keeping A' and A'' distinct means B cannot even check that the

177 two messages originate from the same source. *)

178 "[| evsSF: tls;

179 Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}

180 : set evsSF;

181 Says B A {|Nonce NB, Number SID, Number XB,

182 certificate B (pubK B)|}

183 : set evsSF;

184 Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}

185 : set evsSF;

186 M = PRF(PMS,NA,NB) |]

187 ==> Says B A (Crypt (serverK(NA,NB,M))

188 (Hash{|Nonce M, Number SID,

189 Nonce NA, Number XA, Agent A,

190 Nonce NB, Number XB, Agent B|}))

191 # evsSF : tls"

193 ClientAccepts

194 (*Having transmitted ClientFinished and received an identical

195 message encrypted with serverK, the client stores the parameters

196 needed to resume this session. The "Notes A ..." premise is

197 used to prove Notes_master_imp_Crypt_PMS.*)

198 "[| evsCA: tls;

199 Notes A {|Agent B, Nonce PMS|} : set evsCA;

200 M = PRF(PMS,NA,NB);

201 X = Hash{|Nonce M, Number SID,

202 Nonce NA, Number XA, Agent A,

203 Nonce NB, Number XB, Agent B|};

204 Says A B (Crypt (clientK(NA,NB,M)) X) : set evsCA;

205 Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]

206 ==>

207 Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA : tls"

209 ServerAccepts

210 (*Having transmitted ServerFinished and received an identical

211 message encrypted with clientK, the server stores the parameters

212 needed to resume this session. The "Says A'' B ..." premise is

213 used to prove Notes_master_imp_Crypt_PMS.*)

214 "[| evsSA: tls;

215 Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}

216 : set evsSA;

217 M = PRF(PMS,NA,NB);

218 X = Hash{|Nonce M, Number SID,

219 Nonce NA, Number XA, Agent A,

220 Nonce NB, Number XB, Agent B|};

221 Says B A (Crypt (serverK(NA,NB,M)) X) : set evsSA;

222 Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]

223 ==>

224 Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA : tls"

226 ServerResume

227 (*Resumption is described in 7.3. If B finds the SESSION_ID

228 then he sends HELLO and FINISHED messages, using the

229 previously stored MASTER SECRET*)

230 "[| evsSR: tls; A ~= B; Nonce NB ~: used evsSR; NB ~: range PRF;

231 Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;

232 Says A' B {|Agent A, Nonce NA, Number SID, Number XA|}

233 : set evsSR |]

234 ==> Says B A (Crypt (serverK(NA,NB,M))

235 (Hash{|Nonce M, Number SID,

236 Nonce NA, Number XA, Agent A,

237 Nonce NB, Number XB, Agent B|}))

238 # Says B A {|Nonce NB, Number SID, Number XB|} # evsSR : tls"

240 ClientResume

241 (*If the response to ClientHello is ServerResume then send

242 a FINISHED message using the new nonces and stored MASTER SECRET.*)

243 "[| evsCR: tls;

244 Says A B {|Agent A, Nonce NA, Number SID, Number XA|}

245 : set evsCR;

246 Says B' A {|Nonce NB, Number SID, Number XB|} : set evsCR;

247 Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evsCR |]

248 ==> Says A B (Crypt (clientK(NA,NB,M))

249 (Hash{|Nonce M, Number SID,

250 Nonce NA, Number XA, Agent A,

251 Nonce NB, Number XB, Agent B|}))

252 # evsCR : tls"

254 Oops

255 (*The most plausible compromise is of an old session key. Losing

256 the MASTER SECRET or PREMASTER SECRET is more serious but

257 rather unlikely.*)

258 "[| evso: tls; A ~= Spy;

259 Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]

260 ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso : tls"

262 end