44 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
48 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
45 |
49 |
46 |
50 |
47 (** For reasoning about the encrypted portion of messages **) |
51 (** For reasoning about the encrypted portion of messages **) |
48 |
52 |
49 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \ |
53 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \ |
50 \ X : analz (spies evs)"; |
54 \ ==> X : analz (spies evs)"; |
51 by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); |
55 by (dtac (Says_imp_spies RS analz.Inj) 1); |
|
56 by (Blast_tac 1); |
52 qed "OR2_analz_spies"; |
57 qed "OR2_analz_spies"; |
53 |
58 |
54 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \ |
59 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ |
55 \ X : analz (spies evs)"; |
60 \ ==> X : analz (spies evs)"; |
56 by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); |
61 by (dtac (Says_imp_spies RS analz.Inj) 1); |
|
62 by (Blast_tac 1); |
57 qed "OR4_analz_spies"; |
63 qed "OR4_analz_spies"; |
58 |
64 |
59 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ |
65 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ |
60 \ ==> K : parts (spies evs)"; |
66 \ ==> K : parts (spies evs)"; |
61 by (blast_tac (claset() addSEs spies_partsEs) 1); |
67 by (Blast_tac 1); |
62 qed "Oops_parts_spies"; |
68 qed "Oops_parts_spies"; |
63 |
|
64 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
|
65 argument as for the Fake case. This is possible for most, but not all, |
|
66 proofs: Fake does not invent new nonces (as in OR2), and of course Fake |
|
67 messages originate from the Spy. *) |
|
68 |
69 |
69 bind_thm ("OR2_parts_spies", |
70 bind_thm ("OR2_parts_spies", |
70 OR2_analz_spies RS (impOfSubs analz_subset_parts)); |
71 OR2_analz_spies RS (impOfSubs analz_subset_parts)); |
71 bind_thm ("OR4_parts_spies", |
72 bind_thm ("OR4_parts_spies", |
72 OR4_analz_spies RS (impOfSubs analz_subset_parts)); |
73 OR4_analz_spies RS (impOfSubs analz_subset_parts)); |
123 (*** Proofs involving analz ***) |
123 (*** Proofs involving analz ***) |
124 |
124 |
125 (*Describes the form of K and NA when the Server sends this message. Also |
125 (*Describes the form of K and NA when the Server sends this message. Also |
126 for Oops case.*) |
126 for Oops case.*) |
127 goal thy |
127 goal thy |
128 "!!evs. [| Says Server B \ |
128 "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
129 \ {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
129 \ evs : otway |] \ |
130 \ evs : otway |] \ |
|
131 \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; |
130 \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; |
132 by (etac rev_mp 1); |
131 by (etac rev_mp 1); |
133 by (etac otway.induct 1); |
132 by (etac otway.induct 1); |
134 by (prove_simple_subgoals_tac 1); |
133 by (ALLGOALS Simp_tac); |
135 by (Blast_tac 1); |
134 by (ALLGOALS Blast_tac); |
136 qed "Says_Server_message_form"; |
135 qed "Says_Server_message_form"; |
137 |
136 |
138 |
137 |
139 (*For proofs involving analz.*) |
138 (*For proofs involving analz.*) |
140 val analz_spies_tac = |
139 val analz_spies_tac = |
141 dtac OR2_analz_spies 4 THEN |
140 dtac OR2_analz_spies 4 THEN |
142 dtac OR4_analz_spies 6 THEN |
141 dtac OR4_analz_spies 6 THEN |
143 forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN |
142 forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN |
144 REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); |
143 REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); |
145 |
144 |
146 |
145 |
147 (**** |
146 (**** |
148 The following is to prove theorems of the form |
147 The following is to prove theorems of the form |
190 by (etac otway.induct 1); |
189 by (etac otway.induct 1); |
191 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
190 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
192 by (ALLGOALS Clarify_tac); |
191 by (ALLGOALS Clarify_tac); |
193 (*Remaining cases: OR3 and OR4*) |
192 (*Remaining cases: OR3 and OR4*) |
194 by (ex_strip_tac 2); |
193 by (ex_strip_tac 2); |
195 by (Blast_tac 2); |
194 by (Best_tac 2); (*Blast_tac's too slow (in reconstruction)*) |
196 by (expand_case_tac "K = ?y" 1); |
195 by (expand_case_tac "K = ?y" 1); |
197 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
196 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
198 (*...we assume X is a recent message, and handle this case by contradiction*) |
197 (*...we assume X is a recent message, and handle this case by contradiction*) |
199 by (blast_tac (claset() addSEs spies_partsEs |
198 by (blast_tac (claset() addSEs spies_partsEs) 1); |
200 delrules [conjI] (*no split-up to 4 subgoals*)) 1); |
|
201 val lemma = result(); |
199 val lemma = result(); |
202 |
200 |
203 goal thy |
201 goal thy |
204 "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \ |
202 "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \ |
205 \ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \ |
203 \ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \ |
206 \ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"; |
204 \ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"; |
207 by (prove_unique_tac lemma 1); |
205 by (prove_unique_tac lemma 1); |
208 qed "unique_session_keys"; |
206 qed "unique_session_keys"; |
209 |
207 |
210 |
208 |
211 (*Crucial security property, but not itself enough to guarantee correctness!*) |
209 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
212 goal thy |
210 Does not in itself guarantee security: an attack could violate |
213 "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \ |
211 the premises, e.g. by having A=Spy **) |
|
212 |
|
213 goal thy |
|
214 "!!evs. [| A ~: bad; B ~: bad; evs : otway |] \ |
214 \ ==> Says Server B \ |
215 \ ==> Says Server B \ |
215 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
216 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
216 \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ |
217 \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ |
217 \ Says B Spy {|NA, NB, Key K|} ~: set evs --> \ |
218 \ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ |
218 \ Key K ~: analz (spies evs)"; |
219 \ Key K ~: analz (spies evs)"; |
219 by (etac otway.induct 1); |
220 by (etac otway.induct 1); |
220 by analz_spies_tac; |
221 by analz_spies_tac; |
221 by (ALLGOALS |
222 by (ALLGOALS |
222 (asm_simp_tac (simpset() addcongs [conj_cong] |
223 (asm_simp_tac (simpset() addcongs [conj_cong] |
223 addsimps [analz_insert_eq, analz_insert_freshK] |
224 addsimps [analz_insert_eq, analz_insert_freshK] |
224 addsimps (pushes@expand_ifs)))); |
225 addsimps (pushes@expand_ifs)))); |
225 (*Oops*) |
226 (*Oops*) |
226 by (blast_tac (claset() addSDs [unique_session_keys]) 4); |
227 by (blast_tac (claset() addSDs [unique_session_keys]) 4); |
227 (*OR4*) |
228 (*OR4*) |
228 by (Blast_tac 3); |
229 by (Blast_tac 3); |
229 (*OR3*) |
230 (*OR3*) |
230 by (blast_tac (claset() addSEs spies_partsEs |
231 by (Blast_tac 2); |
231 addIs [impOfSubs analz_subset_parts]) 2); |
|
232 (*Fake*) |
232 (*Fake*) |
233 by (spy_analz_tac 1); |
233 by (spy_analz_tac 1); |
234 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
234 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
235 |
235 |
236 goal thy |
236 goal thy |
237 "!!evs. [| Says Server B \ |
237 "!!evs. [| Says Server B \ |
238 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
238 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
239 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
239 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
240 \ Says B Spy {|NA, NB, Key K|} ~: set evs; \ |
240 \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
241 \ A ~: bad; B ~: bad; evs : otway |] \ |
241 \ A ~: bad; B ~: bad; evs : otway |] \ |
242 \ ==> Key K ~: analz (spies evs)"; |
242 \ ==> Key K ~: analz (spies evs)"; |
243 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
243 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
244 by (blast_tac (claset() addSEs [lemma]) 1); |
244 by (blast_tac (claset() addSEs [lemma]) 1); |
245 qed "Spy_not_see_encrypted_key"; |
245 qed "Spy_not_see_encrypted_key"; |
246 |
246 |
255 "!!evs. [| A ~: bad; A ~= B; evs : otway |] \ |
255 "!!evs. [| A ~: bad; A ~= B; evs : otway |] \ |
256 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \ |
256 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \ |
257 \ Says A B {|NA, Agent A, Agent B, \ |
257 \ Says A B {|NA, Agent A, Agent B, \ |
258 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs"; |
258 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs"; |
259 by (parts_induct_tac 1); |
259 by (parts_induct_tac 1); |
260 by (Fake_parts_insert_tac 1); |
260 by (ALLGOALS Blast_tac); |
261 by (Blast_tac 1); |
|
262 qed_spec_mp "Crypt_imp_OR1"; |
261 qed_spec_mp "Crypt_imp_OR1"; |
263 |
262 |
264 |
263 |
265 (*Crucial property: If the encrypted message appears, and A has used NA |
264 (*Crucial property: If the encrypted message appears, and A has used NA |
266 to start a run, then it originated with the Server!*) |
265 to start a run, then it originated with the Server!*) |
275 \ (EX B NB. Says Server B \ |
274 \ (EX B NB. Says Server B \ |
276 \ {|NA, \ |
275 \ {|NA, \ |
277 \ Crypt (shrK A) {|NA, Key K|}, \ |
276 \ Crypt (shrK A) {|NA, Key K|}, \ |
278 \ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; |
277 \ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; |
279 by (parts_induct_tac 1); |
278 by (parts_induct_tac 1); |
280 by (Fake_parts_insert_tac 1); |
279 (*Fake*) |
|
280 by (Blast_tac 1); |
281 (*OR1: it cannot be a new Nonce, contradiction.*) |
281 (*OR1: it cannot be a new Nonce, contradiction.*) |
282 by (blast_tac (claset() addSIs [parts_insertI] |
282 by (Blast_tac 1); |
283 addSEs spies_partsEs) 1); |
|
284 (*OR3 and OR4*) |
283 (*OR3 and OR4*) |
285 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); |
284 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); |
286 by (ALLGOALS Clarify_tac); |
285 by (ALLGOALS Clarify_tac); |
287 (*OR4*) |
286 (*OR4*) |
288 by (blast_tac (claset() addSIs [Crypt_imp_OR1] |
287 by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2); |
289 addEs spies_partsEs) 2); |
|
290 (*OR3*) (** LEVEL 5 **) |
288 (*OR3*) (** LEVEL 5 **) |
291 (*The hypotheses at this point suggest an attack in which nonce NB is used |
289 (*The hypotheses at this point suggest an attack in which nonce NB is used |
292 in two different roles: |
290 in two different roles: |
293 Says B' Server |
291 Says B' Server |
294 {|Nonce NA, Agent Aa, Agent A, |
292 {|Nonce NA, Agent Aa, Agent A, |