diff --git a/Ascon.cry b/Ascon.cry index 21c1244..4ba78e8 100644 --- a/Ascon.cry +++ b/Ascon.cry @@ -147,7 +147,8 @@ private ] property - SBoxCorrect x0 x1 x2 x3 x4 = [y0, y1, y2, y3, y4] == SBox [x0, x1, x2, x3, x4] + SBoxCorrect x0 x1 x2 x3 x4 = + [y0, y1, y2, y3, y4] == SBox [x0, x1, x2, x3, x4] where y0 = x4&&x1 ^ x3 ^ x2&&x1 ^ x2 ^ x1&&x0 ^ x1 ^ x0 y1 = x4 ^ x3&&x2 ^ x3&&x1 ^ x3 ^ x2&&x1 ^ x2 ^ x1 ^ x0 @@ -157,7 +158,9 @@ private // 3.4. Linear Diffusion Layer pL - /** The linear diffusion layer 𝑝𝐿 provides diffusion within each 64-bit word 𝑆𝑖. */ + /** The linear diffusion layer 𝑝𝐿 provides diffusion within each 64-bit + * word 𝑆𝑖. + */ pL : State -> State pL [S0, S1, S2, S3, S4] = [ sigma S0 19 28 @@ -195,27 +198,37 @@ private * Returns: * - Authenticated ciphertext */ -AEAD128_encrypt : {a, p} (fin a, fin p) => [128] -> [128] -> [a] -> [p] -> [p + 128] -AEAD128_encrypt K N A P = C # T +AEAD128_encrypt : + {a, p} (fin a, fin p) => + [128] -> [128] -> [a] -> [p] -> ([p], [128]) +AEAD128_encrypt K N A P = (C, T) where [K0, K1] = bitsToWords K [N0, N1] = bitsToWords N - // 𝑆 ← 𝐼𝑉 β€– 𝐾 β€– 𝑁 (15) - // 𝑆 ← Ascon-p[12](𝑆) (16) - // 𝑆 ← 𝑆 βŠ• (0¹⁹² β€– K) (17) + // 𝑆 ← 𝐼𝑉 β€– 𝐾 β€– 𝑁 (15) + // 𝑆 ← Ascon-p[12](𝑆) (16) + // 𝑆 ← 𝑆 βŠ• (0¹⁹² β€– 𝐾) (17) S0 = Ascon_p`{12} [AEAD128_IV, K0, K1, N0, N1] ^ [0, 0, 0, K0, K1] SA = AddAD S0 A - // 𝑃₀, 𝑃₁, …, 𝑃ₙ₋₁, 𝑃͠ₙ ← parse(𝑃,128) (23) + // 𝑃₀, 𝑃₁, …, 𝑃ₙ₋₁, 𝑃͠ₙ ← parse(𝑃,128) (23) // For each 𝑃ᡒ, 0 ≀ 𝑖 ≀ π‘›βˆ’1 - // 𝑆[0:127] ← 𝑆[0:127] βŠ• 𝑃ᡒ (24) - // 𝐢ᡒ ← 𝑆[0:127] (25) - // 𝑆 ← Ascon-p[8](𝑆) (26) + // 𝑆[0:127] ← 𝑆[0:127] βŠ• 𝑃ᡒ (24) + // 𝐢ᡒ ← 𝑆[0:127] (25) + // 𝑆 ← Ascon-p[8](𝑆) (26) + // For the last block 𝑃͠ₙ + // 𝑆[0:127] ← 𝑆[0:127] βŠ• pad(𝑃͠ₙ,128) (27) + // 𝐢͠ₙ ← 𝑆[0:β„“βˆ’1] (28) SCs = [XorBlock s p | s <- [SA] # map Ascon_p`{8} SCs | p <- toBlocks P] + + // 𝐢 ← 𝐢₀ β€– … β€– 𝐢ₙ₋₁ β€– 𝐢͠ₙ (29) C = take (join (map ExtractC SCs)) + // 𝑆 ← 𝑆 βŠ• (0¹²⁸ β€– 𝐾 β€– 0⁢⁴) (30) + // 𝑆 ← Ascon-p[12](𝑆) (31) + // 𝑇 ← 𝑆[192:319] βŠ• 𝐾 (32) ST = Ascon_p`{12} (last SCs ^ [0, 0, K0, K1, 0]) T = ExtractT ST ^ K @@ -235,8 +248,17 @@ AEAD128_encrypt K N A P = C # T * - Some plaintext on authentication success * - None on authentication failure */ -AEAD128_decrypt : {a, p} (fin a, fin p) => [128] -> [128] -> [a] -> [p + 128] -> Option [p] -AEAD128_decrypt K N A (C # T) = if T == T' then Some P else None +AEAD128_decrypt : + {a, p} (fin a, fin p) => + [128] -> [128] -> [a] -> [p] -> [128] -> Option [p] +AEAD128_decrypt K N A C T1 = if T1 == T2 then Some P else None + where + (P, T2) = AEAD128_decrypt_raw K N A C + +AEAD128_decrypt_raw : + {a, p} (fin a, fin p) => + [128] -> [128] -> [a] -> [p] -> ([p], [128]) +AEAD128_decrypt_raw K N A C = (P, T) where // key and nonce as two 64-bit integers [K0, K1] = bitsToWords K @@ -254,7 +276,7 @@ AEAD128_decrypt K N A (C # T) = if T == T' then Some P else None Cl = Cl1 # (0b1#0 ^ Cl2) // xor toggles the padding bit ST1 = AssignC (last SCs) Cl ST2 = Ascon_p`{12} (ST1 ^ [0, 0, K0, K1, 0]) - T' = ExtractT ST2 ^ K + T = ExtractT ST2 ^ K /** Ascon-AEAD128 encryption algorithm on bytes. * @@ -271,9 +293,16 @@ AEAD128_decrypt K N A (C # T) = if T == T' then Some P else None * Returns: * - Authenticated ciphertext */ -AEAD128_encrypt_bytes : {a, p} (fin a, fin p) => [16][8] -> [16][8] -> [a][8] -> [p][8] -> [p + 16][8] -AEAD128_encrypt_bytes K N A P = - bitsToWords (AEAD128_encrypt (wordsToBits K) (wordsToBits N) (wordsToBits A) (wordsToBits P)) +AEAD128_encrypt_bytes : + {a, p} (fin a, fin p) => + [16][8] -> [16][8] -> [a][8] -> [p][8] -> ([p][8], [16][8]) +AEAD128_encrypt_bytes K N A P = (bitsToWords C, bitsToWords T) + where + (C, T) = AEAD128_encrypt K' N' A' P' + K' = wordsToBits K + N' = wordsToBits N + A' = wordsToBits A + P' = wordsToBits P /** Ascon-AEAD128 decryption algorithm on bytes. * @@ -291,11 +320,19 @@ AEAD128_encrypt_bytes K N A P = * - Some plaintext on authentication success * - None on authentication failure */ -AEAD128_decrypt_bytes : {a, p} (fin a, fin p) => [16][8] -> [16][8] -> [a][8] -> [p + 16][8] -> Option ([p][8]) -AEAD128_decrypt_bytes K N A C = - case AEAD128_decrypt (wordsToBits K) (wordsToBits N) (wordsToBits A) (wordsToBits C) of +AEAD128_decrypt_bytes : + {a, p} (fin a, fin p) => + [16][8] -> [16][8] -> [a][8] -> [p][8] -> [16][8] -> Option ([p][8]) +AEAD128_decrypt_bytes K N A C T = + case AEAD128_decrypt K' N' A' C' T' of None -> None Some p -> Some (bitsToWords p) + where + K' = wordsToBits K + N' = wordsToBits N + A' = wordsToBits A + C' = wordsToBits C + T' = wordsToBits T private /** Absorb all of the associated data into the permutation state. */ @@ -328,7 +365,8 @@ private /** Add a single block of data into the permutation state. */ XorBlock : State -> [128] -> State - XorBlock [s0, s1, s2, s3, s4] (xhi # xlo) = [s0 ^ xlo, s1 ^ xhi, s2, s3, s4] + XorBlock [s0, s1, s2, s3, s4] (xhi # xlo) = + [s0 ^ xlo, s1 ^ xhi, s2, s3, s4] /** Extracts the first two words of permutation state as a bitstream. */ ExtractC : State -> [128] @@ -350,6 +388,9 @@ private private /** Hash function construction + * + * All three of the modes in Ascon use the same message + * absorbtion and * * Parameters: * - Initialization vector @@ -359,13 +400,25 @@ private * - Infinite message digest bitstream to be truncated by caller */ hashBlocks : {n} (fin n) => [64] -> [n][64] -> [inf] - hashBlocks IV Ms = wordsToBits [head S | S <- iterate Ascon_p`{12} Sn] + hashBlocks IV Ms = H where + // 𝑆 ← Ascon-p[12](𝐼𝑉 β€– 0²⁡⁢) (54) S0 = Ascon_p`{12} [IV, 0, 0, 0, 0] + + // Each message block 𝑀ᡒ is XORed with the state as + // 𝑆[0:63] ← 𝑆[0:63] βŠ• 𝑀ᡒ (57) + // 𝑆 ← Ascon-p[12](𝑆) (58) Sn = foldl AbsorbBlock64 S0 Ms + // Each output hash block is computed as + // 𝐻ᡒ ← 𝑆[0:63] (60) + // 𝑆 ← Ascon-p[12](𝑆) (61) + // 𝐻ᡒ ← 𝐻₀ β€– 𝐻₁ β€– … + H = wordsToBits [head S | S <- iterate Ascon_p`{12} Sn] + + /** Absorb a block of hash input into the permutation state. */ AbsorbBlock64 : State -> [64] -> State - AbsorbBlock64 [s0, s1, s2, s3, s4] X = Ascon_p`{12} [X ^ s0, s1, s2, s3, s4] + AbsorbBlock64 [s0, s1, s2, s3, s4] Mi = Ascon_p`{12} [s0 ^ Mi, s1, s2, s3, s4] // 5.1. Specification of Ascon-Hash256 @@ -453,10 +506,12 @@ private XOF128_IV = 0x0000080000cc0003 * Returns: * - Variable-length message digest */ -CXOF128 : {r, c, m} (fin m, fin r, fin c, 64 >= width c) => [c] -> [m] -> [r] +CXOF128 : + {r, z, m} (fin m, fin r, 64 >= width z) => + [z] -> [m] -> [r] CXOF128 Z M = take (hashBlocks CXOF128_IV Ms) where - Ms = [`c] + Ms = [`z] # toBlocks Z # toBlocks M @@ -464,7 +519,7 @@ CXOF128 Z M = take (hashBlocks CXOF128_IV Ms) * * Type parameters: * - r: Byte-length of digest - * - c: Byte-length of customization string + * - z: Byte-length of customization string * - m: Byte-length of message * * Parameters: @@ -474,9 +529,30 @@ CXOF128 Z M = take (hashBlocks CXOF128_IV Ms) * Returns: * - Variable-length message digest */ -CXOF128_bytes : {r, z, m} (fin m, fin r, 61 >= width z) => [z][8] -> [m][8] -> [r][8] +CXOF128_bytes : + {r, z, m} (fin m, fin r, 61 >= width z) => + [z][8] -> [m][8] -> [r][8] CXOF128_bytes Z M = bitsToWords (CXOF128 (wordsToBits Z) (wordsToBits M)) /** Ascon-CXOF128 initialization vector */ CXOF128_IV : [64] private CXOF128_IV = 0x0000080000cc0004 + +// Appendix B. Determination of the Initial Values + +private + computeIV : [8] -> [4] -> [4] -> [16] -> [8] -> [64] + computeIV v a b t r = + // 𝐼𝑉 = 𝑣 β€– 0⁸ β€– π‘Ž β€– 𝑏 β€– 𝑑 β€– π‘Ÿ/8 β€– 0¹⁢ + reverse ( reverse v // is a unique identifier for the algorithm + # (0:[8]) + # reverse a // is the number of rounds during initialization and finalization + # reverse b // is the number of rounds during the processing of AD, P, C, M + # reverse t // is 128 for AEAD128, 256 for Hash256, and 0 for XOF128/CXOF128 + # reverse r // is the number of input bytes processed per permutation invocation + # (0:[16])) + + property check_AEAD128_IV = AEAD128_IV == computeIV 1 12 8 128 16 + property check_Hash256_IV = Hash256_IV == computeIV 2 12 12 256 8 + property check_XOF128_IV = XOF128_IV == computeIV 3 12 12 0 8 + property check_CXOF128_IV = CXOF128_IV == computeIV 4 12 12 0 8