~/jendhub

def au_tag_len

bend-osdev-aead@0.1.0.0 · PROOF.bend:224

import bend-osdev-aead@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-aead@0.1.0.0/authenc.bend as Au

224# every tag has tlen bytes
225def au_tag_len(~KE: Data, ~KM: Data, ~mac: KM -> B.Octets -> B.Octets, ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets, ~tlen: Nat, k: Au.AdAuthencKey<KE, KM>, +aad: B.Octets, +iv: B.Octets, +c: B.Octets) -> {B.Octets.len(Au.AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, k, aad, iv, c)) == tlen : Nat}:
226  match k:
227    case Au.AdAuthencKey{ke, +km}:
228      %olen_of(Au.ad.au.fit(tlen, B.Octets.to_list(mac(km, input(aad, iv, c))))) : {_ == tlen : Nat}
229      fit_len(tlen, B.Octets.to_list(mac(km, input(aad, iv, c))))

Uses (9)

Used by (1)