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