aes-gcm: update to use cipher interface #78

- modifies the GCM mode implementation to use the interface - replaces AES_GCM with separate instantiations of the GCM functor for our AES's of interest, and an independent test file -
GaloisInc · Jul 3, 2024 · fb0a046 · fb0a046
1 parent 01af25c
commit fb0a046
Show file tree

Hide file tree

Showing 5 changed files with 121 additions and 98 deletions.
diff --git a/Primitive/Symmetric/Cipher/Authenticated/GCM.cry b/Primitive/Symmetric/Cipher/Authenticated/GCM.cry
@@ -4,45 +4,38 @@ Copyright (c) 2017-2018, Galois, Inc.
 Author: Sean Weaver, Marcella Hastings
 
 This implementation follows NIST special publication 800-38D:
-[NISTSP800-38D] Morris Dworkin. Recommendation for Block Cipher Modes
+[NIST-SP-800-38D] Morris Dworkin. Recommendation for Block Cipher Modes
 of Operation: Galois/Counter Mode (GCM) and GMAC. NIST Special
 Publication 800-38D. November 2007.
 */
 
 module Primitive::Symmetric::Cipher::Authenticated::GCM where
+import interface Primitive::Symmetric::Cipher::Block::CipherInterface as C
 
-parameter
-  /** Key size */
-  type K : #
-  type constraint (fin K)
-
-  /** Size of initialization vector */
-  type IV : #
-  type constraint (64 >= width IV, IV >= 1)
-
-  /** Size of additional authenticated data */
-  type AAD  : #
-  type constraint (64 >= width AAD)
-
-  /** Size of authentication tag */
-  type T : #
-  type constraint (128 >= T, T >= 64)
-
-  /** Block encryption function */
-  E : [K] -> [128] -> [128]
+// GCM mode is only defined for ciphers that operate over 128-bit blocks.
+interface constraint (C::BlockSize == 128)
 
+type constraint ValidIV IV = (64 >= width IV, IV >= 1)
+type constraint ValidAAD AAD = (64 >= width AAD)
+type constraint ValidTag T = (128 >= T, T >= 64)
+/**
+ * The plaintext (for encryption) and ciphertext (for decryption) must not
+ * be too large.
+ * This constraint comes from [NIST-SP-800-38D].
+ */
+type constraint ValidText P = (fin P, P <= 2^^39 - 256 )
 
 /**
- * GCM-AE Function, [NISTSP800-38D] Section 7.1, Algorithm 4. This provides
+ * GCM-AE Function, [NIST-SP-800-38D] Section 7.1, Algorithm 4. This provides
  * authenticated encryption.
  */
 
-GCM_AE : { P } (fin P, P <= 2^^39 - 256 ) // This constraint comes from [NISTSP800-38D]
- => [K] -> [IV] -> [P] -> [AAD] -> ([P], [T])
+GCM_AE : { P, IV, AAD, T } (ValidText P, ValidIV IV, ValidAAD AAD, ValidTag T)
+ => [C::KeySize] -> [IV] -> [P] -> [AAD] -> ([P], [T])
 GCM_AE k iv p a = (C, T)
   where
     // Set names to match the spec
-    CIPHk = E k
+    CIPHk = C::encrypt k
     type len_A = AAD
     // Ciphertext length is the same as the input plaintext length
     type len_C = P
@@ -57,19 +50,18 @@ GCM_AE k iv p a = (C, T)
     T = MSB`{T} (GCTR CIPHk J0 S)
 
 /**
- * GCM-AD Function, [NISTSP800-38D] Section 7.2, Algorithm 5. This provides
+ * GCM-AD Function, [NIST-SP-800-38D] Section 7.2, Algorithm 5. This provides
  * authenticated decryption.
  */
 
-GCM_AD : { C }
-    ( fin C, C <= 2^^39 - 256 )  // This constraint comes from [NISTSP800-38D]
- => [K] -> [IV] -> [C] -> [AAD] -> [T] -> { valid : Bool, pt : [C] }
+GCM_AD : { C, IV, AAD, T } (ValidText C, ValidIV IV, ValidAAD AAD, ValidTag T)
+ => [C::KeySize] -> [IV] -> [C] -> [AAD] -> [T] -> { valid : Bool, pt : [C] }
 GCM_AD key iv ct aad tag =
   if tag == T'
   then { valid = True, pt = P }
   else { valid = False, pt = 0 }
   where
-    CIPHk = E key
+    CIPHk = C::encrypt key
     len_IV = `IV
     type len_A = AAD
     type len_C = C
@@ -91,13 +83,13 @@ property dotAndMultAreEquivalent X Y = mult X Y == X • Y
 /**
  * Property demonstrating that decryption is the inverse of encryption.
  *
- * This should be instantiated for each block cipher `E` that uses GCM mode.
+ * This should be instantiated for each block cipher `C::encrypt` that uses GCM mode.
  */
