|- ∀k0 k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14 k15 k16 k17 k18 k19 k20 k21 k22 k23 k24 k25 k26 k27 k28 k29 k30 k31 k32 k33 k34 k35 k36 k37 k38 k39 k40 k41 k42 k43. GETKEYS (k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17, k18,k19,k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33, k34,k35,k36,k37,k38,k39,k40,k41,k42,k43) = (k0,k1) |- ∀k a b c d. PreWhitening k (a,b,c,d) = (a,b + FST (GETKEYS k),c,d + SND (GETKEYS k)) |- ∀k0 k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14 k15 k16 k17 k18 k19 k20 k21 k22 k23 k24 k25 k26 k27 k28 k29 k30 k31 k32 k33 k34 k35 k36 k37 k38 k39 k40 k41 k42 k43. ROTKEYS (k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17, k18,k19,k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33, k34,k35,k36,k37,k38,k39,k40,k41,k42,k43) = (k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,k19, k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,k35, k36,k37,k38,k39,k40,k41,k42,k43,k0,k1) |- ∀k a b c d. InvPostWhitening k (a,b,c,d) = (a,b − FST (GETKEYS k),c,d − SND (GETKEYS k)) |- ∀k a b c d. InvPreWhitening k (a,b,c,d) = (a − SND (GETKEYS k),b,c − SND (GETKEYS k),d) |- ∀x n. x >>> n = x ⇄ w2n n |- ∀x n. x <<< n = x ⇆ w2n n |- ∀x. CompUT x = (x * (x + x + 1w)) ⇆ 5 |- ∀a b c d k0 k1. FwdRound (a,b,c,d) (k0,k1) = (b,(c ⊕ CompUT d) <<< CompUT b + k1,d, (a ⊕ CompUT b) <<< CompUT d + k0) |- ∀a b c d k0 k1. BwdRound (a,b,c,d) (k0,k1) = ((d − k0) >>> CompUT c ⊕ CompUT a,a, (b − k1) >>> CompUT a ⊕ CompUT c,c) |- ∀k a b c d. PostWhitening k (a,b,c,d) = (a + SND (GETKEYS k),b,c + SND (GETKEYS k),d) |- Round n k b = if n = 0 then PostWhitening k b else Round (n − 1) (ROTKEYS k) (FwdRound b (GETKEYS k)) |- InvRound n k b = if n = 0 then InvPreWhitening k b else BwdRound (InvRound (n − 1) (ROTKEYS k) b) (GETKEYS k) |- r = 20 |- ∀keys. RC6_FWD keys = Round r keys o PreWhitening keys |- ∀keys. RC6_BWD keys = InvPostWhitening keys o InvRound r keys