diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry
new file mode 100644
index 00000000..7acce0bc
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry
@@ -0,0 +1,53 @@
+// Cryptol AES CBC test vectors
+// Copyright (c) 2010-2018, Galois Inc.
+// www.cryptol.net
+// Author: Ajay Kumar Eeralla
+
+module Primitive::Symmetric::Cipher::Block::Modes::AES128_CBC where
+import Primitive::Symmetric::Cipher::Block::Modes::CBC
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
+
+AES128_CBC_encrypt: {n} (fin n) => [AES128::AesKeySize] -> iv -> [n]block -> [n]block
+AES128_CBC_encrypt = cbcEnc AES128::encrypt
+
+AES128_CBC_decrypt: {n} (fin n) => [AES128::AesKeySize] -> iv -> [n]block -> [n]block
+AES128_CBC_decrypt = cbcDec AES128::decrypt
+// Test vectors from https://tools.ietf.org/html/rfc3602
+
+// No. of blocks := 1
+property testEncCbcPassB1 = and [ (AES128_CBC_encrypt k iv ps) == cs
+                                | k <- testKey | iv <- testIv | ps <- testPt | cs <- testCt ]
+    where
+        testKey = [0x06a9214036b8a15b512e03d534120006]
+        testIv = [0x3dafba429d9eb430b422da802c9fac41]
+        testPt = [[join "Single block msg"]]
+        testCt = [[0xe353779c1079aeb82708942dbe77181a]]
+
+
+// No. of blocks := 2
+property testEncCbcPassB2 = and [ (AES128_CBC_encrypt k iv ps) == cs
+                                | k <- testKey2 | iv <- testIv2 | ps <- testPt2 | cs <- testCt2 ]
+    where
+        testKey2 = [0xc286696d887c9aa0611bbb3e2025a45a]
+        testIv2 = [0x562e17996d093d28ddb3ba695a2e6f58]
+        testPt2 = [[0x000102030405060708090a0b0c0d0e0f, 0x101112131415161718191a1b1c1d1e1f]]
+        testCt2 = [[0xd296cd94c2cccf8a3a863028b5e1dc0a, 0x7586602d253cfff91b8266bea6d61ab1]]
+
+
+// No. of blocks := 3
+property testEncCbcPassB3 = and [ (AES128_CBC_encrypt k iv ps) == cs
+                                | k <- testKey3 | iv <- testIv3 | ps <- testPt3 | cs <- testCt3 ]
+    where
+        testKey3 = [0x6c3ea0477630ce21a2ce334aa746c2cd]
+        testIv3 = [0xc782dc4c098c66cbd9cd27d825682c81]
+        testPt3 = [[0x5468697320697320612034382d627974, 0x65206d65737361676520286578616374, 0x6c7920332041455320626c6f636b7329]]
+        testCt3 = [[0xd0a02b3836451753d493665d33f0e886, 0x2dea54cdb293abc7506939276772f8d5, 0x021c19216bad525c8579695d83ba2684]]
+
+// No. of blocks := 4
+property testEncCbcPassB4 = and [ (AES128_CBC_encrypt k iv ps) == cs
+                                | k <- testKey4 | iv <- testIv4 | ps <- testPt4 | cs <- testCt4 ]
+    where
+        testKey4 = [0x56e47a38c5598974bc46903dba290349]
+        testIv4 = [0x8ce82eefbea0da3c44699ed7db51b7d9]
+        testPt4 = [[0xa0a1a2a3a4a5a6a7a8a9aaabacadaeaf, 0xb0b1b2b3b4b5b6b7b8b9babbbcbdbebf, 0xc0c1c2c3c4c5c6c7c8c9cacbcccdcecf, 0xd0d1d2d3d4d5d6d7d8d9dadbdcdddedf]]
+        testCt4 = [[0xc30e32ffedc0774e6aff6af0869f71aa, 0x0f3af07a9a31a9c684db207eb0ef8e4e, 0x35907aa632c3ffdf868bb7b29d3d46ad, 0x83ce9f9a102ee99d49a53e87f4c3da55]]
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES128_CFB.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CFB.cry
new file mode 100644
index 00000000..3dc78d81
--- /dev/null
+++ b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CFB.cry
@@ -0,0 +1,37 @@
+// Cryptol AES CFB test vectors
+// Copyright (c) 2010-2018, Galois Inc.
+// www.cryptol.net
+// You can freely use this source code for educational purposes.
+// Author: Ajay Kumar Eeralla
+
+module Primitive::Symmetric::Cipher::Block::Modes::AES128_CFB where
+import Primitive::Symmetric::Cipher::Block::Modes::CFB
+import Primitive::Symmetric::Cipher::Block::AES128 as AES128
+
+AES128_CFB_encrypt: {n} (fin n) => [AES128::AesKeySize] -> iv -> [n]block -> [n]block
+AES128_CFB_encrypt = cfbEnc AES128::encrypt
+
+AES128_CFB_decrypt: {n} (fin n) => [AES128::AesKeySize] -> iv -> [n]block -> [n]block
+AES128_CFB_decrypt = cfbDec AES128::decrypt
+
+// Test vectors from https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-38a.pdf
+// No. of blocks := 1
+property testEncCfbPassB1 = and [ (AES128_CFB_encrypt k iv ps) == cs
+                                | k <- testKey | iv <- testIv | ps <- testPt | cs <- testCt ]
+    where
+        testKey = [0x2b7e151628aed2a6abf7158809cf4f3c]
+        testIv = [0x000102030405060708090a0b0c0d0e0f]
+        testPt = [[0x6bc1bee22e409f96e93d7e117393172a]]
+        testCt = [[0x3b3fd92eb72dad20333449f8e83cfb4a]]
+
+
+// No. of blocks := 2
+property testEncCfbPassB2 = and [ (AES128_CFB_encrypt k iv ps) == cs
+                                | k <- testKey2 | iv <- testIv2 | ps <- testPt2 | cs <- testCt2 ]
+    where
+        testKey2 = [0x2b7e151628aed2a6abf7158809cf4f3c]
+        testIv2 = [0x000102030405060708090a0b0c0d0e0f]
+        testPt2 = [[0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]]
+        testCt2 = [[0x3b3fd92eb72dad20333449f8e83cfb4a, 0xc8a64537a0b3a93fcde3cdad9f1ce58b, 0x26751f67a3cbb140b1808cf187a4f4df, 0xc04b05357c5d1c0eeac4c66f9ff7f2e6]]
+
+
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES256_CTR.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CTR.cry
similarity index 63%
rename from Primitive/Symmetric/Cipher/Block/Modes/AES256_CTR.cry
rename to Primitive/Symmetric/Cipher/Block/Modes/AES128_CTR.cry
index 45d724ab..7e4b0153 100644
--- a/Primitive/Symmetric/Cipher/Block/Modes/AES256_CTR.cry
+++ b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CTR.cry
@@ -4,9 +4,8 @@
 // Author: Ajay Kumar Eeralla
 // Test vector from https://nvlpubs.nist.gov/nistpubs/Legacy/SP nistspecialpublication800-38a.pdf
 
