48 |
45 |
49 |
46 |
50 (** For reasoning about the encrypted portion of messages **) |
47 (** For reasoning about the encrypted portion of messages **) |
51 |
48 |
52 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \ |
49 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \ |
53 \ X : analz (sees lost Spy evs)"; |
50 \ X : analz (sees Spy evs)"; |
54 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); |
51 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
55 qed "OR2_analz_sees_Spy"; |
52 qed "OR2_analz_sees_Spy"; |
56 |
53 |
57 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \ |
54 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \ |
58 \ X : analz (sees lost Spy evs)"; |
55 \ X : analz (sees Spy evs)"; |
59 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); |
56 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); |
60 qed "OR4_analz_sees_Spy"; |
57 qed "OR4_analz_sees_Spy"; |
61 |
58 |
62 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ |
59 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ |
63 \ ==> K : parts (sees lost Spy evs)"; |
60 \ ==> K : parts (sees Spy evs)"; |
64 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
61 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); |
65 qed "Oops_parts_sees_Spy"; |
62 qed "Oops_parts_sees_Spy"; |
66 |
63 |
67 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
64 (*OR2_analz... and OR4_analz... let us treat those cases using the same |
68 argument as for the Fake case. This is possible for most, but not all, |
65 argument as for the Fake case. This is possible for most, but not all, |
72 bind_thm ("OR2_parts_sees_Spy", |
69 bind_thm ("OR2_parts_sees_Spy", |
73 OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
70 OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
74 bind_thm ("OR4_parts_sees_Spy", |
71 bind_thm ("OR4_parts_sees_Spy", |
75 OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
72 OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
76 |
73 |
77 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) |
74 (*For proving the easier theorems about X ~: parts (sees Spy evs).*) |
78 val parts_induct_tac = |
75 fun parts_induct_tac i = |
79 etac otway.induct 1 THEN |
76 etac otway.induct i THEN |
80 forward_tac [OR2_parts_sees_Spy] 4 THEN |
77 forward_tac [Oops_parts_sees_Spy] (i+6) THEN |
81 forward_tac [OR4_parts_sees_Spy] 6 THEN |
78 forward_tac [OR4_parts_sees_Spy] (i+5) THEN |
82 forward_tac [Oops_parts_sees_Spy] 7 THEN |
79 forward_tac [OR2_parts_sees_Spy] (i+3) THEN |
83 prove_simple_subgoals_tac 1; |
80 prove_simple_subgoals_tac i; |
84 |
81 |
85 |
82 |
86 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
83 (** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY |
87 sends messages containing X! **) |
84 sends messages containing X! **) |
88 |
85 |
89 (*Spy never sees another agent's shared key! (unless it's lost at start)*) |
86 (*Spy never sees another agent's shared key! (unless it's lost at start)*) |
90 goal thy |
87 goal thy |
91 "!!evs. evs : otway \ |
88 "!!evs. evs : otway ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)"; |
92 \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; |
89 by (parts_induct_tac 1); |
93 by parts_induct_tac; |
|
94 by (Fake_parts_insert_tac 1); |
90 by (Fake_parts_insert_tac 1); |
95 by (Blast_tac 1); |
91 by (Blast_tac 1); |
96 qed "Spy_see_shrK"; |
92 qed "Spy_see_shrK"; |
97 Addsimps [Spy_see_shrK]; |
93 Addsimps [Spy_see_shrK]; |
98 |
94 |
99 goal thy |
95 goal thy |
100 "!!evs. evs : otway \ |
96 "!!evs. evs : otway ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)"; |
101 \ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; |
|
102 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
97 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
103 qed "Spy_analz_shrK"; |
98 qed "Spy_analz_shrK"; |
104 Addsimps [Spy_analz_shrK]; |
99 Addsimps [Spy_analz_shrK]; |
105 |
100 |
106 goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
101 goal thy "!!A. [| Key (shrK A) : parts (sees Spy evs); \ |
107 \ evs : otway |] ==> A:lost"; |
102 \ evs : otway |] ==> A:lost"; |
108 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
103 by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
109 qed "Spy_see_shrK_D"; |
104 qed "Spy_see_shrK_D"; |
110 |
105 |
111 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
106 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
112 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
107 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
113 |
108 |
114 |
109 |
115 (*Nobody can have used non-existent keys!*) |
110 (*Nobody can have used non-existent keys!*) |
116 goal thy "!!evs. evs : otway ==> \ |
111 goal thy "!!evs. evs : otway ==> \ |
117 \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; |
112 \ Key K ~: used evs --> K ~: keysFor (parts (sees Spy evs))"; |
118 by parts_induct_tac; |
113 by (parts_induct_tac 1); |
119 (*Fake*) |
114 (*Fake*) |
120 by (best_tac |
115 by (best_tac |
121 (!claset addIs [impOfSubs analz_subset_parts] |
116 (!claset addIs [impOfSubs analz_subset_parts] |
122 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
117 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
123 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
118 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
159 |
154 |
160 |
155 |
161 (**** |
156 (**** |
162 The following is to prove theorems of the form |
157 The following is to prove theorems of the form |
163 |
158 |
164 Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> |
159 Key K : analz (insert (Key KAB) (sees Spy evs)) ==> |
165 Key K : analz (sees lost Spy evs) |
160 Key K : analz (sees Spy evs) |
166 |
161 |
167 A more general formula must be proved inductively. |
162 A more general formula must be proved inductively. |
168 ****) |
163 ****) |
169 |
164 |
170 |
165 |
171 (** Session keys are not used to encrypt other session keys **) |
166 (** Session keys are not used to encrypt other session keys **) |
172 |
167 |
173 (*The equality makes the induction hypothesis easier to apply*) |
168 (*The equality makes the induction hypothesis easier to apply*) |
174 goal thy |
169 goal thy |
175 "!!evs. evs : otway ==> \ |
170 "!!evs. evs : otway ==> \ |
176 \ ALL K KK. KK <= Compl (range shrK) --> \ |
171 \ ALL K KK. KK <= Compl (range shrK) --> \ |
177 \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ |
172 \ (Key K : analz (Key``KK Un (sees Spy evs))) = \ |
178 \ (K : KK | Key K : analz (sees lost Spy evs))"; |
173 \ (K : KK | Key K : analz (sees Spy evs))"; |
179 by (etac otway.induct 1); |
174 by (etac otway.induct 1); |
180 by analz_sees_tac; |
175 by analz_sees_tac; |
181 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
176 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
182 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
177 by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); |
183 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
178 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
229 "!!evs. [| A ~: lost; B ~: lost; evs : otway |] \ |
224 "!!evs. [| A ~: lost; B ~: lost; evs : otway |] \ |
230 \ ==> Says Server B \ |
225 \ ==> Says Server B \ |
231 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
226 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
232 \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ |
227 \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ |
233 \ Says B Spy {|NA, NB, Key K|} ~: set evs --> \ |
228 \ Says B Spy {|NA, NB, Key K|} ~: set evs --> \ |
234 \ Key K ~: analz (sees lost Spy evs)"; |
229 \ Key K ~: analz (sees Spy evs)"; |
235 by (etac otway.induct 1); |
230 by (etac otway.induct 1); |
236 by analz_sees_tac; |
231 by analz_sees_tac; |
237 by (ALLGOALS |
232 by (ALLGOALS |
238 (asm_simp_tac (!simpset addcongs [conj_cong] |
233 (asm_simp_tac (!simpset addcongs [conj_cong] |
239 addsimps [analz_insert_eq, not_parts_not_analz, |
234 addsimps [analz_insert_eq, not_parts_not_analz, |
254 "!!evs. [| Says Server B \ |
249 "!!evs. [| Says Server B \ |
255 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
250 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
256 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
251 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
257 \ Says B Spy {|NA, NB, Key K|} ~: set evs; \ |
252 \ Says B Spy {|NA, NB, Key K|} ~: set evs; \ |
258 \ A ~: lost; B ~: lost; evs : otway |] \ |
253 \ A ~: lost; B ~: lost; evs : otway |] \ |
259 \ ==> Key K ~: analz (sees lost Spy evs)"; |
254 \ ==> Key K ~: analz (sees Spy evs)"; |
260 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
255 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
261 by (blast_tac (!claset addSEs [lemma]) 1); |
256 by (blast_tac (!claset addSEs [lemma]) 1); |
262 qed "Spy_not_see_encrypted_key"; |
257 qed "Spy_not_see_encrypted_key"; |
263 |
258 |
264 |
259 |
269 Perhaps it's because OR2 has two similar-looking encrypted messages in |
264 Perhaps it's because OR2 has two similar-looking encrypted messages in |
270 this version.*) |
265 this version.*) |
271 goal thy |
266 goal thy |
272 "!!evs. [| A ~: lost; A ~= B; evs : otway |] \ |
267 "!!evs. [| A ~: lost; A ~= B; evs : otway |] \ |
273 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
268 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \ |
274 \ : parts (sees lost Spy evs) --> \ |
269 \ : parts (sees Spy evs) --> \ |
275 \ Says A B {|NA, Agent A, Agent B, \ |
270 \ Says A B {|NA, Agent A, Agent B, \ |
276 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs"; |
271 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs"; |
277 by parts_induct_tac; |
272 by (parts_induct_tac 1); |
278 by (Fake_parts_insert_tac 1); |
273 by (Fake_parts_insert_tac 1); |
279 by (Blast_tac 1); |
274 by (Blast_tac 1); |
280 qed_spec_mp "Crypt_imp_OR1"; |
275 qed_spec_mp "Crypt_imp_OR1"; |
281 |
276 |
282 |
277 |
283 (*Crucial property: If the encrypted message appears, and A has used NA |
278 (*Crucial property: If the encrypted message appears, and A has used NA |
284 to start a run, then it originated with the Server!*) |
279 to start a run, then it originated with the Server!*) |
285 (*Only it is FALSE. Somebody could make a fake message to Server |
280 (*Only it is FALSE. Somebody could make a fake message to Server |
286 substituting some other nonce NA' for NB.*) |
281 substituting some other nonce NA' for NB.*) |
287 goal thy |
282 goal thy |
288 "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \ |
283 "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \ |
289 \ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \ |
284 \ ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs) --> \ |
290 \ Says A B {|NA, Agent A, Agent B, \ |
285 \ Says A B {|NA, Agent A, Agent B, \ |
291 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
286 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
292 \ : set evs --> \ |
287 \ : set evs --> \ |
293 \ (EX B NB. Says Server B \ |
288 \ (EX B NB. Says Server B \ |
294 \ {|NA, \ |
289 \ {|NA, \ |
295 \ Crypt (shrK A) {|NA, Key K|}, \ |
290 \ Crypt (shrK A) {|NA, Key K|}, \ |
296 \ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; |
291 \ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; |
297 by parts_induct_tac; |
292 by (parts_induct_tac 1); |
298 by (Fake_parts_insert_tac 1); |
293 by (Fake_parts_insert_tac 1); |
299 (*OR1: it cannot be a new Nonce, contradiction.*) |
294 (*OR1: it cannot be a new Nonce, contradiction.*) |
300 by (blast_tac (!claset addSIs [parts_insertI] |
295 by (blast_tac (!claset addSIs [parts_insertI] |
301 addSEs sees_Spy_partsEs) 1); |
296 addSEs sees_Spy_partsEs) 1); |
302 (*OR4*) |
297 (*OR4*) |