1 (* Title: HOL/Auth/NS_Public_Bad |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. |
|
7 Flawed version, vulnerable to Lowe's attack. |
|
8 |
|
9 From page 260 of |
|
10 Burrows, Abadi and Needham. A Logic of Authentication. |
|
11 Proc. Royal Soc. 426 (1989) |
|
12 *) |
|
13 |
|
14 AddEs spies_partsEs; |
|
15 AddDs [impOfSubs analz_subset_parts]; |
|
16 AddDs [impOfSubs Fake_parts_insert]; |
|
17 |
|
18 AddIffs [Spy_in_bad]; |
|
19 |
|
20 Addsimps [image_eq_UN]; (*accelerates proofs involving nested images*) |
|
21 |
|
22 (*A "possibility property": there are traces that reach the end*) |
|
23 Goal |
|
24 "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
|
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); |
|
27 by possibility_tac; |
|
28 result(); |
|
29 |
|
30 |
|
31 (**** Inductive proofs about ns_public ****) |
|
32 |
|
33 (*Induction for regularity theorems. If induction formula has the form |
|
34 X ~: analz (spies evs) --> ... then it shortens the proof by discarding |
|
35 needless information about analz (insert X (spies evs)) *) |
|
36 fun parts_induct_tac i = |
|
37 etac ns_public.induct i |
|
38 THEN |
|
39 REPEAT (FIRSTGOAL analz_mono_contra_tac) |
|
40 THEN |
|
41 prove_simple_subgoals_tac i; |
|
42 |
|
43 |
|
44 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
|
45 sends messages containing X! **) |
|
46 |
|
47 (*Spy never sees another agent's private key! (unless it's bad at start)*) |
|
48 Goal "evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; |
|
49 by (parts_induct_tac 1); |
|
50 by (Blast_tac 1); |
|
51 qed "Spy_see_priK"; |
|
52 Addsimps [Spy_see_priK]; |
|
53 |
|
54 Goal "evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; |
|
55 by Auto_tac; |
|
56 qed "Spy_analz_priK"; |
|
57 Addsimps [Spy_analz_priK]; |
|
58 |
|
59 AddSDs [Spy_see_priK RSN (2, rev_iffD1), |
|
60 Spy_analz_priK RSN (2, rev_iffD1)]; |
|
61 |
|
62 |
|
63 (**** Authenticity properties obtained from NS2 ****) |
|
64 |
|
65 (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce |
|
66 is secret. (Honest users generate fresh nonces.)*) |
|
67 Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
|
68 \ Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
|
69 \ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies evs)"; |
|
70 by (etac rev_mp 1); |
|
71 by (etac rev_mp 1); |
|
72 by (parts_induct_tac 1); |
|
73 by (ALLGOALS Blast_tac); |
|
74 qed "no_nonce_NS1_NS2"; |
|
75 |
|
76 (*Adding it to the claset slows down proofs...*) |
|
77 val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE); |
|
78 |
|
79 |
|
80 (*Unicity for NS1: nonce NA identifies agents A and B*) |
|
81 Goal "[| Nonce NA ~: analz (spies evs); evs : ns_public |] \ |
|
82 \ ==> EX A' B'. ALL A B. \ |
|
83 \ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \ |
|
84 \ A=A' & B=B'"; |
|
85 by (etac rev_mp 1); |
|
86 by (parts_induct_tac 1); |
|
87 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
|
88 (*NS1*) |
|
89 by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2); |
|
90 (*Fake*) |
|
91 by (Clarify_tac 1); |
|
92 by (Blast_tac 1); |
|
93 val lemma = result(); |
|
94 |
|
95 Goal "[| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \ |
|
96 \ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \ |
|
97 \ Nonce NA ~: analz (spies evs); \ |
|
98 \ evs : ns_public |] \ |
|
99 \ ==> A=A' & B=B'"; |
|
100 by (prove_unique_tac lemma 1); |
|
101 qed "unique_NA"; |
|
102 |
|
103 |
|
104 (*Tactic for proving secrecy theorems*) |
|
105 fun analz_induct_tac i = |
|
106 etac ns_public.induct i THEN |
|
107 ALLGOALS Asm_simp_tac; |
|
108 |
|
109 |
|
110 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) |
|
111 Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
|
112 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
|
113 \ ==> Nonce NA ~: analz (spies evs)"; |
|
114 by (etac rev_mp 1); |
|
115 by (analz_induct_tac 1); |
|
116 (*NS3*) |
|
117 by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4); |
|
118 (*NS2*) |
|
119 by (blast_tac (claset() addDs [unique_NA]) 3); |
|
120 (*NS1*) |
|
121 by (Blast_tac 2); |
|
122 (*Fake*) |
|
123 by (spy_analz_tac 1); |
|
124 qed "Spy_not_see_NA"; |
|
125 |
|
126 |
|
127 (*Authentication for A: if she receives message 2 and has used NA |
|
128 to start a run, then B has sent message 2.*) |
|
129 Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ |
|
130 \ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs; \ |
|
131 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
|
132 \ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs"; |
|
133 by (etac rev_mp 1); |
|
134 (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*) |
|
135 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
|
136 by (etac ns_public.induct 1); |
|
137 by (ALLGOALS Asm_simp_tac); |
|
138 by (ALLGOALS Clarify_tac); |
|
139 (*NS2*) |
|
140 by (blast_tac (claset() addDs [Spy_not_see_NA, unique_NA]) 3); |
|
141 (*NS1*) |
|
142 by (Blast_tac 2); |
|
143 (*Fake*) |
|
144 by (blast_tac (claset() addDs [Spy_not_see_NA]) 1); |
|
145 qed "A_trusts_NS2"; |
|
146 |
|
147 |
|
148 (*If the encrypted message appears then it originated with Alice in NS1*) |
|
149 Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ |
|
150 \ Nonce NA ~: analz (spies evs); \ |
|
151 \ evs : ns_public |] \ |
|
152 \==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; |
|
153 by (etac rev_mp 1); |
|
154 by (etac rev_mp 1); |
|
155 by (parts_induct_tac 1); |
|
156 by (Blast_tac 1); |
|
157 qed "B_trusts_NS1"; |
|
158 |
|
159 |
|
160 |
|
161 (**** Authenticity properties obtained from NS2 ****) |
|
162 |
|
163 (*Unicity for NS2: nonce NB identifies nonce NA and agent A |
|
164 [proof closely follows that for unique_NA] *) |
|
165 Goal "[| Nonce NB ~: analz (spies evs); evs : ns_public |] \ |
|
166 \ ==> EX A' NA'. ALL A NA. \ |
|
167 \ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies evs) \ |
|
168 \ --> A=A' & NA=NA'"; |
|
169 by (etac rev_mp 1); |
|
170 by (parts_induct_tac 1); |
|
171 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
|
172 (*NS2*) |
|
173 by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2); |
|
174 (*Fake*) |
|
175 by (Blast_tac 1); |
|
176 val lemma = result(); |
|
177 |
|
178 Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies evs); \ |
|
179 \ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \ |
|
180 \ Nonce NB ~: analz (spies evs); \ |
|
181 \ evs : ns_public |] \ |
|
182 \ ==> A=A' & NA=NA'"; |
|
183 by (prove_unique_tac lemma 1); |
|
184 qed "unique_NB"; |
|
185 |
|
186 |
|
187 (*NB remains secret PROVIDED Alice never responds with round 3*) |
|
188 Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ |
|
189 \ ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs; \ |
|
190 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
|
191 \ ==> Nonce NB ~: analz (spies evs)"; |
|
192 by (etac rev_mp 1); |
|
193 by (etac rev_mp 1); |
|
194 by (analz_induct_tac 1); |
|
195 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
|
196 by (ALLGOALS Clarify_tac); |
|
197 (*NS3: because NB determines A*) |
|
198 by (blast_tac (claset() addDs [unique_NB]) 4); |
|
199 (*NS2: by freshness and unicity of NB*) |
|
200 by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3); |
|
201 (*NS1: by freshness*) |
|
202 by (Blast_tac 2); |
|
203 (*Fake*) |
|
204 by (spy_analz_tac 1); |
|
205 qed "Spy_not_see_NB"; |
|
206 |
|
207 |
|
208 |
|
209 (*Authentication for B: if he receives message 3 and has used NB |
|
210 in message 2, then A has sent message 3--to somebody....*) |
|
211 Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \ |
|
212 \ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \ |
|
213 \ A ~: bad; B ~: bad; evs : ns_public |] \ |
|
214 \ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs"; |
|
215 by (etac rev_mp 1); |
|
216 (*prepare induction over Crypt (pubK B) NB : parts H*) |
|
217 by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); |
|
218 by (parts_induct_tac 1); |
|
219 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); |
|
220 by (ALLGOALS Clarify_tac); |
|
221 (*NS3: because NB determines A (this use of unique_NB is more robust) *) |
|
222 by (blast_tac (claset() addDs [Spy_not_see_NB] |
|
223 addIs [unique_NB RS conjunct1]) 3); |
|
224 (*NS1: by freshness*) |
|
225 by (Blast_tac 2); |
|
226 (*Fake*) |
|
227 by (blast_tac (claset() addDs [Spy_not_see_NB]) 1); |
|
228 qed "B_trusts_NS3"; |
|
229 |
|
230 |
|
231 (*Can we strengthen the secrecy theorem? NO*) |
|
232 Goal "[| A ~: bad; B ~: bad; evs : ns_public |] \ |
|
233 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \ |
|
234 \ --> Nonce NB ~: analz (spies evs)"; |
|
235 by (analz_induct_tac 1); |
|
236 by (ALLGOALS Clarify_tac); |
|
237 (*NS2: by freshness and unicity of NB*) |
|
238 by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3); |
|
239 (*NS1: by freshness*) |
|
240 by (Blast_tac 2); |
|
241 (*Fake*) |
|
242 by (spy_analz_tac 1); |
|
243 (*NS3: unicity of NB identifies A and NA, but not B*) |
|
244 by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1 |
|
245 THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1)); |
|
246 by Auto_tac; |
|
247 by (rename_tac "C B' evs3" 1); |
|
248 |
|
249 (* |
|
250 THIS IS THE ATTACK! |
|
251 Level 8 |
|
252 !!evs. [| A ~: bad; B ~: bad; evs : ns_public |] |
|
253 ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs --> |
|
254 Nonce NB ~: analz (spies evs) |
|
255 1. !!C B' evs3. |
|
256 [| A ~: bad; B ~: bad; evs3 : ns_public; |
|
257 Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) : set evs3; |
|
258 Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3; C : bad; |
|
259 Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3; |
|
260 Nonce NB ~: analz (spies evs3) |] |
|
261 ==> False |
|
262 *) |
|