1	import Base
2	import ./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.
12	def 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.
16	def 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.
20	def 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	
23	def 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)