author | paulson |
Fri, 11 Jul 1997 13:30:01 +0200 | |
changeset 3515 | d8a71f6eaf40 |
parent 3506 | a36e0a49d2cd |
child 3519 | ab0a9fbed4c0 |
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 |
|
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
10 |
* B upon receiving CERTIFICATE VERIFY knows that A is present (But this |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
11 |
message is optional!) |
3474 | 12 |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
13 |
* A upon receiving SERVER FINISHED knows that B is present |
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 |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
16 |
party agrees on all message components, including XA and XB (thus foiling |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
17 |
rollback attacks). |
3474 | 18 |
*) |
19 |
||
20 |
open TLS; |
|
21 |
||
22 |
proof_timing:=true; |
|
23 |
HOL_quantifiers := false; |
|
24 |
||
25 |
AddIffs [Spy_in_lost, Server_not_lost]; |
|
3500 | 26 |
Addsimps [certificate_def]; |
3474 | 27 |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
28 |
goal thy "!!A. A ~: lost ==> A ~= Spy"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
29 |
by (Blast_tac 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
30 |
qed "not_lost_not_eq_Spy"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
31 |
Addsimps [not_lost_not_eq_Spy]; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
32 |
|
3474 | 33 |
(*Injectiveness of key-generating functions*) |
34 |
AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq]; |
|
35 |
||
36 |
(* invKey(clientK x) = clientK x and similarly for serverK*) |
|
37 |
Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK, |
|
38 |
isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK]; |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
39 |
|
3474 | 40 |
|
41 |
(*Replacing the variable by a constant improves search speed by 50%!*) |
|
42 |
val Says_imp_sees_Spy' = |
|
43 |
read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; |
|
44 |
||
45 |
||
46 |
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***) |
|
47 |
||
48 |
goal thy "pubK A ~= clientK arg"; |
|
49 |
br notI 1; |
|
50 |
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); |
|
51 |
by (Full_simp_tac 1); |
|
52 |
qed "pubK_neq_clientK"; |
|
53 |
||
54 |
goal thy "pubK A ~= serverK arg"; |
|
55 |
br notI 1; |
|
56 |
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); |
|
57 |
by (Full_simp_tac 1); |
|
58 |
qed "pubK_neq_serverK"; |
|
59 |
||
60 |
goal thy "priK A ~= clientK arg"; |
|
61 |
br notI 1; |
|
62 |
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); |
|
63 |
by (Full_simp_tac 1); |
|
64 |
qed "priK_neq_clientK"; |
|
65 |
||
66 |
goal thy "priK A ~= serverK arg"; |
|
67 |
br notI 1; |
|
68 |
by (dres_inst_tac [("f","isSymKey")] arg_cong 1); |
|
69 |
by (Full_simp_tac 1); |
|
70 |
qed "priK_neq_serverK"; |
|
71 |
||
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
72 |
(*clientK and serverK have disjoint ranges*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
73 |
goal thy "clientK arg ~= serverK arg'"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
74 |
by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
75 |
by (Blast_tac 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
76 |
qed "clientK_neq_serverK"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
77 |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
78 |
val keys_distinct = [pubK_neq_clientK, pubK_neq_serverK, |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
79 |
priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK]; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
80 |
AddIffs (keys_distinct @ (keys_distinct RL [not_sym])); |
3474 | 81 |
|
82 |
||
83 |
(**** Protocol Proofs ****) |
|
84 |
||
85 |
(*A "possibility property": there are traces that reach the end. |
|
86 |
This protocol has three end points and six messages to consider.*) |
|
87 |
||
88 |
(*Possibility property ending with ServerFinished.*) |
|
89 |
goal thy |
|
90 |
"!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \ |
|
91 |
\ Says B A (Crypt (serverK(NA,NB,M)) \ |
|
92 |
\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \ |
|
93 |
\ Nonce NA, Agent XA, Agent A, \ |
|
94 |
\ Nonce NB, Agent XB, \ |
|
3500 | 95 |
\ certificate B (pubK B)|})) \ |
3474 | 96 |
\ : set evs"; |
97 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
|
98 |
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx |
|
99 |
RS tls.ServerFinished) 2); |
|
100 |
by possibility_tac; |
|
101 |
result(); |
|
102 |
||
103 |
(*And one for ClientFinished. Either FINISHED message may come first.*) |
|
104 |
goal thy |
|
105 |
"!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls. \ |
|
106 |
\ Says A B (Crypt (clientK(NA,NB,M)) \ |
|
107 |
\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \ |
|
108 |
\ Nonce NA, Agent XA, \ |
|
3500 | 109 |
\ certificate A (pubK A), \ |
3474 | 110 |
\ Nonce NB, Agent XB, Agent B|})) : set evs"; |
111 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
|
112 |
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx |
|
113 |
RS tls.ClientFinished) 2); |
|
114 |
by possibility_tac; |
|
115 |
result(); |
|
116 |
||
117 |
(*Another one, for CertVerify (which is optional)*) |
|
118 |
goal thy |
|
3506 | 119 |
"!!A B. A ~= B ==> EX NB M. EX evs: tls. \ |
3474 | 120 |
\ Says A B (Crypt (priK A) \ |
3506 | 121 |
\ (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs"; |
3474 | 122 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
3506 | 123 |
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx |
124 |
RS tls.CertVerify) 2); |
|
3474 | 125 |
by possibility_tac; |
126 |
result(); |
|
127 |
||
128 |
||
129 |
(**** Inductive proofs about tls ****) |
|
130 |
||
131 |
(*Nobody sends themselves messages*) |
|
132 |
goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs"; |
|
133 |
by (etac tls.induct 1); |
|
134 |
by (Auto_tac()); |
|
135 |
qed_spec_mp "not_Says_to_self"; |
|
136 |
Addsimps [not_Says_to_self]; |
|
137 |
AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
138 |
||
139 |
||
140 |
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
|
141 |
sends messages containing X! **) |
|
142 |
||
143 |
(*Spy never sees another agent's private key! (unless it's lost at start)*) |
|
144 |
goal thy |
|
145 |
"!!evs. evs : tls \ |
|
146 |
\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; |
|
147 |
by (etac tls.induct 1); |
|
148 |
by (prove_simple_subgoals_tac 1); |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
149 |
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 2); |
3474 | 150 |
by (Fake_parts_insert_tac 1); |
151 |
qed "Spy_see_priK"; |
|
152 |
Addsimps [Spy_see_priK]; |
|
153 |
||
154 |
goal thy |
|
155 |
"!!evs. evs : tls \ |
|
156 |
\ ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)"; |
|
157 |
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
|
158 |
qed "Spy_analz_priK"; |
|
159 |
Addsimps [Spy_analz_priK]; |
|
160 |
||
161 |
goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \ |
|
162 |
\ evs : tls |] ==> A:lost"; |
|
163 |
by (blast_tac (!claset addDs [Spy_see_priK]) 1); |
|
164 |
qed "Spy_see_priK_D"; |
|
165 |
||
166 |
bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); |
|
167 |
AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; |
|
168 |
||
169 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
170 |
(*This lemma says that no false certificates exist. One might extend the |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
171 |
model to include bogus certificates for the lost agents, but there seems |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
172 |
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
|
173 |
breach of security.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
174 |
goalw thy [certificate_def] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
175 |
"!!evs. evs : tls \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
176 |
\ ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
177 |
by (etac tls.induct 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
178 |
by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]))); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
179 |
by (Fake_parts_insert_tac 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
180 |
by (Blast_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
181 |
bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp)); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
182 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
183 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
184 |
(*Replace key KB in ClientCertKeyEx by (pubK B) *) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
185 |
val ClientCertKeyEx_tac = |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
186 |
forward_tac [Says_imp_sees_Spy' RS parts.Inj RS |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
187 |
parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
188 |
THEN' assume_tac |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
189 |
THEN' hyp_subst_tac; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
190 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
191 |
fun analz_induct_tac i = |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
192 |
etac tls.induct i THEN |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
193 |
ClientCertKeyEx_tac (i+7) THEN (*ClientFinished*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
194 |
ClientCertKeyEx_tac (i+6) THEN (*CertVerify*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
195 |
ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
196 |
rewrite_goals_tac [certificate_def] THEN |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
197 |
ALLGOALS (asm_simp_tac |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
198 |
(!simpset addsimps [not_parts_not_analz] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
199 |
setloop split_tac [expand_if])) THEN |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
200 |
(*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
|
201 |
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
|
202 |
ALLGOALS (asm_simp_tac |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
203 |
(!simpset addsimps [insert_absorb] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
204 |
setloop split_tac [expand_if])); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
205 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
206 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
207 |
(*** Hashing of nonces ***) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
208 |
|
3474 | 209 |
(*Every Nonce that's hashed is already in past traffic. *) |
210 |
goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs); \ |
|
211 |
\ evs : tls |] \ |
|
212 |
\ ==> Nonce N : parts (sees lost Spy evs)"; |
|
213 |
by (etac rev_mp 1); |
|
214 |
by (etac tls.induct 1); |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
215 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
216 |
setloop split_tac [expand_if]))); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
217 |
by (Fake_parts_insert_tac 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
218 |
by (REPEAT (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
219 |
addSEs partsEs) 1)); |
3474 | 220 |
qed "Hash_imp_Nonce1"; |
221 |
||
222 |
(*Lemma needed to prove Hash_Hash_imp_Nonce*) |
|
223 |
goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|} \ |
|
224 |
\ : parts (sees lost Spy evs); \ |
|
225 |
\ evs : tls |] \ |
|
226 |
\ ==> Nonce M : parts (sees lost Spy evs)"; |
|
227 |
by (etac rev_mp 1); |
|
228 |
by (etac tls.induct 1); |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
229 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
230 |
setloop split_tac [expand_if]))); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
231 |
by (Fake_parts_insert_tac 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
232 |
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
233 |
addSEs partsEs) 1); |
3474 | 234 |
qed "Hash_imp_Nonce2"; |
235 |
AddSDs [Hash_imp_Nonce2]; |
|
236 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
237 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
238 |
goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs; evs : tls |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
239 |
\ ==> Crypt (pubK B) X : parts (sees lost Spy evs)"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
240 |
by (etac rev_mp 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
241 |
by (analz_induct_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
242 |
by (blast_tac (!claset addIs [parts_insertI]) 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
243 |
qed "Notes_Crypt_parts_sees"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
244 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
245 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
246 |
(*NEEDED??*) |
3474 | 247 |
goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |} \ |
248 |
\ : parts (sees lost Spy evs); \ |
|
249 |
\ evs : tls |] \ |
|
250 |
\ ==> Nonce M : parts (sees lost Spy evs)"; |
|
251 |
by (etac rev_mp 1); |
|
252 |
by (etac tls.induct 1); |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
253 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
254 |
setloop split_tac [expand_if]))); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
255 |
by (Fake_parts_insert_tac 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
256 |
by (step_tac (!claset addSDs [Notes_Crypt_parts_sees, |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
257 |
Says_imp_sees_Spy' RS parts.Inj] |
3474 | 258 |
addSEs partsEs) 1); |
259 |
qed "Hash_Hash_imp_Nonce"; |
|
260 |
||
261 |
||
262 |
(*NEEDED?? |
|
263 |
Every Nonce that's hashed is already in past traffic. |
|
264 |
This general formulation is tricky to prove and hard to use, since the |
|
265 |
2nd premise is typically proved by simplification.*) |
|
266 |
goal thy "!!evs. [| Hash X : parts (sees lost Spy evs); \ |
|
267 |
\ Nonce N : parts {X}; evs : tls |] \ |
|
268 |
\ ==> Nonce N : parts (sees lost Spy evs)"; |
|
269 |
by (etac rev_mp 1); |
|
270 |
by (etac tls.induct 1); |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
271 |
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
272 |
by (step_tac (!claset addSDs [Notes_Crypt_parts_sees, |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
273 |
Says_imp_sees_Spy' RS parts.Inj] |
3474 | 274 |
addSEs partsEs) 1); |
275 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees]))); |
|
276 |
by (Fake_parts_insert_tac 1); |
|
3506 | 277 |
(*CertVerify, ClientFinished, ServerFinished (?)*) |
278 |
by (REPEAT (Blast_tac 1)); |
|
3474 | 279 |
qed "Hash_imp_Nonce_seen"; |
280 |
||
281 |
||
282 |
(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***) |
|
283 |
||
3506 | 284 |
(*B can check A's signature if he has received A's certificate. |
285 |
Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
286 |
message is Fake. We don't need guarantees for the Spy anyway. We must |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
287 |
assume A~:lost; otherwise, the Spy can forge A's signature.*) |
3500 | 288 |
goalw thy [certificate_def] |
3506 | 289 |
"!!evs. [| X = Crypt (priK A) \ |
290 |
\ (Hash{|Nonce NB, certificate B KB, Nonce M|}); \ |
|
291 |
\ evs : tls; A ~: lost; B ~= Spy |] \ |
|
292 |
\ ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} \ |
|
293 |
\ : set evs --> \ |
|
3474 | 294 |
\ X : parts (sees lost Spy evs) --> Says A B X : set evs"; |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
295 |
by (hyp_subst_tac 1); |
3474 | 296 |
by (etac tls.induct 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
297 |
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); |
3474 | 298 |
by (Fake_parts_insert_tac 1); |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
299 |
(*ServerHello: nonce NB cannot be in X because it's fresh!*) |
3474 | 300 |
by (blast_tac (!claset addSDs [Hash_imp_Nonce1] |
301 |
addSEs sees_Spy_partsEs) 1); |
|
302 |
qed_spec_mp "TrustCertVerify"; |
|
303 |
||
304 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
305 |
(*If CERTIFICATE VERIFY is present then A has chosen M.*) |
3506 | 306 |
goal thy |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
307 |
"!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|}) \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
308 |
\ : parts (sees lost Spy evs); \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
309 |
\ evs : tls; A ~: lost |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
310 |
\ ==> Notes A {|Agent B, Nonce M|} : set evs"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
311 |
be rev_mp 1; |
3506 | 312 |
by (etac tls.induct 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
313 |
by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]))); |
3474 | 314 |
by (Fake_parts_insert_tac 2); |
315 |
by (Blast_tac 1); |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
316 |
qed "UseCertVerify"; |
3474 | 317 |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
318 |
|
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
319 |
(*No collection of keys can help the spy get new private keys*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
320 |
goal thy |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
321 |
"!!evs. evs : tls ==> \ |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
322 |
\ ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) = \ |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
323 |
\ (priK B : KK | B : lost)"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
324 |
by (etac tls.induct 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
325 |
by (ALLGOALS |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
326 |
(asm_simp_tac (analz_image_keys_ss |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
327 |
addsimps (certificate_def::keys_distinct)))); |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
328 |
(*Fake*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
329 |
by (spy_analz_tac 2); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
330 |
(*Base*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
331 |
by (Blast_tac 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
332 |
qed_spec_mp "analz_image_priK"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
333 |
|
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
334 |
|
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
335 |
(*Lemma for the trivial direction of the if-and-only-if*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
336 |
goal thy |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
337 |
"!!evs. (X : analz (G Un H)) --> (X : analz H) ==> \ |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
338 |
\ (X : analz (G Un H)) = (X : analz H)"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
339 |
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
340 |
val lemma = result(); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
341 |
|
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
342 |
(*Knowing some clientKs and serverKs is no help in getting new nonces*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
343 |
goal thy |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
344 |
"!!evs. evs : tls ==> \ |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
345 |
\ ALL KK. KK <= (range clientK Un range serverK) --> \ |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
346 |
\ (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \ |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
347 |
\ (Nonce N : analz (sees lost Spy evs))"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
348 |
by (etac tls.induct 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
349 |
by (ClientCertKeyEx_tac 6); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
350 |
by (REPEAT_FIRST (resolve_tac [allI, impI])); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
351 |
by (REPEAT_FIRST (rtac lemma)); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
352 |
writeln"SLOW simplification: 50 secs!??"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
353 |
by (ALLGOALS |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
354 |
(asm_simp_tac (analz_image_keys_ss |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
355 |
addsimps (analz_image_priK::certificate_def:: |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
356 |
keys_distinct)))); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
357 |
by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK]))); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
358 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb]))); |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
359 |
(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
360 |
by (Blast_tac 3); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
361 |
(*Fake*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
362 |
by (spy_analz_tac 2); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
363 |
(*Base*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
364 |
by (Blast_tac 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
365 |
qed_spec_mp "analz_image_keys"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
366 |
|
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
367 |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
368 |
(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
369 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
370 |
"!!evs. [| evs : tls; A ~: lost; B ~: lost |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
371 |
\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
372 |
\ Nonce M ~: analz (sees lost Spy evs)"; |
3474 | 373 |
by (analz_induct_tac 1); |
374 |
(*ClientHello*) |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
375 |
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
376 |
addSEs sees_Spy_partsEs) 3); |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
377 |
(*SpyKeys*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
378 |
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2); |
3474 | 379 |
(*Fake*) |
380 |
by (spy_analz_tac 1); |
|
381 |
(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*) |
|
382 |
by (REPEAT (blast_tac (!claset addSEs partsEs |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
383 |
addDs [Notes_Crypt_parts_sees, |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
384 |
impOfSubs analz_subset_parts, |
3474 | 385 |
Says_imp_sees_Spy' RS analz.Inj]) 1)); |
386 |
bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp)); |
|
387 |
||
388 |
||
389 |
(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***) |
|
390 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
391 |
(** First, some lemmas about those write keys. The proofs for serverK are |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
392 |
nearly identical to those for clientK. **) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
393 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
394 |
(*Lemma: those write keys are never sent if M is secure. |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
395 |
Converse doesn't hold; betraying M doesn't force the keys to be sent!*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
396 |
|
3474 | 397 |
goal thy |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
398 |
"!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \ |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
399 |
\ ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
400 |
by (etac rev_mp 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
401 |
by (analz_induct_tac 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
402 |
(*SpyKeys*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
403 |
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
404 |
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
405 |
(*Fake*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
406 |
by (spy_analz_tac 2); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
407 |
(*Base*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
408 |
by (Blast_tac 1); |
3474 | 409 |
qed "clientK_notin_parts"; |
410 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
411 |
Addsimps [clientK_notin_parts]; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
412 |
AddSEs [clientK_notin_parts RSN (2, rev_notE)]; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
413 |
|
3474 | 414 |
goal thy |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
415 |
"!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \ |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
416 |
\ ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
417 |
by (etac rev_mp 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
418 |
by (analz_induct_tac 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
419 |
(*SpyKeys*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
420 |
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
421 |
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
422 |
(*Fake*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
423 |
by (spy_analz_tac 2); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
424 |
(*Base*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
425 |
by (Blast_tac 1); |
3474 | 426 |
qed "serverK_notin_parts"; |
427 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
428 |
Addsimps [serverK_notin_parts]; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
429 |
AddSEs [serverK_notin_parts RSN (2, rev_notE)]; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
430 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
431 |
(*Lemma: those write keys are never used if M is fresh. |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
432 |
Converse doesn't hold; betraying M doesn't force the keys to be sent! |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
433 |
NOT suitable as safe elim rules.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
434 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
435 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
436 |
"!!evs. [| Nonce M ~: used evs; evs : tls |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
437 |
\ ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees lost Spy evs)"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
438 |
by (etac rev_mp 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
439 |
by (analz_induct_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
440 |
(*ClientFinished: since M is fresh, a different instance of clientK was used.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
441 |
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
442 |
addSEs sees_Spy_partsEs) 3); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
443 |
by (Fake_parts_insert_tac 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
444 |
(*Base*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
445 |
by (Blast_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
446 |
qed "Crypt_clientK_notin_parts"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
447 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
448 |
Addsimps [Crypt_clientK_notin_parts]; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
449 |
AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)]; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
450 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
451 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
452 |
"!!evs. [| Nonce M ~: used evs; evs : tls |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
453 |
\ ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees lost Spy evs)"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
454 |
by (etac rev_mp 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
455 |
by (analz_induct_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
456 |
(*ServerFinished: since M is fresh, a different instance of serverK was used.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
457 |
by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
458 |
addSEs sees_Spy_partsEs) 3); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
459 |
by (Fake_parts_insert_tac 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
460 |
(*Base*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
461 |
by (Blast_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
462 |
qed "Crypt_serverK_notin_parts"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
463 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
464 |
Addsimps [Crypt_serverK_notin_parts]; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
465 |
AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)]; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
466 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
467 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
468 |
(*Weakening A~:lost to A~=Spy would complicate later uses of the rule*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
469 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
470 |
"!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs; \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
471 |
\ A ~: lost; evs : tls |] ==> KB = pubK B"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
472 |
be rev_mp 1; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
473 |
by (analz_induct_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
474 |
qed "A_Crypt_pubB"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
475 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
476 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
477 |
(*** Unicity results for M, the pre-master-secret ***) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
478 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
479 |
(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ... |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
480 |
It simplifies the proof by discarding needless information about |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
481 |
analz (insert X (sees lost Spy evs)) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
482 |
*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
483 |
fun analz_mono_parts_induct_tac i = |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
484 |
etac tls.induct i THEN |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
485 |
ClientCertKeyEx_tac (i+5) THEN (*ClientCertKeyEx*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
486 |
REPEAT_FIRST analz_mono_contra_tac; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
487 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
488 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
489 |
(*M determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
490 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
491 |
"!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
492 |
\ ==> EX B'. ALL B. \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
493 |
\ Crypt (pubK B) (Nonce M) : parts (sees lost Spy evs) --> B=B'"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
494 |
by (etac rev_mp 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
495 |
by (analz_mono_parts_induct_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
496 |
by (prove_simple_subgoals_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
497 |
by (asm_simp_tac (!simpset addsimps [all_conj_distrib] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
498 |
setloop split_tac [expand_if]) 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
499 |
(*ClientCertKeyEx*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
500 |
by (expand_case_tac "M = ?y" 2 THEN |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
501 |
REPEAT (blast_tac (!claset addSEs partsEs) 2)); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
502 |
by (Fake_parts_insert_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
503 |
val lemma = result(); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
504 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
505 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
506 |
"!!evs. [| Crypt(pubK B) (Nonce M) : parts (sees lost Spy evs); \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
507 |
\ Crypt(pubK B') (Nonce M) : parts (sees lost Spy evs); \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
508 |
\ Nonce M ~: analz (sees lost Spy evs); \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
509 |
\ evs : tls |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
510 |
\ ==> B=B'"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
511 |
by (prove_unique_tac lemma 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
512 |
qed "unique_M"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
513 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
514 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
515 |
(*In A's note to herself, M determines A and B.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
516 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
517 |
"!!evs. [| Nonce M ~: analz (sees lost Spy evs); evs : tls |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
518 |
\ ==> EX A' B'. ALL A B. \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
519 |
\ Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
520 |
by (etac rev_mp 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
521 |
by (analz_mono_parts_induct_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
522 |
by (prove_simple_subgoals_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
523 |
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
524 |
(*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
525 |
by (expand_case_tac "M = ?y" 1 THEN |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
526 |
blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
527 |
val lemma = result(); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
528 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
529 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
530 |
"!!evs. [| Notes A {|Agent B, Nonce M|} : set evs; \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
531 |
\ Notes A' {|Agent B', Nonce M|} : set evs; \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
532 |
\ Nonce M ~: analz (sees lost Spy evs); \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
533 |
\ evs : tls |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
534 |
\ ==> A=A' & B=B'"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
535 |
by (prove_unique_tac lemma 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
536 |
qed "Notes_unique_M"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
537 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
538 |
|
3474 | 539 |
|
540 |
(*** Protocol goals: if A receives SERVER FINISHED, then B is present |
|
541 |
and has used the quoted values XA, XB, etc. Note that it is up to A |
|
542 |
to compare XA with what she originally sent. |
|
543 |
***) |
|
544 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
545 |
(*The mention of her name (A) in X assumes A that B knows who she is.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
546 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
547 |
"!!evs. [| X = Crypt (serverK(NA,NB,M)) \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
548 |
\ (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
549 |
\ Nonce NA, Agent XA, Agent A, \ |
3506 | 550 |
\ Nonce NB, Agent XB, certificate B (pubK B)|}); \ |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
551 |
\ evs : tls; A ~: lost; B ~: lost |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
552 |
\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \ |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
553 |
\ X : parts (sees lost Spy evs) --> Says B A X : set evs"; |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
554 |
by (hyp_subst_tac 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
555 |
by (analz_induct_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
556 |
by (REPEAT_FIRST (rtac impI)); |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
557 |
(*Fake: the Spy doesn't have the critical session key!*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
558 |
by (REPEAT (rtac impI 1)); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
559 |
by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
560 |
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
561 |
not_parts_not_analz]) 2); |
3474 | 562 |
by (Fake_parts_insert_tac 1); |
563 |
qed_spec_mp "TrustServerFinished"; |
|
564 |
||
565 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
566 |
(*This version refers not to SERVER FINISHED but to any message from B. |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
567 |
We don't assume B has received CERTIFICATE VERIFY, and an intruder could |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
568 |
have changed A's identity in all other messages, so we can't be sure |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
569 |
that B sends his message to A.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
570 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
571 |
"!!evs. [| evs : tls; A ~: lost; B ~: lost |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
572 |
\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
573 |
\ Crypt (serverK(NA,NB,M)) Y : parts (sees lost Spy evs) --> \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
574 |
\ (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
575 |
by (analz_induct_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
576 |
by (REPEAT_FIRST (rtac impI)); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
577 |
(*Fake: the Spy doesn't have the critical session key!*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
578 |
by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
579 |
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
580 |
not_parts_not_analz]) 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
581 |
by (Fake_parts_insert_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
582 |
(*ServerFinished. If the message is old then apply induction hypothesis...*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
583 |
by (rtac conjI 1 THEN Blast_tac 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
584 |
(*...otherwise delete induction hyp and use unicity of M.*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
585 |
by (thin_tac "?PP-->?QQ" 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
586 |
by (Step_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
587 |
by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
588 |
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
589 |
by (blast_tac (!claset addSEs [MPair_parts] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
590 |
addDs [Notes_Crypt_parts_sees, |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
591 |
Says_imp_sees_Spy' RS parts.Inj, |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
592 |
unique_M]) 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
593 |
qed_spec_mp "TrustServerMsg"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
594 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
595 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
596 |
(*** Protocol goal: if B receives any message encrypted with clientK |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
597 |
then A has sent it, ASSUMING that A chose M. Authentication is |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
598 |
assumed here; B cannot verify it. But if the message is |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
599 |
CLIENT FINISHED, then B can then check the quoted values XA, XB, etc. |
3506 | 600 |
***) |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
601 |
goal thy |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
602 |
"!!evs. [| evs : tls; A ~: lost; B ~: lost |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
603 |
\ ==> Notes A {|Agent B, Nonce M|} : set evs --> \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
604 |
\ Crypt (clientK(NA,NB,M)) Y : parts (sees lost Spy evs) --> \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
605 |
\ Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
606 |
by (analz_induct_tac 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
607 |
by (REPEAT_FIRST (rtac impI)); |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
608 |
(*Fake: the Spy doesn't have the critical session key!*) |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
609 |
by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1); |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
610 |
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
611 |
not_parts_not_analz]) 2); |
3474 | 612 |
by (Fake_parts_insert_tac 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
613 |
(*ClientFinished. If the message is old then apply induction hypothesis...*) |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
614 |
by (step_tac (!claset delrules [conjI]) 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
615 |
by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
616 |
by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
617 |
by (blast_tac (!claset addSEs [MPair_parts] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
618 |
addDs [Notes_unique_M]) 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
619 |
qed_spec_mp "TrustClientMsg"; |
3506 | 620 |
|
621 |
||
622 |
(*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to |
|
623 |
check a CERTIFICATE VERIFY from A, then A has used the quoted |
|
624 |
values XA, XB, etc. Even this one requires A to be uncompromised. |
|
625 |
***) |
|
626 |
goal thy |
|
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
627 |
"!!evs. [| Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs; \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
628 |
\ Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|} \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
629 |
\ : set evs; \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
630 |
\ Says A'' B (Crypt (priK A) \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
631 |
\ (Hash{|Nonce NB, certificate B KB, Nonce M|})) \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
632 |
\ : set evs; \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
633 |
\ evs : tls; A ~: lost; B ~: lost |] \ |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
634 |
\ ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
635 |
by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify] |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
636 |
addDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
637 |
qed "AuthClientFinished"; |