1open HolKernel Parse boolLib; 2 3(* ------------------------------------------------------------------------ *) 4(* Representing cryptographic messages as a new datatype in the HOL logic. *) 5(* *) 6(* This is a representation in HOL using Homeier's quotient package of the *) 7(* symmetric-key cryptographic system modeled in Lawrence C. Paulson's *) 8(* paper, "Defining Functions on Equivalence Classes," Computer Laboratory, *) 9(* University of Cambridge, England, 20 April 2004. *) 10(* ------------------------------------------------------------------------ *) 11 12 13val _ = new_theory "msg"; 14val _ = ParseExtras.temp_loose_equality() 15 16 17(* In interactive sessions, do: 18 19app load ["pred_setTheory", 20 "ind_rel", 21 "bossLib", 22 "quotientLib"]; 23 24*) 25 26open pred_setTheory; 27open ind_rel; 28open bossLib; 29 30open quotientLib; 31 32 33val REWRITE_THM = fn th => REWRITE_TAC[th]; 34 35 36(* --------------------------------------------------------------------- *) 37(* Section 5.1, The Concrete Datatype and the Equivalence Relation. *) 38(* --------------------------------------------------------------------- *) 39 40(* --------------------------------------------------------------------- *) 41(* Create datatypes for the free algebra of cryptographic messages. *) 42(* --------------------------------------------------------------------- *) 43 44 45val _ = Hol_datatype 46 47 ` msg1 = Nonce1 of num 48 | Mpair1 of msg1 => msg1 49 | Crypt1 of num => msg1 50 | Decrypt1 of num => msg1 ` ; 51 52(* Notice: no nesting or mutual recursion; a simply recursive type. *) 53 54 55val msg1_distinct = theorem "msg1_distinct"; 56val msg1_one_one = theorem "msg1_11"; 57val msg1_cases = theorem "msg1_nchotomy"; 58val msg1_case_cong = theorem "msg1_case_cong"; 59 60val msg1_induction = theorem "msg1_induction"; 61val msg1_Axiom = theorem "msg1_Axiom"; 62 63val msg1_distinct2 = save_thm("msg1_distinct2", 64 CONJ msg1_distinct (GSYM msg1_distinct)); 65val _ = save_thm("msg1_one_one", msg1_one_one); 66val _ = save_thm("msg1_cases", msg1_cases); 67 68 69 70(* --------------------------------------------------------------------- *) 71(* Definition of equivalence between cryptographic messges. *) 72(* This uses Myra VanInwegen's mutually recursive rule induction pkg. *) 73(* --------------------------------------------------------------------- *) 74 75val msgrel = 76���msgrel : msg1 -> msg1 -> bool���; 77 78val msgrel_patterns = [���^msgrel X Y���]; 79 80val msgrel_rules_tm = 81��� 82 83 (* -------------------------------------------- *) 84 (^msgrel (Crypt1 k (Decrypt1 k X)) X) /\ 85 86 87 (* -------------------------------------------- *) 88 (^msgrel (Decrypt1 k (Crypt1 k X)) X) /\ 89 90 91 (* -------------------------------------------- *) 92 (^msgrel (Nonce1 N) (Nonce1 N)) /\ 93 94 95 ((^msgrel X X') /\ (^msgrel Y Y') 96 (* -------------------------------------------- *) ==> 97 (^msgrel (Mpair1 X Y) (Mpair1 X' Y'))) /\ 98 99 100 ((^msgrel X X') 101 (* -------------------------------------------- *) ==> 102 (^msgrel (Crypt1 k X) (Crypt1 k X'))) /\ 103 104 105 ((^msgrel X X') 106 (* -------------------------------------------- *) ==> 107 (^msgrel (Decrypt1 k X) (Decrypt1 k X'))) /\ 108 109 110 ((^msgrel X Y) 111 (* -------------------------------------------- *) ==> 112 (^msgrel Y X)) /\ 113 114 115 ((^msgrel X Y) /\ (^msgrel Y Z) 116 (* -------------------------------------------- *) ==> 117 (^msgrel X Z)) 118 119���; 120 121val (msgrel_rules_sat,msgrel_ind_thm) = 122 define_inductive_relations msgrel_patterns msgrel_rules_tm; 123 124val msgrel_inv_thms = prove_inversion_theorems 125 msgrel_rules_sat msgrel_ind_thm; 126 127val msgrel_strong_ind = prove_strong_induction 128 msgrel_rules_sat msgrel_ind_thm; 129 130val _ = save_thm ("msgrel_rules_sat", msgrel_rules_sat); 131val _ = save_thm ("msgrel_ind_thm", msgrel_ind_thm); 132val _ = save_thm ("msgrel_inv_thms", LIST_CONJ msgrel_inv_thms); 133val _ = save_thm ("msgrel_strong_ind", msgrel_strong_ind); 134 135 136val [CD, DC, NONCE, MPAIR, CRYPT, DECRYPT, msgSYM, msgTRANS] 137 = CONJUNCTS msgrel_rules_sat; 138 139 140(* The cryptographic message equivalence relation is reflexive, *) 141(* symmetric and transitive. *) 142 143val msgrel_REFL = store_thm 144 ("msgrel_REFL", 145 ���!X. msgrel X X���, 146 Induct 147 THEN RW_TAC std_ss [msgrel_rules_sat] 148 ); 149 150val msgrel_SYM = store_thm 151 ("msgrel_SYM", 152 ���!X Y. msgrel X Y ==> msgrel Y X���, 153 REWRITE_TAC [msgSYM] 154 ); 155 156val msgrel_TRANS = store_thm 157 ("msgrel_TRANS", 158 ���!X Y Z. msgrel X Y /\ msgrel Y Z ==> msgrel X Z���, 159 PROVE_TAC [msgTRANS] 160 ); 161 162 163 164(* --------------------------------------------------------------------- *) 165(* Section 5.2, Two Functions on the Free Algebra (well, actually 4). *) 166(* --------------------------------------------------------------------- *) 167 168(* --------------------------------------------------------------------- *) 169(* Definition of function to return all nonces from an expression. *) 170(* --------------------------------------------------------------------- *) 171 172val freenonces1_def = Define 173 `(freenonces1 (Nonce1 n) = {n}) /\ 174 (freenonces1 (Mpair1 x y) = freenonces1 x UNION freenonces1 y) /\ 175 (freenonces1 (Crypt1 k x) = freenonces1 x) /\ 176 (freenonces1 (Decrypt1 k x) = freenonces1 x)`; 177 178(* Respectfulness theorem for the freenonces1 function. *) 179 180val freenonces_RSP = store_thm 181 ("freenonces_RSP", 182 ���!V W. msgrel V W ==> (freenonces1 V = freenonces1 W)���, 183 rule_induct msgrel_ind_thm 184 THEN REPEAT STRIP_TAC 185 THEN RW_TAC std_ss [freenonces1_def] 186 ); 187 188 189(* --------------------------------------------------------------------- *) 190(* Definition of left part of the uppermost Mpair1 constructor. *) 191(* --------------------------------------------------------------------- *) 192 193val freeleft1_def = Define 194 `(freeleft1 (Nonce1 n) = Nonce1 n) /\ 195 (freeleft1 (Mpair1 x y) = x) /\ 196 (freeleft1 (Crypt1 k x) = freeleft1 x) /\ 197 (freeleft1 (Decrypt1 k x) = freeleft1 x)`; 198 199(* Respectfulness theorem for the freeleft1 function. *) 200 201val freeleft_RSP = store_thm 202 ("freeleft_RSP", 203 ���!V W. msgrel V W ==> msgrel (freeleft1 V) (freeleft1 W)���, 204 rule_induct msgrel_strong_ind 205 THEN REPEAT STRIP_TAC 206 THEN RW_TAC std_ss[freeleft1_def,msgrel_REFL,msgrel_SYM] 207 THEN IMP_RES_TAC msgrel_TRANS 208 ); 209 210 211(* --------------------------------------------------------------------- *) 212(* Definition of right part of the uppermost Mpair1 constructor. *) 213(* --------------------------------------------------------------------- *) 214 215val freeright1_def = Define 216 `(freeright1 (Nonce1 n) = Nonce1 n) /\ 217 (freeright1 (Mpair1 x y) = y) /\ 218 (freeright1 (Crypt1 k x) = freeright1 x) /\ 219 (freeright1 (Decrypt1 k x) = freeright1 x)`; 220 221(* Respectfulness theorem for the freeright1 function. *) 222 223val freeright_RSP = store_thm 224 ("freeright_RSP", 225 ���!V W. msgrel V W ==> msgrel (freeright1 V) (freeright1 W)���, 226 rule_induct msgrel_strong_ind 227 THEN REPEAT STRIP_TAC 228 THEN RW_TAC std_ss[freeright1_def,msgrel_REFL,msgrel_SYM] 229 THEN IMP_RES_TAC msgrel_TRANS 230 ); 231 232 233(* --------------------------------------------------------------------- *) 234(* Definition of is_nonce, true if the uppermost constructor is Nonce, *) 235(* not Mpair. *) 236(* --------------------------------------------------------------------- *) 237 238val is_nonce1_def = Define 239 `(is_nonce1 (Nonce1 n) = T) /\ 240 (is_nonce1 (Mpair1 x y) = F) /\ 241 (is_nonce1 (Crypt1 k x) = is_nonce1 x) /\ 242 (is_nonce1 (Decrypt1 k x) = is_nonce1 x)`; 243 244(* Respectfulness theorem for the is_nonce1 function. *) 245 246val is_nonce_RSP = store_thm 247 ("is_nonce_RSP", 248 ���!V W. msgrel V W ==> (is_nonce1 V = is_nonce1 W)���, 249 rule_induct msgrel_strong_ind 250 THEN REPEAT STRIP_TAC 251 THEN RW_TAC std_ss[is_nonce1_def] 252 ); 253 254 255 256(* --------------------------------------------------------------------- *) 257(* Section 5.3, The Abstract Message Type and its Constructors. *) 258(* --------------------------------------------------------------------- *) 259 260 261val msgrel_EQUIV = save_thm("msgrel_EQUIV", 262 refl_sym_trans_equiv msgrel_REFL msgrel_SYM msgrel_TRANS); 263 264val equivs = [msgrel_EQUIV]; 265 266val old_thms = 267 [msg1_cases, 268 CD, 269 DC, 270 freenonces1_def, 271 freeleft1_def, 272 freeright1_def, 273 is_nonce1_def, 274 msg1_induction 275 ]; 276 277 278(* ==================================================== *) 279(* LIFT TYPES, CONSTANTS, AND THEOREMS BY QUOTIENTS *) 280(* ==================================================== *) 281 282val _ = quotient.chatting := true; 283fun mk_fn (nm,t) = {def_name=nm^"_def", fname = nm, func = t, fixity = NONE} 284 285val [msg_cases, 286 msgCD, 287 msgDC, 288 nonces_def, 289 left_def, 290 right_def, 291 is_nonce_def, 292 msg_induction 293 ] = 294 define_quotient_types 295 {types = [{name = "msg", equiv = msgrel_EQUIV}], 296 defs = map mk_fn [("Nonce", ``Nonce1``), 297 ("Mpair", ``Mpair1``), 298 ("Crypt", ``Crypt1``), 299 ("Decrypt", ``Decrypt1``), 300 ("nonces", ``freenonces1``), 301 ("left", ``freeleft1``), 302 ("right", ``freeright1``), 303 ("is_nonce", ``is_nonce1``)], 304 tyop_equivs = [], 305 tyop_quotients = [FUN_QUOTIENT], 306 tyop_simps = [FUN_REL_EQ, FUN_MAP_I], 307 respects = [NONCE, MPAIR, CRYPT, DECRYPT, 308 freenonces_RSP, freeleft_RSP, freeright_RSP, is_nonce_RSP], 309 poly_preserves = [FORALL_PRS, EXISTS_PRS], 310 poly_respects = [RES_FORALL_RSP, RES_EXISTS_RSP], 311 old_thms = old_thms}; 312 313 314 315(* ---------------------------------------------------------------- *) 316(* Save the theorems lifted by the quotient operations. *) 317(* ---------------------------------------------------------------- *) 318 319val _ = map save_thm 320 [("msg_cases",msg_cases), 321 ("msgCD",msgCD), 322 ("msgDC",msgDC), 323 ("nonces_def",nonces_def), 324 ("left_def",left_def), 325 ("right_def",right_def), 326 ("is_nonce_def",is_nonce_def), 327 ("msg_induction",msg_induction) 328 ]; 329 330(* Notice the important induction theorem for the lifted msg type: 331 332msg_induction 333 |- !P. 334 (!n. P (Nonce n)) /\ 335 (!m m0. P m /\ P m0 ==> P (Mpair m m0)) /\ 336 (!m. P m ==> !n. P (Crypt n m)) /\ 337 (!m. P m ==> !n. P (Decrypt n m)) ==> 338 !m. P m 339 340This was not lifted by Paulson. It requires higher order quotients 341to lift automatically. 342*) 343 344 345(* ---------------------------------------------------------------- *) 346(* End of saving important theorems from lifting. *) 347(* ---------------------------------------------------------------- *) 348 349 350(* ---------------------------------------------------------------- *) 351(* The rest of these proofs, accomplishing results from Paulson's *) 352(* article, are achieved purely through reasoning at the higher, *) 353(* quotient level (regarding the type "msg", not "msg1"). *) 354(* There is never again any need to deal with concepts at the *) 355(* lower level. That layer may now be completely forgotten. *) 356(* ---------------------------------------------------------------- *) 357 358val Mpair_EQUALS = store_thm 359 ("Mpair_EQUALS", 360 ���!X X' Y Y'. (Mpair X Y = Mpair X' Y') = (X = X') /\ (Y = Y')���, 361 PROVE_TAC[left_def,right_def] 362 ); 363 364val Nonce_EQUALS = store_thm 365 ("Nonce_EQUALS", 366 ���!n n'. (Nonce n = Nonce n') = (n = n')���, 367 REPEAT GEN_TAC 368 THEN EQ_TAC 369 THENL 370 [ DISCH_THEN (MP_TAC o AP_TERM ``nonces``) 371 THEN RW_TAC std_ss [nonces_def,EXTENSION,NOT_IN_EMPTY,IN_INSERT] 372 THEN POP_ASSUM (REWRITE_THM o GSYM), 373 374 DISCH_THEN REWRITE_THM 375 ] 376 ); 377 378val Crypt_EQUALS = store_thm 379 ("Crypt_EQUALS", 380 ���!k X X'. (Crypt k X = Crypt k X') = (X = X')���, 381 PROVE_TAC[msgDC] 382 ); 383 384val Decrypt_EQUALS = store_thm 385 ("Decrypt_EQUALS", 386 ���!k X X'. (Decrypt k X = Decrypt k X') = (X = X')���, 387 PROVE_TAC[msgCD] 388 ); 389 390val Nonce_NOT_EQ_Mpair = store_thm 391 ("Decrypt_NOT_EQ_Mpair", 392 ���!N X Y. ~(Nonce N = Mpair X Y)���, 393 PROVE_TAC[is_nonce_def] 394 ); 395 396(* Here is a proof using the lifted induction theorem for messages: *) 397 398val FINITE_nonces = store_thm 399 ("FINITE_nonces", 400 ���!M. FINITE (nonces M)���, 401 HO_MATCH_MP_TAC msg_induction 402 THEN REWRITE_TAC[nonces_def] 403 THEN REWRITE_TAC[FINITE_INSERT,FINITE_EMPTY,FINITE_UNION] 404 ); 405 406 407 408 409(* ===================================================================== *) 410(* End of the lifting of cryptographic expression types and definitions *) 411(* to the higher, more abstract level where equivalent expressions are *) 412(* actually equal in HOL. *) 413(* ===================================================================== *) 414 415 416 417 418val _ = export_theory(); 419 420val _ = print_theory_to_file "-" "msg.lst"; 421 422val _ = html_theory "msg"; 423 424fun print_theory_size () = 425 (print "The theory "; 426 print (current_theory ()); 427 print " has "; 428 print (Int.toString (length (types (current_theory ())))); 429 print " types, "; 430 print (Int.toString (length (axioms "-"))); 431 print " axioms, "; 432 print (Int.toString (length (definitions "-"))); 433 print " definitions, and "; 434 print (Int.toString (length (theorems "-"))); 435 print " theorems."; 436 print "\n" ); 437 438val _ = print_theory_size(); 439