author | paulson |
Fri, 25 Apr 2003 11:18:14 +0200 | |
changeset 13922 | 75ae4244a596 |
parent 13507 | febb8e5d2a9d |
child 13956 | 8fe7e12290e1 |
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 |
||
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 |
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 |
|
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 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 |
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
|
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 |
||
11287 | 42 |
theory TLS = Public: |
3474 | 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" |
13922 | 46 |
"certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}" |
47 |
||
48 |
text{*TLS apparently does not require separate keypairs for encryption and |
|
49 |
signature. Therefore, we formalize signature as encryption using the |
|
50 |
private encryption key.*} |
|
5653
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset
|
51 |
|
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
52 |
datatype role = ClientRole | ServerRole |
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
53 |
|
3474 | 54 |
consts |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
55 |
(*Pseudo-random function of Section 5*) |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
56 |
PRF :: "nat*nat*nat => nat" |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
57 |
|
3704 | 58 |
(*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
|
59 |
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
|
60 |
tag (not a bool, to avoid the peculiarities of if-and-only-if). |
3704 | 61 |
Session keys implicitly include MAC secrets.*) |
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
62 |
sessionK :: "(nat*nat*nat) * role => key" |
3474 | 63 |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
64 |
syntax |
11287 | 65 |
clientK :: "nat*nat*nat => key" |
66 |
serverK :: "nat*nat*nat => key" |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
67 |
|
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
68 |
translations |
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
69 |
"clientK X" == "sessionK(X, ClientRole)" |
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
70 |
"serverK X" == "sessionK(X, ServerRole)" |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
71 |
|
11287 | 72 |
axioms |
13922 | 73 |
--{*the pseudo-random function is collision-free*} |
11287 | 74 |
inj_PRF: "inj PRF" |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
75 |
|
13922 | 76 |
--{*sessionK is collision-free; also, no clientK clashes with any serverK.*} |
11287 | 77 |
inj_sessionK: "inj sessionK" |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
78 |
|
13922 | 79 |
--{*sessionK makes symmetric keys*} |
11287 | 80 |
isSym_sessionK: "sessionK nonces \<in> symKeys" |
3474 | 81 |
|
13922 | 82 |
--{*sessionK never clashes with a long-term symmetric key |
83 |
(they don't exist in TLS anyway)*} |
|
84 |
sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A" |
|
85 |
||
3474 | 86 |
|
11287 | 87 |
consts tls :: "event list set" |
3474 | 88 |
inductive tls |
11287 | 89 |
intros |
13922 | 90 |
Nil: --{*The initial, empty trace*} |
11287 | 91 |
"[] \<in> tls" |
3474 | 92 |
|
13922 | 93 |
Fake: --{*The Spy may say anything he can say. The sender field is correct, |
94 |
but agents don't use that information.*} |
|
11287 | 95 |
"[| evsf \<in> tls; X \<in> synth (analz (spies evsf)) |] |
96 |
==> Says Spy B X # evsf \<in> tls" |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
97 |
|
13922 | 98 |
SpyKeys: --{*The spy may apply PRF & sessionK to available nonces*} |
11287 | 99 |
"[| evsSK \<in> tls; |
5359 | 100 |
{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
|
101 |
==> Notes Spy {| Nonce (PRF(M,NA,NB)), |
11287 | 102 |
Key (sessionK((NA,NB,M),role)) |} # evsSK \<in> tls" |
3474 | 103 |
|
11287 | 104 |
ClientHello: |
13922 | 105 |
--{*(7.4.1.2) |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
106 |
PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS. |
3474 | 107 |
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
|
108 |
NA is CLIENT RANDOM, while SID is SESSION_ID. |
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset
|
109 |
UNIX TIME is omitted because the protocol doesn't use it. |
11287 | 110 |
May assume NA \<notin> range PRF because CLIENT RANDOM is 28 bytes |
13922 | 111 |
while MASTER SECRET is 48 bytes*} |
11287 | 112 |
"[| evsCH \<in> tls; Nonce NA \<notin> used evsCH; NA \<notin> 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|} |
11287 | 114 |
# evsCH \<in> tls" |
3474 | 115 |
|
11287 | 116 |
ServerHello: |
13922 | 117 |
--{*7.4.1.3 of the TLS Internet-Draft |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
118 |
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
|
119 |
SERVER CERTIFICATE (7.4.2) is always present. |
13922 | 120 |
CERTIFICATE_REQUEST (7.4.4) is implied.*} |
11287 | 121 |
"[| evsSH \<in> tls; Nonce NB \<notin> used evsSH; NB \<notin> range PRF; |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
122 |
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|} |
11287 | 123 |
\<in> set evsSH |] |
124 |
==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH \<in> tls" |
|
3474 | 125 |
|
11287 | 126 |
Certificate: |
13922 | 127 |
--{*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*} |
11287 | 128 |
"evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC \<in> tls" |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
129 |
|
11287 | 130 |
ClientKeyExch: |
13922 | 131 |
--{*CLIENT KEY EXCHANGE (7.4.7). |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
132 |
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
|
133 |
She encrypts PMS using the supplied KB, which ought to be pubK B. |
11287 | 134 |
We assume PMS \<notin> range PRF because a clash betweem the PMS |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
The Note event records in the trace that she knows PMS |
13922 | 138 |
(see REMARK at top). *} |
11287 | 139 |
"[| evsCX \<in> tls; Nonce PMS \<notin> used evsCX; PMS \<notin> range PRF; |
140 |
Says B' A (certificate B KB) \<in> set evsCX |] |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
141 |
==> 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
|
142 |
# Notes A {|Agent B, Nonce PMS|} |
11287 | 143 |
# evsCX \<in> tls" |
3474 | 144 |
|
11287 | 145 |
CertVerify: |
13922 | 146 |
--{*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
|
147 |
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
|
148 |
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
|
149 |
Checking the signature, which is the only use of A's certificate, |
13922 | 150 |
assures B of A's presence*} |
11287 | 151 |
"[| evsCV \<in> tls; |
152 |
Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCV; |
|
153 |
Notes A {|Agent B, Nonce PMS|} \<in> set evsCV |] |
|
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
154 |
==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) |
11287 | 155 |
# evsCV \<in> tls" |
3474 | 156 |
|
13922 | 157 |
--{*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
|
158 |
among other things. The master-secret is PRF(PMS,NA,NB). |
13922 | 159 |
Either party may send its message first.*} |
3474 | 160 |
|
11287 | 161 |
ClientFinished: |
13922 | 162 |
--{*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
|
163 |
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
|
164 |
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
|
165 |
Spy does not know PMS and could not send ClientFinished. One |
11287 | 166 |
could simply put A\<noteq>Spy into the rule, but one should not |
13922 | 167 |
expect the spy to be well-behaved.*} |
11287 | 168 |
"[| evsCF \<in> tls; |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
169 |
Says A B {|Agent A, Nonce NA, Number SID, Number PA|} |
11287 | 170 |
\<in> set evsCF; |
171 |
Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCF; |
|
172 |
Notes A {|Agent B, Nonce PMS|} \<in> set evsCF; |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
173 |
M = PRF(PMS,NA,NB) |] |
3474 | 174 |
==> 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
|
175 |
(Hash{|Number SID, Nonce M, |
11287 | 176 |
Nonce NA, Number PA, Agent A, |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
177 |
Nonce NB, Number PB, Agent B|})) |
11287 | 178 |
# evsCF \<in> tls" |
3474 | 179 |
|
11287 | 180 |
ServerFinished: |
13922 | 181 |
--{*Keeping A' and A'' distinct means B cannot even check that the |
182 |
two messages originate from the same source. *} |
|
11287 | 183 |
"[| evsSF \<in> tls; |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
184 |
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|} |
11287 | 185 |
\<in> set evsSF; |
186 |
Says B A {|Nonce NB, Number SID, Number PB|} \<in> set evsSF; |
|
187 |
Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSF; |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
188 |
M = PRF(PMS,NA,NB) |] |
3474 | 189 |
==> 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
|
190 |
(Hash{|Number SID, Nonce M, |
11287 | 191 |
Nonce NA, Number PA, Agent A, |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
192 |
Nonce NB, Number PB, Agent B|})) |
11287 | 193 |
# evsSF \<in> tls" |
3474 | 194 |
|
11287 | 195 |
ClientAccepts: |
13922 | 196 |
--{*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
|
197 |
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
|
198 |
needed to resume this session. The "Notes A ..." premise is |
13922 | 199 |
used to prove Notes_master_imp_Crypt_PMS.*} |
11287 | 200 |
"[| evsCA \<in> tls; |
201 |
Notes A {|Agent B, Nonce PMS|} \<in> set evsCA; |
|
202 |
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
|
203 |
X = Hash{|Number SID, Nonce M, |
11287 | 204 |
Nonce NA, Number PA, Agent A, |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
205 |
Nonce NB, Number PB, Agent B|}; |
11287 | 206 |
Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evsCA; |
207 |
Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA |] |
|
208 |
==> |
|
209 |
Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA \<in> tls" |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
210 |
|
11287 | 211 |
ServerAccepts: |
13922 | 212 |
--{*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
|
213 |
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
|
214 |
needed to resume this session. The "Says A'' B ..." premise is |
13922 | 215 |
used to prove Notes_master_imp_Crypt_PMS.*} |
11287 | 216 |
"[| evsSA \<in> tls; |
217 |
A \<noteq> B; |
|
218 |
Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA; |
|
219 |
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
|
220 |
X = Hash{|Number SID, Nonce M, |
11287 | 221 |
Nonce NA, Number PA, Agent A, |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
222 |
Nonce NB, Number PB, Agent B|}; |
11287 | 223 |
Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evsSA; |
224 |
Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA |] |
|
225 |
==> |
|
226 |
Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA \<in> tls" |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
227 |
|
11287 | 228 |
ClientResume: |
13922 | 229 |
--{*If A recalls the SESSION_ID, then she sends a FINISHED message |
230 |
using the new nonces and stored MASTER SECRET.*} |
|
11287 | 231 |
"[| evsCR \<in> tls; |
3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset
|
232 |
Says A B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsCR; |
11287 | 233 |
Says B' A {|Nonce NB, Number SID, Number PB|} \<in> set evsCR; |
234 |
Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evsCR |] |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
235 |
==> 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
|
236 |
(Hash{|Number SID, Nonce M, |
11287 | 237 |
Nonce NA, Number PA, Agent A, |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset
|
238 |
Nonce NB, Number PB, Agent B|})) |
11287 | 239 |
# evsCR \<in> tls" |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
240 |
|
11287 | 241 |
ServerResume: |
13922 | 242 |
--{*Resumption (7.3): If B finds the SESSION_ID then he can send |
243 |
a FINISHED message using the recovered MASTER SECRET*} |
|
11287 | 244 |
"[| evsSR \<in> tls; |
3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset
|
245 |
Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}: set evsSR; |
11287 | 246 |
Says B A {|Nonce NB, Number SID, Number PB|} \<in> set evsSR; |
247 |
Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evsSR |] |
|
3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset
|
248 |
==> 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
|
249 |
(Hash{|Number SID, Nonce M, |
11287 | 250 |
Nonce NA, Number PA, Agent A, |
3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset
|
251 |
Nonce NB, Number PB, Agent B|})) # evsSR |
11287 | 252 |
\<in> tls" |
3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset
|
253 |
|
11287 | 254 |
Oops: |
13922 | 255 |
--{*The most plausible compromise is of an old session key. Losing |
3686
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset
|
256 |
the MASTER SECRET or PREMASTER SECRET is more serious but |
11287 | 257 |
rather unlikely. The assumption A \<noteq> Spy is essential: otherwise |
13922 | 258 |
the Spy could learn session keys merely by replaying messages!*} |
11287 | 259 |
"[| evso \<in> tls; A \<noteq> Spy; |
260 |
Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso |] |
|
261 |
==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso \<in> tls" |
|
262 |
||
263 |
(* |
|
264 |
Protocol goals: |
|
265 |
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two |
|
266 |
parties (though A is not necessarily authenticated). |
|
267 |
||
268 |
* B upon receiving CertVerify knows that A is present (But this |
|
269 |
message is optional!) |
|
270 |
||
271 |
* A upon receiving ServerFinished knows that B is present |
|
272 |
||
273 |
* Each party who has received a FINISHED message can trust that the other |
|
274 |
party agrees on all message components, including PA and PB (thus foiling |
|
275 |
rollback attacks). |
|
276 |
*) |
|
277 |
||
278 |
declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
279 |
declare parts.Body [dest] |
|
280 |
declare analz_into_parts [dest] |
|
281 |
declare Fake_parts_insert_in_Un [dest] |
|
282 |
||
283 |
||
13922 | 284 |
text{*Automatically unfold the definition of "certificate"*} |
11287 | 285 |
declare certificate_def [simp] |
286 |
||
13922 | 287 |
text{*Injectiveness of key-generating functions*} |
11287 | 288 |
declare inj_PRF [THEN inj_eq, iff] |
289 |
declare inj_sessionK [THEN inj_eq, iff] |
|
290 |
declare isSym_sessionK [simp] |
|
291 |
||
292 |
||
293 |
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***) |
|
294 |
||
13922 | 295 |
lemma pubK_neq_sessionK [iff]: "publicKey b A \<noteq> sessionK arg" |
11287 | 296 |
by (simp add: symKeys_neq_imp_neq) |
297 |
||
298 |
declare pubK_neq_sessionK [THEN not_sym, iff] |
|
299 |
||
13922 | 300 |
lemma priK_neq_sessionK [iff]: "invKey (publicKey b A) \<noteq> sessionK arg" |
11287 | 301 |
by (simp add: symKeys_neq_imp_neq) |
302 |
||
303 |
declare priK_neq_sessionK [THEN not_sym, iff] |
|
304 |
||
305 |
lemmas keys_distinct = pubK_neq_sessionK priK_neq_sessionK |
|
306 |
||
307 |
||
13922 | 308 |
subsection{*Protocol Proofs*} |
11287 | 309 |
|
13922 | 310 |
text{*Possibility properties state that some traces run the protocol to the |
311 |
end. Four paths and 12 rules are considered.*} |
|
11287 | 312 |
|
313 |
||
314 |
(** These proofs assume that the Nonce_supply nonces |
|
315 |
(which have the form @ N. Nonce N \<notin> used evs) |
|
316 |
lie outside the range of PRF. It seems reasonable, but as it is needed |
|
317 |
only for the possibility theorems, it is not taken as an axiom. |
|
318 |
**) |
|
319 |
||
320 |
||
13922 | 321 |
text{*Possibility property ending with ClientAccepts.*} |
11287 | 322 |
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |] |
323 |
==> \<exists>SID M. \<exists>evs \<in> tls. |
|
324 |
Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs" |
|
325 |
apply (intro exI bexI) |
|
326 |
apply (rule_tac [2] tls.Nil |
|
327 |
[THEN tls.ClientHello, THEN tls.ServerHello, |
|
328 |
THEN tls.Certificate, THEN tls.ClientKeyExch, |
|
329 |
THEN tls.ClientFinished, THEN tls.ServerFinished, |
|
13507 | 330 |
THEN tls.ClientAccepts], possibility, blast+) |
11287 | 331 |
done |
332 |
||
333 |
||
13922 | 334 |
text{*And one for ServerAccepts. Either FINISHED message may come first.*} |
11287 | 335 |
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |] |
336 |
==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls. |
|
337 |
Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs" |
|
338 |
apply (intro exI bexI) |
|
339 |
apply (rule_tac [2] tls.Nil |
|
340 |
[THEN tls.ClientHello, THEN tls.ServerHello, |
|
341 |
THEN tls.Certificate, THEN tls.ClientKeyExch, |
|
342 |
THEN tls.ServerFinished, THEN tls.ClientFinished, |
|
13507 | 343 |
THEN tls.ServerAccepts], possibility, blast+) |
11287 | 344 |
done |
345 |
||
346 |
||
13922 | 347 |
text{*Another one, for CertVerify (which is optional)*} |
11287 | 348 |
lemma "[| \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B |] |
349 |
==> \<exists>NB PMS. \<exists>evs \<in> tls. |
|
350 |
Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) |
|
351 |
\<in> set evs" |
|
352 |
apply (intro exI bexI) |
|
353 |
apply (rule_tac [2] tls.Nil |
|
354 |
[THEN tls.ClientHello, THEN tls.ServerHello, |
|
355 |
THEN tls.Certificate, THEN tls.ClientKeyExch, |
|
13507 | 356 |
THEN tls.CertVerify], possibility, blast+) |
11287 | 357 |
done |
358 |
||
359 |
||
13922 | 360 |
text{*Another one, for session resumption (both ServerResume and ClientResume). |
361 |
NO tls.Nil here: we refer to a previous session, not the empty trace.*} |
|
11287 | 362 |
lemma "[| evs0 \<in> tls; |
363 |
Notes A {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0; |
|
364 |
Notes B {|Number SID, Agent A, Agent B, Nonce M|} \<in> set evs0; |
|
365 |
\<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; |
|
366 |
A \<noteq> B |] |
|
367 |
==> \<exists>NA PA NB PB X. \<exists>evs \<in> tls. |
|
368 |
X = Hash{|Number SID, Nonce M, |
|
369 |
Nonce NA, Number PA, Agent A, |
|
370 |
Nonce NB, Number PB, Agent B|} & |
|
371 |
Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evs & |
|
372 |
Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evs" |
|
373 |
apply (intro exI bexI) |
|
374 |
apply (rule_tac [2] tls.ClientHello |
|
375 |
[THEN tls.ServerHello, |
|
13507 | 376 |
THEN tls.ServerResume, THEN tls.ClientResume], possibility, blast+) |
11287 | 377 |
done |
378 |
||
379 |
||
13922 | 380 |
subsection{*Inductive proofs about tls*} |
11287 | 381 |
|
382 |
||
383 |
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY |
|
384 |
sends messages containing X! **) |
|
385 |
||
13922 | 386 |
text{*Spy never sees a good agent's private key!*} |
11287 | 387 |
lemma Spy_see_priK [simp]: |
13922 | 388 |
"evs \<in> tls ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)" |
389 |
by (erule tls.induct, force, simp_all, blast) |
|
11287 | 390 |
|
391 |
lemma Spy_analz_priK [simp]: |
|
13922 | 392 |
"evs \<in> tls ==> (Key (privateKey b A) \<in> analz (spies evs)) = (A \<in> bad)" |
11287 | 393 |
by auto |
394 |
||
395 |
lemma Spy_see_priK_D [dest!]: |
|
13922 | 396 |
"[|Key (privateKey b A) \<in> parts (knows Spy evs); evs \<in> tls|] ==> A \<in> bad" |
11287 | 397 |
by (blast dest: Spy_see_priK) |
398 |
||
399 |
||
13922 | 400 |
text{*This lemma says that no false certificates exist. One might extend the |
11287 | 401 |
model to include bogus certificates for the agents, but there seems |
402 |
little point in doing so: the loss of their private keys is a worse |
|
13922 | 403 |
breach of security.*} |
11287 | 404 |
lemma certificate_valid: |
405 |
"[| certificate B KB \<in> parts (spies evs); evs \<in> tls |] ==> KB = pubK B" |
|
406 |
apply (erule rev_mp) |
|
13507 | 407 |
apply (erule tls.induct, force, simp_all, blast) |
11287 | 408 |
done |
409 |
||
410 |
lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid] |
|
411 |
||
412 |
||
13922 | 413 |
subsubsection{*Properties of items found in Notes*} |
11287 | 414 |
|
415 |
lemma Notes_Crypt_parts_spies: |
|
416 |
"[| Notes A {|Agent B, X|} \<in> set evs; evs \<in> tls |] |
|
417 |
==> Crypt (pubK B) X \<in> parts (spies evs)" |
|
418 |
apply (erule rev_mp) |
|
419 |
apply (erule tls.induct, |
|
420 |
frule_tac [7] CX_KB_is_pubKB, force, simp_all) |
|
421 |
apply (blast intro: parts_insertI) |
|
422 |
done |
|
423 |
||
13922 | 424 |
text{*C may be either A or B*} |
11287 | 425 |
lemma Notes_master_imp_Crypt_PMS: |
426 |
"[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs; |
|
427 |
evs \<in> tls |] |
|
428 |
==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)" |
|
429 |
apply (erule rev_mp) |
|
430 |
apply (erule tls.induct, force, simp_all) |
|
13922 | 431 |
txt{*Fake*} |
11287 | 432 |
apply (blast intro: parts_insertI) |
13922 | 433 |
txt{*Client, Server Accept*} |
11287 | 434 |
apply (blast dest!: Notes_Crypt_parts_spies)+ |
435 |
done |
|
436 |
||
13922 | 437 |
text{*Compared with the theorem above, both premise and conclusion are stronger*} |
11287 | 438 |
lemma Notes_master_imp_Notes_PMS: |
439 |
"[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \<in> set evs; |
|
440 |
evs \<in> tls |] |
|
441 |
==> Notes A {|Agent B, Nonce PMS|} \<in> set evs" |
|
442 |
apply (erule rev_mp) |
|
443 |
apply (erule tls.induct, force, simp_all) |
|
13922 | 444 |
txt{*ServerAccepts*} |
11287 | 445 |
apply blast |
446 |
done |
|
447 |
||
448 |
||
13922 | 449 |
subsubsection{*Protocol goal: if B receives CertVerify, then A sent it*} |
11287 | 450 |
|
13922 | 451 |
text{*B can check A's signature if he has received A's certificate.*} |
11287 | 452 |
lemma TrustCertVerify_lemma: |
453 |
"[| X \<in> parts (spies evs); |
|
454 |
X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); |
|
455 |
evs \<in> tls; A \<notin> bad |] |
|
456 |
==> Says A B X \<in> set evs" |
|
457 |
apply (erule rev_mp, erule ssubst) |
|
13507 | 458 |
apply (erule tls.induct, force, simp_all, blast) |
11287 | 459 |
done |
460 |
||
13922 | 461 |
text{*Final version: B checks X using the distributed KA instead of priK A*} |
11287 | 462 |
lemma TrustCertVerify: |
463 |
"[| X \<in> parts (spies evs); |
|
464 |
X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); |
|
465 |
certificate A KA \<in> parts (spies evs); |
|
466 |
evs \<in> tls; A \<notin> bad |] |
|
467 |
==> Says A B X \<in> set evs" |
|
468 |
by (blast dest!: certificate_valid intro!: TrustCertVerify_lemma) |
|
469 |
||
470 |
||
13922 | 471 |
text{*If CertVerify is present then A has chosen PMS.*} |
11287 | 472 |
lemma UseCertVerify_lemma: |
473 |
"[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \<in> parts (spies evs); |
|
474 |
evs \<in> tls; A \<notin> bad |] |
|
475 |
==> Notes A {|Agent B, Nonce PMS|} \<in> set evs" |
|
476 |
apply (erule rev_mp) |
|
13507 | 477 |
apply (erule tls.induct, force, simp_all, blast) |
11287 | 478 |
done |
479 |
||
13922 | 480 |
text{*Final version using the distributed KA instead of priK A*} |
11287 | 481 |
lemma UseCertVerify: |
482 |
"[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) |
|
483 |
\<in> parts (spies evs); |
|
484 |
certificate A KA \<in> parts (spies evs); |
|
485 |
evs \<in> tls; A \<notin> bad |] |
|
486 |
==> Notes A {|Agent B, Nonce PMS|} \<in> set evs" |
|
487 |
by (blast dest!: certificate_valid intro!: UseCertVerify_lemma) |
|
488 |
||
489 |
||
490 |
lemma no_Notes_A_PRF [simp]: |
|
491 |
"evs \<in> tls ==> Notes A {|Agent B, Nonce (PRF x)|} \<notin> set evs" |
|
492 |
apply (erule tls.induct, force, simp_all) |
|
13922 | 493 |
txt{*ClientKeyExch: PMS is assumed to differ from any PRF.*} |
11287 | 494 |
apply blast |
495 |
done |
|
496 |
||
497 |
||
498 |
lemma MS_imp_PMS [dest!]: |
|
499 |
"[| Nonce (PRF (PMS,NA,NB)) \<in> parts (spies evs); evs \<in> tls |] |
|
500 |
==> Nonce PMS \<in> parts (spies evs)" |
|
501 |
apply (erule rev_mp) |
|
502 |
apply (erule tls.induct, force, simp_all) |
|
13922 | 503 |
txt{*Fake*} |
11287 | 504 |
apply (blast intro: parts_insertI) |
13922 | 505 |
txt{*Easy, e.g. by freshness*} |
11287 | 506 |
apply (blast dest: Notes_Crypt_parts_spies)+ |
507 |
done |
|
508 |
||
509 |
||
510 |
||
511 |
||
13922 | 512 |
subsubsection{*Unicity results for PMS, the pre-master-secret*} |
11287 | 513 |
|
13922 | 514 |
text{*PMS determines B.*} |
11287 | 515 |
lemma Crypt_unique_PMS: |
516 |
"[| Crypt(pubK B) (Nonce PMS) \<in> parts (spies evs); |
|
517 |
Crypt(pubK B') (Nonce PMS) \<in> parts (spies evs); |
|
518 |
Nonce PMS \<notin> analz (spies evs); |
|
519 |
evs \<in> tls |] |
|
520 |
==> B=B'" |
|
521 |
apply (erule rev_mp, erule rev_mp, erule rev_mp) |
|
522 |
apply (erule tls.induct, analz_mono_contra, force, simp_all (no_asm_simp)) |
|
13922 | 523 |
txt{*Fake, ClientKeyExch*} |
11287 | 524 |
apply blast+ |
525 |
done |
|
526 |
||
527 |
||
528 |
(** It is frustrating that we need two versions of the unicity results. |
|
529 |
But Notes A {|Agent B, Nonce PMS|} determines both A and B. Sometimes |
|
530 |
we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which |
|
531 |
determines B alone, and only if PMS is secret. |
|
532 |
**) |
|
533 |
||
13922 | 534 |
text{*In A's internal Note, PMS determines A and B.*} |
11287 | 535 |
lemma Notes_unique_PMS: |
536 |
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs; |
|
537 |
Notes A' {|Agent B', Nonce PMS|} \<in> set evs; |
|
538 |
evs \<in> tls |] |
|
539 |
==> A=A' & B=B'" |
|
540 |
apply (erule rev_mp, erule rev_mp) |
|
541 |
apply (erule tls.induct, force, simp_all) |
|
13922 | 542 |
txt{*ClientKeyExch*} |
11287 | 543 |
apply (blast dest!: Notes_Crypt_parts_spies) |
544 |
done |
|
545 |
||
546 |
||
13922 | 547 |
subsection{*Secrecy Theorems*} |
11287 | 548 |
|
13922 | 549 |
text{*Key compromise lemma needed to prove analz_image_keys. |
550 |
No collection of keys can help the spy get new private keys.*} |
|
11287 | 551 |
lemma analz_image_priK [rule_format]: |
552 |
"evs \<in> tls |
|
553 |
==> \<forall>KK. (Key(priK B) \<in> analz (Key`KK Un (spies evs))) = |
|
554 |
(priK B \<in> KK | B \<in> bad)" |
|
555 |
apply (erule tls.induct) |
|
556 |
apply (simp_all (no_asm_simp) |
|
557 |
del: image_insert |
|
558 |
add: image_Un [THEN sym] |
|
559 |
insert_Key_image Un_assoc [THEN sym]) |
|
13922 | 560 |
txt{*Fake*} |
11287 | 561 |
apply spy_analz |
562 |
done |
|
563 |
||
564 |
||
13922 | 565 |
text{*slightly speeds up the big simplification below*} |
11287 | 566 |
lemma range_sessionkeys_not_priK: |
567 |
"KK <= range sessionK ==> priK B \<notin> KK" |
|
568 |
by blast |
|
569 |
||
570 |
||
13922 | 571 |
text{*Lemma for the trivial direction of the if-and-only-if*} |
11287 | 572 |
lemma analz_image_keys_lemma: |
573 |
"(X \<in> analz (G Un H)) --> (X \<in> analz H) ==> |
|
574 |
(X \<in> analz (G Un H)) = (X \<in> analz H)" |
|
575 |
by (blast intro: analz_mono [THEN subsetD]) |
|
576 |
||
577 |
(** Strangely, the following version doesn't work: |
|
578 |
\<forall>Z. (Nonce N \<in> analz (Key`(sessionK`Z) Un (spies evs))) = |
|
579 |
(Nonce N \<in> analz (spies evs))" |
|
580 |
**) |
|
581 |
||
582 |
lemma analz_image_keys [rule_format]: |
|
583 |
"evs \<in> tls ==> |
|
584 |
\<forall>KK. KK <= range sessionK --> |
|
585 |
(Nonce N \<in> analz (Key`KK Un (spies evs))) = |
|
586 |
(Nonce N \<in> analz (spies evs))" |
|
587 |
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
588 |
apply (safe del: iffI) |
|
589 |
apply (safe del: impI iffI intro!: analz_image_keys_lemma) |
|
590 |
apply (simp_all (no_asm_simp) (*faster*) |
|
591 |
del: image_insert imp_disjL (*reduces blow-up*) |
|
592 |
add: image_Un [THEN sym] Un_assoc [THEN sym] |
|
593 |
insert_Key_singleton |
|
594 |
range_sessionkeys_not_priK analz_image_priK) |
|
595 |
apply (simp_all add: insert_absorb) |
|
13922 | 596 |
txt{*Fake*} |
11287 | 597 |
apply spy_analz |
598 |
done |
|
599 |
||
13922 | 600 |
text{*Knowing some session keys is no help in getting new nonces*} |
11287 | 601 |
lemma analz_insert_key [simp]: |
602 |
"evs \<in> tls ==> |
|
11655 | 603 |
(Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) = |
11287 | 604 |
(Nonce N \<in> analz (spies evs))" |
605 |
by (simp del: image_insert |
|
606 |
add: insert_Key_singleton analz_image_keys) |
|
607 |
||
608 |
||
13922 | 609 |
subsubsection{*Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure*} |
11287 | 610 |
|
611 |
(** Some lemmas about session keys, comprising clientK and serverK **) |
|
612 |
||
613 |
||
13922 | 614 |
text{*Lemma: session keys are never used if PMS is fresh. |
11287 | 615 |
Nonces don't have to agree, allowing session resumption. |
616 |
Converse doesn't hold; revealing PMS doesn't force the keys to be sent. |
|
13922 | 617 |
THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*} |
11287 | 618 |
lemma PMS_lemma: |
619 |
"[| Nonce PMS \<notin> parts (spies evs); |
|
620 |
K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role); |
|
621 |
evs \<in> tls |] |
|
622 |
==> Key K \<notin> parts (spies evs) & (\<forall>Y. Crypt K Y \<notin> parts (spies evs))" |
|
623 |
apply (erule rev_mp, erule ssubst) |
|
13922 | 624 |
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
11287 | 625 |
apply (force, simp_all (no_asm_simp)) |
13922 | 626 |
txt{*Fake*} |
11287 | 627 |
apply (blast intro: parts_insertI) |
13922 | 628 |
txt{*SpyKeys*} |
11287 | 629 |
apply blast |
13922 | 630 |
txt{*Many others*} |
11287 | 631 |
apply (force dest!: Notes_Crypt_parts_spies Notes_master_imp_Crypt_PMS)+ |
632 |
done |
|
633 |
||
634 |
lemma PMS_sessionK_not_spied: |
|
635 |
"[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) \<in> parts (spies evs); |
|
636 |
evs \<in> tls |] |
|
637 |
==> Nonce PMS \<in> parts (spies evs)" |
|
638 |
by (blast dest: PMS_lemma) |
|
639 |
||
640 |
lemma PMS_Crypt_sessionK_not_spied: |
|
641 |
"[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y |
|
642 |
\<in> parts (spies evs); evs \<in> tls |] |
|
643 |
==> Nonce PMS \<in> parts (spies evs)" |
|
644 |
by (blast dest: PMS_lemma) |
|
645 |
||
13922 | 646 |
text{*Write keys are never sent if M (MASTER SECRET) is secure. |
11287 | 647 |
Converse fails; betraying M doesn't force the keys to be sent! |
648 |
The strong Oops condition can be weakened later by unicity reasoning, |
|
649 |
with some effort. |
|
13922 | 650 |
NO LONGER USED: see clientK_not_spied and serverK_not_spied*} |
11287 | 651 |
lemma sessionK_not_spied: |
652 |
"[| \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs; |
|
653 |
Nonce M \<notin> analz (spies evs); evs \<in> tls |] |
|
654 |
==> Key (sessionK((NA,NB,M),role)) \<notin> parts (spies evs)" |
|
655 |
apply (erule rev_mp, erule rev_mp) |
|
656 |
apply (erule tls.induct, analz_mono_contra) |
|
657 |
apply (force, simp_all (no_asm_simp)) |
|
13922 | 658 |
txt{*Fake, SpyKeys*} |
11287 | 659 |
apply blast+ |
660 |
done |
|
661 |
||
662 |
||
13922 | 663 |
text{*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*} |
11287 | 664 |
lemma Spy_not_see_PMS: |
665 |
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs; |
|
666 |
evs \<in> tls; A \<notin> bad; B \<notin> bad |] |
|
667 |
==> Nonce PMS \<notin> analz (spies evs)" |
|
668 |
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
669 |
apply (force, simp_all (no_asm_simp)) |
|
13922 | 670 |
txt{*Fake*} |
11287 | 671 |
apply spy_analz |
13922 | 672 |
txt{*SpyKeys*} |
11287 | 673 |
apply force |
674 |
apply (simp_all add: insert_absorb) |
|
13922 | 675 |
txt{*ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning*} |
11287 | 676 |
apply (blast dest: Notes_Crypt_parts_spies) |
677 |
apply (blast dest: Notes_Crypt_parts_spies) |
|
678 |
apply (blast dest: Notes_Crypt_parts_spies) |
|
13922 | 679 |
txt{*ClientAccepts and ServerAccepts: because PMS \<notin> range PRF*} |
11287 | 680 |
apply force+ |
681 |
done |
|
682 |
||
683 |
||
13922 | 684 |
text{*If A sends ClientKeyExch to an honest B, then the MASTER SECRET |
685 |
will stay secret.*} |
|
11287 | 686 |
lemma Spy_not_see_MS: |
687 |
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs; |
|
688 |
evs \<in> tls; A \<notin> bad; B \<notin> bad |] |
|
689 |
==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)" |
|
690 |
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
691 |
apply (force, simp_all (no_asm_simp)) |
|
13922 | 692 |
txt{*Fake*} |
11287 | 693 |
apply spy_analz |
13922 | 694 |
txt{*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*} |
11287 | 695 |
apply (blast dest!: Spy_not_see_PMS) |
696 |
apply (simp_all add: insert_absorb) |
|
13922 | 697 |
txt{*ClientAccepts and ServerAccepts: because PMS was already visible; |
698 |
others, freshness etc.*} |
|
11287 | 699 |
apply (blast dest: Notes_Crypt_parts_spies Spy_not_see_PMS |
700 |
Notes_imp_knows_Spy [THEN analz.Inj])+ |
|
701 |
done |
|
702 |
||
703 |
||
704 |
||
13922 | 705 |
subsubsection{*Weakening the Oops conditions for leakage of clientK*} |
11287 | 706 |
|
13922 | 707 |
text{*If A created PMS then nobody else (except the Spy in replays) |
708 |
would send a message using a clientK generated from that PMS.*} |
|
11287 | 709 |
lemma Says_clientK_unique: |
710 |
"[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs; |
|
711 |
Notes A {|Agent B, Nonce PMS|} \<in> set evs; |
|
712 |
evs \<in> tls; A' \<noteq> Spy |] |
|
713 |
==> A = A'" |
|
714 |
apply (erule rev_mp, erule rev_mp) |
|
715 |
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
716 |
apply (force, simp_all) |
|
13922 | 717 |
txt{*ClientKeyExch*} |
11287 | 718 |
apply (blast dest!: PMS_Crypt_sessionK_not_spied) |
13922 | 719 |
txt{*ClientFinished, ClientResume: by unicity of PMS*} |
11287 | 720 |
apply (blast dest!: Notes_master_imp_Notes_PMS |
721 |
intro: Notes_unique_PMS [THEN conjunct1])+ |
|
722 |
done |
|
723 |
||
724 |
||
13922 | 725 |
text{*If A created PMS and has not leaked her clientK to the Spy, |
726 |
then it is completely secure: not even in parts!*} |
|
11287 | 727 |
lemma clientK_not_spied: |
728 |
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs; |
|
729 |
Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs; |
|
730 |
A \<notin> bad; B \<notin> bad; |
|
731 |
evs \<in> tls |] |
|
732 |
==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)" |
|
733 |
apply (erule rev_mp, erule rev_mp) |
|
734 |
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
735 |
apply (force, simp_all (no_asm_simp)) |
|
13922 | 736 |
txt{*ClientKeyExch*} |
11287 | 737 |
apply blast |
13922 | 738 |
txt{*SpyKeys*} |
11287 | 739 |
apply (blast dest!: Spy_not_see_MS) |
13922 | 740 |
txt{*ClientKeyExch*} |
11287 | 741 |
apply (blast dest!: PMS_sessionK_not_spied) |
13922 | 742 |
txt{*Oops*} |
11287 | 743 |
apply (blast intro: Says_clientK_unique) |
744 |
done |
|
745 |
||
746 |
||
13922 | 747 |
subsubsection{*Weakening the Oops conditions for leakage of serverK*} |
11287 | 748 |
|
13922 | 749 |
text{*If A created PMS for B, then nobody other than B or the Spy would |
750 |
send a message using a serverK generated from that PMS.*} |
|
11287 | 751 |
lemma Says_serverK_unique: |
752 |
"[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs; |
|
753 |
Notes A {|Agent B, Nonce PMS|} \<in> set evs; |
|
754 |
evs \<in> tls; A \<notin> bad; B \<notin> bad; B' \<noteq> Spy |] |
|
755 |
==> B = B'" |
|
756 |
apply (erule rev_mp, erule rev_mp) |
|
757 |
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
758 |
apply (force, simp_all) |
|
13922 | 759 |
txt{*ClientKeyExch*} |
11287 | 760 |
apply (blast dest!: PMS_Crypt_sessionK_not_spied) |
13922 | 761 |
txt{*ServerResume, ServerFinished: by unicity of PMS*} |
11287 | 762 |
apply (blast dest!: Notes_master_imp_Crypt_PMS |
763 |
dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+ |
|
764 |
done |
|
765 |
||
766 |
||
13922 | 767 |
text{*If A created PMS for B, and B has not leaked his serverK to the Spy, |
768 |
then it is completely secure: not even in parts!*} |
|
11287 | 769 |
lemma serverK_not_spied: |
770 |
"[| Notes A {|Agent B, Nonce PMS|} \<in> set evs; |
|
771 |
Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs; |
|
772 |
A \<notin> bad; B \<notin> bad; evs \<in> tls |] |
|
773 |
==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)" |
|
774 |
apply (erule rev_mp, erule rev_mp) |
|
775 |
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
776 |
apply (force, simp_all (no_asm_simp)) |
|
13922 | 777 |
txt{*Fake*} |
11287 | 778 |
apply blast |
13922 | 779 |
txt{*SpyKeys*} |
11287 | 780 |
apply (blast dest!: Spy_not_see_MS) |
13922 | 781 |
txt{*ClientKeyExch*} |
11287 | 782 |
apply (blast dest!: PMS_sessionK_not_spied) |
13922 | 783 |
txt{*Oops*} |
11287 | 784 |
apply (blast intro: Says_serverK_unique) |
785 |
done |
|
786 |
||
787 |
||
13922 | 788 |
subsubsection{*Protocol goals: if A receives ServerFinished, then B is present |
11287 | 789 |
and has used the quoted values PA, PB, etc. Note that it is up to A |
790 |
to compare PA with what she originally sent. |
|
791 |
***) |
|
792 |
||
13922 | 793 |
text{*The mention of her name (A) in X assures A that B knows who she is.*} |
11287 | 794 |
lemma TrustServerFinished [rule_format]: |
795 |
"[| X = Crypt (serverK(Na,Nb,M)) |
|
796 |
(Hash{|Number SID, Nonce M, |
|
797 |
Nonce Na, Number PA, Agent A, |
|
798 |
Nonce Nb, Number PB, Agent B|}); |
|
799 |
M = PRF(PMS,NA,NB); |
|
800 |
evs \<in> tls; A \<notin> bad; B \<notin> bad |] |
|
801 |
==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs --> |
|
802 |
Notes A {|Agent B, Nonce PMS|} \<in> set evs --> |
|
803 |
X \<in> parts (spies evs) --> Says B A X \<in> set evs" |
|
804 |
apply (erule ssubst)+ |
|
805 |
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
806 |
apply (force, simp_all (no_asm_simp)) |
|
13922 | 807 |
txt{*Fake: the Spy doesn't have the critical session key!*} |
11287 | 808 |
apply (blast dest: serverK_not_spied) |
13922 | 809 |
txt{*ClientKeyExch*} |
11287 | 810 |
apply (blast dest!: PMS_Crypt_sessionK_not_spied) |
811 |
done |
|
812 |
||
13922 | 813 |
text{*This version refers not to ServerFinished but to any message from B. |
11287 | 814 |
We don't assume B has received CertVerify, and an intruder could |
815 |
have changed A's identity in all other messages, so we can't be sure |
|
816 |
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented |
|
13922 | 817 |
to bind A's identity with PMS, then we could replace A' by A below.*} |
11287 | 818 |
lemma TrustServerMsg [rule_format]: |
819 |
"[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |] |
|
820 |
==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs --> |
|
821 |
Notes A {|Agent B, Nonce PMS|} \<in> set evs --> |
|
822 |
Crypt (serverK(Na,Nb,M)) Y \<in> parts (spies evs) --> |
|
823 |
(\<exists>A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) \<in> set evs)" |
|
824 |
apply (erule ssubst) |
|
825 |
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
826 |
apply (force, simp_all (no_asm_simp) add: ex_disj_distrib) |
|
13922 | 827 |
txt{*Fake: the Spy doesn't have the critical session key!*} |
11287 | 828 |
apply (blast dest: serverK_not_spied) |
13922 | 829 |
txt{*ClientKeyExch*} |
11287 | 830 |
apply (clarify, blast dest!: PMS_Crypt_sessionK_not_spied) |
13922 | 831 |
txt{*ServerResume, ServerFinished: by unicity of PMS*} |
11287 | 832 |
apply (blast dest!: Notes_master_imp_Crypt_PMS |
833 |
dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+ |
|
834 |
done |
|
835 |
||
836 |
||
13922 | 837 |
subsubsection{*Protocol goal: if B receives any message encrypted with clientK |
838 |
then A has sent it*} |
|
839 |
||
840 |
text{*ASSUMING that A chose PMS. Authentication is |
|
11287 | 841 |
assumed here; B cannot verify it. But if the message is |
13922 | 842 |
ClientFinished, then B can then check the quoted values PA, PB, etc.*} |
11287 | 843 |
|
844 |
lemma TrustClientMsg [rule_format]: |
|
845 |
"[| M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad |] |
|
846 |
==> Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs --> |
|
847 |
Notes A {|Agent B, Nonce PMS|} \<in> set evs --> |
|
848 |
Crypt (clientK(Na,Nb,M)) Y \<in> parts (spies evs) --> |
|
849 |
Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs" |
|
850 |
apply (erule ssubst) |
|
851 |
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) |
|
852 |
apply (force, simp_all (no_asm_simp)) |
|
13922 | 853 |
txt{*Fake: the Spy doesn't have the critical session key!*} |
11287 | 854 |
apply (blast dest: clientK_not_spied) |
13922 | 855 |
txt{*ClientKeyExch*} |
11287 | 856 |
apply (blast dest!: PMS_Crypt_sessionK_not_spied) |
13922 | 857 |
txt{*ClientFinished, ClientResume: by unicity of PMS*} |
11287 | 858 |
apply (blast dest!: Notes_master_imp_Notes_PMS dest: Notes_unique_PMS)+ |
859 |
done |
|
860 |
||
861 |
||
13922 | 862 |
subsubsection{*Protocol goal: if B receives ClientFinished, and if B is able to |
11287 | 863 |
check a CertVerify from A, then A has used the quoted |
864 |
values PA, PB, etc. Even this one requires A to be uncompromised. |
|
13922 | 865 |
*} |
11287 | 866 |
lemma AuthClientFinished: |
867 |
"[| M = PRF(PMS,NA,NB); |
|
868 |
Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs; |
|
869 |
Says A' B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs; |
|
870 |
certificate A KA \<in> parts (spies evs); |
|
871 |
Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})) |
|
872 |
\<in> set evs; |
|
873 |
evs \<in> tls; A \<notin> bad; B \<notin> bad |] |
|
874 |
==> Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs" |
|
875 |
by (blast intro!: TrustClientMsg UseCertVerify) |
|
876 |
||
877 |
(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) |
|
878 |
(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*) |
|
879 |
(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*) |
|
880 |
(*30/9/97: loads in 476s, after removing unused theorems*) |
|
881 |
(*30/9/97: loads in 448s, after fixing ServerResume*) |
|
882 |
||
883 |
(*08/9/97: loads in 189s (pike), after much reorganization, |
|
884 |
back to 621s on albatross?*) |
|
885 |
||
886 |
(*10/2/99: loads in 139s (pike) |
|
887 |
down to 433s on albatross*) |
|
888 |
||
889 |
(*5/5/01: conversion to Isar script |
|
890 |
loads in 137s (perch) |
|
891 |
the last ML version loaded in 122s on perch, a 600MHz machine: |
|
892 |
twice as fast as pike. No idea why it's so much slower! |
|
893 |
The Isar script is slower still, perhaps because simp_all simplifies |
|
894 |
the assumptions be default. |
|
895 |
*) |
|
3474 | 896 |
|
897 |
end |