		Search-engine friendly clone of the ACL2 documentation.

Cryptography

Padding

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:

(pad-to-448 bits): Given list of any number of bits, add a single 1 bit, followed by enough 0 bits to make the resulting list's length be congruent to 448 modulo 512.
(pad-to-896 bits): Given list of any number of bits, add a single 1 bit, followed by enough 0 bits to make the resulting list's length be congruent to 896 modulo 1024.

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.