glguy/ascon
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Documentation and layout

Browse Source
This commit is contained in:
Eric Mertens
2025-09-07 17:37:10 -07:00
parent 639ad1f1dd
commit 1acbbe633f
1 changed files with 103 additions and 27 deletions
Download Patch File Download Diff File Expand all files Collapse all files

118
Ascon.cry
View File

@@ -147,7 +147,8 @@ private
] ]
property 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 where
y0 = x4&&x1 ^ x3 ^ x2&&x1 ^ x2 ^ x1&&x0 ^ x1 ^ x0 y0 = x4&&x1 ^ x3 ^ x2&&x1 ^ x2 ^ x1&&x0 ^ x1 ^ x0
y1 = x4 ^ x3&&x2 ^ x3&&x1 ^ x3 ^ x2&&x1 ^ x2 ^ 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 // 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 : State -> State
pL [S0, S1, S2, S3, S4] = pL [S0, S1, S2, S3, S4] =
[ sigma S0 19 28 [ sigma S0 19 28
@@ -195,15 +198,17 @@ private
* Returns: * Returns:
* - Authenticated ciphertext * - Authenticated ciphertext
*/ */
AEAD128_encrypt : {a, p} (fin a, fin p) => [128] -> [128] -> [a] -> [p] -> [p + 128] AEAD128_encrypt :
AEAD128_encrypt K N A P = C # T {a, p} (fin a, fin p) =>
[128] -> [128] -> [a] -> [p] -> ([p], [128])
AEAD128_encrypt K N A P = (C, T)
where where
[K0, K1] = bitsToWords K [K0, K1] = bitsToWords K
[N0, N1] = bitsToWords N [N0, N1] = bitsToWords N
// 𝑆 ← 𝐼𝑉 ‖ 𝐾 ‖ 𝑁 (15) // 𝑆 ← 𝐼𝑉 ‖ 𝐾 ‖ 𝑁 (15)
// 𝑆 ← Ascon-p[12](𝑆) (16) // 𝑆 ← Ascon-p[12](𝑆) (16)
// 𝑆 ← 𝑆 ⊕ (0¹⁹² ‖ K) (17) // 𝑆 ← 𝑆 ⊕ (0¹⁹² ‖ 𝐾) (17)
S0 = Ascon_p`{12} [AEAD128_IV, K0, K1, N0, N1] ^ [0, 0, 0, K0, K1] S0 = Ascon_p`{12} [AEAD128_IV, K0, K1, N0, N1] ^ [0, 0, 0, K0, K1]
SA = AddAD S0 A SA = AddAD S0 A
@@ -213,9 +218,17 @@ AEAD128_encrypt K N A P = C # T
// 𝑆[0:127] ← 𝑆[0:127] ⊕ 𝑃ᵢ (24) // 𝑆[0:127] ← 𝑆[0:127] ⊕ 𝑃ᵢ (24)
// 𝐶ᵢ ← 𝑆[0:127] (25) // 𝐶ᵢ ← 𝑆[0:127] (25)
// 𝑆 ← Ascon-p[8](𝑆) (26) // 𝑆 ← 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] SCs = [XorBlock s p | s <- [SA] # map Ascon_p`{8} SCs | p <- toBlocks P]
// 𝐶 ← 𝐶₀ ‖ … ‖ 𝐶ₙ₋₁ ‖ 𝐶͠ₙ (29)
C = take (join (map ExtractC SCs)) 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]) ST = Ascon_p`{12} (last SCs ^ [0, 0, K0, K1, 0])
T = ExtractT ST ^ K T = ExtractT ST ^ K
@@ -235,8 +248,17 @@ AEAD128_encrypt K N A P = C # T
* - Some plaintext on authentication success * - Some plaintext on authentication success
* - None on authentication failure * - None on authentication failure
*/ */
AEAD128_decrypt : {a, p} (fin a, fin p) => [128] -> [128] -> [a] -> [p + 128] -> Option [p] AEAD128_decrypt :
AEAD128_decrypt K N A (C # T) = if T == T' then Some P else None {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 where
// key and nonce as two 64-bit integers // key and nonce as two 64-bit integers
[K0, K1] = bitsToWords K [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 Cl = Cl1 # (0b1#0 ^ Cl2) // xor toggles the padding bit
ST1 = AssignC (last SCs) Cl ST1 = AssignC (last SCs) Cl
ST2 = Ascon_p`{12} (ST1 ^ [0, 0, K0, K1, 0]) ST2 = Ascon_p`{12} (ST1 ^ [0, 0, K0, K1, 0])
T' = ExtractT ST2 ^ K T = ExtractT ST2 ^ K
/** Ascon-AEAD128 encryption algorithm on bytes. /** 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: * Returns:
* - Authenticated ciphertext * - 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 :
AEAD128_encrypt_bytes K N A P = {a, p} (fin a, fin p) =>
bitsToWords (AEAD128_encrypt (wordsToBits K) (wordsToBits N) (wordsToBits A) (wordsToBits 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. /** Ascon-AEAD128 decryption algorithm on bytes.
* *
@@ -291,11 +320,19 @@ AEAD128_encrypt_bytes K N A P =
* - Some plaintext on authentication success * - Some plaintext on authentication success
* - None on authentication failure * - 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 :
AEAD128_decrypt_bytes K N A C = {a, p} (fin a, fin p) =>
case AEAD128_decrypt (wordsToBits K) (wordsToBits N) (wordsToBits A) (wordsToBits C) of [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 None -> None
Some p -> Some (bitsToWords p) Some p -> Some (bitsToWords p)
where
K' = wordsToBits K
N' = wordsToBits N
A' = wordsToBits A
C' = wordsToBits C
T' = wordsToBits T
private private
/** Absorb all of the associated data into the permutation state. */ /** 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. */ /** Add a single block of data into the permutation state. */
XorBlock : State -> [128] -> 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. */ /** Extracts the first two words of permutation state as a bitstream. */
ExtractC : State -> [128] ExtractC : State -> [128]
@@ -350,6 +388,9 @@ private
private private
/** Hash function construction /** Hash function construction
*
* All three of the modes in Ascon use the same message
* absorbtion and
* *
* Parameters: * Parameters:
* - Initialization vector * - Initialization vector
@@ -359,13 +400,25 @@ private
* - Infinite message digest bitstream to be truncated by caller * - Infinite message digest bitstream to be truncated by caller
*/ */
hashBlocks : {n} (fin n) => [64] -> [n][64] -> [inf] 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 where
// 𝑆 ← Ascon-p[12](𝐼𝑉 ‖ 0²⁵⁶) (54)
S0 = Ascon_p`{12} [IV, 0, 0, 0, 0] 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 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 : 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 // 5.1. Specification of Ascon-Hash256
@@ -453,10 +506,12 @@ private XOF128_IV = 0x0000080000cc0003
* Returns: * Returns:
* - Variable-length message digest * - 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) CXOF128 Z M = take (hashBlocks CXOF128_IV Ms)
where where
Ms = [`c] Ms = [`z]
# toBlocks Z # toBlocks Z
# toBlocks M # toBlocks M
@@ -464,7 +519,7 @@ CXOF128 Z M = take (hashBlocks CXOF128_IV Ms)
* *
* Type parameters: * Type parameters:
* - r: Byte-length of digest * - r: Byte-length of digest
* - c: Byte-length of customization string * - z: Byte-length of customization string
* - m: Byte-length of message * - m: Byte-length of message
* *
* Parameters: * Parameters:
@@ -474,9 +529,30 @@ CXOF128 Z M = take (hashBlocks CXOF128_IV Ms)
* Returns: * Returns:
* - Variable-length message digest * - 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)) CXOF128_bytes Z M = bitsToWords (CXOF128 (wordsToBits Z) (wordsToBits M))
/** Ascon-CXOF128 initialization vector */ /** Ascon-CXOF128 initialization vector */
CXOF128_IV : [64] CXOF128_IV : [64]
private CXOF128_IV = 0x0000080000cc0004 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