author  paulson 
Tue, 16 Sep 1997 14:40:01 +0200  
changeset 3676  cbaec955056b 
parent 3672  56e4365a0c99 
child 3677  f2569416d18b 
permissions  rwrr 
3474  1 
(* Title: HOL/Auth/TLS 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

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

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

7 
This protocol is essentially the same as SSL 3.0. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

8 

56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

9 
Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

10 
Allen, Transport Layer Security Working Group, 21 May 1997, 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

11 
INTERNETDRAFT draftietftlsprotocol03.txt. Section numbers below refer 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

12 
to that memo. 
3474  13 

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. 

17 

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. 

20 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

21 
The model assumes that no fraudulent certificates are present, but it does 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

22 
assume that some private keys are to the spy. 
3474  23 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

24 
REMARK. The event "Notes A {Agent B, Nonce PMS}" appears in ClientCertKeyEx, 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

25 
CertVerify, ClientFinished to record that A knows M. It is a note from A to 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

26 
herself. Nobody else can see it. In ClientCertKeyEx, the Spy can substitute 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

27 
his own certificate for A's, but he cannot replace A's note by one for himself. 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

28 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

29 
The Note event avoids a weakness in the publickey model. Each 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

30 
agent's state is recorded as the trace of messages. When the true client (A) 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

31 
invents PMS, he encrypts PMS with B's public key before sending it. The model 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

32 
does not distinguish the original occurrence of such a message from a replay. 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

33 

d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

34 
In the sharedkey model, the ability to encrypt implies the ability to 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

35 
decrypt, so the problem does not arise. 
3474  36 
*) 
37 

38 
TLS = Public + 

39 

40 
consts 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

41 
(*Pseudorandom function of Section 5*) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

42 
PRF :: "nat*nat*nat => nat" 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

43 

56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

44 
(*Client, server write keys implicitly include the MAC secrets.*) 
3474  45 
clientK, serverK :: "nat*nat*nat => key" 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

46 

3500  47 
certificate :: "[agent,key] => msg" 
48 

49 
defs 

50 
certificate_def 

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

3474  52 

53 
rules 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

54 
inj_PRF "inj PRF" 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

55 

3474  56 
(*clientK is collisionfree and makes symmetric keys*) 
57 
inj_clientK "inj clientK" 

58 
isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*) 

59 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

60 
(*serverK is similar*) 
3474  61 
inj_serverK "inj serverK" 
62 
isSym_serverK "isSymKey (serverK x)" (*server write keys are symmetric*) 

63 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

64 
(*Clashes with pubK and priK are impossible, but this axiom is needed.*) 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

65 
clientK_range "range clientK <= Compl (range serverK)" 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

66 

3474  67 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

68 
consts tls :: event list set 
3474  69 
inductive tls 
70 
intrs 

71 
Nil (*Initial trace is empty*) 

72 
"[]: tls" 

73 

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

75 
"[ evs: tls; B ~= Spy; 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

76 
X: synth (analz (sees Spy evs)) ] 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

77 
==> Says Spy B X # evs : tls" 
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

78 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

79 
SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

80 
"[ evsSK: tls; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

81 
Says Spy B {Nonce NA, Nonce NB, Nonce M} : set evsSK ] 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

82 
==> Says Spy B { Nonce (PRF(M,NA,NB)), 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

83 
Key (clientK(NA,NB,M)), 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

84 
Key (serverK(NA,NB,M)) } # evsSK : tls" 
3474  85 

86 
ClientHello 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

87 
(*(7.4.1.2) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

88 
XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS. 
3474  89 
It is uninterpreted but will be confirmed in the FINISHED messages. 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

90 
NA is CLIENT RANDOM, while SID is SESSION_ID. 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

91 
UNIX TIME is omitted because the protocol doesn't use it. 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

92 
May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

93 
while MASTER SECRET is 48 byptes*) 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

94 
"[ evsCH: tls; A ~= B; Nonce NA ~: used evsCH; NA ~: range PRF ] 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

95 
==> Says A B {Agent A, Nonce NA, Number SID, Number XA} 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

96 
# evsCH : tls" 
3474  97 

98 
ServerHello 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

99 
(*7.4.1.3 of the TLS InternetDraft 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

100 
XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

101 
SERVER CERTIFICATE (7.4.2) is always present. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

102 
CERTIFICATE_REQUEST (7.4.4) is implied.*) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

103 
"[ evsSH: tls; A ~= B; Nonce NB ~: used evsSH; NB ~: range PRF; 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

