src/crypto/aesgcm.bend

bend-collections-laws-crypto@1.0.0.0 · 24 lines · 4 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as G
3
4# AES-GCM authenticated encryption (NIST SP 800-38D, AES from FIPS 197):
5# 96-bit (12-byte) nonces, 128-bit (16-byte) tags appended to the
6# ciphertext. Bytes are U32 values below 256. A key or nonce of the wrong
7# length gives None; decryption gives None when the tag does not match
8# (compared in constant time with subtle.eq). Proved equal to the executable
9# specification spec/crypto/aes/gcm.bend (proofs/crypto/aes/).
10
11# AES-128-GCM: a 16-byte key. Returns ciphertext || tag.
12def aes128_gcm_encrypt(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +pt: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
13  G.seal_key(G.schedule_of(16n, key), nonce, aad, pt)
14
15# The plaintext of ciphertext || tag, or None.
16def aes128_gcm_decrypt(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
17  G.open_key(G.schedule_of(16n, key), nonce, aad, ct)
18
19# AES-256-GCM: a 32-byte key.
20def aes256_gcm_encrypt(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +pt: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
21  G.seal_key(G.schedule_of(32n, key), nonce, aad, pt)
22
23def aes256_gcm_decrypt(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
24  G.open_key(G.schedule_of(32n, key), nonce, aad, ct)