Skip to content

Commit

Permalink
modes: add AES192 CBC instantiation and test vectors #80
Browse files Browse the repository at this point in the history
  • Loading branch information
staslyakhov committed Aug 24, 2024
1 parent 38ae90b commit dad7d78
Show file tree
Hide file tree
Showing 2 changed files with 51 additions and 0 deletions.
10 changes: 10 additions & 0 deletions Primitive/Symmetric/Cipher/Block/Instantiations/AES192_CBC.cry
Original file line number Diff line number Diff line change
@@ -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
}
41 changes: 41 additions & 0 deletions Primitive/Symmetric/Cipher/Block/Tests/TestAES_CBC.cry
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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]

0 comments on commit dad7d78

Please sign in to comment.