author  paulson 
Tue, 16 Sep 1997 13:32:22 +0200  
changeset 3672  56e4365a0c99 
parent 3519  ab0a9fbed4c0 
child 3676  cbaec955056b 
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. 
90 
As an initial simplification, SESSION_ID is identified with NA 

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

91 
and reuse of sessions is not supported. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

92 
May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

93 
while MASTER SECRET is 48 byptes (6.1)*) 
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 ] 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

95 
==> Says A B {Agent A, Nonce NA, Number XA} # evsCH : tls" 
3474  96 

97 
ServerHello 

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

98 
(*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

99 
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

100 
NA is returned in its role as SESSION_ID. 
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; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

104 
Says A' B {Agent A, Nonce NA, Number XA} : set evsSH ] 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

107 
# evsSH : tls" 
3474  108 

109 
ClientCertKeyEx 

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

110 
(*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

111 
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

112 
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

113 
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

114 
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

115 
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

116 
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

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

118 
"[ evsCX: tls; A ~= B; Nonce PMS ~: used evsCX; PMS ~: range PRF; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

121 
==> 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

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

123 
# evsCX : tls" 
3474  124 

125 
CertVerify 

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

126 
(*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

127 
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

128 
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

129 
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

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

131 
"[ evsCV: tls; A ~= B; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

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

136 
(Hash{Nonce NB, certificate B KB, Nonce PMS})) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

137 
# evsCV : tls" 
3474  138 

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

139 
(*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

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

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

143 
(*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

144 
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

145 
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

146 
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

147 
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

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

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

151 
Says A B {Agent A, Nonce NA, Number XA} : set evsCF; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

154 
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

155 
M = PRF(PMS,NA,NB) ] 
3474  156 
==> Says A B (Crypt (clientK(NA,NB,M)) 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

159 
Nonce NB, Number XB, Agent B})) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

160 
# evsCF : tls" 
3474  161 

162 
(*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

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

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

166 
Says A' B {Agent A, Nonce NA, Number XA} : set evsSF; 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

170 
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

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

172 
M = PRF(PMS,NA,NB) ] 
3474  173 
==> Says B A (Crypt (serverK(NA,NB,M)) 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

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

176 
Nonce NB, Number XB, Agent B})) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

177 
# evsSF : tls" 
3474  178 

179 
(**Oops message??**) 

180 

181 
end 