modes: improve code quality in CTR mode #80

- Rewrite CTR mode to be in terms of the `CipherInterface`
- Update CTR mode to more closely match the original spec (naming,
  parameter order, etc.), and add docs for deviations
- Adds top-level documentation on deviations from the original spec and
  warnings for failure modes that cryptol cannot detect
- Rearranges instantiations and test vectors for AES (including adding
  more test vectors)

Primitive/Symmetric/Cipher/Block/Instantiations/AES128_CTR.cry

@@ -0,0 +1,5 @@
+// Instantiate CTR mode with AES 128
+module Primitive::Symmetric::Cipher::Block::Instantiations::AES128_CTR =
+    Primitive::Symmetric::Cipher::Block::Modes::CTR {
+        Primitive::Symmetric::Cipher::Block::AES128
+    }

Primitive/Symmetric/Cipher/Block/Instantiations/AES256_CTR.cry

@@ -0,0 +1,6 @@
+// Instantiate CTR mode with AES 256
+module Primitive::Symmetric::Cipher::Block::Instantiations::AES256_CTR =
+    Primitive::Symmetric::Cipher::Block::Modes::CTR {
+        Primitive::Symmetric::Cipher::Block::AES256
+    }
+

Primitive/Symmetric/Cipher/Block/Instantiations/README.md

@@ -0,0 +1,7 @@
+This directory defines concrete instantiations of modes of operation for a given block cipher.
+
+This is not intended to be exhaustive; there may be modes that can be instantiated with other ciphers than those included here. This is mainly here to provide convenient instantiations for ciphers and modes that are commonly used or particularly interesting.
+
+At this time, this directory does not contain all the instantiations included in the repo; they're scattered in multiple locations. As modes of operation are refactored to use the `CipherInterface`, we'll aim to add or move their instantiations here.
+
+Test vectors for these instantiations can be found in the `Primitive/Symmetric/Cipher/Block/Tests/` directory.

Primitive/Symmetric/Cipher/Block/Modes/CTR.cry

@@ -1,26 +1,66 @@
-// Cryptol CBC Implementation
-// Copyright (c) 2010-2018, Galois Inc.
-// www.cryptol.net
-// Author: Ajay Kumar Eeralla
+/*
+ * Counter mode of operation, as defined in [NIST-SP-800-38A], Section 6.5.
+ *
+ * ⚠️ Warning ⚠️: CTR mode will fail catastrophically if a (key, counter) pair is ever reused.
+ * Cryptol cannot detect such failures! Please audit your implementations separately for
+ * this issue.
+ *
+ *
+ * This deviates from the original NIST spec in several ways:
+ * - The spec allows arbitrary length plaintexts. This implementation fixes
+ *   the plaintext to be an exact multiple of the block length.
+ * - The spec allows any incrementing function that generates `n` unique strings
+ *   of `m` bits in succession, where `n` is the plaintext length and `m` is the
+ *   number of bits to be updated in the counter block (n <= C::BlockSize).
+ *   This implementation fixes the incrementing function to be the standard
+ *   incrementing function: [x]_m -> [x + 1 mod 2^m]_m for m = C::BlockSize.
+ *   See Appendix B of [NIST-SP-800-38A] for discussion.
+ *
+ *  Copyright (c) 2010-2024, Galois Inc.
+ *  www.cryptol.net
+ *  Author: Ajay Kumar Eeralla, Marcella Hastings
+ */
 
 module Primitive::Symmetric::Cipher::Block::Modes::CTR where
+import interface Primitive::Symmetric::Cipher::Block::CipherInterface as C
 
-// set the sizes
-type ic = [128]
-type block = [128]
+/**
+ * CTR encryption: [NIST-SP-800-38A] Section 6.5.
+ *
+ * Parameters: key, initial counter, plaintext
+ *
+ * ⚠️ Warning ⚠️: CTR mode will fail catastrophically if a (key, counter) pair is ever reused.
+ * Cryptol cannot detect such failures!
+ */
+encrypt : {n} (fin n) => [C::KeySize] -> [C::BlockSize] -> [n][C::BlockSize] -> [n][C::BlockSize]
+encrypt k t_1 ps = cs
+    where
+        ciph_k = C::encrypt k
+        // (ciph_k t_j) is called O_j in the original spec
+        cs = [p_j ^ (ciph_k t_j) | p_j <- ps | t_j <- ctrs]
+        // Counters are called T_1, ..., T_n in the original spec
+        ctrs = [t_1 + i | i<- [0...]]
 
