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-listpfor 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-listpfor 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.

- Definterface-encrypt-init-fn
- Events generated by
`definterface-encrypt-init`. - Definterface-encrypt-init-macro-definition
- Definition of the
`definterface-encrypt-init`macro.