1 # Encrypt-then-MAC: an AEAD from any cipher with an IV and any MAC, as the 2 # Linux kernel's "authenc(mac, cipher)" composes them (for example 3 # authenc(hmac(sha256), cbc(aes)) for IPsec) and as D. McGrew, J. Foley, K. 4 # Paterson, "Authenticated Encryption with AES-CBC and HMAC-SHA" 5 # (draft-mcgrew-aead-aes-cbc-hmac-sha2-05, 2014) specifies it: 6 # C = Enc(K_E, IV, P), T = the first tlen bytes of MAC(K_M, input), 7 # the AEAD's ciphertext C || T 8 # Opening checks T before decrypting anything, and releases nothing when it 9 # differs. What the MAC covers is a parameter (~input, from the associated 10 # data A, the IV and C), with two named defaults: 11 # AdAuthenc.input_kernel A || C (the kernel's authenc: an IV to be 12 # authenticated is part of A, as ESP does) 13 # AdAuthenc.input_mcgrew A || IV || C || AL, AL the bit length of A as a 14 # 64-bit big-endian number (the draft's section 15 # 2.1, with S = IV || C) 16 # A MAC shorter than tlen is zero-padded, so every tag has tlen bytes. 17 # 18 # The cipher (template arguments ~KE, ~ekey, ~enc, ~dec) takes a key 19 # schedule, an IV and bytes; ivcipher.bend makes one of any block cipher in 20 # CBC, with or without PKCS #7 padding. The MAC is the crypto package's MAC 21 # interface (~KM, ~mkey, ~mac). The key is the two keys (AdAuthencKey); a raw 22 # key is the MAC key then the cipher key, as both the kernel (after its 23 # length header) and the draft lay it out. 24 # 25 # Laws (LAWS.bend): open accepts what seal produced, wherever the cipher's 26 # decryption undoes its encryption (authenc_round_trip_if); and any tag but 27 # the one the MAC computes is refused (authenc_tamper). 28 import Base 29 import bend-osdev-bytes@0.1.0.0/bytes.bend as B 30 import bend-osdev-word64@0.1.0.0/word64.bend as W 31 import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr 32 import ./aead.bend as Ad 33 34 # The two keys 35 type AdAuthencKey<-KE: Data, -KM: Data> is Data: 36 AdAuthencKey{ke: KE, km: KM} 37 38 # The named MAC inputs 39 40 def AdAuthenc.input_kernel(aad: B.Octets, iv: B.Octets, c: B.Octets) -> B.Octets: 41 B.Octets.append(aad, c) 42 43 def ad.au.mcgrew(+aad: B.Octets, iv: B.Octets, c: B.Octets) -> B.Octets: 44 B.Octets.append(aad, B.Octets.append(iv, B.Octets.append(c, B.Octets.of_list(B.be64(W.W64.shl(W.W64.from_nat(B.Octets.len(aad)), 3n)))))) 45 46 def AdAuthenc.input_mcgrew(aad: B.Octets, iv: B.Octets, c: B.Octets) -> B.Octets: 47 ad.au.mcgrew(aad, iv, c) 48 49 # the first n bytes of xs, zero-padded to n 50 def ad.au.fit(n: Nat, xs: List<&2, U32>) -> List<&2, U32>: 51 match n: 52 case 0n: 53 Nil{} 54 case 1n+m: 55 match xs: 56 case Nil{}: 57 Con{0, ad.au.fit(m, Nil{})} 58 case Con{h, t}: 59 Con{h, ad.au.fit(m, t)} 60 61 # The tag of the ciphertext c: the MAC's first tlen bytes (zero-padded) 62 def AdAuthenc.tag(~KE: Data, ~KM: Data, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, k: AdAuthencKey, aad: B.Octets, iv: B.Octets, c: B.Octets) -> B.Octets: 63 match k: 64 case AdAuthencKey{ke, km}: 65 B.Octets.of_list(ad.au.fit(tlen, B.Octets.to_list(mac(km, input(aad, iv, c))))) 66 67 def ad.au.sealed(~KE: Data, ~KM: Data, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, +k: AdAuthencKey, +aad: B.Octets, +iv: B.Octets, +c: B.Octets) -> B.Octets: 68 Ad.AdTag.join(c, AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, k, aad, iv, c)) 69 70 def ad.au.ke(~KE: Data, ~KM: Data, k: AdAuthencKey) -> KE: 71 match k: 72 case AdAuthencKey{ke, km}: 73 ke 74 75 def ad.au.seal(~KE: Data, ~KM: Data, ~enc: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, +k: AdAuthencKey, +iv: B.Octets, +aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>: 76 Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => ad.au.sealed(~KE, ~KM, ~mac, ~input, ~tlen, k, aad, iv, c), enc(ad.au.ke(~KE, ~KM, k), iv, p)) 77 78 # p sealed under the IV: C || T 79 def AdAuthenc.seal(~KE: Data, ~KM: Data, ~enc: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, k: AdAuthencKey, iv: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>: 80 ad.au.seal(~KE, ~KM, ~enc, ~mac, ~input, ~tlen, k, iv, aad, p) 81 82 def ad.au.check(ok: Bool) -> Result<&2, &2, Cr.CrError, Unit>: 83 Cr.CrError.check(ok, Cr.CrTagMismatch{}) 84 85 def ad.au.open.go(~KE: Data, ~KM: Data, ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, +k: AdAuthencKey, +iv: B.Octets, +aad: B.Octets, s: Ad.AdSplit) -> Result<&2, &2, Cr.CrError, B.Octets>: 86 match s: 87 case Ad.AdSplit{+c, t}: 88 Result.bind(&2, &2, Cr.CrError, Unit, B.Octets, ad.au.check(Ad.AdTag.is_eq(AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, k, aad, iv, c), t)), u => dec(ad.au.ke(~KE, ~KM, k), iv, c)) 89 90 def ad.au.open(~KE: Data, ~KM: Data, ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, +k: AdAuthencKey, +iv: B.Octets, +aad: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>: 91 Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(tlen, c), s => ad.au.open.go(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, k, iv, aad, s)) 92 93 # C || T opened: P, or CrTagMismatch (the cipher is not run), CrTooShort 94 def AdAuthenc.open(~KE: Data, ~KM: Data, ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, k: AdAuthencKey, iv: B.Octets, aad: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>: 95 ad.au.open(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, k, iv, aad, c) 96 97 # The key from the two raw keys 98 def AdAuthenc.key_of(~KE: Data, ~KM: Data, ~ekey: B.Octets -> Result<&2, &2, Cr.CrError, KE>, ~mkey: B.Octets -> Result<&2, &2, Cr.CrError, KM>, eo: B.Octets, mo: B.Octets) -> Result<&2, &2, Cr.CrError, AdAuthencKey>: 99 do Result<&2, &2, Cr.CrError, AdAuthencKey>: 100 ke : KE <- ekey(eo) 101 km : KM <- mkey(mo) 102 return AdAuthencKey{ke, km} 103 104 def ad.au.key(~KE: Data, ~KM: Data, ~ekey: B.Octets -> Result<&2, &2, Cr.CrError, KE>, ~mkey: B.Octets -> Result<&2, &2, Cr.CrError, KM>, +elen: Nat, +o: B.Octets) -> Result<&2, &2, Cr.CrError, AdAuthencKey>: 105 +n = B.Octets.len(o) 106 +m = Nat.sub(n, elen) 107 Result.bind(&2, &2, Cr.CrError, Unit, AdAuthencKey, Cr.CrError.check(Nat.is_le(elen, n), Cr.CrBadKeyLength{n}), u => AdAuthenc.key_of(~KE, ~KM, ~ekey, ~mkey, B.Octets.drop(m, o), B.Octets.take(m, o))) 108 109 # The key from one raw key: the MAC key, then the cipher key of elen bytes 110 # (CrBadKeyLength for fewer than elen bytes, or a key either refuses) 111 def AdAuthenc.key(~KE: Data, ~KM: Data, ~ekey: B.Octets -> Result<&2, &2, Cr.CrError, KE>, ~mkey: B.Octets -> Result<&2, &2, Cr.CrError, KM>, ~elen: Nat, o: B.Octets) -> Result<&2, &2, Cr.CrError, AdAuthencKey>: 112 ad.au.key(~KE, ~KM, ~ekey, ~mkey, elen, o)