-module Primitive::Symmetric::Cipher::Block::Modes::AES_CTR where
+module Primitive::Symmetric::Cipher::Block::Modes::AES128_CTR where
 import Primitive::Symmetric::Cipher::Block::Modes::CTR
-import Primitive::Symmetric::Cipher::Block::AES_parameterized
 import Primitive::Symmetric::Cipher::Block::AES128 as AES128
 
 AES128_CTR_encrypt: {n} (fin n) => [AES128::AesKeySize] -> ic -> [n]block -> [n]block
@@ -15,7 +14,6 @@ AES128_CTR_encrypt = ctrEnc AES128::encrypt
 AES128_CTR_decrypt: {n} (fin n) => [AES128::AesKeySize] -> ic -> [n]block -> [n]block
 AES128_CTR_decrypt = ctrDec AES128::decrypt
 
-
 // This `:prove`s quickly!
 property aes128_ctr_enc_test_vector_passes = (AES128_CTR_encrypt k ic plaintext) == ciphertext
     where
@@ -23,10 +21,3 @@ property aes128_ctr_enc_test_vector_passes = (AES128_CTR_encrypt k ic plaintext)
     ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
     plaintext = [0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]
     ciphertext = [0x874d6191b620e3261bef6864990db6ce, 0x9806f66b7970fdff8617187bb9fffdff, 0x5ae4df3edbd5d35e5b4f09020db03eab, 0x1e031dda2fbe03d1792170a0f3009cee]
