Interfaces
Cryptographic interfaces.
Cryptographic functions are largely black boxes,
in the sense that most of their details
are not needed in order to describe the behavior of
systems that use cryptography.
Thus, it is useful to introduce interfaces for cryptographic functions,
in the form of (weakly) constrained ACL2 functions,
whose only properties concern, for instance,
the types of their inputs and outputs.
A formalization that involves cryptography
can include and use these interfaces,
whose relatively shallow properties should nonetheless suffice,
because of the aforementioned black-box nature of cryptography.
In other words, a formalization can be parameterized
over the details of the cryptographic functions,
without having to include and use full definitions of these functions.
Executable attachments for these interfaces can be used
to execute code that calls these interfaces.
It should be also possible to automatically specialize
code that uses these interfaces
to use (compatible) full definitions of the functions.
We provide macros to generate cryptographic interfaces of various kinds
(e.g. interfaces for hash functions),
as well as interfaces for various standard cryptographic functions.
Subtopics
- Definterface-hmac
- Introduce an interface for a cryptographic
hash-based message authentication (HMAC) function.
- Definterface-encrypt-block
- Introduce an interface for a cryptographic block encryption function.
- Definterface-hash
- Introduce an interface for a cryptographic hash function.
- Definterface-encrypt-init
- Introduce an interface for a cryptographic encryption function
with an initialization vector.
- Definterface-pbkdf2
- Introduce an interface for a password-based key derivation function 2 (PBKDF2).
- Aes-256-cbc-pkcs7-interface
- AES-256 CBC PKCS7 interface.
- Aes-192-cbc-pkcs7-interface
- AES-192 CBC PKCS7 interface.
- Aes-128-cbc-pkcs7-interface
- AES-128 CBC PKCS7 interface.
- Aes-256-interface
- AES-256 interface.
- Aes-192-interface
- AES-192 interface.
- Aes-128-interface
- AES-128 interface.
- Pbkdf2-hmac-sha-512-interface
- PBKDF2-HMAC-SHA-512 interface.
- Keccak-256-interface
- Keccak-256 interface.
- Sha-256-interface
- SHA-256 interface.
- Keccak-512-interface
- Keccak-512 interface.
- Ripemd-160-interface
- RIPEMD-160 interface.
- Sha-512-interface
- SHA-512 interface.
- Pbkdf2-hmac-sha-256-interface
- PBKDF2 HMAC-SHA-256 interface.
- Hmac-sha-512-interface
- HMAC-SHA-512 interface.
- Hmac-sha-256-interface
- HMAC-SHA-256 interface.
- Secp256k1-interface
- Elliptic curve secp256k1 interface.
- Secp256k1-ecdsa-interface
- ECDSA interface for the elliptic curve secp256k1.
