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

src/HOL/Auth/TLS.thy

author | paulson |

Tue Feb 27 16:13:23 2001 +0100 (2001-02-27) | |

changeset 11185 | 1b737b4c2108 |

parent 6284 | 147db42c1009 |

child 11230 | 756c5034f08b |

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

Some X-symbols for <notin>, <noteq>, <forall>, <exists>

Streamlining of Yahalom proofs

Removal of redundant proofs

Streamlining of Yahalom proofs

Removal of redundant proofs

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 constdefs

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

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

48 datatype role = ClientRole | ServerRole

50 consts

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

52 PRF :: "nat*nat*nat => nat"

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

55 to avoid duplicating their properties. They are distinguished by a

56 tag (not a bool, to avoid the peculiarities of if-and-only-if).

57 Session keys implicitly include MAC secrets.*)

58 sessionK :: "(nat*nat*nat) * role => key"

60 syntax

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

63 translations

64 "clientK X" == "sessionK(X, ClientRole)"

65 "serverK X" == "sessionK(X, ServerRole)"

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 "[| evsf \\<in> tls; X \\<in> synth (analz (spies evsf)) |]

86 ==> Says Spy B X # evsf \\<in> tls"

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

89 "[| evsSK \\<in> tls;

90 {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]

91 ==> Notes Spy {| Nonce (PRF(M,NA,NB)),

92 Key (sessionK((NA,NB,M),role)) |} # evsSK \\<in> tls"

94 ClientHello

95 (*(7.4.1.2)

96 PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.

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

98 NA is CLIENT RANDOM, while SID is SESSION_ID.

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

100 May assume NA \\<notin> range PRF because CLIENT RANDOM is 28 bytes

101 while MASTER SECRET is 48 bytes*)

102 "[| evsCH \\<in> tls; Nonce NA \\<notin> used evsCH; NA \\<notin> range PRF |]

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

104 # evsCH \\<in> tls"

106 ServerHello

107 (*7.4.1.3 of the TLS Internet-Draft

108 PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.

109 SERVER CERTIFICATE (7.4.2) is always present.

110 CERTIFICATE_REQUEST (7.4.4) is implied.*)

111 "[| evsSH \\<in> tls; Nonce NB \\<notin> used evsSH; NB \\<notin> range PRF;

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

113 \\<in> set evsSH |]

114 ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH \\<in> tls"

116 Certificate

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

118 "evsC \\<in> tls ==> Says B A (certificate B (pubK B)) # evsC \\<in> tls"

120 ClientKeyExch

121 (*CLIENT KEY EXCHANGE (7.4.7).

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

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

124 We assume PMS \\<notin> range PRF because a clash betweem the PMS

125 and another MASTER SECRET is highly unlikely (even though

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

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

128 (see REMARK at top). *)

129 "[| evsCX \\<in> tls; Nonce PMS \\<notin> used evsCX; PMS \\<notin> range PRF;

130 Says B' A (certificate B KB) \\<in> set evsCX |]

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

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

133 # evsCX \\<in> tls"

135 CertVerify

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

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

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

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

140 assures B of A's presence*)

141 "[| evsCV \\<in> tls;

142 Says B' A {|Nonce NB, Number SID, Number PB|} \\<in> set evsCV;

143 Notes A {|Agent B, Nonce PMS|} \\<in> set evsCV |]

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

145 # evsCV \\<in> tls"

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

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

149 Either party may sent its message first.*)

151 ClientFinished

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

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

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

155 Spy does not know PMS and could not send ClientFinished. One

156 could simply put A\\<noteq>Spy into the rule, but one should not

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

158 "[| evsCF \\<in> tls;

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

160 \\<in> set evsCF;

161 Says B' A {|Nonce NB, Number SID, Number PB|} \\<in> set evsCF;

162 Notes A {|Agent B, Nonce PMS|} \\<in> set evsCF;

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

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

165 (Hash{|Number SID, Nonce M,

166 Nonce NA, Number PA, Agent A,

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

168 # evsCF \\<in> tls"

170 ServerFinished

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

172 two messages originate from the same source. *)

173 "[| evsSF \\<in> tls;

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

175 \\<in> set evsSF;

176 Says B A {|Nonce NB, Number SID, Number PB|} \\<in> set evsSF;

177 Says A'' B (Crypt (pubK B) (Nonce PMS)) \\<in> set evsSF;

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

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

180 (Hash{|Number SID, Nonce M,

181 Nonce NA, Number PA, Agent A,

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

183 # evsSF \\<in> tls"

185 ClientAccepts

186 (*Having transmitted ClientFinished and received an identical

187 message encrypted with serverK, the client stores the parameters

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

189 used to prove Notes_master_imp_Crypt_PMS.*)

190 "[| evsCA \\<in> tls;

191 Notes A {|Agent B, Nonce PMS|} \\<in> set evsCA;

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

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

194 Nonce NA, Number PA, Agent A,

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

196 Says A B (Crypt (clientK(NA,NB,M)) X) \\<in> set evsCA;

197 Says B' A (Crypt (serverK(NA,NB,M)) X) \\<in> set evsCA |]

198 ==>

199 Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA \\<in> tls"

201 ServerAccepts

202 (*Having transmitted ServerFinished and received an identical

203 message encrypted with clientK, the server stores the parameters

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

205 used to prove Notes_master_imp_Crypt_PMS.*)

206 "[| evsSA \\<in> tls;

207 A \\<noteq> B;

208 Says A'' B (Crypt (pubK B) (Nonce PMS)) \\<in> set evsSA;

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

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

211 Nonce NA, Number PA, Agent A,

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

213 Says B A (Crypt (serverK(NA,NB,M)) X) \\<in> set evsSA;

214 Says A' B (Crypt (clientK(NA,NB,M)) X) \\<in> set evsSA |]

215 ==>

216 Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA \\<in> tls"

218 ClientResume

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

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

221 "[| evsCR \\<in> tls;

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

223 Says B' A {|Nonce NB, Number SID, Number PB|} \\<in> set evsCR;

224 Notes A {|Number SID, Agent A, Agent B, Nonce M|} \\<in> set evsCR |]

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

226 (Hash{|Number SID, Nonce M,

227 Nonce NA, Number PA, Agent A,

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

229 # evsCR \\<in> tls"

231 ServerResume

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

233 a FINISHED message using the recovered MASTER SECRET*)

234 "[| evsSR \\<in> tls;

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

236 Says B A {|Nonce NB, Number SID, Number PB|} \\<in> set evsSR;

237 Notes B {|Number SID, Agent A, Agent B, Nonce M|} \\<in> set evsSR |]

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

239 (Hash{|Number SID, Nonce M,

240 Nonce NA, Number PA, Agent A,

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

242 \\<in> tls"

244 Oops

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

246 the MASTER SECRET or PREMASTER SECRET is more serious but

247 rather unlikely. The assumption A \\<noteq> Spy is essential: otherwise

248 the Spy could learn session keys merely by replaying messages!*)

249 "[| evso \\<in> tls; A \\<noteq> Spy;

250 Says A B (Crypt (sessionK((NA,NB,M),role)) X) \\<in> set evso |]

251 ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso \\<in> tls"

253 end