added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
theory Larry+ −
imports Main "../QuotMain"+ −
begin+ −
+ −
subsection{*Defining the Free Algebra*}+ −
+ −
datatype+ −
freemsg = NONCE nat+ −
| MPAIR freemsg freemsg+ −
| CRYPT nat freemsg + −
| DECRYPT nat freemsg+ −
+ −
inductive + −
msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)+ −
where + −
CD: "CRYPT K (DECRYPT K X) \<sim> X"+ −
| DC: "DECRYPT K (CRYPT K X) \<sim> X"+ −
| NONCE: "NONCE N \<sim> NONCE N"+ −
| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"+ −
| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"+ −
| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"+ −
| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"+ −
| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"+ −
+ −
text{*Proving that it is an equivalence relation*}+ −
+ −
lemma msgrel_refl: "X \<sim> X"+ −
by (induct X, (blast intro: msgrel.intros)+)+ −
+ −
theorem equiv_msgrel: "equivp msgrel"+ −
proof (rule equivpI)+ −
show "reflp msgrel" by (simp add: reflp_def msgrel_refl)+ −
show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)+ −
show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)+ −
qed+ −
+ −
subsection{*Some Functions on the Free Algebra*}+ −
+ −
subsubsection{*The Set of Nonces*}+ −
+ −
primrec+ −
freenonces :: "freemsg \<Rightarrow> nat set"+ −
where+ −
"freenonces (NONCE N) = {N}"+ −
| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"+ −
| "freenonces (CRYPT K X) = freenonces X"+ −
| "freenonces (DECRYPT K X) = freenonces X"+ −
+ −
theorem msgrel_imp_eq_freenonces: + −
"U \<sim> V \<Longrightarrow> freenonces U = freenonces V"+ −
by (erule msgrel.induct, auto) + −
+ −
subsubsection{*The Left Projection*}+ −
+ −
text{*A function to return the left part of the top pair in a message. It will+ −
be lifted to the initial algrebra, to serve as an example of that process.*}+ −
fun+ −
freeleft :: "freemsg \<Rightarrow> freemsg"+ −
where+ −
"freeleft (NONCE N) = NONCE N"+ −
| "freeleft (MPAIR X Y) = X"+ −
| "freeleft (CRYPT K X) = freeleft X"+ −
| "freeleft (DECRYPT K X) = freeleft X"+ −
+ −
text{*This theorem lets us prove that the left function respects the+ −
equivalence relation. It also helps us prove that MPair+ −
(the abstract constructor) is injective*}+ −
lemma msgrel_imp_eqv_freeleft_aux:+ −
shows "freeleft U \<sim> freeleft U"+ −
apply(induct rule: freeleft.induct)+ −
apply(auto intro: msgrel.intros)+ −
done+ −
+ −
theorem msgrel_imp_eqv_freeleft:+ −
"U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"+ −
apply(erule msgrel.induct)+ −
apply(auto intro: msgrel.intros msgrel_imp_eqv_freeleft_aux)+ −
done+ −
+ −
subsubsection{*The Right Projection*}+ −
+ −
text{*A function to return the right part of the top pair in a message.*}+ −
fun+ −
freeright :: "freemsg \<Rightarrow> freemsg"+ −
where+ −
"freeright (NONCE N) = NONCE N"+ −
| "freeright (MPAIR X Y) = Y"+ −
| "freeright (CRYPT K X) = freeright X"+ −
| "freeright (DECRYPT K X) = freeright X"+ −
+ −
text{*This theorem lets us prove that the right function respects the+ −
equivalence relation. It also helps us prove that MPair+ −
(the abstract constructor) is injective*}+ −
lemma msgrel_imp_eqv_freeright_aux:+ −
shows "freeright U \<sim> freeright U"+ −
apply(induct rule: freeright.induct)+ −
apply(auto intro: msgrel.intros)+ −
done+ −
+ −
theorem msgrel_imp_eqv_freeright:+ −
"U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"+ −
by (erule msgrel.induct, auto intro: msgrel.intros msgrel_imp_eqv_freeright_aux)+ −
+ −
subsubsection{*The Discriminator for Constructors*}+ −
+ −
text{*A function to distinguish nonces, mpairs and encryptions*}+ −
fun + −
freediscrim :: "freemsg \<Rightarrow> int"+ −
where+ −
"freediscrim (NONCE N) = 0"+ −
| "freediscrim (MPAIR X Y) = 1"+ −
| "freediscrim (CRYPT K X) = freediscrim X + 2"+ −
| "freediscrim (DECRYPT K X) = freediscrim X - 2"+ −
+ −
text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}+ −
theorem msgrel_imp_eq_freediscrim:+ −
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"+ −
by (erule msgrel.induct, auto)+ −
+ −
+ −
subsection{*The Initial Algebra: A Quotiented Message Type*}+ −
+ −
quotient msg = freemsg / msgrel+ −
by (rule equiv_msgrel)+ −
+ −
text{*The abstract message constructors*}+ −
+ −
quotient_def+ −
Nonce::"Nonce :: nat \<Rightarrow> msg"+ −
where+ −
"NONCE"+ −
+ −
quotient_def+ −
MPair::"MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"+ −
where+ −
"MPAIR"+ −
+ −
quotient_def+ −
Crypt::"Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"+ −
where+ −
"CRYPT"+ −
+ −
quotient_def+ −
Decrypt::"Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"+ −
where+ −
"DECRYPT"+ −
+ −
lemma [quot_respect]:+ −
shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"+ −
by (auto intro: CRYPT)+ −
+ −
lemma [quot_respect]:+ −
shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"+ −
by (auto intro: DECRYPT)+ −
+ −
text{*Establishing these two equations is the point of the whole exercise*}+ −
theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"+ −
by (lifting CD)+ −
+ −
theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"+ −
by (lifting DC)+ −
+ −
subsection{*The Abstract Function to Return the Set of Nonces*}+ −
+ −
quotient_def+ −
nonces :: "nounces:: msg \<Rightarrow> nat set"+ −
where+ −
"freenonces"+ −
+ −
text{*Now prove the four equations for @{term nonces}*}+ −
+ −
lemma [quot_respect]:+ −
shows "(op \<sim> ===> op =) freenonces freenonces"+ −
by (simp add: msgrel_imp_eq_freenonces)+ −
+ −
lemma [quot_respect]:+ −
shows "(op = ===> op \<sim>) NONCE NONCE"+ −
by (simp add: NONCE)+ −
+ −
lemma nonces_Nonce [simp]: + −
shows "nonces (Nonce N) = {N}"+ −
by (lifting freenonces.simps(1))+ −
+ −
lemma [quot_respect]:+ −
shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"+ −
by (simp add: MPAIR)+ −
+ −
lemma nonces_MPair [simp]: + −
shows "nonces (MPair X Y) = nonces X \<union> nonces Y"+ −
by (lifting freenonces.simps(2))+ −
+ −
lemma nonces_Crypt [simp]: + −
shows "nonces (Crypt K X) = nonces X"+ −
by (lifting freenonces.simps(3))+ −
+ −
lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"+ −
by (lifting freenonces.simps(4))+ −
+ −
subsection{*The Abstract Function to Return the Left Part*}+ −
+ −
quotient_def+ −
left :: "left:: msg \<Rightarrow> msg"+ −
where+ −
"freeleft"+ −
+ −
lemma [quot_respect]:+ −
shows "(op \<sim> ===> op \<sim>) freeleft freeleft"+ −
by (simp add: msgrel_imp_eqv_freeleft)+ −
+ −
lemma left_Nonce [simp]: + −
shows "left (Nonce N) = Nonce N"+ −
by (lifting freeleft.simps(1))+ −
+ −
lemma left_MPair [simp]: + −
shows "left (MPair X Y) = X"+ −
by (lifting freeleft.simps(2))+ −
+ −
lemma left_Crypt [simp]: + −
shows "left (Crypt K X) = left X"+ −
by (lifting freeleft.simps(3))+ −
+ −
lemma left_Decrypt [simp]: + −
shows "left (Decrypt K X) = left X"+ −
by (lifting freeleft.simps(4))+ −
+ −
subsection{*The Abstract Function to Return the Right Part*}+ −
+ −
quotient_def+ −
right :: "right:: msg \<Rightarrow> msg"+ −
where+ −
"freeright"+ −
+ −
text{*Now prove the four equations for @{term right}*}+ −
+ −
lemma [quot_respect]:+ −
shows "(op \<sim> ===> op \<sim>) freeright freeright"+ −
by (simp add: msgrel_imp_eqv_freeright)+ −
+ −
lemma right_Nonce [simp]: + −
shows "right (Nonce N) = Nonce N"+ −
by (lifting freeright.simps(1))+ −
+ −
lemma right_MPair [simp]: + −
shows "right (MPair X Y) = Y"+ −
by (lifting freeright.simps(2))+ −
+ −
lemma right_Crypt [simp]: + −
shows "right (Crypt K X) = right X"+ −
by (lifting freeright.simps(3))+ −
+ −
lemma right_Decrypt [simp]: + −
shows "right (Decrypt K X) = right X"+ −
by (lifting freeright.simps(4))+ −
+ −
subsection{*Injectivity Properties of Some Constructors*}+ −
+ −
lemma NONCE_imp_eq: + −
shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"+ −
by (drule msgrel_imp_eq_freenonces, simp)+ −
+ −
text{*Can also be proved using the function @{term nonces}*}+ −
lemma Nonce_Nonce_eq [iff]: + −
shows "(Nonce m = Nonce n) = (m = n)"+ −
apply(rule iffI)+ −
apply(lifting NONCE_imp_eq)+ −
apply(simp)+ −
done+ −
+ −
lemma MPAIR_imp_eqv_left: + −
shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"+ −
by (drule msgrel_imp_eqv_freeleft, simp)+ −
+ −
lemma MPair_imp_eq_left: + −
assumes eq: "MPair X Y = MPair X' Y'" + −
shows "X = X'"+ −
using eq by (lifting MPAIR_imp_eqv_left)+ −
+ −
lemma MPAIR_imp_eqv_right: + −
shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"+ −
by (drule msgrel_imp_eqv_freeright, simp)+ −
+ −
lemma MPair_imp_eq_right: + −
shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"+ −
by (lifting MPAIR_imp_eqv_right)+ −
+ −
theorem MPair_MPair_eq [iff]: + −
shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" + −
by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)+ −
+ −
lemma NONCE_neqv_MPAIR: + −
shows "\<not>(NONCE m \<sim> MPAIR X Y)"+ −
by (auto dest: msgrel_imp_eq_freediscrim)+ −
+ −
theorem Nonce_neq_MPair [iff]: + −
shows "Nonce N \<noteq> MPair X Y"+ −
by (lifting NONCE_neqv_MPAIR)+ −
+ −
text{*Example suggested by a referee*}+ −
+ −
lemma CRYPT_NONCE_neq_NONCE:+ −
shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"+ −
by (auto dest: msgrel_imp_eq_freediscrim)+ −
+ −
theorem Crypt_Nonce_neq_Nonce: + −
shows "Crypt K (Nonce M) \<noteq> Nonce N"+ −
by (lifting CRYPT_NONCE_neq_NONCE)+ −
+ −
text{*...and many similar results*}+ −
lemma CRYPT2_NONCE_neq_NONCE: + −
shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"+ −
by (auto dest: msgrel_imp_eq_freediscrim) + −
+ −
theorem Crypt2_Nonce_neq_Nonce: + −
shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"+ −
by (lifting CRYPT2_NONCE_neq_NONCE) + −
+ −
theorem Crypt_Crypt_eq [iff]: + −
shows "(Crypt K X = Crypt K X') = (X=X')" + −
proof+ −
assume "Crypt K X = Crypt K X'"+ −
hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp+ −
thus "X = X'" by simp+ −
next+ −
assume "X = X'"+ −
thus "Crypt K X = Crypt K X'" by simp+ −
qed+ −
+ −
theorem Decrypt_Decrypt_eq [iff]: + −
shows "(Decrypt K X = Decrypt K X') = (X=X')" + −
proof+ −
assume "Decrypt K X = Decrypt K X'"+ −
hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp+ −
thus "X = X'" by simp+ −
next+ −
assume "X = X'"+ −
thus "Decrypt K X = Decrypt K X'" by simp+ −
qed+ −
+ −
lemma msg_induct_aux:+ −
shows "\<lbrakk>\<And>N. P (Nonce N);+ −
\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);+ −
\<And>K X. P X \<Longrightarrow> P (Crypt K X);+ −
\<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"+ −
by (lifting freemsg.induct)+ −
+ −
lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:+ −
assumes N: "\<And>N. P (Nonce N)"+ −
and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"+ −
and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"+ −
and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"+ −
shows "P msg"+ −
using N M C D by (blast intro: msg_induct_aux)+ −
+ −
subsection{*The Abstract Discriminator*}+ −
+ −
text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't+ −
need this function in order to prove discrimination theorems.*}+ −
+ −
quotient_def+ −
discrim :: "discrim:: msg \<Rightarrow> int"+ −
where+ −
"freediscrim"+ −
+ −
text{*Now prove the four equations for @{term discrim}*}+ −
+ −
lemma [quot_respect]:+ −
shows "(op \<sim> ===> op =) freediscrim freediscrim"+ −
by (auto simp add: msgrel_imp_eq_freediscrim)+ −
+ −
lemma discrim_Nonce [simp]: + −
shows "discrim (Nonce N) = 0"+ −
by (lifting freediscrim.simps(1))+ −
+ −
lemma discrim_MPair [simp]: + −
shows "discrim (MPair X Y) = 1"+ −
by (lifting freediscrim.simps(2))+ −
+ −
lemma discrim_Crypt [simp]: + −
shows "discrim (Crypt K X) = discrim X + 2"+ −
by (lifting freediscrim.simps(3))+ −
+ −
lemma discrim_Decrypt [simp]: + −
shows "discrim (Decrypt K X) = discrim X - 2"+ −
by (lifting freediscrim.simps(4))+ −
+ −
end+ −
+ −