-gcmIsSymmetric : {P} ( fin P, P < 2^^39 - 256 )
-  => [K] -> [IV] -> [P] -> [AAD] -> Bool
+gcmIsSymmetric : { P, IV, AAD } ( ValidText P, ValidIV IV, ValidAAD AAD )
+  => [C::KeySize] -> [IV] -> [P] -> [AAD] -> Bool
 property gcmIsSymmetric key iv pt aad = dec.valid && (dec.pt == pt)
     where
-        (ct, tag) = GCM_AE key iv pt aad
+        (ct, tag : [96]) = GCM_AE key iv pt aad
         dec = GCM_AD key iv ct aad tag
 
 private
@@ -106,9 +98,9 @@ private
   * level due to its use of Cryptol's numeric constraint guards feature, which
   * currently only works in top-level definitions.
   *
-  * This renames the IV type to `len_IV` to better match [NISTSP800-38D].
+  * This renames the IV type to `len_IV` to better match [NIST-SP-800-38D].
   */
-  define_J0 : { len_IV } ( len_IV == IV) => [K] -> [len_IV] -> [128] -> [128]
+  define_J0 : { len_IV } ( ValidIV len_IV ) => [C::KeySize] -> [len_IV] -> [128] -> [128]
   define_J0 k iv H
     | len_IV == 96 => iv # (0 : [31]) # (1 : [1])
     | len_IV != 96 => GHASH`{len_IV /^ 128 + 1} H (iv # (0 : [s + 64]) # (`len_IV: [64]))
@@ -117,7 +109,7 @@ private
       type s = len_IV %^ 128  // Equivalently: 128 * len_IV /^ 128 - len_IV
 
   /**
-  * Multiplication Operation on Blocks, [NISTSP800-38D] Section
+  * Multiplication Operation on Blocks, [NIST-SP-800-38D] Section
   * 6.3, Algorithm 1. This is optimized to use Cryptol's built-in `pmult` and
   * `pmod` functions. This operation is described using little-endian
   * notation, hence the `reverse`s.
@@ -128,7 +120,7 @@ private
                           <| 1 + x + x^^2 + x^^7 + x^^128|>)
 
   /**
-  * Multiplication Operation on Blocks, [NISTSP800-38D] Section
+  * Multiplication Operation on Blocks, [NIST-SP-800-38D] Section
   * 6.3. This matches the spec very closely.
   */
 
@@ -144,7 +136,7 @@ private
                 | Vi <- V ]
 
   /**
-  * GHASH Function, [NISTSP800-38D] Section 6.4, Algorithm 2.
+  * GHASH Function, [NIST-SP-800-38D] Section 6.4, Algorithm 2.
   */
 
   GHASH : {m} (fin m) => [128] -> [m * 128] -> [128]
@@ -154,7 +146,7 @@ private
   /**
   * The output of incrementing the right-most s bits of the bit
   * string X, regarded as the binary representation of an integer, by
-  * 1 modulo 2s, [NISTSP800-38D] Sections 4.2.2 and 6.2. Care was
+  * 1 modulo 2s, [NIST-SP-800-38D] Sections 4.2.2 and 6.2. Care was
   * taken here to ensure `s` could be zero.
   */
 
@@ -164,22 +156,22 @@ private
 
   /**
   * The bit string consisting of the s right-most bits
-  * of the bit string X, [NISTSP800-38D] Section 4.2.2.
+  * of the bit string X, [NIST-SP-800-38D] Section 4.2.2.
   */
 
   LSB : {s, a} (fin s, fin a, a >= s) => [a] -> [s]
   LSB X = drop X
 
   /**
   * The bit string consisting of the s left-most bits of
-  * the bit string X, [NISTSP800-38D] Section 4.2.2.
+  * the bit string X, [NIST-SP-800-38D] Section 4.2.2.
   */
 
   MSB : {s, a} (fin s, a >= s) => [a] -> [s]
   MSB X = take X
 
   /**
-  * GCTR Function, [NISTSP800-38D] Section 6.5, Algorithm 3.
+  * GCTR Function, [NIST-SP-800-38D] Section 6.5, Algorithm 3.
   */
 
   GCTR : {a} (fin a) => ([128] -> [128]) -> [128] -> [a] -> [a]

