author  paulson 
Wed, 01 Oct 1997 13:41:38 +0200  
changeset 3759  3d1ac6b82b28 
parent 3757  7524781c5c83 
child 4198  c63639beeff1 
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 

3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

6 
Inductive relation "tls" for the 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 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

24 
REMARK. The event "Notes A {Agent B, Nonce PMS}" appears in ClientKeyExch, 
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 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

26 
herself. Nobody else can see it. In ClientKeyExch, the Spy can substitute 
3515
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 
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

34 
decrypt, so the problem does not arise. 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

35 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

36 
Proofs would be simpler if ClientKeyExch included A's name within 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

37 
Crypt KB (Nonce PMS). As things stand, there is much overlap between proofs 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

38 
about that message (which B receives) and the stronger event 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

39 
Notes A {Agent B, Nonce PMS}. 
3474  40 
*) 
41 

42 
TLS = Public + 

43 

44 
consts 

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

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

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

47 

3704  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 ifandonlyif. 

51 
Session keys implicitly include MAC secrets.*) 

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

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

53 

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

56 
defs 

57 
certificate_def 

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

3474  59 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

60 
syntax 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

61 
clientK, serverK :: "nat*nat*nat => key" 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

62 

f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

63 
translations 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

64 
"clientK (nonces)" == "sessionK(nonces,0)" 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

65 
"serverK (nonces)" == "sessionK(nonces,1)" 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

66 

3474  67 
rules 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

68 
(*the pseudorandom function is collisionfree*) 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

70 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

71 
(*sessionK is collisionfree; also, no clientK clashes with any serverK.*) 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

72 
inj_sessionK "inj sessionK" 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

73 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

74 
(*sessionK makes symmetric keys*) 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

75 
isSym_sessionK "isSymKey (sessionK nonces)" 
3474  76 

77 

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

78 
consts tls :: event list set 
3474  79 
inductive tls 
80 
intrs 

81 
Nil (*Initial trace is empty*) 

82 
"[]: tls" 

83 

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

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

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

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

88 

3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

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

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

91 
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

92 
==> Says Spy B { Nonce (PRF(M,NA,NB)), 
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

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

95 
ClientHello 

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

96 
(*(7.4.1.2) 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

97 
PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS. 
3474  98 
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

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

100 
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

101 
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

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

103 
"[ evsCH: tls; A ~= B; Nonce NA ~: used evsCH; NA ~: range PRF ] 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

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

105 
# evsCH : tls" 
3474  106 

107 
ServerHello 

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

108 
(*7.4.1.3 of the TLS InternetDraft 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

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

110 
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

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

112 
"[ evsSH: tls; A ~= B; Nonce NB ~: used evsSH; NB ~: range PRF; 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

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

114 
: set evsSH ] 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

117 
Certificate 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

118 
(*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*) 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

119 
"[ evsC: tls; A ~= B ] 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

120 
==> Says B A (certificate B (pubK B)) # evsC : tls" 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

121 

4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

122 
ClientKeyExch 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

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

124 
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

125 
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

126 
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

127 
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

128 
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

129 
The Note event records in the trace that she knows PMS 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

131 
"[ evsCX: tls; A ~= B; Nonce PMS ~: used evsCX; PMS ~: range PRF; 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

132 
Says B' A {Nonce NB, Number SID, Number PB} : set evsCX; 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

133 
Says B'' A (certificate B KB) : set evsCX ] 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

134 
==> Says A B (Crypt KB (Nonce PMS)) 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

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

136 
# evsCX : tls" 
3474  137 

138 
CertVerify 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

139 
(*The optional Certificate Verify (7.4.8) message contains the 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

140 
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

141 
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

142 
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

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

144 
"[ evsCV: tls; A ~= B; 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

145 
Says B' A {Nonce NB, Number SID, Number PB} : set evsCV; 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

146 
Notes A {Agent B, Nonce PMS} : set evsCV ] 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

147 
==> Says A B (Crypt (priK A) (Hash{Nonce NB, Agent B, Nonce PMS})) 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

148 
# evsCV : tls" 
3474  149 

3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

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

151 
among other things. The mastersecret is PRF(PMS,NA,NB). 
3474  152 
Either party may sent its message first.*) 
153 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

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

156 
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

157 
repaying messages sent by the true client; in that case, the 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

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

159 
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

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

161 
"[ evsCF: tls; 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

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

163 
: set evsCF; 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

164 
Says B' A {Nonce NB, Number SID, Number PB} : set evsCF; 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

165 
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

