38 Addsimps [not_Says_to_self]; |
38 Addsimps [not_Says_to_self]; |
39 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
39 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
40 |
40 |
41 |
41 |
42 (*Induction for regularity theorems. If induction formula has the form |
42 (*Induction for regularity theorems. If induction formula has the form |
43 X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding |
43 X ~: analz (spies evs) --> ... then it shortens the proof by discarding |
44 needless information about analz (insert X (sees Spy evs)) *) |
44 needless information about analz (insert X (spies evs)) *) |
45 fun parts_induct_tac i = |
45 fun parts_induct_tac i = |
46 etac ns_public.induct i |
46 etac ns_public.induct i |
47 THEN |
47 THEN |
48 REPEAT (FIRSTGOAL analz_mono_contra_tac) |
48 REPEAT (FIRSTGOAL analz_mono_contra_tac) |
49 THEN |
49 THEN |
50 prove_simple_subgoals_tac i; |
50 prove_simple_subgoals_tac i; |
51 |
51 |
52 |
52 |
53 (** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY |
53 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
54 sends messages containing X! **) |
54 sends messages containing X! **) |
55 |
55 |
56 (*Spy never sees another agent's private key! (unless it's lost at start)*) |
56 (*Spy never sees another agent's private key! (unless it's bad at start)*) |
57 goal thy |
57 goal thy |
58 "!!A. evs: ns_public ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)"; |
58 "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; |
59 by (parts_induct_tac 1); |
59 by (parts_induct_tac 1); |
60 by (Fake_parts_insert_tac 1); |
60 by (Fake_parts_insert_tac 1); |
61 qed "Spy_see_priK"; |
61 qed "Spy_see_priK"; |
62 Addsimps [Spy_see_priK]; |
62 Addsimps [Spy_see_priK]; |
63 |
63 |
64 goal thy |
64 goal thy |
65 "!!A. evs: ns_public ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)"; |
65 "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; |
66 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
66 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
67 qed "Spy_analz_priK"; |
67 qed "Spy_analz_priK"; |
68 Addsimps [Spy_analz_priK]; |
68 Addsimps [Spy_analz_priK]; |
69 |
69 |
70 goal thy "!!A. [| Key (priK A) : parts (sees Spy evs); \ |
70 goal thy "!!A. [| Key (priK A) : parts (spies evs); \ |
71 \ evs : ns_public |] ==> A:lost"; |
71 \ evs : ns_public |] ==> A:bad"; |
72 by (blast_tac (!claset addDs [Spy_see_priK]) 1); |
72 by (blast_tac (!claset addDs [Spy_see_priK]) 1); |
73 qed "Spy_see_priK_D"; |
73 qed "Spy_see_priK_D"; |
74 |
74 |
75 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); |
75 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); |
76 AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; |
76 AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; |
79 (**** Authenticity properties obtained from NS2 ****) |
79 (**** Authenticity properties obtained from NS2 ****) |
80 |
80 |
81 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
81 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
82 is secret. (Honest users generate fresh nonces.)*) |
82 is secret. (Honest users generate fresh nonces.)*) |
83 goal thy |
83 goal thy |
84 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \ |
84 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
85 \ Nonce NA ~: analz (sees Spy evs); evs : ns_public |] \ |
85 \ Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
86 \ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees Spy evs)"; |
86 \ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies evs)"; |
87 by (etac rev_mp 1); |
87 by (etac rev_mp 1); |
88 by (etac rev_mp 1); |
88 by (etac rev_mp 1); |
89 by (parts_induct_tac 1); |
89 by (parts_induct_tac 1); |
90 (*NS3*) |
90 (*NS3*) |
91 by (blast_tac (!claset addSEs partsEs) 3); |
91 by (blast_tac (!claset addSEs partsEs) 3); |
95 qed "no_nonce_NS1_NS2"; |
95 qed "no_nonce_NS1_NS2"; |
96 |
96 |
97 |
97 |
98 (*Unicity for NS1: nonce NA identifies agents A and B*) |
98 (*Unicity for NS1: nonce NA identifies agents A and B*) |
99 goal thy |
99 goal thy |
100 "!!evs. [| Nonce NA ~: analz (sees Spy evs); evs : ns_public |] \ |
100 "!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
101 \ ==> EX A' B'. ALL A B. \ |
101 \ ==> EX A' B'. ALL A B. \ |
102 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs) --> \ |
102 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ |
103 \ A=A' & B=B'"; |
103 \ A=A' & B=B'"; |
104 by (etac rev_mp 1); |
104 by (etac rev_mp 1); |
105 by (parts_induct_tac 1); |
105 by (parts_induct_tac 1); |
106 by (ALLGOALS |
106 by (ALLGOALS |
107 (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]))); |
107 (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]))); |
108 (*NS1*) |
108 (*NS1*) |
109 by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); |
109 by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); |
110 (*Fake*) |
110 (*Fake*) |
111 by (step_tac (!claset addSIs [analz_insertI]) 1); |
111 by (step_tac (!claset addSIs [analz_insertI]) 1); |
112 by (ex_strip_tac 1); |
112 by (ex_strip_tac 1); |
113 by (Fake_parts_insert_tac 1); |
113 by (Fake_parts_insert_tac 1); |
114 val lemma = result(); |
114 val lemma = result(); |
115 |
115 |
116 goal thy |
116 goal thy |
117 "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees Spy evs); \ |
117 "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ |
118 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees Spy evs); \ |
118 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ |
119 \ Nonce NA ~: analz (sees Spy evs); \ |
119 \ Nonce NA ~: analz (spies evs); \ |
120 \ evs : ns_public |] \ |
120 \ evs : ns_public |] \ |
121 \ ==> A=A' & B=B'"; |
121 \ ==> A=A' & B=B'"; |
122 by (prove_unique_tac lemma 1); |
122 by (prove_unique_tac lemma 1); |
123 qed "unique_NA"; |
123 qed "unique_NA"; |
124 |
124 |
131 |
131 |
132 |
132 |
133 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
133 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
134 goal thy |
134 goal thy |
135 "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
135 "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
136 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
136 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
137 \ ==> Nonce NA ~: analz (sees Spy evs)"; |
137 \ ==> Nonce NA ~: analz (spies evs)"; |
138 by (etac rev_mp 1); |
138 by (etac rev_mp 1); |
139 by (analz_induct_tac 1); |
139 by (analz_induct_tac 1); |
140 (*NS3*) |
140 (*NS3*) |
141 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj] |
141 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] |
142 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); |
142 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); |
143 (*NS2*) |
143 (*NS2*) |
144 by (blast_tac (!claset addSEs [MPair_parts] |
144 by (blast_tac (!claset addSEs [MPair_parts] |
145 addDs [Says_imp_sees_Spy RS parts.Inj, |
145 addDs [Says_imp_spies RS parts.Inj, |
146 parts.Body, unique_NA]) 3); |
146 parts.Body, unique_NA]) 3); |
147 (*NS1*) |
147 (*NS1*) |
148 by (blast_tac (!claset addSEs sees_Spy_partsEs |
148 by (blast_tac (!claset addSEs spies_partsEs |
149 addIs [impOfSubs analz_subset_parts]) 2); |
149 addIs [impOfSubs analz_subset_parts]) 2); |
150 (*Fake*) |
150 (*Fake*) |
151 by (spy_analz_tac 1); |
151 by (spy_analz_tac 1); |
152 qed "Spy_not_see_NA"; |
152 qed "Spy_not_see_NA"; |
153 |
153 |
155 (*Authentication for A: if she receives message 2 and has used NA |
155 (*Authentication for A: if she receives message 2 and has used NA |
156 to start a run, then B has sent message 2.*) |
156 to start a run, then B has sent message 2.*) |
157 goal thy |
157 goal thy |
158 "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
158 "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
159 \ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs; \ |
159 \ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs; \ |
160 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
160 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
161 \ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs"; |
161 \ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs"; |
162 by (etac rev_mp 1); |
162 by (etac rev_mp 1); |
163 (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*) |
163 (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*) |
164 by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1); |
164 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
165 by (etac ns_public.induct 1); |
165 by (etac ns_public.induct 1); |
166 by (ALLGOALS Asm_simp_tac); |
166 by (ALLGOALS Asm_simp_tac); |
167 (*NS1*) |
167 (*NS1*) |
168 by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); |
168 by (blast_tac (!claset addSEs spies_partsEs) 2); |
169 (*Fake*) |
169 (*Fake*) |
170 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
170 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
171 addDs [Spy_not_see_NA, |
171 addDs [Spy_not_see_NA, |
172 impOfSubs analz_subset_parts]) 1); |
172 impOfSubs analz_subset_parts]) 1); |
173 (*NS2; not clear why blast_tac needs to be preceeded by Step_tac*) |
173 (*NS2; not clear why blast_tac needs to be preceeded by Step_tac*) |
174 by (Step_tac 1); |
174 by (Step_tac 1); |
175 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj, |
175 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, |
176 Spy_not_see_NA, unique_NA]) 1); |
176 Spy_not_see_NA, unique_NA]) 1); |
177 qed "A_trusts_NS2"; |
177 qed "A_trusts_NS2"; |
178 |
178 |
179 (*If the encrypted message appears then it originated with Alice in NS1*) |
179 (*If the encrypted message appears then it originated with Alice in NS1*) |
180 goal thy |
180 goal thy |
181 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees Spy evs); \ |
181 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
182 \ Nonce NA ~: analz (sees Spy evs); \ |
182 \ Nonce NA ~: analz (spies evs); \ |
183 \ evs : ns_public |] \ |
183 \ evs : ns_public |] \ |
184 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; |
184 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; |
185 by (etac rev_mp 1); |
185 by (etac rev_mp 1); |
186 by (etac rev_mp 1); |
186 by (etac rev_mp 1); |
187 by (parts_induct_tac 1); |
187 by (parts_induct_tac 1); |
193 (**** Authenticity properties obtained from NS2 ****) |
193 (**** Authenticity properties obtained from NS2 ****) |
194 |
194 |
195 (*Unicity for NS2: nonce NB identifies agent A and nonce NA |
195 (*Unicity for NS2: nonce NB identifies agent A and nonce NA |
196 [proof closely follows that for unique_NA] *) |
196 [proof closely follows that for unique_NA] *) |
197 goal thy |
197 goal thy |
198 "!!evs. [| Nonce NB ~: analz (sees Spy evs); evs : ns_public |] \ |
198 "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \ |
199 \ ==> EX A' NA'. ALL A NA. \ |
199 \ ==> EX A' NA'. ALL A NA. \ |
200 \ Crypt (pubK A) {|Nonce NA, Nonce NB|} \ |
200 \ Crypt (pubK A) {|Nonce NA, Nonce NB|} \ |
201 \ : parts (sees Spy evs) --> A=A' & NA=NA'"; |
201 \ : parts (spies evs) --> A=A' & NA=NA'"; |
202 by (etac rev_mp 1); |
202 by (etac rev_mp 1); |
203 by (parts_induct_tac 1); |
203 by (parts_induct_tac 1); |
204 by (ALLGOALS |
204 by (ALLGOALS |
205 (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]))); |
205 (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]))); |
206 (*NS2*) |
206 (*NS2*) |
207 by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); |
207 by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2); |
208 (*Fake*) |
208 (*Fake*) |
209 by (step_tac (!claset addSIs [analz_insertI]) 1); |
209 by (step_tac (!claset addSIs [analz_insertI]) 1); |
210 by (ex_strip_tac 1); |
210 by (ex_strip_tac 1); |
211 by (Fake_parts_insert_tac 1); |
211 by (Fake_parts_insert_tac 1); |
212 val lemma = result(); |
212 val lemma = result(); |
213 |
213 |
214 goal thy |
214 goal thy |
215 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(sees Spy evs); \ |
215 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies evs); \ |
216 \ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees Spy evs); \ |
216 \ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \ |
217 \ Nonce NB ~: analz (sees Spy evs); \ |
217 \ Nonce NB ~: analz (spies evs); \ |
218 \ evs : ns_public |] \ |
218 \ evs : ns_public |] \ |
219 \ ==> A=A' & NA=NA'"; |
219 \ ==> A=A' & NA=NA'"; |
220 by (prove_unique_tac lemma 1); |
220 by (prove_unique_tac lemma 1); |
221 qed "unique_NB"; |
221 qed "unique_NB"; |
222 |
222 |
223 |
223 |
224 (*NB remains secret PROVIDED Alice never responds with round 3*) |
224 (*NB remains secret PROVIDED Alice never responds with round 3*) |
225 goal thy |
225 goal thy |
226 "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ |
226 "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ |
227 \ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs); \ |
227 \ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs); \ |
228 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
228 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
229 \ ==> Nonce NB ~: analz (sees Spy evs)"; |
229 \ ==> Nonce NB ~: analz (spies evs)"; |
230 by (etac rev_mp 1); |
230 by (etac rev_mp 1); |
231 by (etac rev_mp 1); |
231 by (etac rev_mp 1); |
232 by (analz_induct_tac 1); |
232 by (analz_induct_tac 1); |
233 (*NS1*) |
233 (*NS1*) |
234 by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); |
234 by (blast_tac (!claset addSEs spies_partsEs) 2); |
235 (*Fake*) |
235 (*Fake*) |
236 by (spy_analz_tac 1); |
236 by (spy_analz_tac 1); |
237 (*NS2 and NS3*) |
237 (*NS2 and NS3*) |
238 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
238 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
239 by (step_tac (!claset delrules [allI]) 1); |
239 by (step_tac (!claset delrules [allI]) 1); |
240 by (Blast_tac 5); |
240 by (Blast_tac 5); |
241 (*NS3*) |
241 (*NS3*) |
242 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj, unique_NB]) 4); |
242 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4); |
243 (*NS2*) |
243 (*NS2*) |
244 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); |
244 by (blast_tac (!claset addSEs spies_partsEs) 3); |
245 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] |
245 by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj] |
246 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2); |
246 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2); |
247 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); |
247 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); |
248 qed "Spy_not_see_NB"; |
248 qed "Spy_not_see_NB"; |
249 |
249 |
250 |
250 |
252 (*Authentication for B: if he receives message 3 and has used NB |
252 (*Authentication for B: if he receives message 3 and has used NB |
253 in message 2, then A has sent message 3--to somebody....*) |
253 in message 2, then A has sent message 3--to somebody....*) |
254 goal thy |
254 goal thy |
255 "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ |
255 "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ |
256 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
256 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
257 \ A ~: lost; B ~: lost; evs : ns_public |] \ |
257 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
258 \ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs"; |
258 \ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs"; |
259 by (etac rev_mp 1); |
259 by (etac rev_mp 1); |
260 (*prepare induction over Crypt (pubK B) NB : parts H*) |
260 (*prepare induction over Crypt (pubK B) NB : parts H*) |
261 by (etac (Says_imp_sees_Spy RS parts.Inj RS rev_mp) 1); |
261 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
262 by (parts_induct_tac 1); |
262 by (parts_induct_tac 1); |
263 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
263 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
264 (*NS1*) |
264 (*NS1*) |
265 by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); |
265 by (blast_tac (!claset addSEs spies_partsEs) 2); |
266 (*Fake*) |
266 (*Fake*) |
267 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
267 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
268 addDs [Spy_not_see_NB, |
268 addDs [Spy_not_see_NB, |
269 impOfSubs analz_subset_parts]) 1); |
269 impOfSubs analz_subset_parts]) 1); |
270 (*NS3; not clear why blast_tac needs to be preceeded by Step_tac*) |
270 (*NS3; not clear why blast_tac needs to be preceeded by Step_tac*) |
271 by (Step_tac 1); |
271 by (Step_tac 1); |
272 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj, |
272 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, |
273 Spy_not_see_NB, unique_NB]) 1); |
273 Spy_not_see_NB, unique_NB]) 1); |
274 qed "B_trusts_NS3"; |
274 qed "B_trusts_NS3"; |
275 |
275 |
276 |
276 |
277 (*Can we strengthen the secrecy theorem? NO*) |
277 (*Can we strengthen the secrecy theorem? NO*) |
278 goal thy |
278 goal thy |
279 "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ |
279 "!!evs. [| A ~: bad; B ~: bad; evs : ns_public |] \ |
280 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \ |
280 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \ |
281 \ --> Nonce NB ~: analz (sees Spy evs)"; |
281 \ --> Nonce NB ~: analz (spies evs)"; |
282 by (analz_induct_tac 1); |
282 by (analz_induct_tac 1); |
283 (*NS1*) |
283 (*NS1*) |
284 by (blast_tac (!claset addSEs partsEs |
284 by (blast_tac (!claset addSEs partsEs |
285 addSDs [Says_imp_sees_Spy RS parts.Inj]) 2); |
285 addSDs [Says_imp_spies RS parts.Inj]) 2); |
286 (*Fake*) |
286 (*Fake*) |
287 by (spy_analz_tac 1); |
287 by (spy_analz_tac 1); |
288 (*NS2 and NS3*) |
288 (*NS2 and NS3*) |
289 by (Step_tac 1); |
289 by (Step_tac 1); |
290 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1); |
290 by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1); |
291 (*NS2*) |
291 (*NS2*) |
292 by (blast_tac (!claset addSEs partsEs |
292 by (blast_tac (!claset addSEs partsEs |
293 addSDs [Says_imp_sees_Spy RS parts.Inj]) 2); |
293 addSDs [Says_imp_spies RS parts.Inj]) 2); |
294 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] |
294 by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj] |
295 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); |
295 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); |
296 (*NS3*) |
296 (*NS3*) |
297 by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy RS parts.Inj RS unique_NB) 1 |
297 by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1 |
298 THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy RS parts.Inj] 1)); |
298 THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1)); |
299 by (Step_tac 1); |
299 by (Step_tac 1); |
300 |
300 |
301 (* |
301 (* |
302 THIS IS THE ATTACK! |
302 THIS IS THE ATTACK! |
303 Level 9 |
303 Level 9 |
304 !!evs. [| A ~: lost; B ~: lost; evs : ns_public |] |
304 !!evs. [| A ~: bad; B ~: bad; evs : ns_public |] |
305 ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) |
305 ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) |
306 : set evs --> |
306 : set evs --> |
307 Nonce NB ~: analz (sees Spy evs) |
307 Nonce NB ~: analz (spies evs) |
308 1. !!evs Aa Ba B' NAa NBa evsa. |
308 1. !!evs Aa Ba B' NAa NBa evsa. |
309 [| A ~: lost; B ~: lost; evsa : ns_public; A ~= Ba; |
309 [| A ~: bad; B ~: bad; evsa : ns_public; A ~= Ba; |
310 Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa; |
310 Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa; |
311 Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set evsa; |
311 Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set evsa; |
312 Ba : lost; |
312 Ba : bad; |
313 Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa; |
313 Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evsa; |
314 Nonce NB ~: analz (sees Spy evsa) |] |
314 Nonce NB ~: analz (spies evsa) |] |
315 ==> False |
315 ==> False |
316 *) |
316 *) |