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