(* Title: HOL/Quotient_Examples/Quotient_Message.thy

Author: Christian Urban

Message datatype, based on an older version by Larry Paulson.

*)

theory Quotient_Message

imports Main "~~/src/HOL/Library/Quotient_Syntax"

begin

subsection{*Defining the Free Algebra*}

datatype

freemsg = NONCE nat

| MPAIR freemsg freemsg

| CRYPT nat freemsg

| DECRYPT nat freemsg

inductive

msgrel::"freemsg => freemsg => bool" (infixl "∼" 50)

where

CD: "CRYPT K (DECRYPT K X) ∼ X"

| DC: "DECRYPT K (CRYPT K X) ∼ X"

| NONCE: "NONCE N ∼ NONCE N"

| MPAIR: "[|X ∼ X'; Y ∼ Y'|] ==> MPAIR X Y ∼ MPAIR X' Y'"

| CRYPT: "X ∼ X' ==> CRYPT K X ∼ CRYPT K X'"

| DECRYPT: "X ∼ X' ==> DECRYPT K X ∼ DECRYPT K X'"

| SYM: "X ∼ Y ==> Y ∼ X"

| TRANS: "[|X ∼ Y; Y ∼ Z|] ==> X ∼ Z"

lemmas msgrel.intros[intro]

text{*Proving that it is an equivalence relation*}

lemma msgrel_refl: "X ∼ X"

by (induct X) (auto intro: msgrel.intros)

theorem equiv_msgrel: "equivp msgrel"

proof (rule equivpI)

show "reflp msgrel" by (rule reflpI) (simp add: msgrel_refl)

show "symp msgrel" by (rule sympI) (blast intro: msgrel.SYM)

show "transp msgrel" by (rule transpI) (blast intro: msgrel.TRANS)

qed

subsection{*Some Functions on the Free Algebra*}

subsubsection{*The Set of Nonces*}

primrec

freenonces :: "freemsg => nat set"

where

"freenonces (NONCE N) = {N}"

| "freenonces (MPAIR X Y) = freenonces X ∪ freenonces Y"

| "freenonces (CRYPT K X) = freenonces X"

| "freenonces (DECRYPT K X) = freenonces X"

theorem msgrel_imp_eq_freenonces:

assumes a: "U ∼ V"

shows "freenonces U = freenonces V"

using a by (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.*}

primrec

freeleft :: "freemsg => 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 ∼ freeleft U"

by (fact msgrel_refl)

theorem msgrel_imp_eqv_freeleft:

assumes a: "U ∼ V"

shows "freeleft U ∼ freeleft V"

using a

by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)

subsubsection{*The Right Projection*}

text{*A function to return the right part of the top pair in a message.*}

primrec

freeright :: "freemsg => 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 ∼ freeright U"

by (fact msgrel_refl)

theorem msgrel_imp_eqv_freeright:

assumes a: "U ∼ V"

shows "freeright U ∼ freeright V"

using a

by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)

subsubsection{*The Discriminator for Constructors*}

text{*A function to distinguish nonces, mpairs and encryptions*}

primrec

freediscrim :: "freemsg => 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 ≠ MPair X Y"}*}

theorem msgrel_imp_eq_freediscrim:

assumes a: "U ∼ V"

shows "freediscrim U = freediscrim V"

using a by (induct) (auto)

subsection{*The Initial Algebra: A Quotiented Message Type*}

quotient_type msg = freemsg / msgrel

by (rule equiv_msgrel)

text{*The abstract message constructors*}

quotient_definition

"Nonce :: nat => msg"

is

"NONCE"

done

quotient_definition

"MPair :: msg => msg => msg"

is

"MPAIR"

by (rule MPAIR)

quotient_definition

"Crypt :: nat => msg => msg"

is

"CRYPT"

by (rule CRYPT)

quotient_definition

"Decrypt :: nat => msg => msg"

is

"DECRYPT"

by (rule DECRYPT)

text{*Establishing these two equations is the point of the whole exercise*}

theorem CD_eq [simp]:

shows "Crypt K (Decrypt K X) = X"

by (lifting CD)

theorem DC_eq [simp]:

shows "Decrypt K (Crypt K X) = X"

by (lifting DC)

subsection{*The Abstract Function to Return the Set of Nonces*}

quotient_definition

"nonces:: msg => nat set"

is

"freenonces"

by (rule msgrel_imp_eq_freenonces)

text{*Now prove the four equations for @{term nonces}*}

lemma nonces_Nonce [simp]:

shows "nonces (Nonce N) = {N}"

by (lifting freenonces.simps(1))

lemma nonces_MPair [simp]:

shows "nonces (MPair X Y) = nonces X ∪ 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]:

shows "nonces (Decrypt K X) = nonces X"

by (lifting freenonces.simps(4))

subsection{*The Abstract Function to Return the Left Part*}

quotient_definition

"left:: msg => msg"

is

"freeleft"

by (rule 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_definition

"right:: msg => msg"

is

"freeright"

by (rule msgrel_imp_eqv_freeright)

text{*Now prove the four equations for @{term right}*}

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*}

text{*Can also be proved using the function @{term nonces}*}

lemma Nonce_Nonce_eq [iff]:

shows "(Nonce m = Nonce n) = (m = n)"

proof

assume "Nonce m = Nonce n"

then show "m = n"

by (descending) (drule msgrel_imp_eq_freenonces, simp)

next

assume "m = n"

then show "Nonce m = Nonce n" by simp

qed

lemma MPair_imp_eq_left:

assumes eq: "MPair X Y = MPair X' Y'"

shows "X = X'"

using eq

by (descending) (drule msgrel_imp_eqv_freeleft, simp)

lemma MPair_imp_eq_right:

shows "MPair X Y = MPair X' Y' ==> Y = Y'"

by (descending) (drule msgrel_imp_eqv_freeright, simp)

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)

theorem Nonce_neq_MPair [iff]:

shows "Nonce N ≠ MPair X Y"

by (descending) (auto dest: msgrel_imp_eq_freediscrim)

text{*Example suggested by a referee*}

theorem Crypt_Nonce_neq_Nonce:

shows "Crypt K (Nonce M) ≠ Nonce N"

by (descending) (auto dest: msgrel_imp_eq_freediscrim)

text{*...and many similar results*}

theorem Crypt2_Nonce_neq_Nonce:

shows "Crypt K (Crypt K' (Nonce M)) ≠ Nonce N"

by (descending) (auto dest: msgrel_imp_eq_freediscrim)

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 [case_names Nonce MPair Crypt Decrypt, cases type: msg]:

assumes N: "!!N. P (Nonce N)"

and M: "!!X Y. [|P X; P Y|] ==> P (MPair X Y)"

and C: "!!K X. P X ==> P (Crypt K X)"

and D: "!!K X. P X ==> P (Decrypt K X)"

shows "P msg"

using N M C D

by (descending) (auto intro: freemsg.induct)

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_definition

"discrim:: msg => int"

is

"freediscrim"

by (rule msgrel_imp_eq_freediscrim)

text{*Now prove the four equations for @{term discrim}*}

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