author | paulson |
Wed, 15 Jul 1998 10:15:13 +0200 | |
changeset 5143 | b94cd208f073 |
parent 5114 | c729d4c299c1 |
child 5223 | 4cb05273f764 |
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 |
||
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
6 |
Protocol goals: |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
7 |
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
8 |
parties (though A is not necessarily authenticated). |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
9 |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
10 |
* B upon receiving CertVerify knows that A is present (But this |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
11 |
message is optional!) |
3474 | 12 |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
13 |
* A upon receiving ServerFinished knows that B is present |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
14 |
|
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
15 |
* Each party who has received a FINISHED message can trust that the other |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
16 |
party agrees on all message components, including PA and PB (thus foiling |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
17 |
rollback attacks). |
3474 | 18 |
*) |
19 |
||
3961 | 20 |
open TLS; |
3704 | 21 |
|
4449 | 22 |
set proof_timing; |
3474 | 23 |
HOL_quantifiers := false; |
24 |
||
3772 | 25 |
(*Automatically unfold the definition of "certificate"*) |
26 |
Addsimps [certificate_def]; |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
27 |
|
3474 | 28 |
(*Injectiveness of key-generating functions*) |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
29 |
AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq]; |
3474 | 30 |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
31 |
(* invKey(sessionK x) = sessionK x*) |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
32 |
Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK]; |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
33 |
|
3474 | 34 |
|
35 |
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***) |
|
36 |
||
5076 | 37 |
Goal "pubK A ~= sessionK arg"; |
4423 | 38 |
by (rtac notI 1); |
3474 | 39 |
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); |
40 |
by (Full_simp_tac 1); |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
41 |
qed "pubK_neq_sessionK"; |
3474 | 42 |
|
5076 | 43 |
Goal "priK A ~= sessionK arg"; |
4423 | 44 |
by (rtac notI 1); |
3474 | 45 |
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); |
46 |
by (Full_simp_tac 1); |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
47 |
qed "priK_neq_sessionK"; |
3474 | 48 |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
49 |
val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK]; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
50 |
AddIffs (keys_distinct @ (keys_distinct RL [not_sym])); |
3474 | 51 |
|
52 |
||
53 |
(**** Protocol Proofs ****) |
|
54 |
||
3772 | 55 |
(*Possibility properties state that some traces run the protocol to the end. |
56 |
Four paths and 12 rules are considered.*) |
|
3474 | 57 |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
58 |
|
3772 | 59 |
(** These proofs assume that the Nonce_supply nonces |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
60 |
(which have the form @ N. Nonce N ~: used evs) |
3772 | 61 |
lie outside the range of PRF. It seems reasonable, but as it is needed |
62 |
only for the possibility theorems, it is not taken as an axiom. |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
63 |
**) |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
64 |
|
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
65 |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
66 |
(*Possibility property ending with ClientAccepts.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
67 |
Goal "[| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
68 |
\ A ~= B |] \ |
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset
|
69 |
\ ==> EX SID M. EX evs: tls. \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
70 |
\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs"; |
3474 | 71 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
72 |
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
73 |
tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
74 |
tls.ClientAccepts) 2); |
3474 | 75 |
by possibility_tac; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
76 |
by (REPEAT (Blast_tac 1)); |
3474 | 77 |
result(); |
78 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
79 |
(*And one for ServerAccepts. Either FINISHED message may come first.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
80 |
Goal "[| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
81 |
\ A ~= B |] \ |
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset
|
82 |
\ ==> EX SID NA PA NB PB M. EX evs: tls. \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
83 |
\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs"; |
3474 | 84 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
85 |
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
86 |
tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
87 |
tls.ServerAccepts) 2); |
3474 | 88 |
by possibility_tac; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
89 |
by (REPEAT (Blast_tac 1)); |
3474 | 90 |
result(); |
91 |
||
92 |
(*Another one, for CertVerify (which is optional)*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
93 |
Goal "[| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
94 |
\ A ~= B |] \ |
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset
|
95 |
\ ==> EX NB PMS. EX evs: tls. \ |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
96 |
\ Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs"; |
3474 | 97 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
98 |
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
99 |
tls.ClientKeyExch RS tls.CertVerify) 2); |
3474 | 100 |
by possibility_tac; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
101 |
by (REPEAT (Blast_tac 1)); |
3474 | 102 |
result(); |
103 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
104 |
(*Another one, for session resumption (both ServerResume and ClientResume) *) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
105 |
Goal "[| evs0 : tls; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
106 |
\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
107 |
\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
108 |
\ ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
109 |
\ A ~= B |] ==> EX NA PA NB PB X. EX evs: tls. \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
110 |
\ X = Hash{|Number SID, Nonce M, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
111 |
\ Nonce NA, Number PA, Agent A, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
112 |
\ Nonce NB, Number PB, Agent B|} & \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
113 |
\ Says A B (Crypt (clientK(NA,NB,M)) X) : set evs & \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
114 |
\ Says B A (Crypt (serverK(NA,NB,M)) X) : set evs"; |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
115 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
116 |
by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
117 |
tls.ClientResume) 2); |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
118 |
by possibility_tac; |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
119 |
by (REPEAT (Blast_tac 1)); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
120 |
result(); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
121 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
122 |
|
3474 | 123 |
|
124 |
(**** Inductive proofs about tls ****) |
|
125 |
||
126 |
(*Nobody sends themselves messages*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
127 |
Goal "evs : tls ==> ALL A X. Says A A X ~: set evs"; |
3474 | 128 |
by (etac tls.induct 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4472
diff
changeset
|
129 |
by Auto_tac; |
3474 | 130 |
qed_spec_mp "not_Says_to_self"; |
131 |
Addsimps [not_Says_to_self]; |
|
132 |
AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
133 |
||
134 |
||
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
135 |
(*Induction for regularity theorems. If induction formula has the form |
3683 | 136 |
X ~: analz (spies evs) --> ... then it shortens the proof by discarding |
137 |
needless information about analz (insert X (spies evs)) *) |
|
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
138 |
fun parts_induct_tac i = |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
139 |
etac tls.induct i |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
140 |
THEN |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
141 |
REPEAT (FIRSTGOAL analz_mono_contra_tac) |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
142 |
THEN |
4091 | 143 |
fast_tac (claset() addss (simpset())) i THEN |
4686 | 144 |
ALLGOALS Asm_simp_tac; |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
145 |
|
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
146 |
|
3683 | 147 |
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
3474 | 148 |
sends messages containing X! **) |
149 |
||
3683 | 150 |
(*Spy never sees another agent's private key! (unless it's bad at start)*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
151 |
Goal "evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
152 |
by (parts_induct_tac 1); |
3474 | 153 |
by (Fake_parts_insert_tac 1); |
154 |
qed "Spy_see_priK"; |
|
155 |
Addsimps [Spy_see_priK]; |
|
156 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
157 |
Goal "evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; |
4091 | 158 |
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); |
3474 | 159 |
qed "Spy_analz_priK"; |
160 |
Addsimps [Spy_analz_priK]; |
|
161 |
||
4472 | 162 |
AddSDs [Spy_see_priK RSN (2, rev_iffD1), |
163 |
Spy_analz_priK RSN (2, rev_iffD1)]; |
|
3474 | 164 |
|
165 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
166 |
(*This lemma says that no false certificates exist. One might extend the |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
167 |
model to include bogus certificates for the agents, but there seems |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
168 |
little point in doing so: the loss of their private keys is a worse |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
169 |
breach of security.*) |
5076 | 170 |
Goalw [certificate_def] |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
171 |
"[| certificate B KB : parts (spies evs); evs : tls |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
172 |
\ ==> pubK B = KB"; |
3772 | 173 |
by (etac rev_mp 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
174 |
by (parts_induct_tac 1); |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
175 |
by (Fake_parts_insert_tac 1); |
3772 | 176 |
qed "certificate_valid"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
177 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
178 |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
179 |
(*Replace key KB in ClientKeyExch by (pubK B) *) |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
180 |
val ClientKeyExch_tac = |
3772 | 181 |
forward_tac [Says_imp_spies RS parts.Inj RS certificate_valid] |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
182 |
THEN' assume_tac |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
183 |
THEN' hyp_subst_tac; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
184 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
185 |
fun analz_induct_tac i = |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
186 |
etac tls.induct i THEN |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
187 |
ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*) |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
188 |
ALLGOALS (asm_simp_tac |
4091 | 189 |
(simpset() addcongs [if_weak_cong] |
4831 | 190 |
addsimps (split_ifs@pushes))) THEN |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
191 |
(*Remove instances of pubK B: the Spy already knows all public keys. |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
192 |
Combining the two simplifier calls makes them run extremely slowly.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
193 |
ALLGOALS (asm_simp_tac |
4091 | 194 |
(simpset() addcongs [if_weak_cong] |
4686 | 195 |
addsimps [insert_absorb])); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
196 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
197 |
|
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset
|
198 |
(*** Properties of items found in Notes ***) |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
199 |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
200 |
Goal "[| Notes A {|Agent B, X|} : set evs; evs : tls |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
201 |
\ ==> Crypt (pubK B) X : parts (spies evs)"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
202 |
by (etac rev_mp 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
203 |
by (analz_induct_tac 1); |
4091 | 204 |
by (blast_tac (claset() addIs [parts_insertI]) 1); |
3683 | 205 |
qed "Notes_Crypt_parts_spies"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
206 |
|
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset
|
207 |
(*C may be either A or B*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
208 |
Goal "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
209 |
\ evs : tls \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
210 |
\ |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)"; |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
211 |
by (etac rev_mp 1); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
212 |
by (parts_induct_tac 1); |
3711 | 213 |
by (ALLGOALS Clarify_tac); |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
214 |
(*Fake*) |
4091 | 215 |
by (blast_tac (claset() addIs [parts_insertI]) 1); |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
216 |
(*Client, Server Accept*) |
4091 | 217 |
by (REPEAT (blast_tac (claset() addSEs spies_partsEs |
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
218 |
addSDs [Notes_Crypt_parts_spies]) 1)); |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
219 |
qed "Notes_master_imp_Crypt_PMS"; |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
220 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
221 |
(*Compared with the theorem above, both premise and conclusion are stronger*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
222 |
Goal "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
223 |
\ evs : tls \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
224 |
\ |] ==> Notes A {|Agent B, Nonce PMS|} : set evs"; |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
225 |
by (etac rev_mp 1); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
226 |
by (parts_induct_tac 1); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
227 |
(*ServerAccepts*) |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
228 |
by (Fast_tac 1); (*Blast_tac's very slow here*) |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
229 |
qed "Notes_master_imp_Notes_PMS"; |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
230 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
231 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
232 |
(*** Protocol goal: if B receives CertVerify, then A sent it ***) |
3474 | 233 |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
234 |
(*B can check A's signature if he has received A's certificate.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
235 |
Goal "[| X : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
236 |
\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
237 |
\ evs : tls; A ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
238 |
\ ==> Says A B X : set evs"; |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
239 |
by (etac rev_mp 1); |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
240 |
by (hyp_subst_tac 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
241 |
by (parts_induct_tac 1); |
3474 | 242 |
by (Fake_parts_insert_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
243 |
val lemma = result(); |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
244 |
|
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
245 |
(*Final version: B checks X using the distributed KA instead of priK A*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
246 |
Goal "[| X : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
247 |
\ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
248 |
\ certificate A KA : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
249 |
\ evs : tls; A ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
250 |
\ ==> Says A B X : set evs"; |
4091 | 251 |
by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
252 |
qed "TrustCertVerify"; |
3474 | 253 |
|
254 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
255 |
(*If CertVerify is present then A has chosen PMS.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
256 |
Goal "[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
257 |
\ : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
258 |
\ evs : tls; A ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
259 |
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; |
4423 | 260 |
by (etac rev_mp 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
261 |
by (parts_induct_tac 1); |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
262 |
by (Fake_parts_insert_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
263 |
val lemma = result(); |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
264 |
|
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
265 |
(*Final version using the distributed KA instead of priK A*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
266 |
Goal "[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
267 |
\ : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
268 |
\ certificate A KA : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
269 |
\ evs : tls; A ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
270 |
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs"; |
4091 | 271 |
by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
272 |
qed "UseCertVerify"; |
3474 | 273 |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
274 |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
275 |
Goal "evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs"; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
276 |
by (parts_induct_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
277 |
(*ClientKeyExch: PMS is assumed to differ from any PRF.*) |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
278 |
by (Blast_tac 1); |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
279 |
qed "no_Notes_A_PRF"; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
280 |
Addsimps [no_Notes_A_PRF]; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
281 |
|
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
282 |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
283 |
Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
284 |
\ evs : tls |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
285 |
\ ==> Nonce PMS : parts (spies evs)"; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
286 |
by (etac rev_mp 1); |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
287 |
by (parts_induct_tac 1); |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
288 |
by (Fake_parts_insert_tac 1); |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
289 |
(*Six others, all trivial or by freshness*) |
4091 | 290 |
by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies] |
4201 | 291 |
addSEs spies_partsEs) 1)); |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
292 |
qed "MS_imp_PMS"; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
293 |
AddSDs [MS_imp_PMS]; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
294 |
|
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
295 |
|
3474 | 296 |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
297 |
(*** Unicity results for PMS, the pre-master-secret ***) |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
298 |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
299 |
(*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
300 |
Goal "[| Nonce PMS ~: analz (spies evs); evs : tls |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
301 |
\ ==> EX B'. ALL B. \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
302 |
\ Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
303 |
by (etac rev_mp 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
304 |
by (parts_induct_tac 1); |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
305 |
by (Fake_parts_insert_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
306 |
(*ClientKeyExch*) |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
307 |
by (ClientKeyExch_tac 1); |
4091 | 308 |
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
309 |
by (expand_case_tac "PMS = ?y" 1 THEN |
4091 | 310 |
blast_tac (claset() addSEs partsEs) 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
311 |
val lemma = result(); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
312 |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
313 |
Goal "[| Crypt(pubK B) (Nonce PMS) : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
314 |
\ Crypt(pubK B') (Nonce PMS) : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
315 |
\ Nonce PMS ~: analz (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
316 |
\ evs : tls |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
317 |
\ ==> B=B'"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
318 |
by (prove_unique_tac lemma 1); |
3704 | 319 |
qed "Crypt_unique_PMS"; |
320 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
321 |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
322 |
(** It is frustrating that we need two versions of the unicity results. |
3704 | 323 |
But Notes A {|Agent B, Nonce PMS|} determines both A and B. Sometimes |
324 |
we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which |
|
325 |
determines B alone, and only if PMS is secret. |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
326 |
**) |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
327 |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
328 |
(*In A's internal Note, PMS determines A and B.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
329 |
Goal "evs : tls \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
330 |
\ ==> EX A' B'. ALL A B. \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
331 |
\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'"; |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
332 |
by (parts_induct_tac 1); |
4091 | 333 |
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
334 |
(*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*) |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
335 |
by (expand_case_tac "PMS = ?y" 1 THEN |
4091 | 336 |
blast_tac (claset() addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
337 |
val lemma = result(); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
338 |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
339 |
Goal "[| Notes A {|Agent B, Nonce PMS|} : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
340 |
\ Notes A' {|Agent B', Nonce PMS|} : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
341 |
\ evs : tls |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
342 |
\ ==> A=A' & B=B'"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
343 |
by (prove_unique_tac lemma 1); |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
344 |
qed "Notes_unique_PMS"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
345 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
346 |
|
3474 | 347 |
|
3772 | 348 |
(**** Secrecy Theorems ****) |
349 |
||
350 |
(*Key compromise lemma needed to prove analz_image_keys. |
|
351 |
No collection of keys can help the spy get new private keys.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
352 |
Goal "evs : tls ==> \ |
3772 | 353 |
\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
354 |
\ (priK B : KK | B : bad)"; |
3772 | 355 |
by (etac tls.induct 1); |
356 |
by (ALLGOALS |
|
357 |
(asm_simp_tac (analz_image_keys_ss |
|
358 |
addsimps (certificate_def::keys_distinct)))); |
|
359 |
(*Fake*) |
|
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
360 |
by (spy_analz_tac 1); |
3772 | 361 |
qed_spec_mp "analz_image_priK"; |
362 |
||
363 |
||
364 |
(*slightly speeds up the big simplification below*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
365 |
Goal "KK <= range sessionK ==> priK B ~: KK"; |
3772 | 366 |
by (Blast_tac 1); |
367 |
val range_sessionkeys_not_priK = result(); |
|
368 |
||
369 |
(*Lemma for the trivial direction of the if-and-only-if*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
370 |
Goal "(X : analz (G Un H)) --> (X : analz H) ==> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
371 |
\ (X : analz (G Un H)) = (X : analz H)"; |
4091 | 372 |
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); |
3961 | 373 |
val analz_image_keys_lemma = result(); |
3772 | 374 |
|
375 |
(** Strangely, the following version doesn't work: |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
376 |
\ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
377 |
\ (Nonce N : analz (spies evs))"; |
3772 | 378 |
**) |
379 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
380 |
Goal "evs : tls ==> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
381 |
\ ALL KK. KK <= range sessionK --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
382 |
\ (Nonce N : analz (Key``KK Un (spies evs))) = \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
383 |
\ (Nonce N : analz (spies evs))"; |
3772 | 384 |
by (etac tls.induct 1); |
385 |
by (ClientKeyExch_tac 7); |
|
386 |
by (REPEAT_FIRST (resolve_tac [allI, impI])); |
|
3961 | 387 |
by (REPEAT_FIRST (rtac analz_image_keys_lemma)); |
5076 | 388 |
by (ALLGOALS (*4.5 seconds*) |
3772 | 389 |
(asm_simp_tac (analz_image_keys_ss |
4831 | 390 |
addsimps (split_ifs@pushes) |
3772 | 391 |
addsimps [range_sessionkeys_not_priK, |
392 |
analz_image_priK, certificate_def]))); |
|
4091 | 393 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]))); |
3772 | 394 |
(*Fake*) |
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
395 |
by (spy_analz_tac 1); |
3772 | 396 |
qed_spec_mp "analz_image_keys"; |
397 |
||
398 |
(*Knowing some session keys is no help in getting new nonces*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
399 |
Goal "evs : tls ==> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
400 |
\ Nonce N : analz (insert (Key (sessionK z)) (spies evs)) = \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
401 |
\ (Nonce N : analz (spies evs))"; |
3772 | 402 |
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1); |
403 |
qed "analz_insert_key"; |
|
404 |
Addsimps [analz_insert_key]; |
|
405 |
||
406 |
||
407 |
(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***) |
|
408 |
||
409 |
(** Some lemmas about session keys, comprising clientK and serverK **) |
|
410 |
||
411 |
||
412 |
(*Lemma: session keys are never used if PMS is fresh. |
|
413 |
Nonces don't have to agree, allowing session resumption. |
|
414 |
Converse doesn't hold; revealing PMS doesn't force the keys to be sent. |
|
415 |
THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
416 |
Goal "[| Nonce PMS ~: parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
417 |
\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
418 |
\ evs : tls |] \ |
3772 | 419 |
\ ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))"; |
420 |
by (etac rev_mp 1); |
|
421 |
by (hyp_subst_tac 1); |
|
422 |
by (analz_induct_tac 1); |
|
423 |
(*SpyKeys*) |
|
4091 | 424 |
by (blast_tac (claset() addSEs spies_partsEs) 3); |
3772 | 425 |
(*Fake*) |
426 |
by (Fake_parts_insert_tac 2); |
|
427 |
(** LEVEL 6 **) |
|
428 |
(*Oops*) |
|
4091 | 429 |
by (fast_tac (claset() addSEs [MPair_parts] |
3772 | 430 |
addDs [Says_imp_spies RS parts.Inj] |
4091 | 431 |
addss (simpset())) 6); |
3772 | 432 |
by (REPEAT |
4091 | 433 |
(blast_tac (claset() addSDs [Notes_Crypt_parts_spies, |
4201 | 434 |
Notes_master_imp_Crypt_PMS] |
435 |
addSEs spies_partsEs) 1)); |
|
3772 | 436 |
val lemma = result(); |
437 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
438 |
Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
439 |
\ evs : tls |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
440 |
\ ==> Nonce PMS : parts (spies evs)"; |
4091 | 441 |
by (blast_tac (claset() addDs [lemma]) 1); |
3772 | 442 |
qed "PMS_sessionK_not_spied"; |
443 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
444 |
Goal "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
445 |
\ : parts (spies evs); evs : tls |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
446 |
\ ==> Nonce PMS : parts (spies evs)"; |
4091 | 447 |
by (blast_tac (claset() addDs [lemma]) 1); |
3772 | 448 |
qed "PMS_Crypt_sessionK_not_spied"; |
449 |
||
450 |
(*Lemma: write keys are never sent if M (MASTER SECRET) is secure. |
|
451 |
Converse doesn't hold; betraying M doesn't force the keys to be sent! |
|
452 |
The strong Oops condition can be weakened later by unicity reasoning, |
|
453 |
with some effort.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
454 |
Goal "[| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
455 |
\ Nonce M ~: analz (spies evs); evs : tls |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
456 |
\ ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)"; |
3772 | 457 |
by (etac rev_mp 1); |
458 |
by (etac rev_mp 1); |
|
459 |
by (analz_induct_tac 1); (*17 seconds*) |
|
460 |
(*SpyKeys*) |
|
4091 | 461 |
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3); |
3772 | 462 |
(*Fake*) |
463 |
by (spy_analz_tac 2); |
|
464 |
(*Base*) |
|
465 |
by (Blast_tac 1); |
|
466 |
qed "sessionK_not_spied"; |
|
467 |
Addsimps [sessionK_not_spied]; |
|
468 |
||
469 |
||
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
470 |
(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
471 |
Goal "[| evs : tls; A ~: bad; B ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
472 |
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
473 |
\ Nonce PMS ~: analz (spies evs)"; |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
474 |
by (analz_induct_tac 1); (*11 seconds*) |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
475 |
(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*) |
4091 | 476 |
by (REPEAT (fast_tac (claset() addss (simpset())) 6)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
477 |
(*ClientHello, ServerHello, ClientKeyExch, ServerResume: |
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset
|
478 |
mostly freshness reasoning*) |
4091 | 479 |
by (REPEAT (blast_tac (claset() addSEs partsEs |
4201 | 480 |
addDs [Notes_Crypt_parts_spies, |
481 |
impOfSubs analz_subset_parts, |
|
482 |
Says_imp_spies RS analz.Inj]) 3)); |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
483 |
(*SpyKeys*) |
4091 | 484 |
by (fast_tac (claset() addss (simpset())) 2); |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
485 |
(*Fake*) |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
486 |
by (spy_analz_tac 1); |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
487 |
bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp)); |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
488 |
|
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
489 |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
490 |
(*If A sends ClientKeyExch to an honest B, then the MASTER SECRET |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
491 |
will stay secret.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
492 |
Goal "[| evs : tls; A ~: bad; B ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
493 |
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
494 |
\ Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)"; |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
495 |
by (analz_induct_tac 1); (*13 seconds*) |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
496 |
(*ClientAccepts and ServerAccepts: because PMS was already visible*) |
4091 | 497 |
by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, |
4201 | 498 |
Says_imp_spies RS analz.Inj, |
499 |
Notes_imp_spies RS analz.Inj]) 6)); |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
500 |
(*ClientHello*) |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
501 |
by (Blast_tac 3); |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
502 |
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*) |
4091 | 503 |
by (blast_tac (claset() addSDs [Spy_not_see_PMS, |
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
504 |
Says_imp_spies RS analz.Inj]) 2); |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
505 |
(*Fake*) |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
506 |
by (spy_analz_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
507 |
(*ServerHello and ClientKeyExch: mostly freshness reasoning*) |
4091 | 508 |
by (REPEAT (blast_tac (claset() addSEs partsEs |
4201 | 509 |
addDs [Notes_Crypt_parts_spies, |
510 |
impOfSubs analz_subset_parts, |
|
511 |
Says_imp_spies RS analz.Inj]) 1)); |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
512 |
bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp)); |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
513 |
|
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
514 |
|
3704 | 515 |
(*** Weakening the Oops conditions for leakage of clientK ***) |
516 |
||
517 |
(*If A created PMS then nobody other than the Spy would send a message |
|
518 |
using a clientK generated from that PMS.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
519 |
Goal "[| evs : tls; A' ~= Spy |] \ |
3704 | 520 |
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
521 |
\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
522 |
\ A = A'"; |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
523 |
by (analz_induct_tac 1); (*8 seconds*) |
3711 | 524 |
by (ALLGOALS Clarify_tac); |
3704 | 525 |
(*ClientFinished, ClientResume: by unicity of PMS*) |
526 |
by (REPEAT |
|
4091 | 527 |
(blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS] |
4201 | 528 |
addIs [Notes_unique_PMS RS conjunct1]) 2)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
529 |
(*ClientKeyExch*) |
4472 | 530 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied, |
531 |
Says_imp_spies RS parts.Inj]) 1); |
|
3704 | 532 |
bind_thm ("Says_clientK_unique", |
533 |
result() RSN(2,rev_mp) RSN(2,rev_mp)); |
|
534 |
||
535 |
||
536 |
(*If A created PMS and has not leaked her clientK to the Spy, |
|
537 |
then nobody has.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
538 |
Goal "evs : tls \ |
3704 | 539 |
\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
540 |
\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
541 |
\ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) "; |
3704 | 542 |
by (etac tls.induct 1); |
543 |
(*This roundabout proof sequence avoids looping in simplification*) |
|
544 |
by (ALLGOALS Simp_tac); |
|
3711 | 545 |
by (ALLGOALS Clarify_tac); |
3704 | 546 |
by (Fake_parts_insert_tac 1); |
547 |
by (ALLGOALS Asm_simp_tac); |
|
548 |
(*Oops*) |
|
4091 | 549 |
by (blast_tac (claset() addIs [Says_clientK_unique]) 2); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
550 |
(*ClientKeyExch*) |
4472 | 551 |
by (blast_tac (claset() addSDs [PMS_sessionK_not_spied] |
552 |
addSEs spies_partsEs) 1); |
|
3704 | 553 |
qed_spec_mp "clientK_Oops_ALL"; |
554 |
||
555 |
||
556 |
||
557 |
(*** Weakening the Oops conditions for leakage of serverK ***) |
|
558 |
||
559 |
(*If A created PMS for B, then nobody other than B or the Spy would |
|
560 |
send a message using a serverK generated from that PMS.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
561 |
Goal "[| evs : tls; A ~: bad; B ~: bad; B' ~= Spy |] \ |
3704 | 562 |
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
563 |
\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
564 |
\ B = B'"; |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
565 |
by (analz_induct_tac 1); (*9 seconds*) |
3711 | 566 |
by (ALLGOALS Clarify_tac); |
3704 | 567 |
(*ServerResume, ServerFinished: by unicity of PMS*) |
568 |
by (REPEAT |
|
4091 | 569 |
(blast_tac (claset() addSEs [MPair_parts] |
4201 | 570 |
addSDs [Notes_master_imp_Crypt_PMS, |
571 |
Says_imp_spies RS parts.Inj] |
|
572 |
addDs [Spy_not_see_PMS, |
|
573 |
Notes_Crypt_parts_spies, |
|
574 |
Crypt_unique_PMS]) 2)); |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
575 |
(*ClientKeyExch*) |
4472 | 576 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied, |
577 |
Says_imp_spies RS parts.Inj]) 1); |
|
3704 | 578 |
bind_thm ("Says_serverK_unique", |
579 |
result() RSN(2,rev_mp) RSN(2,rev_mp)); |
|
580 |
||
581 |
(*If A created PMS for B, and B has not leaked his serverK to the Spy, |
|
582 |
then nobody has.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
583 |
Goal "[| evs : tls; A ~: bad; B ~: bad |] \ |
3704 | 584 |
\ ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
585 |
\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
586 |
\ (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) "; |
3704 | 587 |
by (etac tls.induct 1); |
588 |
(*This roundabout proof sequence avoids looping in simplification*) |
|
589 |
by (ALLGOALS Simp_tac); |
|
3711 | 590 |
by (ALLGOALS Clarify_tac); |
3704 | 591 |
by (Fake_parts_insert_tac 1); |
592 |
by (ALLGOALS Asm_simp_tac); |
|
593 |
(*Oops*) |
|
4091 | 594 |
by (blast_tac (claset() addIs [Says_serverK_unique]) 2); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
595 |
(*ClientKeyExch*) |
4472 | 596 |
by (blast_tac (claset() addSDs [PMS_sessionK_not_spied] |
597 |
addSEs spies_partsEs) 1); |
|
3704 | 598 |
qed_spec_mp "serverK_Oops_ALL"; |
599 |
||
600 |
||
601 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
602 |
(*** Protocol goals: if A receives ServerFinished, then B is present |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
603 |
and has used the quoted values PA, PB, etc. Note that it is up to A |
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
604 |
to compare PA with what she originally sent. |
3474 | 605 |
***) |
606 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
607 |
(*The mention of her name (A) in X assures A that B knows who she is.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
608 |
Goal "[| X = Crypt (serverK(Na,Nb,M)) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
609 |
\ (Hash{|Number SID, Nonce M, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
610 |
\ Nonce Na, Number PA, Agent A, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
611 |
\ Nonce Nb, Number PB, Agent B|}); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
612 |
\ M = PRF(PMS,NA,NB); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
613 |
\ evs : tls; A ~: bad; B ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
614 |
\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
615 |
\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
616 |
\ X : parts (spies evs) --> Says B A X : set evs"; |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
617 |
by (hyp_subst_tac 1); |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
618 |
by (analz_induct_tac 1); (*10 seconds*) |
4091 | 619 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
3711 | 620 |
by (ALLGOALS Clarify_tac); |
4472 | 621 |
(*ClientKeyExch*) |
622 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
623 |
(*Fake: the Spy doesn't have the critical session key!*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
624 |
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evs)" 1); |
4091 | 625 |
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, |
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
626 |
not_parts_not_analz]) 2); |
3474 | 627 |
by (Fake_parts_insert_tac 1); |
3772 | 628 |
val lemma = normalize_thm [RSmp] (result()); |
3704 | 629 |
|
630 |
(*Final version*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
631 |
Goal "[| X = Crypt (serverK(Na,Nb,M)) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
632 |
\ (Hash{|Number SID, Nonce M, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
633 |
\ Nonce Na, Number PA, Agent A, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
634 |
\ Nonce Nb, Number PB, Agent B|}); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
635 |
\ M = PRF(PMS,NA,NB); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
636 |
\ X : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
637 |
\ Notes A {|Agent B, Nonce PMS|} : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
638 |
\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
639 |
\ evs : tls; A ~: bad; B ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
640 |
\ ==> Says B A X : set evs"; |
4091 | 641 |
by (blast_tac (claset() addIs [lemma] |
4201 | 642 |
addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1); |
3474 | 643 |
qed_spec_mp "TrustServerFinished"; |
644 |
||
645 |
||
3704 | 646 |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
647 |
(*This version refers not to ServerFinished but to any message from B. |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
648 |
We don't assume B has received CertVerify, and an intruder could |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
649 |
have changed A's identity in all other messages, so we can't be sure |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
650 |
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented |
3704 | 651 |
to bind A's identity with PMS, then we could replace A' by A below.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
652 |
Goal "[| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
653 |
\ ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
654 |
\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
655 |
\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs) --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
656 |
\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)"; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
657 |
by (hyp_subst_tac 1); |
3686
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset
|
658 |
by (analz_induct_tac 1); (*20 seconds*) |
4091 | 659 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); |
3711 | 660 |
by (ALLGOALS Clarify_tac); |
3704 | 661 |
(*ServerResume, ServerFinished: by unicity of PMS*) |
662 |
by (REPEAT |
|
4091 | 663 |
(blast_tac (claset() addSEs [MPair_parts] |
4201 | 664 |
addSDs [Notes_master_imp_Crypt_PMS, |
665 |
Says_imp_spies RS parts.Inj] |
|
666 |
addDs [Spy_not_see_PMS, |
|
667 |
Notes_Crypt_parts_spies, |
|
668 |
Crypt_unique_PMS]) 3)); |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
669 |
(*ClientKeyExch*) |
4472 | 670 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
671 |
(*Fake: the Spy doesn't have the critical session key!*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
672 |
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evs)" 1); |
4091 | 673 |
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, |
4201 | 674 |
not_parts_not_analz]) 2); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
675 |
by (Fake_parts_insert_tac 1); |
3772 | 676 |
val lemma = normalize_thm [RSmp] (result()); |
3704 | 677 |
|
678 |
(*Final version*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
679 |
Goal "[| M = PRF(PMS,NA,NB); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
680 |
\ Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
681 |
\ Notes A {|Agent B, Nonce PMS|} : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
682 |
\ Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
683 |
\ evs : tls; A ~: bad; B ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
684 |
\ ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs"; |
4091 | 685 |
by (blast_tac (claset() addIs [lemma] |
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
686 |
addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
687 |
qed_spec_mp "TrustServerMsg"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
688 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
689 |
|
3704 | 690 |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
691 |
(*** Protocol goal: if B receives any message encrypted with clientK |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
692 |
then A has sent it, ASSUMING that A chose PMS. Authentication is |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
693 |
assumed here; B cannot verify it. But if the message is |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
694 |
ClientFinished, then B can then check the quoted values PA, PB, etc. |
3506 | 695 |
***) |
3704 | 696 |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
697 |
Goal "[| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
698 |
\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
699 |
\ Notes A {|Agent B, Nonce PMS|} : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
700 |
\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
701 |
\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; |
3772 | 702 |
by (hyp_subst_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
703 |
by (analz_induct_tac 1); (*15 seconds*) |
3711 | 704 |
by (ALLGOALS Clarify_tac); |
3704 | 705 |
(*ClientFinished, ClientResume: by unicity of PMS*) |
4091 | 706 |
by (REPEAT (blast_tac (claset() delrules [conjI] |
4201 | 707 |
addSDs [Notes_master_imp_Notes_PMS] |
708 |
addDs [Notes_unique_PMS]) 3)); |
|
4472 | 709 |
(*ClientKeyExch*) |
710 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
711 |
(*Fake: the Spy doesn't have the critical session key!*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
712 |
by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evs)" 1); |
4091 | 713 |
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, |
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
714 |
not_parts_not_analz]) 2); |
3474 | 715 |
by (Fake_parts_insert_tac 1); |
3772 | 716 |
val lemma = normalize_thm [RSmp] (result()); |
3704 | 717 |
|
718 |
(*Final version*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
719 |
Goal "[| M = PRF(PMS,NA,NB); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
720 |
\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
721 |
\ Notes A {|Agent B, Nonce PMS|} : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
722 |
\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
723 |
\ evs : tls; A ~: bad; B ~: bad |] \ |
3772 | 724 |
\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; |
4091 | 725 |
by (blast_tac (claset() addIs [lemma] |
4201 | 726 |
addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1); |
3772 | 727 |
qed "TrustClientMsg"; |
3506 | 728 |
|
729 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
730 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
731 |
(*** Protocol goal: if B receives ClientFinished, and if B is able to |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
732 |
check a CertVerify from A, then A has used the quoted |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
733 |
values PA, PB, etc. Even this one requires A to be uncompromised. |
3506 | 734 |
***) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
735 |
Goal "[| M = PRF(PMS,NA,NB); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
736 |
\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
737 |
\ Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
738 |
\ certificate A KA : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
739 |
\ Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
740 |
\ : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
741 |
\ evs : tls; A ~: bad; B ~: bad |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
742 |
\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs"; |
4091 | 743 |
by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify] |
4201 | 744 |
addDs [Says_imp_spies RS parts.Inj]) 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
745 |
qed "AuthClientFinished"; |
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset
|
746 |
|
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset
|
747 |
(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) |
3711 | 748 |
(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*) |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
749 |
(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*) |
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset
|
750 |
(*30/9/97: loads in 476s, after removing unused theorems*) |
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset
|
751 |
(*30/9/97: loads in 448s, after fixing ServerResume*) |