Bijection-Family MAC: Optimal Information-Theoretic Unforgeability #

A message-authentication code built from a bijection family achieves the information-theoretically optimal forgery probability 1 / |Tag|. Following Rosulek, The Joy of Cryptography, §9 (MACs).

For each message m, if the map k ↦ mac k m is a bijection from keys to tags, then over a uniform key the tag mac k m is uniform on the tag space. A fixed forgery attempt (m*, t*) therefore verifies for exactly one key, so the single-query EUF-CMA game accepts the forgery with probability exactly 1 / |Tag| — the smallest a forger can be forced below by an honest random tag, and the best any |Tag|-tag MAC can achieve against a blind guess.

Overview #

This mirrors the bijection-coupling examples (CatCrypt.Examples.OTP, CatCrypt.Examples.PRF). Where those collapse a distinguishing advantage to 0, a MAC's forgery probability is not 0 (a forger may always guess a tag); the sharp statement is that it equals 1 / |Tag|. The forgery probability is a prTrue of the real game, computed by prTrue_sample_pure_bool: it counts the keys under which the forgery verifies, divided by |Key|. The bijection makes that count exactly 1, and |Key| = |Tag| since bij m* is an equivalence.

Main definitions #

BijMACFamily — a family of key→tag bijections indexed by message.
BijMACFamily.toMACScheme — the core MACScheme it induces (mac k m = bij m k).
boolXorMAC — the XOR MAC over Bool (mac k m = k ⊕ m), the MAC counterpart of the one-time pad.

Main results #

bijMAC_forgery_prob — the single-query EUF-CMA forgery probability of a bijection-family MAC is exactly 1 / |Tag|.
bijMAC_euf_cma_adv — the same, phrased through the core EUF_CMA_Adv game with the identity (no-post-processing) forger.
boolXorMAC_forgery_prob — the Bool XOR MAC has forgery probability 1 / 2.

References #

[Rosulek, The Joy of Cryptography, §9 (MACs)]
[Wegman & Carter, New hash functions and their use in authentication, 1981]

Bijection-Family MAC #

source

structure CatCrypt.Examples.MAC.BijMACFamily :

Type 1

A MAC given by a family of bijections bij m : Key ≃ Tag, one per message.

For a uniform key, bij m maps the uniform key distribution onto the uniform tag distribution, which forces the forgery probability down to 1 / |Tag|.

Key : Type
Key type
Message : Type
Message type
Tag : Type
Tag type
finKey : Fintype self.Key
neKey : Nonempty self.Key
finTag : Fintype self.Tag
neTag : Nonempty self.Tag
decTag : DecidableEq self.Tag
bij : self.Message → self.Key ≃ self.Tag
For each message, a bijection from keys to tags

Instances For

source

def CatCrypt.Examples.MAC.BijMACFamily.toMACScheme (B : BijMACFamily) :

Crypto.SecurityDefs.MACScheme

The core MACScheme induced by a bijection family: mac k m = bij m k, verification recomputing and comparing (the MACScheme default).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CatCrypt.Examples.MAC.toMACScheme_mac (B : BijMACFamily) (k : B.Key) (m : B.Message) :

B.toMACScheme.mac k m = (B.bij m) k

source

@[simp]

theorem CatCrypt.Examples.MAC.toMACScheme_verify (B : BijMACFamily) (k : B.Key) (m : B.Message) (t : B.Tag) :

B.toMACScheme.verify k m t = (t == (B.bij m) k)

Forgery Probability #

source

theorem CatCrypt.Examples.MAC.bijMAC_forgery_filter (B : BijMACFamily) (m_star : B.Message) (t_star : B.Tag) :

{k : B.Key | B.toMACScheme.verify k m_star t_star = true}.card = 1

A fixed forgery attempt (m*, t*) verifies under exactly one key: the map k ↦ bij m* k is a bijection, so bij m* k = t* pins k = (bij m*).symm t*.

source

theorem CatCrypt.Examples.MAC.bijMAC_forgery_prob (B : BijMACFamily) (m m_star : B.Message) (t_star : B.Tag) :

Crypto.prTrue (Crypto.SecurityDefs.EUF_CMA_Real B.toMACScheme m m_star t_star) Core.Heap.empty = 1 / ↑(Fintype.card B.Tag)

Optimal forgery probability. For a bijection-family MAC the single-query EUF-CMA game accepts a fixed forgery (m*, t*) with probability exactly 1 / |Tag|.

The real game samples a key k and returns verify k m* t* = (t* == bij m* k); prTrue_sample_pure_bool turns this into #{k | forgery verifies} / |Key|. The forgery verifies for exactly one k (bijMAC_forgery_filter), and |Key| = |Tag| because bij m* is an equivalence.

source

theorem CatCrypt.Examples.MAC.bijMAC_euf_cma_adv (B : BijMACFamily) (m m_star : B.Message) (t_star : B.Tag) :

Crypto.SecurityDefs.EUF_CMA_Adv B.toMACScheme m m_star t_star Core.SPComp.pure = 1 / ↑(Fintype.card B.Tag)

Forgery probability through the core EUF_CMA_Adv game. With the identity forger (no post-processing of the verification bit), the bijection-family MAC's EUF-CMA advantage is exactly 1 / |Tag|.

Example: the XOR MAC over `Bool` #

mac k m = k ⊕ m is the bijection family m ↦ boolXorBij m; it is the MAC counterpart of the one-time pad and the XOR PRF, and attains the optimal 1-bit forgery probability 1 / 2.

source

def CatCrypt.Examples.MAC.boolXorMAC :

BijMACFamily

The XOR MAC over Bool as a bijection family: bij m = boolXorBij m.

Equations