1 theory LarryDatatype

     2 imports Main "../Quotient" "../Quotient_Syntax"

     3 begin

     4 

     5 subsection{*Defining the Free Algebra*}

     6 

     7 datatype

     8   freemsg = NONCE  nat

     9         | MPAIR  freemsg freemsg

    10         | CRYPT  nat freemsg  

    11         | DECRYPT  nat freemsg

    12 

    13 inductive 

    14   msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)

    15 where 

    16   CD:    "CRYPT K (DECRYPT K X) \<sim> X"

    17 | DC:    "DECRYPT K (CRYPT K X) \<sim> X"

    18 | NONCE: "NONCE N \<sim> NONCE N"

    19 | MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"

    20 | CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"

    21 | DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"

    22 | SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"

    23 | TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"

    24 

    25 lemmas msgrel.intros[intro]

    26 

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

    28 

    29 lemma msgrel_refl: "X \<sim> X"

    30 by (induct X, (blast intro: msgrel.intros)+)

    31 

    32 theorem equiv_msgrel: "equivp msgrel"

    33 proof (rule equivpI)

    34   show "reflp msgrel" by (simp add: reflp_def msgrel_refl)

    35   show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)

    36   show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)

    37 qed

    38 

    39 subsection{*Some Functions on the Free Algebra*}

    40 

    41 subsubsection{*The Set of Nonces*}

    42 

    43 fun

    44   freenonces :: "freemsg \<Rightarrow> nat set"

    45 where

    46   "freenonces (NONCE N) = {N}"

    47 | "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"

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

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

    50 

    51 theorem msgrel_imp_eq_freenonces: 

    52   assumes a: "U \<sim> V"

    53   shows "freenonces U = freenonces V"

    54   using a by (induct) (auto) 

    55 

    56 subsubsection{*The Left Projection*}

    57 

    58 text{*A function to return the left part of the top pair in a message.  It will

    59 be lifted to the initial algrebra, to serve as an example of that process.*}

    60 fun

    61   freeleft :: "freemsg \<Rightarrow> freemsg"

    62 where

    63   "freeleft (NONCE N) = NONCE N"

    64 | "freeleft (MPAIR X Y) = X"

    65 | "freeleft (CRYPT K X) = freeleft X"

    66 | "freeleft (DECRYPT K X) = freeleft X"

    67 

    68 text{*This theorem lets us prove that the left function respects the

    69 equivalence relation.  It also helps us prove that MPair

    70   (the abstract constructor) is injective*}

    71 lemma msgrel_imp_eqv_freeleft_aux:

    72   shows "freeleft U \<sim> freeleft U"

    73   by (induct rule: freeleft.induct) (auto)

    74 

    75 theorem msgrel_imp_eqv_freeleft:

    76   assumes a: "U \<sim> V" 

    77   shows "freeleft U \<sim> freeleft V"

    78   using a

    79   by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)

    80 

    81 subsubsection{*The Right Projection*}

    82 

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

    84 fun

    85   freeright :: "freemsg \<Rightarrow> freemsg"

    86 where

    87   "freeright (NONCE N) = NONCE N"

    88 | "freeright (MPAIR X Y) = Y"

    89 | "freeright (CRYPT K X) = freeright X"

    90 | "freeright (DECRYPT K X) = freeright X"

    91 

    92 text{*This theorem lets us prove that the right function respects the

    93 equivalence relation.  It also helps us prove that MPair

    94   (the abstract constructor) is injective*}

    95 lemma msgrel_imp_eqv_freeright_aux:

    96   shows "freeright U \<sim> freeright U"

    97   by (induct rule: freeright.induct) (auto)

    98 

    99 theorem msgrel_imp_eqv_freeright:

   100   assumes a: "U \<sim> V" 

   101   shows "freeright U \<sim> freeright V"

   102   using a

   103   by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)

   104 

   105 subsubsection{*The Discriminator for Constructors*}

   106 

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

   108 fun 

   109   freediscrim :: "freemsg \<Rightarrow> int"

   110 where

   111    "freediscrim (NONCE N) = 0"

   112  | "freediscrim (MPAIR X Y) = 1"

   113  | "freediscrim (CRYPT K X) = freediscrim X + 2"

   114  | "freediscrim (DECRYPT K X) = freediscrim X - 2"

   115 

   116 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}

   117 theorem msgrel_imp_eq_freediscrim:

   118   assumes a: "U \<sim> V"

   119   shows "freediscrim U = freediscrim V"

   120   using a by (induct) (auto)

   121 

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

   123 

   124 quotient_type msg = freemsg / msgrel

   125   by (rule equiv_msgrel)

   126 

   127 text{*The abstract message constructors*}

   128 

   129 quotient_definition

   130   "Nonce :: nat \<Rightarrow> msg"

   131 is

   132   "NONCE"

   133 

   134 quotient_definition

   135   "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"

   136 is

   137   "MPAIR"

   138 

   139 quotient_definition

   140   "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"

   141 is

   142   "CRYPT"

   143 

   144 quotient_definition

   145   "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"

   146 is

   147   "DECRYPT"

   148 

   149 lemma [quot_respect]:

   150   shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"

   151 by (auto intro: CRYPT)

   152 

   153 lemma [quot_respect]:

   154   shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"

   155 by (auto intro: DECRYPT)

   156 

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

   158 theorem CD_eq [simp]: 

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

   160   by (lifting CD)

   161 

   162 theorem DC_eq [simp]: 

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

   164   by (lifting DC)

   165 

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

   167 

   168 quotient_definition

   169    "nonces:: msg \<Rightarrow> nat set"

   170 is

   171   "freenonces"

   172 

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

   174 

   175 lemma [quot_respect]:

   176   shows "(op \<sim> ===> op =) freenonces freenonces"

   177   by (simp add: msgrel_imp_eq_freenonces)

   178 

   179 lemma [quot_respect]:

   180   shows "(op = ===> op \<sim>) NONCE NONCE"

   181   by (simp add: NONCE)

   182 

   183 lemma nonces_Nonce [simp]: 

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

   185   by (lifting freenonces.simps(1))

   186  

   187 lemma [quot_respect]:

   188   shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"

   189   by (simp add: MPAIR)

   190 

   191 lemma nonces_MPair [simp]: 

   192   shows "nonces (MPair X Y) = nonces X \<union> nonces Y"

   193   by (lifting freenonces.simps(2))

   194 

   195 lemma nonces_Crypt [simp]: 

   196   shows "nonces (Crypt K X) = nonces X"

   197   by (lifting freenonces.simps(3))

   198 

   199 lemma nonces_Decrypt [simp]: 

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

   201   by (lifting freenonces.simps(4))

   202 

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

   204 

   205 quotient_definition

   206   "left:: msg \<Rightarrow> msg"

   207 is

   208   "freeleft"

   209 

   210 lemma [quot_respect]:

   211   shows "(op \<sim> ===> op \<sim>) freeleft freeleft"

   212   by (simp add: msgrel_imp_eqv_freeleft)

   213 

   214 lemma left_Nonce [simp]: 

   215   shows "left (Nonce N) = Nonce N"

   216   by (lifting freeleft.simps(1))

   217 

   218 lemma left_MPair [simp]: 

   219   shows "left (MPair X Y) = X"

   220   by (lifting freeleft.simps(2))

   221 

   222 lemma left_Crypt [simp]: 

   223   shows "left (Crypt K X) = left X"

   224   by (lifting freeleft.simps(3))

   225 

   226 lemma left_Decrypt [simp]: 

   227   shows "left (Decrypt K X) = left X"

   228   by (lifting freeleft.simps(4))

   229 

   230 subsection{*The Abstract Function to Return the Right Part*}

   231 

   232 quotient_definition

   233   "right:: msg \<Rightarrow> msg"

   234 is

   235   "freeright"

   236 

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

   238 

   239 lemma [quot_respect]:

   240   shows "(op \<sim> ===> op \<sim>) freeright freeright"

   241   by (simp add: msgrel_imp_eqv_freeright)

   242 

   243 lemma right_Nonce [simp]: 

   244   shows "right (Nonce N) = Nonce N"

   245   by (lifting freeright.simps(1))

   246 

   247 lemma right_MPair [simp]: 

   248   shows "right (MPair X Y) = Y"

   249   by (lifting freeright.simps(2))

   250 

   251 lemma right_Crypt [simp]: 

   252   shows "right (Crypt K X) = right X"

   253   by (lifting freeright.simps(3))

   254 

   255 lemma right_Decrypt [simp]: 

   256   shows "right (Decrypt K X) = right X"

   257   by (lifting freeright.simps(4))

   258 

   259 subsection{*Injectivity Properties of Some Constructors*}

   260 

   261 lemma NONCE_imp_eq: 

   262   shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"

   263   by (drule msgrel_imp_eq_freenonces, simp)

   264 

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

   266 lemma Nonce_Nonce_eq [iff]: 

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

   268 proof

   269   assume "Nonce m = Nonce n"

   270   then show "m = n" by (lifting NONCE_imp_eq)

   271 next

   272   assume "m = n" 

   273   then show "Nonce m = Nonce n" by simp

   274 qed

   275 

   276 lemma MPAIR_imp_eqv_left: 

   277   shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"

   278   by (drule msgrel_imp_eqv_freeleft) (simp)

   279 

   280 lemma MPair_imp_eq_left: 

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

   282   shows "X = X'"

   283   using eq by (lifting MPAIR_imp_eqv_left)

   284 

   285 lemma MPAIR_imp_eqv_right: 

   286   shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"

   287   by (drule msgrel_imp_eqv_freeright) (simp)

   288 

   289 lemma MPair_imp_eq_right: 

   290   shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"

   291   by (lifting  MPAIR_imp_eqv_right)

   292 

   293 theorem MPair_MPair_eq [iff]: 

   294   shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" 

   295   by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)

   296 

   297 lemma NONCE_neqv_MPAIR: 

   298   shows "\<not>(NONCE m \<sim> MPAIR X Y)"

   299   by (auto dest: msgrel_imp_eq_freediscrim)

   300 

   301 theorem Nonce_neq_MPair [iff]: 

   302   shows "Nonce N \<noteq> MPair X Y"

   303   by (lifting NONCE_neqv_MPAIR)

   304 

   305 text{*Example suggested by a referee*}

   306 

   307 lemma CRYPT_NONCE_neq_NONCE:

   308   shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"

   309   by (auto dest: msgrel_imp_eq_freediscrim)

   310 

   311 theorem Crypt_Nonce_neq_Nonce: 

   312   shows "Crypt K (Nonce M) \<noteq> Nonce N"

   313   by (lifting CRYPT_NONCE_neq_NONCE)

   314 

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

   316 lemma CRYPT2_NONCE_neq_NONCE: 

   317   shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"

   318   by (auto dest: msgrel_imp_eq_freediscrim)  

   319 

   320 theorem Crypt2_Nonce_neq_Nonce: 

   321   shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"

   322   by (lifting CRYPT2_NONCE_neq_NONCE) 

   323 

   324 theorem Crypt_Crypt_eq [iff]: 

   325   shows "(Crypt K X = Crypt K X') = (X=X')" 

   326 proof

   327   assume "Crypt K X = Crypt K X'"

   328   hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp

   329   thus "X = X'" by simp

   330 next

   331   assume "X = X'"

   332   thus "Crypt K X = Crypt K X'" by simp

   333 qed

   334 

   335 theorem Decrypt_Decrypt_eq [iff]: 

   336   shows "(Decrypt K X = Decrypt K X') = (X=X')" 

   337 proof

   338   assume "Decrypt K X = Decrypt K X'"

   339   hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp

   340   thus "X = X'" by simp

   341 next

   342   assume "X = X'"

   343   thus "Decrypt K X = Decrypt K X'" by simp

   344 qed

   345 

   346 lemma msg_induct_aux:

   347   shows "\<lbrakk>\<And>N. P (Nonce N);

   348           \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);

   349           \<And>K X. P X \<Longrightarrow> P (Crypt K X);

   350           \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"

   351   by (lifting freemsg.induct)

   352 

   353 lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:

   354   assumes N: "\<And>N. P (Nonce N)"

   355       and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"

   356       and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"

   357       and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"

   358   shows "P msg"

   359   using N M C D by (rule msg_induct_aux)

   360 

   361 subsection{*The Abstract Discriminator*}

   362 

   363 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't

   364 need this function in order to prove discrimination theorems.*}

   365 

   366 quotient_definition

   367   "discrim:: msg \<Rightarrow> int"

   368 is

   369   "freediscrim"

   370 

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

   372 

   373 lemma [quot_respect]:

   374   shows "(op \<sim> ===> op =) freediscrim freediscrim"

   375   by (auto simp add: msgrel_imp_eq_freediscrim)

   376 

   377 lemma discrim_Nonce [simp]: 

   378   shows "discrim (Nonce N) = 0"

   379   by (lifting freediscrim.simps(1))

   380 

   381 lemma discrim_MPair [simp]: 

   382   shows "discrim (MPair X Y) = 1"

   383   by (lifting freediscrim.simps(2))

   384 

   385 lemma discrim_Crypt [simp]: 

   386   shows "discrim (Crypt K X) = discrim X + 2"

   387   by (lifting freediscrim.simps(3))

   388 

   389 lemma discrim_Decrypt [simp]: 

   390   shows "discrim (Decrypt K X) = discrim X - 2"

   391   by (lifting freediscrim.simps(4))

   392 

   393 end

   394