equal
deleted
inserted
replaced
352 assumes N: "\<And>N. P (Nonce N)" |
352 assumes N: "\<And>N. P (Nonce N)" |
353 and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)" |
353 and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)" |
354 and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)" |
354 and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)" |
355 and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)" |
355 and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)" |
356 shows "P msg" |
356 shows "P msg" |
357 using N M C D by (blast intro: msg_induct_aux) |
357 using N M C D by (rule msg_induct_aux) |
358 |
358 |
359 subsection{*The Abstract Discriminator*} |
359 subsection{*The Abstract Discriminator*} |
360 |
360 |
361 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't |
361 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't |
362 need this function in order to prove discrimination theorems.*} |
362 need this function in order to prove discrimination theorems.*} |