166 
M = PRF(PMS,NA,NB) ] 
3474  167 
==> Says A B (Crypt (clientK(NA,NB,M)) 
3757
7524781c5c83
Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents:
3745
diff
changeset

168 
(Hash{Number SID, Nonce M, 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

169 
Nonce NA, Number PA, Agent A, 
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

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

171 
# evsCF : tls" 
3474  172 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

173 
ServerFinished 
3474  174 
(*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

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

176 
"[ evsSF: tls; 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

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

178 
: set evsSF; 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

179 
Says B A {Nonce NB, Number SID, Number PB} : set evsSF; 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

180 
Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF; 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

181 
M = PRF(PMS,NA,NB) ] 
3474  182 
==> Says B A (Crypt (serverK(NA,NB,M)) 
3757
7524781c5c83
Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents:
3745
diff
changeset

183 
(Hash{Number SID, Nonce M, 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

184 
Nonce NA, Number PA, Agent A, 
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

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

186 
# evsSF : tls" 
3474  187 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

188 
ClientAccepts 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

189 
(*Having transmitted ClientFinished and received an identical 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

190 
message encrypted with serverK, the client stores the parameters 
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

191 
needed to resume this session. The "Notes A ..." premise is 
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

192 
used to prove Notes_master_imp_Crypt_PMS.*) 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

193 
"[ evsCA: tls; 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

194 
Notes A {Agent B, Nonce PMS} : set evsCA; 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

195 
M = PRF(PMS,NA,NB); 
3757
7524781c5c83
Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents:
3745
diff
changeset

196 
X = Hash{Number SID, Nonce M, 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

197 
Nonce NA, Number PA, Agent A, 
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

198 
Nonce NB, Number PB, Agent B}; 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

199 
Says A B (Crypt (clientK(NA,NB,M)) X) : set evsCA; 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

200 
Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA ] 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

201 
==> 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

202 
Notes A {Number SID, Agent A, Agent B, Nonce M} # evsCA : tls" 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

203 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

204 
ServerAccepts 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

205 
(*Having transmitted ServerFinished and received an identical 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

206 
message encrypted with clientK, the server stores the parameters 
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

207 
needed to resume this session. The "Says A'' B ..." premise is 
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

208 
used to prove Notes_master_imp_Crypt_PMS.*) 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

209 
"[ evsSA: tls; 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

210 
Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA; 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

211 
M = PRF(PMS,NA,NB); 
3757
7524781c5c83
Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents:
3745
diff
changeset

212 
X = Hash{Number SID, Nonce M, 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

213 
Nonce NA, Number PA, Agent A, 
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

214 
Nonce NB, Number PB, Agent B}; 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

215 
Says B A (Crypt (serverK(NA,NB,M)) X) : set evsSA; 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

216 
Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA ] 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

217 
==> 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

218 
Notes B {Number SID, Agent A, Agent B, Nonce M} # evsSA : tls" 
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

219 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

220 
ClientResume 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

221 
(*If A recalls the SESSION_ID, then she sends a FINISHED message 
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

222 
using the new nonces and stored MASTER SECRET.*) 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

223 
"[ evsCR: tls; 
3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

224 
Says A B {Agent A, Nonce NA, Number SID, Number PA}: set evsCR; 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

225 
Says B' A {Nonce NB, Number SID, Number PB} : set evsCR; 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

226 
Notes A {Number SID, Agent A, Agent B, Nonce M} : set evsCR ] 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

227 
==> Says A B (Crypt (clientK(NA,NB,M)) 
3757
7524781c5c83
Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson
parents:
3745
diff
changeset

228 
(Hash{Number SID, Nonce M, 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

229 
Nonce NA, Number PA, Agent A, 
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

230 
Nonce NB, Number PB, Agent B})) 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

231 
# evsCR : tls" 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

232 

3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

233 
ServerResume 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

234 
(*Resumption (7.3): If B finds the SESSION_ID then he can send 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

235 
a FINISHED message using the recovered MASTER SECRET*) 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

236 
"[ evsSR: tls; 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

237 
Says A' B {Agent A, Nonce NA, Number SID, Number PA}: set evsSR; 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

238 
Says B A {Nonce NB, Number SID, Number PB} : set evsSR; 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

239 
Notes B {Number SID, Agent A, Agent B, Nonce M} : set evsSR ] 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

240 
==> Says B A (Crypt (serverK(NA,NB,M)) 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

241 
(Hash{Number SID, Nonce M, 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

242 
Nonce NA, Number PA, Agent A, 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

243 
Nonce NB, Number PB, Agent B})) # evsSR 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

244 
: tls" 
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

245 

3686
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset

246 
Oops 
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset

247 
(*The most plausible compromise is of an old session key. Losing 
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset

248 
the MASTER SECRET or PREMASTER SECRET is more serious but 
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset

249 
rather unlikely.*) 
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset

250 
"[ evso: tls; A ~= Spy; 
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset

251 
Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso ] 
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset

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

254 
end 