essiv.bend

bend-osdev-aead@0.1.0.0 · 83 lines · 15 definitions

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).
17import Base
18import bend-osdev-bytes@0.1.0.0/bytes.bend as B
19import 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
22type AdEssivKey<-KD: Data, -KS: Data> is Data:
23  AdEssivKey{kd: KD, ks: KS}
24
25def 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
32def 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)
38def 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
41def ad.es.kd(~KD: Data, ~KS: Data, k: AdEssivKey<KD, KS>) -> KD:
42  match k:
43    case AdEssivKey{kd, ks}:
44      kd
45
46def 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)
54def 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
59def 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
62def 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
65def 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
68def 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
73def 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
76def 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
79def 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
82def 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)