Created
February 2, 2017 20:24
-
-
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 ] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment