21 AddDs [impOfSubs analz_subset_parts]; |
21 AddDs [impOfSubs analz_subset_parts]; |
22 AddDs [impOfSubs Fake_parts_insert]; |
22 AddDs [impOfSubs Fake_parts_insert]; |
23 |
23 |
24 |
24 |
25 (*A "possibility property": there are traces that reach the end*) |
25 (*A "possibility property": there are traces that reach the end*) |
26 goal thy |
26 Goal |
27 "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ |
27 "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ |
28 \ ==> EX X NB K. EX evs: yahalom. \ |
28 \ ==> EX X NB K. EX evs: yahalom. \ |
29 \ Says A B {|X, Crypt K (Nonce NB)|} : set evs"; |
29 \ Says A B {|X, Crypt K (Nonce NB)|} : set evs"; |
30 by (REPEAT (resolve_tac [exI,bexI] 1)); |
30 by (REPEAT (resolve_tac [exI,bexI] 1)); |
31 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS |
31 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS |
35 |
35 |
36 |
36 |
37 (**** Inductive proofs about yahalom ****) |
37 (**** Inductive proofs about yahalom ****) |
38 |
38 |
39 (*Nobody sends themselves messages*) |
39 (*Nobody sends themselves messages*) |
40 goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs"; |
40 Goal "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs"; |
41 by (etac yahalom.induct 1); |
41 by (etac yahalom.induct 1); |
42 by Auto_tac; |
42 by Auto_tac; |
43 qed_spec_mp "not_Says_to_self"; |
43 qed_spec_mp "not_Says_to_self"; |
44 Addsimps [not_Says_to_self]; |
44 Addsimps [not_Says_to_self]; |
45 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
45 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
46 |
46 |
47 |
47 |
48 (** For reasoning about the encrypted portion of messages **) |
48 (** For reasoning about the encrypted portion of messages **) |
49 |
49 |
50 (*Lets us treat YM4 using a similar argument as for the Fake case.*) |
50 (*Lets us treat YM4 using a similar argument as for the Fake case.*) |
51 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \ |
51 Goal "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \ |
52 \ X : analz (spies evs)"; |
52 \ X : analz (spies evs)"; |
53 by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); |
53 by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); |
54 qed "YM4_analz_spies"; |
54 qed "YM4_analz_spies"; |
55 |
55 |
56 bind_thm ("YM4_parts_spies", |
56 bind_thm ("YM4_parts_spies", |
57 YM4_analz_spies RS (impOfSubs analz_subset_parts)); |
57 YM4_analz_spies RS (impOfSubs analz_subset_parts)); |
58 |
58 |
59 (*Relates to both YM4 and Oops*) |
59 (*Relates to both YM4 and Oops*) |
60 goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \ |
60 Goal "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \ |
61 \ K : parts (spies evs)"; |
61 \ K : parts (spies evs)"; |
62 by (Blast_tac 1); |
62 by (Blast_tac 1); |
63 qed "YM4_Key_parts_spies"; |
63 qed "YM4_Key_parts_spies"; |
64 |
64 |
65 (*For proving the easier theorems about X ~: parts (spies evs).*) |
65 (*For proving the easier theorems about X ~: parts (spies evs).*) |
80 |
80 |
81 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
81 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
82 sends messages containing X! **) |
82 sends messages containing X! **) |
83 |
83 |
84 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
84 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
85 goal thy |
85 Goal |
86 "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
86 "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
87 by (parts_induct_tac 1); |
87 by (parts_induct_tac 1); |
88 by (ALLGOALS Blast_tac); |
88 by (ALLGOALS Blast_tac); |
89 qed "Spy_see_shrK"; |
89 qed "Spy_see_shrK"; |
90 Addsimps [Spy_see_shrK]; |
90 Addsimps [Spy_see_shrK]; |
91 |
91 |
92 goal thy |
92 Goal |
93 "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
93 "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
94 by Auto_tac; |
94 by Auto_tac; |
95 qed "Spy_analz_shrK"; |
95 qed "Spy_analz_shrK"; |
96 Addsimps [Spy_analz_shrK]; |
96 Addsimps [Spy_analz_shrK]; |
97 |
97 |
98 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), |
98 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), |
99 Spy_analz_shrK RSN (2, rev_iffD1)]; |
99 Spy_analz_shrK RSN (2, rev_iffD1)]; |
100 |
100 |
101 |
101 |
102 (*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) |
102 (*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*) |
103 goal thy "!!evs. evs : yahalom ==> \ |
103 Goal "!!evs. evs : yahalom ==> \ |
104 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
104 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
105 by (parts_induct_tac 1); |
105 by (parts_induct_tac 1); |
106 (*YM4: Key K is not fresh!*) |
106 (*YM4: Key K is not fresh!*) |
107 by (Blast_tac 3); |
107 by (Blast_tac 3); |
108 (*YM3*) |
108 (*YM3*) |
117 |
117 |
118 Addsimps [new_keys_not_used, new_keys_not_analzd]; |
118 Addsimps [new_keys_not_used, new_keys_not_analzd]; |
119 |
119 |
120 (*Describes the form of K when the Server sends this message. Useful for |
120 (*Describes the form of K when the Server sends this message. Useful for |
121 Oops as well as main secrecy property.*) |
121 Oops as well as main secrecy property.*) |
122 goal thy |
122 Goal |
123 "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ |
123 "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ |
124 \ : set evs; \ |
124 \ : set evs; \ |
125 \ evs : yahalom |] \ |
125 \ evs : yahalom |] \ |
126 \ ==> K ~: range shrK & A ~= B"; |
126 \ ==> K ~: range shrK & A ~= B"; |
127 by (etac rev_mp 1); |
127 by (etac rev_mp 1); |
148 |
148 |
149 ****) |
149 ****) |
150 |
150 |
151 (** Session keys are not used to encrypt other session keys **) |
151 (** Session keys are not used to encrypt other session keys **) |
152 |
152 |
153 goal thy |
153 Goal |
154 "!!evs. evs : yahalom ==> \ |
154 "!!evs. evs : yahalom ==> \ |
155 \ ALL K KK. KK <= Compl (range shrK) --> \ |
155 \ ALL K KK. KK <= Compl (range shrK) --> \ |
156 \ (Key K : analz (Key``KK Un (spies evs))) = \ |
156 \ (Key K : analz (Key``KK Un (spies evs))) = \ |
157 \ (K : KK | Key K : analz (spies evs))"; |
157 \ (K : KK | Key K : analz (spies evs))"; |
158 by (etac yahalom.induct 1); |
158 by (etac yahalom.induct 1); |
162 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
162 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
163 (*Fake*) |
163 (*Fake*) |
164 by (spy_analz_tac 1); |
164 by (spy_analz_tac 1); |
165 qed_spec_mp "analz_image_freshK"; |
165 qed_spec_mp "analz_image_freshK"; |
166 |
166 |
167 goal thy |
167 Goal |
168 "!!evs. [| evs : yahalom; KAB ~: range shrK |] ==> \ |
168 "!!evs. [| evs : yahalom; KAB ~: range shrK |] ==> \ |
169 \ Key K : analz (insert (Key KAB) (spies evs)) = \ |
169 \ Key K : analz (insert (Key KAB) (spies evs)) = \ |
170 \ (K = KAB | Key K : analz (spies evs))"; |
170 \ (K = KAB | Key K : analz (spies evs))"; |
171 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
171 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
172 qed "analz_insert_freshK"; |
172 qed "analz_insert_freshK"; |
173 |
173 |
174 |
174 |
175 (*** The Key K uniquely identifies the Server's message. **) |
175 (*** The Key K uniquely identifies the Server's message. **) |
176 |
176 |
177 goal thy |
177 Goal |
178 "!!evs. evs : yahalom ==> \ |
178 "!!evs. evs : yahalom ==> \ |
179 \ EX A' B' na' nb' X'. ALL A B na nb X. \ |
179 \ EX A' B' na' nb' X'. ALL A B na nb X. \ |
180 \ Says Server A \ |
180 \ Says Server A \ |
181 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ |
181 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ |
182 \ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'"; |
182 \ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'"; |
189 (*...we assume X is a recent message and handle this case by contradiction*) |
189 (*...we assume X is a recent message and handle this case by contradiction*) |
190 by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*) |
190 by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*) |
191 addss (simpset() addsimps [parts_insertI])) 1); |
191 addss (simpset() addsimps [parts_insertI])) 1); |
192 val lemma = result(); |
192 val lemma = result(); |
193 |
193 |
194 goal thy |
194 Goal |
195 "!!evs. [| Says Server A \ |
195 "!!evs. [| Says Server A \ |
196 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \ |
196 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \ |
197 \ Says Server A' \ |
197 \ Says Server A' \ |
198 \ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \ |
198 \ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \ |
199 \ evs : yahalom |] \ |
199 \ evs : yahalom |] \ |
202 qed "unique_session_keys"; |
202 qed "unique_session_keys"; |
203 |
203 |
204 |
204 |
205 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) |
205 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) |
206 |
206 |
207 goal thy |
207 Goal |
208 "!!evs. [| A ~: bad; B ~: bad; A ~= B; \ |
208 "!!evs. [| A ~: bad; B ~: bad; A ~= B; \ |
209 \ evs : yahalom |] \ |
209 \ evs : yahalom |] \ |
210 \ ==> Says Server A \ |
210 \ ==> Says Server A \ |
211 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ |
211 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ |
212 \ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ |
212 \ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ |
227 by (spy_analz_tac 1); |
227 by (spy_analz_tac 1); |
228 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
228 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
229 |
229 |
230 |
230 |
231 (*Final version*) |
231 (*Final version*) |
232 goal thy |
232 Goal |
233 "!!evs. [| Says Server A \ |
233 "!!evs. [| Says Server A \ |
234 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ |
234 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ |
235 \ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ |
235 \ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ |
236 \ : set evs; \ |
236 \ : set evs; \ |
237 \ Notes Spy {|na, nb, Key K|} ~: set evs; \ |
237 \ Notes Spy {|na, nb, Key K|} ~: set evs; \ |
244 |
244 |
245 (** Security Guarantee for A upon receiving YM3 **) |
245 (** Security Guarantee for A upon receiving YM3 **) |
246 |
246 |
247 (*If the encrypted message appears then it originated with the Server. |
247 (*If the encrypted message appears then it originated with the Server. |
248 May now apply Spy_not_see_encrypted_key, subject to its conditions.*) |
248 May now apply Spy_not_see_encrypted_key, subject to its conditions.*) |
249 goal thy |
249 Goal |
250 "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} \ |
250 "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} \ |
251 \ : parts (spies evs); \ |
251 \ : parts (spies evs); \ |
252 \ A ~: bad; evs : yahalom |] \ |
252 \ A ~: bad; evs : yahalom |] \ |
253 \ ==> EX nb. Says Server A \ |
253 \ ==> EX nb. Says Server A \ |
254 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ |
254 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ |
258 by (parts_induct_tac 1); |
258 by (parts_induct_tac 1); |
259 by (ALLGOALS Blast_tac); |
259 by (ALLGOALS Blast_tac); |
260 qed "A_trusts_YM3"; |
260 qed "A_trusts_YM3"; |
261 |
261 |
262 (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) |
262 (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) |
263 goal thy |
263 Goal |
264 "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} : parts (spies evs); \ |
264 "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} : parts (spies evs); \ |
265 \ ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs; \ |
265 \ ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs; \ |
266 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
266 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
267 \ ==> Key K ~: analz (spies evs)"; |
267 \ ==> Key K ~: analz (spies evs)"; |
268 by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1); |
268 by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1); |
271 |
271 |
272 (** Security Guarantee for B upon receiving YM4 **) |
272 (** Security Guarantee for B upon receiving YM4 **) |
273 |
273 |
274 (*B knows, by the first part of A's message, that the Server distributed |
274 (*B knows, by the first part of A's message, that the Server distributed |
275 the key for A and B, and has associated it with NB.*) |
275 the key for A and B, and has associated it with NB.*) |
276 goal thy |
276 Goal |
277 "!!evs. [| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ |
277 "!!evs. [| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ |
278 \ : parts (spies evs); \ |
278 \ : parts (spies evs); \ |
279 \ B ~: bad; evs : yahalom |] \ |
279 \ B ~: bad; evs : yahalom |] \ |
280 \ ==> EX NA. Says Server A \ |
280 \ ==> EX NA. Says Server A \ |
281 \ {|Nonce NB, \ |
281 \ {|Nonce NB, \ |
291 (*With this protocol variant, we don't need the 2nd part of YM4 at all: |
291 (*With this protocol variant, we don't need the 2nd part of YM4 at all: |
292 Nonce NB is available in the first part.*) |
292 Nonce NB is available in the first part.*) |
293 |
293 |
294 (*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom |
294 (*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom |
295 because we do not have to show that NB is secret. *) |
295 because we do not have to show that NB is secret. *) |
296 goal thy |
296 Goal |
297 "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ |
297 "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ |
298 \ X|} \ |
298 \ X|} \ |
299 \ : set evs; \ |
299 \ : set evs; \ |
300 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
300 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
301 \ ==> EX NA. Says Server A \ |
301 \ ==> EX NA. Says Server A \ |
306 by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1); |
306 by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1); |
307 qed "B_trusts_YM4"; |
307 qed "B_trusts_YM4"; |
308 |
308 |
309 |
309 |
310 (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) |
310 (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) |
311 goal thy |
311 Goal |
312 "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ |
312 "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ |
313 \ X|} \ |
313 \ X|} \ |
314 \ : set evs; \ |
314 \ : set evs; \ |
315 \ ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs; \ |
315 \ ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs; \ |
316 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
316 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
321 |
321 |
322 |
322 |
323 (*** Authenticating B to A ***) |
323 (*** Authenticating B to A ***) |
324 |
324 |
325 (*The encryption in message YM2 tells us it cannot be faked.*) |
325 (*The encryption in message YM2 tells us it cannot be faked.*) |
326 goal thy |
326 Goal |
327 "!!evs. [| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs); \ |
327 "!!evs. [| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs); \ |
328 \ B ~: bad; evs : yahalom \ |
328 \ B ~: bad; evs : yahalom \ |
329 \ |] ==> EX NB. Says B Server {|Agent B, Nonce NB, \ |
329 \ |] ==> EX NB. Says B Server {|Agent B, Nonce NB, \ |
330 \ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ |
330 \ Crypt (shrK B) {|Agent A, Nonce NA|}|} \ |
331 \ : set evs"; |
331 \ : set evs"; |
335 by (ALLGOALS Blast_tac); |
335 by (ALLGOALS Blast_tac); |
336 qed "B_Said_YM2"; |
336 qed "B_Said_YM2"; |
337 |
337 |
338 |
338 |
339 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*) |
339 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*) |
340 goal thy |
340 Goal |
341 "!!evs. [| Says Server A \ |
341 "!!evs. [| Says Server A \ |
342 \ {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ |
342 \ {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ |
343 \ : set evs; \ |
343 \ : set evs; \ |
344 \ B ~: bad; evs : yahalom \ |
344 \ B ~: bad; evs : yahalom \ |
345 \ |] ==> EX nb'. Says B Server {|Agent B, nb', \ |
345 \ |] ==> EX nb'. Says B Server {|Agent B, nb', \ |
354 (*Fake, YM2*) |
354 (*Fake, YM2*) |
355 by (ALLGOALS Blast_tac); |
355 by (ALLGOALS Blast_tac); |
356 val lemma = result(); |
356 val lemma = result(); |
357 |
357 |
358 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*) |
358 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*) |
359 goal thy |
359 Goal |
360 "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ |
360 "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ |
361 \ : set evs; \ |
361 \ : set evs; \ |
362 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
362 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
363 \ ==> EX nb'. Says B Server \ |
363 \ ==> EX nb'. Says B Server \ |
364 \ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \ |
364 \ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \ |
371 |
371 |
372 (*Assuming the session key is secure, if both certificates are present then |
372 (*Assuming the session key is secure, if both certificates are present then |
373 A has said NB. We can't be sure about the rest of A's message, but only |
373 A has said NB. We can't be sure about the rest of A's message, but only |
374 NB matters for freshness. Note that Key K ~: analz (spies evs) must be |
374 NB matters for freshness. Note that Key K ~: analz (spies evs) must be |
375 the FIRST antecedent of the induction formula.*) |
375 the FIRST antecedent of the induction formula.*) |
376 goal thy |
376 Goal |
377 "!!evs. evs : yahalom \ |
377 "!!evs. evs : yahalom \ |
378 \ ==> Key K ~: analz (spies evs) --> \ |
378 \ ==> Key K ~: analz (spies evs) --> \ |
379 \ Crypt K (Nonce NB) : parts (spies evs) --> \ |
379 \ Crypt K (Nonce NB) : parts (spies evs) --> \ |
380 \ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ |
380 \ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \ |
381 \ : parts (spies evs) --> \ |
381 \ : parts (spies evs) --> \ |
396 |
396 |
397 |
397 |
398 (*If B receives YM4 then A has used nonce NB (and therefore is alive). |
398 (*If B receives YM4 then A has used nonce NB (and therefore is alive). |
399 Moreover, A associates K with NB (thus is talking about the same run). |
399 Moreover, A associates K with NB (thus is talking about the same run). |
400 Other premises guarantee secrecy of K.*) |
400 Other premises guarantee secrecy of K.*) |
401 goal thy |
401 Goal |
402 "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ |
402 "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \ |
403 \ Crypt K (Nonce NB)|} : set evs; \ |
403 \ Crypt K (Nonce NB)|} : set evs; \ |
404 \ (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \ |
404 \ (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \ |
405 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
405 \ A ~: bad; B ~: bad; evs : yahalom |] \ |
406 \ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs"; |
406 \ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs"; |