From 86aab13dc4c59f2ae8c3f962fce61e48dfc412f3 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Thu, 4 Sep 2025 20:58:32 -0700 Subject: [PATCH] Comments and fix error introduce in previous cleanup --- Ascon.cry | 42 +++++++++++++++++++++++++----------------- 1 file changed, 25 insertions(+), 17 deletions(-) diff --git a/Ascon.cry b/Ascon.cry index df98a57..dda685c 100644 --- a/Ascon.cry +++ b/Ascon.cry @@ -1,16 +1,22 @@ -/** - -Implementation of Ascon-Based Lightweight Cryptography - -Reference: - -Meltem Sönmez Turan, Kerry A. McKay, Donghoon Chang, Jinkeon Kang, -John Kelsey (2025) Ascon-Based Lightweight Cryptography Standards -for Constrained Devices. (National Institute of Standards and Technology, -Gaithersburg, MD), NIST Special Publication (SP) NIST SP 800-232. -https://doi.org/10.6028/NIST.SP.800-232 - -*/ +/** Implementation of Ascon-Based Lightweight Cryptography + * + * Author: Eric Mertens + * + * Key algorithms: + * - Ascon_p: Core permutation function + * - AEAD128_encrypt/decrypt: Authenticated encryption + * - Hash256: Cryptographic hash function + * - XOF128: Extendable output function + * - CXOF128: Customizable extendable output function + * + * Reference: + * + * Meltem Sönmez Turan, Kerry A. McKay, Donghoon Chang, Jinkeon Kang, + * John Kelsey (2025) Ascon-Based Lightweight Cryptography Standards + * for Constrained Devices. (National Institute of Standards and Technology, + * Gaithersburg, MD), NIST Special Publication (SP) NIST SP 800-232. + * https://doi.org/10.6028/NIST.SP.800-232 + */ module Ascon where // 2.1. Auxiliary Functions @@ -55,7 +61,10 @@ type constraint ValidRnd rnd = rnd <= 16 Ascon_p : {rnd} (ValidRnd rnd) => State -> State Ascon_p S = foldl round S (drop`{back=rnd} Const) -/** Single round of the Ascon-p permutation. */ +/** + * Single round of the Ascon-p permutation parameterized by the round + * constant. + */ round : State -> [64] -> State round S ci = pL (pS (pC S ci)) @@ -217,7 +226,7 @@ AEAD128_decrypt K N A (Cs_ # Cl # T) = S0 = Ascon_p`{12} [Ascon_AEAD128_IV, K0, K1, N0, N1] ^ [0, 0, 0, K0, K1] SA = AddAD S0 A - Cs = split`{p/128, 128} Cs_ + Cs = split`{p / 128} Cs_ SCs # [SCl] = [SA] # [Ascon_p`{8} (AssignC s c) | s <- SCs | c <- Cs] Masks = map ExtractC SCs @@ -225,8 +234,7 @@ AEAD128_decrypt K N A (Cs_ # Cl # T) = Maskl # SCl' = ExtractC SCl Sl' = AssignC SCl (Cl # (0b1#0 ^ SCl')) - Ps = zipWith (\x y -> ExtractC x ^ y) SCs Cs - P = join (Ps ^ Masks) # (Maskl ^ Cl) + P = join (Masks ^ Cs) # (Maskl ^ Cl) ST = Ascon_p`{12} (Sl' ^ [0, 0, K0, K1, 0]) T' = ExtractT ST ^ K