1	# ESSIV, "encrypted salt-sector initialization vector" (C. Fruhwirth, "New
2	# Methods in Hard Disk Encryption", 2005, section 4.2; the Linux kernel's
3	# "essiv(cipher, hash)", as dm-crypt and fscrypt use it): the IV of a sector
4	# is the sector's number encrypted under a key derived from the data key,
5	#   salt = H(K),  IV' = E(salt, IV)
6	# where H is any hash of the crypto package's hash interface (~digest) and E
7	# any block cipher of its block-cipher interface (the "salt cipher", whose
8	# key is the digest: SHA-256 and AES-256 in dm-crypt's aes-cbc-essiv:sha256).
9	#
10	# Two forms, both taking the data key K whole:
11	#   * over a cipher with an IV (ivcipher.bend: CBC): AdEssiv.encrypt and
12	#     AdEssiv.decrypt run it under IV';
13	#   * over an AEAD (crypto's AEAD interface, the kernel's essiv(authenc(..)))
14	#     AdEssiv.seal and AdEssiv.open run it under the nonce IV'.
15	# Laws (LAWS.bend): each undoes itself wherever what it wraps does, at the
16	# derived IV (essiv_round_trip_if, essiv_aead_round_trip_if).
17	import Base
18	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
19	import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
20	
21	# The key: the wrapped algorithm's key, and the salt cipher's key schedule
22	type AdEssivKey<-KD: Data, -KS: Data> is Data:
23	  AdEssivKey{kd: KD, ks: KS}
24	
25	def ad.es.e(~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_to: Blk -> B.Octets, +ks: KS, x: Maybe<&2, Blk>, +iv: B.Octets) -> B.Octets:
26	  match x:
27	    case None{}:
28	      iv
29	    case Some{b}:
30	      blk_to(enc(ks, b))
31	
32	def ad.es.iv(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, k: AdEssivKey<KD, KS>, +iv: B.Octets) -> B.Octets:
33	  match k:
34	    case AdEssivKey{kd, +ks}:
35	      ad.es.e(~KS, ~Blk, ~enc, ~blk_to, ks, blk_of(iv), iv)
36	
37	# IV' = E(salt, IV) (an IV the salt cipher's format refuses is used as it is)
38	def AdEssiv.iv(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, k: AdEssivKey<KD, KS>, +iv: B.Octets) -> B.Octets:
39	  ad.es.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, k, iv)
40	
41	def ad.es.kd(~KD: Data, ~KS: Data, k: AdEssivKey<KD, KS>) -> KD:
42	  match k:
43	    case AdEssivKey{kd, ks}:
44	      kd
45	
46	def ad.es.key(~KD: Data, ~KS: Data, ~dkey: B.Octets -> Result<&2, &2, Cr.CrError, KD>, ~skey: B.Octets -> Result<&2, &2, Cr.CrError, KS>, ~digest: B.Octets -> B.Octets, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdEssivKey<KD, KS>>:
47	  do Result<&2, &2, Cr.CrError, AdEssivKey<KD, KS>>:
48	    kd : KD <- dkey(o)
49	    ks : KS <- skey(digest(o))
50	    return AdEssivKey{kd, ks}
51	
52	# The key from the data key K: the wrapped algorithm's key of K, and the
53	# salt cipher's key of H(K)
54	def AdEssiv.key(~KD: Data, ~KS: Data, ~dkey: B.Octets -> Result<&2, &2, Cr.CrError, KD>, ~skey: B.Octets -> Result<&2, &2, Cr.CrError, KS>, ~digest: B.Octets -> B.Octets, o: B.Octets) -> Result<&2, &2, Cr.CrError, AdEssivKey<KD, KS>>:
55	  ad.es.key(~KD, ~KS, ~dkey, ~skey, ~digest, o)
56	
57	# Over a cipher with an IV (~cenc, ~cdec: key schedule, IV, bytes)
58	
59	def ad.es.encrypt(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~cenc: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: AdEssivKey<KD, KS>, +iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
60	  cenc(ad.es.kd(~KD, ~KS, k), AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, k, iv), m)
61	
62	def AdEssiv.encrypt(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~cenc: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, k: AdEssivKey<KD, KS>, iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
63	  ad.es.encrypt(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~cenc, k, iv, m)
64	
65	def ad.es.decrypt(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~cdec: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: AdEssivKey<KD, KS>, +iv: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
66	  cdec(ad.es.kd(~KD, ~KS, k), AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, k, iv), c)
67	
68	def AdEssiv.decrypt(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~cdec: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, k: AdEssivKey<KD, KS>, iv: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
69	  ad.es.decrypt(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~cdec, k, iv, c)
70	
71	# Over an AEAD (~seal, ~open: key, nonce, associated data, bytes)
72	
73	def ad.es.seal(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~seal: KD -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: AdEssivKey<KD, KS>, +iv: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
74	  seal(ad.es.kd(~KD, ~KS, k), AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, k, iv), aad, p)
75	
76	def AdEssiv.seal(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~seal: KD -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, k: AdEssivKey<KD, KS>, iv: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
77	  ad.es.seal(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~seal, k, iv, aad, p)
78	
79	def ad.es.open(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~open: KD -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, +k: AdEssivKey<KD, KS>, +iv: B.Octets, aad: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
80	  open(ad.es.kd(~KD, ~KS, k), AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, k, iv), aad, c)
81	
82	def AdEssiv.open(~KD: Data, ~KS: Data, ~Blk: Data, ~enc: KS -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, ~open: KD -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, k: AdEssivKey<KD, KS>, iv: B.Octets, aad: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
83	  ad.es.open(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~open, k, iv, aad, c)