15 AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; |
15 AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; |
16 AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; |
16 AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; |
17 |
17 |
18 |
18 |
19 (*A "possibility property": there are traces that reach the end*) |
19 (*A "possibility property": there are traces that reach the end*) |
20 Goal "B ~= Server \ |
20 Goal "B \\<noteq> Server \ |
21 \ ==> \\<exists>NA K. \\<exists>evs \\<in> otway. \ |
21 \ ==> \\<exists>NA K. \\<exists>evs \\<in> otway. \ |
22 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ |
22 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ |
23 \ : set evs"; |
23 \ \\<in> set evs"; |
24 by (REPEAT (resolve_tac [exI,bexI] 1)); |
24 by (REPEAT (resolve_tac [exI,bexI] 1)); |
25 by (rtac (otway.Nil RS |
25 by (rtac (otway.Nil RS |
26 otway.OR1 RS otway.Reception RS |
26 otway.OR1 RS otway.Reception RS |
27 otway.OR2 RS otway.Reception RS |
27 otway.OR2 RS otway.Reception RS |
28 otway.OR3 RS otway.Reception RS otway.OR4) 2); |
28 otway.OR3 RS otway.Reception RS otway.OR4) 2); |
29 by possibility_tac; |
29 by possibility_tac; |
30 result(); |
30 result(); |
31 |
31 |
32 Goal "[| Gets B X : set evs; evs : otway |] ==> \\<exists>A. Says A B X : set evs"; |
32 Goal "[| Gets B X \\<in> set evs; evs \\<in> otway |] ==> \\<exists>A. Says A B X \\<in> set evs"; |
33 by (etac rev_mp 1); |
33 by (etac rev_mp 1); |
34 by (etac otway.induct 1); |
34 by (etac otway.induct 1); |
35 by Auto_tac; |
35 by Auto_tac; |
36 qed"Gets_imp_Says"; |
36 qed"Gets_imp_Says"; |
37 |
37 |
38 (*Must be proved separately for each protocol*) |
38 (*Must be proved separately for each protocol*) |
39 Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs"; |
39 Goal "[| Gets B X \\<in> set evs; evs \\<in> otway |] ==> X \\<in> knows Spy evs"; |
40 by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); |
40 by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); |
41 qed"Gets_imp_knows_Spy"; |
41 qed"Gets_imp_knows_Spy"; |
42 AddSDs [Gets_imp_knows_Spy RS parts.Inj]; |
42 AddSDs [Gets_imp_knows_Spy RS parts.Inj]; |
43 |
43 |
44 |
44 |
45 (**** Inductive proofs about otway ****) |
45 (**** Inductive proofs about otway ****) |
46 |
46 |
47 (** For reasoning about the encrypted portion of messages **) |
47 (** For reasoning about the encrypted portion of messages **) |
48 |
48 |
49 Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs; evs : otway |] \ |
49 Goal "[| Gets B {|N, Agent A, Agent B, X|} \\<in> set evs; evs \\<in> otway |] \ |
50 \ ==> X : analz (knows Spy evs)"; |
50 \ ==> X \\<in> analz (knows Spy evs)"; |
51 by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); |
51 by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); |
52 qed "OR2_analz_knows_Spy"; |
52 qed "OR2_analz_knows_Spy"; |
53 |
53 |
54 Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs; evs : otway |] \ |
54 Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} \\<in> set evs; evs \\<in> otway |] \ |
55 \ ==> X : analz (knows Spy evs)"; |
55 \ ==> X \\<in> analz (knows Spy evs)"; |
56 by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); |
56 by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); |
57 qed "OR4_analz_knows_Spy"; |
57 qed "OR4_analz_knows_Spy"; |
58 |
58 |
59 Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ |
59 Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \\<in> set evs \ |
60 \ ==> K : parts (knows Spy evs)"; |
60 \ ==> K \\<in> parts (knows Spy evs)"; |
61 by (Blast_tac 1); |
61 by (Blast_tac 1); |
62 qed "Oops_parts_knows_Spy"; |
62 qed "Oops_parts_knows_Spy"; |
63 |
63 |
64 bind_thm ("OR2_parts_knows_Spy", |
64 bind_thm ("OR2_parts_knows_Spy", |
65 OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts)); |
65 OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts)); |
117 |
117 |
118 |
118 |
119 (**** |
119 (**** |
120 The following is to prove theorems of the form |
120 The following is to prove theorems of the form |
121 |
121 |
122 Key K : analz (insert (Key KAB) (knows Spy evs)) ==> |
122 Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) ==> |
123 Key K : analz (knows Spy evs) |
123 Key K \\<in> analz (knows Spy evs) |
124 |
124 |
125 A more general formula must be proved inductively. |
125 A more general formula must be proved inductively. |
126 ****) |
126 ****) |
127 |
127 |
128 |
128 |
129 (** Session keys are not used to encrypt other session keys **) |
129 (** Session keys are not used to encrypt other session keys **) |
130 |
130 |
131 (*The equality makes the induction hypothesis easier to apply*) |
131 (*The equality makes the induction hypothesis easier to apply*) |
132 Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) --> \ |
132 Goal "evs \\<in> otway ==> ALL K KK. KK <= - (range shrK) --> \ |
133 \ (Key K : analz (Key`KK Un (knows Spy evs))) = \ |
133 \ (Key K \\<in> analz (Key`KK Un (knows Spy evs))) = \ |
134 \ (K : KK | Key K : analz (knows Spy evs))"; |
134 \ (K \\<in> KK | Key K \\<in> analz (knows Spy evs))"; |
135 by (etac otway.induct 1); |
135 by (etac otway.induct 1); |
136 by analz_knows_Spy_tac; |
136 by analz_knows_Spy_tac; |
137 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
137 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
138 by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); |
138 by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); |
139 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
139 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
140 (*Fake*) |
140 (*Fake*) |
141 by (spy_analz_tac 1); |
141 by (spy_analz_tac 1); |
142 qed_spec_mp "analz_image_freshK"; |
142 qed_spec_mp "analz_image_freshK"; |
143 |
143 |
144 |
144 |
145 Goal "[| evs : otway; KAB \\<notin> range shrK |] \ |
145 Goal "[| evs \\<in> otway; KAB \\<notin> range shrK |] \ |
146 \ ==> Key K : analz (insert (Key KAB) (knows Spy evs)) = \ |
146 \ ==> Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) = \ |
147 \ (K = KAB | Key K : analz (knows Spy evs))"; |
147 \ (K = KAB | Key K \\<in> analz (knows Spy evs))"; |
148 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
148 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
149 qed "analz_insert_freshK"; |
149 qed "analz_insert_freshK"; |
150 |
150 |
151 |
151 |
152 (*** The Key K uniquely identifies the Server's message. **) |
152 (*** The Key K uniquely identifies the Server's message. **) |
153 |
153 |
154 Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \ |
154 Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \\<in> set evs; \ |
155 \ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \ |
155 \ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \\<in> set evs; \ |
156 \ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"; |
156 \ evs \\<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"; |
157 by (etac rev_mp 1); |
157 by (etac rev_mp 1); |
158 by (etac rev_mp 1); |
158 by (etac rev_mp 1); |
159 by (etac otway.induct 1); |
159 by (etac otway.induct 1); |
160 by (ALLGOALS Asm_simp_tac); |
160 by (ALLGOALS Asm_simp_tac); |
161 (*Remaining cases: OR3 and OR4*) |
161 (*Remaining cases: OR3 and OR4*) |
164 |
164 |
165 |
165 |
166 (**** Authenticity properties relating to NA ****) |
166 (**** Authenticity properties relating to NA ****) |
167 |
167 |
168 (*Only OR1 can have caused such a part of a message to appear.*) |
168 (*Only OR1 can have caused such a part of a message to appear.*) |
169 Goal "[| A \\<notin> bad; evs : otway |] \ |
169 Goal "[| A \\<notin> bad; evs \\<in> otway |] \ |
170 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \ |
170 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \ |
171 \ Says A B {|NA, Agent A, Agent B, \ |
171 \ Says A B {|NA, Agent A, Agent B, \ |
172 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
172 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
173 \ : set evs"; |
173 \ \\<in> set evs"; |
174 by (parts_induct_tac 1); |
174 by (parts_induct_tac 1); |
175 by (Blast_tac 1); |
175 by (Blast_tac 1); |
176 qed_spec_mp "Crypt_imp_OR1"; |
176 qed_spec_mp "Crypt_imp_OR1"; |
177 |
177 |
178 Goal "[| Gets B {|NA, Agent A, Agent B, \ |
178 Goal "[| Gets B {|NA, Agent A, Agent B, \ |
179 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
179 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \ |
180 \ A \\<notin> bad; evs : otway |] \ |
180 \ A \\<notin> bad; evs \\<in> otway |] \ |
181 \ ==> Says A B {|NA, Agent A, Agent B, \ |
181 \ ==> Says A B {|NA, Agent A, Agent B, \ |
182 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
182 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
183 \ : set evs"; |
183 \ \\<in> set evs"; |
184 by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1); |
184 by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1); |
185 qed"Crypt_imp_OR1_Gets"; |
185 qed"Crypt_imp_OR1_Gets"; |
186 |
186 |
187 |
187 |
188 (** The Nonce NA uniquely identifies A's message. **) |
188 (** The Nonce NA uniquely identifies A's message. **) |
189 |
189 |
190 Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (knows Spy evs); \ |
190 Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (knows Spy evs); \ |
191 \ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (knows Spy evs); \ |
191 \ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (knows Spy evs); \ |
192 \ evs : otway; A \\<notin> bad |] \ |
192 \ evs \\<in> otway; A \\<notin> bad |] \ |
193 \ ==> B = C"; |
193 \ ==> B = C"; |
194 by (etac rev_mp 1); |
194 by (etac rev_mp 1); |
195 by (etac rev_mp 1); |
195 by (etac rev_mp 1); |
196 by (parts_induct_tac 1); |
196 by (parts_induct_tac 1); |
197 (*Fake, OR1*) |
197 (*Fake, OR1*) |
200 |
200 |
201 |
201 |
202 (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
202 (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
203 OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
203 OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
204 over-simplified version of this protocol: see OtwayRees_Bad.*) |
204 over-simplified version of this protocol: see OtwayRees_Bad.*) |
205 Goal "[| A \\<notin> bad; evs : otway |] \ |
205 Goal "[| A \\<notin> bad; evs \\<in> otway |] \ |
206 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \ |
206 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \ |
207 \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ |
207 \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ |
208 \ \\<notin> parts (knows Spy evs)"; |
208 \ \\<notin> parts (knows Spy evs)"; |
209 by (parts_induct_tac 1); |
209 by (parts_induct_tac 1); |
210 by Auto_tac; |
210 by Auto_tac; |
211 qed_spec_mp "no_nonce_OR1_OR2"; |
211 qed_spec_mp "no_nonce_OR1_OR2"; |
212 |
212 |
213 val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); |
213 val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); |
214 |
214 |
215 (*Crucial property: If the encrypted message appears, and A has used NA |
215 (*Crucial property: If the encrypted message appears, and A has used NA |
216 to start a run, then it originated with the Server!*) |
216 to start a run, then it originated with the Server!*) |
217 Goal "[| A \\<notin> bad; evs : otway |] \ |
217 Goal "[| A \\<notin> bad; evs \\<in> otway |] \ |
218 \ ==> Says A B {|NA, Agent A, Agent B, \ |
218 \ ==> Says A B {|NA, Agent A, Agent B, \ |
219 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs --> \ |
219 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs --> \ |
220 \ Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \ |
220 \ Crypt (shrK A) {|NA, Key K|} \\<in> parts (knows Spy evs) \ |
221 \ --> (\\<exists>NB. Says Server B \ |
221 \ --> (\\<exists>NB. Says Server B \ |
222 \ {|NA, \ |
222 \ {|NA, \ |
223 \ Crypt (shrK A) {|NA, Key K|}, \ |
223 \ Crypt (shrK A) {|NA, Key K|}, \ |
224 \ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; |
224 \ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs)"; |
225 by (parts_induct_tac 1); |
225 by (parts_induct_tac 1); |
226 by (Blast_tac 1); |
226 by (Blast_tac 1); |
227 (*OR1: it cannot be a new Nonce, contradiction.*) |
227 (*OR1: it cannot be a new Nonce, contradiction.*) |
228 by (Blast_tac 1); |
228 by (Blast_tac 1); |
229 (*OR4*) |
229 (*OR4*) |
236 (*Corollary: if A receives B's OR4 message and the nonce NA agrees |
236 (*Corollary: if A receives B's OR4 message and the nonce NA agrees |
237 then the key really did come from the Server! CANNOT prove this of the |
237 then the key really did come from the Server! CANNOT prove this of the |
238 bad form of this protocol, even though we can prove |
238 bad form of this protocol, even though we can prove |
239 Spy_not_see_encrypted_key*) |
239 Spy_not_see_encrypted_key*) |
240 Goal "[| Says A B {|NA, Agent A, Agent B, \ |
240 Goal "[| Says A B {|NA, Agent A, Agent B, \ |
241 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
241 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \ |
242 \ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
242 \ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \ |
243 \ A \\<notin> bad; evs : otway |] \ |
243 \ A \\<notin> bad; evs \\<in> otway |] \ |
244 \ ==> \\<exists>NB. Says Server B \ |
244 \ ==> \\<exists>NB. Says Server B \ |
245 \ {|NA, \ |
245 \ {|NA, \ |
246 \ Crypt (shrK A) {|NA, Key K|}, \ |
246 \ Crypt (shrK A) {|NA, Key K|}, \ |
247 \ Crypt (shrK B) {|NB, Key K|}|} \ |
247 \ Crypt (shrK B) {|NB, Key K|}|} \ |
248 \ : set evs"; |
248 \ \\<in> set evs"; |
249 by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); |
249 by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); |
250 qed "A_trusts_OR4"; |
250 qed "A_trusts_OR4"; |
251 |
251 |
252 |
252 |
253 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
253 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
254 Does not in itself guarantee security: an attack could violate |
254 Does not in itself guarantee security: an attack could violate |
255 the premises, e.g. by having A=Spy **) |
255 the premises, e.g. by having A=Spy **) |
256 |
256 |
257 Goal "[| A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
257 Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \ |
258 \ ==> Says Server B \ |
258 \ ==> Says Server B \ |
259 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
259 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
260 \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ |
260 \ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs --> \ |
261 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs --> \ |
261 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs --> \ |
262 \ Key K \\<notin> analz (knows Spy evs)"; |
262 \ Key K \\<notin> analz (knows Spy evs)"; |
263 by (etac otway.induct 1); |
263 by (etac otway.induct 1); |
264 by analz_knows_Spy_tac; |
264 by analz_knows_Spy_tac; |
265 by (ALLGOALS |
265 by (ALLGOALS |
276 by (spy_analz_tac 1); |
276 by (spy_analz_tac 1); |
277 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
277 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
278 |
278 |
279 Goal "[| Says Server B \ |
279 Goal "[| Says Server B \ |
280 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
280 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
281 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
281 \ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \ |
282 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \ |
282 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \ |
283 \ A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
283 \ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \ |
284 \ ==> Key K \\<notin> analz (knows Spy evs)"; |
284 \ ==> Key K \\<notin> analz (knows Spy evs)"; |
285 by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1); |
285 by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1); |
286 qed "Spy_not_see_encrypted_key"; |
286 qed "Spy_not_see_encrypted_key"; |
287 |
287 |
288 |
288 |
289 (*A's guarantee. The Oops premise quantifies over NB because A cannot know |
289 (*A's guarantee. The Oops premise quantifies over NB because A cannot know |
290 what it is.*) |
290 what it is.*) |
291 Goal "[| Says A B {|NA, Agent A, Agent B, \ |
291 Goal "[| Says A B {|NA, Agent A, Agent B, \ |
292 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
292 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \ |
293 \ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
293 \ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \ |
294 \ ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \ |
294 \ ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \ |
295 \ A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
295 \ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \ |
296 \ ==> Key K \\<notin> analz (knows Spy evs)"; |
296 \ ==> Key K \\<notin> analz (knows Spy evs)"; |
297 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); |
297 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); |
298 qed "A_gets_good_key"; |
298 qed "A_gets_good_key"; |
299 |
299 |
300 |
300 |
301 (**** Authenticity properties relating to NB ****) |
301 (**** Authenticity properties relating to NB ****) |
302 |
302 |
303 (*Only OR2 can have caused such a part of a message to appear. We do not |
303 (*Only OR2 can have caused such a part of a message to appear. We do not |
304 know anything about X: it does NOT have to have the right form.*) |
304 know anything about X: it does NOT have to have the right form.*) |
305 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
305 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
306 \ : parts (knows Spy evs); \ |
306 \ \\<in> parts (knows Spy evs); \ |
307 \ B \\<notin> bad; evs : otway |] \ |
307 \ B \\<notin> bad; evs \\<in> otway |] \ |
308 \ ==> \\<exists>X. Says B Server \ |
308 \ ==> \\<exists>X. Says B Server \ |
309 \ {|NA, Agent A, Agent B, X, \ |
309 \ {|NA, Agent A, Agent B, X, \ |
310 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
310 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
311 \ : set evs"; |
311 \ \\<in> set evs"; |
312 by (etac rev_mp 1); |
312 by (etac rev_mp 1); |
313 by (parts_induct_tac 1); |
313 by (parts_induct_tac 1); |
314 by (ALLGOALS Blast_tac); |
314 by (ALLGOALS Blast_tac); |
315 qed "Crypt_imp_OR2"; |
315 qed "Crypt_imp_OR2"; |
316 |
316 |
317 |
317 |
318 (** The Nonce NB uniquely identifies B's message. **) |
318 (** The Nonce NB uniquely identifies B's message. **) |
319 |
319 |
320 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs); \ |
320 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \\<in> parts(knows Spy evs); \ |
321 \ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(knows Spy evs); \ |
321 \ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \\<in> parts(knows Spy evs); \ |
322 \ evs : otway; B \\<notin> bad |] \ |
322 \ evs \\<in> otway; B \\<notin> bad |] \ |
323 \ ==> NC = NA & C = A"; |
323 \ ==> NC = NA & C = A"; |
324 by (etac rev_mp 1); |
324 by (etac rev_mp 1); |
325 by (etac rev_mp 1); |
325 by (etac rev_mp 1); |
326 by (parts_induct_tac 1); |
326 by (parts_induct_tac 1); |
327 (*Fake, OR2*) |
327 (*Fake, OR2*) |
328 by (REPEAT (Blast_tac 1)); |
328 by (REPEAT (Blast_tac 1)); |
329 qed "unique_NB"; |
329 qed "unique_NB"; |
330 |
330 |
331 (*If the encrypted message appears, and B has used Nonce NB, |
331 (*If the encrypted message appears, and B has used Nonce NB, |
332 then it originated with the Server! Quite messy proof.*) |
332 then it originated with the Server! Quite messy proof.*) |
333 Goal "[| B \\<notin> bad; evs : otway |] \ |
333 Goal "[| B \\<notin> bad; evs \\<in> otway |] \ |
334 \ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs) \ |
334 \ ==> Crypt (shrK B) {|NB, Key K|} \\<in> parts (knows Spy evs) \ |
335 \ --> (ALL X'. Says B Server \ |
335 \ --> (ALL X'. Says B Server \ |
336 \ {|NA, Agent A, Agent B, X', \ |
336 \ {|NA, Agent A, Agent B, X', \ |
337 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
337 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
338 \ : set evs \ |
338 \ \\<in> set evs \ |
339 \ --> Says Server B \ |
339 \ --> Says Server B \ |
340 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
340 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
341 \ Crypt (shrK B) {|NB, Key K|}|} \ |
341 \ Crypt (shrK B) {|NB, Key K|}|} \ |
342 \ : set evs)"; |
342 \ \\<in> set evs)"; |
343 by (asm_full_simp_tac (simpset() addsimps []) 1); |
343 by (asm_full_simp_tac (simpset() addsimps []) 1); |
344 by (parts_induct_tac 1); |
344 by (parts_induct_tac 1); |
345 by (Blast_tac 1); |
345 by (Blast_tac 1); |
346 (*OR1: it cannot be a new Nonce, contradiction.*) |
346 (*OR1: it cannot be a new Nonce, contradiction.*) |
347 by (Blast_tac 1); |
347 by (Blast_tac 1); |
355 |
355 |
356 (*Guarantee for B: if it gets a message with matching NB then the Server |
356 (*Guarantee for B: if it gets a message with matching NB then the Server |
357 has sent the correct message.*) |
357 has sent the correct message.*) |
358 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ |
358 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ |
359 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
359 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
360 \ : set evs; \ |
360 \ \\<in> set evs; \ |
361 \ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
361 \ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \ |
362 \ B \\<notin> bad; evs : otway |] \ |
362 \ B \\<notin> bad; evs \\<in> otway |] \ |
363 \ ==> Says Server B \ |
363 \ ==> Says Server B \ |
364 \ {|NA, \ |
364 \ {|NA, \ |
365 \ Crypt (shrK A) {|NA, Key K|}, \ |
365 \ Crypt (shrK A) {|NA, Key K|}, \ |
366 \ Crypt (shrK B) {|NB, Key K|}|} \ |
366 \ Crypt (shrK B) {|NB, Key K|}|} \ |
367 \ : set evs"; |
367 \ \\<in> set evs"; |
368 by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); |
368 by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); |
369 qed "B_trusts_OR3"; |
369 qed "B_trusts_OR3"; |
370 |
370 |
371 |
371 |
372 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) |
372 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) |
373 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ |
373 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ |
374 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
374 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
375 \ : set evs; \ |
375 \ \\<in> set evs; \ |
376 \ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
376 \ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \ |
377 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \ |
377 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \ |
378 \ A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
378 \ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \ |
379 \ ==> Key K \\<notin> analz (knows Spy evs)"; |
379 \ ==> Key K \\<notin> analz (knows Spy evs)"; |
380 by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); |
380 by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); |
381 qed "B_gets_good_key"; |
381 qed "B_gets_good_key"; |
382 |
382 |
383 |
383 |
384 Goal "[| Says Server B \ |
384 Goal "[| Says Server B \ |
385 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
385 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
386 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
386 \ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \ |
387 \ B \\<notin> bad; evs : otway |] \ |
387 \ B \\<notin> bad; evs \\<in> otway |] \ |
388 \ ==> \\<exists>X. Says B Server {|NA, Agent A, Agent B, X, \ |
388 \ ==> \\<exists>X. Says B Server {|NA, Agent A, Agent B, X, \ |
389 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
389 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
390 \ : set evs"; |
390 \ \\<in> set evs"; |
391 by (etac rev_mp 1); |
391 by (etac rev_mp 1); |
392 by (etac otway.induct 1); |
392 by (etac otway.induct 1); |
393 by (ALLGOALS Asm_simp_tac); |
393 by (ALLGOALS Asm_simp_tac); |
394 by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 3); |
394 by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 3); |
395 by (ALLGOALS Blast_tac); |
395 by (ALLGOALS Blast_tac); |
397 |
397 |
398 |
398 |
399 (*After getting and checking OR4, agent A can trust that B has been active. |
399 (*After getting and checking OR4, agent A can trust that B has been active. |
400 We could probably prove that X has the expected form, but that is not |
400 We could probably prove that X has the expected form, but that is not |
401 strictly necessary for authentication.*) |
401 strictly necessary for authentication.*) |
402 Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
402 Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \ |
403 \ Says A B {|NA, Agent A, Agent B, \ |
403 \ Says A B {|NA, Agent A, Agent B, \ |
404 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
404 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \ |
405 \ A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
405 \ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \ |
406 \ ==> \\<exists>NB X. Says B Server {|NA, Agent A, Agent B, X, \ |
406 \ ==> \\<exists>NB X. Says B Server {|NA, Agent A, Agent B, X, \ |
407 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ |
407 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ |
408 \ : set evs"; |
408 \ \\<in> set evs"; |
409 by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj] |
409 by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj] |
410 addSDs [A_trusts_OR4, OR3_imp_OR2]) 1); |
410 addSDs [A_trusts_OR4, OR3_imp_OR2]) 1); |
411 qed "A_auths_B"; |
411 qed "A_auths_B"; |