author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 6284  147db42c1009 
child 11185  1b737b4c2108 
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 

5653
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset

44 
constdefs 
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset

45 
certificate :: "[agent,key] => msg" 
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset

46 
"certificate A KA == Crypt (priK Server) {Agent A, Key KA}" 
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset

47 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

48 
datatype role = ClientRole  ServerRole 
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

49 

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

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

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

53 

3704  54 
(*Client, server write keys are generated uniformly by function sessionK 
5653
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset

55 
to avoid duplicating their properties. They are distinguished by a 
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset

56 
tag (not a bool, to avoid the peculiarities of ifandonlyif). 
3704  57 
Session keys implicitly include MAC secrets.*) 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

58 
sessionK :: "(nat*nat*nat) * role => key" 
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 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

64 
"clientK X" == "sessionK(X, ClientRole)" 
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

65 
"serverK X" == "sessionK(X, ServerRole)" 
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.*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

85 
"[ evs: tls; X: synth (analz (spies evs)) ] 
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

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

87 

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

88 
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

89 
"[ evsSK: tls; 
5359  90 
{Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) ] 
4421
88639289be39
Simplified SpyKeys and ClientKeyExch as suggested by James Margetson
paulson
parents:
4198
diff
changeset

91 
==> Notes Spy { Nonce (PRF(M,NA,NB)), 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

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

94 
ClientHello 

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

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

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

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

99 
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

100 
May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes 
4198  101 
while MASTER SECRET is 48 bytes*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

102 
"[ evsCH: tls; 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

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

104 
# evsCH : tls" 
3474  105 

106 
ServerHello 

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

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

108 
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

109 
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

110 
CERTIFICATE_REQUEST (7.4.4) is implied.*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

111 
"[ evsSH: tls; 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

112 
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

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

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

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

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

117 
(*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*) 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

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

119 

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

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

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

122 
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

123 
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

124 
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

125 
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

126 
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

127 
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

128 
(see REMARK at top). *) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

129 
"[ evsCX: tls; Nonce PMS ~: used evsCX; PMS ~: range PRF; 
4421
88639289be39
Simplified SpyKeys and ClientKeyExch as suggested by James Margetson
paulson
parents:
4198
diff
changeset

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

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

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

133 
# evsCX : tls" 
3474  134 

135 
CertVerify 

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

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

137 
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

138 
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

139 
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

140 
assures B of A's presence*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

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

142 
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

143 
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

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

145 
# evsCV : tls" 
3474  146 

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

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

148 
among other things. The mastersecret is PRF(PMS,NA,NB). 
3474  149 
Either party may sent its message first.*) 
150 

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

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

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

153 
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

154 
repaying messages sent by the true client; in that case, the 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

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

156 
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

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

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

159 
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

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

161 
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

162 
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

163 
M = PRF(PMS,NA,NB) ] 
3474  164 
==> 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

165 
(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

166 
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

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

168 
# evsCF : tls" 
3474  169 

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

170 
ServerFinished 
3474  171 
(*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

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

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

174 
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

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

176 
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

177 
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

178 
M = PRF(PMS,NA,NB) ] 
3474  179 
==> 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

180 
(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

181 
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

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

183 
# evsSF : tls" 
3474  184 

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

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

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

187 
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

188 
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

189 
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

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

191 
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

192 
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

193 
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

194 
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

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

196 
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

197 
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

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

199 
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

200 

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

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

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

203 
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

204 
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

205 
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

206 
"[ evsSA: tls; 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

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

208 
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

209 
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

210 
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

211 
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

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

213 
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

214 
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

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

216 
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

217 

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

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

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

220 
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

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

222 
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

223 
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

224 
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

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

226 
(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

227 
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

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

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

230 

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

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

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

233 
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

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

235 
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

236 
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

237 
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

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

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

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

241 
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

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

243 

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

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

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

246 
the MASTER SECRET or PREMASTER SECRET is more serious but 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

247 
rather unlikely. The assumption A ~= Spy is essential: otherwise 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

248 
the Spy could learn session keys merely by replaying messages!*) 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset

249 
"[ evso: tls; A ~= Spy; 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

250 
Says A B (Crypt (sessionK((NA,NB,M),role)) X) : set evso ] 
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

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

253 
end 