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

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

   124 

   125 quotient  msg = freemsg / msgrel

   126   by (rule equiv_msgrel)

   127 

   128 text{*The abstract message constructors*}

   129 

   130 quotient_def

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

   132 where

   133   "NONCE"

   134 

   135 quotient_def

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

   137 where

   138   "MPAIR"

   139 

   140 quotient_def

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

   142 where

   143   "CRYPT"

   144 

   145 quotient_def

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

   147 where

   148   "DECRYPT"

   149 

   150 lemma [quot_respect]:

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

   152 by (auto intro: CRYPT)

   153 

   154 lemma [quot_respect]:

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

   156 by (auto intro: DECRYPT)

   157 

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

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

   160 by (lifting CD)

   161 

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

   163 by (lifting DC)

   164 

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

   166 

   167 quotient_def

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

   169 where

   170   "freenonces"

   171 

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

   173 

   174 lemma [quot_respect]:

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

   176 by (simp add: msgrel_imp_eq_freenonces)

   177 

   178 lemma [quot_respect]:

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

   180 by (simp add: NONCE)

   181 

   182 lemma nonces_Nonce [simp]: 

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

   184 by (lifting freenonces.simps(1))

   185  

   186 lemma [quot_respect]:

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

   188 by (simp add: MPAIR)

   189 

   190 lemma nonces_MPair [simp]: 

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

   192 by (lifting freenonces.simps(2))

   193 

   194 lemma nonces_Crypt [simp]: 

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

   196 by (lifting freenonces.simps(3))

   197 

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

   199 by (lifting freenonces.simps(4))

   200 

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

   202 

   203 quotient_def

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

   205 where

   206   "freeleft"

   207 

   208 lemma [quot_respect]:

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

   210 by (simp add: msgrel_imp_eqv_freeleft)

   211 

   212 lemma left_Nonce [simp]: 

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

   214 by (lifting freeleft.simps(1))

   215 

   216 lemma left_MPair [simp]: 

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

   218 by (lifting freeleft.simps(2))

   219 

   220 lemma left_Crypt [simp]: 

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

   222 by (lifting freeleft.simps(3))

   223 

   224 lemma left_Decrypt [simp]: 

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

   226 by (lifting freeleft.simps(4))

   227 

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

   229 

   230 quotient_def

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

   232 where

   233   "freeright"

   234 

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

   236 

   237 lemma [quot_respect]:

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

   239 by (simp add: msgrel_imp_eqv_freeright)

   240 

   241 lemma right_Nonce [simp]: 

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

   243 by (lifting freeright.simps(1))

   244 

   245 lemma right_MPair [simp]: 

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

   247 by (lifting freeright.simps(2))

   248 

   249 lemma right_Crypt [simp]: 

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

   251 by (lifting freeright.simps(3))

   252 

   253 lemma right_Decrypt [simp]: 

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

   255 by (lifting freeright.simps(4))

   256 

   257 subsection{*Injectivity Properties of Some Constructors*}

   258 

   259 lemma NONCE_imp_eq: 

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

   261 by (drule msgrel_imp_eq_freenonces, simp)

   262 

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

   264 lemma Nonce_Nonce_eq [iff]: 

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

   266 proof

   267   assume "Nonce m = Nonce n"

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

   269 next

   270   assume "m = n" 

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

   272 qed

   273 

   274 lemma MPAIR_imp_eqv_left: 

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

   276 by (drule msgrel_imp_eqv_freeleft) (simp)

   277 

   278 lemma MPair_imp_eq_left: 

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

   280   shows "X = X'"

   281 using eq by (lifting MPAIR_imp_eqv_left)

   282 

   283 lemma MPAIR_imp_eqv_right: 

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

   285 by (drule msgrel_imp_eqv_freeright) (simp)

   286 

   287 lemma MPair_imp_eq_right: 

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

   289 by (lifting  MPAIR_imp_eqv_right)

   290 

   291 theorem MPair_MPair_eq [iff]: 

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

   293 by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)

   294 

   295 lemma NONCE_neqv_MPAIR: 

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

   297 by (auto dest: msgrel_imp_eq_freediscrim)

   298 

   299 theorem Nonce_neq_MPair [iff]: 

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

   301 by (lifting NONCE_neqv_MPAIR)

   302 

   303 text{*Example suggested by a referee*}

   304 

   305 lemma CRYPT_NONCE_neq_NONCE:

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

   307 by (auto dest: msgrel_imp_eq_freediscrim)

   308 

   309 theorem Crypt_Nonce_neq_Nonce: 

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

   311 by (lifting CRYPT_NONCE_neq_NONCE)

   312 

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

   314 lemma CRYPT2_NONCE_neq_NONCE: 

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

   316 by (auto dest: msgrel_imp_eq_freediscrim)  

   317 

   318 theorem Crypt2_Nonce_neq_Nonce: 

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

   320 by (lifting CRYPT2_NONCE_neq_NONCE) 

   321 

   322 theorem Crypt_Crypt_eq [iff]: 

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

   324 proof

   325   assume "Crypt K X = Crypt K X'"

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

   327   thus "X = X'" by simp

   328 next

   329   assume "X = X'"

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

   331 qed

   332 

   333 theorem Decrypt_Decrypt_eq [iff]: 

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

   335 proof

   336   assume "Decrypt K X = Decrypt K X'"

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

   338   thus "X = X'" by simp

   339 next

   340   assume "X = X'"

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

   342 qed

   343 

   344 lemma msg_induct_aux:

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

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

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

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

   349 by (lifting freemsg.induct)

   350 

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

   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)"

   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)"

   356   shows "P msg"

   357 using N M C D by (rule msg_induct_aux)

   358 

   359 subsection{*The Abstract Discriminator*}

   360 

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

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

   363 

   364 quotient_def

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

   366 where

   367   "freediscrim"

   368 

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

   370 

   371 lemma [quot_respect]:

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

   373 by (auto simp add: msgrel_imp_eq_freediscrim)

   374 

   375 lemma discrim_Nonce [simp]: 

   376   shows "discrim (Nonce N) = 0"

   377 by (lifting freediscrim.simps(1))

   378 

   379 lemma discrim_MPair [simp]: 

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

   381 by (lifting freediscrim.simps(2))

   382 

   383 lemma discrim_Crypt [simp]: 

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

   385 by (lifting freediscrim.simps(3))

   386 

   387 lemma discrim_Decrypt [simp]: 

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

   389 by (lifting freediscrim.simps(4))

   390 

   391 end

   392