equal
deleted
inserted
replaced
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 thy |
22 Goal |
23 "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ |
23 "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ |
24 \ 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)); |
25 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); |
26 by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); |
27 by possibility_tac; |
27 by possibility_tac; |
29 |
29 |
30 |
30 |
31 (**** Inductive proofs about ns_public ****) |
31 (**** Inductive proofs about ns_public ****) |
32 |
32 |
33 (*Nobody sends themselves messages*) |
33 (*Nobody sends themselves messages*) |
34 goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs"; |
34 Goal "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs"; |
35 by (etac ns_public.induct 1); |
35 by (etac ns_public.induct 1); |
36 by Auto_tac; |
36 by Auto_tac; |
37 qed_spec_mp "not_Says_to_self"; |
37 qed_spec_mp "not_Says_to_self"; |
38 Addsimps [not_Says_to_self]; |
38 Addsimps [not_Says_to_self]; |
39 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
39 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
52 |
52 |
53 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
53 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
54 sends messages containing X! **) |
54 sends messages containing X! **) |
55 |
55 |
56 (*Spy never sees another agent's private key! (unless it's bad at start)*) |
56 (*Spy never sees another agent's private key! (unless it's bad at start)*) |
57 goal thy |
57 Goal |
58 "!!A. 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); |
59 by (parts_induct_tac 1); |
60 by (Blast_tac 1); |
60 by (Blast_tac 1); |
61 qed "Spy_see_priK"; |
61 qed "Spy_see_priK"; |
62 Addsimps [Spy_see_priK]; |
62 Addsimps [Spy_see_priK]; |
63 |
63 |
64 goal thy |
64 Goal |
65 "!!A. 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; |
66 by Auto_tac; |
67 qed "Spy_analz_priK"; |
67 qed "Spy_analz_priK"; |
68 Addsimps [Spy_analz_priK]; |
68 Addsimps [Spy_analz_priK]; |
69 |
69 |
73 |
73 |
74 (**** Authenticity properties obtained from NS2 ****) |
74 (**** Authenticity properties obtained from NS2 ****) |
75 |
75 |
76 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
76 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
77 is secret. (Honest users generate fresh nonces.)*) |
77 is secret. (Honest users generate fresh nonces.)*) |
78 goal thy |
78 Goal |
79 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
79 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
80 \ 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)"; |
81 \ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)"; |
82 by (etac rev_mp 1); |
82 by (etac rev_mp 1); |
83 by (etac rev_mp 1); |
83 by (etac rev_mp 1); |
88 (*Adding it to the claset slows down proofs...*) |
88 (*Adding it to the claset slows down proofs...*) |
89 val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE); |
89 val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE); |
90 |
90 |
91 |
91 |
92 (*Unicity for NS1: nonce NA identifies agents A and B*) |
92 (*Unicity for NS1: nonce NA identifies agents A and B*) |
93 goal thy |
93 Goal |
94 "!!evs. [| 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. \ |
95 \ ==> EX A' B'. ALL A B. \ |
96 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ |
96 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ |
97 \ A=A' & B=B'"; |
97 \ A=A' & B=B'"; |
98 by (etac rev_mp 1); |
98 by (etac rev_mp 1); |
103 (*Fake*) |
103 (*Fake*) |
104 by (Clarify_tac 1); |
104 by (Clarify_tac 1); |
105 by (Blast_tac 1); |
105 by (Blast_tac 1); |
106 val lemma = result(); |
106 val lemma = result(); |
107 |
107 |
108 goal thy |
108 Goal |
109 "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ |
109 "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ |
110 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ |
110 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ |
111 \ Nonce NA ~: analz (spies evs); \ |
111 \ Nonce NA ~: analz (spies evs); \ |
112 \ evs : ns_public |] \ |
112 \ evs : ns_public |] \ |
113 \ ==> A=A' & B=B'"; |
113 \ ==> A=A' & B=B'"; |
120 etac ns_public.induct i THEN |
120 etac ns_public.induct i THEN |
121 ALLGOALS Asm_simp_tac; |
121 ALLGOALS Asm_simp_tac; |
122 |
122 |
123 |
123 |
124 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
124 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
125 goal thy |
125 Goal |
126 "!!evs. [| 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; \ |
127 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
127 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
128 \ ==> Nonce NA ~: analz (spies evs)"; |
128 \ ==> Nonce NA ~: analz (spies evs)"; |
129 by (etac rev_mp 1); |
129 by (etac rev_mp 1); |
130 by (analz_induct_tac 1); |
130 by (analz_induct_tac 1); |
139 qed "Spy_not_see_NA"; |
139 qed "Spy_not_see_NA"; |
140 |
140 |
141 |
141 |
142 (*Authentication for A: if she receives message 2 and has used NA |
142 (*Authentication for A: if she receives message 2 and has used NA |
143 to start a run, then B has sent message 2.*) |
143 to start a run, then B has sent message 2.*) |
144 goal thy |
144 Goal |
145 "!!evs. [| 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; \ |
146 \ 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|}) \ |
147 \ : set evs; \ |
147 \ : set evs; \ |
148 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
148 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
149 \ ==> 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|}) \ |
159 by (blast_tac (claset() addDs [Spy_not_see_NA]) 1); |
159 by (blast_tac (claset() addDs [Spy_not_see_NA]) 1); |
160 qed "A_trusts_NS2"; |
160 qed "A_trusts_NS2"; |
161 |
161 |
162 |
162 |
163 (*If the encrypted message appears then it originated with Alice in NS1*) |
163 (*If the encrypted message appears then it originated with Alice in NS1*) |
164 goal thy |
164 Goal |
165 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
165 "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
166 \ Nonce NA ~: analz (spies evs); \ |
166 \ Nonce NA ~: analz (spies evs); \ |
167 \ evs : ns_public |] \ |
167 \ evs : ns_public |] \ |
168 \ ==> 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); |
169 by (etac rev_mp 1); |
177 (**** Authenticity properties obtained from NS2 ****) |
177 (**** Authenticity properties obtained from NS2 ****) |
178 |
178 |
179 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B |
179 (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B |
180 [unicity of B makes Lowe's fix work] |
180 [unicity of B makes Lowe's fix work] |
181 [proof closely follows that for unique_NA] *) |
181 [proof closely follows that for unique_NA] *) |
182 goal thy |
182 Goal |
183 "!!evs. [| 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. \ |
184 \ ==> EX A' NA' B'. ALL A NA B. \ |
185 \ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \ |
185 \ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \ |
186 \ --> A=A' & NA=NA' & B=B'"; |
186 \ --> A=A' & NA=NA' & B=B'"; |
187 by (etac rev_mp 1); |
187 by (etac rev_mp 1); |
192 (*Fake*) |
192 (*Fake*) |
193 by (Clarify_tac 1); |
193 by (Clarify_tac 1); |
194 by (Blast_tac 1); |
194 by (Blast_tac 1); |
195 val lemma = result(); |
195 val lemma = result(); |
196 |
196 |
197 goal thy |
197 Goal |
198 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
198 "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ |
199 \ : parts(spies evs); \ |
199 \ : parts(spies evs); \ |
200 \ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ |
200 \ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ |
201 \ : parts(spies evs); \ |
201 \ : parts(spies evs); \ |
202 \ Nonce NB ~: analz (spies evs); \ |
202 \ Nonce NB ~: analz (spies evs); \ |
207 |
207 |
208 AddDs [unique_NB]; |
208 AddDs [unique_NB]; |
209 |
209 |
210 |
210 |
211 (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) |
211 (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) |
212 goal thy |
212 Goal |
213 "!!evs. [| 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|}) \ |
214 \ : set evs; \ |
214 \ : set evs; \ |
215 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
215 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
216 \ ==> Nonce NB ~: analz (spies evs)"; |
216 \ ==> Nonce NB ~: analz (spies evs)"; |
217 by (etac rev_mp 1); |
217 by (etac rev_mp 1); |
229 AddDs [Spy_not_see_NB]; |
229 AddDs [Spy_not_see_NB]; |
230 |
230 |
231 |
231 |
232 (*Authentication for B: if he receives message 3 and has used NB |
232 (*Authentication for B: if he receives message 3 and has used NB |
233 in message 2, then A has sent message 3.*) |
233 in message 2, then A has sent message 3.*) |
234 goal thy |
234 Goal |
235 "!!evs. [| 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|}) \ |
236 \ : set evs; \ |
236 \ : set evs; \ |
237 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
237 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
238 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
238 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
239 \ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
239 \ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
253 read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies; |
253 read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies; |
254 |
254 |
255 |
255 |
256 (*If B receives NS3 and the nonce NB agrees with the nonce he joined with |
256 (*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!*) |
257 NA, then A initiated the run using NA. SAME proof as B_trusts_NS3!*) |
258 goal thy |
258 Goal |
259 "!!evs. [| 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|}) \ |
260 \ : set evs; \ |
260 \ : set evs; \ |
261 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
261 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
262 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
262 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
263 \ ==> 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"; |