MAC

In-circuit verification of a message authentication code over GF(2^128) on a 256-bit hidden message. The construction is a polynomial MAC whose key is split additively between the prover (committed as witness) and the verifier (sampled fresh per batch), giving classical universal-hash soundness of 2^-128 per invocation. If you are building for TPM2 or Intel TDX attestation you likely will not reach for this gadget directly — MAC is used in mdoc device authentication, not in attestation flows — but it remains the clearest worked example in the library of why a binary ambient field beats a prime one when the statement you are proving is bitwise in nature.

Construction

Here x[0] and x[1] are the two 128-bit halves of a 256-bit message, a_p[0] and a_p[1] are the prover’s key components (committed as part of the private witness, one per half), and a_v is a single 128-bit value sampled fresh by the verifier for the whole batch. All arithmetic is in GF(2^128): the + is XOR and the · is binary-field multiplication. The soundness argument is standard: fix any prover-chosen a_p and x; for y != x, the probability over the verifier’s coin flip a_v that mac(x) = mac(y) is at most 2^-128. An adversary who has not seen a_v ahead of time forges with the same probability.

When to reach for it

• Your statement’s soundness can lean on a MAC rather than a full signature — MAC verification is dramatically cheaper per invocation than ECDSA.
• You want a worked example of a binary-field gadget to read before writing your own.
• You are working in the mdoc case study, where this MAC gates device authentication.

Why GF(2^128)?

The MAC formula leans on exactly two field operations, and both are binary-native. Addition in GF(2^k) is bitwise XOR — literally the same circuit gate — and multiplication in GF(2^128) is a well-studied primitive that Longfellow exposes as a single call (gf2_128_mul) built on top of vxor. In a binary ambient field, (a_p + a_v) · x compiles to one XOR of two 128-bit words plus one binary-field multiply. That is it. No bit-decomposition, no carry chains, no reassembly.

Now imagine the same formula in a prime-field ambient world, say Fp256Base. XOR over 128-bit operands is not free there: you must first bit-decompose both operands (that is 256 bit-constraints before you even touch the XOR), perform the XOR bitwise, and then reassemble the result — so one “free” operation in GF(2^128) becomes hundreds of constraints. Multiplication is worse: a GF(2^128) multiply emulated in a prime field requires a carry-chain over packed limbs with further bit-level checks, multiplying constraint counts yet again. Per MAC invocation the overhead runs into the thousands of constraints, none of which do any useful work — they exist solely to paper over the field mismatch. Longfellow still makes this case work through the bit-packed MacWitness<Field> path (the 256 message bits plus each 128-bit a_p[i] are committed as bit-packed witness and lifted through a BitPlucker), but you pay for the mismatch.

If the rest of your circuit is already over GF(2^128) — or can be, using the Ligero-over-GF backend — the MAC gadget becomes essentially free, and the specialized MACGF2 path drops the bit-packing entirely: the message is a native field element, and only the prover’s key is committed. If your ambient field has to be a prime (for example because you also need ECDSA in the same proof, which wants Fp256Base), you use the generic MAC<Logic, BitPlucker> path and accept the tax. The takeaway for your own gadget design: field choice is design-shaped, not a detail. A binary-native statement wants a binary ambient field, and picking wrong costs you at every invocation.

API surface

In-circuit

MAC<Logic, BitPlucker> — generic path usable over any field at least 256 bits wide. Constructed as MAC(const Logic& lc). Entry point:

void verify_mac(EltW msg, const v128 mac[2], const v128& av,
                const Witness& vw, Nat order) const;

The inner Witness class has void input(const Logic& lc) which pulls a_p[0], a_p[1], and the 256 bits of x from the private tape, all bit-packed through the BitPlucker. The order argument bounds x so the reassembled element cannot overflow the ambient field. A companion MACGF2<Backend, BitPlucker> specializes the construction for an ambient GF(2^128) and only commits a_p as witness. Note that MACGF2 still accepts the BitPlucker template parameter for API consistency, but does not use it internally — in the GF(2^128) path the 128-bit message halves are packed directly as native field elements rather than through a BitPlucker.

Host-side witness

Two builders in mac_witness.h:

• MacWitness<Field>::compute_witness(const gf2k a_p[2], const uint8_t x[32]) — for when the ambient circuit field is not GF(2^128). Packs the key and the 256 message bits into Field elements for the BitPlucker to consume.
• MacGF2Witness::compute_witness(const gf2k a_p[2]) — for when the ambient field is GF(2^128). The 256-bit message is handed to the circuit as native inputs, so only a_p needs to be committed.

For test oracles, MACReference<GF>::compute(gf2k mac[2], const gf2k& av, const gf2k ap[2], uint8_t msg[32]) evaluates the naive host-side formula, used to precompute expected tags.

Example

const CompilerBackend cbk(&Q);
const Logic<Field, CompilerBackend> L(&cbk, F);
MAC<Logic, BitPlucker> mac(L);
 
EltW msg = L.eltw_input();            // one message element
v128 mac_tag[2] = { L.vinput<128>(), L.vinput<128>() };
v128 av = L.vinput<128>();            // verifier-contributed key
MAC::Witness vwc; vwc.input(L);
 
mac.verify_mac(msg, mac_tag, av, vwc, n256_order);

See it used

• mac_circuit_test.cc — batched three-message test over Fp256Base; the adjacent full_circuit_GF2_128 test runs the same construction with GF(2^128) as the ambient field and is worth diffing against to see the constraint-count difference.
• mac_reference.h — the naive host-side oracle used to precompute expected MAC tags for tests.

Related

• Binary Fields (GF(2^k)) — the ambient-field choice that makes this gadget cheap.
• Logic — source of vxor and gf2_128_mul.