|
|
|---|
|
|
|
|---|
Introduce an interface for a cryptographic block encryption function.
A cryptographic block encryption function turns a block of plaintext into a block of ciphertext, given a key. Its inverse, a cryptographic block decryption function, turns a block of ciphertext into a block of plaintext, given the same key. Blocks and keys have known sizes in bits. Given an endianness convention to covert between bit and byte sequences, the encryption and decryption functions can be regarded as operating on byte sequences instead of bit sequences.
This macro introduces weakly constrained ACL2 functions for two pairs of cryptographic block encryption and decryption functions: one that operates on bits and one that operates on bytes. Each of these four functions takes as inputs a key and a block, and has a guard requiring them to be bit or byte lists of the right key and block sizes. These functions are constrained to return blocks of the right sizes, 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.
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-block name :key-size ... :block-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 block, 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 both 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 block size (specified by:block-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 divided by 8 (specified by
:key-size ) and the length of the second argument to be the block size divided by 8 (specified by:block-size ).Each function is constrained to:
- Return a byte-listp of the length specified by
:block-size divided by 8.- 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.