🐣

Ascon.cry

@@ -0,0 +1,87 @@
+/**
+
+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
+
+*/
+module Ascon where
+
+// 3. Ascon Permutations
+
+type constraint ValidRnd rnd = (1 <= rnd, rnd <= 16)
+
+Ascon_p : {rnd} (ValidRnd rnd) => State -> State
+Ascon_p S = foldl p`{rnd} S (drop`{back=rnd} Const)
+
+p : {rnd} (ValidRnd rnd) => State -> [64] -> State
+p S ci = pL (pS (pC S ci))
+
+// 3.1. Internal State
+
+type State = [5][64]
+
+// 3.2. Constant-Addition Layer pC 
+
+pC : State -> [64] -> State
+pC [S0, S1, S2, S3, S4] ci = [S0, S1, S2 ^ ci, S3, S4]
+
+/// Table 5. The constants constᵢ to derive round constants of the Ascon permutations
+Const : [16][64]
+Const =
+    [ 0x000000000000003c
+    , 0x000000000000002d
+    , 0x000000000000001e
+    , 0x000000000000000f
+    , 0x00000000000000f0
+    , 0x00000000000000e1
+    , 0x00000000000000d2
+    , 0x00000000000000c3
+    , 0x00000000000000b4
+    , 0x00000000000000a5
+    , 0x0000000000000096
+    , 0x0000000000000087
+    , 0x0000000000000078
+    , 0x0000000000000069
+    , 0x000000000000005a
+    , 0x000000000000004b
+    ]
+
+// 3.3. Substitution Layer pS
+
+pS : State -> State
+pS S = transpose (map SBox (transpose S))
+
+SBox : [5] -> [5]
+SBox i = SBoxTable@i
+
+/// Table 6.
+SBoxTable : [32][5]
+SBoxTable =
+    map drop
+    [ 0x04, 0x0b, 0x1f, 0x14, 0x1a, 0x15, 0x09, 0x02, 0x1b, 0x05, 0x08, 0x12, 0x1d, 0x03, 0x06, 0x1c
+    , 0x1e, 0x13, 0x07, 0x0e, 0x00, 0x0d, 0x11, 0x18, 0x10, 0x0c, 0x01, 0x19, 0x16, 0x0a, 0x0f, 0x17
+    ]
+
+// 3.4. Linear Diffusion Layer pL
+
+pL : State -> State
+pL [S0, S1, S2, S3, S4] =
+    [ sigma S0 19 28
+    , sigma S1 61 39
+    , sigma S2  1  6
+    , sigma S3 10 17
+    , sigma S4  7 41
+    ]
+    where
+        sigma : [64] -> [6] -> [6] -> [64]
+        sigma x i j = x ^ (x >>> i) ^ (x >>> j)
+
+LE : {n} (fin n, n % 8 == 0) => [n] -> [n]
+LE x = join (reverse (split`{n / 8, 8} x))

AsconHash256.cry

@@ -0,0 +1,31 @@
+module AsconHash256 where
+
+import Ascon
+
+parse : {r, n} (fin n, fin r, 0 < r) => [n] -> ([n/r][r], [n%r])
+parse (M_ # Ml) = (split M_, Ml)
+
+pad : {n} (n < 64) => [n] -> [64]
+pad M = bs # b # zero
+  where
+    bs : [n/8*8]
+    b_ : [n%8]
+    bs # b_ = M
+    b : [8]
+    b = zext`{8} (0b1 # b_)
+
+/// 5.1. Specification of Ascon-Hash256
+Ascon_Hash256 : {n} (fin n) => [n] -> [256]
+Ascon_Hash256 M =
+    join [LE (head S) | S <- take (iterate Ascon_p`{12} Sn)]
+    where
+    (M1, M2) = parse M
+    M2' = pad M2
+    M' = M1 # [pad M2]
+
+    AddBlock [s0, s1, s2, s3, s4] X = Ascon_p`{12} [LE X ^ s0, s1, s2, s3, s4]
+    S0 = Ascon_p`{12} [Ascon_Hash256_IV, 0, 0, 0, 0]
+    Sn = foldl AddBlock S0 M'
+
+Ascon_Hash256_IV : [64]
+Ascon_Hash256_IV = 0x0000080100cc0002