seqiv.bend

bend-osdev-aead@0.1.0.0 · 79 lines · 10 definitions

1# seqiv: an AEAD whose nonce is made from a sequence number, sent in front
2# of the ciphertext (the Linux kernel's "seqiv(aead)", as IPsec ESP uses
3# it with GCM and CCM). The sender keeps a counter (the packet's sequence
4# number); the nonce is the counter, right-aligned in the nonce's length and
5# XORed with a secret salt from the key material, as RFC 8446 (TLS 1.3),
6# section 5.3, forms its per-record nonce, and as RFC 5116, section 3.2,
7# recommends (a counter, so that no nonce repeats under one key). The nonce
8# travels with the ciphertext, as ESP's explicit IV does, so the receiver
9# needs no counter:
10#   IV = salt xor (0 .. 0 || seq),  sealed: IV || AEAD.seal(K, IV, A || IV, P)
11#   opened: the first ivlen bytes are the IV, AEAD.open(K, IV, A || IV, the rest)
12# The IV is part of the AEAD's associated data, so it is authenticated even
13# under an AEAD that does not bind its nonce (Encrypt-then-MAC over A || C,
14# authenc.bend's kernel layout), as ESP authenticates its IV (RFC 4303,
15# section 3.3.2.1, with the IV part of the payload the ICV covers).
16# The salt is the last ivlen bytes of the raw key (as RFC 4106's GCM in ESP
17# takes its salt from the end of the key material); the kernel's seqiv draws
18# its salt at random, so its IVs differ from these, but a receiver reads the
19# IV from the packet, and the two interoperate.
20#
21# Over any AEAD of the crypto package's AEAD interface (~KA, ~akey, ~seal,
22# ~open) with an ivlen-byte nonce. Laws (LAWS.bend): open accepts what seal
23# produced wherever the AEAD's open accepts what its seal produced, at the
24# generated IV (seqiv_round_trip_if).
25import Base
26import bend-osdev-bytes@0.1.0.0/bytes.bend as B
27import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
28import bend-osdev-crypto@0.1.0.0/octets.bend as O
29
30# The key: the AEAD's key and the salt
31type AdSeqivKey<-KA: Data> is Data:
32  AdSeqivKey{ka: KA, salt: B.Octets}
33
34def ad.sq.ka(~KA: Data, k: AdSeqivKey<KA>) -> KA:
35  match k:
36    case AdSeqivKey{ka, salt}:
37      ka
38
39# The IV of sequence number seq (big-endian bytes, at most as long as the
40# salt): the salt XOR seq, right-aligned
41def AdSeqiv.iv(~KA: Data, k: AdSeqivKey<KA>, +seq: B.Octets) -> B.Octets:
42  match k:
43    case AdSeqivKey{ka, +salt}:
44      O.CrOct.xor(salt, B.Octets.append(B.Octets.zeros(Nat.sub(B.Octets.len(salt), B.Octets.len(seq))), seq))
45
46def ad.sq.key(~KA: Data, ~akey: B.Octets -> Result<&2, &2, Cr.CrError, KA>, +ivlen: Nat, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdSeqivKey<KA>>:
47  +n = B.Octets.len(o)
48  +m = Nat.sub(n, ivlen)
49  do Result<&2, &2, Cr.CrError, AdSeqivKey<KA>>:
50    Cr.CrError.check(Nat.is_le(ivlen, n), Cr.CrBadKeyLength{n})
51    ka : KA <- akey(B.Octets.take(m, o))
52    return AdSeqivKey{ka, B.Octets.drop(m, o)}
53
54# The key from raw key material: the AEAD's key, then an ivlen-byte salt
55def AdSeqiv.key(~KA: Data, ~akey: B.Octets -> Result<&2, &2, Cr.CrError, KA>, ~ivlen: Nat, o: B.Octets) -> Result<&2, &2, Cr.CrError, AdSeqivKey<KA>>:
56  ad.sq.key(~KA, ~akey, ivlen, o)
57
58def ad.sq.seal(~KA: Data, ~seal: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: AdSeqivKey<KA>, +seq: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
59  +iv = AdSeqiv.iv(~KA, k, seq)
60  Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), seal(ad.sq.ka(~KA, k), iv, B.Octets.append(aad, iv), p))
61
62# p sealed under the sequence number seq: IV || the AEAD's ciphertext
63def AdSeqiv.seal(~KA: Data, ~seal: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, k: AdSeqivKey<KA>, seq: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
64  ad.sq.seal(~KA, ~seal, k, seq, aad, p)
65
66def ad.sq.open.go(~KA: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: AdSeqivKey<KA>, aad: B.Octets, +n: Nat, s: Maybe<&2, B.OctetsSplit>) -> Result<&2, &2, Cr.CrError, B.Octets>:
67  match s:
68    case None{}:
69      Fail{Cr.CrTooShort{n}}
70    case Some{B.OctetsSplit{+iv, c}}:
71      open(ad.sq.ka(~KA, k), iv, B.Octets.append(aad, iv), c)
72
73# IV || C opened (the IV the first ivlen bytes; the sequence number is not
74# needed): the AEAD's open of C under that IV and A || IV, or CrTooShort
75def ad.sq.open(~KA: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~ivlen: Nat, +k: AdSeqivKey<KA>, seq: B.Octets, aad: B.Octets, +c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
76  ad.sq.open.go(~KA, ~open, k, aad, B.Octets.len(c), B.Octets.split_at(ivlen, c))
77
78def AdSeqiv.open(~KA: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~ivlen: Nat, k: AdSeqivKey<KA>, seq: B.Octets, aad: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
79  ad.sq.open(~KA, ~open, ~ivlen, k, seq, aad, c)