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