diff --git a/Primitive/Symmetric/Cipher/Authenticated/Instantiations/AES128_GCM.cry b/Primitive/Symmetric/Cipher/Authenticated/Instantiations/AES128_GCM.cry
@@ -0,0 +1,11 @@
+/*
+ * Instantiate GCM mode for AES 128.
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <[email protected]>
+ */
+module Primitive::Symmetric::Cipher::Authenticated::Instantiations::AES128_GCM =
+    Primitive::Symmetric::Cipher::Authenticated::GCM {
+        Primitive::Symmetric::Cipher::Block::AES128
+    }
+
diff --git a/Primitive/Symmetric/Cipher/Authenticated/Instantiations/AES256_GCM.cry b/Primitive/Symmetric/Cipher/Authenticated/Instantiations/AES256_GCM.cry
@@ -0,0 +1,11 @@
+/*
+ * Instantiate GCM mode for AES 256.
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <[email protected]>
+ */
+module Primitive::Symmetric::Cipher::Authenticated::Instantiations::AES256_GCM =
+    Primitive::Symmetric::Cipher::Authenticated::GCM {
+        Primitive::Symmetric::Cipher::Block::AES256
+    }
+
diff --git a/...ymmetric/Cipher/Authenticated/AES_GCM.cry → ...ipher/Authenticated/Tests/TestAES_GCM.cry b/...ymmetric/Cipher/Authenticated/AES_GCM.cry → ...ipher/Authenticated/Tests/TestAES_GCM.cry
@@ -1,39 +1,33 @@
+import Primitive::Symmetric::Cipher::Authenticated::Instantiations::AES128_GCM as AES128_GCM
+import Primitive::Symmetric::Cipher::Authenticated::Instantiations::AES256_GCM as AES256_GCM
 
-// 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
+/*
+ Sources for test vectors:
 
-// Test vectors from http://luca-giuzzi.unibs.it/corsi/Support/papers-cryptography/gcm-spec.pdf
+ [GCM Submission]: David A. McGrew and John Viega. The Galois/Counter Mode of
+ Operation (GCM). Submission to NIST Modes of Operation Process. 2004.
+ Accessed from http://luca-giuzzi.unibs.it/corsi/Support/papers-cryptography/gcm-spec.pdf
 
-module Primitive::Symmetric::Cipher::Authenticated::AES_GCM where
-import `Primitive::Symmetric::Cipher::Authenticated::GCM
-import Primitive::Symmetric::Cipher::Block::AES128 as AES128
-import Primitive::Symmetric::Cipher::Block::AES256 as AES256
+ [OPENSSL]: The OpenSSL Project Authors. aesgcmtest.c. 2022.
+ Accessed from https://github.com/openssl/openssl/blob/master/test/aesgcmtest.c
+ */
 
-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=AES128::encrypt } key iv pt aad
-
-property AES_GCM_test_vector_0 = ct == expected_ct /\ tag == expected_tag /\ valid_dec
+// This can be `:prove`n quickly.
+// Source: [GCM Submission]
+property aes128_vector_0 = ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
         pt = []
         key = zero : [128]
         iv = zero : [96]
-        (ct, tag) = AES128_GCM_encrypt key iv pt []
-        dec = AES128_GCM_decrypt key iv ct [] tag
+        (ct, tag) = AES128_GCM::GCM_AE key iv pt []
+        dec = AES128_GCM::GCM_AD key iv ct [] tag
         expected_ct = [] : [0]
         expected_tag = 0x58e2fccefa7e3061367f1d57a4e7455a : [128]
         valid_dec = dec.valid && (dec.pt == pt)
 
-property AES_GCM_test_vector_1 =
+// This can be `:prove`n quickly.
+// Source: [GCM Submission]
+property aes128_vector_1 =
     ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
         key = zero
@@ -42,24 +36,28 @@ property AES_GCM_test_vector_1 =
         aad = []
         expected_ct = 0x0388dace60b6a392f328c2b971b2fe78 : [128]
         expected_tag = 0xab6e47d42cec13bdf53a67b21257bddf : [128]
-        (ct, tag) = AES128_GCM_encrypt key iv pt aad
-        dec = AES128_GCM_decrypt key iv ct aad tag
+        (ct, tag) = AES128_GCM::GCM_AE key iv pt aad
+        dec = AES128_GCM::GCM_AD key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
-property AES_GCM_test_vector_2 =
+// This can be `:prove`n quickly.
+// Source: [GCM Submission]
+property aes128_vector_2 =
     ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
-        key = 0xfeffe9928665731c6d6a8f9467308308 : [128]
+        key = 0xfeffe9928665731c6d6a8f9467308308
         iv = 0xcafebabefacedbaddecaf888 : [96]
         pt = 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255
         aad = []
         expected_ct = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985
         expected_tag = 0x4d5c2af327cd64a62cf35abd2ba6fab4 : [128]
-        (ct, tag) = AES128_GCM_encrypt key iv pt aad
-        dec = AES128_GCM_decrypt key iv ct aad tag
+        (ct, tag) = AES128_GCM::GCM_AE key iv pt aad
+        dec = AES128_GCM::GCM_AD key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
-property AES_GCM_test_vector_3 =
+// This can be `:prove`n quickly.
+// Source: [GCM Submission]
+property aes128_vector_3 =
     ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
         key = 0xfeffe9928665731c6d6a8f9467308308
