mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-16 03:05:44 +03:00
126 lines
5.3 KiB
Plaintext
126 lines
5.3 KiB
Plaintext
/* Cryptol specification of the Simon block cipher
|
|
* Author: David Lazar
|
|
*/
|
|
|
|
///////////////////////////////////////////////////////////////////////
|
|
// parameters
|
|
///////////////////////////////////////////////////////////////////////
|
|
|
|
Simon32_64 = encrypt `{n=16,m=4,T=32,j=0}
|
|
Simon48_72 = encrypt `{n=24,m=3,T=36,j=0}
|
|
Simon48_96 = encrypt `{n=24,m=4,T=36,j=1}
|
|
Simon64_96 = encrypt `{n=32,m=3,T=42,j=2}
|
|
Simon64_128 = encrypt `{n=32,m=4,T=44,j=3}
|
|
Simon96_96 = encrypt `{n=48,m=2,T=52,j=2}
|
|
Simon96_144 = encrypt `{n=48,m=3,T=54,j=3}
|
|
Simon128_128 = encrypt `{n=64,m=2,T=68,j=2}
|
|
Simon128_192 = encrypt `{n=64,m=3,T=69,j=3}
|
|
Simon128_256 = encrypt `{n=64,m=4,T=72,j=4}
|
|
|
|
Simon32_64' = decrypt `{n=16,m=4,T=32,j=0}
|
|
Simon48_72' = decrypt `{n=24,m=3,T=36,j=0}
|
|
Simon48_96' = decrypt `{n=24,m=4,T=36,j=1}
|
|
Simon64_96' = decrypt `{n=32,m=3,T=42,j=2}
|
|
Simon64_128' = decrypt `{n=32,m=4,T=44,j=3}
|
|
Simon96_96' = decrypt `{n=48,m=2,T=52,j=2}
|
|
Simon96_144' = decrypt `{n=48,m=3,T=54,j=3}
|
|
Simon128_128' = decrypt `{n=64,m=2,T=68,j=2}
|
|
Simon128_192' = decrypt `{n=64,m=3,T=69,j=3}
|
|
Simon128_256' = decrypt `{n=64,m=4,T=72,j=4}
|
|
|
|
// check only a few of them for now
|
|
property correctSimon32_64 k p = Simon32_64' k (Simon32_64 k p) == p
|
|
property correctSimon64_96 k p = Simon64_96' k (Simon64_96 k p) == p
|
|
property correctSimon96_144 k p = Simon96_144' k (Simon96_144 k p) == p
|
|
property correctSimon128_128 k p = Simon128_128' k (Simon128_128 k p) == p
|
|
property correctSimon128_256 k p = Simon128_256' k (Simon128_256 k p) == p
|
|
|
|
|
|
///////////////////////////////////////////////////////////////////////
|
|
// round function
|
|
///////////////////////////////////////////////////////////////////////
|
|
|
|
R k (x, y) = (y ^ f x ^ k, x)
|
|
|
|
// inverse
|
|
R' k (x, y) = (y, x ^ f y ^ k)
|
|
|
|
f x = ((x <<< 1) && (x <<< 8)) ^ (x <<< 2)
|
|
|
|
|
|
///////////////////////////////////////////////////////////////////////
|
|
// encryption / decryption
|
|
///////////////////////////////////////////////////////////////////////
|
|
|
|
encrypt : {n, m, T, j}
|
|
( fin n, fin m, fin T, fin j
|
|
, n >= 2, T - 1 >= m, T >= 1
|
|
) => [m][n] -> ([n], [n]) -> ([n], [n])
|
|
encrypt k0 p0 = ps ! 0
|
|
where
|
|
ps = [p0] # [ R k p | p <- ps | k <- ks ]
|
|
ks = expandKey `{n=n,m=m,T=T,j=j} (reverse k0)
|
|
|
|
|
|
decrypt : {n, m, T, j}
|
|
( fin n, fin m, fin T, fin j
|
|
, n >= 2, T - 1 >= m, T >= 1
|
|
) => [m][n] -> ([n], [n]) -> ([n], [n])
|
|
decrypt k0 p0 = ps ! 0
|
|
where
|
|
ps = [p0] # [ R' k p | p <- ps | k <- reverse ks ]
|
|
ks = expandKey `{n=n,m=m,T=T,j=j} (reverse k0)
|
|
|
|
|
|
///////////////////////////////////////////////////////////////////////
|
|
// key expansion
|
|
///////////////////////////////////////////////////////////////////////
|
|
|
|
expandKey : {n, m, T, j}
|
|
( fin n, fin m, fin T, fin j
|
|
, n >= 2, T - 1 >= m, T >= 1
|
|
) => [m][n] -> [T][n]
|
|
expandKey k0 = k
|
|
where
|
|
k = k0 # [ r where
|
|
o = k @ (i - 1) >>> 3
|
|
p = if `m == 4 then o ^ k @ (i - 3) else o
|
|
q = p ^ p >>> 1
|
|
r = ~ k @ (i - `m) ^ q ^ z ^ 3
|
|
z = Z @ `j @ ((i - `m) % 62)
|
|
| i <- [m .. T - 1]
|
|
]
|
|
|
|
// TODO specify how Z is constructed
|
|
Z = [[1,1,1,1,1,0,1,0,0,0,1,0,0,1,0,1,0,1,1,0,0,0,0,1,1,1,0,0,1,1,0
|
|
,1,1,1,1,1,0,1,0,0,0,1,0,0,1,0,1,0,1,1,0,0,0,0,1,1,1,0,0,1,1,0],
|
|
[1,0,0,0,1,1,1,0,1,1,1,1,1,0,0,1,0,0,1,1,0,0,0,0,1,0,1,1,0,1,0
|
|
,1,0,0,0,1,1,1,0,1,1,1,1,1,0,0,1,0,0,1,1,0,0,0,0,1,0,1,1,0,1,0],
|
|
[1,0,1,0,1,1,1,1,0,1,1,1,0,0,0,0,0,0,1,1,0,1,0,0,1,0,0,1,1,0,0
|
|
,0,1,0,1,0,0,0,0,1,0,0,0,1,1,1,1,1,1,0,0,1,0,1,1,0,1,1,0,0,1,1],
|
|
[1,1,0,1,1,0,1,1,1,0,1,0,1,1,0,0,0,1,1,0,0,1,0,1,1,1,1,0,0,0,0
|
|
,0,0,1,0,0,1,0,0,0,1,0,1,0,0,1,1,1,0,0,1,1,0,1,0,0,0,0,1,1,1,1],
|
|
[1,1,0,1,0,0,0,1,1,1,1,0,0,1,1,0,1,0,1,1,0,1,1,0,0,0,1,0,0,0,0
|
|
,0,0,1,0,1,1,1,0,0,0,0,1,1,0,0,1,0,1,0,0,1,0,0,1,1,1,0,1,1,1,1]
|
|
]
|
|
|
|
|
|
///////////////////////////////////////////////////////////////////////
|
|
// tests
|
|
///////////////////////////////////////////////////////////////////////
|
|
|
|
property testsPass = tests == ~zero
|
|
|
|
tests = [t01, t02, t03, t04, t05, t06, t07, t08, t09]
|
|
|
|
t00 = Simon32_64 [0x1918, 0x1110, 0x0908, 0x0100] (0x6565, 0x6877) == (0xc69b, 0xe9bb)
|
|
t01 = Simon48_72 [0x121110, 0x0a0908, 0x020100] (0x612067, 0x6e696c) == (0xdae5ac, 0x292cac)
|
|
t02 = Simon48_96 [0x1a1918, 0x121110, 0x0a0908, 0x020100] (0x726963, 0x20646e) == (0x6e06a5, 0xacf156)
|
|
t03 = Simon64_96 [0x13121110, 0x0b0a0908, 0x03020100] (0x6f722067, 0x6e696c63) == (0x5ca2e27f, 0x111a8fc8)
|
|
t04 = Simon64_128 [0x1b1a1918, 0x13121110, 0x0b0a0908, 0x03020100] (0x656b696c, 0x20646e75) == (0x44c8fc20, 0xb9dfa07a)
|
|
t05 = Simon96_96 [0x0d0c0b0a0908, 0x050403020100] (0x2072616c6c69, 0x702065687420) == (0x602807a462b4, 0x69063d8ff082)
|
|
t06 = Simon96_144 [0x151413121110, 0x0d0c0b0a0908, 0x050403020100] (0x746168742074, 0x73756420666f) == (0xecad1c6c451e, 0x3f59c5db1ae9)
|
|
t07 = Simon128_128 [0x0f0e0d0c0b0a0908, 0x0706050403020100] (0x6373656420737265, 0x6c6c657661727420) == (0x49681b1e1e54fe3f, 0x65aa832af84e0bbc)
|
|
t08 = Simon128_192 [0x1716151413121110, 0x0f0e0d0c0b0a0908, 0x0706050403020100] (0x206572656874206e, 0x6568772065626972) == (0xc4ac61effcdc0d4f, 0x6c9c8d6e2597b85b)
|
|
t09 = Simon128_256 [0x1f1e1d1c1b1a1918, 0x1716151413121110, 0x0f0e0d0c0b0a0908, 0x0706050403020100] (0x74206e69206d6f6f, 0x6d69732061207369) == (0x8d2b5579afc8a3a0, 0x3bf72a87efe7b868)
|