83 lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>N K. \\<exists>evs \\<in> ns_shared. |
83 lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>N K. \\<exists>evs \\<in> ns_shared. |
84 Says A B (Crypt K \\<lbrace>Nonce N, Nonce N\\<rbrace>) \\<in> set evs" |
84 Says A B (Crypt K \\<lbrace>Nonce N, Nonce N\\<rbrace>) \\<in> set evs" |
85 apply (intro exI bexI) |
85 apply (intro exI bexI) |
86 apply (rule_tac [2] ns_shared.Nil |
86 apply (rule_tac [2] ns_shared.Nil |
87 [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3, |
87 [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3, |
88 THEN ns_shared.NS4, THEN ns_shared.NS5]) |
88 THEN ns_shared.NS4, THEN ns_shared.NS5], possibility) |
89 apply possibility |
|
90 done |
89 done |
91 |
90 |
92 (*This version is similar, while instantiating ?K and ?N to epsilon-terms |
91 (*This version is similar, while instantiating ?K and ?N to epsilon-terms |
93 lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>evs \\<in> ns_shared. |
92 lemma "A \\<noteq> Server \\<Longrightarrow> \\<exists>evs \\<in> ns_shared. |
94 Says A B (Crypt ?K \\<lbrace>Nonce ?N, Nonce ?N\\<rbrace>) \\<in> set evs" |
93 Says A B (Crypt ?K \\<lbrace>Nonce ?N, Nonce ?N\\<rbrace>) \\<in> set evs" |
114 sends messages containing X! **) |
113 sends messages containing X! **) |
115 |
114 |
116 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
115 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
117 lemma Spy_see_shrK [simp]: |
116 lemma Spy_see_shrK [simp]: |
118 "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)" |
117 "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)" |
119 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
118 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+) |
120 apply simp_all |
|
121 apply blast+; |
|
122 done |
119 done |
123 |
120 |
124 lemma Spy_analz_shrK [simp]: |
121 lemma Spy_analz_shrK [simp]: |
125 "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)" |
122 "evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)" |
126 by auto |
123 by auto |
127 |
124 |
128 |
125 |
129 (*Nobody can have used non-existent keys!*) |
126 (*Nobody can have used non-existent keys!*) |
130 lemma new_keys_not_used [rule_format, simp]: |
127 lemma new_keys_not_used [rule_format, simp]: |
131 "evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))" |
128 "evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))" |
132 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
129 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all) |
133 apply simp_all |
|
134 (*Fake, NS2, NS4, NS5*) |
130 (*Fake, NS2, NS4, NS5*) |
135 apply (blast dest!: keysFor_parts_insert)+ |
131 apply (blast dest!: keysFor_parts_insert)+ |
136 done |
132 done |
137 |
133 |
138 |
134 |
152 lemma A_trusts_NS2: |
148 lemma A_trusts_NS2: |
153 "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs); |
149 "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs); |
154 A \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
150 A \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
155 \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs" |
151 \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs" |
156 apply (erule rev_mp) |
152 apply (erule rev_mp) |
157 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
153 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto) |
158 apply auto |
|
159 done |
154 done |
160 |
155 |
161 lemma cert_A_form: |
156 lemma cert_A_form: |
162 "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs); |
157 "\\<lbrakk>Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace> \\<in> parts (spies evs); |
163 A \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
158 A \\<notin> bad; evs \\<in> ns_shared\\<rbrakk> |
180 "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs; |
175 "\\<lbrakk>Says S A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs; |
181 evs \\<in> ns_shared\\<rbrakk> |
176 evs \\<in> ns_shared\\<rbrakk> |
182 \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs |
177 \\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs |
183 \\<or> X \\<in> analz (spies evs)" |
178 \\<or> X \\<in> analz (spies evs)" |
184 apply (case_tac "A \\<in> bad") |
179 apply (case_tac "A \\<in> bad") |
185 apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]); |
180 apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]) |
186 by (blast dest!: A_trusts_NS2 Says_Server_message_form) |
181 by (blast dest!: A_trusts_NS2 Says_Server_message_form) |
187 *) |
182 *) |
188 |
183 |
189 |
184 |
190 (**** |
185 (**** |
200 to encrypt messages containing other keys, in the actual protocol. |
195 to encrypt messages containing other keys, in the actual protocol. |
201 We require that agents should behave like this subsequently also.*) |
196 We require that agents should behave like this subsequently also.*) |
202 lemma "\\<lbrakk>evs \\<in> ns_shared; Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow> |
197 lemma "\\<lbrakk>evs \\<in> ns_shared; Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow> |
203 (Crypt KAB X) \\<in> parts (spies evs) \\<and> |
198 (Crypt KAB X) \\<in> parts (spies evs) \\<and> |
204 Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)" |
199 Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)" |
205 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
200 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all) |
206 apply simp_all |
|
207 (*Fake*) |
201 (*Fake*) |
208 apply (blast dest: parts_insert_subset_Un) |
202 apply (blast dest: parts_insert_subset_Un) |
209 (*Base, NS4 and NS5*) |
203 (*Base, NS4 and NS5*) |
210 apply auto |
204 apply auto |
211 done |
205 done |
220 \\<forall>K KK. KK \\<subseteq> - (range shrK) \\<longrightarrow> |
214 \\<forall>K KK. KK \\<subseteq> - (range shrK) \\<longrightarrow> |
221 (Key K \\<in> analz (Key`KK \\<union> (spies evs))) = |
215 (Key K \\<in> analz (Key`KK \\<union> (spies evs))) = |
222 (K \\<in> KK \\<or> Key K \\<in> analz (spies evs))" |
216 (K \\<in> KK \\<or> Key K \\<in> analz (spies evs))" |
223 apply (erule ns_shared.induct, force) |
217 apply (erule ns_shared.induct, force) |
224 apply (drule_tac [7] Says_Server_message_form) |
218 apply (drule_tac [7] Says_Server_message_form) |
225 apply (erule_tac [4] Says_S_message_form [THEN disjE]) |
219 apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz) |
226 apply analz_freshK |
|
227 apply spy_analz |
|
228 done |
220 done |
229 |
221 |
230 |
222 |
231 lemma analz_insert_freshK: |
223 lemma analz_insert_freshK: |
232 "\\<lbrakk>evs \\<in> ns_shared; KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow> |
224 "\\<lbrakk>evs \\<in> ns_shared; KAB \\<notin> range shrK\\<rbrakk> \\<Longrightarrow> |
240 (*In messages of this form, the session key uniquely identifies the rest*) |
232 (*In messages of this form, the session key uniquely identifies the rest*) |
241 lemma unique_session_keys: |
233 lemma unique_session_keys: |
242 "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs; |
234 "\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs; |
243 Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs; |
235 Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs; |
244 evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'" |
236 evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'" |
245 apply (erule rev_mp, erule rev_mp, erule ns_shared.induct) |
237 apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+) |
246 apply simp_all |
|
247 apply blast+ |
|
248 done |
238 done |
249 |
239 |
250 |
240 |
251 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) |
241 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) |
252 |
242 |
261 apply (erule rev_mp) |
251 apply (erule rev_mp) |
262 apply (erule ns_shared.induct, force) |
252 apply (erule ns_shared.induct, force) |
263 apply (frule_tac [7] Says_Server_message_form) |
253 apply (frule_tac [7] Says_Server_message_form) |
264 apply (frule_tac [4] Says_S_message_form) |
254 apply (frule_tac [4] Says_S_message_form) |
265 apply (erule_tac [5] disjE) |
255 apply (erule_tac [5] disjE) |
266 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs) |
256 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz) (*Fake*) |
267 apply spy_analz (*Fake*) |
|
268 apply blast (*NS2*) |
257 apply blast (*NS2*) |
269 (*NS3, Server sub-case*) (**LEVEL 8 **) |
258 (*NS3, Server sub-case*) (**LEVEL 8 **) |
270 apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2 |
259 apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2 |
271 dest: Says_imp_knows_Spy analz.Inj unique_session_keys) |
260 dest: Says_imp_knows_Spy analz.Inj unique_session_keys) |
272 (*NS3, Spy sub-case; also Oops*) |
261 (*NS3, Spy sub-case; also Oops*) |
293 \\<Longrightarrow> \\<exists>NA. Says Server A |
282 \\<Longrightarrow> \\<exists>NA. Says Server A |
294 (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, |
283 (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, |
295 Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) |
284 Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) |
296 \\<in> set evs" |
285 \\<in> set evs" |
297 apply (erule rev_mp) |
286 apply (erule rev_mp) |
298 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
287 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto) |
299 apply auto |
|
300 done |
288 done |
301 |
289 |
302 |
290 |
303 lemma A_trusts_NS4_lemma [rule_format]: |
291 lemma A_trusts_NS4_lemma [rule_format]: |
304 "evs \\<in> ns_shared \\<Longrightarrow> |
292 "evs \\<in> ns_shared \\<Longrightarrow> |
305 Key K \\<notin> analz (spies evs) \\<longrightarrow> |
293 Key K \\<notin> analz (spies evs) \\<longrightarrow> |
306 Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow> |
294 Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow> |
307 Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow> |
295 Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow> |
308 Says B A (Crypt K (Nonce NB)) \\<in> set evs" |
296 Says B A (Crypt K (Nonce NB)) \\<in> set evs" |
309 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
297 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
310 apply (analz_mono_contra, simp_all) |
298 apply (analz_mono_contra, simp_all, blast) (*Fake*) |
311 apply blast (*Fake*) |
|
312 (*NS2: contradiction from the assumptions |
299 (*NS2: contradiction from the assumptions |
313 Key K \\<notin> used evs2 and Crypt K (Nonce NB) \\<in> parts (spies evs2) *) |
300 Key K \\<notin> used evs2 and Crypt K (Nonce NB) \\<in> parts (spies evs2) *) |
314 apply (force dest!: Crypt_imp_keysFor) |
301 apply (force dest!: Crypt_imp_keysFor, blast) (*NS3*) |
315 apply blast (*NS3*) |
|
316 (*NS4*) |
302 (*NS4*) |
317 apply (blast dest!: B_trusts_NS3 |
303 apply (blast dest!: B_trusts_NS3 |
318 dest: Says_imp_knows_Spy [THEN analz.Inj] |
304 dest: Says_imp_knows_Spy [THEN analz.Inj] |
319 Crypt_Spy_analz_bad unique_session_keys) |
305 Crypt_Spy_analz_bad unique_session_keys) |
320 done |
306 done |
336 "evs \\<in> ns_shared \\<Longrightarrow> |
322 "evs \\<in> ns_shared \\<Longrightarrow> |
337 Key K \\<notin> analz (spies evs) \\<longrightarrow> |
323 Key K \\<notin> analz (spies evs) \\<longrightarrow> |
338 Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow> |
324 Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow> |
339 Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow> |
325 Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow> |
340 (\\<exists>A'. Says A' B X \\<in> set evs)" |
326 (\\<exists>A'. Says A' B X \\<in> set evs)" |
341 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
327 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra) |
342 apply analz_mono_contra |
328 apply (simp_all add: ex_disj_distrib, blast) (*Fake*) |
343 apply (simp_all add: ex_disj_distrib) |
|
344 apply blast (*Fake*) |
|
345 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*) |
329 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*) |
346 apply blast (*NS3*) |
330 apply blast (*NS3*) |
347 (*NS4*) |
331 (*NS4*) |
348 apply (blast dest!: B_trusts_NS3 |
332 apply (blast dest!: B_trusts_NS3 |
349 dest: Says_imp_knows_Spy [THEN analz.Inj] |
333 dest: Says_imp_knows_Spy [THEN analz.Inj] |
357 Says Server A |
341 Says Server A |
358 (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, |
342 (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, |
359 Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow> |
343 Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow> |
360 Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow> |
344 Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow> |
361 Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs" |
345 Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs" |
362 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
346 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast) (*Fake*) |
363 apply analz_mono_contra |
|
364 apply simp_all |
|
365 apply blast (*Fake*) |
|
366 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*) |
347 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*) |
367 apply (blast dest!: cert_A_form) (*NS3*) |
348 apply (blast dest!: cert_A_form) (*NS3*) |
368 (*NS5*) |
349 (*NS5*) |
369 apply (blast dest!: A_trusts_NS2 |
350 apply (blast dest!: A_trusts_NS2 |
370 dest: Says_imp_knows_Spy [THEN analz.Inj] |
351 dest: Says_imp_knows_Spy [THEN analz.Inj] |