|
|
|---|
|
|
|
|---|
Introduce an interface for a cryptographic encryption function with an initialization vector.
Block encryption functions (whose interfaces may be generated via definterface-encrypt-block) may be used to encrypt data larger than single blocks by combining multiple block encryptions according to various schemes (e.g. CBC). Some of these schemes require an initialization vector as additional input. This also applies to the inverse decryption functions.
This macro introduces weakly constrained ACL2 functions for two pairs of cryptographic encryption and decryption functions that use an initialization vector: one that operates on bits and one that operates on bytes. Each of these four functions takes as inputs a key, an initialization vector, and some arbitrary data, and has a guard requiring all three to be bit or byte lists and the first two to have the right key and block sizes. These functions are constrained to return sequences of bits or bytes, and also to fix their inputs to bit or byte lists. We may extend this macro to generate additional constraints, such as the fact that encryption and decryption are mutual inverses, or that the size of the ouput data is suitably related to the input data. These functions are meant to also pad the input data to the block size; then the size of the output data consist of as many blocks as the padded input blocks.
This macro also introduces a few theorems that follow from the constraints. It also introduces an XDOC topic for the generated functions, constraints, and theorems.
(definterface-encrypt-init name :key-size ... :init-size ... :name-encrypt-bits ... :name-decrypt-bits ... :name-encrypt-bytes ... :name-decrypt-bytes ... :topic ... :parents ... :short ... :long ... )
A symbol that names the encryption algorithm.
A constant expression whose value is a positive integer multiple of 8. This is the size of the key, in bits.
A constant expression whose value is a positive integer multiple of 8. This is the size of the initialization vector, in bits.
A symbol that names the generated constrained encryption function that operates on bits.
If not supplied, it defaults to
name followed by-encrypt-bits .
A symbol that names the generated constrained decryption function that operates on bits.
If not supplied, it defaults to
name followed by-decrypt-bits .
A symbol that names the generated constrained encryption function that operates on bytes.
If not supplied, it defaults to
name followed by-encrypt-bytes .
A symbol that names the generated constrained decryption function that operates on bytes.
If not supplied, it defaults to
name followed by-decrypt-bytes .
A symbol that names the generated XDOC topic that surrounds the generated functions and theorems.
If not supplied, it defaults to
name followed by-interface .
These, if present, are added to the XDOC topic generated for the fixtype.
Constrained encryption and decryption functions that operate on bits.
Their guard consists of bit-listp for all arguments and requires the length of the first argument to be the key size (specified by
:key-size and the length of the second argument to be the initialization vector size (specified by:init-size .Each function is constrained to:
The following additional theorems are also generated:
- A type prescription rules saying that each function returns a true-listp.
- A type prescription rule saying that each function returns a consp.
Constrained encryption and decryption functions that operate on bytes.
Their guard consists of byte-listp for both arguments and requires the length of the first argument to be the key size (specified by
:key-size ) divided by 8 and the length of the second argument to be the initialization vector size (specified by:init-size ) divided by 8.Each function is constrained to:
- Return a byte-listp.
- Fix its input to a byte-listp.
The following additional theorems are also generated:
- A type prescription rules saying that each function returns a true-listp.
- A type prescription rule saying that each function returns a consp.