equal
deleted
inserted
replaced
40 (*Alice proves her existence by sending NB back to Bob.*) |
40 (*Alice proves her existence by sending NB back to Bob.*) |
41 NS3: "\<lbrakk>evs3 \<in> ns_public; |
41 NS3: "\<lbrakk>evs3 \<in> ns_public; |
42 Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
42 Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
43 Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk> |
43 Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk> |
44 \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public" |
44 \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public" |
45 |
|
46 (*No Oops message. Should there be one?*) |
|
47 |
45 |
48 declare knows_Spy_partsEs [elim] |
46 declare knows_Spy_partsEs [elim] |
49 declare analz_subset_parts [THEN subsetD, dest] |
47 declare analz_subset_parts [THEN subsetD, dest] |
50 declare Fake_parts_insert [THEN subsetD, dest] |
48 declare Fake_parts_insert [THEN subsetD, dest] |
51 declare image_eq_UN [simp] (*accelerates proofs involving nested images*) |
49 declare image_eq_UN [simp] (*accelerates proofs involving nested images*) |