Merge pull request #124 from GaloisInc/cbc-cipher-interface

CBC mode refactor/improvements

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

@@ -0,0 +1,10 @@
+/*
+ * Instantiate CBC mode for AES 128.
+ *
+ * @copyright Galois, Inc.
+ * @author Stanislav Lyakhov <stan@galois.com>
+ */
+module Primitive::Symmetric::Cipher::Block::Instantiations::AES128_CBC =
+    Primitive::Symmetric::Cipher::Block::Modes::CBC {
+        Primitive::Symmetric::Cipher::Block::AES128
+    }

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

@@ -0,0 +1,10 @@
+/*
+ * Instantiate CBC mode for AES 192.
+ *
+ * @copyright Galois, Inc.
+ * @author Stanislav Lyakhov <stan@galois.com>
+ */
+module Primitive::Symmetric::Cipher::Block::Instantiations::AES192_CBC =
+    Primitive::Symmetric::Cipher::Block::Modes::CBC {
+        Primitive::Symmetric::Cipher::Block::AES192
+    }

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

@@ -0,0 +1,10 @@
+/*
+ * Instantiate CBC mode for AES 256.
+ *
+ * @copyright Galois, Inc.
+ * @author Stanislav Lyakhov <stan@galois.com>
+ */
+module Primitive::Symmetric::Cipher::Block::Instantiations::AES256_CBC =
+    Primitive::Symmetric::Cipher::Block::Modes::CBC {
+        Primitive::Symmetric::Cipher::Block::AES256
+    }

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

@@ -1,21 +1,66 @@
-// Cryptol CBC Implementation
-// Copyright (c) 2010-2018, Galois Inc.
-// www.cryptol.net
-// Author: Ajay Kumar Eeralla
+/*
+ * Cipher Block Chaining mode of operation, as defined in [NIST-SP-800-38A], Section 6.2.
+ *
+ * ⚠️ Warning ⚠️: To ensure confidentiality, CBC mode requires that the initialization vector (IV) is generated "unpredictably".
+ * This specification does not verify IV generation;
+ * implementors must manually verify that their IVs were chosen appropriately.
+ *
+ * For guidelines on generating IVs, see Appendix C of [NIST-SP-800-38A].
+ * For information on the importance of protecting IV integrity, see Appendix D of [NIST-SP-800-38A].
+ *
+ * @copyright Galois, Inc.
+ * @author Ajay Kumar Eeralla
+ * @author Marcella Hastings <marcella@galois.com>
+ * @author Stanislav Lyakhov <stan@galois.com>
+ * www.cryptol.net
+ *
+ * [NIST-SP-800-38A]: Morris Dworkin. Recommendation for Block Cipher
+ *     Modes of Operation: Methods and Techniques. NIST Special Publication
+ *     800-38A. December 2001.
+ *     @see https://doi.org/10.6028/NIST.SP.800-38A 
+ *
+ */
 
-module Primitive::Symmetric::Cipher::Block::Modes::CBC where
-
-// set the sizes
-type iv = [128]
-type block = [128]
 
+module Primitive::Symmetric::Cipher::Block::Modes::CBC where
+import interface Primitive::Symmetric::Cipher::Block::CipherInterface as C
 
