mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-22 03:19:57 +03:00
96 lines
3.5 KiB
Plaintext
96 lines
3.5 KiB
Plaintext
/*
|
|
* Copyright (c) 2013-2016 Galois, Inc.
|
|
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
*/
|
|
module SCrypt where
|
|
|
|
import Salsa20
|
|
import PBKDF2
|
|
|
|
// SCrypt paper page 10: BlockMix specialized to Salsa20
|
|
BlockMix : {r} (fin r, r >= 1) => [2*r][64*8] -> [2*r][64*8]
|
|
BlockMix B = ys @@ ([0,2..2*r-2] # [1,3..2*r-1])
|
|
where
|
|
rs = [B!0] # [ join (Salsa20 `{r=8} (split (X ^ bi))) | X <- rs | bi <- B ]
|
|
ys = drop `{1} rs
|
|
|
|
// SMix with the ROMix algorithm (section 5) inlined (specialized to BlockMix)
|
|
// N = 2^^17
|
|
SMix : {N,r} ( fin r
|
|
, r >= 1
|
|
, N >= 1
|
|
, 512 >= width N
|
|
, 1 + width N >= width (N-1)
|
|
) => [128 * 8 * r] -> [128 * 8 * r]
|
|
SMix B = join (Xs ! 0)
|
|
where
|
|
Vs = [split B] # [ BlockMix x | x <- Vs | _ <- [0..N-1] : [_][width N + 1]]
|
|
V = take `{front=N} Vs
|
|
|
|
Xs : [N+1][2*r][64*8]
|
|
Xs = [Vs!0] # [ (x' where
|
|
j = integerify x
|
|
T = x ^ (V@j)
|
|
x' = BlockMix T)
|
|
| x <- Xs | _ <- [0..N-1] : [_][width N + 1] ]
|
|
|
|
integerify w = (join (reverse (split `{each=8} (w!0)))) % `N
|
|
|
|
// SCrypt paper, page 11: MFCrypt specialized to sha256 (see the 'pbkdf2' function)
|
|
// p = 1
|
|
MFcrypt : { pwBytes, saltBytes, dkLen, r, N }
|
|
( fin dkLen
|
|
, 4*r >= 1
|
|
, 8 * dkLen >= 1
|
|
, 64 >= width (8 * pwBytes)
|
|
, 32 >= width (4 + saltBytes)
|
|
, 512 >= width N, 1+width N >= width (N-1)
|
|
, 32 >= width ((255 + 8 * dkLen) / 256)
|
|
, 32 >= width (4 + 128 * r)
|
|
, N >= 1
|
|
)
|
|
=> [pwBytes][8] -> [saltBytes][8] -> [dkLen][8]
|
|
MFcrypt P S = split DK
|
|
where
|
|
B = pbkdf2 `{C=1} P S
|
|
B' = SMix `{N=N,r=r} B
|
|
DK = pbkdf2 `{dkLenBits=dkLen*8, C=1} P (split B')
|
|
|
|
SCrypt : {pwBytes, saltBytes, dkBytes, r, N}
|
|
( fin dkBytes, 4*r >= 1
|
|
, 8 * dkBytes >= 1
|
|
, 32 >= width ((255 + 8 * dkBytes) / 256)
|
|
, 64 >= width (8 * pwBytes)
|
|
, 512 >= width N, 1+width N >= width (N-1)
|
|
, 32 >= width (4 + saltBytes)
|
|
, 32 >= width (4 + 128 * r)
|
|
, N >= 1
|
|
)
|
|
=> [pwBytes][8] -> [saltBytes][8] -> [dkBytes][8]
|
|
SCrypt P S = MFcrypt `{r=r,N=N} P S
|
|
|
|
property kats_pass = ~zero ==
|
|
[ SCrypt `{N=2^^4,r=1} "" "" ==
|
|
[ 0x77, 0xd6, 0x57, 0x62, 0x38, 0x65, 0x7b, 0x20
|
|
, 0x3b, 0x19, 0xca, 0x42, 0xc1, 0x8a, 0x04, 0x97
|
|
, 0xf1, 0x6b, 0x48, 0x44, 0xe3, 0x07, 0x4a, 0xe8
|
|
, 0xdf, 0xdf, 0xfa, 0x3f, 0xed, 0xe2, 0x14, 0x42
|
|
, 0xfc, 0xd0, 0x06, 0x9d, 0xed, 0x09, 0x48, 0xf8
|
|
, 0x32, 0x6a, 0x75, 0x3a, 0x0f, 0xc8, 0x1f, 0x17
|
|
, 0xe8, 0xd3, 0xe0, 0xfb, 0x2e, 0x0d, 0x36, 0x28
|
|
, 0xcf, 0x35, 0xe2, 0x0c, 0x38, 0xd1, 0x89, 0x06
|
|
]
|
|
// This tests takes too long in the Cryptol interpreter. Run once, comment it
|
|
// out and be happy.
|
|
// , SCrypt {N=2^^14, r=8} "pleaseletmein" "SodiumChloride" ==
|
|
// [ 0x70, 0x23, 0xbd, 0xcb, 0x3a, 0xfd, 0x73, 0x48
|
|
// , 0x46, 0x1c, 0x06, 0xcd, 0x81, 0xfd, 0x38, 0xeb
|
|
// , 0xfd, 0xa8, 0xfb, 0xba, 0x90, 0x4f, 0x8e, 0x3e
|
|
// , 0xa9, 0xb5, 0x43, 0xf6, 0x54, 0x5d, 0xa1, 0xf2
|
|
// , 0xd5, 0x43, 0x29, 0x55, 0x61, 0x3f, 0x0f, 0xcf
|
|
// , 0x62, 0xd4, 0x97, 0x05, 0x24, 0x2a, 0x9a, 0xf9
|
|
// , 0xe6, 0x1e, 0x85, 0xdc, 0x0d, 0x65, 0x1e, 0x40
|
|
// , 0xdf, 0xcf, 0x01, 0x7b, 0x45, 0x57, 0x58, 0x87
|
|
// ]
|
|
]
|