aes: use explicit AES in cbc, cfb, ctr modes #77

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]]

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]]
+
+

Primitive/Symmetric/Cipher/Block/Modes/AES256_CTR.cry → 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,18 +14,10 @@ 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
     k = 0x2b7e151628aed2a6abf7158809cf4f3c
     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]

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

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