mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-16 20:03:27 +03:00
122 lines
5.0 KiB
Plaintext
122 lines
5.0 KiB
Plaintext
/*
|
|
* Copyright (c) 2013-2016 Galois, Inc.
|
|
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
*/
|
|
|
|
/* Cryptol specification of the Speck block cipher
|
|
* Author: David Lazar
|
|
*/
|
|
|
|
///////////////////////////////////////////////////////////////////////
|
|
// parameters
|
|
///////////////////////////////////////////////////////////////////////
|
|
|
|
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}
|
|
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
|
|
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
|
|
|
|
|
|
///////////////////////////////////////////////////////////////////////
|
|
// 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])
|
|
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)
|
|
|
|
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
|
|
///////////////////////////////////////////////////////////////////////
|
|
|
|
encrypt : {n, m, T}
|
|
( fin n, fin m, fin T
|
|
, m >= 2, T >= 2, n >= 2
|
|
, n >= width (T-2)
|
|
) => [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
|
|
, n >= width (T-2)
|
|
) => [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)
|
|
|
|
|
|
///////////////////////////////////////////////////////////////////////
|
|
// key expansion
|
|
///////////////////////////////////////////////////////////////////////
|
|
|
|
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
|
|
|
|
|
|
///////////////////////////////////////////////////////////////////////
|
|
// tests
|
|
///////////////////////////////////////////////////////////////////////
|
|
|
|
property testsPass = tests == ~zero
|
|
|
|
tests = [t01, t02, t03, t04, t05, t06, t07, t08, t09]
|
|
|
|
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)
|