1	# The AEAD interface (authenticated encryption with associated data, in the
2	# shape of RFC 5116).
3	#
4	# An AEAD (template arguments, in this order):
5	#   ~K: Data                                       its key, prepared
6	#   ~key: B.Octets -> Result<&2, &2, CrError, K>   the key of a raw key
7	#   ~seal: K -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, CrError, B.Octets>
8	#                                                  key, nonce, associated
9	#                                                  data, plaintext: the
10	#                                                  ciphertext with its tag,
11	#                                                  or the refusal of a bad
12	#                                                  nonce or length
13	#   ~open: K -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, CrError, B.Octets>
14	#                                                  key, nonce, associated
15	#                                                  data, ciphertext with tag:
16	#                                                  the plaintext, or
17	#                                                  CrTagMismatch (no
18	#                                                  plaintext released)
19	# Laws (README.md, "Laws"):
20	#   round_trip  open accepts what seal produced and gives the plaintext
21	#               back; when seal refuses, open-after-seal refuses alike:
22	#               bind(seal(k, n, a, p), c => open(k, n, a, c)) ==
23	#               map(c => p, seal(k, n, a, p))
24	#   tamper      a changed tag, ciphertext or associated data is refused
25	#               (CrTagMismatch): tested (a forgery succeeds with
26	#               probability 2^-8tlen, so it is not a law for every input)
27	#
28	# The instances: CCM over any 128-bit block cipher (inst_ccm.bend).
29	import Base
30	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
31	import ./crypto.bend as Cr
32	
33	# p sealed under a raw key
34	def CrAead.seal_with(~K: Data, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~seal: K -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, key_o: B.Octets, nonce: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
35	  Result.bind(&2, &2, Cr.CrError, K, B.Octets, key(key_o), k => seal(k, nonce, aad, p))
36	
37	# c opened under a raw key
38	def CrAead.open_with(~K: Data, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, ~open: K -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, key_o: B.Octets, nonce: B.Octets, aad: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
39	  Result.bind(&2, &2, Cr.CrError, K, B.Octets, key(key_o), k => open(k, nonce, aad, c))