1 theory Larry

     2 imports Main "../QuotMain"

     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 text{*Proving that it is an equivalence relation*}

    26 

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

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

    29 

    30 theorem equiv_msgrel: "equivp msgrel"

    31 proof (rule equivpI)

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

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

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

    35 qed

    36 

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

    38 

    39 subsubsection{*The Set of Nonces*}

    40 

    41 primrec

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

    43 where

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

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

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

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

    48 

    49 theorem msgrel_imp_eq_freenonces: 

    50   "U \<sim> V \<Longrightarrow> freenonces U = freenonces V"

    51 by (erule msgrel.induct, auto) 

    52 

    53 subsubsection{*The Left Projection*}

    54 

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

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

    57 fun

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

    59 where

    60   "freeleft (NONCE N) = NONCE N"

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

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

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

    64 

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

    66 equivalence relation.  It also helps us prove that MPair

    67   (the abstract constructor) is injective*}

    68 lemma msgrel_imp_eqv_freeleft_aux:

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

    70 apply(induct rule: freeleft.induct)

    71 apply(auto intro: msgrel.intros)

    72 done

    73 

    74 theorem msgrel_imp_eqv_freeleft:

    75   "U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"

    76 apply(erule msgrel.induct)

    77 apply(auto intro: msgrel.intros msgrel_imp_eqv_freeleft_aux)

    78 done

    79 

    80 subsubsection{*The Right Projection*}

    81 

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

    83 fun

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

    85 where

    86   "freeright (NONCE N) = NONCE N"

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

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

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

    90 

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

    92 equivalence relation.  It also helps us prove that MPair

    93   (the abstract constructor) is injective*}

    94 lemma msgrel_imp_eqv_freeright_aux:

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

    96 apply(induct rule: freeright.induct)

    97 apply(auto intro: msgrel.intros)

    98 done

    99 

   100 theorem msgrel_imp_eqv_freeright:

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

   102 by (erule msgrel.induct, auto intro: msgrel.intros msgrel_imp_eqv_freeright_aux)

   103 

   104 subsubsection{*The Discriminator for Constructors*}

   105 

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

   107 fun 

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

   109 where

   110    "freediscrim (NONCE N) = 0"

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

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

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

   114 

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

   116 theorem msgrel_imp_eq_freediscrim:

   117      "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"

   118 by (erule msgrel.induct, auto)

   119 

   120 

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

   122 

   123 quotient  msg = freemsg / msgrel

   124   by (rule equiv_msgrel)

   125 

   126 text{*The abstract message constructors*}

   127 

   128 quotient_def

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

   130 where

   131   "NONCE"

   132 

   133 quotient_def

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

   135 where

   136   "MPAIR"

   137 

   138 quotient_def

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

   140 where

   141   "CRYPT"

   142 

   143 quotient_def

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

   145 where

   146   "DECRYPT"

   147 

   148 lemma [quot_respect]:

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

   150 by (auto intro: CRYPT)

   151 

   152 lemma [quot_respect]:

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

   154 by (auto intro: DECRYPT)

   155 

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

   157 theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"

   158 by (lifting CD)

   159 

   160 theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"

   161 by (lifting DC)

   162 

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

   164 

   165 quotient_def

   166   nonces :: "nounces:: msg \<Rightarrow> nat set"

   167 where

   168   "freenonces"

   169 

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

   171 

   172 lemma [quot_respect]:

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

   174 by (simp add: msgrel_imp_eq_freenonces)

   175 

   176 lemma [quot_respect]:

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

   178 by (simp add: NONCE)

   179 

   180 lemma nonces_Nonce [simp]: 

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

   182 by (lifting freenonces.simps(1))

   183  

   184 lemma [quot_respect]:

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

   186 by (simp add: MPAIR)

   187 

   188 lemma nonces_MPair [simp]: 

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

   190 by (lifting freenonces.simps(2))

   191 

   192 lemma nonces_Crypt [simp]: 

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

   194 by (lifting freenonces.simps(3))

   195 

   196 lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"

   197 by (lifting freenonces.simps(4))

   198 

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

   200 

   201 quotient_def

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

   203 where

   204   "freeleft"

   205 

   206 lemma [quot_respect]:

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

   208 by (simp add: msgrel_imp_eqv_freeleft)

   209 

   210 lemma left_Nonce [simp]: 

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

   212 by (lifting freeleft.simps(1))

   213 

   214 lemma left_MPair [simp]: 

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

   216 by (lifting freeleft.simps(2))

   217 

   218 lemma left_Crypt [simp]: 

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

   220 by (lifting freeleft.simps(3))

   221 

   222 lemma left_Decrypt [simp]: 

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

   224 by (lifting freeleft.simps(4))

   225 

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

   227 

   228 quotient_def

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

   230 where

   231   "freeright"

   232 

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

   234 

   235 lemma [quot_respect]:

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

   237 by (simp add: msgrel_imp_eqv_freeright)

   238 

   239 lemma right_Nonce [simp]: 

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

   241 by (lifting freeright.simps(1))

   242 

   243 lemma right_MPair [simp]: 

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

   245 by (lifting freeright.simps(2))

   246 

   247 lemma right_Crypt [simp]: 

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

   249 by (lifting freeright.simps(3))

   250 

   251 lemma right_Decrypt [simp]: 

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

   253 by (lifting freeright.simps(4))

   254 

   255 subsection{*Injectivity Properties of Some Constructors*}

   256 

   257 lemma NONCE_imp_eq: 

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

   259 by (drule msgrel_imp_eq_freenonces, simp)

   260 

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

   262 lemma Nonce_Nonce_eq [iff]: 

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

   264 apply(rule iffI)

   265 apply(lifting NONCE_imp_eq)

   266 apply(simp)

   267 done

   268 

   269 lemma MPAIR_imp_eqv_left: 

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

   271 by (drule msgrel_imp_eqv_freeleft, simp)

   272 

   273 lemma MPair_imp_eq_left: 

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

   275   shows "X = X'"

   276 using eq by (lifting MPAIR_imp_eqv_left)

   277 

   278 lemma MPAIR_imp_eqv_right: 

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

   280 by (drule msgrel_imp_eqv_freeright, simp)

   281 

   282 lemma MPair_imp_eq_right: 

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

   284 by (lifting  MPAIR_imp_eqv_right)

   285 

   286 theorem MPair_MPair_eq [iff]: 

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

   288 by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)

   289 

   290 lemma NONCE_neqv_MPAIR: 

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

   292 by (auto dest: msgrel_imp_eq_freediscrim)

   293 

   294 theorem Nonce_neq_MPair [iff]: 

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

   296 by (lifting NONCE_neqv_MPAIR)

   297 

   298 text{*Example suggested by a referee*}

   299 

   300 lemma CRYPT_NONCE_neq_NONCE:

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

   302 by (auto dest: msgrel_imp_eq_freediscrim)

   303 

   304 theorem Crypt_Nonce_neq_Nonce: 

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

   306 by (lifting CRYPT_NONCE_neq_NONCE)

   307 

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

   309 lemma CRYPT2_NONCE_neq_NONCE: 

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

   311 by (auto dest: msgrel_imp_eq_freediscrim)  

   312 

   313 theorem Crypt2_Nonce_neq_Nonce: 

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

   315 by (lifting CRYPT2_NONCE_neq_NONCE) 

   316 

   317 theorem Crypt_Crypt_eq [iff]: 

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

   319 proof

   320   assume "Crypt K X = Crypt K X'"

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

   322   thus "X = X'" by simp

   323 next

   324   assume "X = X'"

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

   326 qed

   327 

   328 theorem Decrypt_Decrypt_eq [iff]: 

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

   330 proof

   331   assume "Decrypt K X = Decrypt K X'"

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

   333   thus "X = X'" by simp

   334 next

   335   assume "X = X'"

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

   337 qed

   338 

   339 lemma msg_induct_aux:

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

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

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

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

   344 by (lifting freemsg.induct)

   345 

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

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

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

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

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

   351   shows "P msg"

   352 using N M C D by (blast intro:  msg_induct_aux)

   353 

   354 subsection{*The Abstract Discriminator*}

   355 

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

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

   358 

   359 quotient_def

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

   361 where

   362   "freediscrim"

   363 

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

   365 

   366 lemma [quot_respect]:

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

   368 by (auto simp add: msgrel_imp_eq_freediscrim)

   369 

   370 lemma discrim_Nonce [simp]: 

   371   shows "discrim (Nonce N) = 0"

   372 by (lifting freediscrim.simps(1))

   373 

   374 lemma discrim_MPair [simp]: 

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

   376 by (lifting freediscrim.simps(2))

   377 

   378 lemma discrim_Crypt [simp]: 

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

   380 by (lifting freediscrim.simps(3))

   381 

   382 lemma discrim_Decrypt [simp]: 

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

   384 by (lifting freediscrim.simps(4))

   385 

   386 end

   387