-cbcEnc : {n, k} (fin n, fin k) => ([k]->block -> block) -> [k] -> iv -> [n]block -> [n]block
-cbcEnc enc k iv ps = cs
-    where cs = [ enc k (p ^ c') | p <- ps | c' <- [iv] # cs ]
+/**
+ * CBC encryption: [NIST-SP-800-38A] Section 6.2.
+ *
+ * Parameters: key, initialization vector, plaintext
+ *
+ * ⚠️ Warning ⚠️: To ensure confidentiality, CBC mode requires that the initialization vector (IV) is generated "unpredictably".
+ * This specification does not verify IV generation;
+ * implementors must manually verify that their IVs were chosen appropriately.
+ */
+encrypt : {n} (fin n) => [C::KeySize] -> [C::BlockSize] -> [n][C::BlockSize] -> [n][C::BlockSize]
+encrypt K IV Ps = Cs
+    where 
+        CIPH_K = C::encrypt K
+        Cs = [ CIPH_K (P_j ^ C_j_1) | P_j <- Ps | C_j_1 <- [IV] # Cs] 
 
-cbcDec : {n, k} (fin n, fin k) => ([k]->block -> block) -> [k] -> iv -> [n]block -> [n]block
-cbcDec dec k iv cs = [ (dec k c) ^ c' | c <- cs | c' <- [iv] # cs ]
+/**
+ * CBC decryption: [NIST-SP-800-38A] Section 6.2.
+ *
+ * Parameters: key, initialization vector, ciphertext
+ *
+ * ⚠️ Warning ⚠️: To ensure confidentiality, CBC mode requires that the initialization vector (IV) is generated "unpredictably".
+ * This specification does not verify IV generation;
+ * implementors must manually verify that their IVs were chosen appropriately.
+ */
+decrypt : {n} (fin n) => [C::KeySize] -> [C::BlockSize] -> [n][C::BlockSize] -> [n][C::BlockSize]
+decrypt K IV Cs = Ps
+    where 
+        CIPH_K_inv = C::decrypt K
+        Ps = [ (CIPH_K_inv C_j) ^ C_j_1 | C_j <- Cs | C_j_1 <- [IV] # Cs] 
 
-// This will need to be parameterized with a specific encryption function before it can be proved
-property cbcEncCorrect encrypt k c ps = (cbcDec encrypt k c (cbcEnc encrypt k c ps)) == ps
+/**
+ * Decryption must be the inverse of encryption.
+ * With high probability, this will be incredibly slow to prove.
+ * ```repl
+ * :check encryptCorrect`{n=5}
+ * ```
+ */
+encryptCorrect : {n} (fin n) => [C::KeySize] -> [C::BlockSize] -> [n][C::BlockSize] -> Bool
+property encryptCorrect K IV Ps = (decrypt K IV (encrypt K IV Ps)) == Ps

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

@@ -0,0 +1,139 @@
+/*
+ * Test vectors for AES-CBC mode.
+ * These are taken from [NIST-SP-800-38A] Appendix F.2
+ *
+ * @copyright Galois, Inc.
+ * @author Ajay Kumar Eeralla
+ * @author Marcella Hastings <marcella@galois.com>
+ * @author Stanislav Lyakhov <stan@galois.com>
+ *  www.cryptol.net
+ *
+ * References:
+ * [NIST-SP-800-38A]: Morris Dworkin. Recommendation for Block Cipher
+ * Modes of Operation: Methods and Techniques. NIST Special Publication
+ * 800-38A. December 2001.
+ *
+ */
+import Primitive::Symmetric::Cipher::Block::Instantiations::AES128_CBC as AES128_CBC
+import Primitive::Symmetric::Cipher::Block::Instantiations::AES192_CBC as AES192_CBC
+import Primitive::Symmetric::Cipher::Block::Instantiations::AES256_CBC as AES256_CBC
+
+/**
+ * ```repl
+ * :prove aes128_cbc_encrypt_vector
+ * ```
+ */
+property aes128_cbc_encrypt_vector = (AES128_CBC::encrypt k iv plaintext) == ciphertext
+    where
+    k = 0x2b7e151628aed2a6abf7158809cf4f3c
+    iv = 0x000102030405060708090a0b0c0d0e0f
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]
+    ciphertext = [
+        0x7649abac8119b246cee98e9b12e9197d,
+        0x5086cb9b507219ee95db113a917678b2,
+        0x73bed6b8e3c1743b7116e69e22229516,
+        0x3ff1caa1681fac09120eca307586e1a7]
+
+/**
+ * ```repl
+ * :prove aes128_cbc_decrypt_vector
+ * ```
+ */
+property aes128_cbc_decrypt_vector = (AES128_CBC::decrypt k iv ciphertext) == plaintext
+    where
+    k = 0x2b7e151628aed2a6abf7158809cf4f3c
+    iv = 0x000102030405060708090a0b0c0d0e0f
+    ciphertext = [
+        0x7649abac8119b246cee98e9b12e9197d,
+        0x5086cb9b507219ee95db113a917678b2,
+        0x73bed6b8e3c1743b7116e69e22229516,
+        0x3ff1caa1681fac09120eca307586e1a7]
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]
+
+/**
+ * ```repl
+ * :prove aes192_cbc_encrypt_vector
+ * ```
+ */
+property aes192_cbc_encrypt_vector = (AES192_CBC::encrypt k iv plaintext) == ciphertext
+    where
+    k = 0x8e73b0f7da0e6452c810f32b809079e562f8ead2522c6b7b
+    iv = 0x000102030405060708090a0b0c0d0e0f
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]
+    ciphertext = [
+        0x4f021db243bc633d7178183a9fa071e8,
+        0xb4d9ada9ad7dedf4e5e738763f69145a,
+        0x571b242012fb7ae07fa9baac3df102e0,
+        0x08b0e27988598881d920a9e64f5615cd]
+
+/**
+ * ```repl
+ * :prove aes192_cbc_decrypt_vector
+ * ```
+ */
+property aes192_cbc_decrypt_vector = (AES192_CBC::decrypt k iv ciphertext) == plaintext
+    where
+    k = 0x8e73b0f7da0e6452c810f32b809079e562f8ead2522c6b7b
+    iv = 0x000102030405060708090a0b0c0d0e0f
+    ciphertext = [
+        0x4f021db243bc633d7178183a9fa071e8,
+        0xb4d9ada9ad7dedf4e5e738763f69145a,
+        0x571b242012fb7ae07fa9baac3df102e0,
+        0x08b0e27988598881d920a9e64f5615cd]
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]
+
+/**
+ * ```repl
+ * :prove aes256_cbc_encrypt_vector
+ * ```
+ */
+property aes256_cbc_encrypt_vector = (AES256_CBC::encrypt k iv plaintext) == ciphertext
+    where
+    k = 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4
+    iv = 0x000102030405060708090a0b0c0d0e0f
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]
+    ciphertext = [
+        0xf58c4c04d6e5f1ba779eabfb5f7bfbd6,
+        0x9cfc4e967edb808d679f777bc6702c7d,
+        0x39f23369a9d9bacfa530e26304231461,
+        0xb2eb05e2c39be9fcda6c19078c6a9d1b]
+
+/**
+ * ```repl
+ * :prove aes256_cbc_decrypt_vector
+ * ```
+ */
+property aes256_cbc_decrypt_vector = (AES256_CBC::decrypt k iv ciphertext) == plaintext
+    where
+    k = 0x603deb1015ca71be2b73aef0857d77811f352c073b6108d72d9810a30914dff4
+    iv = 0x000102030405060708090a0b0c0d0e0f
+    ciphertext = [
+        0xf58c4c04d6e5f1ba779eabfb5f7bfbd6,
+        0x9cfc4e967edb808d679f777bc6702c7d,
+        0x39f23369a9d9bacfa530e26304231461,
+        0xb2eb05e2c39be9fcda6c19078c6a9d1b]
+    plaintext = [
+        0x6bc1bee22e409f96e93d7e117393172a,
+        0xae2d8a571e03ac9c9eb76fac45af8e51,
+        0x30c81c46a35ce411e5fbc1191a0a52ef,
+        0xf69f2445df4f9b17ad2b417be66c3710]