16 AddDs [impOfSubs analz_subset_parts]; |
16 AddDs [impOfSubs analz_subset_parts]; |
17 AddDs [impOfSubs Fake_parts_insert]; |
17 AddDs [impOfSubs Fake_parts_insert]; |
18 |
18 |
19 |
19 |
20 (*A "possibility property": there are traces that reach the end*) |
20 (*A "possibility property": there are traces that reach the end*) |
21 Goal "[| A ~= B; A ~= Server; B ~= Server |] \ |
21 Goal "EX X NB K. EX evs: yahalom. \ |
22 \ ==> EX X NB K. EX evs: yahalom. \ |
|
23 \ Says A B {|X, Crypt K (Nonce NB)|} : set evs"; |
22 \ Says A B {|X, Crypt K (Nonce NB)|} : set evs"; |
24 by (REPEAT (resolve_tac [exI,bexI] 1)); |
23 by (REPEAT (resolve_tac [exI,bexI] 1)); |
25 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS |
24 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS |
26 yahalom.YM4) 2); |
25 yahalom.YM4) 2); |
27 by possibility_tac; |
26 by possibility_tac; |
28 result(); |
27 result(); |
29 |
28 |
30 |
29 |
31 (**** Inductive proofs about yahalom ****) |
30 (**** Inductive proofs about yahalom ****) |
32 |
|
33 (*Nobody sends themselves messages*) |
|
34 Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs"; |
|
35 by (etac yahalom.induct 1); |
|
36 by Auto_tac; |
|
37 qed_spec_mp "not_Says_to_self"; |
|
38 Addsimps [not_Says_to_self]; |
|
39 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
40 |
|
41 |
31 |
42 (** For reasoning about the encrypted portion of messages **) |
32 (** For reasoning about the encrypted portion of messages **) |
43 |
33 |
44 (*Lets us treat YM4 using a similar argument as for the Fake case.*) |
34 (*Lets us treat YM4 using a similar argument as for the Fake case.*) |
45 Goal "Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \ |
35 Goal "Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \ |
112 (*Describes the form of K when the Server sends this message. Useful for |
102 (*Describes the form of K when the Server sends this message. Useful for |
113 Oops as well as main secrecy property.*) |
103 Oops as well as main secrecy property.*) |
114 Goal "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ |
104 Goal "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \ |
115 \ : set evs; \ |
105 \ : set evs; \ |
116 \ evs : yahalom |] \ |
106 \ evs : yahalom |] \ |
117 \ ==> K ~: range shrK & A ~= B"; |
107 \ ==> K ~: range shrK"; |
118 by (etac rev_mp 1); |
108 by (etac rev_mp 1); |
119 by (etac yahalom.induct 1); |
109 by (etac yahalom.induct 1); |
120 by (ALLGOALS Asm_simp_tac); |
110 by (ALLGOALS Asm_simp_tac); |
121 qed "Says_Server_message_form"; |
111 qed "Says_Server_message_form"; |
122 |
112 |
189 qed "unique_session_keys"; |
179 qed "unique_session_keys"; |
190 |
180 |
191 |
181 |
192 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) |
182 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) |
193 |
183 |
194 Goal "[| A ~: bad; B ~: bad; A ~= B; \ |
184 Goal "[| A ~: bad; B ~: bad; evs : yahalom |] \ |
195 \ evs : yahalom |] \ |
|
196 \ ==> Says Server A \ |
185 \ ==> Says Server A \ |
197 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ |
186 \ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \ |
198 \ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ |
187 \ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \ |
199 \ : set evs --> \ |
188 \ : set evs --> \ |
200 \ Notes Spy {|na, nb, Key K|} ~: set evs --> \ |
189 \ Notes Spy {|na, nb, Key K|} ~: set evs --> \ |