Skip to content

Instantly share code, notes, and snippets.

@thoughtpolice

thoughtpolice/wbob.cry

Created February 2, 2017 20:24
Show Gist options
  • Save thoughtpolice/1d62a8ea309b523aaed3f1e2e04bb345 to your computer and use it in GitHub Desktop.
Save thoughtpolice/1d62a8ea309b523aaed3f1e2e04bb345 to your computer and use it in GitHub Desktop.
Download ZIP
WHIRLBOB Pi Permutation (based on Whirlpool key schedule)
Raw
wbob.cry
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 ]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment