mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-30 23:45:23 +03:00
Merge branch 'master' of https://github.com/davidlazar/cryptol into davidlazar-master
This commit is contained in:
Dylan McNamee
commit
203b2c8596
@ -35,9 +35,9 @@ 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 b = Simon32_64' k (Simon32_64 k b) == b
|
||||
property correctSimon64_96 k b = Simon64_96' k (Simon64_96 k b) == b
|
||||
property correctSimon96_144 k b = Simon96_144' k (Simon96_144 k b) == b
|
||||
property correctSimon32_64 k b = Simon32_64' k (Simon32_64 k b) == b
|
||||
property correctSimon64_96 k b = Simon64_96' k (Simon64_96 k b) == b
|
||||
property correctSimon96_144 k b = Simon96_144' k (Simon96_144 k b) == b
|
||||
property correctSimon128_128 k b = Simon128_128' k (Simon128_128 k b) == b
|
||||
property correctSimon128_256 k b = Simon128_256' k (Simon128_256 k b) == b
|
||||
|
||||
|
||||
@ -1,170 +0,0 @@
|
||||
/*
|
||||
* 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
|
||||
///////////////////////////////////////////////////////////////////////
|
||||
|
||||
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
|
||||
/* pragma correctSpeck32_64 : TODO */
|
||||
property correctSpeck64_96 (k, b) = Speck64_96' k (Speck64_96 k b) == b
|
||||
/* pragma correctSpeck64_96 : TODO */
|
||||
property correctSpeck96_144 (k, b) = Speck96_144' k (Speck96_144 k b) == b
|
||||
/* pragma correctSpeck96_144 : TODO */
|
||||
property correctSpeck128_128 (k, b) =
|
||||
Speck128_128' k (Speck128_128 k b) == b
|
||||
/* pragma correctSpeck128_128 : TODO */
|
||||
property correctSpeck128_256 (k, b) =
|
||||
Speck128_256' k (Speck128_256 k b) == b
|
||||
/* pragma correctSpeck128_256 : TODO */
|
||||
|
||||
|
||||
///////////////////////////////////////////////////////////////////////
|
||||
// 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, 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, 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)
|
||||
121
examples/contrib/speck.cry
Normal file
121
examples/contrib/speck.cry
Normal file
@ -0,0 +1,121 @@
|
||||
/*
|
||||
* 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
|
||||
///////////////////////////////////////////////////////////////////////
|
||||
|
||||
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)
|
||||
Loading…
Reference in New Issue
Block a user