diff --git a/examples/FNV-a1.cry b/examples/FNV-a1.cry deleted file mode 100644 index 881ceab2..00000000 --- a/examples/FNV-a1.cry +++ /dev/null @@ -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 diff --git a/examples/HMAC.cry b/examples/HMAC.cry deleted file mode 100644 index 58378f45..00000000 --- a/examples/HMAC.cry +++ /dev/null @@ -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)) - - - - - - - - - diff --git a/examples/MD5.cry b/examples/MD5.cry deleted file mode 100644 index bc7ebe9c..00000000 --- a/examples/MD5.cry +++ /dev/null @@ -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 diff --git a/examples/SHA1.cry b/examples/SHA1.cry deleted file mode 100644 index cdf49ae7..00000000 --- a/examples/SHA1.cry +++ /dev/null @@ -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 diff --git a/examples/SHA256.cry b/examples/SHA256.cry deleted file mode 100644 index 02d8ad56..00000000 --- a/examples/SHA256.cry +++ /dev/null @@ -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 \ No newline at end of file diff --git a/examples/SIV-rfc5297.md b/examples/SIV-rfc5297.md deleted file mode 100644 index 5d24ff1f..00000000 --- a/examples/SIV-rfc5297.md +++ /dev/null @@ -1,1308 +0,0 @@ -``` -module SIV where - -import AES -// Uses ../bench/data/AES.cry: -// CRYPTOLPATH=../bench/data cryptol SIV-rfc5297.md - -type Key = [AESKeySize] -``` - -Network Working Group D. Harkins -Request for Comments: 5297 Aruba Networks -Category: Informational October 2008 - - -Synthetic Initialization Vector (SIV) Authenticated Encryption -Using the Advanced Encryption Standard (AES) - -Status of This Memo - - This memo provides information for the Internet community. It does - not specify an Internet standard of any kind. Distribution of this - memo is unlimited. - -Abstract - - This memo describes SIV (Synthetic Initialization Vector), a block - cipher mode of operation. SIV takes a key, a plaintext, and multiple - variable-length octet strings that will be authenticated but not - encrypted. It produces a ciphertext having the same length as the - plaintext and a synthetic initialization vector. Depending on how it - is used, SIV achieves either the goal of deterministic authenticated - encryption or the goal of nonce-based, misuse-resistant authenticated - encryption. - -Table of Contents - - 1. Introduction ....................................................3 - 1.1. Background .................................................3 - 1.2. Definitions ................................................4 - 1.3. Motivation .................................................4 - 1.3.1. Key Wrapping ........................................4 - 1.3.2. Resistance to Nonce Misuse/Reuse ....................4 - 1.3.3. Key Derivation ......................................5 - 1.3.4. Robustness versus Performance .......................6 - 1.3.5. Conservation of Cryptographic Primitives ............6 - 2. Specification of SIV ............................................6 - 2.1. Notation ...................................................6 - 2.2. Overview ...................................................7 - 2.3. Doubling ...................................................7 - 2.4. S2V ........................................................8 - 2.5. CTR .......................................................10 - 2.6. SIV Encrypt ...............................................10 - 2.7. SIV Decrypt ...............................................12 - 3. Nonce-Based Authenticated Encryption with SIV ..................14 - 4. Deterministic Authenticated Encryption with SIV ................15 - 5. Optimizations ..................................................15 - 6. IANA Considerations ............................................15 - 6.1. AEAD_AES_SIV_CMAC_256 .....................................17 - 6.2. AEAD_AES_SIV_CMAC_384 .....................................17 - 6.3. AEAD_AES_SIV_CMAC_512 .....................................18 - 7. Security Considerations ........................................18 - 8. Acknowledgments ................................................19 - 9. References .....................................................19 - 9.1. Normative References ......................................19 - 9.2. Informative References ....................................19 - Appendix A. Test Vectors ....................................... 22 - A.1. Deterministic Authenticated Encryption Example ........... 22 - A.2. Nonce-Based Authenticated Encryption Example ............. 23 - - -1. Introduction - -1.1. Background - - Various attacks have been described (e.g., [BADESP]) when data is - merely privacy protected and not additionally authenticated or - integrity protected. Therefore, combined modes of encryption and - authentication have been developed ([RFC5116], [RFC3610], [GCM], - [JUTLA], [OCB]). These provide conventional authenticated encryption - when used with a nonce ("a number used once") and typically accept - additional inputs that are authenticated but not encrypted, - hereinafter referred to as "associated data" or AD. - - A deterministic, nonce-less, form of authenticated encryption has - been used to protect the transportation of cryptographic keys (e.g., - [X9F1], [RFC3217], [RFC3394]). This is generally referred to as "Key - Wrapping". - - This memo describes a new block cipher mode, SIV, that provides both - nonce-based authenticated encryption as well as deterministic, nonce- - less key wrapping. It contains a Pseudo-Random Function (PRF) - construction called S2V and an encryption/decryption construction, - called CTR. SIV was specified by Phillip Rogaway and Thomas - Shrimpton in [DAE]. The underlying block cipher used herein for both - S2V and CTR is AES with key lengths of 128 bits, 192 bits, or 256 - bits. S2V uses AES in Cipher-based Message Authentication Code - ([CMAC]) mode, CTR uses AES in counter ([MODES]) mode. - - Associated data is data input to an authenticated-encryption mode - that will be authenticated but not encrypted. [RFC5116] says that - associated data can include "addresses, ports, sequence numbers, - protocol version numbers, and other fields that indicate how the - plaintext or ciphertext should be handled, forwarded, or processed". - These are multiple, distinct inputs and may not be contiguous. Other - authenticated-encryption cipher modes allow only a single associated - data input. Such a limitation may require implementation of a - scatter/gather form of data marshalling to combine the multiple - components of the associated data into a single input or may require - a pre-processing step where the associated data inputs are - concatenated together. SIV accepts multiple variable-length octet - strings (hereinafter referred to as a "vector of strings") as - associated data inputs. This obviates the need for data marshalling - or pre-processing of associated data to package it into a single - input. - - By allowing associated data to consist of a vector of strings SIV - also obviates the requirement to encode the length of component - fields of the associated data when those fields have variable length. - -1.2. Definitions - - The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", - "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this - document are to be interpreted as described in RFC 2119 [RFC2119]. - -1.3. Motivation - -1.3.1. Key Wrapping - - A key distribution protocol must protect keys it is distributing. - This has not always been done correctly. For example, RADIUS - [RFC2865] uses Microsoft Point-to-Point Encryption (MPPE) [RFC2548] - to encrypt a key prior to transmission from server to client. It - provides no integrity checking of the encrypted key. [RADKEY] - specifies the use of [RFC3394] to wrap a key in a RADIUS request but - because of the inability to pass associated data, a Hashed Message - Authentication Code (HMAC) [RFC2104] is necessary to provide - authentication of the entire request. - - SIV can be used as a drop-in replacement for any specification that - uses [RFC3394] or [RFC3217], including the aforementioned use. It is - a more general purpose solution as it allows for associated data to - be specified. - -1.3.2. Resistance to Nonce Misuse/Reuse - - The nonce-based authenticated encryption schemes described above are - susceptible to reuse and/or misuse of the nonce. Depending on the - specific scheme there are subtle and critical requirements placed on - the nonce (see [SP800-38D]). [GCM] states that it provides - "excellent security" if its nonce is guaranteed to be distinct but - provides "no security" otherwise. Confidentiality guarantees are - voided if a counter in [RFC3610] is reused. In many cases, - guaranteeing no reuse of a nonce/counter/IV is not a problem, but in - others it will be. - - For example, many applications obtain access to cryptographic - functions via an application program interface to a cryptographic - library. These libraries are typically not stateful and any nonce, - initialization vector, or counter required by the cipher mode is - passed to the cryptographic library by the application. Putting the - construction of a security-critical datum outside the control of the - encryption engine places an onerous burden on the application writer - who may not provide the necessary cryptographic hygiene. Perhaps his - random number generator is not very good or maybe an application - fault causes a counter to be reset. The fragility of the cipher mode - may result in its inadvertent misuse. Also, if one's environment is - (knowingly or unknowingly) a virtual machine, it may be possible to - roll back a virtual state machine and cause nonce reuse thereby - gutting the security of the authenticated encryption scheme (see - [VIRT]). - - If the nonce is random, a requirement that it never repeat will limit - the amount of data that can be safely protected with a single key to - one block. More sensibly, a random nonce is required to "almost - always" be non-repeating, but that will drastically limit the amount - of data that can be safely protected. - - SIV provides a level of resistance to nonce reuse and misuse. If the - nonce is never reused, then the usual notion of nonce-based security - of an authenticated encryption mode is achieved. If, however, the - nonce is reused, authenticity is retained and confidentiality is only - compromised to the extent that an attacker can determine that the - same plaintext (and same associated data) was protected with the same - nonce and key. See Security Considerations (Section 7). - -1.3.3. Key Derivation - - A PRF is frequently used as a key derivation function (e.g., [WLAN]) - by passing it a key and a single string. Typically, this single - string is the concatenation of a series of smaller strings -- for - example, a label and some context to bind into the derived string. - - These are usually multiple strings but are mapped to a single string - because of the way PRFs are typically defined -- two inputs: a key - and data. Such a crude mapping is inefficient because additional - data must be included -- the length of variable-length inputs must be - encoded separately -- and, depending on the PRF, memory allocation - and copying may be needed. Also, if only one or two of the inputs - changed when deriving a new key, it may still be necessary to process - all of the other constants that preceded it every time the PRF is - invoked. - - When a PRF is used in this manner its input is a vector of strings - and not a single string and the PRF should handle the data as such. - The S2V ("string to vector") PRF construction accepts a vector of - inputs and provides a more natural mapping of input that does not - require additional lengths encodings and obviates the memory and - processing overhead to marshal inputs and their encoded lengths into - a single string. Constant inputs to the PRF need only be computed - once. - -1.3.4. Robustness versus Performance - - SIV cannot perform at the same high throughput rates that other - authenticated encryption schemes can (e.g., [GCM] or [OCB]) due to - the requirement for two passes of the data, but for situations where - performance is not a limiting factor -- e.g., control plane - applications -- it can provide a robust alternative, especially when - considering its resistance to nonce reuse. - -1.3.5. Conservation of Cryptographic Primitives - - The cipher mode described herein can do authenticated encryption, key - wrapping, key derivation, and serve as a generic message - authentication algorithm. It is therefore possible to implement all - these functions with a single tool, instead of one tool for each - function. This is extremely attractive for devices that are memory - and/or processor constrained and that cannot afford to implement - multiple cryptographic primitives to accomplish these functions. - -2. Specification of SIV - -2.1. Notation - - SIV and S2V use the following notation: - - len(A) - returns the number of bits in A. - - pad(X) - indicates padding of string X, len(X) < 128, out to 128 bits by - the concatenation of a single bit of 1 followed by as many 0 bits - as are necessary. - -``` -pad : {x} (fin x) => [x] -> [128] -pad x = take `{128} (x # [True] # (zero : [127])) -``` - - leftmost(A,n) - the n most significant bits of A. - - rightmost(A,n) - the n least significant bits of A. - - A || B - means concatenation of string A with string B. - - A xor B - is the exclusive OR operation on two equal length strings, A and - B. - - A xorend B - where len(A) >= len(B), means xoring a string B onto the end of - string A -- i.e., leftmost(A, len(A)-len(B)) || (rightmost(A, - len(B)) xor B). - -``` -xorend : {a,b} (fin a, fin b, a >= b) => [a] -> [b] -> [a] -xorend a b = a ^ ((zero : [a-b]) # b) -``` - - A bitand B - is the logical AND operation on two equal length strings, A and B. - -``` -bitand a b = a && b -``` - - dbl(S) - is the multiplication of S and 0...010 in the finite field - represented using the primitive polynomial - x^128 + x^7 + x^2 + x + 1. See Doubling (Section 2.3). - - a^b - indicates a string that is "b" bits, each having the value "a". - -``` -// In cryptol tye symbole '^' is taken, we will use the native name 'repeat' -// instead. This should not lead to errors due to the different types, which -// the compiler would detect if one operation were used in place of the other. -``` - - - indicates a string that is 128 zero bits. - - - indicates a string that is 127 zero bits concatenated with a - single one bit, that is 0^127 || 1^1. - - A/B - indicates the greatest integer less than or equal to the real- - valued quotient of A and B. - - E(K,X) - indicates AES encryption of string X using key K. - -``` -E : (Key,[128]) -> [128] -E(K,X) = aesEncrypt (X,K) - -// 1. Apply the subkey generation process in Sec. 6.1 to K to produce K1 and K2. -// 2. If Mlen = 0, let n = 1; else, let n = ⎡Mlen/b⎤. -// 3. Let M1, M2, ... , Mn-1, Mn* denote the unique sequence of bit strings such that M = M1 || M2 || ... || Mn-1 || Mn*, where M1, M2,..., Mn-1 are complete blocks. -// 4. If Mn* is a complete block, let Mn = K1 ⊕ Mn* ; else, let Mn = K2 ⊕ (Mn* ||10j), where j = nb-Mlen-1. -// 5. Let C0 = 0b. -// 6. For i = 1 to n, let Ci = CIPHK(Ci-1 ⊕ Mi). -// 7. Let T = MSBTlen(Cn). -// 8. Return T. - -aesCMAC : {m} (fin m) => Key -> [m] -> [128] -aesCMAC K m = - cmacBlocks K ((`m%128) == 0 /\ `m > 0) (split `{each=128,parts=blocks} full) - where - pd = [True] # zero : [128] - full = take `{front=128 * blocks, back = (m + 128) - 128*blocks} (m # pd) - type blocks = max ((m + 127) / 128) 1 - -cmacBlocks : {blocks} (fin blocks, blocks >= 1) => Key -> Bit -> [blocks][128] -> [128] -cmacBlocks K completeMn ms = ci ! 0 - where - (K1,K2) = subkeyGen K - xs = take `{back=1} ms - mn = KN ^ (ms ! 0) - KN = if completeMn then K1 else K2 - ci = [zero] # [ E(K,c ^ mi) | c <- ci | mi <- (xs # [mn]) ] - -property cmacKAT1 = - ~zero == - [ aesCMAC 0x2b7e151628aed2a6abf7158809cf4f3c [] == 0xbb1d6929e95937287fa37d129b756746 - , aesCMAC 0x2b7e151628aed2a6abf7158809cf4f3c 0x6bc1bee22e409f96e93d7e117393172a == 0x070a16b46b4d4144f79bdd9dd04a287c - , aesCMAC 0x2b7e151628aed2a6abf7158809cf4f3c 0x6bc1bee22e409f96e93d7e117393172aae2d8a571e03ac9c9eb76fac45af8e5130c81c46a35ce411 == 0xdfa66747de9ae63030ca32611497c827 - , aesCMAC 0x2b7e151628aed2a6abf7158809cf4f3c 0x6bc1bee22e409f96e93d7e117393172aae2d8a571e03ac9c9eb76fac45af8e5130c81c46a35ce411e5fbc1191a0a52eff69f2445df4f9b17ad2b417be66c3710 == 0x51f0bebf7e3b9d92fc49741779363cfe - ] - -repeat : {n,a} (n >= 1, fin n) => a -> [n]a -repeat a = [a | _ <- [1..n]] -``` - -``` -// 1. Let L = CIPHK(0b). -// 2. If MSB1(L) = 0 -// then K1 = L << 1; -// else K1 = (L << 1) ⊕ Rb; see Sec. 5.3 for the definition of Rb. -// 3. If MSB1(K1) = 0 -// then K2 = K1 << 1; -// else K2 = (K1 << 1) ⊕ Rb. -// 4. Return K1, K2. -private - subkeyGen : Key -> (Key, Key) - subkeyGen K = (K1,K2) - where - L = E(K,zero) - K1 = ite (L@0 == False) (L << 1) ((L << 1) ^ Rb) - K2 = ite ((K1@0) == False) (K1 << 1) ((K1 << 1) ^ Rb) - Rb = `0b10000111 - -ite : {n} (fin n, n >= 1) => Bit -> [n] -> [n] -> [n] -ite pred t e = t && m1 || e && m2 - where m1 = [pred | _ <- [1..n]] - m2 = ~m1 -``` - -2.2. Overview - - SIV-AES uses AES in CMAC mode (S2V) and in counter mode (CTR). SIV- - AES takes either a 256-, 384-, or 512-bit key (which is broken up - into two equal-sized keys, one for S2V and the other for CTR), a - variable length plaintext, and multiple variable-length strings - representing associated data. Its output is a ciphertext that - comprises a synthetic initialization vector concatenated with the - encrypted plaintext. - -2.3. Doubling - - The doubling operation on a 128-bit input string is performed using a - left-shift of the input followed by a conditional xor operation on - the result with the constant: - -> 00000000 00000000 00000000 00000087 - - The condition under which the xor operation is performed is when the - bit being shifted off is one. - - Note that this is the same operation used to generate sub-keys for - CMAC-AES. - -``` -// dblRef x = if x@0 == False then (x << 1) -// else (x << 1) ^ `0x87 -// :prove \x -> dbl x == (dblRef x : [128]) -// Q.E.D. - -dbl x = ite ((x@0) == False) (x << 1) ((x << 1) ^ `0x87) -``` - -2.4. S2V - - The S2V operation consists of the doubling and xoring of the outputs - of a pseudo-random function, CMAC, operating over individual strings - in the input vector: S1, S2, ... , Sn. It is bootstrapped by - performing CMAC on a 128-bit string of zeros. If the length of the - final string in the vector is greater than or equal to 128 bits, the - output of the double/xor chain is xored onto the end of the final - input string. That result is input to a final CMAC operation to - produce the output V. If the length of the final string is less than - 128 bits, the output of the double/xor chain is doubled once more and - it is xored with the final string padded using the padding function - pad(X). That result is input to a final CMAC operation to produce - the output V. - - S2V with key K on a vector of n inputs S1, S2, ..., Sn-1, Sn, and - len(Sn) >= 128: - -> +----+ +----+ +------+ +----+ -> | S1 | | S2 | . . . | Sn-1 | | Sn | -> +----+ +----+ +------+ +----+ -> K | | | | -> | | | | | V -> V | V V V /----> xorend -> +-----+ | +-----+ +-----+ +-----+ | | -> | AES-|<----->| AES-| K-->| AES-| K--->| AES-| | | -> | CMAC| | CMAC| | CMAC| | CMAC| | | -> +-----+ +-----+ +-----+ +-----+ | V -> | | | | | +-----+ -> | | | | | K-->| AES-| -> | | | | | | CMAC| -> | | | | | +-----+ -> \-> dbl -> xor -> dbl -> xor -> dbl -> xor---/ | -> V -> +---+ -> | V | -> +---+ -> -> Figure 2 - - S2V with key K on a vector of n inputs S1, S2, ..., Sn-1, Sn, and - len(Sn) < 128: - -> +----+ +----+ +------+ +---------+ -> | S1 | | S2 | . . . | Sn-1 | | pad(Sn) | -> +----+ +----+ +------+ +---------+ -> K | | | | -> | | | | | V -> V | V V V /------> xor -> +-----+ | +-----+ +-----+ +-----+ | | -> | AES-|<--->| AES-| K-->| AES-| K-->| AES-| | | -> | CMAC| | CMAC| | CMAC| | CMAC| | | -> +-----+ +-----+ +-----+ +-----+ | V -> | | | | | +-----+ -> | | | | | K-->| AES-| -> | | | | | | CMAC| -> | | | | | +-----+ -> \-> dbl -> xor -> dbl -> xor -> dbl -> xor-> dbl | -> V -> +---+ -> | V | -> +---+ -> -> Figure 3 - - Algorithmically S2V can be described as: - -> S2V(K, S1, ..., Sn) { -> if n = 0 then -> return V = AES-CMAC(K, ) -> fi -> D = AES-CMAC(K, ) -> for i = 1 to n-1 do -> D = dbl(D) xor AES-CMAC(K, Si) -> done -> if len(Sn) >= 128 then -> T = Sn xorend D -> else -> T = dbl(D) xor pad(Sn) -> fi -> return V = AES-CMAC(K, T) -> } - -``` -// S2V for n=2 -S2V : {k, ad, p} (fin ad, fin p) => Key -> [ad] -> [p] -> [128] -S2V K S1 S2 = res - where - D0 = aesCMAC K (zero : [128]) - D1 = dbl D0 ^ aesCMAC K S1 - res = if `p >= 128 - then aesCMAC K (xorend (fixSize S2) D1) - else aesCMAC K (dbl D1 ^ pad S2) - -private - // The length of 'p' is >= 128, but Cryptol lacks - // dependent types and can not infer this fact. We - // Provide a no-op computation that results in a - // new type for 'p' that is at least 128 bits - fixSize : {p} (fin p) => [p] -> [max p 128] - fixSize p = take `{front=max p 128, back = p + 128 - max p 128} (p # (zero : [128])) -``` - -2.5. CTR - - CTR is a counter mode of AES. It takes as input a plaintext P of - arbitrary length, a key K of length 128, 192, or 256 bits, and a - counter X that is 128 bits in length, and outputs Z, which represents - a concatenation of a synthetic initialization vector V and the - ciphertext C, which is the same length as the plaintext. - - The ciphertext is produced by xoring the plaintext with the first - len(P) bits of the following string: - -> E(K, X) || E(K, X+1) || E(K, X+2) || ... - - Before beginning counter mode, the 31st and 63rd bits (where the - rightmost bit is the 0th bit) of the counter are cleared. This - enables implementations that support native 32-bit (64-bit) addition - to increment the counter modulo 2^32 (2^64) in a manner that cannot - be distinguished from 128-bit increments, as long as the number of - increment operations is limited by an upper bound that safely avoids - carry to occur out of the respective pre-cleared bit. More formally, - for 32-bit addition, the counter is incremented as: - -> SALT=leftmost(X,96) -> -> n=rightmost(X,32) -> -> X+i = SALT || (n + i mod 2^32). - - For 64-bit addition, the counter is incremented as: - -> SALT=leftmost(X,64) -> -> n=rightmost(X,64) -> -> X+i = SALT || (n + i mod 2^64). - - Performing 32-bit or 64-bit addition on the counter will limit the - amount of plaintext that can be safely protected by SIV-AES to 2^39 - - 128 bits or 2^71 - 128 bits, respectively. - -``` -ctr32 : {n} (2^^39 - 128 >= n) => Key -> [128] -> [n] -> [n] -ctr32 k iv pt = pt ^ take stream - where - stream = join [E(k,v) | v <- ivs] - ivs = [take `{96} iv # cnt + i | i <- [0 ...]] - cnt = drop `{back=32} iv - -ctr64 : {n} (2^^71 - 128 >= n) => Key -> [128] -> [n] -> [n] -ctr64 k iv pt = pt ^ take stream - where - stream = join [E(k,v) | v <- ivs] - ivs = [take `{64} iv # cnt + i | i <- [0 ...]] - cnt = drop `{back=64} iv -``` - -2.6. SIV Encrypt - - SIV-encrypt takes as input a key K of length 256, 384, or 512 bits, - plaintext of arbitrary length, and a vector of associated data AD[ ] - where the number of components in the vector is not greater than 126 - (see Section 7). It produces output, Z, which is the concatenation - of a 128-bit synthetic initialization vector and ciphertext whose - length is equal to the length of the plaintext. - - The key is split into equal halves, K1 = leftmost(K, len(K)/2) and K2 - = rightmost(K, len(K)/2). K1 is used for S2V and K2 is used for CTR. - - In the encryption mode, the associated data and plaintext represent - the vector of inputs to S2V, with the plaintext being the last string - in the vector. The output of S2V is a synthetic IV that represents - the initial counter to CTR. - - The encryption construction of SIV is as follows: - -> +------+ +------+ +------+ +---+ -> | AD 1 | | AD 2 |...| AD n | | P | -> +------+ +------+ +------+ +---+ -> | | | | -> | | ... | ------------------| -> \ | / / | -> \ | / / +------------+ | -> \ | / / | K = K1||K2 | | -> \ | / / +------------+ V -> \ | / / | | +-----+ -> \ | / / K1 | | K2 | | -> \ | / / ------/ \------>| CTR | -> \ | / / / ------->| | -> | | | | | | +-----+ -> V V V V V | | -> +------------+ +--------+ V -> | S2V |------>| V | +----+ -> +------------+ +--------+ | C | -> | +----+ -> | | -> -----\ | -> \ | -> \ | -> V V -> +-----+ -> | Z | -> +-----+ - - where the plaintext is P, the associated data is AD1 through ADn, V - is the synthetic IV, the ciphertext is C, and Z is the output. - - Algorithmically, SIV Encrypt can be described as: - -> SIV-ENCRYPT(K, P, AD1, ..., ADn) { -> K1 = leftmost(K, len(K)/2) -> K2 = rightmost(K, len(K)/2) -> V = S2V(K1, AD1, ..., ADn, P) -> Q = V bitand (1^64 || 0^1 || 1^31 || 0^1 || 1^31) -> m = (len(P) + 127)/128 -> -> for i = 0 to m-1 do -> Xi = AES(K2, Q+i) -> done -> X = leftmost(X0 || ... || Xm-1, len(P)) -> C = P xor X -> -> return V || C -> } - -``` -sivEncrypt : {p, ad} (fin ad, 2^^71-128 >= p) => [256] -> [ad] -> [p] -> [128 + p] -sivEncrypt K ad P = V # C - where - [K1,K2] = split K - V = S2V K1 ad P - Q = bitand V (repeat `{64} True # [False] # repeat `{31} True # [False] # repeat `{31} True) - C = ctr64 K2 Q P -``` - - where the key length used by AES in CTR and S2V is len(K)/2 and will - each be either 128 bits, 192 bits, or 256 bits. - - The 31st and 63rd bit (where the rightmost bit is the 0th) of the - counter are zeroed out just prior to being used by CTR for - optimization purposes, see Section 5. - -2.7. SIV Decrypt - - SIV-decrypt takes as input a key K of length 256, 384, or 512 bits, - Z, which represents a synthetic initialization vector V concatenated - with a ciphertext C, and a vector of associated data AD[ ] where the - number of components in the vector is not greater than 126 (see - Section 7). It produces either the original plaintext or the special - symbol FAIL. - - The key is split as specified in Section 2.6 - - The synthetic initialization vector acts as the initial counter to - CTR to decrypt the ciphertext. The associated data and the output of - CTR represent a vector of strings that is passed to S2V, with the CTR - output being the last string in the vector. The output of S2V is - then compared against the synthetic IV that accompanied the original - ciphertext. If they match, the output from CTR is returned as the - decrypted and authenticated plaintext; otherwise, the special symbol - FAIL is returned. - - The decryption construction of SIV is as follows: - -> +------+ +------+ +------+ +---+ -> | AD 1 | | AD 2 |...| AD n | | P | -> +------+ +------+ +------+ +---+ -> | | | ^ -> | | ... / | -> | | / /----------------| -> | | / / | -> \ | / / +------------+ | -> \ | / / | K = K1||k2 | | -> \ | / / +------------+ | -> \ | / / | | +-----+ -> \ | / / K1 | | K2 | | -> \ | | | /-----/ \----->| CTR | -> \ | | | | ------->| | -> | | | | | | +-----+ -> V V V V V | ^ -> +-------------+ +--------+ | -> | S2V | | V | +---+ -> +-------------+ +--------+ | C | -> | | ^ +---+ -> | | | ^ -> | | \ | -> | | \___ | -> V V \ | -> +-------+ +---------+ +---+ -> | T |----->| if != | | Z | -> +-------+ +---------+ +---+ -> | -> | -> V -> FAIL -> -> Figure 10 - - - Algorithmically, SIV-Decrypt can be described as: - -> SIV-DECRYPT(K, Z, AD1, ..., ADn) { -> V = leftmost(Z, 128) -> C = rightmost(Z, len(Z)-128) -> K1 = leftmost(K, len(K)/2) -> K2 = rightmost(K, len(K)/2) -> Q = V bitand (1^64 || 0^1 || 1^31 || 0^1 || 1^31) -> -> m = (len(C) + 127)/128 -> for i = 0 to m-1 do -> Xi = AES(K2, Q+i) -> done -> X = leftmost(X0 || ... || Xm-1, len(C)) -> P = C xor X -> T = S2V(K1, AD1, ..., ADn, P) -> -> if T = V then -> return P -> else -> return FAIL -> fi -> } - -``` -sivDecrypt : {p, ad} (2^^71 - 128 >= p, fin ad) => [256] -> [ad] -> [p+128] -> (Bit, [p]) -sivDecrypt K ad Z = (T == V, P) - where - V = take `{128} Z - C = drop `{back=p} Z - [K1,K2] = split `{parts=2} K - Q = bitand V (repeat `{64} True # [False] # repeat `{31} True # [False] # repeat `{31} True) - P = ctr64 K2 Q C - T = S2V K1 ad P -``` - - where the key length used by AES in CTR and S2V is len(K)/2 and will - each be either 128 bits, 192 bits, or 256 bits. - - The 31st and 63rd bit (where the rightmost bit is the 0th) of the - counter are zeroed out just prior to being used in CTR mode for - optimization purposes, see Section 5. - -3. Nonce-Based Authenticated Encryption with SIV - - SIV performs nonce-based authenticated encryption when a component of - the associated data is a nonce. For purposes of interoperability the - final component -- i.e., the string immediately preceding the - plaintext in the vector input to S2V -- is used for the nonce. Other - associated data are optional. It is up to the specific application - of SIV to specify how the rest of the associated data are input. - - If the nonce is random, it SHOULD be at least 128 bits in length and - be harvested from a pool having at least 128 bits of entropy. A non- - random source MAY also be used, for instance, a time stamp, or a - counter. The definition of a nonce precludes reuse, but SIV is - resistant to nonce reuse. See Section 1.3.2 for a discussion on the - security implications of nonce reuse. - - It MAY be necessary to transport this nonce with the output generated - by S2V. - -4. Deterministic Authenticated Encryption with SIV - - When the plaintext to encrypt and authenticate contains data that is - unpredictable to an adversary -- for example, a secret key -- SIV can - be used in a deterministic mode to perform "key wrapping". Because - S2V allows for associated data and imposes no unnatural size - restrictions on the data it is protecting, it is a more useful and - general purpose solution than [RFC3394]. Protocols that use SIV for - deterministic authenticated encryption (i.e., for more than just - wrapping of keys) MAY define associated data inputs to SIV. It is - not necessary to add a nonce component to the AD in this case. - -5. Optimizations - - Implementations that cannot or do not wish to support addition modulo - 2^128 can take advantage of the fact that the 31st and 63rd bits - (where the rightmost bit is the 0th bit) in the counter are cleared - before being used by CTR. This allows implementations that natively - support 32-bit or 64-bit addition to increment the counter naturally. - Of course, in this case, the amount of plaintext that can be safely - protected by SIV is reduced by a commensurate amount -- addition - modulo 2^32 limits plaintext to (2^39 - 128) bits, addition modulo - 2^64 limits plaintext to (2^71 - 128) bits. - - It is possible to optimize an implementation of S2V when it is being - used as a key derivation function (KDF), for example in [WLAN]. This - is because S2V operates on a vector of distinct strings and typically - the data passed to a KDF contains constant strings. Depending on the - location of variant components of the input different optimizations - are possible. The CMACed output of intermediate and invariant - components can be computed once and cached. This can then be doubled - and xored with the running sum to produce the output. Or an - intermediate value that represents the doubled and xored output of - multiple components, up to the variant component, can be computed - once and cached. - -6. IANA Considerations - - [RFC5116] defines a uniform interface to cipher modes that provide - nonce-based Authenticated Encryption with Associated Data (AEAD). It - does this via a registry of AEAD algorithms. - - The Internet Assigned Numbers Authority (IANA) assigned three entries - from the AEAD Registry for AES-SIV-CMAC-256 (15), AES-SIV-CMAC-384 - (16), and AES-SIV-CMAC-512 (17) based upon the following AEAD - algorithm definitions. [RFC5116] defines operations in octets, not - bits. Limits in this section will therefore be specified in octets. - The security analysis for each of these algorithms is in [DAE]. - - Unfortunately, [RFC5116] restricts AD input to a single component and - limits the benefit SIV offers for dealing in a natural fashion with - AD consisting of multiple distinct components. Therefore, when it is - required to access SIV through the interface defined in [RFC5116], it - is necessary to marshal multiple AD inputs into a single string (see - Section 1.1) prior to invoking SIV. Note that this requirement is - not unique to SIV. All cipher modes using [RFC5116] MUST similarly - marshal multiple AD inputs into a single string, and any technique - used for any other AEAD mode (e.g., a scatter/gather technique) can - be used with SIV. - - [RFC5116] requires AEAD algorithm specifications to include maximal - limits to the amount of plaintext, the amount of associated data, and - the size of a nonce that the AEAD algorithm can accept. - - SIV uses AES in counter mode and the security guarantees of SIV would - be lost if the counter was allowed to repeat. Since the counter is - 128 bits, a limit to the amount of plaintext that can be safely - protected by a single invocation of SIV is 2^128 blocks. - - To prevent the possibility of collisions, [CMAC] recommends that no - more than 2^48 invocations be made to CMAC with the same key. This - is not a limit on the amount of data that can be passed to CMAC, - though. There is no practical limit to the amount of data that can - be made to a single invocation of CMAC, and likewise, there is no - practical limit to the amount of associated data or nonce material - that can be passed to SIV. - - A collision in the output of S2V would mean the same counter would be - used with different plaintext in counter mode. This would void the - security guarantees of SIV. The "Birthday Paradox" (see [APPCRY]) - would imply that no more than 2^64 distinct invocations to SIV be - made with the same key. It is prudent to follow the example of - [CMAC] though, and further limit the number of distinct invocations - of SIV using the same key to 2^48. Note that [RFC5116] does not - provide a variable to describe this limit. - - The counter-space for SIV is 2^128. Each invocation of SIV consumes - a portion of that counter-space and the amount consumed depends on - the amount of plaintext being passed to that single invocation. - Multiple invocations of SIV with the same key can increase the - possibility of distinct invocations overlapping the counter-space. - The total amount of plaintext that can be safely protected with a - single key is, therefore, a function of the number of distinct - invocations and the amount of plaintext protected with each - invocation. - -6.1. AEAD_AES_SIV_CMAC_256 - - The AES-SIV-CMAC-256 AEAD algorithm works as specified in Sections - 2.6 and 2.7. The input and output lengths for AES-SIV-CMAC-256 as - defined by [RFC5116] are: - - K_LEN is 32 octets. - - P_MAX is 2^132 octets. - - A_MAX is unlimited. - - N_MIN is 1 octet. - - N_MAX is unlimited. - - C_MAX is 2^132 + 16 octets. - - The security implications of nonce reuse and/or misuse are described - in Section 1.3.2. - -6.2. AEAD_AES_SIV_CMAC_384 - - The AES-SIV-CMAC-384 AEAD algorithm works as specified in Sections - 2.6 and 2.7. The input and output lengths for AES-SIV-CMAC-384 as - defined by [RFC5116] are: - - K_LEN is 48 octets. - - P_MAX is 2^132 octets. - - A_MAX is unlimited. - - N_MIN is 1 octet. - - N_MAX is unlimited. - - C_MAX is 2^132 + 16 octets. - - The security implications of nonce reuse and/or misuse are described - in Section 1.3.2. - -6.3. AEAD_AES_SIV_CMAC_512 - - The AES-SIV-CMAC-512 AEAD algorithm works as specified in Sections - 2.6 and 2.7. The input and output lengths for AES-SIV-CMAC-512 as - defined by [RFC5116] are: - - K_LEN is 64 octets. - - P_MAX is 2^132 octets. - - A_MAX is unlimited. - - N_MIN is 1 octet. - - N_MAX is unlimited. - - C_MAX is 2^132 + 16 octets. - - The security implications of nonce reuse and/or misuse are described - in Section 1.3.2. - -7. Security Considerations - - SIV provides confidentiality in the sense that the output of SIV- - Encrypt is indistinguishable from a random string of bits. It - provides authenticity in the sense that an attacker is unable to - construct a string of bits that will return other than FAIL when - input to SIV-Decrypt. A proof of the security of SIV with an "all- - in-one" notion of security for an authenticated encryption scheme is - provided in [DAE]. - - SIV provides deterministic "key wrapping" when the plaintext contains - data that is unpredictable to an adversary (for instance, a - cryptographic key). Even when this key is made available to an - attacker the output of SIV-Encrypt is indistinguishable from random - bits. Similarly, even when this key is made available to an - attacker, she is unable to construct a string of bits that when input - to SIV-Decrypt will return anything other than FAIL. - - When the nonce used in the nonce-based authenticated encryption mode - of SIV-AES is treated with the care afforded a nonce or counter in - other conventional nonce-based authenticated encryption schemes -- - i.e., guarantee that it will never be used with the same key for two - distinct invocations -- then SIV achieves the level of security - described above. If, however, the nonce is reused SIV continues to - provide the level of authenticity described above but with a slightly - reduced amount of privacy (see Section 1.3.2). - - If S2V is used as a key derivation function, the secret input MUST be - generated uniformly at random. S2V is a pseudo-random function and - is not suitable for use as a random oracle as defined in [RANDORCL]. - - The security bound set by the proof of security of S2V in [DAE] - depends on the number of vector-based queries made by an adversary - and the total number of all components in those queries. The - security is only proven when the number of components in each query - is limited to n-1, where n is the blocksize of the underlying pseudo- - random function. The underlying pseudo-random function used here is - based on AES whose blocksize is 128 bits. Therefore, S2V must not be - passed more than 127 components. Since SIV includes the plaintext as - a component to S2V, that limits the number of components of - associated data that can be safely passed to SIV to 126. - -8. Acknowledgments - - Thanks to Phil Rogaway for patiently answering numerous questions on - SIV and S2V and for useful critiques of earlier versions of this - paper. Thanks also to David McGrew for numerous helpful comments and - suggestions for improving this paper. Thanks to Jouni Malinen for - reviewing this paper and producing another independent implementation - of SIV, thereby confirming the correctness of the test vectors. - -9. References - -9.1. Normative References - - [CMAC] Dworkin, M., "Recommendation for Block Cipher Modes of - Operation: The CMAC Mode for Authentication", NIST - Special Pulication 800-38B, May 2005. - - [MODES] Dworkin, M., "Recommendation for Block Cipher Modes of - Operation: Methods and Techniques", NIST Special - Pulication 800-38A, 2001 edition. - - [RFC2119] Bradner, S., "Key words for use in RFCs to Indicate - Requirement Levels", BCP 14, RFC 2119, March 1997. - - [RFC5116] McGrew, D., "An Interface and Algorithms for - Authenticated Encryption", RFC 5116, January 2008. - -9.2. Informative References - - [APPCRY] Menezes, A., van Oorshot, P., and S. Vanstone, "Handbook - of Applied Cryptography", CRC Press Series on Discrete - Mathematics and Its Applications, 1996. - - [BADESP] Bellovin, S., "Problem Areas for the IP Security - Protocols", Proceedings from the 6th Usenix UNIX Security - Symposium, July 22-25 1996. - - [RFC3610] Whiting, D., Housley, R., and N. Ferguson, "Counter with - CBC-MAC (CCM)", RFC 3610, September 2003. - - [DAE] Rogaway, P. and T. Shrimpton, "Deterministic - Authenticated Encryption, A Provable-Security Treatment - of the Key-Wrap Problem", Advances in Cryptology -- - EUROCRYPT '06 St. Petersburg, Russia, 2006. - - [GCM] McGrew, D. and J. Viega, "The Galois/Counter Mode of - Operation (GCM)". - - [JUTLA] Jutla, C., "Encryption Modes With Almost Free Message - Integrity", Proceedings of the International Conference - on the Theory and Application of Cryptographic - Techniques: Advances in Cryptography. - - [OCB] Krovetz, T. and P. Rogaway, "The OCB Authenticated - Encryption Algorithm", Work in Progress, March 2005. - - [RADKEY] Zorn, G., Zhang, T., Walker, J., and J. Salowey, "RADIUS - Attributes for the Delivery of Keying Material", Work in - Progress, April 2007. - - [RANDORCL] Bellare, M. and P. Rogaway, "Random Oracles are - Practical: A Paradigm for Designing Efficient - Protocols", Proceeding of the First ACM Conference on - Computer and Communications Security, November 1993. - - [RFC2104] Krawczyk, H., Bellare, M., and R. Canetti, "HMAC: Keyed- - Hashing for Message Authentication", RFC 2104, February - 1997. - - [RFC2548] Zorn, G., "Microsoft Vendor-specific RADIUS Attributes", - RFC 2548, March 1999. - - [RFC2865] Rigney, C., Willens, S., Rubens, A., and W. Simpson, - "Remote Authentication Dial In User Service (RADIUS)", - RFC 2865, June 2000. - - [RFC3217] Housley, R., "Triple-DES and RC2 Key Wrapping", RFC 3217, - December 2001. - - - [RFC3394] Schaad, J. and R. Housley, "Advanced Encryption Standard - (AES) Key Wrap Algorithm", RFC 3394, September 2002. - - [SP800-38D] Dworkin, M., "Recommendations for Block Cipher Modes of - Operation: Galois Counter Mode (GCM) and GMAC", NIST - Special Pulication 800-38D, June 2007. - - [VIRT] Garfinkel, T. and M. Rosenblum, "When Virtual is Harder - than Real: Security Challenges in Virtual Machine Based - Computing Environments" In 10th Workshop on Hot Topics in - Operating Systems, May 2005. - - [WLAN] "Draft Standard for IEEE802.11: Wireless LAN Medium - Access Control (MAC) and Physical Layer (PHY) - Specification", 2007. - - [X9F1] Dworkin, M., "Wrapping of Keys and Associated Data", - Request for review of key wrap algorithms. Cryptology - ePrint report 2004/340, 2004. Contents are excerpts from - a draft standard of the Accredited Standards Committee, - X9, entitled ANS X9.102. - - -Appendix A. Test Vectors - - The following test vectors are for the mode defined in Section 6.1. - -A.1. Deterministic Authenticated Encryption Example - - Input: - ----- - Key: - fffefdfc fbfaf9f8 f7f6f5f4 f3f2f1f0 - f0f1f2f3 f4f5f6f7 f8f9fafb fcfdfeff - - AD: - 10111213 14151617 18191a1b 1c1d1e1f - 20212223 24252627 - - Plaintext: - 11223344 55667788 99aabbcc ddee - -``` -property KAT1 = - sivEncrypt 0xfffefdfcfbfaf9f8f7f6f5f4f3f2f1f0f0f1f2f3f4f5f6f7f8f9fafbfcfdfeff - 0x101112131415161718191a1b1c1d1e1f2021222324252627 - 0x112233445566778899aabbccddee - == 0x85632d07c6e8f37f950acd320a2ecc9340c02b9690c4dc04daef7f6afe5c - -enc_dec : {ad,p} (fin ad, fin p, 2^^71 - 128 >= p) => [256] -> [ad] -> [p] -> Bit -property enc_dec k ad p = (sivDecrypt k ad (sivEncrypt k ad p)).1 == p - -// `encrypt . decrypt ~ ident` for inputs larger, equal to, and smaller than the block size -// Expect ~20 minutes for ABC to prove each property -property enc_dec_ll k ad p = enc_dec `{431,500} k ad p -property enc_dec_el k ad p = enc_dec `{128,140} k ad p -property enc_dec_le k ad p = enc_dec `{148,128} k ad p -property enc_dec_se k ad p = enc_dec `{18,128} k ad p -property enc_dec_es k ad p = enc_dec `{128,18} k ad p -property enc_dec_sl k ad p = enc_dec `{12,180} k ad p -property enc_dec_ls k ad p = enc_dec `{140,18} k ad p -property enc_dec_ee k ad p = enc_dec `{128,128} k ad p -property enc_dec_ss k ad p = enc_dec `{50,80} k ad p - -property enc_dec_block k ad p = (sivDecrypt k (ad : [50]) (sivEncrypt k ad p)).1 == (p : [500]) -``` - - S2V-CMAC-AES - ------------ - CMAC(zero): - 0e04dfaf c1efbf04 01405828 59bf073a - - double(): - 1c09bf5f 83df7e08 0280b050 b37e0e74 - - CMAC(ad): - f1f922b7 f5193ce6 4ff80cb4 7d93f23b - - xor: - edf09de8 76c642ee 4d78bce4 ceedfc4f - - double(): - dbe13bd0 ed8c85dc 9af179c9 9ddbf819 - - pad: - 11223344 55667788 99aabbcc ddee8000 - - xor: - cac30894 b8eaf254 035bc205 40357819 - - CMAC(final): - 85632d07 c6e8f37f 950acd32 0a2ecc93 - - CTR-AES - ------- - CTR: - 85632d07 c6e8f37f 150acd32 0a2ecc93 - - E(K,CTR): - 51e218d2 c5a2ab8c 4345c4a6 23b2f08f - - ciphertext: - 40c02b96 90c4dc04 daef7f6a fe5c - - output - ------ - IV || C: - 85632d07 c6e8f37f 950acd32 0a2ecc93 - 40c02b96 90c4dc04 daef7f6a fe5c - -A.2. Nonce-Based Authenticated Encryption Example - - Input: - ----- - Key: - 7f7e7d7c 7b7a7978 77767574 73727170 - 40414243 44454647 48494a4b 4c4d4e4f - - AD1: - 00112233 44556677 8899aabb ccddeeff - deaddada deaddada ffeeddcc bbaa9988 - 77665544 33221100 - - AD2: - 10203040 50607080 90a0 - - Nonce: - 09f91102 9d74e35b d84156c5 635688c0 - - Plaintext: - 74686973 20697320 736f6d65 20706c61 - 696e7465 78742074 6f20656e 63727970 - 74207573 696e6720 5349562d 414553 - - S2V-CMAC-AES - ------------ - CMAC(zero): - c8b43b59 74960e7c e6a5dd85 231e591a - - double(): - 916876b2 e92c1cf9 cd4bbb0a 463cb2b3 - - CMAC(ad1) - 3c9b689a b41102e4 80954714 1dd0d15a - - xor: - adf31e28 5d3d1e1d 4ddefc1e 5bec63e9 - - double(): - 5be63c50 ba7a3c3a 9bbdf83c b7d8c755 - - CMAC(ad2) - d98c9b0b e42cb2d7 aa98478e d11eda1b - - xor: - 826aa75b 5e568eed 3125bfb2 66c61d4e - - double(): - 04d54eb6 bcad1dda 624b7f64 cd8c3a1b - - CMAC(nonce) - 128c62a1 ce3747a8 372c1c05 a538b96d - - xor: - 16592c17 729a5a72 55676361 68b48376 - - xorend: - 74686973 20697320 736f6d65 20706c61 - 696e7465 78742074 6f20656e 63727966 - 2d0c6201 f3341575 342a3745 f5c625 - - CMAC(final) - 7bdb6e3b 432667eb 06f4d14b ff2fbd0f - - - - CTR-AES - ------- - CTR: - 7bdb6e3b 432667eb 06f4d14b 7f2fbd0f - - E(K,CTR): - bff8665c fdd73363 550f7400 e8f9d376 - - CTR+1: - 7bdb6e3b 432667eb 06f4d14b 7f2fbd10 - - E(K,CTR+1): - b2c9088e 713b8617 d8839226 d9f88159 - - CTR+2 - 7bdb6e3b 432667eb 06f4d14b 7f2fbd11 - - E(K,CTR+2): - 9e44d827 234949bc 1b12348e bc195ec7 - - ciphertext: - cb900f2f ddbe4043 26601965 c889bf17 - dba77ceb 094fa663 b7a3f748 ba8af829 - ea64ad54 4a272e9c 485b62a3 fd5c0d - - output - ------ - IV || C: - 7bdb6e3b 432667eb 06f4d14b ff2fbd0f - cb900f2f ddbe4043 26601965 c889bf17 - dba77ceb 094fa663 b7a3f748 ba8af829 - ea64ad54 4a272e9c 485b62a3 fd5c0d - -Author's Address - - Dan Harkins - Aruba Networks - - EMail: dharkins@arubanetworks.com - - -Full Copyright Statement - - Copyright (C) The IETF Trust (2008). - - This document is subject to the rights, licenses and restrictions - contained in BCP 78, and except as set forth therein, the authors - retain all their rights. - - This document and the information contained herein are provided on an - "AS IS" basis and THE CONTRIBUTOR, THE ORGANIZATION HE/SHE REPRESENTS - OR IS SPONSORED BY (IF ANY), THE INTERNET SOCIETY, THE IETF TRUST AND - THE INTERNET ENGINEERING TASK FORCE DISCLAIM ALL WARRANTIES, EXPRESS - OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTY THAT THE USE OF - THE INFORMATION HEREIN WILL NOT INFRINGE ANY RIGHTS OR ANY IMPLIED - WARRANTIES OF MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. - -Intellectual Property - - The IETF takes no position regarding the validity or scope of any - Intellectual Property Rights or other rights that might be claimed to - pertain to the implementation or use of the technology described in - this document or the extent to which any license under such rights - might or might not be available; nor does it represent that it has - made any independent effort to identify any such rights. Information - on the procedures with respect to rights in RFC documents can be - found in BCP 78 and BCP 79. - - Copies of IPR disclosures made to the IETF Secretariat and any - assurances of licenses to be made available, or the result of an - attempt made to obtain a general license or permission for the use of - such proprietary rights by implementers or users of this - specification can be obtained from the IETF on-line IPR repository at - http://www.ietf.org/ipr. - - The IETF invites any interested party to bring to its attention any - copyrights, patents or patent applications, or other proprietary - rights that may cover technology that may be required to implement - this standard. Please address the information to the IETF at - ietf-ipr@ietf.org. diff --git a/examples/Salsa20.cry b/examples/Salsa20.cry deleted file mode 100644 index 782d5d96..00000000 --- a/examples/Salsa20.cry +++ /dev/null @@ -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 | 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 | 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 diff --git a/examples/Threefish.cry b/examples/Threefish.cry deleted file mode 100644 index a5acbdd7..00000000 --- a/examples/Threefish.cry +++ /dev/null @@ -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 diff --git a/examples/TripleDES.cry b/examples/TripleDES.cry deleted file mode 100644 index c8657099..00000000 --- a/examples/TripleDES.cry +++ /dev/null @@ -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 diff --git a/examples/ZUC.cry b/examples/ZUC.cry deleted file mode 100644 index 28a83ce1..00000000 --- a/examples/ZUC.cry +++ /dev/null @@ -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 diff --git a/examples/contrib/bivium.cry b/examples/contrib/bivium.cry deleted file mode 100644 index 2d667baf..00000000 --- a/examples/contrib/bivium.cry +++ /dev/null @@ -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 diff --git a/examples/contrib/keccak.cry b/examples/contrib/keccak.cry deleted file mode 100644 index 381e3062..00000000 --- a/examples/contrib/keccak.cry +++ /dev/null @@ -1,181 +0,0 @@ -/* - * Copyright (c) 2013 David Lazar - * - * 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 diff --git a/examples/contrib/simon.cry b/examples/contrib/simon.cry deleted file mode 100644 index ca1fc6e2..00000000 --- a/examples/contrib/simon.cry +++ /dev/null @@ -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) diff --git a/examples/contrib/speck.cry b/examples/contrib/speck.cry deleted file mode 100644 index 3f9b973c..00000000 --- a/examples/contrib/speck.cry +++ /dev/null @@ -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) diff --git a/examples/contrib/trivium.cry b/examples/contrib/trivium.cry deleted file mode 100644 index c2c0716c..00000000 --- a/examples/contrib/trivium.cry +++ /dev/null @@ -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) diff --git a/tests/issues/allexamples.icry b/tests/issues/allexamples.icry index f813e7a0..1b74cce8 100644 --- a/tests/issues/allexamples.icry +++ b/tests/issues/allexamples.icry @@ -6,18 +6,8 @@ :l Cipher.cry :l DES.cry :l DEStest.cry -:l FNV-a1.cry -:l HMAC.cry :l Karatsuba.cry -:l MD5.cry -:l SHA1.cry -:l SHA256.cry -:l SIV-rfc5297.md -:l Salsa20.cry :l Test.cry -:l Threefish.cry -:l TripleDES.cry -:l ZUC.cry :l append.cry :l builtin_lifting.cry :l builtins.cry @@ -36,12 +26,7 @@ :l contrib/EvenMansour.cry :l contrib/MISTY1.cry :l contrib/RC4.cry -:l contrib/bivium.cry -:l contrib/keccak.cry :l contrib/mkrand.cry -:l contrib/simon.cry -:l contrib/speck.cry -:l contrib/trivium.cry :l funstuff/Coins.cry :l funstuff/FoxChickenCorn.cry :l funstuff/NQueens.cry diff --git a/tests/issues/allexamples.icry.stdout b/tests/issues/allexamples.icry.stdout index 6caf5ce0..3c2d00cc 100644 --- a/tests/issues/allexamples.icry.stdout +++ b/tests/issues/allexamples.icry.stdout @@ -26,39 +26,11 @@ Loading module DES Loading module Test Loading module DEStest Loading module Cryptol -Loading module Main -Loading module Cryptol -Loading module SHA256 -Loading module HMAC -Loading module Cryptol Loading module Karatsuba 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 Test 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 Cryptol Loading module Main @@ -97,18 +69,8 @@ Loading module MISTY1 Loading module Cryptol Loading module Main Loading module Cryptol -Loading module Main -Loading module Cryptol -Loading module Main -Loading module Cryptol Loading module MKRAND 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 Cryptol Loading module FoxChickenCorn