aead.bend
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).
29import Base
30import bend-osdev-bytes@0.1.0.0/bytes.bend as B
31import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
32
33# p sealed under a raw key
34def 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
38def 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))