A library containing come padding operations useful for cryptography
The padding library contains executable formal specifications of several cryptographic padding operations. These operations are described in, for example, Section 5.1.1 of FIPS PUB 180-4.
The library also includes tests and validation theorems about the padding operations.
The following include-book commands may be helpful to bring in the library:
(include-book "kestrel/crypto/padding/pad-to-448" :dir :system) (include-book "kestrel/crypto/padding/pad-to-896" :dir :system)
Or one can do:
(include-book "kestrel/crypto/padding/top" :dir :system)
The interface functions are:
The above functions do not include the encoded length field, as is often done when using these padding operations, leaving that up to the caller if desired. The reason is that cryptogtaphic algorithms differ on the endianness that should be used when storing the length field.
See the comments in the source files for more information.