104 
Says A' B {Agent A, Nonce NA, Number SID, Number XA} 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

105 
: set evsSH ] 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

106 
==> Says B A {Nonce NB, Number SID, Number XB, 
3500  107 
certificate B (pubK B)} 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

108 
# evsSH : tls" 
3474  109 

110 
ClientCertKeyEx 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

111 
(*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7). 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

112 
The client, A, chooses PMS, the PREMASTER SECRET. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

113 
She encrypts PMS using the supplied KB, which ought to be pubK B. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

114 
We assume PMS ~: range PRF because a clash betweem the PMS 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

115 
and another MASTER SECRET is highly unlikely (even though 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

116 
both items have the same length, 48 bytes). 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

117 
The Note event records in the trace that she knows PMS 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

118 
(see REMARK at top).*) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

119 
"[ evsCX: tls; A ~= B; Nonce PMS ~: used evsCX; PMS ~: range PRF; 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

120 
Says B' A {Nonce NB, Number SID, Number XB, certificate B KB} 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

121 
: set evsCX ] 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

122 
==> Says A B {certificate A (pubK A), Crypt KB (Nonce PMS)} 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

123 
# Notes A {Agent B, Nonce PMS} 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

124 
# evsCX : tls" 
3474  125 

126 
CertVerify 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

127 
(*The optional CERTIFICATE VERIFY (7.4.8) message contains the 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

128 
specific components listed in the security analysis, F.1.1.2. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

129 
It adds the premastersecret, which is also essential! 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

130 
Checking the signature, which is the only use of A's certificate, 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

131 
assures B of A's presence*) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

132 
"[ evsCV: tls; A ~= B; 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

133 
Says B' A {Nonce NB, Number SID, Number XB, certificate B KB} 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

134 
: set evsCV; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

135 
Notes A {Agent B, Nonce PMS} : set evsCV ] 
3474  136 
==> Says A B (Crypt (priK A) 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

137 
(Hash{Nonce NB, certificate B KB, Nonce PMS})) 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

138 
# evsCV : tls" 
3474  139 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

140 
(*Finally come the FINISHED messages (7.4.8), confirming XA and XB 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

141 
among other things. The mastersecret is PRF(PMS,NA,NB). 
3474  142 
Either party may sent its message first.*) 
143 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

144 
(*The occurrence of Notes A {Agent B, Nonce PMS} stops the 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

145 
rule's applying when the Spy has satisfied the "Says A B" by 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

146 
repaying messages sent by the true client; in that case, the 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

147 
Spy does not know PMS and could not sent CLIENT FINISHED. One 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

148 
could simply put A~=Spy into the rule, but one should not 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

149 
expect the spy to be wellbehaved.*) 
3474  150 
ClientFinished 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

151 
"[ evsCF: tls; 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

152 
Says A B {Agent A, Nonce NA, Number SID, Number XA} 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

153 
: set evsCF; 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

154 
Says B' A {Nonce NB, Number SID, Number XB, certificate B KB} 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

155 
: set evsCF; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

156 
Notes A {Agent B, Nonce PMS} : set evsCF; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

157 
M = PRF(PMS,NA,NB) ] 
3474  158 
==> Says A B (Crypt (clientK(NA,NB,M)) 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

159 
(Hash{Nonce M, Number SID, 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

160 
Nonce NA, Number XA, Agent A, 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

161 
Nonce NB, Number XB, Agent B})) 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

162 
# evsCF : tls" 
3474  163 

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

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

165 
two messages originate from the same source. *) 
3474  166 
ServerFinished 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

167 
"[ evsSF: tls; 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

168 
Says A' B {Agent A, Nonce NA, Number SID, Number XA} 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

169 
: set evsSF; 
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

170 
Says B A {Nonce NB, Number SID, Number XB, 
3500  171 
certificate B (pubK B)} 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

172 
: set evsSF; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

173 
Says A'' B {certificate A KA, Crypt (pubK B) (Nonce PMS)} 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

174 
: set evsSF; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

175 
M = PRF(PMS,NA,NB) ] 
3474  176 
==> Says B A (Crypt (serverK(NA,NB,M)) 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

177 
(Hash{Nonce M, Number SID, 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

178 
Nonce NA, Number XA, Agent A, 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

179 
Nonce NB, Number XB, Agent B})) 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

180 
# evsSF : tls" 
3474  181 

182 
(**Oops message??**) 

183 

184 
end 