@@ -68,12 +66,13 @@ property AES_GCM_test_vector_3 =
         aad = 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2
         expected_ct  = 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091
         expected_tag = 0x5bc94fbc3221a5db94fae95ae7121a47
-        (ct, tag) = AES128_GCM_encrypt key iv pt aad
-        dec = AES128_GCM_decrypt key iv ct aad tag
+        (ct, tag) = AES128_GCM::GCM_AE key iv pt aad
+        dec = AES128_GCM::GCM_AD key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
-// A test case from aesgcmtest.c
-property AES_GCM_test_vector_4 =
+// This can be `:prove`n quickly.
+// Source: [OPENSSL]
+property aes256_vector_0 =
     ct == expected_ct /\ tag == expected_tag /\ valid_dec
     where
         key   = 0xeebc1f57487f51921c0465665f8ae6d1658bb26de6f8a069a3520293a572078f : [256]
@@ -82,11 +81,14 @@ property AES_GCM_test_vector_4 =
         aad   = 0x4d23c3cec334b49bdb370c437fec78de : [128]
         expected_ct   = 0xf7264413a84c0e7cd536867eb9f21736
         expected_tag  = 0x67ba0510262ae487d737ee6298f77e0c
-        (ct, tag) = AES256_GCM_encrypt key iv pt aad
-        dec = AES256_GCM_decrypt key iv ct aad tag
+        (ct, tag) = AES256_GCM::GCM_AE key iv pt aad
+        dec = AES256_GCM::GCM_AD key iv ct aad tag
         valid_dec = dec.valid && (dec.pt == pt)
 
-property AES_GCM_invalid_test_vector =
+// This can be `:prove`n quickly.
+// Source: Modified from [OPENSSL]. I just borked the tag to make sure decryption fails if
+// the tag is wrong.
+property aes256_invalid_vector_1 =
     ct == expected_ct /\ tag == expected_tag /\ ~dec.valid
     where
         key   = 0xeebc1f57487f51921c0465665f8ae6d1658bb26de6f8a069a3520293a572078f : [256]
@@ -96,5 +98,5 @@ property AES_GCM_invalid_test_vector =
         expected_ct   = 0xf7264413a84c0e7cd536867eb9f21736
         expected_tag  = 0x67ba0510262ae487d737ee6298f77e0c
         invalid_tag  = 0x67ba0510262ae487d737ee6298f77888
-        (ct, tag) = AES256_GCM_encrypt key iv pt aad
-        dec = AES256_GCM_decrypt key iv ct aad invalid_tag
+        (ct, tag) = AES256_GCM::GCM_AE key iv pt aad
+        dec = AES256_GCM::GCM_AD key iv ct aad invalid_tag
diff --git a/Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat b/Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat
@@ -1,28 +1,35 @@
-:l AES_GCM.cry
+:l Tests/TestAES_GCM.cry
 
-:prove AES_GCM_test_vector_0
-:prove AES_GCM_test_vector_1
-:prove AES_GCM_test_vector_2
-:prove AES_GCM_test_vector_3
-:prove AES_GCM_test_vector_4
-:prove AES_GCM_invalid_test_vector
+:prove aes128_vector_0
+:prove aes128_vector_1
+:prove aes128_vector_2
+:prove aes128_vector_3
+
+:prove aes256_vector_0
+:prove aes256_invalid_vector_1
 
 // The following checks do not really provide any significant formal
 // verification because they check so little of the sample space.
 // They each take a long time to `:prove` and would likely require
 // manual modification to prove in a reasonable amount of time.
 
-// These properties can be checked manually; one of the APIs calls the other.
-// They take more than an hour to `:prove`.
-:check aesGcmDecryptionApisAreEquivalent
-:check aesGcmEncryptionApisAreEquivalent
 
-// 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=AES128::encrypt}
+:l Instantiations/AES128_GCM.cry
 
 // Make sure that decryption is the inverse of encryption
 // This property takes more than 20 minutes to `:prove`.
 // It's also spot-checked in the test vectors
-:check aesGcmIsSymmetric
+// Here, we just pick a fixed set of parameters, but it should be true
+// for all valid tag, aad, and plaintext lengths.
+// - P = 256 because we want to test the block chaining, so we need at least 2
+// - IV = 96 because it's the shortest allowable value
+// - AAD = 5 because we want to make sure it's incorporated
+:check gcmIsSymmetric `{AAD=5, P=256, IV=96}
+
+// This takes more than 25 minutes to `:prove`.
+:check dotAndMultAreEquivalent
+
+// Repeat the above checks for AES256
+:l Instantiations/AES256_GCM.cry
+:check gcmIsSymmetric `{AAD=5, P=256, IV=96}
+:check dotAndMultAreEquivalent