diff --git a/Primitive/Symmetric/Cipher/Block/README.md b/Primitive/Symmetric/Cipher/Block/README.md index 75e57515..692b0a3e 100644 --- a/Primitive/Symmetric/Cipher/Block/README.md +++ b/Primitive/Symmetric/Cipher/Block/README.md @@ -1 +1,43 @@ Symmetric ciphers that work on a block at a time. + +## AES Migration Guide +In [PR #79](https://github.com/GaloisInc/cryptol-specs/pull/79), we simplified the AES modules and in doing so changed the public API used for AES. +To update to the new module structure, you may need to make changes to your cryptol specs that use AES. + +If you previously used `AES.cry`, you were implicitly using AES256. Update your import line to use `AES256.cry`, and update your encrypt and decrypt functions to change the name and order of arguments. +Before: +```haskell +import Primitive::Symmetric::Cipher::Block::AES +... +ct = aesEncrypt(data, key) +pt = aesDecrypt(ct, key) +``` +After: +```haskell +import Primitive::Symmetric::Cipher::Block::AES256 as AES256 +... +ct = AES256::encrypt key data +pt = AES256::decrypt key ct +``` + +If you previously used `AES_parameterized.cry`, or if you want to implement something using AES with an arbitrary key length, update your import line to use `AES_specification.cry`, paramterized +with your own key length parameter. The remaining API is unchanged, although we added a publicly accessible `KeySize` type. +Before: +```haskell +import Primitive::Symmetric::Cipher::Block::AES_parameterized as AES + +parameter + /** 0: use AES128, 1: use AES192, 2: use AES256 */ + type Mode : # + type constraint (2 >= Mode) +``` +After +```haskell +parameter + // This constraint enforces the standard key sizes of 128, 192, and 256 bits. + type KeySize : # + type constraint (fin KeySize, KeySize % 64 == 0, KeySize / 64 >= 1, KeySize / 64 <= 4) + +import Primitive::Symmetric::Cipher::Block::AES_specification as AES where + type KeySize' = KeySize +``` \ No newline at end of file