mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-24 16:31:34 +03:00
Remove some duplicate files from /examples that were also in cryptol-specs.
See #571.
This commit is contained in:
Brian Huffman
parent
acafb2952d
commit
9584fdb54d
@ -1,34 +0,0 @@
|
|||||||
/*
|
|
||||||
* Copyright (c) 2014-2016 Galois, Inc.
|
|
||||||
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
||||||
*/
|
|
||||||
|
|
||||||
fnv1a : {n} (fin n) => [n] -> [64]
|
|
||||||
fnv1a ws = fnv1a' (pad ws)
|
|
||||||
|
|
||||||
pad : {msgLen} (fin msgLen) => [msgLen] -> [msgLen /^ 8][8]
|
|
||||||
pad msg = split (msg # (zero:[msgLen %^ 8]))
|
|
||||||
|
|
||||||
fnv1a' : {chunks} (fin chunks) => [chunks][8] -> [64]
|
|
||||||
fnv1a' msg = Ss ! 0
|
|
||||||
where
|
|
||||||
Ss = [fnv1a_offset_basis] #
|
|
||||||
[ block s m
|
|
||||||
| s <- Ss
|
|
||||||
| m <- msg
|
|
||||||
]
|
|
||||||
|
|
||||||
block : {padLen} ( padLen == 64 - 8) => [64] -> [8] -> [64]
|
|
||||||
block state val = (state ^ ((zero : [padLen]) # val)) * fnv1a_prime
|
|
||||||
|
|
||||||
fnv1a_offset_basis : [64]
|
|
||||||
fnv1a_offset_basis = 14695981039346656037
|
|
||||||
|
|
||||||
fnv1a_prime : [64]
|
|
||||||
fnv1a_prime = 1099511628211
|
|
||||||
|
|
||||||
t1 = fnv1a [] == 0xcbf29ce484222325
|
|
||||||
t2 = fnv1a (join "a") == 0xaf63dc4c8601ec8c
|
|
||||||
t3 = fnv1a (join "foobar") == 0x85944171f73967e8
|
|
||||||
|
|
||||||
property testsPass = [t1, t2, t3] == ~zero
|
|
||||||
@ -1,72 +0,0 @@
|
|||||||
////////////////////////////////////////////////////////////////
|
|
||||||
// Copyright 2016 Galois, Inc. All Rights Reserved
|
|
||||||
//
|
|
||||||
// Authors:
|
|
||||||
// Aaron Tomb : atomb@galois.com
|
|
||||||
// Nathan Collins : conathan@galois.com
|
|
||||||
// Joey Dodds : jdodds@galois.com
|
|
||||||
//
|
|
||||||
// Licensed under the Apache License, Version 2.0 (the "License").
|
|
||||||
// You may not use this file except in compliance with the License.
|
|
||||||
// A copy of the License is located at
|
|
||||||
//
|
|
||||||
// http://aws.amazon.com/apache2.0
|
|
||||||
//
|
|
||||||
// or in the "license" file accompanying this file. This file is distributed
|
|
||||||
// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
|
|
||||||
// express or implied. See the License for the specific language governing
|
|
||||||
// permissions and limitations under the License.
|
|
||||||
//
|
|
||||||
////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
module HMAC where
|
|
||||||
|
|
||||||
import SHA256
|
|
||||||
|
|
||||||
//////// Functional version ////////
|
|
||||||
|
|
||||||
hmacSHA256 : {pwBytes, msgBytes}
|
|
||||||
(fin pwBytes, fin msgBytes
|
|
||||||
, 32 >= width msgBytes
|
|
||||||
, 64 >= width (8*pwBytes)
|
|
||||||
, 64 >= width (8 * (64 + msgBytes))
|
|
||||||
) => [pwBytes][8] -> [msgBytes][8] -> [256]
|
|
||||||
hmacSHA256 = hmac `{blockLength=64} SHA256 SHA256 SHA256
|
|
||||||
|
|
||||||
kinit : { pwBytes, blockLength, digest }
|
|
||||||
( fin pwBytes, fin blockLength, fin digest )
|
|
||||||
=> ([pwBytes][8] -> [8*digest])
|
|
||||||
-> [pwBytes][8]
|
|
||||||
-> [blockLength][8]
|
|
||||||
kinit hash key =
|
|
||||||
if `pwBytes > (`blockLength : [max (width pwBytes) (width blockLength)])
|
|
||||||
then take `{blockLength} (split (hash key) # (zero : [blockLength][8]))
|
|
||||||
else take `{blockLength} (key # (zero : [blockLength][8]))
|
|
||||||
|
|
||||||
// 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 )
|
|
||||||
=> ([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 = kinit hash3 key
|
|
||||||
okey = [k ^ 0x5C | k <- ks]
|
|
||||||
ikey = [k ^ 0x36 | k <- ks]
|
|
||||||
internal = split (hash (ikey # message))
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
271
examples/MD5.cry
271
examples/MD5.cry
@ -1,271 +0,0 @@
|
|||||||
// Copyright (c) 2001, 2014 Galois, Inc.
|
|
||||||
// Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
||||||
//
|
|
||||||
// MD5 digest algorithm from RFC 1321
|
|
||||||
// https://www.ietf.org/rfc/rfc1321.txt
|
|
||||||
//
|
|
||||||
// Based on a previous Cryptol 1.* implementation
|
|
||||||
|
|
||||||
// Swap byte order from network to host order (long word)
|
|
||||||
ntohl : [32] -> [32]
|
|
||||||
ntohl w = join (reverse (groupBy`{8} w))
|
|
||||||
|
|
||||||
// Swap byte order from host to network order (long word)
|
|
||||||
htonl : [32] -> [32]
|
|
||||||
htonl w = join (reverse (groupBy`{8} w))
|
|
||||||
|
|
||||||
// Swap byte order from host to network order (long long word)
|
|
||||||
htonll : [64] -> [64]
|
|
||||||
htonll w = join (reverse (groupBy`{8} w))
|
|
||||||
|
|
||||||
// apply a function to every element of a sequence
|
|
||||||
map : {n, a, b} (a -> b) -> [n]a -> [n]b
|
|
||||||
map f xs = [ f x | x <- xs ]
|
|
||||||
|
|
||||||
// fold with left associativity
|
|
||||||
foldl : {n, a, b} (fin n) => a -> (a -> b -> a) -> [n]b -> a
|
|
||||||
foldl seed f xs = res ! 0
|
|
||||||
where res = [seed] # [ f a x | a <- res
|
|
||||||
| x <- xs
|
|
||||||
]
|
|
||||||
|
|
||||||
// Test driver. Given a sequence of bytes, calculate the MD5 sum.
|
|
||||||
test s = md5 (join s)
|
|
||||||
|
|
||||||
// Reference implementation of MD5 on exactly 16 bytes.
|
|
||||||
|
|
||||||
md5_ref : [16][8] -> [16][8]
|
|
||||||
md5_ref msg = map reverse (groupBy`{8} (md5`{p=319} (join (map reverse msg))))
|
|
||||||
|
|
||||||
md5_ref' : [128] -> [128]
|
|
||||||
md5_ref' msg = join (md5_ref (groupBy`{8} msg))
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
// The state of the MD5 algorithm after each 512 bit block
|
|
||||||
// consists of 4 32-bit words.
|
|
||||||
type MD5State = ([32],[32],[32],[32])
|
|
||||||
|
|
||||||
// Main MD5 algorithm.
|
|
||||||
//
|
|
||||||
// First, pad the message to a multiple of 512 bits.
|
|
||||||
// Next, initilize the MD5 state using the fixed values from the RFC.
|
|
||||||
// Then, process each message block in turn by computing
|
|
||||||
// the MD5 rounds using the message block. Add the result
|
|
||||||
// of the final round to the current MD5 state.
|
|
||||||
// Finally, return the current MD5 state after all blocks are processed,
|
|
||||||
// interpreting the 4 32-bit words as a single 128-bit sequence.
|
|
||||||
|
|
||||||
md5 : {a, b, p} (fin p, 512 * b == 65 + (a + p), 64 >= width a, 511 >= p) =>
|
|
||||||
[a] -> [128]
|
|
||||||
md5 msg = md5output finalState
|
|
||||||
where
|
|
||||||
finalState : MD5State
|
|
||||||
finalState = foldl initialMD5State processBlock blocks
|
|
||||||
|
|
||||||
blocks : [b][512]
|
|
||||||
blocks = groupBy`{512} (pad `{a,p} msg)
|
|
||||||
|
|
||||||
add : MD5State -> MD5State -> MD5State
|
|
||||||
add (a, b, c, d) (e, f, g, h) = (a + e, b + f, c + g, d + h)
|
|
||||||
|
|
||||||
processBlock : MD5State -> [512] -> MD5State
|
|
||||||
processBlock st blk = add st (computeRounds (decodeBlock blk) st)
|
|
||||||
|
|
||||||
|
|
||||||
// Initial seed for the digest rounds
|
|
||||||
//
|
|
||||||
// See RFC 1321, section 3.3
|
|
||||||
|
|
||||||
initialMD5State : MD5State
|
|
||||||
initialMD5State = (A, B, C, D)
|
|
||||||
where
|
|
||||||
f x = ntohl (join x)
|
|
||||||
A = f [ 0x01, 0x23, 0x45, 0x67 ]
|
|
||||||
B = f [ 0x89, 0xAB, 0xCD, 0xEF ]
|
|
||||||
C = f [ 0xFE, 0xDC, 0xBA, 0x98 ]
|
|
||||||
D = f [ 0x76, 0x54, 0x32, 0x10 ]
|
|
||||||
|
|
||||||
|
|
||||||
// Each MD5 message block 512 bits long, interpreted as a sequence of 16 32-bit words
|
|
||||||
// Each word is given as a sequence of 4 bytes, with LEAST significant byte first
|
|
||||||
// Each byte is given as a sequence of 8 bits, with MOST significant bit first
|
|
||||||
//
|
|
||||||
// The output of the algorithm is a sequence of 4 words, interpreted as above
|
|
||||||
//
|
|
||||||
// See RFC 1321, section 2
|
|
||||||
|
|
||||||
decodeBlock : [512] -> [16][32]
|
|
||||||
decodeBlock s = map ntohl (groupBy`{32} s)
|
|
||||||
|
|
||||||
|
|
||||||
// Interpret 4 32-bit words as a single 128-bit sequence
|
|
||||||
//
|
|
||||||
// See RFC 1321 section 3.5
|
|
||||||
|
|
||||||
md5output : MD5State -> [128]
|
|
||||||
md5output (a,b,c,d) = htonl a # htonl b # htonl c # htonl d
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
// Given an arbitrary byte sequence whose length can be described
|
|
||||||
// by a 64-bit number, pad the message so it is exactly a multiple of 512.
|
|
||||||
//
|
|
||||||
// This is done by adding a single 1 bit to the end of the message, and
|
|
||||||
// then adding enough zero bits to make the whole message 64 bits shorter
|
|
||||||
// than a multiple of 512. The size (in bits) of the original message is
|
|
||||||
// then appended to complete the padded message.
|
|
||||||
//
|
|
||||||
// See RFC 1321, sections 3.1 and 3.2
|
|
||||||
|
|
||||||
pad : {a, p} (fin p, 64 >= width a) => [a] -> [65 + (a + p)]
|
|
||||||
pad msg =
|
|
||||||
msg # [True] # zero # htonll sz
|
|
||||||
where
|
|
||||||
sz : [64]
|
|
||||||
sz = length msg
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
// Given a message block (interpreted as 16 32-bit words) and a current MD5 state
|
|
||||||
// (as 4 32-bit words) compute the values of all the rounds of the MD5 algorithm.
|
|
||||||
//
|
|
||||||
// In the main MD5 function, the final round will be used to compute the next MD5 state.
|
|
||||||
//
|
|
||||||
// See RFC 1321, section 3.4
|
|
||||||
|
|
||||||
computeRounds : [16][32] -> MD5State -> MD5State
|
|
||||||
computeRounds msg st = rounds (msg,st) @ 64
|
|
||||||
|
|
||||||
rounds : ([16][32], MD5State) -> [65]MD5State
|
|
||||||
rounds (msg, (a0, b0, c0, d0)) =
|
|
||||||
[ (a, b, c, d) | a <- as
|
|
||||||
| b <- bs
|
|
||||||
| c <- cs
|
|
||||||
| d <- ds
|
|
||||||
]
|
|
||||||
where
|
|
||||||
bs =
|
|
||||||
[b0] #
|
|
||||||
[box (i, a, b, c, d, m, t, s) | i <- [0 .. 63]
|
|
||||||
| a <- as
|
|
||||||
| b <- bs
|
|
||||||
| c <- cs
|
|
||||||
| d <- ds
|
|
||||||
| m <- join [m @@ p | m <- [msg, msg, msg, msg]
|
|
||||||
| p <- permutes
|
|
||||||
]
|
|
||||||
| t <- sineTbl
|
|
||||||
| s <- s_constants
|
|
||||||
]
|
|
||||||
cs = [c0] # bs
|
|
||||||
ds = [d0] # cs
|
|
||||||
as = [a0] # ds
|
|
||||||
|
|
||||||
|
|
||||||
// 'S' constants from the MD5 algorithm, used to indicated how many
|
|
||||||
// bits to rotate in the box function.
|
|
||||||
//
|
|
||||||
// See RFC 1321, section 3.4, and the appendix on page 10
|
|
||||||
|
|
||||||
s_constants : [64][6]
|
|
||||||
s_constants =
|
|
||||||
repeat4 [7, 12, 17, 22] #
|
|
||||||
repeat4 [5, 9, 14, 20] #
|
|
||||||
repeat4 [4, 11, 16, 23] #
|
|
||||||
repeat4 [6, 10, 15, 21]
|
|
||||||
where
|
|
||||||
repeat4 abcd = abcd # abcd # abcd # abcd
|
|
||||||
|
|
||||||
|
|
||||||
// This table of permutations indicates which word of the message block to
|
|
||||||
// use in a given MD5 round. Its structure is most evident via observing
|
|
||||||
// the indices of the message block in the order they are used in the MD5
|
|
||||||
// reference implementation.
|
|
||||||
//
|
|
||||||
// See the appendix of RFC 1321, starting on page 13.
|
|
||||||
|
|
||||||
permutes : [4][16][4]
|
|
||||||
permutes =
|
|
||||||
[ [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
|
|
||||||
, [ 1, 6, 11, 0, 5, 10, 15, 4, 9, 14, 3, 8, 13, 2, 7, 12]
|
|
||||||
, [ 5, 8, 11, 14, 1, 4, 7, 10, 13, 0, 3, 6, 9, 12, 15, 2]
|
|
||||||
, [ 0, 7, 14, 5, 12, 3, 10, 1, 8, 15, 6, 13, 4, 11, 2, 9]
|
|
||||||
]
|
|
||||||
|
|
||||||
|
|
||||||
// The main "box" operation. The first argument indicates
|
|
||||||
// the round number, which is used to select between the box
|
|
||||||
// operations, F, G, H, and I.
|
|
||||||
//
|
|
||||||
// See RFC 1321, section 3.4
|
|
||||||
|
|
||||||
box : ([6], [32], [32], [32], [32], [32], [32], [6]) -> [32]
|
|
||||||
box (i, a, b, c, d, m, t, s) =
|
|
||||||
b + (a + boxfunc (i, b, c, d) + m + t <<< s)
|
|
||||||
|
|
||||||
boxfunc : ([6],[32],[32],[32]) -> [32]
|
|
||||||
boxfunc (i, b, c, d) =
|
|
||||||
if i < 16 then F (b, c, d) else
|
|
||||||
if i < 32 then G (b, c, d) else
|
|
||||||
if i < 48 then H (b, c, d) else
|
|
||||||
I (b, c, d)
|
|
||||||
|
|
||||||
F : ([32], [32], [32]) -> [32]
|
|
||||||
F (x, y, z) = x && y || (~x) && z
|
|
||||||
|
|
||||||
G : ([32], [32], [32]) -> [32]
|
|
||||||
G (x, y, z) = x && z || y && ~z
|
|
||||||
|
|
||||||
H : ([32], [32], [32]) -> [32]
|
|
||||||
H (x, y, z) = x ^ y ^ z
|
|
||||||
|
|
||||||
I : ([32], [32], [32]) -> [32]
|
|
||||||
I (x, y, z) = y ^ (x || ~z)
|
|
||||||
|
|
||||||
|
|
||||||
// The table of values generated from the sin function, as described
|
|
||||||
// in RFC 1321, section 3.4. These values are transcribed from
|
|
||||||
// the appendix, starting on page 13.
|
|
||||||
|
|
||||||
sineTbl : [64][32]
|
|
||||||
sineTbl =
|
|
||||||
[0xD76AA478, 0xE8C7B756, 0x242070DB, 0xC1BDCEEE, 0xF57C0FAF,
|
|
||||||
0x4787C62A, 0xA8304613, 0xFD469501, 0x698098D8, 0x8B44F7AF,
|
|
||||||
0xFFFF5BB1, 0x895CD7BE, 0x6B901122, 0xFD987193, 0xA679438E,
|
|
||||||
0x49B40821, 0xF61E2562, 0xC040B340, 0x265E5A51, 0xE9B6C7AA,
|
|
||||||
0xD62F105D, 0x02441453, 0xD8A1E681, 0xE7D3FBC8, 0x21E1CDE6,
|
|
||||||
0xC33707D6, 0xF4D50D87, 0x455A14ED, 0xA9E3E905, 0xFCEFA3F8,
|
|
||||||
0x676F02D9, 0x8D2A4C8A, 0xFFFA3942, 0x8771F681, 0x6D9D6122,
|
|
||||||
0xFDE5380C, 0xA4BEEA44, 0x4BDECFA9, 0xF6BB4B60, 0xBEBFBC70,
|
|
||||||
0x289B7EC6, 0xEAA127FA, 0xD4EF3085, 0x04881D05, 0xD9D4D039,
|
|
||||||
0xE6DB99E5, 0x1FA27CF8, 0xC4AC5665, 0xF4292244, 0x432AFF97,
|
|
||||||
0xAB9423A7, 0xFC93A039, 0x655B59C3, 0x8F0CCC92, 0xFFEFF47D,
|
|
||||||
0x85845DD1, 0x6FA87E4F, 0xFE2CE6E0, 0xA3014314, 0x4E0811A1,
|
|
||||||
0xF7537E82, 0xBD3AF235, 0x2AD7D2BB, 0xEB86D391]
|
|
||||||
|
|
||||||
|
|
||||||
// The MD5 test suite from RFC 1321, appendix A.5
|
|
||||||
|
|
||||||
property r0 = test ""
|
|
||||||
== 0xd41d8cd98f00b204e9800998ecf8427e
|
|
||||||
|
|
||||||
property r1 = test "a"
|
|
||||||
== 0x0cc175b9c0f1b6a831c399e269772661
|
|
||||||
|
|
||||||
property r2 = test "abc"
|
|
||||||
== 0x900150983cd24fb0d6963f7d28e17f72
|
|
||||||
|
|
||||||
property r3 = test "message digest"
|
|
||||||
== 0xf96b697d7cb7938d525a2f31aaf161d0
|
|
||||||
|
|
||||||
property r4 = test "abcdefghijklmnopqrstuvwxyz"
|
|
||||||
== 0xc3fcd3d76192e4007dfb496cca67e13b
|
|
||||||
|
|
||||||
property r5 = test "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789"
|
|
||||||
== 0xd174ab98d277d9f5a5611c2c9f419d9f
|
|
||||||
|
|
||||||
property r6 = test "12345678901234567890123456789012345678901234567890123456789012345678901234567890"
|
|
||||||
== 0x57edf4a22be3c955ac49da2e2107b67a
|
|
||||||
|
|
||||||
alltests = r0 /\ r1 /\ r2 /\ r3 /\ r4 /\ r5 /\ r6
|
|
||||||
@ -1,88 +0,0 @@
|
|||||||
/*
|
|
||||||
* Copyright (c) 2004, 2013-2016 Galois, Inc.
|
|
||||||
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
||||||
*/
|
|
||||||
|
|
||||||
// Description of SHA1 at http://www.itl.nist.gov/fipspubs/fip180-4.htm
|
|
||||||
|
|
||||||
sha1 : {n} (width (8*n) <= 64) => [n][8] -> [160]
|
|
||||||
sha1 msg = sha1' pmsg
|
|
||||||
where
|
|
||||||
pmsg = pad(join(msg))
|
|
||||||
|
|
||||||
sha1' : {chunks} (fin chunks) => [chunks][512] -> [160]
|
|
||||||
sha1' pmsg = join (Hs!0)
|
|
||||||
where
|
|
||||||
Hs = [[0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476, 0xc3d2e1f0]] #
|
|
||||||
[ block(H, split(M))
|
|
||||||
| H <- Hs
|
|
||||||
| M <- pmsg
|
|
||||||
]
|
|
||||||
|
|
||||||
/*
|
|
||||||
As a summary, a "1" followed by m "0"s followed by a 64-
|
|
||||||
bit integer are appended to the end of the message to produce a
|
|
||||||
padded message of length 512 * n. The 64-bit integer is the length
|
|
||||||
of the original message. The padded message is then processed by the
|
|
||||||
SHA-1 as n 512-bit blocks.
|
|
||||||
*/
|
|
||||||
|
|
||||||
pad : {msgLen}
|
|
||||||
( fin msgLen
|
|
||||||
, 64 >= width msgLen // message width fits in a word
|
|
||||||
)
|
|
||||||
=> [msgLen] -> [(msgLen + 65) /^ 512][512]
|
|
||||||
pad msg = split (msg # [True] # (zero:[padLen]) # (`msgLen:[64]))
|
|
||||||
where type contentLen = msgLen + 65 // message + header
|
|
||||||
type padLen = (msgLen + 65) %^ 512
|
|
||||||
|
|
||||||
f : ([8], [32], [32], [32]) -> [32]
|
|
||||||
f (t, x, y, z) =
|
|
||||||
if (0 <= t) /\ (t <= 19) then (x && y) ^ (~x && z)
|
|
||||||
| (20 <= t) /\ (t <= 39) then x ^ y ^ z
|
|
||||||
| (40 <= t) /\ (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
|
|
||||||
| (60 <= t) /\ (t <= 79) then x ^ y ^ z
|
|
||||||
else error "f: t out of range"
|
|
||||||
|
|
||||||
Ks : [80][32]
|
|
||||||
Ks = [ 0x5a827999 | t <- [0..19] ]
|
|
||||||
# [ 0x6ed9eba1 | t <- [20..39] ]
|
|
||||||
# [ 0x8f1bbcdc | t <- [40..59] ]
|
|
||||||
# [ 0xca62c1d6 | t <- [60..79] ]
|
|
||||||
|
|
||||||
block : ([5][32], [16][32]) -> [5][32]
|
|
||||||
block ([H0, H1, H2, H3, H4], M) =
|
|
||||||
[(H0+As@80), (H1+Bs@80), (H2+Cs@80), (H3+Ds@80), (H4+Es@80)]
|
|
||||||
where
|
|
||||||
Ws : [80][32]
|
|
||||||
Ws = M # [ (W3 ^ W8 ^ W14 ^ W16) <<< 1
|
|
||||||
| W16 <- drop`{16 - 16} Ws
|
|
||||||
| W14 <- drop`{16 - 14} Ws
|
|
||||||
| W8 <- drop`{16 - 8} Ws
|
|
||||||
| W3 <- drop`{16 - 3} Ws
|
|
||||||
| t <- [16..79]
|
|
||||||
]
|
|
||||||
As = [H0] # TEMP
|
|
||||||
Bs = [H1] # As
|
|
||||||
Cs = [H2] # [ B <<< 30 | B <- Bs ]
|
|
||||||
Ds = [H3] # Cs
|
|
||||||
Es = [H4] # Ds
|
|
||||||
TEMP : [80][32]
|
|
||||||
TEMP = [ (A <<< 5) + f(t, B, C, D) + E + W + K
|
|
||||||
| A <- As | B <- Bs | C <- Cs | D <- Ds | E <- Es
|
|
||||||
| W <- Ws | K <- Ks
|
|
||||||
| t <- [0..79]
|
|
||||||
]
|
|
||||||
|
|
||||||
|
|
||||||
t0 = sha1 "" == 0xda39a3ee5e6b4b0d3255bfef95601890afd80709
|
|
||||||
|
|
||||||
// Sample messages and their digests from FIPS180-1 appendix.
|
|
||||||
|
|
||||||
t1 = sha1 "abc" == 0xA9993E364706816ABA3E25717850C26C9CD0D89D
|
|
||||||
t2 = sha1 "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" ==
|
|
||||||
0x84983E441C3BD26EBAAE4AA1F95129E5E54670F1
|
|
||||||
t3 = sha1 [ 'a' | i <- [1..1000000] ] ==
|
|
||||||
0x34AA973CD4C4DAA4F61EEB2BDBAD27316534016F
|
|
||||||
|
|
||||||
property testsPass = [t0, t1, t2, t3] == ~zero
|
|
||||||
@ -1,188 +0,0 @@
|
|||||||
/*
|
|
||||||
* Copyright (c) 2013-2016 Galois, Inc.
|
|
||||||
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
||||||
*
|
|
||||||
* @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}
|
|
||||||
( fin msgLen
|
|
||||||
, 64 >= width msgLen // message width fits in a word
|
|
||||||
)
|
|
||||||
=> [msgLen] -> [(msgLen + 65) /^ 512][512]
|
|
||||||
preprocess msg = split (msg # [True] # (zero:[(msgLen + 65) %^ 512]) # (`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])
|
|
||||||
|
|
||||||
SHA256Block : [8][32] -> [16][32] -> [8][32]
|
|
||||||
SHA256Block H M = SHA256Compress H (SHA256MessageSchedule M)
|
|
||||||
|
|
||||||
//////// Functional/idiomatic top level ////////
|
|
||||||
|
|
||||||
/*
|
|
||||||
* 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] # [SHA256Block h 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)
|
|
||||||
// , ([0x61 | i <- [1..1000000] : [_][32]]
|
|
||||||
// , 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0)
|
|
||||||
]
|
|
||||||
|
|
||||||
//////// Imperative top level ////////
|
|
||||||
|
|
||||||
type SHA256State = { h : [8][32]
|
|
||||||
, block : [64][8]
|
|
||||||
, n : [16]
|
|
||||||
, sz : [64]
|
|
||||||
}
|
|
||||||
|
|
||||||
SHA256Init : SHA256State
|
|
||||||
SHA256Init = { h = H0
|
|
||||||
, block = zero
|
|
||||||
, n = 0
|
|
||||||
, sz = 0
|
|
||||||
}
|
|
||||||
|
|
||||||
SHA256Update1 : SHA256State -> [8] -> SHA256State
|
|
||||||
SHA256Update1 s b =
|
|
||||||
if s.n == 64
|
|
||||||
then { h = SHA256Block s.h (split (join s.block))
|
|
||||||
, block = [b] # zero
|
|
||||||
, n = 1
|
|
||||||
, sz = s.sz + 8
|
|
||||||
}
|
|
||||||
else { h = s.h
|
|
||||||
, block = update s.block s.n b
|
|
||||||
, n = s.n + 1
|
|
||||||
, sz = s.sz + 8
|
|
||||||
}
|
|
||||||
|
|
||||||
SHA256Update : {n} (fin n) => SHA256State -> [n][8] -> SHA256State
|
|
||||||
SHA256Update sinit bs = ss!0
|
|
||||||
where ss = [sinit] # [ SHA256Update1 s b | s <- ss | b <- bs ]
|
|
||||||
|
|
||||||
// Add padding and size and process the final block.
|
|
||||||
SHA256Final : SHA256State -> [256]
|
|
||||||
SHA256Final s = join (SHA256Block h b')
|
|
||||||
// Because the message is always made up of bytes, and the size is a
|
|
||||||
// fixed number of bytes, the 1 pad will always be at least a byte.
|
|
||||||
where s' = SHA256Update1 s 0x80
|
|
||||||
// Don't need to add zeros. They're already there. Just update
|
|
||||||
// the count of bytes in this block. After adding the 1 pad, there
|
|
||||||
// are two possible cases: the size will fit in the current block,
|
|
||||||
// or it won't.
|
|
||||||
(h, b) = if s'.n <= 56 then (s'.h, s'.block)
|
|
||||||
else (SHA256Block s'.h (split (join s'.block)), zero)
|
|
||||||
b' = split (join b || (zero # s.sz))
|
|
||||||
|
|
||||||
SHA256Imp : {a} (64 >= width (8*a)) => [a][8] -> [256]
|
|
||||||
SHA256Imp msg = SHA256Final (SHA256Update SHA256Init msg)
|
|
||||||
|
|
||||||
property katsPassImp = ~zero == [test == kat | (test,kat) <- katsImp ]
|
|
||||||
|
|
||||||
katsImp = [ (SHA256Imp "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq", 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1), (SHA256Imp ""
|
|
||||||
, 0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855)
|
|
||||||
, (SHA256Imp "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
|
|
||||||
, 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1)
|
|
||||||
// , ([0x61 | i <- [1..1000000] : [_][32]]
|
|
||||||
// , 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0)
|
|
||||||
]
|
|
||||||
|
|
||||||
property imp_correct msg = SHA256 msg == SHA256Imp msg
|
|
||||||
File diff suppressed because it is too large
Load Diff
@ -1,182 +0,0 @@
|
|||||||
/*
|
|
||||||
* 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
|
|
||||||
|
|
||||||
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] ]
|
|
||||||
|
|
||||||
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] ])
|
|
||||||
|
|
||||||
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])
|
|
||||||
|
|
||||||
littleendian : [4][8] -> [32]
|
|
||||||
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
|
|
||||||
|
|
||||||
Salsa20 : [64][8] -> [64][8]
|
|
||||||
Salsa20 xs = join ar
|
|
||||||
where
|
|
||||||
ar = [ littleendian_inverse words | words <- xw + zs@10 ]
|
|
||||||
xw = [ littleendian xi | xi <- split xs ]
|
|
||||||
zs = [xw] # [ doubleround zi | zi <- zs ]
|
|
||||||
|
|
||||||
property Salsa20_passes_tests =
|
|
||||||
(Salsa20 [ 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 [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 [ 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 =
|
|
||||||
if(x1 != x2) then (doubleround x1) != (doubleround x2) else True
|
|
||||||
|
|
||||||
// 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) then s0 # k0 # s1 # n # s2 # k1 # s3
|
|
||||||
else t0 # k0 # t1 # n # t2 # k0 # t3
|
|
||||||
z = Salsa20(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#(reverse (split i))) | i <- [0, 1 ... ] ])
|
|
||||||
c = m ^ salsa
|
|
||||||
@ -1,208 +0,0 @@
|
|||||||
module Threefish where
|
|
||||||
|
|
||||||
// This implementation is based on Skein version 1.3:
|
|
||||||
// http://www.skein-hash.info/sites/default/files/skein1.3.pdf
|
|
||||||
|
|
||||||
//////////////////////////////////////////////////////////////////////
|
|
||||||
// Section 3.2: Bit and Byte Order
|
|
||||||
|
|
||||||
// "To convert from a sequence of bytes to an integer, we use the
|
|
||||||
// least-significant-byte-first convention."
|
|
||||||
|
|
||||||
ToInt : {n} (fin n) => [n][8] -> [8 * n]
|
|
||||||
ToInt bytes = join (reverse bytes)
|
|
||||||
|
|
||||||
ToBytes : {n} (fin n) => [8 * n] -> [n][8]
|
|
||||||
ToBytes bits = reverse (split`{each = 8} bits)
|
|
||||||
|
|
||||||
BytesToWords : {n} (fin n) => [8 * n][8] -> [n][64]
|
|
||||||
BytesToWords bytes = [ ToInt bs | bs <- split`{each = 8} bytes ]
|
|
||||||
|
|
||||||
WordsToBytes : {n} (fin n) => [n][64] -> [8 * n][8]
|
|
||||||
WordsToBytes words = join [ ToBytes w | w <- words ]
|
|
||||||
|
|
||||||
//////////////////////////////////////////////////////////////////////
|
|
||||||
// Section 3.3: A Full Specification of Threefish
|
|
||||||
|
|
||||||
enc256 = encrypt`{Nr=72} R4 pi4
|
|
||||||
enc512 = encrypt`{Nr=72} R8 pi8
|
|
||||||
enc1024 = encrypt`{Nr=80} R16 pi16
|
|
||||||
|
|
||||||
encrypt :
|
|
||||||
{Nr, Nw} (fin Nr, fin Nw, Nw >= 3, Nr % 4 == 0, Nw % 2 == 0) =>
|
|
||||||
[8][Nw/2]Rot ->
|
|
||||||
([Nw][64] -> [Nw][64]) ->
|
|
||||||
[8 * Nw][8] -> [16][8] -> [8 * Nw][8] -> [8 * Nw][8]
|
|
||||||
encrypt R pi key tweak plaintext = WordsToBytes (encrypt'`{Nr=Nr} R pi K T P)
|
|
||||||
where
|
|
||||||
K = BytesToWords key
|
|
||||||
T = BytesToWords tweak
|
|
||||||
P = BytesToWords plaintext
|
|
||||||
|
|
||||||
// Encryption in terms of 64-bit words.
|
|
||||||
encrypt' :
|
|
||||||
{Nr, Nw} (fin Nr, fin Nw, Nw >= 3, Nr % 4 == 0, Nw % 2 == 0) =>
|
|
||||||
[8][Nw/2]Rot -> ([Nw][64] -> [Nw][64]) ->
|
|
||||||
[Nw][64] -> [2][64] -> [Nw][64] -> [Nw][64]
|
|
||||||
encrypt' R pi key tweak plaintext = last v + last ks
|
|
||||||
where
|
|
||||||
ks : [Nr/4 + 1][Nw][64]
|
|
||||||
ks = KeySchedule key tweak
|
|
||||||
|
|
||||||
// Add a subkey from the key schedule once every four rounds.
|
|
||||||
e : [Nr][Nw][64]
|
|
||||||
e = [ vd + kd
|
|
||||||
| vd <- v
|
|
||||||
| subkey <- take`{Nr/4} ks, kd <- [subkey, zero, zero, zero] ]
|
|
||||||
|
|
||||||
// Cycle over the eight lists of rotation amounts for the mixing function.
|
|
||||||
f : [Nr][Nw][64]
|
|
||||||
f = [ mixing Rd ed | Rd <- join (repeat`{inf} R) | ed <- e ]
|
|
||||||
|
|
||||||
// Permute the words every round.
|
|
||||||
v : [Nr+1][Nw][64]
|
|
||||||
v = [plaintext] # [ pi fd | fd <- f ]
|
|
||||||
|
|
||||||
// One round of mixing.
|
|
||||||
mixing : {w} (fin w) => [w]Rot -> [2 * w][64] -> [2 * w][64]
|
|
||||||
mixing Rd e = join [ MIX R x | R <- Rd | x <- split`{each=2} e ]
|
|
||||||
|
|
||||||
// Table 3: Values for the word permutation π(i).
|
|
||||||
|
|
||||||
pi4 : [4][64] -> [4][64]
|
|
||||||
pi4 xs = xs @@ [0, 3, 2, 1:[2]]
|
|
||||||
|
|
||||||
pi8 : [8][64] -> [8][64]
|
|
||||||
pi8 xs = xs @@ [2, 1, 4, 7, 6, 5, 0, 3:[3]]
|
|
||||||
|
|
||||||
pi16 : [16][64] -> [16][64]
|
|
||||||
pi16 xs = xs @@ [0, 9, 2, 13, 6, 11, 4, 15, 10, 7, 12, 3, 14, 5, 8, 1:[4]]
|
|
||||||
|
|
||||||
//////////////////////////////////////////////////////////////////////
|
|
||||||
// Section 3.3.1: MIX Functions
|
|
||||||
|
|
||||||
// Rotation amount for a 64-bit word
|
|
||||||
type Rot = [6]
|
|
||||||
|
|
||||||
MIX : Rot -> [2][64] -> [2][64]
|
|
||||||
MIX R [x0, x1] = [y0, y1]
|
|
||||||
where
|
|
||||||
y0 = x0 + x1
|
|
||||||
y1 = (x1 <<< R) ^ y0
|
|
||||||
|
|
||||||
// Table 4: Rotation constants
|
|
||||||
|
|
||||||
R4 : [8][2]Rot
|
|
||||||
R4 =
|
|
||||||
[[14, 16],
|
|
||||||
[52, 57],
|
|
||||||
[23, 40],
|
|
||||||
[ 5, 37],
|
|
||||||
[25, 33],
|
|
||||||
[46, 12],
|
|
||||||
[58, 22],
|
|
||||||
[32, 32]]
|
|
||||||
|
|
||||||
R8 : [8][4]Rot
|
|
||||||
R8 =
|
|
||||||
[[46, 36, 19, 37],
|
|
||||||
[33, 27, 14, 42],
|
|
||||||
[17, 49, 36, 39],
|
|
||||||
[44, 9, 54, 56],
|
|
||||||
[39, 30, 34, 24],
|
|
||||||
[13, 50, 10, 17],
|
|
||||||
[25, 29, 39, 43],
|
|
||||||
[ 8, 35, 56, 22]]
|
|
||||||
|
|
||||||
R16 : [8][8]Rot
|
|
||||||
R16 =
|
|
||||||
[[24, 13, 8, 47, 8, 17, 22, 37],
|
|
||||||
[38, 19, 10, 55, 49, 18, 23, 52],
|
|
||||||
[33, 4, 51, 13, 34, 41, 59, 17],
|
|
||||||
[ 5, 20, 48, 41, 47, 28, 16, 25],
|
|
||||||
[41, 9, 37, 31, 12, 47, 44, 30],
|
|
||||||
[16, 34, 56, 51, 4, 53, 42, 41],
|
|
||||||
[31, 44, 47, 46, 19, 42, 44, 25],
|
|
||||||
[ 9, 48, 35, 52, 23, 31, 37, 20]]
|
|
||||||
|
|
||||||
|
|
||||||
//////////////////////////////////////////////////////////////////////
|
|
||||||
// Section 3.3.2: The Key Schedule
|
|
||||||
|
|
||||||
// "The key schedule turns the key and tweak into a sequence of Nr/4+1
|
|
||||||
// subkeys, each of which consists of Nw words."
|
|
||||||
|
|
||||||
KeySchedule :
|
|
||||||
{Nw, r} (fin Nw, fin r, Nw >= 3) =>
|
|
||||||
[Nw][64] -> [2][64] -> [r][Nw][64]
|
|
||||||
KeySchedule k [t0,t1] = take`{r} [ subkey s | s <- [0...] ]
|
|
||||||
where
|
|
||||||
k' = k # [foldl (^) C240 k]
|
|
||||||
t' = [t0, t1, t0 ^ t1]
|
|
||||||
|
|
||||||
subkey : [64] -> [Nw][64]
|
|
||||||
subkey s = take`{Nw} (k' <<< s) + tweak s
|
|
||||||
|
|
||||||
tweak : [64] -> [Nw][64]
|
|
||||||
tweak s = zero # take`{2} (t' <<< s) # [s]
|
|
||||||
|
|
||||||
C240 : [64]
|
|
||||||
C240 = 0x1BD11BDAA9FC1A22
|
|
||||||
|
|
||||||
|
|
||||||
//////////////////////////////////////////////////////////////////////
|
|
||||||
// Test Vectors
|
|
||||||
|
|
||||||
// https://sites.google.com/site/bartoszmalkowski/threefish
|
|
||||||
|
|
||||||
property test256a =
|
|
||||||
enc256 zero zero zero ==
|
|
||||||
split 0x84da2a1f8beaee947066ae3e3103f1ad536db1f4a1192495116b9f3ce6133fd8
|
|
||||||
|
|
||||||
property test256b =
|
|
||||||
enc256
|
|
||||||
(split 0x101112131415161718191a1b1c1d1e1f202122232425262728292a2b2c2d2e2f)
|
|
||||||
(split 0x000102030405060708090a0b0c0d0e0f)
|
|
||||||
(split 0xFFFEFDFCFBFAF9F8F7F6F5F4F3F2F1F0EFEEEDECEBEAE9E8E7E6E5E4E3E2E1E0)
|
|
||||||
==
|
|
||||||
split 0xe0d091ff0eea8fdfc98192e62ed80ad59d865d08588df476657056b5955e97df
|
|
||||||
|
|
||||||
property test512a =
|
|
||||||
enc512 zero zero zero ==
|
|
||||||
split 0xb1a2bbc6ef6025bc40eb3822161f36e375d1bb0aee3186fbd19e47c5d479947b #
|
|
||||||
split 0x7bc2f8586e35f0cff7e7f03084b0b7b1f1ab3961a580a3e97eb41ea14a6d7bbe
|
|
||||||
|
|
||||||
property test512b =
|
|
||||||
enc512
|
|
||||||
(split 0x101112131415161718191a1b1c1d1e1f202122232425262728292a2b2c2d2e2f #
|
|
||||||
split 0x303132333435363738393a3b3c3d3e3f404142434445464748494a4b4c4d4e4f)
|
|
||||||
(split 0x000102030405060708090a0b0c0d0e0f)
|
|
||||||
(split 0xfffefdfcfbfaf9f8f7f6f5f4f3f2f1f0efeeedecebeae9e8e7e6e5e4e3e2e1e0 #
|
|
||||||
split 0xdfdedddcdbdad9d8d7d6d5d4d3d2d1d0cfcecdcccbcac9c8c7c6c5c4c3c2c1c0)
|
|
||||||
==
|
|
||||||
split 0xe304439626d45a2cb401cad8d636249a6338330eb06d45dd8b36b90e97254779 #
|
|
||||||
split 0x272a0a8d99463504784420ea18c9a725af11dffea10162348927673d5c1caf3d
|
|
||||||
|
|
||||||
property test1024a =
|
|
||||||
enc1024 zero zero zero ==
|
|
||||||
split 0xf05c3d0a3d05b304f785ddc7d1e036015c8aa76e2f217b06c6e1544c0bc1a90d #
|
|
||||||
split 0xf0accb9473c24e0fd54fea68057f43329cb454761d6df5cf7b2e9b3614fbd5a2 #
|
|
||||||
split 0x0b2e4760b40603540d82eabc5482c171c832afbe68406bc39500367a592943fa #
|
|
||||||
split 0x9a5b4a43286ca3c4cf46104b443143d560a4b230488311df4feef7e1dfe8391e
|
|
||||||
|
|
||||||
property test1024b =
|
|
||||||
enc1024
|
|
||||||
(split 0x101112131415161718191a1b1c1d1e1f202122232425262728292a2b2c2d2e2f #
|
|
||||||
split 0x303132333435363738393a3b3c3d3e3f404142434445464748494a4b4c4d4e4f #
|
|
||||||
split 0x505152535455565758595a5b5c5d5e5f606162636465666768696a6b6c6d6e6f #
|
|
||||||
split 0x707172737475767778797a7b7c7d7e7f808182838485868788898a8b8c8d8e8f)
|
|
||||||
(split 0x000102030405060708090a0b0c0d0e0f)
|
|
||||||
(split 0xfffefdfcfbfaf9f8f7f6f5f4f3f2f1f0efeeedecebeae9e8e7e6e5e4e3e2e1e0 #
|
|
||||||
split 0xdfdedddcdbdad9d8d7d6d5d4d3d2d1d0cfcecdcccbcac9c8c7c6c5c4c3c2c1c0 #
|
|
||||||
split 0xbfbebdbcbbbab9b8b7b6b5b4b3b2b1b0afaeadacabaaa9a8a7a6a5a4a3a2a1a0 #
|
|
||||||
split 0x9f9e9d9c9b9a999897969594939291908f8e8d8c8b8a89888786858483828180)
|
|
||||||
==
|
|
||||||
split 0xa6654ddbd73cc3b05dd777105aa849bce49372eaaffc5568d254771bab85531c #
|
|
||||||
split 0x94f780e7ffaae430d5d8af8c70eebbe1760f3b42b737a89cb363490d670314bd #
|
|
||||||
split 0x8aa41ee63c2e1f45fbd477922f8360b388d6125ea6c7af0ad7056d01796e90c8 #
|
|
||||||
split 0x3313f4150a5716b30ed5f569288ae974ce2b4347926fce57de44512177dd7cde
|
|
||||||
@ -1,41 +0,0 @@
|
|||||||
/*
|
|
||||||
* Copyright (c) 2013-2016 Galois, Inc.
|
|
||||||
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
||||||
*/
|
|
||||||
|
|
||||||
module TripleDES where
|
|
||||||
|
|
||||||
import DES
|
|
||||||
|
|
||||||
blockEncrypt : ([64],[64],[64],[64]) -> [64]
|
|
||||||
blockEncrypt (k1,k2,k3,data) = result where
|
|
||||||
ex = DES.encrypt k1 data
|
|
||||||
dx = DES.decrypt k2 ex
|
|
||||||
result = DES.encrypt k3 dx
|
|
||||||
|
|
||||||
// Test vectors from NIST 800-67
|
|
||||||
|
|
||||||
Key1, Key2, Key3 : [64]
|
|
||||||
Key1 = 0x0123456789ABCDEF
|
|
||||||
Key2 = 0x23456789ABCDEF01
|
|
||||||
Key3 = 0x456789ABCDEF0123
|
|
||||||
|
|
||||||
P1, P2, P3 : [64]
|
|
||||||
PlainText = "The qufck brown fox jump"
|
|
||||||
// Yes, that's the correct phrase.. (see the 7th letter of the phrase).
|
|
||||||
// It's supposed to be "the quick..." but they made a mistake in transcribing
|
|
||||||
// the ASCII into hex.
|
|
||||||
[P1, P2, P3] = split`{3} (join PlainText)
|
|
||||||
|
|
||||||
// B.1
|
|
||||||
|
|
||||||
C1, C2, C3 : [64]
|
|
||||||
C1 = 0xA826FD8CE53B855F
|
|
||||||
C2 = 0xCCE21C8112256FE6
|
|
||||||
C3 = 0x68D5C05DD9B6B900
|
|
||||||
|
|
||||||
test_B1_1 = blockEncrypt (Key1, Key2, Key3, P1) == C1
|
|
||||||
test_B1_2 = blockEncrypt (Key1, Key2, Key3, P2) == C2
|
|
||||||
test_B1_3 = blockEncrypt (Key1, Key2, Key3, P3) == C3
|
|
||||||
|
|
||||||
property passesTests = [test_B1_1, test_B1_2, test_B1_3] == ~zero
|
|
||||||
308
examples/ZUC.cry
308
examples/ZUC.cry
@ -1,308 +0,0 @@
|
|||||||
// Copyright (c) 2011-2016 Galois, Inc.
|
|
||||||
// An implementation of ZUC, Version 1.5
|
|
||||||
|
|
||||||
// Version info: If the following variable is set to True, then we implement
|
|
||||||
// Version 1.5 of ZUC. Otherwise, version 1.4 is implemented. There are
|
|
||||||
// precisely two points in the implementation where the difference matters,
|
|
||||||
// search for occurrences of version1_5 to spot them.
|
|
||||||
|
|
||||||
// Note that the ZUC test vectors below will not work for version 1.4, as the
|
|
||||||
// old test vectors are no longer published.
|
|
||||||
|
|
||||||
version1_5 : Bit
|
|
||||||
version1_5 = True
|
|
||||||
|
|
||||||
// addition in GF(2^31-1) over a list of terms
|
|
||||||
add : {a} (fin a) => [a][31] -> [31]
|
|
||||||
add xs =
|
|
||||||
sums ! 0
|
|
||||||
where
|
|
||||||
sums =
|
|
||||||
[0] #
|
|
||||||
[plus (s, x) | s <- sums
|
|
||||||
| x <- xs]
|
|
||||||
// the binary addition specified in the note at the end of section 3.2
|
|
||||||
plus : ([31], [31]) -> [31]
|
|
||||||
plus (a, b) =
|
|
||||||
if sab @ 0 then sab' + 1 else sab'
|
|
||||||
where
|
|
||||||
sab : [32]
|
|
||||||
sab = ((zero : [1]) # a) + ((zero : [1]) # b)
|
|
||||||
sab' : [31]
|
|
||||||
sab' = drop sab
|
|
||||||
|
|
||||||
// The ZUC LFSR is 16 31-bit words
|
|
||||||
type LFSR = [16][31]
|
|
||||||
|
|
||||||
// Section 3.2
|
|
||||||
LFSRWithInitializationMode : ([31], LFSR) -> LFSR
|
|
||||||
LFSRWithInitializationMode (u, ss) =
|
|
||||||
ss @@ [1 .. 15] # [s16]
|
|
||||||
where
|
|
||||||
v = add [s <<< c | s <- ss @@ [15, 13, 10, 4, 0, 0]
|
|
||||||
| c <- [15, 17, 21, 20, 8, 0]]
|
|
||||||
vu = if version1_5 then add [v, u] else v ^ u
|
|
||||||
s16 = if vu == 0 then `0x7FFFFFFF else vu
|
|
||||||
|
|
||||||
// Section 3.2
|
|
||||||
LFSRWithWorkMode : LFSR -> LFSR
|
|
||||||
LFSRWithWorkMode ss =
|
|
||||||
ss @@ [1 .. 15] # [s16]
|
|
||||||
where
|
|
||||||
v = add [s <<< c | s <- ss @@ [15, 13, 10, 4, 0, 0]
|
|
||||||
| c <- [15, 17, 21, 20, 8, 0]]
|
|
||||||
s16 = if v == 0 then `0x7FFFFFFF else v
|
|
||||||
|
|
||||||
// Section 3.3
|
|
||||||
BitReorganization : LFSR -> [4][32]
|
|
||||||
BitReorganization ss =
|
|
||||||
[ hi s15 # lo s14
|
|
||||||
, lo s11 # hi s9
|
|
||||||
, lo s7 # hi s5
|
|
||||||
, lo s2 # hi s0]
|
|
||||||
where
|
|
||||||
lo : [31] -> [16]
|
|
||||||
hi : [31] -> [16]
|
|
||||||
lo x = x @@ [15 .. 30]
|
|
||||||
hi x = x @@ [0 .. 15]
|
|
||||||
[s0, s2, s5, s7, s9, s11, s14, s15] = ss @@ [0, 2, 5, 7, 9, 11, 14, 15]
|
|
||||||
|
|
||||||
// Section 3.4
|
|
||||||
F : ([3][32], [2][32]) -> ([32], [2][32])
|
|
||||||
F ([X0, X1, X2], [R1, R2]) =
|
|
||||||
(W, [R1', R2'])
|
|
||||||
where
|
|
||||||
W = (X0 ^ R1) + R2
|
|
||||||
W1 = R1 + X1
|
|
||||||
W2 = R2 ^ X2
|
|
||||||
[W1H, W1L] = split W1
|
|
||||||
[W2H, W2L] = split W2
|
|
||||||
R1' = S (L1 (W1L # W2H))
|
|
||||||
R2' = S (L2 (W2L # W1H))
|
|
||||||
|
|
||||||
// Section 3.4.1
|
|
||||||
S : [32] -> [32]
|
|
||||||
S X =
|
|
||||||
Y0 # Y1 # Y2 # Y3
|
|
||||||
where
|
|
||||||
[X0, X1, X2, X3] = split X
|
|
||||||
[Y0, Y1, Y2, Y3] = [S0 X0, S1 X1, S2 X2, S3 X3]
|
|
||||||
|
|
||||||
// Example 8
|
|
||||||
property example8 = S(0x12345678) == 0xF9C05A4E
|
|
||||||
|
|
||||||
S0 : [8] -> [8]
|
|
||||||
S1 : [8] -> [8]
|
|
||||||
S2 : [8] -> [8]
|
|
||||||
S3 : [8] -> [8]
|
|
||||||
S0 x = S0Table @ x
|
|
||||||
S1 x = S1Table @ x
|
|
||||||
S2 = S0
|
|
||||||
S3 = S1
|
|
||||||
|
|
||||||
// Table 3.1
|
|
||||||
S0Table : [256][8]
|
|
||||||
S0Table =
|
|
||||||
[0x3E, 0x72, 0x5B, 0x47, 0xCA, 0xE0, 0x00, 0x33, 0x04, 0xD1, 0x54,
|
|
||||||
0x98, 0x09, 0xB9, 0x6D, 0xCB, 0x7B, 0x1B, 0xF9, 0x32, 0xAF, 0x9D,
|
|
||||||
0x6A, 0xA5, 0xB8, 0x2D, 0xFC, 0x1D, 0x08, 0x53, 0x03, 0x90, 0x4D,
|
|
||||||
0x4E, 0x84, 0x99, 0xE4, 0xCE, 0xD9, 0x91, 0xDD, 0xB6, 0x85, 0x48,
|
|
||||||
0x8B, 0x29, 0x6E, 0xAC, 0xCD, 0xC1, 0xF8, 0x1E, 0x73, 0x43, 0x69,
|
|
||||||
0xC6, 0xB5, 0xBD, 0xFD, 0x39, 0x63, 0x20, 0xD4, 0x38, 0x76, 0x7D,
|
|
||||||
0xB2, 0xA7, 0xCF, 0xED, 0x57, 0xC5, 0xF3, 0x2C, 0xBB, 0x14, 0x21,
|
|
||||||
0x06, 0x55, 0x9B, 0xE3, 0xEF, 0x5E, 0x31, 0x4F, 0x7F, 0x5A, 0xA4,
|
|
||||||
0x0D, 0x82, 0x51, 0x49, 0x5F, 0xBA, 0x58, 0x1C, 0x4A, 0x16, 0xD5,
|
|
||||||
0x17, 0xA8, 0x92, 0x24, 0x1F, 0x8C, 0xFF, 0xD8, 0xAE, 0x2E, 0x01,
|
|
||||||
0xD3, 0xAD, 0x3B, 0x4B, 0xDA, 0x46, 0xEB, 0xC9, 0xDE, 0x9A, 0x8F,
|
|
||||||
0x87, 0xD7, 0x3A, 0x80, 0x6F, 0x2F, 0xC8, 0xB1, 0xB4, 0x37, 0xF7,
|
|
||||||
0x0A, 0x22, 0x13, 0x28, 0x7C, 0xCC, 0x3C, 0x89, 0xC7, 0xC3, 0x96,
|
|
||||||
0x56, 0x07, 0xBF, 0x7E, 0xF0, 0x0B, 0x2B, 0x97, 0x52, 0x35, 0x41,
|
|
||||||
0x79, 0x61, 0xA6, 0x4C, 0x10, 0xFE, 0xBC, 0x26, 0x95, 0x88, 0x8A,
|
|
||||||
0xB0, 0xA3, 0xFB, 0xC0, 0x18, 0x94, 0xF2, 0xE1, 0xE5, 0xE9, 0x5D,
|
|
||||||
0xD0, 0xDC, 0x11, 0x66, 0x64, 0x5C, 0xEC, 0x59, 0x42, 0x75, 0x12,
|
|
||||||
0xF5, 0x74, 0x9C, 0xAA, 0x23, 0x0E, 0x86, 0xAB, 0xBE, 0x2A, 0x02,
|
|
||||||
0xE7, 0x67, 0xE6, 0x44, 0xA2, 0x6C, 0xC2, 0x93, 0x9F, 0xF1, 0xF6,
|
|
||||||
0xFA, 0x36, 0xD2, 0x50, 0x68, 0x9E, 0x62, 0x71, 0x15, 0x3D, 0xD6,
|
|
||||||
0x40, 0xC4, 0xE2, 0x0F, 0x8E, 0x83, 0x77, 0x6B, 0x25, 0x05, 0x3F,
|
|
||||||
0x0C, 0x30, 0xEA, 0x70, 0xB7, 0xA1, 0xE8, 0xA9, 0x65, 0x8D, 0x27,
|
|
||||||
0x1A, 0xDB, 0x81, 0xB3, 0xA0, 0xF4, 0x45, 0x7A, 0x19, 0xDF, 0xEE,
|
|
||||||
0x78, 0x34, 0x60]
|
|
||||||
|
|
||||||
// Table 3.2
|
|
||||||
S1Table : [256][8]
|
|
||||||
S1Table =
|
|
||||||
[0x55, 0xC2, 0x63, 0x71, 0x3B, 0xC8, 0x47, 0x86, 0x9F, 0x3C, 0xDA,
|
|
||||||
0x5B, 0x29, 0xAA, 0xFD, 0x77, 0x8C, 0xC5, 0x94, 0x0C, 0xA6, 0x1A,
|
|
||||||
0x13, 0x00, 0xE3, 0xA8, 0x16, 0x72, 0x40, 0xF9, 0xF8, 0x42, 0x44,
|
|
||||||
0x26, 0x68, 0x96, 0x81, 0xD9, 0x45, 0x3E, 0x10, 0x76, 0xC6, 0xA7,
|
|
||||||
0x8B, 0x39, 0x43, 0xE1, 0x3A, 0xB5, 0x56, 0x2A, 0xC0, 0x6D, 0xB3,
|
|
||||||
0x05, 0x22, 0x66, 0xBF, 0xDC, 0x0B, 0xFA, 0x62, 0x48, 0xDD, 0x20,
|
|
||||||
0x11, 0x06, 0x36, 0xC9, 0xC1, 0xCF, 0xF6, 0x27, 0x52, 0xBB, 0x69,
|
|
||||||
0xF5, 0xD4, 0x87, 0x7F, 0x84, 0x4C, 0xD2, 0x9C, 0x57, 0xA4, 0xBC,
|
|
||||||
0x4F, 0x9A, 0xDF, 0xFE, 0xD6, 0x8D, 0x7A, 0xEB, 0x2B, 0x53, 0xD8,
|
|
||||||
0x5C, 0xA1, 0x14, 0x17, 0xFB, 0x23, 0xD5, 0x7D, 0x30, 0x67, 0x73,
|
|
||||||
0x08, 0x09, 0xEE, 0xB7, 0x70, 0x3F, 0x61, 0xB2, 0x19, 0x8E, 0x4E,
|
|
||||||
0xE5, 0x4B, 0x93, 0x8F, 0x5D, 0xDB, 0xA9, 0xAD, 0xF1, 0xAE, 0x2E,
|
|
||||||
0xCB, 0x0D, 0xFC, 0xF4, 0x2D, 0x46, 0x6E, 0x1D, 0x97, 0xE8, 0xD1,
|
|
||||||
0xE9, 0x4D, 0x37, 0xA5, 0x75, 0x5E, 0x83, 0x9E, 0xAB, 0x82, 0x9D,
|
|
||||||
0xB9, 0x1C, 0xE0, 0xCD, 0x49, 0x89, 0x01, 0xB6, 0xBD, 0x58, 0x24,
|
|
||||||
0xA2, 0x5F, 0x38, 0x78, 0x99, 0x15, 0x90, 0x50, 0xB8, 0x95, 0xE4,
|
|
||||||
0xD0, 0x91, 0xC7, 0xCE, 0xED, 0x0F, 0xB4, 0x6F, 0xA0, 0xCC, 0xF0,
|
|
||||||
0x02, 0x4A, 0x79, 0xC3, 0xDE, 0xA3, 0xEF, 0xEA, 0x51, 0xE6, 0x6B,
|
|
||||||
0x18, 0xEC, 0x1B, 0x2C, 0x80, 0xF7, 0x74, 0xE7, 0xFF, 0x21, 0x5A,
|
|
||||||
0x6A, 0x54, 0x1E, 0x41, 0x31, 0x92, 0x35, 0xC4, 0x33, 0x07, 0x0A,
|
|
||||||
0xBA, 0x7E, 0x0E, 0x34, 0x88, 0xB1, 0x98, 0x7C, 0xF3, 0x3D, 0x60,
|
|
||||||
0x6C, 0x7B, 0xCA, 0xD3, 0x1F, 0x32, 0x65, 0x04, 0x28, 0x64, 0xBE,
|
|
||||||
0x85, 0x9B, 0x2F, 0x59, 0x8A, 0xD7, 0xB0, 0x25, 0xAC, 0xAF, 0x12,
|
|
||||||
0x03, 0xE2, 0xF2]
|
|
||||||
|
|
||||||
// Section 3.4.2
|
|
||||||
L1 : [32] -> [32]
|
|
||||||
L1 X = X ^ X <<< 2 ^ X <<< 10 ^ X <<< 18 ^ X <<< 24
|
|
||||||
|
|
||||||
// Section 3.4.2
|
|
||||||
L2 : [32] -> [32]
|
|
||||||
L2 X = X ^ X <<< 8 ^ X <<< 14 ^ X <<< 22 ^ X <<< 30
|
|
||||||
|
|
||||||
// Section 3.5
|
|
||||||
LoadKey : ([128], [128]) -> LFSR
|
|
||||||
LoadKey (key, iv) =
|
|
||||||
[k # d # i | k <- ks
|
|
||||||
| i <- is
|
|
||||||
| d <- ds]
|
|
||||||
where
|
|
||||||
ks : [16][8]
|
|
||||||
ks = split key
|
|
||||||
is : [16][8]
|
|
||||||
is = split iv
|
|
||||||
ds : [16][15]
|
|
||||||
ds =
|
|
||||||
[ 0b100010011010111, 0b010011010111100
|
|
||||||
, 0b110001001101011, 0b001001101011110
|
|
||||||
, 0b101011110001001, 0b011010111100010
|
|
||||||
, 0b111000100110101, 0b000100110101111
|
|
||||||
, 0b100110101111000, 0b010111100010011
|
|
||||||
, 0b110101111000100, 0b001101011110001
|
|
||||||
, 0b101111000100110, 0b011110001001101
|
|
||||||
, 0b111100010011010, 0b100011110101100
|
|
||||||
]
|
|
||||||
|
|
||||||
type ZUC = (LFSR, [32], [32])
|
|
||||||
|
|
||||||
// Return an infinite sequence of ZUC states by applying the initialization step
|
|
||||||
// repeatedly. This is a generalization of section 3.6.1
|
|
||||||
InitializeZUC : ([128], [128]) -> [inf]ZUC
|
|
||||||
InitializeZUC (key, iv) =
|
|
||||||
outs
|
|
||||||
where
|
|
||||||
initLFSR = LoadKey (key, iv)
|
|
||||||
outs = [(initLFSR, 0, 0)] # [step out | out <- outs]
|
|
||||||
step (lfsr, R1, R2) =
|
|
||||||
(LFSRWithInitializationMode (drop (w >> 1), lfsr), R1', R2')
|
|
||||||
where
|
|
||||||
[X0, X1, X2, X3] = BitReorganization lfsr
|
|
||||||
(w', [R1', R2']) = F ([X0, X1, X2], [R1, R2])
|
|
||||||
w = if version1_5 then w' else w' ^ X3
|
|
||||||
|
|
||||||
// Section 3.6.2
|
|
||||||
WorkingStage : ZUC -> ZUC
|
|
||||||
WorkingStage (lfsr, R1, R2) =
|
|
||||||
(lfsr', R1', R2')
|
|
||||||
where
|
|
||||||
[X0, X1, X2, _] = BitReorganization lfsr
|
|
||||||
(_, [R1', R2']) = F ([X0, X1, X2], [R1, R2])
|
|
||||||
lfsr' = LFSRWithWorkMode lfsr
|
|
||||||
|
|
||||||
// Section 3.6.2
|
|
||||||
ProductionStage : ZUC -> ([32], ZUC)
|
|
||||||
ProductionStage (lfsr, R1, R2) =
|
|
||||||
(w ^ X3, (lfsr', R1', R2'))
|
|
||||||
where
|
|
||||||
[X0, X1, X2, X3] = BitReorganization lfsr
|
|
||||||
(w, [R1', R2']) = F ([X0, X1, X2], [R1, R2])
|
|
||||||
lfsr' = LFSRWithWorkMode lfsr
|
|
||||||
|
|
||||||
// ZUC API
|
|
||||||
ZUC : [128] -> [128] -> [inf][32]
|
|
||||||
ZUC key iv =
|
|
||||||
tail [w | (w, _) <- zucs]
|
|
||||||
where
|
|
||||||
initZuc = WorkingStage (InitializeZUC (key, iv) @ 32)
|
|
||||||
zucs = [(zero, initZuc)] # [ProductionStage zuc | (_, zuc) <- zucs]
|
|
||||||
|
|
||||||
// Test vectors
|
|
||||||
property ZUC_TestVectors =
|
|
||||||
t1 /\ t2 /\ t3 /\ t4
|
|
||||||
where
|
|
||||||
t1 = take (ZUC zero zero ) == [0x27BEDE74, 0x018082DA]
|
|
||||||
t2 = take (ZUC (~zero) (~zero)) == [0x0657CFA0, 0x7096398B]
|
|
||||||
t3 = take (ZUC (join [ 0x3D, 0x4C, 0x4B, 0xE9, 0x6A, 0x82, 0xFD, 0xAE
|
|
||||||
, 0xB5, 0x8F, 0x64, 0x1D, 0xB1, 0x7B, 0x45, 0x5B
|
|
||||||
])
|
|
||||||
(join [ 0x84, 0x31, 0x9A, 0xA8, 0xDE, 0x69, 0x15, 0xCA
|
|
||||||
, 0x1F, 0x6B, 0xDA, 0x6B, 0xFB, 0xD8, 0xC7, 0x66
|
|
||||||
])) == [0x14F1C272, 0x3279C419]
|
|
||||||
t4 = take ks # [ks @ 1999] == [0xED4400E7, 0x0633E5C5, 0x7A574CDB]
|
|
||||||
where
|
|
||||||
ks = ZUC (join [ 0x4D, 0x32, 0x0B, 0xFA, 0xD4, 0xC2, 0x85, 0xBF
|
|
||||||
, 0xD6, 0xB8, 0xBD, 0x00, 0xF3, 0x9D, 0x8B, 0x41
|
|
||||||
])
|
|
||||||
(join [ 0x52, 0x95, 0x9D, 0xAB, 0xA0, 0xBF, 0x17, 0x6E
|
|
||||||
, 0xCE, 0x2D, 0xC3, 0x15, 0x04, 0x9E, 0xB5, 0x74
|
|
||||||
])
|
|
||||||
|
|
||||||
// 3.3-3.6 of the implementor's test data document lists "LFSR-state at the
|
|
||||||
// beginning", which is immediately after running LoadKey.
|
|
||||||
property LoadKey_TestVectors =
|
|
||||||
[ LoadKey(k, iv) == lfsr0
|
|
||||||
| k <- ks
|
|
||||||
| iv <- ivs
|
|
||||||
| lfsr0 <- lfsr0s
|
|
||||||
] == ~0
|
|
||||||
where
|
|
||||||
ks = [ 0
|
|
||||||
, ~0
|
|
||||||
, 0x3d4c4be96a82fdaeb58f641db17b455b
|
|
||||||
, 0x4d320bfad4c285bfd6b8bd00f39d8b41
|
|
||||||
]
|
|
||||||
ivs = [ 0
|
|
||||||
, ~0
|
|
||||||
, 0x84319aa8de6915ca1f6bda6bfbd8c766
|
|
||||||
, 0x52959daba0bf176ece2dc315049eb574
|
|
||||||
]
|
|
||||||
lfsr0s = [ [ `0x0044d700, `0x0026bc00, `0x00626b00, `0x00135e00
|
|
||||||
, `0x00578900, `0x0035e200, `0x00713500, `0x0009af00
|
|
||||||
, `0x004d7800, `0x002f1300, `0x006bc400, `0x001af100
|
|
||||||
, `0x005e2600, `0x003c4d00, `0x00789a00, `0x0047ac00
|
|
||||||
]
|
|
||||||
, [ `0x7fc4d7ff, `0x7fa6bcff, `0x7fe26bff, `0x7f935eff
|
|
||||||
, `0x7fd789ff, `0x7fb5e2ff, `0x7ff135ff, `0x7f89afff
|
|
||||||
, `0x7fcd78ff, `0x7faf13ff, `0x7febc4ff, `0x7f9af1ff
|
|
||||||
, `0x7fde26ff, `0x7fbc4dff, `0x7ff89aff, `0x7fc7acff
|
|
||||||
]
|
|
||||||
, [ `0x1ec4d784, `0x2626bc31, `0x25e26b9a, `0x74935ea8
|
|
||||||
, `0x355789de, `0x4135e269, `0x7ef13515, `0x5709afca
|
|
||||||
, `0x5acd781f, `0x47af136b, `0x326bc4da, `0x0e9af16b
|
|
||||||
, `0x58de26fb, `0x3dbc4dd8, `0x22f89ac7, `0x2dc7ac66
|
|
||||||
]
|
|
||||||
, [ `0x26c4d752, `0x1926bc95, `0x05e26b9d, `0x7d135eab
|
|
||||||
, `0x6a5789a0, `0x6135e2bf, `0x42f13517, `0x5f89af6e
|
|
||||||
, `0x6b4d78ce, `0x5c2f132d, `0x5eebc4c3, `0x001af115
|
|
||||||
, `0x79de2604, `0x4ebc4d9e, `0x45f89ab5, `0x20c7ac74
|
|
||||||
]
|
|
||||||
]
|
|
||||||
|
|
||||||
|
|
||||||
// Collision attack on ZUC. Only version1.5 is resistant to it. Thus, the
|
|
||||||
// following theorem holds only when version1_5 is set to True.
|
|
||||||
//
|
|
||||||
// NB. We only compare the first output of the InitializeZUC sequence, as it
|
|
||||||
// cuts down on the problem size and is sufficient to ensure the iv's will be
|
|
||||||
// the same. That is, if this theorem fails, then so would the final iv's used
|
|
||||||
// by ZUC.
|
|
||||||
//
|
|
||||||
// Use a solver other than CVC4; Z3 and Boolector do it quickly.
|
|
||||||
property ZUC_isResistantToCollisionAttack k iv1 iv2 =
|
|
||||||
if iv1 != iv2
|
|
||||||
then InitializeZUC (k, iv1) @ 1 != InitializeZUC (k, iv2) @ 1
|
|
||||||
else True
|
|
||||||
@ -1,75 +0,0 @@
|
|||||||
/* Source:
|
|
||||||
Alexander Semenov
|
|
||||||
Institute for System Dynamics and Control Theory
|
|
||||||
Russian Academy of Sciences
|
|
||||||
*/
|
|
||||||
|
|
||||||
Bivium_stream : [93] -> [84] -> [inf]
|
|
||||||
Bivium_stream R1 R2 = stream
|
|
||||||
where
|
|
||||||
(stream, ra, rb) = shift_regs R1 R2
|
|
||||||
|
|
||||||
type N = 200
|
|
||||||
Bivium : ([93], [84]) -> [N]Bit
|
|
||||||
Bivium (reg1, reg2) = keystream
|
|
||||||
where
|
|
||||||
keystream = take`{N} (Bivium_stream reg1 reg2)
|
|
||||||
|
|
||||||
|
|
||||||
shift : {d} (fin d, d >=1) => [d] -> Bit -> [d]
|
|
||||||
shift fill bit = fills
|
|
||||||
where
|
|
||||||
fills = [bit]#(drop`{1} (fill >> 1))
|
|
||||||
|
|
||||||
|
|
||||||
shift_regs : {d,e} (fin d, fin e, d >=1, e >=1) => [d] -> [e] -> ([inf],[inf][d],[inf][e])
|
|
||||||
shift_regs r1 r2 = (stream, regA, regB)
|
|
||||||
where
|
|
||||||
s1 = [(f1 @ 65) ^ (f1 @ 92) | f1 <- regA]
|
|
||||||
s2 = [(f2 @ 68) ^ (f2 @ 83) | f2 <- regB]
|
|
||||||
|
|
||||||
stream = s1 ^ s2
|
|
||||||
t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) |
|
|
||||||
f2 <- regB |
|
|
||||||
f1 <- regA ]
|
|
||||||
t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f1 @ 68) |
|
|
||||||
f1 <- regA |
|
|
||||||
f2 <- regB ]
|
|
||||||
|
|
||||||
regA = [r1] # [shift f b| f <- regA | b <- t2]
|
|
||||||
regB = [r2] # [shift f b| f <- regB | b <- t1]
|
|
||||||
|
|
||||||
Bivium_alt : ([93], [84]) -> [N]Bit
|
|
||||||
Bivium_alt (r1, r2) = take`{N} (s1 ^ s2)
|
|
||||||
where
|
|
||||||
a_65 = drop`{27} a_92
|
|
||||||
a_68 = drop`{24} a_92
|
|
||||||
a_90 = drop`{2} a_92
|
|
||||||
a_91 = drop`{1} a_92
|
|
||||||
a_92 = reverse r1 # t2
|
|
||||||
|
|
||||||
b_68 = drop`{15} b_83
|
|
||||||
b_77 = drop`{6} b_83
|
|
||||||
b_81 = drop`{2} b_83
|
|
||||||
b_82 = drop`{1} b_83
|
|
||||||
b_83 = reverse r2 # t1
|
|
||||||
|
|
||||||
s1 = a_65 ^ a_92
|
|
||||||
s2 = b_68 ^ b_83
|
|
||||||
|
|
||||||
t1 = s1 ^ (a_90 && a_91) ^ b_77
|
|
||||||
t2 = s2 ^ (b_81 && b_82) ^ a_68
|
|
||||||
|
|
||||||
/*************************************************************/
|
|
||||||
|
|
||||||
iv1 = 0b111110000000101010100100010001000000101010100001011111111111111100100100111111111011111111111
|
|
||||||
iv2 = 0b000000000000000000001000000000000000000001000000000000000000001000000000000000000001
|
|
||||||
|
|
||||||
test_keystream = 0b01000010000100000101110001100011111101110101110111111110100001111111100110101001000010101100100010000100001100011100000010001001100101101001011101110100000001011010001101000011001000110011111010100110
|
|
||||||
|
|
||||||
|
|
||||||
suffix = 0b000000001000000000000000000001
|
|
||||||
property Bivium_correct = (Bivium(iv1, iv2)) == test_keystream
|
|
||||||
property Bivium_search (x, y) = (Bivium(x, y)) == test_keystream
|
|
||||||
property Bivium_search_with_suffix (x, y) = (Bivium(x, y#suffix)) == test_keystream
|
|
||||||
property Bivium_alt_equivalent r = Bivium_alt r == Bivium r
|
|
||||||
@ -1,181 +0,0 @@
|
|||||||
/*
|
|
||||||
* Copyright (c) 2013 David Lazar <lazard@galois.com>
|
|
||||||
*
|
|
||||||
* Permission is hereby granted, free of charge, to any person obtaining a copy
|
|
||||||
* of this software and associated documentation files (the "Software"), to deal
|
|
||||||
* in the Software without restriction, including without limitation the rights
|
|
||||||
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
|
||||||
* copies of the Software, and to permit persons to whom the Software is
|
|
||||||
* furnished to do so, subject to the following conditions:
|
|
||||||
*
|
|
||||||
* The above copyright notice and this permission notice shall be included in
|
|
||||||
* all copies or substantial portions of the Software.
|
|
||||||
*
|
|
||||||
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
|
||||||
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
|
||||||
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
|
||||||
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
|
||||||
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
|
||||||
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
|
|
||||||
* THE SOFTWARE.
|
|
||||||
*/
|
|
||||||
|
|
||||||
// Specification of the Keccak (SHA-3) hash function
|
|
||||||
// Author: David Lazar
|
|
||||||
|
|
||||||
SHA_3_224 M = take`{224} (Keccak `{r = 1152, c = 448} (M # 0b01))
|
|
||||||
SHA_3_256 M = take`{256} (Keccak `{r = 1088, c = 512} (M # 0b01))
|
|
||||||
SHA_3_384 M = take`{384} (Keccak `{r = 832, c = 768} (M # 0b01))
|
|
||||||
SHA_3_512 M = take`{512} (Keccak `{r = 576, c = 1024} (M # 0b01))
|
|
||||||
SHAKE128 M = Keccak`{r = 1344, c = 256} (M # 0b1111)
|
|
||||||
SHAKE256 M = Keccak`{r = 1088, c = 512} (M # 0b1111)
|
|
||||||
|
|
||||||
Keccak : {r, c, m}
|
|
||||||
( fin r, fin c, fin m
|
|
||||||
, r >= 1
|
|
||||||
, (r + c) % 25 == 0
|
|
||||||
, 64 >= (r + c) / 25
|
|
||||||
) => [m] -> [inf]
|
|
||||||
Keccak M = squeeze `{r = r} (absorb `{w = (r + c) / 25} Ps)
|
|
||||||
where Ps = pad `{r = r} M
|
|
||||||
|
|
||||||
squeeze : {r, w} (fin r, fin w, 64 >= w, r >= 0, 25 * w >= r) => [5][5][w] -> [inf]
|
|
||||||
squeeze A = take`{r} (flatten A) # squeeze`{r = r} (Keccak_f A)
|
|
||||||
|
|
||||||
absorb : {r, w, n} (fin r, fin w, fin n, 64 >= w, 25 * w >= r) => [n][r] -> [5][5][w]
|
|
||||||
absorb Ps = as ! 0
|
|
||||||
where
|
|
||||||
as = [zero] # [ Keccak_f `{w = w} (s ^ (unflatten p)) | s <- as | p <- Ps ]
|
|
||||||
|
|
||||||
pad : {r, m}
|
|
||||||
( fin r, fin m
|
|
||||||
, r >= 1
|
|
||||||
) => [m] -> [(m + 2) /^ r][r]
|
|
||||||
pad M = split (M # [True] # zero # [True])
|
|
||||||
|
|
||||||
Keccak_f : {w} (fin w, 64 >= w) => [5][5][w] -> [5][5][w]
|
|
||||||
Keccak_f A0 = rounds ! 0
|
|
||||||
where
|
|
||||||
rounds = [A0] # [ Round RC A | RC <- RCs`{w = w} | A <- rounds ]
|
|
||||||
|
|
||||||
Round : {w} (fin w) => [5][5][w] -> [5][5][w] -> [5][5][w]
|
|
||||||
Round RC A = ι RC (χ (π (ρ (θ A))))
|
|
||||||
|
|
||||||
θ : {w} (fin w) => [5][5][w] -> [5][5][w]
|
|
||||||
θ A = A'
|
|
||||||
where
|
|
||||||
C = [ xor a | a <- A ]
|
|
||||||
D = [ C @ x ^ (C @ y <<< 1)
|
|
||||||
| (x:[8]) <- [4,0,1,2,3]
|
|
||||||
| (y:[8]) <- [1,2,3,4,0]
|
|
||||||
]
|
|
||||||
A' = [ [ a ^ (D @ x) | a <- A @ x ] | (x:[8]) <- [0 .. 4] ]
|
|
||||||
|
|
||||||
ρ : {w} (fin w) => [5][5][w] -> [5][5][w]
|
|
||||||
ρ A = groupBy`{5} [ a <<< r | a <- join A | (r:[8]) <- R ]
|
|
||||||
where R = [00, 36, 03, 41, 18,
|
|
||||||
01, 44, 10, 45, 02,
|
|
||||||
62, 06, 43, 15, 61,
|
|
||||||
28, 55, 25, 21, 56,
|
|
||||||
27, 20, 39, 08, 14]
|
|
||||||
|
|
||||||
π : {w} (fin w) => [5][5][w] -> [5][5][w]
|
|
||||||
π A = groupBy`{5} [ A @ ((x + 3*y) % 5) @ x
|
|
||||||
| (x:[8]) <- [0..4], (y:[8]) <- [0..4]
|
|
||||||
]
|
|
||||||
|
|
||||||
χ : {w} (fin w) => [5][5][w] -> [5][5][w]
|
|
||||||
χ A = groupBy`{5} [ (A @ x @ y) ^ (~ A @ ((x + 1) % 5) @ y
|
|
||||||
&& A @ ((x + 2) % 5) @ y)
|
|
||||||
| (x:[8]) <- [0..4], (y:[8]) <- [0..4]
|
|
||||||
]
|
|
||||||
|
|
||||||
ι : {w} (fin w) => [5][5][w] -> [5][5][w] -> [5][5][w]
|
|
||||||
ι RC A = A ^ RC
|
|
||||||
|
|
||||||
RCs : {w, n} (fin w, fin n, 24 >= n, n == 12 + 2 * (lg2 w)) => [n][5][5][w]
|
|
||||||
RCs = take`{n} [ [[take`{w} RC] # zero] # zero | RC <- RCs64 ]
|
|
||||||
|
|
||||||
RCs64 : [24][64]
|
|
||||||
RCs64 = join (transpose [
|
|
||||||
[0x0000000000000001, 0x000000008000808B],
|
|
||||||
[0x0000000000008082, 0x800000000000008B],
|
|
||||||
[0x800000000000808A, 0x8000000000008089],
|
|
||||||
[0x8000000080008000, 0x8000000000008003],
|
|
||||||
[0x000000000000808B, 0x8000000000008002],
|
|
||||||
[0x0000000080000001, 0x8000000000000080],
|
|
||||||
[0x8000000080008081, 0x000000000000800A],
|
|
||||||
[0x8000000000008009, 0x800000008000000A],
|
|
||||||
[0x000000000000008A, 0x8000000080008081],
|
|
||||||
[0x0000000000000088, 0x8000000000008080],
|
|
||||||
[0x0000000080008009, 0x0000000080000001],
|
|
||||||
[0x000000008000000A, 0x8000000080008008]
|
|
||||||
])
|
|
||||||
|
|
||||||
unflatten : {r, w} (fin w, 25*w >= r) => [r] -> [5][5][w]
|
|
||||||
unflatten p = transpose (groupBy`{5} (reverse (groupBy`{w} (reverse (p # zero)))))
|
|
||||||
|
|
||||||
flatten : {w} (fin w) => [5][5][w] -> [5 * 5 * w]
|
|
||||||
flatten A = reverse (join (reverse (join (transpose A))))
|
|
||||||
|
|
||||||
xor : {a, b} (fin a) => [a][b] -> [b]
|
|
||||||
xor xs = xors ! 0
|
|
||||||
where xors = [zero] # [ x ^ z | x <- xs | z <- xors ]
|
|
||||||
|
|
||||||
property RC_correct i j =
|
|
||||||
(i:[8]) < 24 ==> (j:[8]) < 7 ==> RCs64@i!(2^^j - 1) == lfsr@(j + 7*i)
|
|
||||||
|
|
||||||
lfsr : [inf]
|
|
||||||
lfsr = [ p!0 | p <- ps ]
|
|
||||||
where
|
|
||||||
/* powers of x modulo m */
|
|
||||||
ps = [0x01] # [ pmod (pmult p 0b10) m | p <- ps ]
|
|
||||||
m = <| x^^8 + x^^6 + x^^5 + x^^4 + 1 |>
|
|
||||||
|
|
||||||
/* See https://keccak.team/files/Keccak-reference-3.0.pdf, Section 1.2 */
|
|
||||||
property unflatten_correct x y z p =
|
|
||||||
x < 5 ==> y < 5 ==> z < (64:[12]) ==>
|
|
||||||
p@((5*y + x)*64 + z) == unflatten`{1600,64} p @ x @ y ! z
|
|
||||||
|
|
||||||
property flatten_correct s =
|
|
||||||
unflatten`{1600,64} (flatten`{64} s) == s
|
|
||||||
|
|
||||||
/** Splits a list of bits into bytes, using little-endian bit order. **/
|
|
||||||
toBytes : {n} (fin n) => [8*n] -> [n][8]
|
|
||||||
toBytes s = reverse (split (reverse s))
|
|
||||||
|
|
||||||
/** Joins a list of bytes into a list of bits, using little-endian bit order. **/
|
|
||||||
fromBytes : {n} (fin n) => [n][8] -> [8*n]
|
|
||||||
fromBytes bs = reverse (join (reverse bs))
|
|
||||||
|
|
||||||
/*
|
|
||||||
Test vectors from
|
|
||||||
https://csrc.nist.gov/projects/cryptographic-standards-and-guidelines/example-values#aHashing
|
|
||||||
*/
|
|
||||||
|
|
||||||
property t1 = join (toBytes (SHA_3_224 [])) ==
|
|
||||||
0x6b4e03423667dbb73b6e15454f0eb1abd4597f9a1b078e3f5b5a6bc7
|
|
||||||
property t2 = join (toBytes (SHA_3_256 [])) ==
|
|
||||||
0xa7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a
|
|
||||||
property t3 = join (toBytes (SHA_3_384 [])) ==
|
|
||||||
0x0c63a75b845e4f7d01107d852e4c2485c51a50aaaa94fc61995e71bbee983a2ac3713831264adb47fb6bd1e058d5f004
|
|
||||||
property t4 = join (toBytes (SHA_3_512 [])) ==
|
|
||||||
0xa69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26
|
|
||||||
|
|
||||||
property u1 = join (toBytes (SHA_3_224 0b11001)) ==
|
|
||||||
0xffbad5da96bad71789330206dc6768ecaeb1b32dca6b3301489674ab
|
|
||||||
property u2 = join (toBytes (SHA_3_256 0b11001)) ==
|
|
||||||
0x7b0047cf5a456882363cbf0fb05322cf65f4b7059a46365e830132e3b5d957af
|
|
||||||
property u3 = join (toBytes (SHA_3_384 0b11001)) ==
|
|
||||||
0x737c9b491885e9bf7428e792741a7bf8dca9653471c3e148473f2c236b6a0a6455eb1dce9f779b4b6b237fef171b1c64
|
|
||||||
property u4 = join (toBytes (SHA_3_512 0b11001)) ==
|
|
||||||
0xa13e01494114c09800622a70288c432121ce70039d753cadd2e006e4d961cb27544c1481e5814bdceb53be6733d5e099795e5e81918addb058e22a9f24883f37
|
|
||||||
|
|
||||||
msg1600 : [1600]
|
|
||||||
msg1600 = join [ 0b11000101 | _ <- zero : [200] ]
|
|
||||||
|
|
||||||
property v1 = join (toBytes (SHA_3_224 msg1600)) ==
|
|
||||||
0x9376816aba503f72f96ce7eb65ac095deee3be4bf9bbc2a1cb7e11e0
|
|
||||||
|
|
||||||
property w1 = join (toBytes (SHA_3_224 (msg1600 # 0b11000))) ==
|
|
||||||
0x22d2f7bb0b173fd8c19686f9173166e3ee62738047d7eadd69efb228
|
|
||||||
@ -1,146 +0,0 @@
|
|||||||
/*
|
|
||||||
* Copyright (c) 2013-2016 Galois, Inc.
|
|
||||||
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
||||||
*/
|
|
||||||
|
|
||||||
/* Cryptol specification of the Simon block cipher
|
|
||||||
* Author: David Lazar
|
|
||||||
*/
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// parameters
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
module simon where
|
|
||||||
|
|
||||||
Simon32_64 = encrypt `{n=16,m=4,T=32,j=0}
|
|
||||||
Simon48_72 = encrypt `{n=24,m=3,T=36,j=0}
|
|
||||||
Simon48_96 = encrypt `{n=24,m=4,T=36,j=1}
|
|
||||||
Simon64_96 = encrypt `{n=32,m=3,T=42,j=2}
|
|
||||||
Simon64_128 = encrypt `{n=32,m=4,T=44,j=3}
|
|
||||||
Simon96_96 = encrypt `{n=48,m=2,T=52,j=2}
|
|
||||||
Simon96_144 = encrypt `{n=48,m=3,T=54,j=3}
|
|
||||||
Simon128_128 = encrypt `{n=64,m=2,T=68,j=2}
|
|
||||||
Simon128_192 = encrypt `{n=64,m=3,T=69,j=3}
|
|
||||||
Simon128_256 = encrypt `{n=64,m=4,T=72,j=4}
|
|
||||||
|
|
||||||
Simon32_64' = decrypt `{n=16,m=4,T=32,j=0}
|
|
||||||
Simon48_72' = decrypt `{n=24,m=3,T=36,j=0}
|
|
||||||
Simon48_96' = decrypt `{n=24,m=4,T=36,j=1}
|
|
||||||
Simon64_96' = decrypt `{n=32,m=3,T=42,j=2}
|
|
||||||
Simon64_128' = decrypt `{n=32,m=4,T=44,j=3}
|
|
||||||
Simon96_96' = decrypt `{n=48,m=2,T=52,j=2}
|
|
||||||
Simon96_144' = decrypt `{n=48,m=3,T=54,j=3}
|
|
||||||
Simon128_128' = decrypt `{n=64,m=2,T=68,j=2}
|
|
||||||
Simon128_192' = decrypt `{n=64,m=3,T=69,j=3}
|
|
||||||
Simon128_256' = decrypt `{n=64,m=4,T=72,j=4}
|
|
||||||
|
|
||||||
// check only a few of them for now
|
|
||||||
property correctSimon32_64 k b = Simon32_64' k (Simon32_64 k b) == b
|
|
||||||
property correctSimon64_96 k b = Simon64_96' k (Simon64_96 k b) == b
|
|
||||||
property correctSimon96_144 k b = Simon96_144' k (Simon96_144 k b) == b
|
|
||||||
property correctSimon128_128 k b = Simon128_128' k (Simon128_128 k b) == b
|
|
||||||
property correctSimon128_256 k b = Simon128_256' k (Simon128_256 k b) == b
|
|
||||||
|
|
||||||
property uniqueExpandSimon32_64 k1 k2 = (k1 == k2) || (expandKey `{n=16,m=4,T=32,j=0} k1 != expandKey `{n=16,m=4,T=32,j=0} k2)
|
|
||||||
property uniqueExpandSimon48_72 k1 k2 = (k1 == k2) || (expandKey `{n=24,m=3,T=36,j=0} k1 != expandKey `{n=24,m=3,T=36,j=0} k2)
|
|
||||||
property uniqueExpandSimon48_96 k1 k2 = (k1 == k2) || (expandKey `{n=24,m=4,T=36,j=1} k1 != expandKey `{n=24,m=4,T=36,j=1} k2)
|
|
||||||
property uniqueExpandSimon64_96 k1 k2 = (k1 == k2) || (expandKey `{n=32,m=3,T=42,j=2} k1 != expandKey `{n=32,m=3,T=42,j=2} k2)
|
|
||||||
property uniqueExpandSimon64_128 k1 k2 = (k1 == k2) || (expandKey `{n=32,m=4,T=44,j=3} k1 != expandKey `{n=32,m=4,T=44,j=3} k2)
|
|
||||||
property uniqueExpandSimon96_96 k1 k2 = (k1 == k2) || (expandKey `{n=48,m=2,T=52,j=2} k1 != expandKey `{n=48,m=2,T=52,j=2} k2)
|
|
||||||
property uniqueExpandSimon96_144 k1 k2 = (k1 == k2) || (expandKey `{n=48,m=3,T=54,j=3} k1 != expandKey `{n=48,m=3,T=54,j=3} k2)
|
|
||||||
property uniqueExpandSimon128_128 k1 k2 = (k1 == k2) || (expandKey `{n=64,m=2,T=68,j=2} k1 != expandKey `{n=64,m=2,T=68,j=2} k2)
|
|
||||||
property uniqueExpandSimon128_192 k1 k2 = (k1 == k2) || (expandKey `{n=64,m=3,T=69,j=3} k1 != expandKey `{n=64,m=3,T=69,j=3} k2)
|
|
||||||
property uniqueExpandSimon128_256 k1 k2 = (k1 == k2) || (expandKey `{n=64,m=4,T=72,j=4} k1 != expandKey `{n=64,m=4,T=72,j=4} k2)
|
|
||||||
|
|
||||||
// A weak key theorem would look something like:
|
|
||||||
// :prove exists (\k1 -> exists (\k2 -> forall (\x -> Simon32_64 k1 (Simon32_64 k2 x) != x)))
|
|
||||||
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// round function
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
R k (x, y) = (y ^ f x ^ k, x)
|
|
||||||
|
|
||||||
// inverse
|
|
||||||
R' k (x, y) = (y, x ^ f y ^ k)
|
|
||||||
|
|
||||||
f x = ((x <<< 1) && (x <<< 8)) ^ (x <<< 2)
|
|
||||||
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// encryption / decryption
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
encrypt : {n, m, T, j}
|
|
||||||
( fin n, fin m, fin T, fin j
|
|
||||||
, n >= 2, 4 >= m, T >= 4, T-1 >= m
|
|
||||||
) => [m][n] -> ([n], [n]) -> ([n], [n])
|
|
||||||
encrypt k0 b0 = bs ! 0
|
|
||||||
where
|
|
||||||
bs = [b0] # [ R k b | b <- bs | k <- ks ]
|
|
||||||
ks = expandKey `{n=n,m=m,T=T,j=j} (reverse k0)
|
|
||||||
|
|
||||||
decrypt : {n, m, T, j}
|
|
||||||
( fin n, fin m, fin T, fin j
|
|
||||||
, n >= 2, 4 >= m, T >= 4, T-1 >= m
|
|
||||||
) => [m][n] -> ([n], [n]) -> ([n], [n])
|
|
||||||
decrypt k0 b0 = bs ! 0
|
|
||||||
where
|
|
||||||
bs = [b0] # [ R' k b | b <- bs | k <- reverse ks ]
|
|
||||||
ks = expandKey `{n=n,m=m,T=T,j=j} (reverse k0)
|
|
||||||
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// key expansion
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
expandKey : {n, m, T, j}
|
|
||||||
( fin n, fin m, fin T, fin j
|
|
||||||
, n >= 2, 4 >= m, T >= 4, T-1 >= m
|
|
||||||
) => [m][n] -> [T][n]
|
|
||||||
expandKey k0 = k
|
|
||||||
where
|
|
||||||
k = k0 # [ r where
|
|
||||||
o = k @ (i - 1) >>> 3
|
|
||||||
p = if `m == 4 then o ^ k @ (i - 3) else o
|
|
||||||
q = p ^ p >>> 1
|
|
||||||
r = ~ k @ (i - `m) ^ q ^ z ^ 3
|
|
||||||
z = Z @ `j @ ((i - `m) % 62)
|
|
||||||
| i <- [m .. T - 1]
|
|
||||||
]
|
|
||||||
|
|
||||||
// TODO specify how Z is constructed
|
|
||||||
Z = [[1, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0, 1, 1, 0,
|
|
||||||
0, 0, 0, 1, 1, 1, 0, 0, 1, 1, 0, 1, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1,
|
|
||||||
0, 0, 1, 0, 1, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 0, 0, 1, 1, 0],
|
|
||||||
[1, 0, 0, 0, 1, 1, 1, 0, 1, 1, 1, 1, 1, 0, 0, 1, 0, 0, 1, 1, 0, 0,
|
|
||||||
0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 0, 1, 1, 1, 1, 1,
|
|
||||||
0, 0, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 0, 1, 1, 0, 1, 0],
|
|
||||||
[1, 0, 1, 0, 1, 1, 1, 1, 0, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 1,
|
|
||||||
0, 0, 1, 0, 0, 1, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 1,
|
|
||||||
1, 1, 1, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 1, 0, 0, 1, 1],
|
|
||||||
[1, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1,
|
|
||||||
0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0,
|
|
||||||
0, 1, 1, 1, 0, 0, 1, 1, 0, 1, 0, 0, 0, 0, 1, 1, 1, 1],
|
|
||||||
[1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1,
|
|
||||||
1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 1, 1, 1, 0, 0, 0, 0, 1, 1,
|
|
||||||
0, 0, 1, 0, 1, 0, 0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 1, 1]]
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// tests
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
tests = [t00, t01,t02,t03,t04,t05,t06,t07,t08,t09]
|
|
||||||
property testsPass = tests == ~zero
|
|
||||||
|
|
||||||
t00 = Simon32_64 [0x1918, 0x1110, 0x0908, 0x0100] (0x6565, 0x6877) == (0xc69b, 0xe9bb)
|
|
||||||
t01 = Simon48_72 [0x121110, 0x0a0908, 0x020100] (0x612067, 0x6e696c) == (0xdae5ac, 0x292cac)
|
|
||||||
t02 = Simon48_96 [0x1a1918, 0x121110, 0x0a0908, 0x020100] (0x726963, 0x20646e) == (0x6e06a5, 0xacf156)
|
|
||||||
t03 = Simon64_96 [0x13121110, 0x0b0a0908, 0x03020100] (0x6f722067, 0x6e696c63) == (0x5ca2e27f, 0x111a8fc8)
|
|
||||||
t04 = Simon64_128 [0x1b1a1918, 0x13121110, 0x0b0a0908, 0x03020100] (0x656b696c, 0x20646e75) == (0x44c8fc20, 0xb9dfa07a)
|
|
||||||
t05 = Simon96_96 [0x0d0c0b0a0908, 0x050403020100] (0x2072616c6c69, 0x702065687420) == (0x602807a462b4, 0x69063d8ff082)
|
|
||||||
t06 = Simon96_144 [0x151413121110, 0x0d0c0b0a0908, 0x050403020100] (0x746168742074, 0x73756420666f) == (0xecad1c6c451e, 0x3f59c5db1ae9)
|
|
||||||
t07 = Simon128_128 [0x0f0e0d0c0b0a0908, 0x0706050403020100] (0x6373656420737265, 0x6c6c657661727420) == (0x49681b1e1e54fe3f, 0x65aa832af84e0bbc)
|
|
||||||
t08 = Simon128_192 [0x1716151413121110, 0x0f0e0d0c0b0a0908, 0x0706050403020100] (0x206572656874206e, 0x6568772065626972) == (0xc4ac61effcdc0d4f, 0x6c9c8d6e2597b85b)
|
|
||||||
t09 = Simon128_256 [0x1f1e1d1c1b1a1918, 0x1716151413121110, 0x0f0e0d0c0b0a0908, 0x0706050403020100] (0x74206e69206d6f6f, 0x6d69732061207369) == (0x8d2b5579afc8a3a0, 0x3bf72a87efe7b868)
|
|
||||||
@ -1,121 +0,0 @@
|
|||||||
/*
|
|
||||||
* Copyright (c) 2013-2016 Galois, Inc.
|
|
||||||
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
||||||
*/
|
|
||||||
|
|
||||||
/* Cryptol specification of the Speck block cipher
|
|
||||||
* Author: David Lazar
|
|
||||||
*/
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// parameters
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
Speck32_64 = encrypt`{n = 16, m = 4, T = 22}
|
|
||||||
Speck48_72 = encrypt`{n = 24, m = 3, T = 22}
|
|
||||||
Speck48_96 = encrypt`{n = 24, m = 4, T = 23}
|
|
||||||
Speck64_96 = encrypt`{n = 32, m = 3, T = 26}
|
|
||||||
Speck64_128 = encrypt`{n = 32, m = 4, T = 27}
|
|
||||||
Speck96_96 = encrypt`{n = 48, m = 2, T = 28}
|
|
||||||
Speck96_144 = encrypt`{n = 48, m = 3, T = 29}
|
|
||||||
Speck128_128 = encrypt`{n = 64, m = 2, T = 32}
|
|
||||||
Speck128_192 = encrypt`{n = 64, m = 3, T = 33}
|
|
||||||
Speck128_256 = encrypt`{n = 64, m = 4, T = 34}
|
|
||||||
|
|
||||||
Speck32_64' = decrypt`{n = 16, m = 4, T = 22}
|
|
||||||
Speck48_72' = decrypt`{n = 24, m = 3, T = 22}
|
|
||||||
Speck48_96' = decrypt`{n = 24, m = 4, T = 23}
|
|
||||||
Speck64_96' = decrypt`{n = 32, m = 3, T = 26}
|
|
||||||
Speck64_128' = decrypt`{n = 32, m = 4, T = 27}
|
|
||||||
Speck96_96' = decrypt`{n = 48, m = 2, T = 28}
|
|
||||||
Speck96_144' = decrypt`{n = 48, m = 3, T = 29}
|
|
||||||
Speck128_128' = decrypt`{n = 64, m = 2, T = 32}
|
|
||||||
Speck128_192' = decrypt`{n = 64, m = 3, T = 33}
|
|
||||||
Speck128_256' = decrypt`{n = 64, m = 4, T = 34}
|
|
||||||
|
|
||||||
// check only a few of them for now
|
|
||||||
property correctSpeck32_64 (k, b) = Speck32_64' k (Speck32_64 k b) == b
|
|
||||||
property correctSpeck64_96 (k, b) = Speck64_96' k (Speck64_96 k b) == b
|
|
||||||
property correctSpeck96_144 (k, b) = Speck96_144' k (Speck96_144 k b) == b
|
|
||||||
property correctSpeck128_128 (k, b) = Speck128_128' k (Speck128_128 k b) == b
|
|
||||||
property correctSpeck128_256 (k, b) = Speck128_256' k (Speck128_256 k b) == b
|
|
||||||
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// round function
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
R : {n} (fin n) => [n] -> ([n], [n]) -> ([n], [n])
|
|
||||||
R k (x, y) = f2 (f1 k (x, y))
|
|
||||||
|
|
||||||
R' : {n} (fin n) => [n] -> ([n], [n]) -> ([n], [n])
|
|
||||||
R' k (x, y) = ((x ^ k) - z <<< (if `n == 16 then 7 else 8), z)
|
|
||||||
where z = (x ^ y) >>> (if `n == 16 then 2 else 3)
|
|
||||||
|
|
||||||
f1 : {n} (fin n) => [n] -> ([n], [n]) -> ([n], [n])
|
|
||||||
f1 k (x, y) = (y, (x >>> (if `n == 16 then 7 else 8)) + y ^ k)
|
|
||||||
|
|
||||||
f2 : {n} (fin n) => ([n], [n]) -> ([n], [n])
|
|
||||||
f2 (x, y) = (y, x <<< (if `n == 16 then 2 else 3) ^ y)
|
|
||||||
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// encryption / decryption
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
encrypt : {n, m, T}
|
|
||||||
( fin n, fin m, fin T
|
|
||||||
, m >= 2, T >= 2, n >= 2
|
|
||||||
, n >= width (T-2)
|
|
||||||
) => [m][n] -> ([n], [n]) -> ([n], [n])
|
|
||||||
encrypt k0 b0 = bs ! 0
|
|
||||||
where
|
|
||||||
bs = [b0] # [R k b | b <- bs | k <- ks]
|
|
||||||
ks = expandKey`{n = n, m = m, T = T} (reverse k0)
|
|
||||||
|
|
||||||
|
|
||||||
decrypt : {n, m, T}
|
|
||||||
( fin n, fin m, fin T
|
|
||||||
, m >= 2, T >= 2, n >= 2
|
|
||||||
, n >= width (T-2)
|
|
||||||
) => [m][n] -> ([n], [n]) -> ([n], [n])
|
|
||||||
decrypt k0 b0 = bs ! 0
|
|
||||||
where
|
|
||||||
bs = [b0] # [R' k b | b <- bs | k <- reverse ks]
|
|
||||||
ks = expandKey`{n = n, m = m, T = T} (reverse k0)
|
|
||||||
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// key expansion
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
expandKey : {n, m, T}
|
|
||||||
( fin n, fin m, fin T
|
|
||||||
, m >= 2, n >= 2, T >= 2
|
|
||||||
, n >= width (T-2)
|
|
||||||
) => [m][n] -> [T][n]
|
|
||||||
expandKey K = ks
|
|
||||||
where
|
|
||||||
ls = drop`{1} K # [snd (f1 i (l, k)) | l <- ls | k <- ks | i <- [0 .. T - 2]]
|
|
||||||
ks = take`{1} K # [snd (f2 (k, l)) | l <- drop`{m - 1} ls | k <- ks]
|
|
||||||
snd (x, y) = y
|
|
||||||
|
|
||||||
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
// tests
|
|
||||||
///////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
property testsPass = tests == ~zero
|
|
||||||
|
|
||||||
tests = [t01, t02, t03, t04, t05, t06, t07, t08, t09]
|
|
||||||
|
|
||||||
t00 = Speck32_64 [0x1918, 0x1110, 0x0908, 0x0100] (0x6574, 0x694C) == (0xA868, 0x42F2)
|
|
||||||
t01 = Speck48_72 [0x121110, 0x0A0908, 0x020100] (0x20796C, 0x6C6172) == (0xC049A5, 0x385ADC)
|
|
||||||
t02 = Speck48_96 [0x1A1918, 0x121110, 0x0A0908, 0x020100] (0x6D2073, 0x696874) == (0x735E10, 0xB6445D)
|
|
||||||
t03 = Speck64_96 [0x13121110, 0x0B0A0908, 0x03020100] (0x74614620, 0x736E6165) == (0x9F7952EC, 0x4175946C)
|
|
||||||
t04 = Speck64_128 [0x1B1A1918, 0x13121110, 0x0B0A0908, 0x03020100] (0x3B726574, 0x7475432D) == (0x8C6FA548, 0x454E028B)
|
|
||||||
t05 = Speck96_96 [0x0D0C0B0A0908, 0x050403020100] (0x65776F68202C, 0x656761737520) == (0x9E4D09AB7178, 0x62BDDE8F79AA)
|
|
||||||
t06 = Speck96_144 [0x151413121110, 0x0D0C0B0A0908, 0x050403020100] (0x656D6974206E, 0x69202C726576) == (0x2BF31072228A, 0x7AE440252EE6)
|
|
||||||
t07 = Speck128_128 [0x0F0E0D0C0B0A0908, 0x0706050403020100] (0x6C61766975716520, 0x7469206564616D20) == (0xA65D985179783265, 0x7860FEDF5C570D18)
|
|
||||||
t08 = Speck128_192 [0x1716151413121110, 0x0F0E0D0C0B0A0908, 0x0706050403020100] (0x7261482066656968, 0x43206F7420746E65) == (0x1BE4CF3A13135566, 0xF9BC185DE03C1886)
|
|
||||||
t09 = Speck128_256 [0x1F1E1D1C1B1A1918, 0x1716151413121110, 0x0F0E0D0C0B0A0908, 0x0706050403020100] (0x65736F6874206E49, 0x202E72656E6F6F70) == (0x4109010405C0F53E, 0x4EEEB48D9C188F43)
|
|
||||||
@ -1,87 +0,0 @@
|
|||||||
/* Source:
|
|
||||||
Alexander Semenov
|
|
||||||
Institute for System Dynamics and Control Theory
|
|
||||||
Russian Academy of Sciences
|
|
||||||
*/
|
|
||||||
|
|
||||||
Trivium_stream : [93] -> [84] -> [111] -> [inf]
|
|
||||||
Trivium_stream R1 R2 R3 = stream
|
|
||||||
where
|
|
||||||
(stream, ra, rb, rc) = shift_regs R1 R2 R3
|
|
||||||
|
|
||||||
type N = 300
|
|
||||||
Trivium : ([93], [84], [111]) -> [N]Bit
|
|
||||||
Trivium (reg1, reg2, reg3) = keystream
|
|
||||||
where
|
|
||||||
keystream = take`{N} (Trivium_stream reg1 reg2 reg3)
|
|
||||||
|
|
||||||
shift : {d} (fin d, d >=1) => [d] -> Bit -> [d]
|
|
||||||
shift fill bit = fills
|
|
||||||
where
|
|
||||||
fills = [bit]#(drop`{1} (fill >> 1))
|
|
||||||
|
|
||||||
|
|
||||||
shift_regs : {d,e,f} (fin d, fin e, fin f, d >=1, e >=1, f>=1) => [d] -> [e] -> [f] -> ([inf],[inf][d],[inf][e],[inf][f])
|
|
||||||
shift_regs r1 r2 r3 = (stream, regA, regB, regC)
|
|
||||||
where
|
|
||||||
|
|
||||||
s1 = [(f1 @ 65) ^ (f1 @ 92) | f1 <- regA]
|
|
||||||
s2 = [(f2 @ 68) ^ (f2 @ 83) | f2 <- regB]
|
|
||||||
s3 = [(f3 @ 65) ^ (f3 @ 110) | f3 <- regC]
|
|
||||||
|
|
||||||
stream = s1 ^ s2 ^ s3
|
|
||||||
t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) |
|
|
||||||
f2 <- regB |
|
|
||||||
f1 <- regA ]
|
|
||||||
t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f3 @ 86) |
|
|
||||||
f2 <- regB |
|
|
||||||
f3 <- regC ]
|
|
||||||
t3 = [(f3 @ 65) ^ ((f3 @ 108) && (f3 @ 109)) ^ (f3 @ 110) ^ (f1 @ 68)|
|
|
||||||
f1 <- regA |
|
|
||||||
f3 <- regC ]
|
|
||||||
|
|
||||||
regA = [r1] # [shift f b| f <- regA | b <- t3]
|
|
||||||
regB = [r2] # [shift f b| f <- regB | b <- t1]
|
|
||||||
regC = [r3] # [shift f b| f <- regC | b <- t2]
|
|
||||||
|
|
||||||
Trivium_alt : ([93], [84], [111]) -> [N]Bit
|
|
||||||
Trivium_alt (r1, r2, r3) = take`{N} (s1 ^ s2 ^ s3)
|
|
||||||
where
|
|
||||||
a_65 = drop`{27} a_92
|
|
||||||
a_68 = drop`{24} a_92
|
|
||||||
a_90 = drop`{2} a_92
|
|
||||||
a_91 = drop`{1} a_92
|
|
||||||
a_92 = reverse r1 # t3
|
|
||||||
|
|
||||||
b_68 = drop`{15} b_83
|
|
||||||
b_77 = drop`{6} b_83
|
|
||||||
b_81 = drop`{2} b_83
|
|
||||||
b_82 = drop`{1} b_83
|
|
||||||
b_83 = reverse r2 # t1
|
|
||||||
|
|
||||||
c_65 = drop`{45} c_110
|
|
||||||
c_86 = drop`{24} c_110
|
|
||||||
c_108 = drop`{2} c_110
|
|
||||||
c_109 = drop`{1} c_110
|
|
||||||
c_110 = reverse r3 # t2
|
|
||||||
|
|
||||||
s1 = a_65 ^ a_92
|
|
||||||
s2 = b_68 ^ b_83
|
|
||||||
s3 = c_65 ^ c_110
|
|
||||||
|
|
||||||
t1 = s1 ^ (a_90 && a_91) ^ b_77
|
|
||||||
t2 = s2 ^ (b_81 && b_82) ^ c_86
|
|
||||||
t3 = s3 ^ (c_108 && c_109) ^ a_68
|
|
||||||
|
|
||||||
/*********************************************************/
|
|
||||||
|
|
||||||
iv1 = 0b111111111111111111101111111111111111111011111111111111111110111111111111111111101111111111111
|
|
||||||
iv2 = 0b000000000000000000001000000000000000000001000000000000000000001000000000000000000001
|
|
||||||
iv3 = 0b111111111111111110111111111111111111101111111111111111111011111111111111111110111111111111100000000000000000000
|
|
||||||
|
|
||||||
test_keystream = 0b011111110111101111110100001110000000000000100010000000000000000100011000101100001110001011011010101010000100101110001111100011000110000101001011001111011101110110111010011011010110001000111101101111101100101001000111010001010011111110011100100011101010011110101001001000011100001111111100000001110001
|
|
||||||
|
|
||||||
property Trivium_correct = (Trivium(iv1, iv2, iv3)) == test_keystream
|
|
||||||
property Trivium_search (x, y, z) = (Trivium(x, y, z)) == test_keystream
|
|
||||||
property Trivium_alt_correct = (Trivium_alt(iv1, iv2, iv3)) == test_keystream
|
|
||||||
property Trivium_alt_equivalent x = take`{200}(Trivium_alt x) == take (Trivium x)
|
|
||||||
@ -6,18 +6,8 @@
|
|||||||
:l Cipher.cry
|
:l Cipher.cry
|
||||||
:l DES.cry
|
:l DES.cry
|
||||||
:l DEStest.cry
|
:l DEStest.cry
|
||||||
:l FNV-a1.cry
|
|
||||||
:l HMAC.cry
|
|
||||||
:l Karatsuba.cry
|
:l Karatsuba.cry
|
||||||
:l MD5.cry
|
|
||||||
:l SHA1.cry
|
|
||||||
:l SHA256.cry
|
|
||||||
:l SIV-rfc5297.md
|
|
||||||
:l Salsa20.cry
|
|
||||||
:l Test.cry
|
:l Test.cry
|
||||||
:l Threefish.cry
|
|
||||||
:l TripleDES.cry
|
|
||||||
:l ZUC.cry
|
|
||||||
:l append.cry
|
:l append.cry
|
||||||
:l builtin_lifting.cry
|
:l builtin_lifting.cry
|
||||||
:l builtins.cry
|
:l builtins.cry
|
||||||
@ -36,12 +26,7 @@
|
|||||||
:l contrib/EvenMansour.cry
|
:l contrib/EvenMansour.cry
|
||||||
:l contrib/MISTY1.cry
|
:l contrib/MISTY1.cry
|
||||||
:l contrib/RC4.cry
|
:l contrib/RC4.cry
|
||||||
:l contrib/bivium.cry
|
|
||||||
:l contrib/keccak.cry
|
|
||||||
:l contrib/mkrand.cry
|
:l contrib/mkrand.cry
|
||||||
:l contrib/simon.cry
|
|
||||||
:l contrib/speck.cry
|
|
||||||
:l contrib/trivium.cry
|
|
||||||
:l funstuff/Coins.cry
|
:l funstuff/Coins.cry
|
||||||
:l funstuff/FoxChickenCorn.cry
|
:l funstuff/FoxChickenCorn.cry
|
||||||
:l funstuff/NQueens.cry
|
:l funstuff/NQueens.cry
|
||||||
|
|||||||
@ -26,39 +26,11 @@ Loading module DES
|
|||||||
Loading module Test
|
Loading module Test
|
||||||
Loading module DEStest
|
Loading module DEStest
|
||||||
Loading module Cryptol
|
Loading module Cryptol
|
||||||
Loading module Main
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module SHA256
|
|
||||||
Loading module HMAC
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Karatsuba
|
Loading module Karatsuba
|
||||||
Loading module Cryptol
|
Loading module Cryptol
|
||||||
Loading module Main
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Main
|
|
||||||
[warning] at ./SHA1.cry:36:16--36:26 Unused name: contentLen
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module SHA256
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module AES
|
|
||||||
Loading module SIV
|
|
||||||
[warning] at ./SIV-rfc5297.md:494:8--494:9 Unused name: k
|
|
||||||
[warning] at ./SIV-rfc5297.md:494:7--494:64:
|
|
||||||
Assuming k to have a numeric type
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Salsa20
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Cipher
|
Loading module Cipher
|
||||||
Loading module Test
|
Loading module Test
|
||||||
Loading module Cryptol
|
Loading module Cryptol
|
||||||
Loading module Threefish
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Cipher
|
|
||||||
Loading module DES
|
|
||||||
Loading module TripleDES
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Main
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Main
|
Loading module Main
|
||||||
Loading module Cryptol
|
Loading module Cryptol
|
||||||
Loading module Main
|
Loading module Main
|
||||||
@ -97,18 +69,8 @@ Loading module MISTY1
|
|||||||
Loading module Cryptol
|
Loading module Cryptol
|
||||||
Loading module Main
|
Loading module Main
|
||||||
Loading module Cryptol
|
Loading module Cryptol
|
||||||
Loading module Main
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Main
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module MKRAND
|
Loading module MKRAND
|
||||||
Loading module Cryptol
|
Loading module Cryptol
|
||||||
Loading module simon
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Main
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Main
|
|
||||||
Loading module Cryptol
|
|
||||||
Loading module Main
|
Loading module Main
|
||||||
Loading module Cryptol
|
Loading module Cryptol
|
||||||
Loading module FoxChickenCorn
|
Loading module FoxChickenCorn
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user