GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 09:23:04 +03:00
Code Issues Projects Releases Wiki Activity

Example: miniLock in Cryptol

Browse Source
This commit is contained in:
Thomas M. DuBuisson 2016-01-19 13:47:35 -08:00 committed by Adam C. Foltzer
parent 58a605e8ff
commit a4e42b8429
18 changed files with 3702 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

254
examples/MiniLock/File.md Normal file
View File

@ -0,0 +1,254 @@
Define the minilock file format, encoding only.
```cryptol
module File where
import Keys
import CfrgCurves
import Blake2s
import Base64
import Poly1305
import Salsa20
import CryptoBox
```
The file format is:
> miniLock magic bytes (8 bytes)
> Header length in bytes (4 bytes, little-endian)
> Header bytes (JSON, fields sometimes encrypted)
> Ciphertext bytes
Variable sized formats are potentially awkward for Cryptol because Cryptol
encodes the length of values in the type. For example, the header size varies
in the JS implementation. Fortunately this variablity is all due to either the
arbitrary choices of the encoder or things deterministicly dependent on the
input type (vs value). For an example of the later case, the number of
recipients leads to a variable header size that is computable from the input
type. The former is a larger issue - for example a Base58 encoding of 0 could
be an arbitrary number of the letter 'A' ("A", "AA", etc). For encoding this
is handled by emitting the maximum encoding (46 bytes for minilock
identifications), but this issue prevents us from implementing a decoder that
would interoperate with anything interesting.
The header format is:
> {
> version: Version of the miniLock protocol used for this file (Currently 1) (Number)
> ephemeral: Public key from ephemeral key pair used to encrypt decryptInfo object (Base64),
> decryptInfo: {
> (One copy of the below object for every recipient)
> Unique nonce for decrypting this object (Base64): {
> senderID: Sender's miniLock ID (Base58),
> recipientID: miniLock ID of this recipient (used for verfication) (Base58),
> fileInfo: {
> fileKey: Key for file decryption (Base64),
> fileNonce: Nonce for file decryption (Base64),
> fileHash: BLAKE2 hash (32 bytes) of the ciphertext bytes. (Base64)
> } (fileInfo is encrypted to recipient's public key using long-term key pair) (Base64),
> } (encrypted to recipient's public key using ephemeral key pair) (Base64)
> }
```cryptol
// Size of a given minilock container depends soley on the number of recipients and the plaintext
type MiniLockBytes nrRecip fileSize = 8 + 4 + 89 + (DecryptInfoSize + 1) * nrRecip + EncryptedBytes fileSize - 1
minilock : {nrRecip, fileNameBytes, msgBytes}
( fin nrRecip, fin fileNameBytes, fin msgBytes // All the values are finite
, nrRecip >= 1, 22 >= width nrRecip // Between 1 and 4M recipients
, 63 >= width msgBytes // Messages leq 2^63 bytes
, fileNameBytes >= 1, 256 >= fileNameBytes // Between 1 and 256 byte file name
) =>
[nrRecip](MinilockID,[24][8]) // Recipients and nonces for the fileInfo field
-> [fileNameBytes][8] // File name
-> [msgBytes][8] // Plaintext
-> (Private25519, Public25519) // Sender keys
-> [32][8] // File key (random)
-> [16][8] // File nonce (random)
-> (Private25519, Public25519) // Ephemeral keys (random)
-> [MiniLockBytes nrRecip msgBytes][8]
minilock rs fileName0 msg senderKeys fileKey fileNonce ephemKeys = lockFile
where
filename = take `{256} (fileName0 # (zero : [256][8]))
ct = encryptData fileKey fileNonce filename msg
fileInfo = mkFileInfoBlob (fileKey, fileNonce, split (blake2s `{nn=32} ct))
lockFile = mkMiniLock rs senderKeys ephemKeys fileInfo ct
private
magic : [8][8]
magic = [0x6d, 0x69, 0x6e, 0x69, 0x4c, 0x6f, 0x63, 0x6b]
encryptData : {msgBytes} (63 >= width msgBytes)
=> [32][8]-> [16][8] -> [256][8] -> [msgBytes][8] -> [EncryptedBytes msgBytes][8]
encryptData k n f m = encryptChunks k n f cs cN
where
(cs,cN) = mkChunks m
// encrypt chunks results in the ciphertext AND poly1305 tag for each chunk.
encryptChunks : {chunks,rem}
(fin chunks, fin rem
, 32 >= width rem
, 64 >= width chunks)
=> [32][8] -> [16][8] -> [256][8] -> [chunks]Chunk -> [rem][8]
-> [4 + 16 + 256 + chunks*((2^^20) + 4 + 16) + 4 + 16 + rem][8]
encryptChunks key nonce c0 cs end = encChunk0 # join ctChunks # ctFinal
where
fullNonce0 = nonce # put64le zero
encChunk0 = put32le 256 # crypto_secretbox c0 key fullNonce0 : [4 + 16 + 256][8]
nonces = [nonce # put64le i | i <- [1...]]
ctChunks = [put32le (2^^20) # crypto_secretbox cnk key n | n <- nonces | cnk <- cs]
nFinal = nonce # put64le ((`chunks + 1) || 0x8000000000000000)
ctFinal = put32le `rem # crypto_secretbox end key nFinal
```
The minilock file format is a concatenation of the magic, header length field, header, and ciphertext.
```cryptol
// Size of the 'decryptInfo' javascript record.
type DecryptInfoSize = 549
mkMiniLock : {nrRecip, ctBytes} (22 >= width nrRecip, nrRecip >= 1) =>
[nrRecip](MinilockID,[24][8])
-> (Private25519, Public25519)
-> (Private25519, Public25519)
-> FileInfoBlob
-> [ctBytes][8]
-> [8 + 4 + 89 + (DecryptInfoSize + 1) * nrRecip + ctBytes - 1][8]
mkMiniLock rs senderKeys ephemKeys fileInfo ct =
magic # put32le (width header) # header # ct
where
header = mkHeader rs senderKeys ephemKeys fileInfo
```
Construction of the "file info blob" means we build the plaintext value:
> {
> fileKey: Key for file decryption (Base64),
> fileNonce: Nonce for file decryption (Base64),
> fileHash: BLAKE2 hash (32 bytes) of the ciphertext bytes. (Base64)
> }
```cryptol
// The triple of Key and nonce protecting the file along with the file's hash
type FileInfo = ([32][8], [16][8], [32][8])
type FileInfoBlob = [155][8]
mkFileInfoBlob : FileInfo
-> FileInfoBlob
mkFileInfoBlob (key,nonce,hash) =
brace(
jsonPair "fileKey" (quote64 key) # "," #
jsonPair "fileNonce" (quote64 nonce) # "," #
jsonPair "fileHash" (quote64 hash)
)
```
The header includes the public ephemeral key, version, and NrRecip copies of the
fileinfo inside a decryptInfo field as such:
> version: Version of the miniLock protocol used for this file (Currently 1) (Number)
> ephemeral: Public key from ephemeral key pair used to encrypt decryptInfo object (Base64),
> decryptInfo: { nonce1 : { encryptedFileInfo }
> , nonce2 : ...
> , ...
> }
```cryptol
mkHeader : {nrRecip} (fin nrRecip, nrRecip >= 1)
=> [nrRecip](MinilockID,[24][8])
-> (Private25519, Public25519)
-> (Private25519, Public25519)
-> FileInfoBlob
-> [89 + (DecryptInfoSize+1) * nrRecip - 1][8]
mkHeader rs senderKeys ephemKeys infoBlob =
brace (
jsonPair "version" "1" # ","
# jsonPair "ephemeral" (quote64 ephemKeys.1) # ","
# jsonPair "decryptInfo" (brace decInfoFull)
)
where
ds = [ mkDecryptInfo senderKeys ephemKeys recvID recvNonce infoBlob # "," | (recvID,recvNonce) <- rs ]
// Drop the trailing comma
decInfoFull = take `{back = min nrRecip 1} (join ds)
// XXX return 'succ' for successful decode of the public id
mkDecryptInfo :
(Private25519, Public25519)
-> (Private25519, Public25519)
-> MinilockID -> [24][8] -> FileInfoBlob -> [DecryptInfoSize][8]
mkDecryptInfo senderKeys ephemKeys theirID nonce infoBlob = quote64 nonce # ":" # quote ct
where
ct = encryptWith nonce (ephemKeys.0) theirPublic internals
internals = brace ( jsonPair "senderID" (quote (encodeID senderKeys.1)) # ","
# jsonPair "recipientID" (quote theirID) # ","
# jsonPair "fileInfo" (quote fileInfoCT)
)
fileInfoCT = encryptWith nonce (senderKeys.0) theirPublic infoBlob
(succ,theirPublic) = decodeID theirID
encryptWith : {n} (2^^64 >= 32 + n) => [24][8] -> Private25519 -> Public25519 -> [n][8] -> [Enc64 (n+16)][8]
encryptWith nonce secret public pt = base64enc (crypto_box pt nonce public secret)
type NrChunks ptBytes = ptBytes / (2^^20)
type LastChunkSize ptBytes = ptBytes - (NrChunks ptBytes) * 2^^20
type EncryptedBytes ptBytes = 4 + 16 + 256 + (NrChunks ptBytes) * ((2^^20) + 4 + 16) + 4 + 16 + LastChunkSize ptBytes
type ChunkSize = 2^^20
type Chunk = [ChunkSize][8]
type FullChunks bytes = bytes / ChunkSize
type Rem bytes = bytes - FullChunks bytes * ChunkSize
mkChunks : {bytes} ( fin bytes )
=> [bytes][8] -> ([FullChunks bytes]Chunk, [Rem bytes][8])
mkChunks pt = (cs,last)
where cs = split (take `{front = FullChunks bytes * ChunkSize, back = Rem bytes} pt)
last = drop `{FullChunks bytes * ChunkSize} pt
```
The above code used some custom utility functions, which appear below.
```cryptol
put32le : [32] -> [4][8]
put32le x = reverse (split x)
put64le : [64] -> [8][8]
put64le x = reverse (split x)
quote : {m} (fin m) => [m][8] -> [m+2][8]
quote m = "\"" # m # "\""
brace : {m} (fin m) => [m][8] -> [m+2][8]
brace m = "{" # m # "}"
quote64 : {m} (fin m) => [m][8] -> [4*(m + (3 - m % 3) % 3)/3 + 2][8]
quote64 m = quote (base64enc m)
jsonPair : {m,n} (fin m) => [m][8] -> [n][8] -> [3+m+n][8]
jsonPair m n = quote m # ":" # n
// Encrypt a file such that one recipient
// User: "example@example.com
// Pass: "some bears eat all the honey in the jar"
//
// Can decrypt.
test_lock fname cont = file
where
myPriv = testPriv
myPub = testPub
theirID = testID
ephemPriv = zero # "ephemeral Curve25519"
ephemPub = Curve25519 ephemPriv basePoint25519
nonceA = zero # "recip1 nonce"
nonceF = zero # "file nonce"
key = zero # "file key"
file = minilock [(theirID,nonceA)] fname cont (myPriv,myPub) key nonceF (ephemPriv,ephemPub)
test_construction : [MiniLockBytes 1 13][8]
test_construction = test_lock "some_filename" "some contents"
```

71
examples/MiniLock/Keys.cry Normal file
View File

@ -0,0 +1,71 @@
module Keys where
import CfrgCurves
import Blake2s
import SCrypt
import Base58
type MinilockID = [46][8]
// Given a public key compute the ASCII ID
encodeID : Public25519 -> MinilockID
encodeID pub = base58enc (join (pub # [h]))
where
h = blake2s `{nn=1} pub : [8]
decodeID : MinilockID -> (Bit,Public25519)
decodeID ident = (hComp == hRecv, key)
where
bs = split (base58dec ident) : [33][8]
hRecv = bs ! 0
hComp = blake2s `{nn=1} key : [8]
key = take bs : [32][8]
// Accept a possibly-short key (base58 is value dependent encoding)
// and expand it to the full, fixed, size.
mkFullLengthID : {n} (46 >= n, n>= 1) => [n][8] -> MinilockID
mkFullLengthID n = drop (['1' | _ <- [0..45] : [_][8]] # n)
mkID : {passBytes, saltBytes}
( fin passBytes, fin saltBytes
, 64 >= width passBytes
, 32 >= width (4*saltBytes)
)
=> [passBytes][8] -> [saltBytes][8] -> (MinilockID,Private25519)
mkID pw email = (encodeID pub,priv)
where
// XXX wait for cryptol 2.3: priv = SCrypt `{N=2^^17,r=8} (split (blake2s `{nn=32} pw)) email
priv : Private25519
priv = SCrypt `{N=2^^1,r=8} (split (blake2s `{nn=32} pw)) email
// XXX we can't interpret N=2^^17 so this N value is a place holder...
pub = Curve25519 priv basePoint25519
// XXX we can not run these tests in the cryptol interpreter, SCrypt is too expensive.
testPass = "some bears eat all the honey in the jar"
testEmail = "example@example.com"
testID : MinilockID
testID = mkFullLengthID "28ZvW9rqRqvqpFTtHnusUntRqrxb4qqZAaNAd3QsqjSsXq"
testID_computed = "28ZvW9rqRqvqpFTtHnusUntRqrxb4qqZAaNAd3QsqjSsXq" // Computed on deathstar
testPriv_computed =
[0x12, 0x86, 0xe0, 0x18, 0xc6, 0x68, 0x34, 0x96, 0x09, 0x2e, 0x53,
0x32, 0x37, 0x76, 0x80, 0x3c, 0x30, 0xb4, 0x75, 0x2d, 0xd7, 0x70,
0xea, 0xa9, 0x6f, 0x0d, 0xda, 0x25, 0xc7, 0xfe, 0x28, 0x1f]
// Deathstar results:
// ([0x32, 0x38, 0x5a, 0x76, 0x57, 0x39, 0x72, 0x71, 0x52, 0x71, 0x76,
// 0x71, 0x70, 0x46, 0x54, 0x74, 0x48, 0x6e, 0x75, 0x73, 0x55, 0x6e,
// 0x74, 0x52, 0x71, 0x72, 0x78, 0x62, 0x34, 0x71, 0x71, 0x5a, 0x41,
// 0x61, 0x4e, 0x41, 0x64, 0x33, 0x51, 0x73, 0x71, 0x6a, 0x53, 0x73,
// 0x58, 0x71],
// [0x12, 0x86, 0xe0, 0x18, 0xc6, 0x68, 0x34, 0x96, 0x09, 0x2e, 0x53,
// 0x32, 0x37, 0x76, 0x80, 0x3c, 0x30, 0xb4, 0x75, 0x2d, 0xd7, 0x70,
// 0xea, 0xa9, 0x6f, 0x0d, 0xda, 0x25, 0xc7, 0xfe, 0x28, 0x1f])
// testPriv : Private25519
testPriv = [0x12, 0x86, 0xe0, 0x18, 0xc6, 0x68, 0x34, 0x96, 0x09, 0x2e, 0x53, 0x32, 0x37, 0x76, 0x80, 0x3c, 0x30, 0xb4, 0x75, 0x2d, 0xd7, 0x70,0xea, 0xa9, 0x6f, 0x0d, 0xda, 0x25, 0xc7, 0xfe, 0x28, 0x1f]
testPub = Curve25519 testPriv basePoint25519
property kat_pub_id_eq = testPub == (decodeID testID).1 && encodeID testPub == testID && testID == testID_computed && testPriv == testPriv_computed

38
examples/MiniLock/README.md Normal file
View File

@ -0,0 +1,38 @@
# Minilock in Cryptol
[miniLock](https://minilock.io) is a low-barrier to use file encryption utility
based on the algorithms:
* SCrypt
- PBKDF2
- HMAC-SHA512
* Blake2s
* Base64
* Base58
* CryptoBox
- Salsa20
- Curve25519
- Poly1305
This example is a specification of miniLock file encryption in Cryptol including
all component algorithms as well as primitive JSON encoding to allow
inter-operability between the official miniLock written in JavaScript and files
produced by Cryptol.
# Use
To encrypt a file consider:
```
CRYPTOLPATH=`pwd`/prim cryptol File.md
```
Then use the `miniLock` function such as can be seen in `test_lock`:
```
miniLock [(theirID, nonceA)] filename contents (myPrivKey, myPubKey) key nonceF (ephemPriv, ephemPub)
```
Note SCrypt, and thus miniLock ID and key derivation from user passwords, is too
expensive for the Cryptol interpreter to compute on all but todays more powerful
computers. The ID generation can be done using `mkID` from `Keys.cry`.

40
examples/MiniLock/prim/Base58.cry Normal file
View File

@ -0,0 +1,40 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module Base58 where
// Base 58 is a dependent format - the length of the encoded value depends on
// the value being encoded This does not play well with Cryptol, which expects
// a static type. Thus we must consume the worst-case number of bytes and
// produce a length value which we return to the callee.
// Convert an N bit number (33 bytes for minilock) into a big endian base 58 representation (46 byte max for minilock).
base58enc : {n,m} (fin n, fin m, n >= 6 ) => [n] -> [m][8]
base58enc ns = [ x.1 | x <- reverse (take `{m} (drop `{1} enc))]
where
enc = [(ns,zero)] # [ (n/58,charOf (n%58)) | (n,_) <- enc ]
charOf x = charMap @ x
charMap : [58][8]
charMap = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz"
base58dec : {n,m} (fin n, fin m, n >= 1, n >= width m, n >= 8) => [m][8] -> [n]
base58dec ms = sum [ (dec m) * 58 ^^ i | m <- reverse ms | i <- [0..m] ]
where
dec : [8] -> [n]
dec x = zero # dec' x
dec' : [8] -> [8]
dec' x =
if x >= 'm'
then x - 'm' + 44
else if x >= 'a'
then x - 'a' + 33
else if x >= 'P'
then x - 'P' + 22
else if x > 'I'
then x - 'J' + 17
else if x >= 'A'
then x - 'A' + 9
else x - '1'

53
examples/MiniLock/prim/Base64.cry Normal file
View File

@ -0,0 +1,53 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module Base64 where
type Enc64 n = 4*(((3-(n%3))%3) + n)/3
base64enc : {n,m,padZ} (4*(padZ + n)/3 == m, fin n, fin m, padZ == (3-(n%3))%3, 2>=padZ)
=> [n][8] -> [Enc64 n][8]
base64enc ns = take `{m} (chunks # padEq)
where
chunks = take `{(4*n+2)/3} (base64chunks `{(n+2)/3} (ns # padZero))
padZero = take `{padZ} [zero | _ <- [1..2] : [_][2]]
padEq = "=="
alphabet = ['A'..'Z'] # ['a'..'z'] # ['0'..'9'] # "+/"
base64chunks : {n} (fin n) => [n*3][8] -> [n*4][8]
base64chunks m = [basify x | x <- ns]
where
ns = split (join m) : [_][6]
basify : [6] -> [8]
basify x = alphabet @ x
// Base64 strings are always in 4n byte chunks, the final chunk might be
// padded. We can not give a proper cryptol implementation that strips the
// padding because that would require the type, n, to depend on the value
// (dependant types). Instead we return possibly excess bytes and, separetely,
// the number of pad bytes (0,1 or 2) as a value.
base64dec : {n,m} (fin m, 4*n == 3*m, fin n) => [m][8] -> ([n][8],[2])
base64dec ms = (split (join [debase x | x <- ms]), nrEq)
where
nrEq : [2]
nrEq = sum [ zero # [x == '='] | x <- take `{2} (reverse ms # [zero,zero]) ]
debase : [8] -> [6]
debase x = drop `{2} (debase' x)
debase' : [8] -> [8]
debase' x =
if x >= 'A' && x <= 'Z'
then x - 'A'
else if x >= 'a' && x <= 'z'
then x - 'a' + 26
else if x >= '0' && x <= '9'
then x - '0' + 52
else if x == '+'
then 62
else if x == '/'
then 63
else zero // Pad bytes are decoded as NUL

686
examples/MiniLock/prim/Blake2s.cry Normal file
View File

@ -0,0 +1,686 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module Blake2s where
type Block = [16][32]
type State = [8][32]
type LocalState = [16][32]
type BCounter = [64]
type Context = { state : State, counter : BCounter }
// Block size
bbVal : [64]
bbVal = 64
IV : [8][32]
IV = [ 0x6A09E667, 0xBB67AE85, 0x3C6EF372, 0xA54FF53A,
0x510E527F, 0x9B05688C, 0x1F83D9AB, 0x5BE0CD19
]
SIGMA_TABLE : [10][16][4]
SIGMA_TABLE =
[ [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 ]
, [ 14, 10, 4, 8, 9, 15, 13, 6, 1, 12, 0, 2, 11, 7, 5, 3 ]
, [ 11, 8, 12, 0, 5, 2, 15, 13, 10, 14, 3, 6, 7, 1, 9, 4 ]
, [ 7, 9, 3, 1, 13, 12, 11, 14, 2, 6, 5, 10, 4, 0, 15, 8 ]
, [ 9, 0, 5, 7, 2, 4, 10, 15, 14, 1, 11, 12, 6, 8, 3, 13 ]
, [ 2, 12, 6, 10, 0, 11, 8, 3, 4, 13, 7, 5, 15, 14, 1, 9 ]
, [ 12, 5, 1, 15, 14, 13, 4, 10, 0, 7, 6, 3, 9, 2, 8, 11 ]
, [ 13, 11, 7, 14, 12, 1, 3, 9, 5, 0, 15, 4, 8, 6, 2, 10 ]
, [ 6, 15, 14, 9, 11, 3, 0, 8, 12, 2, 13, 7, 1, 4, 10, 5 ]
, [ 10, 2, 8, 4, 7, 6, 1, 5, 15, 11, 9, 14, 3, 12, 13, 0 ]
]
// Section 2.1 constants
R1,R2,R3,R4 : [6]
R1 = 16
R2 = 12
R3 = 08
R4 = 07
// Section 3.1: Mixing function 'G'
G : [4] -> [4] -> LocalState -> [4][6] -> Block -> [16][32]
G r i vec abcd ms = foldl updateVector vec (zip abcd new)
where
new = G' r i (vec @@ abcd) ms
G' : [4] -> [4] -> [4][32] -> Block -> [4][32]
G' r i vals ms = [a2, b2, c2, d2]
where
x = ms @ (SIGMA_TABLE @ r @ (2*i))
y = ms @ (SIGMA_TABLE @ r @ (2*i+1))
[a,b,c,d] = vals
a1 = a + b + x
d1 = (d ^ a1) >>> R1
c1 = c + d1
b1 = (b ^ c1) >>> R2
a2 = a1 + b1 + y
d2 = (d1 ^ a2) >>> R3
c2 = c1 + d2
b2 = (b1 ^ c2) >>> R4
// Section 3.2: Compression function
F : State -> Block -> BCounter -> Bit -> State
F h ms t f = h ^ (take (vs!0)) ^ (drop (vs!0))
where
v = h # IV ^ (zero # [t0,t1,f0,zero])
[t1,t0] = split t : [2][32]
f0 = [f | _ <- [0..31] : [_][6]]
vs = [v] # [ round i ms v' | v' <- vs | i <- [0..9] ]
// Sub-function of F (first for loop)
round : [4] -> Block -> LocalState -> LocalState
round r ms v = vs ! 0
where
vs = [v] # [ G r i v' ix ms
| v' <- vs
| i <- [0..7]
| ix <- [ [0,4,8,12], [1,5,9,13]
, [2,6,10,14], [3,7,11,15]
, [0,5,10,15], [1,6,11,12]
, [2,7,8,13], [3,4,9,14] ]
]
// Section 3.3: Padding
// Recall kk == key bytes (0)
// nn == hash bytes (32)
// ll == input bytes (ceiling $ len / 8)
// bb == block bytes (64, 1024 bits)
// dd == nr Blocks
blake2s : {ll,nn} (fin ll, 32 >= nn, 64 >= width ll)
=> [ll][8] -> [nn*8]
blake2s m = blake2s' `{ll=ll,nn=nn} m
blake2s' : {ll,dd,nn}
(fin ll
, 32 >= nn
, dd == (max 1 ((ll+63)/64)) - 1
, 64 >= width ll
)
=> [ll][8]
-> [nn*8]
blake2s' m = take `{nn*8} (blake2sFinish ({ state = (hs!0).state, counter = `ll}) lastBlock)
where
fullBlocks : [dd]Block
fullBlocks = [mkBlock b | b <- split (join (take `{front=64*dd,back=ll-64*dd} m))]
partialBlock = drop `{front=64*dd,back=ll-64*dd} m
lastBlock : Block
lastBlock =
if (`ll == (zero:[64]))
then zero // Special case full zero block for empty messages
else mkBlock ((split (join (partialBlock # (zero : [inf][8]))))@0)
h : Context
h = { state = [IV@0 ^ `0x01010000 ^ `nn] # drop `{1} IV, counter = 0 }
hs : [dd+1]Context
hs = [h] # [blake2Update h' dX | h' <- hs | dX <- fullBlocks]
blake2Update : Context -> Block -> Context
blake2Update ctx d = { state = newState, counter = newCount }
where newState = F ctx.state d newCount False
newCount = ctx.counter + (64 : [64])
postprocess : {ll} (64 >= ll, 64 >= width ll) => BCounter -> [ll][8] -> Block
postprocess c m =
if c == 0 && `ll == (zero:[64])
then zero
else split (join m # zero)
// The final round of blake
blake2sFinish : Context -> Block -> [256]
blake2sFinish ctx b = join [ reverseBytes w | w <- F ctx.state b ctx.counter True ]
////////////////////////////////////////////////////////////////////////////////
// Utilities
////////////////////////////////////////////////////////////////////////////////
mkBlock x = reverse (split (reverseBytes x))
reverseBytes x = join (reverse (bytes x))
bytes x = split x : [_] [8]
// XXX can probably do a cleaner merge-sort style update.
updateVector : {a, b, c} (c >= width (a-1), a >= 1, fin a, fin c) => [a]b -> ([c], b) -> [a]b
updateVector orig idxNew = vs
where
idx = idxNew.0
new = idxNew.1
vs = [if i == idx then new else orig@i | i <- [0..a-1]]
property katsPass = ~zero ==
[ nthKat `{0}
, nthKat `{1}
, nthKat `{2}
, nthKat `{3}
, nthKat `{4}
, nthKat `{5}
, nthKat `{6}
, nthKat `{7}
, nthKat `{8}
, nthKat `{9}
, nthKat `{10}
, nthKat `{11}
, nthKat `{12}
, nthKat `{13}
, nthKat `{14}
, nthKat `{15}
, nthKat `{16}
, nthKat `{17}
, nthKat `{18}
, nthKat `{19}
, nthKat `{20}
, nthKat `{21}
, nthKat `{22}
, nthKat `{23}
, nthKat `{24}
, nthKat `{25}
, nthKat `{26}
, nthKat `{27}
, nthKat `{28}
, nthKat `{29}
, nthKat `{30}
, nthKat `{31}
, nthKat `{32}
, nthKat `{33}
, nthKat `{34}
, nthKat `{35}
, nthKat `{36}
, nthKat `{37}
, nthKat `{38}
, nthKat `{39}
, nthKat `{40}
, nthKat `{41}
, nthKat `{42}
, nthKat `{43}
, nthKat `{44}
, nthKat `{45}
, nthKat `{46}
, nthKat `{47}
, nthKat `{48}
, nthKat `{49}
, nthKat `{50}
, nthKat `{51}
, nthKat `{52}
, nthKat `{53}
, nthKat `{54}
, nthKat `{55}
, nthKat `{56}
, nthKat `{57}
, nthKat `{58}
, nthKat `{59}
, nthKat `{60}
, nthKat `{61}
, nthKat `{62}
, nthKat `{63}
, nthKat `{64}
, nthKat `{65}
, nthKat `{66}
, nthKat `{67}
, nthKat `{68}
, nthKat `{69}
, nthKat `{70}
, nthKat `{71}
, nthKat `{72}
, nthKat `{73}
, nthKat `{74}
, nthKat `{75}
, nthKat `{76}
, nthKat `{77}
, nthKat `{78}
, nthKat `{79}
, nthKat `{80}
, nthKat `{81}
, nthKat `{82}
, nthKat `{83}
, nthKat `{84}
, nthKat `{85}
, nthKat `{86}
, nthKat `{87}
, nthKat `{88}
, nthKat `{89}
, nthKat `{90}
, nthKat `{91}
, nthKat `{92}
, nthKat `{93}
, nthKat `{94}
, nthKat `{95}
, nthKat `{96}
, nthKat `{97}
, nthKat `{98}
, nthKat `{99}
, nthKat `{100}
, nthKat `{101}
, nthKat `{102}
, nthKat `{103}
, nthKat `{104}
, nthKat `{105}
, nthKat `{106}
, nthKat `{107}
, nthKat `{108}
, nthKat `{109}
, nthKat `{110}
, nthKat `{111}
, nthKat `{112}
, nthKat `{113}
, nthKat `{114}
, nthKat `{115}
, nthKat `{116}
, nthKat `{117}
, nthKat `{118}
, nthKat `{119}
, nthKat `{120}
, nthKat `{121}
, nthKat `{122}
, nthKat `{123}
, nthKat `{124}
, nthKat `{125}
, nthKat `{126}
, nthKat `{127}
, nthKat `{128}
, nthKat `{129}
, nthKat `{130}
, nthKat `{131}
, nthKat `{132}
, nthKat `{133}
, nthKat `{134}
, nthKat `{135}
, nthKat `{136}
, nthKat `{137}
, nthKat `{138}
, nthKat `{139}
, nthKat `{140}
, nthKat `{141}
, nthKat `{142}
, nthKat `{143}
, nthKat `{144}
, nthKat `{145}
, nthKat `{146}
, nthKat `{147}
, nthKat `{148}
, nthKat `{149}
, nthKat `{150}
, nthKat `{151}
, nthKat `{152}
, nthKat `{153}
, nthKat `{154}
, nthKat `{155}
, nthKat `{156}
, nthKat `{157}
, nthKat `{158}
, nthKat `{159}
, nthKat `{160}
, nthKat `{161}
, nthKat `{162}
, nthKat `{163}
, nthKat `{164}
, nthKat `{165}
, nthKat `{166}
, nthKat `{167}
, nthKat `{168}
, nthKat `{169}
, nthKat `{170}
, nthKat `{171}
, nthKat `{172}
, nthKat `{173}
, nthKat `{174}
, nthKat `{175}
, nthKat `{176}
, nthKat `{177}
, nthKat `{178}
, nthKat `{179}
, nthKat `{180}
, nthKat `{181}
, nthKat `{182}
, nthKat `{183}
, nthKat `{184}
, nthKat `{185}
, nthKat `{186}
, nthKat `{187}
, nthKat `{188}
, nthKat `{189}
, nthKat `{190}
, nthKat `{191}
, nthKat `{192}
, nthKat `{193}
, nthKat `{194}
, nthKat `{195}
, nthKat `{196}
, nthKat `{197}
, nthKat `{198}
, nthKat `{199}
, nthKat `{200}
, nthKat `{201}
, nthKat `{202}
, nthKat `{203}
, nthKat `{204}
, nthKat `{205}
, nthKat `{206}
, nthKat `{207}
, nthKat `{208}
, nthKat `{209}
, nthKat `{210}
, nthKat `{211}
, nthKat `{212}
, nthKat `{213}
, nthKat `{214}
, nthKat `{215}
, nthKat `{216}
, nthKat `{217}
, nthKat `{218}
, nthKat `{219}
, nthKat `{220}
, nthKat `{221}
, nthKat `{222}
, nthKat `{223}
, nthKat `{224}
, nthKat `{225}
, nthKat `{226}
, nthKat `{227}
, nthKat `{228}
, nthKat `{229}
, nthKat `{230}
, nthKat `{231}
, nthKat `{232}
, nthKat `{233}
, nthKat `{234}
, nthKat `{235}
, nthKat `{236}
, nthKat `{237}
, nthKat `{238}
, nthKat `{239}
, nthKat `{240}
, nthKat `{241}
, nthKat `{242}
, nthKat `{243}
, nthKat `{244}
, nthKat `{245}
, nthKat `{246}
, nthKat `{247}
, nthKat `{248}
, nthKat `{249}
, nthKat `{250}
, nthKat `{251}
, nthKat `{252}
, nthKat `{253}
, nthKat `{254}
, nthKat `{255}
]
nthKat : {n} (fin n, 8 >= width n) => Bit
nthKat = blake2s (nthKatInput `{n}) == kats @ (`n : [8])
nthKatInput : {n} (fin n) => [n][8]
nthKatInput = take ([0 ... ] : [inf][8])
kats = [ 0x69217a3079908094e11121d042354a7c1f55b6482ca1a51e1b250dfd1ed0eef9
, 0xe34d74dbaf4ff4c6abd871cc220451d2ea2648846c7757fbaac82fe51ad64bea
, 0xddad9ab15dac4549ba42f49d262496bef6c0bae1dd342a8808f8ea267c6e210c
, 0xe8f91c6ef232a041452ab0e149070cdd7dd1769e75b3a5921be37876c45c9900
, 0x0cc70e00348b86ba2944d0c32038b25c55584f90df2304f55fa332af5fb01e20
, 0xec1964191087a4fe9df1c795342a02ffc191a5b251764856ae5b8b5769f0c6cd
, 0xe1fa51618d7df4eb70cf0d5a9e906f806e9d19f7f4f01e3b621288e4120405d6
, 0x598001fafbe8f94ec66dc827d012cfcbba2228569f448e89ea2208c8bf769293
, 0xc7e887b546623635e93e0495598f1726821996c2377705b93a1f636f872bfa2d
, 0xc315a437dd28062a770d481967136b1b5eb88b21ee53d0329c5897126e9db02c
, 0xbb473deddc055fea6228f207da575347bb00404cd349d38c18026307a224cbff
, 0x687e1873a8277591bb33d9adf9a13912efefe557cafc39a7952623e47255f16d
, 0x1ac7ba754d6e2f94e0e86c46bfb262abbb74f450ef456d6b4d97aa80ce6da767
, 0x012c97809614816b5d9494477d4b687d15b96eb69c0e8074a8516f31224b5c98
, 0x91ffd26cfa4da5134c7ea262f7889c329f61f6a657225cc212f40056d986b3f4
, 0xd97c828d8182a72180a06a78268330673f7c4e0635947c04c02323fd45c0a52d
, 0xefc04cdc391c7e9119bd38668a534e65fe31036d6a62112e44ebeb11f9c57080
, 0x992cf5c053442a5fbc4faf583e04e50bb70d2f39fbb6a503f89e56a63e18578a
, 0x38640e9f21983e67b539caccae5ecf615ae2764f75a09c9c59b76483c1fbc735
, 0x213dd34c7efe4fb27a6b35f6b4000d1fe03281af3c723e5c9f94747a5f31cd3b
, 0xec246eeeb9ced3f7ad33ed28660dd9bb0732513db4e2fa278b60cde3682a4ccd
, 0xac9b61d446648c3005d7892bf3a8719f4c8181cfdcbc2b79fef10a279b911095
, 0x7bf8b22959e34e3a43f7079223e83a9754617d391e213dfd808e41b9bead4ce7
, 0x68d4b5d4fa0e302b64ccc5af792913ac4c88ec95c07ddf40694256eb88ce9f3d
, 0xb2c2420f05f9abe36315919336b37e4e0fa33ff7e76a492767006fdb5d935462
, 0x134f61bbd0bbb69aed5343904551a3e6c1aa7dcdd77e903e7023eb7c60320aa7
, 0x4693f9bff7d4f3986a7d176e6e06f72ad1490d805c99e25347b8de77b4db6d9b
, 0x853e26f741953b0fd5bdb424e8ab9e8b3750eaa8ef61e47902c91e554e9c73b9
, 0xf7de536361abaa0e158156cf0ea4f63a99b5e4054f8fa4c9d45f6285cad55694
, 0x4c230608860a99ae8d7bd5c2cc17fa52096b9a61bedb17cb7617864ad29ca7a6
, 0xaeb920ea87952dadb1fb759291e3388139a872865001886ed84752e93c250c2a
, 0xaba4ad9b480b9df3d08ca5e87b0c2440d4e4ea21224c2eb42cbae469d089b931
, 0x05825607d7fdf2d82ef4c3c8c2aea961ad98d60edff7d018983e21204c0d93d1
, 0xa742f8b6af82d8a6ca2357c5f1cf91defbd066267d75c048b352366585025962
, 0x2bcac89599000b42c95ae23835a713704ed79789c84fef149a874ff733f017a2
, 0xac1ed07d048f105a9e5b7ab85b09a492d5baff14b8bfb0e9fd789486eea2b974
, 0xe48d0ecfaf497d5b27c25d99e156cb0579d440d6e31fb62473696dbf95e010e4
, 0x12a91fadf8b21644fd0f934f3c4a8f62ba862ffd20e8e961154c15c13884ed3d
, 0x7cbee96e139897dc98fbef3be81ad4d964d235cb12141fb66727e6e5df73a878
, 0xebf66abb597ae572a7297cb0871e355accafad8377b8e78bf164ce2a18de4baf
, 0x71b933b07e4ff7818ce059d008829e453c6ff02ec0a7db393fc2d870f37a7286
, 0x7cf7c51331220b8d3ebaed9c29398a16d98156e2613cb088f2b0e08a1be4cf4f
, 0x3e41a108e0f64ad276b979e1ce068279e16f7bc7e4aa1d211e17b81161df1602
, 0x886502a82ab47ba8d86710aa9de3d46ea65c47af6ee8de450cceb8b11b045f50
, 0xc021bc5f0954fee94f46ea09487e10a84840d02f64810bc08d9e551f7d416814
, 0x2030516e8a5fe19ae79c336fce26382a749d3fd0ec91e537d4bd2358c12dfb22
, 0x556698dac8317fd36dfbdf25a79cb112d5425860605cbaf507f23bf7e9f42afe
, 0x2f867ba67773fdc3e92fced99a6409ad39d0b880fde8f109a81730c4451d0178
, 0x172ec218f119dfae98896dff29dd9876c94af87417f9ae4c7014bb4e4b96afc7
, 0x3f85814a18195f879aa962f95d26bd82a278f2b82320218f6b3bd6f7f667a6d9
, 0x1b618fbaa566b3d498c12e982c9ec52e4da85a8c54f38f34c090394f23c184c1
, 0x0c758fb5692ffd41a3575d0af00cc7fbf2cbe5905a58323a88ae4244f6e4c993
, 0xa931360cad628c7f12a6c1c4b753b0f4062aef3ce65a1ae3f19369dadf3ae23d
, 0xcbac7d773b1e3b3c6691d7abb7e9df045c8ba19268ded153207f5e804352ec5d
, 0x23a196d3802ed3c1b384019a82325840d32f71950c4580b03445e0898e14053c
, 0xf4495470f226c8c214be08fdfad4bc4a2a9dbea9136a210df0d4b64929e6fc14
, 0xe290dd270b467f34ab1c002d340fa016257ff19e5833fdbbf2cb401c3b2817de
, 0x9fc7b5ded3c15042b2a6582dc39be016d24a682d5e61ad1eff9c63309848f706
, 0x8cca67a36d17d5e6341cb592fd7bef9926c9e3aa1027ea11a7d8bd260b576e04
, 0x409392f560f86831da4373ee5e0074260595d7bc24183b60ed700d4583d3f6f0
, 0x2802165de090915546f3398cd849164a19f92adbc361adc99b0f20c8ea071054
, 0xad839168d9f8a4be95ba9ef9a692f07256ae43fe6f9864e290691b0256ce50a9
, 0x75fdaa5038c284b86d6e8affe8b2807e467b86600e79af3689fbc06328cbf894
, 0xe57cb79487dd57902432b250733813bd96a84efce59f650fac26e6696aefafc3
, 0x56f34e8b96557e90c1f24b52d0c89d51086acf1b00f634cf1dde9233b8eaaa3e
, 0x1b53ee94aaf34e4b159d48de352c7f0661d0a40edff95a0b1639b4090e974472
, 0x05705e2a81757c14bd383ea98dda544eb10e6bc07bae435e2518dbe133525375
, 0xd8b2866e8a309db53e529ec32911d82f5ca16cff76216891a9676aa31aaa6c42
, 0xf5041c241270eb04c71ec2c95d4c38d803b1237b0f29fd4db3eb397669e88699
, 0x9a4ce077c349322f595e0ee79ed0da5fab66752cbfef8f87d0e9d0723c7530dd
, 0x657b09f3d0f52b5b8f2f97163a0edf0c04f075408a07bbeb3a4101a891990d62
, 0x1e3f7bd5a58fa533344aa8ed3ac122bb9e70d4ef50d004530821948f5fe6315a
, 0x80dccf3fd83dfd0d35aa28585922ab89d5313997673eaf905cea9c0b225c7b5f
, 0x8a0d0fbf6377d83bb08b514b4b1c43acc95d751714f8925645cb6bc856ca150a
, 0x9fa5b487738ad2844cc6348a901918f659a3b89e9c0dfeead30dd94bcf42ef8e
, 0x80832c4a1677f5ea2560f668e9354dd36997f03728cfa55e1b38337c0c9ef818
, 0xab37ddb683137e74080d026b590b96ae9bb447722f305a5ac570ec1df9b1743c
, 0x3ee735a694c2559b693aa68629361e15d12265ad6a3dedf488b0b00fac9754ba
, 0xd6fcd23219b647e4cbd5eb2d0ad01ec8838a4b2901fc325cc3701981ca6c888b
, 0x0520ec2f5bf7a755dacb50c6bf233e3515434763db0139ccd9faefbb8207612d
, 0xaff3b75f3f581264d7661662b92f5ad37c1d32bd45ff81a4ed8adc9ef30dd989
, 0xd0dd650befd3ba63dc25102c627c921b9cbeb0b130686935b5c927cb7ccd5e3b
, 0xe1149816b10a8514fb3e2cab2c08bee9f73ce76221701246a589bbb67302d8a9
, 0x7da3f441de9054317e72b5dbf979da01e6bceebb8478eae6a22849d90292635c
, 0x1230b1fc8a7d9215edc2d4a2decbdd0a6e216c924278c91fc5d10e7d60192d94
, 0x5750d716b4808f751febc38806ba170bf6d5199a7816be514e3f932fbe0cb871
, 0x6fc59b2f10feba954aa6820b3ca987ee81d5cc1da3c63ce827301c569dfb39ce
, 0xc7c3fe1eebdc7b5a939326e8ddb83e8bf2b780b65678cb62f208b040abdd35e2
, 0x0c75c1a15cf34a314ee478f4a5ce0b8a6b36528ef7a820696c3e4246c5a15864
, 0x216dc12a108569a3c7cdde4aed43a6c330139dda3ccc4a108905db3861899050
, 0xa57be6ae6756f28b02f59dadf7e0d7d8807f10fa15ced1ad3585521a1d995a89
, 0x816aef875953716cd7a581f732f53dd435dab66d09c361d2d6592de17755d8a8
, 0x9a76893226693b6ea97e6a738f9d10fb3d0b43ae0e8b7d8123ea76ce97989c7e
, 0x8daedb9a271529dbb7dc3b607fe5eb2d3211770758dd3b0a3593d2d7954e2d5b
, 0x16dbc0aa5dd2c774f505100f733786d8a175fcbbb59c43e1fbff3e1eaf31cb4a
, 0x8606cb899c6aeaf51b9db0fe4924a9fd5dabc19f8826f2bc1c1d7da14d2c2c99
, 0x8479731aeda57bd37eadb51a507e307f3bd95e69dbca94f3bc21726066ad6dfd
, 0x58473a9ea82efa3f3b3d8fc83ed8863127b33ae8deae6307201edb6dde61de29
, 0x9a9255d53af116de8ba27ce35b4c7e15640657a0fcb888c70d95431dacd8f830
, 0x9eb05ffba39fd8596a45493e18d2510bf3ef065c51d6e13abe66aa57e05cfdb7
, 0x81dcc3a505eace3f879d8f702776770f9df50e521d1428a85daf04f9ad2150e0
, 0xe3e3c4aa3acbbc85332af9d564bc24165e1687f6b1adcbfae77a8f03c72ac28c
, 0x6746c80b4eb56aea45e64e7289bba3edbf45ecf8206481ff6302122984cd526a
, 0x2b628e52764d7d62c0868b212357cdd12d9149822f4e9845d918a08d1ae990c0
, 0xe4bfe80d58c91994613909dc4b1a12496896c004af7b5701483de45d2823d78e
, 0xebb4ba150cef2734345b5d641bbed03a21eafae933c99e009212ef04574a8530
, 0x3966ec73b154acc697ac5cf5b24b40bdb0db9e398836d76d4b880e3b2af1aa27
, 0xef7e4831b3a84636518d6e4bfce64a43db2a5dda9cca2b44f39033bdc40d6243
, 0x7abf6acf5c8e549ddbb15ae8d8b388c1c197e698737c9785501ed1f94930b7d9
, 0x88018ded66813f0ca95def474c630692019967b9e36888dadd94124719b682f6
, 0x3930876b9fc7529036b008b1b8bb997522a441635a0c25ec02fb6d9026e55a97
, 0x0a4049d57e833b5695fac93dd1fbef3166b44b12ad11248662383ae051e15827
, 0x81dcc0678bb6a765e48c3209654fe90089ce44ff5618477e39ab286476df052b
, 0xe69b3a36a4461912dc08346b11ddcb9db796f885fd01936e662fe29297b099a4
, 0x5ac6503b0d8da6917646e6dcc87edc58e94245324cc204f4dd4af01563acd427
, 0xdf6dda21359a30bc271780971c1abd56a6ef167e480887888e73a86d3bf605e9
, 0xe8e6e47071e7b7df2580f225cfbbedf84ce67746626628d33097e4b7dc571107
, 0x53e40ead62051e19cb9ba8133e3e5c1ce00ddcad8acf342a224360b0acc14777
, 0x9ccd53fe80be786aa984638462fb28afdf122b34d78f4687ec632bb19de2371a
, 0xcbd48052c48d788466a3e8118c56c97fe146e5546faaf93e2bc3c47e45939753
, 0x256883b14e2af44dadb28e1b34b2ac0f0f4c91c34ec9169e29036158acaa95b9
, 0x4471b91ab42db7c4dd8490ab95a2ee8d04e3ef5c3d6fc71ac74b2b26914d1641
, 0xa5eb08038f8f1155ed86e631906fc13095f6bba41de5d4e795758ec8c8df8af1
, 0xdc1db64ed8b48a910e060a6b866374c578784e9ac49ab2774092ac71501934ac
, 0x285413b2f2ee873d34319ee0bbfbb90f32da434cc87e3db5ed121bb398ed964b
, 0x0216e0f81f750f26f1998bc3934e3e124c9945e685a60b25e8fbd9625ab6b599
, 0x38c410f5b9d4072050755b31dca89fd5395c6785eeb3d790f320ff941c5a93bf
, 0xf18417b39d617ab1c18fdf91ebd0fc6d5516bb34cf39364037bce81fa04cecb1
, 0x1fa877de67259d19863a2a34bcc6962a2b25fcbf5cbecd7ede8f1fa36688a796
, 0x5bd169e67c82c2c2e98ef7008bdf261f2ddf30b1c00f9e7f275bb3e8a28dc9a2
, 0xc80abeebb669ad5deeb5f5ec8ea6b7a05ddf7d31ec4c0a2ee20b0b98caec6746
, 0xe76d3fbda5ba374e6bf8e50fadc3bbb9ba5c206ebdec89a3a54cf3dd84a07016
, 0x7bba9dc5b5db2071d17752b1044c1eced96aaf2dd46e9b433750e8ea0dcc1870
, 0xf29b1b1ab9bab163018ee3da15232cca78ec52dbc34eda5b822ec1d80fc21bd0
, 0x9ee3e3e7e900f1e11d308c4b2b3076d272cf70124f9f51e1da60f37846cdd2f4
, 0x70ea3b0176927d9096a18508cd123a290325920a9d00a89b5de04273fbc76b85
, 0x67de25c02a4aaba23bdc973c8bb0b5796d47cc0659d43dff1f97de174963b68e
, 0xb2168e4e0f18b0e64100b517ed95257d73f0620df885c13d2ecf79367b384cee
, 0x2e7dec2428853b2c71760745541f7afe9825b5dd77df06511d8441a94bacc927
, 0xca9ffac4c43f0b48461dc5c263bea3f6f00611ceacabf6f895ba2b0101dbb68d
, 0x7410d42d8fd1d5e9d2f5815cb93417998828ef3c4230bfbd412df0a4a7a2507a
, 0x5010f684516dccd0b6ee0852c2512b4dc0066cf0d56f35302978db8ae32c6a81
, 0xacaab585f7b79b719935ceb89523ddc54827f75c56883856154a56cdcd5ee988
, 0x666de5d1440fee7331aaf0123a62ef2d8ba57453a0769635ac6cd01e633f7712
, 0xa6f98658f6eabaf902d8b3871a4b101d16196e8a4b241e1558fe29966e103e8d
, 0x891546a8b29f3047ddcfe5b00e45fd55756373105ea8637dfcff547b6ea9535f
, 0x18dfbc1ac5d25b0761137dbd22c17c829d0f0ef1d82344e9c89c286694da24e8
, 0xb54b9b67f8fed54bbf5a2666dbdf4b23cff1d1b6f4afc985b2e6d3305a9ff80f
, 0x7db442e132ba59bc1289aa98b0d3e806004f8ec12811af1e2e33c69bfde729e1
, 0x250f37cdc15e817d2f160d9956c71fe3eb5db74556e4adf9a4ffafba74010396
, 0x4ab8a3dd1ddf8ad43dab13a27f66a6544f290597fa96040e0e1db9263aa479f8
, 0xee61727a0766df939ccdc860334044c79a3c9b156200bc3aa32973483d8341ae
, 0x3f68c7ec63ac11ebb98f94b339b05c104984fda50103060144e5a2bfccc9da95
, 0x056f29816b8af8f56682bc4d7cf094111da7733e726cd13d6b3e8ea03e92a0d5
, 0xf5ec43a28acbeff1f3318a5bcac7c66ddb5230b79db2d105bcbe15f3c1148d69
, 0x2a6960ad1d8dd547555cfbd5e4600f1eaa1c8eda34de0374ec4a26eaaaa33b4e
, 0xdcc1ea7baab93384f76b796866199754742f7b96d6b4c120165c04a6c4f5ce10
, 0x13d5df179221379c6a78c07c793ff53487cae6bf9fe882541ab0e735e3eada3b
, 0x8c59e4407641a01e8ff91f9980dc236f4ecd6fcf52589a099a961633967714e1
, 0x833b1ac6a251fd08fd6d908fea2a4ee1e040bca93fc1a38ec3820e0c10bd82ea
, 0xa244f927f3b40b8f6c391570c765418f2f6e708eac9006c51a7feff4af3b2b9e
, 0x3d99ed9550cf1196e6c4d20c259620f858c3d703374c128ce7b590310c83046d
, 0x2b35c47d7b87761f0ae43ac56ac27b9f25830367b595be8c240e94600c6e3312
, 0x5d11ed37d24dc767305cb7e1467d87c065ac4bc8a426de38991ff59aa8735d02
, 0xb836478e1ca0640dce6fd910a5096272c8330990cd97864ac2bf14ef6b23914a
, 0x9100f946d6ccde3a597f90d39fc1215baddc7413643d85c21c3eee5d2dd32894
, 0xda70eedd23e663aa1a74b9766935b479222a72afba5c795158dad41a3bd77e40
, 0xf067ed6a0dbd43aa0a9254e69fd66bdd8acb87de936c258cfb02285f2c11fa79
, 0x715c99c7d57580cf9753b4c1d795e45a83fbb228c0d36fbe20faf39bdd6d4e85
, 0xe457d6ad1e67cb9bbd17cbd698fa6d7dae0c9b7ad6cbd6539634e32a719c8492
, 0xece3ea8103e02483c64a70a4bdcee8ceb6278f2533f3f48dbeedfba94531d4ae
, 0x388aa5d3667a97c68d3d56f8f3ee8d3d36091f17fe5d1b0d5d84c93b2ffe40bd
, 0x8b6b31b9ad7c3d5cd84bf98947b9cdb59df8a25ff738101013be4fd65e1dd1a3
, 0x066291f6bbd25f3c853db7d8b95c9a1cfb9bf1c1c99fb95a9b7869d90f1c2903
, 0xa707efbccdceed42967a66f5539b93ed7560d467304016c4780d7755a565d4c4
, 0x38c53dfb70be7e792b07a6a35b8a6a0aba02c5c5f38baf5c823fdfd9e42d657e
, 0xf2911386501d9ab9d720cf8ad10503d5634bf4b7d12b56dfb74fecc6e4093f68
, 0xc6f2bdd52b81e6e4f6595abd4d7fb31f651169d00ff326926b34947b28a83959
, 0x293d94b18c98bb3223366b8ce74c28fbdf28e1f84a3350b0eb2d1804a577579b
, 0x2c2fa5c0b51533165bc375c22e2781768270a383985d13bd6b67b6fd67f889eb
, 0xcaa09b82b72562e43f4b2275c091918e624d911661cc811bb5faec51f6088ef7
, 0x24761e45e674395379fb17729c78cb939e6f74c5dffb9c961f495982c3ed1fe3
, 0x55b70a82131ec94888d7ab54a7c515255c3938bb10bc784dc9b67f076e341a73
, 0x6ab9057b977ebc3ca4d4ce74506c25cccdc566497c450b5415a39486f8657a03
, 0x24066deee0ecee15a45f0a326d0f8dbc79761ebb93cf8c0377af440978fcf994
, 0x20000d3f66ba76860d5a950688b9aa0d76cfea59b005d859914b1a46653a939b
, 0xb92daa79603e3bdbc3bfe0f419e409b2ea10dc435beefe2959da16895d5dca1c
, 0xe947948705b206d572b0e8f62f66a6551cbd6bc305d26ce7539a12f9aadf7571
, 0x3d67c1b3f9b23910e3d35e6b0f2ccf44a0b540a45c18ba3c36264dd48e96af6a
, 0xc7558babda04bccb764d0bbf3358425141902d22391d9f8c59159fec9e49b151
, 0x0b732bb035675a50ff58f2c242e4710aece64670079c13044c79c9b7491f7000
, 0xd120b5ef6d57ebf06eaf96bc933c967b16cbe6e2bf00741c30aa1c54ba64801f
, 0x58d212ad6f58aef0f80116b441e57f6195bfef26b61463edec1183cdb04fe76d
, 0xb8836f51d1e29bdfdba325565360268b8fad627473edecef7eaefee837c74003
, 0xc547a3c124ae5685ffa7b8edaf96ec86f8b2d0d50cee8be3b1f0c76763069d9c
, 0x5d168b769a2f67853d6295f7568be40bb7a16b8d65ba87635d1978d2ab11ba2a
, 0xa2f675dc7302638cb60201064ca55077714d71fe096a315f2fe7401277caa5af
, 0xc8aab5cd0160ae78cd2e8ac5fb0e093cdb5c4b6052a0a97bb04216826fa7a437
, 0xff68ca4035bfeb43fbf145fddd5e43f1cea54f11f7bee13058f027329a4a5fa4
, 0x1d4e5487ae3c740f2ba6e541ac91bc2bfcd2999c518d807b426748803a350fd4
, 0x6d244e1a06ce4ef578dd0f63aff0936706735119ca9c8d22d86c801414ab9741
, 0xdecf7329dbcc827b8fc524c9431e8998029ece12ce93b7b2f3e769a941fb8cea
, 0x2fafcc0f2e63cbd07755be7b75ecea0adff9aa5ede2a52fdab4dfd0374cd483f
, 0xaa85010dd46a546b535ef4cf5f07d65161e89828f3a77db7b9b56f0df59aae45
, 0x07e8e1ee732cb0d356c9c0d1069c89d17adf6a9a334f745ec7867332548ca8e9
, 0x0e01e81cada8162bfd5f8a8c818a6c69fedf02ceb5208523cbe5313b89ca1053
, 0x6bb6c6472655084399852e00249f8cb247896d392b02d73b7f0dd818e1e29b07
, 0x42d4636e2060f08f41c882e76b396b112ef627cc24c43dd5f83a1d1a7ead711a
, 0x4858c9a188b0234fb9a8d47d0b4133650a030bd0611b87c3892e94951f8df852
, 0x3fab3e36988d445a51c8783e531be3a02be40cd04796cfb61d40347442d3f794
, 0xebabc49636bd433d2ec8f0e518732ef8fa21d4d071cc3bc46cd79fa38a28b810
, 0xa1d0343523b893fca84f47feb4a64d350a17d8eef5497ece697d02d79178b591
, 0x262ebfd9130b7d28760d08ef8bfd3b86cdd3b2113d2caef7ea951a303dfa3846
, 0xf76158edd50a154fa78203ed2362932fcb8253aae378903eded1e03f7021a257
, 0x26178e950ac722f67ae56e571b284c0207684a6334a17748a94d260bc5f55274
, 0xc378d1e493b40ef11fe6a15d9c2737a37809634c5abad5b33d7e393b4ae05d03
, 0x984bd8379101be8fd80612d8ea2959a7865ec9718523550107ae3938df32011b
, 0xc6f25a812a144858ac5ced37a93a9f4759ba0b1c0fdc431dce35f9ec1f1f4a99
, 0x924c75c94424ff75e74b8b4e94358958b027b171df5e57899ad0d4dac37353b6
, 0x0af35892a63f45931f6846ed190361cd073089e077165714b50b81a2e3dd9ba1
, 0xcc80cefb26c3b2b0daef233e606d5ffc80fa17427d18e30489673e06ef4b87f7
, 0xc2f8c8117447f3978b0818dcf6f70116ac56fd184dd1278494e103fc6d74a887
, 0xbdecf6bfc1ba0df6e862c831992207796acc797968358828c06e7a51e090098f
, 0x24d1a26e3dab02fe4572d2aa7dbd3ec30f0693db26f273d0ab2cb0c13b5e6451
, 0xec56f58b09299a300b140565d7d3e68782b6e2fbeb4b7ea97ac057989061dd3f
, 0x11a437c1aba3c119ddfab31b3e8c841deeeb913ef57f7e48f2c9cf5a28fa42bc
, 0x53c7e6114b850a2cb496c9b3c69a623eaea2cb1d33dd817e4765edaa6823c228
, 0x154c3e96fee5db14f8773e18af14857913509da999b46cdd3d4c169760c83ad2
, 0x40b9916f093e027a8786641818920620472fbcf68f701d1b680632e6996bded3
, 0x24c4cbba07119831a726b05305d96da02ff8b148f0da440fe233bcaa32c72f6f
, 0x5d201510250020b783689688abbf8ecf2594a96a08f2bfec6ce0574465dded71
, 0x043b97e336ee6fdbbe2b50f22af83275a4084805d2d5645962454b6c9b8053a0
, 0x564835cbaea774948568be36cf52fcdd83934eb0a27512dbe3e2db47b9e6635a
, 0xf21c33f47bde40a2a101c9cde8027aaf61a3137de2422b30035a04c270894183
, 0x9db0ef74e66cbb842eb0e07343a03c5c567e372b3f23b943c788a4f250f67891
, 0xab8d08655ff1d3fe8758d562235fd23e7cf9dcaad658872a49e5d3183b6ccebd
, 0x6f27f77e7bcf46a1e963ade0309733543031dccdd47caac174d7d27ce8077e8b
, 0xe3cd54da7e444caa6207569525a670ebae1278de4e3fe2684b3e33f5ef90cc1b
, 0xb2c3e33a51d22c4c08fc0989c873c9cc4150579b1e6163fa694ad51d53d712dc
, 0xbe7fda983e13189b4c77e0a80920b6e0e0ea80c3b84dbe7e7117d253f48112f4
, 0xb6008c28fae08aa427e5bd3aad36f10021f16c77cfeabed07f97cc7dc1f1284a
, 0x6e4e6760c538f2e97b3adbfbbcde57f8966b7ea8fcb5bf7efec913fd2a2b0c55
, 0x4ae51fd1834aa5bd9a6f7ec39fc663338dc5d2e20761566d90cc68b1cb875ed8
, 0xb673aad75ab1fdb5401abfa1bf89f3add2ebc468df3624a478f4fe859d8d55e2
, 0x13c9471a9855913539836660398da0f3f99ada08479c69d1b7fcaa3461dd7e59
, 0x2c11f4a7f99a1d23a58bb636350fe849f29cbac1b2a1112d9f1ed5bc5b313ccd
, 0xc7d3c0706b11ae741c05a1ef150dd65b5494d6d54c9a86e2617854e6aeeebbd9
, 0x194e10c93893afa064c3ac04c0dd808d791c3d4b7556e89d8d9cb225c4b33339
, 0x6fc4988b8f78546b1688991845908f134b6a482e6994b3d48317bf08db292185
, 0x5665beb8b0955525813b5981cd142ed4d03fba38a6f3e5ad268e0cc270d1cd11
, 0xb883d68f5fe51936431ba4256738053b1d0426d4cb64b16e83badc5e9fbe3b81
, 0x53e7b27ea59c2f6dbb50769e43554df35af89f4822d0466b007dd6f6deafff02
, 0x1f1a0229d4640f01901588d9dec22d13fc3eb34a61b32938efbf5334b2800afa
, 0xc2b405afa0fa6668852aee4d88040853fab800e72b57581418e5506f214c7d1f
, 0xc08aa1c286d709fdc7473744977188c895ba011014247e4efa8d07e78fec695c
, 0xf03f5789d3336b80d002d59fdf918bdb775b00956ed5528e86aa994acb38fe2d
]

1071
examples/MiniLock/prim/CfrgCurves.md Normal file
View File

File diff suppressed because it is too large Load Diff

61
examples/MiniLock/prim/CryptoBox.cry Normal file
View File

@ -0,0 +1,61 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module CryptoBox where
import Salsa20
import Poly1305
import CfrgCurves
crypto_box : {msgBytes} (fin msgBytes, 2^^64 >= msgBytes + 32) => [msgBytes][8] -> [24][8] -> Public25519 -> Private25519 -> [msgBytes + 16][8]
crypto_box m n pub priv = crypto_secretbox m k n
where
s = Curve25519 priv pub
k = HSalsa20_bytes `{r=20} s zero
crypto_box_open : {msgBytes} (fin msgBytes, 2^^64 >= msgBytes + 32) => [msgBytes+16][8] -> [24][8] -> Public25519 -> Private25519 -> (Bit,[msgBytes][8])
crypto_box_open box n pub priv = crypto_secretbox_open box k n
where
(tag,ct) = splitAt `{16} box
s = Curve25519 priv pub
k = HSalsa20_bytes `{r=20} s zero
crypto_secretbox : {msgBytes} (fin msgBytes, 2^^64 >= msgBytes + 32)
=> [msgBytes][8] -> [32][8] -> [24][8] -> [msgBytes + 16][8]
crypto_secretbox m k n = box
where
blob = XSalsa20_encrypt `{r=20} k n ((zero : [32][8]) # m)
authKey = join (take `{32} blob)
ciphertext = drop `{32} blob
authTag = Poly1305 authKey ciphertext
box = authTag # ciphertext
crypto_secretbox_open : {msgBytes} (fin msgBytes, 2^^64 >= msgBytes + 32)
=> [msgBytes + 16][8] -> [32][8] -> [24][8] -> (Bit,[msgBytes][8])
crypto_secretbox_open box k n = (valid,pt)
where
(tag,ct) = splitAt `{16} box
blob = XSalsa20_encrypt `{r=20} k n ((zero : [32][8]) # ct)
authKey = join (take `{32} blob)
plaintext = drop blob : [msgBytes][8]
cTag = Poly1305 authKey ct
valid = cTag == tag
pt = if valid then plaintext else zero
property cat_in_a_box priv1 priv2 msg nonce = open == msg
where pub1 = Curve25519 priv1 basePoint25519
pub2 = Curve25519 priv2 basePoint25519
box = crypto_box (msg : [100][8]) nonce pub2 priv1
open = (crypto_box_open box nonce pub1 priv2).1
property hat_in_a_box k msg nonce = open == msg
where box = crypto_secretbox (msg : [88][8]) k nonce
open = (crypto_secretbox_open box k nonce).1
property crypto_box_kats = zero != [ katTest1 ]
// KAT generated from sodium
katTest1 = crypto_secretbox "hello" zero zero == split 0xc769f9d535dc338e99ac93440502c7ceae5bd79391

58
examples/MiniLock/prim/HMAC.cry Normal file
View File

@ -0,0 +1,58 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module HMAC where
import SHA256
hmacSHA256 : {pwBytes, msgBytes}
(fin pwBytes, fin msgBytes
, 32 >= width msgBytes
, 64 >= width (8*pwBytes)
, 64 >= width (8 * (64 + msgBytes))
// Keeping cryptol <2.3 happy
, max 6 (width pwBytes) >= 6
, max 6 (width pwBytes) >= width pwBytes
, max 7 (width pwBytes) >= 7
, max 7 (width pwBytes) >= width pwBytes
, max (width pwBytes) 7 >= 7
, max (width pwBytes) 7 >= width pwBytes
) => [pwBytes][8] -> [msgBytes][8] -> [256]
hmacSHA256 = hmac `{blockLength=64} SHA256 SHA256 SHA256
// Due to limitations of the type system we must accept two
// separate arguments (both aledgedly the same) for two
// separate length inputs.
hmac : { msgBytes, pwBytes, digest, blockLength }
( fin pwBytes, fin digest, fin blockLength
// Keeping cryptol <2.3 happy
, max (width digest) (width pwBytes) >= width pwBytes // XXX cryptol! width digest == width pwBytes
, max (width digest) (width pwBytes) >= width digest
, max (width blockLength) (width pwBytes) >= width blockLength
, max (width blockLength) (width pwBytes) >= width pwBytes
, max (width pwBytes) (width blockLength) >= width blockLength
, max (width pwBytes) (width blockLength) >= width pwBytes
)
=> ([blockLength + msgBytes][8] -> [8*digest])
-> ([blockLength + digest][8] -> [8*digest])
-> ([pwBytes][8] -> [8*digest])
-> [pwBytes][8]
-> [msgBytes][8]
-> [digest*8]
hmac hash hash2 hash3 key message = hash2 (okey # internal)
where
ks : [blockLength][8]
ks = if `pwBytes > (`blockLength : [max (width pwBytes) (width blockLength)])
then take `{blockLength} (split (hash3 key) # (zero : [blockLength][8]))
else take `{blockLength} (key # (zero : [blockLength][8]))
okey = [k ^ 0x5C | k <- ks]
ikey = [k ^ 0x36 | k <- ks]
internal = split (hash (ikey # message))
property pass =
~zero ==
[ hmacSHA256 [0x0b | _ <- [1..20] : [_][6]] "Hi There" == 0xb0344c61d8db38535ca8afceaf0bf12b881dc200c9833da726e9376c2e32cff7
, hmacSHA256 "Jefe" "what do ya want for nothing?" == 0x5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843
]

21
examples/MiniLock/prim/LittleEndian.cry Normal file
View File

@ -0,0 +1,21 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module LittleEndian where
// Takes a finite sequence of bytes, and turns them into a word via
// a little-endian interpretation
littleendian : {a}(fin a) => [a][8] -> [a*8]
littleendian b = join(reverse b)
property littleendian_passes_tests =
(littleendian [ 0, 0, 0, 0] == 0x00000000) &&
(littleendian [ 86, 75, 30, 9] == 0x091e4b56) &&
(littleendian [255, 255, 255, 250] == 0xfaffffff)
littleendian_inverse : [32] -> [4][8]
littleendian_inverse b = reverse(split b)
property littleendian_is_invertable b = littleendian_inverse(littleendian b) == b

73
examples/MiniLock/prim/PBKDF2.cry Normal file
View File

@ -0,0 +1,73 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module PBKDF2 where
import SHA256
import HMAC
// PBKDF2 specialized to HMAC_SHA256 to avoid monomorphic type issues.
pbkdf2 : {pwBytes, saltBytes, dkLenBits, len, C}
( 32 >= width (pwBytes*8), len == (dkLenBits + 255)/256
, len >= 1, 32 >= width len, fin saltBytes, fin dkLenBits, fin pwBytes
, 64 >= width (8 * (pwBytes + (4 + saltBytes)))
, 64 >= width (8 * (pwBytes + 32))
, C >= 1, fin C, 64 >= width (8*(pwBytes + (2 + saltBytes))), 16 >= width C
, 16 >= width len
// cryptol < 2.3 can't math!
, dkLenBits == 256 * len // Cryptol 2.3 doesn't understand 'take'?
, max 6 (width pwBytes) >= width pwBytes
, max 6 (width pwBytes) >= 6
, max 7 (width pwBytes) >= 7
, max 7 (width pwBytes) >= width pwBytes
, max (width pwBytes) 7 >= 7
, max (width pwBytes) 7 >= width pwBytes
, 64 >= width (8 * pwBytes)
, 64 >= width (8 * (68 + saltBytes))
, 32 >= width (4 + saltBytes)
)
=> [pwBytes][8] -> [saltBytes][8] -> [dkLenBits]
pbkdf2 P S = take `{dkLenBits} (join Ts)
where
Ts : [_][256]
Ts = [ inner `{C=C} P (split (hmacSHA256 P (S # split i))) | i <- [1..len] : [_][32] ]
inner : {pwBytes, C}
( fin pwBytes
, 64 >= width (8 * (pwBytes + 32))
, fin C, C >= 1, 16 >= width C
// Cryptol < 2.3 can't math
, 64 >= width (8 * pwBytes)
, max 7 (width pwBytes) >= width pwBytes
, max 7 (width pwBytes) >= 7
, max (width pwBytes) 7 >= width pwBytes
, max (width pwBytes) 7 >= 7
, max 6 (width pwBytes) >= width pwBytes
, max 6 (width pwBytes) >= 6
)
=> [pwBytes][8] -> [32][8] -> [256]
inner P U0 = (Ts @ 0).0 // XXX should be ! 0
where
// Ts : [_][([256],[32][8])]
Ts = [(join U0, U0)] # [ F P t u | _ <- [1..C] : [_][16] | (t,u) <- Ts ]
F : {pwBytes} (fin pwBytes
, 64 >= width (8*(32+pwBytes))
// cryptol < 2.3 can't math
, 64 >= width (8 * pwBytes)
, max 7 (width pwBytes) >= width pwBytes
, max 7 (width pwBytes) >= 7
, max (width pwBytes) 7 >= width pwBytes
, max (width pwBytes) 7 >= 7
, max 6 (width pwBytes) >= width pwBytes
, max 6 (width pwBytes) >= 6
) => [pwBytes][8] -> [256] -> [32][8] -> ([256],[32][8])
F P Tprev Uprev = (Tnext,Unext)
where
Unext = split (hmacSHA256 P Uprev)
Tnext = Tprev ^ join Unext
test1 : Bit
property test1 = pbkdf2 `{C=1,dkLenBits=64*8} "passwd" "salt" == 0x55ac046e56e3089fec1691c22544b605f94185216dde0465e68b9d57c20dacbc49ca9cccf179b645991664b39d77ef317c71b845b1e30bd509112041d3a19783

686
examples/MiniLock/prim/Poly1305.md Normal file
View File

@ -0,0 +1,686 @@
% Poly1305 for IETF protocols
% Y. Nir (Check Point), A. Langley (Google Inc), D. McNamee (Galois, Inc)
% July 28, 2014
%
% Poly1305 extracted from the original RFC by Thomas DuBuisson
```cryptol
module Poly1305 where
```
# The Poly1305 algorithm
Poly1305 is a one-time authenticator designed by D. J. Bernstein.
Poly1305 takes a 32-byte one-time key and a message and produces a
16-byte tag.
The original article ([poly1305]) is entitled "The Poly1305-AES
message-authentication code", and the MAC function there requires a
128-bit AES key, a 128-bit "additional key", and a 128-bit (non-
secret) nonce. AES is used there for encrypting the nonce, so as to
get a unique (and secret) 128-bit string, but as the paper states,
"There is nothing special about AES here. One can replace AES with
an arbitrary keyed function from an arbitrary set of nonces to 16-
byte strings."
Regardless of how the key is generated, the key is partitioned into
two parts, called "r" and "s". The pair ``(r,s)`` should be unique, and
MUST be unpredictable for each invocation (that is why it was
originally obtained by encrypting a nonce), while "r" MAY be
constant, but needs to be modified as follows before being used: ("r"
is treated as a 16-octet little-endian number):
* r[3], r[7], r[11], and r[15] are required to have their top four
bits clear (be smaller than 16)
```cryptol
Om = 15 // odd masks - for 3, 7, 11 & 15
```
* r[4], r[8], and r[12] are required to have their bottom two bits
clear (be divisible by 4)
The following Cryptol code clamps "r" to be appropriate:
```cryptol
Em = 252 // even masks - for 4, 8 & 12
nm = 255 // no mask
PolyMasks : [16][8] // mask indices
PolyMasks = [ nm, nm, nm, Om, // 0-3
Em, nm, nm, Om, // 4-7
Em, nm, nm, Om, // 8-11
Em, nm, nm, Om ] // 12-15
Poly1305_clamp : [16][8] -> [16][8]
Poly1305_clamp r = [ re && mask | re <- r | mask <- PolyMasks ]
```
The "s" should be unpredictable, but it is perfectly acceptable to
generate both "r" and "s" uniquely each time. Because each of them
is 128-bit, pseudo-randomly generating them (see "Generating the
Poly1305 key using ChaCha20") is also acceptable.
The inputs to Poly1305 are:
* A 256-bit one-time key
* An arbitrary length message (comprised of `floorBlocks` 16-byte blocks,
and `rem` bytes left over)
The output is a 128-bit tag.
```cryptol
Poly1305 : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16)
=> [256] -> [m][8] -> [16][8]
```
Set the constant prime "P" be 2^130-5.
```cryptol
P : [136]
P = 2^^130 - 5
```
First, the "r" value should be clamped.
```cryptol
Poly1305 key msg = result where
[ru, su] = split key
r : [136] // internal arithmetic on (128+8)-bit numbers
r = littleendian ((Poly1305_clamp (split ru)) # [0x00])
s = littleendian ((split su) # [0x00])
```
Next, divide the message into 16-byte blocks. The last block might be shorter:
* Read each block as a little-endian number.
* Add one bit beyond the number of octets. For a 16-byte block this
is equivalent to adding 2^128 to the number. For the shorter
block it can be 2^120, 2^112, or any power of two that is evenly
divisible by 8, all the way down to 2^8.
```cryptol
// pad all the blocks uniformly (we'll handle the final block later)
paddedBlocks = [ 0x01 # (littleendian block)
| block <- groupBy`{16}(msg # (zero:[inf][8])) ]
```
* If the block is not 17 bytes long (the last block), then left-pad it with
zeros. This is meaningless if you're treating them as numbers.
```cryptol
lastBlock : [136]
lastBlock = zero # 0x01 # (littleendian (drop`{16*floorBlocks} msg))
```
* Add the current block to the accumulator.
* Multiply by "r"
* Set the accumulator to the result modulo p. To summarize:
``accum[i+1] = ((accum[i]+block)*r) % p``.
```cryptol
accum:[_][136]
accum = [zero:[136]] # [ computeElt a b r P | a <- accum | b <- paddedBlocks ]
// ^ the accumulator starts at zero
```
* If the block division leaves no remainder, the last value of the accumulator is good
otherwise compute the special-case padded block, and compute the final value of the accumulator
```cryptol
lastAccum : [136]
lastAccum = if `rem == 0
then accum@`floorBlocks
else computeElt (accum@`floorBlocks) lastBlock r P
```
Finally, the value of the secret key "s" is added to the accumulator,
and the 128 least significant bits are serialized in little-endian
order to form the tag.
```cryptol
result = reverse (groupBy`{8} (drop`{8}(lastAccum + s)))
// Compute ((a + b) * r ) % P being pedantic about bit-widths
computeElt : [136] -> [136] -> [136] -> [136] -> [136]
computeElt a b r p = (drop`{137}bigResult) where
bigResult : [273]
aPlusB : [137]
aPlusB = (0b0#a) + (0b0#b) // make room for carry
timesR : [273]
timesR = ((zero:[136])#aPlusB) * ((zero:[137])#r) // [a]*[b]=[a+b]
bigResult = timesR % ((zero:[137])#p)
```
### Poly1305 Example and Test Vector
For our example, we will dispense with generating the one-time key
using AES, and assume that we got the following keying material:
* Key Material: 85:d6:be:78:57:55:6d:33:7f:44:52:fe:42:d5:06:a8:01:
03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b
```cryptol
Poly1305TestKey = join (parseHexString
( "85:d6:be:78:57:55:6d:33:7f:44:52:fe:42:d5:06:a8:01:"
# "03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b."
) )
```
* s as an octet string: 01:03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b
* s as a 128-bit number: 1bf54941aff6bf4afdb20dfb8a800301
```cryptol
Poly1305Test_s = parseHexString
"01:03:80:8a:fb:0d:b2:fd:4a:bf:f6:af:41:49:f5:1b."
Poly1305Test_sbits = join (reverse Poly1305Test_s)
property poly1306Sokay = Poly1305Test_sbits == 0x1bf54941aff6bf4afdb20dfb8a800301
```
```cryptol
Poly1305TestMessage = "Cryptographic Forum Research Group"
```
* r before clamping: 85:d6:be:78:57:55:6d:33:7f:44:52:fe:42:d5:06:a8
* Clamped r as a number: 806d5400e52447c036d555408bed685.
Since Poly1305 works in 16-byte chunks, the 34-byte message divides
into 3 blocks. In the following calculation, "Acc" denotes the
accumulator and "Block" the current block:
Here we define a Cryptol function that returns all of the intermediate
values of the accumulator:
```cryptol
// TODO: refactor the Poly function in terms of this AccumBlocks
// challenge: doing so while maintaining the clean literate correspondence with the spec
AccumBlocks : {m, floorBlocks, rem} (fin m, floorBlocks == m/16, rem == m - floorBlocks*16)
=> [256] -> [m][8] -> ([_][136], [136])
AccumBlocks key msg = (accum, lastAccum) where
[ru, su] = split key
r : [136] // internal arithmetic on (128+8)-bit numbers
r = littleendian ((Poly1305_clamp (split ru)) # [0x00])
s = littleendian ((split su) # [0x00])
// pad all the blocks uniformly (we'll handle the final block later)
paddedBlocks = [ 0x01 # (littleendian block)
| block <- groupBy`{16}(msg # (zero:[inf][8])) ]
lastBlock : [136]
lastBlock = zero # 0x01 # (littleendian (drop`{16*floorBlocks} msg))
accum:[_][136]
accum = [zero:[136]] # [ computeElt a b r P | a <- accum | b <- paddedBlocks ]
// ^ the accumulator starts at zero
lastAccum : [136]
lastAccum = if `rem == 0
then accum@`floorBlocks
else computeElt (accum@`floorBlocks) lastBlock r P
```
```example
Block #1
Acc = 00
Block = 6f4620636968706172676f7470797243
Block with 0x01 byte = 016f4620636968706172676f7470797243
Acc + block = 016f4620636968706172676f7470797243
(Acc+Block) * r =
b83fe991ca66800489155dcd69e8426ba2779453994ac90ed284034da565ecf
Acc = ((Acc+Block)*r) % P = 2c88c77849d64ae9147ddeb88e69c83fc
Block #2
Acc = 2c88c77849d64ae9147ddeb88e69c83fc
Block = 6f7247206863726165736552206d7572
Block with 0x01 byte = 016f7247206863726165736552206d7572
Acc + block = 437febea505c820f2ad5150db0709f96e
(Acc+Block) * r =
21dcc992d0c659ba4036f65bb7f88562ae59b32c2b3b8f7efc8b00f78e548a26
Acc = ((Acc+Block)*r) % P = 2d8adaf23b0337fa7cccfb4ea344b30de
Last Block
Acc = 2d8adaf23b0337fa7cccfb4ea344b30de
Block = 7075
Block with 0x01 byte = 017075
Acc + block = 2d8adaf23b0337fa7cccfb4ea344ca153
(Acc + Block) * r =
16d8e08a0f3fe1de4fe4a15486aca7a270a29f1e6c849221e4a6798b8e45321f
((Acc + Block) * r) % P = 28d31b7caff946c77c8844335369d03a7
```
```cryptol
property polyBlocksOK =
(blocks @ 1 == 0x02c88c77849d64ae9147ddeb88e69c83fc) &&
(blocks @ 2 == 0x02d8adaf23b0337fa7cccfb4ea344b30de) &&
(lastBlock == 0x028d31b7caff946c77c8844335369d03a7) where
(blocks, lastBlock) = AccumBlocks Poly1305TestKey Poly1305TestMessage
```
Adding s we get this number, and serialize if to get the tag:
Acc + s = 2a927010caf8b2bc2c6365130c11d06a8
Tag: a8:06:1d:c1:30:51:36:c6:c2:2b:8b:af:0c:01:27:a9
```cryptol
// Putting it all together and testing:
Poly1305TestTag = "a8:06:1d:c1:30:51:36:c6:c2:2b:8b:af:0c:01:27:a9."
property Poly1305_passes_test = Poly1305 Poly1305TestKey Poly1305TestMessage ==
parseHexString Poly1305TestTag
```
## Generating the Poly1305 key using ChaCha20
As said in the "Poly 1305 Algorithm" section, it is acceptable to generate
the one-time Poly1305 pseudo-randomly. This section proposes such a method.
To generate such a key pair (r,s), we will use the ChaCha20 block
function described in Section 2.3. This assumes that we have a 256-
bit session key for the MAC function, such as SK_ai and SK_ar in
IKEv2 ([RFC5996]), the integrity key in ESP and AH, or the
client_write_MAC_key and server_write_MAC_key in TLS. Any document
that specifies the use of Poly1305 as a MAC algorithm for some
protocol must specify that 256 bits are allocated for the integrity
key. Note that in the AEAD construction defined in Section 2.8, the
same key is used for encryption and key generation, so the use of
SK_a* or *_write_MAC_key is only for stand-alone Poly1305.
The method is to call the block function with the following
parameters:
* The 256-bit session integrity key is used as the ChaCha20 key.
* The block counter is set to zero.
* The protocol will specify a 96-bit or 64-bit nonce. This MUST be
unique per invocation with the same key, so it MUST NOT be
randomly generated. A counter is a good way to implement this,
but other methods, such as an LFSR are also acceptable. ChaCha20
as specified here requires a 96-bit nonce. So if the provided
nonce is only 64-bit, then the first 32 bits of the nonce will be
set to a constant number. This will usually be zero, but for
protocols with multiple senders it may be different for each
sender, but should be the same for all invocations of the function
with the same key by a particular sender.
After running the block function, we have a 512-bit state. We take
the first 256 bits or the serialized state, and use those as the one-
time Poly1305 key: The first 128 bits are clamped, and form "r",
while the next 128 bits become "s". The other 256 bits are
discarded.
Note that while many protocols have provisions for a nonce for
encryption algorithms (often called Initialization Vectors, or IVs),
they usually don't have such a provision for the MAC function. In
that case the per-invocation nonce will have to come from somewhere
else, such as a message counter.
### Poly1305 Key Generation Test Vector
For this example, we'll set:
```cryptol
PolyKeyTest = join (parseHexString (
"80 81 82 83 84 85 86 87 88 89 8a 8b 8c 8d 8e 8f " #
"90 91 92 93 94 95 96 97 98 99 9a 9b 9c 9d 9e 9f "
))
PolyNonceTest : [96]
PolyNonceTest = join (
parseHexString ("00 00 00 00 00 01 02 03 04 05 06 07 "))
```
The ChaCha state set up with key, nonce, and block counter zero:
## A Pseudo-Random Function for ChaCha/Poly-1305 based Crypto Suites
Some protocols such as IKEv2([RFC5996]) require a Pseudo-Random
Function (PRF), mostly for key derivation. In the IKEv2 definition,
a PRF is a function that accepts a variable-length key and a
variable-length input, and returns a fixed-length output. This
section does not specify such a function.
Poly-1305 is an obvious choice, because MAC functions are often used
as PRFs. However, Poly-1305 prohibits using the same key twice,
whereas the PRF in IKEv2 is used multiple times with the same key.
Adding a nonce or a counter to Poly-1305 can solve this issue, much
as we do when using this function as a MAC, but that would require
changing the interface for the PRF function.
Chacha20 could be used as a key-derivation function, by generating an
arbitrarily long keystream. However, that is not what protocols such
as IKEv2 require.
For this reason, this document does not specify a PRF, and recommends
that crypto suites use some other PRF such as PRF_HMAC_SHA2_256
(section 2.1.2 of [RFC4868])
## AEAD Construction
AEAD_CHACHA20-POLY1305 is an authenticated encryption with additional
data algorithm. The inputs to AEAD_CHACHA20-POLY1305 are:
* A 256-bit key
* A 96-bit nonce - different for each invocation with the same key.
* An arbitrary length plaintext (fewer than 2^64 bytes)
* Arbitrary length additional data (AAD) (fewer than 2^64 bytes)
Some protocols may have unique per-invocation inputs that are not 96-
bit in length. For example, IPsec may specify a 64-bit nonce. In
such a case, it is up to the protocol document to define how to
transform the protocol nonce into a 96-bit nonce, for example by
concatenating a constant value.
The ChaCha20 and Poly1305 primitives are combined into an AEAD that
takes a 256-bit key and 96-bit nonce as follows:
* First, a Poly1305 one-time key is generated from the 256-bit key
and nonce using the procedure described in "Generating the Poly1305 key using ChaCha20".
* Next, the ChaCha20 encryption function is called to encrypt the
plaintext, using the input key and nonce, and with the initial
counter set to 1.
* Finally, the Poly1305 function is called with the Poly1305 key
calculated above, and a message constructed as a concatenation of
the following:
* The AAD
* padding1 - the padding is up to 15 zero bytes, and it brings
the total length so far to an integral multiple of 16. If the
length of the AAD was already an integral multiple of 16 bytes,
this field is zero-length.
* The ciphertext
* padding2 - the padding is up to 15 zero bytes, and it brings
the total length so far to an integral multiple of 16. If the
length of the ciphertext was already an integral multiple of 16
bytes, this field is zero-length.
* The length of the additional data in octets (as a 64-bit
little-endian integer).
* The length of the ciphertext in octets (as a 64-bit little-
endian integer).
The output from the AEAD is twofold:
* A ciphertext of the same length as the plaintext.
* A 128-bit tag, which is the output of the Poly1305 function.
Decryption is pretty much the same thing.
A few notes about this design:
1. The amount of encrypted data possible in a single invocation is
2^32-1 blocks of 64 bytes each, because of the size of the block
counter field in the ChaCha20 block function. This gives a total
of 247,877,906,880 bytes, or nearly 256 GB. This should be
enough for traffic protocols such as IPsec and TLS, but may be
too small for file and/or disk encryption. For such uses, we can
return to the original design, reduce the nonce to 64 bits, and
use the integer at position 13 as the top 32 bits of a 64-bit
block counter, increasing the total message size to over a
million petabytes (1,180,591,620,717,411,303,360 bytes to be
exact).
1. Despite the previous item, the ciphertext length field in the
construction of the buffer on which Poly1305 runs limits the
ciphertext (and hence, the plaintext) size to 2^64 bytes, or
sixteen thousand petabytes (18,446,744,073,709,551,616 bytes to
be exact).
### Example and Test Vector for AEAD_CHACHA20-POLY1305
For a test vector, we will use the following inputs to the
AEAD_CHACHA20-POLY1305 function:
Plaintext:
```cryptol
AeadPt = "Ladies and Gentlemen of the class of '99: " #
"If I could offer you only one tip for " #
"the future, sunscreen would be it."
AeadAAD = parseHexString "50 51 52 53 c0 c1 c2 c3 c4 c5 c6 c7 "
AeadKey = join (parseHexString (
"80 81 82 83 84 85 86 87 88 89 8a 8b 8c 8d 8e 8f " #
"90 91 92 93 94 95 96 97 98 99 9a 9b 9c 9d 9e 9f " ))
AeadIV = join [ 0x40, 0x41, 0x42, 0x43, 0x44, 0x45, 0x46, 0x47 ]
AeadC = join [0x07, 0x00, 0x00, 0x00]
AeadNonce = AeadC # AeadIV
```
32-bit fixed-common part:
Poly1305 Key:
```cryptol
AeadConstructionTestVector = parseHexString (
"50:51:52:53:c0:c1:c2:c3:c4:c5:c6:c7:00:00:00:00:" #
"d3:1a:8d:34:64:8e:60:db:7b:86:af:bc:53:ef:7e:c2:" #
"a4:ad:ed:51:29:6e:08:fe:a9:e2:b5:a7:36:ee:62:d6:" #
"3d:be:a4:5e:8c:a9:67:12:82:fa:fb:69:da:92:72:8b:" #
"1a:71:de:0a:9e:06:0b:29:05:d6:a5:b6:7e:cd:3b:36:" #
"92:dd:bd:7f:2d:77:8b:8c:98:03:ae:e3:28:09:1b:58:" #
"fa:b3:24:e4:fa:d6:75:94:55:85:80:8b:48:31:d7:bc:" #
"3f:f4:de:f0:8e:4b:7a:9d:e5:76:d2:65:86:ce:c6:4b:" #
"61:16:00:00:00:00:00:00:00:00:00:00:00:00:00:00:" #
"0c:00:00:00:00:00:00:00:72:00:00:00:00:00:00:00." )
```
Note the 4 zero bytes in line 000 and the 14 zero bytes in line 128
```cryptol
// Tag:
AeadTagTestVector = parseHexString "1a:e1:0b:59:4f:09:e2:6a:7e:90:2e:cb:d0:60:06:91."
```
# Implementation Advice
Each block of ChaCha20 involves 16 move operations and one increment
operation for loading the state, 80 each of XOR, addition and Roll
operations for the rounds, 16 more add operations and 16 XOR
operations for protecting the plaintext. Section 2.3 describes the
ChaCha block function as "adding the original input words". This
implies that before starting the rounds on the ChaCha state, we copy
it aside, only to add it in later. This is correct, but we can save
a few operations if we instead copy the state and do the work on the
copy. This way, for the next block you don't need to recreate the
state, but only to increment the block counter. This saves
approximately 5.5% of the cycles.
It is not recommended to use a generic big number library such as the
one in OpenSSL for the arithmetic operations in Poly1305. Such
libraries use dynamic allocation to be able to handle any-sized
integer, but that flexibility comes at the expense of performance as
well as side-channel security. More efficient implementations that
run in constant time are available, one of them in DJB's own library,
NaCl ([NaCl]). A constant-time but not optimal approach would be to
naively implement the arithmetic operations for a 288-bit integers,
because even a naive implementation will not exceed 2^288 in the
multiplication of (acc+block) and r. An efficient constant-time
implementation can be found in the public domain library poly1305-
donna ([poly1305_donna]).
# Security Considerations
The ChaCha20 cipher is designed to provide 256-bit security.
The Poly1305 authenticator is designed to ensure that forged messages
are rejected with a probability of 1-(n/(2^102)) for a 16n-byte
message, even after sending 2^64 legitimate messages, so it is SUF-
CMA in the terminology of [AE].
Proving the security of either of these is beyond the scope of this
document. Such proofs are available in the referenced academic
papers.
The most important security consideration in implementing this draft
is the uniqueness of the nonce used in ChaCha20. Counters and LFSRs
are both acceptable ways of generating unique nonces, as is
encrypting a counter using a 64-bit cipher such as DES. Note that it
is not acceptable to use a truncation of a counter encrypted with a
128-bit or 256-bit cipher, because such a truncation may repeat after
a short time.
The Poly1305 key MUST be unpredictable to an attacker. Randomly
generating the key would fulfill this requirement, except that
Poly1305 is often used in communications protocols, so the receiver
should know the key. Pseudo-random number generation such as by
encrypting a counter is acceptable. Using ChaCha with a secret key
and a nonce is also acceptable.
The algorithms presented here were designed to be easy to implement
in constant time to avoid side-channel vulnerabilities. The
operations used in ChaCha20 are all additions, XORs, and fixed
rotations. All of these can and should be implemented in constant
time. Access to offsets into the ChaCha state and the number of
operations do not depend on any property of the key, eliminating the
chance of information about the key leaking through the timing of
cache misses.
For Poly1305, the operations are addition, multiplication and
modulus, all on >128-bit numbers. This can be done in constant time,
but a naive implementation (such as using some generic big number
library) will not be constant time. For example, if the
multiplication is performed as a separate operation from the modulus,
the result will some times be under 2^256 and some times be above
2^256. Implementers should be careful about timing side-channels for
Poly1305 by using the appropriate implementation of these operations.
# IANA Considerations
There are no IANA considerations for this document.
# Acknowledgements
ChaCha20 and Poly1305 were invented by Daniel J. Bernstein. The AEAD
construction and the method of creating the one-time poly1305 key
were invented by Adam Langley.
Thanks to Robert Ransom, Watson Ladd, Stefan Buhler, and kenny
patterson for their helpful comments and explanations. Thanks to
Niels Moeller for suggesting the more efficient AEAD construction in
this document. Special thanks to Ilari Liusvaara for providing extra
test vectors, helpful comments, and for being the first to attempt an
implementation from this draft.
# References
## Normative References
```example
[RFC2119] Bradner, S., "Key words for use in RFCs to Indicate
Requirement Levels", BCP 14, RFC 2119, March 1997.
[chacha] Bernstein, D., "ChaCha, a variant of Salsa20", Jan 2008.
[poly1305]
Bernstein, D., "The Poly1305-AES message-authentication
code", Mar 2005.
```
## Informative References
```example
[AE] Bellare, M. and C. Namprempre, "Authenticated Encryption:
Relations among notions and analysis of the generic
composition paradigm",
<http://cseweb.ucsd.edu/~mihir/papers/oem.html>.
[FIPS-197]
National Institute of Standards and Technology, "Advanced
Encryption Standard (AES)", FIPS PUB 197, November 2001.
[FIPS-46] National Institute of Standards and Technology, "Data
Encryption Standard", FIPS PUB 46-2, December 1993,
<http://www.itl.nist.gov/fipspubs/fip46-2.htm>.
[LatinDances]
Aumasson, J., Fischer, S., Khazaei, S., Meier, W., and C.
Rechberger, "New Features of Latin Dances: Analysis of
Salsa, ChaCha, and Rumba", Dec 2007.
[NaCl] Bernstein, D., Lange, T., and P. Schwabe, "NaCl:
Networking and Cryptography library",
<http://nacl.cace-project.eu/index.html>.
[RFC4868] Kelly, S. and S. Frankel, "Using HMAC-SHA-256, HMAC-SHA-
384, and HMAC-SHA-512 with IPsec", RFC 4868, May 2007.
[RFC5116] McGrew, D., "An Interface and Algorithms for Authenticated
Encryption", RFC 5116, January 2008.
[RFC5996] Kaufman, C., Hoffman, P., Nir, Y., and P. Eronen,
"Internet Key Exchange Protocol Version 2 (IKEv2)",
RFC 5996, September 2010.
[Zhenqing2012]
Zhenqing, S., Bin, Z., Dengguo, F., and W. Wenling,
"Improved key recovery attacks on reduced-round salsa20
and chacha", 2012.
[poly1305_donna]
Floodyberry, A., "Poly1305-donna",
<https://github.com/floodyberry/poly1305-donna>.
[standby-cipher]
McGrew, D., Grieco, A., and Y. Sheffer, "Selection of
Future Cryptographic Standards",
draft-mcgrew-standby-cipher (work in progress).
```
Authors' Addresses
```verbatim
Yoav Nir
Check Point Software Technologies Ltd.
5 Hasolelim st.
Tel Aviv 6789735
Israel
Email: ynir.ietf@gmail.com
Adam Langley
Google Inc
Email: agl@google.com
Dylan McNamee
Galois Inc
Email: dylan@galois.com
```
## Utilities
```cryptol
// Converts a bytestring encoded like "fe:ed:fa:ce." into a sequence of bytes
// Note: the trailing punctuation is needed
parseHexString : {n} (fin n) => [3*n][8] -> [n][8]
parseHexString hexString = [ charsToByte (take`{2} cs) | cs <- groupBy`{3} hexString ] where
charsToByte : [2][8] -> [8]
charsToByte [ ub, lb ] = (charToByte ub) << 4 || (charToByte lb)
charToByte c = if c >= '0' && c <= '9' then c-'0'
| c >= 'a' && c <= 'f' then 10+(c-'a')
else 0 // error case
property parseHexString_check =
join (parseHexString
("00:01:02:03:04:05:06:07:08:09:0a:0b:0c:0d:0e:0f:10:11:12:13:" #
"14:15:16:17:18:19:1a:1b:1c:1d:1e:1f.")) ==
0x000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f
// Takes a finite sequence of bytes, and turns them into a word via
// a little-endian interpretation
littleendian : {a}(fin a) => [a][8] -> [a*8]
littleendian b = join(reverse b)
```

89
examples/MiniLock/prim/SCrypt.cry Normal file
View File

@ -0,0 +1,89 @@
/*
* 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 N, 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 pwBytes, fin saltBytes, fin r
, 4*r >= 1, 16 >= width (4*r)
, ((dkLen*8 + 255) / 256) >= 1
, 32 >= width (8*pwBytes)
, 32 >= width (4 + saltBytes)
, 16 >= width ((255 + 8 * dkLen) / 256)
, 8 * dkLen == 256 * ((255 + 8 * dkLen) / 256) // seriously cryptol?
, fin N, N >= 1, 512 >= width N, 1+width N >= width (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 `{len=((dkLen*8)+255)/256,C=1} P (split B')
SCrypt : {pwBytes, saltBytes, dkBytes, r, N}
( fin pwBytes, fin saltBytes, fin r
, 4*r >= 1, 16 >= width (4*r)
, (dkBytes * 8 + 255) / 256 >= 1
, 16 >= width ((255 + 8 * dkBytes) / 256)
, 8 * dkBytes == 256 * ((255 + 8 * dkBytes) / 256)
, 32 >= width (8 * pwBytes)
, 32 >= width (4 * saltBytes)
, fin N, N >= 1, 512 >= width N, 1+width N >= width (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
// ]
]

120
examples/MiniLock/prim/SHA256.cry Normal file
View File

@ -0,0 +1,120 @@
/*
* @tmd - 24 April 2015 - took Ian's SHA512, converted to SHA256
* @ian - 15 August 2015 - he lies, probably ment 2014.
*
* This is a very simple implementation of SHA256, designed to be as clearly
* mathced to the specification in NIST's FIPS-PUB-180-4 as possible
*
* * The output correctly matches on all test vectors from
* http://csrc.nist.gov/groups/ST/toolkit/documents/Examples/SHA256.pdf
*/
module SHA256 where
/*
* SHA256 Functions : Section 4.1.2
*/
Ch : [32] -> [32] -> [32] -> [32]
Ch x y z = (x && y) ^ (~x && z)
Maj : [32] -> [32] -> [32] -> [32]
Maj x y z = (x && y) ^ (x && z) ^ (y && z)
S0 : [32] -> [32]
S0 x = (x >>> 2) ^ (x >>> 13) ^ (x >>> 22)
S1 : [32] -> [32]
S1 x = (x >>> 6) ^ (x >>> 11) ^ (x >>> 25)
s0 : [32] -> [32]
s0 x = (x >>> 7) ^ (x >>> 18) ^ (x >> 3)
s1 : [32] -> [32]
s1 x = (x >>> 17) ^ (x >>> 19) ^ (x >> 10)
/*
* SHA256 Constants : Section 4.2.2
*/
K : [64][32]
K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5,
0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174,
0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da,
0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967,
0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85,
0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070,
0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3,
0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2
]
/*
* Preprocessing (padding and parsing) for SHA256 : Section 5.1.1 and 5.2.1
*/
preprocess : {msgLen,contentLen,chunks,padding}
( fin msgLen
, 64 >= width msgLen // message width fits in a word
, contentLen == msgLen + 65 // message + header
, chunks == (contentLen+511) / 512
, padding == (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0
)
=> [msgLen] -> [chunks][512]
preprocess msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
/*
* SHA256 Initial Hash Value : Section 5.3.3
*/
H0 : [8][32]
H0 = [ 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a,
0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19]
/*
* The SHA256 Hash computation : Section 6.2.2
*
* We have split the computation into a message scheduling function, corresponding
* to step 1 in the documents loop, and a compression function, corresponding to steps 2-4.
*/
SHA256MessageSchedule : [16][32] -> [64][32]
SHA256MessageSchedule M = W where
W = M # [ s1 (W@(j-2)) + (W@(j-7)) + s0 (W@(j-15)) + (W@(j-16)) | j <- [16 .. 63]:[_][8] ]
SHA256Compress : [8][32] -> [64][32] -> [8][32]
SHA256Compress H W = [as!0 + H@0, bs!0 + H@1, cs!0 + H@2, ds!0 + H@3, es!0 + H@4, fs!0 + H@5, gs!0 + H@6, hs!0 + H@7] where
T1 = [h + S1 e + Ch e f g + k + w | h <- hs | e <- es | f <- fs | g <- gs | k <- K | w <- W]
T2 = [S0 a + Maj a b c | a <- as | b <- bs | c <- cs]
hs = take `{65} ([H@7] # gs)
gs = take `{65} ([H@6] # fs)
fs = take `{65} ([H@5] # es)
es = take `{65} ([H@4] # [d + t1 | d <- ds | t1 <- T1])
ds = take `{65} ([H@3] # cs)
cs = take `{65} ([H@2] # bs)
bs = take `{65} ([H@1] # as)
as = take `{65} ([H@0] # [t1 + t2 | t1 <- T1 | t2 <- T2])
/*
* The SHA256' function hashes a preprocessed sequence of blocks with the
* compression function. The SHA256 function hashes a sequence of bytes, and
* is more likely the function that will be similar to those seein in an
* implementation to be verified.
*/
SHA256' : {a} (fin a) => [a][16][32] -> [8][32]
SHA256' blocks = hash!0 where
hash = [H0] # [SHA256Compress h (SHA256MessageSchedule b) | h <- hash | b <- blocks]
SHA256 : {a} (fin a, 64 >= width (8*a)) => [a][8] -> [256]
SHA256 msg = join (SHA256' [ split x | x <- preprocess(join msg)])
property katsPass = ~zero == [test == kat | (test,kat) <- kats ]
kats = [ (SHA256 "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
, 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1)
, (SHA256 ""
,0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855)
, (SHA256 "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
, 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1)
// , (SHA256 [0x61 | i <- [1..1000000] : [_][32]]
// , 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0)
]

274
examples/MiniLock/prim/Salsa20.cry Normal file
View File

@ -0,0 +1,274 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
// see http://cr.yp.to/snuffle/spec.pdf
module Salsa20 where
import LittleEndian
quarterround : [4][32] -> [4][32]
quarterround [y0, y1, y2, y3] = [z0, z1, z2, z3]
where
z1 = y1 ^ ((y0 + y3) <<< 0x7)
z2 = y2 ^ ((z1 + y0) <<< 0x9)
z3 = y3 ^ ((z2 + z1) <<< 0xd)
z0 = y0 ^ ((z3 + z2) <<< 0x12)
property quarterround_passes_tests =
(quarterround [0x00000000, 0x00000000, 0x00000000, 0x00000000] == [0x00000000, 0x00000000, 0x00000000, 0x00000000]) &&
(quarterround [0x00000001, 0x00000000, 0x00000000, 0x00000000] == [0x08008145, 0x00000080, 0x00010200, 0x20500000]) &&
(quarterround [0x00000000, 0x00000001, 0x00000000, 0x00000000] == [0x88000100, 0x00000001, 0x00000200, 0x00402000]) &&
(quarterround [0x00000000, 0x00000000, 0x00000001, 0x00000000] == [0x80040000, 0x00000000, 0x00000001, 0x00002000]) &&
(quarterround [0x00000000, 0x00000000, 0x00000000, 0x00000001] == [0x00048044, 0x00000080, 0x00010000, 0x20100001]) &&
(quarterround [0xe7e8c006, 0xc4f9417d, 0x6479b4b2, 0x68c67137] == [0xe876d72b, 0x9361dfd5, 0xf1460244, 0x948541a3]) &&
(quarterround [0xd3917c5b, 0x55f1c407, 0x52a58a7a, 0x8f887a3b] == [0x3e2f308c, 0xd90a8f36, 0x6ab2a923, 0x2883524c])
rowround : [16][32] -> [16][32]
rowround [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] =
[z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15]
where
[ z0, z1, z2, z3] = quarterround [ y0, y1, y2, y3]
[ z5, z6, z7, z4] = quarterround [ y5, y6, y7, y4]
[z10, z11, z8, z9] = quarterround [y10, y11, y8, y9]
[z15, z12, z13, z14] = quarterround [y15, y12, y13, y14]
property rowround_passes_tests =
(rowround [0x00000001, 0x00000000, 0x00000000, 0x00000000,
0x00000001, 0x00000000, 0x00000000, 0x00000000,
0x00000001, 0x00000000, 0x00000000, 0x00000000,
0x00000001, 0x00000000, 0x00000000, 0x00000000] ==
[0x08008145, 0x00000080, 0x00010200, 0x20500000,
0x20100001, 0x00048044, 0x00000080, 0x00010000,
0x00000001, 0x00002000, 0x80040000, 0x00000000,
0x00000001, 0x00000200, 0x00402000, 0x88000100]) &&
(rowround [0x08521bd6, 0x1fe88837, 0xbb2aa576, 0x3aa26365,
0xc54c6a5b, 0x2fc74c2f, 0x6dd39cc3, 0xda0a64f6,
0x90a2f23d, 0x067f95a6, 0x06b35f61, 0x41e4732e,
0xe859c100, 0xea4d84b7, 0x0f619bff, 0xbc6e965a] ==
[0xa890d39d, 0x65d71596, 0xe9487daa, 0xc8ca6a86,
0x949d2192, 0x764b7754, 0xe408d9b9, 0x7a41b4d1,
0x3402e183, 0x3c3af432, 0x50669f96, 0xd89ef0a8,
0x0040ede5, 0xb545fbce, 0xd257ed4f, 0x1818882d])
rowround_opt : [16][32] -> [16][32]
rowround_opt ys = join [ (quarterround (yi<<<i))>>>i | yi <- split ys | i <- [0 .. 3] : [_][8] ]
property rowround_opt_is_rowround ys = rowround ys == rowround_opt ys
columnround : [16][32] -> [16][32]
columnround [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15] =
[y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15]
where
[ y0, y4, y8, y12] = quarterround [ x0, x4, x8, x12]
[ y5, y9, y13, y1] = quarterround [ x5, x9, x13, x1]
[y10, y14, y2, y6] = quarterround [x10, x14, x2, x6]
[y15, y3, y7, y11] = quarterround [x15, x3, x7, x11]
property columnround_passes_tests =
(columnround [0x00000001, 0x00000000, 0x00000000, 0x00000000,
0x00000001, 0x00000000, 0x00000000, 0x00000000,
0x00000001, 0x00000000, 0x00000000, 0x00000000,
0x00000001, 0x00000000, 0x00000000, 0x00000000] ==
[0x10090288, 0x00000000, 0x00000000, 0x00000000,
0x00000101, 0x00000000, 0x00000000, 0x00000000,
0x00020401, 0x00000000, 0x00000000, 0x00000000,
0x40a04001, 0x00000000, 0x00000000, 0x00000000]) &&
(columnround [0x08521bd6, 0x1fe88837, 0xbb2aa576, 0x3aa26365,
0xc54c6a5b, 0x2fc74c2f, 0x6dd39cc3, 0xda0a64f6,
0x90a2f23d, 0x067f95a6, 0x06b35f61, 0x41e4732e,
0xe859c100, 0xea4d84b7, 0x0f619bff, 0xbc6e965a] ==
[0x8c9d190a, 0xce8e4c90, 0x1ef8e9d3, 0x1326a71a,
0x90a20123, 0xead3c4f3, 0x63a091a0, 0xf0708d69,
0x789b010c, 0xd195a681, 0xeb7d5504, 0xa774135c,
0x481c2027, 0x53a8e4b5, 0x4c1f89c5, 0x3f78c9c8])
columnround_opt : [16][32] -> [16][32]
columnround_opt xs = join (transpose [ (quarterround (xi<<<i))>>>i | xi <- transpose(split xs) | i <- [0 .. 3] : [_][8] ])
columnround_opt_is_columnround xs = columnround xs == columnround_opt xs
property columnround_is_transpose_of_rowround ys =
rowround ys == join(transpose(split`{4}(columnround xs)))
where xs = join(transpose(split`{4} ys))
doubleround : [16][32] -> [16][32]
doubleround(xs) = rowround(columnround(xs))
property doubleround_passes_tests =
(doubleround [0x00000001, 0x00000000, 0x00000000, 0x00000000,
0x00000000, 0x00000000, 0x00000000, 0x00000000,
0x00000000, 0x00000000, 0x00000000, 0x00000000,
0x00000000, 0x00000000, 0x00000000, 0x00000000] ==
[0x8186a22d, 0x0040a284, 0x82479210, 0x06929051,
0x08000090, 0x02402200, 0x00004000, 0x00800000,
0x00010200, 0x20400000, 0x08008104, 0x00000000,
0x20500000, 0xa0000040, 0x0008180a, 0x612a8020]) &&
(doubleround [0xde501066, 0x6f9eb8f7, 0xe4fbbd9b, 0x454e3f57,
0xb75540d3, 0x43e93a4c, 0x3a6f2aa0, 0x726d6b36,
0x9243f484, 0x9145d1e8, 0x4fa9d247, 0xdc8dee11,
0x054bf545, 0x254dd653, 0xd9421b6d, 0x67b276c1] ==
[0xccaaf672, 0x23d960f7, 0x9153e63a, 0xcd9a60d0,
0x50440492, 0xf07cad19, 0xae344aa0, 0xdf4cfdfc,
0xca531c29, 0x8e7943db, 0xac1680cd, 0xd503ca00,
0xa74b2ad6, 0xbc331c5c, 0x1dda24c7, 0xee928277])
Salsa20 : {r} (8 >= width r) => [64][8] -> [64][8]
Salsa20 xs = join ar
where
ar = [ littleendian_inverse words | words <- xw + zs@(`r/2 : [8]) ]
xw = [ littleendian xi | xi <- split xs ]
zs = [xw] # [ doubleround zi | zi <- zs ]
property Salsa20_bijective a b = (a == b) || (Salsa20 `{r=20} a != Salsa20 `{r=20} b)
property Salsa20_passes_tests =
(Salsa20 `{r=20}
[ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ==
[ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) &&
(Salsa20 `{r=20}
[211, 159, 13, 115, 76, 55, 82, 183, 3, 117, 222, 37, 191, 187, 234, 136,
49, 237, 179, 48, 1, 106, 178, 219, 175, 199, 166, 48, 86, 16, 179, 207,
31, 240, 32, 63, 15, 83, 93, 161, 116, 147, 48, 113, 238, 55, 204, 36,
79, 201, 235, 79, 3, 81, 156, 47, 203, 26, 244, 243, 88, 118, 104, 54] ==
[109, 42, 178, 168, 156, 240, 248, 238, 168, 196, 190, 203, 26, 110, 170, 154,
29, 29, 150, 26, 150, 30, 235, 249, 190, 163, 251, 48, 69, 144, 51, 57,
118, 40, 152, 157, 180, 57, 27, 94, 107, 42, 236, 35, 27, 111, 114, 114,
219, 236, 232, 135, 111, 155, 110, 18, 24, 232, 95, 158, 179, 19, 48, 202]) &&
(Salsa20 `{r=20}
[ 88, 118, 104, 54, 79, 201, 235, 79, 3, 81, 156, 47, 203, 26, 244, 243,
191, 187, 234, 136, 211, 159, 13, 115, 76, 55, 82, 183, 3, 117, 222, 37,
86, 16, 179, 207, 49, 237, 179, 48, 1, 106, 178, 219, 175, 199, 166, 48,
238, 55, 204, 36, 31, 240, 32, 63, 15, 83, 93, 161, 116, 147, 48, 113] ==
[179, 19, 48, 202, 219, 236, 232, 135, 111, 155, 110, 18, 24, 232, 95, 158,
26, 110, 170, 154, 109, 42, 178, 168, 156, 240, 248, 238, 168, 196, 190, 203,
69, 144, 51, 57, 29, 29, 150, 26, 150, 30, 235, 249, 190, 163, 251, 48,
27, 111, 114, 114, 118, 40, 152, 157, 180, 57, 27, 94, 107, 42, 236, 35])
property Salsa20_has_no_collisions x1 x2 =
x1 == x2 || doubleround x1 != doubleround x2
// if(x1 != x2) then (doubleround x1) != (doubleround x2) else True
property Salsa20_passes_scrypt_tests =
Salsa20 `{r=8}
[ 0x7e, 0x87, 0x9a, 0x21, 0x4f, 0x3e, 0xc9, 0x86, 0x7c, 0xa9, 0x40, 0xe6, 0x41, 0x71, 0x8f, 0x26
, 0xba, 0xee, 0x55, 0x5b, 0x8c, 0x61, 0xc1, 0xb5, 0x0d, 0xf8, 0x46, 0x11, 0x6d, 0xcd, 0x3b, 0x1d
, 0xee, 0x24, 0xf3, 0x19, 0xdf, 0x9b, 0x3d, 0x85, 0x14, 0x12, 0x1e, 0x4b, 0x5a, 0xc5, 0xaa, 0x32
, 0x76, 0x02, 0x1d, 0x29, 0x09, 0xc7, 0x48, 0x29, 0xed, 0xeb, 0xc6, 0x8d, 0xb8, 0xb8, 0xc2, 0x5e
]
== [ 0xa4, 0x1f, 0x85, 0x9c, 0x66, 0x08, 0xcc, 0x99, 0x3b, 0x81, 0xca, 0xcb, 0x02, 0x0c, 0xef, 0x05
, 0x04, 0x4b, 0x21, 0x81, 0xa2, 0xfd, 0x33, 0x7d, 0xfd, 0x7b, 0x1c, 0x63, 0x96, 0x68, 0x2f, 0x29
, 0xb4, 0x39, 0x31, 0x68, 0xe3, 0xc9, 0xe6, 0xbc, 0xfe, 0x6b, 0xc5, 0xb7, 0xa0, 0x6d, 0x96, 0xba
, 0xe4, 0x24, 0xcc, 0x10, 0x2c, 0x91, 0x74, 0x5c, 0x24, 0xad, 0x67, 0x3d, 0xc7, 0x61, 0x8f, 0x81
]
// Salsa 20 supports two key sizes, [16][8] and [32][8]
Salsa20_expansion : {a} (a >= 1, 2 >= a) => ([16*a][8], [16][8]) -> [64][8]
Salsa20_expansion(k, n) = z
where
[s0, s1, s2, s3] = split "expand 32-byte k" : [4][4][8]
[t0, t1, t2, t3] = split "expand 16-byte k" : [4][4][8]
x = if(`a == (2 : [8])) then s0 # k0 # s1 # n # s2 # k1 # s3
else t0 # k0 # t1 # n # t2 # k0 # t3
z = Salsa20 `{r=20} x
[k0, k1] = (split(k#zero)):[2][16][8]
Salsa20_encrypt : {a, l} (a >= 1, 2 >= a, l <= 2^^70) => ([16*a][8], [8][8], [l][8]) -> [l][8]
Salsa20_encrypt(k, v, m) = c
where
salsa = take (join [ Salsa20_expansion(k, v#(split i)) | i <- [0, 1 ... ] ])
c = m ^ salsa
HSalsa20 : {r} (8 >= width r) => Key -> Nonce -> [8][32]
HSalsa20 key0 nonce0 = zs @@ ([0,5,10,15,6,7,8,9] : [_][8])
where
zs = infZs @ (`r/2 :[8])
infZs = [xs] # [ doubleround x | x <- infZs ]
nonce = [ littleendian (split n) | n <- split (join nonce0)]
[x0,x5,x10,x15] = Salsa20_Constant
[x1,x2,x3,x4,x11,x12,x13,x14] = [ littleendian (split k) | k <- split (join key0)]
[x6,x7,x8,x9] = nonce @@ ([0..3] : [_][8])
xs : [16][32]
xs = [x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15]
HSalsa20_bytes : {r} (8 >= width r) => Key -> Nonce -> [32][8]
HSalsa20_bytes key0 nonce0 = join [littleendian_inverse x | x <- HSalsa20 `{r=r} key0 nonce0]
type Key = [256/8][8]
type Nonce = [192/8][8]
type Counter = [64]
Salsa20_Constant : [4][32]
Salsa20_Constant = [littleendian (split x) | x <- split (join "expand 32-byte k") : [4][32]]
XSalsa20 : {r} (8 >= width r) => Key -> Nonce -> Counter -> [64][8]
XSalsa20 key0 nonce0 ctr =
split (join [littleendian (split (x' + z')) | x' <- xs' | z' <- zs'])
where
nonce = [ littleendian (split n) | n <- split (join nonce0)]
subKey = HSalsa20 `{r=r} key0 nonce0 // 'zs' in the literature
[x'0,x'5,x'10,x'15] = Salsa20_Constant
[x'1,x'2,x'3,x'4,x'11,x'12,x'13,x'14] = subKey
[x'6,x'7] = nonce @@ ([4,5] : [_][8])
[x'8,x'9] = reverse (split ctr)
xs', zs' : [16][32]
xs' = [ x'0 ,x'1 ,x'2 ,x'3 ,x'4 ,x'5 ,x'6 ,x'7 ,x'8
, x'9 ,x'10 ,x'11 ,x'12 ,x'13 ,x'14 ,x'15
]
infZs' = [xs'] # [ doubleround x | x <- infZs' ]
zs' = infZs' @ (`r/2 : [8])
XSalsa20_expansion : {n,r} (8 >= width r, 64 >= width n) => Key -> Nonce -> [n][8]
XSalsa20_expansion k n = take (join ks)
where
ks = [XSalsa20 `{r=r} k n i | i <- [0...]]
XSalsa20_encrypt : {n,r} (8 >= width r, 64 >= width n) => Key -> Nonce -> [n][8] -> [n][8]
XSalsa20_encrypt k n msg = ks ^ msg
where ks = XSalsa20_expansion `{r=r} k n
property test =
ct == [0x00, 0x2d, 0x45, 0x13, 0x84, 0x3f, 0xc2, 0x40, 0xc4, 0x01, 0xe5, 0x41]
where
ct = XSalsa20_encrypt `{r=20} key nonce "Hello world!"
key = "this is 32-byte key for xsalsa20"
nonce = "24-byte nonce for xsalsa"
property theorem1 a = quarterround [a, -a, a, -a] == [a,-a,a,-a]
property theorem2 a b c d = rowround val == val
where val = [a,-a,a,-a
,b,-b,b,-b
,c,-c,c,-c
,d,-d,d,-d]
property theorem3 a b c d = columnround val == val
where val = [a,-b,c,-d
,-a,b,-c,d
,a,-b,c,-d
,-a,b,-c,d]
property theorem4 a = doubleround val == val
where val = [a,-a,a,-a
,-a,a,-a,a
,a,-a,a,-a
,-a,a,-a,a]
property theorem7 a b =
a ^ b != diff || Salsa20Words a == Salsa20Words b
where
diff = [ 0x80000000 | _ <- [0..15]]
Salsa20Words : [16][32] -> [16][32]
Salsa20Words x = [join (reverse r) | r <- split `{each=4} (Salsa20 `{r=20} (join [reverse (split `{4} v) | v <- x]))]

10
examples/MiniLock/prim/TestHMAC.cry Normal file
View File

@ -0,0 +1,10 @@
module TestHMAC where
import HMAC
import SHA256
property pass =
~zero ==
[ hmacSHA256 [0x0b | _ <- [1..20] : [_][6]] "Hi There" == 0xb0344c61d8db38535ca8afceaf0bf12b881dc200c9833da726e9376c2e32cff7
, hmacSHA256 "Jefe" "what do ya want for nothing?" == 0x5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843
]

42
examples/MiniLock/prim/bv.cry Normal file
View File

@ -0,0 +1,42 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module bv where
/* Unsigned word extension. */
uext : {a, b} (fin b,fin a) => [a] -> [a+b]
uext(x) = zero # x
iext : {a, b} (fin b,fin a) => [a] -> [a+b]
iext(x) = (if x@0 then ~zero else zero) # x
/* Returns the (n+1)-bit sum of two n-bit numbers. */
safe_add : {n} (fin n) => ([n],[n]) -> [n+1]
safe_add(x,y) = uext(x) + uext(y)
/* returns the (n+1)-bit subtraction of two n-bit numbers. */
safe_sub : {n} (fin n) => ([n],[n]) -> [n+1]
safe_sub(x,y) = uext(x) - uext(y)
/* Is x in normalized form (relative to prime p)? */
is_normal : {a} (fin a) => [a] -> [a] -> Bit
is_normal p x = (x < p)
/* Returns the product of two inputs. */
safe_product : {a} (fin a) => ([a],[a]) -> [2*a]
safe_product(x,y) = uext(x) * uext(y)
/* Returns module reduction on input. */
safe_mod : {a, b} (fin a, fin b) => ([b],[a+b]) -> [b]
safe_mod(p,x) = drop `{a} (x % uext(p))
/* Add two n-bit numbers and input carry to obtain a n bit number and output carry. */
adc : {n} (fin n) => ([n],[n]) -> ([n],Bit)
adc(x,y) = (drop(sm), sm@0)
where sm = safe_add(x,y)
/* sbb(x,y) subtracts y from x, and returns result along with output borrow bit. */
sbb : {n} (fin n) => ([n],[n]) -> ([n],Bit)
sbb(x,y) = (drop(r), r@0)
where r = ([False] # x) - ([False] # y)

55
examples/MiniLock/prim/mod_arith.cry Normal file
View File

@ -0,0 +1,55 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module mod_arith where
import bv
/* Add two numbers in normalized form. */
mod_add : {n} (fin n) => ([n],[n],[n]) -> [n]
mod_add(p,x,y) = if c1 || ~c2 then r2 else r1
where
(r1,c1) = adc( x, y)
(r2,c2) = sbb(r1, p)
/* Subtract two numbers in normalized form. */
mod_sub : {n} (fin n) => ([n],[n],[n]) -> [n]
mod_sub(p,x,y) = if b then r2 else r1
where
(r1,b) = sbb( x, y)
(r2,_) = adc(r1, p)
mod_neg : {n} (fin n) => ([n],[n]) -> [n]
mod_neg(p,x) = if x == 0 then 0 else (p - x)
mod_half : {n} (fin n, n >= 1) => ([n],[n]) -> [n]
mod_half(p, x) = if even(x) then x >> 1
else take(safe_add(x, p))
where even y = (y && 1) == 0
/* Definition of modular multiplication. */
mod_mul : {n} (fin n) => ([n],[n],[n]) -> [n]
mod_mul(p,x,y) = safe_mod(p, safe_product(x, y))
/* Returns x/y in F_p using Euler's binary gcd algorithm. */
/* Taken from [HMV] */
mod_div : {a} (fin a, a >= 1) => ([a],[a],[a]) -> [a]
mod_div(p,x,y) = egcd(p,0,y,x)
where
/* In code below, a is always odd. */
egcd(a,ra,b,rb) =
if b == 0 then
ra
else if (b && 1) == 0 then /* b is even. */
egcd(a, ra, b >> 1, mod_half(p, rb))
else if a < b then
egcd(a, ra, (b - a) >> 1, mod_half(p, mod_sub(p, rb, ra)))
else
egcd(b, rb, (a - b) >> 1, mod_half(p, mod_sub(p, ra, rb)))
mod_pow : {a} (fin a, a >= 1) => ([a] , [a] , [a]) -> [a]
mod_pow (p,x0,e0) = (results ! 0).2
where
results = [(x0,e0,1)] # [ (mod_mul (p,x,x), e>>1, if(e!0) then mod_mul(p,result,x) else result)
| (x,e,result) <- results | _ <- [0..a] :[_][width a] ]