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

src/HOL/Auth/TLS.thy

author | paulson |

Tue Nov 11 11:16:18 1997 +0100 (1997-11-11) | |

changeset 4198 | c63639beeff1 |

parent 3759 | 3d1ac6b82b28 |

child 4421 | 88639289be39 |

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

Fixed spelling error

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 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 ClientKeyExch,

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

26 herself. Nobody else can see it. In ClientKeyExch, 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 ClientKeyExch 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 are generated uniformly by function sessionK

49 to avoid duplicating their properties. They are indexed by a further

50 natural number, not a bool, to avoid the peculiarities of if-and-only-if.

51 Session keys implicitly include MAC secrets.*)

52 sessionK :: "(nat*nat*nat)*nat => key"

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

56 defs

57 certificate_def

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

60 syntax

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

63 translations

64 "clientK (nonces)" == "sessionK(nonces,0)"

65 "serverK (nonces)" == "sessionK(nonces,1)"

67 rules

68 (*the pseudo-random function is collision-free*)

69 inj_PRF "inj PRF"

71 (*sessionK is collision-free; also, no clientK clashes with any serverK.*)

72 inj_sessionK "inj sessionK"

74 (*sessionK makes symmetric keys*)

75 isSym_sessionK "isSymKey (sessionK nonces)"

78 consts tls :: event list set

79 inductive tls

80 intrs

81 Nil (*Initial trace is empty*)

82 "[]: tls"

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

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

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

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

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

90 "[| evsSK: tls;

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

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

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

95 ClientHello

96 (*(7.4.1.2)

97 PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.

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

99 NA is CLIENT RANDOM, while SID is SESSION_ID.

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

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

102 while MASTER SECRET is 48 bytes*)

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

104 ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}

105 # evsCH : tls"

107 ServerHello

108 (*7.4.1.3 of the TLS Internet-Draft

109 PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.

110 SERVER CERTIFICATE (7.4.2) is always present.

111 CERTIFICATE_REQUEST (7.4.4) is implied.*)

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

113 Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}

114 : set evsSH |]

115 ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH : tls"

117 Certificate

118 (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)

119 "[| evsC: tls; A ~= B |]

120 ==> Says B A (certificate B (pubK B)) # evsC : tls"

122 ClientKeyExch

123 (*CLIENT KEY EXCHANGE (7.4.7).

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

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

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

127 and another MASTER SECRET is highly unlikely (even though

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

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

130 (see REMARK at top). *)

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

132 Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCX;

133 Says B'' A (certificate B KB) : set evsCX |]

134 ==> Says A B (Crypt KB (Nonce PMS))

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

136 # evsCX : tls"

138 CertVerify

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

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

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

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

143 assures B of A's presence*)

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

145 Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;

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

147 ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))

148 # evsCV : tls"

150 (*Finally come the FINISHED messages (7.4.8), confirming PA and PB

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

152 Either party may sent its message first.*)

154 ClientFinished

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

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

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

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

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

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

161 "[| evsCF: tls;

162 Says A B {|Agent A, Nonce NA, Number SID, Number PA|}

163 : set evsCF;

164 Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCF;

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

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

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

168 (Hash{|Number SID, Nonce M,

169 Nonce NA, Number PA, Agent A,

170 Nonce NB, Number PB, Agent B|}))

171 # evsCF : tls"

173 ServerFinished

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

175 two messages originate from the same source. *)

176 "[| evsSF: tls;

177 Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}

178 : set evsSF;

179 Says B A {|Nonce NB, Number SID, Number PB|} : set evsSF;

180 Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF;

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

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

183 (Hash{|Number SID, Nonce M,

184 Nonce NA, Number PA, Agent A,

185 Nonce NB, Number PB, Agent B|}))

186 # evsSF : tls"

188 ClientAccepts

189 (*Having transmitted ClientFinished and received an identical

190 message encrypted with serverK, the client stores the parameters

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

192 used to prove Notes_master_imp_Crypt_PMS.*)

193 "[| evsCA: tls;

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

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

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

197 Nonce NA, Number PA, Agent A,

198 Nonce NB, Number PB, Agent B|};

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

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

201 ==>

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

204 ServerAccepts

205 (*Having transmitted ServerFinished and received an identical

206 message encrypted with clientK, the server stores the parameters

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

208 used to prove Notes_master_imp_Crypt_PMS.*)

209 "[| evsSA: tls;

210 Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;

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

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

213 Nonce NA, Number PA, Agent A,

214 Nonce NB, Number PB, Agent B|};

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

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

217 ==>

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

220 ClientResume

221 (*If A recalls the SESSION_ID, then she sends a FINISHED message

222 using the new nonces and stored MASTER SECRET.*)

223 "[| evsCR: tls;

224 Says A B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR;

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

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

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

228 (Hash{|Number SID, Nonce M,

229 Nonce NA, Number PA, Agent A,

230 Nonce NB, Number PB, Agent B|}))

231 # evsCR : tls"

233 ServerResume

234 (*Resumption (7.3): If B finds the SESSION_ID then he can send

235 a FINISHED message using the recovered MASTER SECRET*)

236 "[| evsSR: tls;

237 Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR;

238 Says B A {|Nonce NB, Number SID, Number PB|} : set evsSR;

239 Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR |]

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

241 (Hash{|Number SID, Nonce M,

242 Nonce NA, Number PA, Agent A,

243 Nonce NB, Number PB, Agent B|})) # evsSR

244 : tls"

246 Oops

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

248 the MASTER SECRET or PREMASTER SECRET is more serious but

249 rather unlikely.*)

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

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

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

254 end