Add CXOF128 and AEAD128

Ascon.cry

@@ -23,6 +23,11 @@ parse (M_ # Ml) = (split M_, Ml)
 pad : {r, n} (n < r, fin r) => [n] -> [r]
 pad M = M # 0b1 # 0
 
+toBlocks : {r, n} (r >= 1, fin r, fin n) => [n] -> [n / r + 1][r]
+toBlocks M = M1 # [pad M2]
+  where
+    (M1, M2) = parse M
+
 // 3. Ascon Permutations
 
 type constraint ValidRnd rnd = (1 <= rnd, rnd <= 16)
@@ -93,5 +98,5 @@ pL [S0, S1, S2, S3, S4] =
         sigma : [64] -> [6] -> [6] -> [64]
         sigma x i j = x ^ (x >>> i) ^ (x >>> j)
 
-LE : {n} (fin n, n % 8 == 0) => [n] -> [n]
+little_bytes : {n} (fin n) => [8*n] -> [8*n]
-LE x = join (reverse (split`{n / 8, 8} x))
+little_bytes M = join (map reverse (groupBy`{8} M))

AsconCipher.cry

@@ -0,0 +1,43 @@
+module AsconCipher where
+
+import Ascon
+
+// 4. Authenticated Encryption Schema: Ascon-AEAD128
+
+Ascon_AEAD128 : {a, p} (fin a, fin p) => [128] -> [128] -> [a] -> [p] -> [p + 128]
+Ascon_AEAD128 (Khi_ # Klo_) (Nhi_ # Nlo_) A P = C # reverse T
+  where
+    Khi = reverse Khi_
+    Klo = reverse Klo_
+    Nhi = reverse Nhi_
+    Nlo = reverse Nlo_
+
+    S0 = Ascon_p`{12} [Ascon_AEAD128_IV, Khi, Klo, Nhi, Nlo]
+       ^ [0, 0, 0, Khi, Klo]
+    
+    SA = AddAD S0 A
+  
+    SCs = zipWith XorBlock (take ([SA] # map Ascon_p`{8} SCs)) (toBlocks P)
+
+    C = take (join [reverse s0 # reverse s1 | [s0, s1, _, _, _] <- SCs])
+
+    ST = Ascon_p`{12} (last SCs ^ [0, 0, Khi, Klo, 0])
+    T = ST@(4:[3]) # ST@(3:[3])
+      ^ Klo # Khi
+
+AddAD : {a} (fin a) => State -> [a] -> State
+AddAD S A
+  | a == 0 => DomainSep S
+  | a > 0  => DomainSep (foldl AbsorbBlock S (toBlocks A))
+
+XorBlock : State -> [128] -> State
+XorBlock [s0, s1, s2, s3, s4] (x0 # x1) = [s0 ^ reverse x0, s1 ^ reverse x1, s2, s3, s4]
+
+AbsorbBlock : State -> [128] -> State
+AbsorbBlock S X = Ascon_p`{8} (XorBlock S X)
+
+DomainSep : State -> State
+DomainSep [s0, s1, s2, s3, s4] = [s0, s1, s2, s3, s4 ^ 0b1 # 0]
+
+Ascon_AEAD128_IV : [64]
+Ascon_AEAD128_IV = 0x00001000808c0001

AsconHash.cry

@@ -1,23 +1,21 @@
-module AsconHash256 where
+module AsconHash where
 
 import Ascon
 
 // 5. Hash and eXtendable-Output Functions (XOFs)
 
-Ascon_Digest : {n} (fin n) => [64] -> [n] -> [inf]
+Ascon_Digest : {n} (fin n) => [64] -> [n][64] -> [inf]
-Ascon_Digest IV M = join [reverse (head S) | S <- iterate Ascon_p`{12} Sn]
+Ascon_Digest IV Ms = join [reverse (head S) | S <- iterate Ascon_p`{12} Sn]
     where
-    (M1, M2) = parse M
-    M' = map reverse (M1 # [pad M2])
-
-    AddBlock [s0, s1, s2, s3, s4] X = Ascon_p`{12} [X ^ s0, s1, s2, s3, s4]
     S0 = Ascon_p`{12} [IV, 0, 0, 0, 0]
-    Sn = foldl AddBlock S0 M'
+    Sn = foldl AbsorbBlock S0 Ms
 
+AbsorbBlock : State -> [64] -> State
+AbsorbBlock [s0, s1, s2, s3, s4] X = Ascon_p`{12} [reverse X ^ s0, s1, s2, s3, s4]
 
 /// 5.1. Specification of Ascon-Hash256
 Ascon_Hash256 : {n} (fin n) => [n] -> [256]
-Ascon_Hash256 M = take (Ascon_Digest Ascon_Hash256_IV M)
+Ascon_Hash256 M = take (Ascon_Digest Ascon_Hash256_IV (toBlocks M))
 
 Ascon_Hash256_IV : [64]
 Ascon_Hash256_IV = 0x0000080100cc0002
@@ -34,7 +32,7 @@ property
 // 5.2. Specification of Ascon-XOF128
 
 Ascon_XOF128 : {r, n} (fin n, fin r) => [n] -> [r]
-Ascon_XOF128 M = take (Ascon_Digest Ascon_XOF128_IV M)
+Ascon_XOF128 M = take (Ascon_Digest Ascon_XOF128_IV (toBlocks M))
 
 Ascon_XOF128_IV : [64]
 Ascon_XOF128_IV = 0x0000080000cc0003
@@ -42,9 +40,17 @@ Ascon_XOF128_IV = 0x0000080000cc0003
 Ascon_XOF128_bytes : {r, n} (fin n, fin r) => [n][8] -> [r][8]
 Ascon_XOF128_bytes M = map reverse (split (Ascon_XOF128 (join (map reverse M))))
 
-/// 5.3. Specification of Ascon-CXOF128
+// 5.3. Specification of Ascon-CXOF128
+
+Ascon_CXOF128 : {r, c, n} (fin n, fin r, fin c, 64 >= width c) => [c] -> [n] -> [r]
+Ascon_CXOF128 Z M = take (Ascon_Digest Ascon_CXOF128_IV Ms)
+  where
+    Ms = [reverse `c]
+       # toBlocks Z
+       # toBlocks M
+
+Ascon_CXOF128_bytes : {r, z, n} (fin n, fin r, 61 >= width z) => [z][8] -> [n][8] -> [r][8]
+Ascon_CXOF128_bytes Z M = map reverse (split (Ascon_CXOF128 (join (map reverse Z)) (join (map reverse M))))
+
 Ascon_CXOF128_IV : [64]
 Ascon_CXOF128_IV = 0x0000080000cc0004
-
-little_bytes : {n} (fin n) => [8*n] -> [8*n]
-little_bytes M = join (map reverse (groupBy`{8} M))