From b1b3bdf8fcd8f750cd3d27072a1de7a465871a58 Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Fri, 23 Aug 2024 16:56:26 -0700 Subject: [PATCH 1/8] modes: CBC implementation based on CipherInterface #80 The previous implementation of CBC (not yet removed) takes as input a keysize and an encrypt/decrypt function, and hardcodes the IV and block size to 128 bits. Instead, we'd like to make use of CipherInterface, which makes it easier to instantiate CBC with different block ciphers (and without any hardcoded assumptions on the block size). Removal of the old implementation and updating module-level comments is reserved for future commits --- .../Symmetric/Cipher/Block/Modes/CBC.cry | 41 ++++++++++++++++++- 1 file changed, 40 insertions(+), 1 deletion(-) diff --git a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry index 6cc68637..7b3cbf9f 100644 --- a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry +++ b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry @@ -4,6 +4,7 @@ // Author: Ajay Kumar Eeralla module Primitive::Symmetric::Cipher::Block::Modes::CBC where +import interface Primitive::Symmetric::Cipher::Block::CipherInterface as C // set the sizes type iv = [128] @@ -18,4 +19,42 @@ cbcDec : {n, k} (fin n, fin k) => ([k]->block -> block) -> [k] -> iv -> [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 +property cbcEncCorrect enc k c ps = (cbcDec enc k c (cbcEnc enc k c ps)) == ps + +/** + * CBC encryption: [NIST-SP-800-38A] Section 6.2. + * + * Parameters: key, initialization vector, plaintext + * + * ⚠️ Warning ⚠️: CBC mode requires that the initialization vector (IV) is generated "unpredictably". + * See Appendix C of [NIST-SP-800-38A] for discussion. + */ +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') | p_j <- ps | c' <- [iv] # cs] + +/** + * CBC decryption: [NIST-SP-800-38A] Section 6.2. + * + * Parameters: key, initialization vector, ciphertext + * + * ⚠️ Warning ⚠️: CBC mode requires that the initialization vector (IV) is generated "unpredictably". + * See Appendix C of [NIST-SP-800-38A] for discussion. + */ +decrypt : {n} (fin n) => [C::KeySize] -> [C::BlockSize] -> [n][C::BlockSize] -> [n][C::BlockSize] +decrypt k iv cs = ps + where + ciph_inv_k = C::decrypt k + ps = [ (ciph_inv_k c) ^ c' | c <- cs | c' <- [iv] # cs] + +/** + * 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 From 99514705f256eff95fc18c15d64edbc7a8946a3a Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Fri, 23 Aug 2024 17:01:38 -0700 Subject: [PATCH 2/8] modes: add instantiation + test for AES128_CBC #80 Further tests the new CipherInterface implementation of CBC by instantiating it with AES128. The instantiation can be imported from: Primitive::Symmetric::Cipher::Block::Instantiations::AES128_CBC --- .../Block/Instantiations/AES128_CBC.cry | 10 ++++ .../Cipher/Block/Tests/TestAES_CBC.cry | 57 +++++++++++++++++++ 2 files changed, 67 insertions(+) create mode 100644 Primitive/Symmetric/Cipher/Block/Instantiations/AES128_CBC.cry create mode 100644 Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry diff --git a/Primitive/Symmetric/Cipher/Block/Instantiations/AES128_CBC.cry b/Primitive/Symmetric/Cipher/Block/Instantiations/AES128_CBC.cry new file mode 100644 index 00000000..c009b2cb --- /dev/null +++ b/Primitive/Symmetric/Cipher/Block/Instantiations/AES128_CBC.cry @@ -0,0 +1,10 @@ +/* + * Instantiate CBC mode for AES 128. + * + * @copyright Galois, Inc. + * @author Stanislav Lyakhov + */ +module Primitive::Symmetric::Cipher::Block::Instantiations::AES128_CBC = + Primitive::Symmetric::Cipher::Block::Modes::CBC { + Primitive::Symmetric::Cipher::Block::AES128 + } diff --git a/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry b/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry new file mode 100644 index 00000000..b6b5a47b --- /dev/null +++ b/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry @@ -0,0 +1,57 @@ +/* + * 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 + * @author Stanislav Lyakhov + * 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 + +/** + * ```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] From af37f80e9a44eaa29384c69d45615bf83cd8c4c5 Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Fri, 23 Aug 2024 17:07:00 -0700 Subject: [PATCH 3/8] modes: remove old AES128 CBC implementation/test #80 Now that we've established Modes/CBC.cry, Instantiations/AES128_CBC.cry, and Tests/TestAES_CBC.cry as the CBC implementation, instantiation, and testing, we can remove the old implementations. --- .../Cipher/Block/Modes/AES128_CBC.cry | 73 ------------------- .../Symmetric/Cipher/Block/Modes/CBC.cry | 15 ---- 2 files changed, 88 deletions(-) delete mode 100644 Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry diff --git a/Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry deleted file mode 100644 index 76421a61..00000000 --- a/Primitive/Symmetric/Cipher/Block/Modes/AES128_CBC.cry +++ /dev/null @@ -1,73 +0,0 @@ -// Cryptol AES CBC test vectors -// @copyright Galois Inc. 2010-2018, -// @author Ajay Kumar Eeralla -// www.cryptol.net - -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::KeySize] -> iv -> [n]block -> [n]block -AES128_CBC_encrypt = cbcEnc AES128::encrypt - -AES128_CBC_decrypt: {n} (fin n) => [AES128::KeySize] -> iv -> [n]block -> [n]block -AES128_CBC_decrypt = cbcDec AES128::decrypt -// Test vectors from https://tools.ietf.org/html/rfc3602 - -/** - * CBC mode with 1 block works. - * ```repl - * :prove testEncCbcPassB1 - * ``` - */ -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]] - - -/** - * CBC mode with 2 block works. - * ```repl - * :prove testEncCbcPassB2 - * ``` - */ -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]] - - -/** - * CBC mode with 3 block works. - * ```repl - * :prove testEncCbcPassB3 - * ``` - */ -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]] - -/** - * CBC mode with 4 block works. - * ```repl - * :prove testEncCbcPassB4 - * ``` - */ -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/CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry index 7b3cbf9f..e285fca2 100644 --- a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry +++ b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry @@ -6,21 +6,6 @@ module Primitive::Symmetric::Cipher::Block::Modes::CBC where import interface Primitive::Symmetric::Cipher::Block::CipherInterface as C -// set the sizes -type iv = [128] -type block = [128] - - -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 ] - -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 enc k c ps = (cbcDec enc k c (cbcEnc enc k c ps)) == ps - /** * CBC encryption: [NIST-SP-800-38A] Section 6.2. * From 38ae90bc55e54214a2675e7fc7d7dbe0f206e724 Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Fri, 23 Aug 2024 17:23:28 -0700 Subject: [PATCH 4/8] modes: update CBC module comment #80 Comment updated to follow format set throughout cryptol-specs. --- .../Symmetric/Cipher/Block/Modes/CBC.cry | 23 +++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry index e285fca2..a204737a 100644 --- a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry +++ b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry @@ -1,7 +1,22 @@ -// 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 ⚠️: CBC mode requires that the initialization vector (IV) is generated "unpredictably". + * See Appendix C of [NIST-SP-800-38A] for discussion. + * + * @copyright Galois, Inc. + * @author Ajay Kumar Eeralla + * @author Marcella Hastings + * @author Stanislav Lyakhov + * 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. + * + */ + module Primitive::Symmetric::Cipher::Block::Modes::CBC where import interface Primitive::Symmetric::Cipher::Block::CipherInterface as C From dad7d7867b70358affaafc9b3edd8c116afaa0f6 Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Fri, 23 Aug 2024 17:49:03 -0700 Subject: [PATCH 5/8] modes: add AES192 CBC instantiation and test vectors #80 --- .../Block/Instantiations/AES192_CBC.cry | 10 +++++ .../Cipher/Block/Tests/TestAES_CBC.cry | 41 +++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 Primitive/Symmetric/Cipher/Block/Instantiations/AES192_CBC.cry diff --git a/Primitive/Symmetric/Cipher/Block/Instantiations/AES192_CBC.cry b/Primitive/Symmetric/Cipher/Block/Instantiations/AES192_CBC.cry new file mode 100644 index 00000000..80eebb19 --- /dev/null +++ b/Primitive/Symmetric/Cipher/Block/Instantiations/AES192_CBC.cry @@ -0,0 +1,10 @@ +/* + * Instantiate CBC mode for AES 192. + * + * @copyright Galois, Inc. + * @author Stanislav Lyakhov + */ +module Primitive::Symmetric::Cipher::Block::Instantiations::AES192_CBC = + Primitive::Symmetric::Cipher::Block::Modes::CBC { + Primitive::Symmetric::Cipher::Block::AES192 + } diff --git a/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry b/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry index b6b5a47b..a731619a 100644 --- a/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry +++ b/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry @@ -15,6 +15,7 @@ * */ import Primitive::Symmetric::Cipher::Block::Instantiations::AES128_CBC as AES128_CBC +import Primitive::Symmetric::Cipher::Block::Instantiations::AES192_CBC as AES192_CBC /** * ```repl @@ -55,3 +56,43 @@ property aes128_cbc_decrypt_vector = (AES128_CBC::decrypt k iv ciphertext) == pl 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] From 2f56503676ae05524e0f2838ed4bbf23b00a35aa Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Fri, 23 Aug 2024 21:32:32 -0700 Subject: [PATCH 6/8] modes: add AES256 CBC instantiation and test vectors #80 --- .../Block/Instantiations/AES256_CBC.cry | 10 +++++ .../Cipher/Block/Tests/TestAES_CBC.cry | 41 +++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 Primitive/Symmetric/Cipher/Block/Instantiations/AES256_CBC.cry diff --git a/Primitive/Symmetric/Cipher/Block/Instantiations/AES256_CBC.cry b/Primitive/Symmetric/Cipher/Block/Instantiations/AES256_CBC.cry new file mode 100644 index 00000000..710bd9f7 --- /dev/null +++ b/Primitive/Symmetric/Cipher/Block/Instantiations/AES256_CBC.cry @@ -0,0 +1,10 @@ +/* + * Instantiate CBC mode for AES 256. + * + * @copyright Galois, Inc. + * @author Stanislav Lyakhov + */ +module Primitive::Symmetric::Cipher::Block::Instantiations::AES256_CBC = + Primitive::Symmetric::Cipher::Block::Modes::CBC { + Primitive::Symmetric::Cipher::Block::AES256 + } diff --git a/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry b/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry index a731619a..39256fd1 100644 --- a/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry +++ b/Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry @@ -16,6 +16,7 @@ */ 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 @@ -96,3 +97,43 @@ property aes192_cbc_decrypt_vector = (AES192_CBC::decrypt k iv ciphertext) == pl 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] From 9b9d5a0a803dcecd116c71b87b7035cb541f64e6 Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Wed, 28 Aug 2024 10:48:24 -0700 Subject: [PATCH 7/8] modes: elaborate on IV generation warnings for CBC #80 * Mention Appendix D that discusses what can go wrong if the IV is predictable. * Emphasize that cryptol cannot check that IVs were generated correctly. --- .../Symmetric/Cipher/Block/Modes/CBC.cry | 24 ++++++++++++------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry index a204737a..a8c1ee9c 100644 --- a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry +++ b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry @@ -1,8 +1,12 @@ /* * Cipher Block Chaining mode of operation, as defined in [NIST-SP-800-38A], Section 6.2. * - * ⚠️ Warning ⚠️: CBC mode requires that the initialization vector (IV) is generated "unpredictably". - * See Appendix C of [NIST-SP-800-38A] for discussion. + * ⚠️ 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 @@ -10,10 +14,10 @@ * @author Stanislav Lyakhov * 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. + * Modes of Operation: Methods and Techniques. NIST Special Publication + * 800-38A. December 2001. + * @see https://doi.org/10.6028/NIST.SP.800-38A * */ @@ -26,8 +30,9 @@ import interface Primitive::Symmetric::Cipher::Block::CipherInterface as C * * Parameters: key, initialization vector, plaintext * - * ⚠️ Warning ⚠️: CBC mode requires that the initialization vector (IV) is generated "unpredictably". - * See Appendix C of [NIST-SP-800-38A] for discussion. + * ⚠️ 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 @@ -40,8 +45,9 @@ encrypt k iv ps = cs * * Parameters: key, initialization vector, ciphertext * - * ⚠️ Warning ⚠️: CBC mode requires that the initialization vector (IV) is generated "unpredictably". - * See Appendix C of [NIST-SP-800-38A] for discussion. + * ⚠️ 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 From b00f2001d6d973e072368872e6f2bf7f5bd1e991 Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Wed, 28 Aug 2024 13:35:53 -0700 Subject: [PATCH 8/8] modes: match cbc variable names closer to spec #80 * Match variable capitalization * Use C_j_1 instead of c' to refer to $C_{j-1}$ --- Primitive/Symmetric/Cipher/Block/Modes/CBC.cry | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry index a8c1ee9c..680f410a 100644 --- a/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry +++ b/Primitive/Symmetric/Cipher/Block/Modes/CBC.cry @@ -35,10 +35,10 @@ import interface Primitive::Symmetric::Cipher::Block::CipherInterface as C * 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 +encrypt K IV Ps = Cs where - ciph_k = C::encrypt k - cs = [ ciph_k (p_j ^ c') | p_j <- ps | c' <- [iv] # cs] + CIPH_K = C::encrypt K + Cs = [ CIPH_K (P_j ^ C_j_1) | P_j <- Ps | C_j_1 <- [IV] # Cs] /** * CBC decryption: [NIST-SP-800-38A] Section 6.2. @@ -50,10 +50,10 @@ encrypt k iv ps = cs * 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 +decrypt K IV Cs = Ps where - ciph_inv_k = C::decrypt k - ps = [ (ciph_inv_k c) ^ c' | c <- cs | c' <- [iv] # cs] + CIPH_K_inv = C::decrypt K + Ps = [ (CIPH_K_inv C_j) ^ C_j_1 | C_j <- Cs | C_j_1 <- [IV] # Cs] /** * Decryption must be the inverse of encryption. @@ -63,4 +63,4 @@ decrypt k iv cs = ps * ``` */ 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 +property encryptCorrect K IV Ps = (decrypt K IV (encrypt K IV Ps)) == Ps