Merge pull request #79 from GaloisInc/77-refactor-aes-modules

Simplify AES module structure

Primitive/Keyless/Generator/DRBG.cry

@@ -5,9 +5,9 @@
 
 module Primitive::Keyless::Generator::DRBG where
 
-import Primitive::Symmetric::Cipher::Block::AES
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
 
-type keylen   = AESKeySize // bits
+type keylen   = AES256::KeySize // bits
 type blocklen = 128 // bits
 type seedlen  = 384 // bits, 384 bits fixed by table 3 for AES-256
 type reseed_limit = 2 ^^ 35 // max number of bytes to generate before reseeding
@@ -19,7 +19,7 @@ type seedsize = 48
 type cipher_ctx = { key : [keylen] }
 
 block_encrypt : [keylen] -> [blocklen] -> [blocklen]
-block_encrypt key data = aesEncrypt(data, key)
+block_encrypt key data = AES256::encrypt key data
 
 type s2n_drbg =
   { bytes_used : [64]

Primitive/Symmetric/Cipher/Authenticated/AES_256_GCM.cry

@@ -1,10 +1,9 @@
 module Primitive::Symmetric::Cipher::Authenticated::AES_256_GCM where
 
-import Primitive::Symmetric::Cipher::Block::AES
-
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
 
 aes_hw_encrypt : [16][8] -> [32][8] -> [16][8]
-aes_hw_encrypt in key = split (aesEncrypt ((join in), (join key)))
+aes_hw_encrypt in key = split (AES256::encrypt (join key) (join in))
 
 
 gcm_pmult_pmod : [128] -> [128] -> [128]

Primitive/Symmetric/Cipher/Authenticated/AES_GCM.cry

@@ -1,5 +1,5 @@
 
-// Cryptol AES GCM test vectors
+// Cryptol instatiation of AES128-GCM and AES256-GCM, and test vectors for each.
 // Copyright (c) 2010-2024, Galois Inc.
 // www.cryptol.net
 // Author: Ajay Kumar Eeralla
@@ -8,43 +8,52 @@
 
 module Primitive::Symmetric::Cipher::Authenticated::AES_GCM where
 import `Primitive::Symmetric::Cipher::Authenticated::GCM
-import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
+import Primitive::Symmetric::Cipher::Block::AES256 as AES256
+
+AES128_GCM_encrypt = GCM_AE `{K=128} {E=AES128::encrypt}
+AES128_GCM_decrypt = GCM_AD `{K=128} {E=AES128::encrypt}
+
+AES256_GCM_encrypt = GCM_AE `{K=256} {E=AES256::encrypt}
+AES256_GCM_decrypt = GCM_AD `{K=256} {E=AES256::encrypt}
 
 // GCM's symmetry property must hold for AES.
 // The other type parameter sizes are chosen arbitrarily.
 aesGcmIsSymmetric: [128] -> [96] -> [256] -> [0] -> Bool
-property aesGcmIsSymmetric key iv pt aad = gcmIsSymmetric `{T=128} { E=AES::encrypt } key iv pt aad
+property aesGcmIsSymmetric key iv pt aad = gcmIsSymmetric `{T=128} { E=AES128::encrypt } key iv pt aad
 
 // GCM's decryption API equivalence must hold for AES.
 // The other type parameter sizes are chosen arbitrarily.
 aesGcmDecryptionApisAreEquivalent: [128] -> [96] -> [256] -> [128] -> Bool
-property aesGcmDecryptionApisAreEquivalent key iv ct tag = decryptionApisAreEquivalent {E=AES::encrypt} key iv ct [] tag
+property aesGcmDecryptionApisAreEquivalent key iv ct tag = decryptionApisAreEquivalent {E=AES128::encrypt} key iv ct [] tag
 
 // GCM's encryption API equivalence must hold for AES.
 // The other type parameter sizes are chosen arbitrarily.
 aesGcmEncryptionApisAreEquivalent: [128] -> [96] -> [256] -> [128] -> Bool
-property aesGcmEncryptionApisAreEquivalent key iv pt = decryptionApisAreEquivalent {E=AES::encrypt} key iv pt []
+property aesGcmEncryptionApisAreEquivalent key iv pt = decryptionApisAreEquivalent {E=AES128::encrypt} key iv pt []
 
 property AES_GCM_test_vector_0 = ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
         pt = []
-        (ct, tag) = GCM_AE `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt} zero zero pt []
-        dec = GCM_AD `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt} zero zero ct [] tag
-        expected_ct = []
-        expected_tag = 0x58e2fccefa7e3061367f1d57a4e7455a
+        key = zero : [128]
+        iv = zero : [96]
+        (ct, tag) = AES128_GCM_encrypt key iv pt []
+        dec = AES128_GCM_decrypt key iv ct [] tag
+        expected_ct = [] : [0]
+        expected_tag = 0x58e2fccefa7e3061367f1d57a4e7455a : [128]
         valid_dec = dec.valid && (dec.pt == pt)
 
 property AES_GCM_test_vector_1 =
     ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
         key = zero
-        iv = zero
+        iv = zero : [96]
         pt = zero
         aad = []
-        expected_ct = 0x0388dace60b6a392f328c2b971b2fe78
+        expected_ct = 0x0388dace60b6a392f328c2b971b2fe78 : [128]
         expected_tag = 0xab6e47d42cec13bdf53a67b21257bddf : [128]
-        (ct, tag) = GCM_AE `{K=128, IV=96} {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD `{K=128, IV=96} {E=AES::encrypt} key iv ct aad tag
+        (ct, tag) = AES128_GCM_encrypt key iv pt aad
+        dec = AES128_GCM_decrypt key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
 property AES_GCM_test_vector_2 =
@@ -56,8 +65,8 @@ property AES_GCM_test_vector_2 =
         aad = []
         expected_ct = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985
         expected_tag = 0x4d5c2af327cd64a62cf35abd2ba6fab4 : [128]
-        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
+        (ct, tag) = AES128_GCM_encrypt key iv pt aad
+        dec = AES128_GCM_decrypt key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
 property AES_GCM_test_vector_3 =
@@ -69,8 +78,8 @@ property AES_GCM_test_vector_3 =
         aad = 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2
         expected_ct  = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091
         expected_tag = 0x5bc94fbc3221a5db94fae95ae7121a47
-        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
+        (ct, tag) = AES128_GCM_encrypt key iv pt aad
+        dec = AES128_GCM_decrypt key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
 // A test case from aesgcmtest.c
@@ -83,8 +92,8 @@ property AES_GCM_test_vector_4 =
         aad   = 0x4d23c3cec334b49bdb370c437fec78de : [128]
         expected_ct   = 0xf7264413a84c0e7cd536867eb9f21736
         expected_tag  = 0x67ba0510262ae487d737ee6298f77e0c
-        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD {E=AES::encrypt} key iv ct aad tag
+        (ct, tag) = AES256_GCM_encrypt key iv pt aad
+        dec = AES256_GCM_decrypt key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
 property AES_GCM_invalid_test_vector =
@@ -97,5 +106,5 @@ property AES_GCM_invalid_test_vector =
         expected_ct   = 0xf7264413a84c0e7cd536867eb9f21736
         expected_tag  = 0x67ba0510262ae487d737ee6298f77e0c
         invalid_tag  = 0x67ba0510262ae487d737ee6298f77888
-        (ct, tag) = GCM_AE {E=AES::encrypt} key iv pt aad
-        dec = GCM_AD {E=AES::encrypt} key iv ct aad invalid_tag
+        (ct, tag) = AES256_GCM_encrypt key iv pt aad
+        dec = AES256_GCM_decrypt key iv ct aad invalid_tag

Primitive/Symmetric/Cipher/Authenticated/AES_GCM_SIV.cry

@@ -14,26 +14,33 @@
 
 module Primitive::Symmetric::Cipher::Authenticated::AES_GCM_SIV where
 
-import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES
-
 parameter
-  /** 0: use AES128, 1: use AES256 */
-  type Mode : #
-  type constraint (1 >= Mode)
+  // This constraint enforces the standard key sizes of 128 and
+  // 256-bits recommended in the draft RFC.
+  type KeySize : #
+  type constraint (fin KeySize, KeySize % 128 == 0, KeySize / 128 >= 1, KeySize / 128 <= 2)
 
   type AAD : #
   type constraint ( (36 + 8) >= width AAD )
 
 
+/** This bit of algebra is here to satisfy the constraint solver.
+ * `K` should be the same as `KeySize`, but the type inference doesn't work
+ * if you set it directly equal.
+ * `Mode` is 0 for AES-128 and 1 for AES-256.
+ */
+type Mode = KeySize / 128 - 1
 type K  = 128 + 128 * Mode
-type KS = AES::EncKey (2 * Mode)
+import Primitive::Symmetric::Cipher::Block::AES_specification as AES where
+  type KeySize' = KeySize
+type KS = AES::EncryptionKey
 
 
 /** Note the weird byte-swapping business (also in `blockify` and `unblockify`)
-It is not quite clear in what format we want the inputs/outputs, but we
-do the swapping so that inputs/ouputs match the test vectors at
-https://tools.ietf.org/html/draft-irtf-cfrg-gcmsiv-06
-*/
+ * It is not quite clear in what format we want the inputs/outputs, but we
+ * do the swapping so that inputs/ouputs match the test vectors at
+ * https://tools.ietf.org/html/draft-irtf-cfrg-gcmsiv-06
+ */
 aes_gcm_siv :
   {n} ((36 + 8) >= width n) =>
       { key   : [K]
@@ -73,7 +80,7 @@ gcm_siv_plus (K1,K2) N AAD MSG = (unblockify Cs,TAG)
   T       = polyvalFrom K1 (A # M # [msg_len # aad_len]) 0
   A       = blockify AAD
   M       = blockify MSG
-  aad_len = `AAD : [64]
+  aad_len = `AAD: [64]
   msg_len = `n   : [64]
 
   _ # tUpper # tLower = TAG
@@ -115,4 +122,3 @@ unblockify xs = take (join [ byteSwap b | b <- xs ])
 // This function changes back and forth.
 byteSwap : {n} (fin n) => [8 * n] -> [8 * n]
 byteSwap xs = join (reverse (split`{each=8} xs))
-

Primitive/Symmetric/Cipher/Authenticated/SIV_rfc5297.md

@@ -1,9 +1,9 @@
 ```
 module Primitive::Symmetric::Cipher::Authenticated::SIV_rfc5297 where
 
-import Primitive::Symmetric::Cipher::Block::AES
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
 
-type Key = [AESKeySize]
+type Key = [AES128::KeySize]
 ```
 
 Network Working Group                                         D. Harkins
@@ -307,7 +307,7 @@ bitand a b = a && b
 
 ```
 E : (Key,[128]) -> [128]
-E(K,X) = aesEncrypt (X,K)
+E(K,X) = AES128::encrypt K X
 
 // 1. Apply the subkey generation process in Sec. 6.1 to K to produce K1 and K2.
 // 2. If Mlen = 0, let n = 1; else, let n = ⎡Mlen/b⎤.

Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat

@@ -20,7 +20,7 @@
 // This property is independent of the type parameters but we have to specify
 // them anyway.
 // It takes more than 25 minutes to `:prove`.
-:check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES::encrypt}
+:check dotAndMultAreEquivalent `{K=128, IV=96, AAD=0, T=128} {E=AES128::encrypt}
 
 // Make sure that decryption is the inverse of encryption
 // This property takes more than 20 minutes to `:prove`.