(**********************************************************************) (* Proofs about sponge function and MITB machine *) (**********************************************************************) (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! WARNING: this file is very messy and could benefit from cleaning up in several ways: - removing unused proofs and redoing unnecessarily complicated ones; - standardising the style of identifiers; - more comments on what is going on and identifying sidetracks. I don't really consider this file suitable for reading by others, but at least it certifies the theorems in the accompanying paper. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*) (* This file should be loaded into HOL4 using "proofs.ml". It would need some work to turn it into a script file that would work with Holmake. *) (* Preamble stuff below for running interactively *) PolyML.print_depth 0; use "/local/scratch-1/mjcg/preface.ml" handle _ => print "/local/scratch-1/mjcg/HOL/preface.ml not loaded\n"; val db = print_apropos; set_trace "Unicode" 0; app load ["rich_listTheory","intLib","Cooper","pairTheory"]; open HolKernel Parse boolLib bossLib listTheory rich_listTheory arithmeticTheory Arith numLib computeLib Cooper pairTheory; PolyML.print_depth 1000; intLib.deprecate_int(); (* Start a new theory named "proofs" *) val _ = new_theory "proofs"; (* Experiment - possible slight speedup: val PROVE_TAC = METIS_TAC[]; *) (* Load in definitions of sponge function and MITB machine *) use "sponge.ml"; use "MITB.ml"; (* Some elementary lemmas about Moore machines proved to sanity check stuff in (or maybe only in early drafts of) the MITB paper. A sidetrack Not used in main proofsk should be in a separate file. *) val isTrace_def = Define `isTrace moore tr = !t. ?inp. tr(t+1) = moore inp (tr t)`; val mkTrace_def = Define `(mkTrace moore s inputs 0 = s) /\ (mkTrace moore s inputs (SUC t) = moore (inputs t) (mkTrace moore s inputs t))`; val mkTrace_isTrace = store_thm ("mkTrace_isTrace", ``isTrace moore (mkTrace moore s inputs)``, RW_TAC std_ss [isTrace_def] THEN Q.EXISTS_TAC `inputs t` THEN RW_TAC std_ss [mkTrace_def,GSYM ADD1]); val isTrace_mkTrace = store_thm ("isTrace_mkTrace", ``isTrace moore tr ==> ?s inputs. tr = mkTrace moore s inputs``, RW_TAC std_ss [isTrace_def] THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [boolTheory.EXISTS_DEF]) THEN Q.EXISTS_TAC `tr 0` THEN Q.EXISTS_TAC `\t. @inp. tr (t + 1) = moore inp (tr t)` THEN RW_TAC std_ss [FUN_EQ_THM] THEN Induct_on `x` THEN POP_ASSUM(ASSUME_TAC o GSYM) THEN RW_TAC std_ss [mkTrace_def,GSYM ADD1] THEN RW_TAC std_ss [ADD1]); (* Start proofs about definitions in sponge.ml about splitting and padding *) (* Sanity checks *) val LengthZeros = store_thm ("LengthZeros", ``!n. LENGTH(Zeros n) = n``, Induct THEN RW_TAC list_ss [Zeros_def]); val ZerosOneToOne = store_thm ("ZerosOneToOne", ``!m n. (Zeros m = Zeros n) = (m = n)``, Induct THEN Induct THEN RW_TAC list_ss [Zeros_def]); val LengthPadLemma1 = store_thm ("LengthPadLemma1", ``!r msg n. (2 < r) /\ (LENGTH msg = n * r) ==> (LENGTH(Pad r msg) = (n + 1) * r)``, RW_TAC list_ss [Pad_def,PadZeros_def,LengthZeros,MOD_TIMES]); val MOD_SUB_MOD = store_thm ("MOD_SUB_MOD", ``!m n r. 0 < r /\ 0 < n MOD r ==> ((r - n MOD r) MOD r = r - n MOD r)``, RW_TAC arith_ss []); val MULT_ADD_MOD = store_thm ("MULT_ADD_MOD", ``!n p r. p < r ==> ((n * r + p) MOD r = p)``, RW_TAC arith_ss[] THEN `0 < r` by DECIDE_TAC THEN PROVE_TAC[MOD_TIMES,ADD_SYM,LESS_MOD]); val LengthPadLemma2 = store_thm ("LengthPadLemma2", ``!r msg n p. (0 < p) /\ (p + 2 < r) /\ (LENGTH msg = n * r + p) ==> (LENGTH(Pad r msg) = (n + 1) * r)``, RW_TAC list_ss [Pad_def,PadZeros_def,LengthZeros,MOD_TIMES] THEN `0 < p + 2` by DECIDE_TAC THEN `p + (n * r + 2) = n * r + (p + 2)` by PROVE_TAC[ADD_SYM,ADD_ASSOC] THEN `0 < (n * r + (p + 2)) MOD r` by PROVE_TAC[MULT_ADD_MOD] THEN `p < r` by DECIDE_TAC THEN `0 < r` by DECIDE_TAC THEN RW_TAC std_ss [MOD_SUB_MOD,MULT_ADD_MOD] THEN DECIDE_TAC); val LengthPadLemma3 = store_thm ("LengthPadLemma3", ``!r msg n. (2 < r) /\ (LENGTH msg = n * r + (r - 2)) ==> (LENGTH(Pad r msg) = (n + 1) * r)``, RW_TAC list_ss [Pad_def,PadZeros_def,LengthZeros,MOD_TIMES] THEN `r + n * r = (n + 1) * r` by DECIDE_TAC THEN `0 < r` by DECIDE_TAC THEN RW_TAC std_ss [MOD_EQ_0] THEN RW_TAC arith_ss []); val LengthPadLemma4 = store_thm ("LengthPadLemma4", ``!r msg n. (2 < r) /\ (LENGTH msg = n * r + (r - 1)) ==> (LENGTH(Pad r msg) = (n + 2) * r)``, RW_TAC list_ss [Pad_def,PadZeros_def,LengthZeros,MOD_TIMES] THEN `r + (n * r + 1) = (n + 1) * r + 1` by PROVE_TAC[ADD_SYM,ADD_ASSOC,RIGHT_ADD_DISTRIB,MULT_LEFT_1] THEN RW_TAC std_ss [] THEN `1 < r` by DECIDE_TAC THEN RW_TAC std_ss [MULT_ADD_MOD] THEN `r - 1 < r` by DECIDE_TAC THEN RW_TAC std_ss [LESS_MOD] THEN DECIDE_TAC); val LengthPadLemma5 = store_thm ("LengthPadLemma5", ``!r msg n p. 2 < r /\ p < r /\ (LENGTH msg = n * r + p) ==> (LENGTH(Pad r msg) = (n + (if p = r - 1 then 2 else 1)) * r)``, RW_TAC std_ss [] THENL [PROVE_TAC[LengthPadLemma4], Cases_on `0 < p` THENL [`p + 2 < r \/ (p = r - 2) \/ (p = r - 1)` by PROVE_TAC [DECIDE ``2 < r /\ p < r ==> p + 2 < r \/ (p = r - 2) \/ (p = r - 1)``] THENL [PROVE_TAC[LengthPadLemma2], PROVE_TAC[LengthPadLemma3]], `p = 0` by DECIDE_TAC THEN RW_TAC arith_ss [] THEN `LENGTH msg = n * r` by PROVE_TAC[ADD_0] THEN IMP_RES_TAC LengthPadLemma1 THEN DECIDE_TAC]]); val LengthPadLemma6 = store_thm ("LengthPadLemma6", ``!r msg. 2 < r ==> ?n p. p < r /\ (LENGTH msg = n*r + p) /\ (LENGTH(Pad r msg) = if p = r-1 then (n+2)*r else (n+1)*r)``, RW_TAC std_ss [] THEN `?n p. (LENGTH msg = n * r + p) /\ p < r` by PROVE_TAC[DIVISION, DECIDE ``2 0 (LENGTH(Pad r msg) = (if (LENGTH msg MOD r) = r-1 then ((LENGTH msg DIV r) + 2) else ((LENGTH msg DIV r) + 1)) * r)``, RW_TAC std_ss [] THEN IMP_RES_TAC LengthPadLemma6 THEN POP_ASSUM(STRIP_ASSUME_TAC o SPEC ``msg : bool list``) THEN PROVE_TAC[DIV_UNIQUE,MOD_UNIQUE]); val LengthPadCor = store_thm ("LengthPadCor", ``!r msg. 2 < r ==> r <= LENGTH(Pad r msg)``, RW_TAC std_ss [LengthPad] THEN DECIDE_TAC); val LengthPadDivides = store_thm ("LengthPadDivides", ``!r msg. 2 < r ==> (LENGTH(Pad r msg) MOD r = 0)``, RW_TAC std_ss [] THEN `0 < r` by DECIDE_TAC THEN RW_TAC std_ss [LengthPad,MOD_EQ_0]); (* More lemmas needed for proving that minimal padding added *) val ADD_MOD_ZERO1 = store_thm ("ADD_MOD_ZERO1", ``!m p r. 0 < r /\ ((m + p) MOD r = 0) ==> ?n. p = n * r - m MOD r``, RW_TAC arith_ss [] THEN `?d. m + p = d * r` by PROVE_TAC[MOD_EQ_0_DIVISOR] THEN `((m DIV r) * r + m MOD r + p = d * r) /\ m MOD r < r` by PROVE_TAC[DIVISION] THEN Q.EXISTS_TAC `d - (m DIV r)` THEN RW_TAC arith_ss [RIGHT_SUB_DISTRIB]); val ADD_MOD_ZERO1_COR = store_thm ("ADD_MOD_ZERO1_COR", ``!m p r. 0 < r /\ 0 < p /\ ((m + p) MOD r = 0) ==> ?n. 0 < n /\ (p = n * r - m MOD r)``, RW_TAC std_ss [] THEN IMP_RES_TAC ADD_MOD_ZERO1 THEN POP_ASSUM(K ALL_TAC) THEN Cases_on `n=0` THEN RW_TAC arith_ss [] THEN `0 < n` by DECIDE_TAC THEN PROVE_TAC[]); val ADD_MOD_ZERO2 = store_thm ("ADD_MOD_ZERO2", ``!m p r. 0 < r /\ (?n. 0 < n /\ (p = n * r - m MOD r)) ==> ((m + p) MOD r = 0)``, RW_TAC arith_ss [] THEN `(m = (m DIV r) * r + m MOD r) /\ m MOD r < r` by PROVE_TAC[DIVISION] THEN `n = SUC(PRE n)` by DECIDE_TAC THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE arith_ss [ADD1]) THEN POP_ASSUM(fn th => SUBST_TAC[th]) THEN RW_TAC arith_ss [RIGHT_ADD_DISTRIB] THEN `(m + (r + r * PRE n) - m MOD r) = m DIV r * r + r + r * PRE n` by DECIDE_TAC THEN RW_TAC std_ss [] THEN `m DIV r * r + r + r * PRE n = m DIV r * r + 1 * r + PRE n * r` by PROVE_TAC[MULT_SYM,MULT_LEFT_1] THEN ONCE_ASM_REWRITE_TAC[] THEN PROVE_TAC[MOD_EQ_0,RIGHT_ADD_DISTRIB]); val ADD_MOD_ZERO = store_thm ("ADD_MOD_ZERO", ``!m p r. 0 < r /\ 0 < p ==> (((m + p) MOD r = 0) = ?n. 0 < n /\ (p = n * r - m MOD r))``, RW_TAC arith_ss [] THEN EQ_TAC THENL [PROVE_TAC[ADD_MOD_ZERO1_COR], PROVE_TAC[ADD_MOD_ZERO2]]); val ADD_MOD_ZERO_COR1 = store_thm ("ADD_MOD_ZERO_COR1", ``!msg n r. 0 < r ==> ((LENGTH(msg ++ [T] ++ Zeros n ++ [T]) MOD r = 0) = ?m. 0 < m /\ (n + 2 = m * r - LENGTH msg MOD r))``, RW_TAC list_ss [LengthZeros] THEN PROVE_TAC [DECIDE ``0 < n+2 /\ (m + (n + 2) = n + (m + 2))``, ADD_MOD_ZERO]); val ADD_MOD_ZERO_COR2 = store_thm ("ADD_MOD_ZERO_COR2", ``!msg n r. 2 < r ==> ((LENGTH(msg ++ [T] ++ Zeros n ++ [T]) MOD r = 0) = ?m. (if LENGTH msg MOD r = r - 1 then 1 else 0) < m /\ (n = m * r - LENGTH msg MOD r - 2))``, RW_TAC std_ss [] THEN `0 < r` by DECIDE_TAC THEN RW_TAC std_ss [ADD_MOD_ZERO_COR1] THENL [EQ_TAC THENL [RW_TAC std_ss [] THEN Cases_on `m = 1` THEN RW_TAC arith_ss [] THEN `?m'. m = m' + 2` by COOPER_TAC THEN `?r'. r = r' + 3` by COOPER_TAC THEN FULL_SIMP_TAC arith_ss [LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB] THEN `n = 3 * m' + (r' + (m' * r' + 4)) - 2` by DECIDE_TAC THEN RW_TAC arith_ss [] THEN Q.EXISTS_TAC `2+m'` THEN RW_TAC arith_ss [], RW_TAC std_ss [] THEN `?m'. m = m' + 2` by COOPER_TAC THEN RW_TAC std_ss [RIGHT_ADD_DISTRIB] THEN Q.EXISTS_TAC `m'+2` THEN RW_TAC arith_ss []], `LENGTH msg MOD r < r` by PROVE_TAC[MOD_LESS] THEN `LENGTH msg MOD r < r-1` by DECIDE_TAC THEN EQ_TAC THEN RW_TAC std_ss [] THEN`?m'. m = m' + 1` by COOPER_TAC THEN FULL_SIMP_TAC arith_ss [LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB] THEN Q.EXISTS_TAC `m'+1` THEN RW_TAC arith_ss []]); val MOD_ADD2_EQ = store_thm ("MOD_ADD2_EQ", ``!m r. 1 < r /\ (m MOD r = r - 1) ==> ((m + 2) MOD r = 1)``, RW_TAC arith_ss [] THEN `0 < r` by DECIDE_TAC THEN `m = m DIV r * r + (r - 1)` by PROVE_TAC[DIVISION] THEN POP_ASSUM(fn th => SUBST_TAC[th]) THEN `m DIV r * r + (r - 1) + 2 = m DIV r * r + (r + 1)` by DECIDE_TAC THEN RW_TAC std_ss [MOD_TIMES] THEN PROVE_TAC[MULT_LEFT_1,MULT_ADD_MOD]); val MOD_ADD2_NEQ = store_thm ("MOD_ADD2_NEQ", ``!m r. 1 < r /\ m MOD r <> r - 1 ==> ((r - (m + 2) MOD r) MOD r = r - m MOD r - 2)``, RW_TAC arith_ss [] THEN `0 < r` by DECIDE_TAC THEN `m MOD r < r` by PROVE_TAC[MOD_LESS] THEN `m MOD r < r - 1` by DECIDE_TAC THEN `m = m DIV r * r + m MOD r` by PROVE_TAC[DIVISION] THEN POP_ASSUM(fn th => SUBST_TAC[th]) THEN `m DIV r * r + m MOD r + 2 = m DIV r * r + (m MOD r + 2)` by DECIDE_TAC THEN RW_TAC std_ss [MOD_TIMES] THEN Cases_on `m MOD r + 2 = r` THEN RW_TAC arith_ss []); val PadZerosLemma1 = store_thm ("PadZerosLemma1", ``!r msg. 1 < r /\ (LENGTH msg MOD r = r - 1) ==> (PadZeros r msg = r - 1)``, RW_TAC arith_ss [PadZeros_def,MOD_ADD2_EQ]); val PadZerosLemma2 = store_thm ("PadZerosLemma2", ``!r msg. 1 < r /\ ~(LENGTH msg MOD r = r - 1) ==> (PadZeros r msg = r - LENGTH msg MOD r - 2)``, REWRITE_TAC[PadZeros_def,MOD_ADD2_NEQ]); val PadZeros = store_thm ("PadZeros", ``!r msg. 1 < r ==> (PadZeros r msg = if (LENGTH msg MOD r = r - 1 ) then r - 1 else r - LENGTH msg MOD r - 2)``, RW_TAC arith_ss [PadZerosLemma1,PadZerosLemma2]); val PadZerosCor1 = store_thm ("PadZerosCor1", ``!r msg. 1 < r /\ LENGTH msg <= r-2 ==> (PadZeros r msg = r - (LENGTH msg + 2))``, RW_TAC std_ss [] THEN `0 < r` by DECIDE_TAC THEN `LENGTH msg < r` by DECIDE_TAC THEN `LENGTH msg MOD r = LENGTH msg` by PROVE_TAC[LESS_MOD] THEN `LENGTH msg MOD r <> r - 1` by DECIDE_TAC THEN RW_TAC list_ss [PadZeros]); val LeastPad1 = store_thm ("LeastPad1", ``!r msg. 2 < r /\ (LENGTH msg MOD r = r - 1 ) ==> (LENGTH(msg ++ [T] ++ Zeros(r - 1) ++ [T]) MOD r = 0)``, RW_TAC std_ss [] THEN `0 < r` by DECIDE_TAC THEN `1 < r` by DECIDE_TAC THEN `r - 1 = PadZeros r msg` by PROVE_TAC[PadZeros] THEN RW_TAC arith_ss [GSYM Pad_def,LengthPad] THEN PROVE_TAC[MOD_EQ_0,MULT_SYM]); val LeastPad2 = store_thm ("LeastPad2", ``!r msg. 2 < r /\ (LENGTH msg MOD r = r - 1 ) /\ (LENGTH(msg ++ [T] ++ Zeros n ++ [T]) MOD r = 0) ==> r - 1 <= n``, RW_TAC std_ss [] THEN `?m. 1 < m /\ (n = m * r - LENGTH msg MOD r - 2)` by PROVE_TAC[ADD_MOD_ZERO_COR2] THEN `?m'. m = m' + 2` by COOPER_TAC THEN RW_TAC std_ss [RIGHT_ADD_DISTRIB] THEN DECIDE_TAC); val LeastPad3 = store_thm ("LeastPad3", ``!r msg. 2 < r /\ ~(LENGTH msg MOD r = r - 1 ) ==> (LENGTH(msg ++ [T] ++ Zeros(r - LENGTH msg MOD r - 2) ++ [T]) MOD r = 0)``, RW_TAC std_ss [] THEN `0 < r` by DECIDE_TAC THEN `1 < r` by DECIDE_TAC THEN `r - LENGTH msg MOD r - 2 = PadZeros r msg` by PROVE_TAC[PadZeros] THEN RW_TAC arith_ss [GSYM Pad_def,LengthPad] THEN PROVE_TAC[MOD_EQ_0,MULT_SYM]); val LeastPad4 = store_thm ("LeastPad4", ``!r msg. 2 < r /\ ~(LENGTH msg MOD r = r - 1 ) /\ (LENGTH(msg ++ [T] ++ Zeros n ++ [T]) MOD r = 0) ==> r - LENGTH msg MOD r - 2 <= n``, RW_TAC std_ss [] THEN `?m. 0 < m /\ (n = m * r - LENGTH msg MOD r - 2)` by PROVE_TAC[ADD_MOD_ZERO_COR2] THEN `?m'. m = m' + 1` by COOPER_TAC THEN FULL_SIMP_TAC std_ss [RIGHT_ADD_DISTRIB] THEN DECIDE_TAC); (* Proof that PadZeros r msg computes the smallest number n such that the length of (msg ++ [T] ++ Zeros n ++ [T]) is a multiple of r, i.e.: *) val LeastPad = store_thm ("LeastPad", ``!r msg. 2 < r ==> (LENGTH(msg ++ [T] ++ Zeros(PadZeros r msg) ++ [T]) MOD r = 0) /\ !n. (LENGTH(msg ++ [T] ++ Zeros n ++ [T]) MOD r = 0) ==> PadZeros r msg <= n``, REPEAT GEN_TAC THEN DISCH_TAC THEN `1 < r` by DECIDE_TAC THEN Cases_on `LENGTH msg MOD r = r - 1` THEN RW_TAC pure_ss [PadZeros] THEN RW_TAC std_ss [LeastPad1,LeastPad2,LeastPad3,LeastPad4] THEN `r - 1 <= n` by PROVE_TAC[LeastPad2] THEN DECIDE_TAC); (* A couple of lemmas about TAKE and DROP *) val LEQ_TAKE = store_thm ("LEQ_TAKE", ``!n l. LENGTH l <= n ==> (TAKE n l = l)``, Induct THEN RW_TAC list_ss [LENGTH_NIL] THEN Cases_on `l` THEN FULL_SIMP_TAC list_ss [LENGTH_NIL]); val LEQ_DROP = store_thm ("LEQ_DROP", ``!n l. LENGTH l <= n ==> (DROP n l = [])``, Induct THEN RW_TAC list_ss [LENGTH_NIL] THEN Cases_on `l` THEN FULL_SIMP_TAC list_ss [LENGTH_NIL]); (* Lemmas about Split *) val SplitNotEmpty = store_thm ("SplitNotEmpty", ``!r msg. ~(Split r msg = [])``, RW_TAC list_ss [Once Split_def]); val FlattenSplit = store_thm ("FlattenSplit", ``!r msg. 0 < r ==> (FLAT(Split r msg) = msg)``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def]); (* Lemmas needed to characterise LENGTH(Split r msg) *) val MOD0 = store_thm ("MOD0", ``!m n. m <= n /\ m <> 0 /\ (m MOD n = 0) ==> (m = n)``, RW_TAC arith_ss [] THEN `0 < n` by DECIDE_TAC THEN `?d. m = d * n` by PROVE_TAC[MOD_EQ_0_DIVISOR] THEN RW_TAC arith_ss [] THEN Cases_on `d` THEN FULL_SIMP_TAC arith_ss [] THEN `n' = 0` by DECIDE_TAC THEN RW_TAC arith_ss []); val MOD_NEQ0_LESS = store_thm ("MOD_NEQ0_LESS", ``!m n. 0 < n /\ m <= n /\ m MOD n <> 0 ==> m < n``, RW_TAC arith_ss [] THEN Cases_on `m` THEN FULL_SIMP_TAC arith_ss [] THEN Cases_on `SUC n' = n` THEN FULL_SIMP_TAC arith_ss []); val DIV_SUB_COR = store_thm ("DIV_SUB_COR", ``!m n. 0 < n /\ n <= m ==> ((m - n) DIV n = (m DIV n) - 1)``, RW_TAC arith_ss [] THEN `n * 1 <= m` by DECIDE_TAC THEN IMP_RES_TAC DIV_SUB THEN FULL_SIMP_TAC arith_ss []); val LESS_DIV = store_thm ("LESS_DIV", ``!m n. 0 < n /\ n <= m ==> 0 < m DIV n``, RW_TAC arith_ss [] THEN `(m = m DIV n * n + m MOD n) /\ m MOD n < n` by PROVE_TAC[DIVISION] THEN Cases_on `m DIV n = 0` THEN FULL_SIMP_TAC arith_ss []); val MOD0_SUB = store_thm ("MOD0_SUB", ``!m n. 0 < n /\ n < m /\ (m MOD n = 0) ==> n <= m - n``, RW_TAC arith_ss [] THEN `?d. m = d * n` by PROVE_TAC[MOD_EQ_0_DIVISOR] THEN `(d = 0) \/ (d = 1) \/ ?u. d = 2 + u` by COOPER_TAC THEN RW_TAC arith_ss [LEFT_ADD_DISTRIB]); val SplitAppendLemma = store_thm ("SplitAppendLemma", ``!r msg l1. 0 < r /\ (LENGTH l1 MOD r = 0) /\ r <= LENGTH l1 ==> !l2. (msg = l1 ++ l2) /\ 0 < LENGTH l2 ==> (Split r msg = Split r l1 ++ Split r l2)``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN FULL_SIMP_TAC list_ss [] THEN Cases_on `r < LENGTH l1` THENL [RW_TAC list_ss [] THEN FULL_SIMP_TAC list_ss [] THEN ASSUM_LIST (fn thl => ASSUME_TAC(Q.SPECL[`DROP r l1`](el 6 thl))) THEN IMP_RES_TAC MOD0_SUB THEN FULL_SIMP_TAC list_ss [LENGTH_DROP] THEN `r <= LENGTH l1` by DECIDE_TAC THEN `(LENGTH l1 - r) MOD r = 0` by RW_TAC list_ss [SUB_MOD] THEN `r <= LENGTH l1 - r` by RW_TAC list_ss [MOD0_SUB] THEN `(Split r (DROP r l1 ++ l2) = Split r (DROP r l1) ++ Split r l2)` by PROVE_TAC[DROP_APPEND1] THEN `~((r = 0) \/ LENGTH l1 <= r)` by DECIDE_TAC THEN `Split r l1 = TAKE r l1::Split r (DROP r l1)` by PROVE_TAC[Split_def] THEN POP_ASSUM(fn th => SUBST_TAC[th]) THEN `~((r = 0) \/ LENGTH l1 + LENGTH l2 <= r)` by DECIDE_TAC THEN `~((r = 0) \/ LENGTH(l1 ++ l2) <= r)` by PROVE_TAC[LENGTH_APPEND] THEN `Split r (l1++l2) = TAKE r (l1++l2)::Split r (DROP r (l1++l2))` by PROVE_TAC[Split_def] THEN POP_ASSUM(fn th => SUBST_TAC[th]) THEN RW_TAC list_ss [TAKE_APPEND1,DROP_APPEND1], `LENGTH l1 = r` by DECIDE_TAC THEN `Split (LENGTH l1) l1 = [l1]` by RW_TAC list_ss [Once Split_def] THEN RW_TAC list_ss [] THEN `~((LENGTH l1 = 0) \/ LENGTH l1 + LENGTH l2 <= LENGTH l1)` by DECIDE_TAC THEN `~((LENGTH l1 = 0) \/ LENGTH(l1++l2) <= LENGTH l1)` by PROVE_TAC[LENGTH_APPEND] THEN `Split (LENGTH l1) (l1++l2) = TAKE (LENGTH l1) (l1++l2) :: Split (LENGTH l1) (DROP (LENGTH l1) (l1++l2))` by RW_TAC list_ss [Once Split_def] THEN RW_TAC list_ss [TAKE_APPEND1,DROP_APPEND1,DROP_LENGTH_NIL]]); val SplitAppend = store_thm ("SplitAppend", ``!r l1 l2. 0 < r /\ (LENGTH l1 MOD r = 0) /\ r <= LENGTH l1 /\ 0 < LENGTH l2 ==> (Split r (l1 ++ l2) = Split r l1 ++ Split r l2)``, PROVE_TAC[SplitAppendLemma]); (* Characterise LENGTH(Split r msg) *) val LengthSplit = store_thm ("LengthSplit", ``!r msg. 0 < r ==> (LENGTH(Split r msg) = if msg = [] then 1 else if LENGTH msg MOD r = 0 then (LENGTH msg DIV r) else (LENGTH msg DIV r) + 1)``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def] THENL [`LENGTH msg = r` by PROVE_TAC[LENGTH_NIL,MOD0] THEN RW_TAC arith_ss [], FULL_SIMP_TAC arith_ss [DROP_NIL], `LENGTH msg < r` by PROVE_TAC[MOD_NEQ0_LESS] THEN RW_TAC arith_ss [LESS_DIV_EQ_ZERO], FULL_SIMP_TAC arith_ss [DROP_NIL], `LENGTH msg = r` by PROVE_TAC[LENGTH_NIL,MOD0] THEN RW_TAC arith_ss [], `r <= LENGTH msg` by DECIDE_TAC THEN RW_TAC arith_ss [DIV_SUB_COR] THEN `0 < LENGTH msg DIV r` by PROVE_TAC[LESS_DIV] THEN DECIDE_TAC, `LENGTH msg < r` by PROVE_TAC[MOD_NEQ0_LESS] THEN RW_TAC arith_ss [LESS_DIV_EQ_ZERO], `r <= LENGTH msg` by DECIDE_TAC THEN RW_TAC arith_ss [DIV_SUB_COR] THEN `0 < LENGTH msg DIV r` by PROVE_TAC[LESS_DIV] THEN `(LENGTH msg - r) MOD r = LENGTH msg MOD r` by PROVE_TAC[SUB_MOD] THEN DECIDE_TAC, `LENGTH msg = r` by PROVE_TAC[LENGTH_NIL,MOD0] THEN RW_TAC arith_ss [], `r <= LENGTH msg` by DECIDE_TAC THEN RW_TAC arith_ss [DIV_SUB_COR] THEN `0 < LENGTH msg DIV r` by PROVE_TAC[LESS_DIV] THEN `(LENGTH msg - r) MOD r = LENGTH msg MOD r` by PROVE_TAC[SUB_MOD] THEN DECIDE_TAC, `LENGTH msg < r` by PROVE_TAC[MOD_NEQ0_LESS] THEN RW_TAC arith_ss [LESS_DIV_EQ_ZERO], `r <= LENGTH msg` by DECIDE_TAC THEN RW_TAC arith_ss [DIV_SUB_COR] THEN `0 < LENGTH msg DIV r` by PROVE_TAC[LESS_DIV] THEN `(LENGTH msg - r) MOD r = LENGTH msg MOD r` by PROVE_TAC[SUB_MOD] THEN DECIDE_TAC]); (* Alternative version of Split with a simple recursion *) val SplitN_def = Define `(SplitN 0 r msg = []) /\ (SplitN (SUC n) r msg = if LENGTH msg <= r then [msg] else TAKE r msg::SplitN n r (DROP r msg))`; (* Maybe this isn't true! val SplitN_APPEND = store_thm ("SplitN_APPEND", ``!m n r msg. 0 < r ==> (SplitN (m+n) r msg = SplitN m r msg ++ SplitN n r (DROP (m * r) msg))``, Induct THEN RW_TAC list_ss [SplitN_def] *) val SplitSplitNLemma = store_thm ("SplitSplitNLemma", ``!n r msg. 0 < r ==> (TAKE n (Split r msg) = SplitN n r msg)``, Induct THEN RW_TAC list_ss [Once Split_def,SplitN_def,TAKE]); val SplitSplitN = store_thm ("SplitSplitN", ``!r msg. 0 < r ==> (Split r msg = if msg = [] then [[]] else if LENGTH msg MOD r = 0 then SplitN (LENGTH msg DIV r) r msg else SplitN (LENGTH msg DIV r + 1) r msg)``, PROVE_TAC [EVAL ``SplitN 1 r []``, SplitSplitNLemma,TAKE_LENGTH_ID,LengthSplit]); (* Lemmas characterising Split r (Pad rmsg) under various assumptions *) val SplitPadLemma1 = store_thm ("SplitPadLemma1", ``!r msg. 2 < r /\ LENGTH msg <= r-2 ==> (Split r (Pad r msg) = [msg ++ [T] ++ Zeros(r - (LENGTH msg + 2)) ++ [T]])``, RW_TAC std_ss [Pad_def] THEN `1 < r` by DECIDE_TAC THEN RW_TAC std_ss [PadZerosCor1] THEN `LENGTH msg <= r` by DECIDE_TAC THEN `LENGTH(msg ++ [T] ++ Zeros (r - (LENGTH msg + 2)) ++ [T]) <= r` by RW_TAC list_ss [LengthZeros] THEN `Split r (msg ++ [T] ++ Zeros (r - (LENGTH msg + 2)) ++ [T]) = [(msg ++ [T] ++ Zeros (r - (LENGTH msg + 2)) ++ [T])]` by PROVE_TAC[Split_def]); val SplitPadLemma2 = store_thm ("SplitPadLemma2", ``!r msg. 2 < r /\ (LENGTH msg = r-1) ==> (Split r (Pad r msg) = [(msg ++ [T]);(Zeros(r - 1) ++ [T])])``, SIMP_TAC std_ss [Pad_def] THEN recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def] THEN `LENGTH(msg ++ [T]) = r` by RW_TAC list_ss[] THEN `msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T] = (msg ++ [T]) ++ (Zeros (PadZeros r msg) ++ [T])` by PROVE_TAC[APPEND_ASSOC] THEN RW_TAC std_ss [TAKE_LENGTH_APPEND,DROP_LENGTH_APPEND] THEN POP_ASSUM(K ALL_TAC) THEN POP_ASSUM(K ALL_TAC) THEN FULL_SIMP_TAC list_ss [PadZeros] THEN `LENGTH(Zeros(LENGTH msg) ++ [T]) <= LENGTH msg + 1` by RW_TAC list_ss [LengthZeros] THEN PROVE_TAC[Split_def]); val SplitPadLemma3 = store_thm ("SplitPadLemma3", ``!r msg. 2 < r /\ (LENGTH msg = r) ==> (Split r (Pad r msg) = [msg;([T] ++ Zeros(r - 2) ++ [T])])``, REWRITE_TAC[Pad_def] THEN recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def] THEN `msg ++ [T] ++ Zeros (PadZeros (LENGTH msg) msg) ++ [T] = msg ++ ([T] ++ Zeros (PadZeros (LENGTH msg) msg) ++ [T])` by PROVE_TAC[APPEND_ASSOC] THEN RW_TAC std_ss [TAKE_LENGTH_APPEND,DROP_LENGTH_APPEND] THEN POP_ASSUM(K ALL_TAC) THEN FULL_SIMP_TAC list_ss [PadZeros] THEN `LENGTH(T::(Zeros(LENGTH msg - 2) ++ [T])) <= LENGTH msg` by RW_TAC list_ss [LengthZeros] THEN PROVE_TAC[Split_def]); (* Lemmas about lengths of elements of Split r msg *) val SplitLengthsLemma1 = store_thm ("SplitLengthsLemma1", ``!r msg n. n < PRE(LENGTH(Split r msg)) ==> (LENGTH(EL n (Split r msg)) = r)``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def] THENL [`n < PRE (LENGTH [msg])` by PROVE_TAC[Split_def] THEN FULL_SIMP_TAC list_ss [], `n < PRE (LENGTH [msg])` by PROVE_TAC[Split_def] THEN FULL_SIMP_TAC list_ss [], Cases_on `n` THEN RW_TAC list_ss [] THEN `n' < PRE (LENGTH (Split r (DROP r msg))) ==> (LENGTH (EL n' (Split r (DROP r msg))) = r)` by PROVE_TAC[] THEN `Split r msg = TAKE r msg::Split r (DROP r msg)` by PROVE_TAC[Split_def] THEN FULL_SIMP_TAC list_ss []]); val SplitLengthsLemma2 = store_thm ("SplitLengthsLemma2", ``!r msg. 0 < LENGTH(Split r msg)``, RW_TAC list_ss [Once Split_def]); val SplitLengthsLemma3 = store_thm ("SplitLengthsLemma3", ``!r msg. 0 < r ==> LENGTH(EL (PRE(LENGTH(Split r msg))) (Split r msg)) <= r``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def] THENL [`Split r msg = [msg]` by PROVE_TAC[Split_def] THEN RW_TAC list_ss [], `r <> 0` by DECIDE_TAC THEN `LENGTH (EL (PRE (LENGTH (Split r (DROP r msg)))) (Split r (DROP r msg))) <= r` by PROVE_TAC[] THEN `Split r msg = TAKE r msg::Split r (DROP r msg)` by PROVE_TAC[Split_def] THEN `0 < (LENGTH (Split r (DROP r msg)))` by PROVE_TAC[SplitLengthsLemma2] THEN RW_TAC list_ss [EL_CONS]]); val SplitBlockLengths = store_thm ("SplitBlockLengths", ``!r msg. 0 < r ==> (LENGTH(EL (PRE(LENGTH(Split r msg))) (Split r msg)) <= r) /\ (!n. n < PRE(LENGTH(Split r msg)) ==> (LENGTH(EL n (Split r msg)) = r))``, PROVE_TAC[SplitLengthsLemma1,SplitLengthsLemma3]); val SplitLastLength = store_thm ("SplitLastLength", ``!r msg. 0 < r /\ 0 < LENGTH msg MOD r ==> (LENGTH(EL (PRE(LENGTH(Split r msg))) (Split r msg)) = LENGTH msg MOD r)``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def] THENL [`Split r msg = [msg]` by PROVE_TAC[Split_def] THEN RW_TAC list_ss [] THEN Cases_on `LENGTH msg < r` THEN RW_TAC arith_ss [] THEN `LENGTH msg = r` by DECIDE_TAC THEN `0 < r MOD r` by PROVE_TAC[] THEN `r MOD r = 0` by PROVE_TAC[DIVMOD_ID] THEN DECIDE_TAC, `r <> 0` by DECIDE_TAC THEN `r <= LENGTH msg` by DECIDE_TAC THEN `(LENGTH msg - r) MOD r = LENGTH msg MOD r` by PROVE_TAC[SUB_MOD] THEN `LENGTH (EL (PRE (LENGTH (Split r (DROP r msg)))) (Split r (DROP r msg))) = (LENGTH msg - r) MOD r` by PROVE_TAC[SUB_MOD] THEN `Split r msg = TAKE r msg::Split r (DROP r msg)` by PROVE_TAC[Split_def] THEN `0 < (LENGTH (Split r (DROP r msg)))` by PROVE_TAC[SplitLengthsLemma2] THEN RW_TAC list_ss [EL_CONS]]); val LengthLastSplit = store_thm ("LengthLastSplit", ``!r msg. 0 < r /\ 0 < LENGTH msg MOD r ==> (LENGTH (LAST(Split r msg)) = LENGTH msg MOD r)``, RW_TAC list_ss [] THEN `Split r msg <> []` by PROVE_TAC[SplitNotEmpty] THEN RW_TAC list_ss [LAST_EL,SplitLastLength]); val LengthEveryFrontSplit = store_thm ("LengthEveryFrontSplit", ``!r (msg:bits). 0 < r ==> EVERY (\l. LENGTH l = r) (FRONT (Split r msg))``, RW_TAC std_ss [] THEN `Split r msg <> []` by PROVE_TAC[SplitNotEmpty] THEN IMP_RES_TAC LENGTH_FRONT THEN ASSUME_TAC (ISPECL [``FRONT (Split r (msg:bits))``,``\l:bits. LENGTH l = r``] EVERY_EL) THEN PROVE_TAC[NULL_EQ,EL_FRONT,SplitBlockLengths]); (* Characterise length of FRONT(Split r msg) *) val SNOC_LAST_FRONT = store_thm ("SNOC_LAST_FRONT", ``!l. 0 < LENGTH l ==> (SNOC (LAST l) (FRONT l) = l)``, Induct THEN RW_TAC list_ss [APPEND_FRONT_LAST,SNOC_APPEND]); val SNOC_LAST_Split = store_thm ("SNOC_LAST_Split", ``!r msg. SNOC (LAST (Split r msg)) (FRONT (Split r msg)) = (Split r msg)``, PROVE_TAC[SplitLengthsLemma2,SNOC_LAST_FRONT]); val LengthFrontSplit = store_thm ("LengthFrontSplit", ``!r msg. 0 < r ==> (LENGTH(FRONT(Split r msg)) = if LENGTH msg MOD r = 0 then LENGTH msg DIV r - 1 else LENGTH msg DIV r)``, RW_TAC std_ss [Once(GSYM SNOC_LAST_Split),SNOC_APPEND] THEN `Split r msg <> []` by PROVE_TAC[SplitNotEmpty] THEN RW_TAC list_ss [LENGTH_FRONT,LengthSplit,ZERO_DIV]); (* Sanity check *) val LengthXor = store_thm ("LengthXor", ``!l1 l2. LENGTH(l1 Xor l2) = MAX (LENGTH l1) (LENGTH l2)``, REPEAT Induct THEN RW_TAC list_ss [Xor_def,MAX_DEF]); (* Relate Absorb to FOLDL and then derive some easy consequences *) val Absorb_FOLDL = store_thm ("Absorb_FOLDL", ``Absorb f c = FOLDL (\s bk. f(s Xor (bk ++ Zeros c)))``, RW_TAC std_ss [FUN_EQ_THM] THEN Q.SPEC_TAC(`x`,`s0`) THEN Q.SPEC_TAC(`x'`,`bkl`) THEN Induct THEN RW_TAC list_ss [Absorb_def]); val Absorb_APPEND = store_thm ("Absorb_APPEND", ``!f c s bkl1 bkl2. Absorb f c s (bkl1 ++ bkl2) = Absorb f c (Absorb f c s bkl1) bkl2``, RW_TAC list_ss [FOLDL_APPEND,Absorb_FOLDL]); val Absorb_SNOC = store_thm ("Absorb_SNOC", ``!f c s bk bkl. Absorb f c s (SNOC bk bkl) = f(Absorb f c s bkl Xor (bk ++ Zeros c))``, RW_TAC list_ss [FOLDL_SNOC,Absorb_FOLDL]); (* Start proos about MITB machine defined in MITB.ml *) (* Predicate to test for a well-formed state *) val GoodState_def = Define `GoodState (r,c,n) (cntl,pmem,vmem) = (LENGTH pmem = r + c) /\ (LENGTH vmem = r + c)`; (* Predicate to test for a well-formed command *) val GoodCommand_def = Define `(GoodCommand (r,c,n) Ready (Input key len) = (LENGTH key = r) /\ (len <= r)) /\ (GoodCommand (r,c,n) Absorbing (Input bk len) = (LENGTH bk = r) /\ len <= r) /\ (GoodCommand (r,c,n) AbsorbEnd cmd = T) /\ (GoodCommand (r,c,n) cntl Move = T) /\ (GoodCommand (r,c,n) cntl Skip = T)`; (* Sanity check *) val LENGTH_ZEROS = store_thm ("LENGTH_ZEROS", ``!n. LENGTH(ZEROS n) = n``, Induct THEN RW_TAC list_ss [ZEROS_def]); (* Sanity check *) val LENGTH_XOR = store_thm ("LENGTH_XOR", ``!l1 l2. LENGTH(l1 XOR l2) = MAX (LENGTH l1) (LENGTH l2)``, REPEAT Induct THEN RW_TAC list_ss [XOR_def,MAX_DEF]); (* Sanity check *) val MITB_PreservesGoodStates = store_thm ("MITB_PreservesGoodStates", ``!cntl cmd. GoodParameters(r,c,n) /\ GoodState (r,c,n) (cntl,pmem,vmem) /\ GoodCommand (r,c,n) cntl cmd /\ (!s. LENGTH(f s) = LENGTH s) ==> GoodState (r,c,n) (MITB_FUN (r,c,n) f (cntl,pmem,vmem) cmd)``, REPEAT Cases THEN RW_TAC list_ss [GoodParameters_def,GoodState_def,GoodCommand_def, MITB_FUN_def,LENGTH_ZEROS,LENGTH_XOR]); (* XOR and Xor are equal *) val XOREqXor = store_thm ("XOREQXor", ``$XOR = $Xor``, RW_TAC std_ss [FUN_EQ_THM] THEN SPEC_TAC(``x':bits``,``bl2:bits``) THEN SPEC_TAC(``x:bits``,``bl1:bits``) THEN Induct THEN RW_TAC list_ss [XOR_def,Xor_def] THEN Induct_on `bl2` THEN RW_TAC list_ss [XOR_def,Xor_def]); (* ZEROS and Zeros are equal *) val ZEROSEqZeros = store_thm ("ZEROSEqZeros", ``ZEROS = Zeros``, RW_TAC std_ss [FUN_EQ_THM] THEN SPEC_TAC(``x:num``,``n:num``) THEN Induct THEN RW_TAC list_ss [ZEROS_def,Zeros_def]); (* Lemmas needed later *) val ZerosXorZeros = store_thm ("ZerosXorZeros", ``!c. Zeros c Xor Zeros c = Zeros c``, Induct THEN RW_TAC list_ss [Zeros_def,Xor_def]); val ZerosXorLENGTH = store_thm ("ZerosXorLENGTH", ``!key c. Zeros (c + LENGTH key) Xor (key ++ Zeros c) = key ++ Zeros c``, Induct THEN RW_TAC list_ss [Zeros_def,ZerosXorZeros,Xor_def,GSYM ADD_SUC]); val AbsorbFrontLast = store_thm ("AbsorbFrontLast", ``!r msg f c s. Absorb f c s (Split r msg) = f(Absorb f c s (FRONT (Split r msg)) Xor (LAST (Split r msg) ++ Zeros c))``, PROVE_TAC[Absorb_SNOC,SNOC_LAST_Split]); val LASTN_DROP_LASTN = store_thm ("LASTN_DROP_LASTN", ``!n l. 2 * n <= LENGTH l ==> (LASTN n (DROP n l) = LASTN n l)``, RW_TAC list_ss [] THEN ASSUME_TAC(Q.AP_TERM `LASTN n` (SPEC_ALL TAKE_DROP)) THEN ASSUME_TAC(SPEC_ALL LENGTH_DROP) THEN `n <= LENGTH l - n` by DECIDE_TAC THEN PROVE_TAC[LASTN_APPEND2]); val FRONT_FLAT_LEMMA = prove (``!r msg bkl l. 0 < r /\ (LENGTH l = r) /\ EVERY (\bk. LENGTH bk = r) bkl /\ (msg = FLAT bkl ++ l) ==> (FRONT(Split r msg) = bkl)``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN Cases_on `bkl` THEN FULL_SIMP_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def] THEN RW_TAC std_ss [GSYM APPEND_ASSOC] THEN ASSUM_LIST(fn thl => ONCE_REWRITE_TAC[GSYM(el 2 thl)]) THEN RW_TAC std_ss [TAKE_LENGTH_APPEND] THEN ASSUM_LIST (fn thl => ASSUME_TAC (SIMP_RULE std_ss [el 1 thl,GSYM(el 2 thl),DROP_LENGTH_APPEND,GSYM APPEND_ASSOC] (Q.SPECL[`t`,`l`](el 4 thl)))) THEN ASSUM_LIST(fn thl => REWRITE_TAC[GSYM(el 3 thl),DROP_LENGTH_APPEND]) THEN RW_TAC list_ss [FRONT_DEF,SplitNotEmpty]); val FRONT_FLAT = store_thm ("FRONT_FLAT", ``!r bkl (l:bits). 0 < r /\ (LENGTH l = r) /\ EVERY (\bk. LENGTH bk = r) bkl ==> (FRONT(Split r (FLAT bkl ++ l)) = bkl)``, REWRITE_TAC [SIMP_RULE std_ss [] (SPECL [``r:num``,``FLAT bkl ++ (l:'a list)``, ``bkl:('a list)list``,``l:'a list``] FRONT_FLAT_LEMMA)]); val LASTSplitLASTN1 = store_thm ("LASTSplitLASTN1", ``!r msg. 1 < r /\ (r <= LENGTH msg) /\ (LENGTH msg MOD r = 0) ==> (LAST(Split r msg) = LASTN r msg)``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def,LAST_DEF,SplitNotEmpty] THENL [`LENGTH msg = r` by DECIDE_TAC THEN RW_TAC list_ss [LASTN_LENGTH_ID], `0 < r /\ r <> 0` by DECIDE_TAC THEN `(LENGTH msg - r) MOD r = 0` by PROVE_TAC[SUB_MOD] THEN `?k. LENGTH msg = k * r` by PROVE_TAC[DIVISION,ADD_0] THEN Cases_on `k` THENL[FULL_SIMP_TAC arith_ss [],ALL_TAC] THEN Cases_on `n` THENL [`LENGTH msg = r` by PROVE_TAC[ONE,MULT_LEFT_1] THEN `LENGTH msg <= r` by DECIDE_TAC, ALL_TAC] THEN `SUC (SUC n') = n' + 2` by DECIDE_TAC THEN `LENGTH msg = n'* r + 2 *r` by PROVE_TAC[RIGHT_ADD_DISTRIB] THEN `r <= LENGTH msg - r` by DECIDE_TAC THEN `LAST (Split r (DROP r msg)) = LASTN r (DROP r msg)` by PROVE_TAC[] THEN RW_TAC list_ss [] THEN `2 * r <= LENGTH msg` by DECIDE_TAC THEN RW_TAC list_ss [LASTN_DROP_LASTN]]); (* Stonger version of LASTSplitLASTN1, which should eventually replace it (but not done so as to preserve proofs depending on weaker version above) *) val LASTSplitLASTN2 = store_thm ("LASTSplitLASTN2", ``!r msg. 1 < r /\ msg <> [] /\ (LENGTH msg MOD r = 0) ==> (LAST(Split r msg) = LASTN r msg)``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def,LAST_DEF,SplitNotEmpty] THENL [`0 < r` by DECIDE_TAC THEN `?d. LENGTH msg = d * r` by PROVE_TAC[MOD_EQ_0_DIVISOR] THEN `(d = 0) \/ (d = 1) \/ ?m. d = 2 + m` by COOPER_TAC THEN RW_TAC list_ss [] THEN FULL_SIMP_TAC list_ss [LENGTH_NIL] THEN RW_TAC list_ss [LASTN_LENGTH_ID], `0 < r /\ r <> 0` by DECIDE_TAC THEN `r <= LENGTH msg` by DECIDE_TAC THEN `(LENGTH msg - r) MOD r = 0` by PROVE_TAC[SUB_MOD] THEN `?k. LENGTH msg = k * r` by PROVE_TAC[DIVISION,ADD_0] THEN Cases_on `k` THENL[FULL_SIMP_TAC arith_ss [],ALL_TAC] THEN Cases_on `n` THENL [`LENGTH msg = r` by PROVE_TAC[ONE,MULT_LEFT_1] THEN `LENGTH msg <= r` by DECIDE_TAC, ALL_TAC] THEN `SUC (SUC n') = n' + 2` by DECIDE_TAC THEN `LENGTH msg = n'* r + 2 * r` by PROVE_TAC[RIGHT_ADD_DISTRIB] THEN `r <= LENGTH msg - r` by DECIDE_TAC THEN `~(r >= LENGTH msg)` by DECIDE_TAC THEN `LAST (Split r (DROP r msg)) = LASTN r (DROP r msg)` by PROVE_TAC[DROP_NIL] THEN RW_TAC list_ss [] THEN `2 * r <= LENGTH msg` by DECIDE_TAC THEN RW_TAC list_ss [LASTN_DROP_LASTN]]); val MOD_LESS_SUB = store_thm ("MOD_LESS_SUB", ``!m n. 0 < n /\ n <= m ==> m MOD n <= m - n``, PROVE_TAC[MOD_LESS_EQ,SUB_MOD]); val LASTSplitLASTN3 = store_thm ("LASTSplitLASTN3", ``!r msg. 1 < r /\ msg <> [] /\ 0 < LENGTH msg MOD r ==> (LAST(Split r msg) = LASTN (LENGTH msg MOD r) msg)``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def,LAST_DEF,SplitNotEmpty] THEN `0 < r` by DECIDE_TAC THENL [Cases_on `LENGTH msg = r` THEN FULL_SIMP_TAC arith_ss [LASTN_LENGTH_ID], `r < LENGTH msg /\ r <= LENGTH msg /\ ~(r >= LENGTH msg) /\ r <> 0` by DECIDE_TAC THEN `(LENGTH msg - r) MOD r = LENGTH msg MOD r` by PROVE_TAC[SUB_MOD] THEN `0 < (LENGTH msg - r) MOD r` by PROVE_TAC[] THEN `DROP r msg <> []` by PROVE_TAC[DROP_NIL] THEN RW_TAC list_ss [LASTN_LENGTH_ID,DROP_LASTN] THEN `LENGTH msg MOD r <= LENGTH msg - r` by PROVE_TAC[MOD_LESS_SUB] THEN RW_TAC list_ss [LASTN_LASTN]]); (* Combining the above *) val LASTSplitLASTN = store_thm ("LASTSplitLASTN", ``!r msg. 1 < r /\ msg <> [] ==> (LAST(Split r msg) = if (LENGTH msg MOD r = 0) then LASTN r msg else LASTN (LENGTH msg MOD r) msg)``, RW_TAC list_ss [LASTSplitLASTN2,LASTSplitLASTN3]); (* Consequence of LengthLastSplit and LASTSplitLASTN2 *) val LENGTH_LAST_Split = store_thm ("LENGTH_LAST_Split", ``!r msg. 1 < r ==> (LENGTH(LAST(Split r msg)) = if msg = [] then 0 else if LENGTH msg MOD r = 0 then r else LENGTH msg MOD r)``, RW_TAC list_ss [] THEN `0 < r` by DECIDE_TAC THENL [RW_TAC list_ss [Once Split_def], RW_TAC list_ss [LASTSplitLASTN2] THEN `?d. LENGTH msg = d * r` by PROVE_TAC[MOD_EQ_0_DIVISOR] THEN `(d = 0) \/ (d = 1) \/ ?m. d = 2 + m` by COOPER_TAC THEN RW_TAC list_ss [] THEN FULL_SIMP_TAC list_ss [LENGTH_NIL,LEFT_ADD_DISTRIB] THEN RW_TAC list_ss [LASTN_LENGTH_ID] THEN `r <= LENGTH msg` by DECIDE_TAC THEN RW_TAC list_ss [LENGTH_LASTN], `0 < LENGTH msg MOD r` by DECIDE_TAC THEN RW_TAC std_ss [LengthLastSplit]]); val EVERY_LENGTH_FLAT = store_thm ("EVERY_LENGTH_FLAT", ``!l n. EVERY (\x. LENGTH x = n) l ==> (LENGTH(FLAT l) = n * LENGTH l)``, Induct THEN RW_TAC list_ss [] THEN RES_TAC THEN RW_TAC std_ss [ADD1,LEFT_ADD_DISTRIB] THEN DECIDE_TAC); val APPEND_DIV_MOD = store_thm ("APPEND_DIV_MOD", ``!r msg. 0 < r ==> (msg = TAKE ((LENGTH msg DIV r) * r) msg ++ LASTN (LENGTH msg MOD r) msg)``, PROVE_TAC[DIVISION,ADD_SYM,APPEND_TAKE_LASTN]); val Lemma1 = prove (``n' + 2 <= LENGTH l ==> (LENGTH(TAKE n' l ++ [T] ++ Zeros (LENGTH l - (n' + 2)) ++ [T]) = LENGTH l)``, RW_TAC list_ss [LengthZeros,LENGTH_TAKE]); val Lemma2 = prove (``1 < LENGTH l ==> (LENGTH(TAKE (LENGTH l - 1) l ++ [T] ++ Zeros (LENGTH l - 1) ++ [T]) = 2*LENGTH l)``, RW_TAC list_ss [LengthZeros,LENGTH_TAKE]); val Lemma3 = prove (``1 < LENGTH l ==> (LENGTH(Zeros (LENGTH l - 1) ++ [T]) = LENGTH l)``, RW_TAC list_ss [LengthZeros]); val Lemma4 = prove (``1 < LENGTH l ==> (LENGTH(TAKE (LENGTH l - 1) l ++ [T]) = LENGTH l)``, RW_TAC list_ss [LengthZeros,LENGTH_TAKE]); (* From http://keccak.noekeon.org/: Unlike SHA-1 and SHA-2, Keccak does not have the length-extension weakness, hence does not need the HMAC nested construction. Instead, MAC computation can be performed by simply prepending the message with the key. isMAC (r,c,n) f key str is true iff bitstring s is the hash of key++msg for some msg. *) val isMAC_def = Define `isMAC (r,c,n) f key s = ?msg. s = Hash (r,c,n) f (Zeros(r+c)) (key++msg)`; (* Proof that MITB_MAC computes the Keccak hash of the key prefixed to the message. *) (* MITB state invariant *) val Invariant_def = Define `(Invariant (r,c,n) f (Ready,pmem,vmem) = (?key. (LENGTH key = r) /\ (pmem = f(key++(ZEROS c)))) /\ ((vmem = Zeros(r+c)) \/ ?msg. vmem = Absorb f c (Zeros(r+c)) (Split r (Pad r msg)))) /\ (Invariant (r,c,n) f (Absorbing,pmem,vmem) = (?key. (LENGTH key = r) /\ (pmem = f(key++(ZEROS c)))) /\ (?bkl. EVERY (\bk. LENGTH bk = r) bkl /\ (vmem = Absorb f c (Zeros(r+c)) bkl))) /\ (Invariant (r,c,n) f (AbsorbEnd,pmem,vmem) = (?key. (LENGTH key = r) /\ (pmem = f(key++(ZEROS c)))) /\ (?bkl bk. EVERY (\bk. LENGTH bk = r) bkl /\ (LENGTH bk = r-1) /\ (vmem = f(Absorb f c (Zeros(r+c)) bkl XOR (TAKE (r-1) bk ++ [T] ++ ZEROS c)))))`; (* The following horrendous proof could probably be substantially cleaned up by replacing repeated sequences of inferences into proved-once lemmas. The tactics tac1-tac5 defined below are used in the proof of the theorem MITB_Invariant. *) val tac1 = Q.EXISTS_TAC `[key]` THEN RW_TAC list_ss [Absorb_def,ZerosXorLENGTH]; val tac2 = DISJ2_TAC THEN Q.EXISTS_TAC `FLAT(SNOC (TAKE n' l) bkl)` THEN ONCE_REWRITE_TAC[GSYM SNOC_LAST_Split] THEN RW_TAC list_ss [Absorb_FOLDL,FOLDL_SNOC] THEN RW_TAC list_ss [GSYM Absorb_FOLDL] THEN `n' <= LENGTH l` by DECIDE_TAC THEN IMP_RES_TAC EVERY_LENGTH_FLAT THEN `LENGTH(FLAT (SNOC (TAKE n' l) bkl)) = LENGTH bkl * LENGTH l + n'` by PROVE_TAC[FLAT_SNOC,LENGTH_TAKE,LENGTH_APPEND,MULT_SYM] THEN `2 < LENGTH l` by PROVE_TAC[GoodParameters_def] THEN `0 < LENGTH l /\ 1 < LENGTH l /\ 2 <= LENGTH l /\ n' < LENGTH l /\ n' <= LENGTH l` by DECIDE_TAC THEN `n' <> LENGTH l - 1 /\ n' + 2 <= LENGTH l` by DECIDE_TAC THEN `LENGTH l - n' - 2 = LENGTH l - (n' + 2)` by DECIDE_TAC THEN `LENGTH(FLAT (SNOC (TAKE n' l) bkl)) MOD LENGTH l = n'` by PROVE_TAC[MULT_ADD_MOD] THEN `LENGTH (Pad (LENGTH l) (FLAT (SNOC (TAKE n' l) bkl))) MOD LENGTH l = 0` by PROVE_TAC[LengthPadDivides] THEN `LAST (Split (LENGTH l) (Pad (LENGTH l) (FLAT (SNOC (TAKE n' l) bkl)))) = LASTN (LENGTH l) (Pad (LENGTH l) (FLAT (SNOC (TAKE n' l) bkl)))` by PROVE_TAC[LASTSplitLASTN1,LengthPadCor] THEN RW_TAC std_ss [] THEN `(PadZeros (LENGTH l) (FLAT (SNOC (TAKE n' l) bkl)) = LENGTH l - LENGTH (FLAT (SNOC (TAKE n' l) bkl)) MOD LENGTH l - 2)` by PROVE_TAC[PadZerosLemma2] THEN `(PadZeros (LENGTH l) (FLAT (SNOC (TAKE n' l) bkl)) = LENGTH l - n' - 2)` by PROVE_TAC[] THEN `Pad (LENGTH l) (FLAT (SNOC (TAKE n' l) bkl)) = FLAT bkl ++ TAKE n' l ++ [T] ++ Zeros (LENGTH l - (n' + 2)) ++ [T]` by PROVE_TAC[Pad_def,FLAT_SNOC] THEN `LENGTH (TAKE n' l ++ [T] ++ Zeros (LENGTH l - (n' + 2)) ++ [T]) = LENGTH l` by PROVE_TAC[Lemma1] THEN RW_TAC list_ss [] THEN `FLAT bkl ++ TAKE n' l ++ [T] ++ Zeros (LENGTH l - (n' + 2)) ++ [T] = FLAT bkl ++ (TAKE n' l ++ [T] ++ Zeros (LENGTH l - (n' + 2)) ++ [T])` by PROVE_TAC[APPEND_ASSOC] THEN POP_ASSUM(fn th => REWRITE_TAC[th]) THEN `LASTN (LENGTH l) (FLAT bkl ++ (TAKE n' l ++ [T] ++ Zeros (LENGTH l - (n' + 2)) ++ [T])) = (TAKE n' l ++ [T] ++ Zeros (LENGTH l - (n' + 2)) ++ [T])` by PROVE_TAC[LASTN_LENGTH_APPEND] THEN RW_TAC list_ss [] THEN `LENGTH l = LENGTH(TAKE n' l ++ ([T] ++ (Zeros (LENGTH l - (n' + 2)) ++ [T])))` by PROVE_TAC[APPEND_ASSOC] THEN RW_TAC std_ss [GSYM APPEND_ASSOC, FRONT_FLAT]; val tac3 = Q.EXISTS_TAC `bkl` THEN Q.EXISTS_TAC `TAKE (LENGTH l - 1) l` THEN RW_TAC arith_ss [LENGTH_TAKE,TAKE_TAKE]; val tac4 = Q.EXISTS_TAC `SNOC l bkl` THEN RW_TAC list_ss [XOREqXor,Absorb_FOLDL,FOLDL_SNOC, ZerosXorLENGTH,ZEROSEqZeros,EVERY_SNOC]; val tac5 = DISJ2_TAC THEN Q.EXISTS_TAC `FLAT(SNOC (TAKE (LENGTH key - 1) bk) bkl)` THEN ONCE_REWRITE_TAC[GSYM SNOC_LAST_Split] THEN RW_TAC list_ss [Absorb_FOLDL,FOLDL_SNOC] THEN RW_TAC list_ss [GSYM Absorb_FOLDL] THEN IMP_RES_TAC EVERY_LENGTH_FLAT THEN `LENGTH key - 1 <= LENGTH bk` by DECIDE_TAC THEN `LENGTH(FLAT (SNOC (TAKE (LENGTH key - 1) bk) bkl)) = LENGTH bkl * LENGTH key + (LENGTH key - 1)` by PROVE_TAC[FLAT_SNOC,LENGTH_TAKE,LENGTH_APPEND,MULT_SYM] THEN `2 < LENGTH key` by PROVE_TAC[GoodParameters_def] THEN `1 < LENGTH key /\ 0 < LENGTH key` by DECIDE_TAC THEN `LENGTH key - 1 < LENGTH key` by DECIDE_TAC THEN `LENGTH(FLAT (SNOC (TAKE (LENGTH key - 1) bk) bkl)) MOD LENGTH key = LENGTH key - 1` by PROVE_TAC[MULT_ADD_MOD] THEN `LENGTH (Pad (LENGTH key) (FLAT (SNOC (TAKE (LENGTH key - 1) bk) bkl))) MOD LENGTH key = 0` by PROVE_TAC[LengthPadDivides] THEN `LAST (Split (LENGTH key) (Pad (LENGTH key) (FLAT (SNOC (TAKE (LENGTH key - 1) bk) bkl)))) = LASTN (LENGTH key) (Pad (LENGTH key) (FLAT (SNOC (TAKE (LENGTH key - 1) bk) bkl)))` by PROVE_TAC[LASTSplitLASTN1,LengthPadCor] THEN RW_TAC std_ss [] THEN `PadZeros (LENGTH key) (FLAT (SNOC (TAKE (LENGTH key - 1) bk) bkl)) = LENGTH key - 1` by PROVE_TAC[PadZerosLemma1] THEN `Pad (LENGTH key) (FLAT (SNOC (TAKE (LENGTH key - 1) bk) bkl)) = FLAT bkl ++ TAKE (LENGTH key - 1) bk ++ [T] ++ Zeros (LENGTH key - 1) ++ [T]` by PROVE_TAC[Pad_def,FLAT_SNOC] THEN RW_TAC list_ss [] THEN `FLAT bkl ++ TAKE (LENGTH key - 1) bk ++ [T] ++ Zeros (LENGTH key - 1) ++ [T] = ((FLAT bkl ++ (TAKE (LENGTH key - 1) bk ++ [T]))) ++ (Zeros (LENGTH key - 1) ++ [T])` by PROVE_TAC[APPEND_ASSOC] THEN POP_ASSUM(fn th => REWRITE_TAC[th]) THEN `LASTN (LENGTH key) (((FLAT bkl ++ (TAKE (LENGTH key - 1) bk ++ [T]))) ++ (Zeros (LENGTH key - 1) ++ [T])) = Zeros (LENGTH key - 1) ++ [T]` by PROVE_TAC[LASTN_LENGTH_APPEND,Lemma3] THEN RW_TAC std_ss [] THEN `EVERY (\bk. LENGTH bk = LENGTH key) (SNOC (TAKE (LENGTH key - 1) bk ++ [T]) bkl)` by RW_TAC list_ss [Lemma4,EVERY_SNOC] THEN RW_TAC std_ss [GSYM FLAT_SNOC] THEN `LENGTH (Zeros(LENGTH key - 1) ++ [T]) = LENGTH key` by PROVE_TAC[Lemma3] THEN `FLAT (SNOC (Zeros (LENGTH key - 1) ++ [T]) (SNOC (TAKE (LENGTH key - 1) bk ++ [T]) bkl)) = FLAT (SNOC (TAKE (LENGTH key - 1) bk ++ [T]) bkl) ++ (Zeros (LENGTH key - 1) ++ [T])` by RW_TAC list_ss [FLAT_SNOC] THEN RW_TAC std_ss [FRONT_FLAT] THEN RW_TAC std_ss [SNOC_APPEND] THEN REWRITE_TAC [(SIMP_CONV std_ss [Absorb_FOLDL,GSYM SNOC_APPEND,FOLDL_SNOC] THENC SIMP_CONV std_ss [GSYM Absorb_FOLDL]) ``Absorb f c (Zeros (c + r)) (bkl ++ [bk])``]; val MITB_Invariant = store_thm ("MITB_Invariant", ``!r c n f cmd cntl pmem vmem. Invariant (r,c,n) f (cntl,pmem,vmem) /\ GoodParameters (r,c,n) /\ GoodCommand (r,c,n) cntl cmd /\ GoodState (r,c,n) (cntl,pmem,vmem) ==> Invariant (r,c,n) f (MITB_FUN (r,c,n) f (cntl,pmem,vmem) cmd)``, REPEAT GEN_TAC THEN Cases_on `cntl` THEN Cases_on `cmd` THEN RW_TAC list_ss [Invariant_def, MITB_FUN_def,LENGTH_ZEROS,LENGTH_XOR,ZEROSEqZeros,XOREqXor, GoodCommand_def,GoodState_def] THEN RW_TAC list_ss [Invariant_def, MITB_FUN_def,LENGTH_ZEROS,LENGTH_XOR,ZEROSEqZeros,XOREqXor, GoodCommand_def,GoodState_def] THEN TRY(PROVE_TAC[]) THENL [tac1,tac1,tac2,tac3,tac4,tac5]); (* Derived behaviour *) val MITB_IMP_BEH = store_thm ("MITB_IMP_BEH", ``MITB_IMP key (r,c,n) f (cntl_sig,pmem_sig,vmem_sig) (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) = GoodParameters(r,c,n) /\ (!s. LENGTH(f s) = LENGTH s) /\ (LENGTH key = r) /\ Width pmem_sig (r+c) /\ Width vmem_sig (r+c) /\ Width skip_inp 1 /\ Width move_inp 1 /\ Width block_inp r /\ (!t. size_inp t <= r) /\ Width ready_out 1 /\ Width digest_out n /\ (* .......... Unwound behaviour .......... *) ((cntl_sig 0, pmem_sig 0, vmem_sig 0) = (Ready, f(key ++ ZEROS c), ZEROS(r+c))) /\ (!t. (cntl_sig(t+1), pmem_sig(t+1), vmem_sig(t+1)) = MITB_FUN (r,c,n) f (cntl_sig t, pmem_sig t, vmem_sig t) (if skip_inp t = [T] then Skip else if move_inp t = [T] then Move else Input (block_inp t) (size_inp t))) /\ (!t. ready_out t = [cntl_sig t = Ready]) /\ (!t. digest_out t = if cntl_sig t = Ready then TAKE n (vmem_sig t) else ZEROS n)``, RW_TAC std_ss [MITB_IMP_def,REGISTER_def,MITB_CONTROL_LOGIC_def,MITB_def] THEN EQ_TAC THEN RW_TAC std_ss [] THEN RW_TAC std_ss [] THEN Q.EXISTS_TAC `\t. cntl_sig(t+1)` THEN Q.EXISTS_TAC `\t. pmem_sig(t+1)` THEN Q.EXISTS_TAC `\t. vmem_sig(t+1)` THEN FULL_SIMP_TAC arith_ss [Width_def]); val Lemma5 = prove (``!(r:num) (c:num) (n:num) (t:num). (LENGTH(block_inp t) = r) /\ (size_inp t <= r) ==> GoodCommand (r,c,n) (cntl_sig t) (if skip_inp t = [T] then Skip else if move_inp t = [T] then Move else Input (block_inp t) (size_inp t))``, RW_TAC std_ss [] THEN Cases_on `cntl_sig t` THEN RW_TAC std_ss [GoodCommand_def]); val MITB_IMP_Invariant = store_thm ("MITB_IMP_Invariant", ``!key r c n f cntl_sig pmem_sig vmem_sig skip_inp move_inp block_inp size_inp ready_out digest_out. MITB_IMP key (r,c,n) f (cntl_sig,pmem_sig,vmem_sig) (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) ==> !t. Invariant (r,c,n) f (cntl_sig t,pmem_sig t,vmem_sig t)``, REPEAT GEN_TAC THEN STRIP_TAC THEN Induct THEN FULL_SIMP_TAC std_ss [MITB_IMP_BEH,ADD1,Width_def,GoodState_def] THENL [RW_TAC list_ss [Invariant_def] THEN PROVE_TAC[ZEROSEqZeros], ASSUM_LIST(fn thl => ASSUME_TAC(SPEC_ALL(el 4 thl))) THEN ASSUM_LIST (fn thl => ASSUME_TAC (SIMP_RULE std_ss [el 11 thl,el 12 thl](SPEC_ALL Lemma5))) THEN `(LENGTH(pmem_sig t) = LENGTH key + c) /\ (LENGTH(vmem_sig t) = LENGTH key + c)` by RW_TAC std_ss [] THEN `GoodState (r,c,n) (cntl_sig t,pmem_sig t,vmem_sig t)` by RW_TAC std_ss [GoodState_def] THEN IMP_RES_TAC MITB_Invariant]); val TAKE_ZEROS = store_thm ("TAKE_ZEROS", ``!m n. m <= n ==> (TAKE m (Zeros n) = Zeros m)``, REPEAT Induct THEN RW_TAC list_ss [TAKE,Zeros_def]); val DigestLemma = prove (``!r c n. GoodParameters(r,c,n) ==> (TAKE n (Zeros (r + c)) = Zeros n)``, RW_TAC list_ss [GoodParameters_def] THEN `n <= c + r` by DECIDE_TAC THEN PROVE_TAC[TAKE_ZEROS]); (* Verification that only hashes or zeros appear on digest output *) val MITB_IMP_SAFE = store_thm ("MITB_IMP_SAFE", ``!key r c n f cntl_sig pmem_sig vmem_sig skip_inp move_inp block_inp size_inp ready_out digest_out. MITB_IMP key (r,c,n) f (cntl_sig,pmem_sig,vmem_sig) (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) ==> !t. if ready_out t = [T] then (digest_out t = Zeros n) \/ (?msg. digest_out t = Hash (r,c,n) f (Zeros(r+c)) msg) else digest_out t = Zeros n``, RW_TAC std_ss [] THEN IMP_RES_TAC MITB_IMP_Invariant THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) THEN Cases_on `cntl_sig t` THEN FULL_SIMP_TAC (srw_ss()) [MITB_IMP_BEH,Invariant_def,Hash_def, Output_def,ZEROSEqZeros,DigestLemma] THEN PROVE_TAC[]); val MITB_DEV_SAFE = store_thm ("MITB_DEV_SAFE", ``!key r c n f skip_inp move_inp block_inp size_inp ready_out digest_out. MITB_DEV key (r,c,n) f (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) ==> !t. if ready_out t = [T] then (digest_out t = Zeros n) \/ (?msg. digest_out t = Hash (r,c,n) f (Zeros(r+c)) msg) else digest_out t = Zeros n``, RW_TAC std_ss [MITB_DEV_def,MITB_IMP_SAFE] THEN IMP_RES_TAC MITB_IMP_SAFE THEN RW_TAC std_ss []); (* Verify that iterated MITB_FUN implements the sponge function Absorb f c initial_state Split r (Pad r msg) *) val MITB_AbsorbIter_def = Define `(MITB_AbsorbIter (r,c,n) f (cntl,pmem,vmem) [] = if cntl = Ready then (Ready,pmem,vmem) else if cntl = AbsorbEnd then (Ready,pmem,f(vmem XOR (ZEROS(r-1) ++ [T] ++ ZEROS c))) else (Ready,pmem,f(vmem XOR ([T] ++ ZEROS(r-2) ++ [T] ++ ZEROS c)))) /\ (MITB_AbsorbIter (r,c,n) f (cntl,pmem,vmem) ((bk,len)::bll) = if cntl = Ready then (Ready,pmem,vmem) else if cntl = AbsorbEnd then (Ready,pmem,f(vmem XOR (ZEROS(r-1) ++ [T] ++ ZEROS c))) else MITB_AbsorbIter (r,c,n) f (MITB_FUN (r,c,n) f (Absorbing,pmem,vmem) (Input bk len)) bll)`; val MITB_AbsorbingIter = store_thm ("MITB_AbsorbingIter", ``(MITB_AbsorbIter (r,c,n) f (Absorbing,pmem,vmem) [] = (Ready,pmem,f(vmem XOR ([T] ++ ZEROS(r-2) ++ [T] ++ ZEROS c)))) /\ (MITB_AbsorbIter (r,c,n) f (Absorbing,pmem,vmem) ((bk,len)::bll) = MITB_AbsorbIter (r,c,n) f (MITB_FUN (r,c,n) f (Absorbing,pmem,vmem) (Input bk len)) bll)``, RW_TAC (srw_ss()) [MITB_AbsorbIter_def]); val MITB_AbsorbIterLemma1 = store_thm ("MITB_AbsorbIterLemma1", ``!bll. MITB_AbsorbIter (r,c,n) f (cntl,pmem,vmem) bll = if cntl = Ready then (Ready,pmem,vmem) else if cntl = AbsorbEnd then (Ready,pmem,f(vmem XOR (ZEROS(r-1) ++ [T] ++ ZEROS c))) else if bll = [] then (Ready,pmem,f(vmem XOR ([T] ++ ZEROS(r-2) ++ [T] ++ ZEROS c))) else MITB_AbsorbIter (r,c,n) f (MITB_FUN (r,c,n) f (Absorbing,pmem,vmem) (Input (FST(HD bll)) (SND(HD bll)))) (TL bll)``, Induct THEN RW_TAC list_ss [MITB_AbsorbIter_def] THEN Cases_on `h` THEN RW_TAC list_ss [MITB_AbsorbIter_def]); val MITB_AbsorbIterLemma2 = store_thm ("MITB_AbsorbIterLemma2", ``MITB_AbsorbIter (r,c,n) f (cntl,pmem,vmem) ((bk,len)::bll) = if cntl = Ready then (Ready,pmem,vmem) else if cntl = AbsorbEnd then (Ready,pmem,f(vmem XOR (ZEROS(r-1) ++ [T] ++ ZEROS c))) else MITB_AbsorbIter (r,c,n) f (MITB_FUN (r,c,n) f (Absorbing,pmem,vmem) (Input bk len)) bll``, RW_TAC list_ss [MITB_AbsorbIterLemma1]); val PadZeros_DROP = store_thm ("PadZeros_DROP", ``!r msg. 1 < r /\ r <= LENGTH msg ==> (PadZeros r (DROP r msg) = PadZeros r msg)``, RW_TAC std_ss [PadZeros,LENGTH_DROP] THEN `0 < r` by DECIDE_TAC THEN PROVE_TAC[SUB_MOD]); (* Proof that MITB_AbsorbIter absorbs messages properly (take a long time) *) val MITB_AbsorbIter = store_thm ("MITB_AbsorbIter", ``!r msg c n f pmem vmem. (2 < r) ==> (MITB_AbsorbIter (r,c,n) f (Absorbing,pmem,vmem) (MAP (\bk. (bk, LENGTH bk)) (Split r msg)) = (Ready, pmem, Absorb f c vmem (Split r (Pad r msg))))``, recInduct(fetch "-" "Split_ind") THEN RW_TAC list_ss [] THEN RW_TAC list_ss [Once Split_def,MITB_AbsorbIter_def,Pad_def,MITB_FUN_def] THENL [ALL_TAC, `r <> 0` by DECIDE_TAC THEN `LENGTH (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = LENGTH msg + (PadZeros r msg + 2)` by SIMP_TAC list_ss [LengthZeros] THEN `~(r = 0) /\ r <= LENGTH (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T])` by DECIDE_TAC THEN `Split r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = TAKE r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) :: Split r (DROP r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]))` by RW_TAC list_ss [Once Split_def] THEN RW_TAC std_ss [Absorb_def] THEN `1 < r /\ r <= LENGTH msg` by DECIDE_TAC THEN `(msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = msg ++ ([T] ++ Zeros (PadZeros r msg) ++ [T])` by PROVE_TAC[APPEND_ASSOC] THEN RW_TAC std_ss [TAKE_APPEND1,DROP_APPEND1,ZEROSEqZeros,XOREqXor] THEN RW_TAC std_ss [GSYM APPEND_ASSOC,PadZeros_DROP]] THEN Cases_on `LENGTH msg <= r - 2` THEN RW_TAC std_ss [MITB_AbsorbIter_def] THEN ONCE_REWRITE_TAC[GSYM SNOC_LAST_Split] THEN RW_TAC list_ss [Absorb_FOLDL,FOLDL_SNOC] THEN RW_TAC list_ss [GSYM Absorb_FOLDL] THEN `LENGTH (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = LENGTH msg + (PadZeros r msg + 2)` by SIMP_TAC list_ss [LengthZeros] THENL [`1 < r /\ LENGTH msg < r /\ ~(LENGTH msg = r-1)` by DECIDE_TAC THEN `LENGTH msg MOD r = LENGTH msg` by PROVE_TAC[LESS_MOD] THEN `PadZeros r msg = r - LENGTH msg MOD r - 2` by PROVE_TAC[PadZeros] THEN `PadZeros r msg = r - LENGTH msg - 2` by PROVE_TAC[] THEN `LENGTH (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = r` by DECIDE_TAC THEN `LENGTH (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) <= r` by DECIDE_TAC THEN `Split r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = [msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]]` by PROVE_TAC[Split_def] THEN `r - (LENGTH msg + 2) = r - LENGTH msg - 2` by DECIDE_TAC THEN RW_TAC std_ss [FRONT_CONS,LAST_CONS,Absorb_def,ZEROSEqZeros,XOREqXor], `1 < r /\ LENGTH msg < r` by DECIDE_TAC THEN `LENGTH msg MOD r = LENGTH msg` by PROVE_TAC[LESS_MOD] THEN `PadZeros r msg = r - 1` by PROVE_TAC[PadZeros] THEN `LENGTH (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = 2*r` by DECIDE_TAC THEN `~((r = 0) \/ LENGTH(msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) <= r)` by DECIDE_TAC THEN `Split r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = TAKE r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) :: Split r (DROP r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]))` by PROVE_TAC[Split_def] THEN RW_TAC std_ss [] THEN `LENGTH (msg ++ [T]) = LENGTH msg + 1` by SIMP_TAC list_ss [] THEN `r <= LENGTH (msg ++ [T])` by DECIDE_TAC THEN `msg ++ [T] ++ Zeros (r - 1) ++ [T] = (msg ++ [T]) ++ (Zeros (r - 1) ++ [T])` by PROVE_TAC[APPEND_ASSOC] THEN POP_ASSUM(fn th => REWRITE_TAC[th]) THEN RW_TAC std_ss [TAKE_APPEND1] THEN `LENGTH (msg ++ [T]) = r` by DECIDE_TAC THEN `TAKE r (msg ++ [T]) = msg ++ [T]` by PROVE_TAC[TAKE_LENGTH_ID] THEN `DROP r (msg ++ [T] ++ (Zeros (r - 1) ++ [T])) = Zeros (r - 1) ++ [T]` by PROVE_TAC[DROP_LENGTH_APPEND] THEN ASM_REWRITE_TAC[] THEN `LENGTH(Zeros (r - 1) ++ [T]) = (r-1) + 1` by SIMP_TAC list_ss [LengthZeros] THEN `LENGTH(Zeros (r - 1) ++ [T]) <= r` by DECIDE_TAC THEN `Split r (Zeros (r - 1) ++ [T]) = [Zeros (r - 1) ++ [T]]` by PROVE_TAC[Split_def] THEN ASM_REWRITE_TAC [FRONT_CONS,LAST_CONS,Absorb_def,ZEROSEqZeros,XOREqXor], `0 < r /\ 1 < r /\ (LENGTH msg = r) /\ ~(LENGTH msg = r-1)` by DECIDE_TAC THEN `LENGTH msg MOD r = 0` by PROVE_TAC[DIVMOD_ID] THEN `~(LENGTH msg MOD r = r - 1)` by DECIDE_TAC THEN `PadZeros r msg = r - LENGTH msg MOD r - 2` by PROVE_TAC[PadZeros] THEN `PadZeros r msg = r - 0 - 2` by PROVE_TAC[] THEN `PadZeros r msg = r - 2` by DECIDE_TAC THEN `LENGTH (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = 2 * r` by DECIDE_TAC THEN `~((r = 0) \/ LENGTH(msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) <= r)` by DECIDE_TAC THEN `Split r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) = TAKE r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]) :: Split r (DROP r (msg ++ [T] ++ Zeros (PadZeros r msg) ++ [T]))` by PROVE_TAC[Split_def] THEN RW_TAC std_ss [] THEN `msg ++ [T] ++ Zeros (LENGTH msg - 2) ++ [T] = msg ++ ([T] ++ Zeros (LENGTH msg - 2) ++ [T])` by PROVE_TAC[APPEND_ASSOC] THEN POP_ASSUM(fn th => REWRITE_TAC[th]) THEN RW_TAC std_ss [TAKE_APPEND1,TAKE_LENGTH_ID,DROP_LENGTH_APPEND] THEN `LENGTH([T] ++ Zeros (LENGTH msg - 2) ++ [T]) = 1 + (LENGTH msg-2) + 1` by SIMP_TAC list_ss [LengthZeros] THEN `LENGTH([T] ++ Zeros (LENGTH msg - 2) ++ [T]) = LENGTH msg` by DECIDE_TAC THEN `LENGTH([T] ++ Zeros (LENGTH msg - 2) ++ [T]) <= LENGTH msg` by DECIDE_TAC THEN `Split (LENGTH msg) ([T] ++ Zeros (LENGTH msg - 2) ++ [T]) = [[T] ++ Zeros (LENGTH msg - 2) ++ [T]]` by PROVE_TAC[Split_def] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC [FRONT_CONS,LAST_CONS,Absorb_def, ZEROSEqZeros,XOREqXor,GSYM CONS_APPEND] THEN REWRITE_TAC[APPEND]]); (* Various lemmas about Split, Pad etc *) val SplitTake = store_thm ("SplitTake", ``!r msg. 0 < r ==> (Split r msg = if LENGTH msg <= r then [msg] else if LENGTH msg MOD r = 0 then (Split r (TAKE (LENGTH msg DIV r * r) msg)) else (Split r (TAKE (LENGTH msg DIV r * r) msg) ++ [LASTN (LENGTH msg MOD r) msg]))``, RW_TAC std_ss [] THEN RW_TAC std_ss [Once(ISPECL[``r:num``,``msg:bits``]APPEND_DIV_MOD)] THEN `0 < LENGTH[LASTN (LENGTH msg MOD r) msg]` by RW_TAC list_ss [] THEN ASSUME_TAC(MP (SPEC_ALL LengthSplit) (ASSUME ``0 < r``)) THENL [RW_TAC list_ss [Once Split_def], `(LENGTH msg DIV r * r = LENGTH msg) /\ LENGTH msg MOD r < r` by PROVE_TAC[DIVISION,ADD_CLAUSES] THEN RW_TAC list_ss [], `(LENGTH msg = LENGTH msg DIV r * r + LENGTH msg MOD r) /\ LENGTH msg MOD r < r` by PROVE_TAC[DIVISION] THEN `LENGTH msg DIV r * r <= LENGTH msg` by DECIDE_TAC THEN `LENGTH(TAKE (LENGTH msg DIV r * r) msg) = LENGTH msg DIV r * r` by PROVE_TAC[LENGTH_TAKE] THEN `LENGTH(TAKE (LENGTH msg DIV r * r) msg) MOD r = 0` by PROVE_TAC[MOD_EQ_0] THEN `LENGTH msg MOD r <= LENGTH msg` by DECIDE_TAC THEN `LENGTH(LASTN (LENGTH msg MOD r) msg) = LENGTH msg MOD r` by PROVE_TAC[LENGTH_LASTN] THEN `LENGTH(LASTN (LENGTH msg MOD r) msg) <= r` by DECIDE_TAC THEN `[LASTN (LENGTH msg MOD r) msg] = Split r (LASTN (LENGTH msg MOD r) msg)` by RW_TAC list_ss [Once Split_def] THEN `r <= LENGTH msg` by DECIDE_TAC THEN `0 < LENGTH msg DIV r` by PROVE_TAC[LESS_DIV] THEN `?d. LENGTH msg DIV r = 1 + d` by COOPER_TAC THEN `LENGTH msg DIV r * r = r + d * r` by PROVE_TAC[MULT_LEFT_1,RIGHT_ADD_DISTRIB] THEN `r <= LENGTH(TAKE (LENGTH msg DIV r * r) msg)` by DECIDE_TAC THEN `0 < LENGTH (LASTN (LENGTH msg MOD r) msg)` by DECIDE_TAC THEN `Split r msg = Split r (TAKE (LENGTH msg DIV r * r) msg) ++ Split r (LASTN (LENGTH msg MOD r) msg)` by PROVE_TAC[SplitAppend,APPEND_DIV_MOD] THEN PROVE_TAC[]]); val SplitPadLemma4A = prove (``!r msg. 2 < r /\ msg <> [] /\ LENGTH msg MOD r <> 0 ==> (msg ++ [T] ++ Zeros (r - (LENGTH msg MOD r + 2)) ++ [T] = TAKE (LENGTH msg DIV r * r) msg ++ LAST(Split r msg) ++ [T] ++ Zeros (r - (LENGTH msg MOD r + 2)) ++ [T])``, RW_TAC std_ss [] THEN `0 < r /\ 1 < r` by DECIDE_TAC THEN `LENGTH msg MOD r + LENGTH msg DIV r * r = LENGTH msg` by PROVE_TAC[DIVISION,ADD_SYM] THEN IMP_RES_TAC (ISPECL [``LENGTH(msg:bits) MOD r``, ``LENGTH(msg:bits) DIV r * r``,``msg:bits``] APPEND_TAKE_LASTN) THEN RW_TAC std_ss [LASTSplitLASTN]); val FrontSplit = store_thm ("FrontSplit", ``!r msg. 0 < r /\ r < LENGTH msg /\ LENGTH msg MOD r <> 0 ==> (FRONT(Split r msg) = Split r (TAKE (LENGTH msg DIV r * r) msg))``, RW_TAC std_ss [Once SplitTake] THEN IMP_RES_TAC(DECIDE ``m <= n /\ n < m ==> F``) THEN PROVE_TAC[SNOC_APPEND,FRONT_SNOC]); val SplitPadLemma4 = store_thm ("SplitPadLemma4", ``!r msg. 2 < r /\ r < LENGTH msg /\ 0 < LENGTH msg MOD r /\ LENGTH msg MOD r <= r-2 ==> (Split r (Pad r msg) = FRONT(Split r msg) ++ [LAST(Split r msg) ++ [T] ++ Zeros(r - (LENGTH msg MOD r + 2)) ++ [T]])``, RW_TAC list_ss [Pad_def] THEN `0 < r /\ 1 < r /\ LENGTH msg MOD r <> r - 1` by DECIDE_TAC THEN `PadZeros r msg = r - LENGTH msg MOD r - 2` by PROVE_TAC[PadZerosLemma2] THEN RW_TAC list_ss [] THEN `Split r msg <> []` by PROVE_TAC[SplitNotEmpty] THEN `LENGTH msg <> 0 /\ LENGTH msg MOD r <> 0` by DECIDE_TAC THEN `msg <> []` by PROVE_TAC[LENGTH_NIL] THEN RW_TAC std_ss [SplitPadLemma4A] THEN `LENGTH msg MOD r + LENGTH msg DIV r * r = LENGTH msg` by PROVE_TAC[DIVISION,ADD_SYM] THEN `LENGTH msg DIV r * r <= LENGTH msg` by DECIDE_TAC THEN `LENGTH(TAKE (LENGTH msg DIV r * r) msg) = LENGTH msg DIV r * r` by PROVE_TAC[LENGTH_TAKE] THEN `LENGTH((TAKE (LENGTH msg DIV r * r) msg)) MOD r = 0` by PROVE_TAC[MOD_EQ_0] THEN `r <= LENGTH msg` by DECIDE_TAC THEN `0 < LENGTH msg DIV r` by PROVE_TAC[LESS_DIV] THEN `?d. LENGTH msg DIV r = 1 + d` by COOPER_TAC THEN `LENGTH msg DIV r * r = r + d * r` by PROVE_TAC[MULT_LEFT_1,RIGHT_ADD_DISTRIB] THEN `r <= LENGTH msg DIV r * r` by DECIDE_TAC THEN `r <= LENGTH((TAKE (LENGTH msg DIV r * r) msg))` by PROVE_TAC[] THEN REWRITE_TAC[GSYM APPEND_ASSOC] THEN `0 < LENGTH (LAST (Split r msg) ++ ([T] ++ (Zeros (r - (LENGTH msg MOD r + 2)) ++ [T])))` by RW_TAC list_ss [] THEN `(Split r (TAKE (LENGTH msg DIV r * r) msg ++ (LAST (Split r msg) ++ ([T] ++ (Zeros (r - (LENGTH msg MOD r + 2)) ++ [T])))) = Split r (TAKE (LENGTH msg DIV r * r) msg) ++ Split r (LAST (Split r msg) ++ ([T] ++ (Zeros (r - (LENGTH msg MOD r + 2)) ++ [T]))))` by PROVE_TAC [ISPECL [``r:num``, ``TAKE (LENGTH(msg:bits) DIV r * r) msg``, ``(LAST (Split r msg) ++ ([T] ++ (Zeros (r - (LENGTH msg MOD r + 2)) ++ [T])))``] SplitAppend] THEN POP_ASSUM(fn th => REWRITE_TAC[th]) THEN `FRONT (Split r msg) = Split r (TAKE (LENGTH msg DIV r * r) msg)` by PROVE_TAC[FrontSplit] THEN POP_ASSUM(fn th => REWRITE_TAC[th]) THEN REWRITE_TAC[APPEND_11] THEN `LENGTH ((LAST (Split r msg) ++ ([T] ++ (Zeros (r - (LENGTH msg MOD r + 2)) ++ [T])))) = r` by RW_TAC list_ss [LengthZeros,LengthLastSplit] THEN RW_TAC list_ss [Once Split_def]); val AbsorbSplitPadShort2 = store_thm ("AbsorbSplitPadShort2", ``!r msg. 2 < r /\ r < LENGTH msg /\ 0 < LENGTH msg MOD r /\ LENGTH msg MOD r <= r-2 ==> (Absorb f c s (Split r (Pad r msg)) = f(Absorb f c s (FRONT (Split r msg)) Xor (LAST (Split r msg) ++ [T] ++ Zeros (r - (LENGTH msg MOD r + 2)) ++ [T] ++ Zeros c)))``, RW_TAC list_ss [SplitPadLemma4,Absorb_APPEND,Absorb_def]); val SplitPadLemma5 = store_thm ("SplitPadLemma5", ``!r msg. 2 < r /\ msg <> [] /\ (LENGTH msg MOD r =0) ==> (Split r (Pad r msg) = Split r msg ++ [[T] ++ Zeros(r - 2) ++ [T]])``, RW_TAC list_ss [Pad_def] THEN `0 < r /\ 1 < r /\ LENGTH msg MOD r <> r - 1` by DECIDE_TAC THEN `PadZeros r msg = r - 2` by RW_TAC arith_ss [PadZerosLemma2] THEN RW_TAC list_ss [] THEN `?d. LENGTH msg = d * r` by PROVE_TAC [MOD_EQ_0_DIVISOR] THEN Cases_on `d = 0` THENL [RW_TAC arith_ss [] THEN FULL_SIMP_TAC arith_ss [LENGTH_NIL], ALL_TAC] THEN `?n. 1 + n = d` by COOPER_TAC THEN `LENGTH msg = (1 + n) * r` by PROVE_TAC[RIGHT_ADD_DISTRIB] THEN RW_TAC arith_ss [] THEN FULL_SIMP_TAC std_ss [RIGHT_ADD_DISTRIB,MULT_CLAUSES] THEN `r <= LENGTH msg` by DECIDE_TAC THEN REWRITE_TAC[GSYM APPEND_ASSOC] THEN `0 < LENGTH([T] ++ (Zeros (r - 2) ++ [T]))` by RW_TAC list_ss [] THEN `Split r (msg ++ ([T] ++ (Zeros (r - 2) ++ [T]))) = Split r msg ++ Split r ([T] ++ (Zeros (r - 2) ++ [T]))` by PROVE_TAC [ISPECL [``r:num``,``msg:bits``,``([T] ++ (Zeros (r - 2) ++ [T]))``] SplitAppend] THEN POP_ASSUM(fn th => REWRITE_TAC[th]) THEN REWRITE_TAC[APPEND_11] THEN `LENGTH([T] ++ (Zeros (r - 2) ++ [T])) = r` by RW_TAC list_ss[LengthZeros] THEN RW_TAC list_ss [Once Split_def]); val AbsorbSplitPadFull = store_thm ("AbsorbSplitPadFull", ``!r msg. 2 < r /\ msg <> [] /\ (LENGTH msg MOD r = 0) ==> (Absorb f c s (Split r (Pad r msg)) = f (f(Absorb f c s (FRONT (Split r msg)) Xor (LAST (Split r msg) ++ Zeros c)) Xor (T::(Zeros (r - 2) ++ [T] ++ Zeros c))))``, RW_TAC list_ss [SplitPadLemma5,Absorb_APPEND,Absorb_def] THEN RW_TAC list_ss [AbsorbFrontLast]); val SplitPadLemma6A = prove (``!r msg. 2 < r /\ msg <> [] /\ (LENGTH msg MOD r = r-1) ==> (msg ++ [T] ++ Zeros (r - 1) ++ [T] = TAKE (LENGTH msg DIV r * r) msg ++ LAST(Split r msg) ++ [T] ++ Zeros (r - 1) ++ [T])``, RW_TAC std_ss [] THEN `0 < r /\ 1 < r` by DECIDE_TAC THEN `LENGTH msg MOD r + LENGTH msg DIV r * r = LENGTH msg` by PROVE_TAC[DIVISION,ADD_SYM] THEN IMP_RES_TAC (ISPECL [``LENGTH(msg:bits) MOD r``, ``LENGTH(msg:bits) DIV r * r``,``msg:bits``] APPEND_TAKE_LASTN) THEN RW_TAC list_ss [LASTSplitLASTN] THEN PROVE_TAC[MULT_SYM]); val APPEND2 = store_thm ("APPEND2", ``!l x y. l ++ [x;y] = l ++ ([x] ++ [y])``, Induct THEN RW_TAC list_ss []); val SplitPadLemma6 = store_thm ("SplitPadLemma6", ``!r msg. 2 < r /\ r < LENGTH msg /\ (LENGTH msg MOD r = r-1) ==> (Split r (Pad r msg) = FRONT(Split r msg) ++ [(LAST(Split r msg) ++ [T]); (Zeros(r - 1) ++ [T])])``, RW_TAC list_ss [Pad_def] THEN `0 < r /\ 1 < r /\ 0 < LENGTH msg MOD r /\ LENGTH msg <> 0` by DECIDE_TAC THEN `PadZeros r msg = r - 1` by PROVE_TAC[PadZerosLemma1] THEN RW_TAC list_ss [] THEN `Split r msg <> []` by PROVE_TAC[SplitNotEmpty] THEN `msg <> []` by PROVE_TAC[LENGTH_NIL] THEN RW_TAC std_ss [SplitPadLemma6A] THEN `LENGTH msg MOD r + LENGTH msg DIV r * r = LENGTH msg` by PROVE_TAC[DIVISION,ADD_SYM] THEN `LENGTH msg DIV r * r <= LENGTH msg` by DECIDE_TAC THEN `LENGTH(TAKE (LENGTH msg DIV r * r) msg) = LENGTH msg DIV r * r` by PROVE_TAC[LENGTH_TAKE] THEN `LENGTH((TAKE (LENGTH msg DIV r * r) msg)) MOD r = 0` by PROVE_TAC[MOD_EQ_0] THEN `r <= LENGTH msg` by DECIDE_TAC THEN `0 < LENGTH msg DIV r` by PROVE_TAC[LESS_DIV] THEN `?d. LENGTH msg DIV r = 1 + d` by COOPER_TAC THEN `LENGTH msg DIV r * r = r + d * r` by PROVE_TAC[MULT_LEFT_1,RIGHT_ADD_DISTRIB] THEN `r <= LENGTH msg DIV r * r` by DECIDE_TAC THEN POP_ASSUM(fn th1 => POP_ASSUM(fn th2 => POP_ASSUM(fn th3 => ASSUME_TAC th1))) THEN `r <= LENGTH((TAKE (LENGTH msg DIV r * r) msg))` by PROVE_TAC[] THEN REWRITE_TAC[GSYM APPEND_ASSOC] THEN `0 < LENGTH(LAST(Split r msg) ++ ([T] ++ (Zeros (r - 1) ++ [T])))` by RW_TAC list_ss [] THEN `(Split r (TAKE (LENGTH msg DIV r * r) msg ++ (LAST (Split r msg) ++ ([T] ++ (Zeros (r - 1) ++ [T])))) = Split r (TAKE (LENGTH msg DIV r * r) msg) ++ Split r (LAST (Split r msg) ++ ([T] ++ (Zeros (r - 1) ++ [T]))))` by PROVE_TAC [ISPECL [``r:num``, ``TAKE (LENGTH(msg:bits) DIV r * r) msg``, ``LAST (Split r msg) ++ ([T] ++ (Zeros (r - 1) ++ [T]))``] SplitAppend] THEN POP_ASSUM(fn th => REWRITE_TAC[th]) THEN `LENGTH (LAST (Split r msg)) = r-1` by PROVE_TAC[LengthLastSplit] THEN `LENGTH(LAST(Split r msg) ++ [T]) MOD r = 0` by RW_TAC list_ss [DIVMOD_ID] THEN `r <= LENGTH(LAST(Split r msg) ++ [T])` by RW_TAC list_ss [] THEN `0 < LENGTH(Zeros (r - 1) ++ [T])` by RW_TAC list_ss [LengthZeros] THEN `LAST (Split r msg) ++ ([T] ++ (Zeros (r - 1) ++ [T])) = (LAST (Split r msg) ++ [T]) ++ (Zeros (r - 1) ++ [T])` by PROVE_TAC[APPEND_ASSOC] THEN POP_ASSUM(fn th => REWRITE_TAC[th]) THEN RW_TAC std_ss [SplitAppend] THEN `LENGTH(LAST(Split r msg) ++ [T]) <= r` by RW_TAC list_ss [] THEN `LENGTH(Zeros (r - 1) ++ [T]) <= r` by RW_TAC list_ss [LengthZeros] THEN `Split r (LAST (Split r msg) ++ [T]) = [LAST (Split r msg) ++ [T]]` by RW_TAC std_ss [Once Split_def] THEN `Split r (Zeros (r - 1) ++ [T]) = [Zeros (r - 1) ++ [T]]` by RW_TAC std_ss [Once Split_def] THEN RW_TAC std_ss [APPEND2,APPEND_11] THEN `LENGTH msg MOD r <> 0` by DECIDE_TAC THEN RW_TAC std_ss [FrontSplit]); val AbsorbSplitPadShort1Lemma1 = store_thm ("AbsorbSplitPadShort1Lemma1", ``!r msg. 2 < r /\ r < LENGTH msg /\ (LENGTH msg MOD r = r - 1) ==> (Absorb f c s (Split r (Pad r msg)) = f(f(Absorb f c s (FRONT (Split r msg)) Xor (TAKE (r - 1) (LAST (Split r msg)) ++ [T] ++ Zeros c)) Xor (Zeros (r - 1) ++ [T] ++ Zeros c)))``, RW_TAC list_ss [SplitPadLemma6,Absorb_APPEND,Absorb_def] THEN `1 < r` by DECIDE_TAC THEN `LENGTH msg <> 0` by DECIDE_TAC THEN `msg <> []` by PROVE_TAC[LENGTH_NIL] THEN `LENGTH msg MOD r <> 0` by DECIDE_TAC THEN `LENGTH (LAST (Split r msg)) = LENGTH msg MOD r` by PROVE_TAC[LENGTH_LAST_Split] THEN `r - 1 = LENGTH (LAST (Split r msg))` by DECIDE_TAC THEN POP_ASSUM(fn th => REWRITE_TAC[th,TAKE_LENGTH_ID])); val AbsorbSplitPadShort1Lemma2 = store_thm ("AbsorbSplitPadShort1Lemma2", ``!r msg. 2 < r /\ (LENGTH msg = r - 1) ==> (Absorb f c s (Split r (Pad r msg)) = f(f(Absorb f c s (FRONT (Split r msg)) Xor (TAKE (r - 1) (LAST (Split r msg)) ++ [T] ++ Zeros c)) Xor (Zeros (r - 1) ++ [T] ++ Zeros c)))``, RW_TAC list_ss [SplitPadLemma2,Absorb_APPEND,Absorb_def] THEN `1 < r` by DECIDE_TAC THEN `LENGTH msg <= r` by DECIDE_TAC THEN `Split r msg = [msg]` by PROVE_TAC[Split_def] THEN `TAKE (r-1) msg = msg` by PROVE_TAC[TAKE_LENGTH_ID] THEN RW_TAC list_ss [Absorb_def]); val AbsorbSplitPadShort1 = store_thm ("AbsorbSplitPadShort1", ``!r msg. 2 < r /\ (LENGTH msg MOD r = r - 1) ==> (Absorb f c s (Split r (Pad r msg)) = f(f(Absorb f c s (FRONT (Split r msg)) Xor (TAKE (r - 1) (LAST (Split r msg)) ++ [T] ++ Zeros c)) Xor (Zeros (r - 1) ++ [T] ++ Zeros c)))``, REPEAT GEN_TAC THEN Cases_on `r < LENGTH msg` THEN RW_TAC std_ss [AbsorbSplitPadShort1Lemma1] THEN `LENGTH msg <= r` by DECIDE_TAC THEN `0 < r` by DECIDE_TAC THEN Cases_on `LENGTH msg = r` THEN FULL_SIMP_TAC arith_ss [DIVMOD_ID,AbsorbSplitPadShort1Lemma2]); (* Some LTL-style properties on traces modelled as functions on num *) val _ = set_fixity "|=" (Infixr 325); val Models_def = xDefine "Models" `$|= (dev : 'state_sigs -> 'port_sigs -> bool) phi = !ssigs psigs. dev ssigs psigs ==> phi(ssigs,psigs)`; (* Specific types for MITB: 'state_sigs |-> state_sigs 'port_sigs |-> port_sigs *) val _ = type_abbrev ("state_sigs", ``:(num -> control) # (* cntl_sig *) (num -> bits) # (* pmem_sig *) (num -> bits)``); (* vmem_sig *) val _ = type_abbrev ("port_sigs", ``:(num -> bits) # (* skip_inp *) (num -> bits) # (* move_inp *) (num -> bits) # (* block_inp *) (num -> num) # (* size_inp *) (num -> bits) # (* ready_out *) (num -> bits)``); (* digest_out *) val _ = type_abbrev ("inp_sigs", ``:(num -> bits) # (* skip_inp *) (num -> bits) # (* move_inp *) (num -> bits) # (* block_inp *) (num -> num)``); (* size_inp *) val _ = type_abbrev ("out_sigs", ``:(num -> bits) # (* ready_out *) (num -> bits)``); (* digest_out *) (* Explode quantified pair variables ssigs and psigs *) val Models_MITB = store_thm ("Models_MITB", ``$|= (dev:state_sigs->port_sigs->bool) phi = !cntl_sig pmem_sig vmem_sig skip_inp move_inp block_inp size_inp ready_out digest_out. dev (cntl_sig,pmem_sig,vmem_sig) (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) ==> phi((cntl_sig,pmem_sig,vmem_sig), (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out))``, RW_TAC std_ss [Models_def,FORALL_PROD]); (* Lifted Boolean operators *) val BOOL_def = Define `BOOL b sigs = b`; val NOT_def = Define `NOT phi sigs = ~(phi sigs)`; val _ = set_fixity "AND" (Infixr 655); val AND_def = Define `$AND phi1 phi2 sigs = (phi1 sigs /\ phi2 sigs)`; (* Associativity and commutativity *) val AND_ASSOC = store_thm ("AND_ASSOC", ``!phi1 phi2 phi3. (phi1 AND phi2) AND phi3 = phi1 AND phi2 AND phi3``, RW_TAC std_ss [FUN_EQ_THM,AND_def] THEN PROVE_TAC[]); val AND_SYM = store_thm ("AND_SYM", ``!phi1 phi2. phi1 AND phi2 = phi2 AND phi1``, RW_TAC std_ss [FUN_EQ_THM,AND_def] THEN PROVE_TAC[]); val _ = set_fixity "OR" (Infixr 645); val OR_def = Define `$OR phi1 phi2 sigs = (phi1 sigs \/ phi2 sigs)`; (* Associativity and commutativity *) val OR_ASSOC = store_thm ("OR_ASSOC", ``!phi1 phi2 phi3. (phi1 OR phi2) OR phi3 = phi1 OR phi2 OR phi3``, RW_TAC std_ss [FUN_EQ_THM,OR_def] THEN PROVE_TAC[]); val OR_COMM = store_thm ("OR_COMM", ``!phi1 phi2. phi1 OR phi2 = phi2 OR phi1``, RW_TAC std_ss [FUN_EQ_THM,OR_def] THEN PROVE_TAC[]); val _ = set_fixity "IMPLIES" (Infixr 635); val IMPLIES_def = Define `$IMPLIES phi1 phi2 sigs = (phi1 sigs ==> phi2 sigs)`; val _ = set_fixity "IFF" (Infixr 625); val IFF_def = Define `$IFF phi1 phi2 sigs = (phi1 sigs = phi2 sigs)`; (* Lifted quantifiers (rigid) *) val _ = new_binder("ALL",``:('a -> 'b -> bool) -> 'b -> bool``); val ALL_def = Define `$ALL bdy sigs = !x. bdy x sigs`; val _ = new_binder("EXIST",``:('a -> 'b -> bool) -> 'b -> bool``); val EXIST_def = Define `$EXIST bdy sigs = ?x. bdy x sigs`; (* Temporal operators *) (* Chop the first n elements off a signal - like TAKE on lists *) val Chop_def = Define `(Chop 0 sig = sig) /\ (Chop (SUC n) sig = Chop n (\t. sig (t + 1)))`; (* Elementary properties of Chop *) val Chop = store_thm ("Chop", ``!n sig. Chop n sig = \t. sig(t+n)``, Induct THEN RW_TAC arith_ss [Chop_def,ETA_AX,FUN_EQ_THM, DECIDE ``n + (t + 1) = t + SUC n``]); val ChopRec = store_thm ("ChopRec", ``!n sig. Chop n sig = if n = 0 then sig else Chop (n-1) (\t. sig (t + 1))``, Induct THEN RW_TAC arith_ss [Chop_def]); val Chop0 = store_thm ("Chop0", ``!n sig. Chop n sig 0 = sig n``, Induct THEN RW_TAC std_ss [GSYM ADD1,Chop_def]); val Chop1 = store_thm ("Chop1", ``!sig. Chop 1 sig = \t. sig(t+1)``, REWRITE_TAC [ONE,Chop_def]); val Chop_SUC = store_thm ("Chop_SUC", ``!n sig. (\t. Chop n sig (SUC t)) = Chop n (\t. sig (t + 1))``, SIMP_TAC std_ss [FUN_EQ_THM] THEN Induct THEN RW_TAC std_ss [GSYM ADD1,Chop_def]); val ChopChop = store_thm ("ChopChop", ``!m n sig. Chop m (Chop n sig) = Chop (m + n) sig``, SIMP_TAC std_ss [FUN_EQ_THM] THEN Induct THEN RW_TAC std_ss [GSYM ADD1,Chop_def] THEN POP_ASSUM (fn th => ASSUME_TAC(SIMP_RULE std_ss [Chop_def] (SPEC ``SUC n`` th))) THEN RW_TAC std_ss [Chop_SUC, DECIDE ``m + SUC n = SUC m + n``]); (* Chop the first n elements off all signals in a (ssigs,psigs) pair *) val ChopAll_def = Define `ChopAll n ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = ((Chop n cntl_sig,Chop n pmem_sig,Chop n vmem_sig), (Chop n skip_inp,Chop n move_inp,Chop n block_inp, Chop n size_inp,Chop n ready_out,Chop n digest_out))`; (* Elementary properties of ChopChop *) val ChopAll0 = store_thm ("ChopAll0", ``!sigs. ChopAll 0 sigs = sigs``, SIMP_TAC std_ss [FORALL_PROD,ChopAll_def,Chop_def]); val ChopAllChopAll = store_thm ("ChopAllChopAll", ``!m n sigs. ChopAll m (ChopAll n sigs) = ChopAll (m + n) sigs``, SIMP_TAC std_ss [FUN_EQ_THM,FORALL_PROD,ChopAll_def,ChopChop]); (* NEXT operator (sometimes called "X") *) val NEXT_def = Define `NEXT phi sigs = phi(ChopAll 1 sigs)`; (* Sanity checking lemma on iterated NEXTs *) val NEXT_AND = store_thm ("NEXT_AND", ``!phi1 phi2. NEXT phi1 AND NEXT(NEXT phi2) = NEXT(phi1 AND NEXT phi2)``, RW_TAC std_ss [FUN_EQ_THM,NEXT_def,AND_def]); (* Iterate NEXT a given number of times *) val NEXTN_def = Define `(NEXTN 0 phi = phi) /\ (NEXTN (SUC n) phi = NEXT (NEXTN n phi))`; (* Not used Apply property generating function psi to successive elements of a list on successive cycles val NEXTITER_def = Define `(NEXTITER [] psi = BOOL T) /\ (NEXTITER (x::xl) psi = NEXT (psi x AND NEXTITER xl psi))`; *) val SOMETIME_def = Define `SOMETIME phi sigs = ?t. phi(ChopAll t sigs)`; val ALWAYS_def = Define `ALWAYS phi sigs = !t. phi(ChopAll t sigs)`; (* Traditional UNTIL *) val _ = set_fixity "UNTIL" (Infixr 625); val UNTIL_def = Define `$UNTIL phi1 phi2 sigs = ?t1. phi2(ChopAll t1 sigs) /\ !t2. t2 < t1 ==> phi1(ChopAll t2 sigs)`; (* Clocked UNTIL (in paper this is written phi1 UNTILN(n) phi2), but here I can only get the parser to support uninfixed: UNTIL(n) phi1 phi2) *) val UNTILN_def = Define `(UNTILN 0 phi1 phi2 = phi2) /\ (UNTILN (SUC n) phi1 phi2 = phi1 AND NEXT(UNTILN n phi1 phi2))`; val UNTIL_IMP_UNTILN = store_thm ("UNTIL_IMP_UNTILN", ``!sigs phi1 phi2. (phi1 UNTIL phi2) sigs ==> (EXIST n. UNTILN n phi1 phi2) sigs``, RW_TAC std_ss [UNTIL_def,UNTILN_def,EXIST_def] THEN Q.EXISTS_TAC `t1` THEN RW_TAC std_ss [] THEN ASSUM_LIST(fn thl => UNDISCH_TAC(concl(el 1 thl))) THEN ASSUM_LIST(fn thl => UNDISCH_TAC(concl(el 1 thl))) THEN SPEC_TAC (``sigs :state_sigs # port_sigs``, ``sigs :state_sigs # port_sigs``) THEN Induct_on `t1` THEN RW_TAC arith_ss [UNTILN_def,ChopAll0,ChopAll_def,Chop_def,AND_def] THENL [POP_ASSUM (fn th => REWRITE_TAC[SIMP_RULE arith_ss [ChopAll0] (SPEC ``0`` th)]), FULL_SIMP_TAC std_ss [NEXT_def] THEN ASSUM_LIST (fn thl => ASSUME_TAC(Q.SPEC `ChopAll 1 sigs` (el 3 thl))) THEN FULL_SIMP_TAC std_ss [ADD1,ChopAllChopAll]]); val UNTILN_IMP_UNTIL = store_thm ("UNTILN_IMP_UNTIL", ``!sigs phi1 phi2. (EXIST n. UNTILN n phi1 phi2) sigs ==> (phi1 UNTIL phi2) sigs``, RW_TAC std_ss [UNTIL_def,UNTILN_def,EXIST_def] THEN Q.EXISTS_TAC `n` THEN ASSUM_LIST(fn thl => UNDISCH_TAC(concl(el 1 thl))) THEN SPEC_TAC (``sigs :state_sigs # port_sigs``, ``sigs :state_sigs # port_sigs``) THEN Induct_on `n` THEN RW_TAC arith_ss [UNTILN_def,ChopAll0,ChopAll_def,Chop_def,AND_def,NEXT_def] THENL [ASSUM_LIST (fn thl => ASSUME_TAC(Q.SPEC `ChopAll 1 sigs` (el 3 thl))) THEN FULL_SIMP_TAC std_ss [ADD1,ChopAllChopAll], ASSUM_LIST (fn thl => ASSUME_TAC(Q.SPEC `ChopAll 1 sigs` (el 4 thl))) THEN FULL_SIMP_TAC std_ss [ADD1,ChopAllChopAll] THEN `!t2. t2 < n ==> phi1 (ChopAll (t2 + 1) sigs)` by RES_TAC THEN Cases_on `t2` THEN FULL_SIMP_TAC arith_ss [ChopAll0] THEN `n' < n` by DECIDE_TAC THEN PROVE_TAC[ADD1]]); val UNTIL_UNTILN = store_thm ("UNTIL_UNTILN", ``!phi1 phi2. phi1 UNTIL phi2 = EXIST n. UNTILN n phi1 phi2``, SIMP_TAC std_ss [FUN_EQ_THM] THEN RW_TAC std_ss [] THEN EQ_TAC THEN RW_TAC std_ss [UNTIL_IMP_UNTILN,UNTILN_IMP_UNTIL]); (* MITB-specific operators *) (* val readyOutAlt_def = Define `readyOutAlt b ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp) : inp_sigs) = ((cntl_sig 0 = Ready) = b)`; val readyOut = store_thm ("readyOut", ``!n b. readyOutAlt b = AddOutputs n (readyOut b)``, RW_TAC std_ss [FUN_EQ_THM] THEN `?cntl_sig pmem_sig vmem_sig skip_inp move_inp block_inp size_inp. x = ((cntl_sig,pmem_sig,vmem_sig),(skip_inp,move_inp,block_inp,size_inp))` by METIS_TAC[PAIR] THEN RW_TAC std_ss [AddOutputs_def,readyOutAlt_def,readyOut_def]); *) val readyOut_def = Define `readyOut b ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (ready_out 0 = [b])`; val digestOut_def = Define `digestOut bits ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (digest_out 0 = bits)`; (* val digestOutAlt_def = Define `digestOutAlt n b ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp) : inp_sigs) = ((if cntl_sig 0 = Ready then TAKE n (vmem_sig 0) else Zeros n) = b)`; val digestOut = store_thm ("digestOut", ``!n b. digestOutAlt n b = AddOutputs n (digestOut b)``, RW_TAC std_ss [FUN_EQ_THM] THEN `?cntl_sig pmem_sig vmem_sig skip_inp move_inp block_inp size_inp. x = ((cntl_sig,pmem_sig,vmem_sig),(skip_inp,move_inp,block_inp,size_inp))` by METIS_TAC[PAIR] THEN RW_TAC std_ss [AddOutputs_def,digestOutAlt_def,digestOut_def]); val digestOutAlt_def = Define `digestOutAlt n b ((skip_inp,move_inp,block_inp,size_inp) : inp_sigs, (cntl_sig,pmem_sig,vmem_sig) : state_sigs) = ((if cntl_sig 0 = Ready then TAKE n (vmem_sig 0) else Zeros n) = b)`; val digestOut = store_thm ("digestOut", ``!n b. digestOutAlt n b = ConvertPred n (digestOut b)``, RW_TAC std_ss [FUN_EQ_THM] THEN `?cntl_sig pmem_sig vmem_sig skip_inp move_inp block_inp size_inp. x = ((cntl_sig,pmem_sig,vmem_sig),(skip_inp,move_inp,block_inp,size_inp))` by METIS_TAC[PAIR] THEN RW_TAC std_ss [AddOutputs_def,digestOutAlt_def,digestOut_def]); *) val skipInp_def = Define `skipInp b ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (skip_inp 0 = [b])`; val moveInp_def = Define `moveInp b ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (move_inp 0 = [b])`; val blockInp_def = Define `blockInp bits ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (block_inp 0 = bits)`; val sizeInp_def = Define `sizeInp len ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (size_inp 0 = len)`; val cntlState_def = Define `cntlState bits ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (cntl_sig 0 = bits)`; val pmemState_def = Define `pmemState bits ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (pmem_sig 0 = bits)`; val vmemState_def = Define `vmemState bits ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (vmem_sig 0 = bits)`; (* Old version: val mitbState_def = Define `mitbState (cntl,pmem,vmem) ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (cntl_sig 0 = cntl) /\ (pmem_sig 0 = pmem) /\ (vmem_sig 0 = vmem)`; *) val mitbState_def = Define `mitbState state ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = ((cntl_sig 0, pmem_sig 0, vmem_sig 0) = state)`; (* Decode the input signals into an element of type command *) val mitbCommand_def = Define `mitbCommand cmd ((cntl_sig,pmem_sig,vmem_sig) : state_sigs, (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out) : port_sigs) = (cmd = if skip_inp 0 = [T] then Skip else if move_inp 0 = [T] then Move else Input (block_inp 0) (size_inp 0))`; (* Check mitbState is conjunction of compomponent state predicates *) val mitbState = store_thm ("mitbState", ``mitbState(cntl,pmem,vmem) = cntlState cntl AND pmemState pmem AND vmemState vmem``, RW_TAC std_ss [FUN_EQ_THM] THEN Q.SPEC_TAC(`x`,`x`) THEN SIMP_TAC std_ss [FORALL_PROD,AND_def,mitbState_def, cntlState_def,pmemState_def,vmemState_def]); (* InputBlocks, defined below, models the actions of an MITB client inputting the blocks obtained by splitting a message. MITB is transitioned from the Ready state to Absorbing by inputting Move. Data and size inputs are not read during this step. Note that padding adds an extra block [T]++Zeros(r-2)++[T] if the length of the message is divisible by r (LENGTH msg MOD r = 0) and it adds an extra block zeros(r-1)++[T] if if the length of the block is just 1 element short of being divisible by r (LENGTH msg MOD r = 1). The MITB machine handles this padding, so the client just has to input a sequence of blocks obtained by splitting a message (using Split). Such a sequence is non-empty has the form [bk0;bk1;...;bkn] where LENGTH bki = r (for 0 <= i < n) and LENGTH bkn <= r. If LENGTH bkn = n, then after absorbing all the blocks, MITB will move to state Absorbing and won't know that it is at the end of the message. The client thus has to indicate end-of-message, which is done be inputting an empty block. This is reflected in the definition of InputBlocks below. If LENGTH bkn = r-1 them MITB can tell that it is the last block in the message, but it needs an additional step to add zeros(r-1)++[T], which it does by moving into state AbsorbEnd for one cycle. The user can observe this as ready_out stays F. If LENGTH bkn < r-1 them MITB can tell that it is the last block in the message and can finish absorbing in the current cycle. The user can observe this as ready_out goes to T. Thus, to summarize: 1. splits the message into blocks of length r except, perhaps, for the last one, which may have length less than r; 2. if the last block does have length r, then an empty block is added; 3. the blocks are absorbed when ready_out is asserted, which will happen immediately after the last block being input is absorbed unless the length of this last block is exactly r-1, in which case an extra cycle is needed (i.e. a transition through state AbsorbEnd). InputBlocks, defined below, performs 1 and 2. *) val InputBlock_def = Define `InputBlock bk = blockInp bk AND sizeInp(LENGTH bk) AND skipInp F AND moveInp F`; val InputBlocks_def = Define `(InputBlocks r [] = BOOL F) (* This should not occur as Split returns a non-empty list *) /\ (InputBlocks r (bk::bkl) = if (bkl = []) then (if (LENGTH bk = r) then InputBlock bk AND NEXT(InputBlock []) else if (LENGTH bk = r-1) then InputBlock bk AND NEXT(skipInp F AND moveInp F) else InputBlock bk) else InputBlock bk AND NEXT(InputBlocks r bkl))`; val InputMessage_def = Define `InputMessage r msg = skipInp F AND moveInp T AND NEXT(InputBlocks r (Split r msg))`; (* Sanity tests: EVAL ``Split 3 []``; EVAL ``InputMessage 3 []``; EVAL ``InputMessage 3 [b1]``; EVAL ``InputMessage 3 [b1;b2]``; EVAL ``InputMessage 3 [b1;b2;b3]``; EVAL ``InputMessage 3 [b1;b2;b3;b4;b5;b6;b7;b8;b9]``; EVAL ``InputMessage 3 [b1;b2;b3;b4;b5;b6;b7;b8;b9;b10]``; EVAL ``InputMessage 3 [b1;b2;b3;b4;b5;b6;b7;b8;b9;b10;b11]``; EVAL ``InputMessage 3 [b1;b2;b3;b4;b5;b6;b7;b8;b9;b10;b11;b12]``; *) (* General tactic for "model checking" properties *) val MC_THMS = [Models_MITB,NOT_def,AND_def,OR_def,IMPLIES_def,IFF_def,BOOL_def, NEXT_def,NEXTN_def,ALWAYS_def,SOMETIME_def,UNTIL_def, ALL_def,EXIST_def,MITB_IMP_BEH,ZEROSEqZeros, ChopAll_def,Chop_def,Chop0,skipInp_def,moveInp_def,blockInp_def,sizeInp_def, readyOut_def,digestOut_def,mitbState_def,mitbCommand_def, InputBlock_def,InputBlocks_def,InputMessage_def, cntlState_def,pmemState_def,vmemState_def,ChopChop,MITB_FUN_def]; fun MC_TAC thl = RW_TAC list_ss (MC_THMS@thl); (* Verify initial state *) val MITB_INIT = store_thm ("MITB_INIT", ``MITB_IMP key (r,c,n) f |= readyOut T AND digestOut(Zeros n) AND cntlState Ready AND pmemState(f (key ++ ZEROS c)) AND vmemState(Zeros(r + c))``, MC_TAC[] THEN `n <= LENGTH key` by PROVE_TAC[GoodParameters_def] THEN `n <= c + LENGTH key` by DECIDE_TAC THEN RW_TAC std_ss [TAKE_ZEROS]); (* The next two theorems are sanity tests for the temporal quantifiers ALL and EXISTS *) val MITB_INIT_EXIST = store_thm ("MITB_INIT_EXIST", ``MITB_IMP key (r,c,n) f |= EXIST b. readyOut b``, MC_TAC[]); val MITB_INIT_NOT_ALL = store_thm ("MITB_INIT_NOT_ALL", ``MITB_IMP key (r,c,n) f |= NOT(ALL b. readyOut b)``, MC_TAC[]); (* Some temporal logic rules *) val BOOL_T_IMPLIES = store_thm ("BOOL_T_IMPLIES", ``!P. BOOL T IMPLIES P = P``, RW_TAC std_ss [FUN_EQ_THM,IMPLIES_def,BOOL_def]); val BOOL_F_IMPLIES = store_thm ("BOOL_F_IMPLIES", ``!P. BOOL F IMPLIES P = BOOL T``, RW_TAC std_ss [FUN_EQ_THM,IMPLIES_def,BOOL_def]); val BOOL_T_AND = store_thm ("BOOL_T_AND", ``!P. (BOOL T AND P = P) /\ (P AND BOOL T = P) ``, RW_TAC std_ss [FUN_EQ_THM,AND_def,BOOL_def]); val IF_IMPLIES = store_thm ("IF_IMPLIES", ``!b P Q. (if b then P else Q) = ((BOOL b IMPLIES P) AND (BOOL ~b IMPLIES Q))``, RW_TAC std_ss [FUN_EQ_THM,BOOL_def,IMPLIES_def,AND_def]); val ALWAYS_ALL = store_thm ("ALWAYS_ALL", ``!dev P. (dev |= ALWAYS(ALL x. P x)) = !x. dev |= ALWAYS(P x)``, REPEAT GEN_TAC THEN EQ_TAC THEN MC_TAC[]); val ALWAYS_BOOL_IMPLIES = store_thm ("ALWAYS_BOOL_IMPLIES", ``!dev b P. (dev |= ALWAYS(BOOL b IMPLIES P)) = b ==> dev |= ALWAYS P``, REPEAT GEN_TAC THEN EQ_TAC THEN MC_TAC[]); val ALWAYS_BOOL_AND_IMPLIES = store_thm ("ALWAYS_BOOL_AND_IMPLIES", ``!dev b P Q. (dev |= ALWAYS(BOOL b AND P IMPLIES Q)) = b ==> dev |= ALWAYS(P IMPLIES Q)``, REPEAT GEN_TAC THEN EQ_TAC THEN MC_TAC[]); val IMPLIES_IMP = store_thm ("IMPLIES_IMP", ``(dev |= P IMPLIES Q) ==> (dev |= P) ==> (dev |= Q)``, RW_TAC std_ss [Models_def,IMPLIES_def]); val IMPLIES_NEXT_IMP = store_thm ("IMPLIES_NEXT_IMP", ``!dev P Q R. (dev |= ALWAYS(P IMPLIES NEXT Q)) /\ (dev |= ALWAYS(Q IMPLIES R)) ==> (dev |= ALWAYS(P IMPLIES NEXT R))``, RW_TAC std_ss [Models_def,IMPLIES_def,ALWAYS_def,NEXT_def,ChopAllChopAll]); (* An iteration rule for NEXTN *) val ALWAYS_NEXTN_FOLDL_LEMMA = store_thm ("ALWAYS_NEXTN_FOLDL_LEMMA", ``!dev (step:'b->'a->'b) P Q. (!xl x y. dev |= ALWAYS(P(x::xl) AND Q y IMPLIES (NEXT(P xl AND Q(step y x))))) ==> (!xl y. dev |= ALWAYS ((P xl AND Q y) IMPLIES (NEXTN (LENGTH xl) (P[] AND Q(FOLDL step y xl)))))``, REPEAT GEN_TAC THEN DISCH_TAC THEN Induct THENL [MC_TAC[], RW_TAC list_ss [NEXTN_def] THEN ASSUM_LIST (fn thl => ASSUME_TAC (Q.SPECL[`xl`,`h`,`y`](el 2 thl))) THEN ASSUM_LIST (fn thl => ASSUME_TAC (Q.SPEC `(step:'b->'a->'b) y h` (el 2 thl))) THEN ASSUME_TAC (ISPECL [``dev:state_sigs -> port_sigs -> bool``, ``(P:'a list -> state_sigs # port_sigs -> bool) (h::xl) AND (Q:'b -> state_sigs # port_sigs -> bool) y``, ``(P:'a list -> state_sigs # port_sigs -> bool) xl AND (Q:'b -> state_sigs # port_sigs -> bool) ((step:'b->'a->'b) y h)``, ``NEXTN (LENGTH xl) ((P:'a list -> state_sigs # port_sigs -> bool) [] AND (Q:'b -> state_sigs # port_sigs -> bool) (FOLDL (step:'b->'a->'b) (step y h) xl))``] IMPLIES_NEXT_IMP) THEN RES_TAC]); val ALWAYS_NEXTN_FOLDL = store_thm ("ALWAYS_NEXTN_FOLDL", ``!dev step P Q. dev |= ALWAYS (ALL xl x y. P(x::xl) AND Q y IMPLIES (NEXT(P xl AND Q(step y x)))) ==> dev |= ALWAYS (ALL xl y. (P xl AND Q y) IMPLIES (NEXTN (LENGTH xl) (P[] AND Q(FOLDL step y xl))))``, RW_TAC std_ss [ALWAYS_ALL,ALWAYS_NEXTN_FOLDL_LEMMA]); val IMPLIES_EXIST_NEXT = store_thm ("IMPLIES_EXIST_NEXT", ``P xl AND Q y IMPLIES (EXIST xl y. P xl AND Q y) AND NEXT R = P xl AND Q y IMPLIES NEXT R``, RW_TAC std_ss [FUN_EQ_THM] THEN EQ_TAC THEN MC_TAC[] THEN PROVE_TAC[]); (* An iteration rule for UNTILN *) val ALWAYS_UNTILN_FOLDL_LEMMA = store_thm ("ALWAYS_UNTILN_FOLDL_LEMMA", ``!dev (step:'b->'a->'b) P Q. (!xl x y. dev |= ALWAYS(P(x::xl) AND Q y IMPLIES (NEXT(P xl AND Q(step y x))))) ==> (!xl y. dev |= ALWAYS ((P xl AND Q y) IMPLIES (UNTILN (LENGTH xl) (EXIST xl y . P xl AND Q y) (P[] AND Q(FOLDL step y xl)))))``, REPEAT GEN_TAC THEN DISCH_TAC THEN Induct THENL [MC_TAC[UNTILN_def], RW_TAC list_ss [UNTILN_def] THEN ASSUM_LIST (fn thl => ASSUME_TAC (Q.SPECL[`xl`,`h`,`y`](el 2 thl))) THEN ASSUM_LIST (fn thl => ASSUME_TAC (Q.SPEC `(step:'b->'a->'b) y h` (el 2 thl))) THEN ASSUME_TAC (ISPECL [``dev:state_sigs -> port_sigs -> bool``, ``(P:'a list -> state_sigs # port_sigs -> bool) (h::xl) AND (Q:'b -> state_sigs # port_sigs -> bool) y``, ``(P:'a list -> state_sigs # port_sigs -> bool) xl AND (Q:'b -> state_sigs # port_sigs -> bool) ((step:'b->'a->'b) y h)``, ``UNTILN (LENGTH xl) (EXIST xl y. (P:'a list -> state_sigs # port_sigs -> bool) xl AND (Q:'b -> state_sigs # port_sigs -> bool) y) ((P:'a list -> state_sigs # port_sigs -> bool) [] AND (Q:'b -> state_sigs # port_sigs -> bool) (FOLDL (step:'b->'a->'b) (step y h) xl))``] IMPLIES_NEXT_IMP) THEN RES_TAC THEN RW_TAC std_ss [IMPLIES_EXIST_NEXT]]); val ALWAYS_UNTILN_FOLDL = store_thm ("ALWAYS_UNTILN_FOLDL", ``!dev step P Q. dev |= ALWAYS (ALL xl x y. P(x::xl) AND Q y IMPLIES (NEXT(P xl AND Q(step y x)))) ==> dev |= ALWAYS (ALL xl y. (P xl AND Q y) IMPLIES UNTILN (LENGTH xl) (EXIST xl y. P xl AND Q y) (P[] AND Q(FOLDL step y xl)))``, RW_TAC std_ss [ALWAYS_ALL,ALWAYS_UNTILN_FOLDL_LEMMA]); val ALWAYS_NEXT = store_thm ("ALWAYS_NEXT", ``!dev P. dev |= ALWAYS P ==> dev |= ALWAYS(NEXT P)``, MC_TAC[]); val ALWAYS_NEXT_IMP = store_thm ("ALWAYS_NEXT_IMP", ``!dev P Q. dev |= ALWAYS(P IMPLIES Q) ==> dev |= ALWAYS(NEXT P IMPLIES NEXT Q)``, MC_TAC[]); val ALWAYS_AND1 = store_thm ("ALWAYS_AND1", ``!dev P1 P2. dev |= ALWAYS(P1 AND P2) ==> dev |= ALWAYS P1``, MC_TAC[]); val ALWAYS_AND2 = store_thm ("ALWAYS_AND2", ``!dev P1 P2. dev |= ALWAYS(P1 AND P2) ==> dev |= ALWAYS P2``, MC_TAC[]); val ALWAYS_AND1_IMPLIES = store_thm ("ALWAYS_AND1_IMPLIES", ``!dev P1 P2. dev |= ALWAYS(P1 AND P2 IMPLIES P1)``, MC_TAC[]); val ALWAYS_AND2_IMPLIES = store_thm ("ALWAYS_AND2_IMPLIES", ``!dev P1 P2. dev |= ALWAYS(P1 AND P2 IMPLIES P2)``, MC_TAC[]); val ALWAYS_AND = store_thm ("ALWAYS_AND2", ``!dev P1 P2. dev |= ALWAYS P1 ==> dev |= ALWAYS P2 ==> dev |= ALWAYS(P1 AND P2)``, MC_TAC[]); val ALWAYS_MP = store_thm ("ALWAYS_MP", ``!dev P1 P2. dev |= ALWAYS(P1 IMPLIES P2) ==> dev |= ALWAYS P1 ==> dev |= ALWAYS P2``, MC_TAC[]); val ALWAYS_IMP_TRANS = store_thm ("ALWAYS_IMP_TRANS", ``!dev P Q R. dev |= ALWAYS(P IMPLIES Q) ==> dev |= ALWAYS(Q IMPLIES R) ==> dev |= ALWAYS(P IMPLIES R)``, MC_TAC[]); val ALWAYS_IMP_TRANS_AND1 = store_thm ("ALWAYS_IMP_TRANS_AND1", ``!dev P Q1 Q2 R. dev |= ALWAYS(P IMPLIES Q1) ==> dev |= ALWAYS(Q1 AND Q2 AND Q3 IMPLIES R) ==> dev |= ALWAYS(P AND Q2 AND Q3 IMPLIES R)``, MC_TAC[]); val ALWAYS_IMP_TRANS_AND2 = store_thm ("ALWAYS_IMP_TRANS_AND2", ``dev |= ALWAYS (P IMPLIES Q) ==> dev |= ALWAYS (Q IMPLIES R) ==> dev |= ALWAYS (P IMPLIES (P AND R))``, MC_TAC[]); val ALWAYS_IMP_TRANS_AND3 = store_thm ("ALWAYS_IMP_TRANS_AND3", ``!dev P Q1 Q2 R. dev |= ALWAYS(P IMPLIES Q1) ==> dev |= ALWAYS(Q1 AND Q2 IMPLIES R) ==> dev |= ALWAYS(P AND Q2 IMPLIES R)``, MC_TAC[]); val ALWAYS_IMP_AND1 = store_thm ("ALWAYS_IMP_AND1", ``!dev Q1 Q2 R1 R2. dev |= ALWAYS(Q1 IMPLIES Q2) ==> dev |= ALWAYS(R1 IMPLIES R2) ==> dev |= ALWAYS((Q1 AND R1) IMPLIES (Q2 AND R2))``, MC_TAC[]); val ALWAYS_IMP_AND2 = store_thm ("ALWAYS_IMP_AND2", ``!dev P Q1 Q2 R1 R2. dev |= ALWAYS(Q1 IMPLIES Q2) ==> dev |= ALWAYS((P IMPLIES R1) IMPLIES (P IMPLIES R2)) ==> dev |= ALWAYS((P IMPLIES Q1 AND R1) IMPLIES (P IMPLIES Q2 AND R2))``, MC_TAC[]); val ALWAYS_IMP_NEXT_AND = store_thm ("ALWAYS_IMP_NEXT_AND", ``!dev P Q1 Q2 R. dev |= ALWAYS(P IMPLIES NEXT Q1) ==> dev |= ALWAYS(Q2 AND Q1 IMPLIES R) ==> dev |= ALWAYS(P IMPLIES NEXT(Q2 IMPLIES R))``, MC_TAC[]); val ALWAYS_IMPLIES_NEXT_AND = store_thm ("ALWAYS_IMPLIES_NEXT_AND", ``!dev P Q1 Q2. dev |= ALWAYS (P IMPLIES NEXT Q1) ==> dev |= ALWAYS((P AND NEXT Q2) IMPLIES (P AND NEXT(Q2 AND Q1)))``, MC_TAC []); val ALWAYS_IMP_REFL = store_thm ("ALWAYS_IMP_REFL", ``!dev P. dev |= ALWAYS(P IMPLIES P)``, MC_TAC[]); val ALWAYS_UNTILN_MONO1 = store_thm ("ALWAYS_UNTILN_MONO1", ``!t dev Q1 Q2. dev |= ALWAYS(Q1 IMPLIES Q2) ==> dev |= ALWAYS(UNTILN t Q1 R IMPLIES UNTILN t Q2 R)``, Induct THEN RW_TAC std_ss [UNTILN_def] THEN PROVE_TAC [ALWAYS_IMP_REFL,ALWAYS_NEXT_IMP,ALWAYS_IMP_AND1]); val ALWAYS_UNTILN_MONO2 = store_thm ("ALWAYS_UNTILN_MONO2", ``!t dev Q R1 R2. dev |= ALWAYS(R1 IMPLIES R2) ==> dev |= ALWAYS(UNTILN t Q R1 IMPLIES UNTILN t Q R2)``, Induct THEN RW_TAC std_ss [UNTILN_def] THEN PROVE_TAC [ALWAYS_IMP_REFL,ALWAYS_NEXT_IMP,ALWAYS_IMP_AND1]); val ALWAYS_IMP_UNTILN_MONO1 = store_thm ("ALWAYS_IMP_UNTILN_MONO1", ``!t dev P Q1 Q2 R. dev |= ALWAYS(Q1 IMPLIES Q2) ==> dev |= ALWAYS(P IMPLIES UNTILN t Q1 R) ==> dev |= ALWAYS(P IMPLIES UNTILN t Q2 R)``, PROVE_TAC[ALWAYS_UNTILN_MONO1,ALWAYS_IMP_TRANS]); val ALWAYS_IMP_UNTILN_MONO2 = store_thm ("ALWAYS_IMP_UNTILN_MONO2", ``!t dev P Q R1 R2. dev |= ALWAYS(R1 IMPLIES R2) ==> dev |= ALWAYS(P IMPLIES UNTILN t Q R1) ==> dev |= ALWAYS(P IMPLIES UNTILN t Q R2)``, PROVE_TAC[ALWAYS_UNTILN_MONO2,ALWAYS_IMP_TRANS]); val ALWAYS_IMP_AND = store_thm ("ALWAYS_IMP_AND", ``!dev P Q R. dev |= ALWAYS(P IMPLIES Q) ==> dev |= ALWAYS(R AND P IMPLIES R AND Q)``, MC_TAC[]); val ALWAYS_AND_NEXT_AND_IMP = store_thm ("ALWAYS_AND_NEXT_AND_IMP", ``!dev P1 P2 R1 R2 R3. dev |= ALWAYS((P1 AND P2) AND NEXT(R1 AND R2) IMPLIES (P1 AND P2) AND NEXT R3) ==> dev |= ALWAYS((P1 AND NEXT R1) AND P2 AND NEXT R2 IMPLIES (P1 AND P2) AND NEXT R3)``, MC_TAC[]); val ALWAYS_UNTILN_AND_IMP = store_thm ("ALWAYS_UNTILN_AND_IMP", ``!t P1 P2 Q1 Q2. dev |= ALWAYS ((UNTILN t P1 Q1) AND (UNTILN t P2 Q2) IMPLIES (UNTILN t (P1 AND P2) (Q1 AND Q2)))``, Induct THEN RW_TAC std_ss [UNTILN_def,ALWAYS_AND,ALWAYS_IMP_REFL] THEN `dev |= ALWAYS((P1 AND P2) AND NEXT(UNTILN t P1 Q1 AND UNTILN t P2 Q2) IMPLIES (P1 AND P2) AND NEXT(UNTILN t (P1 AND P2) (Q1 AND Q2)))` by PROVE_TAC[ALWAYS_IMP_AND,ALWAYS_NEXT_IMP] THEN IMP_RES_TAC ALWAYS_AND_NEXT_AND_IMP); val ALWAYS_UNTILN_AND = store_thm ("ALWAYS_UNTILN_AND", ``!t P1 P2 Q1 Q2. (dev |= ALWAYS(UNTILN t P1 Q1)) /\ (dev |= ALWAYS(UNTILN t P2 Q2)) ==> (dev |= ALWAYS(UNTILN t (P1 AND P2) (Q1 AND Q2)))``, RW_TAC std_ss [] THEN PROVE_TAC[ALWAYS_AND,ALWAYS_MP,ALWAYS_UNTILN_AND_IMP]); val ALWAYS_UNTILN_IMP_NEXT = store_thm ("ALWAYS_UNTILN_IMP_NEXT", ``!t dev P Q R. dev |= ALWAYS(Q IMPLIES P) ==> dev |= ALWAYS(UNTILN t P (Q AND NEXT R) IMPLIES UNTILN (t+1) P R)``, Induct THEN REWRITE_TAC [UNTILN_def,ONE,ADD_CLAUSES,ALWAYS_IMP_REFL] THENL [MC_TAC[], FULL_SIMP_TAC std_ss [UNTILN_def,GSYM ADD1] THEN RW_TAC std_ss [] THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) THEN PROVE_TAC[ALWAYS_NEXT_IMP,ALWAYS_IMP_AND1,ALWAYS_IMP_REFL]]); val ALWAYS_UNTILN_AND_IMP_NEXT = store_thm ("ALWAYS_UNTILN_AND_IMP_NEXT", ``!dev t P Q R1 R2 R3 R4. dev |= ALWAYS(R1 AND R3 IMPLIES Q) ==> dev |= ALWAYS(P IMPLIES UNTILN t Q ((R1 AND NEXT R2) AND R3)) ==> dev |= ALWAYS((R1 AND R3) IMPLIES NEXT R4) ==> dev |= ALWAYS(P IMPLIES UNTILN (t+1) Q (R2 AND R4))``, RW_TAC std_ss [] THEN `dev |= ALWAYS (P IMPLIES UNTILN t Q ((R1 AND R3) AND NEXT R2))` by PROVE_TAC[AND_ASSOC,AND_SYM] THEN PROVE_TAC [ALWAYS_AND2_IMPLIES, ALWAYS_IMPLIES_NEXT_AND, ALWAYS_UNTILN_MONO2,ALWAYS_IMP_TRANS, ALWAYS_UNTILN_IMP_NEXT]); (* Subsumed by theorem above using ALWAYS_IMP_REFL (but proved first) *) val ALWAYS_UNTILN_NEXT = store_thm ("ALWAYS_UNTILN_NEXT", ``!t dev P Q. dev |= ALWAYS(UNTILN t P (P AND NEXT Q) IMPLIES UNTILN (t+1) P Q)``, Induct THEN REWRITE_TAC [UNTILN_def,ONE,ADD_CLAUSES,ALWAYS_IMP_REFL] THEN FULL_SIMP_TAC std_ss [UNTILN_def,GSYM ADD1] THEN RW_TAC std_ss [] THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) THEN PROVE_TAC[ALWAYS_NEXT_IMP,ALWAYS_IMP_AND1,ALWAYS_IMP_REFL]); val ALWAYS_UNTILN_IMP = store_thm ("ALWAYS_UNTILN_IMP", ``!n dev P Q R. (dev |= ALWAYS(Q IMPLIES R)) ==> (dev |= ALWAYS(UNTILN n P Q IMPLIES UNTILN n P (Q AND R)))``, Induct THENL [MC_TAC[UNTILN_def], RW_TAC std_ss [UNTILN_def] THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) THEN IMP_RES_TAC ALWAYS_NEXT_IMP THEN PROVE_TAC[ALWAYS_NEXT_IMP,ALWAYS_IMP_REFL,ALWAYS_IMP_AND1]]); (* Following model-checking-style theorems verify instances of MITB behaviour (esentially just special cases of MITB_IMP_BEH - so mainly a sanity check) *) (* Verify ready_out T iff MITB in state Ready *) val MITB_Ready = store_thm ("MITB_Ready", ``MITB_IMP key (r,c,n) f |= ALWAYS(cntlState Ready IFF readyOut T)``, MC_TAC[]); (* Verify Skip behaviour: (MITB_FUN (r,c,n) f (cntl,pmem,vmem) Skip = (cntl,pmem,vmem)) *) val MITB_Skip = store_thm ("MITB_Skip", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL cntl pmem vmem. skipInp T AND cntlState cntl AND pmemState pmem AND vmemState vmem IMPLIES NEXT(cntlState cntl AND pmemState pmem AND vmemState vmem))``, MC_TAC[] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE std_ss [el 1 thl,MITB_FUN_def] (SPEC ``t:num`` (el 4 thl))))); (* Verify protocol to set a new keys: Set key: if ready_out then hold skip_inp F and move_inp F for (time t) one cycle and f(block_inp t ++ ZEROS c) will be stored in pmem. Keeping skip_inp T in subsequent cycles freezes the state. (MITB_FUN (r,c,n) f (Ready,pmem,vmem) (Input key len) = (Ready,f(key++(ZEROS c)),ZEROS(r+c))) *) val MITB_SetKey = store_thm ("MITB_SetKey", ``MITB_IMP key (r,c,n) f |= ALWAYS (readyOut T AND skipInp F AND moveInp F IMPLIES (ALL new_key. blockInp new_key IMPLIES NEXT(pmemState(f(new_key ++ ZEROS c)))))``, MC_TAC[] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE list_ss [el 1 thl,el 2 thl,el 3 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 6 thl))))); (* Verify end of absorbing when len <= r-2 (MITB_FUN (r,c,n) f (Absorbing,pmem,vmem) (Input bk len) = if len <= r-2 then (* More than one bit too small *) (Ready, pmem, f(vmem XOR (TAKE len bk ++ [T] ++ ZEROS(r-len-2) ++ [T] ++ ZEROS c))) *) val MITB_EndAbsorbingLenLeq2 = store_thm ("MITB_EndAbsorbingLenLeq2", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bk len pmem vmem. readyOut F AND skipInp F AND moveInp F AND blockInp bk AND sizeInp len AND BOOL(len <= r-2) AND cntlState Absorbing AND pmemState pmem AND vmemState vmem IMPLIES NEXT (cntlState Ready AND pmemState pmem AND vmemState (f(vmem XOR (TAKE len bk ++ [T] ++ ZEROS(r-len-2) ++ [T] ++ ZEROS c)))))``, MC_TAC[] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE (srw_ss()) [el 1 thl,el 2 thl,el 3 thl,el 4 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 8 thl)))) THEN `LENGTH key - (size_inp t + 2) = LENGTH key - size_inp t - 2` by DECIDE_TAC THEN RW_TAC std_ss []); (* Verify end of absorbing when len = r-1 (MITB_FUN (r,c,n) f (Absorbing,pmem,vmem) (Input bk len) = ... if len = r-1 then (* Exactly one-bit too small *) (AbsorbEnd, pmem, f(vmem XOR (TAKE len bk ++ [T] ++ ZEROS c))) *) val MITB_AbsorbingToAbsorbEnd = store_thm ("MITB_AbsorbingToAbsorbEnd", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bk len pmem vmem. readyOut F AND skipInp F AND moveInp F AND blockInp bk AND sizeInp len AND BOOL(len = r-1) AND cntlState Absorbing AND pmemState pmem AND vmemState vmem IMPLIES NEXT (cntlState AbsorbEnd AND pmemState pmem AND vmemState (f(vmem XOR (TAKE len bk ++ [T] ++ ZEROS c)))))``, MC_TAC[] THEN `2 < LENGTH key` by PROVE_TAC[GoodParameters_def] THEN `~(LENGTH key <= 1 + (LENGTH key - 2))` by DECIDE_TAC THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE (srw_ss()) [el 1 thl,el 2 thl,el 3 thl,el 4 thl,el 5 thl,el 6 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 10 thl))))); (* Verify continue absorbing when len = r (MITB_FUN (r,c,n) f (Absorbing,pmem,vmem) (Input bk len) = (Absorbing,pmem,f(vmem XOR (bk ++ ZEROS c)))) *) val MITB_ContinueAbsorbing = store_thm ("MITB_ContinueAbsorbing", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bk len pmem vmem. readyOut F AND skipInp F AND moveInp F AND blockInp bk AND sizeInp len AND BOOL(len = r) AND cntlState Absorbing AND pmemState pmem AND vmemState vmem IMPLIES NEXT (cntlState Absorbing AND pmemState pmem AND vmemState (f(vmem XOR (bk ++ ZEROS c)))))``, MC_TAC[] THEN `2 < LENGTH key` by PROVE_TAC[GoodParameters_def] THEN `~(size_inp t <= size_inp t - 2) /\ ~(size_inp t = size_inp t - 1)` by DECIDE_TAC THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE (srw_ss()) [el 1 thl,el 2 thl,el 3 thl,el 4 thl,el 5 thl,el 6 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 10 thl))))); (* Verify end absorbing immediately after entering AbsorbEnd (MITB_FUN (r,c,n) f (AbsorbEnd,pmem,vmem) cmd = (Ready, pmem, f(vmem XOR (ZEROS(r-1) ++ [T] ++ ZEROS c)))) *) val MITB_AbsorbEndReady = store_thm ("MITB_AbsorbEndReady", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL pmem vmem. readyOut F AND skipInp F AND moveInp F AND cntlState AbsorbEnd AND pmemState pmem AND vmemState vmem IMPLIES NEXT (cntlState Ready AND pmemState pmem AND vmemState (f(vmem XOR (ZEROS(r-1) ++ [T] ++ ZEROS c)))))``, MC_TAC[] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE (srw_ss()) [el 1 thl,el 2 thl,el 3 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 7 thl))))); (* Verify MITB_FUN corresponds to a single step *) val MITB_STEP = store_thm ("MITB_STEP", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL cmd cntl pmem vmem. mitbCommand cmd AND mitbState(cntl,pmem,vmem) IMPLIES NEXT(mitbState(MITB_FUN (r,c,n) f (cntl,pmem,vmem) cmd)))``, MC_TAC[]); (* Verify protocol to hash a message: Hash msg: if ready_out then hold skip_inp F and move_inp T (time t) for one cycle, then hold both skip_inp and move_inp F until ready_out goes to T again. The message is absorbed starting at t+1, data inputs (message block and size) is read on successive cycles until the last block is read (indicated by its length being less than r). Keeping skip_inp T in subsequent cycles freezes the state so the digest can be read. *) (* Start absorbing *) val MITB_StartAbsorbing = store_thm ("MITB_StartAbsorbing", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL pmem vmem. mitbState(Ready,pmem,vmem) AND skipInp F AND moveInp T IMPLIES NEXT(mitbState(Absorbing,pmem,pmem)))``, MC_TAC[] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE list_ss [el 1 thl,el 2 thl,el 3 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 6 thl))))); (* Absorb an arbitrary block *) val MITB_AbsorbBlock = store_thm ("MITB_AbsorbBlock", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL pmem vmem bk. mitbState(Absorbing,pmem,vmem) AND InputBlock bk IMPLIES NEXT (mitbState (MITB_FUN (r,c,n) f (Absorbing,pmem,vmem) (Input bk (LENGTH bk)))))``, MC_TAC[]); (* Absorb a full block !!! Possibly wrong !!! *) val MITB_AbsorbBlockFull = store_thm ("MITB_AbsorbBlockFull", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL pmem vmem bk. mitbState(Absorbing,pmem,vmem) AND InputBlock bk IMPLIES NEXT (BOOL(LENGTH bk = r) IMPLIES mitbState (Absorbing, pmem, f(vmem XOR (bk ++ ZEROS c)))))``, MC_TAC[] THEN `2 < LENGTH key` by PROVE_TAC[GoodParameters_def] THEN `~(LENGTH (block_inp t) <= LENGTH key - 2)` by DECIDE_TAC THEN `~(LENGTH (block_inp t) = LENGTH key - 1)` by DECIDE_TAC THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE list_ss [el 1 thl,el 2 thl,el 3 thl,el 4 thl,el 5 thl,el 6 thl,el 7 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 10 thl))))); (* Absorb a block that is one short of full *) val MITB_AbsorbBlockShort1 = store_thm ("MITB_AbsorbBlockShort1", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL pmem vmem bk. mitbState(Absorbing,pmem,vmem) AND InputBlock bk IMPLIES NEXT (BOOL(LENGTH bk = r-1) IMPLIES mitbState (AbsorbEnd, pmem, f(vmem XOR (TAKE (r-1) bk ++ [T] ++ Zeros c)))))``, MC_TAC[] THEN `2 < LENGTH key` by PROVE_TAC[GoodParameters_def] THEN `~(LENGTH (block_inp t) <= LENGTH key - 2)` by DECIDE_TAC THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE list_ss [el 1 thl,el 3 thl,el 4 thl,el 5 thl,el 6 thl,el 7 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 10 thl))))); (* Absorb a block that is at least two short of full *) val MITB_AbsorbBlockShort2 = store_thm ("MITB_AbsorbBlockShort2", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL pmem vmem bk. mitbState(Absorbing,pmem,vmem) AND InputBlock bk IMPLIES NEXT (BOOL(LENGTH bk <= r-2) IMPLIES mitbState (Ready, pmem, f(vmem XOR (TAKE (LENGTH bk) bk ++ [T] ++ Zeros(r - LENGTH bk - 2) ++ [T] ++ Zeros c)))))``, MC_TAC[] THEN `2 < LENGTH key` by PROVE_TAC[GoodParameters_def] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE list_ss [el 1 thl,el 2 thl,el 3 thl,el 4 thl,el 5 thl,el 6 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 9 thl))))); (* Ad hoc lemmas used to prove MITB_AbsorbBlockStep *) val Lemma7 = prove (``!dev P Q U. dev |= ALWAYS(P AND Q IMPLIES NEXT U) ==> !V. dev |= ALWAYS((Q AND NEXT V) AND P IMPLIES NEXT(V AND U))``, RW_TAC std_ss [Models_def,AND_def,IMPLIES_def,ALWAYS_def,NEXT_def,ChopAllChopAll]); val Lemma8 = ISPEC ``InputBlocks (LENGTH (bk:bits)) ((bkl++[end_bk]))`` (MATCH_MP Lemma7 (SIMP_RULE list_ss [ALWAYS_ALL,BOOL_T_IMPLIES] (INST[``r:num``|->``LENGTH(bk:bits)``] (SPEC_ALL (SIMP_RULE std_ss [ALWAYS_ALL] MITB_AbsorbBlockFull))))); val MITB_AbsorbBlockStep = store_thm ("MITB_AbsorbBlockStep", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl bk end_bk vmem. BOOL(EVERY (\l. (LENGTH l = r)) (bk::bkl)) IMPLIES InputBlocks r (bk::(bkl++[end_bk])) AND mitbState(Absorbing,pmem,vmem) IMPLIES NEXT (InputBlocks r (bkl++[end_bk]) AND mitbState(Absorbing,pmem,f(vmem XOR (bk ++ ZEROS c)))))``, RW_TAC list_ss [InputBlocks_def,ALWAYS_BOOL_IMPLIES,ALWAYS_ALL] THEN ASSUME_TAC Lemma8 THEN RW_TAC std_ss []); (* More ad hoc lemmas used to prove MITB_AbsorbBlockIter *) val Lemma9 = prove (``!dev P Q U V b1 b2. (b1 ==> b2) ==> dev |= ALWAYS(BOOL b1 IMPLIES P AND Q IMPLIES NEXT(U AND V)) ==> dev |= ALWAYS(BOOL b1 AND P AND Q IMPLIES NEXT(BOOL b2 AND U AND V))``, RW_TAC std_ss [Models_def,AND_def,IMPLIES_def,ALWAYS_def,NEXT_def, ChopAllChopAll,BOOL_def]); val Lemma10 = SPECL [``MITB_IMP (key :bits) ((r :num),(c :num),(n :num)) (f :bits -> bits)``, ``InputBlocks r (bk::((bkl ++ [end_bk]) :bits list))``, ``mitbState (Absorbing,(pmem :bits),vmem)``, ``InputBlocks r ((bkl ++ [end_bk]) :bits list)``, ``mitbState(Absorbing,pmem,f (vmem XOR ((bk ++ ZEROS c) :bits)))``, ``EVERY (\(l:bits). LENGTH l = r) ((bk::bkl) :bits list)``, ``EVERY (\l:bits. LENGTH l = r) (bkl: bits list)``] Lemma9; val Lemma11 = MATCH_MP Lemma10 (prove(fst(dest_imp(concl Lemma10)),RW_TAC list_ss [])); val Lemma12 = SIMP_RULE std_ss [GSYM APPEND] (MATCH_MP Lemma11 (SPEC_ALL(SIMP_RULE std_ss [ALWAYS_ALL]MITB_AbsorbBlockStep))); val Lemma13 = SIMP_RULE std_ss [] (ISPECL [``MITB_IMP key (r,c,n) f``, ``\vmem bk. f(vmem XOR (bk ++ ZEROS c)):bits``, ``\xl. BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl++[end_bk])``, ``\vmem. mitbState(Absorbing,pmem,vmem)``] ALWAYS_NEXTN_FOLDL); (* Lemmas and theorems with a postfixed U are similar to the ones without a U, but are about UNTILN rather than NEXTN. I proved the NEXTN versions first, but then decided the UNTILN versions were needed, so I just tweaked the proofs. *) val Lemma13U = SIMP_RULE std_ss [] (ISPECL [``MITB_IMP key (r,c,n) f``, ``\vmem bk. f(vmem XOR (bk ++ ZEROS c)):bits``, ``\xl. BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl++[end_bk])``, ``\vmem. mitbState(Absorbing,pmem,vmem)``] ALWAYS_UNTILN_FOLDL); val Lemma14 = prove (``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl bk end_bk pmem vmem. (BOOL (EVERY (\l. LENGTH l = r) (bk::bkl)) AND InputBlocks r (bk::bkl ++ [end_bk])) AND mitbState (Absorbing,pmem,vmem) IMPLIES NEXT ((BOOL (EVERY (\l. LENGTH l = r) bkl) AND InputBlocks r (bkl ++ [end_bk])) AND mitbState (Absorbing,pmem,f (vmem XOR (bk ++ ZEROS c))))) ==> MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl end_bk pmem vmem. (BOOL (EVERY (\l. LENGTH l = r) bkl) AND InputBlocks r (bkl ++ [end_bk])) AND mitbState (Absorbing,pmem,vmem) IMPLIES NEXTN (LENGTH bkl) ((BOOL (EVERY (\l:bits. LENGTH l = r) []) AND InputBlocks r ([] ++ [end_bk])) AND mitbState (Absorbing,pmem, FOLDL (\vmem bk. f (vmem XOR (bk ++ ZEROS c))) vmem bkl)))``, SIMP_TAC std_ss [ALWAYS_ALL,SIMP_RULE std_ss [ALWAYS_ALL] Lemma13]); val Lemma14U = prove (``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl bk end_bk pmem vmem. (BOOL (EVERY (\l. LENGTH l = r) (bk::bkl)) AND InputBlocks r (bk::bkl ++ [end_bk])) AND mitbState (Absorbing,pmem,vmem) IMPLIES NEXT ((BOOL (EVERY (\l. LENGTH l = r) bkl) AND InputBlocks r (bkl ++ [end_bk])) AND mitbState (Absorbing,pmem,f (vmem XOR (bk ++ ZEROS c))))) ==> MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl end_bk pmem vmem. (BOOL (EVERY (\l. LENGTH l = r) bkl) AND InputBlocks r (bkl ++ [end_bk])) AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl) (EXIST xl y. (BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl ++ [end_bk])) AND mitbState (Absorbing,pmem,y)) ((BOOL (EVERY (\l:bits. LENGTH l = r) []) AND InputBlocks r ([] ++ [end_bk])) AND mitbState (Absorbing,pmem, FOLDL (\vmem bk. f (vmem XOR (bk ++ ZEROS c))) vmem bkl)))``, SIMP_TAC std_ss [ALWAYS_ALL,SIMP_RULE std_ss [ALWAYS_ALL] Lemma13U]); val Lemma15 = prove (fst(dest_imp(concl Lemma14)), ASSUME_TAC Lemma14 THEN RW_TAC std_ss [ALWAYS_ALL,AND_ASSOC,Lemma12]); val Lemma15U = prove (fst(dest_imp(concl Lemma14U)), RW_TAC std_ss [ALWAYS_ALL,AND_ASSOC,Lemma12]); val Lemma16 = SIMP_RULE list_ss [BOOL_T_AND] (MP Lemma14 Lemma15); val Lemma16U = SIMP_RULE list_ss [BOOL_T_AND] (MP Lemma14U Lemma15U); val MITB_AbsorbBlockIterLemma = store_thm ("MITB_AbsorbBlockIterLemma", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl end_bk pmem vmem. (BOOL (EVERY (\l. LENGTH l = r) bkl) AND InputBlocks r (bkl ++ [end_bk])) AND mitbState (Absorbing,pmem,vmem) IMPLIES NEXTN (LENGTH bkl) (InputBlocks r [end_bk] AND mitbState (Absorbing,pmem, Absorb f c vmem bkl)))``, RW_TAC list_ss [Lemma16,GSYM XOREqXor,GSYM ZEROSEqZeros,Absorb_FOLDL]); val MITB_AbsorbBlockIterLemmaU = store_thm ("MITB_AbsorbBlockIterLemmaU", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl end_bk pmem vmem. (BOOL (EVERY (\l. LENGTH l = r) bkl) AND InputBlocks r (bkl ++ [end_bk])) AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl) (EXIST xl y. (BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl ++ [end_bk])) AND mitbState (Absorbing,pmem,y)) (InputBlocks r [end_bk] AND mitbState (Absorbing,pmem, Absorb f c vmem bkl)))``, RW_TAC list_ss [Lemma16U,GSYM XOREqXor,GSYM ZEROSEqZeros,Absorb_FOLDL]); (* Yet more ad hoc lemmas *) val Lemma17 = SPECL [``r:num``,``n:num``,``key:bits``,``f:bits->bits``,``c:num``, ``FRONT(bkl: bits list)``,``LAST(bkl: bits list)``, ``pmem:bits``,``vmem:bits``] (GEN_ALL(SIMP_RULE std_ss [ALWAYS_ALL] MITB_AbsorbBlockIterLemma)); val Lemma17U = SPECL [``r:num``,``n:num``,``key:bits``,``f:bits->bits``,``c:num``, ``FRONT(bkl: bits list)``,``LAST(bkl: bits list)``, ``pmem:bits``,``vmem:bits``] (GEN_ALL(SIMP_RULE std_ss [ALWAYS_ALL] MITB_AbsorbBlockIterLemmaU)); val Lemma18 = prove (``!dev P Q R b. (dev |= ALWAYS(BOOL b AND P AND Q IMPLIES R)) = (b ==> dev |= ALWAYS(P AND Q IMPLIES R))``, REPEAT GEN_TAC THEN EQ_TAC THEN RW_TAC std_ss [Models_def,AND_def,IMPLIES_def,ALWAYS_def,BOOL_def]); val Lemma19 = DISCH_ALL (SIMP_RULE std_ss [MP (ISPEC ``bkl:bits list`` APPEND_FRONT_LAST) (ASSUME ``(bkl:bits list) <> []``)] (SPECL [``FRONT(bkl:bits list)``,``LAST(bkl:bits list)``] (SIMP_RULE std_ss [BOOL_T_AND,GSYM AND_ASSOC] (SIMP_RULE std_ss [ALWAYS_ALL,Lemma18,AND_ASSOC] MITB_AbsorbBlockIterLemma)))); val Lemma19U = DISCH_ALL (SIMP_RULE std_ss [MP (ISPEC ``bkl:bits list`` APPEND_FRONT_LAST) (ASSUME ``(bkl:bits list) <> []``)] (SPECL [``FRONT(bkl:bits list)``,``LAST(bkl:bits list)``] (SIMP_RULE std_ss [BOOL_T_AND,GSYM AND_ASSOC] (SIMP_RULE std_ss [ALWAYS_ALL,Lemma18,AND_ASSOC] MITB_AbsorbBlockIterLemmaU)))); val MITB_AbsorbBlockIter = store_thm ("MITB_AbsorbBlockIter", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl pmem vmem. BOOL (bkl<>[] /\ EVERY (\l. LENGTH l = r) (FRONT bkl)) AND InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES NEXTN (LENGTH bkl - 1) (InputBlocks r [LAST bkl] AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))))``, RW_TAC std_ss [ALWAYS_ALL,Lemma18] THEN `LENGTH bkl - 1 = LENGTH(FRONT bkl)` by PROVE_TAC[LENGTH_FRONT,PRE_SUB1] THEN IMP_RES_TAC Lemma19 THEN RW_TAC std_ss []); val MITB_AbsorbBlockIterU = store_thm ("MITB_AbsorbBlockIterU", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl pmem vmem. BOOL (bkl<>[] /\ EVERY (\l. LENGTH l = r) (FRONT bkl)) AND InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1) (EXIST xl y. (BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl ++ [LAST bkl])) AND mitbState (Absorbing,pmem,y)) (InputBlocks r [LAST bkl] AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))))``, RW_TAC std_ss [ALWAYS_ALL,Lemma18] THEN `LENGTH bkl - 1 = LENGTH(FRONT bkl)` by PROVE_TAC[LENGTH_FRONT,PRE_SUB1] THEN IMP_RES_TAC Lemma19U THEN RW_TAC std_ss []); (* val Lemma20 = |- MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl pmem vmem. BOOL (bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl)) AND InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES NEXTN (LENGTH bkl - 1) (((BOOL(LENGTH (LAST bkl) = r) IMPLIES (blockInp (LAST bkl) AND sizeInp (LENGTH (LAST bkl)) AND skipInp F AND moveInp F) AND NEXT (blockInp [] AND sizeInp (LENGTH []) AND skipInp F AND moveInp F)) AND (BOOL(LENGTH (LAST bkl) <> r) IMPLIES blockInp (LAST bkl) AND sizeInp (LENGTH (LAST bkl)) AND skipInp F AND moveInp F)) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)))) *) val Lemma20 = SIMP_RULE std_ss [InputBlocks_def,InputBlock_def,IF_IMPLIES,ALWAYS_ALL, BOOL_T_IMPLIES,BOOL_F_IMPLIES,BOOL_T_AND] MITB_AbsorbBlockIter; (* val Lemma20U = |- MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl pmem vmem. BOOL (bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl)) AND InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1) (EXIST xl y. (BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl ++ [LAST bkl])) AND mitbState (Absorbing,pmem,y)) (((BOOL (LENGTH (LAST bkl) = r) IMPLIES (blockInp (LAST bkl) AND sizeInp (LENGTH (LAST bkl)) AND skipInp F AND moveInp F) AND NEXT (blockInp [] AND sizeInp 0 AND skipInp F AND moveInp F)) AND (BOOL (LENGTH (LAST bkl) <> r) IMPLIES blockInp (LAST bkl) AND sizeInp (LENGTH (LAST bkl)) AND skipInp F AND moveInp F)) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)))) *) val Lemma20U = SIMP_RULE list_ss [InputBlocks_def,InputBlock_def,IF_IMPLIES, BOOL_T_IMPLIES,BOOL_F_IMPLIES,BOOL_T_AND] MITB_AbsorbBlockIterU; val Lemma21U = SIMP_RULE std_ss [ALWAYS_ALL] Lemma20U; (* Verification of properties in paper *) val Init_def = Define `Init key c n f = readyOut T AND digestOut(Zeros n) AND pmemState(f (key ++ ZEROS c))`; val Init = store_thm ("Init", ``MITB_IMP key (r,c,n) f |= Init key c n f``, MC_TAC[Init_def] THEN `n <= LENGTH key` by PROVE_TAC[GoodParameters_def] THEN `n <= c + LENGTH key` by DECIDE_TAC THEN RW_TAC std_ss [TAKE_ZEROS]); val Freeze_def = Define `Freeze = ALWAYS (ALL s b1 b2. skipInp T AND pmemState s AND readyOut b1 AND digestOut b2 IMPLIES NEXT(pmemState s AND readyOut b1 AND digestOut b2))`; val Freeze = store_thm ("Freeze", ``MITB_IMP key (r,c,n) f |= Freeze``, MC_TAC[Freeze_def] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE std_ss [el 1 thl,MITB_FUN_def] (SPEC ``t:num`` (el 4 thl)))) THEN RW_TAC (srw_ss()) []); val Reset_def = Define `Reset n = ALWAYS (ALL s. moveInp T AND skipInp F AND readyOut F AND pmemState s IMPLIES NEXT(readyOut T AND pmemState s AND digestOut(Zeros n)))`; val Reset = store_thm ("Reset", ``MITB_IMP key (r,c,n) f |= Reset n``, MC_TAC[Reset_def] THEN `n <= LENGTH key` by PROVE_TAC[GoodParameters_def] THEN `n <= c + LENGTH key` by DECIDE_TAC THEN Cases_on `cntl_sig t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE list_ss [el 1 thl,el 2 thl,el 5 thl,el 6 thl, MITB_FUN_def] (SPEC ``t:num`` (el 9 thl)))) THEN RW_TAC (srw_ss()) [ZEROSEqZeros,XOREqXor,TAKE_ZEROS]); val KeyUpdate_def = Define `KeyUpdate r c f = ALWAYS (readyOut T AND skipInp F AND moveInp F IMPLIES (ALL key. blockInp key AND BOOL(LENGTH key = r) IMPLIES NEXT(readyOut T AND pmemState(f(key ++ Zeros c)))))`; val KeyUpdate = store_thm ("KeyUpdate", ``MITB_IMP key (r,c,n) f |= KeyUpdate r c f``, MC_TAC[KeyUpdate_def] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE list_ss [el 1 thl,el 2 thl,el 3 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 6 thl))))); val ComputeMAC_def = Define `ComputeMAC (r,c,n) f = ALWAYS (ALL key msg. (pmemState(f(key ++ Zeros c)) AND InputMessage r msg AND readyOut T) IMPLIES UNTILN (if (LENGTH msg MOD r = r-1) then (LENGTH msg DIV r) + 2 else (LENGTH msg DIV r) + 1) (readyOut F AND digestOut(Zeros n)) (readyOut T AND digestOut(Hash (r,c,n) f (Zeros(r+c)) (key++msg))))`; (* Prepare a message for inputting *) val MakeInputBlocks_def = Define `MakeInputBlocks r msg = if msg = [] then [[]] else if LENGTH msg MOD r = 0 then SNOC [] (Split r msg) else Split r msg`; (* Verify prepared message has desired properties (proof based on an earlier version, SplitMessage below, and was harder to prove than I expected, or maybe I missed a simpler argument) *) val MakeInputBlocks = store_thm ("MakeInputBlocks", ``!r msg. 1 < r ==> (MakeInputBlocks r msg) <> [] /\ (msg = FLAT (MakeInputBlocks r msg)) /\ EVERY (\l. LENGTH l = r) (FRONT (MakeInputBlocks r msg)) /\ LENGTH(LAST (MakeInputBlocks r msg)) < r``, REPEAT GEN_TAC THEN DISCH_TAC THEN `0 < r` by DECIDE_TAC THEN IMP_RES_TAC FlattenSplit THEN Cases_on `msg = []` THEN SIMP_TAC list_ss [Once Split_def] THEN RW_TAC list_ss [MakeInputBlocks_def,NOT_SNOC_NIL,SplitNotEmpty, FlattenSplit,FLAT_SNOC,EVERY_EL] THENL [`n < LENGTH (Split r msg) = n < PRE(LENGTH (Split r msg)) \/ (n = LENGTH (Split r msg) - 1)` by DECIDE_TAC THEN RES_TAC THEN IMP_RES_TAC SplitBlockLengths THEN RW_TAC list_ss [GSYM PRE_SUB1,MATCH_MP EL_PRE_LENGTH (SPEC_ALL SplitNotEmpty)] THEN Cases_on `r <= LENGTH msg` THEN RW_TAC list_ss [LASTSplitLASTN1,LENGTH_LASTN] THEN `LENGTH msg < r` by DECIDE_TAC THEN `LENGTH msg MOD r = LENGTH msg` by PROVE_TAC[LESS_MOD] THEN `msg = []` by PROVE_TAC[LENGTH_NIL], IMP_RES_TAC SplitBlockLengths THEN `~NULL(Split r msg)` by PROVE_TAC[NULL_EQ,SplitNotEmpty] THEN IMP_RES_TAC EL_FRONT THEN RW_TAC std_ss [] THEN `n < PRE (LENGTH (Split r msg))` by PROVE_TAC[LENGTH_FRONT,SplitNotEmpty] THEN RES_TAC, `0 < LENGTH msg MOD r` by DECIDE_TAC THEN IMP_RES_TAC SplitLastLength THEN ASSUME_TAC(MATCH_MP LAST_EL (SPEC_ALL SplitNotEmpty)) THEN RW_TAC std_ss []]); (* Various lemmas for simplifying the invariant during the MAC calculation *) val MACInsOuts = store_thm ("MACInsOuts", ``MITB_IMP key (r,c,n) f |= ALWAYS (ALL xl y. (BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl++[LAST bkl])) AND mitbState(Absorbing,pmem,y) IMPLIES (skipInp F AND moveInp F AND readyOut F AND digestOut(Zeros n)))``, SIMP_TAC std_ss [ALWAYS_ALL] THEN Induct THEN MC_TAC[InputBlocks_def,InputBlock_def]); (* Next a lot of temporal logic properties -some may not be needed *) val ALWAYS_IMPLIES_EXIST = store_thm ("ALWAYS_IMPLIES_EXIST", ``!dev P Q. (!x. dev |= ALWAYS(P x IMPLIES Q)) ==> (dev |= ALWAYS((EXIST x. P x) IMPLIES Q))``, MC_TAC[]); val ALWAYS_EXIST_IMP = store_thm ("ALWAYS_EXIST_IMP", ``!dev P Q. dev |= ALWAYS(ALL x. P x IMPLIES Q) IMPLIES ALWAYS((EXIST x. P x) IMPLIES Q)``, MC_TAC[]); val ALWAYS_EXIST_IMP2 = store_thm ("ALWAYS_EXIST_IMP2", ``!dev P Q. dev |= ALWAYS(ALL xl y. P xl y IMPLIES Q) IMPLIES ALWAYS((EXIST xl y. P xl y) IMPLIES Q)``, MC_TAC[] THEN RES_TAC); val ALWAYS_IMP = store_thm ("ALWAYS_IMP", ``!dev P Q. (dev |= ALWAYS(P IMPLIES Q)) ==> ((dev |= ALWAYS P) ==> (dev |= ALWAYS Q))``, MC_TAC[]); val ALWAYS_EXIST_IMP2 = store_thm ("ALWAYS_EXIST_IMP2", ``!dev P Q. (dev |= ALWAYS(ALL xl y. P xl y IMPLIES Q)) ==> (dev |= ALWAYS((EXIST xl y. P xl y) IMPLIES Q))``, MC_TAC[] THEN RES_TAC); (* val MACInsOutsCor = |- MITB_IMP key (r,c,n) f |= ALWAYS ((EXIST xl y. (BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl ++ [LAST bkl])) AND mitbState (Absorbing,pmem,y)) IMPLIES skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) *) val MACInsOutsCor = MP (SIMP_RULE std_ss [] (ISPECL [``MITB_IMP key (r,c,n) f``, ``\xl y. (BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl++[LAST bkl])) AND mitbState (Absorbing,pmem,y)``, ``skipInp F AND moveInp F AND readyOut F AND digestOut(Zeros n)``] ALWAYS_EXIST_IMP2)) MACInsOuts; val Lemma22 = SIMP_RULE std_ss [] (ISPECL [``LENGTH(bkl:bits list) - 1``, ``MITB_IMP key (r,c,n) f``, ``BOOL (bkl<>[] /\ EVERY (\l. LENGTH l = r) (FRONT bkl)) AND InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem)``, ``EXIST xl y. (BOOL (EVERY (\l. LENGTH l = r) xl) AND InputBlocks r (xl ++ [LAST bkl])) AND mitbState (Absorbing,pmem,y)``, ``skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)``, ``InputBlocks r [LAST bkl] AND mitbState(Absorbing,pmem,Absorb f c vmem (FRONT bkl))``] ALWAYS_IMP_UNTILN_MONO1); val Lemma23 = MP Lemma22 MACInsOutsCor; val Lemma24 = MATCH_MP Lemma23 (SPEC_ALL(SIMP_RULE std_ss [ALWAYS_ALL] MITB_AbsorbBlockIterU)); val Lemma25 = SIMP_RULE std_ss [GSYM ALWAYS_ALL](GEN_ALL Lemma24); val MITB_AbsorbBlockIterUCor = store_thm ("MITB_AbsorbBlockIterUCor", ``!key r c n f pmem vmem. MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl. BOOL (bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl)) AND InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (InputBlocks r [LAST bkl] AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))))``, RW_TAC std_ss [Lemma25]); (* OBSOLETE! val Lemma26 = |- !key r c n f pmem vmem. MITB_IMP key (r,c,n) f |= ALWAYS (ALL bkl. BOOL (bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl)) AND InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (((BOOL (LENGTH (LAST bkl) = r) IMPLIES (blockInp (LAST bkl) AND sizeInp (LENGTH (LAST bkl)) AND skipInp F AND moveInp F) AND NEXT (blockInp [] AND sizeInp 0 AND skipInp F AND moveInp F)) AND (BOOL (LENGTH (LAST bkl) <> r) IMPLIES blockInp (LAST bkl) AND sizeInp (LENGTH (LAST bkl)) AND skipInp F AND moveInp F)) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)))) val Lemma26 = SIMP_RULE list_ss [InputBlocks_def,InputBlock_def,IF_IMPLIES, BOOL_T_IMPLIES,BOOL_F_IMPLIES,BOOL_T_AND] MITB_AbsorbBlockIterUCor; *) (* val Lemma26 = |- !key r c n f pmem vmem bkl. MITB_IMP key (r,c,n) f |= ALWAYS (BOOL (bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl)) AND InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((if LENGTH (LAST bkl) = r then InputBlock (LAST bkl) AND NEXT (InputBlock []) else InputBlock (LAST bkl)) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)))) *) val Lemma26 = SIMP_RULE list_ss [ALWAYS_ALL,InputBlocks_def] MITB_AbsorbBlockIterUCor; val Lemma27 = prove (``(InputBlock (LAST bkl) AND NEXT (InputBlock [])) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)) = (InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) AND NEXT (InputBlock [])``, RW_TAC std_ss [FORALL_PROD,FUN_EQ_THM] THEN EQ_TAC THEN MC_TAC[]); val Lemma28 = GEN_ALL (DISCH_ALL (SIMP_RULE std_ss [Lemma27,ASSUME ``LENGTH (LAST(bkl:bits list)) = r``] (SPEC_ALL Lemma26))); val Lemma29 = GEN_ALL (DISCH_ALL (SIMP_RULE std_ss [ASSUME ``LENGTH (LAST(bkl:bits list)) <> r``] (SPEC_ALL Lemma26))); val Lemma30 = prove (``MITB_IMP key (r,c,n) f |= ALWAYS ((InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) IMPLIES (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)))``, MC_TAC[InputBlock_def]); val Lemma31 = SPECL [``LENGTH(bkl:bits list) - 1``, ``MITB_IMP key (r,c,n) f``, ``skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)``, ``InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))``, ``InputBlock []``] ALWAYS_UNTILN_IMP_NEXT; val Lemma32 = SPECL [``MITB_IMP key (r,c,n) f``, ``UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) AND NEXT (InputBlock []))``, ``UNTILN (LENGTH bkl - 1 + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (InputBlock [])``] ALWAYS_MP; val Lemma32 = MP Lemma31 Lemma30; val Lemma33 = SPECL [``MITB_IMP key (r,c,n) f``, ``UNTILN (LENGTH(bkl:bits list) - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) AND NEXT (InputBlock []))``, ``UNTILN (LENGTH(bkl:bits list) - 1 + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (InputBlock [])``] ALWAYS_MP; val Lemma34 = MP Lemma33 Lemma32; (* Restarting proof thread -- cleanup will be needed later *) val Lemma35 = REWRITE_RULE [ALWAYS_BOOL_AND_IMPLIES,InputBlock_def]Lemma28; val Lemma36 = SPEC_ALL (SIMP_RULE list_ss [ALWAYS_BOOL_AND_IMPLIES,InputBlocks_def]Lemma29); val Lemma37 = Q.INST [`bk` |-> `LAST bkl`, `vmem` |-> `Absorb f c vmem (FRONT bkl)`] (SPEC_ALL(SIMP_RULE list_ss [ALWAYS_ALL] MITB_AbsorbBlockShort2)); val ALWAYS_IMP_NEXT_BOOL = store_thm ("ALWAYS_IMP_NEXT_BOOL", ``!dev b P Q. (dev |= ALWAYS(P IMPLIES NEXT(BOOL b IMPLIES Q))) ==> (b ==> dev |= ALWAYS(P IMPLIES NEXT Q))``, MC_TAC[]); val Lemma38 = Q.SPECL [`MITB_IMP key (r,c,n) f`, `LENGTH (LAST(bkl:bits list)) <= r - 2`, `mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)) AND InputBlock (LAST bkl)`, `mitbState (Ready,pmem, f(Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c)))`] ALWAYS_IMP_NEXT_BOOL; val Lemma39 = MP Lemma38 Lemma37; (* Start from MITB_AbsorbBlockIterUCor by removing the ALL quantifiers and hoisting the assumption that the front of bkl consists of blocks of length r. val LEMMA1 = |- !key r c n f pmem vmem bkl. bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl) ==> MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((if LENGTH (LAST bkl) = r then InputBlock (LAST bkl) AND NEXT (InputBlock []) else InputBlock (LAST bkl)) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)))) *) val LEMMA1 = SIMP_RULE list_ss [ALWAYS_ALL,InputBlocks_def,ALWAYS_BOOL_AND_IMPLIES] MITB_AbsorbBlockIterUCor; (* Consider the case when LENGTH (LAST bkl) <> r val LEMMA2 = |- LENGTH (LAST bkl) <> r ==> bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl) ==> MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)))) *) val LEMMA2 = (DISCH_ALL (SIMP_RULE list_ss [Lemma27, ASSUME ``LENGTH (LAST(bkl:bits list)) <> r /\ LENGTH (LAST bkl) <> r-1``] (SPEC_ALL LEMMA1))); (* Remove ALL quantification from MITB_AbsorbBlockShort2, instantiate bk and vmem to match the state reached in LEMMA2, hoist assumption using ALWAYS_IMP_NEXT_BOOL val LEMMA3 = |- LENGTH (LAST bkl) <= r - 2 ==> MITB_IMP key (r,c,n) f |= ALWAYS (InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)) IMPLIES NEXT (mitbState (Ready,pmem, f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c))))) *) val LEMMA3 = MATCH_MP ALWAYS_IMP_NEXT_BOOL (INST [``bk:bits`` |-> ``LAST bkl:bits``, ``vmem:bits`` |-> ``Absorb f c vmem (FRONT bkl)``] (SPEC_ALL (SIMP_RULE list_ss [ALWAYS_ALL,Once AND_SYM] MITB_AbsorbBlockShort2))); (* Prove invariant generated by ALWAYS_UNTILN_IMP_NEXT entails actual invariant. val LEMMA4 = |- MITB_IMP key (r,c,n) f |= ALWAYS (InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl)) IMPLIES skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) *) val LEMMA4 = prove (``MITB_IMP key (r,c,n) f |= ALWAYS ((InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) IMPLIES (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)))``, MC_TAC[InputBlock_def]); (* Instantiate ALWAYS_UNTILN_IMP_NEXT and MP it the result to LEMMA4 val LEMMA5 = |- MITB_IMP key (r,c,n) f |= ALWAYS (UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) AND NEXT (mitbState (Ready,pmem, f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c))))) IMPLIES UNTILN (LENGTH bkl - 1 + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (mitbState (Ready,pmem, f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c))))) *) val LEMMA5 = (SPECL [``LENGTH(bkl:bits list) - 1``, ``mitbState (Ready,pmem, f(Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c)))``] (MATCH_MP ALWAYS_UNTILN_IMP_NEXT LEMMA4)); (* Instantiate ALWAYS_UNTILN_IMP to prepare to combine LEMMA2 and LEMMA3 using ALWAYS_IMP_TRANS val LEMMA6 = [LENGTH (LAST bkl) <= r - 2] |- MITB_IMP key (r,c,n) f |= ALWAYS (UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) IMPLIES UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) AND NEXT (mitbState (Ready,pmem, f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c)))))) *) val LEMMA6 = (SPECL [``LENGTH(bkl:bits list) - 1``, ``skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)``] (MATCH_MP (ALWAYS_UNTILN_IMP) (UNDISCH_ALL LEMMA3))); (* Combine LEMMA6 and LEMMA2 val LEMMA7 = [bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl), LENGTH (LAST bkl) <> r /\ LENGTH (LAST bkl) <> r - 1, LENGTH (LAST bkl) <= r - 2] |- MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) AND NEXT (mitbState (Ready,pmem, f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c)))))) *) val LEMMA7 = MP (Q.SPEC `UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((InputBlock (LAST bkl) AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) AND NEXT (mitbState (Ready,pmem, f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c)))))` (MATCH_MP ALWAYS_IMP_TRANS (UNDISCH_ALL LEMMA2))) LEMMA6; (* val LEMMA8 = [LENGTH (LAST bkl) <> r, bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl), LENGTH (LAST bkl) <= r - 2] |- MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1 + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (mitbState (Ready,pmem, f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c))))) *) val LEMMA8 = MATCH_MP (MATCH_MP ALWAYS_IMP_TRANS (UNDISCH_ALL LEMMA7)) LEMMA5; (* Deduce specified outputs in varous states *) (* Old val LEMMA9 = prove (``!vmem. MITB_IMP key (r,c,n) f |= ALWAYS (mitbState(Ready,pmem,vmem) IMPLIES readyOut T AND digestOut(TAKE n vmem))``, MC_TAC[]); *) val LEMMA9 = prove (``!vmem. MITB_IMP key (r,c,n) f |= ALWAYS (mitbState(Ready,pmem,vmem) IMPLIES readyOut T AND digestOut(TAKE n vmem) AND pmemState pmem)``, MC_TAC[]); val LEMMA9A = prove (``!vmem. MITB_IMP key (r,c,n) f |= ALWAYS (mitbState(Absorbing,pmem,vmem) IMPLIES readyOut F AND digestOut(Zeros n))``, MC_TAC[]); val LEMMA9B = prove (``!vmem. MITB_IMP key (r,c,n) f |= ALWAYS (mitbState(AbsorbEnd,pmem,vmem) IMPLIES readyOut F AND digestOut(Zeros n))``, MC_TAC[]); (* Replace outputs in UNTILN *) val LEMMA10 = MATCH_MP ALWAYS_IMP_UNTILN_MONO2 (SPEC ``f(Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c))`` LEMMA9); (* [LENGTH (LAST bkl) <> r, bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl), LENGTH (LAST bkl) <= r - 2] |- MITB_IMP key (r,c,n) f |= ALWAYS (mitbState (Ready,pmem,vmem) AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r bkl IMPLIES UNTILN (LENGTH bkl - 1 + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (TAKE n (f (Absorb f c pmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r - (LENGTH (LAST bkl) + 2)) ++ [T] ++ Zeros c))))))) *) val LEMMA11 = MATCH_MP (MATCH_MP ALWAYS_IMP_NEXT_AND (SPEC_ALL(SIMP_RULE std_ss [ALWAYS_ALL] MITB_StartAbsorbing))) (INST [``vmem:bits`` |-> ``pmem:bits``] (MATCH_MP LEMMA10 LEMMA8)); val MITBBlockShort2Lemma1 = store_thm ("MITBBlockShort2Lemma1", ``!bkl key r c n f pmem vmem. 2 < r /\ bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl) /\ LENGTH (LAST bkl) <= r - 2 ==> MITB_IMP key (r,c,n) f |= ALWAYS (mitbState (Ready,pmem,vmem) AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r bkl IMPLIES UNTILN (LENGTH bkl) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (TAKE n (f(Absorb f c pmem (FRONT bkl) XOR (LAST bkl ++ [T] ++ Zeros (r-(LENGTH(LAST bkl)+2)) ++ [T] ++ Zeros c)))) AND pmemState pmem)))``, RW_TAC list_ss [] THEN `FRONT(bkl:bits list) ++ [LAST bkl] = bkl` by PROVE_TAC[APPEND_FRONT_LAST] THEN `LENGTH(FRONT(bkl:bits list) ++ [LAST bkl]) = LENGTH bkl` by PROVE_TAC[APPEND_FRONT_LAST] THEN FULL_SIMP_TAC list_ss [] THEN `LENGTH bkl - 1 + 1 = LENGTH bkl` by DECIDE_TAC THEN `LENGTH (LAST bkl) <> r` by DECIDE_TAC THEN `LENGTH (LAST bkl) <> r-1` by DECIDE_TAC THEN IMP_RES_TAC(DISCH_ALL LEMMA11) THEN PROVE_TAC[]); val LEMMA12 = SIMP_RULE list_ss [SplitNotEmpty] (ISPECL [``Split r (msg:bits)``,``key:bits``,``r:num``] MITBBlockShort2Lemma1); val ALWAYS_AND_IMPLIES_EXIST = store_thm ("ALWAYS_AND_IMPLIES_EXIST", ``!dev P Q1 Q2 R. (!x:bits. dev |= ALWAYS(P x AND Q1 AND Q2 IMPLIES R)) ==> (dev |= ALWAYS(((EXIST x. P x) AND Q1 AND Q2) IMPLIES R))``, MC_TAC[]); val ALWAYS_IMPLIES_IMP = store_thm ("ALWAYS_IMPLIES_IMP", ``!dev P Q1 Q2. dev |= ALWAYS(Q1 IMPLIES Q2) ==> dev |= ALWAYS((P IMPLIES Q1) IMPLIES (P IMPLIES Q2))``, MC_TAC[]); val ALWAYS_NEXT_UNTILN_MONO1 = store_thm ("ALWAYS_NEXT_UNTILN_MONO1", ``!dev t P1 P2 P3 P4 P5. (dev |= ALWAYS(P3 IMPLIES P5)) /\ (dev |= ALWAYS(P1 IMPLIES NEXT(P2 IMPLIES UNTILN t P3 P4))) ==> (dev |= ALWAYS(P1 IMPLIES NEXT(P2 IMPLIES UNTILN t P5 P4)))``, PROVE_TAC [ALWAYS_MP,ALWAYS_UNTILN_MONO1,ALWAYS_IMPLIES_IMP,ALWAYS_NEXT_IMP]); (* List of MC type theorems *) val MC_ALWAYS_THMS = [("IMPLIES_IMP",IMPLIES_IMP), ("ALWAYS_ALL",ALWAYS_ALL), ("ALWAYS_AND1",ALWAYS_AND1), ("ALWAYS_AND2",ALWAYS_AND2), ("ALWAYS_AND1_IMPLIES",ALWAYS_AND1_IMPLIES), ("ALWAYS_AND2_IMPLIES",ALWAYS_AND2_IMPLIES), ("ALWAYS_AND_IMPLIES_EXIST",ALWAYS_AND_IMPLIES_EXIST), ("ALWAYS_BOOL_AND_IMPLIES",ALWAYS_BOOL_AND_IMPLIES), ("ALWAYS_BOOL_IMPLIES",ALWAYS_BOOL_IMPLIES), ("ALWAYS_EXIST_IMP",ALWAYS_EXIST_IMP), ("ALWAYS_EXIST_IMP2",ALWAYS_EXIST_IMP2), ("ALWAYS_IMP",ALWAYS_IMP), ("ALWAYS_IMPLIES_IMP",ALWAYS_IMPLIES_IMP), ("ALWAYS_IMP_AND1",ALWAYS_IMP_AND1), ("ALWAYS_IMP_TRANS_AND1",ALWAYS_IMP_TRANS_AND1), ("ALWAYS_IMP_TRANS_AND2",ALWAYS_IMP_TRANS_AND2), ("ALWAYS_IMP_TRANS_AND3",ALWAYS_IMP_TRANS_AND3), ("ALWAYS_IMP_AND2",ALWAYS_IMP_AND2), ("ALWAYS_IMP_NEXT_AND",ALWAYS_IMP_NEXT_AND), ("ALWAYS_IMPLIES_NEXT_AND",ALWAYS_IMPLIES_NEXT_AND), ("ALWAYS_IMP_NEXT_BOOL",ALWAYS_IMP_NEXT_BOOL), ("ALWAYS_IMP_REFL",ALWAYS_IMP_REFL), ("ALWAYS_IMP_TRANS",ALWAYS_IMP_TRANS), ("ALWAYS_IMPLIES_EXIST",ALWAYS_IMPLIES_EXIST), ("ALWAYS_MP",ALWAYS_MP), ("ALWAYS_NEXT",ALWAYS_NEXT), ("ALWAYS_NEXT_IMP",ALWAYS_NEXT_IMP), ("ALWAYS_UNTILN_FOLDL",ALWAYS_UNTILN_FOLDL), ("ALWAYS_UNTILN_FOLDL_LEMMA",ALWAYS_UNTILN_FOLDL_LEMMA), ("ALWAYS_UNTILN_IMP",ALWAYS_UNTILN_IMP), ("ALWAYS_UNTILN_IMP_NEXT",ALWAYS_UNTILN_IMP_NEXT), ("ALWAYS_UNTILN_AND_IMP_NEXT",ALWAYS_UNTILN_AND_IMP_NEXT), ("ALWAYS_UNTILN_AND_IMP",ALWAYS_UNTILN_AND_IMP), ("ALWAYS_UNTILN_AND",ALWAYS_UNTILN_AND), ("ALWAYS_UNTILN_NEXT",ALWAYS_UNTILN_NEXT), ("ALWAYS_IMP_UNTILN_MONO1",ALWAYS_IMP_UNTILN_MONO1), ("ALWAYS_IMP_UNTILN_MONO2",ALWAYS_IMP_UNTILN_MONO2), ("ALWAYS_NEXT_UNTILN_MONO1",ALWAYS_NEXT_UNTILN_MONO1), ("ALWAYS_NEXTN_FOLDL",ALWAYS_NEXTN_FOLDL), ("ALWAYS_NEXTN_FOLDL_LEMMA",ALWAYS_NEXTN_FOLDL_LEMMA), ("ALWAYS_UNTILN_MONO1",ALWAYS_UNTILN_MONO1), ("ALWAYS_UNTILN_MONO2",ALWAYS_UNTILN_MONO2)]; (* EXIST-quantify vmem in LEMMA12 *) val LEMMA13 = MATCH_MP (SIMP_RULE std_ss [] (SPECL [``MITB_IMP key (r,c,n) f``, ``\vmem. mitbState (Ready,pmem,vmem)``] ALWAYS_AND_IMPLIES_EXIST)) (GEN ``vmem:bits`` (UNDISCH_ALL(SPEC_ALL LEMMA12))); (* Hide initial state *) val LEMMA14 = prove (``!pmem. MITB_IMP key (r,c,n) f |= ALWAYS (pmemState pmem AND readyOut T IMPLIES EXIST vmem. mitbState(Ready,pmem,vmem))``, MC_TAC[] THEN Q.EXISTS_TAC `vmem_sig t` THEN RW_TAC std_ss []); (* Combine LEMMA13 and LEMMA14 *) val MITBBlockShort2Lemma2 = store_thm ("MITBBlockShort2Lemma2", ``2 < r /\ LENGTH (LAST (Split r msg)) <= r-2 ==> MITB_IMP key (r,c,n) f |= ALWAYS (pmemState pmem AND readyOut T AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (LENGTH (Split r msg)) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (TAKE n (f(Absorb f c pmem (FRONT (Split r msg)) XOR (LAST (Split r msg) ++ [T] ++ Zeros (r - (LENGTH (LAST (Split r msg)) + 2)) ++ [T] ++ Zeros c)))) AND pmemState pmem)))``, RW_TAC std_ss [] THEN `0 < r` by DECIDE_TAC THEN IMP_RES_TAC LengthEveryFrontSplit THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) THEN ASSUME_TAC (DISCH_ALL (SIMP_RULE std_ss [AND_ASSOC] (MATCH_MP (MATCH_MP ALWAYS_IMP_TRANS_AND1 (SPEC_ALL LEMMA14)) LEMMA13))) THEN RES_TAC); (* Special case of MITBBlockShort2Lemma2 *) val MITBBlockShort2Lemma3 = store_thm ("MITBBlockShort2Lemma3", ``2 < r /\ LENGTH msg <= r-2 ==> MITB_IMP key (r,c,n) f |= ALWAYS (pmemState pmem AND readyOut T AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (LENGTH (Split r msg)) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (TAKE n (f(pmem XOR (Pad r msg ++ Zeros c)))) AND pmemState pmem)))``, RW_TAC std_ss [] THEN `1 < r` by DECIDE_TAC THEN RW_TAC std_ss [PadZerosCor1,Pad_def] THEN `LENGTH msg <= r` by DECIDE_TAC THEN `Split r msg = [msg]` by PROVE_TAC[Split_def] THEN `LAST(Split r msg) = msg` by PROVE_TAC[LAST_CONS] THEN `FRONT(Split r msg) = []` by PROVE_TAC[FRONT_CONS] THEN `LENGTH (LAST (Split r msg)) <= r-2` by PROVE_TAC[] THEN IMP_RES_TAC MITBBlockShort2Lemma2 THEN ASSUM_LIST (fn thl => ASSUME_TAC (SIMP_RULE std_ss [Absorb_def,el 3 thl,el 4 thl,el 5 thl] (SPEC_ALL(el 1 thl)))) THEN RW_TAC std_ss []); (* Complete proof when LENGTH msg <= r-2 *) val MITBBlockShort2Lemma4 = store_thm ("MITBBlockShort2Lemma4", ``2 < r /\ LENGTH msg <= r-2 ==> MITB_IMP key (r,c,n) f |= ALWAYS (pmemState pmem AND readyOut T AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (LENGTH (Split r msg)) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut(Hash (r,c,n) f pmem msg) AND pmemState pmem)))``, RW_TAC std_ss [Hash_def,Output_def] THEN `Split r (Pad r msg) = [msg ++ [T] ++ Zeros (r - (LENGTH msg + 2)) ++ [T]]` by PROVE_TAC[SplitPadLemma1] THEN RW_TAC std_ss [Absorb_def,Pad_def] THEN `LENGTH msg <= r` by DECIDE_TAC THEN `Split r msg = [msg]` by PROVE_TAC[Split_def] THEN `LAST(Split r msg) = msg` by PROVE_TAC[LAST_CONS] THEN `FRONT(Split r msg) = []` by PROVE_TAC[FRONT_CONS] THEN `LENGTH (LAST (Split r msg)) <= r-2` by PROVE_TAC[] THEN IMP_RES_TAC MITBBlockShort2Lemma2 THEN ASSUM_LIST (fn thl => ASSUME_TAC (SIMP_RULE std_ss [XOREqXor,Absorb_def,el 3 thl,el 4 thl,el 5 thl] (SPEC_ALL(el 1 thl)))) THEN RW_TAC std_ss []); (* Complete proof when LENGTH msg MOD r <= r-2 (consequence of MITBBlockShort2Lemma2) *) val MITBBlockShort2Lemma5 = store_thm ("MITBBlockShort2Lemma5", ``!r msg. 2 < r /\ r < LENGTH msg /\ 0 < LENGTH msg MOD r /\ LENGTH msg MOD r <= r - 2 ==> MITB_IMP key (r,c,n) f |= ALWAYS (pmemState pmem AND readyOut T AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (LENGTH (Split r msg)) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut(Hash (r,c,n) f pmem msg) AND pmemState pmem)))``, RW_TAC std_ss [AbsorbSplitPadShort2,Hash_def,Output_def] THEN `0 < r` by DECIDE_TAC THEN `LENGTH msg MOD r = LENGTH (LAST (Split r msg))` by PROVE_TAC[LengthLastSplit] THEN `LENGTH (LAST (Split r msg)) <= r - 2` by PROVE_TAC[LengthLastSplit] THEN RW_TAC std_ss [GSYM XOREqXor, MITBBlockShort2Lemma2]); (* Combine MITBBlockShort2Lemma4, MITBBlockShort2Lemma5 *) val MITBBlockShort2Lemma6 = store_thm ("MITBBlockShort2Lemma6", ``!r msg. 2 < r /\ 0 < LENGTH msg MOD r /\ LENGTH msg MOD r <= r - 2 ==> MITB_IMP key (r,c,n) f |= ALWAYS (pmemState pmem AND readyOut T AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (LENGTH (Split r msg)) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut(Hash (r,c,n) f pmem msg) AND pmemState pmem)))``, RW_TAC std_ss [] THEN `LENGTH msg <= r \/ r < LENGTH msg` by DECIDE_TAC THENL [`0 < r /\ LENGTH msg MOD r <> 0` by DECIDE_TAC THEN `LENGTH msg < r` by PROVE_TAC[MOD_NEQ0_LESS] THEN `LENGTH msg <= r - 2` by PROVE_TAC[LESS_MOD] THEN RW_TAC std_ss [MITBBlockShort2Lemma4], RW_TAC std_ss [MITBBlockShort2Lemma5]]); (* Now replay (and/or improve) the "Short2" development for "Full" *) (* dev |= ALWAYS(P IMPLIES UNTILN t Q ((R1 AND NEXT R2) AND R3)) *) val LEMMA2_Full = (DISCH_ALL (SIMP_RULE list_ss [ASSUME ``LENGTH (LAST(bkl:bits list)) = r``, ALWAYS_BOOL_AND_IMPLIES, BOOL_T_AND,BOOL_T_IMPLIES,BOOL_F_IMPLIES] (SPEC_ALL LEMMA1))); (* dev |= ALWAYS(R1 AND R3 IMPLIES NEXT R4) *) val LEMMA3_Full = MATCH_MP ALWAYS_IMP_NEXT_BOOL (INST [``bk:bits`` |-> ``LAST bkl:bits``, ``vmem:bits`` |-> ``Absorb f c vmem (FRONT bkl)``] (SPEC_ALL (SIMP_RULE list_ss [ALWAYS_ALL,Once AND_SYM] MITB_AbsorbBlockFull))); (* Term abbbreviations used below *) val dev = ``MITB_IMP key (r,c,n) f`` and P = ``InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem)`` and R1 = ``skipInp F`` and R2 = ``moveInp F`` and R3 = ``readyOut F`` and R4 = ``digestOut (Zeros n)`` and R5 = ``InputBlock []`` and R6 = ``mitbState (Absorbing,pmem, f(Absorb f c vmem (FRONT(bkl:bits list)) XOR (LAST bkl ++ ZEROS c)))`` and R7 = ``blockInp []`` and R8 = ``sizeInp 0`` and R9 = ``mitbState (Ready,pmem, f(f(Absorb f c vmem (FRONT(bkl:bits list)) XOR (LAST bkl ++ ZEROS c)) XOR (T::(ZEROS (r - 2) ++ [T] ++ ZEROS c))))`` and R10 = ``InputBlock (LAST(bkl:bits list))`` and R11 = ``NEXT (skipInp F AND moveInp F)`` and R12 = ``mitbState (Absorbing,pmem,Absorb f c vmem (FRONT(bkl:bits list)))`` and R13 = ``blockInp (LAST(bkl:bits list))`` and R14 = ``sizeInp (r - 1)`` and R15 = ``mitbState (AbsorbEnd,pmem, f(vmem XOR (TAKE(r-1) (LAST bkl) ++ [T] ++ ZEROS c)))`` and R16 = ``mitbState(AbsorbEnd,pmem,vmem)`` and R17 = ``mitbState (Ready,pmem,f(vmem XOR (ZEROS (r-1) ++ [T] ++ ZEROS c)))`` ; (* val LEMMA5_Full = [..] |- MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1 + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (InputBlock [] AND mitbState (Absorbing,pmem, f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ ZEROS c))))) dev |= ALWAYS(P IMPLIES UNTILN t (R1 AND R2 AND R3 AND R4) (R5 AND R6)) *) val LEMMA5_Full = SIMP_RULE list_ss [] (* [InputBlock_def] *) (MATCH_MP (MATCH_MP (MATCH_MP ALWAYS_UNTILN_AND_IMP_NEXT LEMMA4) (UNDISCH_ALL LEMMA2_Full)) (UNDISCH_ALL LEMMA3_Full)); (* val MITB_EndAbsorbingFull = |- MITB_IMP key (r,c,n) f |= ALWAYS (readyOut F AND skipInp F AND moveInp F AND blockInp [] AND sizeInp 0 AND mitbState (Absorbing,pmem, f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ ZEROS c))) IMPLIES NEXT (mitbState (Ready,pmem, f (f (Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ ZEROS c)) XOR (T::(ZEROS (r - 2) ++ [T] ++ ZEROS c)))))) dev |= ALWAYS(R3 AND R1 AND R2 AND R7 AND R8 AND R6 IMPLIES NEXT R9) *) val MITB_EndAbsorbingFull = SIMP_RULE list_ss [GSYM mitbState,BOOL_T_AND] (SPECL [``[]:bits``, ``0``, ``pmem:bits``, ``f(Absorb f c vmem (FRONT bkl) XOR (LAST bkl ++ ZEROS c))``] (SIMP_RULE std_ss [ALWAYS_ALL] MITB_EndAbsorbingLenLeq2)); val LEMMA5_SUB_LEMMA1 = prove (``^dev |= ALWAYS ((^R5 AND ^R6) IMPLIES (^R3 AND ^R1 AND ^R2 AND ^R7 AND ^R8 AND ^R6))``, MC_TAC[]); val LEMMA5_SUB_LEMMA2 = prove (``^dev |= ALWAYS ((^R5 AND ^R6) IMPLIES (^R1 AND ^R2 AND ^R3 AND ^R4))``, MC_TAC[]); val LEMMA5_SUB_LEMMA3 = prove (``!dev t P R1 R2 R3 R4 R5 R6 R7 R8 R9. (* LEMMA5_Full *) dev |= ALWAYS(P IMPLIES UNTILN t (R1 AND R2 AND R3 AND R4) (R5 AND R6)) ==> (* MITB_EndAbsorbingFull *) dev |= ALWAYS(R3 AND R1 AND R2 AND R7 AND R8 AND R6 IMPLIES NEXT R9) ==> (* LEMMA5_SUB_LEMMA1 *) dev |= ALWAYS((R5 AND R6) IMPLIES (R3 AND R1 AND R2 AND R7 AND R8 AND R6)) ==> (* LEMMA5_SUB_LEMMA2 *) dev |= ALWAYS((R5 AND R6) IMPLIES (R1 AND R2 AND R3 AND R4)) ==> dev |= ALWAYS(P IMPLIES UNTILN (t+1) (R1 AND R2 AND R3 AND R4) R9)``, RW_TAC std_ss [] THEN `dev |= ALWAYS((R5 AND R6) IMPLIES (R5 AND R6) AND NEXT R9)` by PROVE_TAC [ALWAYS_IMP_TRANS_AND2] THEN `dev |= ALWAYS (P IMPLIES UNTILN t (R1 AND R2 AND R3 AND R4) ((R5 AND R6) AND NEXT R9))` by PROVE_TAC[ALWAYS_IMP_TRANS,ALWAYS_UNTILN_MONO2] THEN PROVE_TAC[ALWAYS_UNTILN_IMP_NEXT,ALWAYS_IMP_TRANS]); val LEMMA6_SUB_LEMMA1 = prove (``!r msg. 2 < r /\ msg <> [] /\ (LENGTH msg MOD r = 0) ==> (LENGTH (LAST (Split r msg)) = r)``, RW_TAC list_ss [] THEN `1 < r` by DECIDE_TAC THEN RW_TAC std_ss [LENGTH_LAST_Split]); val LEMMA6_SUB_LEMMA2 = (SIMP_RULE list_ss [XOREqXor,ZEROSEqZeros,SplitNotEmpty,LengthEveryFrontSplit] o Q.SPEC `Split r msg` o Q.GEN `bkl` o DISCH_ALL o ADD_ASSUM ``LENGTH(msg:bits) MOD r = 0`` o ADD_ASSUM ``(msg:bits) <> []`` o ADD_ASSUM ``2 < r``) (MP (MP ((MP (MP (SPECL [``MITB_IMP key (r,c,n) f``, ``LENGTH(bkl:bits list)-1+1``, P,R1,R2,R3,R4,R5,R6,R7,R8,R9] LEMMA5_SUB_LEMMA3) LEMMA5_Full) MITB_EndAbsorbingFull)) LEMMA5_SUB_LEMMA1) LEMMA5_SUB_LEMMA2); val LEMMA6_Full = store_thm ("LEMMA6_Full", ``!key msg r c n f. 2 < r /\ msg <> [] /\ (LENGTH msg MOD r = 0) ==> MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r (Split r msg) AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH (Split r msg) + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (mitbState (Ready,pmem,Absorb f c vmem (Split r (Pad r msg)))))``, RW_TAC std_ss [] THEN IMP_RES_TAC LEMMA6_SUB_LEMMA1 THEN `0 < LENGTH (Split r msg)` by PROVE_TAC[SplitLengthsLemma2] THEN `LENGTH(Split r msg) + 1 = LENGTH(Split r msg) - 1 + 1 + 1` by DECIDE_TAC THEN RW_TAC std_ss [LEMMA6_SUB_LEMMA2,AbsorbSplitPadFull]); (* val LEMMA10_Full = |- 2 < r /\ msg <> [] /\ (LENGTH msg MOD r = 0) ==> MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r (Split r msg) AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH (Split r msg) + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (Hash (r,c,n) f vmem msg) AND pmemState pmem)) *) val LEMMA10_Full = DISCH_ALL (MP (SPECL [``LENGTH(Split r (msg:bits))+1``, ``InputBlocks r (Split r (msg:bits)) AND mitbState (Absorbing,pmem,vmem)``, ``skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)``] (SIMP_RULE std_ss [GSYM Output_def,GSYM Hash_def] (MATCH_MP ALWAYS_IMP_UNTILN_MONO2 (SPEC ``Absorb f c vmem (Split r (Pad r msg))`` LEMMA9)))) (UNDISCH_ALL(SPEC_ALL LEMMA6_Full))); (* Complete proof when LENGTH msg MOD r = 0 val LEMMA11_Full = |- 2 < r /\ msg <> [] /\ (LENGTH msg MOD r = 0) ==> MITB_IMP key (r,c,n) f |= ALWAYS (mitbState (Ready,pmem,vmem) AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (LENGTH (Split r msg) + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (Hash (r,c,n) f pmem msg) AND pmemState pmem))) *) val LEMMA11_Full = DISCH_ALL (MP (MP (SPECL [``MITB_IMP key (r,c,n) f``, ``mitbState (Ready,pmem,vmem) AND skipInp F AND moveInp T``, ``mitbState (Absorbing,pmem,pmem)``, ``InputBlocks r (Split r msg)``, ``UNTILN (LENGTH (Split r msg) + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (Hash (r,c,n) f pmem msg) AND pmemState pmem)``] ALWAYS_IMP_NEXT_AND) (SPEC_ALL(SIMP_RULE std_ss [ALWAYS_ALL] MITB_StartAbsorbing))) (INST[``vmem:bits``|->``pmem:bits``](UNDISCH_ALL LEMMA10_Full))); (* val LEMMA12_Full = [.] |- MITB_IMP key (r,c,n) f |= ALWAYS ((EXIST x. mitbState (Ready,pmem,x)) AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (LENGTH (Split r msg) + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (Hash (r,c,n) f pmem msg) AND pmemState pmem))) *) val LEMMA12_Full = MATCH_MP (SIMP_RULE std_ss [] (SPECL [``MITB_IMP key (r,c,n) f``, ``\vmem. mitbState (Ready,pmem,vmem)``] ALWAYS_AND_IMPLIES_EXIST)) (GEN ``vmem:bits`` (UNDISCH_ALL(SPEC_ALL LEMMA11_Full))); (* val LEMMA13_Full = |- 2 < r /\ msg <> [] /\ (LENGTH msg MOD r = 0) ==> MITB_IMP key (r,c,n) f |= ALWAYS (pmemState pmem AND readyOut T AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (LENGTH (Split r msg) + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (Hash (r,c,n) f pmem msg) AND pmemState pmem))) *) val LEMMA13_Full = (SIMP_RULE list_ss [AND_ASSOC] o DISCH_ALL) (MATCH_MP (MATCH_MP ALWAYS_IMP_TRANS_AND1 (SPEC_ALL LEMMA14)) LEMMA12_Full); (* Now replay (and/or improve) the "Short2", and "Full" developments for "Short1" *) (* dev |= ALWAYS(P IMPLIES UNTILN t Q ((R1 AND NEXT R2) AND R3)) *) val LEMMA2_Short1 = (DISCH_ALL (SIMP_RULE list_ss [ASSUME ``2 < r /\ (LENGTH (LAST(bkl:bits list)) = r-1)``, ALWAYS_BOOL_AND_IMPLIES, BOOL_T_AND,BOOL_T_IMPLIES,BOOL_F_IMPLIES] (SPEC_ALL LEMMA1))); (* if len = r-1 then (* Exactly one-bit too small *) (AbsorbEnd, pmem, f(vmem XOR (TAKE len blk ++ [T] ++ ZEROS c))) *) val MITB_EndAbsorbingLenLeq1 = store_thm ("MITB_EndAbsorbingLenLeq1", ``!bkl key r c n f pmem vmem. (LENGTH(LAST bkl) = r - 1) ==> MITB_IMP key (r,c,n) f |= ALWAYS (readyOut F AND skipInp F AND moveInp F AND blockInp(LAST bkl) AND sizeInp(r-1) AND mitbState(Absorbing, pmem, vmem) IMPLIES NEXT (mitbState (AbsorbEnd,pmem, f(vmem XOR (TAKE (r-1) (LAST bkl) ++ [T] ++ ZEROS c)))))``, MC_TAC[] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE (srw_ss()) [el 1 thl,el 2 thl,el 3 thl,el 4 thl,el 5 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 9 thl)))) THEN `2 < LENGTH key` by PROVE_TAC[GoodParameters_def] THEN `~(LENGTH key <= 1 + (LENGTH key - 2))` by DECIDE_TAC THEN POP_ASSUM(fn th => FULL_SIMP_TAC std_ss [th])); (* MITB_FUN (r,c,n) f (AbsorbEnd,pmem,vmem) (Input blk len) = (Ready, pmem, f(vmem XOR (ZEROS(r-1) ++ [T] ++ ZEROS c))) *) val MITB_AbsorbEnd = store_thm ("MITB_AbsorbEnd", ``!key r c n f pmem vmem. MITB_IMP key (r,c,n) f |= ALWAYS (readyOut F AND skipInp F AND moveInp F AND mitbState(AbsorbEnd, pmem, vmem) IMPLIES NEXT (mitbState (Ready,pmem,f(vmem XOR (ZEROS(r-1) ++ [T] ++ ZEROS c)))))``, MC_TAC[] THEN ASSUM_LIST (fn thl => STRIP_ASSUME_TAC (SIMP_RULE (srw_ss()) [el 1 thl,el 2 thl,el 3 thl, MITB_FUN_def,ZEROSEqZeros] (SPEC ``t:num`` (el 7 thl))))); val dev = ``MITB_IMP key (r,c,n) f`` and len = ``LENGTH(bkl : bits list) - 1`` and T1 = ``mitbState (Ready,pmem,vmem)`` and T2 = ``skipInp F`` and T3 = ``moveInp T`` and T4 = ``mitbState (Absorbing,pmem,pmem)`` and T5 = ``InputBlocks r (bkl : bits list)`` and T6 = ``moveInp F `` and T7 = ``readyOut F`` and T8 = ``digestOut (Zeros n)`` and T9 = ``InputBlock (LAST (bkl : bits list))`` and T10 = ``mitbState (Absorbing,pmem,Absorb f c vmem (FRONT (bkl : bits list)))`` and T11 = ``blockInp (LAST (bkl : bits list))`` and T12 = ``sizeInp (r - 1)`` and T13 = ``mitbState (AbsorbEnd,pmem, f (vmem XOR (TAKE (r - 1) (LAST (bkl : bits list)) ++ [T] ++ ZEROS c)))`` and T14 = ``mitbState (AbsorbEnd,pmem,vmem)`` and T15 = ``mitbState (Ready,pmem,f (vmem XOR (ZEROS (r - 1) ++ [T] ++ ZEROS c)))`` and T16 = ``mitbState (Absorbing,pmem,vmem)`` and T17 = ``mitbState (AbsorbEnd,pmem, f(Absorb f c vmem (FRONT(bkl : bits list)) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c)))`` and T18 = ``mitbState (Ready,pmem, f(f(Absorb f c vmem (FRONT bkl) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c)) XOR (ZEROS (r - 1) ++ [T] ++ ZEROS c)))``; (* 1. Expand the NEXT in (UNDISCH_ALL LEMMA2_Short1) using (UNDISCH_ALL(SPEC_ALL MITB_EndAbsorbingLenLeq1)) and ALWAYS_IMP_UNTILN_MONO2. *) val PlanLemma1_1 = prove (``^dev |= ALWAYS(^T10 IMPLIES ^T7)``, MC_TAC[]); val PlanLemma1_2 = prove (``dev |= ALWAYS(T10 IMPLIES T7) ==> dev |= ALWAYS(T7 AND T2 AND T6 AND T11 AND T12 AND T10 IMPLIES NEXT T17) ==> dev |= ALWAYS ((((T11 AND T12 AND T2 AND T6) AND NEXT(T2 AND T6)) AND T10) IMPLIES ((T11 AND T12 AND T2 AND T6 AND T10) AND NEXT((T2 AND T6) AND T17)))``, MC_TAC[]); val PlanLemma1_3 = prove (``^dev |= ALWAYS(^T10 IMPLIES ^T7) ==> ^dev |= ALWAYS (^T7 AND ^T2 AND ^T6 AND ^T11 AND ^T12 AND ^T10 IMPLIES NEXT ^T17) ==> ^dev |= ALWAYS ((((^T11 AND ^T12 AND ^T2 AND ^T6) AND NEXT(^T2 AND ^T6)) AND ^T10) IMPLIES ((^T11 AND ^T12 AND ^T2 AND ^T6 AND ^T10) AND NEXT((^T2 AND ^T6) AND ^T17)))``, PURE_REWRITE_TAC[PlanLemma1_2]); val PlanLemma1_4 = MP (MP PlanLemma1_3 PlanLemma1_1) (UNDISCH_ALL (INST [``vmem:bits``|->``Absorb f c vmem (FRONT(bkl:bits list))``] (SPEC_ALL MITB_EndAbsorbingLenLeq1))); (* val PlanLemma1 = |- (LENGTH (LAST bkl) = r - 1) ==> 2 < r /\ (LENGTH (LAST bkl) = r - 1) ==> bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl) ==> MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((blockInp (LAST bkl) AND sizeInp (r - 1) AND skipInp F AND moveInp F AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) AND NEXT ((skipInp F AND moveInp F) AND mitbState (AbsorbEnd,pmem, f (Absorb f c vmem (FRONT bkl) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c)))))) *) val PlanLemma1 = (*DISCH_ALL*) (MATCH_MP (MATCH_MP ALWAYS_IMP_UNTILN_MONO2 PlanLemma1_4) (UNDISCH_ALL (SIMP_RULE std_ss [InputBlock_def] LEMMA2_Short1))); (* 2. Use ALWAYS_UNTILN_IMP_NEXT to get UNTILN (LENGTH bkl - 1 + 1) *) val PlanLemma2_1 = prove (``^dev |= ALWAYS (^T11 AND ^T12 AND ^T2 AND ^T6 AND ^T10 IMPLIES ^T2 AND ^T6 AND ^T7 AND ^T8)``, MC_TAC[]); (* val PlanLemma2_1 = |- MITB_IMP key (r,c,n) f |= ALWAYS (UNTILN (LENGTH bkl - 1) (UNTILN (LENGTH bkl - 1 + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (mitbState (AbsorbEnd,pmem, f (Absorb f c vmem (FRONT bkl) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c))))) (UNTILN (LENGTH bkl - 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((blockInp (LAST bkl) AND sizeInp (r - 1) AND skipInp F AND moveInp F AND mitbState (Absorbing,pmem,Absorb f c vmem (FRONT bkl))) AND NEXT (mitbState (AbsorbEnd,pmem, f (Absorb f c vmem (FRONT bkl) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c))))) AND NEXT ((skipInp F AND moveInp F) AND mitbState (AbsorbEnd,pmem, f (Absorb f c vmem (FRONT bkl) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c))))) IMPLIES UNTILN (LENGTH bkl - 1 + 1) (UNTILN (LENGTH bkl - 1 + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (mitbState (AbsorbEnd,pmem, f (Absorb f c vmem (FRONT bkl) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c))))) ((skipInp F AND moveInp F) AND mitbState (AbsorbEnd,pmem, f (Absorb f c vmem (FRONT bkl) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c))))) *) val PlanLemma2_2 = SPECL [``LENGTH(bkl : bits list) - 1``,``(^T2 AND ^T6) AND ^T17``] (MATCH_MP ALWAYS_UNTILN_IMP_NEXT PlanLemma2_1) ; (* DISCH_ALL PlanLemma2_3; |- (LENGTH (LAST bkl) = r - 1) ==> 2 < r /\ (LENGTH (LAST bkl) = r - 1) ==> bkl <> [] /\ EVERY (\l. LENGTH l = r) (FRONT bkl) ==> MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r bkl AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH bkl - 1 + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) ((skipInp F AND moveInp F) AND mitbState (AbsorbEnd,pmem, f (Absorb f c vmem (FRONT bkl) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c))))) *) val PlanLemma2_3 = MATCH_MP (MATCH_MP ALWAYS_IMP_TRANS PlanLemma1) PlanLemma2_2 (* 3. Repeat with (SPEC_ALL MITB_AbsorbEnd) to get UNTILN (LENGTH bkl - 1 + 1 + 1) *) val PlanLemma3_1 = INST [``vmem:bits`` |-> ``f(Absorb f c vmem (FRONT bkl) XOR (TAKE (r - 1) (LAST bkl) ++ [T] ++ ZEROS c))``] (SPEC_ALL MITB_AbsorbEnd); val PlanLemma3_2 = prove (``dev |= ALWAYS(T17 IMPLIES T7) ==> dev |= ALWAYS(T7 AND T2 AND T6 AND T17 IMPLIES NEXT T18) ==> dev |= ALWAYS((T2 AND T6) AND T17 IMPLIES ((T2 AND T6) AND T17) AND NEXT T18)``, MC_TAC[]); val PlanLemma3_3 = prove (``^dev |= ALWAYS(^T17 IMPLIES ^T7) ==> ^dev |= ALWAYS(^T7 AND ^T2 AND ^T6 AND ^T17 IMPLIES NEXT ^T18) ==> ^dev |= ALWAYS((^T2 AND ^T6) AND ^T17 IMPLIES ((^T2 AND ^T6) AND ^T17) AND NEXT ^T18)``, PURE_REWRITE_TAC[PlanLemma3_2]); val PlanLemma3_4 = prove (``^dev |= ALWAYS(^T17 IMPLIES ^T7)``, MC_TAC[]); val PlanLemma3_5 = MP (ISPECL [``LENGTH(bkl : bits list) - 1 + 1``, ``^T5 AND ^T16``, ``^T2 AND ^T6 AND ^T7 AND ^T8``] (MATCH_MP ALWAYS_IMP_UNTILN_MONO2 (MP (MP PlanLemma3_3 PlanLemma3_4) PlanLemma3_1))) PlanLemma2_3; val PlanLemma3_6 = prove (``^dev |= ALWAYS((^T2 AND ^T6) AND ^T17 IMPLIES ^T2 AND ^T6 AND ^T7 AND ^T8)``, MC_TAC[]); val PlanLemma3_7 = SPECL [``LENGTH(bkl : bits list) - 1 + 1``,T18] (MATCH_MP ALWAYS_UNTILN_IMP_NEXT PlanLemma3_6); val PlanLemma3 = (SIMP_RULE list_ss [SplitNotEmpty,XOREqXor,ZEROSEqZeros, LengthEveryFrontSplit] o Q.SPEC `Split r msg` o Q.GEN `bkl` o DISCH_ALL) (MATCH_MP (MATCH_MP ALWAYS_IMP_TRANS PlanLemma3_5) PlanLemma3_7); val LENGTH_LAST_SplitShort1 = store_thm ("LENGTH_LAST_SplitShort1", ``!r msg. 2 < r /\ (LENGTH msg MOD r = r - 1) ==> (LENGTH (LAST (Split r msg)) = r - 1)``, RW_TAC std_ss [] THEN `1 < r` by DECIDE_TAC THEN Cases_on `msg=[]` THEN FULL_SIMP_TAC list_ss [] THEN `LENGTH msg MOD r <> 0` by DECIDE_TAC THEN RW_TAC std_ss [LENGTH_LAST_Split]); val PlanLemma4_1 = prove (``2 < r /\ (LENGTH msg MOD r = r - 1) ==> MITB_IMP key (r,c,n) f |= ALWAYS (InputBlocks r (Split r msg) AND mitbState (Absorbing,pmem,vmem) IMPLIES UNTILN (LENGTH (Split r msg) + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (mitbState(Ready,pmem,Absorb f c vmem (Split r (Pad r msg)))))``, RW_TAC list_ss [AbsorbSplitPadShort1] THEN `0 < LENGTH(Split r msg)` by PROVE_TAC[SplitLengthsLemma2] THEN `LENGTH (Split r msg) - 1 + 1 + 1 = LENGTH (Split r msg) + 1` by DECIDE_TAC THEN PROVE_TAC[LENGTH_LAST_SplitShort1,PlanLemma3]); val PlanLemma4_2 = (SIMP_RULE std_ss [GSYM Output_def,GSYM Hash_def] o DISCH_ALL) (MATCH_MP (MATCH_MP ALWAYS_IMP_UNTILN_MONO2 (SPEC ``Absorb f c vmem (Split r (Pad r msg))`` LEMMA9)) (UNDISCH_ALL PlanLemma4_1)); (* Complete proof when Short1 *) val PlanLemma4_3 = DISCH_ALL (MATCH_MP (MATCH_MP ALWAYS_IMP_NEXT_AND (SPEC_ALL(SIMP_RULE std_ss [ALWAYS_ALL] MITB_StartAbsorbing))) (INST[``vmem:bits``|->``pmem:bits``](UNDISCH_ALL PlanLemma4_2))); val PlanLemma4_4 = MATCH_MP (SIMP_RULE std_ss [] (SPECL [``MITB_IMP key (r,c,n) f``, ``\vmem. mitbState (Ready,pmem,vmem)``] ALWAYS_AND_IMPLIES_EXIST)) (GEN ``vmem:bits`` (UNDISCH_ALL(SPEC_ALL PlanLemma4_3))); (* val PlanLemma4_5 = |- 2 < r /\ (LENGTH msg MOD r = r - 1) ==> MITB_IMP key (r,c,n) f |= ALWAYS (pmemState pmem AND readyOut T AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (LENGTH (Split r msg) + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (Hash (r,c,n) f pmem msg) AND pmemState pmem))) *) val PlanLemma4_5 = (SIMP_RULE list_ss [AND_ASSOC] o DISCH_ALL) (MATCH_MP (MATCH_MP ALWAYS_IMP_TRANS_AND1 (SPEC_ALL LEMMA14)) PlanLemma4_4); (* Cases to be stiched together *) val MITBCasesThm = store_thm ("MITBCasesThm", ``!m n. 2 < n ==> (m <= n - 2 \/ (0 < m MOD n /\ m MOD n <= n - 2) \/ (m MOD n = n - 1) \/ (m <> 0 /\ (m MOD n = 0)))``, RW_TAC arith_ss [] THEN Cases_on `m MOD n = 0` THEN RW_TAC arith_ss [] THEN Cases_on `m <= n - 2` THEN RW_TAC arith_ss [] THEN Cases_on `m MOD n = r - 1` THEN RW_TAC arith_ss [] THEN `0 < n` by DECIDE_TAC THEN `m MOD n < n` by PROVE_TAC[MOD_LESS] THEN DECIDE_TAC); (* Failed attempt to simplify cases val MITBCasesSimpLemma = prove (``!m n. 2 < n ==> (m <= n-2 \/ (0 < m MOD n /\ m MOD n <= n-2) = 0 < m MOD n \/ m <= n - 2 \/ m MOD n <= n - 2)``, RW_TAC arith_ss [] *) (* Yay! Final complete theorem for hash computation! *) (* Number of steps to compute the hash *) val StepCount_def = Define `StepCount r msg = if LENGTH msg MOD r = r - 1 then LENGTH msg DIV r + 2 else LENGTH msg DIV r + 1`; val StepCountLemma = store_thm ("StepCountLemma", ``!r msg. 2 < r ==> (StepCount r msg = if LENGTH msg <= r-2 \/ (0 < LENGTH msg MOD r /\ LENGTH msg MOD r <= r-2) then LENGTH(Split r msg) else LENGTH(Split r msg) + 1)``, RW_TAC list_ss [LengthSplit,StepCount_def] THEN FULL_SIMP_TAC list_ss [ZERO_MOD,ZERO_DIV] THENL [Cases_on `0 < r` THEN FULL_SIMP_TAC list_ss [ZERO_MOD], Cases_on `2 < r` THEN FULL_SIMP_TAC list_ss [], Cases_on `2 < r` THEN FULL_SIMP_TAC list_ss [LENGTH_NIL], Cases_on `2 < r` THEN FULL_SIMP_TAC list_ss [DECIDE ``~(m <= n) = n < m``] THEN `0 < r` by DECIDE_TAC THEN `LENGTH msg MOD r < r` by PROVE_TAC[MOD_LESS] THEN DECIDE_TAC]); val ComputeHash = store_thm ("ComputeHash", ``!key r c n f pmem msg. 2 < r ==> MITB_IMP key (r,c,n) f |= ALWAYS (pmemState pmem AND readyOut T AND skipInp F AND moveInp T IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (StepCount r msg) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (Hash (r,c,n) f pmem msg) AND pmemState pmem)))``, REPEAT STRIP_TAC THEN IMP_RES_TAC(ISPECL[``r:num``,``msg : bits``]StepCountLemma) THEN SIMP_TAC std_ss [] THEN IMP_RES_TAC(SPECL[``LENGTH(msg : bits)``,``r:num``]MITBCasesThm) THEN POP_ASSUM(STRIP_ASSUME_TAC o SIMP_RULE std_ss [LENGTH_NIL] o SPEC_ALL) THEN RW_TAC std_ss [] THEN RW_TAC std_ss [MITBBlockShort2Lemma4,MITBBlockShort2Lemma6, PlanLemma4_5,LEMMA13_Full]); val MAC_def = Define `MAC (r,c,n) f key msg = Hash (r,c,n) f (Zeros(r+c)) (key ++ msg)`; (* Old versions val ComputeMAC_def = Define `ComputeMAC key (r,c,n) f = ALWAYS (ALL msg. (readyOut T AND skipInp F AND moveInp T AND pmemState(f(key ++ Zeros c))) IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (if LENGTH msg MOD r = r-1 then LENGTH msg DIV r + 2 else LENGTH msg DIV r + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (MAC (r,c,n) f key msg) AND pmemState(f(key ++ Zeros c)))))`; val ComputeMAC_def = Define `ComputeMAC (r,c,n) f = ALWAYS (ALL key msg. (readyOut T AND skipInp F AND moveInp T AND BOOL(LENGTH key = r) AND pmemState(f(key ++ Zeros c))) IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (if LENGTH msg MOD r = r-1 then LENGTH msg DIV r + 2 else LENGTH msg DIV r + 1) (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (MAC (r,c,n) f key msg) AND pmemState(f(key ++ Zeros c)))))`; *) val ComputeMAC_def = Define `ComputeMAC (r,c,n) f = ALWAYS (ALL key msg. (readyOut T AND skipInp F AND moveInp T AND BOOL(LENGTH key = r) AND pmemState(f(key ++ Zeros c))) IMPLIES NEXT (InputBlocks r (Split r msg) IMPLIES UNTILN (if LENGTH msg MOD r = r-1 then LENGTH msg DIV r + 2 else LENGTH msg DIV r + 1) (readyOut F AND digestOut (Zeros n)) (readyOut T AND digestOut (MAC (r,c,n) f key msg) AND pmemState(f(key ++ Zeros c)))))`; val SplitKey = store_thm ("SplitKey", ``!r bk l. 0 < r /\ (LENGTH bk = r) /\ l <> [] ==> (Split r (bk ++ l) = bk :: Split r l)``, RW_TAC std_ss [] THEN CONV_TAC(LHS_CONV(ONCE_REWRITE_CONV[Split_def])) THEN RW_TAC list_ss [TAKE_LENGTH_APPEND,DROP_LENGTH_APPEND] THEN FULL_SIMP_TAC list_ss [GSYM LENGTH_NIL]); val PadZerosKey = store_thm ("PadZerosKey", ``!key msg. 1 < r /\ (LENGTH key = r) ==> (PadZeros r (key ++ msg) = PadZeros r msg)``, RW_TAC list_ss [PadZeros] THENL [Cases_on `1 < r` THEN FULL_SIMP_TAC list_ss [] THEN `0 < r` by DECIDE_TAC THEN PROVE_TAC[ADD_MODULUS_RIGHT], Cases_on `1 < r` THEN FULL_SIMP_TAC list_ss [] THEN `0 < r` by DECIDE_TAC THEN PROVE_TAC[ADD_MODULUS_RIGHT], `0 < LENGTH key` by DECIDE_TAC THEN RW_TAC std_ss [ADD_MODULUS_RIGHT]]); val MAC_Hash = store_thm ("MAC_Hash", ``!r c n f key msg. 1 < r /\ (LENGTH key = r) ==> (MAC (r,c,n) f key msg = Hash (r,c,n) f (f(key ++ Zeros c)) msg)``, RW_TAC std_ss [MAC_def,Hash_def,Pad_def] THEN `0 < LENGTH key` by DECIDE_TAC THEN `LENGTH (msg ++ [T] ++ Zeros (PadZeros (LENGTH key) (key ++ msg)) ++ [T]) = LENGTH msg + 1 + (PadZeros (LENGTH key) (key ++ msg)) + 1` by RW_TAC list_ss [LengthZeros] THEN `LENGTH (msg ++ [T] ++ Zeros (PadZeros (LENGTH key) (key ++ msg)) ++ [T]) <> 0` by DECIDE_TAC THEN `(msg ++ [T] ++ Zeros (PadZeros (LENGTH key) (key ++ msg)) ++ [T]) <> []` by PROVE_TAC[LENGTH_NIL] THEN FULL_SIMP_TAC std_ss [SplitKey,GSYM APPEND_ASSOC,Absorb_def] THEN `LENGTH key + c = c + LENGTH key` by PROVE_TAC [ADD_SYM] THEN RW_TAC std_ss [ZerosXorLENGTH,PadZerosKey]); (* Old versions val ComputeMACLemma = store_thm ("ComputeMacLemma", ``!key r c n f. 2 < r /\ (LENGTH key = r) ==> MITB_IMP key (r,c,n) f |= ComputeMAC key (r,c,n) f``, RW_TAC std_ss [ComputeMAC_def,ALWAYS_ALL,GSYM StepCount_def] THEN `1 < LENGTH key` by DECIDE_TAC THEN `readyOut T AND skipInp F AND moveInp T AND pmemState(f(key ++ Zeros c)) = pmemState(f(key ++ Zeros c)) AND readyOut T AND skipInp F AND moveInp T` by PROVE_TAC[AND_SYM,AND_ASSOC] THEN RW_TAC list_ss [MAC_Hash,ComputeHash]); val ComputeMACLemma = store_thm ("ComputeMacLemma", ``!key r c n f. 2 < r ==> MITB_IMP key (r,c,n) f |= ComputeMAC (r,c,n) f``, RW_TAC std_ss [ComputeMAC_def,ALWAYS_ALL,GSYM StepCount_def] THEN `readyOut T AND skipInp F AND moveInp T AND BOOL(LENGTH key' = r) AND pmemState(f(key' ++ Zeros c)) = BOOL(LENGTH key' = r) AND (pmemState(f(key' ++ Zeros c)) AND readyOut T AND skipInp F AND moveInp T)` by PROVE_TAC[AND_SYM,AND_ASSOC] THEN RW_TAC std_ss [ALWAYS_BOOL_AND_IMPLIES] THEN `1 < LENGTH key'` by DECIDE_TAC THEN RW_TAC list_ss [MAC_Hash,ComputeHash]); *) val ComputeMACLemma = store_thm ("ComputeMacLemma", ``!key r c n f. 2 < r ==> MITB_IMP key (r,c,n) f |= ComputeMAC (r,c,n) f``, RW_TAC std_ss [ComputeMAC_def,ALWAYS_ALL,GSYM StepCount_def] THEN `readyOut T AND skipInp F AND moveInp T AND BOOL(LENGTH key' = r) AND pmemState(f(key' ++ Zeros c)) = BOOL(LENGTH key' = r) AND (pmemState(f(key' ++ Zeros c)) AND readyOut T AND skipInp F AND moveInp T)` by PROVE_TAC[AND_SYM,AND_ASSOC] THEN RW_TAC std_ss [ALWAYS_BOOL_AND_IMPLIES] THEN `1 < LENGTH key'` by DECIDE_TAC THEN `MITB_IMP key (LENGTH key',c,n) f |= ALWAYS (skipInp F AND moveInp F AND readyOut F AND digestOut (Zeros n) IMPLIES readyOut F AND digestOut (Zeros n))` by MC_TAC[] THEN PROVE_TAC[ALWAYS_NEXT_UNTILN_MONO1,ComputeHash,MAC_Hash]); val MITBImplicit = store_thm ("MITBImplicit", ``!phi. (!key r c n f. MITB_IMP key (r,c,n) f |= phi key r c n f) = (!key r c n f. 2 < r /\ (LENGTH key = r) ==> MITB_IMP key (r,c,n) f |= phi key r c n f)``, MC_TAC[] THEN EQ_TAC THEN RW_TAC std_ss [GoodParameters_def]); val ComputeMAC = store_thm ("ComputeMac", ``!key r c n f. MITB_IMP key (r,c,n) f |= ComputeMAC (r,c,n) f``, ONCE_REWRITE_TAC [SIMP_RULE std_ss [] (ISPEC ``\(key:bits) (r:num) (c:num) (n:num) (f:bits->bits). ^(rand(snd(dest_imp(concl(SPEC_ALL ComputeMACLemma)))))`` MITBImplicit)] THEN RW_TAC std_ss [ComputeMACLemma]); (* Verify main security property *) val Secure_def = Define `Secure (r,c,n) f = ALWAYS (digestOut(Zeros n) OR EXIST m. digestOut(Hash (r,c,n) f (Zeros(r+c)) m))`; val Secure = store_thm ("Secure", ``MITB_IMP key (r,c,n) f |= Secure (r,c,n) f``, RW_TAC std_ss [Secure_def,Models_MITB,ALWAYS_def,OR_def, EXIST_def,ChopAll_def,Chop,digestOut_def] THEN PROVE_TAC[MITB_DEV_def,MITB_DEV_SAFE]); (* Proof reconciling definition of |= in paper (formalised by |== below) and the one used in main proof development (called |= here) *) val _ = set_fixity "|==" (Infixr 325); val AltModels_def = xDefine "AltModels" `$|== (next_state, s0) psi = !inp sigma. (sigma 0 = s0) /\ (!t. sigma(t+1) = next_state(inp t,sigma t)) ==> psi(\t. (inp t, sigma t))`; val ModelsLemma = store_thm ("ModelsLemma", ``!inp sigma tau. (tau 0 = (inp 0,s0)) /\ (!t. tau(t+1) = (inp(t+1),next_state(tau t))) /\ (sigma 0 = s0) /\ (!t. sigma (t + 1) = next_state (inp t,sigma t)) ==> (!t. tau t = (inp t, sigma t))``, RW_TAC std_ss [] THEN Induct_on `t` THEN RW_TAC arith_ss [ADD1]); val ModelsIter1_def = Define `(ModelsIter1 next_state inp s0 0 = s0) /\ (ModelsIter1 next_state inp s0 (SUC t) = next_state (inp t,ModelsIter1 next_state inp s0 t))`; val ModelsIter1Unique = store_thm ("ModelsIter1Unique", ``!tau next_state inp s0. (tau 0 = s0) /\ (!t. tau(t+1) = next_state(inp t,tau t)) ==> (tau = ModelsIter1 next_state inp s0)``, RW_TAC std_ss [FUN_EQ_THM] THEN Induct_on `x` THEN RW_TAC arith_ss [ModelsIter1_def,ADD1]); (* val ModelsIter1Unique = store_thm ("ModelsIter1Unique", ``!tau next_state inp s0. (tau 0 = s0) /\ (!t. tau(t+1) = next_state(inp t,tau t)) = (tau = ModelsIter1 next_state inp s0)``, RW_TAC std_ss [FUN_EQ_THM] THEN EQ_TAC THENL [RW_TAC std_ss [] THEN Induct_on `x` THEN RW_TAC arith_ss [ModelsIter1_def,ADD1]); *) val ModelsIter2_def = Define `(ModelsIter2 next_state inp s0 0 = (inp 0, s0)) /\ (ModelsIter2 next_state inp s0 (SUC t) = (inp(t+1), next_state (ModelsIter2 next_state inp s0 t)))`; val ModelsIter2Unique = store_thm ("ModelsIter2Unique", ``!sigma next_state inp s0. (sigma 0 = (inp 0, s0)) /\ (!t. sigma(t+1) = (inp(t+1),next_state(sigma t))) ==> (sigma = ModelsIter2 next_state inp s0)``, RW_TAC std_ss [FUN_EQ_THM] THEN Induct_on `x` THEN RW_TAC arith_ss [ModelsIter2_def,ADD1]); val ModeslsIter1Iter2 = store_thm ("ModeslsIter1Iter2", ``!t next_state inp s0. (inp t,ModelsIter1 next_state inp s0 t) = ModelsIter2 next_state inp s0 t``, Induct THEN RW_TAC arith_ss [ModelsIter1_def,ModelsIter2_def,ADD1]); (* val AltModels = store_thm ("AltModels", ``((next_state, s0) |== psi) <=> !inp tau. (tau 0 = (inp 0,s0)) /\ (!t. tau(t+1) = (inp(t+1),next_state(tau t))) ==> psi tau``, RW_TAC std_ss [AltModels_def,Models_def] THEN EQ_TAC THEN RW_TAC std_ss [] THEN IMP_RES_TAC ModelsLemma *) val Dev_def = Define `Dev (next_state,s0) inp sigma = (sigma 0 = s0) /\ !t. sigma(t+1) = next_state(inp t, sigma t)`; val DevModels = store_thm ("DevModels", ``!next_state s0 phi. (Dev (next_state,s0) |= phi) = ((next_state,s0) |== (\sigma. phi((\t. FST(sigma t)), (\t. SND(sigma t)))))``, RW_TAC std_ss [Dev_def,Models_def,AltModels_def] THEN EQ_TAC THEN RW_TAC std_ss [ETA_AX]); (* Zip tuples of signals into a single tuple-valued signal. *) val Zip_def = Define `Zip ((cntl_sig,pmem_sig,vmem_sig), (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out)) = \t. ((skip_inp t,move_inp t,block_inp t,size_inp t), (cntl_sig t,pmem_sig t,vmem_sig t))`; (* Unzip tuple-valued signal intp tiples of signals *) val cntl_of_def = Define `cntl_of ((skip,move,block,size),(cntl,pmem,vmem)) = cntl`; val pmem_of_def = Define `pmem_of ((skip,move,block,size),(cntl,pmem,vmem)) = pmem`; val vmem_of_def = Define `vmem_of ((skip,move,block,size),(cntl,pmem,vmem)) = vmem`; val skip_of_def = Define `skip_of ((skip,move,block,size),(cntl,pmem,vmem)) = skip`; val move_of_def = Define `move_of ((skip,move,block,size),(cntl,pmem,vmem)) = move`; val block_of_def = Define `block_of ((skip,move,block,size),(cntl,pmem,vmem)) = block`; val size_of_def = Define `size_of ((skip,move,block,size),(cntl,pmem,vmem)) = size`; val ready_of_def = Define `ready_of ((skip,move,block,size),(cntl,pmem,vmem)) = [cntl = Ready]`; val digest_of_def = Define `digest_of n ((skip,move,block,size),(cntl,pmem,vmem)) = if cntl = Ready then TAKE n vmem else Zeros n`; val of_defs = [cntl_of_def,pmem_of_def,vmem_of_def,skip_of_def,move_of_def, block_of_def,size_of_def,ready_of_def,digest_of_def]; val Unzip_def = Define `Unzip n sigma = (((cntl_of o sigma),(pmem_of o sigma),(vmem_of o sigma)), ((skip_of o sigma),(move_of o sigma),(block_of o sigma), (size_of o sigma),(ready_of o sigma),(digest_of n o sigma)))`; val ZipUnzip = store_thm ("ZipUnzip", ``!n sigma. Zip (Unzip n sigma) = sigma``, RW_TAC list_ss [FUN_EQ_THM,Zip_def,Unzip_def] THEN Cases_on `sigma x` THEN Cases_on `q` THEN Cases_on `r` THEN Cases_on `r'` THEN Cases_on `r''` THEN Cases_on `r` THEN RW_TAC std_ss of_defs); val UnzipZipLemma = store_thm ("UnzipZipLemma", ``(!t. ready_out t = [cntl_sig t = Ready]) /\ (!t. digest_out t = if cntl_sig t = Ready then TAKE n (vmem_sig t) else Zeros n) ==> (Unzip n (Zip ((cntl_sig,pmem_sig,vmem_sig), (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out))) = ((cntl_sig,pmem_sig,vmem_sig), (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out)))``, RW_TAC list_ss ([Zip_def,Unzip_def,FUN_EQ_THM]@of_defs)); (* Convert a predicate on state-port signals to one on input-state signals (by adding the outputs) *) val ConvertPred_def = Define `ConvertPred n (phi : state_sigs # port_sigs -> bool) ((inp_sig : num -> mitb_inp), (state_sig : num -> mitb_state)) = (phi: state_sigs # port_sigs -> bool) (((\t. cntl_of (inp_sig t, state_sig t)), (\t. pmem_of (inp_sig t, state_sig t)), (\t. vmem_of (inp_sig t, state_sig t))), ((\t. skip_of (inp_sig t, state_sig t)), (\t. move_of (inp_sig t, state_sig t)), (\t. block_of (inp_sig t, state_sig t)), (\t. size_of (inp_sig t, state_sig t)), (\t. ready_of (inp_sig t, state_sig t)), (\t. digest_of n (inp_sig t, state_sig t))))`; (* Generate and execution trace from an initial state (cntl0,pmem0,vmem0) and user supplied inputs (skip_inp,move_inp,block_inp,size_inp) *) val MITB_TRACE_def = Define `(MITB_TRACE (r,c,n) f (skip_inp,move_inp,block_inp,size_inp) (cntl0,pmem0,vmem0) 0 = (cntl0,pmem0,vmem0)) /\ (MITB_TRACE (r,c,n) f (skip_inp,move_inp,block_inp,size_inp) (cntl0,pmem0,vmem0) (SUC t) = MITB (r,c,n) f ((skip_inp t,move_inp t,block_inp t,size_inp t), MITB_TRACE (r,c,n) f (skip_inp,move_inp,block_inp,size_inp) (cntl0,pmem0,vmem0) t))`; (* Show implementation doesn't change sizes of pmem and vmem *) (* The theorem MITB_FUN_LENGTH is not currently used *) val MITB_FUN_LENGTH = store_thm ("MITB_FUN_LENGTH", ``!cntl cmd. (!s. LENGTH(f s) = LENGTH s) /\ GoodParameters(r,c,n) /\ GoodCommand (r,c,n) cntl cmd /\ (LENGTH pmem = r + c) /\ (LENGTH vmem = r + c) ==> (LENGTH(FST(SND(MITB_FUN (r,c,n) f (cntl,pmem,vmem) cmd))) = LENGTH pmem) /\ (LENGTH(SND(SND(MITB_FUN (r,c,n) f (cntl,pmem,vmem) cmd))) = LENGTH vmem)``, Induct THEN Induct THEN RW_TAC list_ss [MITB_FUN_def,LENGTH_ZEROS,LENGTH_XOR, GoodCommand_def,GoodParameters_def]); val MITB_TRACE_LENGTH = store_thm ("MITB_TRACE_LENGTH", ``!t. (!s. LENGTH(f s) = LENGTH s) /\ GoodParameters(r,c,n) /\ (LENGTH key = r) /\ Width skip_inp 1 /\ Width move_inp 1 /\ Width block_inp r /\ (!t. size_inp t <= r) ==> (LENGTH (FST (SND(MITB_TRACE (r,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f (key ++ Zeros c),Zeros (c + LENGTH key)) t))) = r + c) /\ (LENGTH (SND (SND(MITB_TRACE (r,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f (key ++ Zeros c),Zeros (c + LENGTH key)) t))) = r + c)``, Induct THEN RW_TAC list_ss [MITB_TRACE_def] THEN `?cntl pmem vmem. MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f (key ++ Zeros c),Zeros (c + LENGTH key)) t = (cntl,pmem,vmem)` by METIS_TAC[PAIR] THEN Cases_on `cntl` THEN RW_TAC list_ss [MITB_def,MITB_FUN_def,LENGTH_ZEROS,LENGTH_XOR,LengthZeros] THEN TRY(METIS_TAC[ADD_SYM,FST,SND]) THEN FULL_SIMP_TAC list_ss [Width_def,GoodParameters_def] THEN ASSUM_LIST(ASSUME_TAC o SPEC_ALL o el 5) THEN `(size_inp t <= LENGTH key - 2) \/ (size_inp t = LENGTH key - 1) \/ (size_inp t = LENGTH key)` by DECIDE_TAC THEN RW_TAC list_ss [LENGTH_ZEROS,LENGTH_XOR]); val MITB_IMP_EXISTS = store_thm ("MITB_IMP_EXISTS", ``!key r c n f skip_inp move_inp block_inp size_inp. (!s. LENGTH(f s) = LENGTH s) /\ GoodParameters(r,c,n) /\ (LENGTH key = r) /\ Width skip_inp 1 /\ Width move_inp 1 /\ Width block_inp r /\ (!t. size_inp t <= r) ==> ?cntl_sig pmem_sig vmem_sig ready_out digest_out. MITB_IMP key (r,c,n) f (cntl_sig,pmem_sig,vmem_sig) (skip_inp,move_inp,block_inp,size_inp,ready_out,digest_out)``, RW_TAC std_ss [] THEN `?cntl_sig. cntl_sig = \t. FST(MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f(key++Zeros c),Zeros(LENGTH key + c)) t)` by METIS_TAC[EXISTS_REFL] THEN `?pmem_sig. pmem_sig = \t. FST(SND(MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f(key++Zeros c),Zeros(LENGTH key + c)) t))` by METIS_TAC[EXISTS_REFL] THEN `?vmem_sig. vmem_sig = \t. SND(SND(MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f(key++Zeros c),Zeros(LENGTH key + c)) t))` by METIS_TAC[EXISTS_REFL] THEN Q.EXISTS_TAC `cntl_sig` THEN Q.EXISTS_TAC `pmem_sig` THEN Q.EXISTS_TAC `vmem_sig` THEN Q.EXISTS_TAC `\t. [cntl_sig t = Ready]` THEN Q.EXISTS_TAC `\t. if cntl_sig t = Ready then TAKE n (vmem_sig t) else Zeros n` THEN RW_TAC std_ss [MITB_IMP_def,REGISTER_def,MITB_TRACE_def,ZEROSEqZeros] THEN Q.EXISTS_TAC `\t. FST (MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f (key ++ Zeros c),Zeros (LENGTH key + c)) (t + 1))` THEN Q.EXISTS_TAC `\t. FST (SND (MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f (key ++ Zeros c),Zeros (LENGTH key + c)) (t + 1)))` THEN Q.EXISTS_TAC `\t. SND (SND (MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f (key ++ Zeros c),Zeros (LENGTH key + c)) (t + 1)))` THEN RW_TAC list_ss [SIMP_RULE std_ss [ADD1] MITB_TRACE_def, ZEROSEqZeros,Width_def,MITB_CONTROL_LOGIC_def, MITB_TRACE_LENGTH] THEN `?cntl pmem vmem. MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f (key ++ Zeros c),Zeros (c + LENGTH key)) t = (cntl,pmem,vmem)` by METIS_TAC[PAIR] THEN RW_TAC list_ss [MITB_def,MITB_FUN_def,LengthZeros] THEN TRY(Cases_on `cntl` THEN RW_TAC std_ss [MITB_FUN_def]) THEN `(LENGTH (SND (SND(MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f (key ++ Zeros c),Zeros (c + LENGTH key)) t))) = LENGTH key + c)` by METIS_TAC[MITB_TRACE_LENGTH] THEN `(LENGTH (FST (SND(MITB_TRACE (LENGTH key,c,n) f (skip_inp,move_inp,block_inp,size_inp) (Ready,f (key ++ Zeros c),Zeros (c + LENGTH key)) t))) = LENGTH key + c)` by METIS_TAC[MITB_TRACE_LENGTH] THEN FULL_SIMP_TAC list_ss [LENGTH_ZEROS,LENGTH_XOR,Width_def,GoodParameters_def] THEN RW_TAC arith_ss [MAX_DEF] THEN ASSUM_LIST(MAP_EVERY (TRY o ASSUME_TAC o SPEC_ALL)) THEN `LENGTH vmem = c + LENGTH key` by METIS_TAC[FST,SND,ADD_SYM] THEN RW_TAC list_ss [LENGTH_TAKE] THEN METIS_TAC[FST,SND,ADD_SYM]); (* ==================== ==================== *) val _ = export_theory();