aead.bend

bend-osdev-aead@0.1.0.0 · 36 lines · 5 definitions

1# bend-osdev-aead: authenticated encryption with associated data, as
2# instances of bend-osdev-crypto's AEAD interface (crypto/aead.bend, the
3# shape of RFC 5116): AEGIS-128 (aegis128.bend), encrypt-then-MAC over any
4# cipher and any MAC (authenc.bend), and the IV generators ESSIV
5# (essiv.bend), seqiv (seqiv.bend) and echainiv (echainiv.bend), which turn
6# one AEAD (or, for ESSIV, one cipher with an IV) into another.
7#
8# This file holds what they share: a ciphertext with its tag appended, and
9# split again. Bend imports do not re-export: import the files you use.
10import Base
11import bend-osdev-bytes@0.1.0.0/bytes.bend as B
12import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
13
14# A ciphertext and its tag, split from the bytes of both (the tag the last
15# tlen bytes; CrTooShort for fewer than tlen bytes)
16type AdSplit is Data:
17  AdSplit{c: B.Octets, t: B.Octets}
18
19def ad.split.pick(short: Bool, +tlen: Nat, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdSplit>:
20  match short:
21    case True{}:
22      Fail{Cr.CrTooShort{B.Octets.len(o)}}
23    case False{}:
24      +n = Nat.sub(B.Octets.len(o), tlen)
25      Done{AdSplit{B.Octets.take(n, o), B.Octets.drop(n, o)}}
26
27def AdTag.split(+tlen: Nat, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdSplit>:
28  ad.split.pick(Nat.is_lt(B.Octets.len(o), tlen), tlen, o)
29
30# the ciphertext with its tag appended
31def AdTag.join(c: B.Octets, t: B.Octets) -> B.Octets:
32  B.Octets.append(c, t)
33
34# Whether two tags are equal, every byte compared (no early exit)
35def AdTag.is_eq(a: B.Octets, b: B.Octets) -> Bool:
36  B.Octets.is_eq(a, b)