+/**
+ * CTR decryption: [NIST-SP-800-38A] Section 6.5.
+ *
+ * Parameters: key, initial counter, ciphertext
+ *
+ * ⚠️ Warning ⚠️: CTR mode will fail catastrophically if a (key, counter) pair is ever reused.
+ * Cryptol cannot detect such failures!
+ */
+decrypt : {n} (fin n) => [C::KeySize] -> [C::BlockSize] -> [n][C::BlockSize] -> [n][C::BlockSize]
+decrypt k t_1 cs = ps
+    where
+        ciph_k = C::encrypt k
+        // (ciph_k t_j) is called O_j in the original spec
+        ps = [c_j ^ (ciph_k t_j) | c_j <- cs | t_j <- ctrs]
+        // Counters are called T_1, ..., T_n in the original spec
+        ctrs = [t_1 + i | i<- [0...]]
 
-ctrEnc : {n, k} (fin n, fin k) => ([k]->block -> block) -> [k] -> ic -> [n]block -> [n]block
-ctrEnc enc k c ps = cs
-    where cs = [(enc k c')^p | p <- ps | c' <- ctrs]
-          ctrs = [c+i | i<- [0...]]
-
-ctrDec : {n, k} (fin n, fin k) => ([k]->block -> block) -> [k] -> ic -> [n]block -> [n]block
-ctrDec enc k c cs = ps
-    where ps = [(enc k c')^ct | ct <- cs | c' <- ctrs]
-          ctrs = [c+i | i<- [0...]]
-
-// This will need to be parameterized with a specific encryption function before it can be proved
-property ctrEncCorrect enc k c ps = (ctrDec enc k c (ctrEnc enc k c ps)) == ps
+// Decryption must be the inverse of encryption.
+// With high probability, this will be incredibly slow to prove, and should be
+// `:check`ed instead for each instantiation of this module.
+property encryptCorrect k c ps = (decrypt k c (encrypt k c ps)) == ps
 
 

Primitive/Symmetric/Cipher/Block/Tests/TestAES_CTR.cry

@@ -0,0 +1,71 @@
+/*
+ * Test vectors for AES-CTR mode.
+ * These are taken from [NIST-SP-800-38A] Appendix F.5
+ *
+ */
+import Primitive::Symmetric::Cipher::Block::Instantiations::AES128_CTR as AES128_CTR
+import Primitive::Symmetric::Cipher::Block::Instantiations::AES256_CTR as AES256_CTR
+
+// This can be `:prove`n.
+property aes128_ctr_encrypt_vector = (AES128_CTR::encrypt k ic plaintext) == ciphertext
+    where
+    k = 0x2b7e151628aed2a6abf7158809cf4f3c
+    ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]
+    ciphertext = [
+        0x874d6191b620e3261bef6864990db6ce,
+        0x9806f66b7970fdff8617187bb9fffdff,
+        0x5ae4df3edbd5d35e5b4f09020db03eab,
+        0x1e031dda2fbe03d1792170a0f3009cee]
+
+// This can be `:prove`n.
+property aes128_ctr_decrypt_vector = (AES128_CTR::decrypt k ic ciphertext) == plaintext
+    where
+    k = 0x2b7e151628aed2a6abf7158809cf4f3c
+    ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
+    ciphertext = [
+        0x874d6191b620e3261bef6864990db6ce,
+        0x9806f66b7970fdff8617187bb9fffdff,
+        0x5ae4df3edbd5d35e5b4f09020db03eab,
+        0x1e031dda2fbe03d1792170a0f3009cee]
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]
+
+// This can be `:prove`n.
+property aes256_ctr_encrypt_vector = (AES256_CTR::encrypt k ic plaintext) == ciphertext
+    where
+    k = 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4
+    ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]
+    ciphertext = [
+        0x601ec313775789a5b7a7f504bbf3d228,
+        0xf443e3ca4d62b59aca84e990cacaf5c5,
+        0x2b0930daa23de94ce87017ba2d84988d,
+        0xdfc9c58db67aada613c2dd08457941a6]
+
+// This can be `:prove`n.
+property aes256_ctr_decrypt_vector = (AES256_CTR::decrypt k ic ciphertext) == plaintext
+    where
+    k = 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4
+    ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
+    ciphertext = [
+        0x601ec313775789a5b7a7f504bbf3d228,
+        0xf443e3ca4d62b59aca84e990cacaf5c5,
+        0x2b0930daa23de94ce87017ba2d84988d,
+        0xdfc9c58db67aada613c2dd08457941a6]
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]