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 (spies 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 (spies 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_spies]))); |
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 (Clarify_tac 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(spies evs); \ |
117 "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ |
118 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ |
118 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ |
119 \ Nonce NA ~: analz (spies 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 |
125 |
125 |
130 (!simpset setloop split_tac [expand_if])); |
130 (!simpset setloop split_tac [expand_if])); |
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 ~: bad; B ~: bad; evs : ns_public |] \ |
136 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
137 \ ==> Nonce NA ~: analz (spies 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*) |
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 ~: bad; B ~: bad; 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_spies 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 by (ALLGOALS Clarify_tac); |
|
168 (*NS2*) |
|
169 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, |
|
170 Spy_not_see_NA, unique_NA]) 3); |
167 (*NS1*) |
171 (*NS1*) |
168 by (blast_tac (!claset addSEs spies_partsEs) 2); |
172 by (blast_tac (!claset addSEs spies_partsEs) 2); |
169 (*Fake*) |
173 (*Fake*) |
170 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
174 by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] |
171 addDs [Spy_not_see_NA, |
175 addDs [Spy_not_see_NA, |
172 impOfSubs analz_subset_parts]) 1); |
176 impOfSubs analz_subset_parts]) 1); |
173 (*NS2; not clear why blast_tac needs to be preceeded by Step_tac*) |
|
174 by (Step_tac 1); |
|
175 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, |
|
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 (spies evs); \ |
181 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
182 \ Nonce NA ~: analz (spies 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); |
188 by (Fake_parts_insert_tac 1); |
188 by (Fake_parts_insert_tac 1); |
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 (spies 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 (spies 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_spies]))); |
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 (Clarify_tac 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(spies evs); \ |
215 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies evs); \ |
216 \ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \ |
216 \ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \ |
217 \ Nonce NB ~: analz (spies 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 |
229 \ ==> Nonce NB ~: analz (spies 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 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
233 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); |
234 by clarify_tac; |
234 by (ALLGOALS Clarify_tac); |
235 (*NS3: because NB determines A*) |
235 (*NS3: because NB determines A*) |
236 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4); |
236 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4); |
237 (*NS2: by freshness and unicity of NB*) |
237 (*NS2: by freshness and unicity of NB*) |
238 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] |
238 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] |
239 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] |
239 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] |
257 by (etac rev_mp 1); |
257 by (etac rev_mp 1); |
258 (*prepare induction over Crypt (pubK B) NB : parts H*) |
258 (*prepare induction over Crypt (pubK B) NB : parts H*) |
259 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
259 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
260 by (parts_induct_tac 1); |
260 by (parts_induct_tac 1); |
261 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
261 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); |
262 by clarify_tac; |
262 by (ALLGOALS Clarify_tac); |
263 (*NS3: because NB determines A*) |
263 (*NS3: because NB determines A*) |
264 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, |
264 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, |
265 Spy_not_see_NB, unique_NB]) 3); |
265 Spy_not_see_NB, unique_NB]) 3); |
266 (*NS1: by freshness*) |
266 (*NS1: by freshness*) |
267 by (blast_tac (!claset addSEs spies_partsEs) 2); |
267 by (blast_tac (!claset addSEs spies_partsEs) 2); |
276 goal thy |
276 goal thy |
277 "!!evs. [| A ~: bad; B ~: bad; evs : ns_public |] \ |
277 "!!evs. [| A ~: bad; B ~: bad; evs : ns_public |] \ |
278 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \ |
278 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \ |
279 \ --> Nonce NB ~: analz (spies evs)"; |
279 \ --> Nonce NB ~: analz (spies evs)"; |
280 by (analz_induct_tac 1); |
280 by (analz_induct_tac 1); |
281 by clarify_tac; |
281 by (ALLGOALS Clarify_tac); |
282 (*NS2: by freshness and unicity of NB*) |
282 (*NS2: by freshness and unicity of NB*) |
283 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] |
283 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] |
284 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] |
284 addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] |
285 addEs partsEs |
285 addEs partsEs |
286 addIs [impOfSubs analz_subset_parts]) 3); |
286 addIs [impOfSubs analz_subset_parts]) 3); |