cryptol/examples/contrib/speck.cry

122 lines
5.0 KiB
Plaintext
Raw Normal View History

2014-04-18 02:34:25 +04:00
/*
* Copyright (c) 2013-2014 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
/* Cryptol specification of the Speck block cipher
* Author: David Lazar
*/
///////////////////////////////////////////////////////////////////////
// parameters
///////////////////////////////////////////////////////////////////////
2014-04-25 01:27:34 +04:00
Speck32_64 = encrypt`{n = 16, m = 4, T = 22}
Speck48_72 = encrypt`{n = 24, m = 3, T = 22}
Speck48_96 = encrypt`{n = 24, m = 4, T = 23}
Speck64_96 = encrypt`{n = 32, m = 3, T = 26}
Speck64_128 = encrypt`{n = 32, m = 4, T = 27}
Speck96_96 = encrypt`{n = 48, m = 2, T = 28}
Speck96_144 = encrypt`{n = 48, m = 3, T = 29}
Speck128_128 = encrypt`{n = 64, m = 2, T = 32}
Speck128_192 = encrypt`{n = 64, m = 3, T = 33}
Speck128_256 = encrypt`{n = 64, m = 4, T = 34}
Speck32_64' = decrypt`{n = 16, m = 4, T = 22}
Speck48_72' = decrypt`{n = 24, m = 3, T = 22}
Speck48_96' = decrypt`{n = 24, m = 4, T = 23}
Speck64_96' = decrypt`{n = 32, m = 3, T = 26}
Speck64_128' = decrypt`{n = 32, m = 4, T = 27}
Speck96_96' = decrypt`{n = 48, m = 2, T = 28}
Speck96_144' = decrypt`{n = 48, m = 3, T = 29}
2014-04-18 02:34:25 +04:00
Speck128_128' = decrypt`{n = 64, m = 2, T = 32}
Speck128_192' = decrypt`{n = 64, m = 3, T = 33}
Speck128_256' = decrypt`{n = 64, m = 4, T = 34}
// check only a few of them for now
property correctSpeck32_64 (k, b) = Speck32_64' k (Speck32_64 k b) == b
property correctSpeck64_96 (k, b) = Speck64_96' k (Speck64_96 k b) == b
property correctSpeck96_144 (k, b) = Speck96_144' k (Speck96_144 k b) == b
2014-04-25 01:27:34 +04:00
property correctSpeck128_128 (k, b) = Speck128_128' k (Speck128_128 k b) == b
property correctSpeck128_256 (k, b) = Speck128_256' k (Speck128_256 k b) == b
2014-04-18 02:34:25 +04:00
///////////////////////////////////////////////////////////////////////
// round function
///////////////////////////////////////////////////////////////////////
R : {n} (fin n) => [n] -> ([n], [n]) -> ([n], [n])
R k (x, y) = f2 (f1 k (x, y))
R' : {n} (fin n) => [n] -> ([n], [n]) -> ([n], [n])
2014-04-25 01:27:34 +04:00
R' k (x, y) = ((x ^ k) - z <<< (if `n == 16 then 7 else 8), z)
where z = (x ^ y) >>> (if `n == 16 then 2 else 3)
2014-04-18 02:34:25 +04:00
f1 : {n} (fin n) => [n] -> ([n], [n]) -> ([n], [n])
f1 k (x, y) = (y, (x >>> (if `n == 16 then 7 else 8)) + y ^ k)
f2 : {n} (fin n) => ([n], [n]) -> ([n], [n])
f2 (x, y) = (y, x <<< (if `n == 16 then 2 else 3) ^ y)
///////////////////////////////////////////////////////////////////////
// encryption / decryption
///////////////////////////////////////////////////////////////////////
2014-04-25 01:27:34 +04:00
encrypt : {n, m, T}
( fin n, fin m, fin T
, m >= 2, T >= 2, n >= 2
2014-04-25 01:33:43 +04:00
, n >= width (T-2)
2014-04-25 01:27:34 +04:00
) => [m][n] -> ([n], [n]) -> ([n], [n])
encrypt k0 b0 = bs ! 0
where
bs = [b0] # [R k b | b <- bs | k <- ks]
ks = expandKey`{n = n, m = m, T = T} (reverse k0)
decrypt : {n, m, T}
( fin n, fin m, fin T
, m >= 2, T >= 2, n >= 2
2014-04-25 01:33:43 +04:00
, n >= width (T-2)
2014-04-25 01:27:34 +04:00
) => [m][n] -> ([n], [n]) -> ([n], [n])
decrypt k0 b0 = bs ! 0
where
bs = [b0] # [R' k b | b <- bs | k <- reverse ks]
ks = expandKey`{n = n, m = m, T = T} (reverse k0)
2014-04-18 02:34:25 +04:00
///////////////////////////////////////////////////////////////////////
// key expansion
///////////////////////////////////////////////////////////////////////
2014-04-25 01:27:34 +04:00
expandKey : {n, m, T}
( fin n, fin m, fin T
, m >= 2, n >= 2, T >= 2
, n >= width (T-2)
) => [m][n] -> [T][n]
expandKey K = ks
where
ls = drop`{1} K # [snd (f1 i (l, k)) | l <- ls | k <- ks | i <- [0 .. T - 2]]
ks = take`{1} K # [snd (f2 (k, l)) | l <- drop`{m - 1} ls | k <- ks]
snd (x, y) = y
2014-04-18 02:34:25 +04:00
///////////////////////////////////////////////////////////////////////
// tests
///////////////////////////////////////////////////////////////////////
property testsPass = tests == ~zero
tests = [t01, t02, t03, t04, t05, t06, t07, t08, t09]
2014-04-25 01:27:34 +04:00
t00 = Speck32_64 [0x1918, 0x1110, 0x0908, 0x0100] (0x6574, 0x694C) == (0xA868, 0x42F2)
t01 = Speck48_72 [0x121110, 0x0A0908, 0x020100] (0x20796C, 0x6C6172) == (0xC049A5, 0x385ADC)
t02 = Speck48_96 [0x1A1918, 0x121110, 0x0A0908, 0x020100] (0x6D2073, 0x696874) == (0x735E10, 0xB6445D)
t03 = Speck64_96 [0x13121110, 0x0B0A0908, 0x03020100] (0x74614620, 0x736E6165) == (0x9F7952EC, 0x4175946C)
t04 = Speck64_128 [0x1B1A1918, 0x13121110, 0x0B0A0908, 0x03020100] (0x3B726574, 0x7475432D) == (0x8C6FA548, 0x454E028B)
t05 = Speck96_96 [0x0D0C0B0A0908, 0x050403020100] (0x65776F68202C, 0x656761737520) == (0x9E4D09AB7178, 0x62BDDE8F79AA)
t06 = Speck96_144 [0x151413121110, 0x0D0C0B0A0908, 0x050403020100] (0x656D6974206E, 0x69202C726576) == (0x2BF31072228A, 0x7AE440252EE6)
t07 = Speck128_128 [0x0F0E0D0C0B0A0908, 0x0706050403020100] (0x6C61766975716520, 0x7469206564616D20) == (0xA65D985179783265, 0x7860FEDF5C570D18)
t08 = Speck128_192 [0x1716151413121110, 0x0F0E0D0C0B0A0908, 0x0706050403020100] (0x7261482066656968, 0x43206F7420746E65) == (0x1BE4CF3A13135566, 0xF9BC185DE03C1886)
t09 = Speck128_256 [0x1F1E1D1C1B1A1918, 0x1716151413121110, 0x0F0E0D0C0B0A0908, 0x0706050403020100] (0x65736F6874206E49, 0x202E72656E6F6F70) == (0x4109010405C0F53E, 0x4EEEB48D9C188F43)