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).
22	import Base
23	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
24	import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
25	import 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
28	type AdEchainivKey<-KA: Data, -KC: Data> is Data:
29	  AdEchainivKey{ka: KA, kc: KC, salt: B.Octets}
30	
31	def ad.ec.ka(~KA: Data, ~KC: Data, k: AdEchainivKey<KA, KC>) -> KA:
32	  match k:
33	    case AdEchainivKey{ka, kc, salt}:
34	      ka
35	
36	def 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)
44	def 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
51	def 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	
57	def 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
62	def 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	
65	def 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	
72	def 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
77	def 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)