author | paulson |
Tue, 16 Sep 1997 14:40:01 +0200 | |
changeset 3676 | cbaec955056b |
parent 3672 | 56e4365a0c99 |
child 3677 | f2569416d18b |
permissions | -rw-r--r-- |
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 |
INTERNET-DRAFT draft-ietf-tls-protocol-03.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 public-key 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 shared-key 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 |
(*Pseudo-random 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 collision-free and makes symmetric keys*) |
57 |
inj_clientK "inj clientK" |
|
58 |
isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*) |
|
59 |
||
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
60 |
(*serverK is similar*) |
3474 | 61 |
inj_serverK "inj serverK" |
62 |
isSym_serverK "isSymKey (serverK x)" (*server write keys are symmetric*) |
|
63 |
||
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
64 |
(*Clashes with pubK and priK are impossible, but this axiom is needed.*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
65 |
clientK_range "range clientK <= Compl (range serverK)" |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
66 |
|
3474 | 67 |
|
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
68 |
consts tls :: event list set |
3474 | 69 |
inductive tls |
70 |
intrs |
|
71 |
Nil (*Initial trace is empty*) |
|
72 |
"[]: tls" |
|
73 |
||
74 |
Fake (*The spy, an active attacker, MAY say anything he CAN say.*) |
|
75 |
"[| evs: tls; B ~= Spy; |
|
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
76 |
X: synth (analz (sees Spy evs)) |] |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
77 |
==> Says Spy B X # evs : tls" |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
78 |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
79 |
SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*) |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
80 |
"[| evsSK: tls; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
81 |
Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |] |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
82 |
==> Says Spy B {| Nonce (PRF(M,NA,NB)), |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
83 |
Key (clientK(NA,NB,M)), |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
84 |
Key (serverK(NA,NB,M)) |} # evsSK : tls" |
3474 | 85 |
|
86 |
ClientHello |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
87 |
(*(7.4.1.2) |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
88 |
XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS. |
3474 | 89 |
It is uninterpreted but will be confirmed in the FINISHED messages. |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
90 |
NA is CLIENT RANDOM, while SID is SESSION_ID. |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
91 |
UNIX TIME is omitted because the protocol doesn't use it. |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
92 |
May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
93 |
while MASTER SECRET is 48 byptes*) |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
94 |
"[| evsCH: tls; A ~= B; Nonce NA ~: used evsCH; NA ~: range PRF |] |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
95 |
==> Says A B {|Agent A, Nonce NA, Number SID, Number XA|} |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
96 |
# evsCH : tls" |
3474 | 97 |
|
98 |
ServerHello |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
99 |
(*7.4.1.3 of the TLS Internet-Draft |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
100 |
XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD. |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
101 |
SERVER CERTIFICATE (7.4.2) is always present. |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
102 |
CERTIFICATE_REQUEST (7.4.4) is implied.*) |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
103 |
"[| evsSH: tls; A ~= B; Nonce NB ~: used evsSH; NB ~: range PRF; |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
104 |
Says A' B {|Agent A, Nonce NA, Number SID, Number XA|} |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
105 |
: set evsSH |] |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
106 |
==> Says B A {|Nonce NB, Number SID, Number XB, |
3500 | 107 |
certificate B (pubK B)|} |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
108 |
# evsSH : tls" |
3474 | 109 |
|
110 |
ClientCertKeyEx |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
111 |
(*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7). |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
112 |
The client, A, chooses PMS, the PREMASTER SECRET. |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
113 |
She encrypts PMS using the supplied KB, which ought to be pubK B. |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
114 |
We assume PMS ~: range PRF because a clash betweem the PMS |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
115 |
and another MASTER SECRET is highly unlikely (even though |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
116 |
both items have the same length, 48 bytes). |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
117 |
The Note event records in the trace that she knows PMS |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
118 |
(see REMARK at top).*) |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
119 |
"[| evsCX: tls; A ~= B; Nonce PMS ~: used evsCX; PMS ~: range PRF; |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
120 |
Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|} |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
121 |
: set evsCX |] |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
122 |
==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|} |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
123 |
# Notes A {|Agent B, Nonce PMS|} |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
124 |
# evsCX : tls" |
3474 | 125 |
|
126 |
CertVerify |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
127 |
(*The optional CERTIFICATE VERIFY (7.4.8) message contains the |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
128 |
specific components listed in the security analysis, F.1.1.2. |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
129 |
It adds the pre-master-secret, which is also essential! |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
130 |
Checking the signature, which is the only use of A's certificate, |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
131 |
assures B of A's presence*) |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
132 |
"[| evsCV: tls; A ~= B; |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
133 |
Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|} |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
134 |
: set evsCV; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
135 |
Notes A {|Agent B, Nonce PMS|} : set evsCV |] |
3474 | 136 |
==> Says A B (Crypt (priK A) |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
137 |
(Hash{|Nonce NB, certificate B KB, Nonce PMS|})) |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
138 |
# evsCV : tls" |
3474 | 139 |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
140 |
(*Finally come the FINISHED messages (7.4.8), confirming XA and XB |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
141 |
among other things. The master-secret is PRF(PMS,NA,NB). |
3474 | 142 |
Either party may sent its message first.*) |
143 |
||
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
144 |
(*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
145 |
rule's applying when the Spy has satisfied the "Says A B" by |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
146 |
repaying messages sent by the true client; in that case, the |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
147 |
Spy does not know PMS and could not sent CLIENT FINISHED. One |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
148 |
could simply put A~=Spy into the rule, but one should not |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
149 |
expect the spy to be well-behaved.*) |
3474 | 150 |
ClientFinished |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
151 |
"[| evsCF: tls; |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
152 |
Says A B {|Agent A, Nonce NA, Number SID, Number XA|} |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
153 |
: set evsCF; |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
154 |
Says B' A {|Nonce NB, Number SID, Number XB, certificate B KB|} |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
155 |
: set evsCF; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
156 |
Notes A {|Agent B, Nonce PMS|} : set evsCF; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
157 |
M = PRF(PMS,NA,NB) |] |
3474 | 158 |
==> Says A B (Crypt (clientK(NA,NB,M)) |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
159 |
(Hash{|Nonce M, Number SID, |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
160 |
Nonce NA, Number XA, Agent A, |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
161 |
Nonce NB, Number XB, Agent B|})) |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
162 |
# evsCF : tls" |
3474 | 163 |
|
164 |
(*Keeping A' and A'' distinct means B cannot even check that the |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
165 |
two messages originate from the same source. *) |
3474 | 166 |
ServerFinished |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
167 |
"[| evsSF: tls; |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
168 |
Says A' B {|Agent A, Nonce NA, Number SID, Number XA|} |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
169 |
: set evsSF; |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
170 |
Says B A {|Nonce NB, Number SID, Number XB, |
3500 | 171 |
certificate B (pubK B)|} |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
172 |
: set evsSF; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
173 |
Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|} |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
174 |
: set evsSF; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
175 |
M = PRF(PMS,NA,NB) |] |
3474 | 176 |
==> Says B A (Crypt (serverK(NA,NB,M)) |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
177 |
(Hash{|Nonce M, Number SID, |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
178 |
Nonce NA, Number XA, Agent A, |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
179 |
Nonce NB, Number XB, Agent B|})) |
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
180 |
# evsSF : tls" |
3474 | 181 |
|
182 |
(**Oops message??**) |
|
183 |
||
184 |
end |