Bijection-Family PRF: Perfect Security #
A pseudorandom function built from a bijection family has perfect security. Following Rosulek, The Joy of Cryptography, §6 (pseudorandom functions).
For each input x, if the map k ↦ eval k x is a bijection from keys to
outputs, then over a uniform key the PRF output eval k x is itself uniform on
the output space and independent of x. Hence the PRF real game (keyed
evaluation) and the PRF ideal game (a fresh uniform output) are perfectly
indistinguishable: the PRF advantage of every adversary is exactly 0.
Overview #
This mirrors the one-time-pad argument (CatCrypt.Examples.OTP): the security
proof is the bijection-coupling technique. liftR_uniform_bij couples the
uniform key with the uniform output through the bijection bij x : Key ≃ Output;
liftR_bind/liftR_pure push the coupling through the sample-then-pure
structure of the games; and PRF_Adv_zero_of_rHoare collapses the advantage to
0.
Main definitions #
BijPRFFamily— a family of key→output bijections indexed by input.BijPRFFamily.toPRFScheme— the corePRFSchemeit induces (eval k x = bij x k).
Main results #
bijPRF_coupling— the real and ideal PRF games couple witheqPost.bijPRF_perfect— a bijection-family PRF has perfect PRF security:PRF_Adv B.toPRFScheme x A = 0for every inputxand adversaryA.
References #
- [Rosulek, The Joy of Cryptography, §6 (pseudorandom functions)]
Bijection-Family PRF #
A PRF given by a family of bijections bij x : Key ≃ Output, one per input.
For a uniform key, bij x maps the uniform key distribution onto the uniform
output distribution, which is the source of perfect security.
- Key : Type
Key type
- Input : Type
Input (domain) type
- Output : Type
Output (range) type
For each input, a bijection from keys to outputs
Instances For
The core PRFScheme induced by a bijection family: eval k x = bij x k.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Perfect PRF Security #
Coupling: for a bijection-family PRF the real and ideal games are equidistributed.
Over a uniform key k, the real game returns bij x k while the ideal game
returns a fresh uniform output r; liftR_uniform_bij (B.bij x) couples them so
that bij x k = r, so the two games agree pointwise.
A bijection-family PRF has perfect PRF security: every adversary has PRF
advantage exactly 0.
Example: the XOR PRF over Bool #
F(k, x) = k ⊕ x is the bijection family x ↦ boolXorBij x; it is the PRF
counterpart of the one-time pad and inherits perfect security.
The XOR PRF has perfect PRF security.
Cascade PRF: the computational bound #
The bijection-family result above is perfect (ε = 0). The computational
cascade bound follows. For the double-encryption construction
`cascade(k₁, k₂, x) = F(k₂, F(k₁, x))`
the PRF advantage is bounded by
`Adv ≤ 2·ε_prf + q(q-1)/(2N)`,
a reduction to the base PRF's security (ε_prf) plus the PRF/PRP switching
(birthday) term. The three game hops are the Bellare–Rogaway triple-encryption
ladder:
| Step | Transition | Bound |
|---|---|---|
| 0→1 | inner F(k₁,·) → random function | ε_prf (PRF assumption) |
| 1→2 | random function → random permutation | q(q-1)/(2N) (switching) |
| 2→3 | outer F(k₂,·) → random function | ε_prf (PRF assumption) |
The hop bounds are the cryptographic hypotheses (a PRFAssumption on the base
function, and the SwitchingLemma for the middle step); the theorem composes
them into the total bound by the advantage triangle inequality.
Birthday collision term q(q-1)/(2N), the cost of the PRF→PRP switch.
Instances For
Cascade PRF computational bound (the headline).
For any 4-game hybrid sequence G realising the cascade ladder, if the three
hops are bounded by ε_prf, the birthday term, and ε_prf respectively, then
`Adv(G₀, G₃) ≤ 2·ε_prf + q(q-1)/(2N)`.
The hop hypotheses h01/h23 are the base-PRF security assumption (see
cascade_prf_bound_of_assumption) and h12 is the PRF/PRP switching bound
(CatCrypt.Crypto.SwitchingLemma). The composition is the advantage triangle
inequality.
Cascade PRF bound from a base-PRF security assumption.
If the inner and outer single-query components each satisfy a PRFAssumption
(with Hout.ε ≤ Hin.ε), and the outer cascade hops are bounded by the
corresponding component PRF advantages (h01, h23 — the reduction's
soundness) with the middle hop bounded by the switching term, then the cascade
advantage is at most 2·Hin.ε + q(q-1)/(2N).
Perfect cascade corollary. When the base PRF is information-theoretically
secure (ε_prf = 0) and there is no collision opportunity (q ≤ 1, so the
birthday term is 0), the cascade advantage is exactly 0.
Tactic showcase: discharging a cascade hop with bind_vcgen #
For a bijection-family base function each cascade hop is perfectly
indistinguishable — its advantage is 0. We discharge such a hop by proving the
two single-query games are literally the same SPComp distribution, using the
bind_vcgen run-to-completion tactic: it normalizes the monad structure and, via
the supplied change-of-variables bijection B.bij x, collapses sample k; return bij(x,k) to a fresh uniform sample. This is the ε = 0 exact-coupling case that
feeds cascade_prf_bound with ε_prf = 0.
The real and ideal single-query PRF games for a bijection family are the
same SPComp computation. Proved by bind_vcgen using (B.bij x): the
change-of-variables through the bijection rewrites the keyed evaluation into a
plain uniform sample.
A bijection-family PRF has PRF advantage 0, re-proved through the
bind_vcgen game-equality bijPRF_game_eq (an alternative to the relational
coupling of bijPRF_perfect). This is exactly a cascade hop with ε_prf = 0.
A bijection-family base function satisfies the PRFAssumption with ε = 0,
witnessed by the bind_vcgen proof bijPRF_adv_zero_via_vcgen.