-
-property aes128_ctr_dec_test_vector_passes = (AES128_CTR_decrypt k ic ciphertext) == plaintext
-    where
-    k = 0x2b7e151628aed2a6abf7158809cf4f3c
-    ic = 0xf0f1f2f3f4f5f6f7f8f9fafbfcfdfeff
-    ciphertext = [0x874d6191b620e3261bef6864990db6ce, 0x9806f66b7970fdff8617187bb9fffdff, 0x5ae4df3edbd5d35e5b4f09020db03eab, 0x1e031dda2fbe03d1792170a0f3009cee]
-    plaintext = [0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]
\ No newline at end of file
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES_CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES_CBC.cry
deleted file mode 100644
index 6c08af7f..00000000
--- a/Primitive/Symmetric/Cipher/Block/Modes/AES_CBC.cry
+++ /dev/null
@@ -1,53 +0,0 @@
-// Cryptol AES CBC test vectors
-// Copyright (c) 2010-2018, Galois Inc.
-// www.cryptol.net
-// Author: Ajay Kumar Eeralla
-
-module Primitive::Symmetric::Cipher::Block::Modes::AES_CBC where
-import Primitive::Symmetric::Cipher::Block::Modes::CBC
-import Primitive::Symmetric::Cipher::Block::AES_parameterized
-
-property cbcEncCorrect encrypt k c ps = (cbcDec encrypt k c (cbcEnc encrypt k c ps)) == ps
-
-// Test vectors from https://tools.ietf.org/html/rfc3602
-
-// No. of blocks := 1
-
-testKey = [0x06a9214036b8a15b512e03d534120006]
-testIv = [0x3dafba429d9eb430b422da802c9fac41]
-testPt = [[join "Single block msg"]]
-testCt = [[0xe353779c1079aeb82708942dbe77181a]]
-
-property testEncCbcPassB1 = and [ (cbcEnc encrypt k iv ps) == cs
-                                | k <- testKey | iv <- testIv | ps <- testPt | cs <- testCt ]
-
-// No. of blocks := 2
-
-testKey2 = [0xc286696d887c9aa0611bbb3e2025a45a]
-testIv2 = [0x562e17996d093d28ddb3ba695a2e6f58]
-testPt2 = [[0x000102030405060708090a0b0c0d0e0f, 0x101112131415161718191a1b1c1d1e1f]]
-testCt2 = [[0xd296cd94c2cccf8a3a863028b5e1dc0a, 0x7586602d253cfff91b8266bea6d61ab1]]
-
-property testEncCbcPassB2 = and [ (cbcEnc encrypt k iv ps) == cs
-                                | k <- testKey2 | iv <- testIv2 | ps <- testPt2 | cs <- testCt2 ]
-                                
-
-// No. of blocks := 3
-
-testKey3 = [0x6c3ea0477630ce21a2ce334aa746c2cd]
-testIv3 = [0xc782dc4c098c66cbd9cd27d825682c81]
-testPt3 = [[0x5468697320697320612034382d627974, 0x65206d65737361676520286578616374, 0x6c7920332041455320626c6f636b7329]]
-testCt3 = [[0xd0a02b3836451753d493665d33f0e886, 0x2dea54cdb293abc7506939276772f8d5, 0x021c19216bad525c8579695d83ba2684]]
-
-property testEncCbcPassB3 = and [ (cbcEnc encrypt k iv ps) == cs
-                                | k <- testKey3 | iv <- testIv3 | ps <- testPt3 | cs <- testCt3 ]
-
-// No. of blocks := 4
-
-testKey4 = [0x56e47a38c5598974bc46903dba290349]
-testIv4 = [0x8ce82eefbea0da3c44699ed7db51b7d9]
-testPt4 = [[0xa0a1a2a3a4a5a6a7a8a9aaabacadaeaf, 0xb0b1b2b3b4b5b6b7b8b9babbbcbdbebf, 0xc0c1c2c3c4c5c6c7c8c9cacbcccdcecf, 0xd0d1d2d3d4d5d6d7d8d9dadbdcdddedf]]
-testCt4 = [[0xc30e32ffedc0774e6aff6af0869f71aa, 0x0f3af07a9a31a9c684db207eb0ef8e4e, 0x35907aa632c3ffdf868bb7b29d3d46ad, 0x83ce9f9a102ee99d49a53e87f4c3da55]]
-
-property testEncCbcPassB4 = and [ (cbcEnc encrypt k iv ps) == cs
-                                | k <- testKey4 | iv <- testIv4 | ps <- testPt4 | cs <- testCt4 ]
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES_CFB.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES_CFB.cry
deleted file mode 100644
index 67899af8..00000000
--- a/Primitive/Symmetric/Cipher/Block/Modes/AES_CFB.cry
+++ /dev/null
@@ -1,33 +0,0 @@
-// Cryptol AES CFB test vectors
-// Copyright (c) 2010-2018, Galois Inc.
-// www.cryptol.net
-// You can freely use this source code for educational purposes.
-// Author: Ajay Kumar Eeralla
-
-module Primitive::Symmetric::Cipher::Block::Modes::AES_CFB where
-import Primitive::Symmetric::Cipher::Block::Modes::CFB
-import Primitive::Symmetric::Cipher::Block::AES_parameterized
-
-property cfbEncCorrect encrypt k c ps = (cfbDec encrypt k c (cfbEnc encrypt k c ps)) == ps
-
-// Test vectors from https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-38a.pdf
-// No. of blocks := 1
-
-testKey = [0x2b7e151628aed2a6abf7158809cf4f3c]
-testIv = [0x000102030405060708090a0b0c0d0e0f]
-testPt = [[0x6bc1bee22e409f96e93d7e117393172a]]
-testCt = [[0x3b3fd92eb72dad20333449f8e83cfb4a]]
-
-property testEncCfbPassB1 = and [ (cfbEnc encrypt k iv ps) == cs
-                                | k <- testKey | iv <- testIv | ps <- testPt | cs <- testCt ]
-
-// No. of blocks := 2
-
-testKey2 = [0x2b7e151628aed2a6abf7158809cf4f3c]
-testIv2 = [0x000102030405060708090a0b0c0d0e0f]
-testPt2 = [[0x6bc1bee22e409f96e93d7e117393172a, 0xae2d8a571e03ac9c9eb76fac45af8e51, 0x30c81c46a35ce411e5fbc1191a0a52ef, 0xf69f2445df4f9b17ad2b417be66c3710]]
-testCt2 = [[0x3b3fd92eb72dad20333449f8e83cfb4a, 0xc8a64537a0b3a93fcde3cdad9f1ce58b, 0x26751f67a3cbb140b1808cf187a4f4df, 0xc04b05357c5d1c0eeac4c66f9ff7f2e6]]
-
-property testEncCfbPassB2 = and [ (cfbEnc encrypt k iv ps) == cs
-                                | k <- testKey2 | iv <- testIv2 | ps <- testPt2 | cs <- testCt2 ]
-
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry
index 470ea0e0..6cc68637 100644
--- a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry
+++ b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry
@@ -17,4 +17,5 @@ cbcEnc enc k iv ps = 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 ]
 
-
+// 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
diff --git a/Primitive/Symmetric/Cipher/Block/Modes/CFB.cry b/Primitive/Symmetric/Cipher/Block/Modes/CFB.cry
index f7c0195e..8a4d887a 100644
--- a/Primitive/Symmetric/Cipher/Block/Modes/CFB.cry
+++ b/Primitive/Symmetric/Cipher/Block/Modes/CFB.cry
@@ -18,4 +18,6 @@ cfbEnc enc k iv ps = cs
 cfbDec : {n, k} (fin n, fin k) => ([k]->block -> block) -> [k] -> iv -> [n]block -> [n]block
 cfbDec enc k iv cs = [ (enc k c')^c | c <- cs | c' <- [iv] # cs ]
 
+// This will need to be parameterized with a specific encryption function before it can be proved
+property cfbEncCorrect encrypt k c ps = (cfbDec encrypt k c (cfbEnc encrypt k c ps)) == ps