echainiv.bend

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

1# echainiv, "encrypted chain IV": an AEAD whose nonce is a sequence number
2# encrypted under a block cipher, sent in front of the ciphertext (the Linux
3# kernel's "echainiv(aead)", for IPsec with CBC-based AEADs, where an IV
4# must be unpredictable as well as unique). The IV is generated as NIST SP
5# 800-38A, Appendix C, recommends for CBC ("apply the forward cipher
6# function, under the same key that is used for the encryption of the
7# plaintext, to a nonce", here a nonce made from the sequence number and a
8# secret salt, as in seqiv.bend):
9#   IV = E(Kc, salt xor (0 .. 0 || seq)),  sealed: IV || AEAD.seal(K, IV, A || IV, P)
10#   opened: the first ivlen bytes are the IV, AEAD.open(K, IV, A || IV, the rest)
11# The IV is part of the AEAD's associated data, so it is authenticated even
12# under an AEAD that does not bind its nonce (as seqiv.bend).
13# Kc is the key schedule of a block cipher of the crypto package's
14# interface (for authenc(hmac(..), cbc(aes)), AES under the AEAD's cipher
15# key), and the salt one block. The kernel's echainiv draws its salt at
16# random and chains through earlier IVs, so its IVs differ from these, but a
17# receiver reads the IV from the packet, and the two interoperate.
18#
19# Over any AEAD with an ivlen-byte nonce. Laws (LAWS.bend): open accepts what
20# seal produced wherever the AEAD's does, at the generated IV
21# (echainiv_round_trip_if).
22import Base
23import bend-osdev-bytes@0.1.0.0/bytes.bend as B
24import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
25import bend-osdev-crypto@0.1.0.0/octets.bend as O
26
27# The key: the AEAD's key, the IV cipher's key schedule, and the salt
28type AdEchainivKey<-KA: Data, -KC: Data> is Data:
29  AdEchainivKey{ka: KA, kc: KC, salt: B.Octets}
30
31def ad.ec.ka(~KA: Data, ~KC: Data, k: AdEchainivKey<KA, KC>) -> KA:
32  match k:
33    case AdEchainivKey{ka, kc, salt}:
34      ka
35
36def ad.ec.e(~KC: Data, ~Blk: Data, ~enc: KC -> Blk -> Blk, ~blk_to: Blk -> B.Octets, +kc: KC, x: Maybe<&2, Blk>, +o: B.Octets) -> B.Octets:
37  match x:
38    case None{}:
39      o
40    case Some{b}:
41      blk_to(enc(kc, b))
42
43# The IV of sequence number seq: E(Kc, salt xor seq right-aligned)
44def AdEchainiv.iv(~KA: Data, ~KC: Data, ~Blk: Data, ~enc: KC -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, k: AdEchainivKey<KA, KC>, +seq: B.Octets) -> B.Octets:
45  match k:
46    case AdEchainivKey{ka, +kc, +salt}:
47      +x = O.CrOct.xor(salt, B.Octets.append(B.Octets.zeros(Nat.sub(B.Octets.len(salt), B.Octets.len(seq))), seq))
48      ad.ec.e(~KC, ~Blk, ~enc, ~blk_to, kc, blk_of(x), x)
49
50# The key from the AEAD's raw key, the IV cipher's raw key and the salt
51def AdEchainiv.key(~KA: Data, ~KC: Data, ~akey: B.Octets -> Result<&2, &2, Cr.CrError, KA>, ~ckey: B.Octets -> Result<&2, &2, Cr.CrError, KC>, ao: B.Octets, co: B.Octets, salt: B.Octets) -> Result<&2, &2, Cr.CrError, AdEchainivKey<KA, KC>>:
52  do Result<&2, &2, Cr.CrError, AdEchainivKey<KA, KC>>:
53    ka : KA <- akey(ao)
54    kc : KC <- ckey(co)
55    return AdEchainivKey{ka, kc, salt}
56
57def ad.ec.seal(~KA: Data, ~KC: Data, ~Blk: Data, ~enc: KC -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~seal: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: AdEchainivKey<KA, KC>, +seq: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
58  +iv = AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, k, seq)
59  Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => B.Octets.append(iv, c), seal(ad.ec.ka(~KA, ~KC, k), iv, B.Octets.append(aad, iv), p))
60
61# p sealed under the sequence number seq: IV || the AEAD's ciphertext
62def AdEchainiv.seal(~KA: Data, ~KC: Data, ~Blk: Data, ~enc: KC -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~seal: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, k: AdEchainivKey<KA, KC>, seq: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
63  ad.ec.seal(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, ~seal, k, seq, aad, p)
64
65def ad.ec.open.go(~KA: Data, ~KC: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: AdEchainivKey<KA, KC>, aad: B.Octets, +n: Nat, s: Maybe<&2, B.OctetsSplit>) -> Result<&2, &2, Cr.CrError, B.Octets>:
66  match s:
67    case None{}:
68      Fail{Cr.CrTooShort{n}}
69    case Some{B.OctetsSplit{+iv, c}}:
70      open(ad.ec.ka(~KA, ~KC, k), iv, B.Octets.append(aad, iv), c)
71
72def ad.ec.open(~KA: Data, ~KC: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~ivlen: Nat, +k: AdEchainivKey<KA, KC>, seq: B.Octets, aad: B.Octets, +c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
73  ad.ec.open.go(~KA, ~KC, ~open, k, aad, B.Octets.len(c), B.Octets.split_at(ivlen, c))
74
75# IV || C opened: the AEAD's open of C under the first ivlen bytes and
76# A || IV, or CrTooShort
77def AdEchainiv.open(~KA: Data, ~KC: Data, ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~ivlen: Nat, k: AdEchainivKey<KA, KC>, seq: B.Octets, aad: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
78  ad.ec.open(~KA, ~KC, ~open, ~ivlen, k, seq, aad, c)