authenc.bend

bend-osdev-aead@0.1.0.0 · 112 lines · 17 definitions

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).
28import Base
29import bend-osdev-bytes@0.1.0.0/bytes.bend as B
30import bend-osdev-word64@0.1.0.0/word64.bend as W
31import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
32import bend-osdev-aead@0.1.0.0/aead.bend as Ad
33
34# The two keys
35type AdAuthencKey<-KE: Data, -KM: Data> is Data:
36  AdAuthencKey{ke: KE, km: KM}
37
38# The named MAC inputs
39
40def AdAuthenc.input_kernel(aad: B.Octets, iv: B.Octets, c: B.Octets) -> B.Octets:
41  B.Octets.append(aad, c)
42
43def 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
46def 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
50def 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)
62def 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<KE, KM>, 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
67def 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<KE, KM>, +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
70def ad.au.ke(~KE: Data, ~KM: Data, k: AdAuthencKey<KE, KM>) -> KE:
71  match k:
72    case AdAuthencKey{ke, km}:
73      ke
74
75def 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<KE, KM>, +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
79def 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<KE, KM>, 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
82def ad.au.check(ok: Bool) -> Result<&2, &2, Cr.CrError, Unit>:
83  Cr.CrError.check(ok, Cr.CrTagMismatch{})
84
85def 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<KE, KM>, +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
90def 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<KE, KM>, +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
94def 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<KE, KM>, 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
98def 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<KE, KM>>:
99  do Result<&2, &2, Cr.CrError, AdAuthencKey<KE, KM>>:
100    ke : KE <- ekey(eo)
101    km : KM <- mkey(mo)
102    return AdAuthencKey{ke, km}
103
104def 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<KE, KM>>:
105  +n = B.Octets.len(o)
106  +m = Nat.sub(n, elen)
107  Result.bind(&2, &2, Cr.CrError, Unit, AdAuthencKey<KE, KM>, 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)
111def 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<KE, KM>>:
112  ad.au.key(~KE, ~KM, ~ekey, ~mkey, elen, o)