Skip to content

Instantly share code, notes, and snippets.

# thoughtpolice/wbob.cry

Created February 2, 2017 20:24
Show Gist options
• Save thoughtpolice/1d62a8ea309b523aaed3f1e2e04bb345 to your computer and use it in GitHub Desktop.
WHIRLBOB Pi Permutation (based on Whirlpool key schedule)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 module pi::wbob where import Basics::Sequence /* -------------------------------------------------------------------------- */ /* -- Pi function: Whirlpool ------------------------------------------------ */ /** * STRIBOBr2 Pi: the WhirlBob permutation, parameterized * by the number of rounds `r`. */ wbob_pi : { r } // The number of rounds ( fin r, r >= 1 // Must have at least 1 round , 8 >= width r // inferred: size constraint ) => [64][8] // Input state -> [64][8] // Output state wbob_pi x0 = join (results ! 0) where results = v where // Iterate over the initial state and apply the permutation // a specified number of times. v = [ split x0 ] # [ perm i x | x <- v | i <- rng ] // The number of times to apply the permutation, specified // as a sequence. rng = [ 0 .. r-1 ] : [r][8] /* Full permutation, mixed with the round keys */ perm : [8] -> [8][8][8] -> [8][8][8] perm i x = L (P (S x)) ^ C i /* SubBytes: M[i][j] <- Sbox(M[i][j]) */ S : [8][8][8] -> [8][8][8] S = map (map mbox) /* ShiftColumns */ P : [8][8][8] -> [8][8][8] P x = transpose [ v >>> i | v <- transpose x | i <- ([ 0 .. 7 ] : [_][8]) ] /* MixRows */ L : [8][8][8] -> [8][8][8] L xs = [ vect x (transpose mds) | x <- xs ] where // List summation under GF(2^8) add : {n} (fin n) => [n][8] -> [8] add ps = sums ! 0 where sums = [zero] # [ p ^ s | p <- ps | s <- sums ] // Dot product under GF(2^8) dot : {n} (fin n) => [n][8] -> [n][8] -> [8] dot y z = add (zipWith mult y z) // Vector-by-matrix multiplication vect : {n, m} (fin n) => [n][8] -> [m][n][8] -> [m][8] vect v ys = [ dot v y | y <- ys ] // Multiply in GF(2^8), reduced by the Whirlpool polynomial. mult : [8] -> [8] -> [8] mult a b = pmod (pmult a b) <| x^^8 + x^^4 + x^^3 + x^^2 + 1 |> // Circular MDS Matrix mds : [8][8][8] mds = [ [ 0x01, 0x01, 0x04, 0x01, 0x08, 0x05, 0x02, 0x09 ] , [ 0x09, 0x01, 0x01, 0x04, 0x01, 0x08, 0x05, 0x02 ] , [ 0x02, 0x09, 0x01, 0x01, 0x04, 0x01, 0x08, 0x05 ] , [ 0x05, 0x02, 0x09, 0x01, 0x01, 0x04, 0x01, 0x08 ] , [ 0x08, 0x05, 0x02, 0x09, 0x01, 0x01, 0x04, 0x01 ] , [ 0x01, 0x08, 0x05, 0x02, 0x09, 0x01, 0x01, 0x04 ] , [ 0x04, 0x01, 0x08, 0x05, 0x02, 0x09, 0x01, 0x01 ] , [ 0x01, 0x04, 0x01, 0x08, 0x05, 0x02, 0x09, 0x01 ] ] /* AddRoundKey */ C : [8] -> [8][8][8] C i = [Cr @ i] # zero /** * Full set of computed round keys. Equivalent to the first 96 bytes * of the sbox. */ Cr : [12][8][8] Cr = split [ mbox ((8*r) + j) | r <- [ 0 .. 11 ], j <- [ 0 .. 7 ] ] /** * WhirlPool 3.0 permutation function, also known as the `W` function, using * "miniboxes" to compute sbox results. */ wpool : [64][8] -> [64][8] wpool = wbob_pi`{r=10} /** * STRIBOBr2 Pi: The "WhirlBob" permutation, using "miniboxes" to compute sbox * results. This is the same as the WhirlPool `W` function, but with 12 rounds * instead of 10. */ wbob : [64][8] -> [64][8] wbob = wbob_pi`{r=12} /* -- S-boxes --------------------------------------------------------------- */ private /** * The WhirlPool/WhirlBob Sbox function, as described by the specification. * This uses three small "miniboxes" to calculate the full sbox. */ mbox : [8] -> [8] mbox i = join [t', b'] where [t, b] = split i : [2][4] m = (E t) ^ (E_1 b) t' = E ((E t) ^ (R m)) b' = E_1 ((E_1 b) ^ (R m)) // Derivation rule 1 E : [4] -> [4] E x = v @ x where v = [ 0x1, 0xB, 0x9, 0xC , 0xD, 0x6, 0xF, 0x3 , 0xE, 0x8, 0x7, 0x4 , 0xA, 0x2, 0x5, 0x0 ] // Derivation rule 2 (read: "E's inverse", e.g. E^(-1)) E_1 : [4] -> [4] E_1 x = v @ x where v = [ 0xF, 0x0, 0xD, 0x7 , 0xB, 0xE, 0x5, 0xA , 0x9, 0x2, 0xC, 0x1 , 0x3, 0x4, 0x8, 0x6 ] // Derivation rule 3 R : [4] -> [4] R x = v @ x where v = [ 0x7, 0xC, 0xB, 0xD , 0xE, 0x4, 0x9, 0xF , 0x6, 0x3, 0x8, 0xA , 0x2, 0x5, 0x1, 0x0 ] /** * The WhirlPool/WhirlBob Sbox function, as a pre-computed table. * While this might be faster than 'mbox', it generally takes up * much more space. */ sbox : [8] -> [8] sbox i = box @ i where box = [ 0x18, 0x23, 0xC6, 0xE8, 0x87, 0xB8, 0x01, 0x4F , 0x36, 0xA6, 0xD2, 0xF5, 0x79, 0x6F, 0x91, 0x52 , 0x60, 0xBC, 0x9B, 0x8E, 0xA3, 0x0C, 0x7B, 0x35 , 0x1D, 0xE0, 0xD7, 0xC2, 0x2E, 0x4B, 0xFE, 0x57 , 0x15, 0x77, 0x37, 0xE5, 0x9F, 0xF0, 0x4A, 0xDA , 0x58, 0xC9, 0x29, 0x0A, 0xB1, 0xA0, 0x6B, 0x85 , 0xBD, 0x5D, 0x10, 0xF4, 0xCB, 0x3E, 0x05, 0x67 , 0xE4, 0x27, 0x41, 0x8B, 0xA7, 0x7D, 0x95, 0xD8 , 0xFB, 0xEE, 0x7C, 0x66, 0xDD, 0x17, 0x47, 0x9E , 0xCA, 0x2D, 0xBF, 0x07, 0xAD, 0x5A, 0x83, 0x33 , 0x63, 0x02, 0xAA, 0x71, 0xC8, 0x19, 0x49, 0xD9 , 0xF2, 0xE3, 0x5B, 0x88, 0x9A, 0x26, 0x32, 0xB0 , 0xE9, 0x0F, 0xD5, 0x80, 0xBE, 0xCD, 0x34, 0x48 , 0xFF, 0x7A, 0x90, 0x5F, 0x20, 0x68, 0x1A, 0xAE , 0xB4, 0x54, 0x93, 0x22, 0x64, 0xF1, 0x73, 0x12 , 0x40, 0x08, 0xC3, 0xEC, 0xDB, 0xA1, 0x8D, 0x3D , 0x97, 0x00, 0xCF, 0x2B, 0x76, 0x82, 0xD6, 0x1B , 0xB5, 0xAF, 0x6A, 0x50, 0x45, 0xF3, 0x30, 0xEF , 0x3F, 0x55, 0xA2, 0xEA, 0x65, 0xBA, 0x2F, 0xC0 , 0xDE, 0x1C, 0xFD, 0x4D, 0x92, 0x75, 0x06, 0x8A , 0xB2, 0xE6, 0x0E, 0x1F, 0x62, 0xD4, 0xA8, 0x96 , 0xF9, 0xC5, 0x25, 0x59, 0x84, 0x72, 0x39, 0x4C , 0x5E, 0x78, 0x38, 0x8C, 0xD1, 0xA5, 0xE2, 0x61 , 0xB3, 0x21, 0x9C, 0x1E, 0x43, 0xC7, 0xFC, 0x04 , 0x51, 0x99, 0x6D, 0x0D, 0xFA, 0xDF, 0x7E, 0x24 , 0x3B, 0xAB, 0xCE, 0x11, 0x8F, 0x4E, 0xB7, 0xEB , 0x3C, 0x81, 0x94, 0xF7, 0xB9, 0x13, 0x2C, 0xD3 , 0xE7, 0x6E, 0xC4, 0x03, 0x56, 0x44, 0x7F, 0xA9 , 0x2A, 0xBB, 0xC1, 0x53, 0xDC, 0x0B, 0x9D, 0x6C , 0x31, 0x74, 0xF6, 0x46, 0xAC, 0x89, 0x14, 0xE1 , 0x16, 0x3A, 0x69, 0x09, 0x70, 0xB6, 0xD0, 0xED , 0xCC, 0x42, 0x98, 0xA4, 0x28, 0x5C, 0xF8, 0x86 ] /* -------------------------------------------------------------------------- */ /* -- Theorems, tests ------------------------------------------------------- */ private // -- Test vector 1 ---------------------------------------------------------- input = [ 0x77, 0x38, 0xE1, 0xB5, 0x41, 0xA0, 0x36, 0xEA, 0x45, 0x8D, 0x50, 0xF8, 0x0F, 0xA0, 0x1C, 0x44, 0x72, 0x88, 0xCE, 0x97, 0xD1, 0xA0, 0xDC, 0xF0, 0x16, 0x95, 0xFF, 0xD6, 0xE7, 0x1D, 0x09, 0x25, 0x33, 0xBE, 0x30, 0x9F, 0x01, 0x2A, 0x59, 0x09, 0x72, 0x91, 0x14, 0x59, 0x5F, 0x08, 0x6E, 0x76, 0x07, 0x18, 0xAF, 0xE3, 0x65, 0xBC, 0x09, 0xDE, 0xB6, 0xAF, 0xA1, 0x80, 0xBC, 0xEC, 0x2A, 0x98 ] wbob01 = wbob_pi`{r=1} input == out where out = [ 0x1A, 0x78, 0x4D, 0x7D, 0xBD, 0x4C, 0x17, 0xE6 , 0x27, 0x31, 0x10, 0xAA, 0x63, 0xC5, 0x9E, 0x25 , 0x7A, 0x2E, 0xB7, 0x48, 0xC4, 0x5D, 0xE0, 0x23 , 0x6D, 0x0D, 0x61, 0x9F, 0x6C, 0x1D, 0x80, 0xAE , 0x01, 0xA2, 0xD5, 0x6E, 0xDB, 0x41, 0xD9, 0xA0 , 0xE9, 0x06, 0x4C, 0xD1, 0x27, 0x95, 0xFA, 0x86 , 0x77, 0x62, 0x31, 0xBC, 0xB4, 0x4E, 0xC6, 0x01 , 0x6F, 0xCD, 0xBC, 0x98, 0x10, 0x78, 0x6F, 0xEC ] wbob02 = wbob_pi`{r=10} input == out where out = [ 0xB4, 0x74, 0xE1, 0x56, 0x96, 0x31, 0xB9, 0x6C , 0x21, 0xA1, 0xB6, 0x33, 0xCC, 0x89, 0x68, 0x1A , 0xB1, 0x97, 0x25, 0x86, 0x7B, 0x2B, 0x3F, 0x09 , 0x4C, 0x73, 0xC7, 0x62, 0x93, 0xA8, 0x15, 0xCF , 0x55, 0x15, 0xC0, 0xC0, 0x9A, 0x05, 0x05, 0x16 , 0x23, 0x44, 0x8D, 0x8D, 0xD3, 0x5F, 0xB3, 0x6E , 0x7E, 0x6C, 0x2D, 0x37, 0x12, 0xD0, 0xF3, 0x3E , 0xCE, 0xB8, 0x04, 0xF2, 0x8D, 0x9F, 0xC9, 0x99 ] wbob03 = wbob_pi`{r=12} input == out where out = [ 0x3F, 0x72, 0xC2, 0x60, 0xEE, 0x28, 0xEF, 0xEA , 0x42, 0x8E, 0xB5, 0x3A, 0xFB, 0x8A, 0x33, 0xA2 , 0x03, 0xE4, 0x72, 0x31, 0x90, 0xA5, 0x1A, 0xD3 , 0x3E, 0x68, 0xE6, 0x46, 0xFC, 0x94, 0x3C, 0xC7 , 0x80, 0x42, 0x9E, 0x2E, 0xCB, 0x32, 0x75, 0x93 , 0x30, 0xAA, 0xE2, 0x21, 0x21, 0xC8, 0x99, 0xED , 0x86, 0x1E, 0x06, 0x9E, 0x91, 0x1F, 0x89, 0x6C , 0xD2, 0x99, 0xEC, 0x7E, 0xE9, 0x0B, 0x01, 0x10 ] property allTestsPass = ([ wbob01, wbob02, wbob03 ] : [_]Bit) == ~zero // All tests should return True // Show that the sbox derivation is correct, and that we // can interchange the derived sbox and minisbox algorithm // as equivalent. property sbox_deriv_correct x = sbox x == mbox x // The set of round keys is equivalent to the first 96 bytes // of the sbox. property roundkeys_correct = join Cr == map sbox [ 0 .. 95 ]
to join this conversation on GitHub. Already have an account? Sign in to comment