17 AddDs [impOfSubs Fake_parts_insert]; |
17 AddDs [impOfSubs Fake_parts_insert]; |
18 |
18 |
19 AddIffs [Spy_in_bad]; |
19 AddIffs [Spy_in_bad]; |
20 |
20 |
21 (*A "possibility property": there are traces that reach the end*) |
21 (*A "possibility property": there are traces that reach the end*) |
22 Goal |
22 Goal "A ~= B ==> EX NB. EX evs: ns_public. \ |
23 "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ |
23 \ Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
24 \ Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
|
25 by (REPEAT (resolve_tac [exI,bexI] 1)); |
24 by (REPEAT (resolve_tac [exI,bexI] 1)); |
26 by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); |
25 by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); |
27 by possibility_tac; |
26 by possibility_tac; |
28 result(); |
27 result(); |
29 |
28 |
30 |
29 |
31 (**** Inductive proofs about ns_public ****) |
30 (**** Inductive proofs about ns_public ****) |
32 |
31 |
33 (*Nobody sends themselves messages*) |
32 (*Nobody sends themselves messages*) |
34 Goal "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs"; |
33 Goal "evs : ns_public ==> ALL A X. Says A A X ~: set evs"; |
35 by (etac ns_public.induct 1); |
34 by (etac ns_public.induct 1); |
36 by Auto_tac; |
35 by Auto_tac; |
37 qed_spec_mp "not_Says_to_self"; |
36 qed_spec_mp "not_Says_to_self"; |
38 Addsimps [not_Says_to_self]; |
37 Addsimps [not_Says_to_self]; |
39 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
38 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
52 |
51 |
53 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
52 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
54 sends messages containing X! **) |
53 sends messages containing X! **) |
55 |
54 |
56 (*Spy never sees another agent's private key! (unless it's bad at start)*) |
55 (*Spy never sees another agent's private key! (unless it's bad at start)*) |
57 Goal |
56 Goal "evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; |
58 "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; |
|
59 by (parts_induct_tac 1); |
57 by (parts_induct_tac 1); |
60 by (Blast_tac 1); |
58 by (Blast_tac 1); |
61 qed "Spy_see_priK"; |
59 qed "Spy_see_priK"; |
62 Addsimps [Spy_see_priK]; |
60 Addsimps [Spy_see_priK]; |
63 |
61 |
64 Goal |
62 Goal "evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; |
65 "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; |
|
66 by Auto_tac; |
63 by Auto_tac; |
67 qed "Spy_analz_priK"; |
64 qed "Spy_analz_priK"; |
68 Addsimps [Spy_analz_priK]; |
65 Addsimps [Spy_analz_priK]; |
69 |
66 |
70 AddSDs [Spy_see_priK RSN (2, rev_iffD1), |
67 AddSDs [Spy_see_priK RSN (2, rev_iffD1), |
73 |
70 |
74 (**** Authenticity properties obtained from NS2 ****) |
71 (**** Authenticity properties obtained from NS2 ****) |
75 |
72 |
76 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
73 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
77 is secret. (Honest users generate fresh nonces.)*) |
74 is secret. (Honest users generate fresh nonces.)*) |
78 Goal |
75 Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
79 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
76 \ Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
80 \ Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
|
81 \ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)"; |
77 \ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)"; |
82 by (etac rev_mp 1); |
78 by (etac rev_mp 1); |
83 by (etac rev_mp 1); |
79 by (etac rev_mp 1); |
84 by (parts_induct_tac 1); |
80 by (parts_induct_tac 1); |
85 by (ALLGOALS Blast_tac); |
81 by (ALLGOALS Blast_tac); |
88 (*Adding it to the claset slows down proofs...*) |
84 (*Adding it to the claset slows down proofs...*) |
89 val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE); |
85 val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE); |
90 |
86 |
91 |
87 |
92 (*Unicity for NS1: nonce NA identifies agents A and B*) |
88 (*Unicity for NS1: nonce NA identifies agents A and B*) |
93 Goal |
89 Goal "[| Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
94 "!!evs. [| Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
|
95 \ ==> EX A' B'. ALL A B. \ |
90 \ ==> EX A' B'. ALL A B. \ |
96 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ |
91 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ |
97 \ A=A' & B=B'"; |
92 \ A=A' & B=B'"; |
98 by (etac rev_mp 1); |
93 by (etac rev_mp 1); |
99 by (parts_induct_tac 1); |
94 by (parts_induct_tac 1); |
100 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
95 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
101 (*NS1*) |
96 (*NS1*) |
102 by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2); |
97 by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2); |
103 (*Fake*) |
98 (*Fake*) |
104 by (Clarify_tac 1); |
99 by (Clarify_tac 1); |
105 by (Blast_tac 1); |
100 by (Blast_tac 1); |
106 val lemma = result(); |
101 val lemma = result(); |
107 |
102 |
108 Goal |
103 Goal "[| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ |
109 "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ |
104 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ |
110 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ |
105 \ Nonce NA ~: analz (spies evs); \ |
111 \ Nonce NA ~: analz (spies evs); \ |
106 \ evs : ns_public |] \ |
112 \ evs : ns_public |] \ |
107 \ ==> A=A' & B=B'"; |
113 \ ==> A=A' & B=B'"; |
|
114 by (prove_unique_tac lemma 1); |
108 by (prove_unique_tac lemma 1); |
115 qed "unique_NA"; |
109 qed "unique_NA"; |
116 |
110 |
117 |
111 |
118 (*Tactic for proving secrecy theorems*) |
112 (*Tactic for proving secrecy theorems*) |
120 etac ns_public.induct i THEN |
114 etac ns_public.induct i THEN |
121 ALLGOALS Asm_simp_tac; |
115 ALLGOALS Asm_simp_tac; |
122 |
116 |
123 |
117 |
124 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
118 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
125 Goal |
119 Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
126 "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
120 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
127 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
121 \ ==> Nonce NA ~: analz (spies evs)"; |
128 \ ==> Nonce NA ~: analz (spies evs)"; |
|
129 by (etac rev_mp 1); |
122 by (etac rev_mp 1); |
130 by (analz_induct_tac 1); |
123 by (analz_induct_tac 1); |
131 (*NS3*) |
124 (*NS3*) |
132 by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4); |
125 by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4); |
133 (*NS2*) |
126 (*NS2*) |
139 qed "Spy_not_see_NA"; |
132 qed "Spy_not_see_NA"; |
140 |
133 |
141 |
134 |
142 (*Authentication for A: if she receives message 2 and has used NA |
135 (*Authentication for A: if she receives message 2 and has used NA |
143 to start a run, then B has sent message 2.*) |
136 to start a run, then B has sent message 2.*) |
144 Goal |
137 Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
145 "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
138 \ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
146 \ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
139 \ : set evs; \ |
147 \ : set evs; \ |
140 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
148 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
141 \ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
149 \ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
142 \ : set evs"; |
150 \ : set evs"; |
|
151 by (etac rev_mp 1); |
143 by (etac rev_mp 1); |
152 (*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*) |
144 (*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*) |
153 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
145 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
154 by (etac ns_public.induct 1); |
146 by (etac ns_public.induct 1); |
155 by (ALLGOALS Asm_simp_tac); |
147 by (ALLGOALS Asm_simp_tac); |
159 by (blast_tac (claset() addDs [Spy_not_see_NA]) 1); |
151 by (blast_tac (claset() addDs [Spy_not_see_NA]) 1); |
160 qed "A_trusts_NS2"; |
152 qed "A_trusts_NS2"; |
161 |
153 |
162 |
154 |
163 (*If the encrypted message appears then it originated with Alice in NS1*) |
155 (*If the encrypted message appears then it originated with Alice in NS1*) |
164 Goal |
156 Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
165 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
157 \ Nonce NA ~: analz (spies evs); \ |
166 \ Nonce NA ~: analz (spies evs); \ |
158 \ evs : ns_public |] \ |
167 \ evs : ns_public |] \ |
159 \==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; |
168 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; |
|
169 by (etac rev_mp 1); |
160 by (etac rev_mp 1); |
170 by (etac rev_mp 1); |
161 by (etac rev_mp 1); |
171 by (parts_induct_tac 1); |
162 by (parts_induct_tac 1); |
172 by (Blast_tac 1); |
163 by (Blast_tac 1); |
173 qed "B_trusts_NS1"; |
164 qed "B_trusts_NS1"; |
177 (**** Authenticity properties obtained from NS2 ****) |
168 (**** Authenticity properties obtained from NS2 ****) |
178 |
169 |
179 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B |
170 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B |
180 [unicity of B makes Lowe's fix work] |
171 [unicity of B makes Lowe's fix work] |
181 [proof closely follows that for unique_NA] *) |
172 [proof closely follows that for unique_NA] *) |
182 Goal |
173 Goal "[| Nonce NB ~: analz (spies evs); evs : ns_public |] \ |
183 "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \ |
|
184 \ ==> EX A' NA' B'. ALL A NA B. \ |
174 \ ==> EX A' NA' B'. ALL A NA B. \ |
185 \ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \ |
175 \ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \ |
186 \ --> A=A' & NA=NA' & B=B'"; |
176 \ --> A=A' & NA=NA' & B=B'"; |
187 by (etac rev_mp 1); |
177 by (etac rev_mp 1); |
188 by (parts_induct_tac 1); |
178 by (parts_induct_tac 1); |
189 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
179 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
190 (*NS2*) |
180 (*NS2*) |
191 by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2); |
181 by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2); |
192 (*Fake*) |
182 (*Fake*) |
193 by (Clarify_tac 1); |
183 by (Clarify_tac 1); |
194 by (Blast_tac 1); |
184 by (Blast_tac 1); |
195 val lemma = result(); |
185 val lemma = result(); |
196 |
186 |
197 Goal |
187 Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
198 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
188 \ : parts(spies evs); \ |
199 \ : parts(spies evs); \ |
189 \ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ |
200 \ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ |
190 \ : parts(spies evs); \ |
201 \ : parts(spies evs); \ |
191 \ Nonce NB ~: analz (spies evs); \ |
202 \ Nonce NB ~: analz (spies evs); \ |
192 \ evs : ns_public |] \ |
203 \ evs : ns_public |] \ |
193 \ ==> A=A' & NA=NA' & B=B'"; |
204 \ ==> A=A' & NA=NA' & B=B'"; |
|
205 by (prove_unique_tac lemma 1); |
194 by (prove_unique_tac lemma 1); |
206 qed "unique_NB"; |
195 qed "unique_NB"; |
207 |
196 |
208 AddDs [unique_NB]; |
197 AddDs [unique_NB]; |
209 |
198 |
210 |
199 |
211 (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) |
200 (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) |
212 Goal |
201 Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
213 "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
202 \ : set evs; \ |
214 \ : set evs; \ |
203 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
215 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
|
216 \ ==> Nonce NB ~: analz (spies evs)"; |
204 \ ==> Nonce NB ~: analz (spies evs)"; |
217 by (etac rev_mp 1); |
205 by (etac rev_mp 1); |
218 by (analz_induct_tac 1); |
206 by (analz_induct_tac 1); |
219 (*NS3*) |
207 (*NS3*) |
220 by (Blast_tac 4); |
208 by (Blast_tac 4); |
229 AddDs [Spy_not_see_NB]; |
217 AddDs [Spy_not_see_NB]; |
230 |
218 |
231 |
219 |
232 (*Authentication for B: if he receives message 3 and has used NB |
220 (*Authentication for B: if he receives message 3 and has used NB |
233 in message 2, then A has sent message 3.*) |
221 in message 2, then A has sent message 3.*) |
234 Goal |
222 Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
235 "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
223 \ : set evs; \ |
236 \ : set evs; \ |
224 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
237 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
225 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
238 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
226 \ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
239 \ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
|
240 by (etac rev_mp 1); |
227 by (etac rev_mp 1); |
241 (*prepare induction over Crypt (pubK B) NB : parts H*) |
228 (*prepare induction over Crypt (pubK B) NB : parts H*) |
242 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
229 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
243 by (parts_induct_tac 1); |
230 by (parts_induct_tac 1); |
244 by (ALLGOALS Clarify_tac); |
231 by (ALLGOALS Clarify_tac); |
253 read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies; |
240 read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies; |
254 |
241 |
255 |
242 |
256 (*If B receives NS3 and the nonce NB agrees with the nonce he joined with |
243 (*If B receives NS3 and the nonce NB agrees with the nonce he joined with |
257 NA, then A initiated the run using NA. SAME proof as B_trusts_NS3!*) |
244 NA, then A initiated the run using NA. SAME proof as B_trusts_NS3!*) |
258 Goal |
245 Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
259 "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ |
246 \ : set evs; \ |
260 \ : set evs; \ |
247 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
261 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
248 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
262 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
249 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; |
263 \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; |
|
264 by (etac rev_mp 1); |
250 by (etac rev_mp 1); |
265 (*prepare induction over Crypt (pubK B) {|NB|} : parts H*) |
251 (*prepare induction over Crypt (pubK B) {|NB|} : parts H*) |
266 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
252 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
267 by (etac ns_public.induct 1); |
253 by (etac ns_public.induct 1); |
268 by (ALLGOALS Asm_simp_tac); |
254 by (ALLGOALS Asm_simp_tac); |